Mai 2022 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][location-sinfo] Suppression du module Int
by Ismaila FALL (＠Fallismaila) 31 Mai '22

31 Mai '22

Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: 5b74723c by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-31T22:18:07+00:00 Suppression du module Int - - - - - 5 changed files: - − Int - src/debug.ml - src/elab.ml - src/eval.ml - src/pexp.ml Changes: ===================================== Int deleted ===================================== @@ -1,28 +0,0 @@ -btl/builtins.typer:Integer->Int = Built-in "Integer->Int" : Integer -> Int; -btl/builtins.typer:Integer->String = Built-in "Integer->String" : Integer -> String; -btl/pervasive.typer: | nil => (Integer->Int 0) -btl/pervasive.typer: (Int_+ (Integer->Int 1) (List_length tl)); -btl/pervasive.typer: => case Int_<= n (Integer->Int 0) -btl/pervasive.typer: | false => List_nth (Int_- n (Integer->Int 1)) xs d; -btl/pervasive.typer: | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); -btl/pervasive.typer:in helper f (Integer->Int 0) xs; -btl/pervasive.typer:List_empty xs = Int_eq (List_length xs) (Integer->Int 0); -btl/pervasive.typer: (cons (List_nth (Integer->Int 1) ss Sexp_error) nil))); -btl/pervasive.typer: head = List_nth (Integer->Int 0) head-pair Sexp_error; -btl/pervasive.typer: type-type = List_nth (Integer->Int 1) head-pair Sexp_error; -btl/pervasive.typer: | vnil (p ::: Eq n (Integer->Int 0)) -btl/pervasive.typer: | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1))); -btl/pervasive.typer: let e1 = List_nth (Integer->Int 0) args Sexp_error; -btl/pervasive.typer: e2 = List_nth (Integer->Int 1) args Sexp_error; -btl/pervasive.typer: e3 = List_nth (Integer->Int 2) args Sexp_error; -btl/pervasive.typer:in case (Int_eq r (Integer->Int -1)) -btl/poly-lits.typer:IntFromInteger = mkFromInteger Integer->Int; -btl/tuple.typer: elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); -samples/nats.typer:Integer->Nat : Integer -> Nat; -samples/nats.typer:Integer->Nat i = -samples/nats.typer: S (Integer->Nat (Integer_- i 1)) -samples/nats.typer:NatFromInteger = mkFromInteger Integer->Nat; -src/eval.ml: let name = "Integer->Int" in -src/eval.ml: | _ -> error loc "Integer->String expects one Integer argument" -src/eval.ml: ("Integer->String", integer_to_string, 1); -tests/eval_test.ml:intFromIntegerCoercion = mkCoercible (Integer->Int); ===================================== src/debug.ml ===================================== @@ -121,7 +121,8 @@ let debug_lexp_decls decls = List.iter (fun e -> let ((loc, _name), lxp, _ltp) = e in - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc)); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string + (sexp_location loc)); let str = lexp_str_decls (!debug_ppctx) [e] in ===================================== src/elab.ml ===================================== @@ -1114,7 +1114,7 @@ and lexp_parse_inductive ctors ctx = acc impossible in let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t _l e - -> mkArrow (lexp_sinfo altacc, Aerasable, vname, t, e)) + -> mkArrow (lexp_sinfo e, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1334,7 +1334,8 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (Symbol(loc, ""), Some vname) in + -> let ltp = infer_and_generalize_type nctx stp (stp, + Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1355,7 +1356,7 @@ and lexp_decls_1 pending_defs then (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (Symbol(loc, ""), Some vname) ForwardRef ltp) + else recur [] (ectx_extend nctx (stp, Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ @@ -1367,13 +1368,13 @@ and lexp_decls_1 | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((_l, vname)); sexp] + | [Symbol ((l, vname)); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (sexp, Some vname) in + let var = (epsilon (l), Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, ===================================== src/eval.ml ===================================== @@ -717,7 +717,7 @@ and print_eval_trace trace = print_trace " EVAL TRACE " trace a let io_bind loc depth args_val = - let trace_dum = (Var ((Symbol(loc, ""), None), -1)) in + let trace_dum = (Var ((epsilon loc, None), -1)) in match args_val with | [Vcommand cmd; callback] ===================================== src/pexp.ml ===================================== @@ -20,9 +20,6 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) -(* -*open Util -*) open Sexp (* Symbol *) let pexp_error loc = Log.log_error ~section:"PEXP" ~loc View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5b74723c05d49bbca4f84c67b6eaf384a… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5b74723c05d49bbca4f84c67b6eaf384a… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][location-sinfo] Suppression du dossier idea
by Ismaila FALL (＠Fallismaila) 31 Mai '22

31 Mai '22

Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: b638446c by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-31T22:03:08+00:00 Suppression du dossier idea - - - - - 4 changed files: - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== @@ -176,7 +176,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var = let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in - let loc = sinfo_location lxp in + let loc = lexp_sinfo lxp in let ltype' = try OL.check lctx lxp with e -> match e with @@ -652,7 +652,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = | (e, Inferred t) -> (e, t) and elab_special_form ctx f args ot = - let loc = sinfo_location f in + let loc = lexp_sinfo f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) @@ -663,7 +663,7 @@ and elab_special_form ctx f args ot = sform_dummy_ret ctx loc and elab_special_decl_form ctx f args = - let loc = sinfo_location f in + let loc = lexp_sinfo f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) @@ -675,9 +675,9 @@ and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow (_, ((Aerasable | Aimplicit) as ak), (_, v), t1, t2) - -> let arg = newInstanceMetavar ctx (sinfo_location e, v) t1 in + -> let arg = newInstanceMetavar ctx (lexp_sinfo e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (sinfo_location e, e, List.rev args), t) + | _ -> (mkCall (lexp_sinfo e, e, List.rev args), t) in instantiate t [] and resolve_instances e = @@ -718,7 +718,7 @@ and infer_type pexp ectx (var: vname) = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) - let l = sinfo_location s in + let l = lexp_sinfo s in match Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) @@ -1006,7 +1006,7 @@ and elab_macro_call (ot : ltype option) : lexp * sform_type = - let location = sinfo_location func in + let location = lexp_sinfo func in let t = match ot with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location @@ -1029,7 +1029,7 @@ and elab_macro_call (* Identify Call Type and return processed call. *) and elab_call ctx (func, ltp) (sargs: sexp list) = - let loc = sinfo_location func in + let loc = lexp_sinfo func in let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in @@ -1114,7 +1114,7 @@ and lexp_parse_inductive ctors ctx = acc impossible in let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t _l e - -> mkArrow (sinfo_location altacc, Aerasable, vname, t, e)) + -> mkArrow (lexp_sinfo altacc, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) ===================================== src/lexp.ml ===================================== @@ -516,30 +516,30 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) * S.sink (fun l i -> mkVar (l, i)) l s *) -let rec sinfo_location s = +let rec lexp_sinfo s = match lexp_lexp' s with | Sort (l,_) -> l - | SortLevel (SLsucc s) -> sinfo_location s - | SortLevel (SLlub (s, _)) -> sinfo_location s + | SortLevel (SLsucc s) -> lexp_sinfo s + | SortLevel (SLlub (s, _)) -> lexp_sinfo s | SortLevel SLz -> dummy_sinfo | Imm s -> s | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> Symbol (l, "") + | Builtin ((l, _), _) -> epsilon l | Let (l,_,_) -> l | Arrow (l,_,_,_,_) -> l | Lambda (_,(l,_),_,_) -> l - | Call (_,f,_) -> sinfo_location f + | Call (_,f,_) -> lexp_sinfo f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> Symbol (l, "") + | Cons (_,(l,_)) -> epsilon l | Case (l,_,_,_,_) -> l - | Susp (s, _) -> sinfo_location s + | Susp (s, _) -> lexp_sinfo s (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l | Proj (l,_,_) -> l let lexp_location e = - sexp_location (sinfo_location e) + sexp_location (lexp_sinfo e) (********* Normalizing a term *********) ===================================== src/opslexp.ml ===================================== @@ -781,7 +781,7 @@ and check'' erased ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in - mkArrow (sinfo_location t, ak, v, t, + mkArrow (lexp_sinfo t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -937,7 +937,7 @@ and check'' erased ctx e = mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (sinfo_location ftype, ak, vd, ftype, + -> mkArrow (lexp_sinfo ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with @@ -1207,7 +1207,7 @@ and get_type ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (sinfo_location t, ak, v, t, + -> mkArrow (lexp_sinfo t, ak, v, t, arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct @@ -1228,7 +1228,7 @@ and get_type ctx e = mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (sinfo_location ftype, ak, vd, ftype, + -> mkArrow (lexp_sinfo ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with ===================================== src/unification.ml ===================================== @@ -146,7 +146,7 @@ let common_subset ctx s1 s2 = && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((sinfo_location le1, None), 0), + | s' -> S.Cons (mkVar ((lexp_sinfo le1, None), 0), s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b638446cf2ce663e056c4c053c6334b8b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b638446cf2ce663e056c4c053c6334b8b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] 3 commits: [OK] Compilateur
by Ismaila FALL (＠Fallismaila) 31 Mai '22

31 Mai '22

Ismaila FALL pushed to branch main at Stefan / Typer Commits: c422f432 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-26T18:51:50+00:00 [OK] Compilateur - - - - - cbd1e53a by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-31T20:45:09+00:00 Ajout du type sinfo - - - - - 471c1ff6 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-31T20:52:07+00:00 Ajout du type sinfo pour Sexp-info - - - - - 21 changed files: - + .idea/workspace.xml - debug_util.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/instargs.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/instargs_test.ml - tests/positivity_test.ml - tests/unify_test.ml Changes: ===================================== .idea/workspace.xml ===================================== @@ -0,0 +1,41 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project version="4"> + <component name="ChangeListManager"> + <list default="true" id="41ac7a90-abda-4ce7-87d2-87842cc79039" name="Changes" comment="" /> + <option name="SHOW_DIALOG" value="false" /> + <option name="HIGHLIGHT_CONFLICTS" value="true" /> + <option name="HIGHLIGHT_NON_ACTIVE_CHANGELIST" value="false" /> + <option name="LAST_RESOLUTION" value="IGNORE" /> + </component> + <component name="Git.Settings"> + <option name="RECENT_GIT_ROOT_PATH" value="$PROJECT_DIR$" /> + </component> + <component name="MarkdownSettingsMigration"> + <option name="stateVersion" value="1" /> + </component> + <component name="ProjectId" id="29qQStX1boOkZ1Gb6bTR6iBqd5o" /> + <component name="ProjectLevelVcsManager" settingsEditedManually="true"> + <ConfirmationsSetting value="2" id="Add" /> + </component> + <component name="ProjectViewState"> + <option name="hideEmptyMiddlePackages" value="true" /> + <option name="showLibraryContents" value="true" /> + </component> + <component name="PropertiesComponent">{ + "keyToString": { + "RunOnceActivity.OpenProjectViewOnStart": "true", + "RunOnceActivity.ShowReadmeOnStart": "true" + } +}</component> + <component name="SpellCheckerSettings" RuntimeDictionaries="0" Folders="0" CustomDictionaries="0" DefaultDictionary="application-level" UseSingleDictionary="true" transferred="true" /> + <component name="TaskManager"> + <task active="true" id="Default" summary="Default task"> + <changelist id="41ac7a90-abda-4ce7-87d2-87842cc79039" name="Changes" comment="" /> + <created>1653838146676</created> + <option name="number" value="Default" /> + <option name="presentableId" value="Default" /> + <updated>1653838146676</updated> + </task> + <servers /> + </component> +</project> \ No newline at end of file ===================================== debug_util.ml ===================================== @@ -59,6 +59,7 @@ open Debruijn open Env let dloc = dummy_location +let dsinfo = DB.dsinfo let dummy_decl = Imm(String(dloc, "Dummy")) let discard _v = () @@ -306,7 +307,7 @@ let main () = let main = (senv_lookup "main" nctx) in (* get main body *) - let body = (get_rte_variable (dloc, Some "main") main rctx) in + let body = (get_rte_variable (dsinfo, Some "main") main rctx) in (* eval main *) print_eval_result 1 body ===================================== src/builtin.ml ===================================== @@ -98,9 +98,10 @@ let set_predef name lexp (* Builtin types *) let dloc = DB.dloc +let dsinfo = DB.dsinfo -let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, - mkArrow (Anormal, (dloc, None), t, dloc, t)) +let op_binary t = mkArrow (dsinfo, Anormal, (dsinfo, None), t, + mkArrow (dsinfo, Anormal, (dsinfo, None), t, t)) let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx @@ -159,7 +160,7 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl let type_arrow_0 = - mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + mkArrow (dsinfo, Anormal, (dsinfo, None), DB.type0, DB.type0) let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in ===================================== src/debruijn.ml ===================================== @@ -36,6 +36,7 @@ module Str = Str open Util +open Sexp open Lexp @@ -117,45 +118,47 @@ let set_ascending_seq ((o, m) : set) : int Seq.t = * ---------------------------------- *) let dloc = dummy_location -let type_level_sort = mkSort (dloc, StypeLevel) -let sort_omega = mkSort (dloc, StypeOmega) +let dsinfo = dummy_sinfo + +let type_level_sort = mkSort (dsinfo, StypeLevel) +let sort_omega = mkSort (dsinfo, StypeOmega) let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) -let type0 = mkSort (dloc, Stype level0) -let type1 = mkSort (dloc, Stype level1) -let type2 = mkSort (dloc, Stype level2) +let type0 = mkSort (dsinfo, Stype level0) +let type1 = mkSort (dsinfo, Stype level1) +let type2 = mkSort (dsinfo, Stype level2) let type_int = mkBuiltin ((dloc, "Int"), type0) let type_integer = mkBuiltin ((dloc, "Integer"), type0) let type_float = mkBuiltin ((dloc, "Float"), type0) let type_string = mkBuiltin ((dloc, "String"), type0) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1), + mkSort (dsinfo, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - let xv = (dloc, Some "x") in + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + let xv = (dsinfo, Some "x") in mkBuiltin ((dloc, "Eq.refl"), - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, - mkVar (tv, 0), dloc, - mkCall (type_eq, + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Aerasable, xv, + mkVar (tv, 0), + mkCall (dsinfo, type_eq, [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); @@ -465,7 +468,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name @@ -475,7 +478,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = with | Not_found -> fatal - ~loc "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + ~loc:(sexp_location 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 ===================================== @@ -121,7 +121,8 @@ let debug_lexp_decls decls = List.iter (fun e -> let ((loc, _name), lxp, _ltp) = e in - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string + (sexp_location loc)); let str = lexp_str_decls (!debug_ppctx) [e] in @@ -137,7 +138,7 @@ let debug_lexp_decls decls = let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" loc.file scd; + -> printf " FILE: %-25s : %s\n" (sexp_location loc).file scd; tl | _ -> [] in ===================================== src/elab.ml ===================================== @@ -65,6 +65,7 @@ open Printf (* dummies *) let dloc = dummy_location +let dsinfo = DB.dsinfo let parsing_internals = ref false let btl_folder = @@ -108,11 +109,11 @@ type sform_type = | Lazy (* Hasn't looked as the requested type, nor inferred a type. *) type special_forms_map = - (elab_context -> location -> sexp list -> ltype option + (elab_context -> sinfo -> sexp list -> ltype option -> (lexp * sform_type)) SMap.t type special_decl_forms_map = - (elab_context -> location -> sexp list -> elab_context) SMap.t + (elab_context -> sinfo -> sexp list -> elab_context) SMap.t let special_forms : special_forms_map ref = ref SMap.empty let special_decl_forms : special_decl_forms_map ref = ref SMap.empty @@ -141,7 +142,7 @@ let sform_default_ectx = ref empty_elab_context * (i.e. errors signalled here correspond to internal errors rather than * to errors in the user's code). *) -let elab_check_sort (ctx : elab_context) lsort var ltp = +let elab_check_sort (ctx : elab_context) lsort (var: vname) ltp = match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) @@ -152,9 +153,9 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = | _ -> 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, None) -> lexp_error (sexp_location 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 + -> lexp_error (sexp_location 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 @@ -175,7 +176,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var = let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in - let loc = lexp_location lxp in + let loc = lexp_sinfo lxp in let ltype' = try OL.check lctx lxp with e -> match e with @@ -187,7 +188,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc + ~loc:(sexp_location loc) "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' @@ -195,7 +196,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = | e -> info ~print_action:(lexp_print_details lxp) - ~loc + ~loc:(sexp_location loc) "Exception while conversion-checking types: %s and %s" (lexp_string ltype) (lexp_string ltype'); @@ -211,7 +212,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype ]) - ~loc + ~loc:(sexp_location loc) "Type check error: ¡¡ctx_define error!!" let ctx_extend (ctx: elab_context) (var : vname) def ltype = @@ -341,7 +342,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ - -> sexp_error loc "define-operator expects 3 argument"; ctx + -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in @@ -361,7 +362,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 "%s" was not declared%s|} name relateds; + sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc) (* Turn metavar into plain vars after generalization. @@ -490,12 +491,12 @@ let meta_to_var ids (e : lexp) = loop (o' + o) t) :: defs)) defs (len, []) in mkLet (l, ndefs, loop (len + o) e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, loop o t1, loop (1 + o) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, loop o t, loop (1 + o) e) - | Call (f, args) - -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) + | Call (l, f, args) + -> mkCall (l, loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) @@ -599,17 +600,17 @@ let wrapLambda ne vname t _l e = mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e) let elab_p_id ((l,name) : symbol) : vname = - (l, match name with "_" -> None | _ -> Some name) + (Symbol (l, name), match name with "_" -> None | _ -> Some name) (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) - | Symbol ((loc, name) as id) + | Symbol ((loc, name) as _id) -> if not (name = "typer-identifier") then elaborate ctx (Node (Symbol (loc, "typer-identifier"), [se])) ot (* Break the inf-recursion! *) - else elab_varref ctx id + else elab_varref ctx (se, name) (* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) @@ -651,32 +652,32 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = | (e, Inferred t) -> (e, t) and elab_special_form ctx f args ot = - let loc = lexp_location f in + let loc = lexp_sinfo f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) (get_special_form name) ctx loc args ot | _ - -> lexp_error loc f "Unknown special-form: %s" (lexp_string f); + -> lexp_error (sexp_location loc) f "Unknown special-form: %s" (lexp_string f); sform_dummy_ret ctx loc and elab_special_decl_form ctx f args = - let loc = lexp_location f in + let loc = lexp_sinfo f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) (get_special_decl_form name) ctx loc args - | _ -> lexp_error loc f "Unknown special-decl-form: %s" (lexp_string f); ctx + | _ -> lexp_error (sexp_location loc) f "Unknown special-decl-form: %s" (lexp_string f); ctx (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) - -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in + | Arrow (_, ((Aerasable | Aimplicit) as ak), (_, v), t1, t2) + -> let arg = newInstanceMetavar ctx (lexp_sinfo e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args), t) + | _ -> (mkCall (lexp_sinfo e, e, List.rev args), t) in instantiate t [] and resolve_instances e = @@ -686,7 +687,7 @@ and resolve_instances_and_generalize ctx e = resolve_instances e; generalize ctx e -and sdform_typeclass (ctx : elab_context) (_l : location) sargs +and sdform_typeclass (ctx : elab_context) (_l : sinfo) sargs : elab_context = let make_typeclass ctx sarg = let (t, _) = infer sarg ctx in @@ -694,7 +695,7 @@ and sdform_typeclass (ctx : elab_context) (_l : location) sargs in List.fold_left make_typeclass ctx sargs -and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs +and sdform_instance (inst : bool) (ctx : elab_context) (_l : sinfo) sargs : elab_context = let make_instance ctx sarg = let (lxp, _) = infer sarg ctx in @@ -704,7 +705,7 @@ and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs "Only variables can be instances"; ctx) in List.fold_left make_instance ctx sargs -and infer_type pexp ectx var = +and infer_type pexp ectx (var: vname) = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) @@ -717,7 +718,7 @@ and infer_type pexp ectx var = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) - let l = lexp_location s in + let l = lexp_sinfo s in match Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) @@ -729,15 +730,15 @@ and infer_type pexp ectx var = -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) - -> lexp_error l t {|"%s" is not a proper type|} typestr + -> lexp_error (sexp_location l) t {|"%s" is not a proper type|} typestr | (l, Some name) -> lexp_error - l t {|Type of "%s" is not a proper type: %s|} name typestr) + (sexp_location l) t {|Type of "%s" is not a proper type: %s|} name typestr) | [] -> ()); t and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (dsinfo, decls, lxp)) declss body and unify_with_arrow ctx tloc lxp kind var aty @@ -747,11 +748,11 @@ and unify_with_arrow ctx tloc lxp kind var aty let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, var, arg, l, body) in + let arrow = mkArrow (l, kind, var, arg, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error - tloc lxp {|Types:\n %s\n and:\n %s\n do not match!|} + (sexp_location 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 @@ -785,7 +786,7 @@ and unify_or_error lctx lxp ?lxp_name expect actual = and check_inferred ctx e inferred_t t = let (e, inferred_t) = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit), _, _, _, _) + | Arrow (_, (Aerasable | Aimplicit), _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in unify_or_error (ectx_to_lctx ctx) e t inferred_t; @@ -799,7 +800,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let uniqueness_warn pat = warning - ~loc:(pexp_pat_location pat) + ~loc:(sexp_location (pexp_pat_location pat)) "Pattern %s is a duplicate. It will override a previous pattern." (pat_string pat) in @@ -821,7 +822,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) -> lexp_error - loc lctor {|Expected pattern of type "%s", but got "%s"|} + (sexp_location loc) lctor {|Expected pattern of type "%s", but got "%s"|} (lexp_string expected) (lexp_string actual) | [] -> () in match !it_cs_as with @@ -840,12 +841,12 @@ and check_case rtype (loc, target, ppatterns) ctx = (S.identity, []) fargs in let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); + ltarget := check_inferred ctx tlxp tltp (mkCall (loc, it', args)); it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in unify_ind it it'; @@ -875,7 +876,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let tlxp' = shift_to_extended_ctx nctx tlxp in let tltp' = shift_to_extended_ctx nctx tltp in let tlvl' = shift_to_extended_ctx nctx tlvl in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (loc, DB.type_eq, [(Aerasable, tlvl'); (* Typelevel *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) @@ -956,7 +957,7 @@ and check_case rtype (loc, target, ppatterns) ctx = 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 var = ((Symbol(loc, "")), None) in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in if ak = Anormal then sexp_error @@ -969,15 +970,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + (mkCall (dsinfo, lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in let head_lexp_args = List.mapi (fun i (ak, vname) -> (ak, mkVar (vname, List.length fargs - i - 1))) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let head_lexp = mkCall (dsinfo, head_lexp_ctor, head_lexp_args) in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in - SMap.add cons_name (loc, fargs, lexp) lbranches, + SMap.add cons_name (Symbol(loc, ""), fargs, lexp) lbranches, dflt (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it * and try again with the result. *) @@ -988,7 +989,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) -> if Eval.constructor_p name ctx then - add_branch (Symbol (l, name)) [] + add_branch (Symbol (sexp_location l, name)) [] else add_default var (* A named default branch. *) | Ppatcons (pctor, pargs) -> add_branch pctor pargs in @@ -1005,7 +1006,7 @@ and elab_macro_call (ot : ltype option) : lexp * sform_type = - let location = lexp_location func in + let location = lexp_sinfo func in let t = match ot with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location @@ -1014,26 +1015,26 @@ and elab_macro_call if !macro_tracing_enabled then - (trace_macro ~location {|expanding: %s|} (lexp_string func); + (trace_macro ~location:(sexp_location location) {|expanding: %s|} (lexp_string func); List.iteri (fun i arg -> - arg |> sexp_string |> trace_macro ~location {|input %d: %s|} i) + arg |> sexp_string |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) args); let sxp = lexp_expand_macro location func args ctx (Some t) in if !macro_tracing_enabled - then trace_macro ~location {|output: %s|} (sexp_string sxp); + then trace_macro ~location:(sexp_location location) {|output: %s|} (sexp_string sxp); elaborate ctx sxp ot (* Identify Call Type and return processed call. *) and elab_call ctx (func, ltp) (sargs: sexp list) = - let loc = lexp_location func in + let loc = lexp_sinfo func in let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, lexp_lexp' ltp' with - | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) + | _, Arrow (_, ak, (_, Some aname), arg_type, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in let larg = check sarg arg_type ctx in @@ -1042,7 +1043,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (L.mkSusp ret_type (S.substitute larg)) | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, _, arg_type, _, ret_type) + Arrow (_, ak, _, arg_type, ret_type) when (aname = "_") (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in @@ -1062,11 +1063,11 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp (* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, (_l,v), arg_type, _, ret_type) + | _, Arrow (_, ((Aerasable | Aimplicit) as ak), (_l,v), arg_type, ret_type) (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) - -> let arg_loc = try sexp_location (List.hd sargs) with _ -> loc in + -> let arg_loc = try (List.hd sargs) with _ -> loc in let larg = newInstanceMetavar ctx (arg_loc, v) arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) @@ -1083,16 +1084,16 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg :: sargs, _ -> let (arg_type, ret_type) = match lexp_lexp' ltp' with - | Arrow (ak, _, arg_type, _, ret_type) + | Arrow (_, ak, _, arg_type, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) - | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Anormal (dloc, None) None in + | _ -> unify_with_arrow ctx (sarg) + ltp' Anormal (sarg, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs), Inferred ret_type) + (mkCall (loc, func, List.rev largs), Inferred ret_type) (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1109,11 +1110,11 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> mkArrow (ak, n, t, dummy_location, aa)) + -> mkArrow (dsinfo, ak, n, t, aa)) acc impossible in let g = resolve_instances_and_generalize nctx altacc in - let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e)) + let altacc' = g (fun _ne vname t _l e + -> mkArrow (lexp_sinfo e, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1121,7 +1122,7 @@ and lexp_parse_inductive ctors ctx = (* Convert the Lexp back into a list of fields. *) let rec loop e = match lexp_lexp' e with - | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) + | Arrow (_, ak, n, t, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' | (kind, var, exp)::tl @@ -1189,15 +1190,15 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - let value = EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) + let value = EV.eval_call (sexp_location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal loc v "Macro `%s` should return an IO sexp" + | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO sexp" (lexp_string macro_funct)) - | v -> value_fatal loc v "Macro `%s` should return an IO" + | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO" (lexp_string macro_funct) @@ -1222,7 +1223,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* Preserve the new operators added to nctx. *) let (declmap) = List.fold_right - (fun ((l, vname), sexp) (map) -> + (fun ((_l, vname), sexp) (map) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with @@ -1236,7 +1237,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) * proper format, e.g. for `lctx_view`! *) let e = check sexp adjusted_t nctx in (* let d = (v', LetDef (i + 1, e), t) in *) - (IMap.add i ((l, Some vname), e, t) map) + (IMap.add i ((sexp, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1273,13 +1274,13 @@ and infer_and_generalize_type (ctx : elab_context) se name = *) let rec strip_rettype t = match lexp_lexp' t with - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, t1, l, strip_rettype t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, t1, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) + -> mkArrow (Symbol(l,""), Aerasable, name, t, e)) t and infer_and_generalize_def (ctx : elab_context) se = @@ -1288,8 +1289,8 @@ and infer_and_generalize_def (ctx : elab_context) se = let g = resolve_instances_and_generalize nctx e in let e' = g wrapLambda e in let t' = g (fun ne name t _l e - -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, sexp_location se, e)) + -> mkArrow (se, (if ne then Aimplicit else Aerasable), + name, t, e)) t in (e', t') @@ -1333,7 +1334,8 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + -> let ltp = infer_and_generalize_type nctx stp + (stp, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1346,7 +1348,8 @@ and lexp_decls_1 | (_::_) -> lexp_error loc ltp - {|New type annotation "%s" incompatible with previous "%s"|} + {|New type annotation "%s" incompatible with + previous "%s"|} (lexp_string ltp) (lexp_string pt) | [] -> () in recur [] nctx pending_decls pending_defs @@ -1354,7 +1357,8 @@ and lexp_decls_1 pending_defs then (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + else recur [] (ectx_extend nctx (stp, Some vname) + ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ @@ -1366,13 +1370,13 @@ and lexp_decls_1 | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((l, vname)); sexp] + | [Symbol ((_l, vname)); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in + let var = (thesexp, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, @@ -1418,7 +1422,7 @@ and lexp_decls_1 else if (OL.conv_p lctx t (BI.get_predef "Macro" nctx)) then (* expand macro and get the generated declarations *) let lxp, _ltp = infer sxp nctx in - let sdecl' = lexp_expand_macro (sexp_location sxp) lxp sargs nctx None in + let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( error ~loc:(sexp_location sxp) "Invalid declaration syntax"; @@ -1465,9 +1469,9 @@ and sform_declexpr ctx loc sargs _ot = | [e] when is_var e -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; + | None -> error ~loc:(sexp_location loc) "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; + | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1475,7 +1479,7 @@ let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc "decltype expects one argument"; + | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; sform_dummy_ret ctx loc @@ -1492,18 +1496,18 @@ 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 + let bi = mkBuiltin ((sexp_location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc {|Unknown built-in "%s"|} name; + sexp_error (sexp_location 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!"; + | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error ~loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error ~loc "Use of `Built-in` in user code"; + | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs _ot = @@ -1512,9 +1516,9 @@ let sform_datacons ctx loc sargs _ot = -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy) - | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; + | [_;_] -> sexp_error (sexp_location loc) "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc - | _ -> sexp_error loc "##constr requires two arguments"; + | _ -> sexp_error (sexp_location loc) "##constr requires two arguments"; sform_dummy_ret ctx loc let elab_colon_to_ak k = match k with @@ -1525,22 +1529,22 @@ let elab_colon_to_ak k = match k with let elab_datacons_arg s = match s with | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t]) -> (elab_colon_to_ak k, elab_p_id s, t) - | _ -> (Anormal, (sexp_location s, None), s) + | _ -> (Anormal, (s, None), s) let elab_typecons_arg arg : (arg_kind * vname * sexp option) = match arg with - | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e]) + | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (_l,name); e]) -> (elab_colon_to_ak k, - (l, Some name), Some e) - | Symbol (l, name) -> (Anormal, (l, Some name), None) + (arg, Some name), Some e) + | Symbol (_l, name) -> (Anormal, (arg, Some name), None) | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) (sexp_location arg) "Unrecognized formal arg"; - (Anormal, (sexp_location arg, None), None) + (Anormal, (arg, None), None) let sform_typecons ctx loc sargs _ot = match sargs with - | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) + | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) @@ -1589,7 +1593,7 @@ let sform_hastype ctx loc sargs _ot = | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) - | _ -> sexp_error loc "##_:_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_:_ takes two arguments"; sform_dummy_ret ctx loc let sform_arrow kind ctx loc sargs _ot = @@ -1597,12 +1601,12 @@ let sform_arrow kind ctx loc sargs _ot = | [st1; st2] -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) - | _ -> ((sexp_location st1, None), st1) in + | _ -> ((st1, None), st1) in let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type st2 nctx (sexp_location st2, None) in - (mkArrow (kind, v, lt1, loc, lt2), Lazy) - | _ -> sexp_error loc "##_->_ takes two arguments"; + let lt2 = infer_type st2 nctx (st2, None) in + (mkArrow (loc, kind, v, lt1, lt2), Lazy) + | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc let sform_immediate ctx loc sargs ot = @@ -1616,10 +1620,10 @@ let sform_immediate ctx loc sargs ot = let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot | [_se] - -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); + -> (sexp_error (sexp_location loc) ("Non-immediate passed to ##typer-immediate"); sform_dummy_ret ctx loc) | _ - -> (sexp_error loc ("Too many args to ##typer-immediate"); + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-immediate"); sform_dummy_ret ctx loc) @@ -1639,7 +1643,7 @@ let sform_identifier ctx loc sargs ot = (sexp_error l {|Invalid special identifier "%s"|} name; sform_dummy_ret ctx loc) - | [Symbol (loc, name)] + | [Symbol (_loc, name)] when String.length name >= 1 && String.get name 0 = '?' -> let name = if name = "?" then "" else string_sub name 1 (String.length name) in @@ -1663,13 +1667,13 @@ let sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc ("Bug in the elaboration of a metavar" + fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" ^^ " repeated at a different scope level!") | MVal _ -> (* FIXME: We face the same problem as above, but here, the situation is worse, we don't even know the scope level! *) - fatal ~loc "Bug in the elaboration of a repeated metavar!" + fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -1681,19 +1685,20 @@ let sform_identifier ctx loc sargs ot = let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) - | [Symbol id] -> elab_varref ctx id + | [Symbol (_n, name)] + -> elab_varref ctx (loc, name) | [_se] - -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); + -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); sform_dummy_ret ctx loc) | _ - -> (sexp_error loc ("Too many args to ##typer-identifier"); + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); sform_dummy_ret ctx loc) let rec sform_lambda kind ctx loc sargs ot = @@ -1704,7 +1709,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Symbol arg -> (elab_p_id arg, None) | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; - ((dummy_location, None), None) in + ((dsinfo, None), None) in let olt1 = match ost1 with | Some st -> Some (infer_type st ctx arg) @@ -1722,7 +1727,7 @@ let rec sform_lambda kind ctx loc sargs ot = let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (loc, kind, arg, lt1, lt2)) | _ -> alt) in (match ot with @@ -1735,7 +1740,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Some t -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in match lexp_lexp' lp with - | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + | Arrow (_, ak2, _, lt1, lt2) when ak2 = kind -> (match olt1 with | None -> () | Some lt1' @@ -1743,7 +1748,7 @@ let rec sform_lambda kind ctx loc sargs ot = ~lxp_name:"parameter" lt1 lt1'); mklam lt1 (Some lt2) - | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal + | Arrow (_, ak2, v, lt1, lt2) when kind = Anormal (* `t` is an implicit arrow and `kind` is Anormal, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) @@ -1756,7 +1761,7 @@ let rec sform_lambda kind ctx loc sargs ot = let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in (mkLambda (ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) + | Inferred lt2' -> Inferred (mkArrow (loc, ak2, v, lt1, lt2')) | _ -> alt) | _lt @@ -1765,7 +1770,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> sexp_error - loc "##lambda_%s_ takes two arguments" + (sexp_location loc) "##lambda_%s_ takes two arguments" (match kind with | Anormal -> "->" | Aimplicit -> "=>" @@ -1779,7 +1784,7 @@ let rec sform_case ctx loc sargs ot = match sargs with -> (pexp_p_pat pat, code) | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; - (Ppatsym (l, None), Symbol (l, "?")) in + (Ppatsym (se, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in let t = match ot with | Some t -> t @@ -1788,8 +1793,8 @@ let rec sform_case ctx loc sargs ot = match sargs with (le, match ot with Some _ -> Checked | None -> Inferred t) (* In case there are no branches, pretend there was a | anyway. *) - | [_e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot - | _ -> sexp_error loc "Unrecognized case expression"; + | [_e] -> sform_case ctx loc [Node (Symbol (sexp_location loc, "_|_"), sargs)] ot + | _ -> sexp_error (sexp_location loc) "Unrecognized case expression"; sform_dummy_ret ctx loc let sform_letin ctx loc sargs ot = match sargs with @@ -1805,7 +1810,7 @@ let sform_letin ctx loc sargs ot = match sargs with | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) - | _ -> sexp_error loc "Unrecognized let_in_ expression"; + | _ -> sexp_error (sexp_location loc) "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc let sform_proj ctx loc sargs _ = @@ -1815,9 +1820,9 @@ let sform_proj ctx loc sargs _ = let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | [_;_] - -> sexp_error loc "Second argument is not a Symbol!"; + -> sexp_error (sexp_location loc) "Second argument is not a Symbol!"; sform_dummy_ret ctx loc - | _ -> sexp_error loc "Wrong arg number!"; + | _ -> sexp_error (sexp_location loc) "Wrong arg number!"; sform_dummy_ret ctx loc let rec infer_level ctx se : lexp = @@ -1830,7 +1835,7 @@ let rec infer_level ctx se : lexp = -> 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: %s" (sexp_string se); - newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) l) + newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) se) (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1843,7 +1848,7 @@ let sform_type ctx loc sargs _ot = | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) - | _ -> (sexp_error loc "##Type_ expects one argument"; + | _ -> (sexp_error (sexp_location loc) "##Type_ expects one argument"; sform_dummy_ret ctx loc) let sform_debruijn ctx loc sargs _ot = @@ -1854,7 +1859,7 @@ let sform_debruijn ctx loc sargs _ot = sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) - | _ -> (sexp_error loc "##DeBruijn expects one integer argument"; + | _ -> (sexp_error (sexp_location loc) "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc) (* Only print var info *) @@ -1890,7 +1895,7 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc {|Could not load "%s": file not found.|} file_name; [] + -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx @@ -1902,7 +1907,7 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc "argument to load should be one file name (String)"; + | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; !sform_default_ectx) in (* get lexp_context *) @@ -1993,7 +1998,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) in + let v = mkVar ((dsinfo, Some name), idx) in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -2002,7 +2007,7 @@ let default_ectx let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, Some key) e t) + else ctx_define ctx (dsinfo, Some key) e t) (!BI.lmap) lctx in Heap.register_builtins (); ===================================== src/elexp.ml ===================================== @@ -36,8 +36,8 @@ open Sexp (* Sexp type *) module U = Util module L = Lexp -type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type label = symbol module SMap = U.SMap @@ -84,11 +84,11 @@ type elexp = let rec elexp_location e = match e with | Imm s -> sexp_location s - | Var ((l,_), _) -> l + | Var ((l,_), _) -> sexp_location l | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l - | Lambda ((l,_),_) -> l + | Lambda ((l,_),_) -> sexp_location l | Call (f,_) -> elexp_location f | Cons (_, (l, _)) -> l | Case (l,_,_,_) -> l ===================================== src/eval.ml ===================================== @@ -495,7 +495,7 @@ and eval_var ctx lxp v = with | _e -> Log.log_fatal - ~loc + ~loc:(sexp_location loc) "Variable: %s%d was not found\n%s" (L.maybename name) idx (trace_elexp lxp) @@ -558,7 +558,7 @@ and eval_call loc unef i f args = (* 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))])) + -> Vtype (L.mkCall (dsinfo, e, [(Anormal, mkVar (vdummy, -1))])) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) and eval_case ctx i loc target pat dflt = @@ -629,7 +629,7 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let trace_dum = (Var ((loc, None), -1)) in + let trace_dum = (Var ((epsilon (loc), None), -1)) in let eval_call a b = eval_call loc trace_dum depth a b in let sxp, nd, sym, str, it, flt, blk = match args with | [sxp; nd; sym; str; it; flt; blk] -> @@ -717,7 +717,7 @@ and print_eval_trace trace = print_trace " EVAL TRACE " trace a let io_bind loc depth args_val = - let trace_dum = (Var ((loc, None), -1)) in + let trace_dum = (Var ((epsilon (loc), None), -1)) in match args_val with | [Vcommand cmd; callback] @@ -755,8 +755,8 @@ let sys_exit loc _depth args_val = match args_val with let y_operator loc _depth args = match args with | [f] -> let yf_ref = ref Vundefined in - let fname = (dloc, Some "f") in - let yfname = (dloc, Some "yf") in + let fname = (dsinfo, Some "f") in + let yfname = (dsinfo, Some "yf") in let yf = Closure(vdummy, Call (Var (fname, 1), [Var (yfname, 2); @@ -808,7 +808,7 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -822,7 +822,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -843,7 +843,7 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some t), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -861,7 +861,7 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -882,7 +882,7 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i ===================================== src/instargs.ml ===================================== @@ -25,6 +25,7 @@ module U = Util module Unif = Unification open Printf +open Sexp (** If true, log all the matching instances when resolving. *) let debug_list_all_candidates = ref false @@ -40,10 +41,10 @@ let recursion_limit = ref (Some 100) let log_skipped_uncertain_matches = ref (Some Log.Warning) let metavar_resolution_contexts = - ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) + ref (U.IMap.empty : (DB.elab_context * sinfo) U.IMap.t) let lookup_metavar_resolution_ctxt (id : L.meta_id) - : (DB.elab_context * U.location) option + : (DB.elab_context * sinfo) option = U.IMap.find_opt id (!metavar_resolution_contexts) let save_metavar_resolution_ctxt (id : L.meta_id) ctx loc : unit @@ -79,7 +80,7 @@ let in_typeclass_set (ectx : DB.elab_context) (t : L.ltype) : bool = let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = let whnft = OL.lexp_whnf t lctx in match L.lexp_lexp' whnft with - | L.Call (head, _) -> head + | L.Call (_, head, _) -> head | _ -> whnft (** A type is a type class if its head is in the set of type class @@ -112,8 +113,8 @@ let try_match t1 t2 lctx sl = | _ -> Possible let search_instance (instantiate_implicit) (ctx : DB.elab_context) - (loc : U.location) (t : L.ltype) : L.lexp option = - Log.log_debug ~loc "Resolving type `%s`" (L.lexp_string t); + (loc : sinfo) (t : L.ltype) : L.lexp option = + Log.log_debug ~loc:(sexp_location loc) "Resolving type `%s`" (L.lexp_string t); let lctx = DB.ectx_to_lctx ctx in let (_, _, insts) = DB.ectx_to_tcctx ctx in @@ -133,7 +134,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) let var = L.mkVar ((loc,namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc + Log.log_debug ~loc:(sexp_location loc) "Considering potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t); (* All candidates should have a type that is a typeclass. *) @@ -149,7 +150,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | Possible -> (match !log_skipped_uncertain_matches with | Some level -> - Log.log_msg ignore level ~loc + Log.log_msg ignore level ~loc:(sexp_location loc) "Skipping potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t) @@ -178,7 +179,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc + Log.log_debug ~loc:(sexp_location loc) "Found instance for `%s` at index %i: `%s : %s`" (L.lexp_string t) i (L.lexp_string (L.mkVar (vname, i))) (L.lexp_string t'); @@ -199,12 +200,12 @@ let resolve_instances instantiate_implicit e = | MVar _ -> true | _ -> false in if uninstantiated && is_typeclass ctx t then - (match search_instance instantiate_implicit ctx loc t with + (match search_instance instantiate_implicit ctx (loc) t with | Some e -> Unif.associate i e; true | None -> (* The metavar will be generalized, unified, or will remain and cause an error. *) - Log.log_info ~loc "No instance found for type `%s`" + Log.log_info ~loc:(sexp_location loc) "No instance found for type `%s`" (L.lexp_string t); false ) else false ===================================== src/inverse_subst.ml ===================================== @@ -53,6 +53,8 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an type substIR = ((int * int) list * int * int) +let dsinfo = Sexp.dummy_sinfo + (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) @@ -94,7 +96,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) + mkVar ((dsinfo, None), idx) (** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -275,13 +277,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = :: ndefs)) (s, []) defs in mkLet (l, ndefs, apply_inv_subst e s') - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s, l, + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, apply_inv_subst t1 s, apply_inv_subst t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) - | Call (f, args) - -> mkCall (apply_inv_subst f s, + | Call (l, f, args) + -> mkCall (l, apply_inv_subst f s, L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs) ===================================== src/lexp.ml ===================================== @@ -33,9 +33,10 @@ open Grammar (* open Unify *) module S = Subst -type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type meta_id = int (* Identifier of a meta variable. *) +type sinfo = sexp type label = symbol @@ -63,23 +64,23 @@ type ltype = lexp and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level - | Sort of U.location * sort + | Sort of sinfo * sort | Builtin of symbol * ltype | Var of vref - | Proj of U.location * lexp * label + | Proj of sinfo * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype + | Let of sinfo * (vname * lexp * ltype) list * lexp + | Arrow of sinfo * arg_kind * vname * ltype * ltype | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label + | Call of sinfo * lexp * (arg_kind * lexp) list (* Curried call. *) + | Inductive of sinfo * label * ((arg_kind * vname * ltype) list) (* formal Args *) * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp + | Case of sinfo * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (sinfo * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) (* The `subst` will be applied to the the metavar's value when it * gets instantiated. *) @@ -164,6 +165,8 @@ let dummy_scope_level = 0 let builtin_size = ref 0 +let dummy_sinfo = Sexp.dummy_sinfo + let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) @@ -209,11 +212,11 @@ let lexp'_hash (lp : lexp') = (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) - | Arrow (k, v, t1, l, t2) + | Arrow (l, k, v, t1, t2) -> U.combine_hash 7 (U.combine_hash - (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (U.combine_hash (lexp_hash t1) - (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash k)) + (U.combine_hash (Hashtbl.hash v) + (U.combine_hash (lexp_hash t1) (lexp_hash t2)))) | Lambda (k, v, t, e) -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) @@ -239,7 +242,7 @@ let lexp'_hash (lp : lexp') = | Metavar (id, s, v) -> U.combine_hash 12 (U.combine_hash id (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) - | Call (e, args) + | Call (_, e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) @@ -272,11 +275,11 @@ let hc_eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> e1 == e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && t11 == t12 && t21 == t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && t1 == t2 && e1 == e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) @@ -316,17 +319,17 @@ let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkArrow (l, k, v, t1, t2) = hc (Arrow (l, k, v, t1, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) = +let mkCall (l, f, es) = match lexp_lexp' f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | Call (l, f', es'), _ -> hc (Call (l, f', es' @ es)) | _, [] -> f - | _ -> hc (Call (f, es)) + | _ -> hc (Call (l, f, es)) let impossible = mkImm Sexp.dummy_epsilon @@ -513,33 +516,37 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) * S.sink (fun l i -> mkVar (l, i)) l s *) -let rec lexp_location e = - match lexp_lexp' e with +let rec lexp_sinfo s = + match lexp_lexp' s with | Sort (l,_) -> l - | SortLevel (SLsucc e) -> lexp_location e - | SortLevel (SLlub (e, _)) -> lexp_location e - | SortLevel SLz -> U.dummy_location - | Imm s -> sexp_location s + | SortLevel (SLsucc s) -> lexp_sinfo s + | SortLevel (SLlub (s, _)) -> lexp_sinfo s + | SortLevel SLz -> dummy_sinfo + | Imm s -> s | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> l + | Builtin ((l, _), _) -> Symbol (l, "") | Let (l,_,_) -> l - | Arrow (_,_,_,l,_) -> l + | Arrow (l,_,_,_,_) -> l | Lambda (_,(l,_),_,_) -> l - | Call (f,_) -> lexp_location f + | Call (_,f,_) -> lexp_sinfo f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> l + | Cons (_,(l,_)) -> Symbol (l, "") | Case (l,_,_,_,_) -> l - | Susp (e, _) -> lexp_location e + | Susp (s, _) -> lexp_sinfo s (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l | Proj (l,_,_) -> l +let lexp_location e = + sexp_location (lexp_sinfo e) + + (********* Normalizing a term *********) -let vdummy = (U.dummy_location, None) +let vdummy = (dummy_sinfo, None) let maybename n = match n with None -> "<anon>" | Some v -> v -let sname (l,n) = (l, maybename n) +let sname (l,n) = (sexp_location l, maybename n) let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -559,10 +566,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) | (v, def, ty) :: defs -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in mkLet (l, loop s defs, mkSusp e s') - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s)) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, mkSusp t1 s, mkSusp t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) - | Call (f, args) -> mkCall (mkSusp f s, + | Call (l, f, args) -> mkCall (l,mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -627,10 +634,10 @@ let clean e = (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in mkLet (l, ndefs, clean s' e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, clean s t1, clean (ssink v s) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) - | Call (f, args) -> mkCall (clean s f, + | Call (l, f, args) -> mkCall (l, clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -681,9 +688,9 @@ let rec lexp_unparse lxp = | Imm (sexp) -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) - | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) | Proj (l,lxp,(loc,str) ) - -> Node (Symbol (l, "__.__"), + -> Node (Symbol (sexp_location l, "__.__"), [(lexp_unparse lxp);(Symbol (loc,str))]) | Cons (t, (l, name)) -> Node (sdatacons, @@ -697,14 +704,14 @@ let rec lexp_unparse lxp = | Aerasable -> "lambda_≡>_"), [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body]) - | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) + | Arrow (loc, arg_kind, (l,oname), ltp1, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Anormal -> "_->_" + Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), - [Symbol (l,v); ut1])); + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); lexp_unparse ltp2]) | Let (loc, ldecls, body) @@ -717,11 +724,11 @@ let rec lexp_unparse lxp = [Symbol (sname vdef); lexp_unparse lxp]) :: acc) [] ldecls in - Node (Symbol (loc, "let_in_"), + Node (Symbol (sexp_location loc, "let_in_"), [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body]) - | Call(lxp, largs) -> (* (arg_kind * lexp) list *) + | Call(_, lxp, largs) -> (* (arg_kind * lexp) list *) let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs) @@ -735,7 +742,7 @@ let rec lexp_unparse lxp = Node (Symbol label, List.map pexp_u_formal_arg pfargs) :: List.map (fun (name, types) - -> Node (Symbol (loc, name), + -> Node (Symbol (sexp_location loc, name), List.map (fun arg -> match arg with @@ -759,13 +766,13 @@ let rec lexp_unparse lxp = let pat_args = List.map (fun (_kind, ((l,oname) as name)) -> match oname with - | Some vdef -> (Some (l,vdef), name) + | Some vdef -> (Some (sexp_location l,vdef), name) | None -> (None, name)) args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in (Ppatcons (Node (sdatacons, - [bt; Symbol (loc, str)]), + [bt; Symbol (sexp_location loc, str)]), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -775,16 +782,16 @@ let rec lexp_unparse lxp = lexp_unparse dft)::pbranch | None -> pbranch in let e = lexp_unparse target in - Node (Symbol (loc, "case_"), + Node (Symbol (sexp_location loc, "case_"), e :: List.map (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), + Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), [pexp_u_pat pat; branch])) pbranch) (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) - -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx + -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]") | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") @@ -794,8 +801,8 @@ let rec lexp_unparse lxp = | SortLevel (SLlub (l1, l2)) -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), [lexp_unparse l1; lexp_unparse l2]) - | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") + | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -904,10 +911,10 @@ let rec get_precedence expr ctx = | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" - | Arrow (Anormal, _, _, _, _) -> lkp "->" - | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" - | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" - | Call (exp, _) -> get_precedence exp ctx + | Arrow (_, Anormal, _, _, _) -> lkp "->" + | Arrow (_, Aimplicit, _, _, _) -> lkp "=>" + | Arrow (_, Aerasable, _, _, _) -> lkp "≡>" + | Call (_, exp, _) -> get_precedence exp ctx | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> @@ -1015,11 +1022,11 @@ and lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) - | Arrow(k, (_, Some name), tp, _loc, expr) -> + | Arrow(_loc, k, (_, Some name), tp, expr) -> "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str' expr) - | Arrow(k, (_, None), tp, _loc, expr) -> + | Arrow(_loc, k, (_, None), tp, expr) -> "(" ^ (lexp_str' tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" @@ -1032,7 +1039,7 @@ and lexp_str ctx (exp : lexp) : string = | Cons(t, (_, ctor_name)) -> (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name - | Call(fname, args) -> + | Call(_, fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in @@ -1156,11 +1163,11 @@ let rec eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && eq t11 t12 && eq t21 t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && eq t1 t2 && eq e1 e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) ===================================== src/opslexp.ml ===================================== @@ -51,6 +51,9 @@ type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t let error ~location fmt = Log.log_fatal ~section:"OPSLEXP" ~loc:location fmt +let dloc = DB.dloc +let dsinfo = DB.dsinfo + module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but * I haven't found any such functionality in OCaml's libs. *) @@ -127,7 +130,7 @@ let rec lctx_to_subst lctx = L.ssink v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in - let s2 = lexp_defs_subst DB.dloc S.identity + let s2 = lexp_defs_subst dsinfo S.identity (List.rev defs) in L.scompose s2 s1 @@ -177,17 +180,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = * things like full normalization (e.g. lexp_conv_p). *) | Some e' -> lexp_whnf e' ctx) | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - | Call (e, []) -> lexp_whnf e ctx - | Call (f, (((_, arg)::args) as xs)) -> + | Call (_, e, []) -> lexp_whnf e ctx + | Call (l, f, (((_, arg)::args) as xs)) -> (match lexp'_whnf f ctx with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) @@ -200,7 +203,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, + mkCall (l, DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; L.Aerasable, e]) in @@ -230,12 +233,12 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:l + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] - | Call (f, aargs) -> + | Call (_, f, aargs) -> (match lexp'_whnf f ctx with | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) @@ -243,7 +246,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = | Proj (loc, lxp, (_loc, label)) -> let c, args = match lexp'_whnf lxp ctx with - | Call (f, args) -> f, args + | Call (_loc, f, args) -> f, args | _ -> lxp, [] in (match lexp'_whnf c ctx with | Cons (it, _) -> @@ -256,17 +259,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc + | _ , [] -> Log.log_error ~loc:(sexp_location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc + Log.log_fatal ~loc:(sexp_location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc "Proj on a non-tuple in WHNF!"; e) + | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *) | Metavar (idx, s, _) @@ -288,7 +291,7 @@ and eq_cast_whnf ctx args = match args with | [_l; _t; _x; _y; (_, p); _f; (_, fx)] -> (match lexp'_whnf p ctx with - | Call (refl, _) when conv_p ctx refl DB.eq_refl + | Call (_, refl, _) when conv_p ctx refl DB.eq_refl -> Some (lexp_whnf fx ctx) | _ -> None) | _ -> None @@ -378,7 +381,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _ -> false) | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 - | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, _vd2, t21, _, t22)) + | (Arrow (_, ak1, vd1, t11, t12), Arrow (_, ak2, _vd2, t21, t22)) -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') @@ -388,7 +391,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs') e1 e2 - | (Call (f1, args1), Call (f2, args2)) + | (Call (_, f1, args1), Call (_, f2, args2)) -> let conv_arglist_p args1 args2 : bool = List.fold_left2 (fun eqp (ak1,t1) (ak2,t2) @@ -441,7 +444,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) let fargs, ctors = @@ -456,12 +459,12 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tlxp = mkSusp target subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (dsinfo, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) (L.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + DB.lexp_ctx_cons ctx (dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types from the inductive. Instead, we work with the lists of @@ -492,9 +495,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), + let ctor = mkSusp (mkCall (dsinfo, mkCons (it, (DB.dloc, l1)), eaargs)) subst in - let hlxp = mkCall (ctor, args) in + let hlxp = mkCall (dsinfo, ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 ) (SMap.bindings cases1) (SMap.bindings cases2) @@ -505,7 +508,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in - let hlxp = mkVar ((DB.dloc, None), 0) in + let hlxp = mkVar ((dsinfo, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' 2) e1 e2 | None, None -> true @@ -661,7 +664,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -687,14 +690,14 @@ 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, loc, t2) + | Arrow (loc, ak, v, t1, 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 loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; @@ -704,18 +707,18 @@ and check'' erased ctx e = 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, + mkArrow (l, ak, v, t, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) e)) - | Call (f, args) + | Call (_, f, args) -> let ft = check erased ctx f in 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) + | Arrow (_l, ak', _v, t1, t2) -> if ak != ak' then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; assert_type ctx arg at t1; @@ -778,7 +781,7 @@ and check'' erased ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, + mkArrow (lexp_sinfo t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -787,7 +790,7 @@ and check'' erased ctx e = | Proj (l, e, (loc, label)) -> ( let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in @@ -799,20 +802,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:l + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasable field: %s" + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -824,16 +827,16 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:l + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in (* FIXME save the type in the case lexp instead of recomputing @@ -854,14 +857,14 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:l "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (l, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) @@ -882,13 +885,13 @@ and check'' erased ctx e = -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) + (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:l "Wrong number of args to constructor!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, (l, name)), + mkCall (l, mkCons (it, (sexp_location l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -902,7 +905,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:l "Redundant default clause"; + then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -915,8 +918,8 @@ and check'' erased ctx e = -> 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!"); + ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -931,21 +934,21 @@ and check'' erased ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), + mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (lexp_sinfo ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with | Not_found - -> log_tc_error ~loc:l {|Constructor "%s" does not exist|} name; + -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; DB.type_int) | _ -> log_tc_error ~loc:(lexp_location e) @@ -1020,9 +1023,9 @@ and fv (e : lexp) : (DB.set * mv_set) = o - 1)) (fv e, len) defs in fv_hoist len fvs - | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) + | Arrow (_, _, _, t1, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) - | Call (f, args) + | Call (_, f, args) -> List.fold_left (fun fvs (ak, arg) -> let afvs = fv arg in fv_union fvs @@ -1102,7 +1105,7 @@ and get_type ctx e = let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (get_type ctx e) ctx in let it, aargs = call_split etype in @@ -1114,21 +1117,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:l + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1140,16 +1143,16 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:l + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, l, t2) + | Arrow (l, ak, v, t1, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -1158,15 +1161,15 @@ and get_type ctx e = | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) - -> (mkArrow (ak, v, t, l, + -> (mkArrow (l, ak, v, t, get_type (DB.lctx_extend ctx v Variable t) e)) - | Call (f, args) + | Call (_l, f, args) -> let ft = get_type ctx f in List.fold_left (fun ft (_ak,arg) -> match lexp'_whnf ft ctx with - | Arrow (_ak', _v, _t1, _l, t2) + | Arrow (_l, _ak', _v, _t1, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args @@ -1204,14 +1207,14 @@ and get_type ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, + -> mkArrow (lexp_sinfo t, ak, v, t, arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with - | Inductive (_l, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -1222,16 +1225,16 @@ and get_type ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), + mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (lexp_sinfo ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with Not_found -> DB.type_int) @@ -1280,7 +1283,7 @@ let arity_of_cons let pos_of_label lctx label e : int = let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in let it, aargs = call_split (lexp_whnf e lctx) in @@ -1322,7 +1325,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Var (v) -> E.Var (v) | L.Proj (l, exp, label) -> let t = get_type lctx exp in - E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) + E.Proj (sexp_location l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) @@ -1334,15 +1337,15 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - E.Let (l, edecls, erase_type lctx' body) + E.Let (sexp_location l, edecls, erase_type lctx' body) - | L.Call (fct, args) + | L.Call (_, fct, 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 let ebranches = clean_branch_map lctx branches in - E.Case (location, etarget, ebranches, clean_default lctx default) + E.Case (sexp_location location, etarget, ebranches, clean_default lctx default) | L.Susp (l, s) -> erase_type lctx (L.push_susp l s) @@ -1391,7 +1394,7 @@ and clean_branch_map lctx cases = in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (l, eargs, erase_type lctx' (L.push_susp expr subst)) + (sexp_location l, eargs, erase_type lctx' (L.push_susp expr subst)) in SMap.map clean_branch cases @@ -1404,7 +1407,7 @@ let erase_type lctx lxp = Log.log_fatal ~print_action:(fun () -> IMap.iter (fun i (_, t, _, (l, n)) -> - print_endline ("\t" ^ (Source.Location.to_string l) + print_endline ("\t" ^ (Source.Location.to_string (sexp_location l)) ^ " ?" ^ (Option.value ~default:"" n) ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) ) mvs) @@ -1434,17 +1437,17 @@ let ctx2tup ctx nctx = | DB.CVfix (_, nctx) as bloc -> get_blocs nctx (bloc :: blocs) | _ -> assert false in let rec mk_lets_and_tup blocs types = - let loc = U.dummy_location in + let loc = dsinfo in match blocs with | [] -> let cons_name = "cons" in - let cons_label = (loc, cons_name) in - let type_label = (loc, "record") in + let cons_label = (sexp_location loc, cons_name) in + let type_label = (sexp_location loc, "record") in let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) - mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (dsinfo, mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, ===================================== src/pexp.ml ===================================== @@ -20,7 +20,6 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) -open Util open Sexp (* Symbol *) let pexp_error loc = Log.log_error ~section:"PEXP" ~loc @@ -43,7 +42,7 @@ type ppat = let pexp_pat_location e = match e with | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> sexp_location e + | Ppatcons (e, _) -> e let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with @@ -56,28 +55,28 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | None -> Symbol (l, "_")]) let pexp_p_pat_arg (s : sexp) = match s with - | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) - -> (Some f, (l, Some n)) + | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) + | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) + -> (Some f, (s, Some n)) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; - (None, (loc, None)) + (None, (s, None)) let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l,_) as n) -> Node (Symbol (l, "_:=_"), [Symbol n; pname]) let pexp_p_pat (s : sexp) : ppat = match s with - | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) + | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatsym (l, None) + pexp_error l "Unknown pattern"; Ppatsym (s, None) let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (l, "_") - | Ppatsym (l, Some n) -> Symbol (l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args) ===================================== src/positivity.ml ===================================== @@ -69,7 +69,7 @@ let rec positive (index : db_index) (lexp : lexp) : bool = and positive' index lexp = match Lexp.lexp_lexp' lexp with - | Lexp.Arrow (_, _, tau, _, e) + | Lexp.Arrow (_, _, _, tau, e) (* * x ⊢ e pos x ∉ fv(τ) * ────────────────────── @@ -77,7 +77,7 @@ and positive' index lexp = *) -> absent index tau && positive' (index + 1) e - | Lexp.Call (f, args) + | Lexp.Call (_, f, args) (* * x ∉ fv(e⃗) * ────────────── ===================================== src/sexp.ml ===================================== @@ -38,10 +38,15 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Float of location * float | Node of sexp * sexp list type token = sexp +type sinfo = sexp let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location +let dummy_sinfo = epsilon dummy_location + +type vname = sinfo * string option +type vref = vname * db_index (********************** Sexp tests **********************) let pred_symbol s pred = ===================================== src/unification.ml ===================================== @@ -40,6 +40,9 @@ let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int) let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) = create_metavar_1 sl t (Myers.length ctx) +let dloc = DB.dloc +let dsinfo = DB.dsinfo + (* For convenience *) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) @@ -78,9 +81,9 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs - | Arrow (_, _, t1, _, t2) -> oi t1 || oi t2 + | Arrow (_, _, _, t1, t2) -> oi t1 || oi t2 | Lambda (_, _, t, e) -> oi t || oi e - | Call (f, args) + | Call (_, f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args | Inductive (_, _, args, cases) -> SMap.fold @@ -143,7 +146,7 @@ let common_subset ctx s1 s2 = && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), + | s' -> S.Cons (mkVar ((lexp_sinfo le1, None), 0), s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that @@ -151,11 +154,11 @@ let common_subset ctx s1 s2 = * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop s1 (S.Cons (mkVar ((dsinfo, None), 0), S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop (S.Cons (mkVar ((dsinfo, None), 0), S.Identity 1, o1')) s2 o1 o2 o | (S.Identity o1', S.Identity o2') @@ -282,8 +285,8 @@ and unify' (e1: lexp) (e2: lexp) and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' arrow, lexp_lexp' lxp) with - | (Arrow (var_kind1, v1, ltype1, _, lexp1), - Arrow (var_kind2, _, ltype2, _, lexp2)) + | (Arrow (_, var_kind1, v1, ltype1, lexp1), + Arrow (_, var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 (srename v1 lexp2) @@ -445,7 +448,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' call, lexp_lexp' lxp) with - | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) + | (Call (_, lxp_left, lxp_list1), Call (_, lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> (try List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then @@ -457,10 +460,10 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs -> [(CKresidual, ctx, call, lxp)]) | (call', lxp') -> let head_left = match call' with - | Call (head_left, _) -> head_left + | Call (_, head_left, _) -> head_left | _ -> call in let head_right = match lxp' with - | Call (head_right, _) -> head_right + | Call (_, head_right, _) -> head_right | _ -> lxp in let for_sure_irreducible_call_head ctx head = match OL.lexp'_whnf head ctx with ===================================== src/util.ml ===================================== @@ -33,11 +33,9 @@ let dummy_location = Source.Location.dummy (* Occurrence of a variable's symbol: we use DeBruijn index, and for * debugging purposes, we remember the name that was used in the source * code. *) -type vname = location * string option type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vname * db_index type bottom = | B_o_t_t_o_m_ of bottom ===================================== tests/env_test.ml ===================================== @@ -30,6 +30,7 @@ open Typerlib open Utest_lib open Env +let dsinfo = DB.dsinfo let rctx = Elab.default_rctx @@ -41,11 +42,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> if 10 <= (!global_verbose_lvl) then ( let var = [ - ((dloc, Some "a"), DB.type_int, (make_val "a")); - ((dloc, Some "b"), DB.type_int, (make_val "b")); - ((dloc, Some "c"), DB.type_int, (make_val "c")); - ((dloc, Some "d"), DB.type_int, (make_val "d")); - ((dloc, Some "e"), DB.type_int, (make_val "e")); + ((dsinfo, Some "a"), DB.type_int, (make_val "a")); + ((dsinfo, Some "b"), DB.type_int, (make_val "b")); + ((dsinfo, Some "c"), DB.type_int, (make_val "c")); + ((dsinfo, Some "d"), DB.type_int, (make_val "d")); + ((dsinfo, Some "e"), DB.type_int, (make_val "e")); ] in let n = (List.length var) - 1 in ===================================== tests/instargs_test.ml ===================================== @@ -34,10 +34,10 @@ let add_test = add_test "INSTARGS" let default_ectx = E.default_ectx let default_rctx = E.default_rctx -let dummy_vname = Util.dummy_location, None +let dummy_vname = DB.dsinfo, None let make_metavar t ctx = - E.newInstanceMetavar ctx (Util.dummy_location, Some "inst") t + E.newInstanceMetavar ctx (DB.dsinfo, Some "inst") t let lexp_from_str str ctx = List.hd (E.lexp_expr_str str ctx) @@ -171,7 +171,7 @@ let to_nat n ctx = let s = lexp_from_str "S" ctx in let z = lexp_from_str "Z" ctx in let rec loop i nat = - if i = 0 then nat else loop (i - 1) (L.mkCall (s,[Pexp.Anormal, nat])) in + if i = 0 then nat else loop (i - 1) (L.mkCall (DB.dsinfo, s,[Pexp.Anormal, nat])) in loop n z let to_snat n ctx = @@ -181,13 +181,13 @@ let to_snat n ctx = let rec loop i nat snat = if i = 0 then snat else loop (i - 1) - (L.mkCall (s,[Pexp.Anormal, nat])) - (L.mkCall (ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in + (L.mkCall (DB.dsinfo, s,[Pexp.Anormal, nat])) + (L.mkCall (DB.dsinfo, ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in loop n (to_nat 0 ctx) zs let snat_n_t n ctx = let snat = lexp_from_str "SNat" ctx in - L.mkCall (snat, [Pexp.Anormal, to_nat n ctx]) + L.mkCall (DB.dsinfo, snat, [Pexp.Anormal, to_nat n ctx]) let snat_metavar i ctx = make_metavar (snat_n_t i ctx) ctx ===================================== tests/positivity_test.ml ===================================== @@ -23,7 +23,7 @@ open Utest_lib open Lexp open Positivity -open Util +(*open Util*) exception WrongPolarity of vname ===================================== tests/unify_test.ml ===================================== @@ -35,6 +35,8 @@ module U = Util let ectx = Elab.default_ectx let rctx = Elab.default_rctx +let dsinfo = DB.dsinfo + type result = | Constraint | Unification @@ -94,19 +96,19 @@ let _ = | Z | S (Nat); |} ectx in - let dloc = U.dummy_location in - let nat = mkVar ((dloc, Some "Nat"), 2) in + let dsinfo = DB.dsinfo in + let nat = mkVar ((dsinfo, Some "Nat"), 2) in let shift l i = mkSusp l (S.shift i) in let ectx, _ = List.fold_left (fun (ectx, i) (name, lexp) -> - Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) + Elab.ctx_extend ectx (dsinfo, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, - dloc, shift nat 2)))); + [("f", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("g", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("h", (mkArrow (dsinfo, Anormal, (dsinfo, Some "x"), nat, + mkArrow (dsinfo, Anormal, (dsinfo, Some "y"), shift nat 1, + shift nat 2)))); ("a", nat); ("b", nat)] in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a2bc3d5cd1557a79404e1e58f383bc64… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a2bc3d5cd1557a79404e1e58f383bc64… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][location-sinfo] [OK] Compilateur
by Ismaila FALL (＠Fallismaila) 26 Mai '22

26 Mai '22

Ismaila FALL pushed to branch location-sinfo at Stefan / Typer Commits: c422f432 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-05-26T18:51:50+00:00 [OK] Compilateur - - - - - 21 changed files: - + Int - debug_util.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/instargs.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/positivity.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/env_test.ml - tests/instargs_test.ml - tests/positivity_test.ml - tests/unify_test.ml Changes: ===================================== Int ===================================== @@ -0,0 +1,28 @@ +btl/builtins.typer:Integer->Int = Built-in "Integer->Int" : Integer -> Int; +btl/builtins.typer:Integer->String = Built-in "Integer->String" : Integer -> String; +btl/pervasive.typer: | nil => (Integer->Int 0) +btl/pervasive.typer: (Int_+ (Integer->Int 1) (List_length tl)); +btl/pervasive.typer: => case Int_<= n (Integer->Int 0) +btl/pervasive.typer: | false => List_nth (Int_- n (Integer->Int 1)) xs d; +btl/pervasive.typer: | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); +btl/pervasive.typer:in helper f (Integer->Int 0) xs; +btl/pervasive.typer:List_empty xs = Int_eq (List_length xs) (Integer->Int 0); +btl/pervasive.typer: (cons (List_nth (Integer->Int 1) ss Sexp_error) nil))); +btl/pervasive.typer: head = List_nth (Integer->Int 0) head-pair Sexp_error; +btl/pervasive.typer: type-type = List_nth (Integer->Int 1) head-pair Sexp_error; +btl/pervasive.typer: | vnil (p ::: Eq n (Integer->Int 0)) +btl/pervasive.typer: | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1))); +btl/pervasive.typer: let e1 = List_nth (Integer->Int 0) args Sexp_error; +btl/pervasive.typer: e2 = List_nth (Integer->Int 1) args Sexp_error; +btl/pervasive.typer: e3 = List_nth (Integer->Int 2) args Sexp_error; +btl/pervasive.typer:in case (Int_eq r (Integer->Int -1)) +btl/poly-lits.typer:IntFromInteger = mkFromInteger Integer->Int; +btl/tuple.typer: elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); +samples/nats.typer:Integer->Nat : Integer -> Nat; +samples/nats.typer:Integer->Nat i = +samples/nats.typer: S (Integer->Nat (Integer_- i 1)) +samples/nats.typer:NatFromInteger = mkFromInteger Integer->Nat; +src/eval.ml: let name = "Integer->Int" in +src/eval.ml: | _ -> error loc "Integer->String expects one Integer argument" +src/eval.ml: ("Integer->String", integer_to_string, 1); +tests/eval_test.ml:intFromIntegerCoercion = mkCoercible (Integer->Int); ===================================== debug_util.ml ===================================== @@ -59,6 +59,7 @@ open Debruijn open Env let dloc = dummy_location +let dsinfo = DB.dsinfo let dummy_decl = Imm(String(dloc, "Dummy")) let discard _v = () @@ -306,7 +307,7 @@ let main () = let main = (senv_lookup "main" nctx) in (* get main body *) - let body = (get_rte_variable (dloc, Some "main") main rctx) in + let body = (get_rte_variable (dsinfo, Some "main") main rctx) in (* eval main *) print_eval_result 1 body ===================================== src/builtin.ml ===================================== @@ -98,9 +98,10 @@ let set_predef name lexp (* Builtin types *) let dloc = DB.dloc +let dsinfo = DB.dsinfo -let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, - mkArrow (Anormal, (dloc, None), t, dloc, t)) +let op_binary t = mkArrow (dsinfo, Anormal, (dsinfo, None), t, + mkArrow (dsinfo, Anormal, (dsinfo, None), t, t)) let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx @@ -159,7 +160,7 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl let type_arrow_0 = - mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + mkArrow (dsinfo, Anormal, (dsinfo, None), DB.type0, DB.type0) let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in ===================================== src/debruijn.ml ===================================== @@ -36,6 +36,7 @@ module Str = Str open Util +open Sexp open Lexp @@ -117,45 +118,47 @@ let set_ascending_seq ((o, m) : set) : int Seq.t = * ---------------------------------- *) let dloc = dummy_location -let type_level_sort = mkSort (dloc, StypeLevel) -let sort_omega = mkSort (dloc, StypeOmega) +let dsinfo = dummy_sinfo + +let type_level_sort = mkSort (dsinfo, StypeLevel) +let sort_omega = mkSort (dsinfo, StypeOmega) let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) -let type0 = mkSort (dloc, Stype level0) -let type1 = mkSort (dloc, Stype level1) -let type2 = mkSort (dloc, Stype level2) +let type0 = mkSort (dsinfo, Stype level0) +let type1 = mkSort (dsinfo, Stype level1) +let type2 = mkSort (dsinfo, Stype level2) let type_int = mkBuiltin ((dloc, "Int"), type0) let type_integer = mkBuiltin ((dloc, "Integer"), type0) let type_float = mkBuiltin ((dloc, "Float"), type0) let type_string = mkBuiltin ((dloc, "String"), type0) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1), + mkSort (dsinfo, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - let xv = (dloc, Some "x") in + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + let xv = (dsinfo, Some "x") in mkBuiltin ((dloc, "Eq.refl"), - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, - mkVar (tv, 0), dloc, - mkCall (type_eq, + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Aerasable, xv, + mkVar (tv, 0), + mkCall (dsinfo, type_eq, [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); @@ -465,7 +468,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name @@ -475,7 +478,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = with | Not_found -> fatal - ~loc "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + ~loc:(sexp_location 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 ===================================== @@ -121,7 +121,7 @@ let debug_lexp_decls decls = List.iter (fun e -> let ((loc, _name), lxp, _ltp) = e in - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc)); let str = lexp_str_decls (!debug_ppctx) [e] in @@ -137,7 +137,7 @@ let debug_lexp_decls decls = let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" loc.file scd; + -> printf " FILE: %-25s : %s\n" (sexp_location loc).file scd; tl | _ -> [] in ===================================== src/elab.ml ===================================== @@ -65,6 +65,7 @@ open Printf (* dummies *) let dloc = dummy_location +let dsinfo = DB.dsinfo let parsing_internals = ref false let btl_folder = @@ -108,11 +109,11 @@ type sform_type = | Lazy (* Hasn't looked as the requested type, nor inferred a type. *) type special_forms_map = - (elab_context -> location -> sexp list -> ltype option + (elab_context -> sinfo -> sexp list -> ltype option -> (lexp * sform_type)) SMap.t type special_decl_forms_map = - (elab_context -> location -> sexp list -> elab_context) SMap.t + (elab_context -> sinfo -> sexp list -> elab_context) SMap.t let special_forms : special_forms_map ref = ref SMap.empty let special_decl_forms : special_decl_forms_map ref = ref SMap.empty @@ -141,7 +142,7 @@ let sform_default_ectx = ref empty_elab_context * (i.e. errors signalled here correspond to internal errors rather than * to errors in the user's code). *) -let elab_check_sort (ctx : elab_context) lsort var ltp = +let elab_check_sort (ctx : elab_context) lsort (var: vname) ltp = match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) @@ -152,9 +153,9 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = | _ -> 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, None) -> lexp_error (sexp_location 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 + -> lexp_error (sexp_location 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 @@ -175,7 +176,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var = let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in - let loc = lexp_location lxp in + let loc = sinfo_location lxp in let ltype' = try OL.check lctx lxp with e -> match e with @@ -187,7 +188,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc + ~loc:(sexp_location loc) "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' @@ -195,7 +196,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = | e -> info ~print_action:(lexp_print_details lxp) - ~loc + ~loc:(sexp_location loc) "Exception while conversion-checking types: %s and %s" (lexp_string ltype) (lexp_string ltype'); @@ -211,7 +212,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype ]) - ~loc + ~loc:(sexp_location loc) "Type check error: ¡¡ctx_define error!!" let ctx_extend (ctx: elab_context) (var : vname) def ltype = @@ -341,7 +342,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ - -> sexp_error loc "define-operator expects 3 argument"; ctx + -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in @@ -361,7 +362,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 "%s" was not declared%s|} name relateds; + sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc) (* Turn metavar into plain vars after generalization. @@ -490,12 +491,12 @@ let meta_to_var ids (e : lexp) = loop (o' + o) t) :: defs)) defs (len, []) in mkLet (l, ndefs, loop (len + o) e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, loop o t1, loop (1 + o) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, loop o t, loop (1 + o) e) - | Call (f, args) - -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) + | Call (l, f, args) + -> mkCall (l, loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) @@ -599,17 +600,17 @@ let wrapLambda ne vname t _l e = mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e) let elab_p_id ((l,name) : symbol) : vname = - (l, match name with "_" -> None | _ -> Some name) + (Symbol (l, name), match name with "_" -> None | _ -> Some name) (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) - | Symbol ((loc, name) as id) + | Symbol ((loc, name) as _id) -> if not (name = "typer-identifier") then elaborate ctx (Node (Symbol (loc, "typer-identifier"), [se])) ot (* Break the inf-recursion! *) - else elab_varref ctx id + else elab_varref ctx (se, name) (* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) @@ -651,32 +652,32 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = | (e, Inferred t) -> (e, t) and elab_special_form ctx f args ot = - let loc = lexp_location f in + let loc = sinfo_location f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) (get_special_form name) ctx loc args ot | _ - -> lexp_error loc f "Unknown special-form: %s" (lexp_string f); + -> lexp_error (sexp_location loc) f "Unknown special-form: %s" (lexp_string f); sform_dummy_ret ctx loc and elab_special_decl_form ctx f args = - let loc = lexp_location f in + let loc = sinfo_location f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _) -> (* Special form. *) (get_special_decl_form name) ctx loc args - | _ -> lexp_error loc f "Unknown special-decl-form: %s" (lexp_string f); ctx + | _ -> lexp_error (sexp_location loc) f "Unknown special-decl-form: %s" (lexp_string f); ctx (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) - -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in + | Arrow (_, ((Aerasable | Aimplicit) as ak), (_, v), t1, t2) + -> let arg = newInstanceMetavar ctx (sinfo_location e, v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args), t) + | _ -> (mkCall (sinfo_location e, e, List.rev args), t) in instantiate t [] and resolve_instances e = @@ -686,7 +687,7 @@ and resolve_instances_and_generalize ctx e = resolve_instances e; generalize ctx e -and sdform_typeclass (ctx : elab_context) (_l : location) sargs +and sdform_typeclass (ctx : elab_context) (_l : sinfo) sargs : elab_context = let make_typeclass ctx sarg = let (t, _) = infer sarg ctx in @@ -694,7 +695,7 @@ and sdform_typeclass (ctx : elab_context) (_l : location) sargs in List.fold_left make_typeclass ctx sargs -and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs +and sdform_instance (inst : bool) (ctx : elab_context) (_l : sinfo) sargs : elab_context = let make_instance ctx sarg = let (lxp, _) = infer sarg ctx in @@ -704,7 +705,7 @@ and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs "Only variables can be instances"; ctx) in List.fold_left make_instance ctx sargs -and infer_type pexp ectx var = +and infer_type pexp ectx (var: vname) = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) @@ -717,7 +718,7 @@ and infer_type pexp ectx var = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) - let l = lexp_location s in + let l = sinfo_location s in match Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) @@ -729,15 +730,15 @@ and infer_type pexp ectx var = -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) - -> lexp_error l t {|"%s" is not a proper type|} typestr + -> lexp_error (sexp_location l) t {|"%s" is not a proper type|} typestr | (l, Some name) -> lexp_error - l t {|Type of "%s" is not a proper type: %s|} name typestr) + (sexp_location l) t {|Type of "%s" is not a proper type: %s|} name typestr) | [] -> ()); t and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (dsinfo, decls, lxp)) declss body and unify_with_arrow ctx tloc lxp kind var aty @@ -747,11 +748,11 @@ and unify_with_arrow ctx tloc lxp kind var aty let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, var, arg, l, body) in + let arrow = mkArrow (l, kind, var, arg, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error - tloc lxp {|Types:\n %s\n and:\n %s\n do not match!|} + (sexp_location 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 @@ -785,7 +786,7 @@ and unify_or_error lctx lxp ?lxp_name expect actual = and check_inferred ctx e inferred_t t = let (e, inferred_t) = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit), _, _, _, _) + | Arrow (_, (Aerasable | Aimplicit), _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in unify_or_error (ectx_to_lctx ctx) e t inferred_t; @@ -799,7 +800,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let uniqueness_warn pat = warning - ~loc:(pexp_pat_location pat) + ~loc:(sexp_location (pexp_pat_location pat)) "Pattern %s is a duplicate. It will override a previous pattern." (pat_string pat) in @@ -821,7 +822,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) -> lexp_error - loc lctor {|Expected pattern of type "%s", but got "%s"|} + (sexp_location loc) lctor {|Expected pattern of type "%s", but got "%s"|} (lexp_string expected) (lexp_string actual) | [] -> () in match !it_cs_as with @@ -840,12 +841,12 @@ and check_case rtype (loc, target, ppatterns) ctx = (S.identity, []) fargs in let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); + ltarget := check_inferred ctx tlxp tltp (mkCall (loc, it', args)); it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in unify_ind it it'; @@ -875,7 +876,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let tlxp' = shift_to_extended_ctx nctx tlxp in let tltp' = shift_to_extended_ctx nctx tltp in let tlvl' = shift_to_extended_ctx nctx tlvl in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (loc, DB.type_eq, [(Aerasable, tlvl'); (* Typelevel *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) @@ -956,7 +957,7 @@ and check_case rtype (loc, target, ppatterns) ctx = 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 var = ((Symbol(loc, "")), None) in let nctx = ctx_extend ctx var Variable (mkSusp fty s) in if ak = Anormal then sexp_error @@ -969,15 +970,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + (mkCall (dsinfo, lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in let head_lexp_args = List.mapi (fun i (ak, vname) -> (ak, mkVar (vname, List.length fargs - i - 1))) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let head_lexp = mkCall (dsinfo, head_lexp_ctor, head_lexp_args) in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in - SMap.add cons_name (loc, fargs, lexp) lbranches, + SMap.add cons_name (Symbol(loc, ""), fargs, lexp) lbranches, dflt (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it * and try again with the result. *) @@ -988,7 +989,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) -> if Eval.constructor_p name ctx then - add_branch (Symbol (l, name)) [] + add_branch (Symbol (sexp_location l, name)) [] else add_default var (* A named default branch. *) | Ppatcons (pctor, pargs) -> add_branch pctor pargs in @@ -1005,7 +1006,7 @@ and elab_macro_call (ot : ltype option) : lexp * sform_type = - let location = lexp_location func in + let location = sinfo_location func in let t = match ot with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location @@ -1014,26 +1015,26 @@ and elab_macro_call if !macro_tracing_enabled then - (trace_macro ~location {|expanding: %s|} (lexp_string func); + (trace_macro ~location:(sexp_location location) {|expanding: %s|} (lexp_string func); List.iteri (fun i arg -> - arg |> sexp_string |> trace_macro ~location {|input %d: %s|} i) + arg |> sexp_string |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) args); let sxp = lexp_expand_macro location func args ctx (Some t) in if !macro_tracing_enabled - then trace_macro ~location {|output: %s|} (sexp_string sxp); + then trace_macro ~location:(sexp_location location) {|output: %s|} (sexp_string sxp); elaborate ctx sxp ot (* Identify Call Type and return processed call. *) and elab_call ctx (func, ltp) (sargs: sexp list) = - let loc = lexp_location func in + let loc = sinfo_location func in let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, lexp_lexp' ltp' with - | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) + | _, Arrow (_, ak, (_, Some aname), arg_type, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in let larg = check sarg arg_type ctx in @@ -1042,7 +1043,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (L.mkSusp ret_type (S.substitute larg)) | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, _, arg_type, _, ret_type) + Arrow (_, ak, _, arg_type, ret_type) when (aname = "_") (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in @@ -1062,11 +1063,11 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp (* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, (_l,v), arg_type, _, ret_type) + | _, Arrow (_, ((Aerasable | Aimplicit) as ak), (_l,v), arg_type, ret_type) (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) - -> let arg_loc = try sexp_location (List.hd sargs) with _ -> loc in + -> let arg_loc = try (List.hd sargs) with _ -> loc in let larg = newInstanceMetavar ctx (arg_loc, v) arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) @@ -1083,16 +1084,16 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg :: sargs, _ -> let (arg_type, ret_type) = match lexp_lexp' ltp' with - | Arrow (ak, _, arg_type, _, ret_type) + | Arrow (_, ak, _, arg_type, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) - | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Anormal (dloc, None) None in + | _ -> unify_with_arrow ctx (sarg) + ltp' Anormal (sarg, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs), Inferred ret_type) + (mkCall (loc, func, List.rev largs), Inferred ret_type) (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1109,11 +1110,11 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> mkArrow (ak, n, t, dummy_location, aa)) + -> mkArrow (dsinfo, ak, n, t, aa)) acc impossible in let g = resolve_instances_and_generalize nctx altacc in - let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e)) + let altacc' = g (fun _ne vname t _l e + -> mkArrow (sinfo_location altacc, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1121,7 +1122,7 @@ and lexp_parse_inductive ctors ctx = (* Convert the Lexp back into a list of fields. *) let rec loop e = match lexp_lexp' e with - | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) + | Arrow (_, ak, n, t, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' | (kind, var, exp)::tl @@ -1189,15 +1190,15 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - let value = EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) + let value = EV.eval_call (sexp_location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal loc v "Macro `%s` should return an IO sexp" + | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO sexp" (lexp_string macro_funct)) - | v -> value_fatal loc v "Macro `%s` should return an IO" + | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO" (lexp_string macro_funct) @@ -1222,7 +1223,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* Preserve the new operators added to nctx. *) let (declmap) = List.fold_right - (fun ((l, vname), sexp) (map) -> + (fun ((_l, vname), sexp) (map) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with @@ -1236,7 +1237,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) * proper format, e.g. for `lctx_view`! *) let e = check sexp adjusted_t nctx in (* let d = (v', LetDef (i + 1, e), t) in *) - (IMap.add i ((l, Some vname), e, t) map) + (IMap.add i ((sexp, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1273,13 +1274,13 @@ and infer_and_generalize_type (ctx : elab_context) se name = *) let rec strip_rettype t = match lexp_lexp' t with - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, t1, l, strip_rettype t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, t1, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) + -> mkArrow (Symbol(l,""), Aerasable, name, t, e)) t and infer_and_generalize_def (ctx : elab_context) se = @@ -1288,8 +1289,8 @@ and infer_and_generalize_def (ctx : elab_context) se = let g = resolve_instances_and_generalize nctx e in let e' = g wrapLambda e in let t' = g (fun ne name t _l e - -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, sexp_location se, e)) + -> mkArrow (se, (if ne then Aimplicit else Aerasable), + name, t, e)) t in (e', t') @@ -1333,7 +1334,7 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + -> let ltp = infer_and_generalize_type nctx stp (Symbol(loc, ""), Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1354,7 +1355,7 @@ and lexp_decls_1 pending_defs then (error ~loc {|Variable "%s" already defined!|} vname; recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + else recur [] (ectx_extend nctx (Symbol(loc, ""), Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ @@ -1366,13 +1367,13 @@ and lexp_decls_1 | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol ((l, vname)); sexp] + | [Symbol ((_l, vname)); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in + let var = (sexp, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, @@ -1418,7 +1419,7 @@ and lexp_decls_1 else if (OL.conv_p lctx t (BI.get_predef "Macro" nctx)) then (* expand macro and get the generated declarations *) let lxp, _ltp = infer sxp nctx in - let sdecl' = lexp_expand_macro (sexp_location sxp) lxp sargs nctx None in + let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( error ~loc:(sexp_location sxp) "Invalid declaration syntax"; @@ -1465,9 +1466,9 @@ and sform_declexpr ctx loc sargs _ot = | [e] when is_var e -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; + | None -> error ~loc:(sexp_location loc) "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; + | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1475,7 +1476,7 @@ let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc "decltype expects one argument"; + | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; sform_dummy_ret ctx loc @@ -1492,18 +1493,18 @@ 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 + let bi = mkBuiltin ((sexp_location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc {|Unknown built-in "%s"|} name; + sexp_error (sexp_location 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!"; + | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error ~loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error ~loc "Use of `Built-in` in user code"; + | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs _ot = @@ -1512,9 +1513,9 @@ let sform_datacons ctx loc sargs _ot = -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy) - | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; + | [_;_] -> sexp_error (sexp_location loc) "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc - | _ -> sexp_error loc "##constr requires two arguments"; + | _ -> sexp_error (sexp_location loc) "##constr requires two arguments"; sform_dummy_ret ctx loc let elab_colon_to_ak k = match k with @@ -1525,22 +1526,22 @@ let elab_colon_to_ak k = match k with let elab_datacons_arg s = match s with | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t]) -> (elab_colon_to_ak k, elab_p_id s, t) - | _ -> (Anormal, (sexp_location s, None), s) + | _ -> (Anormal, (s, None), s) let elab_typecons_arg arg : (arg_kind * vname * sexp option) = match arg with - | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e]) + | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (_l,name); e]) -> (elab_colon_to_ak k, - (l, Some name), Some e) - | Symbol (l, name) -> (Anormal, (l, Some name), None) + (arg, Some name), Some e) + | Symbol (_l, name) -> (Anormal, (arg, Some name), None) | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) (sexp_location arg) "Unrecognized formal arg"; - (Anormal, (sexp_location arg, None), None) + (Anormal, (arg, None), None) let sform_typecons ctx loc sargs _ot = match sargs with - | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) + | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) @@ -1589,7 +1590,7 @@ let sform_hastype ctx loc sargs _ot = | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) - | _ -> sexp_error loc "##_:_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_:_ takes two arguments"; sform_dummy_ret ctx loc let sform_arrow kind ctx loc sargs _ot = @@ -1597,12 +1598,12 @@ let sform_arrow kind ctx loc sargs _ot = | [st1; st2] -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) - | _ -> ((sexp_location st1, None), st1) in + | _ -> ((st1, None), st1) in let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type st2 nctx (sexp_location st2, None) in - (mkArrow (kind, v, lt1, loc, lt2), Lazy) - | _ -> sexp_error loc "##_->_ takes two arguments"; + let lt2 = infer_type st2 nctx (st2, None) in + (mkArrow (loc, kind, v, lt1, lt2), Lazy) + | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc let sform_immediate ctx loc sargs ot = @@ -1616,10 +1617,10 @@ let sform_immediate ctx loc sargs ot = let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot | [_se] - -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); + -> (sexp_error (sexp_location loc) ("Non-immediate passed to ##typer-immediate"); sform_dummy_ret ctx loc) | _ - -> (sexp_error loc ("Too many args to ##typer-immediate"); + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-immediate"); sform_dummy_ret ctx loc) @@ -1639,7 +1640,7 @@ let sform_identifier ctx loc sargs ot = (sexp_error l {|Invalid special identifier "%s"|} name; sform_dummy_ret ctx loc) - | [Symbol (loc, name)] + | [Symbol (_loc, name)] when String.length name >= 1 && String.get name 0 = '?' -> let name = if name = "?" then "" else string_sub name 1 (String.length name) in @@ -1663,13 +1664,13 @@ let sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc ("Bug in the elaboration of a metavar" + fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" ^^ " repeated at a different scope level!") | MVal _ -> (* FIXME: We face the same problem as above, but here, the situation is worse, we don't even know the scope level! *) - fatal ~loc "Bug in the elaboration of a repeated metavar!" + fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -1681,19 +1682,20 @@ let sform_identifier ctx loc sargs ot = let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) - | [Symbol id] -> elab_varref ctx id + | [Symbol (_n, name)] + -> elab_varref ctx (loc, name) | [_se] - -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); + -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); sform_dummy_ret ctx loc) | _ - -> (sexp_error loc ("Too many args to ##typer-identifier"); + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); sform_dummy_ret ctx loc) let rec sform_lambda kind ctx loc sargs ot = @@ -1704,7 +1706,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Symbol arg -> (elab_p_id arg, None) | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; - ((dummy_location, None), None) in + ((dsinfo, None), None) in let olt1 = match ost1 with | Some st -> Some (infer_type st ctx arg) @@ -1722,7 +1724,7 @@ let rec sform_lambda kind ctx loc sargs ot = let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (loc, kind, arg, lt1, lt2)) | _ -> alt) in (match ot with @@ -1735,7 +1737,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Some t -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in match lexp_lexp' lp with - | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + | Arrow (_, ak2, _, lt1, lt2) when ak2 = kind -> (match olt1 with | None -> () | Some lt1' @@ -1743,7 +1745,7 @@ let rec sform_lambda kind ctx loc sargs ot = ~lxp_name:"parameter" lt1 lt1'); mklam lt1 (Some lt2) - | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal + | Arrow (_, ak2, v, lt1, lt2) when kind = Anormal (* `t` is an implicit arrow and `kind` is Anormal, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) @@ -1756,7 +1758,7 @@ let rec sform_lambda kind ctx loc sargs ot = let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in (mkLambda (ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) + | Inferred lt2' -> Inferred (mkArrow (loc, ak2, v, lt1, lt2')) | _ -> alt) | _lt @@ -1765,7 +1767,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> sexp_error - loc "##lambda_%s_ takes two arguments" + (sexp_location loc) "##lambda_%s_ takes two arguments" (match kind with | Anormal -> "->" | Aimplicit -> "=>" @@ -1779,7 +1781,7 @@ let rec sform_case ctx loc sargs ot = match sargs with -> (pexp_p_pat pat, code) | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; - (Ppatsym (l, None), Symbol (l, "?")) in + (Ppatsym (se, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in let t = match ot with | Some t -> t @@ -1788,8 +1790,8 @@ let rec sform_case ctx loc sargs ot = match sargs with (le, match ot with Some _ -> Checked | None -> Inferred t) (* In case there are no branches, pretend there was a | anyway. *) - | [_e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot - | _ -> sexp_error loc "Unrecognized case expression"; + | [_e] -> sform_case ctx loc [Node (Symbol (sexp_location loc, "_|_"), sargs)] ot + | _ -> sexp_error (sexp_location loc) "Unrecognized case expression"; sform_dummy_ret ctx loc let sform_letin ctx loc sargs ot = match sargs with @@ -1805,7 +1807,7 @@ let sform_letin ctx loc sargs ot = match sargs with | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) - | _ -> sexp_error loc "Unrecognized let_in_ expression"; + | _ -> sexp_error (sexp_location loc) "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc let sform_proj ctx loc sargs _ = @@ -1815,9 +1817,9 @@ let sform_proj ctx loc sargs _ = let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | [_;_] - -> sexp_error loc "Second argument is not a Symbol!"; + -> sexp_error (sexp_location loc) "Second argument is not a Symbol!"; sform_dummy_ret ctx loc - | _ -> sexp_error loc "Wrong arg number!"; + | _ -> sexp_error (sexp_location loc) "Wrong arg number!"; sform_dummy_ret ctx loc let rec infer_level ctx se : lexp = @@ -1830,7 +1832,7 @@ let rec infer_level ctx se : lexp = -> 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: %s" (sexp_string se); - newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) l) + newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) se) (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1843,7 +1845,7 @@ let sform_type ctx loc sargs _ot = | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) - | _ -> (sexp_error loc "##Type_ expects one argument"; + | _ -> (sexp_error (sexp_location loc) "##Type_ expects one argument"; sform_dummy_ret ctx loc) let sform_debruijn ctx loc sargs _ot = @@ -1854,7 +1856,7 @@ let sform_debruijn ctx loc sargs _ot = sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) - | _ -> (sexp_error loc "##DeBruijn expects one integer argument"; + | _ -> (sexp_error (sexp_location loc) "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc) (* Only print var info *) @@ -1890,7 +1892,7 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc {|Could not load "%s": file not found.|} file_name; [] + -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx @@ -1902,7 +1904,7 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc "argument to load should be one file name (String)"; + | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; !sform_default_ectx) in (* get lexp_context *) @@ -1993,7 +1995,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) in + let v = mkVar ((dsinfo, Some name), idx) in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -2002,7 +2004,7 @@ let default_ectx let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, Some key) e t) + else ctx_define ctx (dsinfo, Some key) e t) (!BI.lmap) lctx in Heap.register_builtins (); ===================================== src/elexp.ml ===================================== @@ -36,8 +36,8 @@ open Sexp (* Sexp type *) module U = Util module L = Lexp -type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type label = symbol module SMap = U.SMap @@ -84,11 +84,11 @@ type elexp = let rec elexp_location e = match e with | Imm s -> sexp_location s - | Var ((l,_), _) -> l + | Var ((l,_), _) -> sexp_location l | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l - | Lambda ((l,_),_) -> l + | Lambda ((l,_),_) -> sexp_location l | Call (f,_) -> elexp_location f | Cons (_, (l, _)) -> l | Case (l,_,_,_) -> l ===================================== src/eval.ml ===================================== @@ -495,7 +495,7 @@ and eval_var ctx lxp v = with | _e -> Log.log_fatal - ~loc + ~loc:(sexp_location loc) "Variable: %s%d was not found\n%s" (L.maybename name) idx (trace_elexp lxp) @@ -558,7 +558,7 @@ and eval_call loc unef i f args = (* 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))])) + -> Vtype (L.mkCall (dsinfo, e, [(Anormal, mkVar (vdummy, -1))])) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) and eval_case ctx i loc target pat dflt = @@ -629,7 +629,7 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let trace_dum = (Var ((loc, None), -1)) in + let trace_dum = (Var ((Symbol(loc, ""), None), -1)) in let eval_call a b = eval_call loc trace_dum depth a b in let sxp, nd, sym, str, it, flt, blk = match args with | [sxp; nd; sym; str; it; flt; blk] -> @@ -717,7 +717,7 @@ and print_eval_trace trace = print_trace " EVAL TRACE " trace a let io_bind loc depth args_val = - let trace_dum = (Var ((loc, None), -1)) in + let trace_dum = (Var ((Symbol(loc, ""), None), -1)) in match args_val with | [Vcommand cmd; callback] @@ -755,8 +755,8 @@ let sys_exit loc _depth args_val = match args_val with let y_operator loc _depth args = match args with | [f] -> let yf_ref = ref Vundefined in - let fname = (dloc, Some "f") in - let yfname = (dloc, Some "yf") in + let fname = (dsinfo, Some "f") in + let yfname = (dsinfo, Some "yf") in let yf = Closure(vdummy, Call (Var (fname, 1), [Var (yfname, 2); @@ -808,7 +808,7 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -822,7 +822,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -843,7 +843,7 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some t), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -861,7 +861,7 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -882,7 +882,7 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx)) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i ===================================== src/instargs.ml ===================================== @@ -25,6 +25,7 @@ module U = Util module Unif = Unification open Printf +open Sexp (** If true, log all the matching instances when resolving. *) let debug_list_all_candidates = ref false @@ -40,10 +41,10 @@ let recursion_limit = ref (Some 100) let log_skipped_uncertain_matches = ref (Some Log.Warning) let metavar_resolution_contexts = - ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) + ref (U.IMap.empty : (DB.elab_context * sinfo) U.IMap.t) let lookup_metavar_resolution_ctxt (id : L.meta_id) - : (DB.elab_context * U.location) option + : (DB.elab_context * sinfo) option = U.IMap.find_opt id (!metavar_resolution_contexts) let save_metavar_resolution_ctxt (id : L.meta_id) ctx loc : unit @@ -79,7 +80,7 @@ let in_typeclass_set (ectx : DB.elab_context) (t : L.ltype) : bool = let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = let whnft = OL.lexp_whnf t lctx in match L.lexp_lexp' whnft with - | L.Call (head, _) -> head + | L.Call (_, head, _) -> head | _ -> whnft (** A type is a type class if its head is in the set of type class @@ -112,8 +113,8 @@ let try_match t1 t2 lctx sl = | _ -> Possible let search_instance (instantiate_implicit) (ctx : DB.elab_context) - (loc : U.location) (t : L.ltype) : L.lexp option = - Log.log_debug ~loc "Resolving type `%s`" (L.lexp_string t); + (loc : sinfo) (t : L.ltype) : L.lexp option = + Log.log_debug ~loc:(sexp_location loc) "Resolving type `%s`" (L.lexp_string t); let lctx = DB.ectx_to_lctx ctx in let (_, _, insts) = DB.ectx_to_tcctx ctx in @@ -133,7 +134,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) let var = L.mkVar ((loc,namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc + Log.log_debug ~loc:(sexp_location loc) "Considering potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t); (* All candidates should have a type that is a typeclass. *) @@ -149,7 +150,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | Possible -> (match !log_skipped_uncertain_matches with | Some level -> - Log.log_msg ignore level ~loc + Log.log_msg ignore level ~loc:(sexp_location loc) "Skipping potential instance `%s : %s` while resolving for `%s`" (L.lexp_string var) (L.lexp_string t') (L.lexp_string t) @@ -178,7 +179,7 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc + Log.log_debug ~loc:(sexp_location loc) "Found instance for `%s` at index %i: `%s : %s`" (L.lexp_string t) i (L.lexp_string (L.mkVar (vname, i))) (L.lexp_string t'); @@ -199,12 +200,12 @@ let resolve_instances instantiate_implicit e = | MVar _ -> true | _ -> false in if uninstantiated && is_typeclass ctx t then - (match search_instance instantiate_implicit ctx loc t with + (match search_instance instantiate_implicit ctx (loc) t with | Some e -> Unif.associate i e; true | None -> (* The metavar will be generalized, unified, or will remain and cause an error. *) - Log.log_info ~loc "No instance found for type `%s`" + Log.log_info ~loc:(sexp_location loc) "No instance found for type `%s`" (L.lexp_string t); false ) else false ===================================== src/inverse_subst.ml ===================================== @@ -53,6 +53,8 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an type substIR = ((int * int) list * int * int) +let dsinfo = Sexp.dummy_sinfo + (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) @@ -94,7 +96,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) + mkVar ((dsinfo, None), idx) (** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -275,13 +277,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = :: ndefs)) (s, []) defs in mkLet (l, ndefs, apply_inv_subst e s') - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s, l, + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, apply_inv_subst t1 s, apply_inv_subst t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) - | Call (f, args) - -> mkCall (apply_inv_subst f s, + | Call (l, f, args) + -> mkCall (l, apply_inv_subst f s, L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs) ===================================== src/lexp.ml ===================================== @@ -33,9 +33,10 @@ open Grammar (* open Unify *) module S = Subst -type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type meta_id = int (* Identifier of a meta variable. *) +type sinfo = sexp type label = symbol @@ -63,23 +64,23 @@ type ltype = lexp and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level - | Sort of U.location * sort + | Sort of sinfo * sort | Builtin of symbol * ltype | Var of vref - | Proj of U.location * lexp * label + | Proj of sinfo * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype + | Let of sinfo * (vname * lexp * ltype) list * lexp + | Arrow of sinfo * arg_kind * vname * ltype * ltype | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label + | Call of sinfo * lexp * (arg_kind * lexp) list (* Curried call. *) + | Inductive of sinfo * label * ((arg_kind * vname * ltype) list) (* formal Args *) * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp + | Case of sinfo * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (sinfo * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) (* The `subst` will be applied to the the metavar's value when it * gets instantiated. *) @@ -164,6 +165,8 @@ let dummy_scope_level = 0 let builtin_size = ref 0 +let dummy_sinfo = Sexp.dummy_sinfo + let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) @@ -209,11 +212,11 @@ let lexp'_hash (lp : lexp') = (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) - | Arrow (k, v, t1, l, t2) + | Arrow (l, k, v, t1, t2) -> U.combine_hash 7 (U.combine_hash - (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (U.combine_hash (lexp_hash t1) - (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash k)) + (U.combine_hash (Hashtbl.hash v) + (U.combine_hash (lexp_hash t1) (lexp_hash t2)))) | Lambda (k, v, t, e) -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) @@ -239,7 +242,7 @@ let lexp'_hash (lp : lexp') = | Metavar (id, s, v) -> U.combine_hash 12 (U.combine_hash id (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) - | Call (e, args) + | Call (_, e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) @@ -272,11 +275,11 @@ let hc_eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> e1 == e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && t11 == t12 && t21 == t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && t1 == t2 && e1 == e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) @@ -316,17 +319,17 @@ let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkArrow (l, k, v, t1, t2) = hc (Arrow (l, k, v, t1, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) = +let mkCall (l, f, es) = match lexp_lexp' f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | Call (l, f', es'), _ -> hc (Call (l, f', es' @ es)) | _, [] -> f - | _ -> hc (Call (f, es)) + | _ -> hc (Call (l, f, es)) let impossible = mkImm Sexp.dummy_epsilon @@ -513,33 +516,37 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) * S.sink (fun l i -> mkVar (l, i)) l s *) -let rec lexp_location e = - match lexp_lexp' e with +let rec sinfo_location s = + match lexp_lexp' s with | Sort (l,_) -> l - | SortLevel (SLsucc e) -> lexp_location e - | SortLevel (SLlub (e, _)) -> lexp_location e - | SortLevel SLz -> U.dummy_location - | Imm s -> sexp_location s + | SortLevel (SLsucc s) -> sinfo_location s + | SortLevel (SLlub (s, _)) -> sinfo_location s + | SortLevel SLz -> dummy_sinfo + | Imm s -> s | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> l + | Builtin ((l, _), _) -> Symbol (l, "") | Let (l,_,_) -> l - | Arrow (_,_,_,l,_) -> l + | Arrow (l,_,_,_,_) -> l | Lambda (_,(l,_),_,_) -> l - | Call (f,_) -> lexp_location f + | Call (_,f,_) -> sinfo_location f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> l + | Cons (_,(l,_)) -> Symbol (l, "") | Case (l,_,_,_,_) -> l - | Susp (e, _) -> lexp_location e + | Susp (s, _) -> sinfo_location s (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l | Proj (l,_,_) -> l +let lexp_location e = + sexp_location (sinfo_location e) + + (********* Normalizing a term *********) -let vdummy = (U.dummy_location, None) +let vdummy = (dummy_sinfo, None) let maybename n = match n with None -> "<anon>" | Some v -> v -let sname (l,n) = (l, maybename n) +let sname (l,n) = (sexp_location l, maybename n) let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -559,10 +566,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) | (v, def, ty) :: defs -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in mkLet (l, loop s defs, mkSusp e s') - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s)) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, mkSusp t1 s, mkSusp t2 (ssink v s)) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) - | Call (f, args) -> mkCall (mkSusp f s, + | Call (l, f, args) -> mkCall (l,mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -627,10 +634,10 @@ let clean e = (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in mkLet (l, ndefs, clean s' e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, clean s t1, clean (ssink v s) t2) | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) - | Call (f, args) -> mkCall (clean s f, + | Call (l, f, args) -> mkCall (l, clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -681,9 +688,9 @@ let rec lexp_unparse lxp = | Imm (sexp) -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) - | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) | Proj (l,lxp,(loc,str) ) - -> Node (Symbol (l, "__.__"), + -> Node (Symbol (sexp_location l, "__.__"), [(lexp_unparse lxp);(Symbol (loc,str))]) | Cons (t, (l, name)) -> Node (sdatacons, @@ -697,14 +704,14 @@ let rec lexp_unparse lxp = | Aerasable -> "lambda_≡>_"), [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body]) - | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) + | Arrow (loc, arg_kind, (l,oname), ltp1, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Anormal -> "_->_" + Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), - [Symbol (l,v); ut1])); + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); lexp_unparse ltp2]) | Let (loc, ldecls, body) @@ -717,11 +724,11 @@ let rec lexp_unparse lxp = [Symbol (sname vdef); lexp_unparse lxp]) :: acc) [] ldecls in - Node (Symbol (loc, "let_in_"), + Node (Symbol (sexp_location loc, "let_in_"), [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body]) - | Call(lxp, largs) -> (* (arg_kind * lexp) list *) + | Call(_, lxp, largs) -> (* (arg_kind * lexp) list *) let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs) @@ -735,7 +742,7 @@ let rec lexp_unparse lxp = Node (Symbol label, List.map pexp_u_formal_arg pfargs) :: List.map (fun (name, types) - -> Node (Symbol (loc, name), + -> Node (Symbol (sexp_location loc, name), List.map (fun arg -> match arg with @@ -759,13 +766,13 @@ let rec lexp_unparse lxp = let pat_args = List.map (fun (_kind, ((l,oname) as name)) -> match oname with - | Some vdef -> (Some (l,vdef), name) + | Some vdef -> (Some (sexp_location l,vdef), name) | None -> (None, name)) args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in (Ppatcons (Node (sdatacons, - [bt; Symbol (loc, str)]), + [bt; Symbol (sexp_location loc, str)]), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -775,16 +782,16 @@ let rec lexp_unparse lxp = lexp_unparse dft)::pbranch | None -> pbranch in let e = lexp_unparse target in - Node (Symbol (loc, "case_"), + Node (Symbol (sexp_location loc, "case_"), e :: List.map (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), + Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), [pexp_u_pat pat; branch])) pbranch) (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) - -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx + -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]") | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") @@ -794,8 +801,8 @@ let rec lexp_unparse lxp = | SortLevel (SLlub (l1, l2)) -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), [lexp_unparse l1; lexp_unparse l2]) - | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") + | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -904,10 +911,10 @@ let rec get_precedence expr ctx = | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" - | Arrow (Anormal, _, _, _, _) -> lkp "->" - | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" - | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" - | Call (exp, _) -> get_precedence exp ctx + | Arrow (_, Anormal, _, _, _) -> lkp "->" + | Arrow (_, Aimplicit, _, _, _) -> lkp "=>" + | Arrow (_, Aerasable, _, _, _) -> lkp "≡>" + | Call (_, exp, _) -> get_precedence exp ctx | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> @@ -1015,11 +1022,11 @@ and lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) - | Arrow(k, (_, Some name), tp, _loc, expr) -> + | Arrow(_loc, k, (_, Some name), tp, expr) -> "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str' expr) - | Arrow(k, (_, None), tp, _loc, expr) -> + | Arrow(_loc, k, (_, None), tp, expr) -> "(" ^ (lexp_str' tp) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" @@ -1032,7 +1039,7 @@ and lexp_str ctx (exp : lexp) : string = | Cons(t, (_, ctor_name)) -> (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name - | Call(fname, args) -> + | Call(_, fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in @@ -1156,11 +1163,11 @@ let rec eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && eq t11 t12 && eq t21 t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) -> ak1 = ak2 && eq t1 t2 && eq e1 e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) ===================================== src/opslexp.ml ===================================== @@ -51,6 +51,9 @@ type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t let error ~location fmt = Log.log_fatal ~section:"OPSLEXP" ~loc:location fmt +let dloc = DB.dloc +let dsinfo = DB.dsinfo + module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but * I haven't found any such functionality in OCaml's libs. *) @@ -127,7 +130,7 @@ let rec lctx_to_subst lctx = L.ssink v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in - let s2 = lexp_defs_subst DB.dloc S.identity + let s2 = lexp_defs_subst dsinfo S.identity (List.rev defs) in L.scompose s2 s1 @@ -177,17 +180,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = * things like full normalization (e.g. lexp_conv_p). *) | Some e' -> lexp_whnf e' ctx) | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - | Call (e, []) -> lexp_whnf e ctx - | Call (f, (((_, arg)::args) as xs)) -> + | Call (_, e, []) -> lexp_whnf e ctx + | Call (l, f, (((_, arg)::args) as xs)) -> (match lexp'_whnf f ctx with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) @@ -200,7 +203,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, + mkCall (l, DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; L.Aerasable, e]) in @@ -230,12 +233,12 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:l + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] - | Call (f, aargs) -> + | Call (_, f, aargs) -> (match lexp'_whnf f ctx with | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) @@ -243,7 +246,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = | Proj (loc, lxp, (_loc, label)) -> let c, args = match lexp'_whnf lxp ctx with - | Call (f, args) -> f, args + | Call (_loc, f, args) -> f, args | _ -> lxp, [] in (match lexp'_whnf c ctx with | Cons (it, _) -> @@ -256,17 +259,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc + | _ , [] -> Log.log_error ~loc:(sexp_location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc + Log.log_fatal ~loc:(sexp_location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc "Proj on a non-tuple in WHNF!"; e) + | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *) | Metavar (idx, s, _) @@ -288,7 +291,7 @@ and eq_cast_whnf ctx args = match args with | [_l; _t; _x; _y; (_, p); _f; (_, fx)] -> (match lexp'_whnf p ctx with - | Call (refl, _) when conv_p ctx refl DB.eq_refl + | Call (_, refl, _) when conv_p ctx refl DB.eq_refl -> Some (lexp_whnf fx ctx) | _ -> None) | _ -> None @@ -378,7 +381,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _ -> false) | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 - | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, _vd2, t21, _, t22)) + | (Arrow (_, ak1, vd1, t11, t12), Arrow (_, ak2, _vd2, t21, t22)) -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') @@ -388,7 +391,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs') e1 e2 - | (Call (f1, args1), Call (f2, args2)) + | (Call (_, f1, args1), Call (_, f2, args2)) -> let conv_arglist_p args1 args2 : bool = List.fold_left2 (fun eqp (ak1,t1) (ak2,t2) @@ -441,7 +444,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) let fargs, ctors = @@ -456,12 +459,12 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tlxp = mkSusp target subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (dsinfo, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) (L.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + DB.lexp_ctx_cons ctx (dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types from the inductive. Instead, we work with the lists of @@ -492,9 +495,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), + let ctor = mkSusp (mkCall (dsinfo, mkCons (it, (DB.dloc, l1)), eaargs)) subst in - let hlxp = mkCall (ctor, args) in + let hlxp = mkCall (dsinfo, ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 ) (SMap.bindings cases1) (SMap.bindings cases2) @@ -505,7 +508,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in - let hlxp = mkVar ((DB.dloc, None), 0) in + let hlxp = mkVar ((dsinfo, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' 2) e1 e2 | None, None -> true @@ -661,7 +664,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -687,14 +690,14 @@ 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, loc, t2) + | Arrow (loc, ak, v, t1, 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 loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; @@ -704,18 +707,18 @@ and check'' erased ctx e = 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, + mkArrow (l, ak, v, t, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) e)) - | Call (f, args) + | Call (_, f, args) -> let ft = check erased ctx f in 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) + | Arrow (_l, ak', _v, t1, t2) -> if ak != ak' then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; assert_type ctx arg at t1; @@ -778,7 +781,7 @@ and check'' erased ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, + mkArrow (sinfo_location t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -787,7 +790,7 @@ and check'' erased ctx e = | Proj (l, e, (loc, label)) -> ( let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in @@ -799,20 +802,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:l + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasable field: %s" + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -824,16 +827,16 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:l + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in (* FIXME save the type in the case lexp instead of recomputing @@ -854,14 +857,14 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:l "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (l, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) @@ -882,13 +885,13 @@ and check'' erased ctx e = -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) + (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:l "Wrong number of args to constructor!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, (l, name)), + mkCall (l, mkCons (it, (sexp_location l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -902,7 +905,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:l "Redundant default clause"; + then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -915,8 +918,8 @@ and check'' erased ctx e = -> 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!"); + ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -931,21 +934,21 @@ and check'' erased ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), + mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (sinfo_location ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with | Not_found - -> log_tc_error ~loc:l {|Constructor "%s" does not exist|} name; + -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; DB.type_int) | _ -> log_tc_error ~loc:(lexp_location e) @@ -1020,9 +1023,9 @@ and fv (e : lexp) : (DB.set * mv_set) = o - 1)) (fv e, len) defs in fv_hoist len fvs - | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) + | Arrow (_, _, _, t1, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) - | Call (f, args) + | Call (_, f, args) -> List.fold_left (fun fvs (ak, arg) -> let afvs = fv arg in fv_union fvs @@ -1102,7 +1105,7 @@ and get_type ctx e = let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (get_type ctx e) ctx in let it, aargs = call_split etype in @@ -1114,21 +1117,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:l + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1140,16 +1143,16 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:l + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, l, t2) + | Arrow (l, ak, v, t1, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -1158,15 +1161,15 @@ and get_type ctx e = | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) - -> (mkArrow (ak, v, t, l, + -> (mkArrow (l, ak, v, t, get_type (DB.lctx_extend ctx v Variable t) e)) - | Call (f, args) + | Call (_l, f, args) -> let ft = get_type ctx f in List.fold_left (fun ft (_ak,arg) -> match lexp'_whnf ft ctx with - | Arrow (_ak', _v, _t1, _l, t2) + | Arrow (_l, _ak', _v, _t1, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args @@ -1204,14 +1207,14 @@ and get_type ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, + -> mkArrow (sinfo_location t, ak, v, t, arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with - | Inductive (_l, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -1222,16 +1225,16 @@ and get_type ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), + mkCall (l, mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (sinfo_location ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with Not_found -> DB.type_int) @@ -1280,7 +1283,7 @@ let arity_of_cons let pos_of_label lctx label e : int = let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in let it, aargs = call_split (lexp_whnf e lctx) in @@ -1322,7 +1325,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Var (v) -> E.Var (v) | L.Proj (l, exp, label) -> let t = get_type lctx exp in - E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) + E.Proj (sexp_location l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) @@ -1334,15 +1337,15 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - E.Let (l, edecls, erase_type lctx' body) + E.Let (sexp_location l, edecls, erase_type lctx' body) - | L.Call (fct, args) + | L.Call (_, fct, 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 let ebranches = clean_branch_map lctx branches in - E.Case (location, etarget, ebranches, clean_default lctx default) + E.Case (sexp_location location, etarget, ebranches, clean_default lctx default) | L.Susp (l, s) -> erase_type lctx (L.push_susp l s) @@ -1391,7 +1394,7 @@ and clean_branch_map lctx cases = in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (l, eargs, erase_type lctx' (L.push_susp expr subst)) + (sexp_location l, eargs, erase_type lctx' (L.push_susp expr subst)) in SMap.map clean_branch cases @@ -1404,7 +1407,7 @@ let erase_type lctx lxp = Log.log_fatal ~print_action:(fun () -> IMap.iter (fun i (_, t, _, (l, n)) -> - print_endline ("\t" ^ (Source.Location.to_string l) + print_endline ("\t" ^ (Source.Location.to_string (sexp_location l)) ^ " ?" ^ (Option.value ~default:"" n) ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) ) mvs) @@ -1434,17 +1437,17 @@ let ctx2tup ctx nctx = | DB.CVfix (_, nctx) as bloc -> get_blocs nctx (bloc :: blocs) | _ -> assert false in let rec mk_lets_and_tup blocs types = - let loc = U.dummy_location in + let loc = dsinfo in match blocs with | [] -> let cons_name = "cons" in - let cons_label = (loc, cons_name) in - let type_label = (loc, "record") in + let cons_label = (sexp_location loc, cons_name) in + let type_label = (sexp_location loc, "record") in let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) - mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (dsinfo, mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, ===================================== src/pexp.ml ===================================== @@ -20,7 +20,9 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) -open Util +(* +*open Util +*) open Sexp (* Symbol *) let pexp_error loc = Log.log_error ~section:"PEXP" ~loc @@ -43,7 +45,7 @@ type ppat = let pexp_pat_location e = match e with | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> sexp_location e + | Ppatcons (e, _) -> e let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with @@ -56,28 +58,28 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | None -> Symbol (l, "_")]) let pexp_p_pat_arg (s : sexp) = match s with - | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) - -> (Some f, (l, Some n)) + | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) + | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) + -> (Some f, (s, Some n)) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; - (None, (loc, None)) + (None, (s, None)) let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l,_) as n) -> Node (Symbol (l, "_:=_"), [Symbol n; pname]) let pexp_p_pat (s : sexp) : ppat = match s with - | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) + | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatsym (l, None) + pexp_error l "Unknown pattern"; Ppatsym (s, None) let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (l, "_") - | Ppatsym (l, Some n) -> Symbol (l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args) ===================================== src/positivity.ml ===================================== @@ -69,7 +69,7 @@ let rec positive (index : db_index) (lexp : lexp) : bool = and positive' index lexp = match Lexp.lexp_lexp' lexp with - | Lexp.Arrow (_, _, tau, _, e) + | Lexp.Arrow (_, _, _, tau, e) (* * x ⊢ e pos x ∉ fv(τ) * ────────────────────── @@ -77,7 +77,7 @@ and positive' index lexp = *) -> absent index tau && positive' (index + 1) e - | Lexp.Call (f, args) + | Lexp.Call (_, f, args) (* * x ∉ fv(e⃗) * ────────────── ===================================== src/sexp.ml ===================================== @@ -38,10 +38,15 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Float of location * float | Node of sexp * sexp list type token = sexp +type sinfo = sexp let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location +let dummy_sinfo = epsilon dummy_location + +type vname = sinfo * string option +type vref = vname * db_index (********************** Sexp tests **********************) let pred_symbol s pred = ===================================== src/unification.ml ===================================== @@ -40,6 +40,9 @@ let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int) let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) = create_metavar_1 sl t (Myers.length ctx) +let dloc = DB.dloc +let dsinfo = DB.dsinfo + (* For convenience *) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) @@ -78,9 +81,9 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs - | Arrow (_, _, t1, _, t2) -> oi t1 || oi t2 + | Arrow (_, _, _, t1, t2) -> oi t1 || oi t2 | Lambda (_, _, t, e) -> oi t || oi e - | Call (f, args) + | Call (_, f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args | Inductive (_, _, args, cases) -> SMap.fold @@ -143,7 +146,7 @@ let common_subset ctx s1 s2 = && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), + | s' -> S.Cons (mkVar ((sinfo_location le1, None), 0), s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that @@ -151,11 +154,11 @@ let common_subset ctx s1 s2 = * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop s1 (S.Cons (mkVar ((dsinfo, None), 0), S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop (S.Cons (mkVar ((dsinfo, None), 0), S.Identity 1, o1')) s2 o1 o2 o | (S.Identity o1', S.Identity o2') @@ -282,8 +285,8 @@ and unify' (e1: lexp) (e2: lexp) and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' arrow, lexp_lexp' lxp) with - | (Arrow (var_kind1, v1, ltype1, _, lexp1), - Arrow (var_kind2, _, ltype2, _, lexp2)) + | (Arrow (_, var_kind1, v1, ltype1, lexp1), + Arrow (_, var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 (srename v1 lexp2) @@ -445,7 +448,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' call, lexp_lexp' lxp) with - | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) + | (Call (_, lxp_left, lxp_list1), Call (_, lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> (try List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then @@ -457,10 +460,10 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs -> [(CKresidual, ctx, call, lxp)]) | (call', lxp') -> let head_left = match call' with - | Call (head_left, _) -> head_left + | Call (_, head_left, _) -> head_left | _ -> call in let head_right = match lxp' with - | Call (head_right, _) -> head_right + | Call (_, head_right, _) -> head_right | _ -> lxp in let for_sure_irreducible_call_head ctx head = match OL.lexp'_whnf head ctx with ===================================== src/util.ml ===================================== @@ -33,11 +33,9 @@ let dummy_location = Source.Location.dummy (* Occurrence of a variable's symbol: we use DeBruijn index, and for * debugging purposes, we remember the name that was used in the source * code. *) -type vname = location * string option type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vname * db_index type bottom = | B_o_t_t_o_m_ of bottom ===================================== tests/env_test.ml ===================================== @@ -30,6 +30,7 @@ open Typerlib open Utest_lib open Env +let dsinfo = DB.dsinfo let rctx = Elab.default_rctx @@ -41,11 +42,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> if 10 <= (!global_verbose_lvl) then ( let var = [ - ((dloc, Some "a"), DB.type_int, (make_val "a")); - ((dloc, Some "b"), DB.type_int, (make_val "b")); - ((dloc, Some "c"), DB.type_int, (make_val "c")); - ((dloc, Some "d"), DB.type_int, (make_val "d")); - ((dloc, Some "e"), DB.type_int, (make_val "e")); + ((dsinfo, Some "a"), DB.type_int, (make_val "a")); + ((dsinfo, Some "b"), DB.type_int, (make_val "b")); + ((dsinfo, Some "c"), DB.type_int, (make_val "c")); + ((dsinfo, Some "d"), DB.type_int, (make_val "d")); + ((dsinfo, Some "e"), DB.type_int, (make_val "e")); ] in let n = (List.length var) - 1 in ===================================== tests/instargs_test.ml ===================================== @@ -34,10 +34,10 @@ let add_test = add_test "INSTARGS" let default_ectx = E.default_ectx let default_rctx = E.default_rctx -let dummy_vname = Util.dummy_location, None +let dummy_vname = DB.dsinfo, None let make_metavar t ctx = - E.newInstanceMetavar ctx (Util.dummy_location, Some "inst") t + E.newInstanceMetavar ctx (DB.dsinfo, Some "inst") t let lexp_from_str str ctx = List.hd (E.lexp_expr_str str ctx) @@ -171,7 +171,7 @@ let to_nat n ctx = let s = lexp_from_str "S" ctx in let z = lexp_from_str "Z" ctx in let rec loop i nat = - if i = 0 then nat else loop (i - 1) (L.mkCall (s,[Pexp.Anormal, nat])) in + if i = 0 then nat else loop (i - 1) (L.mkCall (DB.dsinfo, s,[Pexp.Anormal, nat])) in loop n z let to_snat n ctx = @@ -181,13 +181,13 @@ let to_snat n ctx = let rec loop i nat snat = if i = 0 then snat else loop (i - 1) - (L.mkCall (s,[Pexp.Anormal, nat])) - (L.mkCall (ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in + (L.mkCall (DB.dsinfo, s,[Pexp.Anormal, nat])) + (L.mkCall (DB.dsinfo, ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in loop n (to_nat 0 ctx) zs let snat_n_t n ctx = let snat = lexp_from_str "SNat" ctx in - L.mkCall (snat, [Pexp.Anormal, to_nat n ctx]) + L.mkCall (DB.dsinfo, snat, [Pexp.Anormal, to_nat n ctx]) let snat_metavar i ctx = make_metavar (snat_n_t i ctx) ctx ===================================== tests/positivity_test.ml ===================================== @@ -23,7 +23,7 @@ open Utest_lib open Lexp open Positivity -open Util +(*open Util*) exception WrongPolarity of vname ===================================== tests/unify_test.ml ===================================== @@ -35,6 +35,8 @@ module U = Util let ectx = Elab.default_ectx let rctx = Elab.default_rctx +let dsinfo = DB.dsinfo + type result = | Constraint | Unification @@ -94,19 +96,19 @@ let _ = | Z | S (Nat); |} ectx in - let dloc = U.dummy_location in - let nat = mkVar ((dloc, Some "Nat"), 2) in + let dsinfo = DB.dsinfo in + let nat = mkVar ((dsinfo, Some "Nat"), 2) in let shift l i = mkSusp l (S.shift i) in let ectx, _ = List.fold_left (fun (ectx, i) (name, lexp) -> - Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) + Elab.ctx_extend ectx (dsinfo, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, - dloc, shift nat 2)))); + [("f", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("g", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("h", (mkArrow (dsinfo, Anormal, (dsinfo, Some "x"), nat, + mkArrow (dsinfo, Anormal, (dsinfo, Some "y"), shift nat 1, + shift nat 2)))); ("a", nat); ("b", nat)] in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c422f432696c763f421506953ad89beef… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c422f432696c763f421506953ad89beef… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch location-sinfo
by Ismaila FALL (＠Fallismaila) 26 Mai '22

26 Mai '22

Ismaila FALL pushed new branch location-sinfo at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/location-sinfo You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch location->sinfo
by Ismaila FALL (＠Fallismaila) 26 Mai '22

26 Mai '22

Ismaila FALL deleted branch location-&gt;sinfo at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch location->sinfo
by Ismaila FALL (＠Fallismaila) 26 Mai '22

26 Mai '22

Ismaila FALL pushed new branch location-&gt;sinfo at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/location->sinfo You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][minimal-server] fixing variable searching
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 24 Mai '22

24 Mai '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: 8f23b347 by Soilih at 2022-05-24T14:42:30-04:00 fixing variable searching - - - - - 3 changed files: - src/lexp.ml - + src/lsp_server_test.ml - src/typer_lsp_server.ml Changes: ===================================== src/lexp.ml ===================================== @@ -1068,7 +1068,7 @@ and lexp_str ctx (exp : lexp) : string = let print_arg str (arg_type, lxp) = match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) + | Aerasable when pp_erasable ctx -> "" | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) | Anormal -> str ^ " " ^ (lexp_str' lxp) | _ -> str in ( ===================================== src/lsp_server_test.ml ===================================== @@ -0,0 +1,216 @@ +(* +* +* +* HOVER +* +* +**) + +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,_) = Typer_lsp_server.compile_string content in +let (list_list, _) = Option.get ast in +let (l,c) = position in +let pos = Typer_lsp_server.pos_of_tuple position in + +let (lctx,vx) = Typer_lsp_server.lexp_search ctx list_list pos in +let ((lvn,_),lexp,ltyp) = vx in +let (l_ctx_r,_,_,_,_,_) as ret = Typer_lsp_server.browse_lexp lctx lexp pos [] in +let ret' = (l_ctx_r, None, ltyp, None, lvn,[]) in +let (_,_,l_type,_,_,_) = Typer_lsp_server.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 +let res = "result : " ^ (comp expected (Lexp.lexp_string_for_lsp l_type)) in +let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in +let sep = "################################################\n" in +let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in +output_string oc (sep ^ input ^ pos ^ excpect ^ output ^ res ^ sep ); +close_out oc + +let sep name s = +let content = "\n\n\n/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in +let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in +output_string oc content; +close_out oc + + +let test_hover () = +let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in +let name = "/home/soilih/Bureau/test/test.txt" in +sep name "INT"; +hoverTest ctx name "e = 12 ;" (1,1) "##Int"; +hoverTest ctx name "e = 12 ;" (1,5) "##Int"; +sep name "STRING"; +hoverTest ctx name "s = \"hejej\" ;" (1,1) "##String"; +hoverTest ctx name "s = \"hejej\" ;" (1,8) "##String"; +sep name "FLOAT"; +hoverTest ctx name "f = 12.3 ;" (1,1) "##Float"; +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) "##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"; +hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12) "##Int"; +hoverTest ctx name "multiply x y z = _*_ x y ;" (1,14) "τ"; +hoverTest ctx name "multiply x y z = _*_ x y ;" (1,18) "(Int -> (Int -> Int))"; +hoverTest ctx name "multiply x y z = _*_ x y ;" (1,21) "##Int"; +hoverTest ctx name "multiply x y z = _*_ x y ;" (1,23) "##Int"; +hoverTest ctx name "multiply x y z = x + y + z ;" (1,1) "(x : ##Int) -> (y : ##Int) -> (z : ##Int) -> Int"; +hoverTest ctx name "multiply x y z = x + y + z ;" (1,10) "##Int"; +hoverTest ctx name "multiply x y z = x + y + z ;" (1,12) "##Int"; +hoverTest ctx name "multiply x y z = x + y + z ;" (1,14) "##Int"; +hoverTest ctx name "multiply x y z = x + y + z ;" (1,18) "##Int"; +hoverTest ctx name "multiply x y z = x + y + z ;" (1,20) "(Int -> (Int -> Int))"; +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) "##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"; +hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 \"h\" ;" (4,19) "##String"; +sep name "BUILTIN"; +hoverTest ctx name "foo = ##Int ;" (1,1) "##Type"; +hoverTest ctx name "foo = ##Int ;" (1,9) "##Type"; +sep name "SUSP"; +hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; +hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6) "(##Type_ ##TypeLevel.z)"; +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) "(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) ""; +hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; +hoverTest ctx name "v = Int -> Int ;" (1,1) ""; +sep name "INDUCTIVE"; +hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; +hoverTest ctx name "type Floo = bar Int Int ;" (1,18) ""; +hoverTest ctx name "type Floo = bar Int Int ;" (1,22) ""; +hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1) ""; +hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19) ""; +hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26) ""; +hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1) ""; +hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; +hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; +hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; +hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18) ""; +hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,24) ""; +hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,32) ""; +sep name "METAVAR"; +hoverTest ctx name "x : ?t = 3 ;" (1,1) ""; +hoverTest ctx name "x : ?t = 3 ;" (1,6) ""; +hoverTest ctx name "f x = _+_ ?y x ;" (1,1) ""; +hoverTest ctx name "f x = _+_ ?y x ;" (1,3) ""; +hoverTest ctx name "f x = _+_ ?y x ;" (1,12) ""; +hoverTest ctx name "f x = _+_ ?y x ;" (1,14) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15) ""; +hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,24) ""; +sep name "LET"; +hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1) ""; +hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,10) ""; +hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,18) ""; +hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,26) ""; +hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,35) ""; +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 => \"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) "" + + +(* +* +* +* AFFICHER LA LISTE DE LISTE +* +* +**) + +let afficher_lst code filename = + let ch = open_in code in + let content = really_input_string ch (in_channel_length ch) in + close_in ch; + let (_,ast,_) = Typer_lsp_server.compile_string content in + let (list_list, _) = Option.get ast in + List.iteri (fun i x -> + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in + output_string oc ("\n\n---------------liste: " ^ (string_of_int i) ^ " --------------\n\n"); + close_out oc; + List.iteri (fun _j (y : Util.vname * Lexp.lexp * Lexp.ltype)-> + let (vn,_,_) = y in + let (l,ss) = vn in + let s = try Option.get ss + with _ -> failwith "The Var doesn't have a string!" + in + let output = "Var: " ^ s ^ "\nline: " ^ (string_of_int l.start_line) ^ " - " ^ + (string_of_int l.end_line) ^ "\ncolumn: " ^ (string_of_int l.start_column) ^ " - " + ^ (string_of_int l.end_column) ^ "\n\n" + in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in + output_string oc output; + close_out oc; + ) x + ) list_list + +(* +* +* +* BREADCRUMBS +* +* +**) +let testerBread cursor str = + let (_,ast,_) = Typer_lsp_server.compile_string str in + let (list_list, _) = Option.get ast in + let typer_loc = Typer_lsp_server.pos_of_tuple cursor in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let lexp = Typer_lsp_server.trans_list_in_list_to_let list_list in + let (_,_,_,_,_,lst) = Typer_lsp_server.browse_lexp ctx lexp typer_loc [] in + let str = List.fold_left ( + fun str x -> + let (_,st) = x in + (Option.get st) ^ " > " ^ str + ) "" lst in + let name = "/home/soilih/Bureau/test/symbol.txt" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + output_string oc ("bread: " ^ str ^ "\n") + +let bread_test = + afficher_lst "/home/soilih/Bureau/exemple.typer" "/home/soilih/Bureau/test/highlight.txt"; + testerBread (2,2) "multiply _x = \nlet lst = cons 2 nil in\nlst" \ No newline at end of file ===================================== src/typer_lsp_server.ml ===================================== @@ -729,15 +729,15 @@ let rec str_order (substr:string) (str:string) : bool = (* 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 + 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 @@ -746,21 +746,21 @@ 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) + 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 = -if (String.equal str "") then "" -else if (Int.equal pos 0) then String.make 1 str.[pos] ^ ret -else if (List.exists (fun x -> Char.equal x str.[pos]) char_list) then ret -else search_word_in_cursor str char_list (pos - 1) ((String.make 1 str.[pos]) ^ ret) + if (String.equal str "") then "" + else if (Int.equal pos 0) then String.make 1 str.[pos] ^ ret + else if (List.exists (fun x -> Char.equal x str.[pos]) char_list) then ret + else search_word_in_cursor str char_list (pos - 1) ((String.make 1 str.[pos]) ^ ret) let use_search_word (str:string) (char_list:char list) (pos:int) (ret:string) : string = -match pos with -| 0 -> search_word_in_cursor str char_list pos ret -| _ -> search_word_in_cursor str char_list (pos - 1) ret + match pos with + | 0 -> search_word_in_cursor str char_list pos ret + | _ -> search_word_in_cursor str char_list (pos - 1) ret @@ -920,7 +920,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Var _ -> None | Susp (e, s) -> browse_defs (Lexp.push_susp e s) cursor | Let (_, defs, el) - -> let idx = (List.length defs) - 1 in + -> (let idx = (List.length defs) - 1 in let rec foo (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = match ctx_list with | [] -> failwith "No Variable on the cursor" @@ -929,8 +929,29 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = else foo tl cursor (comp + 1) | _::tl -> foo tl cursor (comp + 1) in - foo defs cursor 0 - + let rec foo'' (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = + match ctx_list with + | [] -> failwith "No variable found on the cursor!" + | (_, _, ltp)::tl + -> if (not ((browse_defs lxp cursor) = None)) then + browse_defs ltp cursor + else foo'' tl cursor (comp + 1) + in + let rec foo' (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = + match ctx_list with + | [] -> foo'' ctx_list cursor comp + | (_, lxp, _)::tl + -> if (not ((browse_defs lxp cursor) = None)) then + browse_defs lxp cursor + else foo' tl cursor (comp + 1) + in + try foo defs cursor 0 + with _ + -> if (not ((browse_defs el cursor) = None)) then + browse_defs el cursor + else foo' defs cursor 0 + ) + | Arrow (_, v, t1, _, t2) -> if (vn_on_the_cursor v cursor) then Some (t2, v, 0) @@ -941,7 +962,10 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Lambda (_, v, t, e) -> (*let ctx' = Debruijn.lctx_extend ctx v Variable t in*) if (vn_on_the_cursor v cursor) then Some (e, v, 0) - else browse_defs t cursor + else (if not ((browse_defs e cursor) = None) then + browse_defs e cursor + else browse_defs t cursor + ) | Call (f, args) -> if not ((browse_defs f cursor) = None) then browse_defs f cursor @@ -1361,56 +1385,11 @@ class lsp_server = end - -let afficher_lst code filename = - let ch = open_in code in - let content = really_input_string ch (in_channel_length ch) in - close_in ch; - let (_,ast,_) = compile_string content in - let (list_list, _) = Option.get ast in - List.iteri (fun i x -> - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in - output_string oc ("\n\n---------------liste: " ^ (string_of_int i) ^ " --------------\n\n"); - close_out oc; - List.iteri (fun _j (y : vname * Lexp.lexp * Lexp.ltype)-> - let (vn,_,_) = y in - let (l,ss) = vn in - let s = try Option.get ss - with _ -> failwith "The Var doesn't have a string!" - in - let output = "Var: " ^ s ^ "\nline: " ^ (string_of_int l.start_line) ^ " - " ^ - (string_of_int l.end_line) ^ "\ncolumn: " ^ (string_of_int l.start_column) ^ " - " - ^ (string_of_int l.end_column) ^ "\n\n" - in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in - output_string oc output; - close_out oc; - ) x - ) list_list - -let testerBread cursor str = - let (_,ast,_) = compile_string str in - let (list_list, _) = Option.get ast in - let typer_loc = pos_of_tuple cursor in - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let lexp = trans_list_in_list_to_let list_list in - let (_,_,_,_,_,lst) = browse_lexp ctx lexp typer_loc [] in - let str = List.fold_left ( - fun str x -> - let (_,st) = x in - (Option.get st) ^ " > " ^ str - ) "" lst in - let name = "/home/soilih/Bureau/test/symbol.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in - output_string oc ("bread: " ^ str ^ "\n") - (* Main code This is the code that creates an instance of the lsp server class and runs it as a task. *) let run () = ignore (Arg.Set Log.lsp_enabled); - afficher_lst "/home/soilih/Bureau/exemple.typer" "/home/soilih/Bureau/test/highlight.txt"; - testerBread (2,2) "multiply _x = \nlet lst = cons 2 nil in\nlst"; 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/-/commit/8f23b3470dcd115470055142bcb399b8e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8f23b3470dcd115470055142bcb399b8e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch ja-refl
by Jean-Alexandre Barszcz (＠jabarszcz) 23 Mai '22

23 Mai '22

Jean-Alexandre Barszcz pushed new branch ja-refl at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/ja-refl You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][minimal-server] 3 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 16 Mai '22

16 Mai '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: 30526f2f by Soilih at 2022-05-16T02:06:00-04:00 - - - - - - 2c27abb1 by Soilih at 2022-05-16T13:56:35-04:00 - - - - - - 7795c2bd by Soilih at 2022-05-16T16:24:57-04:00 fixing completion order problem - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -686,45 +686,45 @@ let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = (* 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 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 = 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 + 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 _ -> String.index str (Char.uppercase_ascii chr) + try String.index str (Char.lowercase_ascii chr) + with _ -> 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 + 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 (* Filter completions list by a string *) @@ -891,7 +891,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = let ret' = List.fold_right (fun (_, ( _, l, lxp)) ret -> let j = List.length l in find_references lxp vr (idx_vr + j) ret - ) lst [] + ) lst ret in find_references e vr idx_vr (find_references retu vr idx_vr ret') @@ -923,7 +923,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = -> let idx = (List.length defs) - 1 in let rec foo (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = match ctx_list with - | [] -> failwith "No Variable in the cursor" + | [] -> failwith "No Variable on the cursor" | ((_, (Some _) as v),_,_)::tl -> if (vn_on_the_cursor v cursor) then Some (el, v, comp - idx) else foo tl cursor (comp + 1) @@ -954,22 +954,23 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Proj (_, e, (_, _)) -> browse_defs e cursor | Case (_, e, _, branches, _) -> - let (vn, lxp, comp) = SMap.fold - (fun _name (_l, vdefs, branch) (_lst: vname * Lexp.lexp * int) - -> let rec collect vdefs comp = - match vdefs with - | [] -> failwith "Cursor is not on any branch !" - | (_, vdef)::vdefs - -> if (vn_on_the_cursor vdef cursor) then (vdef, branch, List.length vdefs) - else collect vdefs (comp + 1) - in - collect vdefs 0 - ) - branches ((Source.Location.dummy, Some ""), Lexp.impossible, 0) - in - if (Lexp.hc_eq lxp Lexp.impossible) then - browse_defs e cursor - else Some (lxp, vn, comp) + let ret = SMap.fold + (fun _name (_l, vdefs, branch) (_lst: (Lexp.lexp * vname * int) option) + -> let rec collect vdefs = + match vdefs with + | [] -> browse_defs branch cursor + | (_, vdef)::vdefs + -> if (vn_on_the_cursor vdef cursor) then Some (branch, vdef, List.length vdefs) + else collect vdefs + in + collect vdefs + ) + branches (Some (Lexp.impossible, (Source.Location.dummy, Some ""), 0)) + in + let (lxp, _, _) = Option.get ret in + if (Lexp.hc_eq lxp Lexp.impossible) then + browse_defs e cursor + else ret | Cons _ -> None | Metavar _ -> None @@ -1219,9 +1220,11 @@ class lsp_server = let (list_list, _) = Option.get 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 lexp = trans_list_in_list_to_let list_list in*) + *) + let lexp = trans_list_in_list_to_let list_list in (* let trans_string = Compl.tranform_string doc_state.content in @@ -1229,7 +1232,7 @@ class lsp_server = let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in *) - match browse_lexp lctx lexp typer_loc [] with + match browse_lexp ctx lexp typer_loc [] with | (l_ctx,_,_, None,_,_) -> View it on GitLab: https://gitlab.com/monnier/typer/-/compare/d92349b72ccf64b5dcc6b2e12bc260fb… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/d92349b72ccf64b5dcc6b2e12bc260fb… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mai 2022