Stefan pushed to branch master at Stefan / Typer
Commits: f832b339 by Simon Génier at 2021-10-28T10:43:05-04:00 Remove artisanal formatting functions in favour of printf.
- - - - - 7f6f32dd by Simon Génier at 2021-10-28T10:43:38-04:00 Printfify log functions.
- - - - - edf888bc by Simon Génier at 2021-10-28T11:00:18-04:00 Typer accepts subcommands (repl, compile, run) like git.
This will hopefully simplify option handling as I add more modes of operation with their own option for running Typer code in a Gambit subprocess.
- - - - -
21 changed files:
- debug_util.ml - src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - src/inverse_subst.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - tests/utest_lib.ml - typer.ml
Changes:
===================================== debug_util.ml ===================================== @@ -32,6 +32,8 @@
open Typerlib
+open Printf + (* Utilities *) open Util open Fmt @@ -249,10 +251,10 @@ let main () =
(if (get_p_option "lexp-merge-debug") then( List.iter (fun ((_l, s), lxp, ltp) -> - lalign_print_string (maybename s) 20; + printf "%-20s" (maybename s); lexp_print ltp; print_string "\n";
- lalign_print_string (maybename s) 20; + printf "%-20s" (maybename s); lexp_print lxp; print_string "\n";
) flexps));
===================================== src/REPL.ml ===================================== @@ -36,7 +36,8 @@ this program. If not, see http://www.gnu.org/licenses/. *) * * -------------------------------------------------------------------------- *)
-open Backend +open Printf + open Debruijn open Eval open Fmt @@ -50,20 +51,9 @@ module OL = Opslexp module EL = Elexp
let print_input_line i = - print_string " In["; - ralign_print_int i 2; - print_string "] >> " - -let error = Log.log_error ~section:"REPL" + printf " In[%02d] >> " i
-let print_and_clear_log () = - if (not Log.typer_log_config.Log.print_at_log) then - Log.print_and_clear_log () - -let handle_stopped_compilation msg = - print_and_clear_log (); - print_string msg; print_newline (); - flush stdout +let error fmt = Log.log_error ~section:"REPL" fmt
(* Read stdin for input. Returns only when the last char is ';' * We can use '%' to prevent parsing @@ -112,7 +102,7 @@ let help_msg = Note that all declarations are pulled before expressions, i.e. an expression can refer to variable introduced by later declarations. *) let eval_interactive - (interactive : #interactive_backend) + (interactive : #Backend.interactive) (i : int) (ectx : elab_context) (input : string) @@ -149,59 +139,56 @@ let eval_interactive List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs;
List.iter interactive#process_decls ldecls; - print_and_clear_log (); + Log.print_log ();
let values = List.map interactive#eval_expr lexprs in List.iter (Eval.print_eval_result i) values; - print_and_clear_log (); + Log.print_log ();
ectx'
(* Specials commands %[command-name] [args] *) -let rec repl i (interactive : #interactive_backend) (ectx : elab_context) = - let ipt = try read_input i with End_of_file -> "%quit" in - let ectx = - match ipt with - (* Check special keywords *) - | "%quit" | "%q" -> exit 0 - | "%help" | "%h" -> (print_string help_msg; ectx) - | "%calltrace" | "%ct" -> (print_eval_trace None; ectx) - | "%typertrace" | "%tt" -> (print_typer_trace None; ectx) - | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table); ectx) - - (* command with arguments *) - | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( - match (str_split ipt ' ') with - | "%readfile"::args -> - let ectx = List.fold_left (Elab.eval_file interactive) ectx args in - print_and_clear_log (); - ectx - | "%who"::args | "%w"::args -> ( - let _ = match args with - | ["all"] -> interactive#dump_rte_ctx - | _ -> interactive#print_rte_ctx in - ectx) - | "%info"::args | "%i"::args -> ( - let _ = match args with - | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) - | _ -> print_lexp_ctx (ectx_to_lctx ectx) in - ectx) - - | cmd::_ -> - error (" "" ^ cmd ^ "" is not a correct repl command"); - ectx - | _ -> ectx) - - (* eval input *) - | _ -> - try eval_interactive interactive i ectx ipt with - | Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; ectx) - | Log.Internal_error msg -> - (handle_stopped_compilation ("Internal error: " ^ msg); - ectx) - | Log.User_error msg -> - (handle_stopped_compilation ("Fatal user error: " ^ msg); - ectx) - in - repl (i + 1) interactive ectx +let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) = + let ipt = try read_input i with End_of_file -> "%quit" in + let ectx = + match ipt with + (* Check special keywords *) + | "%quit" | "%q" -> exit 0 + | "%help" | "%h" -> (print_string help_msg; ectx) + | "%calltrace" | "%ct" -> (print_eval_trace None; ectx) + | "%typertrace" | "%tt" -> (print_typer_trace None; ectx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table); ectx) + + (* command with arguments *) + | _ when ipt.[0] = '%' && ipt.[1] != ' ' + -> (match (str_split ipt ' ') with + | "%readfile"::args + -> let ectx' = + List.fold_left (Elab.process_file interactive) ectx args + in + Log.print_log (); + ectx' + | "%who"::args | "%w"::args + -> let _ = match args with + | ["all"] -> interactive#dump_rte_ctx + | _ -> interactive#print_rte_ctx in + ectx + | "%info"::args | "%i"::args + -> let _ = match args with + | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) + | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + ectx + + | cmd::_ + -> error {|"%s" is not a correct REPL command|} cmd; + ectx + + | _ -> ectx) + + (* eval input *) + | _ + -> Log.handle_error + ~on_error:(Fun.const ectx) + (fun () -> eval_interactive interactive i ectx ipt) + in + repl (i + 1) interactive ectx
===================================== src/backend.ml ===================================== @@ -19,26 +19,22 @@ * with this program. If not, see http://www.gnu.org/licenses/. *)
(** A backend is a consumer of fully eleborated and checked lexps. This module - provides a superclass for all backends. *) + provides interfaces for (batch) compilers and interactive backends. *)
open Lexp
type value = Env.value_type
-class virtual backend = object - (* Processes (interpret or compile, depending on the backend) a block of - mutually recursive declarations. *) +class virtual t = object method virtual process_decls : ldecls -> unit - - method interactive : interactive_backend option = None end
-(* Backends may optionaly allow interactive evaluation, i.e. lexps can be - immediately evaluated as opposed compiled for evaluation later. *) -and virtual interactive_backend = object (self) - inherit backend +class virtual compiler = object + inherit t +end
- method! interactive = Some (self :> interactive_backend) +class virtual interactive = object + inherit t
method virtual eval_expr : lexp -> value
===================================== src/builtin.ml ===================================== @@ -61,9 +61,15 @@ open Lexp module DB = Debruijn module E = Env
-let log_raise_error ?loc msg = - Log.log_error ~section:"BUILT-IN" ?loc msg; - Log.internal_error msg +let log_raise_error ?print_action ?loc fmt = + Log.log_msg + (fun s -> raise (Log.Internal_error s)) + Log.Error + ?kind:None + ~section:"BUILT-IN" + ?print_action + ?loc + fmt
let predef_names = [ "cons"; (* FIXME: Should be used but isn't! *) @@ -85,7 +91,7 @@ let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) - with Not_found -> log_raise_error ("""^ name ^ "" was not predefined") + with Not_found -> log_raise_error {|"%s" was not predefined|} name
let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) @@ -116,9 +122,12 @@ let v2o_list v = match v with | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl | E.Vcons ((_, "nil"), []) -> List.rev acc - | _ -> log_raise_error ~loc:(E.value_location v) ( - "Failed to convert the " ^ E.value_name v ^ " with value :\n" - ^ E.value_string v ^ "\n to a list.") in + | _ -> + log_raise_error + ~loc:(E.value_location v) + "Failed to convert the %s with value:\n%s\n to a list." + (E.value_name v) (E.value_string v) + in v2o_list [] v
(* Map of lexp builtin elements accessible via (## <name>). *)
===================================== src/debruijn.ml ===================================== @@ -44,7 +44,8 @@ open Fmt
module S = Subst
-let fatal = Log.log_fatal ~section:"DEBRUIJN" +let fatal ?print_action ?loc fmt = + Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt
(* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. @@ -363,21 +364,18 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = then fun () -> (print_lexp_ctx ctx; print_newline ()) else fun () -> summarize_lctx ctx dbi in - let message = - "DeBruijn index " ^ string_of_int dbi - ^ " refers to wrong name. " - ^ "Expected: `" ^ ename - ^ "` got `" ^ name ^ "`" - in - fatal ~loc ~print_action message + fatal + ~loc ~print_action + ({|DeBruijn index %d refers to wrong name. |} + ^^ {|Expected: "%s" got "%s"|}) + dbi ename name | _ -> () in
ret with | Not_found - -> fatal ~loc ("DeBruijn index " - ^ string_of_int dbi ^ " of `" ^ maybename oename - ^ "` out of bounds!") + -> fatal + ~loc "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename)
let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in
===================================== src/debug.ml ===================================== @@ -31,6 +31,8 @@ * * --------------------------------------------------------------------------- *)
+open Printf + (* removes some warnings *) open Util open Fmt @@ -119,9 +121,7 @@ let debug_lexp_decls decls = List.iter (fun e -> let ((loc, _name), lxp, _ltp) = e in
- print_string " "; - lalign_print_string (lexp_name lxp) 15; - Printf.printf "[%s]" (Source.Location.to_string loc); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc);
let str = lexp_str_decls (!debug_ppctx) [e] in
@@ -136,10 +136,9 @@ let debug_lexp_decls decls = let str = List.flatten (List.map (fun g -> str_split g '\n') str) in
let str = match str with - | scd::tl -> - print_string " FILE: "; - lalign_print_string loc.file 25; - print_string (sep ^ scd); print_string "\n"; tl + | scd :: tl + -> printf " FILE: %-25s : %s\n" loc.file scd; + tl | _ -> [] in
List.iter (fun g ->
===================================== src/elab.ml ===================================== @@ -60,6 +60,8 @@ module Unif = Unification module OL = Opslexp module EL = Elexp
+open Printf + (* dummies *) let dloc = dummy_location
@@ -68,10 +70,14 @@ let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl"
-let fatal = Log.log_fatal ~section:"ELAB" -let error = Log.log_error ~section:"ELAB" -let warning = Log.log_warning ~section:"ELAB" -let info = Log.log_info ~section:"ELAB" +let fatal ?print_action ?loc fmt = + Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt +let error ?print_action ?loc fmt = + Log.log_error ~section:"ELAB" ?print_action ?loc fmt +let warning ?print_action ?loc fmt = + Log.log_warning ~section:"ELAB" ?print_action ?loc fmt +let info ?print_action ?loc fmt = + Log.log_info ~section:"ELAB" ?print_action ?loc fmt
let indent_line str = " > " ^ str @@ -84,8 +90,8 @@ let lexp_print_details lexp () = let value_print_details value () = print_details value_name value_string value
-let lexp_error loc lexp = - error ~loc ~print_action:(lexp_print_details lexp) +let lexp_error loc lexp fmt = + error ~loc ~print_action:(lexp_print_details lexp) fmt let lexp_fatal loc lexp = fatal ~loc ~print_action:(lexp_print_details lexp) let value_fatal loc value = @@ -127,31 +133,29 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in - match var with - | (l, None) -> lexp_error l ltp - ("`" ^ typestr ^ "` is not a proper type") - | (l, Some name) - -> lexp_error l ltp - ("Type of `" ^ name ^ "` is not a proper type: " - ^ typestr) + | _ + -> let tystr = lexp_string ltp ^ " : " ^ lexp_string lsort in + match var with + | (l, None) -> lexp_error l ltp {|"%s" is not a proper type|} tystr + | (l, Some name) + -> lexp_error l ltp {|Type of "%s" is not a proper type: %s|} name tystr
let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> match e with - | Log.Stop_Compilation _ -> raise e - | _ -> - info - ~print_action:(fun _ -> - print_lexp_ctx (ectx_to_lctx ctx); print_newline () - ) - ~loc:(lexp_location ltp) - ("Exception while checking type `" ^ (lexp_string ltp) ^ "`" - ^ (match var with - | (_, None) -> "" - | (_, Some name) - -> " of var `" ^ name ^ "`")); - raise e + | Log.Stop_compilation _ -> raise e + | _ + -> info + ~print_action:(fun _ -> + print_lexp_ctx (ectx_to_lctx ctx); print_newline () + ) + ~loc:(lexp_location ltp) + {|Exception while checking type "%s"%s|} + (lexp_string ltp) + (match var with + | (_, None) -> "" + | (_, Some name) -> " of var `" ^ name ^ "`"); + raise e
let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in @@ -159,7 +163,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
let ltype' = try OL.check lctx lxp with e -> match e with - | Log.Stop_Compilation _ -> raise e + | Log.Stop_compilation _ -> raise e | _ -> info ~print_action:(fun _ -> @@ -171,12 +175,15 @@ let elab_check_def (ctx : elab_context) var lxp ltype = "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e -> - info ~print_action:(lexp_print_details lxp) - ~loc - ("Exception while conversion-checking types: " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) + with + | e + -> info + ~print_action:(lexp_print_details lxp) + ~loc + "Exception while conversion-checking types: %s and %s" + (lexp_string ltype) + (lexp_string ltype'); + raise e) then elab_check_proper_type ctx ltype var else @@ -304,8 +311,7 @@ let elab_varref ctx (loc, name) if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" else "" in - sexp_error loc ("The variable: `" ^ name ^ - "` was not declared" ^ relateds); + sexp_error loc {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc)
(* Turn metavar into plain vars after generalization. @@ -597,8 +603,9 @@ and elab_special_form ctx f args ot = (* Special form. *) (get_special_form name) ctx loc args ot
- | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - sform_dummy_ret ctx loc + | _ + -> lexp_error loc f "Unknown special-form: %s" (lexp_string f); + sform_dummy_ret ctx loc
(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc oname t = @@ -642,12 +649,11 @@ and infer_type pexp ectx var = | (_::_) -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with - | (l, None) -> lexp_error l t - ("`" ^ typestr ^ "` is not a proper type") + | (l, None) + -> lexp_error l t {|"%s" is not a proper type|} typestr | (l, Some name) - -> lexp_error l t - ("Type of `" ^ name ^ "` is not a proper type: " - ^ typestr)) + -> lexp_error + l t {|Type of "%s" is not a proper type: %s|} name typestr) | [] -> ()); t
@@ -665,11 +671,10 @@ and unify_with_arrow ctx tloc lxp kind var aty let arrow = mkArrow (kind, var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) - -> lexp_error tloc lxp ("Types:\n " ^ lexp_string t1 - ^ "\n and:\n " - ^ lexp_string t2 - ^ "\n do not match!"); - (mkDummy_type ctx l, mkDummy_type nctx l) + -> lexp_error + tloc lxp {|Types:\n %s\n and:\n %s\n do not match!|} + (lexp_string t1) (lexp_string t2); + (mkDummy_type ctx l, mkDummy_type nctx l) | [] -> arg, body
and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = @@ -678,17 +683,20 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = and unify_or_error lctx lxp ?lxp_name expect actual = match Unif.unify expect actual lctx with | ((ck, _ctx, t1, t2)::_) - -> lexp_error (lexp_location lxp) lxp - ("Type mismatch" - ^ (match ck with | Unif.CKimpossible -> "" - | Unif.CKresidual -> " (residue)") - ^ "! Context expected:\n " ^ lexp_string expect ^ "\nbut " - ^ (Option.value ~default:"expression" lxp_name) ^ " has type:\n " - ^ lexp_string actual ^ "\ncan't unify:\n " - ^ lexp_string t1 - ^ "\nwith:\n " - ^ lexp_string t2); - assert (not (OL.conv_p lctx expect actual)) + -> lexp_error + (lexp_location lxp) lxp + ({|Type mismatch%s! Context expected:\n%s|} + ^^ {|\nbut %s has type:\n %s\n|} + ^^ {|can't unify:\n %s\nwith:\n %s|}) + (match ck with + | Unif.CKimpossible -> "" + | Unif.CKresidual -> " (residue)") + (lexp_string expect) + (Option.value ~default:"expression" lxp_name) + (lexp_string actual) + (lexp_string t1) + (lexp_string t2); + assert (not (OL.conv_p lctx expect actual)) | [] -> ()
(* This is a crucial function: take an expression `e` of type `inferred_t` @@ -710,10 +718,12 @@ and check_case rtype (loc, target, ppatterns) ctx =
let pat_string p = sexp_string (pexp_u_pat p) in
- let uniqueness_warn pat = - warning ~loc:(pexp_pat_location pat) - ("Pattern " ^ pat_string pat - ^ " is a duplicate. It will override previous pattern.") in + let uniqueness_warn pat = + warning + ~loc:(pexp_pat_location pat) + "Pattern %s is a duplicate. It will override a previous pattern." + (pat_string pat) + in
let check_uniqueness pat name map = if SMap.mem name map then uniqueness_warn pat in @@ -731,9 +741,9 @@ and check_case rtype (loc, target, ppatterns) ctx = let unify_ind expected actual = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) - -> lexp_error loc lctor - ("Expected pattern of type `" ^ lexp_string expected - ^ "` but got `" ^ lexp_string actual ^ "`") + -> lexp_error + loc lctor {|Expected pattern of type "%s", but got "%s"|} + (lexp_string expected) (lexp_string actual) | [] -> () in match !it_cs_as with | Some (it, cs, args) @@ -764,11 +774,12 @@ and check_case rtype (loc, target, ppatterns) ctx = match OL.lexp'_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); - constructors - | _ -> lexp_error (sexp_location target) tlxp - ("Can't `case` on objects of this type: " - ^ lexp_string tltp); - SMap.empty in + constructors + | _ + -> lexp_error + (sexp_location target) tlxp + {|Can't "case" on objects of type "%s"|} (lexp_string tltp); + SMap.empty in it_cs_as := Some (it, constructors, targs); (constructors, targs) in
@@ -818,15 +829,14 @@ and check_case rtype (loc, target, ppatterns) ctx = match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in - let (constructors, targs) = get_cs_as it' lctor in - let cargs - = try SMap.find cons_name constructors - with Not_found - -> lexp_error loc lctor - ("`" ^ (lexp_string it') - ^ "` does not have a `" - ^ cons_name ^ "` constructor"); - [] in + let (constructors, targs) = get_cs_as it' lctor in + let cargs = + try SMap.find cons_name constructors with + | Not_found + -> lexp_error + loc lctor {|"%s" does not a have a "%s" constructor|} + (lexp_string it') cons_name; + [] in
let subst = List.fold_left (fun s (_, t) -> S.cons t s) S.identity targs in @@ -839,11 +849,9 @@ and check_case rtype (loc, target, ppatterns) ctx = match (pargs, cargs) with | (_, []) when not (SMap.is_empty pe) -> let pending = SMap.bindings pe in - sexp_error loc - ("Explicit pattern args `" - ^ String.concat ", " (List.map (fun (l, _) -> l) - pending) - ^ "` have no matching fields"); + sexp_error + loc {|Explicit pattern args "%s" have no matching fields|} + (String.concat ", " (List.map fst pending)); make_nctx ctx s pargs cargs SMap.empty acc | [], [] -> ctx, List.rev acc | (_, _pat)::_, [] @@ -866,18 +874,19 @@ and check_case rtype (loc, target, ppatterns) ctx = ((ak, var)::acc) | ((Some (l, fname), var)::pargs, cargs) -> if SMap.mem fname pe then - sexp_error l ("Duplicate explicit field `" ^ fname ^ "`"); - make_nctx ctx s pargs cargs (SMap.add fname var pe) acc + sexp_error l {|Duplicate explicit field "%s"|} fname; + make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs -> let var = (loc, None) in - let nctx = ctx_extend ctx var Variable (mkSusp fty s) in - if ak = Anormal then - sexp_error loc - ("Missing pattern for normal field" - ^ (match fname with (_, Some n) -> " `" ^ n ^ "`" - | _ -> "")); - make_nctx nctx (ssink var s) pargs cargs pe - ((ak, var)::acc) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + if ak = Anormal then + sexp_error + loc {|Missing pattern for normal field%s|} + (match fname with + | (_, Some n) -> sprintf {| "%s"|} n + | _ -> ""); + make_nctx nctx (ssink var s) pargs cargs pe + ((ak, var)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx @@ -953,14 +962,14 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, Arrow _ -> if SMap.mem aname pending then - sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); - handle_fun_args largs sargs (SMap.add aname sarg pending) ltp + sexp_error l {|Duplicate explicit arg "%s"|} aname; + handle_fun_args largs sargs (SMap.add aname sarg pending) ltp
| (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ - -> sexp_error l - ("Explicit arg `" ^ aname ^ "` to non-function " - ^ "(type = " ^ (lexp_string ltp) ^ ")"); - handle_fun_args largs sargs pending ltp + -> sexp_error + l {|Explicit arg "%s" to non-function (type = %s)|} + aname (lexp_string ltp); + handle_fun_args largs sargs pending ltp
(* Aerasable *) | _, Arrow ((Aerasable | Aimplicit) as ak, (_l,v), arg_type, _, ret_type) @@ -976,16 +985,14 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (L.mkSusp ret_type (S.substitute larg)) | [], _ -> (if not (SMap.is_empty pending) then - let pending = SMap.bindings pending in - let loc = match pending with - | (_, sarg)::_ -> sexp_location sarg - | _ -> assert false in - lexp_error loc func - ("Explicit actual args `" - ^ String.concat ", " (List.map (fun (l, _) -> l) - pending) - ^ "` have no matching formal args")); - largs, ltp + let pending = SMap.bindings pending in + let loc = match pending with + | (_, sarg)::_ -> sexp_location sarg + | _ -> assert false in + lexp_error + loc func {|Explicit actual args "%s" have no matching formal args|} + (String.concat ", " (List.map fst pending))); + largs, ltp
| sarg :: sargs, _ -> let (arg_type, ret_type) = match lexp_lexp' ltp' with @@ -1071,9 +1078,9 @@ and lexp_eval ectx e = let rctx = EV.from_ectx ectx in
if not (EV.closed_p rctx (OL.fv e)) then - lexp_error (lexp_location e) e - ("Expression `" ^ lexp_string e ^ "` is not closed: " - ^ track_fv rctx (ectx_to_lctx ectx) e); + lexp_error + (lexp_location e) e {|Expression "%s" is not closed: %s|} + (lexp_string e) (track_fv rctx (ectx_to_lctx ectx) e);
try EV.eval ee rctx with exc -> @@ -1112,13 +1119,13 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = let ret = lexp_expand_macro loc lxp sargs ctx None in match ret with | Vcommand cmd - -> (match (cmd ()) with - | Vsexp (sexp) -> sexp - | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) - | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO") + -> (match cmd () with + | Vsexp (sexp) -> sexp + | _ -> fatal ~loc {|Macro "%s" should return an IO sexp|} mname) + | _ -> fatal ~loc {|Macro "%s" should return an IO|} mname
with _e -> - fatal ~loc ("Macro `" ^ mname ^ "` not found") + fatal ~loc {|Macro "%s" not found|} mname
(* Elaborate a bunch of mutually-recursive definitions. * FIXME: Currently, we never apply generalization to recursive definitions, @@ -1230,12 +1237,13 @@ and lexp_decls_1 lexp_decls_1 (List.append prepend_sdecls sdecls) toks nctx pending_decls pending_defs in match sdecl with - | None -> (if not (SMap.is_empty pending_decls) then - let (s, loc) = SMap.choose pending_decls in - error ~loc ("Variable `" ^ s ^ "` declared but not defined!") - else - assert (pending_defs == [])); - [], [], [], nctx + | None + -> if not (SMap.is_empty pending_decls) then + let (s, loc) = SMap.choose pending_decls in + error ~loc {|Variable "%s" declared but not defined!|} s + else + assert (pending_defs == []); + [], [], [], nctx
| Some (Symbol (_, "")) -> recur [] nctx pending_decls pending_defs @@ -1258,24 +1266,26 @@ and lexp_decls_1 (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with | (_::_) - -> lexp_error loc ltp - ("New type annotation `" - ^ lexp_string ltp ^ "` incompatible with previous `" - ^ lexp_string pt ^ "`") + -> lexp_error + loc ltp + {|New type annotation "%s" incompatible with previous "%s"|} + (lexp_string ltp) (lexp_string pt) | [] -> () in recur [] nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then - (error ~loc ("Variable `" ^ vname ^ "` already defined!"); + (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs - | _ -> error ~loc ("Invalid type declaration syntax : `" ^ - (sexp_string thesexp) ^ "`"); - recur [] nctx pending_decls pending_defs) + | _ + -> error + ~loc {|Invalid type declaration syntax : "%s"|} + (sexp_string thesexp); + recur [] nctx pending_decls pending_defs)
- | Some (Node (Symbol (l, "_=_") as head, args) as thesexp) + | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol ((l, vname)); sexp] @@ -1290,10 +1300,10 @@ and lexp_decls_1 [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, ctx_define nctx var lexp ltp
- | [Symbol (l, vname); sexp] + | [Symbol (loc, vname); sexp] -> if SMap.mem vname pending_decls then let pending_decls = SMap.remove vname pending_decls in - let pending_defs = (((l, vname), sexp) :: pending_defs) in + let pending_defs = (((loc, vname), sexp) :: pending_defs) in if SMap.is_empty pending_decls then let nctx = ectx_new_scope nctx in let decls, nctx = lexp_check_decls ectx nctx pending_defs in @@ -1302,7 +1312,7 @@ and lexp_decls_1 recur [] nctx pending_decls pending_defs
else - (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); + (error ~loc {|"%s" defined but not declared!|} vname; recur [] nctx pending_decls pending_defs)
| [Node (Symbol s, args) as d; body] @@ -1313,9 +1323,10 @@ and lexp_decls_1 [sexp_u_list args; body])])] nctx pending_decls pending_defs
- | _ -> error ~loc:l ("Invalid definition syntax : `" ^ - (sexp_string thesexp) ^ "`"); - recur [] nctx pending_decls pending_defs) + | _ + -> error + ~loc {|Invalid definition syntax : "%s"|} (sexp_string thesexp); + recur [] nctx pending_decls pending_defs)
| Some (Node (Symbol (l, "define-operator"), args)) (* FIXME: Move this to a "special form"! *) @@ -1398,11 +1409,11 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp') in - if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc ("Unknown built-in `" ^ name ^ "`"); - BI.add_builtin_cst name bi; - (bi, Checked) + let bi = mkBuiltin ((loc, name), ltp') in + if not (SMap.mem name (!EV.builtin_functions)) then + sexp_error loc {|Unknown built-in "%s"|} name; + BI.add_builtin_cst name bi; + (bi, Checked) | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc)
@@ -1534,14 +1545,16 @@ let sform_identifier ctx loc sargs ot = | [Symbol (l,name)] when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then - let name = string_sub name 2 (String.length name) in - try let (e,t) = SMap.find name (! BI.lmap) in - (e, Inferred t) - with Not_found - -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); - sform_dummy_ret ctx loc - else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); - sform_dummy_ret ctx loc) + let name = string_sub name 2 (String.length name) in + try let (e, t) = SMap.find name (! BI.lmap) in + (e, Inferred t) + with + | Not_found + -> sexp_error l {|Unknown builtin "%s"|} name; + sform_dummy_ret ctx loc + else + (sexp_error l {|Invalid special identifier "%s"|} name; + sform_dummy_ret ctx loc)
| [Symbol (loc, name)] when String.length name >= 1 && String.get name 0 = '?' @@ -1568,7 +1581,7 @@ let sform_identifier ctx loc sargs ot = means that `subst` is not the right substitution for the metavar! *) fatal ~loc ("Bug in the elaboration of a metavar" - ^ " repeated at a different scope level!") + ^^ " repeated at a different scope level!") | MVal _ -> (* FIXME: We face the same problem as above, but here, the situation is worse, we don't even know the scope @@ -1668,11 +1681,14 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind arg olt1 in mklam lt1 (Some lt2))
- | _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->" - | Aimplicit -> "=>" - | Aerasable -> "≡>") - ^"_ takes two arguments"); - sform_dummy_ret ctx loc + | _ + -> sexp_error + loc "##lambda_%s_ takes two arguments" + (match kind with + | Anormal -> "->" + | Aimplicit -> "=>" + | Aerasable -> "≡>"); + sform_dummy_ret ctx loc
let rec sform_case ctx loc sargs ot = match sargs with | [Node (Symbol (_, "_|_"), se :: scases)] @@ -1719,7 +1735,7 @@ let rec infer_level ctx se : lexp = | Node (Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in - (sexp_error l ("Unrecognized TypeLevel: " ^ sexp_string se); + (sexp_error l "Unrecognized TypeLevel: %s" (sexp_string se); newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) l)
(* Actually `Type_` could also be defined as a plain constant @@ -1780,8 +1796,8 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc - ("Could not load `" ^ file_name ^ "`: file not found."); [] in + -> error ~loc {|Could not load "%s": file not found.|} file_name; [] + in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx in elctx in @@ -1906,7 +1922,8 @@ let default_ectx ectx with e -> error "Compilation stopped in default context"; - Log.print_and_clear_log (); + Log.print_log (); + Log.clear_log (); raise e
let default_rctx = EV.from_ectx default_ectx @@ -1948,8 +1965,8 @@ let eval_decl_str str ectx rctx = let _, elxps = List.fold_left_map (OL.clean_decls) lctx lxps in (EV.eval_decls_toplevel elxps rctx), ectx'
-let eval_file - (backend : #Backend.backend) +let process_file + (backend : #Backend.t) (ectx : elab_context) (file_name : string) : elab_context = @@ -1963,5 +1980,5 @@ let eval_file ectx' with | Sys_error _ - -> (error (Printf.sprintf {|file %s does not exist.|} file_name); + -> (error {|file %s does not exist.|} file_name; ectx)
===================================== src/env.ml ===================================== @@ -30,6 +30,8 @@ * * --------------------------------------------------------------------------- *)
+open Printf + open Fmt (* make_title, table util *)
open Sexp @@ -42,8 +44,10 @@ module DB = Debruijn
let dloc = Util.dummy_location
-let fatal = Log.log_fatal ~section:"ENV" -let warning = Log.log_warning ~section:"ENV" +let fatal ?print_action ?loc fmt = + Log.log_fatal ~section:"ENV" ?print_action ?loc fmt +let warning ?print_action ?loc fmt = + Log.log_warning ~section:"ENV" ?print_action ?loc fmt
let str_idx idx = "[" ^ (string_of_int idx) ^ "]"
@@ -80,12 +84,16 @@ let rec value_equal a b = | Vin (c1), Vin (c2) -> c1 = c2 | Vout (_c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 - | Vundefined, _ | _, Vundefined -> warning "Vundefined"; false - | Vtype _e1, Vtype _e2 -> warning "Vtype"; false + | Vundefined, _ | _, Vundefined + -> warning "Vundefined"; + false + | Vtype _e1, Vtype _e2 + -> warning "Vtype"; + false
| Closure (s1, _b1, _ctx1), Closure (s2, _b2, _ctx2) -> warning "Closure"; - if (s1 != s2) then false else true + if s1 != s2 then false else true
| Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) -> if not (ct1 = ct2) then false else @@ -175,9 +183,7 @@ let print_myers_list l print_fun start = print_string (make_sep '-');
for i = start to n do - print_string " | "; - ralign_print_int (n - i) 5; - print_string " | "; + printf " | %5d | " (n -i); print_fun (M.nth (n - i) l); done; print_string (make_sep '=') @@ -189,7 +195,7 @@ let print_rte_ctx_n (ctx: runtime_env) start = let g = !vref in let _ = match n with - | (_, Some m) -> lalign_print_string m 12; print_string " | " + | (_, Some m) -> Printf.printf "%-12s | " m | _ -> print_string (make_line ' ' 12); print_string " | " in
value_print g; print_string "\n") start @@ -204,23 +210,22 @@ let dump_rte_ctx ctx =
let get_rte_variable (name: vname) (idx: int) (ctx: runtime_env): value_type = - try ( - let (defname, ref_cell) = (M.nth idx ctx) in - let x = !ref_cell in + try + let (defname, ref_cell) = (M.nth idx ctx) in + let x = !ref_cell in match (defname, name) with - | ((_, Some n1), (_, Some n2)) -> ( - if n1 = n2 then - x - else ( - fatal ~print_action:(fun () -> dump_rte_ctx ctx) - ("Variable lookup failure. Expected: "" ^ - n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """))) - - | _ -> x) - with Not_found -> - let n = match name with (_, Some n) -> n | _ -> "" in - fatal ("Variable lookup failure. Var: "" ^ - n ^ "" idx: " ^ (str_idx idx)) + | ((_, Some n1), (_, Some n2)) + -> if n1 = n2 + then x + else + fatal + ~print_action:(fun () -> dump_rte_ctx ctx) + {|Variable lookup failure. Expected "%s[%d]" got "%s"|} n2 idx n1 + | _ -> x + with + | Not_found + -> let n = match name with (_, Some n) -> n | _ -> "" in + fatal {|Variable lookup failure. Var: "%s" idx: %d|} n idx
let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) : runtime_env = @@ -228,15 +233,14 @@ let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) M.cons (name, valcell) ctx
let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = - let (n, ref_cell) = (M.nth idx ctx) in + let (n, ref_cell) = (M.nth idx ctx) in
- (match (n, name) with - | ((_, Some n1), (_, Some n2)) - -> if (n1 != n2) then - fatal ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) - | _ -> ()); + (match (n, name) with + | ((_, Some n1), (_, Some n2)) when n1 != n2 + -> fatal {|Variable names must match: "%s" vs "%s"|} n1 n2 + | _ -> ());
- ref_cell := v + ref_cell := v
(* Select the n first variable present in the env *) let nfirst_rte_var n ctx = @@ -246,4 +250,3 @@ let nfirst_rte_var n ctx = else List.rev acc in loop 0 [] -
===================================== src/eval.ml ===================================== @@ -31,7 +31,6 @@ * --------------------------------------------------------------------------- *)
open Util -open Fmt
open Sexp (* open Pexp *) (* Arg_kind *) @@ -56,11 +55,6 @@ let global_eval_trace = ref ([], []) let global_eval_ctx = ref make_runtime_ctx (* let eval_max_recursion_depth = ref 23000 *)
-(* eval error are always fatal *) -let error loc ?print_action msg = - Log.log_error ~section:"EVAL" ~loc:loc ?print_action msg; - Log.internal_error msg - type builtin_function = location -> eval_debug_info -> value_type list -> value_type
@@ -86,8 +80,22 @@ let rec_depth trace = let (_a, b) = trace in List.length b
-let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg -let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg +let fatal loc ?print_action fmt = + Log.log_fatal ~section:"EVAL" ~loc ?print_action fmt + +(* eval error are always fatal *) +let error loc ?print_action fmt = + Log.log_msg + (fun s -> raise (Log.Internal_error s)) + Log.Error + ?kind:None + ~section:"EVAL" + ?print_action + ~loc + fmt + +let warning loc ?print_action fmt = + Log.log_warning ~section:"EVAL" ~loc ?print_action fmt
(* Print a message that look like this: * @@ -98,29 +106,25 @@ let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg * *)
-let debug_messages error_type loc message messages = - let msg = List.fold_left (fun str msg -> - str ^ "\n > " ^ msg) message messages in - error_type loc (msg ^ "\n") - let root_string () = let a, _ = !global_eval_trace in match List.rev a with | [] -> "" | e::_ -> elexp_string e
-let debug_message error_type type_name type_string loc expr message = - debug_messages error_type loc - message [ - (type_name expr) ^ ": " ^ (type_string expr); - "Root: " ^ (root_string ()); - ] - -(* Print value name followed by the value in itself, finally throw an exception *) -let value_fatal = debug_message fatal value_name value_string -let value_error = debug_message (error ?print_action:None) value_name value_string -let elexp_fatal = debug_message fatal elexp_name elexp_string +let trace_value (value : value_type) : string = + sprintf + "\t> %s : %s\n\t> Root: %s\n" + (value_name value) + (value_string value) + (root_string ())
+let trace_elexp (elexp : elexp) : string = + sprintf + "\t> %s : %s\n\t> Root: %s\n" + (elexp_name elexp) + (elexp_string elexp) + (root_string ())
(* FIXME: We're not using predef here. This will break if we change * the definition of `Bool` in builtins.typer. *) @@ -148,7 +152,7 @@ let add_binary_iop name f = let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint (v); Vint (w)] -> Vint (f v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in + | _ -> error loc {|"%s" expects 2 Int arguments|} name in add_builtin_function name f 2
let add_binary_iop_with_loc name f = @@ -156,7 +160,7 @@ let add_binary_iop_with_loc name f = let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint (v); Vint (w)] -> Vint (f loc v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in + | _ -> error loc {|"%s" expects 2 Int arguments|} name in add_builtin_function name f 2
let add_with_overflow loc a b = @@ -188,17 +192,17 @@ let div_with_overflow loc a b =
let lsl_with_shift_check loc a b = if b < 0 || b > Sys.int_size - then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.lsl`") + then error loc {|Invalid shift value %d in "Int.lsl"|} b else a lsl b
let lsr_with_shift_check loc a b = if b < 0 || b > Sys.int_size - then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.lsr`") + then error loc {|Invalid shift value %d in "Int.lsr"|} b else a lsr b
let asr_with_shift_check loc a b = if b < 0 || b > Sys.int_size - then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.asr`") + then error loc {|Invalid shift value %d in "Int.ast"|} b else a asr b
let _ = add_binary_iop_with_loc "+" add_with_overflow; @@ -220,7 +224,7 @@ let add_binary_bool_iop name f = let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint v; Vint w] -> o2v_bool (f v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in + | _ -> error loc {|"%s" expects 2 Int arguments|} name in add_builtin_function name f 2
let _ = add_binary_bool_iop "<" (<); @@ -234,7 +238,7 @@ let _ = let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vint v] -> Vint(lnot v) - | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument") in + | _ -> error loc {|"%s" expects 1 Int arguments|} name in add_builtin_function name f 1
(* True integers (aka Z). *) @@ -244,7 +248,7 @@ let add_binary_biop name f = let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vinteger v; Vinteger w] -> Vinteger (f v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in + | _ -> error loc {|"%s" expects 2 Integer arguments|} name in add_builtin_function name f 2
let _ = add_binary_biop "+" BI.add; @@ -257,7 +261,7 @@ let add_binary_bool_biop name f = let f loc (_depth : eval_debug_info) (args_val: value_type list) = match args_val with | [Vinteger v; Vinteger w] -> o2v_bool (f v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in + | _ -> error loc {|"%s" expects 2 Integer arguments|} name in add_builtin_function name f 2
let _ = add_binary_bool_biop "<" BI.lt; @@ -271,27 +275,26 @@ let _ = add_binary_bool_biop "<" BI.lt; (fun loc (_depth : eval_debug_info) (args_val: value_type list) -> match args_val with | [Vint v] -> Vinteger (BI.of_int v) - | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument")) + | _ -> error loc {|"%s" expects 1 Int argument|} name) 1; let name = "Integer->Int" in add_builtin_function name (fun loc (_depth : eval_debug_info) (args_val: value_type list) -> match args_val with - | [Vinteger v] -> - (try Vint (BI.to_int v) with - | Z.Overflow -> error loc ("Overflow in `" ^ name ^ "`")) - | _ -> error loc ("`" ^ name ^ "` expects 1 Integer argument")) + | [Vinteger v] + -> (try Vint (BI.to_int v) with + | Z.Overflow -> error loc {|Overflow in "%s"|} name) + | _ -> error loc {|"%s" expects 1 Integer argument|} name) 1
(* Floating point numers. *)
let add_binary_fop name f = let name = "Float." ^ name in - let f loc (_depth : eval_debug_info) (args_val: value_type list) = - match args_val with + let f loc (_depth : eval_debug_info) = function | [Vfloat v; Vfloat w] -> Vfloat (f v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Float arguments") in + | _ -> error loc {|"%s" expects 2 Float arguments|} name in add_builtin_function name f 2
let _ = add_binary_fop "+" (+.); @@ -301,10 +304,9 @@ let _ = add_binary_fop "+" (+.);
let add_binary_bool_fop name f = let name = "Float." ^ name in - let f loc (_depth : eval_debug_info) (args_val: value_type list) = - match args_val with + let f loc (_depth : eval_debug_info) = function | [Vfloat v; Vfloat w] -> o2v_bool (f v w) - | _ -> error loc ("`" ^ name ^ "` expects 2 Float arguments") in + | _ -> error loc {|"%s" expects 2 Float arguments|} name in add_builtin_function name f 2
let _ = add_binary_bool_fop "<" (<); @@ -314,10 +316,9 @@ let _ = add_binary_bool_fop "<" (<); add_binary_bool_fop "<=" (<=)
let _ = let name = "Float." ^ "trunc" in - let f loc (_depth : eval_debug_info) (args_val : value_type list) = - match args_val with + let f loc (_depth : eval_debug_info) = function | [Vfloat v] -> Vfloat ( snd (modf v) ) - | _ -> error loc ("`" ^ name ^ "` expects 1 Float argument") in + | _ -> error loc {|"%s" expects 1 Float argument|} name in add_builtin_function name f 1
let make_symbol loc _depth args_val = match args_val with @@ -325,16 +326,17 @@ let make_symbol loc _depth args_val = match args_val with | _ -> error loc "Sexp.symbol expects one string as argument"
let make_node loc _depth args_val = match args_val with - | [Vsexp (op); lst] -> - let args = v2o_list lst in - - let s = List.map (fun g -> match g with - | Vsexp(sxp) -> sxp - | _ -> - (* print_rte_ctx ctx; *) - value_error loc g "Sexp.node expects `List Sexp` second as arguments") args in - - Vsexp (Node (op, s)) + | [Vsexp (op); lst] + -> let args = v2o_list lst in + let unwrap_sexp = function + | Vsexp (sexp) -> sexp + | v + -> error + loc + {|Sexp.node expects "List Sexp" second as arguments\n%s|} + (trace_value v) + in + Vsexp (Node (op, List.map unwrap_sexp args))
| _ -> error loc "Sexp.node expects a `Sexp` and a `List Sexp`"
@@ -483,11 +485,14 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type)
and eval_var ctx lxp v = - let (name, idx) = v in - try get_rte_variable name idx ctx - with _e -> - elexp_fatal (fst name) lxp - ("Variable: " ^ L.maybename (snd name) ^ (str_idx idx) ^ " was not found ") + let (loc, name as vname, idx) = v in + try get_rte_variable vname idx ctx + with + | _e + -> Log.log_fatal + ~loc + "Variable: %s%d was not found\n%s" + (L.maybename name) idx (trace_elexp lxp)
(* unef: unevaluated function (to make the trace readable) *) and eval_call loc unef i f args = @@ -538,18 +543,18 @@ and eval_call loc unef i f args = buildctx args Myers.nil)
with - | Not_found -> - error loc ("Requested Built-in `" ^ name ^ "` does not exist") - | e -> - warning loc ("Exception thrown from primitive `" ^ name ^"`"); - raise e) + | Not_found + -> error loc {|Requested Built-in "%s" does not exist|} name + | e + -> warning loc {|Exception thrown from primitive "%s"|} name; + raise e)
| Vtype e, _ (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1))])) - | _ -> value_fatal loc f "Trying to call a non-function!" + | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f)
and eval_case ctx i loc target pat dflt = (* Eval target *) @@ -557,9 +562,12 @@ and eval_case ctx i loc target pat dflt =
(* extract constructor name and arguments *) let ctor_name, args = match v with - | Vcons((_, cname), args) -> cname, args - | _ -> value_error loc v ("Target `" ^ elexp_string target - ^ "` is not a Constructor") in + | Vcons((_, cname), args) -> cname, args + | _ + -> error + loc {|Target "%s" is not a Constructor\n%s|} + (elexp_string target) (trace_value v) + in
(* Get working pattern *) try let (_, pat_args, exp) = SMap.find ctor_name pat in @@ -625,7 +633,11 @@ and sexp_dispatch loc depth args =
let sxp = match sxp with | Vsexp(sxp) -> sxp - | _ -> value_fatal loc sxp "sexp_dispatch expects a Sexp as 1st arg" in + | _ + -> fatal + loc + "sexp_dispatch expects a Sexp as 1st arg\n%s" (trace_value sxp) + in
match sxp with | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] @@ -642,10 +654,9 @@ and sexp_dispatch loc depth args =
(* -------------------------------------------------------------------------- *) and print_eval_result i lxp = - print_string " Out["; - ralign_print_int i 2; - print_string "] >> "; - value_print lxp; print_string "\n"; + Printf.printf " Out[%02d] >> " i; + value_print lxp; + print_string "\n";
and print_typer_trace' trace =
@@ -939,7 +950,7 @@ let test_fatal loc _depth args_val = match args_val with Vcommand (fun () -> Log.print_entry (Log.mkEntry Log.Fatal ~kind:"(Unit test fatal)" ~loc ~section msg); - Log.user_error msg + Log.user_error "%s" msg ) | _ -> error loc "Test.fatal takes two String as argument"
@@ -1178,7 +1189,7 @@ let from_ectx (ctx: elab_context): runtime_env = from_lctx (ectx_to_lctx ctx)
class ast_interpreter lctx = object - inherit Backend.interactive_backend + inherit Backend.interactive
val mutable rctx = from_lctx lctx val mutable lctx = lctx
===================================== src/fmt.ml ===================================== @@ -30,67 +30,9 @@ * * ---------------------------------------------------------------------------*)
-(* Compute the number of character needed to print an integer*) -let str_size_int v = - (int_of_float (log10 (float v))) + 1 - (* print n char 'c' *) let make_line c n = String.make n c
-(* Big numbers are replaced by #### *) -let cut_int (_v:int) (_start:int) (_len:int): int = 0 - -(* RALIGN - * ----------------------- *) -let ralign_generic get_size elem_string cut_elem elem col = - let n = get_size elem in - if n > col then elem_string (cut_elem elem 0 col) - else (make_line ' ' (col - n)) ^ (elem_string elem) - -let ralign_string = - ralign_generic String.length (fun s -> s) String.sub - -let ralign_int = - ralign_generic str_size_int string_of_int cut_int - -let ralign_print_int i c = print_string (ralign_int i c) -let ralign_print_string s c = print_string (ralign_string s c) - -(* LALIGN - * ----------------------- *) -let lalign_generic get_size elem_string cut_elem elem col = - let n = get_size elem in - if n > col then elem_string (cut_elem elem 0 col) - else (elem_string elem) ^ (make_line ' ' (col - n)) - -let lalign_string = - lalign_generic String.length (fun s -> s) String.sub - -let lalign_int = - lalign_generic str_size_int string_of_int cut_int - -let lalign_print_int i c = print_string (lalign_int i c) -let lalign_print_string s c = print_string (lalign_string s c) - -(* CALIGN - * ----------------------- *) -let calign_generic get_size elem_string cut_elem elem col = - let n = get_size elem in - let p = n mod 2 in - let sep_n = (col - n) / 2 in - - if n > col then elem_string (cut_elem elem 0 col) - else (make_line ' ' sep_n) ^ (elem_string elem) ^ (make_line ' ' (sep_n + p)) - -let calign_string = - calign_generic String.length (fun s -> s) String.sub - -let calign_int = - calign_generic str_size_int string_of_int cut_int - -let calign_print_int i c = print_string (calign_int i c) -let calign_print_string s c = print_string (calign_string s c) - (* Table Printing helper *) let make_title title = let title_n = String.length title in @@ -100,18 +42,17 @@ let make_title title = let rsep = (make_line '=' (sep_n + p)) in (" " ^ lsep ^ title ^ rsep ^ "\n")
-let make_rheader (head: (((char* int) option * string) list)) = - print_string " | "; - - List.iter (fun (o, name) -> - let _ = match o with - | Some ('r', size) -> ralign_print_string name size - | Some ('l', size) -> lalign_print_string name size - | _ -> print_string name in - print_string " | ") - head; - - print_string "\n" +let make_rheader (head: ((char * int) option * string) list) = + print_string " | "; + let print_header (o, name) = + (match o with + | Some ('r', size) -> Printf.printf "%*s" size name + | Some ('l', size) -> Printf.printf "%-*s" size name + | _ -> print_string name); + print_string " | " + in + List.iter print_header head; + print_string "\n"
let make_sep c = " " ^ (make_line c 76) ^ "\n"
@@ -125,30 +66,6 @@ let print_ct_tree i = | _ -> print_char ':'; loop (j + 1) in loop 0
-(* iterate of first n of a list l and apply f *) -let print_first n l f = - let rec loop i l = - match l with - | [] -> () - | hd::tl -> - if i < n then ((f i hd); loop (i + 1) tl;) - else () in - loop 0 l - -let print_last n l f = - let len = List.length l in - let start = if (len - n) < 0 then 0 else (len - n) in - - let rec loop i l = - match l with - | [] -> () - | hd::tl -> - if (len > n) && (i <= start) then loop (i + 1) tl - else ((f i hd); loop (i + 1) tl) in - - loop 0 l - - (* Colors *) let red = "\x1b[31m" let green = "\x1b[32m"
===================================== src/gambit.ml ===================================== @@ -286,7 +286,7 @@ let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp])
class gambit_compiler lctx output = object - inherit Backend.backend + inherit Backend.compiler
val mutable sctx = ScmContext.of_lctx lctx val mutable lctx = lctx
===================================== src/heap.ml ===================================== @@ -27,15 +27,15 @@ open Lexp
module IMap = Util.IMap
-type location = Util.location +type location = Source.Location.t type symbol = Sexp.symbol type value = Env.value_type
type size = int type addr = int
-let error ~(location : location) (message : string) : 'a = - Log.log_fatal ~section:"HEAP" ~loc:location message +let error ~(loc : location) ?print_action fmt = + Log.log_fatal ~section:"HEAP" ~loc ?print_action fmt
let dloc = Util.dummy_location let type0 = Debruijn.type0 @@ -72,7 +72,7 @@ let export (address : addr) : value = (** Initializes the header of the object so it is valid for the given data constructor. *) let store_header - (location : location) + (loc : location) (address : addr) (datacons : value) : unit = @@ -81,7 +81,7 @@ let store_header | Env.Vcons (symbol, []) -> let constructor, _ = IMap.find address !heap in constructor := Some symbol - | _ -> error ~location ("not a data constructor: " ^ Env.value_string datacons) + | _ -> error ~loc "not a data constructor: %s" (Env.value_string datacons)
(** If [address] points to an object of at least [cell_index + 1] cells, mutates the value at that index. *) @@ -96,49 +96,49 @@ let load_cell (address : addr) (cell_index : int) : value = Option.get cells.(cell_index)
let datacons_label_of_string : builtin_function = - fun location _ + fun loc _ -> function | [Vstring _ as label] -> label - | _ -> error ~location "`datacons-label<-string` expects [##DataconsLabel]." + | _ -> error ~loc "`datacons-label<-string` expects [##DataconsLabel]."
let heap_alloc : builtin_function = - fun location _ + fun loc _ -> function | [Vint size] -> Vcommand (fun () -> Vint (alloc size)) - | _ -> error ~location "`Heap.alloc` expects [Int]." + | _ -> error ~loc "`Heap.alloc` expects [Int]."
let heap_free : builtin_function = - fun location _ + fun loc _ -> function | [Vint address] -> Vcommand (fun () -> free address; Vint 0) - | _ -> error ~location "`Heap.free` expects [Int]." + | _ -> error ~loc "`Heap.free` expects [Int]."
let heap_export : builtin_function = - fun location _ + fun loc _ -> function | [Vint address] -> Vcommand (fun () -> export address) - | _ -> error ~location "`Heap.export` expects [Int]." + | _ -> error ~loc "`Heap.export` expects [Int]."
let heap_store_header : builtin_function = - fun location _ + fun loc _ -> function | [Vint address; datacons] - -> Vcommand (fun () -> store_header location address datacons; Vint 0) - | _ -> error ~location "`Heap.store-header` expects [Int; 'a]" + -> Vcommand (fun () -> store_header loc address datacons; Vint 0) + | _ -> error ~loc "`Heap.store-header` expects [Int; 'a]"
let heap_store_cell : builtin_function = - fun location _ + fun loc _ -> function | [Vint address; Vint cell_index; value] -> Vcommand (fun () -> store_cell address cell_index value; Vint 0) - | _ -> error ~location "`Heap.store-header` expects [Int; Int; 'a]" + | _ -> error ~loc "`Heap.store-header` expects [Int; Int; 'a]"
let heap_load_cell : builtin_function = - fun location _ + fun loc _ -> function | [Vint address; Vint cell_index; _value] -> Vcommand (fun () -> load_cell address cell_index) - | _ -> error ~location "`Heap.store-cell` expects [Int; Int]" + | _ -> error ~loc "`Heap.store-cell` expects [Int; Int]"
let register_builtins () = add_builtin_cst "DataconsLabel" type_datacons_label;
===================================== src/inverse_subst.ml ===================================== @@ -171,11 +171,12 @@ let inverse (s: subst) : subst option = | Some s1 -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () - else (Log.log_debug ("Subst-inversion-bug: " - ^ subst_string s ^ " ∘ " - ^ subst_string s1 ^ " == " - ^ subst_string (Lexp.scompose s1 s) - ^ " !!\n")) + else + Log.log_debug + "Subst-inversion-bug: %s ∘ %s == %s !!\n" + (subst_string s) + (subst_string s1) + (subst_string (Lexp.scompose s1 s)) | _ -> ()); res
===================================== src/lexp.ml ===================================== @@ -353,8 +353,12 @@ let mkSLlub' (e1, e2) = | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) - | _ -> Log.log_fatal ~section:"internal" - ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2) + | _ + -> Log.log_fatal + ~section:"internal" + "SLlub of non-level: %s ∪ %s" + (lexp_head e1) + (lexp_head e2)
let mkSLsucc e = match lexp_lexp' e with
===================================== src/log.ml ===================================== @@ -22,6 +22,8 @@ this program. If not, see http://www.gnu.org/licenses/. *)
open Util
+open Printf + (* LOGGING LEVELS *)
type log_level = Nothing | Fatal | Error | Warning | Info | Debug @@ -169,44 +171,89 @@ let clear_log () = typer_log := empty_log let print_log () = let reverse = typer_log_config.print_in_reverse in let l = if reverse then !typer_log else List.rev !typer_log in - List.iter print_entry l - -let print_and_clear_log () = - print_log (); clear_log () - -let log_msg level ?kind ?section ?print_action ?loc msg = - log_entry (mkEntry level ?kind ?section ?print_action ?loc msg) + List.iter print_entry l; + typer_log := empty_log + +let log_msg + (k : string -> 'd) + level + ?kind + ?section + ?print_action + ?loc + (fmt : ('a, unit, string, 'd) format4) + : 'a = + + let k' message = + message + |> mkEntry level ?kind ?section ?print_action ?loc + |> log_entry; + k message + in + ksprintf k' fmt
exception Internal_error of string -let internal_error s = raise (Internal_error s) +let internal_error fmt = + ksprintf (fun s -> raise (Internal_error s)) fmt
exception User_error of string -let user_error s = raise (User_error s) +let user_error fmt = + ksprintf (fun s -> raise (User_error s)) fmt + +exception Stop_compilation of string +let stop_compilation fmt = + ksprintf (fun s -> raise (Stop_compilation s)) fmt + +let show_error (message : string) : unit = + print_log (); + print_endline message; + flush stdout + +let handle_error ~(on_error : unit -> 'a) (action : unit -> 'a) : 'a = + try action () with + | Stop_compilation message + -> show_error message; + on_error () + | User_error message + -> show_error ("fatal user error: " ^ message); + on_error () + | Internal_error message + -> show_error ("internal error: " ^ message); + on_error () + +let log_fatal ?section ?print_action ?loc fmt = + typer_log_config.print_at_log <- true; + log_msg + (fun _ -> internal_error "Compiler Fatal Error") + Fatal + ~kind:"[X] Fatal " + ?section + ?print_action + ?loc + fmt
-exception Stop_Compilation of string -let stop_compilation s = raise (Stop_Compilation s) +let log_error ?section ?print_action ?loc fmt = + log_msg (fun _ -> ()) Error ?kind:None ?section ?print_action ?loc fmt
-let log_fatal ?section ?print_action ?loc m = - typer_log_config.print_at_log <- true; - log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; - internal_error "Compiler Fatal Error" -let log_error = log_msg Error ?kind:None -let log_warning = log_msg Warning ?kind:None -let log_info = log_msg Info ?kind:None -let log_debug = log_msg Debug ?kind:None +let log_warning ?section ?print_action ?loc fmt = + log_msg (fun _ -> ()) Warning ?kind:None ?section ?print_action ?loc fmt + +let log_info ?section ?print_action ?loc fmt = + log_msg (fun _ -> ()) Info ?kind:None ?section ?print_action ?loc fmt + +let log_debug ?section ?print_action ?loc fmt = + log_msg (fun _ -> ()) Debug ?kind:None ?section ?print_action ?loc fmt
let stop_on_error () = let count = error_count () in - if (0 < count) then - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" errors\n") + if 0 < count then + stop_compilation "Compiler stopped after: %d errors\n" count
let stop_on_warning () = stop_on_error (); let count = warning_count () in - if (0 < count) then - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" warnings\n") + if 0 < count then + stop_compilation "Compiler stopped after: %d warnings\n" count
(* Compiler Internal Debug print *) let debug_msg expr =
===================================== src/opslexp.ml ===================================== @@ -48,8 +48,8 @@ type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t (* Metavars that appear in non-erasable positions. *) * unit IMap.t
-let error ~location message = - Log.log_fatal ~section:"OPSLEXP" ~loc:location message +let error ~location fmt = + Log.log_fatal ~section:"OPSLEXP" ~loc:location fmt
module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but @@ -62,8 +62,11 @@ let reducible_builtins -> (P.arg_kind * lexp) list (* The builtin's args *) -> lexp option) SMap.t)
-let error_tc = Log.log_error ~section:"TC" -let warning_tc = Log.log_warning ~section:"TC" +let log_tc_error ?print_action ?loc fmt = + Log.log_error ~section:"TC" ?print_action ?loc fmt + +let log_tc_warning ?print_action ?loc fmt = + Log.log_warning ~section:"TC" ?print_action ?loc fmt
(* `conv_erase` is supposed to be safe according to the ICC papers. It might be incompatible with the reduction of `Eq.cast`, though. See : @@ -220,15 +223,16 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in lexp_whnf_aux (push_susp branch subst) ctx - with Not_found - -> match default - with | Some (_v,default) - -> let subst = S.cons (get_refl e') (S.substitute e') in - lexp_whnf_aux (push_susp default subst) ctx - | _ -> Log.log_error ~section:"WHNF" ~loc:l - ("Unhandled constructor " ^ - name ^ "in case expression"); - mkCase (l, e, rt, branches, default) in + with + | Not_found + -> match default with + | Some (_v,default) + -> let subst = S.cons (get_refl e') (S.substitute e') in + lexp_whnf_aux (push_susp default subst) ctx + | _ -> Log.log_error + ~section:"WHNF" ~loc:l + {|Unhandled constructor "%s" in case expression|} name; + mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> @@ -583,27 +587,27 @@ and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else (error_tc ~loc:(lexp_location e) - ("Type mismatch for " - ^ lexp_string e ^ " : " - ^ lexp_string t ^ " != " - ^ lexp_string t'); - (* Log.internal_error "Type mismatch" *)) in + else + log_tc_error + ~loc:(lexp_location e) + "Type mismatch for %s : %s != %s" + (lexp_string e) (lexp_string t) (lexp_string t') + in let check_type erased ctx t = let s = check erased ctx t in (match lexp'_whnf s ctx with - | Sort _ -> () - | _ -> error_tc ~loc:(lexp_location t) - ("Not a proper type: " ^ lexp_string t)); - (* FIXME: return the `sort` rather than the surrounding `lexp`! *) - s in + | Sort _ -> () + | _ + -> let loc = lexp_location t in + log_tc_error ~loc "Not a proper type: %s" (lexp_string t)); + s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; - DB.type_int) + -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; + DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) -> let t = check erased ctx e in @@ -630,12 +634,13 @@ and check'' erased ctx e = -> let _ = check_type DB.set_empty Myers.nil t in t (* FIXME: Check recursive references. *) - | Var (((l, name), idx) as v) + | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then - error_tc ~loc:l - ("Var `" ^ maybename name ^ "`" - ^ " can't be used here, because it's `erasable`"); - lookup_type ctx v + log_tc_error + ~loc + {|Var `%s` can't be used here, because it's erasable|} + (maybename name) ; + lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) -> let _ = @@ -658,23 +663,21 @@ and check'' erased ctx e = (List.length defs) defs in mkSusp (check nerased nctx e) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, l, t2) + | Arrow (ak, v, t1, loc, t2) -> (let k1 = check_type erased ctx t1 in - let nctx = DB.lexp_ctx_cons ctx v Variable t1 in - let k2 = check_type (DB.set_sink 1 erased) nctx t2 in - match sort_compose ctx nctx l ak k1 k2 with - | SortResult k -> k - | SortInvalid - -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; - mkSort (l, StypeOmega) - | SortK1NotType - -> (error_tc ~loc:(lexp_location t1) - "Not a proper type"; - mkSort (l, StypeOmega)) - | SortK2NotType - -> (error_tc ~loc:(lexp_location t2) - "Not a proper type"; - mkSort (l, StypeOmega))) + let nctx = DB.lexp_ctx_cons ctx v Variable t1 in + let k2 = check_type (DB.set_sink 1 erased) nctx t2 in + match sort_compose ctx nctx loc ak k1 k2 with + | SortResult k -> k + | SortInvalid + -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; + mkSort (loc, StypeOmega) + | SortK1NotType + -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; + mkSort (loc, StypeOmega) + | SortK2NotType + -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; + mkSort (loc, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, l, @@ -686,19 +689,17 @@ and check'' erased ctx e = List.fold_left (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) - ctx arg in - match lexp'_whnf ft ctx with - | Arrow (ak', _v, t1, _l, t2) - -> if not (ak == ak') then - (error_tc ~loc:(lexp_location arg) - "arg kind mismatch"; ()) - else (); - assert_type ctx arg at t1; - mkSusp t2 (S.substitute arg) - | _ -> (error_tc ~loc:(lexp_location arg) - ("Calling a non function (type = " - ^ lexp_string ft ^ ")!"); - ft)) + ctx arg in + match lexp'_whnf ft ctx with + | Arrow (ak', _v, t1, _l, t2) + -> if ak != ak' + then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; + assert_type ctx arg at t1; + mkSusp t2 (S.substitute arg) + | _ -> log_tc_error + ~loc:(lexp_location arg) + "Calling a non functin (type = %s)!" (lexp_string ft); + ft) ft args | Inductive (l, _label, args, cases) -> let rec arg_loop ctx erased args = @@ -722,15 +723,14 @@ and check'' erased ctx e = (* FIXME: If it does refer, * we get an ugly error! *) (mkSusp level' (L.sunshift n)) - | _tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); - level), + | _tt + -> log_tc_error + ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline ()) + "Field type %s is not a Type! (%s)" + (lexp_string t) (lexp_string lwhnf); + level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, n + 1)) @@ -771,8 +771,9 @@ and check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (error_tc ~loc:l - "Wrong arg number to inductive type!"; s) in + | _ + -> log_tc_error ~loc:l "Wrong arg number to inductive type!"; + s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in @@ -801,9 +802,9 @@ and check'' erased ctx e = (ssink vdef s) (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes - | _,_ -> (error_tc ~loc:l - "Wrong number of args to constructor!"; - (erased, ctx, hlxp)) in + | _ + -> log_tc_error ~loc:l "Wrong number of args to constructor!"; + (erased, ctx, hlxp) in let hctor = mkCall (mkCons (it, (l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in @@ -818,8 +819,8 @@ and check'' erased ctx e = let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with | Some (v, d) - -> if diff <= 0 then - warning_tc ~loc:l "Redundant default clause"; + -> if diff <= 0 + then log_tc_warning ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -829,10 +830,11 @@ and check'' erased ctx e = assert_type nctx d (check nerased nctx d) (mkSusp ret (S.shift 2)) | None - -> if diff > 0 then - error_tc ~loc:l ("Non-exhaustive match: " - ^ string_of_int diff ^ " cases missing")) - | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); + -> if diff > 0 + then + log_tc_error + ~loc:l "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -859,14 +861,14 @@ and check'' erased ctx e = -> mkArrow (P.Aerasable, vd, atype, l, buildtype fargs) in buildtype fargs - with Not_found - -> (error_tc ~loc:l - ("Constructor "" ^ name ^ "" does not exist"); - DB.type_int)) - | _ -> (error_tc ~loc:(lexp_location e) - ("Cons of a non-inductive type: " - ^ lexp_string t); - DB.type_int)) + with + | Not_found + -> log_tc_error ~loc:l {|Constructor "%s" does not exist|} name; + DB.type_int) + | _ -> log_tc_error + ~loc:(lexp_location e) + "Cons of a non-inductive type: %s" (lexp_string t); + DB.type_int) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> let e = push_susp e s in @@ -1130,15 +1132,13 @@ let arity_of_cons | Inductive (_, _, _, constructors) -> (match SMap.find_opt name constructors with | Some params -> List.fold_left count_unless_erasable 0 params - | None -> error ~location ("invalid constructor: " ^ name)) + | None -> error ~location "invalid constructor: %s" name) | _ - -> let message = - {|can't deduce arity of constructor "|} - ^ name - ^ {|", because it is not an inductive type: |} - ^ lexp_string ty - in - error ~location:(lexp_location ty) message + -> error + ~location:(lexp_location ty) + ({|can't deduce arity of constructor "%s", |} + ^^ {|because it is not an inductive type: %s|}) + name (lexp_string ty)
let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with
===================================== src/prelexer.ml ===================================== @@ -175,7 +175,8 @@ let prelex (source : #Source.t) : pretoken list = let text, location = source#slice start_point in prelexer_error error_location - ("Unterminated escape sequence in: " ^ text); + "Unterminated escape sequence in: %s" + text; loop ctx (Pretoken (location, text) :: acc))
| Some _
===================================== src/sexp.ml ===================================== @@ -24,8 +24,8 @@ open Util open Prelexer open Grammar
-let sexp_error ?print_action loc msg = - Log.log_error ~section:"SEXP" ?print_action ~loc msg +let sexp_error ?print_action loc fmt = + Log.log_error ~section:"SEXP" ?print_action ~loc fmt
type integer = Z.t type symbol = location * string @@ -224,7 +224,7 @@ let sexp_parse_all grm tokens limit : sexp * token list = | Some token -> match SMap.find token grm with | (Some ll, Some _) -> ll + 1 - | _ -> (Log.internal_error ("Can't find level of ""^token^""")) + | _ -> Log.internal_error {|Can't find level of "%s"|} token in let (e, rest) = sexp_parse grm tokens level [] [] [] in let se = match e with | Node (Symbol (_, ""), [e]) -> e @@ -234,7 +234,7 @@ let sexp_parse_all grm tokens limit : sexp * token list = | [] -> (se,rest) | Symbol (l,t) :: rest -> if not (Some t = limit) - then sexp_error l ("Stray closing token: "" ^ t ^ """); + then sexp_error l {|Stray closing token: "%s"|} t; (se,rest) | _ -> (Log.internal_error "Stopped parsing before the end!")
@@ -280,4 +280,3 @@ and sexp_eq_list ss1 ss2 = match ss1, ss2 with | (s1 :: ss1), (s2 :: ss2) -> sexp_equal s1 s2 && sexp_eq_list ss1 ss2 | _ -> false -
===================================== src/unification.ml ===================================== @@ -20,14 +20,12 @@ You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)
open Lexp -(* open Sexp *) -(* open Inverse_subst *) module OL = Opslexp module DB = Debruijn
(** Provide unify function for unifying two Lambda-Expression *)
-let log_info = Log.log_info ~section:"UNIF" +let log_info ?loc fmt = Log.log_info ~section:"UNIF" ?loc fmt
(* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) @@ -303,10 +301,10 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | MVar (_, t, _) -> push_susp t s in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> log_info ?loc:None ("Unification of metavar failed:\n " - ^ "?[" ^ subst_string s ^ "]" - ^ "\nAgainst:\n " - ^ lexp_string lxp ^ "\n"); + -> log_info + "Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n" + (subst_string s) + (lexp_string lxp); [(CKresidual, ctx, lxp1, lxp2)] | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' @@ -316,11 +314,11 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ - -> log_info ?loc:None - ("Unification of metavar type failed:\n " - ^ lexp_string t ^ " != " - ^ lexp_string (OL.get_type ctx lxp) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + -> log_info + "Unificaton of metavar type failed:\n %s != %s\nfor %s\n" + (lexp_string t) + (lxp |> OL.get_type ctx |> lexp_string) + (lexp_string lxp); [(CKresidual, ctx, lxp1, lxp2)] in (* FIXME Here, we unify lxp1 with lxp2 again, because that the metavariables occuring in the associated term might
===================================== tests/utest_lib.ml ===================================== @@ -226,7 +226,7 @@ let for_all_tests sk tmap tk = ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset); ret_code := failure) with - | Log.Stop_Compilation message -> + | Log.Stop_compilation message -> ret_code := failure; ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); ut_string2 ("[ ] " ^ message ^ "\n" ^ reset);
===================================== typer.ml ===================================== @@ -21,27 +21,18 @@
open Typerlib
-open Backend open Debruijn
-let welcome_msg = -" Typer 0.0.0 - Interpreter - (c) 2016-2021 - - %quit (%q) : leave REPL - %help (%h) : print help -" +open Printf
let arg_batch = ref false -let arg_backend_name = ref "interpreter"
-let arg_files = ref [] -let add_input_file file = - arg_files := file :: !arg_files +let add_input_file, list_input_files = + let files = ref [] in + (fun file -> files := file :: !files), (fun () -> List.rev !files)
let arg_defs = - [("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); - - ("--verbosity", + [("--verbosity", Arg.String Log.set_typer_log_level_str, "Set the logging level");
@@ -50,65 +41,79 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, "Print the full lexp context on error."); - - ("--backend", - Arg.Symbol (["interpreter"; "gambit"], fun name -> arg_backend_name := name), - "Select the backend"); ]
-let main () = - let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in - Arg.parse arg_defs add_input_file usage; +let compile_main argv = + let usage = Sys.executable_name ^ " compile [options] <file> …" in + Arg.parse_argv argv arg_defs add_input_file usage;
let ectx = Elab.default_ectx in - let backend = - let lctx = ectx_to_lctx ectx in - match !arg_backend_name with - | "gambit" -> (new Gambit.gambit_compiler lctx stdout :> backend) - | _ -> (new Eval.ast_interpreter lctx :> backend) + let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in + + let _ = + List.fold_left (Elab.process_file backend) ectx (list_input_files ()) in - let interactive = backend#interactive in - let file_names = List.rev !arg_files in - let is_interactive = not !arg_batch && Option.is_some interactive in - - let process_file = - if is_interactive - then - (print_string (Fmt.make_title " TYPER REPL "); - print_string welcome_msg; - print_string (Fmt.make_sep '-'); - flush stdout; - fun ectx i file_name - -> Printf.printf " In[%02d] >> %%readfile %s\n" i file_name; - Elab.eval_file backend ectx file_name) - else - fun ectx _ file_name -> Elab.eval_file backend ectx file_name + Log.print_log () + +let repl_main argv = + let usage = Sys.executable_name ^ " repl [options] [<file>] …" in + Arg.parse_argv argv arg_defs add_input_file usage; + + print_string (Fmt.make_title " TYPER REPL "); + print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; + print_newline (); + print_endline " %quit (%q) : leave REPL"; + print_endline " %help (%h) : print help"; + print_string (Fmt.make_sep '-'); + flush stdout; + + let ectx = Elab.default_ectx in + let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in + + let load_file (ectx, i) file_name = + printf " In[% 2d] >> %%readfile %s\n" i file_name; + Elab.process_file backend ectx file_name, i + 1 in + let ectx, i = List.fold_left load_file (ectx, 0) (list_input_files ()) in + Log.print_log (); + REPL.repl i backend ectx + +let run_main argv = + let usage = Sys.executable_name ^ " run [options] <file> …" in + Arg.parse_argv argv arg_defs add_input_file usage; + + let ectx = Elab.default_ectx in + let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in
- let ectx, i = - try - let res = - List.fold_left - (fun (ectx, i) file_name -> (process_file ectx i file_name, i + 1)) - (ectx, 0) - file_names - in - REPL.print_and_clear_log (); - res - with - | Log.Stop_Compilation msg - -> REPL.handle_stopped_compilation msg; - exit 1 - | (Log.Internal_error msg) as e - -> REPL.handle_stopped_compilation ("Internal error: " ^ msg); - raise e - | Log.User_error msg - -> REPL.handle_stopped_compilation ("Fatal user error: " ^ msg); - exit 1 + let _ = + List.fold_left (Elab.process_file backend) ectx (list_input_files ()) + in + Log.print_log () + +let main () = + let command, argv = + if Array.length Sys.argv <= 1 + then "repl", [||] + else + let command = Sys.argv.(1) in + if command.[0] = '-' || String.contains command '.' + then "repl", Sys.argv + else + (command, + Array.append + [|Sys.argv.(0)|] + (Array.sub Sys.argv 2 (Array.length Sys.argv - 2))) in
- match is_interactive, interactive with - | true, Some (interactive) -> REPL.repl i interactive ectx - | _ -> () + Log.handle_error + ~on_error:(fun () -> exit 1) + (fun () -> + match command with + | "compile" -> compile_main argv + | "repl" -> repl_main argv + | "run" -> run_main argv + | _ + -> eprintf {|unknown command "%s"|} command; + exit 1)
let () = main ()
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/89cc24320ab7feb755a758e792b58252e...