Simon Génier pushed to branch remove-artisanal-printing at Stefan / Typer

Commits: fce0fac4 by Simon Génier at 2021-09-28T18:16:00-04:00 Upgrade to OCaml 4.11.

* Update the README * Remove a few functions that are now part of the standard library.

- - - - - db1cf4da by Stefan Monnier at 2021-10-06T09:38:32-04:00 Merge remote-tracking branch 'gitlab/ocaml-4.11' into trunk

- - - - - 8efdff37 by Stefan Monnier at 2021-10-06T10:01:02-04:00 Merge remote-tracking branch 'gitlab/purge-docstr' into trunk

- - - - - 89cc2432 by Stefan Monnier at 2021-10-06T10:01:55-04:00 Merge remote-tracking branch 'gitlab/source-spans-2' into trunk

- - - - - 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.

- - - - -

26 changed files:

- README.md - debug_util.ml - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/env.ml - src/eval.ml - − src/float.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - − src/int.ml - src/inverse_subst.ml - src/lexp.ml - src/listx.ml - src/log.ml - src/opslexp.ml - − src/option.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/utest_lib.ml - typer.ml

Changes:

===================================== README.md ===================================== @@ -8,7 +8,7 @@ Status []

## Requirement

-* Ocaml 4.05 +* Ocaml 4.11 * Dune 2.x * Zarith

===================================== 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)); @@ -279,7 +281,7 @@ let main () =

(* Type erasure *) let _, clean_lxp = - Listx.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps + List.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps in

(* Eval declaration *)

===================================== src/REPL.ml ===================================== @@ -36,6 +36,8 @@ this program. If not, see http://www.gnu.org/licenses/. *) * * -------------------------------------------------------------------------- *)

+open Printf + open Backend open Debruijn open Eval @@ -50,11 +52,9 @@ module OL = Opslexp module EL = Elexp

let print_input_line i = - print_string " In["; - ralign_print_int i 2; - print_string "] >> " + printf " In[%02d] >> " i

-let error = Log.log_error ~section:"REPL" +let error fmt = Log.log_error ~section:"REPL" fmt

let print_and_clear_log () = if (not Log.typer_log_config.Log.print_at_log) then @@ -188,14 +188,14 @@ let rec repl i (interactive : #interactive_backend) (ectx : elab_context) = ectx)

| cmd::_ -> - error (" "" ^ cmd ^ "" is not a correct repl command"); + error {|"%s" is not a correct REPL command|} cmd; ectx | _ -> ectx)

(* eval input *) | _ -> try eval_interactive interactive i ectx ipt with - | Log.Stop_Compilation msg -> + | Log.Stop_compilation msg -> (handle_stopped_compilation msg; ectx) | Log.Internal_error msg -> (handle_stopped_compilation ("Internal error: " ^ msg);

===================================== 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 " - ^ (U.option_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)] @@ -1701,7 +1717,7 @@ let sform_letin ctx loc sargs ot = match sargs with List.fold_left (fun (s, off) decls -> (OL.lexp_defs_subst loc s decls, off + List.length decls)) (S.identity, 0) declss in - let ot = U.option_map (fun t -> mkSusp t (S.shift off)) ot in + let ot = Option.map (fun t -> mkSusp t (S.shift off)) ot in let bdy, ot = elaborate nctx sbody ot in let ot = match ot with | Inferred t -> Inferred (mkSusp t s) @@ -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 @@ -1945,7 +1961,7 @@ let eval_expr_str str ectx rctx = let eval_decl_str str ectx rctx = let lxps, ectx' = lexp_decl_str str ectx in let lctx = ectx_to_lctx ectx in - let _, elxps = Listx.fold_left_map (OL.clean_decls) lctx lxps in + let _, elxps = List.fold_left_map (OL.clean_decls) lctx lxps in (EV.eval_decls_toplevel elxps rctx), ectx'

let eval_file @@ -1963,5 +1979,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"

===================================== src/float.ml deleted ===================================== @@ -1,25 +0,0 @@ -(* Copyright (C) 2020 Free Software Foundation, Inc. - * - * Author: Simon Génier simon.genier@umontreal.ca - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any later - * version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more - * details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see http://www.gnu.org/licenses/. *) - -type t = float - -let equal (l : t) (r : t) : bool = l = r - -let compare (l : t) (r : t) : int = compare l r

===================================== 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 ===================================== @@ -176,7 +176,7 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = then scheme_of_expr sctx body else let sctx, bindings = - Listx.fold_left_map ScmContext.intro_binding sctx bindings + List.fold_left_map ScmContext.intro_binding sctx bindings in let scheme_of_binding (name, elexp) = Scm.List [Scm.Symbol name; scheme_of_expr sctx elexp] @@ -293,7 +293,7 @@ class gambit_compiler lctx output = object

method process_decls ldecls = let lctx', eldecls = Opslexp.clean_decls lctx ldecls in - let sctx', eldecls = Listx.fold_left_map ScmContext.intro_binding sctx eldecls in + let sctx', eldecls = List.fold_left_map ScmContext.intro_binding sctx eldecls in let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in

sctx <- sctx';

===================================== 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/int.ml deleted ===================================== @@ -1,25 +0,0 @@ -(* Copyright (C) 2020 Free Software Foundation, Inc. - * - * Author: Simon Génier simon.genier@umontreal.ca - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any later - * version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more - * details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see http://www.gnu.org/licenses/. *) - -type t = int - -let equal (l : t) (r : t) : bool = l = r - -let compare (l : t) (r : t) : int = compare l r

===================================== 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/listx.ml ===================================== @@ -18,33 +18,6 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see http://www.gnu.org/licenses/. *)

-(* Backport from 4.08. *) -let filter_map (f : 'a -> 'b option) (xs : 'a list) : 'b list = - let rec loop xs ys = - match xs with - | [] -> List.rev ys - | x :: xs - -> (match f x with - | Some y -> loop xs (y :: ys) - | None -> loop xs ys) - in - loop xs [] - -(* Backport from 4.11. *) -let fold_left_map - (f : 'a -> 'b -> 'a * 'c) - (i : 'a) - (bs : 'b list) - : 'a * 'c list = - - let rec loop fold_acc map_acc bs = match bs with - | [] -> (fold_acc, List.rev map_acc) - | b :: bs - -> let fold_acc, new_element = f fold_acc b in - loop fold_acc (new_element :: map_acc) bs - in - loop i [] bs - (* Backport from 4.12. *) let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = match ls, rs 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 @@ -114,9 +116,12 @@ let maybe_color_string color_opt str = let string_of_log_entry {level; kind; section; loc; msg; _} = let color = if typer_log_config.color then (level_color level) else None in let parens s = "(" ^ s ^ ")" in - (option_default "" (option_map Source.Location.to_string loc) - ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":" - ^ option_default "" (option_map parens section) ^ " " + (Option.value ~default:"" (Option.map Source.Location.to_string loc) + ^ maybe_color_string + color + (Option.value ~default:(string_of_level level) kind) + ^ ":" + ^ Option.value ~default:"" (Option.map parens section) ^ " " ^ msg)

let print_entry entry = @@ -171,39 +176,69 @@ let print_log () = 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) +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 s = raise (Stop_Compilation s) +exception Stop_compilation of string +let stop_compilation fmt = + ksprintf (fun s -> raise (Stop_compilation s)) fmt

-let log_fatal ?section ?print_action ?loc m = +let log_fatal ?section ?print_action ?loc fmt = 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 + log_msg + (fun _ -> internal_error "Compiler Fatal Error") + Fatal + ~kind:"[X] Fatal " + ?section + ?print_action + ?loc + fmt + +let log_error ?section ?print_action ?loc fmt = + log_msg (fun _ -> ()) Error ?kind:None ?section ?print_action ?loc fmt + +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 : @@ -187,7 +190,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | Call (f', xs1) -> mkCall (f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with - | Some f -> U.option_default e (f ctx args) + | Some f -> Option.value ~default:e (f ctx args) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> @@ -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 @@ -1159,7 +1159,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = E.Let (l, edecls, erase_type lctx' body)

| L.Call (fct, args) - -> E.Call (erase_type lctx fct, Listx.filter_map (clean_arg lctx) args) + -> E.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args)

| L.Case (location, target, _, branches, default) -> let etarget = erase_type lctx target in @@ -1227,7 +1227,7 @@ let erase_type lctx lxp = ~print_action:(fun () -> IMap.iter (fun i (_, t, _, (l, n)) -> print_endline ("\t" ^ (Source.Location.to_string l) - ^ " ?" ^ (U.option_default "" n) + ^ " ?" ^ (Option.value ~default:"" n) ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) ) mvs) ("Metavariables in erase_type :");

===================================== src/option.ml deleted ===================================== @@ -1,47 +0,0 @@ -(* Copyright (C) 2020 Free Software Foundation, Inc. - * - * Author: Simon Génier simon.genier@umontreal.ca - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any later - * version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more - * details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see http://www.gnu.org/licenses/. *) - -type 'a t = 'a option - -let equal (inner_equal : 'a -> 'a -> bool) (l : 'a t) (r : 'a t) : bool = - match l, r with - | Some l, Some r -> inner_equal l r - | None, None -> true - | _ -> false - -let get (o : 'a option) : 'a = - match o with - | Some v -> v - | None -> invalid_arg "expected Some" - -let value ~(default : 'a) (o : 'a option) : 'a = - match o with - | Some v -> v - | None -> default - -let is_some (o : 'a option) : bool = - match o with - | Some _ -> true - | None -> false - -let is_none (o : 'a option) : bool = - match o with - | Some _ -> false - | None -> true

===================================== 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

===================================== src/util.ml ===================================== @@ -20,21 +20,8 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-(** Adds the update function to maps. This can be removed when we upgrade to - OCaml >= 4.06 *) -module UPDATABLE(Base : Map.S) = struct - include Base - - let update key f map = - let before = find_opt key map in - match before, f before with - | _, Some after -> add key after map - | Some _before, None -> remove key map - | None, None -> map -end - -module SMap = UPDATABLE(Map.Make(String)) -module IMap = UPDATABLE(Map.Make(Int)) +module SMap = Map.Make(String) +module IMap = Map.Make(Int)

type charpos = int type bytepos = int @@ -66,8 +53,6 @@ let get_vname_name vname = let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b)

-let opt_map f x = match x with None -> None | Some x -> Some (f x) - let str_split str sep = let str = String.trim str in let n = String.length str in @@ -115,16 +100,6 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string = in let lpad = max diff 0 in (String.make lpad char_) ^ str

-let option_default (default : 'a) (opt : 'a option) : 'a = - match opt with - | None -> default - | Some x -> x - -let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = - match opt with - | None -> None - | Some x -> Some (fn x) - (* It seemed good to use the prime number 31. * FIXME: Pick another one ? *) let combine_hash e1 e2 = (e1 * 31) lxor e2

===================================== 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 ===================================== @@ -96,7 +96,7 @@ let main () = REPL.print_and_clear_log (); res with - | Log.Stop_Compilation msg + | Log.Stop_compilation msg -> REPL.handle_stopped_compilation msg; exit 1 | (Log.Internal_error msg) as e

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9cbe376c472e7c11be35f31d3ef6e94ea...