[Typer] [Git][monnier/typer][dev/errors] 17 commits: * src/subst.ml (subst): Fold a `Shift` into the `Identity`.

Jean-Alexandre Barszcz pushed to branch dev/errors at Stefan / Typer

Commits: c25f821e by Stefan Monnier at 2019-07-24T01:56:09Z * src/subst.ml (subst): Fold a `Shift` into the `Identity`.

Generalize `Identity` with `Identity o` where the old `Identity` is now `Identity 0` and `Identity o` is like the old `Shift (Identity, o)`.

(mkShift): Use `Identity` when possible. (shift): Use `Identity`. (identity): Adjust to new `Identity`. (lookup, identity_p, compose): Generalize to the new `Identity o`. (substitute): Use `identity`.

* src/elab.ml (newMetavar): Use S.identity.

* src/inverse_subst.ml (is_identity): Take advantage of the new `Identity o`. (shift_inv_subst): Optimize the case when n is 0. (transfo, invertible, lookup_inv_subst, compose_inv_subst): Generalize to the new `Identity o`.

* src/lexp.ml (subst_string): Handle the new `Identity o`. (subst_eq): Generalize to the new `Identity o`.

* tests/inverse_test.ml (is_identity): Copy new def from inverse_subst.ml.

* tests/unify_test.ml (generate_testable): Use `identity`.

- - - - - 6c5475e1 by Stefan Monnier at 2019-07-24T04:40:25Z * src/subst.ml (subst): Fold the remaining Shift into Cons.

Fold `Shift` into the `Cons`, and hence remove `Shift` since it's not needed as a separate constructor any more.

(sink, substitute): Use `cons` (lookup, mkShift, cons, compose): * src/lexp.ml (subst_string, subst_eq): * src/inverse_subst.ml (transfo, is_identity, invertible) (lookup_inv_subst, compose_inv_subst): Adjust accordingly.

* tests/inverse_test.ml (is_identity): Update from src/inverse_subst.ml.

* src/opslexp.ml (lexp_whnf): Use `S.cons`.

- - - - - d75ab820 by Stefan Monnier at 2019-07-27T03:38:33Z Add comments from a Myers's subst experiment

* src/lexp.ml (lexp_unparse): Prefer S.cons to S.Cons.

* src/subst.ml (subst): Add Myers's optimization in a comment. It probably works, but it currently bumps into another performance problem. (lookup, compose): Add commented-out Myers's optimization.

* tests/inverse_test.ml (is_identity): Remove (lets the code use the version of Inverse_subst).

- - - - - ff16d3ba by Stefan Monnier at 2019-07-27T03:39:04Z * samples/defmacro.typer (define-macro): New package and macro

- - - - - e3a0fe68 by Stefan Monnier at 2019-09-13T18:31:03Z Avoid using Inverse_subst in core type checking

* src/lexp.ml (mkSLlub', mkSLsucc): New constructors with sanity checks. (sunshift): New function. * src/opslexp.ml (check'', get_type): Use it instead of Inverse_subst.

- - - - - cf67844d by Stefan Monnier at 2019-09-13T21:06:03Z First tweak to try and handle parameterized inductives

* src/elab.ml (check_case.add_branch): Try and handle parameterized constructors. (elab_check_def): Slightly improve message.

* src/unification.ml (unify_inductive): New function. (unify'): Use it.

- - - - - 25bb77ab by Stefan Monnier at 2019-09-26T20:51:26Z * lexp.ml (lexp): Typo

- - - - - 5c7f8365 by Stefan Monnier at 2019-09-26T20:52:00Z Merge remote-tracking branch 'refs/remotes/gitlab/master' into trunk

- - - - - 9455fa18 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Extract logging from util.ml

- - - - - c1458d9a by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Replace typer_unreachable exception with 'failwith'

- - - - - 82fa3593 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Refactor logging

- - - - - 51251f1f by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Add optional color to logging

- - - - - 2a2afc56 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print errors/warnings all at once, after compilation stops

- - - - - 09952ed7 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print the log in default context

- - - - - c02e28bc by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add an option to control the verbosity/logging level

- - - - - f41b8bb3 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Always print the log after evaluation

If there are warnings (or other messages of lesser priority in the log), we want to print them. Similarly, errors for which we were able to recover might still exist in the log. Regardless of whether compilation has been stopped, we thus print the log.

- - - - - b948d4c9 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print test messages instead of logging them

- - - - -

22 changed files:

- + samples/defmacro.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.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/subst.ml - src/unification.ml - src/util.ml - tests/inverse_test.ml - tests/unify_test.ml - tests/utest_lib.ml

Changes:

===================================== samples/defmacro.typer ===================================== @@ -0,0 +1,43 @@ +%%% defmacro.typer --- Convenience macro to define macros + +%% Copyright (C) 2018 Stefan Monnier + +%% Author: Stefan Monnier monnier@iro.umontreal.ca +%% Keywords: + +%% This program is free software; you can redistribute it and/or modify +%% it under the terms of the GNU General Public License as published by +%% the Free Software Foundation, either version 3 of the License, or +%% (at your option) any later version. + +%% This program is distributed in the hope that it will be useful, +%% but WITHOUT ANY WARRANTY; without even the implied warranty of +%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +%% GNU General Public License for more details. + +%% You should have received a copy of the GNU General Public License +%% along with this program. If not, see https://www.gnu.org/licenses/. + +%%% Commentary: + +%% + +%%% Code: + +define-macro = + let dm argsym args body = case args + | nil => body + in macro (lambda args -> case args + | nil => Sexp_error + | cons name args' + => case args' + | nil => Sexp_error + | cons args body + => IO_bind + (gensym ()) + (lambda argsym -> + quote (uquote name + = macro (lambda (uquote argsym) + -> uquote (dm argsym args body))))); + +%%% defmacro.typer ends here

===================================== src/REPL.ml ===================================== @@ -63,8 +63,16 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> "

-let ieval_error loc msg = - msg_error "IEVAL" loc msg +let ieval_error = Log.log_error ~section:"IEVAL" + +let print_and_clear_log () = + if (not Log.typer_log_config.print_at_log) then + Log.print_and_clear_log () + +let handle_stopped_compilation msg = + print_and_clear_log (); + print_string msg; print_newline (); + flush stdout

(* Read stdin for input. Returns only when the last char is ';' * We can use '%' to prevent parsing @@ -207,7 +215,7 @@ let readfiles files (i, lctx, rctx) prt = (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with Sys_error _ -> ( - ieval_error dloc ("file "" ^ file ^ "" does not exist."); + ieval_error ("file "" ^ file ^ "" does not exist."); (i, lctx, rctx)) ) (i, lctx, rctx) files @@ -231,8 +239,8 @@ let rec repl i clxp rctx = let (i, clxp, rctx) = try readfiles args (i, clxp, rctx) false - with Stop_Compilation s -> - (print_string s; (i,clxp,rctx)) + with Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; (i,clxp,rctx)) in repl clxp rctx; | "%who"::args | "%w"::args -> ( @@ -247,18 +255,25 @@ let rec repl i clxp rctx = repl clxp rctx)

| cmd::_ -> - ieval_error dloc (" "" ^ cmd ^ "" is not a correct repl command"); + ieval_error (" "" ^ cmd ^ "" is not a correct repl command"); repl clxp rctx | _ -> repl clxp rctx)

(* eval input *) - | _ -> ( + | _ -> try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + print_and_clear_log (); List.iter (print_eval_result i) ret; repl clxp rctx - with e -> match e with - | Stop_Compilation msg -> (print_string msg; repl clxp rctx) - | _ -> catch_error (); repl clxp rctx) + with + | Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; repl clxp rctx) + | Log.Internal_error msg -> + (handle_stopped_compilation ("Internal error: " ^ msg); + repl clxp rctx) + | Log.User_error msg -> + (handle_stopped_compilation ("Fatal user error: " ^ msg); + repl clxp rctx)

let arg_files = ref []

@@ -266,6 +281,9 @@ let arg_files = ref [] (* ./typer [options] files *) let arg_defs = [ ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + ("--verbosity", + Arg.String Log.set_typer_log_level_str, "Set the logging level"); + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), @@ -287,8 +305,19 @@ let main () = print_string (make_sep '-'); flush stdout);

- let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) - (not !arg_batch) in + let (i, ectx, rctx) = ( + try + let res = + readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + print_and_clear_log (); res + with + | Log.Stop_Compilation msg -> + handle_stopped_compilation msg; exit 1 + | Log.Internal_error msg -> + handle_stopped_compilation ("Internal error: " ^ msg); exit 1 + | Log.User_error msg -> + handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 + ) in

flush stdout;

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

-let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) -let warning loc msg = msg_warning "BUILT-IN" loc msg +let log_raise_error ?loc msg = + Log.log_error ~section:"BUILT-IN" ?loc msg; + Log.internal_error msg

let predef_names = [ "cons"; (* FIXME: Should be used but isn't! *) @@ -87,7 +88,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 -> error dummy_location ("""^ name ^ "" was not predefined") + with Not_found -> log_raise_error ("""^ name ^ "" was not predefined")

let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) @@ -131,9 +132,9 @@ let v2o_list v = match v with | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl | E.Vcons ((_, "nil"), []) -> List.rev acc - | _ -> print_string (E.value_name v); print_string "\n"; - E.value_print v; - error dloc "List conversion failure'" in + | _ -> log_raise_error ~loc:(E.value_location v) ( + "Failed to convert the " ^ E.value_name v ^ " with value :\n" + ^ E.value_string v ^ "\n to a list.") in v2o_list [] v

(* Map of lexp builtin elements accessible via (## <name>). *)

===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -42,8 +42,7 @@ open Fmt

module S = Subst

-let error l m = msg_error "DEBRUIJN" l m; internal_error m -let warning = msg_warning "DEBRUIJN" +let fatal = Log.log_fatal ~section:"DEBRUIJN"

(* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. @@ -85,8 +84,8 @@ let sort_level = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) let level0 = mkSortLevel SLz -let level1 = mkSortLevel (SLsucc level0) -let level2 = mkSortLevel (SLsucc level1) +let level1 = mkSortLevel (mkSLsucc level0) +let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) @@ -316,17 +315,17 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = | (((_, Some name), _, _), Some ename) -> (* Check if names match *) if not (ename = name) then - (print_lexp_ctx ctx; - error loc ("DeBruijn index " - ^ string_of_int dbi - ^ " refers to wrong name. " - ^ "Expected: `" ^ ename - ^ "` got `" ^ name ^ "`")) + fatal ~loc ~print_action:(fun _ -> + print_lexp_ctx ctx; print_newline ()) + ("DeBruijn index " ^ string_of_int dbi + ^ " refers to wrong name. " + ^ "Expected: `" ^ ename + ^ "` got `" ^ name ^ "`") | _ -> () in

ret) with - Not_found -> error loc ("DeBruijn index " + Not_found -> fatal ~loc ("DeBruijn index " ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!")

@@ -366,7 +365,7 @@ let rec lctx_view lctx = | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] | Myers.Mcons ((_, LetDef (o, def), _), _, _, _) when o > 1 - -> U.internal_error "Unexpected lexp_context shape!" + -> fatal "Unexpected lexp_context shape!" | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx)

===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -69,21 +69,28 @@ let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl"

-let warning = msg_warning "ELAB" -let error = msg_error "ELAB" -let fatal = msg_fatal "ELAB" - -(* Print Lexp name followed by the lexp in itself, finally throw an exception *) -let debug_message error_type type_name type_string loc expr message = - EV.debug_messages error_type loc - message [ - (type_name expr) ^ ": " ^ (type_string expr); - ] - -let lexp_fatal = debug_message fatal lexp_name lexp_string -let lexp_warning = debug_message warning lexp_name lexp_string -let lexp_error = debug_message error lexp_name lexp_string -let value_fatal = debug_message fatal value_name value_string +let fatal = Log.log_fatal ~section:"ELAB" +let error = Log.log_error ~section:"ELAB" +let warning = Log.log_warning ~section:"ELAB" +let info = Log.log_info ~section:"ELAB" + +let 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 = + error ~loc ~print_action:(lexp_print_details lexp) +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)

(** Type info returned by elaboration. *) type sform_type = @@ -116,9 +123,9 @@ let sform_default_ectx = ref empty_elab_context let elab_check_sort (ctx : elab_context) lsort var ltp = match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> - print_string "Exception during whnf of "; - lexp_print lsort; - print_string "\n"; + info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) + ~loc:(lexp_location lsort) + "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) | _ -> let lexp_string e = lexp_string (L.clean e) in @@ -134,15 +141,19 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = 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 - | Stop_Compilation _ -> raise e - | _ -> print_string "Exception while checking type `"; - lexp_print ltp; - (match var with - | (_, None) -> () - | (_, Some name) - -> print_string ("` of var `" ^ name ^"`\n")); - print_lexp_ctx (ectx_to_lctx ctx); - raise e + | Log.Stop_Compilation _ -> raise e + | _ -> + info + ~print_action:(fun _ -> + print_lexp_ctx (ectx_to_lctx ctx); print_newline () + ) + ~loc:(lexp_location ltp) + ("Exception while checking type `" ^ (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 @@ -151,29 +162,37 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with - (* lexp_error is fatal but Stop_Compilation isn't *) - | Stop_Compilation _ -> raise e - | _ -> lexp_error loc lxp "Error while type-checking"; + | Log.Stop_Compilation _ -> raise e + | _ -> + info + ~print_action:(fun _ -> + lexp_print_details lxp (); print_lexp_ctx (ectx_to_lctx ctx); - raise e in + print_newline () + ) + ~loc + "Error while type-checking"; + raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e - -> print_string ("Exception while conversion-checking types:\n"); - lexp_print ltype; - print_string (" and "); - lexp_print ltype'; - print_string ("\n"); - lexp_error loc lxp - ("Exception while conversion-checking types " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) + with e -> + info ~print_action:(lexp_print_details lxp) + ~loc + ("Exception while conversion-checking types: " + ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); + raise e) then elab_check_proper_type ctx ltype var else - (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype]) + 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 + "Type check error: ¡¡ctx_define error!!"

let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; @@ -238,7 +257,7 @@ let ctx_define_rec (ctx: elab_context) decls =

let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in - mkMetavar (meta, S.Identity, name) + mkMetavar (meta, S.identity, name)

let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level @@ -297,8 +316,8 @@ let rec meta_to_var ids o (e : lexp) = let rec loop e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (loop e1, loop e2)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop e1, loop e2)) | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e @@ -449,7 +468,7 @@ let rec elaborate ctx se ot =

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

@@ -608,7 +627,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let pat_string p = sexp_string (pexp_u_pat p) in

let uniqueness_warn pat = - warning (pexp_pat_location pat) + warning ~loc:(pexp_pat_location pat) ("Pattern " ^ pat_string pat ^ " is a duplicate. It will override previous pattern.") in

@@ -650,7 +669,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let add_branch pctor pargs = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) with + let rec inst_args ctx e = match OL.lexp_whnf e (ectx_to_lctx ctx) with + | Lambda (Aerasable, v, t, body) + -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + v t in + let nctx = ctx_extend ctx v Variable t in + let body = inst_args nctx body in + mkSusp body (S.substitute arg) + | e -> e in + match nosusp (inst_args ctx lctor) with | Cons (it', (_, cons_name)) -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with | (None | Some (_::_)) @@ -676,7 +703,7 @@ and check_case rtype (loc, target, ppatterns) ctx = pargs (* Pattern arguments. *) cargs (* Constructor arguments. *) pe (* Pending explicit pattern args. *) - acc = (* Accumulated reult. *) + acc = (* Accumulated result. *) match (pargs, cargs) with | (_, []) when not (SMap.is_empty pe) -> let pending = SMap.bindings pe in @@ -911,7 +938,11 @@ and lexp_eval ectx e = ^ track_fv rctx (ectx_to_lctx ectx) e);

try EV.eval ee rctx - with exc -> EV.print_eval_trace None; raise exc + 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

and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) : value_type = @@ -945,11 +976,11 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | Vcommand cmd -> (match (cmd ()) with | Vsexp (sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return an IO") + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO")

with e -> - fatal loc ("Macro `" ^ mname ^ "` not found") + fatal ~loc ("Macro `" ^ mname ^ "` not found")

and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -972,7 +1003,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let d = (v', LetDef (i + 1, e), t) in (IMap.add i ((l, Some vname), e, t) map, (grm, ec, Myers.set_nth i d lc, sl)) - | _ -> U.internal_error "Defining same slot!") + | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls @@ -1015,8 +1046,8 @@ and lexp_decls_1 let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then - let (s, l) = SMap.choose pending_decls in - error l ("Variable `" ^ s ^ "` declared but not defined!") + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); [], [], nctx @@ -1028,22 +1059,22 @@ and lexp_decls_1 -> lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs

- | Node (Symbol (l, "_:_"), args) :: sdecls + | Node (Symbol (loc, "_:_"), args) :: sdecls (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol (l, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in (* Take the previous type annotation. *) let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> U.internal_error "Var not found at its index!" in + | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with | (None | Some (_::_)) - -> lexp_error l ltp + -> lexp_error loc ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") @@ -1051,13 +1082,13 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then - (error l ("Variable `" ^ vname ^ "` already defined!"); + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx - (ectx_extend nctx (l, Some vname) ForwardRef ltp) - (SMap.add vname l pending_decls) + (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) pending_defs - | _ -> error l "Invalid type declaration syntax"; + | _ -> error ~loc "Invalid type declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| Node (Symbol (l, "_=_") as head, args) :: sdecls @@ -1093,7 +1124,7 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

else - (error l ("`" ^ vname ^ "` defined but not declared!"); + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| [Node (Symbol s, args) as d; body] @@ -1105,7 +1136,7 @@ and lexp_decls_1 :: sdecls) ectx nctx pending_decls pending_defs

- | _ -> error l "Invalid definition syntax"; + | _ -> error ~loc:l "Invalid definition syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| Node (Symbol (l, "define-operator"), args) :: sdecls @@ -1120,12 +1151,12 @@ and lexp_decls_1 pending_decls pending_defs

| sexp :: sdecls - -> error (sexp_location sexp) "Invalid declaration syntax"; + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

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

and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = @@ -1134,14 +1165,14 @@ and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in let declss, nnctx = lexp_p_decls sdecls nctx in decls :: declss, nnctx in - let res = impl sdecls ctx in (stop_on_error (); res) + let res = impl sdecls ctx in (Log.stop_on_error (); res)

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 - (stop_on_error (); res) + (Log.stop_on_error (); res)

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

(* -------------------------------------------------------------------------- * Special forms implementation @@ -1157,17 +1188,17 @@ and sform_new_attribute ctx loc sargs ot = OL.lexp_close (ectx_to_lctx ctx) ltp, Some AttributeMap.empty), Lazy) - | _ -> fatal loc "new-attribute expects a single Type argument" + | _ -> fatal ~loc "new-attribute expects a single Type argument"

and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr - | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in + | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type - | _ -> fatal loc "add-attribute expects a table as first argument" in + | _ -> fatal ~loc "add-attribute expects a table as first argument" in

(* FIXME: Type check (attr: type == attr_type) *) let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in @@ -1179,11 +1210,11 @@ and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in

let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map - | _ -> fatal loc "get-attribute expects a table as first argument" in + | _ -> fatal ~loc "get-attribute expects a table as first argument" in

try Some (AttributeMap.find var map) with Not_found -> None @@ -1197,7 +1228,7 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx)] -> table, (n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type @@ -1211,9 +1242,9 @@ and sform_declexpr ctx loc sargs ot = | [Var((_, vn), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) - | None -> error loc "no expr available"; + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error loc "declexpr expects one argument"; + | _ -> error ~loc "declexpr expects one argument"; sform_dummy_ret ctx loc

@@ -1221,7 +1252,7 @@ let sform_decltype ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error loc "decltype expects one argument"; + | _ -> error ~loc "decltype expects one argument"; sform_dummy_ret ctx loc

let builtin_value_types : ltype option SMap.t ref = ref SMap.empty @@ -1237,13 +1268,13 @@ let sform_built_in ctx loc sargs ot = sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; (bi, Checked) - | None -> error loc "Built-in's type not provided by context!"; + | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc)

- | true, _ -> error loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc

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

let sform_datacons ctx loc sargs ot = @@ -1273,8 +1304,9 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = -> (elab_colon_to_ak k, (l, Some name), Some e) | Symbol (l, name) -> (Anormal, (l, Some name), None) - | _ -> sexp_print arg; - (sexp_error (sexp_location arg) "Unrecognized formal arg"); + | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) + (sexp_location arg) + "Unrecognized formal arg"; (Anormal, (sexp_location arg, None), None)

let sform_typecons ctx loc sargs ot = @@ -1402,7 +1434,7 @@ let sform_identifier ctx loc sargs ot = (if not (name = "") then let idx = match mv with | Metavar (idx, _, _) -> idx - | _ -> fatal loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mkSusp mv subst, match ot with Some _ -> Checked | None -> Lazy) @@ -1526,7 +1558,7 @@ let sform_type ctx loc sargs ot = match sargs with | [l] -> let l, _ = infer l ctx in (mkSort (loc, Stype l), - Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) + Inferred (mkSort (loc, Stype (SortLevel (mkSLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc

@@ -1583,7 +1615,8 @@ let sform_load usr_elctx loc sargs ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error loc "argument to load should be one file name (String)"; !sform_default_ectx) in + | _ -> (error ~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 @@ -1670,8 +1703,8 @@ let default_ectx let idx = senv_lookup name elctx in let v = mkVar ((dloc, Some name), idx) in BI.set_predef name v) BI.predef_names; - with e -> - warning dloc "Predef not found"; in + with Senv_Lookup_Fail _ -> + warning "Predef not found"; in

(* Empty context *) let lctx = empty_elab_context in @@ -1698,7 +1731,10 @@ let default_ectx (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in let _ = sform_default_ectx := ectx in ectx - with (Stop_Compilation _) -> fatal dloc "compilation stopped in default context" + with e -> + error "Compilation stopped in default context"; + Log.print_and_clear_log (); + raise e

let default_rctx = EV.from_ectx default_ectx

@@ -1714,7 +1750,7 @@ let lexp_expr_str str ctx = List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps - with Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> []

let lexp_decl_str str ctx = try let tenv = default_stt in @@ -1722,7 +1758,7 @@ let lexp_decl_str str ctx = let limit = Some ";" in let sdecls = sexp_parse_str str tenv grm limit in lexp_p_decls sdecls ctx - with Stop_Compilation s -> (print_string s; ([],ctx)) + with Log.Stop_Compilation s -> ([],ctx)

(* Eval String @@ -1733,7 +1769,7 @@ let eval_expr_str str lctx rctx = try let lxps = lexp_expr_str str lctx in let elxps = List.map OL.erase_type lxps in EV.eval_all elxps rctx false - with Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> []

let eval_decl_str str lctx rctx = let prev_lctx, prev_rctx = lctx, rctx in @@ -1741,5 +1777,5 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx - with Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) + with Log.Stop_Compilation s -> (prev_rctx, prev_lctx)

===================================== src/env.ml ===================================== @@ -30,7 +30,6 @@ * * --------------------------------------------------------------------------- *)

-open Util (* msg_error *) open Fmt (* make_title, table util *)

open Sexp @@ -41,10 +40,10 @@ module L = Lexp module BI = Big_int module DB = Debruijn

-let dloc = dummy_location +let dloc = Util.dummy_location

-let error loc msg = msg_error "ENV" loc msg; raise (internal_error msg) -let warning loc msg = msg_warning "ENV" loc msg +let fatal = Log.log_fatal ~section:"ENV" +let warning = Log.log_warning ~section:"ENV"

let str_idx idx = "[" ^ (string_of_int idx) ^ "]"

@@ -81,11 +80,11 @@ let rec value_equal a b = | Vin (c1), Vin (c2) -> c1 = c2 | Vout (c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 - | Vundefined, _ | _, Vundefined -> warning dloc "Vundefined"; false - | Vtype e1, Vtype e2 -> warning dloc "Vtype"; false + | Vundefined, _ | _, Vundefined -> warning "Vundefined"; false + | Vtype e1, Vtype e2 -> warning "Vtype"; false

| Closure (s1, b1, ctx1), Closure (s2, b2, ctx2) - -> warning dloc "Closure"; + -> warning "Closure"; if (s1 != s2) then false else true

| Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) @@ -178,14 +177,14 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - error dloc + fatal ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))

| _ -> x) with Not_found -> let n = match name with (_, Some n) -> n | _ -> "" in - error dloc ("Variable lookup failure. Var: "" ^ + fatal ("Variable lookup failure. Var: "" ^ n ^ "" idx: " ^ (str_idx idx))

let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) @@ -199,7 +198,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = (match (n, name) with | ((_, Some n1), (_, Some n2)) -> if (n1 != n2) then - error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + fatal ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ());

ref_cell := v

===================================== src/eval.ml ===================================== @@ -82,13 +82,12 @@ let rec_depth trace = List.length b

(* eval error are always fatal *) -let error loc msg = - msg_error "EVAL" loc msg; - flush stdout; - raise (internal_error msg) +let error loc ?print_action msg = + Log.log_error ~section:"EVAL" ~loc ?print_action msg; + Log.internal_error msg

-let fatal = msg_fatal "EVAL" -let warning = msg_warning "EVAL" +let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg +let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg

(* Print a message that look like this: * @@ -119,7 +118,7 @@ let debug_message error_type type_name type_string loc expr message =

(* Print value name followed by the value in itself, finally throw an exception *) let value_fatal = debug_message fatal value_name value_string -let value_error = debug_message error value_name value_string +let value_error = debug_message (error ?print_action:None) value_name value_string let elexp_fatal = debug_message fatal elexp_name elexp_string

@@ -341,16 +340,20 @@ let file_read loc depth args_val = match args_val with (* 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) - | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - error loc "File.read expects an in_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:"

let file_write loc depth args_val = match args_val with | [Vout channel; Vstring msg] -> Vcommand (fun () -> fprintf channel "%s" msg; (* FIXME: This should be the unit value! *) Vundefined) - | _ -> List.iter (fun v -> value_print v) args_val; - error loc "File.write expects an out_channel and a string" + | _ -> 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:"

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

@@ -470,9 +473,12 @@ and eval_call loc unef i f args = buildbody (arity - nargs - 1), buildctx args Myers.nil)

- with Not_found - -> error loc ("Requested Built-in `" ^ name ^ "` does not exist") - | e -> error loc ("Exception thrown from primitive `" ^ name ^"`")) + with + | Not_found -> + error loc ("Requested Built-in `" ^ name ^ "` does not exist") + | e -> + warning loc ("Exception thrown from primitive `" ^ name ^"`"); + raise e)

| Vtype e, _ (* We may call a Vlexp e.g. for "x = Map Int String". @@ -902,19 +908,27 @@ let array_empty loc depth args_val = match args_val with

let test_fatal loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_fatal section loc msg) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Fatal ~kind:"(Unit test fatal)" ~loc ~section msg); + Log.user_error msg + ) | _ -> error 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 () -> Util.msg_user_warning section loc msg; - tunit) + 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"

let test_info loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_info section loc msg; - tunit) + 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"

let test_location loc depth args_val = match args_val with @@ -1049,10 +1063,14 @@ let eval lxp ctx = eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx with e -> ( - print_rte_ctx (!global_eval_ctx); - print_eval_trace None; - raise 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 eval_decls decls ctx = eval_decls decls ctx ([], [])

===================================== src/fmt.ml ===================================== @@ -156,3 +156,6 @@ let yellow = "\x1b[33m" let magenta = "\x1b[35m" let cyan = "\x1b[36m" let reset = "\x1b[0m" + +let color_string color str = + color ^ str ^ reset

===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -68,16 +68,17 @@ let transfo (s: Lexp.subst) : substIR option = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in match s with - | S.Cons (Var _ as v, s) -> - (match transfo s off_acc (idx + 1) imp_cnt with - | Some (tail, off, imp) -> let newVar = shiftVar v off_acc - in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off, imp) - | None -> None) - | S.Cons (Imm (Sexp.Symbol (_, "")), s) - -> transfo s off_acc (idx + 1) (imp_cnt + 1) - | S.Shift (s, offset) -> transfo s (offset + off_acc) idx imp_cnt - | S.Identity -> Some ([], off_acc, imp_cnt) (* End of recursion *) + | S.Cons (Var _ as v, s, o) -> + let off_acc = off_acc + o in + (match transfo s off_acc (idx + 1) imp_cnt with + | Some (tail, off, imp) + -> let newVar = shiftVar v off_acc + in if newVar >= off then None (* Error *) + else Some (((shiftVar v off_acc), idx)::tail, off, imp) + | None -> None) + | S.Cons (Imm (Sexp.Symbol (_, "")), s, o) + -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) + | S.Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) in transfo s 0 0 0

@@ -144,8 +145,8 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = let is_identity s = let rec is_identity s acc = match s with - | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> acc = shift + | S.Cons(Var(_, idx), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | S.Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0

@@ -168,11 +169,11 @@ let inverse (s: Lexp.subst) : Lexp.subst option = | Some s1 -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () - else (print_string ("Subst-inversion-bug: " - ^ subst_string s ^ " ∘ " - ^ subst_string s1 ^ " == " - ^ subst_string (Lexp.scompose s1 s) - ^ " !!\n")) + else (Log.log_debug ("Subst-inversion-bug: " + ^ subst_string s ^ " ∘ " + ^ subst_string s1 ^ " == " + ^ subst_string (Lexp.scompose s1 s) + ^ " !!\n")) | _ -> ()); res

@@ -180,10 +181,9 @@ let inverse (s: Lexp.subst) : Lexp.subst option = * possible. This happens when the substitution replaces some variables * with non-variables, in which case the "inverse" is ambiguous. *) let rec invertible (s: subst) : bool = match s with - | S.Identity -> true - | S.Shift (s, _) -> invertible s - | S.Cons (e, s) -> (match e with Var _ -> true | _ -> e = impossible) - && invertible s + | S.Identity _ -> true + | S.Cons (e, s, _) -> (match e with Var _ -> true | _ -> e = impossible) + && invertible s

exception Not_invertible exception Ambiguous @@ -191,18 +191,16 @@ exception Ambiguous (* Lookup variable i in s⁻¹ *) let rec lookup_inv_subst (i : db_index) (s : subst) : db_index = match s with - | S.Identity -> i - | S.Shift (s, n) -> if i < n then - raise Not_invertible - else lookup_inv_subst (i - n) s - | S.Cons (Var (_, i'), s) when i' = i - -> (try let i'' = lookup_inv_subst i s in + | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible + | S.Identity o -> i - o + | S.Cons (Var (_, i'), s, o) when i' = i - o + -> (try let i'' = lookup_inv_subst i' s in assert (i'' != 0); raise Ambiguous with Not_invertible -> 0) - | S.Cons (e, s) + | S.Cons (e, s, o) -> assert (match e with Var _ -> true | _ -> e = impossible); - 1 + lookup_inv_subst i s + 1 + lookup_inv_subst (i - o) s

(* When going under a binder, we have the rule * (λe)[s] ==> λ(e[lift s]) @@ -226,7 +224,8 @@ let shift_inv_subst n s (* We could define it as: * = compose_inv_subst s (S.shift n) * But this can fail if an element of `s` maps to a var with index < n *) - = let shift_n = match inverse (S.shift n) with + = if n = 0 then s else + let shift_n = match inverse (S.shift n) with | Some s -> s | _ -> assert (false) in Lexp.scompose s shift_n @@ -236,13 +235,14 @@ let shift_inv_subst n s * But we can try and do it more directly. *) let rec compose_inv_subst (s' : subst) (s : subst) = match s' with - | S.Cons (e, s') -> S.Cons (apply_inv_subst e s, compose_inv_subst s' s) - | S.Identity -> (match inverse s with - | Some s -> s - (* FIXME: could also be Ambiguous, depending on `s`. *) - | None -> raise Not_invertible) - | S.Shift (s', n) - -> compose_inv_subst s' (shift_inv_subst n s) + | S.Cons (e, s', o) -> + let s = shift_inv_subst o s in + (* FIXME: Why don't we ever return a Shift? *) + S.cons (apply_inv_subst e s) (compose_inv_subst s' s) + | S.Identity o -> (match inverse (shift_inv_subst o s) with + | Some s -> s + (* FIXME: could also be Ambiguous, depending on `s`. *) + | None -> raise Not_invertible)

(* Apply s⁻¹ to e. * The function presumes that `invertible s` was true. @@ -251,9 +251,10 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (apply_inv_subst e s)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (SLlub (apply_inv_subst e1 s, apply_inv_subst e2 s)) + (* Should we use mkSLlub? *) + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e

===================================== src/lexer.ml ===================================== @@ -45,7 +45,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos (* The returned Sexp may not be a Node. *) : sexp * pretoken list * bytepos * charpos = match pts with - | [] -> (internal_error "No next token!") + | [] -> (Log.internal_error "No next token!") | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) | (Pretoken ({file;line;column;docstr}, name) :: pts')

===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language.

-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2019 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -69,7 +69,7 @@ type ltype = lexp | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * lexp + | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of U.location * label @@ -80,8 +80,8 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) - (* The `subst` only applies to the lexp associated - * with the metavar's "value", not to the ltype. *) + (* The `subst` will be applied to the the metavar's value when it + * gets instantiated. *) | Metavar of meta_id * subst * vname (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref @@ -135,7 +135,7 @@ type varbind = * no `eq` hash-tables, ...). * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique - * integer in order to procude a hash anyway (and we'd have to write the hash + * integer in order to produce a hash anyway (and we'd have to write the hash * function by hand, tho that might be a good idea anyway). *)

@@ -166,7 +166,7 @@ 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 - -> U.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!" + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!"

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

@@ -205,6 +205,21 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es))

+let mkSLlub' (e1, e2) = match (e1, e2) with + | (SortLevel SLz, _) | (_, SortLevel SLz) + -> Log.log_fatal ~section:"internal" "lub of SLz" + | (SortLevel (SLsucc _), SortLevel (SLsucc _)) + -> Log.log_fatal ~section:"internal" "lub of two SLsucc" + | ((SortLevel _ | Var _ | Metavar _ | Susp _), + (SortLevel _ | Var _ | Metavar _ | Susp _)) + -> SLlub (e1, e2) + | _ -> Log.log_fatal ~section:"internal" "SLlub of non-level" + +let mkSLsucc e = match e with + | SortLevel _ | Var _ | Metavar _ | Susp _ + -> SLsucc e + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level" + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -260,6 +275,38 @@ and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) s l v let ssink = S.sink (fun l i -> mkVar (l, i))

+(* Shift by a negative amount! *) +let rec sunshift n = + if n = 0 then S.identity + else (assert (n >= 0); + S.cons impossible (sunshift (n - 1))) + +let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) + +(* The quick test below seemed to indicate that about 50% of the "sink"s + * are applied on top of another "sink" and hence cound be combined into + * a single "Lift^n" constructor. Doesn't seem high enough to justify + * the complexity of adding a `Lift` to `subst`. + *) +(* let sink_count_total = ref 0 + * let sink_count_optimizable = ref 0 + * + * let ssink l s = + * sink_count_total := 1 + !sink_count_total; + * (match s with + * | S.Cons (Var (_, 0), (S.Identity o | S.Cons (_, _, o)), 0) when o > 0 + * -> sink_count_optimizable := 1 + !sink_count_optimizable + * | _ -> ()); + * if ((!sink_count_total) mod 10000) = 0 then + * (print_string ("Optimizable = " + * ^ (string_of_int ((100 * !sink_count_optimizable) + * / !sink_count_total)) + * ^ "%\n"); + * if !sink_count_total > 100000 then + * (sink_count_total := !sink_count_total / 2; + * sink_count_optimizable := !sink_count_optimizable / 2)); + * S.sink (fun l i -> mkVar (l, i)) l s *) +

let rec lexp_location e = match e with @@ -292,8 +339,9 @@ let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (mkSusp e1 s, mkSusp e2 s)) + | SortLevel (SLsucc e') -> mkSortLevel (mkSLsucc (mkSusp e' s)) + | SortLevel (SLlub (e1, e2)) + -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e @@ -357,8 +405,10 @@ let clean e = let rec clean s e = match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (clean s e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (clean s e1, clean s e2)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) + | SortLevel (SLlub (e1, e2)) + (* FIXME: The new SLlub could have `succ` on both sides! *) + -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (l, _) -> e | Builtin _ -> e @@ -541,9 +591,10 @@ let rec lexp_unparse lxp = and lexp_string lxp = sexp_string (lexp_unparse lxp)

and subst_string s = match s with - | S.Identity -> "Id" - | S.Shift (s, n) -> "(↑"^ string_of_int n ^ " " ^ subst_string s ^ ")" - | S.Cons (l, s) -> lexp_name l ^ " · " ^ subst_string s + | S.Identity o -> "↑" ^ string_of_int o + | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s + | S.Cons (l, s, o) + -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"

and lexp_name e = match e with @@ -606,20 +657,29 @@ let debug_ppctx = ref ( ("print_implicit", Bool (true)); ("separate_decl" , Bool (false) );])

-let pp_pretty ctx = match SMap.find "pretty" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_type ctx = match SMap.find "print_type" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_dbi ctx = match SMap.find "print_dbi" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_size ctx = match SMap.find "indent_size" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_color ctx = match SMap.find "color" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_decl ctx = match SMap.find "separate_decl" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_indent ctx = match SMap.find "indent_level" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_parent ctx = match SMap.find "parent" ctx with Expr e -> e | _ -> U.typer_unreachable "" -let pp_meta ctx = match SMap.find "metavar" ctx with Expr e -> e | _ -> U.typer_unreachable "" -let pp_grammar ctx = match SMap.find "grammar" ctx with Predtl p -> p | _ -> U.typer_unreachable "" -let pp_colsize ctx = match SMap.find "col_size" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_colmax ctx = match SMap.find "col_max" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_erasable ctx = match SMap.find "print_erasable" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_implicit ctx = match SMap.find "print_implicit" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let smap_bool s ctx = + match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" +and smap_int s ctx = + match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" +and smap_lexp s ctx = + match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" +and smap_predtl s ctx = + match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable" + +let pp_pretty = smap_bool "pretty" +let pp_type = smap_bool "print_type" +let pp_dbi = smap_bool "print_dbi" +let pp_size = smap_int "indent_size" +let pp_color = smap_bool "color" +let pp_decl = smap_bool "separate_decl" +let pp_indent = smap_int "indent_level" +let pp_parent = smap_lexp "parent" +let pp_meta = smap_lexp "metavar" +let pp_grammar = smap_predtl "grammar" +let pp_colsize = smap_int "col_size" +let pp_colmax = smap_int "col_max" +let pp_erasable = smap_bool "print_erasable" +let pp_implicit = smap_bool "print_implicit"

let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx @@ -938,17 +998,17 @@ let rec eq e1 e2 = and subst_eq s1 s2 = s1 == s2 || match (s1, s2) with - | (S.Identity, S.Identity) -> true - | (S.Cons (e1, s1), S.Cons (e2, s2)) - -> eq e1 e2 && subst_eq s1 s2 - | (S.Shift (s1, o1), S.Shift (s2, o2)) - -> let o = min o1 o2 in - subst_eq (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) - | (S.Shift (S.Cons (e1, s1), o1), S.Cons (e2, s2)) - -> eq (mkSusp e1 (S.shift o1)) e2 - && subst_eq (S.mkShift s1 o1) s2 - | (S.Cons (e1, s1), S.Shift (S.Cons (e2, s2), o2)) - -> eq e1 (mkSusp e2 (S.shift o2)) - && subst_eq s1 (S.mkShift s2 o2) + | (S.Identity o1, S.Identity o2) -> o1 = o2 + | (S.Cons (e1, s1, o1), S.Cons (e2, s2, o2)) + -> if o1 = o2 then + eq e1 e2 && subst_eq s1 s2 + else if o1 > o2 then + let o = o1 - o2 in + eq (mkSusp e1 (S.shift o)) e2 + && subst_eq (S.mkShift s1 o) s2 + else + let o = o2 - o1 in + eq e1 (mkSusp e2 (S.shift o)) + && subst_eq s1 (S.mkShift s2 o) | _ -> false

===================================== src/log.ml ===================================== @@ -0,0 +1,216 @@ +(* log.ml --- User Errors/Warnings log for Typer. -*- coding: utf-8 -*- + +Copyright (C) 2019 Free Software Foundation, Inc. + +Author: Jean-Alexandre Barszcz jalex_b@hotmail.com +Keywords: languages, lisp, dependent types. + +This file is part of Typer. + +Typer is free software; you can redistribute it and/or modify it under the +terms of the GNU General Public License as published by the Free Software +Foundation, either version 3 of the License, or (at your option) any +later version. + +Typer is distributed in the hope that it will be useful, but WITHOUT ANY +WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +FOR A PARTICULAR PURPOSE. See the GNU General Public License for +more details. + +You should have received a copy of the GNU General Public License along with +this program. If not, see http://www.gnu.org/licenses/. *) + +open Util + +(* 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 Util.string_uppercase 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 string_of_location (loc : location) = + (loc.file ^ ":" + ^ string_of_int loc.line ^ ":" + ^ string_of_int loc.column ^ ":") + +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 parens s = "(" ^ s ^ ")" in + (option_default "" (option_map string_of_location loc) + ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":" + ^ option_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 () = + 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 + +let print_and_clear_log () = + print_log (); clear_log () + +let log_msg level ?kind ?section ?print_action ?loc msg = + log_entry (mkEntry level ?kind ?section ?print_action ?loc msg) + +exception Internal_error of string +let internal_error s = raise (Internal_error s) + +exception User_error of string +let user_error s = raise (User_error s) + +exception Stop_Compilation of string +let stop_compilation s = raise (Stop_Compilation s) + +let log_fatal ?section ?print_action ?loc m = + log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; + internal_error "Compiler Fatal Error" +let log_error = log_msg Error ?kind:None +let log_warning = log_msg Warning ?kind:None +let log_info = log_msg Info ?kind:None +let log_debug = log_msg Debug ?kind:None + +let stop_on_error () = + let count = error_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" errors\n") + +let stop_on_warning () = + stop_on_error (); + let count = warning_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" warnings\n") + +(* 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 ===================================== @@ -38,6 +38,9 @@ module S = Subst (* module L = List *) module DB = Debruijn

+let error_tc = Log.log_error ~section:"TC" +let warning_tc = Log.log_warning ~section:"TC" + (* `conv_erase` is supposed to be safe according to the ICC papers. *) let conv_erase = true (* Makes conv ignore erased terms. *)

@@ -152,7 +155,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = let (subst, _) = List.fold_left (fun (s,d) (_, arg) -> - (S.Cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d), s), + (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s, d + 1)) (S.identity, 0) aargs in @@ -161,7 +164,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = -> match default with | Some (v,default) -> lexp_whnf (push_susp default (S.substitute e')) ctx - | _ -> U.msg_error "WHNF" l + | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in @@ -332,7 +335,7 @@ let rec mkSLlub ctx e1 e2 = let ce2 = level_canon (L.clean e2') in if level_leq ce1 ce2 then e1 else if level_leq ce2 ce1 then e2 - else mkSortLevel (SLlub (e1, e2)) + else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)

type sort_compose_result = SortResult of ltype @@ -399,17 +402,17 @@ let rec check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else (U.msg_error "TC" (lexp_location e) + else (error_tc ~loc:(lexp_location e) ("Type mismatch for " ^ lexp_string (L.clean e) ^ " : " ^ lexp_string (L.clean t) ^ " != " ^ lexp_string (L.clean t')); - (* U.internal_error "Type mismatch" *)) in + (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in (match lexp_whnf s ctx with | Sort _ -> () - | _ -> U.msg_error "TC" (lexp_location t) + | _ -> error_tc ~loc:(lexp_location t) ("Not a proper type: " ^ lexp_string t)); (* FIXME: return the `sort` rather than the surrounding `lexp`! *) s in @@ -419,7 +422,7 @@ let rec check'' erased ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) - -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; + -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -440,8 +443,8 @@ let rec check'' erased ctx e = mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> ((* U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; - * U.internal_error "Reached unreachable sort!"; *) + -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; + * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) -> let _ = check_type DB.set_empty Myers.nil t in @@ -450,7 +453,7 @@ let rec check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - U.msg_error "TC" l + error_tc ~loc:l ("Var `" ^ maybename name ^ "`" ^ " can't be used here, because it's `erasable`"); lookup_type ctx v @@ -483,14 +486,14 @@ let rec check'' erased ctx e = match sort_compose ctx l ak k1 k2 with | SortResult k -> k | SortInvalid - -> U.msg_error "TC" l "Invalid arrow: inner TypelLevel argument"; + -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; mkSort (l, StypeOmega) | SortK1NotType - -> (U.msg_error "TC" (lexp_location t1) + -> (error_tc ~loc:(lexp_location t1) "Not a proper type"; mkSort (l, StypeOmega)) | SortK2NotType - -> (U.msg_error "TC" (lexp_location t2) + -> (error_tc ~loc:(lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) @@ -508,12 +511,12 @@ let rec check'' erased ctx e = match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then - (U.msg_error "TC" (lexp_location arg) + (error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) else (); assert_type ctx arg t1 at; mkSusp t2 (S.substitute arg) - | _ -> (U.msg_error "TC" (lexp_location arg) + | _ -> (error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " ^ lexp_string ft ^ ")!"); ft)) @@ -535,18 +538,18 @@ let rec check'' erased ctx e = -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* FIXME: We shouldn't use Inverse_subst - * in the plain `check` code! *) - (Inverse_subst.apply_inv_subst level' - (S.shift n)) - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string tt ^")"); - DB.print_lexp_ctx ictx; - (* U.internal_error "Oops"; *) - level), + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, n + 1)) @@ -579,7 +582,7 @@ let rec check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (U.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in SMap.iter @@ -596,7 +599,7 @@ let rec check'' erased ctx e = (S.cons (Var (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes - | _,_ -> (U.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx)) in let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in @@ -608,15 +611,15 @@ let rec check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 then - U.msg_warning "TC" l "Redundant default clause"; + warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in assert_type nctx d (mkSusp ret (S.shift 1)) (check (DB.set_sink 1 erased) nctx d) | None -> if diff > 0 then - U.msg_error "TC" l ("Non-exhaustive match: " + error_tc ~loc:l ("Non-exhaustive match: " ^ string_of_int diff ^ " cases missing")) - | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); + | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) -> (match lexp_whnf t ctx with @@ -644,10 +647,10 @@ let rec check'' erased ctx e = buildtype fargs) in buildtype fargs with Not_found - -> (U.msg_error "TC" l + -> (error_tc ~loc:l ("Constructor "" ^ name ^ "" does not exist"); DB.type_int)) - | _ -> (U.msg_error "TC" (lexp_location e) + | _ -> (error_tc ~loc:(lexp_location e) ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) @@ -659,7 +662,7 @@ let rec check'' erased ctx e =

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

let check = check'

@@ -789,7 +792,7 @@ let rec get_type ctx e = | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t, _) -> t | SortLevel _ -> DB.type_level - | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (SLsucc e))) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, name), idx) as v) -> lookup_type ctx v @@ -835,9 +838,9 @@ let rec get_type ctx e = -> level | Sort (_, Stype level') -> mkSLlub ctx level - (try Inverse_subst.apply_inv_subst level' - (S.shift n) - with _ -> level) + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) | tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) @@ -918,7 +921,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> U.internal_error "Metavar in erase_type" + | L.Metavar _ -> Log.internal_error "Metavar in erase_type"

and filter_arg_list lst = let rec filter_arg_list lst acc = @@ -956,7 +959,7 @@ and clean_map cases = (** Turning a set of declarations into an object. **)

let ctx2tup ctx nctx = - (*U.debug_msg ("Entering ctx2tup\n");*) + (*Log.debug_msg ("Entering ctx2tup\n");*) assert (M.length nctx >= M.length ctx && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); let rec get_blocs nctx blocs = @@ -974,7 +977,7 @@ let ctx2tup ctx nctx = let type_label = (loc, "record") in let offset = List.length types in let types = List.rev types in - (*U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) + (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) Call (Cons (Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t)

===================================== src/pexp.ml ===================================== @@ -25,7 +25,7 @@ open Sexp (* Symbol *) open Lexer open Grammar

-let pexp_error = msg_error "PEXP" +let pexp_error loc = Log.log_error ~section:"PEXP" ~loc

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

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

open Util

-let prelexer_error = msg_error "PRELEXER" +let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc

type pretoken = | Pretoken of location * string

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

-let sexp_error = msg_error "SEXP" +let sexp_error ?print_action loc msg = + Log.log_error ~section:"SEXP" ?print_action ~loc msg

type integer = (* Num.num *) int type symbol = location * string @@ -119,7 +120,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) let sexp_parse = sexp_parse g in

let rec compose_symbol (ss : symbol list) = match ss with - | [] -> (internal_error "empty operator!") + | [] -> (Log.internal_error "empty operator!") | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) (List.rev ss))) in

@@ -201,19 +202,19 @@ let sexp_parse_all grm tokens limit : sexp * token list = | Some token -> match SMap.find token grm with | (Some ll, Some _) -> ll + 1 - | _ -> (internal_error ("Can't find level of ""^token^""")) + | _ -> (Log.internal_error ("Can't find level of ""^token^""")) in let (e, rest) = sexp_parse grm tokens level [] [] [] in let se = match e with | Node (Symbol (_, ""), [e]) -> e | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (internal_error "Didn't find a toplevel") in + | _ -> (Log.internal_error "Didn't find a toplevel") in match rest with | [] -> (se,rest) | Symbol (l,t) :: rest -> if not (Some t = limit) then sexp_error l ("Stray closing token: "" ^ t ^ """); (se,rest) - | _ -> (internal_error "Stopped parsing before the end!") + | _ -> (Log.internal_error "Stopped parsing before the end!")

(* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *)

===================================== src/subst.ml ===================================== @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp

-Copyright (C) 2016-2017 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca

@@ -119,55 +119,86 @@ type db_offset = int (* DeBruijn index offset. *) * - for better modularity of the code. * - to break a mutual dependency between the Lexp and the Subst modules. *) type 'a subst = (* lexp subst *) - (* Lift (n,m) increases indices≥N by M. + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * 'a subst * db_offset *) +(* Lift (n,m) increases indices≥N by M. * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - | Identity - | Cons of 'a * 'a subst - (* we enter a let/lambda/case/inductive (with formal args) *) - | Shift of 'a subst * db_offset (* | Lift of db_index * db_offset *)

+(* Build Myers's "stack" element. *) +(* let mkCons e s o = match s with + * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 + * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) + * | _ -> Cons (e, s, o, 1, s, o) *) + (* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a) (mkShift: 'a -> db_offset -> 'a) (s: 'a subst) (l : 'b) (v:db_index) : 'a = let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = match s with - | Identity -> mkVar l (v+o) - | Shift (s, o') -> lookup' (o+o') s v - | Cons (e, s) -> if v>0 then lookup' o s (v-1) - else mkShift e o + | Identity o' -> mkVar l (v + o + o') + (* Use Myers's fastlane when applicable: + * | Cons (_, _, _, sk, s, o') when v >= sk -> lookup' (o + o') s (v - sk) *) + | Cons (e, s, o') -> let o = o + o' in + if v > 0 then lookup' o s (v - 1) + else mkShift e o in lookup' 0 s v

let mkShift s (m:db_offset) = if m>0 then - match s with Shift (s', n) -> Shift (s', n+m) - | _ -> Shift (s, m) + match s with Identity o -> Identity (o + m) + | Cons (e, s, o) -> Cons (e, s, o + m) else s

(* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) = mkShift Identity m +let shift (m:db_offset) = Identity m + +(* Return a substitution which replaces #0 with `e` and then applies `s` + * to the rest. *) +let cons e s = Cons (e, s, 0)

(* The trivial substitution which doesn't do anything. *) -let identity = Identity +let identity = Identity 0

(* Test if a substitution is trivial. The "_p" stands for "predicate". *) -let identity_p s = match s with | Identity -> true | _ -> false +let identity_p s = match s with | Identity o -> o = 0 | _ -> false

(* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) let compose (mkSusp : 'a -> 'a subst -> 'a) - (s1: 'a subst) (s2: 'a subst) : 'a subst = + (s1: 'a subst) (s2: 'a subst) : 'a subst = + (* There is a bit of flexibility in what we return, in the sense + * that some shifts can be pushed more or less down. Here we + * want the shifts to float as far outside as possible. *) let rec compose' (s1: 'a subst) (s2: 'a subst) : 'a subst = - match s1, s2 with - | (Identity, s2) -> s2 - | (s1, Identity) -> s1 - | (s1, Shift (s2, o2)) -> mkShift (compose' s1 s2) o2 - | (Shift (s1, o1), Cons (e, s2)) -> compose' (mkShift s1 (o1-1)) s2 - | (Cons (e, s1), s2) -> Cons (mkSusp e s2, compose' s1 s2) + match s1 with + | Identity o1 + -> let rec compose_id o1 s o = match s with + | Identity o2 -> Identity (o + o1 + o2) + | Cons (e2, s2, o2) (* , sk2, s2', o2' *) + -> (* Myers's fastlane: + * if o1 >= sk2 then compose_id (o1 - sk2) s2' (o + o2') *) + if o1 > 0 then compose_id (o1 - 1) s2 (o + o2) + else Cons (e2, s2, o + o2) + in compose_id o1 s2 0 + | Cons (e1, s1, o1) + -> let rec compose_cons o1 s o = match s with + | Identity o2 -> Cons (e1, s1, o + o1 + o2) + | Cons (e2, s2, o2) (* , sk2, s2', o2' *) + -> (* Myers's fastlane: + * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) + if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) + else + (* Pull out o2's shift and compose the two Cons. *) + let s' = cons e2 s2 in + Cons (mkSusp e1 s', compose' s1 s', o + o2) + in compose_cons o1 s2 0 in compose' s1 s2

(* Adjust a substitution for use under one more binder. @@ -175,11 +206,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * from Δs,x to Δₜ,x. * Also known as `lift`. *) let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = - Cons (mkVar l 0, mkShift s 1) - -(* Return a substitution which replaces #0 with `e` and the applies `s` - * to the rest. *) -let cons e s = Cons (e, s) + cons (mkVar l 0) (mkShift s 1)

(* Return a substitution which replaces #0 with `e`. *) -let substitute e = Cons (e, Identity) +let substitute e = cons e identity

===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -27,6 +27,8 @@ module DB = Debruijn

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

+let log_info = Log.log_info ~section:"UNIF" + (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*)

@@ -45,7 +47,7 @@ let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst = U.IMap.add id (MVal lxp) subst

let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with - | MVal _ -> U.internal_error + | MVal _ -> Log.internal_error "Checking occurrence of an instantiated metavar!!" | MVar (sl, _, _) -> let rec oi e = match e with @@ -57,7 +59,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, i) -> false - | Susp (e, s) -> U.internal_error "`e` should be "clean" here!?" + | Susp (e, s) -> Log.internal_error "`e` should be "clean" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs @@ -81,7 +83,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Metavar (id', _, name) when id' = id -> true | Metavar (id', _, _) -> (match metavar_lookup id' with - | MVal e -> U.internal_error "`e` should be "clean" here!?" + | MVal e -> Log.internal_error "`e` should be "clean" here!?" (* ; oi e *) | MVar (sl', t, cl) -> if sl' > sl then @@ -132,14 +134,16 @@ let rec unify (e1: lexp) (e2: lexp) and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = + if e1 == e2 then Some [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - let changed = not (e1 == e1' && e2 == e2') in + if e1' == e2' then Some [] else + let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then Some [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _) | (Inductive _, Inductive _)) + | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then Some [] else None | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r @@ -152,7 +156,17 @@ and unify' (e1: lexp) (e2: lexp) (* | (Inductive _ as l, r) -> unify_induct l r subst *) | (Sort _ as l, r) -> unify_sort l r ctx vs' | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' - | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)]) + | (Inductive (_loc1, label1, args1, consts1), + Inductive (_loc2, label2, args2, consts2)) + -> (* print_string ("Unifying inductives " + * ^ snd label1 + * ^ " and " + * ^ snd label2 + * ^ "\n"); *) + unify_inductive ctx vs' args1 args2 consts1 consts2 + | _ -> Some (if OL.conv_p ctx e1' e2' then [] + else ((* print_string "Unification failure on default\n"; *) + [(e1, e2)]))

(********************************* Type specific unify *******************************)

@@ -215,17 +229,16 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with - | MVal _ -> U.internal_error + | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" | MVar (_, t, _) -> push_susp t s in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> print_string "Unification of metavar failed:\n "; - print_string ("?[" ^ subst_string s ^ "]"); - print_string "\nAgainst:\n "; - lexp_print lxp; - print_string "\n"; - None + -> log_info ?loc:None ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); + None | lxp' when occurs_in idx lxp' -> None | lxp' -> metavar_table := associate idx lxp' (!metavar_table); @@ -233,11 +246,12 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | Some [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then @@ -401,6 +415,26 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

+and unify_inductive ctx vs args1 args2 consts1 consts2 = + let unif_formals ctx vs args1 args2 + = if not (List.length args1 == List.length args2) then (ctx, vs, None) else + List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2)) + -> (DB.lexp_ctx_cons ctx v1 Variable t1, + OL.set_shift vs, + if not (ak1 == ak2) then None + else unify_and (unify' t1 t2 ctx vs) residue)) + (ctx, vs, Some []) + (List.combine args1 args2) in + let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in + if not (SMap.cardinal consts1 == SMap.cardinal consts2) then None else + SMap.fold (fun cname args1 residue + -> match SMap.find cname consts2 with + | args2 -> let (_ctx, _vs, residue') + = unif_formals ctx vs args1 args2 in + unify_and residue' residue + | exception Not_found -> None) + consts1 residue + (** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst = * let test l1 l2 subst =

===================================== src/util.ml ===================================== @@ -51,114 +51,6 @@ let loc_string loc =

let loc_print loc = print_string (loc_string loc)

-(* - * -1 - Nothing (* During testing we may want to produce errors *) - * 0 - Fatal - * 1 - Error - * 2 - Warning - * 3 - Info - *) - -let typer_verbose = ref 20 - -exception Internal_error of string -let internal_error s = raise (Internal_error s) - -exception Unreachable_error of string -let typer_unreachable s = raise (Unreachable_error s) - -exception User_error of string -let user_error s = raise (User_error s) - -exception Stop_Compilation of string -let stop_compilation s = raise (Stop_Compilation s) - -(* `error list * warning list` both of type `level * kind * section * loc * msg` *) -type error_log_type = ((int * string * string * location * string) list * - (int * string * string * location * string) list) - -let empty_error_log : error_log_type = ([],[]) - -let error_log = ref empty_error_log - -let error_count () : int = let errors, _ = !error_log in - List.length errors - -let warning_count () : int = let _, warnings = !error_log in - List.length warnings - -let new_error lvl kind section loc msg = let errors, warnings = !error_log in - error_log := ((lvl,kind,section,loc,msg)::errors,warnings) - -let new_warning lvl kind section loc msg = let errors, warnings = !error_log in - error_log := (errors,(lvl,kind,section,loc,msg)::warnings) - -let reset_error_log () = error_log := empty_error_log - -(* Section is the name of the compilation step [for debugging] *) -(* 'prerr' output is ugly *) -let msg_message (error : bool) lvl kind section (loc: location) msg = - let message = (loc.file - ^ ":" ^ string_of_int loc.line - ^ ":" ^ string_of_int loc.column - ^ ":" ^ kind - ^ (if section = "" then " " else "(" ^ section ^ ") ") - ^ msg ^ "\n") in - - if error then - new_error lvl kind section loc msg - else - new_warning lvl kind section loc msg; - - if lvl <= !typer_verbose then - print_string message - else () - -let stop_on_error () = if (0 < (error_count ())) then - (let count = error_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" error\n")) - else () - -let stop_on_warning () = (stop_on_error (); - if (0 < (warning_count ())) then - let count = warning_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" warning\n") - else ()) - -let catch_error () = try stop_on_error () - with e -> match e with - | Stop_Compilation msg -> print_string msg - | _ -> () - -let msg_fatal s l m = - msg_message false 0 "[X] Fatal " s l m; - flush stdout; - reset_error_log (); - internal_error "Compiler Fatal Error" - -let msg_error = msg_message true 1 "Error:" -let msg_warning = msg_message false 2 "Warning:" -let msg_info = msg_message false 3 "Info:" - -let msg_user_fatal s l m = - msg_message true 1 "(Unit test fatal):" s l m; - flush stdout; - reset_error_log (); - user_error "User Fatal Error" - -let msg_user_warning = msg_message false 2 "(Unit test warning):" -let msg_user_info = msg_message false 3 "(Unit test info):" - -(* Compiler Internal Debug print *) -let debug_msg expr = - if 4 <= !typer_verbose then (print_string expr; flush stdout) else () - -let not_implemented_error () = internal_error "not implemented" - let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b)

@@ -214,3 +106,13 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string = let diff = (dim - string_width str) in let lpad = max diff 0 in (String.make lpad char_) ^ str + +let option_default (default : 'a) (opt : 'a option) : 'a = + match opt with + | None -> default + | Some x -> x + +let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = + match opt with + | None -> None + | Some x -> Some (fn x)

===================================== tests/inverse_test.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_test.ml --- Test the substitution-inversion algorithm * - * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * Copyright (C) 2016-2019 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -65,14 +65,6 @@ let input = ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), false):: []

-let is_identity s = - let rec is_identity s acc = - match s with - | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> acc = shift - | _ -> S.identity_p s - in is_identity s 0 - let generateRandInput shiftMax numberOfTest = Random.self_init (); let rec generateList shiftMax numberOfTest =

===================================== tests/unify_test.ml ===================================== @@ -1,6 +1,6 @@ (* unify_test.ml --- Test the unification algorithm * - * Copyright (C) 2016-2018 Free Software Foundation, Inc. + * Copyright (C) 2016-2019 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -183,7 +183,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

::(input_type , input_type_t , Equivalent) (* 44 *)

- ::(Metavar (0, S.Identity, (Util.dummy_location, Some "M")), + ::(Metavar (0, S.identity, (Util.dummy_location, Some "M")), Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)

::[]

===================================== tests/utest_lib.ml ===================================== @@ -76,7 +76,7 @@ let global_ftitle = ref ""

let set_verbose lvl = global_verbose_lvl := lvl; - (if lvl >= 3 then U.typer_verbose := 20 else U.typer_verbose := (-1)) + Log.set_typer_log_level (if lvl >= 3 then Log.Debug else Log.Nothing)

let arg_defs = [ ("--verbose=",

View it on GitLab: https://gitlab.com/monnier/typer/compare/f23283c36f16d75a505e4cffcb137ababff...