Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Mai 2022
- 2 participants
- 15 discussions
[Git][monnier/typer][location-sinfo] Suppression du module Int
by Ismaila FALL (@Fallismaila) 31 Mai '22
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
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
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
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
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
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
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
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
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
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