Simon Génier pushed to branch trace-vs-diagnose at Stefan / Typer

Commits: 078fe770 by Simon Génier at 2022-09-13T14:55:24-04:00 WIP

- - - - -

22 changed files:

- src/REPL.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/instargs.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - src/unification.ml - typer.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -53,8 +53,6 @@ module EL = Elexp let print_input_line i = printf " In[%02d] >> " i

-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 * If return is pressed and the last char is not ';' then @@ -123,7 +121,8 @@ let eval_interactive in loop nodes [] [] in

- let source = new Source.source_string input in + let container = Source.Container.String (sprintf "REPL#%d" i, input) in + let source = new Source.source_string ~container input in let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in (* FIXME: This is too eager: it prevents one declaration from changing the @@ -144,11 +143,11 @@ let eval_interactive List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs;

List.iter interactive#process_decls ldecls; - Log.print_log (); + Log.Diagnostics.print_log ();

let values = List.map interactive#eval_expr lexprs in List.iter (Eval.print_eval_result i) values; - Log.print_log (); + Log.Diagnostics.print_log ();

ectx'

@@ -171,7 +170,7 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) = -> let ectx' = List.fold_left (Elab.process_file interactive) ectx args in - Log.print_log (); + Log.Diagnostics.print_log (); ectx' | "%who"::args | "%w"::args -> let _ = match args with @@ -184,8 +183,8 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) = | _ -> print_lexp_ctx (ectx_to_lctx ectx) in ectx

- | cmd::_ - -> error {|"%s" is not a correct REPL command|} cmd; + | cmd :: _ + -> fprintf stderr "“%s” is not a correct REPL command\n" cmd; ectx

| _ -> ectx)

===================================== src/builtin.ml ===================================== @@ -61,15 +61,8 @@ open Lexp module DB = Debruijn module E = Env

-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 {trace_fatal; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "BUILT-IN"

let predef_names = [ "cons"; (* FIXME: Should be used but isn't! *) @@ -91,7 +84,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 {|"%s" was not predefined|} name + with Not_found -> trace_fatal __POS__ {|"%s" was not predefined|} name

let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) @@ -124,8 +117,9 @@ let v2o_list v = | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl | E.Vcons ((_, "nil"), []) -> List.rev acc | _ -> - log_raise_error + trace_fatal ~loc:(E.value_location v) + __POS__ "Failed to convert the %s with value:\n%s\n to a list." (E.value_name v) (E.value_string v) in

===================================== src/debruijn.ml ===================================== @@ -45,8 +45,8 @@ open Fmt

module S = Subst

-let fatal ?print_action ?loc fmt = - Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt +let {trace_fatal; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "DEBRUIJN"

(** Sets of DeBruijn indices **)

@@ -453,6 +453,19 @@ let summarize_lctx (lctx : lexp_context) (at : int) : unit =

let log_full_lctx = ref false

+let display_lexp_context ?(all : bool = false) ?(around : int option) ctx _ _ = + (* TODO: use channel and colorize *) + match around with + | Some around when not !log_full_lctx + -> summarize_lctx ctx around + | _ + -> if all + then + dump_lexp_ctx ctx + else + print_lexp_ctx ctx; + print_newline () + (* generic lookup *) let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let ((loc, oename), dbi) = v in @@ -460,25 +473,26 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let ret = Myers.nth dbi ctx in let _ = match (ret, oename) with | (((_, Some name), _, _), Some ename) - -> (* Check if names match *) - if not (ename = name) then - let print_action = - if !log_full_lctx - then fun () -> (print_lexp_ctx ctx; print_newline ()) - else fun () -> summarize_lctx ctx dbi - in - fatal - ~loc:(sexp_location loc) ~print_action - ({|DeBruijn index %d refers to wrong name. |} - ^^ {|Expected: "%s" got "%s"|}) + (* Check if names match *) + -> if ename <> name + then + trace_fatal + ~context:[display_lexp_context ~around:dbi ctx] + ~loc:(Sexp.sexp_location loc) + __POS__ + "DeBruijn index %d refers to wrong name. Expected: “%s” got “%s”" dbi ename name | _ -> () in

ret with | Not_found - -> fatal - ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + -> trace_fatal + ~loc:(sexp_location loc) + __POS__ + "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 @@ -516,6 +530,6 @@ let lctx_view lctx = | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] | Myers.Mcons ((_, LetDef (o, _def), _), _, _, _) when o > 1 - -> fatal "Unexpected lexp_context shape!" + -> trace_fatal __POS__ "Unexpected lexp_context shape!" | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx)

===================================== src/debug.ml ===================================== @@ -117,34 +117,36 @@ let debug_pexp_print ptop = print_info (sexp_name ptop) l ptop

let debug_lexp_decls decls = - let sep = " : " in - List.iter (fun e -> - let ((loc, _name), lxp, _ltp) = e in - - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string - (sexp_location loc)); - - let str = lexp_str_decls (!debug_ppctx) [e] in - - (* First col size = 15 + 1 + 2 + 3 + 5 + 6 - * = 32 *) - - let str = match str with - | fst::tl -> print_string (sep ^ fst); print_string "\n"; tl - | _ -> [] in - - (* inefficient but makes things pretty iff -fmt-pretty=on *) - let str = List.flatten (List.map (fun g -> str_split g '\n') str) in - - let str = match str with - | scd :: tl - -> printf " FILE: %-25s : %s\n" (sexp_location loc).file scd; - tl - | _ -> [] in - - List.iter (fun g -> - print_string ((make_line ' ' 32) ^ sep); - print_string g; print_string "\n") - str; - - ) decls + let sep = " : " in + + let debug_lexp_decl e = + let ((loc, _name), lxp, _ltp) = e in + printf + "%-15s[%s]" + (lexp_name lxp) + (Source.Location.to_string (sexp_location loc)); + let str = lexp_str_decls (!debug_ppctx) [e] in + + (* First col size = 15 + 1 + 2 + 3 + 5 + 6 + * = 32 *) + let str = match str with + | fst::tl -> print_string (sep ^ fst); print_string "\n"; tl + | _ -> [] in + + (* inefficient but makes things pretty iff -fmt-pretty=on *) + let str = List.flatten (List.map (fun g -> str_split g '\n') str) in + + let str = + match str with + | scd :: tl + -> let name = Source.Container.name (sexp_location loc).container in + printf " FILE: %-25s : %s\n" name scd; + tl + | _ -> [] in + + List.iter (fun g -> + print_string ((make_line ' ' 32) ^ sep); + print_string g; print_string "\n") str; + in + + List.iter debug_lexp_decl decls

===================================== src/elab.ml ===================================== @@ -72,35 +72,19 @@ let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl"

-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 -let print_indent_line str = - print_endline (indent_line str) -let print_details to_name to_str elem = - print_indent_line ((to_name elem) ^ ": " ^ (to_str elem)) -let lexp_print_details lexp () = - print_details lexp_name lexp_string lexp -let value_print_details value () = - print_details value_name value_string value - -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 = - fatal ~loc ~print_action:(value_print_details value) - -let macro_tracing_enabled = ref false -let trace_macro ~location fmt = Log.log_debug ~loc:location ~section:"MACRO" fmt +let display_lexp_details lexp channel _ = + fprintf channel "\t > %s : %s\n" (lexp_name lexp) (lexp_string lexp) + +let display_value_details value channel _ = + fprintf channel "\t > %s : %s\n" (value_name value) (value_string value) + +let {diagnostic_fatal; diagnostic_error; diagnostic_warning; diagnostic_info; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "EVAL" + +let {diagnostic_info = macro_diagnostic_info; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "MACRO"

(** Type info returned by elaboration. *) type sform_type = @@ -143,76 +127,87 @@ let sform_default_ectx = ref empty_elab_context * to errors in the user's code). *)

let elab_check_sort (ctx : elab_context) lsort (var: vname) ltp = - match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) - with e -> - info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) - ~loc:(lexp_location lsort) - "Exception during whnf of sort:"; - raise e) with + match OL.lexp'_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) | _ -> let tystr = lexp_string ltp ^ " : " ^ lexp_string lsort in - match var with - | (l, None) -> lexp_error (sexp_location l) ltp {|"%s" is not a proper type|} tystr + begin match var with + | (l, None) + -> diagnostic_error + ~context:[display_lexp_details ltp] + (sexp_location l) + {|"%s" is not a proper type|} tystr | (l, Some name) - -> lexp_error (sexp_location l) ltp {|Type of "%s" is not a proper type: %s|} name tystr + -> diagnostic_error + ~context:[display_lexp_details ltp] + (sexp_location l) + {|Type of "%s" is not a proper type: %s|} name tystr + end + | exception e + -> diagnostic_info + ~context:[fun _ _ -> lexp_print lsort; print_newline ()] + (lexp_location lsort) + "Exception during whnf of sort:"; + raise e

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 "%s"%s|} - (lexp_string ltp) - (match var with - | (_, None) -> "" - | (_, Some name) -> " of var `" ^ name ^ "`"); - raise e + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with + | Log.Stop_compilation _ as e -> raise e + | e + -> diagnostic_info + ~context:[fun _ _ -> print_lexp_ctx (ectx_to_lctx ctx); print_newline ()] + (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 let loc = lexp_sinfo lxp in

- let ltype' = try OL.check lctx lxp - with e -> match e with - | Log.Stop_compilation _ -> raise e - | _ -> - info - ~print_action:(fun _ -> - lexp_print_details lxp (); - print_lexp_ctx (ectx_to_lctx ctx); - print_newline () - ) - ~loc:(sexp_location loc) + let ltype' = + try OL.check lctx lxp with + | Log.Stop_compilation _ as e -> raise e + | _ as e + -> diagnostic_info + ~context:[ + display_lexp_details lxp; + fun _ _ -> print_lexp_ctx (ectx_to_lctx ctx); print_newline (); + ] + (sexp_location loc) "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:(sexp_location loc) - "Exception while conversion-checking types: %s and %s" - (lexp_string ltype) - (lexp_string ltype'); - raise e) + raise e + in + if + try OL.conv_p (ectx_to_lctx ctx) ltype ltype' with + | e + -> diagnostic_info + ~context:[display_lexp_details lxp] + (sexp_location 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 - fatal - ~print_action:(fun _ -> - List.iter print_indent_line [ - (match var with (_, Some n) -> n | _ -> "<anon>") - ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype - ]) - ~loc:(sexp_location loc) + diagnostic_fatal + ~context:[ + fun channel _ + -> fprintf + channel + ("\t> %s = %s !: %s\n" + ^^ "\t> because\n" + ^^ "\t> %s != %s\n") + (match var with (_, Some n) -> n | _ -> "<anon>") + (lexp_string lxp) + (lexp_string ltype) + (lexp_string ltype') + (lexp_string ltype)] + (sexp_location loc) "Type check error: ¡¡ctx_define error!!"

let ctx_extend (ctx: elab_context) (var : vname) def ltype = @@ -647,7 +642,7 @@ let rec elaborate ctx se ot =

and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!" + | (_, Checked) -> diagnostic_fatal (sexp_location p) "`infer` got Checked!" | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) | (e, Inferred t) -> (e, t)

@@ -659,7 +654,11 @@ and elab_special_form ctx f args ot = (get_special_form name) ctx loc args ot

| _ - -> lexp_error (sexp_location loc) f "Unknown special-form: %s" (lexp_string f); + -> diagnostic_error + ~context:[display_lexp_details f] + (sexp_location loc) + "Unknown special-form: %s" + (lexp_string f); sform_dummy_ret ctx loc

and elab_special_decl_form ctx f args = @@ -668,7 +667,13 @@ and elab_special_decl_form ctx f args = | Builtin ((_, name), _) -> (* Special form. *) (get_special_decl_form name) ctx loc args - | _ -> lexp_error (sexp_location loc) f "Unknown special-decl-form: %s" (lexp_string f); ctx + | _ + -> diagnostic_error + ~context:[display_lexp_details f] + (sexp_location loc) + "Unknown special-decl-form: %s" + (lexp_string f); + ctx

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -701,8 +706,13 @@ and sdform_instance (inst : bool) (ctx : elab_context) (_l : sinfo) sargs let (lxp, _) = infer sarg ctx in match lexp_lexp' lxp with | Var (_, idx) -> ectx_set_inst ctx idx inst - | _ -> (lexp_error (lexp_location lxp) lxp - "Only variables can be instances"; ctx) in + | _ + -> diagnostic_error + ~context:[display_lexp_details lxp] + (lexp_location lxp) + "Only variables can be instances"; + ctx + in List.fold_left make_instance ctx sargs

and infer_type pexp ectx (var: vname) = @@ -728,12 +738,19 @@ and infer_type pexp ectx (var: vname) = (ectx_to_lctx ectx) with | (_::_) -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in - match var with - | (l, None) - -> lexp_error (sexp_location l) t {|"%s" is not a proper type|} typestr - | (l, Some name) - -> lexp_error - (sexp_location l) t {|Type of "%s" is not a proper type: %s|} name typestr) + match var with + | (l, None) + -> diagnostic_error + ~context:[display_lexp_details t] + (sexp_location l) + {|"%s" is not a proper type|} + typestr + | (l, Some name) + -> diagnostic_error + ~context:[display_lexp_details t] + (sexp_location l) + {|Type of "%s" is not a proper type: %s|} + name typestr) | [] -> ()); t

@@ -751,8 +768,10 @@ and unify_with_arrow ctx tloc lxp kind var aty let arrow = mkArrow (l, kind, var, arg, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) - -> lexp_error - (sexp_location tloc) lxp {|Types:\n %s\n and:\n %s\n do not match!|} + -> diagnostic_error + ~context:[display_lexp_details lxp] + (sexp_location tloc) + {|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 @@ -763,8 +782,9 @@ 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 + -> diagnostic_error + ~context:[display_lexp_details lxp] + (lexp_location lxp) ({|Type mismatch%s! Context expected:\n%s|} ^^ {|\nbut %s has type:\n %s\n|} ^^ {|can't unify:\n %s\nwith:\n %s|}) @@ -799,30 +819,36 @@ 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:(sexp_location (pexp_pat_location pat)) + diagnostic_warning + (sexp_location (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 - - (* get target and its type *) - let tlxp, tltp = infer target ctx in - let tknd = OL.get_type (ectx_to_lctx ctx) tltp in - let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with - | Sort (_, Stype l) -> l - | _ -> fatal "Target lexp's kind is not a sort" in - let it_cs_as = ref None in - let ltarget = ref tlxp in + let check_uniqueness pat name map = + if SMap.mem name map then uniqueness_warn pat in + + (* get target and its type *) + let tlxp, tltp = infer target ctx in + let tknd = OL.get_type (ectx_to_lctx ctx) tltp in + let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with + | Sort (_, Stype l) -> l + | _ + -> diagnostic_fatal + (lexp_location tknd) + "Target lexp's kind is not a sort" + in + let it_cs_as = ref None in + let ltarget = ref tlxp in

let get_cs_as it' lctor = let unify_ind expected actual = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) - -> lexp_error - (sexp_location loc) lctor {|Expected pattern of type "%s", but got "%s"|} + -> diagnostic_error + ~context:[display_lexp_details lctor] + (sexp_location loc) + {|Expected pattern of type "%s", but got "%s"|} (lexp_string expected) (lexp_string actual) | [] -> () in match !it_cs_as with @@ -856,9 +882,11 @@ and check_case rtype (loc, target, ppatterns) ctx = -> assert (List.length fargs = List.length targs); constructors | _ - -> lexp_error - (sexp_location target) tlxp - {|Can't "case" on objects of type "%s"|} (lexp_string tltp); + -> diagnostic_error + ~context:[display_lexp_details tlxp] + (sexp_location target) + {|Can't "case" on objects of type "%s"|} + (lexp_string tltp); SMap.empty in it_cs_as := Some (it, constructors, targs); (constructors, targs) in @@ -913,8 +941,10 @@ and check_case rtype (loc, target, ppatterns) ctx = let cargs = try SMap.find cons_name constructors with | Not_found - -> lexp_error - loc lctor {|"%s" does not a have a "%s" constructor|} + -> diagnostic_error + ~context:[display_lexp_details lctor] + loc + {|"%s" does not a have a "%s" constructor|} (lexp_string it') cons_name; [] in

@@ -935,8 +965,10 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx ctx s pargs cargs SMap.empty acc | [], [] -> ctx, List.rev acc | (_, _pat)::_, [] - -> lexp_error loc lctor - "Too many pattern args to the constructor"; + -> diagnostic_error + ~context:[display_lexp_details lctor] + loc + "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc | (_, (ak, (_, Some fname), fty)::cargs) when SMap.mem fname pe @@ -982,7 +1014,12 @@ and check_case rtype (loc, target, ppatterns) ctx = dflt (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it * and try again with the result. *) - | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt + | _ + -> diagnostic_error + ~context:[display_lexp_details lctor] + loc + "Not a constructor"; + lbranches, dflt in

match pat with @@ -1013,17 +1050,17 @@ and elab_macro_call | Some t -> t in

- if !macro_tracing_enabled - then - (trace_macro ~location:(sexp_location location) {|expanding: %s|} (lexp_string func); - List.iteri - (fun i arg -> - arg |> sexp_string |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) - args); + let location' = sexp_location location in + macro_diagnostic_info location' {|expanding: %s|} (lexp_string func); + List.iteri + (fun i arg -> + arg + |> sexp_string + |> macro_diagnostic_info location' {|input %d: %s|} i) + args;

let sxp = lexp_expand_macro location func args ctx (Some t) in - if !macro_tracing_enabled - then trace_macro ~location:(sexp_location location) {|output: %s|} (sexp_string sxp); + macro_diagnostic_info location' {|output: %s|} (sexp_string sxp);

elaborate ctx sxp ot

@@ -1077,8 +1114,10 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = 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|} + diagnostic_error + ~context:[display_lexp_details func] + loc + {|Explicit actual args "%s" have no matching formal args|} (String.concat ", " (List.map fst pending))); largs, ltp

@@ -1166,18 +1205,22 @@ 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 "%s" is not closed: %s|} + diagnostic_error + ~context:[display_lexp_details e] + (lexp_location 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 -> - let eval_trace = fst (EV.get_trace ()) in - info ~print_action:(fun _ -> EV.print_eval_trace (Some eval_trace)) - "Exception happened during evaluation:"; - raise exc + try EV.eval ee rctx with + | exc + -> let eval_trace = fst (EV.get_trace ()) in + diagnostic_info + ~context:[fun _ _ -> EV.print_eval_trace (Some eval_trace)] + (lexp_location e) + "Exception happened during evaluation:"; + raise exc

-and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) +and lexp_expand_macro (loc : sinfo) macro_funct sargs ctx (_ot : ltype option) : sexp =

(* Build the function to be called *) @@ -1196,10 +1239,18 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO sexp" - (lexp_string macro_funct)) - | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO" - (lexp_string macro_funct) + | v + -> diagnostic_fatal + ~context:[display_value_details v] + (sexp_location loc) + "Macro `%s` should return an IO sexp" + (lexp_string macro_funct)) + | v + -> diagnostic_fatal + ~context:[display_value_details v] + (sexp_location loc) + "Macro `%s` should return an IO" + (lexp_string macro_funct)

(* Print each generated decls *) @@ -1319,7 +1370,7 @@ and lexp_decls_1 | 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 + diagnostic_error loc {|Variable "%s" declared but not defined!|} s else assert (pending_defs == []); [], [], [], nctx @@ -1346,24 +1397,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 "%s" incompatible with - previous "%s"|} + -> diagnostic_error + ~context:[display_lexp_details ltp] + loc + ({|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 "%s" already defined!|} vname; + (diagnostic_error loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) else recur [] (ectx_extend nctx (stp, Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ - -> error - ~loc {|Invalid type declaration syntax : "%s"|} + -> diagnostic_error + loc + {|Invalid type declaration syntax : "%s"|} (sexp_string thesexp); recur [] nctx pending_decls pending_defs)

@@ -1394,7 +1447,7 @@ and lexp_decls_1 recur [] nctx pending_decls pending_defs

else - (error ~loc {|"%s" defined but not declared!|} vname; + (diagnostic_error loc {|"%s" defined but not declared!|} vname; recur [] nctx pending_decls pending_defs)

| [Node (Symbol s, args) as d; body] @@ -1406,8 +1459,8 @@ and lexp_decls_1 nctx pending_decls pending_defs

| _ - -> error - ~loc {|Invalid definition syntax : "%s"|} (sexp_string thesexp); + -> diagnostic_error + loc {|Invalid definition syntax : "%s"|} (sexp_string thesexp); recur [] nctx pending_decls pending_defs)

| Some sexp @@ -1425,14 +1478,15 @@ and lexp_decls_1 let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( - error ~loc:(sexp_location sxp) "Invalid declaration syntax"; + diagnostic_error (sexp_location sxp) "Invalid declaration syntax"; recur [] nctx pending_decls pending_defs )

- in (EV.set_getenv nctx; - let res = lexp_decls_1 sdecls tokens nctx - pending_decls pending_defs in - (Log.stop_on_error (); res)) + in + EV.set_getenv nctx; + let res = lexp_decls_1 sdecls tokens nctx pending_decls pending_defs in + Log.Diagnostics.stop_on_error (); + res

(* Why is the return value a list of list? - each `(vname * lexp * ltype)` is a definition @@ -1448,17 +1502,20 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) | _ -> let decls, sdecls, tokens, nctx = lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in - Log.stop_on_error (); + Log.Diagnostics.stop_on_error (); let declss, nnctx = impl sdecls tokens nctx in decls :: declss, nnctx in impl sdecls tokens ctx

and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in - (Log.stop_on_error (); res) + Log.Diagnostics.stop_on_error (); + res

and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer e ctx in (Log.stop_on_error (); e) + let e, _ = infer e ctx in + Log.Diagnostics.stop_on_error (); + e

(* -------------------------------------------------------------------------- * Special forms implementation @@ -1467,19 +1524,29 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = and sform_declexpr ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e - -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc:(sexp_location loc) "no expr available"; - sform_dummy_ret ctx loc) - | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; + -> begin match + DB.env_lookup_expr + ctx + ((loc, U.get_vname_name_option (get_var_vname (get_var e))), + get_var_db_index (get_var e)) + with + | Some lxp -> (lxp, Lazy) + | None -> diagnostic_error (sexp_location loc) "no expr available"; + sform_dummy_ret ctx loc + end + | _ -> diagnostic_error (sexp_location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc

let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e - -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; + -> (DB.env_lookup_type + ctx + ((loc, U.get_vname_name_option (get_var_vname (get_var e))), + get_var_db_index (get_var e)), + Lazy) + | _ -> diagnostic_error (sexp_location loc) "decltype expects one argument"; sform_dummy_ret ctx loc

@@ -1501,14 +1568,19 @@ let sform_built_in ctx loc sargs ot = sexp_error (sexp_location loc) {|Unknown built-in "%s"|} name; BI.add_builtin_cst name bi; (bi, Checked) - | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; - sform_dummy_ret ctx loc) - - | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; - sform_dummy_ret ctx loc + | None + -> diagnostic_error + (sexp_location loc) + "Built-in's type not provided by context!"; + sform_dummy_ret ctx loc) + + | true, _ + -> diagnostic_error (sexp_location loc) "Wrong Usage of `Built-in`"; + sform_dummy_ret ctx loc

- | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; - sform_dummy_ret ctx loc + | false, _ + -> diagnostic_error (sexp_location loc) "Use of `Built-in` in user code"; + sform_dummy_ret ctx loc

let sform_datacons ctx loc sargs _ot = match sargs with @@ -1537,10 +1609,12 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = -> (elab_colon_to_ak k, (arg, Some name), Some e) | Symbol (_l, name) -> (Anormal, (arg, Some name), None) - | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) - (sexp_location arg) - "Unrecognized formal arg"; - (Anormal, (arg, None), None) + | _ + -> diagnostic_error + ~context:[fun _ _ -> sexp_print arg; print_newline ()] + (sexp_location arg) + "Unrecognized formal arg"; + (Anormal, (arg, None), None)

let sform_typecons ctx loc sargs _ot = match sargs with @@ -1667,13 +1741,16 @@ let sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" - ^^ " repeated at a different scope level!") + diagnostic_fatal + (sexp_location loc) + ("Bug in the elaboration of a metavar 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 - level! *) - fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" + (* FIXME: We face the same problem as above, but here, the situation + is worse, we don't even know the scope level! *) + -> diagnostic_fatal + (sexp_location loc) + "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -1683,9 +1760,13 @@ let sform_identifier ctx loc sargs ot = let mv = newShiftedInstanceMetavar ctx (loc, Some name) t in (if not (name = "") then let idx = - match lexp_lexp' mv with + match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in + | _ + -> diagnostic_fatal + (sexp_location loc) + "newMetavar returned a non-Metavar" + in rmmap := SMap.add name idx (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy)

@@ -1895,7 +1976,11 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] + -> diagnostic_error + (sexp_location 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 @@ -1907,8 +1992,12 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; - !sform_default_ectx) in + | _ + -> diagnostic_error + (sexp_location loc) + "argument to load should be one file name (String)"; + !sform_default_ectx + in

(* get lexp_context *) let usr_lctx = ectx_to_lctx usr_elctx in @@ -2000,8 +2089,9 @@ let default_ectx let idx = senv_lookup name elctx in let v = mkVar ((dsinfo, Some name), idx) in BI.set_predef name v) BI.predef_names; - with Senv_Lookup_Fail _ -> - warning "Predef not found"; in + with + | Senv_Lookup_Fail _ -> trace_warning __POS__ "Predef not found" + in

(* Empty context *) let lctx = empty_elab_context in @@ -2030,11 +2120,11 @@ let default_ectx let ectx = DB.ectx_set_inst_def ectx true in let _ = sform_default_ectx := ectx in ectx - with e -> - error "Compilation stopped in default context"; - Log.print_log (); - Log.clear_log (); - raise e + with + | e + -> trace_warning __POS__ "Compilation stopped in default context"; + Log.Diagnostics.print_log (); + raise e

let default_rctx = EV.from_ectx default_ectx

@@ -2045,7 +2135,8 @@ let lexp_expr_str str ctx = let tenv = default_stt in let grm = ectx_get_grammar ctx in let limit = Some ";" in - let source = new Source.source_string str in + let container = Source.Container.String ("<unknown>", str) in + let source = new Source.source_string ~container str in let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in List.iter (fun lxp -> @@ -2056,7 +2147,8 @@ let lexp_expr_str str ctx =

let lexp_decl_str str ctx = let tenv = default_stt in - let source = new Source.source_string str in + let container = Source.Container.String ("<unknown>", str) in + let source = new Source.source_string ~container str in let tokens = lex_source source tenv in lexp_p_decls [] tokens ctx

@@ -2091,6 +2183,4 @@ let process_file List.iter backend#process_decls ldecls; ectx' with - | Sys_error _ - -> (error {|file %s does not exist.|} file_name; - ectx) + | Sys_error _ -> Log.user_error {|file %s does not exist.|} file_name

===================================== src/env.ml ===================================== @@ -44,18 +44,14 @@ module DB = Debruijn

let dloc = Util.dummy_location

-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 {trace_fatal; trace_warning; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "ENV"

-let str_idx idx = "[" ^ (string_of_int idx) ^ "]" - -type value_type = +type value = | Vint of int | Vinteger of BI.t | Vstring of string - | Vcons of symbol * value_type list + | Vcons of symbol * value list | Vbuiltin of string | Vfloat of float | Closure of vname * elexp * runtime_env @@ -65,13 +61,15 @@ type value_type = | Vtype of L.lexp (* The lexp value can't be trusted. *) | Vin of in_channel | Vout of out_channel - | Vcommand of (unit -> value_type) - | Vref of (value_type ref) + | Vcommand of (unit -> value) + | Vref of (value ref) | Velabctx of DB.elab_context - | Varray of (value_type array) + | Varray of (value array)

(* Runtime Environ *) - and runtime_env = (vname * (value_type ref)) M.myers + and runtime_env = (vname * (value ref)) M.myers + +type value_type = value

let rec value_equal a b = match a, b with @@ -85,14 +83,14 @@ let rec value_equal a b = | Vout (_c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 | Vundefined, _ | _, Vundefined - -> warning "Vundefined"; + -> trace_warning __POS__ "Vundefined"; false | Vtype _e1, Vtype _e2 - -> warning "Vtype"; + -> trace_warning __POS__ "Vtype"; false

| Closure (s1, _b1, _ctx1), Closure (s2, _b2, _ctx2) - -> warning "Closure"; + -> trace_warning __POS__ "Closure"; if s1 != s2 then false else true

| Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) @@ -171,6 +169,25 @@ let rec value_string v =

let value_print (vtp: value_type) = print_string (value_string vtp)

+let display_line = Fmt.make_line '-' 80 ^ "\n" + +let display_values + ~(label : string) + (values : value_type list) + (channel : out_channel) + (_ : Fmt.colorize) + : unit = + + let display_value value = + value + |> value_string + |> fprintf channel "\t%s\n"; + in + + fprintf channel "--- %-72s ---\n" label; + List.iter display_value values; + output_string channel display_line + let make_runtime_ctx = M.nil

let get_rte_size (ctx: runtime_env): int = M.length ctx @@ -218,14 +235,15 @@ let get_rte_variable (name: vname) (idx: int) -> if n1 = n2 then x else - fatal - ~print_action:(fun () -> dump_rte_ctx ctx) + trace_fatal + ~context:[fun _ _ -> dump_rte_ctx ctx] + __POS__ {|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 + trace_fatal __POS__ {|Variable lookup failure. Var: "%s" idx: %d|} n idx

let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) : runtime_env = @@ -237,7 +255,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) =

(match (n, name) with | ((_, Some n1), (_, Some n2)) when n1 != n2 - -> fatal {|Variable names must match: "%s" vs "%s"|} n1 n2 + -> trace_fatal __POS__ {|Variable names must match: "%s" vs "%s"|} n1 n2 | _ -> ());

ref_cell := v

===================================== src/eval.ml ===================================== @@ -47,6 +47,12 @@ module OL = Opslexp module Lexer = Lexer (* lex *) module Prelexer = Prelexer (* prelex_string *)

+let {trace_fatal; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "EVAL" + +let {diagnostic_fatal; diagnostic_warning; diagnostic_info; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "EVAL"

type eval_debug_info = elexp list * elexp list

@@ -80,23 +86,6 @@ let rec_depth trace = let (_a, b) = trace in List.length b

-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: * * [Ln 8, cl 6] ./samples/error.typer @@ -152,7 +141,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 {|"%s" expects 2 Int arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Int arguments|} name in add_builtin_function name f 2

let add_binary_iop_with_loc name f = @@ -160,7 +149,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 {|"%s" expects 2 Int arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Int arguments|} name in add_builtin_function name f 2

let add_with_overflow loc a b = @@ -169,7 +158,7 @@ let add_with_overflow loc a b = same as the sign of the args. *) if (a lxor b) lor (a lxor (lnot c)) < 0 then c - else error loc "Overflow in `Int.+`" + else diagnostic_fatal loc "Overflow in `Int.+`"

let sub_with_overflow loc a b = let c = a - b in @@ -177,32 +166,32 @@ let sub_with_overflow loc a b = the same as the sign of the first arg. *) if (a lxor (lnot b)) lor (a lxor (lnot c)) < 0 then c - else error loc "Overflow in `Int.-`" + else diagnostic_fatal loc "Overflow in `Int.-`"

let mul_with_overflow loc a b = let c = a * b in if b = 0 || not (c = min_int && b = -1) && a = c / b (* Simple but slow *) then c - else error loc "Overflow in `Int.*`" + else diagnostic_fatal loc "Overflow in `Int.*`"

let div_with_overflow loc a b = if not (a = min_int && b = -1) then a / b - else error loc "Overflow in `Int./`" + else diagnostic_fatal loc "Overflow in `Int./`"

let lsl_with_shift_check loc a b = if b < 0 || b > Sys.int_size - then error loc {|Invalid shift value %d in "Int.lsl"|} b + then diagnostic_fatal 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 %d in "Int.lsr"|} b + then diagnostic_fatal 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 %d in "Int.ast"|} b + then diagnostic_fatal loc {|Invalid shift value %d in "Int.ast"|} b else a asr b

let _ = add_binary_iop_with_loc "+" add_with_overflow; @@ -224,7 +213,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 {|"%s" expects 2 Int arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Int arguments|} name in add_builtin_function name f 2

let _ = add_binary_bool_iop "<" (<); @@ -238,7 +227,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 {|"%s" expects 1 Int arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 1 Int arguments|} name in add_builtin_function name f 1

(* True integers (aka Z). *) @@ -248,7 +237,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 {|"%s" expects 2 Integer arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Integer arguments|} name in add_builtin_function name f 2

let _ = add_binary_biop "+" BI.add; @@ -261,7 +250,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 {|"%s" expects 2 Integer arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Integer arguments|} name in add_builtin_function name f 2

let _ = add_binary_bool_biop "<" BI.lt; @@ -275,7 +264,7 @@ 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 {|"%s" expects 1 Int argument|} name) + | _ -> diagnostic_fatal loc {|"%s" expects 1 Int argument|} name) 1; let name = "Integer->Int" in add_builtin_function @@ -284,8 +273,10 @@ let _ = add_binary_bool_biop "<" BI.lt; -> match args_val with | [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) + | Z.Overflow + -> diagnostic_fatal loc {|Overflow in "%s"|} name) + | _ + -> diagnostic_fatal loc {|"%s" expects 1 Integer argument|} name) 1

(* Floating point numers. *) @@ -294,7 +285,7 @@ let add_binary_fop name f = let name = "Float." ^ name in let f loc (_depth : eval_debug_info) = function | [Vfloat v; Vfloat w] -> Vfloat (f v w) - | _ -> error loc {|"%s" expects 2 Float arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Float arguments|} name in add_builtin_function name f 2

let _ = add_binary_fop "+" (+.); @@ -306,7 +297,7 @@ let add_binary_bool_fop name f = let name = "Float." ^ name in let f loc (_depth : eval_debug_info) = function | [Vfloat v; Vfloat w] -> o2v_bool (f v w) - | _ -> error loc {|"%s" expects 2 Float arguments|} name in + | _ -> diagnostic_fatal loc {|"%s" expects 2 Float arguments|} name in add_builtin_function name f 2

let _ = add_binary_bool_fop "<" (<); @@ -318,12 +309,12 @@ let _ = add_binary_bool_fop "<" (<); let _ = let name = "Float." ^ "trunc" in let f loc (_depth : eval_debug_info) = function | [Vfloat v] -> Vfloat ( snd (modf v) ) - | _ -> error loc {|"%s" expects 1 Float argument|} name in + | _ -> diagnostic_fatal 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 | [Vstring str] -> Vsexp (Symbol (loc, str)) - | _ -> error loc "Sexp.symbol expects one string as argument" + | _ -> diagnostic_fatal loc "Sexp.symbol expects one string as argument"

let make_node loc _depth args_val = match args_val with | [Vsexp (op); lst] @@ -331,65 +322,71 @@ let make_node loc _depth args_val = match args_val with let unwrap_sexp = function | Vsexp (sexp) -> sexp | v - -> error + -> diagnostic_fatal 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`" + | _ -> diagnostic_fatal loc "Sexp.node expects a `Sexp` and a `List Sexp`"

let make_string loc _depth args_val = match args_val with | [Vstring str] -> Vsexp (String (loc, str)) - | _ -> error loc "Sexp.string expects one string as argument" + | _ -> diagnostic_fatal loc "Sexp.string expects one string as argument"

let make_integer loc _depth args_val = match args_val with | [Vinteger n] -> Vsexp (Integer (loc, n)) - | _ -> error loc "Sexp.integer expects one integer as argument" + | _ -> diagnostic_fatal loc "Sexp.integer expects one integer as argument"

let make_float loc _depth args_val = match args_val with | [Vfloat x] -> Vsexp (Float (loc, x)) - | _ -> error loc "Sexp.float expects one float as argument" + | _ -> diagnostic_fatal loc "Sexp.float expects one float as argument"

let make_block loc _depth args_val = match args_val with (* From what would we like to make a block? *) | [Vstring str] - -> let source = new Source.source_string str in + -> let container = Source.Container.String ("<make-block>", str) in + let source = new Source.source_string ~container str in Vsexp (Block (loc, (Prelexer.prelex source))) - | _ -> error loc "Sexp.block expects one string as argument" + | _ -> diagnostic_fatal loc "Sexp.block expects one string as argument"

let reader_parse loc _depth = function | [Velabctx ectx; Vsexp (Block (_, toks))] -> let grm = ectx_get_grammar ectx in let tokens = Lexer.lex default_stt toks in o2v_list (sexp_parse_all_to_list grm tokens (Some ";")) - | [Velabctx _; s] -> (warning loc "Reader.parse do nothing without a Block"; s) - | _ -> error loc "Reader.parse expects an ElabContext and a Block as argument" + | [Velabctx _; s] + -> diagnostic_warning loc "Reader.parse do nothing without a Block"; + s + | _ + -> diagnostic_fatal + loc + "Reader.parse expects an ElabContext and a Block as argument"

let string_eq loc _depth args_val = match args_val with | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) - | _ -> error loc "String.= expects 2 strings" + | _ -> diagnostic_fatal loc "String.= expects 2 strings"

(* need either a character type or builtin string operation *) let string_concat loc _depth args_val = match args_val with | [Vstring s1; Vstring s2] -> Vstring (s1 ^ s2) - | _ -> error loc "String.concat expects 2 strings" + | _ -> diagnostic_fatal loc "String.concat expects 2 strings"

let string_sub loc _depth args_val = match args_val with | [Vstring s; Vint start; Vint len] -> Vstring (String.sub s start len) - | _ -> error loc "String.sub expects 1 string and 2 ints" + | _ -> diagnostic_fatal loc "String.sub expects 1 string and 2 ints"

let sexp_eq loc _depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) - | _ -> error loc "Sexp.= expects 2 sexps" + | _ -> diagnostic_fatal loc "Sexp.= expects 2 sexps"

let sexp_debug_print loc _depth args_val = match args_val with | [Vsexp (s1)] -> (let tstr = sexp_name s1 in (print_string ("\n\t"^tstr^" : ["^(sexp_string s1)^"]\n\n") ; Vcommand (fun () -> Vsexp (s1)))) - | _ -> error loc "Sexp.debug_print expects 1 sexps" + | _ -> diagnostic_fatal loc "Sexp.debug_print expects 1 sexps"

let file_open loc _depth args_val = match args_val with | [Vstring (file); Vstring (mode)] -> @@ -398,28 +395,30 @@ let file_open loc _depth args_val = match args_val with match mode with | "r" -> Vin (open_in file) | "w" -> Vout (open_out file) - | _ -> error loc "wrong open mode") + | _ -> diagnostic_fatal loc "wrong open mode")

- | _ -> error loc "File.open expects 2 strings" + | _ -> diagnostic_fatal loc "File.open expects 2 strings"

-let file_read loc _depth args_val = match args_val with +let file_read loc _depth = function (* FIXME: Either rename it to "readline" and drop the second arg, * or actually pay attention to the second arg. *) | [Vin channel; Vint _n] -> Vstring (input_line channel) - | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; - ) - "File.read expects an in_channel. Actual arguments:" + | args + -> diagnostic_fatal + ~context:[Env.display_values ~label:"Arguments File.read" args] + loc + "File.read expects an in_channel."

-let file_write loc _depth args_val = match args_val with +let file_write loc _depth = function | [Vout channel; Vstring msg] -> Vcommand (fun () -> fprintf channel "%s" msg; (* FIXME: This should be the unit value! *) Vundefined) - | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; - ) - "File.write expects an out_channel and a string. Actual arguments:" + | args + -> diagnostic_fatal + ~context:[Env.display_values ~label:"Arguments to File.write" args] + loc + "File.write expects an out_channel and a string."

let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) =

@@ -465,8 +464,11 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (* Proj *) | Proj (loc, e, i) -> (match eval' e ctx with - | Vcons (_, vtl) -> List.nth vtl i - | _ -> error loc "Proj on a non-datatype constructor: %s \n" + | Vcons (_, vtl) -> List.nth vtl i + | _ + -> diagnostic_fatal + loc + "Proj on a non-datatype constructor: %s \n" (elexp_string e)) (* Case *) | Case (loc, target, pat, dflt) @@ -494,8 +496,8 @@ and eval_var ctx lxp v = try get_rte_variable vname idx ctx with | _e - -> Log.log_fatal - ~loc:(sexp_location loc) + -> diagnostic_fatal + (sexp_location loc) "Variable: %s%d was not found\n%s" (L.maybename name) idx (trace_elexp lxp)

@@ -529,7 +531,7 @@ and eval_call loc unef i f args = | 0, _ -> let v = eval_call loc unef i f (List.rev acc) in eval_call loc unef i v vs | _, (v::vs) -> split (n - 1) vs (v::acc) - | _ -> error loc "Impossible!" + | _ -> trace_fatal __POS__ ~loc "Impossible!" in split nargs args [] else let rec buildctx args ctx = match args with @@ -549,9 +551,9 @@ and eval_call loc unef i f args =

with | Not_found - -> error loc {|Requested Built-in "%s" does not exist|} name + -> diagnostic_fatal loc {|Requested Built-in "%s" does not exist|} name | e - -> warning loc {|Exception thrown from primitive "%s"|} name; + -> diagnostic_warning loc {|Exception thrown from primitive "%s"|} name; raise e)

| Vtype e, _ @@ -559,7 +561,7 @@ and eval_call loc unef i f args = * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) -> Vtype (L.mkCall (dsinfo, e, [(Anormal, mkVar (vdummy, -1))])) - | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) + | _ -> diagnostic_fatal loc "Trying to call a non-function!\n%s" (trace_value f)

and eval_case ctx i loc target pat dflt = (* Eval target *) @@ -569,8 +571,8 @@ and eval_case ctx i loc target pat dflt = let ctor_name, args = match v with | Vcons((_, cname), args) -> cname, args | _ - -> error - loc {|Target "%s" is not a Constructor\n%s|} + -> trace_fatal + __POS__ ~loc {|Target "%s" is not a Constructor\n%s|} (elexp_string target) (trace_value v) in

@@ -585,8 +587,12 @@ and eval_case ctx i loc target pat dflt = fold2 nctx pats args (* Errors: those should not happen but they might *) (* List.fold2 would complain. we print more info *) - | _::_, [] -> warning loc "a) Eval::Case Pattern Error"; nctx - | [], _::_ -> warning loc "b) Eval::Case Pattern Error"; nctx + | _::_, [] + -> trace_warning __POS__ ~loc "a) Eval::Case Pattern Error"; + nctx + | [], _::_ + -> trace_warning __POS__ ~loc "b) Eval::Case Pattern Error"; + nctx (* Normal case *) | [], [] -> nctx in

@@ -597,7 +603,7 @@ and eval_case ctx i loc target pat dflt = with Not_found -> (match dflt with | Some (var, lxp) -> eval lxp (add_rte_variable var v ctx) i - | _ -> error loc "Match Failure") + | _ -> diagnostic_fatal loc "Match Failure")

and build_arg_list args ctx i = (* eval every args *) @@ -634,12 +640,12 @@ and sexp_dispatch loc depth args = let sxp, nd, sym, str, it, flt, blk = match args with | [sxp; nd; sym; str; it; flt; blk] -> sxp, nd, sym, str, it, flt, blk - | _ -> error loc "sexp_dispatch expects 7 arguments" in + | _ -> diagnostic_fatal loc "sexp_dispatch expects 7 arguments" in

let sxp = match sxp with | Vsexp(sxp) -> sxp | _ - -> fatal + -> diagnostic_fatal loc "sexp_dispatch expects a Sexp as 1st arg\n%s" (trace_value sxp) in @@ -722,35 +728,42 @@ let io_bind loc depth args_val = match args_val with | [Vcommand cmd; callback] -> (* bind returns another Vcommand *) - Vcommand (fun () - -> match eval_call loc trace_dum depth callback [cmd ()] with - | Vcommand cmd -> cmd () - | _ -> error loc "IO.bind second arg did not return a command") - | _ -> error loc "Wrong number of args or wrong first arg value in `IO.bind`" + Vcommand + (fun () + -> match eval_call loc trace_dum depth callback [cmd ()] with + | Vcommand cmd -> cmd () + | _ + -> diagnostic_fatal + loc + "IO.bind second arg did not return a command") + | _ + -> diagnostic_fatal + loc + "Wrong number of args or wrong first arg value in `IO.bind`"

let io_run loc _depth args_val = match args_val with | [Vcommand cmd; v] -> let _ = cmd () in v - | _ -> error loc "IO.run expects a monad and a function as arguments" + | _ -> diagnostic_fatal loc "IO.run expects a monad and a function as arguments"

let io_return loc _depth args_val = match args_val with | [v] -> Vcommand (fun () -> v) - | _ -> error loc "IO.return takes a single argument" + | _ -> diagnostic_fatal loc "IO.return takes a single argument"

let float_to_string loc _depth args_val = match args_val with | [Vfloat x] -> Vstring (string_of_float x) - | _ -> error loc "Float->String expects one Float argument" + | _ -> diagnostic_fatal loc "Float->String expects one Float argument"

let int_to_string loc _depth args_val = match args_val with | [Vint x] -> Vstring (string_of_int x) - | _ -> error loc "Int->String expects one Int argument" + | _ -> diagnostic_fatal loc "Int->String expects one Int argument"

let integer_to_string loc _depth args_val = match args_val with | [Vinteger x] -> Vstring (BI.to_string x) - | _ -> error loc "Integer->String expects one Integer argument" + | _ -> diagnostic_fatal loc "Integer->String expects one Integer argument"

let sys_exit loc _depth args_val = match args_val with | [Vint n] -> Vcommand (fun _ -> exit n) - | _ -> error loc "Sys.exit takes a single Int argument" + | _ -> diagnostic_fatal loc "Sys.exit takes a single Int argument"

let y_operator loc _depth args = match args with @@ -766,42 +779,45 @@ let y_operator loc _depth args = Myers.nil)) in yf_ref := yf; yf - | _ -> error loc ("Y expects 1 (function) argument") + | _ -> diagnostic_fatal loc ("Y expects 1 (function) argument")

-let arity0_fun loc _ _ = error loc "Called a 0-arity function!?" +let arity0_fun loc _ _ = diagnostic_fatal loc "Called a 0-arity function!?" let nop_fun loc _ vs = match vs with | [v] -> v - | _ -> error loc "Wrong number of argument to nop" + | _ -> diagnostic_fatal loc "Wrong number of argument to nop"

let ref_make loc _depth args_val = match args_val with | [v] -> Vcommand (fun () -> Vref (ref v)) - | _ -> error loc "Ref.make takes a single value as argument" + | _ -> diagnostic_fatal loc "Ref.make takes a single value as argument"

let ref_read loc _depth args_val = match args_val with | [Vref (v)] -> Vcommand (fun () -> !v) - | _ -> error loc "Ref.read takes a single Ref as argument" + | _ -> diagnostic_fatal loc "Ref.read takes a single Ref as argument"

let ref_write loc _depth args_val = match args_val with | [value; Vref (actual)] -> Vcommand (fun () -> actual := value; tunit) - | _ -> error loc "Ref.write takes a value and a Ref as argument" + | _ -> diagnostic_fatal loc "Ref.write takes a value and a Ref as argument"

let gensym = let count = ref 0 in (fun loc _depth args_val -> match args_val with | [_v] -> Vcommand (fun () -> ( count := ((!count) + 1); Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" "))))) - | _ -> error loc "gensym takes a Unit as argument") + | _ -> diagnostic_fatal loc "gensym takes a Unit as argument")

let getenv loc _depth args_val = match args_val with | [_v] -> Vcommand (fun () -> Velabctx !macro_monad_elab_context) - | _ -> error loc "getenv takes a single Unit as argument" + | _ -> diagnostic_fatal loc "getenv takes a single Unit as argument"

let is_bound loc _depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (try (ignore (senv_lookup name ectx); true) with Senv_Lookup_Fail _ -> false) - | _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments" + | _ + -> diagnostic_fatal + loc + "Elab.isbound takes an Elab_Context and a String as arguments"

let constructor_p name ectx = try let idx = senv_lookup name ectx in @@ -893,46 +909,73 @@ let ctor_arg_pos name arg ectx =

let is_constructor loc _depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) - | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments" + | _ + -> diagnostic_fatal + loc + "Elab.isconstructor takes a String and an Elab_Context as arguments"

let is_nth_erasable loc _depth args_val = match args_val with | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx) - | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments" + | _ + -> diagnostic_fatal + loc + "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments"

let is_arg_erasable loc _depth args_val = match args_val with | [Vstring t; Vstring arg; Velabctx ectx] -> o2v_bool (erasable_p2 t arg ectx) - | _ -> error loc "Elab.is-arg-erasable takes two String and an Elab_Context as arguments" + | _ + -> diagnostic_fatal + loc + "Elab.is-arg-erasable takes two String and an Elab_Context as arguments"

let nth_arg loc _depth args_val = match args_val with | [Vstring t; Vint nth; Velabctx ectx] -> Vstring (nth_ctor_arg t nth ectx) - | _ -> error loc "Elab.nth-arg takes a String, an Int and an Elab_Context as arguments" + | _ + -> diagnostic_fatal + loc + "Elab.nth-arg takes a String, an Int and an Elab_Context as arguments"

let arg_pos loc _depth args_val = match args_val with | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx) - | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments" + | _ + -> diagnostic_fatal + loc + "Elab.arg-pos takes two String and an Elab_Context as arguments"

let array_append loc _depth args_val = match args_val with | [v; Varray a] -> Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) - | _ -> error loc "Array.append takes a value followed by an Array as arguments" + | _ + -> diagnostic_fatal + loc + "Array.append takes a value followed by an Array as arguments"

let array_create loc _depth args_val = match args_val with | [Vint len; v] -> Varray (Array.make len v) - | _ -> error loc "Array.make takes an Int and a value and as arguemnts" + | _ + -> diagnostic_fatal + loc + "Array.make takes an Int and a value and as arguemnts"

let array_length loc _depth args_val = match args_val with | [Varray a] -> Vint (Array.length a) - | _ -> error loc "Array.length takes an Array as argument" + | _ -> diagnostic_fatal loc "Array.length takes an Array as argument"

let array_set loc _depth args_val = match args_val with - | [Vint idx; v; Varray a] -> if (idx > (Array.length a) || idx < 0) - then - (warning loc "Array.set index out of bounds (array unchanged)"; - (Varray a)) - else - let copy = (Array.map (fun v -> v) a) in - (Array.set copy idx v; Varray copy) - | _ -> error loc "Array.set takes an Int, a value and an Array as arguments" + | [Vint idx; v; Varray a] + -> if (idx > (Array.length a) || idx < 0) + then + (diagnostic_warning + loc + "Array.set index out of bounds (array unchanged)"; + Varray a) + else + let copy = (Array.map (fun v -> v) a) in + (Array.set copy idx v; Varray copy) + | _ + -> diagnostic_fatal + loc + "Array.set takes an Int, a value and an Array as arguments"

let array_get loc _depth args_val = match args_val with | [dflt; Vint idx; Varray a] -> if (idx >= (Array.length a)) || (idx < 0) @@ -940,7 +983,10 @@ let array_get loc _depth args_val = match args_val with dflt else Array.get a idx - | _ -> error loc "Array.get takes a default value, an Int and an Array as arguments" + | _ + -> diagnostic_fatal + loc + "Array.get takes a default value, an Int and an Array as arguments"

(* Vundefined is used in array_empty because we have no default value @@ -948,36 +994,26 @@ let array_get loc _depth args_val = match args_val with *) let array_empty loc _depth args_val = match args_val with | [_] -> Varray (Array.make 0 Vundefined) - | _ -> error loc "Array.empty takes a Unit as single argument" + | _ -> diagnostic_fatal loc "Array.empty takes a Unit as single argument"

let test_fatal loc _depth args_val = match args_val with - | [Vstring section; Vstring msg] -> - Vcommand (fun () -> - Log.print_entry - (Log.mkEntry Log.Fatal ~kind:"(Unit test fatal)" ~loc ~section msg); - Log.user_error "%s" msg - ) - | _ -> error loc "Test.fatal takes two String as argument" + | [Vstring section; Vstring msg] + -> Vcommand (fun () -> diagnostic_fatal loc "[%s] %s" section msg) + | _ -> diagnostic_fatal loc "Test.fatal takes two String as argument"

let test_warning loc _depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> - Log.print_entry - (Log.mkEntry Log.Warning ~kind:"(Unit test warning)" ~loc ~section msg); - tunit) - | _ -> error loc "Test.warning takes two String as argument" + Vcommand (fun () -> diagnostic_warning loc "[%s] %s" section msg; tunit) + | _ -> diagnostic_fatal loc "Test.warning takes two String as argument"

let test_info loc _depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> - Log.print_entry - (Log.mkEntry Log.Info ~kind:"(Unit test Info)" ~loc ~section msg); - tunit) - | _ -> error loc "Test.info takes two String as argument" + Vcommand (fun () -> diagnostic_info loc "[%s] %s" section msg; tunit) + | _ -> diagnostic_fatal loc "Test.info takes two String as argument"

let test_location loc _depth args_val = match args_val with | [_] -> Vstring (Source.Location.to_string loc) - | _ -> error loc "Test.location takes a Unit as argument" + | _ -> diagnostic_fatal loc "Test.location takes a Unit as argument"

let test_true loc _depth args_val = match args_val with | [Vstring name; Vcons ((_dloc, b), [])] -> @@ -987,7 +1023,7 @@ let test_true loc _depth args_val = match args_val with else Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); tfalse) - | _ -> error loc "Test.true takes a String and a Bool as argument" + | _ -> diagnostic_fatal loc "Test.true takes a String and a Bool as argument"

let test_false loc _depth args_val = match args_val with | [Vstring name; Vcons ((_dloc, b), [])] -> @@ -997,7 +1033,7 @@ let test_false loc _depth args_val = match args_val with else Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); tfalse) - | _ -> error loc "Test.false takes a String and a Bool as argument" + | _ -> diagnostic_fatal loc "Test.false takes a String and a Bool as argument"

let test_eq loc _depth args_val = match args_val with | [Vstring name; v0; v1] -> if Env.value_equal v0 v1 then @@ -1006,7 +1042,7 @@ let test_eq loc _depth args_val = match args_val with else Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); tfalse) - | _ -> error loc "Test.eq takes a String and two values as argument" + | _ -> diagnostic_fatal loc "Test.eq takes a String and two values as argument"

let test_neq loc _depth args_val = match args_val with | [Vstring name; v0; v1] -> if Env.value_equal v0 v1 then @@ -1015,16 +1051,18 @@ let test_neq loc _depth args_val = match args_val with else Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); ttrue) - | _ -> error loc "Test.neq takes a String and two values as argument" + | _ + -> diagnostic_fatal loc "Test.neq takes a String and two values as argument"

let typelevel_succ loc (_depth : eval_debug_info) (args_val: value_type list) = - match args_val with - | [Vint v] -> Vint(v + 1) - | _ -> error loc ("`Typlevel.succ` expects 1 TypeLevel argument") + match args_val with + | [Vint v] -> Vint(v + 1) + | _ -> diagnostic_fatal loc ("`Typlevel.succ` expects 1 TypeLevel argument") + let typelevel_lub loc (_depth : eval_debug_info) (args_val: value_type list) = - match args_val with - | [Vint v1; Vint v2] -> Vint(max v1 v2) - | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2") + match args_val with + | [Vint v1; Vint v2] -> Vint(max v1 v2) + | _ -> diagnostic_fatal loc ("`Typlevel.⊔` expects 2 TypeLevel argument2")

let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) @@ -1090,7 +1128,7 @@ let builtin_constant v loc _depth args_val = match args_val with * *constant* (except for cases like Eq.refl where the contant is not * actually used). *) | [_] -> v - | _ -> error loc "Builtin almost-constant takes a unit argument" + | _ -> diagnostic_fatal loc "Builtin almost-constant takes a unit argument"

let register_builtin_constants () = List.iter (fun (name, v) -> add_builtin_function name (builtin_constant v) 1) @@ -1102,17 +1140,19 @@ let _ = register_builtin_constants ()

let eval lxp ctx = eval lxp ctx ([], [])

-let debug_eval lxp ctx = - try eval lxp ctx - with e -> ( - let ectx = !global_eval_ctx in - let eval_trace = fst (get_trace ()) in - Log.log_info ~section:"EVAL" ~print_action:(fun _ -> - print_rte_ctx ectx; - print_eval_trace (Some eval_trace) - ) - "Exception occured during evaluation in the following context:"; - raise e) +let debug_eval (lxp : elexp) ctx : value = + try eval lxp ctx with + | e + -> let ectx = !global_eval_ctx in + let eval_trace = fst (get_trace ()) in + diagnostic_info + ~context:[ + fun _ _ + -> print_rte_ctx ectx; + print_eval_trace (Some eval_trace)] + (elexp_location lxp) + "Exception occured during evaluation."; + raise e

let eval_decls decls ctx = eval_decls decls ctx ([], [])

===================================== src/fmt.ml ===================================== @@ -81,5 +81,25 @@ let magenta = string_of_format magenta_f let cyan = string_of_format cyan_f let reset = string_of_format reset_f

-let color_string color str = - color ^ str ^ reset +module Color = struct + type t = + | None + | Red + | Green + | Yellow + | Magenta + | Cyan + + let to_string : t -> string = function + | None -> reset + | Red -> red + | Green -> green + | Yellow -> yellow + | Magenta -> magenta + | Cyan -> cyan +end + +type colorize = Color.t -> string -> string + +let colorize : colorize = fun color text -> + Color.to_string color ^ text ^ reset

===================================== src/gambit.ml ===================================== @@ -26,6 +26,9 @@ open Elexp type ldecls = Lexp.ldecls type lexp = Lexp.lexp

+let {trace_info; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "GAMBIT" + let gsc_path : string ref = ref "/usr/local/Gambit/bin/gsc"

module Scm = struct @@ -285,6 +288,7 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp)

class inferior script_path = + let _ = trace_info __POS__ "Starting inferior Gambit" in let down_reader, down_writer = Unix.pipe ~cloexec:true () in let up_reader, up_writer = Unix.pipe ~cloexec:true () in let _ = Unix.clear_close_on_exec down_reader in @@ -299,6 +303,7 @@ class inferior script_path = in let _ = Unix.close down_reader in let _ = Unix.close up_writer in + let _ = trace_info __POS__ "Started inferior Gambit with pid %d" pid in

object (self) val pid = pid

===================================== src/heap.ml ===================================== @@ -34,8 +34,9 @@ type value = Env.value_type type size = int type addr = int

-let error ~(loc : location) ?print_action fmt = - Log.log_fatal ~section:"HEAP" ~loc ?print_action fmt +let {diagnostic_fatal; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "HEAP"

let dloc = Util.dummy_location let type0 = Debruijn.type0 @@ -81,7 +82,11 @@ let store_header | Env.Vcons (symbol, []) -> let constructor, _ = IMap.find address !heap in constructor := Some symbol - | _ -> error ~loc "not a data constructor: %s" (Env.value_string datacons) + | _ + -> diagnostic_fatal + 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. *) @@ -99,46 +104,47 @@ let datacons_label_of_string : builtin_function = fun loc _ -> function | [Vstring _ as label] -> label - | _ -> error ~loc "`datacons-label<-string` expects [##DataconsLabel]." + | _ + -> diagnostic_fatal loc "`datacons-label<-string` expects [##DataconsLabel]."

let heap_alloc : builtin_function = fun loc _ -> function | [Vint size] -> Vcommand (fun () -> Vint (alloc size)) - | _ -> error ~loc "`Heap.alloc` expects [Int]." + | _ -> diagnostic_fatal loc "`Heap.alloc` expects [Int]."

let heap_free : builtin_function = fun loc _ -> function | [Vint address] -> Vcommand (fun () -> free address; Vint 0) - | _ -> error ~loc "`Heap.free` expects [Int]." + | _ -> diagnostic_fatal loc "`Heap.free` expects [Int]."

let heap_export : builtin_function = fun loc _ -> function | [Vint address] -> Vcommand (fun () -> export address) - | _ -> error ~loc "`Heap.export` expects [Int]." + | _ -> diagnostic_fatal loc "`Heap.export` expects [Int]."

let heap_store_header : builtin_function = fun loc _ -> function | [Vint address; datacons] -> Vcommand (fun () -> store_header loc address datacons; Vint 0) - | _ -> error ~loc "`Heap.store-header` expects [Int; 'a]" + | _ -> diagnostic_fatal loc "`Heap.store-header` expects [Int; 'a]"

let heap_store_cell : builtin_function = fun loc _ -> function | [Vint address; Vint cell_index; value] -> Vcommand (fun () -> store_cell address cell_index value; Vint 0) - | _ -> error ~loc "`Heap.store-header` expects [Int; Int; 'a]" + | _ -> diagnostic_fatal loc "`Heap.store-header` expects [Int; Int; 'a]"

let heap_load_cell : builtin_function = fun loc _ -> function | [Vint address; Vint cell_index; _value] -> Vcommand (fun () -> load_cell address cell_index) - | _ -> error ~loc "`Heap.store-cell` expects [Int; Int]" + | _ -> diagnostic_fatal loc "`Heap.store-cell` expects [Int; Int]"

let register_builtins () = add_builtin_cst "DataconsLabel" type_datacons_label;

===================================== src/instargs.ml ===================================== @@ -27,19 +27,20 @@ module Unif = Unification open Printf open Sexp

+let section : string = "INSTARGS" + +let {trace_info; trace_debug; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions section + +let {diagnostic_error; _} : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions section + (** If true, log all the matching instances when resolving. *) let debug_list_all_candidates = ref false

(** Optionnally limit resolution recursion depth. *) let recursion_limit = ref (Some 100)

-(** Some variables may be skipped during instance resolution if - unification returns residual constraints (i.e. at this point during - inference, we do not have enough info to confirm or rule out a - match). If set to `some lvl`, log a message at level `lvl` when - that happens. *) -let log_skipped_uncertain_matches = ref (Some Log.Warning) - let metavar_resolution_contexts = ref (U.IMap.empty : (DB.elab_context * sinfo) U.IMap.t)

@@ -114,7 +115,11 @@ let try_match t1 t2 lctx sl =

let search_instance (instantiate_implicit) (ctx : DB.elab_context) (loc : sinfo) (t : L.ltype) : L.lexp option = - Log.log_debug ~loc:(sexp_location loc) "Resolving type `%s`" (L.lexp_string t); + trace_debug + __POS__ + ~loc:(sexp_location loc) + "Resolving type `%s`" + (L.lexp_string t); let lctx = DB.ectx_to_lctx ctx in let (_, _, insts) = DB.ectx_to_tcctx ctx in

@@ -134,7 +139,9 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) let var = L.mkVar ((loc,namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc:(sexp_location loc) + trace_debug + __POS__ + ~loc:(sexp_location loc) "Considering potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t); (* All candidates should have a type that is a typeclass. *) @@ -148,28 +155,36 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) match try_match t t' lctx sl with | Impossible -> None | Possible -> - (match !log_skipped_uncertain_matches with - | Some level -> - Log.log_msg ignore level ~loc:(sexp_location loc) - "Skipping potential instance `%s : %s` while resolving for `%s`" - (L.lexp_string var) (L.lexp_string t') - (L.lexp_string t) - | None -> ()); + trace_info + __POS__ + ~loc:(sexp_location loc) + "Skipping potential instance `%s : %s` while resolving for `%s`" + (L.lexp_string var) (L.lexp_string t') + (L.lexp_string t); None | Match -> Some (i, elem, e) in

let candidates = DB.env_lookup_set insts lctx |> Seq.filter_map env_elem_match in

- if !debug_list_all_candidates then - Log.log_debug "Candidates for instance of type `%s`:" (L.lexp_string t) - ~print_action:(fun () -> - Seq.iter (fun (i, ((_, so),_,t'), _) -> - printf "%-4i %-10s %s\n" - i (* De Bruijn index *) - (match so with | Some s -> s | None -> "<none>") (* Var name *) - (L.lexp_string t') (* Variable type *) - ) candidates); + if !debug_list_all_candidates then begin + let display_candidates channel _ = + let display_candidate (i, ((_, so),_,t'), _) = + fprintf + channel + "%-4i %-10s %s\n" + i (* De Bruijn index *) + (match so with | Some s -> s | None -> "<none>") (* Var name *) + (L.lexp_string t') (* Variable type *) + in + Seq.iter display_candidate candidates + in + trace_debug + __POS__ + ~context:[display_candidates] + "Candidates for instance of type `%s`:" + (L.lexp_string t) + end;

let inst = match candidates () with | Seq.Nil -> None @@ -179,7 +194,9 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc:(sexp_location loc) + trace_debug + __POS__ + ~loc:(sexp_location loc) "Found instance for `%s` at index %i: `%s : %s`" (L.lexp_string t) i (L.lexp_string (L.mkVar (vname, i))) (L.lexp_string t'); @@ -202,11 +219,15 @@ let resolve_instances instantiate_implicit e = if uninstantiated && is_typeclass ctx t then (match search_instance instantiate_implicit ctx (loc) t with | Some e -> Unif.associate i e; true - | None -> - (* The metavar will be generalized, unified, or - will remain and cause an error. *) - Log.log_info ~loc:(sexp_location loc) "No instance found for type `%s`" - (L.lexp_string t); false + | None + (* The metavar will be generalized, unified, or will remain + and cause an error. *) + -> trace_info + __POS__ + ~loc:(sexp_location loc) + "No instance found for type `%s`" + (L.lexp_string t); + false ) else false | None -> false @@ -216,8 +237,10 @@ let resolve_instances instantiate_implicit e = | Some l when l > 0 -> resolve_instances e (Some (l - 1)) | None -> resolve_instances e None - | _ -> - Log.log_error ~loc:(L.lexp_location e) - "Instance resolution recursion limit reached in expression : `%s`" - (L.lexp_string e) in + | _ + -> diagnostic_error + (L.lexp_location e) + "Instance resolution recursion limit reached in expression : `%s`" + (L.lexp_string e) + in resolve_instances e !recursion_limit

===================================== src/inverse_subst.ml ===================================== @@ -45,6 +45,9 @@ module S = Subst

(** Provide inverse function for computing the inverse of a substitution *)

+let {trace_debug; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "ISUBST" + (* Transformation *)

(** Convenience types and variables *) @@ -174,7 +177,8 @@ let inverse (s: subst) : subst option = -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () else - Log.log_debug + trace_debug + __POS__ "Subst-inversion-bug: %s ∘ %s == %s !!\n" (subst_string s) (subst_string s1)

===================================== src/lexer.ml ===================================== @@ -108,7 +108,7 @@ let lex_symbol

let mksym start_point escaped = if Source.Point.equal start_point source#point - then epsilon (Source.Location.of_point source#file start_point) + then epsilon (Source.Location.of_point source#container start_point) else let raw_name, location = source#slice start_point in let name = if escaped then unescape raw_name else raw_name in @@ -217,8 +217,8 @@ let lex (token_env : token_env) (pretokens : pretoken list) : sexp list = | Prestring (location, text) :: pretokens' -> loop pretokens' (String (location, text) :: acc)

- | Pretoken ({file; start_line = l; start_column = c; _}, name) :: pretokens' - -> let source = new Source.source_string ~file ~line:l ~column:c name in + | Pretoken ({container; start_line = l; start_column = c; _}, name) :: pretokens' + -> let source = new Source.source_string ~container ~line:l ~column:c name in let tokens = split_presymbol token_env source in loop pretokens' (List.rev_append tokens acc) in

===================================== src/lexp.ml ===================================== @@ -167,11 +167,13 @@ let builtin_size = ref 0

let dummy_sinfo = Sexp.dummy_sinfo

+let {trace_fatal; _} : Log.Trace.trace_functions = + Log.Trace.make_trace_functions "LEXP" + let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info - = try U.IMap.find id (!metavar_table) - with Not_found - -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" + = try U.IMap.find id (!metavar_table) with + | Not_found -> trace_fatal __POS__ "metavar lookup failure!"

(********************** Hash-consing **********************)

@@ -357,25 +359,23 @@ let mkSLlub' (e1, e2) = (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l | (SortLevel SLz, _) | (_, SortLevel SLz) - -> Log.log_fatal ~section:"internal" "lub of SLz" + -> trace_fatal __POS__ "lub of SLz" | (SortLevel (SLsucc _), SortLevel (SLsucc _)) - -> Log.log_fatal ~section:"internal" "lub of two SLsucc" + -> trace_fatal __POS__ "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) | _ - -> Log.log_fatal - ~section:"internal" + -> trace_fatal + __POS__ "SLlub of non-level: %s ∪ %s" (lexp_head e1) (lexp_head e2)

let mkSLsucc e = match lexp_lexp' e with - | SortLevel _ | Var _ | Metavar _ | Susp _ - -> SLsucc e - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level: %s" - (lexp_head e) + | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e + | _ -> trace_fatal __POS__ "SLsucc of non-level: %s" (lexp_head e)

(********************** Lexp tests ************************)

@@ -396,7 +396,7 @@ let is_var l = pred_var l (fun _ -> true) let get_var l = match lexp_lexp' l with | Var v -> v - | _ -> Log.log_fatal ~section:"internal" "Lexp is not Var " + | _ -> trace_fatal __POS__ "Lexp is not Var "

let get_var_db_index v = let (_n, idx) = v in idx @@ -412,7 +412,7 @@ let pred_inductive l pred = let get_inductive l = match lexp_lexp' l with | Inductive (l, n, a, cs) -> (l, n, a, cs) - | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive " + | _ -> trace_fatal __POS__ "Lexp is not Inductive "

let get_inductive_ctor i = let (_l, _n, _a, cs) = i in cs @@ -515,9 +515,7 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) * sink_count_optimizable := !sink_count_optimizable / 2)); * S.sink (fun l i -> mkVar (l, i)) l s *)

- -let rec lexp_sinfo s = - match lexp_lexp' s with +let rec lexp'_sinfo : lexp' -> sinfo = function | Sort (l,_) -> l | SortLevel (SLsucc s) -> lexp_sinfo s | SortLevel (SLlub (s, _)) -> lexp_sinfo s @@ -533,10 +531,14 @@ let rec lexp_sinfo s = | Cons (_,(l,_)) -> Symbol (l, "") | Case (l,_,_,_,_) -> l | Susp (s, _) -> lexp_sinfo s - (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l | Proj (l,_,_) -> l

+and lexp_sinfo (lexp : lexp) : sinfo = + lexp'_sinfo (lexp_lexp' lexp) + +let lexp'_location (lexp : lexp') : Source.Location.t = + sexp_location (lexp'_sinfo lexp)

let lexp_location e = sexp_location (lexp_sinfo e)

===================================== src/log.ml ===================================== @@ -1,6 +1,6 @@ (* log.ml --- User Errors/Warnings log for Typer. -*- coding: utf-8 -*-

-Copyright (C) 2019-2020 Free Software Foundation, Inc. +Copyright (C) 2019-2022 Free Software Foundation, Inc.

Author: Jean-Alexandre Barszcz jalex_b@hotmail.com Keywords: languages, lisp, dependent types. @@ -20,177 +20,71 @@ 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/. *)

-open Util +(** There are two different flavours of logging in Typer: diagnostics and + tracing. Diagnostics are for users of Typer: they are put in context of the + Typer source that is fed to the compiler and are presented as a nice log at + the end of a run. On the other hand, tracing is for developers of Typer: + messages are put in the context of the OCaml source of the compiler and are + printed immediately. *)

open Printf

-(* LOGGING LEVELS *) - -type log_level = Nothing | Fatal | Error | Warning | Info | Debug - -let int_of_level lvl = - match lvl with - | Nothing -> -1 (* We might not want to print anything during testing *) - | Fatal -> 0 | Error -> 1 | Warning -> 2 | Info -> 3 | Debug -> 4 - -let level_of_int i = - match i with - | _ when i < 0 -> Nothing - | 0 -> Fatal | 1 -> Error | 2 -> Warning | 3 -> Info - | _ -> Debug - -let string_of_level lvl = - match lvl with - | Nothing -> "Nothing" - | Fatal -> "Fatal" - | Error -> "Error" - | Warning -> "Warning" - | Info -> "Info" - | Debug -> "Debug" - -let level_of_string str = - match String.uppercase_ascii str with - | "NOTHING" -> Nothing - | "FATAL" -> Fatal - | "ERROR" -> Error - | "WARNING" -> Warning - | "INFO" -> Info - | "DEBUG" -> Debug - | _ -> invalid_arg ("`"^str^"` is not a logging level") - -let level_color lvl = - match lvl with - | Nothing -> None - | Fatal -> Some Fmt.red - | Error -> Some Fmt.red - | Warning -> Some Fmt.yellow - | Info -> Some Fmt.cyan - | Debug -> Some Fmt.magenta - -(* LOGGING CONFIGURATION *) - -type log_config = { - mutable level : log_level; - mutable print_at_log : bool; - mutable print_in_reverse : bool; - mutable color : bool; - } - -let typer_log_config = { - level = Warning; - print_at_log = false; - print_in_reverse = false; - color = true; - } - -(* LOG DEFINITION *) - -type log_entry = { - level : log_level; - kind : string option; - section : string option; - print_action : (unit -> unit) option; - loc : location option; - msg : string; - } - -type log = log_entry list - -let empty_log = [] - -let typer_log = ref empty_log - -(* PRIVATE OPERATIONS *) - -let mkEntry level ?kind ?section ?print_action ?loc msg = - {level; kind; section; print_action; loc; msg} - -let log_push (entry : log_entry) = - typer_log := entry::(!typer_log) - -let maybe_color_string color_opt str = - match color_opt with - | Some color -> Fmt.color_string color str - | None -> 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 kind_string = Option.value ~default:(string_of_level level) kind in - let parens s = "(" ^ s ^ ")" in - sprintf - "%s %s:%s %s" - (Option.value ~default:"" (Option.map Source.Location.to_string loc)) - (maybe_color_string color kind_string) - (Option.value ~default:"" (Option.map parens section)) - msg - -let print_entry entry = - print_endline (string_of_log_entry entry); - match entry.print_action with - | Some f -> f () - | None -> () - -let log_entry (entry : log_entry) = - if (entry.level <= typer_log_config.level) - then ( - log_push entry; - if (typer_log_config.print_at_log) - then - (print_entry entry; - flush stdout) - ) - -let count_msgs (lvlp : log_level -> bool) = - let count_step count {level; _} = - if lvlp level then count + 1 else count - in - List.fold_left count_step 0 !typer_log - -let error_count () = count_msgs (fun level -> level <= Error) -let warning_count () = count_msgs (fun level -> level = Warning) - -(* PUBLIC INTERFACE *) - -let set_typer_log_level lvl = - typer_log_config.level <- lvl - -let set_typer_log_level_str str = - try set_typer_log_level (level_of_int (int_of_string str)) - with - _ -> set_typer_log_level (level_of_string str) - -let increment_log_level () : unit = - typer_log_config.level - |> int_of_level - |> (+) 1 - |> level_of_int - |> set_typer_log_level - -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; - 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 +module Level = struct + type t = Nothing | Fatal | Error | Warning | Info | Debug + + let to_int (lvl : t) : int = + match lvl with + | Nothing -> -1 (* We might not want to print anything during testing *) + | Fatal -> 0 | Error -> 1 | Warning -> 2 | Info -> 3 | Debug -> 4 + + let of_int (i : int) : t = + match i with + | _ when i < 0 -> Nothing + | 0 -> Fatal | 1 -> Error | 2 -> Warning | 3 -> Info + | _ -> Debug + + let increment : t -> t = function + | Nothing -> Fatal + | Fatal -> Error + | Error -> Warning + | Warning -> Info + | Info -> Debug + | Debug -> Debug + + let to_string (lvl : t) : string = + match lvl with + | Nothing -> "Nothing" + | Fatal -> "Fatal" + | Error -> "Error" + | Warning -> "Warning" + | Info -> "Info" + | Debug -> "Debug" + + let of_string (str : string) : t = + match String.uppercase_ascii str with + | "NOTHING" -> Nothing + | "FATAL" -> Fatal + | "ERROR" -> Error + | "WARNING" -> Warning + | "INFO" -> Info + | "DEBUG" -> Debug + | _ -> invalid_arg ("`" ^ str ^ "` is not a logging level") + + let parse (str : string) : t = + try of_int (int_of_string str) with + | Failure _ -> of_string str + + let color (lvl : t) : Fmt.Color.t = + match lvl with + | Nothing -> Fmt.Color.None + | Fatal -> Fmt.Color.Red + | Error -> Fmt.Color.Red + | Warning -> Fmt.Color.Yellow + | Info -> Fmt.Color.Cyan + | Debug -> Fmt.Color.Magenta +end + +(** Error handling *)

exception Internal_error of string let internal_error fmt = @@ -204,8 +98,288 @@ exception Stop_compilation of string let stop_compilation fmt = ksprintf (fun s -> raise (Stop_compilation s)) fmt

+let compiler_fatal_error : type a b. a -> b = + fun _ -> internal_error "Compiler fatal error" + +let colour_level + (colorize : Fmt.Color.t -> string -> string) + (level : Level.t) + : string = + let level_string = Level.to_string level |> String.uppercase_ascii in + colorize (Level.color level) level_string + +type display_context = out_channel -> (Fmt.Color.t -> string -> string) -> unit + +module Diagnostics = struct + module Config = struct + let level = ref Level.Warning + + let print_in_reverse = ref false + + let channel = stdout + + let use_colors = channel |> Unix.descr_of_out_channel |> Unix.isatty + + let colorize = + if use_colors + then Fmt.colorize + else fun _ text -> text + end + + (** Private interface *) + + type log_entry = + { level : Level.t + ; section : string option + ; context : display_context list + ; location : Source.Location.t + ; msg : string + } + + let log = ref [] + + let log_push (entry : log_entry) : unit = + log := entry :: !log + + let string_of_log_entry + ({level; section; location; msg; _}: log_entry) + : string = + + let section = + Option.value ~default:"" (Option.map (fun s -> "(" ^ s ^ ") ") section) + in + sprintf + "%s %s:%s%s" + (Source.Location.to_string location) + (colour_level Config.colorize level) + section + msg + + let print_entry ({context; location; _} as entry) = + List.iter (fun f -> f Config.channel Config.colorize) context; + Source.Location.display_context location Config.channel Config.colorize; + print_endline (string_of_log_entry entry) + + let log_entry + ?(section : string option) + ?(context : display_context list = []) + (location : Source.Location.t) + (level : Level.t) + (msg : string) + : unit = + if level <= !Config.level + then log_push {section; context; location; level; msg} + + let count_msgs (lvl : Level.t) : int = + let count_step count {level; _} = + if level <= lvl then count + 1 else count + in + List.fold_left count_step 0 !log + + let clear_log () = log := [] + + let print_log () = + let l = + if !Config.print_in_reverse + then !log + else List.rev !log + in + List.iter print_entry l; + clear_log () + + (** Public interface *) + + type ('a, 'd) diagnostic_function' = + ?context:(display_context list) + -> Source.Location.t + -> ('a, unit, string, 'd) format4 + -> 'a + + type diagnostic_function = {f : 'a. ('a, unit) diagnostic_function'} + + type diagnostic_functions = + { + diagnostic_fatal : 'a 'd. ('a, 'd) diagnostic_function'; + diagnostic_error : 'a. ('a, unit) diagnostic_function'; + diagnostic_warning : 'a. ('a, unit) diagnostic_function'; + diagnostic_info : 'a. ('a, unit) diagnostic_function'; + diagnostic_debug : 'a. ('a, unit) diagnostic_function'; + } + + let make_diagnostic_functions + (section : string) + : diagnostic_functions = + + let make_diagnostic_function (level : Level.t) : diagnostic_function = + {f = fun ?context location fmt + -> if level <= !Config.level + then ksprintf (log_entry ?context ~section location level) fmt + else ikfprintf (fun () -> ()) () fmt} + in + + let diagnostic_fatal = + fun ?context location fmt + -> let k' message = + log_entry ?context ~section location Level.Fatal message; + compiler_fatal_error () + in + ksprintf k' fmt + in + let {f = diagnostic_error} = make_diagnostic_function Level.Error in + let {f = diagnostic_warning} = make_diagnostic_function Level.Warning in + let {f = diagnostic_info} = make_diagnostic_function Level.Info in + let {f = diagnostic_debug} = make_diagnostic_function Level.Debug in + { + diagnostic_fatal; + diagnostic_error; + diagnostic_warning; + diagnostic_info; + diagnostic_debug; + } + + let stop_on_error, stop_on_warning = + let count_entries (lvlp : Level.t -> bool) = + let count_step count {level; _} = + if lvlp level then count + 1 else count + in + List.fold_left count_step 0 !log + in + let stop_on_error () : unit = + let count = count_entries (fun level -> level <= Level.Error) in + if 0 < count + then stop_compilation "Compiler stopped after: %d errors\n" count + in + let stop_on_warning () : unit = + stop_on_error (); + let count = count_entries (fun level -> level = Level.Warning) in + if 0 < count + then stop_compilation "Compiler stopped after: %d warnings\n" count + in + stop_on_error, stop_on_warning +end + +module Trace = struct + module Config = struct + let channel = stderr + + let use_colors = channel |> Unix.descr_of_out_channel |> Unix.isatty + + let colorize = + if use_colors + then Fmt.colorize + else fun _ text -> text + + let default_level = ref Level.Warning + + let levels_by_section = Hashtbl.create 16 + + let initialize (config: string) : unit = + let configure_section (config : string) = + match Str.bounded_split (Str.regexp {| *= *|}) config 2 with + | [] -> failwith "unreachable" + | level :: [] + -> let level = Level.parse level in + fprintf + channel + ("[%s] TRACE:%s:%d: globally enabling tracing at level %s\n") + (colour_level colorize Level.Info) + __FILE__ + __LINE__ + (Level.to_string level); + default_level := level + | section :: level :: _ + -> let level = Level.parse level in + let section = String.uppercase_ascii section in + fprintf + channel + "[%s] TRACE:%s:%d: enabling tracing at level %s for section “%s”\n" + (colour_level colorize Level.Info) + __FILE__ + __LINE__ + (Level.to_string level) + section; + Hashtbl.add levels_by_section section level + in + + config + |> Str.split (Str.regexp {| *, *|}) + |> List.iter configure_section + + let level_of_section (section : string) : Level.t = + try Hashtbl.find levels_by_section section with + | Not_found -> !default_level + end + + let display_context context location = + List.iter (fun c -> c Config.channel Config.colorize) context; + Option.iter + (fun l -> Source.Location.display_context l Config.channel Config.colorize) + location + + type ('a, 'd) trace_function' = + ?context:display_context list + -> ?loc:Source.Location.t + -> string * int * int * int + -> ('a, out_channel, unit, 'd) format4 + -> 'a + + type trace_function = {f : 'a. ('a, unit) trace_function'} + + type trace_functions = + { + trace_fatal : 'a 'd. ('a, 'd) trace_function'; + trace_error : 'a. ('a, unit) trace_function'; + trace_warning : 'a. ('a, unit) trace_function'; + trace_info : 'a. ('a, unit) trace_function'; + trace_debug : 'a. ('a, unit) trace_function'; + } + + + let make_trace_functions (section : string) : trace_functions = + let make_trace_function (level : Level.t) : trace_function = + if level <= Config.level_of_section section + then + {f = fun ?(context = []) ?loc (file, line, _, _) fmt + -> display_context context loc; + fprintf + Config.channel + ("[%s] %s:%s:%d: " ^^ fmt ^^ "\n") + (colour_level Config.colorize level) + section + file + line} + else {f = fun ?context ?loc _ fmt + -> ignore context; + ignore loc; + ifprintf stderr fmt} + in + + let trace_fatal = + fun ?(context = []) ?loc (file, line, _, _) fmt + -> display_context context loc; + kfprintf + compiler_fatal_error + Config.channel + ("[%s] %s:%s:%d: " ^^ fmt ^^ "\n") + (colour_level Config.colorize Level.Fatal) + section + file + line + in + let {f = trace_error} = make_trace_function Level.Error in + let {f = trace_warning} = make_trace_function Level.Warning in + let {f = trace_info} = make_trace_function Level.Info in + let {f = trace_debug} = make_trace_function Level.Debug in + {trace_fatal; trace_error; trace_warning; trace_info; trace_debug} +end + +let () = + match Unix.getenv "TYPER_TRACE" with + | trace_config -> Trace.Config.initialize trace_config + | exception Not_found -> () + let show_error (message : string) : unit = - print_log (); + Diagnostics.print_log (); print_endline message; flush stdout

@@ -223,42 +397,4 @@ let handle_error ~(on_error : unit -> 'a) (action : unit -> 'a) : 'a = * -> 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 - -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: %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: %d warnings\n" count - -(* Compiler Internal Debug print *) -let debug_msg expr = - if Debug <= typer_log_config.level then (print_string expr; flush stdout) - let not_implemented_error () = internal_error "not implemented"

===================================== src/opslexp.ml ===================================== @@ -20,6 +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/. *)

+open Printf + module U = Util module SMap = U.SMap module IMap = U.IMap @@ -48,8 +50,20 @@ type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t (* Metavars that appear in non-erasable positions. *) * unit IMap.t

-let error ~location fmt = - Log.log_fatal ~section:"OPSLEXP" ~loc:location fmt +let {diagnostic_fatal = opslexp_fatal; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "OPSLEXP" + +let { diagnostic_fatal = tc_fatal + ; diagnostic_error = tc_error + ; diagnostic_warning = tc_warning + ; _ + } : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "TC" + +let {diagnostic_fatal = whnf_fatal; diagnostic_error = whnf_error; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "WHNF"

let dloc = DB.dloc let dsinfo = DB.dsinfo @@ -65,12 +79,6 @@ let reducible_builtins -> (P.arg_kind * lexp) list (* The builtin's args *) -> lexp option) SMap.t)

-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 : https://mailman.iro.umontreal.ca/pipermail/typer/2020-October/000870.html *) @@ -210,7 +218,12 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let reduce it name aargs = let targs = match lexp'_whnf it ctx with | Inductive (_,_,fargs,_) -> fargs - | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in + | l + -> whnf_error + (lexp'_location l) + "Case on a non-inductive type in whnf!"; + [] + in try let (_, _, branch) = SMap.find name branches in let (subst, _) @@ -232,10 +245,12 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = | Some (_v,default) -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf (push_susp default subst) ctx - | _ -> Log.log_error - ~section:"WHNF" ~loc:(sexp_location l) - {|Unhandled constructor "%s" in case expression|} name; - mkCase (l, e, rt, branches, default) in + | _ + -> whnf_error + (sexp_location 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) -> @@ -259,17 +274,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc:(sexp_location loc) + | _ , [] -> whnf_error (sexp_location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc:(sexp_location loc) + whnf_fatal (sexp_location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) + | _ -> whnf_error (sexp_location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *)

| Metavar (idx, s, _) @@ -440,7 +455,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_fatal ~loc:(lexp_location ekind) + | _ -> tc_fatal (lexp_location ekind) "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with @@ -451,7 +466,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (match lexp'_whnf it ctx with | Inductive (_, _, fargs, constructors) -> fargs, constructors - | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in + | l + -> tc_fatal + (lexp'_location l) + "Case of non-inductive in conv_p") + in let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) S.identity fargs aargs in (* 3. Compare the branches *) @@ -615,8 +634,8 @@ and check'' erased ctx e = let assert_type ctx e t t' = if conv_p ctx t t' then () else - log_tc_error - ~loc:(lexp_location e) + tc_error + (lexp_location e) "Type mismatch for %s : %s != %s" (lexp_string e) (lexp_string t) (lexp_string t') in @@ -626,14 +645,14 @@ and check'' erased ctx e = | Sort _ -> () | _ -> let loc = lexp_location t in - log_tc_error ~loc "Not a proper type: %s" (lexp_string t)); + 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_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; + -> (tc_error (lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -663,8 +682,8 @@ and check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then - log_tc_error - ~loc:(sexp_location loc) + tc_error + (sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -697,13 +716,13 @@ and check'' erased ctx e = match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; + -> tc_error (sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType - -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; + -> tc_error (lexp_location t1) "Not a proper type"; mkSort (loc, StypeOmega) | SortK2NotType - -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; + -> tc_error (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 @@ -720,12 +739,13 @@ and check'' erased ctx e = match lexp'_whnf ft ctx with | Arrow (_l, ak', _v, t1, t2) -> if ak != ak' - then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; + then tc_error (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); + | _ -> tc_error + (lexp_location arg) + "Calling a non functin (type = %s)!" + (lexp_string ft); ft) ft args | Inductive (l, _label, args, cases) @@ -750,17 +770,15 @@ and check'' erased ctx e = | Sort (_, StypeLevel) -> (if not(ak == P.Aerasable && impredicative_universe_poly) - then log_tc_error - ~loc:(lexp_location t) - ~print_action:(fun _ -> ()) + then tc_error + (lexp_location t) "Field of type %s not-allowed!" (lexp_string t)); level | _tt - -> log_tc_error - ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline ()) + -> tc_error + ~context:[Debruijn.display_lexp_context ictx] + (lexp_location t) "Field type %s is not a Type! (%s)" (lexp_string t) (lexp_string lwhnf); level), @@ -802,20 +820,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(sexp_location l) + | _,_ -> (tc_error (sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; + | [] -> tc_error (sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" + else (tc_error (sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -827,10 +845,13 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(sexp_location l) - "Proj on an inductive type that's not a tuple!"; - etype - | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) + -> tc_error + (sexp_location l) + "Proj on an inductive type that's not a tuple!"; + etype + | _, _ + -> tc_error (sexp_location l) "Proj on a non-inductive type!"; + etype)

| Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) @@ -844,7 +865,7 @@ and check'' erased ctx e = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_error ~loc:(lexp_location ekind) + | _ -> tc_error (lexp_location ekind) "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with @@ -857,7 +878,7 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; + -> tc_error (sexp_location 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 = @@ -888,7 +909,7 @@ and check'' erased ctx e = (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; + -> tc_error (sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = mkCall (l, mkCons (it, (sexp_location l, name)), @@ -905,7 +926,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; + then tc_warning (sexp_location 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 @@ -917,9 +938,11 @@ and check'' erased ctx e = | None -> if diff > 0 then - log_tc_error - ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) - | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); + tc_error + (sexp_location l) + "Non-exhaustive match: %d cases missing" + diff) + | _,_ -> tc_error (sexp_location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -948,12 +971,14 @@ and check'' erased ctx e = buildtype fargs with | Not_found - -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; + -> tc_error (sexp_location 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) + | _ + -> tc_error + (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 @@ -962,7 +987,8 @@ and check'' erased ctx e =

and check' ctx e = let res = check'' DB.set_empty ctx e in - (Log.stop_on_error (); res) + Log.Diagnostics.stop_on_error (); + res

and check ctx e = check' ctx e

@@ -1117,21 +1143,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(sexp_location l) + | _,_ -> (tc_error (sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" + | [] -> tc_error (sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(sexp_location l) + else (tc_error (sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1143,10 +1169,10 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(sexp_location l) - "Proj on an inductive type that's not a tuple!"; - etype - | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; + -> tc_error (sexp_location l) + "Proj on an inductive type that's not a tuple!"; + etype + | _,_ -> tc_error (sexp_location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) @@ -1271,10 +1297,10 @@ 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: %s" name) + | None -> opslexp_fatal location "invalid constructor: %s" name) | _ - -> error - ~location:(lexp_location ty) + -> opslexp_fatal + (lexp_location ty) ({|can't deduce arity of constructor "%s", |} ^^ {|because it is not an inductive type: %s|}) name (lexp_string ty) @@ -1292,30 +1318,31 @@ let pos_of_label lctx label e : int = when SMap.cardinal constructors = 1 -> let (_, st) = label in (match SMap.bindings constructors with - | [(_,l)] -> let rec find_index - label - (l : (arg_kind * vname * ltype) list) - (c: int) : int = - match l with - | [] - -> let (loc,st) = label in - Log.log_error ~loc:loc "Label Not Found: %s" st; - 0 - | (_, (_, Some vn), _ )::_ when (String.equal vn st) - -> c - | _::tl -> find_index label tl (c + 1) - in - find_index label l 0 - | _ -> let (loc, _) = label in - Log.log_fatal ~loc:loc "Wrong arg number to inductive type!") + | [(_,l)] + -> let rec find_index + label + (l : (arg_kind * vname * ltype) list) + (c: int) : int = + match l with + | [] + -> let (loc, st) = label in + tc_error loc "Label Not Found: %s" st; + 0 + | (_, (_, Some vn), _ )::_ when (String.equal vn st) + -> c + | _::tl -> find_index label tl (c + 1) + in + find_index label l 0 + | _ -> let (loc, _) = label in + tc_fatal loc "Wrong arg number to inductive type!") | Inductive _, _ - -> let (loc,_) = label in - Log.log_error ~loc:loc "Proj on an inductive type that's not a tuple!"; - 0 - | _,_ -> let (loc,_) = label in - Log.log_error ~loc:loc "Proj on a non-inductive type: %s" - (Lexp.lexp_string it); - 0 + -> let (loc, _) = label in + tc_error loc "Proj on an inductive type that's not a tuple!"; + 0 + | _, _ + -> let (loc, _) = label in + tc_error loc "Proj on a non-inductive type: %s" (Lexp.lexp_string it); + 0

let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = @@ -1403,16 +1430,22 @@ and clean_branch_map lctx cases = performing the erasure itself. *) let erase_type lctx lxp = let _, (mvs, _) = fv lxp in - if not (IMap.is_empty mvs) then - Log.log_fatal - ~print_action:(fun () -> - IMap.iter (fun i (_, t, _, (l, n)) -> - print_endline ("\t" ^ (Source.Location.to_string (sexp_location l)) - ^ " ?" ^ (Option.value ~default:"" n) - ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) - ) mvs) - ("Metavariables in erase_type :"); - erase_type lctx lxp + if IMap.is_empty mvs + then + erase_type lctx lxp + else + let display_metavariables channel _ = + let display_metavariable i (_, t, _, (l, n)) = + let location = Source.Location.to_string (sexp_location l) in + let name = Option.value ~default:"" n in + fprintf channel "\t%s ?%s[%d] : %s" location name i (lexp_string t) + in + IMap.iter display_metavariable mvs + in + tc_fatal + ~context:[display_metavariables] + (lexp_location lxp) + ("Metavariables in erase_type")

(* Textually identical to the previous definition of `clean_decls`, but calls the new `erase_type`, which checks for metavars. *)

===================================== src/pexp.ml ===================================== @@ -22,7 +22,8 @@ this program. If not, see http://www.gnu.org/licenses/. *)

open Sexp (* Symbol *)

-let pexp_error loc = Log.log_error ~section:"PEXP" ~loc +let {diagnostic_error = pexp_error; _} : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "PEXP"

(*************** The Pexp Parser *********************)

===================================== src/prelexer.ml ===================================== @@ -22,7 +22,9 @@ this program. If not, see http://www.gnu.org/licenses/. *)

open Util

-let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc +let {diagnostic_error = prelexer_error; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "PRELEXER"

type pretoken = | Pretoken of location * string

===================================== src/sexp.ml ===================================== @@ -24,8 +24,9 @@ open Util open Prelexer open Grammar

-let sexp_error ?print_action loc fmt = - Log.log_error ~section:"SEXP" ?print_action ~loc fmt +let {diagnostic_error = sexp_error; _} + : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "SEXP"

type integer = Z.t type symbol = location * string @@ -87,11 +88,13 @@ let rec sexp_string ?(print_locations = false) sexp = (if print_locations then let open Source.Location in - let {file; start_line; start_column; end_line; end_column} = + let {container; start_line; start_column; end_line; end_column; _} = sexp_location sexp in Printf.sprintf - "#;("%s" %d %d %d %d) " file start_line start_column end_line end_column + "#;("%s" %d %d %d %d) " + (Source.Container.name container) + start_line start_column end_line end_column else "") ^ match sexp with | Block(_, pts) -> "{" ^ (pretokens_string pts) ^ " }"

===================================== src/source.ml ===================================== @@ -18,6 +18,40 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see http://www.gnu.org/licenses/. *)

+let width_of_utf8_head (c : char) : int = + let c = Char.code c in + if c < 0x80 then 1 else if c < 0xe0 then 2 else if c < 0xf0 then 3 else 4 + +(** A container is a thing that can hold Typer source code. *) +module Container = struct + type t = + | File of string * string Array.t (** A file can contain source code. *) + | String of string * string Array.t (** A string entred in a REPL can + contain source code. *) + + let of_string ~label (contents : string) : t = + String (label, contents |> String.split_on_char '\n' |> Array.of_list) + + let of_path (path : string) : t = + let channel = open_in path in + let unfold_lines () = + try Some (input_line channel, ()) with + | End_of_file -> None + in + let lines = Array.of_seq (Seq.unfold unfold_lines ()) in + File (path, if Array.length lines = 0 then [|""|] else lines) + + (** The name of a container is either a path or a label in the case of a + string entred in the REPL. *) + let name : t -> string = function + | File (path, _) -> path + | String (label, _) -> label + + let lines : t -> string Array.t = function + | File (_, lines) -> lines + | String (_, lines) -> lines +end + module Point = struct (* offset * line * column *) type t = int * int * int @@ -31,67 +65,80 @@ end module Location = struct type t = { - file : string; + container: Container.t; + start_offset : int; start_line : int; start_column : int; + end_offset : int; end_line : int; end_column : int; }

let dummy = { - file = ""; + container = Container.String ("<dummy>", ""); + start_offset = 0; start_line = 0; start_column = 0; + end_offset = 0; end_line = 0; end_column = 0; }

(* Creates a zero-width location around the given point. *) - let of_point (file : string) (_, line, column : Point.t) : t = + let of_point (container : Container.t) (offset, line, column : Point.t) : t = { - file; + container; + start_offset = offset; start_line = line; start_column = column; + end_offset = offset; end_line = line; end_column = column; }

let to_string - ({file; start_line; start_column; end_line; end_column} : t) + ({container; start_line; start_column; end_line; end_column; _} : t) : string =

+ let name = Container.name container in if Int.equal start_line end_line && Int.equal start_column end_column - then Printf.sprintf "%s:%d:%d" file start_line start_column + then Printf.sprintf "%s:%d:%d" name start_line start_column else Printf.sprintf - "%s:%d:%d-%d:%d" file start_line start_column end_line end_column + "%s:%d:%d-%d:%d" name start_line start_column end_line end_column

let equal (l : t) (r : t) = let { - file = l_file; - start_line = l_start_line; - start_column = l_start_column; - end_line = l_end_line; - end_column = l_end_column; + container = l_container; + start_offset = l_start_offset; + end_offset = l_end_offset; + _; } = l in let { - file = r_file; - start_line = r_start_line; - start_column = r_start_column; - end_line = r_end_line; - end_column = r_end_column; + container = r_container; + start_offset = r_start_offset; + end_offset = r_end_offset; + _; } = r in

- String.equal l_file r_file - && Int.equal l_start_line r_start_line - && Int.equal l_start_column r_start_column - && Int.equal l_end_line r_end_line - && Int.equal l_end_column r_end_column + l_container == r_container + && l_start_offset == r_start_offset + && l_end_offset == r_end_offset + + let display_context + (location : t) + (channel : out_channel) + (colourize : Fmt.colorize) + : unit = + ignore location; + ignore channel; + ignore colourize; + failwith "TODO" end

(* Traditionally, line numbers start at 1… *) @@ -99,43 +146,93 @@ let first_line_of_file = 1 (* … and so do column numbers :-( *) let first_column_of_line = 1

-(* A source object is text paired with a cursor. The text can be lazily loaded - as it is accessed byte by byte, but it must be retained for future reference - by error messages. *) -class virtual t (base_line : int) (base_column : int) (file : string) = +let offset_of_column (line : string) (column : int) : int = + let rec loop offset current_column = + if current_column = column + then offset + else + loop (offset + width_of_utf8_head line.[offset]) (current_column + 1) + in + loop 0 first_column_of_line + +(** A source object is text paired with a cursor. *) +class virtual t + (base_offset : int) + (base_line : int) + (base_column : int) + (container' : Container.t) + = +let line_text = (Container.lines container').(base_line) in +let offset_within_line = offset_of_column line_text base_column in object (self) + val container = container' val mutable line = base_line val mutable column = base_column + val mutable offset_of_line = base_offset - offset_within_line + val mutable offset_within_line = offset_within_line + val mutable line_text = Some line_text + + method container : Container.t = container

- (* A path if the text comes from a file, otherwise a meaningful identifier. *) - method file : string = file + method private offset = offset_of_line + offset_within_line

- (* Return the byte at the cursor, or None if the cursor is at the end of - the text. *) - method virtual peek : char option + (* Returns the byte at the cursor, or None if the cursor is at the end of the + text. *) + method peek = + match line_text with + | None -> None + | Some (line_text') + -> if offset_within_line <= String.length line_text' + then Some (self#peek_unchecked line_text') + else begin + line <- line + 1; + line_text <- begin + try Some (Container.lines container).(line) with + | Invalid_argument _ -> None + end; + offset_of_line <- offset_of_line + 1 + String.length line_text'; + offset_within_line <- 0; + self#peek + end + + method private peek_unchecked line_text = + if offset_within_line < String.length line_text + then line_text.[offset_within_line] + else '\n'

- (* The current point of the cursor. *) + (** The current point of the cursor. *) method point : Point.t = (self#offset, line, column)

- (* The current offset of the cursor in the file, in bytes. *) - method virtual private offset : int - - (* Makes a location starting at the given point and ending at the current - cursor position. *) - method make_location (_, start_line, start_column : Point.t) : Location.t = - {file; start_line; start_column; end_line = line; end_column = column} - - (* Slices the text, from (and including) a starting point and to (and - excluding) the curent cursor offset. + (** Makes a location starting at the given point and ending at the current + cursor position. *) + method make_location + (start_offset, start_line, start_column : Point.t) + : Location.t = + { + container; + start_offset; + start_line; + start_column; + end_offset = self#offset; + end_line = line; + end_column = column; + }

- Note that the source is required only to buffer the last line read and may - raise an Invalid_argument if the slice extends before the start of the - line. *) + (** Slices the text, from (and including) a starting point and to (and + excluding) the curent cursor offset. *) method slice (offset, _, _ as point : Point.t) : string * Location.t = (self#slice_impl offset, self#make_location point)

- method virtual private slice_impl : int -> string + method private slice_impl start_offset = + match line_text with + | Some line_text' + -> let relative_start_offset = start_offset - offset_of_line in + String.sub + line_text' + relative_start_offset + (offset_within_line - relative_start_offset) + | None -> raise (Invalid_argument "")

(* Moves the cursor forward one byte *) method advance : unit = @@ -162,7 +259,8 @@ end let read_buffer_length = 4096

class source_file file_name = object (self) - inherit t (first_line_of_file - 1) first_column_of_line file_name + inherit + t (first_line_of_file - 1) first_column_of_line (Container.of_path file_name)

val in_channel = open_in file_name val mutable end_of_line = false @@ -170,41 +268,20 @@ class source_file file_name = object (self) val mutable line_offset = 0 val mutable offset = 0

- method private peek_unchecked = - if offset < String.length source_line - then source_line.[offset] - else '\n' - - method peek = - if offset <= String.length source_line - then Some self#peek_unchecked - else - try - line_offset <- line_offset + 1 + String.length source_line; - source_line <- input_line in_channel; - offset <- 0; - Some self#peek_unchecked - with - | End_of_file -> None - method private advance_impl = offset <- offset + 1

- method private offset = line_offset + offset

- method private slice_impl start_offset = - let relative_start_offset = start_offset - line_offset in - String.sub source_line relative_start_offset (offset - relative_start_offset) end

class source_string - ?(file : string = "<string>") + ~(container : Container.t) ?(line : int = first_line_of_file) ?(column : int = first_column_of_line) - source + (source : string) = object - inherit t line column file + inherit t line column container

val mutable offset = 0

===================================== src/unification.ml ===================================== @@ -25,7 +25,8 @@ module DB = Debruijn

(** Provide unify function for unifying two Lambda-Expression *)

-let log_info ?loc fmt = Log.log_info ~section:"UNIF" ?loc fmt +let {diagnostic_info = unif_info; _} : Log.Diagnostics.diagnostic_functions = + Log.Diagnostics.make_diagnostic_functions "UNIF"

(* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) @@ -329,7 +330,8 @@ and unify_metavar (matching : scope_level option) then [(CKresidual, ctx, lxp1, lxp2)] else match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> log_info + -> unif_info + (lexp_location lxp) "Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n" (subst_string s) (lexp_string lxp); @@ -342,7 +344,8 @@ and unify_metavar (matching : scope_level option) | [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ - -> log_info + -> unif_info + (lexp_location lxp) "Unificaton of metavar type failed:\n %s != %s\nfor %s\n" (lexp_string t) (lxp |> OL.get_type ctx |> lexp_string)

===================================== typer.ml ===================================== @@ -33,18 +33,19 @@ let add_input_file, list_input_files =

let arg_defs = [("--verbosity", - Arg.String Log.set_typer_log_level_str, + Arg.String (fun s -> Log.Diagnostics.Config.level := Log.Level.parse s), "Set the logging level");

- ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); + ("-v", + Arg.Unit + (fun () + -> Log.Diagnostics.Config.level + := Log.Level.increment !Log.Diagnostics.Config.level), + "Increment verbosity");

("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, "Print the full lexp context on error"); - - ("-Vmacro-expansion", - Arg.Set Elab.macro_tracing_enabled, - "Trace macro expansion"); ]

let parse_args argv usage = @@ -66,7 +67,7 @@ let compile_main argv = (fun () -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) in - Log.print_log () + Log.Diagnostics.print_log ()

let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in @@ -88,7 +89,7 @@ let repl_main argv = 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 (); + Log.Diagnostics.print_log (); REPL.repl i backend ectx

let run_main argv = @@ -101,7 +102,7 @@ let run_main argv = let _ = List.fold_left (Elab.process_file backend) ectx (list_input_files ()) in - Log.print_log () + Log.Diagnostics.print_log ()

let main () = let command, argv =

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/078fe770a7a12a62bf87eb9303a6e307c9...