Octobre 2021 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer] Pushed new branch typer-subcommands
by Simon Génier (＠ilovemonoids) 28 Oct '21

28 Oct '21

Simon Génier pushed new branch typer-subcommands at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/typer-subcommands You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch typerc
by Simon Génier (＠ilovemonoids) 28 Oct '21

28 Oct '21

Simon Génier deleted branch typerc at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][remove-artisanal-printing] 6 commits: Upgrade to OCaml 4.11.
by Simon Génier (＠ilovemonoids) 28 Oct '21

28 Oct '21

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

1 0

[Git][monnier/typer][soilih] 3 commits: my symbol
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 19 Oct '21

19 Oct '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 2910ba93 by Soilih BEN SOILIH at 2021-10-18T21:54:10-04:00 my symbol - - - - - 00d0160e by Soilih BEN SOILIH at 2021-10-18T23:57:07-04:00 fixing on_req_symbol method - - - - - 4e3f9651 by Soilih BEN SOILIH at 2021-10-19T00:02:06-04:00 - - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -87,6 +87,15 @@ let lsp_pos_of_pos_end (p:Source.Location.t) : Lsp.Types.Position.t = let lsp_range_of_loc (l:Source.Location.t) : Lsp.Types.Range.t = Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start l) ~end_:(lsp_pos_of_pos_end l) +let lsp_pos_of_pos_start_for_symbol (p:Source.Location.t) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(p.start_line - 1) ~character:(p.start_column) + +let lsp_pos_of_pos_end_for_symbol (p:Source.Location.t) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(p.end_line - 1) ~character:(p.end_column) + +let lsp_range_of_loc_for_symbol (l:Source.Location.t) : Lsp.Types.Range.t = + Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start_for_symbol l) ~end_:(lsp_pos_of_pos_end_for_symbol l) + let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (location : Source.Location.t): Util.vname = match vname_list with | [] -> let loc = Source.Location.dummy in @@ -819,16 +828,20 @@ let filter_the_list_list (list_list: list_in_list) : list_in_list = let take_all_list_el (list_list: list_in_list) = let rec foo (ll:list_in_list) ret_list = match list_list with - | [] -> [] - | hd::tl -> let hdl = List.nth hd 0 in - foo tl (hdl::ret_list) + | [] -> ret_list + | [n] -> List.append n ret_list + | [hd;tl] -> let apl = List.append hd tl in + List.append apl ret_list + | hd::ml::tl -> let apl = List.append hd ml in + foo tl (List.append apl ret_list) in foo list_list [] let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = - let lst = take_all_list_el list_list in + let filtred_list = filter_the_list_list list_list in + let lst = take_all_list_el filtred_list in List.map ( fun x -> let ((l,s),_,_) = x in - let range = lsp_range_of_loc l in + let range = lsp_range_of_loc_for_symbol l in let nm = Option.get s in Lsp.Types.DocumentSymbol.create ~name:nm @@ -1055,6 +1068,36 @@ class lsp_server = Hashtbl.remove buffers d.uri; Linol_lwt.return () + (*method! config_hover = Some (`Bool true)*) + + (*method! config_definition = Some (`Bool true)*) + + (*method! config_symbol = Some (`Bool true)*) + + method! config_modify_capabilities arg = + let completionProvider = + Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"] + ~resolveProvider:true () + in + + let documentSymbol = + Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true () + in + + let hoverOption = + Lsp.Types.HoverOptions.create ~workDoneProgress:true () + in + + let definitionOption = + Lsp.Types.DefinitionOptions.create ~workDoneProgress:true () + in + + { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider ; + Lsp.Types.ServerCapabilities.hoverProvider = Some (`HoverOptions hoverOption); + Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption); + Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol) + } + method! on_req_definition ~notify_back ~id ~uri ~pos _st = match Hashtbl.find buffers uri with @@ -1097,10 +1140,6 @@ class lsp_server = let e = Some r in let f = Linol_lwt.return e in f - method! config_hover = Some (`Bool true) - - method! config_definition = Some (`Bool true) - (* provisional, to be done later *) method! on_req_execute_command ~notify_back ~id _c _args = match _c with @@ -1113,14 +1152,6 @@ class lsp_server = (Lsp.Types.Command.create ~title:_c ~command:_c () ) in let e = Linol_lwt.return h in e | _ -> assert false - - method! config_modify_capabilities arg = - let completionProvider = - (* TODO even if this re-enabled in general, it should stay disabled for - emacs. It makes completion too slow *) - Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"] - ~resolveProvider:true () in - { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider} (* provisional, to be done later *) @@ -1157,12 +1188,13 @@ class lsp_server = let f = Linol_lwt.return e in f method! on_req_symbol ~notify_back ~id ~uri () = - let doc_ = self#find_doc uri in - let doc_state = Option.get doc_ in - let (_,(list_list, _)) = readstring doc_state.content in - let r = create_symbols list_list in - let e = Some (`DocumentSymbol r) in - let f = Linol_lwt.return e in f + + match Hashtbl.find buffers uri with + + | state_after_processing -> let (_,(list_list, _)) = state_after_processing in + let r = create_symbols list_list in + let e = Some (`DocumentSymbol r) in + let f = Linol_lwt.return e in f end @@ -1172,7 +1204,7 @@ end let comp (a:string) (b:string) : string = if (String.equal a b) then "/*******-----:-):-):-):-):-):-):-)__________SUCCESS_______:-):-):-):-):-):-):-)-----*******/\n\n\n" else "/*******-----:-(:-(:-(:-(:-(:-(:-(____FAILED___:-(:-(:-(:-(:-(:-(:-(-----*******/\n\n\n" - + let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) = let (_, ast) = readstring content in let (list_list, _) = ast in @@ -1225,7 +1257,6 @@ let test () = hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,24) "##Int"; hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,24) "##Int"; hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,26) "##Int"; - sep name "FUNCTION(LAMBDA)"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "##Int"; @@ -1318,9 +1349,6 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,14) "" - - - (*=======================================Test======================================*) @@ -1330,7 +1358,7 @@ let test () = let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); - test (); + (*test ();*) let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/acf01ebf9a5626fcb22a39aa23ca2aa9… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/acf01ebf9a5626fcb22a39aa23ca2aa9… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 2 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 17 Oct '21

17 Oct '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 53c2f370 by Soilih BEN SOILIH at 2021-10-16T20:13:25-04:00 - - - - - - acf01ebf by Soilih BEN SOILIH at 2021-10-17T03:06:02-04:00 adding symbols - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -39,8 +39,10 @@ open Log open Util +type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list + type state_after_processing = (log_entry list * - ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) + (list_in_list * Debruijn.elab_context) ) (* transform a list of logs to a list of tuple @@ -139,7 +141,7 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) -let rec search_lexp_with_a_location (list_list: (vname * Lexp.lexp * Lexp.ltype) list list) (location : Source.Location.t): Lexp.lexp option = +let rec search_lexp_with_a_location (list_list: list_in_list) (location : Source.Location.t): Lexp.lexp option = let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let rec foo (tab:Lexp.lexp list) (loc:Source.Location.t) = @@ -352,9 +354,9 @@ end (*Update the context of a list_list and returns the updated context with the list all in a list *) -let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp * Lexp.ltype) list list ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list = +let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list = - let rec foo (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp * Lexp.ltype) list list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = + let rec foo (ctx: Debruijn.lexp_context) (liste : list_in_list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = match liste with | [] -> list_ret | hd::tl -> let lctx = Debruijn.lctx_extend_rec ctx hd in @@ -371,7 +373,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp (* Return a lexp if the cursor is between his start and end position *) - let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: (vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: list_in_list) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in @@ -390,7 +392,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp in foo lstr cursor (* Find the nearest lexp to the cursor *) - let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in @@ -439,13 +441,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp in foo tab cursor (* Find the lexp the cursor on or the nearest one *) - let lexp_search (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lexp_search (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = try pos_in_lexp_interval ctx lst cursor with exn -> find_the_nearest_lexp ctx lst cursor (* If lexp_search didn't find something, give the last context and a dummy lexp *) - let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in let lstr_rev = List.rev lstr in let (last_ctx,_) = List.hd lstr_rev in @@ -753,6 +755,41 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp (*====================================Lexp parcourir===================================*) +(* Verify if there is a varbind *) +let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option = + let (_,vrbd,_) = env in + match vrbd with + | Variable + | ForwardRef-> None + | LetDef (idx,lxp) -> Some (idx,lxp) + +(* Search if the is the given value in the context *) +let value_in_ctx (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : Debruijn.env_elem * int = + let (_, _, lctxm, _) = ectx in + let lctx = Myers.list lctxm in + let rec foo (lctx: Debruijn.env_elem list) (lxp: Lexp.lexp) (comp:int)= + match lctx with + | [] -> failwith "The value is not in ectx !" + | hd::tl -> match verify_varbind hd with + | None -> foo tl lxp (comp + 1) + | Some (idx,lxpv) -> if String.equal (Lexp.lexp_string lxp) (Lexp.lexp_string lxpv) then (hd, comp) + else foo tl lxp (comp + 1) + in foo lctx lxp 1 + +(* Search the key of a varbind in senv_type *) +let key_of_varbind (ectx: Debruijn.elab_context) (el: Debruijn.env_elem) (idx: int): string = + let (_, (_,snty), _, _) = ectx in + let sntyb = SMap.bindings snty in + let foo (lst: (string * int) list) (id: int) : string = + let (str,_) = List.find (fun (s,i) -> Int.equal i id) lst + in str + in foo sntyb idx + + +(*use value_in_ctx and key_of_varbind *) +let search_the_key (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : string = + let (vlr, idx) = value_in_ctx ectx lxp in + key_of_varbind ectx vlr idx (*====================================Definition===================================*) @@ -769,37 +806,71 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte (*====================================Definition===================================*) +(*=====================================Symbols=====================================*) + +let filter_the_list_list (list_list: list_in_list) : list_in_list = + List.filter ( fun x -> + let ((_,s),_,_) = List.nth x 0 in + match s with + | None -> false + | Some _ -> true + ) list_list + +let take_all_list_el (list_list: list_in_list) = + let rec foo (ll:list_in_list) ret_list = + match list_list with + | [] -> [] + | hd::tl -> let hdl = List.nth hd 0 in + foo tl (hdl::ret_list) + in foo list_list [] + +let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = + let lst = take_all_list_el list_list in + List.map ( fun x -> + let ((l,s),_,_) = x in + let range = lsp_range_of_loc l in + let nm = Option.get s in + Lsp.Types.DocumentSymbol.create + ~name:nm + ~kind:Lsp.Types.SymbolKind.Variable + ~range:range + ~selectionRange:range + () + ) lst + +(*=====================================End Symbols=================================*) + (*====================================Compl===================================*) -let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list = - - let (_,vr,_,loc) = ret in - - match vr with - | None -> [] - | Some v -> let ((_,c),_) = v in - let cp = Option.get c in - let label = cp in - let range = Compl.lsp_range_of_a_tuple - (loc.start_line,(loc.end_column - String.length cp)) - (loc.end_line, loc.end_column) - in - let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:cp in - let kind = Lsp.Types.CompletionItemKind.Text in - let detail = "detail " ^ cp in - let ci = Lsp.Types.CompletionItem.create - ~label:label ~kind:kind - ~textEdit:textEdit ~detail:detail () - in - [ci] + let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list = - let trans_listlist_by_var (ctx:Debruijn.lexp_context) (list_list:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let (_,vr,_,loc) = ret in + + match vr with + | None -> [] + | Some v -> let ((_,c),_) = v in + let cp = Option.get c in + let label = cp in + let range = Compl.lsp_range_of_a_tuple + (loc.start_line,(loc.end_column - String.length cp)) + (loc.end_line, loc.end_column) + in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:cp in + let kind = Lsp.Types.CompletionItemKind.Text in + let detail = "detail " ^ cp in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:detail () + in + [ci] + + let trans_listlist_by_var (ctx:Debruijn.lexp_context) (list_list:list_in_list) (cursor:Source.Location.t) = let lst = update_the_context ctx list_list in let nlst = List.map ( fun x -> let (lctx,liste) = x in let (_,lxp,_) = nearest_lexp_of_the_list liste cursor in browse_lexp lctx lxp cursor - ) lst in + ) lst in List.filter (fun x -> let (_,v,_,_) = x in match v with @@ -807,107 +878,107 @@ let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * str | Some v -> true ) nlst - let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = - let open Elexp in - match Lexp.lexp_lexp' e with - | Lambda (ak, (l,_), t, e) -> Lsp.Types.CompletionItemKind.Function - | Cons (t, (_l, name)) -> Lsp.Types.CompletionItemKind.Constructor - | _ -> Lsp.Types.CompletionItemKind.Variable - - - let kind_of_a_varbind (element : Debruijn.env_elem ) : Lsp.Types.CompletionItemKind.t = - let (_,vrb,_) = element in - match vrb with - | Variable - | ForwardRef -> Lsp.Types.CompletionItemKind.Variable - | LetDef (_,lxp) -> kind_of_a_lexp lxp - - (* Filter the list by the vname with the string option *) - let rec filter_lctx (lctx: Debruijn.env_elem Myers.myers) (ret: Debruijn.env_elem list) : Debruijn.env_elem list = - match lctx with - | Mnil -> ret - | Mcons (hd,tl,_,_) -> let ((_,s),_,_) = hd in - match s with - - | None -> filter_lctx tl ret - | Some _ -> filter_lctx tl (hd::ret) - - - (* Transform a context to a list of completion item *) - let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = - List.map ( fun (x: Debruijn.env_elem) -> - let ((_,s),_,t) = x in - let str = Option.get s in - let label = str in - let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in - let kind = kind_of_a_varbind x in - let ci = Lsp.Types.CompletionItem.create - ~label:label ~kind:kind - ~textEdit:textEdit ~detail:(Lexp.lexp_string t) () - in - ci - - ) lctx - - (* Verify if a string contains some other *) - let string_contain (substr:string) (str:string) : bool = - let r = ref 0 in - for i=0 to ((String.length substr) - 1) do - if ( - String.contains str (Char.lowercase_ascii substr.[i]) - || String.contains str (Char.uppercase_ascii substr.[i]) - ) - then r := !r + 1 - else r := !r + 0 - done; - Int.equal !r (String.length substr) - - let str_to_char_list (str: string) : char list = - let char_list = ref [] in - for i=0 to ((String.length str) - 1) do - char_list := (str.[i])::(!char_list) - done; - List.rev !char_list + let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = + let open Elexp in + match Lexp.lexp_lexp' e with + | Lambda (ak, (l,_), t, e) -> Lsp.Types.CompletionItemKind.Function + | Cons (t, (_l, name)) -> Lsp.Types.CompletionItemKind.Constructor + | _ -> Lsp.Types.CompletionItemKind.Variable - let char_list_to_str (char_list: char list) : string = - match char_list with - | [] -> "" - | _ -> List.fold_left (fun x y -> x ^ (String.make 1 y)) "" char_list - let char_index (str:string) (chr:char) : int = - try String.index str chr - with e -> String.index str (Char.uppercase_ascii chr) - let rec str_order (substr:string) (str:string) : bool = - match str_to_char_list substr with - | [] -> false - | [hd] -> string_contain (String.make 1 hd) str - | [hd;tl] -> let ihd = char_index str hd in - let itl = char_index str tl in - if (ihd < itl) then true + let kind_of_a_varbind (element : Debruijn.env_elem ) : Lsp.Types.CompletionItemKind.t = + let (_,vrb,_) = element in + match vrb with + | Variable + | ForwardRef -> Lsp.Types.CompletionItemKind.Variable + | LetDef (_,lxp) -> kind_of_a_lexp lxp + + (* Filter the list by the vname with the string option *) + let rec filter_lctx (lctx: Debruijn.env_elem Myers.myers) (ret: Debruijn.env_elem list) : Debruijn.env_elem list = + match lctx with + | Mnil -> ret + | Mcons (hd,tl,_,_) -> let ((_,s),_,_) = hd in + match s with + + | None -> filter_lctx tl ret + | Some _ -> filter_lctx tl (hd::ret) + + + (* Transform a context to a list of completion item *) + let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = + List.map ( fun (x: Debruijn.env_elem) -> + let ((_,s),_,t) = x in + let str = Option.get s in + let label = str in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in + let kind = kind_of_a_varbind x in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:(Lexp.lexp_string t) () + in + ci + + ) lctx + + (* Verify if a string contains some other *) + let string_contain (substr:string) (str:string) : bool = + let r = ref 0 in + for i=0 to ((String.length substr) - 1) do + if ( + String.contains str (Char.lowercase_ascii substr.[i]) + || String.contains str (Char.uppercase_ascii substr.[i]) + ) + then r := !r + 1 + else r := !r + 0 + done; + Int.equal !r (String.length substr) + + let str_to_char_list (str: string) : char list = + let char_list = ref [] in + for i=0 to ((String.length str) - 1) do + char_list := (str.[i])::(!char_list) + done; + List.rev !char_list + + let char_list_to_str (char_list: char list) : string = + match char_list with + | [] -> "" + | _ -> List.fold_left (fun x y -> x ^ (String.make 1 y)) "" char_list + + let char_index (str:string) (chr:char) : int = + try String.index str chr + with e -> String.index str (Char.uppercase_ascii chr) + let rec str_order (substr:string) (str:string) : bool = + match str_to_char_list substr with + | [] -> false + | [hd] -> string_contain (String.make 1 hd) str + | [hd;tl] -> let ihd = char_index str hd in + let itl = char_index str tl in + if (ihd < itl) then true + else false + | hd::ml::tl -> let ihd = char_index str hd in + let iml = char_index str ml in + if ( ihd < iml ) then + str_order (char_list_to_str (ml::tl)) str else false - | hd::ml::tl -> let ihd = char_index str hd in - let iml = char_index str ml in - if ( ihd < iml ) then - str_order (char_list_to_str (ml::tl)) str - else false - - (* Filter completions list by a string *) - let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = - match liste with - | [] -> liste - | _ -> let lst = List.filter (fun (x:Lsp.Types.CompletionItem.t) -> - string_contain str x.label - ) liste - in - List.filter (fun (x:Lsp.Types.CompletionItem.t) -> - str_order str x.label - ) lst - (* List of separators that delimit a word *) - let sep_list = [';';',';'(';')';'.';' ';'{';'}'] - - let split_string_line (content:string) (line:int) = - let str_list = String.split_on_char '\n' content in - List.nth str_list (line - 1) + + (* Filter completions list by a string *) + let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = + match liste with + | [] -> liste + | _ -> let lst = List.filter (fun (x:Lsp.Types.CompletionItem.t) -> + string_contain str x.label + ) liste + in + List.filter (fun (x:Lsp.Types.CompletionItem.t) -> + str_order str x.label + ) lst + (* List of separators that delimit a word *) + let sep_list = [';';',';'(';')';'.';' ';'{';'}'] + + let split_string_line (content:string) (line:int) = + let str_list = String.split_on_char '\n' content in + List.nth str_list (line - 1) (* Find the word in which the cursor is *) let rec search_word_in_cursor (str:string) (char_list:char list) (pos:int) (ret:string) : string = @@ -1006,7 +1077,7 @@ class lsp_server = match Hashtbl.find buffers uri with | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in + let (list_list, ectx) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,vx) = lexp_search ctx list_list typer_loc in @@ -1015,7 +1086,10 @@ class lsp_server = let ret' = (l_ctx_r,None,ltyp,lvn) in let (l_ctx,_,l_type,location) = browse_list_lexp [ret;ret'] typer_loc in let range = lsp_range_of_loc location in - let s = Lexp.lexp_string_for_lsp l_type in + let s = try search_the_key ectx l_type + with exe -> Lexp.lexp_string_for_lsp l_type + in + (*let s = Lexp.lexp_string_for_lsp l_type in*) let r = Lsp.Types.Hover.create ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) ~range:range () @@ -1053,34 +1127,42 @@ class lsp_server = method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in - let typer_loc = typer_pos_of_lsp_pos pos in - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let (_,lexp,_) = vx in - let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in - - (* - let trans_string = Compl.tranform_string doc_state.content in - let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in - let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in - *) - - let my_str = split_string_line doc_state.content (pos.line + 1) in - let word = use_search_word my_str sep_list pos.character "" in - - let range = Compl.lsp_range_of_a_tuple - (typer_loc.start_line,(typer_loc.end_column - String.length word)) - (typer_loc.end_line, typer_loc.end_column) - in - - let filtred_list = filter_lctx l_ctx [] in - let comp_list = ctx_to_ci_list filtred_list range in - let comp_list_ret = complete_oth word comp_list in - - let e = Some (`List comp_list_ret) in - let f = Linol_lwt.return e in f + | state_after_processing -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = typer_pos_of_lsp_pos pos in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in + + (* + let trans_string = Compl.tranform_string doc_state.content in + let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in + let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in + *) + + let my_str = split_string_line doc_state.content (pos.line + 1) in + let word = use_search_word my_str sep_list pos.character "" in + + let range = Compl.lsp_range_of_a_tuple + (typer_loc.start_line,(typer_loc.end_column - String.length word)) + (typer_loc.end_line, typer_loc.end_column) + in + + let filtred_list = filter_lctx l_ctx [] in + let comp_list = ctx_to_ci_list filtred_list range in + let comp_list_ret = complete_oth word comp_list in + + let e = Some (`List comp_list_ret) in + let f = Linol_lwt.return e in f + + method! on_req_symbol ~notify_back ~id ~uri () = + let doc_ = self#find_doc uri in + let doc_state = Option.get doc_ in + let (_,(list_list, _)) = readstring doc_state.content in + let r = create_symbols list_list in + let e = Some (`DocumentSymbol r) in + let f = Linol_lwt.return e in f end View it on GitLab: https://gitlab.com/monnier/typer/-/compare/09aacbad9a1e1f80a174bd165b6f1188… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/09aacbad9a1e1f80a174bd165b6f1188… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 2 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 15 Oct '21

15 Oct '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 645d3261 by Soilih BEN SOILIH at 2021-10-14T00:39:33-06:00 - - - - - - 09aacbad by Soilih BEN SOILIH at 2021-10-14T22:37:00-06:00 fix the completion problem at the end of the file - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -377,7 +377,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype)) = match ls with - | [] -> failwith "No Lexp found!" + | [] -> failwith "No Lexp Found!" | hd::tl -> let (lctx_hd, hdl) = hd in let v = nearest_lexp_of_the_list hdl cursor in let (_,lxp,_) = v in @@ -443,6 +443,15 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp try pos_in_lexp_interval ctx lst cursor with exn -> find_the_nearest_lexp ctx lst cursor + (* If lexp_search didn't find something, give the last context + and a dummy lexp *) + let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lstr = update_the_context ctx lst in + let lstr_rev = List.rev lstr in + let (last_ctx,_) = List.hd lstr_rev in + try lexp_search ctx lst cursor + with exn -> (last_ctx,((Source.Location.dummy,None),Lexp.impossible, Lexp.impossible)) + (* search the type of a lexp browsing a lexp *) let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t = @@ -610,14 +619,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | Case (l, e, ret, branches, default) -> - let candidats = ref [] in - + let call_split (e: Lexp.lexp) = - match Lexp.lexp_lexp' e with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in - candidats := (browse_lexp ctx e cursor):: !candidats; + match Lexp.lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + candidats := (browse_lexp ctx e cursor):: !candidats; let etype = Opslexp.get_type ctx e in (* FIXME save the type in the case lexp instead of recomputing it over and over again *) @@ -626,7 +634,8 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | Sort (_, Stype l) -> l | _ -> Debruijn.level0 in let erased = Debruijn.set_empty in - let it, aargs = call_split etype in + + let it, aargs = call_split etype in ( match Opslexp.lexp'_whnf it ctx, aargs with @@ -653,35 +662,35 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in (erased, nctx) in - let brch = SMap.bindings branches in - let lst = - List.map - ( - fun (name, (l, vdefs, branch)) - -> let fieldtypes = SMap.find name constructors in - let rec mkctx erased ctx s hlxp vdefs fieldtypes = - match vdefs, fieldtypes with - | [], [] -> (erased, ctx, hlxp) - (* FIXME: If ak is Aerasable, make sure the var only - * appears in type annotations. *) - | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes - -> mkctx (Opslexp.dbset_push ak erased) - (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) - (Lexp.ssink vdef s) - (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) - vdefs fieldtypes - | _,_ -> (erased, ctx, hlxp) in - let hctor = - Lexp.mkCall (Lexp.mkCons (it, (l, name)), - List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in - let (nerased, nctx, hlxp) = - mkctx erased ctx s hctor vdefs fieldtypes in - let subst = Subst.shift (List.length vdefs) in - let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx branch cursor) :: !candidats; - ) - brch - in + let brch = SMap.bindings branches in + let lst = + List.map + ( + fun (name, (l, vdefs, branch)) + -> let fieldtypes = SMap.find name constructors in + let rec mkctx erased ctx s hlxp vdefs fieldtypes = + match vdefs, fieldtypes with + | [], [] -> (erased, ctx, hlxp) + (* FIXME: If ak is Aerasable, make sure the var only + * appears in type annotations. *) + | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes + -> mkctx (Opslexp.dbset_push ak erased) + (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) + (Lexp.ssink vdef s) + (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) + vdefs fieldtypes + | _,_ -> (erased, ctx, hlxp) in + let hctor = + Lexp.mkCall (Lexp.mkCons (it, (l, name)), + List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in + let (nerased, nctx, hlxp) = + mkctx erased ctx s hctor vdefs fieldtypes in + let subst = Subst.shift (List.length vdefs) in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in + candidats := (browse_lexp nctx branch cursor) :: !candidats; + ) + brch + in let diff = SMap.cardinal constructors - List.length lst in ( @@ -693,9 +702,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp let hlxp = Lexp.mkVar ((l, None), 0) in let (_, nctx) = ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx d cursor) :: !candidats; - () | None -> if diff > 0 then (); () @@ -1050,7 +1057,7 @@ class lsp_server = let (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search ctx list_list typer_loc in + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in let (_,lexp,_) = vx in let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/1403fe8b664aa8b5684785b0d0e9093f… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/1403fe8b664aa8b5684785b0d0e9093f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] fix warnings
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Oct '21

13 Oct '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 1403fe8b by Soilih BEN SOILIH at 2021-10-13T17:33:39-06:00 fix warnings - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -689,19 +689,18 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | Some (v, d) -> if diff <= 0 then (); let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in - let nerased = Debruijn.set_sink 1 erased in let subst = Subst.shift 1 in let hlxp = Lexp.mkVar ((l, None), 0) in - let (nerased, nctx) = + let (_, nctx) = ctx_extend_with_eq nctx subst hlxp in candidats := (browse_lexp nctx d cursor) :: !candidats; - browse_lexp nctx d cursor + () | None - -> if diff > 0 then (); (ctx, None, Lexp.impossible, Source.Location.dummy) + -> if diff > 0 then (); () ) - | _,_ -> (ctx, None, Lexp.impossible, Source.Location.dummy) ; + | _,_ -> () ; ); browse_list_lexp !candidats cursor | Cons (t, (_l, name)) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1403fe8b664aa8b5684785b0d0e9093f1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1403fe8b664aa8b5684785b0d0e9093f1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] fix the case Case
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Oct '21

13 Oct '21

Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer Commits: 83744967 by Soilih BEN SOILIH at 2021-10-04T14:47:34-06:00 fix the case Case - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -610,99 +610,100 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | Case (l, e, ret, branches, default) -> - ( + let candidats = ref [] in + let call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - candidats := (browse_lexp ctx e cursor):: !candidats; - let etype = Opslexp.get_type ctx e in - (* FIXME save the type in the case lexp instead of recomputing - it over and over again *) - let ekind = Opslexp.get_type ctx etype in - let elvl = match Opslexp.lexp'_whnf ekind ctx with - | Sort (_, Stype l) -> l - | _ -> Debruijn.level0 in - let erased = Debruijn.set_empty in - let it, aargs = call_split etype in - + candidats := (browse_lexp ctx e cursor):: !candidats; + let etype = Opslexp.get_type ctx e in + (* FIXME save the type in the case lexp instead of recomputing + it over and over again *) + let ekind = Opslexp.get_type ctx etype in + let elvl = match Opslexp.lexp'_whnf ekind ctx with + | Sort (_, Stype l) -> l + | _ -> Debruijn.level0 in + let erased = Debruijn.set_empty in + let it, aargs = call_split etype in + ( match Opslexp.lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs -> - let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - (* We don't check aarg's type, because we assume that `check` - * returns a valid type. *) - -> mksubst (Subst.cons aarg s) fargs aargs - | _,_ -> s in - let s = mksubst Subst.identity fargs aargs in - let ctx_extend_with_eq ctx subst hlxp = - let tlxp = Lexp.mkSusp e subst in - let tltp = Lexp.mkSusp etype subst in - let tlvl = Lexp.mkSusp elvl subst in - let eqty = Lexp.mkCall (Debruijn.type_eq, - [(Lexp.Aerasable, tlvl); (* Typelevel *) - (Lexp.Aerasable, tltp); (* Inductive type *) - (Lexp.Anormal, hlxp); (* Lexp of the branch head *) - (Lexp.Anormal, tlxp)]) in (* Target lexp *) - (* The eq proof is erasable. *) - let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in - (erased, nctx) in - - let brch = SMap.bindings branches in - let lst = - List.map - ( - fun (name, (l, vdefs, branch)) - -> let fieldtypes = SMap.find name constructors in - let rec mkctx erased ctx s hlxp vdefs fieldtypes = - match vdefs, fieldtypes with - | [], [] -> (erased, ctx, hlxp) - (* FIXME: If ak is Aerasable, make sure the var only - * appears in type annotations. *) - | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes - -> mkctx (Opslexp.dbset_push ak erased) - (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) - (Lexp.ssink vdef s) - (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) - vdefs fieldtypes - | _,_ -> (erased, ctx, hlxp) in - let hctor = - Lexp.mkCall (Lexp.mkCons (it, (l, name)), - List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in - let (nerased, nctx, hlxp) = - mkctx erased ctx s hctor vdefs fieldtypes in - let subst = Subst.shift (List.length vdefs) in - let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx branch cursor) :: !candidats; - ) - brch - in - - let diff = SMap.cardinal constructors - List.length lst in - ( - match default with - | Some (v, d) - -> if diff <= 0 then (); - let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in - let nerased = Debruijn.set_sink 1 erased in - let subst = Subst.shift 1 in - let hlxp = Lexp.mkVar ((l, None), 0) in - let (nerased, nctx) = - ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx d cursor) :: !candidats; - browse_lexp nctx d cursor - | None - -> if diff > 0 then (); (ctx, None, Lexp.impossible, Source.Location.dummy) - ) + + | Inductive (_, _, fargs, constructors), aargs -> + let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + (* We don't check aarg's type, because we assume that `check` + * returns a valid type. *) + -> mksubst (Subst.cons aarg s) fargs aargs + | _,_ -> s in + let s = mksubst Subst.identity fargs aargs in + let ctx_extend_with_eq ctx subst hlxp = + let tlxp = Lexp.mkSusp e subst in + let tltp = Lexp.mkSusp etype subst in + let tlvl = Lexp.mkSusp elvl subst in + let eqty = Lexp.mkCall (Debruijn.type_eq, + [(Lexp.Aerasable, tlvl); (* Typelevel *) + (Lexp.Aerasable, tltp); (* Inductive type *) + (Lexp.Anormal, hlxp); (* Lexp of the branch head *) + (Lexp.Anormal, tlxp)]) in (* Target lexp *) + (* The eq proof is erasable. *) + let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in + (erased, nctx) in + + let brch = SMap.bindings branches in + let lst = + List.map + ( + fun (name, (l, vdefs, branch)) + -> let fieldtypes = SMap.find name constructors in + let rec mkctx erased ctx s hlxp vdefs fieldtypes = + match vdefs, fieldtypes with + | [], [] -> (erased, ctx, hlxp) + (* FIXME: If ak is Aerasable, make sure the var only + * appears in type annotations. *) + | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes + -> mkctx (Opslexp.dbset_push ak erased) + (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) + (Lexp.ssink vdef s) + (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) + vdefs fieldtypes + | _,_ -> (erased, ctx, hlxp) in + let hctor = + Lexp.mkCall (Lexp.mkCons (it, (l, name)), + List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in + let (nerased, nctx, hlxp) = + mkctx erased ctx s hctor vdefs fieldtypes in + let subst = Subst.shift (List.length vdefs) in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in + candidats := (browse_lexp nctx branch cursor) :: !candidats; + ) + brch + in + + let diff = SMap.cardinal constructors - List.length lst in + ( + match default with + | Some (v, d) + -> if diff <= 0 then (); + let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in + let nerased = Debruijn.set_sink 1 erased in + let subst = Subst.shift 1 in + let hlxp = Lexp.mkVar ((l, None), 0) in + let (nerased, nctx) = + ctx_extend_with_eq nctx subst hlxp in + + candidats := (browse_lexp nctx d cursor) :: !candidats; + + browse_lexp nctx d cursor + | None + -> if diff > 0 then (); (ctx, None, Lexp.impossible, Source.Location.dummy) + ) | _,_ -> (ctx, None, Lexp.impossible, Source.Location.dummy) ; - + ); browse_list_lexp !candidats cursor - ) - - | Cons (t, (_l, name)) -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) @@ -1089,9 +1090,13 @@ let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (posit let (list_list, _) = ast in let (l,c) = position in let pos = pos_of_tuple position in + let (lctx,vx) = lexp_search ctx list_list pos in - let (_,lexp,_) = vx in - let (_,_, l_type,_) = browse_lexp lctx lexp pos in + let ((lvn,_),lexp,ltyp) = vx in + let (l_ctx_r,_,_,_) as ret = browse_lexp lctx lexp pos in + let ret' = (l_ctx_r,None,ltyp,lvn) in + let (_,_,l_type,_) = browse_list_lexp [ret;ret'] pos in + let excpect = "excpected : " ^ expected ^ "\n" in let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n\n" in let input = "input : " ^ content ^ "\n" in @@ -1123,10 +1128,16 @@ let test () = hoverTest ctx name "f = 12.3 ;" (1,6) "##Float"; sep name "LAMBDA"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; - hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "(x : ##Int) -> Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "##Int"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "##Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,23) ""; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21) "##Int"; + hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,20) "##Int"; + hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,24) "##Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,24) "##Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,26) "##Int"; + sep name "FUNCTION(LAMBDA)"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "##Int"; @@ -1144,7 +1155,7 @@ let test () = hoverTest ctx name "multiply x y z = x + y + z ;" (1,22) "##Int"; hoverTest ctx name "multiply x y z = x + y + z ;" (1,26) "##Int"; sep name "CALL"; - hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,1) "##Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,13) "##Int"; hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,15) "##Int"; @@ -1158,10 +1169,16 @@ let test () = hoverTest ctx name "foo = ##String ; \n\n\nv = foo ;" (4,1) "(##Type_ (##TypeLevel.succ ##TypeLevel.z))"; hoverTest ctx name "foo = ##Type ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; sep name "LIST"; - hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "##Type"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "(List ##TypeLevel.z ##Int)"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12) "##Int"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; + sep name "TUPLE"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ; \n\n\ntup = (1,2,\"str\",lst) ;" (4,1) "typecons (Tuple) (cons ##Int ##Int ##String (List ##TypeLevel.z ##Int))"; + hoverTest ctx name "tup = (1,2,\"str\",false) ;" (1,8) "##Int"; + hoverTest ctx name "tup = (1,2,\"str\",false) ;" (1,10) "##Int"; + hoverTest ctx name "tup = (1,2,\"str\",false) ;" (1,15) "##String"; + hoverTest ctx name "tup = (1,2,\"str\",false) ;" (1,21) "Bool"; sep name "ARROW"; hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; @@ -1204,13 +1221,13 @@ let test () = hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,37) ""; hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,41) ""; sep name "CASE"; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,1) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,5) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (1,14) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (3,13) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => \"h\"\n\n| false => \"jj\" ;" (5,14) "" + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (1,1) ""; + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (1,5) ""; + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (1,14) ""; + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (3,4) ""; + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (3,13) ""; + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,4) ""; + hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,14) "" View it on GitLab: https://gitlab.com/monnier/typer/-/commit/83744967e73a96a0aee0dcc284108fd14… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/83744967e73a96a0aee0dcc284108fd14… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch source-spans
by Simon Génier (＠ilovemonoids) 06 Oct '21

06 Oct '21

Simon Génier deleted branch source-spans at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch offsets-to-points
by Simon Génier (＠ilovemonoids) 06 Oct '21

06 Oct '21

Simon Génier deleted branch offsets-to-points at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Octobre 2021