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
Mars 2022
- 3 participants
- 21 discussions
[Git][monnier/typer] Pushed new branch minimal-server
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 29 Mar '22
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 29 Mar '22
29 Mar '22
Soilihi BEN SOILIHI BOINA pushed new branch minimal-server at Stefan / Typer
--
View it on GitLab: https://gitlab.com/monnier/typer/-/tree/minimal-server
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][master] * tests/samples_test.ml : Check that the samples can be evaluated.
by Jean-Alexandre Barszcz (@jabarszcz) 17 Mar '22
by Jean-Alexandre Barszcz (@jabarszcz) 17 Mar '22
17 Mar '22
Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer
Commits:
ffd27741 by Jean-Alexandre Barszcz at 2022-03-17T15:34:57-04:00
* tests/samples_test.ml : Check that the samples can be evaluated.
- - - - -
5 changed files:
- + samples/dune
- + samples/unerase.typer
- tests/dune
- + tests/samples_test.ml
- tests/utest_lib.ml
Changes:
=====================================
samples/dune
=====================================
@@ -0,0 +1,5 @@
+;; -*- lisp-data -*-
+
+(alias
+ (name typer_samples)
+ (deps (glob_files *.typer)))
=====================================
samples/unerase.typer
=====================================
@@ -0,0 +1,4 @@
+%Eq_unerase : Eq ?x ?y ≡> Eq ?x ?y;
+Eq_unerase =
+ lambda x y (p : Eq x y) ≡>
+ Eq_cast (p := p) (f := Eq x) Eq_refl;
=====================================
tests/dune
=====================================
@@ -10,9 +10,11 @@
lexer_test
macro_test
positivity_test
+ samples_test
sexp_test
unify_test)
- (deps (alias %{project_root}/btl/typer_stdlib))
+ (deps (alias %{project_root}/btl/typer_stdlib)
+ (alias %{project_root}/samples/typer_samples))
(libraries typerlib)
(action
(chdir %{project_root} (run %{test}))))
=====================================
tests/samples_test.ml
=====================================
@@ -0,0 +1,71 @@
+(* Copyright (C) 2022 Free Software Foundation, Inc.
+ *
+ * Author: Jean-Alexandre Barszcz <jean-alexandre.barszcz(a)umontreal.ca>
+ * Keywords: languages, lisp, dependent types.
+ *
+ * This file is part of Typer.
+ *
+ * Typer is free software; you can redistribute it and/or modify it under the
+ * terms of the GNU General Public License as published by the Free Software
+ * Foundation, either version 3 of the License, or (at your option) any
+ * later version.
+ *
+ * Typer is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
+ * FOR A PARTICULAR PURPOSE. See the GNU General Public License for
+ * more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program. If not, see <http://www.gnu.org/licenses/>. *)
+
+open Typerlib
+open Utest_lib
+module SSet = Set.Make(String)
+
+let ectx = Elab.default_ectx
+
+let add_sample_test filename =
+ let error_expected =
+ Filename.check_suffix (Filename.remove_extension filename) "error" in
+ let run_sample_test () =
+ let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) in
+ let file = Filename.concat "samples" filename in
+ ignore (Elab.process_file backend ectx file);
+ Log.stop_on_error ();
+ success in
+ add_test "SAMPLES" filename (fun () ->
+ if error_expected then
+ expect_throw (fun _ -> "successful evaluation") run_sample_test
+ else
+ run_sample_test ()
+ )
+
+(* Some samples are currently not runnable, let's skip them. *)
+(* FIXME: Fix these samples. *)
+let excluded_samples =
+ SSet.of_list [
+ "autodiff.typer";
+ "batch_test.typer";
+ "bbst_test.typer";
+ "case_test.typer";
+ "defmacro.typer";
+ "dependent.typer";
+ "hurkens.typer";
+ "io.typer";
+ "list_n.typer";
+ "myers_test.typer";
+ "pervasive.typer";
+ "polyfun_test.typer";
+ "table_test.typer";
+ "tuple_test.typer";
+ "typer_proof.typer";
+ ]
+
+let _ =
+ let samples =
+ List.filter (fun fn -> Filename.check_suffix fn ".typer" &&
+ not (SSet.mem fn excluded_samples))
+ (Array.to_list (Sys.readdir "samples")) in
+ List.iter add_sample_test samples
+
+let _ = run_all ()
=====================================
tests/utest_lib.ml
=====================================
@@ -182,6 +182,14 @@ let expect_equal_decls =
in
_expect_equal_t decl_list_eq string_of_decl_list
+let expect_throw to_string test =
+ try let value = test () in
+ ut_string2 (red ^ "EXPECTED an exception" ^ reset ^ "\n");
+ ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n");
+ failure
+ with
+ | _ -> success
+
(* USAGE
*
* (add_test "LET" "Base Case" (fun () ->
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ffd27741d8314eefdea641d2e732d60a4…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ffd27741d8314eefdea641d2e732d60a4…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][keep-samples-alive] * tests/samples_test.ml : Check that the samples can be evaluated.
by Jean-Alexandre Barszcz (@jabarszcz) 17 Mar '22
by Jean-Alexandre Barszcz (@jabarszcz) 17 Mar '22
17 Mar '22
Jean-Alexandre Barszcz pushed to branch keep-samples-alive at Stefan / Typer
Commits:
ffd27741 by Jean-Alexandre Barszcz at 2022-03-17T15:34:57-04:00
* tests/samples_test.ml : Check that the samples can be evaluated.
- - - - -
5 changed files:
- + samples/dune
- + samples/unerase.typer
- tests/dune
- + tests/samples_test.ml
- tests/utest_lib.ml
Changes:
=====================================
samples/dune
=====================================
@@ -0,0 +1,5 @@
+;; -*- lisp-data -*-
+
+(alias
+ (name typer_samples)
+ (deps (glob_files *.typer)))
=====================================
samples/unerase.typer
=====================================
@@ -0,0 +1,4 @@
+%Eq_unerase : Eq ?x ?y ≡> Eq ?x ?y;
+Eq_unerase =
+ lambda x y (p : Eq x y) ≡>
+ Eq_cast (p := p) (f := Eq x) Eq_refl;
=====================================
tests/dune
=====================================
@@ -10,9 +10,11 @@
lexer_test
macro_test
positivity_test
+ samples_test
sexp_test
unify_test)
- (deps (alias %{project_root}/btl/typer_stdlib))
+ (deps (alias %{project_root}/btl/typer_stdlib)
+ (alias %{project_root}/samples/typer_samples))
(libraries typerlib)
(action
(chdir %{project_root} (run %{test}))))
=====================================
tests/samples_test.ml
=====================================
@@ -0,0 +1,71 @@
+(* Copyright (C) 2022 Free Software Foundation, Inc.
+ *
+ * Author: Jean-Alexandre Barszcz <jean-alexandre.barszcz(a)umontreal.ca>
+ * Keywords: languages, lisp, dependent types.
+ *
+ * This file is part of Typer.
+ *
+ * Typer is free software; you can redistribute it and/or modify it under the
+ * terms of the GNU General Public License as published by the Free Software
+ * Foundation, either version 3 of the License, or (at your option) any
+ * later version.
+ *
+ * Typer is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
+ * FOR A PARTICULAR PURPOSE. See the GNU General Public License for
+ * more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program. If not, see <http://www.gnu.org/licenses/>. *)
+
+open Typerlib
+open Utest_lib
+module SSet = Set.Make(String)
+
+let ectx = Elab.default_ectx
+
+let add_sample_test filename =
+ let error_expected =
+ Filename.check_suffix (Filename.remove_extension filename) "error" in
+ let run_sample_test () =
+ let backend = new Eval.ast_interpreter (Debruijn.ectx_to_lctx ectx) in
+ let file = Filename.concat "samples" filename in
+ ignore (Elab.process_file backend ectx file);
+ Log.stop_on_error ();
+ success in
+ add_test "SAMPLES" filename (fun () ->
+ if error_expected then
+ expect_throw (fun _ -> "successful evaluation") run_sample_test
+ else
+ run_sample_test ()
+ )
+
+(* Some samples are currently not runnable, let's skip them. *)
+(* FIXME: Fix these samples. *)
+let excluded_samples =
+ SSet.of_list [
+ "autodiff.typer";
+ "batch_test.typer";
+ "bbst_test.typer";
+ "case_test.typer";
+ "defmacro.typer";
+ "dependent.typer";
+ "hurkens.typer";
+ "io.typer";
+ "list_n.typer";
+ "myers_test.typer";
+ "pervasive.typer";
+ "polyfun_test.typer";
+ "table_test.typer";
+ "tuple_test.typer";
+ "typer_proof.typer";
+ ]
+
+let _ =
+ let samples =
+ List.filter (fun fn -> Filename.check_suffix fn ".typer" &&
+ not (SSet.mem fn excluded_samples))
+ (Array.to_list (Sys.readdir "samples")) in
+ List.iter add_sample_test samples
+
+let _ = run_all ()
=====================================
tests/utest_lib.ml
=====================================
@@ -182,6 +182,14 @@ let expect_equal_decls =
in
_expect_equal_t decl_list_eq string_of_decl_list
+let expect_throw to_string test =
+ try let value = test () in
+ ut_string2 (red ^ "EXPECTED an exception" ^ reset ^ "\n");
+ ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n");
+ failure
+ with
+ | _ -> success
+
(* USAGE
*
* (add_test "LET" "Base Case" (fun () ->
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ffd27741d8314eefdea641d2e732d60a4…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ffd27741d8314eefdea641d2e732d60a4…
You're receiving this email because of your account on gitlab.com.
1
0
17 Mar '22
Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer
Commits:
c6bb08e5 by Fallismaila at 2022-03-17T17:48:53+00:00
Introduce sinfo
- - - - -
12 changed files:
- src/REPL.ml
- src/builtin.ml
- src/debruijn.ml
- src/elab.ml
- src/eval.ml
- src/heap.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/opslexp.ml
- src/positivity.ml
- src/sexp.ml
- src/unification.ml
Changes:
=====================================
src/REPL.ml
=====================================
@@ -136,7 +136,7 @@ let eval_interactive
let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in
let lexprs = Elab.lexp_parse_all exprs ectx' in
- List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs;
+ List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr dummy_sinfo)) lexprs;
List.iter interactive#process_decls ldecls;
Log.print_log ();
=====================================
src/builtin.ml
=====================================
@@ -90,7 +90,7 @@ let predef_map : lexp SMap.t ref
let get_predef (name: string) (ctx: DB.elab_context) : lexp =
try let r = (DB.get_size ctx) - !builtin_size - 0 in
let p = SMap.find name (!predef_map) in
- mkSusp p (S.shift r) sinfo
+ mkSusp p (S.shift r) dummy_sinfo
with Not_found -> log_raise_error {|"%s" was not predefined|} name
let set_predef name lexp
@@ -100,7 +100,7 @@ let set_predef name lexp
let dloc = DB.dloc
let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc,
- mkArrow (Anormal, (dloc, None), t, dloc, t) sinfo) sinfo
+ mkArrow (Anormal, (dloc, None), t, dloc, t) dummy_sinfo) dummy_sinfo
let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx
@@ -136,11 +136,11 @@ let lmap = ref (SMap.empty : (lexp * ltype) SMap.t)
let add_builtin_cst (name : string) (e : lexp)
= let map = !lmap in
assert (not (SMap.mem name map));
- let t = OL.check Myers.nil e in
+ let t = OL.check Myers.nil e dummy_sinfo in
lmap := SMap.add name (e, t) map
let new_builtin_type name kind =
- let t = mkBuiltin ((dloc, name), kind) sinfo in
+ let t = mkBuiltin ((dloc, name), kind) dummy_sinfo in
add_builtin_cst name t;
t
@@ -159,7 +159,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) sinfo
+ mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) dummy_sinfo
let register_builtin_types () =
let _ = new_builtin_type "Sexp" DB.type0 in
=====================================
src/debruijn.ml
=====================================
@@ -44,6 +44,7 @@ open Fmt
module S = Subst
+
let fatal ?print_action ?loc fmt =
Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt
@@ -83,33 +84,35 @@ let fatal ?print_action ?loc fmt =
* ---------------------------------- *)
let dloc = dummy_location
-let type_level_sort = mkSort (dloc, StypeLevel) sinfo
-let sort_omega = mkSort (dloc, StypeOmega) sinfo
-let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) sinfo
-let level0 = mkSortLevel SLz sinfo
-let level1 = mkSortLevel (mkSLsucc level0) sinfo
-let level2 = mkSortLevel (mkSLsucc level1) sinfo
-let type0 = mkSort (dloc, Stype level0) sinfo
-let type1 = mkSort (dloc, Stype level1) sinfo
-let type2 = mkSort (dloc, Stype level2) sinfo
-let type_int = mkBuiltin ((dloc, "Int"), type0) sinfo
-let type_integer = mkBuiltin ((dloc, "Integer"), type0) sinfo
-let type_float = mkBuiltin ((dloc, "Float"), type0) sinfo
-let type_string = mkBuiltin ((dloc, "String"), type0) sinfo
-let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) sinfo
+let type_level_sort = mkSort (dloc, StypeLevel) dummy_sinfo
+let sort_omega = mkSort (dloc, StypeOmega) dummy_sinfo
+let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) dummy_sinfo
+let level0 = mkSortLevel SLz dummy_sinfo
+let level1 = mkSortLevel (mkSLsucc level0) dummy_sinfo
+let level2 = mkSortLevel (mkSLsucc level1) dummy_sinfo
+let type0 = mkSort (dloc, Stype level0) dummy_sinfo
+let type1 = mkSort (dloc, Stype level1) dummy_sinfo
+let type2 = mkSort (dloc, Stype level2) dummy_sinfo
+let type_int = mkBuiltin ((dloc, "Int"), type0) dummy_sinfo
+let type_integer = mkBuiltin ((dloc, "Integer"), type0) dummy_sinfo
+let type_float = mkBuiltin ((dloc, "Float"), type0) dummy_sinfo
+let type_string = mkBuiltin ((dloc, "String"), type0) dummy_sinfo
+let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) dummy_sinfo
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) sinfo)) sinfo, dloc,
+ mkSort (dloc, Stype (mkVar (lv, 0) dummy_sinfo)) dummy_sinfo , dloc,
mkArrow (Anormal, (dloc, None),
- mkVar (tv, 0) sinfo, dloc,
+ mkVar (tv, 0) dummy_sinfo, dloc,
mkArrow (Anormal, (dloc, None),
- mkVar (tv, 1) sinfo, dloc,
- mkSort (dloc, Stype (mkVar (lv, 3) sinfo)) sinfo) sinfo) sinfo) sinfo) sinfo
-let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) sinfo
+ mkVar (tv, 1) dummy_sinfo, dloc,
+ mkSort (dloc, Stype (mkVar (lv, 3) dummy_sinfo)) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo)
+
+let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type dummy_sinfo) dummy_sinfo
+
let eq_refl =
let lv = (dloc, Some "l") in
let tv = (dloc, Some "t") in
@@ -118,14 +121,14 @@ let eq_refl =
mkArrow (Aerasable, lv,
type_level, dloc,
mkArrow (Aerasable, tv,
- mkSort (dloc, Stype (mkVar (lv, 0) sinfo)) sinfo, dloc,
+ mkSort (dloc, Stype (mkVar (lv, 0) dummy_sinfo)) dummy_sinfo, dloc,
mkArrow (Aerasable, xv,
- mkVar (tv, 0) sinfo, dloc,
+ mkVar (tv, 0) dummy_sinfo, dloc,
mkCall (type_eq,
- [Aerasable, mkVar (lv, 2) sinfo;
- Aerasable, mkVar (tv, 1) sinfo;
- Anormal, mkVar (xv, 0) sinfo;
- Anormal, mkVar (xv, 0) sinfo]) sinfo) sinfo) sinfo) sinfo) sinfo
+ [Aerasable, mkVar (lv, 2) dummy_sinfo;
+ Aerasable, mkVar (tv, 1) dummy_sinfo;
+ Anormal, mkVar (xv, 0) dummy_sinfo;
+ Anormal, mkVar (xv, 0) dummy_sinfo]) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo
(* easier to debug with type annotations *)
@@ -293,7 +296,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) =
(match lexp with
| None -> print_string "<var>"
| Some lexp
- -> (let str = lexp_str (!debug_ppctx) lexp in
+ -> (let str = lexp_str (!debug_ppctx) lexp dummy_sinfo in
let strs =
match String.split_on_char '\n' str with
| hd :: tl -> print_string hd; tl
@@ -380,12 +383,12 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp =
let (_, i) = vref in
let (_, _, t) = lctx_lookup ctx vref in
- mkSusp t (S.shift (i + 1)) sinfo
+ mkSusp t (S.shift (i + 1)) dummy_sinfo
let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option =
let (_, i) = vref in
match lctx_lookup ctx vref with
- | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o)))
+ | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o)) dummy_sinfo)
| _ -> None
let env_lookup_type ctx (v : vref): lexp =
=====================================
src/elab.ml
=====================================
@@ -111,7 +111,7 @@ let special_forms : special_forms_map ref = ref SMap.empty
let type_special_form = BI.new_builtin_type "Special-Form" type0
let add_special_form (name, func) =
- BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form) sinfo);
+ BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form) dummy_sinfo);
special_forms := SMap.add name func (!special_forms)
let get_special_form name =
@@ -141,7 +141,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp =
-> lexp_error l ltp {|Type of "%s" is not a proper type: %s|} name tystr
let elab_check_proper_type (ctx : elab_context) ltp var =
- try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp
+ try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp dummy_sinfo) var ltp
with e -> match e with
| Log.Stop_compilation _ -> raise e
| _
@@ -161,7 +161,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
let lctx = ectx_to_lctx ctx in
let loc = lexp_location lxp in
- let ltype' = try OL.check lctx lxp
+ let ltype' = try OL.check lctx lxp dummy_sinfo
with e -> match e with
| Log.Stop_compilation _ -> raise e
| _ ->
@@ -210,13 +210,13 @@ let ctx_define_rec (ctx: elab_context) decls =
let nctx = ectx_extend_rec ctx decls in
let _ = List.fold_left (fun n (var, _lxp, ltp)
-> elab_check_proper_type
- nctx (push_susp ltp (S.shift n)) var;
+ nctx (push_susp ltp (S.shift n) dummy_sinfo) var;
n - 1)
(List.length decls)
decls in
let _ = List.fold_left (fun n (var, lxp, ltp)
-> elab_check_def nctx var lxp
- (push_susp ltp (S.shift n));
+ (push_susp ltp (S.shift n) dummy_sinfo);
n - 1)
(List.length decls)
decls in
@@ -261,14 +261,14 @@ let ctx_define_rec (ctx: elab_context) decls =
let newMetavar (ctx : lexp_context) sl name t =
let meta = Unif.create_metavar ctx sl t in
- mkMetavar (meta, S.identity, name) sinfo
+ mkMetavar (meta, S.identity, name) dummy_sinfo
let newMetalevel (ctx : lexp_context) sl loc =
newMetavar ctx sl (loc, Some "ℓ") type_level
let newMetatype (ctx : lexp_context) sl loc
= newMetavar ctx sl (loc, Some "τ")
- (mkSort (loc, Stype (newMetalevel ctx sl loc)) sinfo)
+ (mkSort (loc, Stype (newMetalevel ctx sl loc)) dummy_sinfo)
(* Functions used when we need to return some lexp/ltype but
* an error makes it impossible to return "the right one". *)
@@ -303,7 +303,7 @@ let elab_varref ctx (loc, name)
= try
let idx = senv_lookup name ctx in
let id = (loc, Some name) in
- let lxp = mkVar (id, idx) sinfo in
+ let lxp = mkVar (id, idx) dummy_sinfo in
let ltp = env_lookup_type ctx (id, idx) in
(lxp, Inferred ltp)
with Senv_Lookup_Fail xs ->
@@ -317,7 +317,7 @@ let elab_varref ctx (loc, name)
(* Turn metavar into plain vars after generalization.
* ids: an IMap that maps metavars to their position as argument
* (first arg gets position 0). *)
-let meta_to_var ids (e : lexp) =
+let meta_to_var ids (e : lexp) sinfo =
let count = IMap.cardinal ids in
@@ -429,7 +429,7 @@ let meta_to_var ids (e : lexp) =
| Sort (_, (StypeOmega | StypeLevel)) -> e
| Builtin _ -> e
| Var (n,i) -> if i < o then e else mkVar (n, i + count) sinfo
- | Susp (e, s) -> loop o (push_susp e s)
+ | Susp (e, s) -> loop o (push_susp e s dummy_sinfo)
| Let (l, defs, e)
-> let len = List.length defs in
let (_, ndefs)
@@ -481,7 +481,7 @@ let meta_to_var ids (e : lexp) =
-> if IMap.mem id ids then
mkVar (name, o + count - IMap.find id ids) sinfo
else match metavar_lookup id with
- | MVal e -> loop o (push_susp e s)
+ | MVal e -> loop o (push_susp e s dummy_sinfo)
| _ -> mkMetavar (id, adjust_subst o s, name) sinfo
in loop 0 e
@@ -503,7 +503,7 @@ let sort_generalized_metavars sl cl ctx mfvs =
then acc else
(assert (cl' >= cl);
let mt = if cl' > cl then
- Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl))
+ Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) dummy_sinfo
else mt in
let mv = (id, vname, mt) in
if (OL.conv_p ctx mt type_level) then
@@ -536,9 +536,9 @@ let generalize (nctx : elab_context) e =
assert (n = IMap.cardinal ids);
match mfvs with
| [] -> assert (n = len);
- meta_to_var ids e
+ meta_to_var ids e dummy_sinfo
| ((id, vname, mt) :: mfvs)
- -> let mt' = meta_to_var ids mt in
+ -> let mt' = meta_to_var ids mt dummy_sinfo in
let n = n + 1 in
let e' = loop (IMap.add id n ids) n mfvs in
wrap (IMap.mem id nes) vname mt' l e' in
@@ -621,11 +621,11 @@ and instantiate_implicit e t ctx =
match OL.lexp'_whnf t (ectx_to_lctx ctx) with
| Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2)
-> let arg = get_implicit_arg ctx (lexp_location e) v t1 in
- instantiate (mkSusp t2 (S.substitute arg) sinfo) ((ak, arg)::args)
- | _ -> (mkCall (e, List.rev args) sinfo, t)
+ instantiate (mkSusp t2 (S.substitute arg) dummy_sinfo) ((ak, arg)::args)
+ | _ -> (mkCall (e, List.rev args) dummy_sinfo, t)
in instantiate t []
-and infer_type pexp ectx var =
+and infer_type pexp ectx var sinfo =
(* We could also use lexp_check with an argument of the form
* Sort (?s), but in most cases the metavar would be allocated
* unnecessarily. *)
@@ -658,7 +658,7 @@ and infer_type pexp ectx var =
t
and lexp_let_decls declss (body: lexp) _ctx =
- List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp) sinfo)
+ List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp) dummy_sinfo)
declss body
and unify_with_arrow ctx tloc lxp kind var aty
@@ -668,7 +668,7 @@ 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) sinfo in
+ let arrow = mkArrow (kind, var, arg, l, body) dummy_sinfo in
match Unif.unify arrow lxp (ectx_to_lctx ctx) with
| ((_ck, _ctx, t1, t2)::_)
-> lexp_error
@@ -756,12 +756,12 @@ and check_case rtype (loc, target, ppatterns) ctx =
-> let arg = newMetavar
(ectx_to_lctx ctx)
(ectx_to_scope_level ctx)
- name (mkSusp t s sinfo) in
+ name (mkSusp t s dummy_sinfo) in
(S.cons arg s, (ak, arg) :: targs))
(S.identity, [])
fargs in
let (cs, args) = (constructors, List.rev targs) in
- ltarget := check_inferred ctx tlxp tltp (mkCall (it', args) sinfo);
+ ltarget := check_inferred ctx tlxp tltp (mkCall (it', args) dummy_sinfo);
it_cs_as := Some (it', cs, args);
(cs, args)
| _ -> let call_split e =
@@ -788,7 +788,7 @@ and check_case rtype (loc, target, ppatterns) ctx =
let shift_to_extended_ctx nctx lexp =
mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx)
- - M.length (ectx_to_lctx ctx))) sinfo in
+ - M.length (ectx_to_lctx ctx))) dummy_sinfo in
let ctx_extend_with_eq nctx head_lexp =
(* Add a proof of equality between the target and the branch
@@ -800,14 +800,14 @@ and check_case rtype (loc, target, ppatterns) ctx =
[(Aerasable, tlvl'); (* Typelevel *)
(Aerasable, tltp'); (* Inductive type *)
(Anormal, head_lexp); (* Lexp of the branch head *)
- (Anormal, tlxp')]) sinfo (* Target lexp *)
+ (Anormal, tlxp')]) dummy_sinfo (* Target lexp *)
in ctx_extend nctx (loc, None) Variable eqty
in
let add_default v =
(if dflt != None then uniqueness_warn pat);
let nctx = ctx_extend ctx v Variable tltp in
- let head_lexp = mkVar (v, 0) sinfo in
+ let head_lexp = mkVar (v, 0) dummy_sinfo 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
@@ -824,7 +824,7 @@ and check_case rtype (loc, target, ppatterns) ctx =
v t in
let nctx = ctx_extend ctx v Variable t in
let body = inst_args nctx body in
- mkSusp body (S.substitute arg) sinfo
+ mkSusp body (S.substitute arg) dummy_sinfo
| _e -> lxp in
match lexp_lexp' (nosusp (inst_args ctx lctor)) with
| Cons (it', (_, cons_name))
@@ -861,16 +861,16 @@ and check_case rtype (loc, target, ppatterns) ctx =
| (_, (ak, (_, Some fname), fty)::cargs)
when SMap.mem fname pe
-> let var = SMap.find fname pe in
- let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in
- make_nctx nctx (ssink var s) pargs cargs
+ let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in
+ make_nctx nctx (ssink dummy_sinfo var s) pargs cargs
(SMap.remove fname pe)
((ak, var)::acc)
| ((ef, var)::pargs, (ak, _, fty)::cargs)
when (match (ef, ak) with
| (Some (_, "_"), _) | (None, Anormal) -> true
| _ -> false)
- -> let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in
- make_nctx nctx (ssink var s) pargs cargs pe
+ -> let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in
+ make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe
((ak, var)::acc)
| ((Some (l, fname), var)::pargs, cargs)
-> if SMap.mem fname pe then
@@ -878,23 +878,23 @@ and check_case rtype (loc, target, ppatterns) ctx =
make_nctx ctx s pargs cargs (SMap.add fname var pe) acc
| pargs, (ak, fname, fty)::cargs
-> let var = (loc, None) in
- let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in
+ let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in
if ak = Anormal then
sexp_error
loc {|Missing pattern for normal field%s|}
(match fname with
| (_, Some n) -> sprintf {| "%s"|} n
| _ -> "");
- make_nctx nctx (ssink var s) pargs cargs pe
+ make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe
((ak, var)::acc) in
let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in
let head_lexp_ctor =
shift_to_extended_ctx nctx
- (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs) sinfo) in
+ (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs) dummy_sinfo) in
let head_lexp_args =
List.mapi (fun i (ak, vname) ->
- (ak, mkVar (vname, List.length fargs - i - 1) sinfo)) fargs in
- let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) sinfo in
+ (ak, mkVar (vname, List.length fargs - i - 1) dummy_sinfo)) fargs in
+ let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) dummy_sinfo 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
@@ -908,7 +908,7 @@ and check_case rtype (loc, target, ppatterns) ctx =
match pat with
| Ppatsym ((_, None) as var) -> add_default var
| Ppatsym ((l, Some name) as var)
- -> if Eval.constructor_p name ctx then
+ -> if Eval.constructor_p name ctx dummy_sinfo then
add_branch (Symbol (l, name)) []
else add_default var (* A named default branch. *)
@@ -917,7 +917,7 @@ and check_case rtype (loc, target, ppatterns) ctx =
let (lpattern, dflt) =
List.fold_left fold_fun (SMap.empty, None) ppatterns in
- mkCase (loc, tlxp, rtype, lpattern, dflt) sinfo
+ mkCase (loc, tlxp, rtype, lpattern, dflt) dummy_sinfo
and elab_macro_call ctx func args ot =
let t
@@ -926,7 +926,7 @@ and elab_macro_call ctx func args ot =
(lexp_location func)
| Some t -> t in
let sxp = match lexp_expand_macro (lexp_location func)
- func args ctx (Some t) with
+ func args ctx (Some t) dummy_sinfo with
| Vcommand cmd
-> (match cmd () with
| Vsexp (sxp) -> sxp
@@ -949,7 +949,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
let larg = check sarg arg_type ctx in
handle_fun_args ((ak, larg) :: largs) sargs
(SMap.remove aname pending)
- (L.mkSusp ret_type (S.substitute larg) sinfo)
+ (L.mkSusp ret_type (S.substitute larg) dummy_sinfo)
| (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs,
Arrow (ak, _, arg_type, _, ret_type)
@@ -957,7 +957,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
(* Explicit-implicit argument. *)
-> let larg = check sarg arg_type ctx in
handle_fun_args ((ak, larg) :: largs) sargs pending
- (L.mkSusp ret_type (S.substitute larg) sinfo)
+ (L.mkSusp ret_type (S.substitute larg) dummy_sinfo)
| (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs,
Arrow _
@@ -982,7 +982,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
| sarg::_ -> sexp_location sarg)
v arg_type in
handle_fun_args ((ak, larg) :: largs) sargs pending
- (L.mkSusp ret_type (S.substitute larg) sinfo)
+ (L.mkSusp ret_type (S.substitute larg) dummy_sinfo)
| [], _
-> (if not (SMap.is_empty pending) then
let pending = SMap.bindings pending in
@@ -1002,10 +1002,10 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
ltp' Anormal (dloc, 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) sinfo) in
+ (L.mkSusp ret_type (S.substitute larg) dummy_sinfo) in
let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in
- (mkCall (func, List.rev largs) sinfo, Inferred ret_type)
+ (mkCall (func, List.rev largs) dummy_sinfo, Inferred ret_type)
(* Parse inductive type definition. *)
and lexp_parse_inductive ctors ctx =
@@ -1022,11 +1022,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) sinfo)
+ -> mkArrow (ak, n, t, dummy_location, aa) dummy_sinfo)
acc impossible in
let g = generalize nctx altacc in
let altacc' = g (fun _ne vname t l e
- -> mkArrow (Aerasable, vname, t, l, e) sinfo)
+ -> mkArrow (Aerasable, vname, t, l, e) dummy_sinfo)
altacc in
if altacc' == altacc
then acc (* No generalization! *)
@@ -1038,7 +1038,7 @@ and lexp_parse_inductive ctors ctx =
| _ -> assert (e = impossible); [] in
loop altacc'
| (kind, var, exp)::tl
- -> let lxp = infer_type exp ctx var in
+ -> let lxp = infer_type exp ctx var dummy_sinfo in
let nctx = ectx_extend ctx var Variable lxp in
loop tl ((kind, var, lxp)::acc) nctx in
loop args [] nctx in
@@ -1089,16 +1089,16 @@ and lexp_eval ectx e =
"Exception happened during evaluation:";
raise exc
-and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option)
+and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) sinfo
: value_type =
(* Build the function to be called *)
let macro_expand = BI.get_predef "Macro_expand" ctx in
(* FIXME: Rather than remember the lexp of "expand_macro" in predef,
* we should remember its value so we don't have to re-eval it everytime. *)
- let macro_expand = lexp_eval ctx macro_expand in
+ let macro_expand = lexp_eval ctx macro_expand sinfo in
(* FIXME: provide `ot` (the optional expected type) for non-decl macros. *)
- let macro = lexp_eval ctx macro_funct in
+ let macro = lexp_eval ctx macro_funct sinfo in
let args = [macro; BI.o2v_list sargs] in
(* FIXME: Make a proper `Var`. *)
@@ -1113,10 +1113,10 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option)
* | e -> sexp_print e; print_string "\n" *)
and lexp_decls_macro (loc, mname) sargs ctx: sexp =
- try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in
+ try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in
(* FIXME: Check that (conv_p ltp Macro)! *)
- let ret = lexp_expand_macro loc lxp sargs ctx None in
+ let ret = lexp_expand_macro loc lxp sargs ctx None dummy_sinfo in
match ret with
| Vcommand cmd
-> (match cmd () with
@@ -1149,14 +1149,14 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)
assert (i < List.length defs);
match Myers.nth i (ectx_to_lctx nctx) with
| (_v', ForwardRef, t)
- -> let adjusted_t = push_susp t (S.shift (i + 1)) in
+ -> let adjusted_t = push_susp t (S.shift (i + 1)) dummy_sinfo in
(* We elab `sexp` within the original `nctx`, i.e.
* the context where the other vars don't have
* a definition yet. This is because we can't yet
* build the proper `nctx`: a partially filled
* mutually-recursive block would not have the
* proper format, e.g. for `lctx_view`! *)
- let e = check sexp adjusted_t nctx in
+ 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)
| _ -> Log.internal_error "Defining same slot!")
@@ -1164,9 +1164,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)
let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in
decls, ctx_define_rec ectx decls
-and infer_and_generalize_type (ctx : elab_context) se name =
+and infer_and_generalize_type (ctx : elab_context) se name sinfo =
let nctx = ectx_new_scope ctx in
- let t = infer_type se nctx name in
+ let t = infer_type se nctx name sinfo in
(* We should not generalize over metavars which only occur on the rightmost
* side of arrows in type annotations (aka declarations), since there's no
* way for the callee to return something of the proper type if those
@@ -1207,11 +1207,11 @@ and infer_and_generalize_def (ctx : elab_context) se =
let g = generalize nctx e in
let e' = g (fun ne vname t _l e
-> mkLambda ((if ne then Aimplicit else Aerasable),
- vname, t, e) sinfo)
+ vname, t, e) dummy_sinfo)
e in
let t' = g (fun ne name t _l e
-> mkArrow ((if ne then Aimplicit else Aerasable),
- name, t, sexp_location se, e) sinfo)
+ name, t, sexp_location se, e) dummy_sinfo)
t in
(e', t')
@@ -1255,13 +1255,13 @@ 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 (loc, Some vname) dummy_sinfo in
if SMap.mem vname pending_decls then
(* Don't burp: take'em all and unify! *)
let pt_idx = senv_lookup vname nctx in
(* Take the previous type annotation. *)
let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with
- | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1))
+ | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) dummy_sinfo
| _ -> Log.internal_error "Var not found at its index!" in
(* Unify it with the new one. *)
let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with
@@ -1297,7 +1297,7 @@ and lexp_decls_1
let var = (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) sinfo, ltp)], sdecls, toks,
+ [(var, mkSusp lexp (S.shift 1) dummy_sinfo, ltp)], sdecls, toks,
ctx_define nctx var lexp ltp
| [Symbol (loc, vname); sexp]
@@ -1408,8 +1408,8 @@ let sform_built_in ctx loc sargs ot =
* function. It's not indispensible, tho it might still be useful for
* 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') sinfo in
+ -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) dummy_sinfo in
+ let bi = mkBuiltin ((loc, name), ltp') dummy_sinfo in
if not (SMap.mem name (!EV.builtin_functions)) then
sexp_error loc {|Unknown built-in "%s"|} name;
BI.add_builtin_cst name bi;
@@ -1427,7 +1427,7 @@ let sform_datacons ctx loc sargs _ot =
match sargs with
| [t; Symbol ((_sloc, _cname) as sym)]
-> let idt, _ = infer t ctx in
- (mkCons (idt, sym) sinfo, Lazy)
+ (mkCons (idt, sym) dummy_sinfo, Lazy)
| [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol";
sform_dummy_ret ctx loc
@@ -1499,12 +1499,12 @@ let sform_typecons ctx loc sargs _ot =
constrs [] in
let map_ctor = lexp_parse_inductive ctors nctx in
- (mkInductive (loc, label, formals, map_ctor) sinfo, Lazy)
+ (mkInductive (loc, label, formals, map_ctor) dummy_sinfo, Lazy)
let sform_hastype ctx loc sargs _ot =
match sargs with
- | [se; st] -> let lt = infer_type st ctx (loc, None) in
- let le = check se lt ctx in
+ | [se; st] -> let lt = infer_type st ctx (loc, None) dummy_sinfo in
+ let le = check se lt ctx in
(le, Inferred lt)
| _ -> sexp_error loc "##_:_ takes two arguments";
sform_dummy_ret ctx loc
@@ -1515,18 +1515,18 @@ let sform_arrow kind ctx loc sargs _ot =
-> let (v, st1) = match st1 with
| Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1)
| _ -> ((sexp_location st1, None), st1) in
- let lt1 = infer_type st1 ctx v in
+ let lt1 = infer_type st1 ctx v dummy_sinfo 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) sinfo, Lazy)
+ let lt2 = infer_type st2 nctx (sexp_location st2, None) dummy_sinfo in
+ (mkArrow (kind, v, lt1, loc, lt2) dummy_sinfo, Lazy)
| _ -> sexp_error loc "##_->_ takes two arguments";
sform_dummy_ret ctx loc
let sform_immediate ctx loc sargs ot =
match sargs with
- | [(String _) as se] -> mkImm (se) sinfo, Inferred DB.type_string
- | [(Integer _) as se] -> mkImm (se) sinfo, Inferred DB.type_int
- | [(Float _) as se] -> mkImm (se) sinfo, Inferred DB.type_float
+ | [(String _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_string
+ | [(Integer _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_int
+ | [(Float _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_float
| [Block (_location, pts)]
-> let grm = ectx_get_grammar ctx in
let tokens = lex default_stt pts in
@@ -1575,7 +1575,7 @@ let sform_identifier ctx loc sargs ot =
match (metavar_lookup idx) with
| MVar (sl',_,_)
-> if sl = sl' then
- (mkMetavar (idx, subst, (loc, Some name)) sinfo, Lazy)
+ (mkMetavar (idx, subst, (loc, Some name)) dummy_sinfo, Lazy)
else
(* FIXME: The variable is from another scope_level! It
means that `subst` is not the right substitution for
@@ -1592,7 +1592,7 @@ let sform_identifier ctx loc sargs ot =
| None -> newMetatype octx sl loc
| Some t
(* `t` is defined in ctx instead of octx. *)
- -> Inverse_subst.apply_inv_subst t subst in
+ -> Inverse_subst.apply_inv_subst t subst dummy_sinfo in
let mv = newMetavar octx sl (loc, Some name) t in
(if not (name = "") then
let idx =
@@ -1600,7 +1600,7 @@ let sform_identifier ctx loc sargs ot =
| Metavar (idx, _, _) -> idx
| _ -> fatal ~loc "newMetavar returned a non-Metavar" in
rmmap := SMap.add name idx (!rmmap));
- (mkSusp mv subst sinfo,
+ (mkSusp mv subst dummy_sinfo,
match ot with Some _ -> Checked | None -> Lazy)
(* Normal identifier. *)
@@ -1625,7 +1625,7 @@ let rec sform_lambda kind ctx loc sargs ot =
((dummy_location, None), None) in
let olt1 = match ost1 with
- | Some st -> Some (infer_type st ctx arg)
+ | Some st -> Some (infer_type st ctx arg dummy_sinfo)
| _ -> None in
let mklam lt1 olt2 =
@@ -1638,9 +1638,9 @@ let rec sform_lambda kind ctx loc sargs ot =
| Some lt2
-> Some (srename arg lt2) in
let (lbody, alt) = elaborate nctx sbody olt2 in
- (mkLambda (kind, arg, lt1, lbody) sinfo,
+ (mkLambda (kind, arg, lt1, lbody) dummy_sinfo,
match alt with
- | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) sinfo)
+ | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) dummy_sinfo)
| _ -> alt) in
(match ot with
@@ -1672,9 +1672,9 @@ let rec sform_lambda kind ctx loc sargs ot =
(* FIXME: Don't go back to sform_lambda, but use an internal
* loop to avoid re-computing olt1 each time. *)
let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in
- (mkLambda (ak2, v, lt1, lam) sinfo,
+ (mkLambda (ak2, v, lt1, lam) dummy_sinfo,
match alt with
- | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') sinfo)
+ | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') dummy_sinfo)
| _ -> alt)
| _lt
@@ -1717,10 +1717,10 @@ let sform_letin ctx loc sargs ot = match sargs with
List.fold_left (fun (s, off) decls ->
(OL.lexp_defs_subst loc s decls, off + List.length decls))
(S.identity, 0) declss in
- let ot = Option.map (fun t -> mkSusp t (S.shift off) sinfo) ot in
+ let ot = Option.map (fun t -> mkSusp t (S.shift off) dummy_sinfo) ot in
let bdy, ot = elaborate nctx sbody ot in
let ot = match ot with
- | Inferred t -> Inferred (mkSusp t s sinfo)
+ | Inferred t -> Inferred (mkSusp t s dummy_sinfo)
| _ -> ot in
(lexp_let_decls declss bdy nctx, ot)
| _ -> sexp_error loc "Unrecognized let_in_ expression";
@@ -1728,10 +1728,10 @@ let sform_letin ctx loc sargs ot = match sargs with
let rec infer_level ctx se : lexp =
match se with
- | Symbol (_, "z") -> mkSortLevel SLz sinfo
+ | Symbol (_, "z") -> mkSortLevel SLz dummy_sinfo
| Symbol _ -> check se type_level ctx
| Node (Symbol (_, "s"), [se])
- -> mkSortLevel (SLsucc (infer_level ctx se)) sinfo
+ -> mkSortLevel (SLsucc (infer_level ctx se)) dummy_sinfo
| Node (Symbol (_, "_∪_"), [se1; se2])
-> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2)
| _ -> let l = (sexp_location se) in
@@ -1747,8 +1747,8 @@ let rec infer_level ctx se : lexp =
let sform_type ctx loc sargs _ot =
match sargs with
| [se] -> let l = infer_level ctx se in
- (mkSort (loc, Stype l) sinfo,
- Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) sinfo)) sinfo))
+ (mkSort (loc, Stype l) dummy_sinfo,
+ Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) dummy_sinfo)) dummy_sinfo))
| _ -> (sexp_error loc "##Type_ expects one argument";
sform_dummy_ret ctx loc)
@@ -1759,7 +1759,7 @@ let sform_debruijn ctx loc sargs _ot =
(sexp_error l "##DeBruijn index out of bounds";
sform_dummy_ret ctx loc)
else
- let lxp = mkVar ((loc, None), i) sinfo in (lxp, Lazy)
+ let lxp = mkVar ((loc, None), i) dummy_sinfo in (lxp, Lazy)
| _ -> (sexp_error loc "##DeBruijn expects one integer argument";
sform_dummy_ret ctx loc)
@@ -1831,7 +1831,7 @@ let sform_load usr_elctx loc sargs _ot =
let tuple' = if !in_pervasive then
tuple
else
- (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) sinfo) in
+ (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) dummy_sinfo) in
(tuple',Lazy)
@@ -1890,7 +1890,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) sinfo in
+ let v = mkVar ((dloc, Some name), idx) dummy_sinfo in
BI.set_predef name v) BI.predef_names;
with Senv_Lookup_Fail _ ->
warning "Predef not found"; in
@@ -1939,7 +1939,7 @@ let lexp_expr_str str ctx =
let source = new Source.source_string str in
let pxps = sexp_parse_source source tenv grm limit in
let lexps = lexp_parse_all pxps ctx in
- List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp))
+ List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp dummy_sinfo))
lexps;
lexps
=====================================
src/eval.ml
=====================================
@@ -421,7 +421,7 @@ let file_write loc _depth args_val = match args_val with
)
"File.write expects an out_channel and a string. Actual arguments:"
-let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) =
+let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info) sinfo : (value_type) =
let trace = append_eval_trace trace lxp in
let eval' lxp ctx = eval lxp ctx trace in
@@ -455,13 +455,13 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type)
(* ---------------- *)
| Let(_, decls, inst)
-> let nctx = eval_decls decls ctx trace in
- eval' inst nctx
+ eval' inst nctx sinfo
(* Function call *)
| Call (f, args)
-> eval_call (elexp_location f) f trace
- (eval f ctx trace)
- (List.map (fun e -> eval e ctx trace) args)
+ (eval f ctx trace sinfo)
+ (List.map (fun e -> eval e ctx trace sinfo) args)
(* Case *)
| Case (loc, target, pat, dflt)
@@ -510,8 +510,8 @@ and eval_call loc unef i f args =
-> bindargs e vs (add_rte_variable x v ctx)
| ([], _) ->
let trace = append_typer_trace i unef in
- eval e ctx trace
- | _ -> eval_call loc unef i (eval e ctx i) vs in
+ eval e ctx trace dummy_sinfo
+ | _ -> eval_call loc unef i (eval e ctx i dummy_sinfo) vs in
bindargs e vs (add_rte_variable x v ctx)
| Vbuiltin (name), args
@@ -553,12 +553,12 @@ 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) sinfo)]) sinfo)
+ -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) dummy_sinfo)]) dummy_sinfo)
| _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f)
and eval_case ctx i loc target pat dflt =
(* Eval target *)
- let v = eval target ctx i in
+ let v = eval target ctx i dummy_sinfo in
(* extract constructor name and arguments *)
let ctor_name, args = match v with
@@ -586,17 +586,17 @@ and eval_case ctx i loc target pat dflt =
| [], [] -> nctx in
let nctx = fold2 ctx pat_args args in
- eval exp nctx i
+ eval exp nctx i dummy_sinfo
(* Run default *)
with Not_found -> (match dflt with
| Some (var, lxp)
- -> eval lxp (add_rte_variable var v ctx) i
+ -> eval lxp (add_rte_variable var v ctx) i dummy_sinfo
| _ -> error loc "Match Failure")
and build_arg_list args ctx i =
(* eval every args *)
- let arg_val = List.map (fun (_k, e) -> eval e ctx i) args in
+ let arg_val = List.map (fun (_k, e) -> eval e ctx i dummy_sinfo) args in
(* Add args inside context *)
List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val
@@ -611,7 +611,7 @@ and eval_decls (decls: (vname * elexp) list)
add_rte_variable name Vundefined ctx) ctx decls in
List.iteri (fun idx (name, lxp) ->
- let v = eval lxp nctx i in
+ let v = eval lxp nctx i dummy_sinfo in
let offset = n - idx in
ignore (set_rte_variable offset name v nctx)) decls;
@@ -798,7 +798,7 @@ let is_bound loc _depth args_val = match args_val with
with Senv_Lookup_Fail _ -> false)
| _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments"
-let constructor_p name ectx =
+let constructor_p name ectx sinfo =
try let idx = senv_lookup name ectx in
(* Use `lexp_whnf` so that `name` can be indirectly
* defined as a constructor
@@ -817,7 +817,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) sinfo) (ectx_to_lctx ectx) with
+ match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_sinfo) (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
@@ -838,7 +838,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) sinfo) (ectx_to_lctx ectx) with
+ match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx) dummy_sinfo) (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
@@ -856,7 +856,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) sinfo) (ectx_to_lctx ectx) with
+ match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_sinfo) (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
@@ -877,7 +877,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) sinfo) (ectx_to_lctx ectx) with
+ match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_sinfo) (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
@@ -887,7 +887,7 @@ let ctor_arg_pos name arg ectx =
with Senv_Lookup_Fail _ -> (-1)
let is_constructor loc _depth args_val = match args_val with
- | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx)
+ | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx dummy_sinfo)
| _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"
let is_nth_erasable loc _depth args_val = match args_val with
@@ -1151,7 +1151,7 @@ let from_lctx (lctx: lexp_context): runtime_env =
ref (match def with
| LetDef (_, e)
-> if closed_p rctx (OL.fv e) then
- eval (OL.erase_type lctx e) rctx
+ eval (OL.erase_type lctx e) rctx dummy_sinfo
else Vundefined
| _ -> Vundefined))
rctx
@@ -1173,7 +1173,7 @@ let from_lctx (lctx: lexp_context): runtime_env =
* are present! *)
let lctx' = DB.lctx_extend_rec lctx defs in
if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then
- List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs
+ List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx dummy_sinfo) evs
else () in
nrctx
and from_lctx lctx =
@@ -1201,7 +1201,7 @@ class ast_interpreter lctx = object
method eval_expr lexp =
let elexp = Opslexp.erase_type lctx lexp in
- debug_eval elexp rctx
+ debug_eval elexp rctx dummy_sinfo
method print_rte_ctx = Env.print_rte_ctx rctx
=====================================
src/heap.ml
=====================================
@@ -39,8 +39,8 @@ let error ~(loc : location) ?print_action fmt =
let dloc = Util.dummy_location
let type0 = Debruijn.type0
-let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) sinfo
-let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) sinfo
+let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) dummy_sinfo
+let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) dummy_sinfo
let next_free_address : addr ref = ref 1
=====================================
src/inverse_subst.ml
=====================================
@@ -56,7 +56,7 @@ type substIR = ((int * int) list * int * int)
(** Transform a substitution to a more linear substitution
* makes the inversion easier
* Example of result : ((new_idx, old_position)::..., shift)*)
-let transfo (s: subst) : substIR option =
+let transfo (s: subst) : substIR option =
let rec transfo (s: subst) (off_acc: int) (idx: int) (imp_cnt : int)
: substIR option =
let indexOf (v: lexp): int = (* Helper : return the index of a variabble *)
@@ -65,7 +65,7 @@ let transfo (s: subst) : substIR option =
| _ -> assert false
in
let shiftVar (var: lexp) (offset: int): int =
- indexOf (mkSusp var (S.shift offset) sinfo) (* Helper : shift the index of a var *)
+ indexOf (mkSusp var (S.shift offset) dummy_sinfo) (* Helper : shift the index of a var *)
in
match s with
| S.Cons (e, s, o) when is_var e
@@ -94,7 +94,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) sinfo
+ mkVar ((U.dummy_location, None), idx) dummy_sinfo
(** Fill the gap between e_i in the list of couple (e_i, i) by adding
dummy variables.
@@ -242,7 +242,7 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with
| S.Cons (e, s', o) ->
let s = shift_inv_subst o s in
(* FIXME: Why don't we ever return a Shift? *)
- S.cons (apply_inv_subst e s) (compose_inv_subst s' s)
+ S.cons (apply_inv_subst e s dummy_sinfo) (compose_inv_subst s' s)
| S.Identity o -> (match inverse (shift_inv_subst o s) with
| Some s -> s
(* FIXME: could also be Ambiguous, depending on `s`. *)
@@ -252,66 +252,66 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with
* The function presumes that `invertible s` was true.
* This can be used like mkSusp/push_susp, but it's not lazy.
* This is because it can signal errors Not_invertible or Ambiguous. *)
-and apply_inv_subst (e : lexp) (s : subst) : lexp =
+and apply_inv_subst (e : lexp) (s : subst) sinfo : lexp =
match lexp_lexp' e with
| Imm _ -> e
| SortLevel (SLz) -> e
- | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) sinfo
+ | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s dummy_sinfo)) sinfo
| SortLevel (SLlub (e1, e2))
(* FIXME: use mkSLlub? *)
- -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) sinfo
- | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) sinfo
+ -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s dummy_sinfo, apply_inv_subst e2 s dummy_sinfo)) sinfo
+ | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s dummy_sinfo)) sinfo
| Sort (_l, (StypeOmega | StypeLevel)) -> e
| Builtin _ -> e
| Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) sinfo
- | Susp (e, s') -> apply_inv_subst (push_susp e s') s
+ | Susp (e, s') -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo
| Let (l, defs, e)
- -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
+ -> let s' = L.fold_left (fun s (v, _, _) -> ssink dummy_sinfo v s) s defs in
let (_,ndefs)
= L.fold_left (fun (s,ndefs) (v, def, ty)
- -> (ssink v s,
- (v, apply_inv_subst def s', apply_inv_subst ty s)
+ -> (ssink dummy_sinfo v s,
+ (v, apply_inv_subst def s' dummy_sinfo, apply_inv_subst ty s dummy_sinfo)
:: ndefs))
(s, []) defs in
- mkLet (l, ndefs, apply_inv_subst e s') sinfo
+ mkLet (l, ndefs, apply_inv_subst e s' dummy_sinfo) sinfo
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, apply_inv_subst t1 s, l,
- apply_inv_subst t2 (ssink v s)) sinfo
+ -> mkArrow (ak, v, apply_inv_subst t1 s dummy_sinfo, l,
+ apply_inv_subst t2 (ssink dummy_sinfo v s) dummy_sinfo) sinfo
| Lambda (ak, v, t, e)
- -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) sinfo
+ -> mkLambda (ak, v, apply_inv_subst t s dummy_sinfo, apply_inv_subst e (ssink dummy_sinfo v s) dummy_sinfo) sinfo
| Call (f, args)
- -> mkCall (apply_inv_subst f s,
- L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) sinfo
+ -> mkCall (apply_inv_subst f s dummy_sinfo,
+ L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s dummy_sinfo)) args) sinfo
| Inductive (l, label, args, cases)
-> let (s, nargs)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs))
+ -> (ssink dummy_sinfo v s, (ak, v, apply_inv_subst t s dummy_sinfo) :: nargs))
(s, []) args in
let nargs = List.rev nargs in
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink v s,
- (ak, v, apply_inv_subst t s)
+ -> (ssink dummy_sinfo v s,
+ (ak, v, apply_inv_subst t s dummy_sinfo)
:: nargs))
(s, []) args in
L.rev ncase)
cases in
mkInductive (l, label, nargs, ncases) sinfo
- | Cons (it, name) -> mkCons (apply_inv_subst it s, name) sinfo
+ | Cons (it, name) -> mkCons (apply_inv_subst it s dummy_sinfo, name) sinfo
| Case (l, e, ret, cases, default)
- -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,
+ -> mkCase (l, apply_inv_subst e s dummy_sinfo, apply_inv_subst ret s dummy_sinfo,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink ov s)
+ (fun s (_,ov) -> ssink dummy_sinfo ov s)
s cargs in
- let s'' = ssink (l, None) s' in
- (l, cargs, apply_inv_subst e s''))
+ let s'' = ssink dummy_sinfo (l, None) s' in
+ (l, cargs, apply_inv_subst e s'' dummy_sinfo ))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) sinfo
+ | Some (v,e) -> Some (v, apply_inv_subst e (ssink dummy_sinfo (l, None) (ssink dummy_sinfo v s)) dummy_sinfo)) sinfo
| Metavar (id, s', name)
-> match metavar_lookup id with
- | MVal e -> apply_inv_subst (push_susp e s') s
+ | MVal e -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo
| MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) sinfo
=====================================
src/lexp.ml
=====================================
@@ -36,12 +36,14 @@ module S = Subst
type vname = U.vname
type vref = U.vref
type meta_id = int (* Identifier of a meta variable. *)
+type sinfo = sexp list
type label = symbol
include Pexp.ArgKind
-let sinfo: (sexp list) = []
+
+let dummy_sinfo : sexp list = []
(*************** Elaboration to Lexp *********************)
@@ -61,7 +63,7 @@ let sinfo: (sexp list) = []
type ltype = lexp
and subst = lexp S.subst
(* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *)
- and lexp = lexp' * int * sexp list
+ and lexp = lexp' * int * sinfo
and lexp' =
| Imm of sexp (* Used for strings, ... *)
| SortLevel of sort_level
@@ -324,7 +326,7 @@ let mkCall (f, es) sinfo =
| _, [] -> f
| _ -> hc (Call (f, es)) sinfo
-let impossible = mkImm Sexp.dummy_epsilon Sexp.dummy_sinfo
+let impossible = mkImm Sexp.dummy_epsilon []
let lexp_head e =
match lexp_lexp' e with
@@ -449,21 +451,22 @@ let rec mkSusp e s sinfo =
match lexp_lexp' e with
| Imm _ -> e
| Builtin _ -> e
- | Susp (e, s') -> mkSusp_memo e (scompose s' s)
- | Var (l, v) -> slookup s l v
- | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) sinfo
+ | Susp (e, s') -> mkSusp_memo e (scompose s' s )
+ | Var (l, v) -> slookup s l v sinfo
+ | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s , vd) sinfo
| _ -> hc (Susp (e, s)) sinfo
and mkSusp_memo e s
= if Hashtbl.mem hcs_table (e, s)
then Hashtbl.find hcs_table (e, s)
- else let res = mkSusp e s sinfo in
- Hashtbl.add hcs_table (e, s) res;
- res
-and scompose s1 s2 = S.compose mkSusp_memo s1 s2
-and slookup s l v = S.lookup (fun l i -> mkVar (l, i) sinfo)
- (fun e o -> mkSusp e (S.shift o) sinfo)
+ else let res = mkSusp e s [] in
+ Hashtbl.add hcs_table (e, s) res;
+ res
+
+and scompose s1 s2 = S.compose mkSusp_memo s1 s2
+and slookup s l v sinfo = S.lookup (fun l i -> mkVar (l, i) sinfo)
+ (fun e o -> mkSusp e (S.shift o) sinfo)
s l v
-let ssink = S.sink (fun l i -> mkVar (l, i) sinfo)
+let ssink sinfo = S.sink (fun l i -> mkVar (l, i) sinfo)
(* Apply a "dummy" substitution which replace #0 with #0
* in order to account for changes to a variable's name.
@@ -472,7 +475,7 @@ let ssink = S.sink (fun l i -> mkVar (l, i) sinfo)
* one stored in the lctx!
* Using DeBruijn *should* make α-renaming unnecessary
* so this is a real PITA! :-( *)
-let srename name le = mkSusp le (S.cons (mkVar (name, 0) sinfo) (S.shift 1)) sinfo
+let srename name le = mkSusp le (S.cons (mkVar (name, 0) dummy_sinfo) (S.shift 1)) dummy_sinfo
(* Shift by a negative amount! *)
let rec sunshift n =
@@ -534,11 +537,11 @@ let vdummy = (U.dummy_location, None)
let maybename n = match n with None -> "<anon>" | Some v -> v
let sname (l,n) = (l, maybename n)
-let rec push_susp e s = (* Push a suspension one level down. *)
+let rec push_susp e s sinfo = (* Push a suspension one level down. *)
match lexp_lexp' e with
| Imm _ -> e
| SortLevel (SLz) -> e
- | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo
+ | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo
| SortLevel (SLlub (e1, e2))
-> mkSortLevel (mkSLlub' (mkSusp e1 s sinfo, mkSusp e2 s sinfo)) sinfo
| Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s sinfo)) sinfo
@@ -546,26 +549,26 @@ let rec push_susp e s = (* Push a suspension one level down. *)
| Builtin _ -> e
| Let (l, defs, e)
- -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
+ -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in
let rec loop s defs = match defs with
| [] -> []
| (v, def, ty) :: defs
- -> (v, mkSusp def s' sinfo, mkSusp ty s sinfo) :: loop (ssink v s) defs in
+ -> (v, mkSusp def s' sinfo, mkSusp ty s sinfo) :: loop (ssink sinfo v s) defs in
mkLet (l, loop s defs, mkSusp e s' sinfo) sinfo
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, mkSusp t1 s sinfo, l, mkSusp t2 (ssink v s) sinfo) sinfo
- | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s sinfo, mkSusp e (ssink v s) sinfo) sinfo
+ -> mkArrow (ak, v, mkSusp t1 s sinfo, l, mkSusp t2 (ssink sinfo v s) sinfo) sinfo
+ | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s sinfo, mkSusp e (ssink sinfo v s) sinfo) sinfo
| Call (f, args) -> mkCall (mkSusp f s sinfo,
L.map (fun (ak, arg) -> (ak, mkSusp arg s sinfo)) args) sinfo
| Inductive (l, label, args, cases)
-> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink v s, (ak, v, mkSusp t s sinfo) :: nargs))
+ -> (ssink sinfo v s, (ak, v, mkSusp t s sinfo) :: nargs))
(s, []) args in
let nargs = List.rev nargs in
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink v s,
+ -> (ssink sinfo v s,
(ak, v, mkSusp t s sinfo)
:: nargs))
(s, []) args in
@@ -577,30 +580,30 @@ let rec push_susp e s = (* Push a suspension one level down. *)
-> mkCase (l, mkSusp e s sinfo, mkSusp ret s sinfo,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink ov s)
+ (fun s (_,ov) -> ssink sinfo ov s)
s cargs in
- (l, cargs, mkSusp e (ssink (l, None) s') sinfo))
+ (l, cargs, mkSusp e (ssink sinfo (l, None) s') sinfo))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)) sinfo)) sinfo
+ | Some (v,e) -> Some (v, mkSusp e (ssink sinfo (l, None) (ssink sinfo v s)) sinfo)) sinfo
(* Susp should never appear around Var/Susp/Metavar because mkSusp
* pushes the subst into them eagerly. IOW if there's a Susp(Var..)
* or Susp(Metavar..) it's because some chunk of code should use mkSusp
* rather than Susp.
* But we still have to handle them here, since push_susp is called
* in many other cases than just when we bump into a Susp. *)
- | Susp (e,s') -> push_susp e (scompose s' s)
+ | Susp (e,s') -> push_susp e (scompose s' s) sinfo
| (Var _ | Metavar _) -> nosusp (mkSusp e s sinfo)
-and nosusp e = (* Return `e` with no outermost `Susp`. *)
+and nosusp (e: lexp ) = (* Return `e` with no outermost `Susp`. *)
match lexp_lexp' e with
- | Susp(e, s) -> push_susp e s
+ | Susp(e, s) -> push_susp e s dummy_sinfo
| _ -> e
(* Get rid of `Susp`ensions and instantiated `Metavar`s. *)
-let clean e =
+let clean e sinfo =
let rec clean s e =
match lexp_lexp' e with
| Imm _ -> e
@@ -613,26 +616,26 @@ let clean e =
| Sort (_, _) -> e
| Builtin _ -> e
| Let (l, defs, e)
- -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
+ -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in
let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty)
- -> (ssink v s,
+ -> (ssink sinfo v s,
(v, clean s' def, clean s ty) :: ndefs))
(s, []) defs in
mkLet (l, ndefs, clean s' e) sinfo
| Arrow (ak, v, t1, l, t2)
- -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) sinfo
- | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) sinfo
+ -> mkArrow (ak, v, clean s t1, l, clean (ssink sinfo v s) t2) sinfo
+ | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink sinfo v s) e) sinfo
| Call (f, args) -> mkCall (clean s f,
L.map (fun (ak, arg) -> (ak, clean s arg)) args) sinfo
| Inductive (l, label, args, cases)
-> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink v s, (ak, v, clean s t) :: nargs))
+ -> (ssink sinfo v s, (ak, v, clean s t) :: nargs))
(s, []) args in
let nargs = List.rev nargs in
let ncases = SMap.map (fun args
-> let (_, ncase)
= L.fold_left (fun (s, nargs) (ak, v, t)
- -> (ssink v s,
+ -> (ssink sinfo v s,
(ak, v, clean s t)
:: nargs))
(s, []) args in
@@ -644,14 +647,14 @@ let clean e =
-> mkCase (l, clean s e, clean s ret,
SMap.map (fun (l, cargs, e)
-> let s' = L.fold_left
- (fun s (_,ov) -> ssink ov s)
+ (fun s (_,ov) -> ssink sinfo ov s)
s cargs in
- let s'' = ssink (l, None) s' in
+ let s'' = ssink sinfo (l, None) s' in
(l, cargs, clean s'' e))
cases,
match default with
| None -> default
- | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) sinfo
+ | Some (v,e) -> Some (v, clean (ssink sinfo (l, None) (ssink sinfo v s)) e)) sinfo
| Susp (e, s') -> clean (scompose s' s) e
| Var _ -> if S.identity_p s then e
else clean S.identity (mkSusp e s sinfo)
@@ -666,9 +669,9 @@ let sdatacons = Symbol (U.dummy_location, "##datacons")
let stypecons = Symbol (U.dummy_location, "##typecons")
(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *)
-let rec lexp_unparse lxp =
+let rec lexp_unparse lxp =
match lexp_lexp' lxp with
- | Susp _ -> lexp_unparse (nosusp lxp)
+ | Susp _ -> lexp_unparse (nosusp lxp )
| Imm (sexp) -> sexp
| Builtin ((l,name), _) -> Symbol (l, "##" ^ name)
(* FIXME: Add a Sexp syntax for debindex references. *)
@@ -684,33 +687,33 @@ let rec lexp_unparse lxp =
| Aimplicit -> "lambda_=>_"
| Aerasable -> "lambda_≡>_"),
[Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]);
- lexp_unparse body])
+ lexp_unparse body ])
| Arrow (arg_kind, (l,oname), ltp1, loc, ltp2)
- -> let ut1 = lexp_unparse ltp1 in
+ -> let ut1 = lexp_unparse ltp1 in
Node (Symbol (loc, match arg_kind with Anormal -> "_->_"
| Aimplicit -> "_=>_"
| Aerasable -> "_≡>_"),
[(match oname with None -> ut1
| Some v -> Node (Symbol (l, "_:_"),
[Symbol (l,v); ut1]));
- lexp_unparse ltp2])
+ lexp_unparse ltp2 ])
| Let (loc, ldecls, body)
-> (* (vdef * lexp * ltype) list *)
let sdecls = List.fold_left
(fun acc (vdef, lxp, ltp)
-> Node (Symbol (U.dummy_location, "_=_"),
- [Symbol (sname vdef); lexp_unparse ltp])
+ [Symbol (sname vdef); lexp_unparse ltp ])
:: Node (Symbol (U.dummy_location, "_=_"),
- [Symbol (sname vdef); lexp_unparse lxp])
+ [Symbol (sname vdef); lexp_unparse lxp ])
:: acc)
[] ldecls in
Node (Symbol (loc, "let_in_"),
[Node (Symbol (U.dummy_location, "_;_"), sdecls);
- lexp_unparse body])
+ lexp_unparse body ])
| Call(lxp, largs) -> (* (arg_kind * lexp) list *)
- let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in
+ let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem ) largs in
Node (lexp_unparse lxp, sargs)
| Inductive(loc, label, lfargs, ctors) ->
@@ -734,12 +737,12 @@ let rec lexp_unparse lxp =
| Anormal -> "_:_"
| Aimplicit -> "_::_"
| Aerasable -> "_:::_"),
- [Symbol id; lexp_unparse t]))
+ [Symbol id; lexp_unparse t ]))
types))
(SMap.bindings ctors))
| Case (loc, target, bltp, branches, default) ->
- let bt = lexp_unparse bltp in
+ let bt = lexp_unparse bltp in
let pbranch = List.map (fun (str, (loc, args, bch)) ->
match args with
| [] -> Ppatsym (loc, Some str), lexp_unparse bch
@@ -755,14 +758,14 @@ let rec lexp_unparse lxp =
in (Ppatcons (Node (sdatacons,
[bt; Symbol (loc, str)]),
pat_args),
- lexp_unparse bch)
+ lexp_unparse bch )
) (SMap.bindings branches) in
let pbranch = match default with
| Some (v,dft) -> (Ppatsym v,
- lexp_unparse dft)::pbranch
+ lexp_unparse dft )::pbranch
| None -> pbranch
- in let e = lexp_unparse target in
+ in let e = lexp_unparse target in
Node (Symbol (loc, "case_"),
e :: List.map
(fun (pat, branch) ->
@@ -781,15 +784,15 @@ let rec lexp_unparse lxp =
[lexp_unparse l])
| SortLevel (SLlub (l1, l2))
-> Node (Symbol (lexp_location l1, "##TypeLevel.∪"),
- [lexp_unparse l1; lexp_unparse l2])
+ [lexp_unparse l1 ; lexp_unparse l2 ])
| Sort (l, StypeOmega) -> Symbol (l, "##Type_ω")
| Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort")
| Sort (_l, Stype sl)
-> Node (Symbol (lexp_location sl, "##Type_"),
- [lexp_unparse sl])
+ [lexp_unparse sl ])
(* FIXME: ¡Unify lexp_print and lexp_string! *)
-and lexp_string lxp = sexp_string (lexp_unparse lxp)
+and lexp_string lxp = sexp_string (lexp_unparse lxp )
and subst_string s = match s with
| S.Identity o -> "↑" ^ string_of_int o
@@ -797,7 +800,7 @@ and subst_string s = match s with
| S.Cons (l, s, o)
-> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"
-and lexp_name e =
+and lexp_name e =
match lexp_lexp' e with
| Imm _ -> lexp_string e
| Var _ -> lexp_string e
@@ -905,19 +908,19 @@ let rec get_precedence expr ctx =
(* Printing Functions
* ========================================== *)
-let rec lexp_print e = print_string (lexp_string e)
-and lexp_string e = lexp_cstring (!debug_ppctx) e
+let rec lexp_print e = print_string (lexp_string e )
+and lexp_string e = lexp_cstring (!debug_ppctx) e
(* Context Print *)
-and lexp_cprint ctx e = print_string (lexp_cstring ctx e)
-and lexp_cstring ctx e = lexp_str ctx e
+and lexp_cprint ctx e = print_string (lexp_cstring ctx e )
+and lexp_cstring ctx e = lexp_str ctx e dummy_sinfo
(* Implementation *)
-and lexp_str ctx (exp : lexp) : string =
+and lexp_str ctx (exp : lexp) sinfo : string =
- let inter_ctx = add_indent ctx 1 in
- let lexp_str' = lexp_str ctx in
- let lexp_stri idt e = lexp_str (add_indent ctx idt) e in
+ let inter_ctx = add_indent ctx 1 in
+ let lexp_str' sinfo = lexp_str ctx sinfo in
+ let lexp_stri idt e sinfo = lexp_str (add_indent ctx idt) e sinfo in
let pretty = pp_pretty ctx in
let color = pp_color ctx in
@@ -971,15 +974,15 @@ and lexp_str ctx (exp : lexp) : string =
| Float (_, s) -> tval (string_of_float s)
| e -> sexp_string e)
- | Susp (e, s) -> lexp_str ctx (push_susp e s)
+ | Susp (e, s) -> lexp_str ctx (push_susp e s sinfo) sinfo
| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;
| Metavar (idx, subst, (_loc, name))
(* print metavar result if any *)
-> (match metavar_lookup idx with
- | MVal e -> lexp_str ctx (push_susp e subst)
- | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))
+ | MVal e -> lexp_str ctx (push_susp e subst sinfo) sinfo
+ | _ -> "?" ^ maybename name ^ (subst_string subst ) ^ (index idx))
| Let (_, decls, body) ->
(* Print first decls without indent *)
@@ -998,35 +1001,35 @@ and lexp_str ctx (exp : lexp) : string =
else decls in
(keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^
- (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)
+ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body sinfo)
| Arrow(k, (_, Some name), tp, _loc, expr) ->
- "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^
- (kind_str k) ^ " " ^ (lexp_str' expr)
+ "(" ^ name ^ " : " ^ (lexp_str' tp sinfo) ^ ") " ^
+ (kind_str k) ^ " " ^ (lexp_str' expr sinfo)
| Arrow(k, (_, None), tp, _loc, expr) ->
- "(" ^ (lexp_str' tp) ^ " "
- ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")"
+ "(" ^ (lexp_str' tp sinfo) ^ " "
+ ^ (kind_str k) ^ " " ^ (lexp_str' expr sinfo) ^ ")"
| Lambda(k, (_loc, name), ltype, lbody) ->
- let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in
+ let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype sinfo) ^ ")" in
(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^
- (make_indent 1) ^ (lexp_stri 1 lbody)
+ (make_indent 1) ^ (lexp_stri 1 lbody sinfo)
| Cons(t, (_, ctor_name)) ->
- (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name
+ (keyword "datacons ") ^ (lexp_str' t sinfo) ^ " " ^ ctor_name
| 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
+ "(" ^ (lexp_str' lhs sinfo) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs sinfo) ^ ")" in
let print_arg str (arg_type, lxp) =
match arg_type with
- | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp)
- | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp)
- | Anormal -> str ^ " " ^ (lexp_str' lxp)
+ | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp sinfo)
+ | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp sinfo)
+ | Anormal -> str ^ " " ^ (lexp_str' lxp sinfo)
| _ -> str in (
match args with
@@ -1034,7 +1037,7 @@ and lexp_str ctx (exp : lexp) : string =
binop_str (" " ^ (get_binary_op_name name)) lhs rhs
| _ -> let args = List.fold_left print_arg "" args in
- "(" ^ (lexp_str' fname) ^ args ^ ")")
+ "(" ^ (lexp_str' fname sinfo) ^ args ^ ")")
| Inductive (_, (_, name), [], ctors) ->
(keyword "typecons") ^ " (" ^ name ^") " ^ newline ^
@@ -1045,14 +1048,14 @@ and lexp_str ctx (exp : lexp) : string =
= List.fold_left
(fun str (arg_kind, (_, name), ltype)
-> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " "
- ^ (lexp_str' ltype) ^ ")")
+ ^ (lexp_str' ltype sinfo) ^ ")")
"" args in
(keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^
- (lexp_str_ctor ctx ctors)
+ (lexp_str_ctor ctx ctors )
| Case (_, target, _ret, map, dflt) ->(
- let str = (keyword "case ") ^ (lexp_str' target) in
+ let str = (keyword "case ") ^ (lexp_str' target sinfo) in
let arg_str arg
= List.fold_left (fun str v
-> match v with
@@ -1062,7 +1065,7 @@ and lexp_str ctx (exp : lexp) : string =
let str = SMap.fold (fun k (_, arg, exp) str ->
str ^ nl ^ (make_indent 1) ^
- "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp))
+ "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp sinfo))
map str in
match dflt with
@@ -1071,7 +1074,7 @@ and lexp_str ctx (exp : lexp) : string =
str ^ nl ^ (make_indent 1)
^ "| " ^ (match v with (_, None) -> "_"
| (_, Some name) -> name)
- ^ " => " ^ (lexp_stri 1 df))
+ ^ " => " ^ (lexp_stri 1 df sinfo))
| Builtin ((_, name), _) -> "##" ^ name
@@ -1079,9 +1082,9 @@ and lexp_str ctx (exp : lexp) : string =
| Sort (_, StypeOmega) -> "##Type_ω"
| SortLevel (SLz) -> "##TypeLevel.z"
- | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")"
+ | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")"
| SortLevel (SLlub (e1, e2))
- -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"
+ -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"
| Sort (_, Stype l)
-> match lexp_lexp' l with
@@ -1100,7 +1103,7 @@ and lexp_str_ctor ctx ctors =
SMap.fold (fun key value str
-> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in
let str = List.fold_left (fun str (_k, _, arg)
- -> str ^ " " ^ (lexp_str ctx arg))
+ -> str ^ " " ^ (lexp_str ctx arg dummy_sinfo))
str value in
str ^ ")")
ctors ""
@@ -1111,87 +1114,87 @@ and lexp_str_decls ctx decls =
let sepdecl = (if pp_decl ctx then "\n" else "") in
let type_str name lxp = (if pp_type ctx then (
- name ^ " : " ^ (lexp_str' lxp) ^ ";") else "") in
+ name ^ " : " ^ (lexp_str' lxp dummy_sinfo) ^ ";") else "") in
let ret = List.fold_left
(fun str ((_, name), lxp, ltp)
-> let name = maybename name in
let str = if pp_type ctx then (type_str name ltp)::str else str in
- (name ^ " = " ^ (lexp_str' lxp) ^ ";" ^ sepdecl)::str)
+ (name ^ " = " ^ (lexp_str' lxp dummy_sinfo) ^ ";" ^ sepdecl)::str)
[] decls in
List.rev ret
(** Syntactic equality (i.e. without β). *******)
-let rec eq e1 e2 =
+let rec eq e1 e2 =
try e1 == e2 ||
match (lexp_lexp' e1, lexp_lexp' e2) with
| (Imm s1, Imm s2) -> sexp_equal s1 s2
| (SortLevel SLz, SortLevel SLz) -> true
| (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2
| (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22)))
- -> eq e11 e12 && eq e21 e22
+ -> eq e11 e12 && eq e21 e22
| (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true
| (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true
| (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2
| (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2
| (Var (_, i1), Var (_, i2)) -> i1 = i2
- | (Susp (e1, s1), _) -> eq (push_susp e1 s1) e2
- | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2)
+ | (Susp (e1, s1), _) -> eq (push_susp e1 s1 dummy_sinfo) e2
+ | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2 dummy_sinfo)
| (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
+ -> 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))
- -> ak1 = ak2 && eq t11 t12 && eq t21 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
+ -> ak1 = ak2 && eq t1 t2 && eq e1 e2
| (Call (e1, as1), Call (e2, as2))
- -> eq e1 e2 && List.for_all2
- (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 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))
-> l1 = l2 && List.for_all2
- (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2
+ (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2 ) as1 as2
&& SMap.equal (List.for_all2
- (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2
- | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2
+ (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2 )) ctor1 ctor2
+ | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2
| (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2))
- -> eq e1 e2 && eq r1 r2 && SMap.equal
- (fun (_, fields1, e1) (_, fields2, e2) -> eq e1 e2 && List.for_all2
+ -> eq e1 e2 && eq r1 r2 && SMap.equal
+ (fun (_, fields1, e1) (_, fields2, e2) -> eq e1 e2 && List.for_all2
(fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) ctor1 ctor2
&& (match (def1, def2) with
| (Some (_, e1), Some (_, e2)) -> eq e1 e2
| _ -> def1 = def2)
| (Metavar (i1, s1, _), Metavar (i2, s2, _))
- -> if i1 == i2 then subst_eq s1 s2 else
+ -> if i1 == i2 then subst_eq s1 s2 else
(match (metavar_lookup i1, metavar_lookup i2) with
- | (MVal l, _) -> eq (push_susp l s1) e2
- | (_, MVal l) -> eq e1 (push_susp l s2)
+ | (MVal l, _) -> eq (push_susp l s1 dummy_sinfo) e2
+ | (_, MVal l) -> eq e1 (push_susp l s2 dummy_sinfo)
| _ -> false)
| (Metavar (i1, s1, _), _)
-> (match metavar_lookup i1 with
- | MVal l -> eq (push_susp l s1) e2
+ | MVal l -> eq (push_susp l s1 dummy_sinfo) e2
| _ -> false)
| (_, Metavar (i2, s2, _))
-> (match metavar_lookup i2 with
- | MVal l -> eq e1 (push_susp l s2)
+ | MVal l -> eq e1 (push_susp l s2 dummy_sinfo)
| _ -> false)
| _ -> false
with
| Invalid_argument _ -> false (* Different lengths in List.for_all2. *)
-and subst_eq s1 s2 =
+and subst_eq s1 s2 =
s1 == s2 ||
match (s1, s2) with
| (S.Identity o1, S.Identity o2) -> o1 = o2
| (S.Cons (e1, s1, o1), S.Cons (e2, s2, o2))
-> if o1 = o2 then
- eq e1 e2 && subst_eq s1 s2
+ eq e1 e2 && subst_eq s1 s2
else if o1 > o2 then
let o = o1 - o2 in
- eq (mkSusp e1 (S.shift o) sinfo) e2
+ eq (mkSusp e1 (S.shift o) dummy_sinfo) e2
&& subst_eq (S.mkShift s1 o) s2
else
let o = o2 - o1 in
- eq e1 (mkSusp e2 (S.shift o) sinfo)
+ eq e1 (mkSusp e2 (S.shift o) dummy_sinfo)
&& subst_eq s1 (S.mkShift s2 o)
| _ -> false
=====================================
src/opslexp.ml
=====================================
@@ -108,7 +108,7 @@ let lookup_value = DB.lctx_lookup_value
let rec lexp_defs_subst l s defs = match defs with
| [] -> s
| (_, lexp, _) :: defs'
- -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) sinfo) s) defs'
+ -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) dummy_sinfo) s) defs'
(** Convert a lexp_context into a substitution. *)
@@ -124,7 +124,7 @@ let rec lctx_to_subst lctx =
* Another option would be to map them to `L.impossible`,
* hence making the target domain be empty (i.e. making the substitution
* generate closed results). *)
- L.ssink v s
+ L.ssink dummy_sinfo v s
| DB.CVfix (defs, lctx)
-> let s1 = lctx_to_subst lctx in
let s2 = lexp_defs_subst DB.dloc S.identity
@@ -142,7 +142,7 @@ let lexp_close lctx e =
* - It turns the lctx (of O(log N) access time) into a subst
* (of O(N) access time)
* Oh well! *)
- mkSusp e (lctx_to_subst lctx) sinfo
+ mkSusp e (lctx_to_subst lctx) dummy_sinfo
(** Reduce to weak head normal form.
@@ -167,26 +167,26 @@ let lexp_close lctx e =
the inductive type of the target (and it's typelevel). A better
solution would be to add these values as annotations in the lexp
datatype. *)
-let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
- let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
+let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : lexp =
+ let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo: lexp =
match lexp_lexp' e with
| Var v -> (match lookup_value ctx v with
| None -> e
(* We can do this blindly even for recursive definitions!
* IOW the risk of inf-looping should only show up when doing
* things like full normalization (e.g. lexp_conv_p). *)
- | Some e' -> lexp_whnf_aux e' ctx)
- | Susp (e, s) -> lexp_whnf_aux (push_susp e s) ctx
- | Call (e, []) -> lexp_whnf_aux e ctx
+ | Some e' -> lexp_whnf_aux e' ctx sinfo)
+ | Susp (e, s) -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo
+ | Call (e, []) -> lexp_whnf_aux e ctx sinfo
| Call (f, (((_, arg)::args) as xs)) ->
- (match lexp_lexp' (lexp_whnf_aux f ctx) with
+ (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) 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_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx)),
- args) sinfo)
- ctx
+ lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx dummy_sinfo)) dummy_sinfo,
+ args) dummy_sinfo)
+ ctx sinfo
| Call (f', xs1) -> mkCall (f', List.append xs1 xs) sinfo
| Builtin ((_, name), _)
-> (match SMap.find_opt name (!reducible_builtins) with
@@ -194,7 +194,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
| None -> e)
| _ -> e) (* Keep `e`, assuming it's more readable! *)
| Case (l, e, rt, branches, default) ->
- let e' = lexp_whnf_aux e ctx in
+ let e' = lexp_whnf_aux e ctx sinfo in
let get_refl e =
let etype = get_type ctx e in (* FIXME we should not need get_type here *)
let elevel = match lexp'_whnf (get_type ctx etype) ctx with
@@ -203,9 +203,9 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
mkCall (DB.eq_refl,
[L.Aerasable, elevel;
L.Aerasable, etype;
- L.Aerasable, e]) sinfo in
+ L.Aerasable, e]) dummy_sinfo in
let reduce it name aargs =
- let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with
+ let targs = match lexp_lexp' (lexp_whnf_aux it ctx dummy_sinfo) with
| Inductive (_,_,fargs,_) -> fargs
| _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in
try
@@ -214,7 +214,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
= List.fold_left
(fun (s, targs) (_, arg) ->
match targs with
- | [] -> (S.cons (lexp_whnf_aux arg ctx) s, [])
+ | [] -> (S.cons (lexp_whnf_aux arg ctx dummy_sinfo) s, [])
| _targ::targs ->
(* Ignore the type arguments *)
(s, targs))
@@ -222,43 +222,43 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
aargs in
(* Substitute case Eq variable by the proof (Eq.refl l t e') *)
let subst = S.cons (get_refl e') subst in
- lexp_whnf_aux (push_susp branch subst) ctx
+ lexp_whnf_aux (push_susp branch subst dummy_sinfo) ctx sinfo
with
| Not_found
-> match default with
| Some (_v,default)
-> let subst = S.cons (get_refl e') (S.substitute e') in
- lexp_whnf_aux (push_susp default subst) ctx
+ lexp_whnf_aux (push_susp default subst dummy_sinfo) ctx sinfo
| _ -> Log.log_error
~section:"WHNF" ~loc:l
{|Unhandled constructor "%s" in case expression|} name;
- mkCase (l, e, rt, branches, default) sinfo in
+ mkCase (l, e, rt, branches, default) dummy_sinfo in
(match lexp_lexp' e' with
| Cons (it, (_, name)) -> reduce it name []
| Call (f, aargs) ->
- (match lexp_lexp' (lexp_whnf_aux f ctx) with
+ (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with
| Cons (it, (_, name)) -> reduce it name aargs
- | _ -> mkCase (l, e, rt, branches, default) sinfo)
+ | _ -> mkCase (l, e, rt, branches, default) dummy_sinfo)
| _ -> mkCase (l, e, rt, branches, default) sinfo)
| Metavar (idx, s, _)
-> (match metavar_lookup idx with
- | MVal e -> lexp_whnf_aux (push_susp e s) ctx
+ | MVal e -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo
| _ -> e)
(* FIXME: I'd really prefer to use "native" recursive substitutions, using
* ideally a trick similar to the db_offsets in lexp_context! *)
| Let (l, defs, body)
- -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs)) ctx
+ -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs) dummy_sinfo) ctx sinfo
| _elem -> e
- in lexp_whnf_aux e ctx
+ in lexp_whnf_aux e ctx sinfo
and lexp'_whnf e (ctx : DB.lexp_context) : lexp' =
- lexp_lexp' (lexp_whnf_aux e ctx)
+ lexp_lexp' (lexp_whnf_aux e ctx dummy_sinfo)
and lexp_whnf e (ctx : DB.lexp_context) : lexp =
- lexp_whnf_aux e ctx
+ lexp_whnf_aux e ctx dummy_sinfo
and eq_cast_whnf ctx args =
match args with
@@ -289,7 +289,7 @@ and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp
((e1, e2) :: s)
and set_shift_n (s : set_plexp) (n : U.db_offset)
= List.map (let s = S.shift n in
- fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s))
+ fun (e1, e2) -> (Lexp.push_susp e1 s dummy_sinfo, Lexp.push_susp e2 s dummy_sinfo))
s
and set_shift s : set_plexp = set_shift_n s 1
@@ -315,9 +315,9 @@ and level_canon e =
| Var (_, i) -> add_var_depth i d acc
| Metavar (i, s, _)
-> (match metavar_lookup i with
- | MVal e -> canon (push_susp e s) d acc
+ | MVal e -> canon (push_susp e s dummy_sinfo) d acc
| _ -> add_var_depth (- i) d acc)
- | Susp (e, s) -> canon (push_susp e s) d acc
+ | Susp (e, s) -> canon (push_susp e s dummy_sinfo) d acc
| _ -> (max_int, m)
in canon e 0 (0,IMap.empty)
@@ -429,14 +429,14 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
S.identity fargs aargs in
(* 3. Compare the branches *)
let ctx_extend_with_eq ctx subst hlxp =
- let tlxp = mkSusp target subst sinfo in
- let tltp = mkSusp etype subst sinfo in
- let tlvl = mkSusp elvl subst sinfo in
+ let tlxp = mkSusp target subst dummy_sinfo in
+ let tltp = mkSusp etype subst dummy_sinfo in
+ let tlvl = mkSusp elvl subst dummy_sinfo in
let eqty = mkCall (DB.type_eq,
[(L.Aerasable, tlvl); (* Typelevel *)
(L.Aerasable, tltp); (* Inductive type *)
(L.Anormal, hlxp); (* Lexp of the branch head *)
- (L.Anormal, tlxp)]) sinfo in (* Target lexp *)
+ (L.Anormal, tlxp)]) dummy_sinfo in (* Target lexp *)
DB.lexp_ctx_cons ctx (DB.dloc, 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
@@ -453,9 +453,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
(ak', _vdef', ftype)::fieldtypes
-> if ak1 = ak2 && ak2 = ak' then
mkctx
- (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s sinfo))
- ((ak1, (mkVar (vdef1, i) sinfo))::args)
- (ssink vdef1 s)
+ (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s dummy_sinfo))
+ ((ak1, (mkVar (vdef1, i) dummy_sinfo))::args)
+ (ssink dummy_sinfo vdef1 s)
(i - 1)
vdefs1 vdefs2 fieldtypes
else None
@@ -468,9 +468,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)) sinfo,
- eaargs) sinfo) subst sinfo in
- let hlxp = mkCall (ctor, args) sinfo in
+ let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) dummy_sinfo,
+ eaargs) dummy_sinfo) subst dummy_sinfo in
+ let hlxp = mkCall (ctor, args) dummy_sinfo 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)
@@ -481,7 +481,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) sinfo in
+ let hlxp = mkVar ((DB.dloc, None), 0) dummy_sinfo in
let nctx = ctx_extend_with_eq nctx subst hlxp in
conv_p' nctx (set_shift_n vs' 2) e1 e2
| None, None -> true
@@ -505,13 +505,13 @@ and mkSLlub ctx e1 e2 =
| (SortLevel SLz, _) -> e2
| (_, SortLevel SLz) -> e1
| (SortLevel (SLsucc e1), SortLevel (SLsucc e2))
- -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) sinfo
+ -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) dummy_sinfo
| (_e1', _e2')
-> let ce1 = level_canon lwhnf1 in
let ce2 = level_canon lwhnf2 in
if level_leq ce1 ce2 then e2
else if level_leq ce2 ce1 then e1
- else mkSortLevel (mkSLlub' (e1, e2)) sinfo (* FIXME: Could be more canonical *)
+ else mkSortLevel (mkSLlub' (e1, e2)) dummy_sinfo (* FIXME: Could be more canonical *)
and sort_compose ctx1 ctx2 l ak k1 k2 =
(* BEWARE! Technically `k2` can refer to `v`, but this should only happen
@@ -523,13 +523,13 @@ and sort_compose ctx1 ctx2 l ak k1 k2 =
-> (match s1, s2 with
| (Stype l1, Stype l2)
-> if ak == P.Aerasable && impredicative_erase
- then SortResult (mkSusp k2 (S.substitute impossible) sinfo)
- else let l2' = (mkSusp l2 (S.substitute impossible) sinfo) in
+ then SortResult (mkSusp k2 (S.substitute impossible) dummy_sinfo)
+ else let l2' = (mkSusp l2 (S.substitute impossible) dummy_sinfo) in
(* print_string ("Normal: " ^ lexp_string l1 ^ " -> "
* ^ lexp_string l2' ^ " ==> "
* ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2')))
* ^ "\n"); *)
- SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) sinfo)
+ SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) dummy_sinfo)
| (StypeLevel, Stype _l2)
when ak == P.Aerasable && impredicative_universe_poly
(* The safety/soundness of this rule is completely unknown.
@@ -540,7 +540,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 =
* ^ lexp_string k2 ^ " ==> "
* ^ lexp_string (mkSusp k2 (S.substitute DB.level0))
* ^ "\n"); *)
- SortResult (mkSusp k2 (S.substitute DB.level0) sinfo)
+ SortResult (mkSusp k2 (S.substitute DB.level0) dummy_sinfo)
| (StypeLevel, Stype _)
| (StypeLevel, StypeOmega)
(* This might be safe, but I don't think it adds much power.
@@ -548,7 +548,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 =
* arguments, but let's not bother for now: it's easier to add it
* later than to remove it later.
* | (Stype _, StypeOmega) *)
- -> SortResult (mkSort (l, StypeOmega) sinfo)
+ -> SortResult (mkSort (l, StypeOmega) dummy_sinfo)
| _ -> SortInvalid)
| (Sort (_, _), _) -> SortK2NotType
| (_, _) -> SortK1NotType
@@ -583,7 +583,7 @@ and nerased_let defs erased =
erased es
(* "check ctx e" should return τ when "Δ ⊢ e : τ" *)
-and check'' erased ctx e =
+and check'' erased ctx e sinfo =
let check = check'' in
let assert_type ctx e t t' =
if conv_p ctx t t' then ()
@@ -594,7 +594,7 @@ and check'' erased ctx e =
(lexp_string e) (lexp_string t) (lexp_string t')
in
let check_type erased ctx t =
- let s = check erased ctx t in
+ let s = check erased ctx t sinfo in
(match lexp'_whnf s ctx with
| Sort _ -> ()
| _
@@ -607,24 +607,24 @@ and check'' erased ctx e =
| Imm (String (_, _)) -> DB.type_string
| Imm (Block (_, _) | Symbol _ | Node (_, _))
-> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!";
- DB.type_int)
+ DB.type_int )
| SortLevel SLz -> DB.type_level
| SortLevel (SLsucc e)
- -> let t = check erased ctx e in
+ -> let t = check erased ctx e sinfo in
(* FIXME: Actually, we should probably have a special function to check
* that `e` is a level, so as to avoid `case` and other funny things. *)
assert_type ctx e t DB.type_level;
DB.type_level
| SortLevel (SLlub (e1, e2))
- -> let t1 = check erased ctx e1 in
+ -> let t1 = check erased ctx e1 sinfo in
assert_type ctx e1 t1 DB.type_level;
- let t2 = check erased ctx e2 in
+ let t2 = check erased ctx e2 sinfo in
assert_type ctx e2 t2 DB.type_level;
DB.type_level
| Sort (l, Stype e)
- -> let t = check erased ctx e in
+ -> let t = check erased ctx e sinfo in
assert_type ctx e t DB.type_level;
- mkSort (l, Stype (mkSortLevel (SLsucc e) sinfo)) sinfo
+ mkSort (l, Stype (mkSortLevel (SLsucc e) dummy_sinfo)) dummy_sinfo
| Sort (_, StypeLevel) -> DB.sort_omega
| Sort (_, StypeOmega)
-> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!";
@@ -641,7 +641,7 @@ and check'' erased ctx e =
{|Var `%s` can't be used here, because it's erasable|}
(maybename name) ;
lookup_type ctx v
- | Susp (e, s) -> check erased ctx (push_susp e s)
+ | Susp (e, s) -> check erased ctx (push_susp e s dummy_sinfo) sinfo
| Let (l, defs, e)
-> let _ =
List.fold_left (fun ctx (v, _e, t)
@@ -657,12 +657,12 @@ and check'' erased ctx e =
(check (if DB.set_mem (n - 1) nerased
then DB.set_empty
else nerased)
- nctx e)
- (push_susp t (S.shift n));
+ nctx e sinfo)
+ (push_susp t (S.shift n) dummy_sinfo);
n - 1)
(List.length defs) defs in
- mkSusp (check nerased nctx e)
- (lexp_defs_subst l S.identity defs) sinfo
+ mkSusp (check nerased nctx e sinfo)
+ (lexp_defs_subst l S.identity defs) dummy_sinfo
| Arrow (ak, v, t1, loc, t2)
-> (let k1 = check_type erased ctx t1 in
let nctx = DB.lexp_ctx_cons ctx v Variable t1 in
@@ -683,19 +683,19 @@ and check'' erased ctx e =
mkArrow (ak, v, t, l,
check (dbset_push ak erased)
(DB.lctx_extend ctx v Variable t)
- e) sinfo)
+ e sinfo) dummy_sinfo)
| Call (f, args)
- -> let ft = check erased ctx f in
+ -> let ft = check erased ctx f sinfo in
List.fold_left
(fun ft (ak,arg)
-> let at = check (if ak = P.Aerasable then DB.set_empty else erased)
- ctx arg in
+ ctx arg sinfo in
match lexp'_whnf ft ctx with
| Arrow (ak', _v, t1, _l, t2)
-> if ak != ak'
then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch";
assert_type ctx arg at t1;
- mkSusp t2 (S.substitute arg) sinfo
+ mkSusp t2 (S.substitute arg) dummy_sinfo
| _ -> log_tc_error
~loc:(lexp_location arg)
"Calling a non functin (type = %s)!" (lexp_string ft);
@@ -744,7 +744,7 @@ and check'' erased ctx e =
mkArrow (ak, v, t, lexp_location t,
arg_loop (DB.lctx_extend ctx v Variable t)
(dbset_push ak erased)
- args) sinfo in
+ args) dummy_sinfo in
let tct = arg_loop ctx erased args in
tct
| Case (l, e, ret, branches, default)
@@ -753,7 +753,7 @@ and check'' erased ctx e =
match lexp_lexp' e with
| Call (f, args) -> (f, args)
| _ -> (e,[]) in
- let etype = lexp_whnf (check erased ctx e) ctx in
+ let etype = lexp_whnf (check erased ctx e sinfo) ctx in
(* FIXME save the type in the case lexp instead of recomputing
it over and over again *)
let ekind = get_type ctx etype in
@@ -776,14 +776,14 @@ and check'' erased ctx e =
s in
let s = mksubst S.identity fargs aargs in
let ctx_extend_with_eq ctx subst hlxp nerased =
- let tlxp = mkSusp e subst sinfo in
- let tltp = mkSusp etype subst sinfo in
- let tlvl = mkSusp elvl subst sinfo in
+ let tlxp = mkSusp e subst dummy_sinfo in
+ let tltp = mkSusp etype subst dummy_sinfo in
+ let tlvl = mkSusp elvl subst dummy_sinfo in
let eqty = mkCall (DB.type_eq,
[(L.Aerasable, tlvl); (* Typelevel *)
(L.Aerasable, tltp); (* Inductive type *)
(L.Anormal, hlxp); (* Lexp of the branch head *)
- (L.Anormal, tlxp)]) sinfo in (* Target lexp *)
+ (L.Anormal, tlxp)]) dummy_sinfo in (* Target lexp *)
(* The eq proof is erasable. *)
let nerased = dbset_push L.Aerasable nerased in
let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in
@@ -799,7 +799,7 @@ and check'' erased ctx e =
| (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes
-> mkctx (dbset_push ak erased)
(DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s sinfo))
- (ssink vdef s)
+ (ssink dummy_sinfo vdef s)
(mkCall (mkSusp hlxp (S.shift 1) sinfo, [(ak, mkVar (vdef, 0) sinfo)]) sinfo)
vdefs fieldtypes
| _
@@ -807,13 +807,13 @@ and check'' erased ctx e =
(erased, ctx, hlxp) in
let hctor =
mkCall (mkCons (it, (l, name)) sinfo,
- List.map (fun (_, a) -> (P.Aerasable, a)) aargs) sinfo in
+ List.map (fun (_, a) -> (P.Aerasable, a)) aargs) dummy_sinfo in
let (nerased, nctx, hlxp) =
mkctx erased ctx s hctor vdefs fieldtypes in
let subst = S.shift (List.length vdefs) in
let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in
assert_type nctx branch
- (check nerased nctx branch)
+ (check nerased nctx branch sinfo)
(mkSusp ret (S.shift ((List.length fieldtypes) + 1)) sinfo))
branches;
let diff = SMap.cardinal constructors - SMap.cardinal branches in
@@ -824,11 +824,11 @@ and check'' erased ctx e =
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
- let hlxp = mkVar ((l, None), 0) sinfo in
+ let hlxp = mkVar ((l, None), 0) dummy_sinfo in
let (nerased, nctx) =
ctx_extend_with_eq nctx subst hlxp nerased in
- assert_type nctx d (check nerased nctx d)
- (mkSusp ret (S.shift 2) sinfo)
+ assert_type nctx d (check nerased nctx d sinfo)
+ (mkSusp ret (S.shift 2) dummy_sinfo)
| None
-> if diff > 0
then
@@ -844,36 +844,36 @@ and check'' erased ctx e =
let rec indtype fargs start_index =
match fargs with
| [] -> []
- | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) sinfo)
+ | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_sinfo)
:: indtype fargs (start_index - 1) in
let rec fieldargs ftypes =
match ftypes with
| [] -> let nargs = List.length fieldtypes + List.length fargs in
- mkCall (mkSusp t (S.shift nargs) sinfo,
- indtype fargs (nargs - 1)) sinfo
+ mkCall (mkSusp t (S.shift nargs) dummy_sinfo,
+ indtype fargs (nargs - 1)) dummy_sinfo
| (ak, vd, ftype) :: ftypes
-> mkArrow (ak, vd, ftype, lexp_location ftype,
- fieldargs ftypes) sinfo in
+ fieldargs ftypes) dummy_sinfo in
let rec buildtype fargs =
match fargs with
| [] -> fieldargs fieldtypes
| (_ak, ((l,_) as vd), atype) :: fargs
-> mkArrow (P.Aerasable, vd, atype, l,
- buildtype fargs) sinfo in
+ buildtype fargs) dummy_sinfo in
buildtype fargs
with
| Not_found
-> log_tc_error ~loc:l {|Constructor "%s" does not exist|} name;
- DB.type_int)
+ DB.type_int )
| _ -> log_tc_error
~loc:(lexp_location e)
"Cons of a non-inductive type: %s" (lexp_string t);
- DB.type_int)
+ DB.type_int )
| Metavar (idx, s, _)
-> (match metavar_lookup idx with
- | MVal e -> let e = push_susp e s in
- check erased ctx e
- | MVar (_, t, _) -> push_susp t s)
+ | MVal e -> let e = push_susp e s dummy_sinfo in
+ check erased ctx e sinfo
+ | MVar (_, t, _) -> push_susp t s dummy_sinfo)
and check' ctx e =
let res = check'' DB.set_empty ctx e in
@@ -926,7 +926,7 @@ and fv (e : lexp) : (DB.set * mv_set) =
| Sort (_, (StypeOmega | StypeLevel)) -> fv_empty
| Builtin _ -> fv_empty
| Var (_, i) -> (DB.set_singleton i, mv_set_empty)
- | Susp (e, s) -> fv (push_susp e s)
+ | Susp (e, s) -> fv (push_susp e s dummy_sinfo)
| Let (_, defs, e)
-> let len = List.length defs in
let (fvs, _)
@@ -975,9 +975,9 @@ and fv (e : lexp) : (DB.set * mv_set) =
cases s
| Metavar (id, s, name)
-> (match metavar_lookup id with
- | MVal e -> fv (push_susp e s)
+ | MVal e -> fv (push_susp e s dummy_sinfo)
| MVar (sl, t, cl)
- -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in
+ -> let (fvs, mvs) = fv_erase (fv (push_susp t s dummy_sinfo)) in
(fvs, mv_set_add mvs id (sl, t, cl, name)))
in
let ofvs = LMap.find_opt fv_memo e in
@@ -1010,14 +1010,15 @@ and get_type ctx e =
| Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int
| Builtin (_, t) -> t
| SortLevel _ -> DB.type_level
- | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) sinfo)) sinfo
+ | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) dummy_sinfo)) dummy_sinfo
| Sort (_, StypeLevel) -> DB.sort_omega
| Sort (_, StypeOmega) -> DB.sort_omega
| Var (((_, _name), _idx) as v) -> lookup_type ctx v
- | Susp (e, s) -> get_type ctx (push_susp e s)
+ | Susp (e, s) -> get_type ctx (push_susp e s dummy_sinfo)
| 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) sinfo
+ mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) dummy_sinfo
+
| Arrow (ak, v, t1, l, t2)
(* FIXME: Use `check` here but silencing errors? *)
-> (let k1 = get_type ctx t1 in
@@ -1025,18 +1026,18 @@ and get_type ctx e =
let k2 = get_type nctx t2 in
match sort_compose ctx nctx l ak k1 k2 with
| SortResult k -> k
- | _ -> mkSort (l, StypeOmega) sinfo)
+ | _ -> mkSort (l, StypeOmega) dummy_sinfo)
| Lambda (ak, ((l,_) as v), t, e)
-> (mkArrow (ak, v, t, l,
get_type (DB.lctx_extend ctx v Variable t)
- e) sinfo)
+ e) dummy_sinfo)
| Call (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)
- -> mkSusp t2 (S.substitute arg) sinfo
+ -> mkSusp t2 (S.substitute arg) dummy_sinfo
| _ -> ft)
ft args
| Inductive (l, _label, args, cases)
@@ -1058,18 +1059,18 @@ and get_type ctx e =
-> mkSLlub ctx level
(* We need to unshift because the final type
* cannot refer to the fields! *)
- (mkSusp level' (L.sunshift n) sinfo)
+ (mkSusp level' (L.sunshift n) dummy_sinfo)
| _tt -> level),
DB.lctx_extend ictx v Variable t,
n + 1))
(level, ctx, 0)
case in
level)
- cases (mkSortLevel SLz sinfo) in
- mkSort (l, Stype level) sinfo
+ cases (mkSortLevel SLz dummy_sinfo) in
+ mkSort (l, Stype level) dummy_sinfo
| (ak, v, t)::args
-> mkArrow (ak, v, t, lexp_location t,
- arg_loop args (DB.lctx_extend ctx v Variable t)) sinfo in
+ arg_loop args (DB.lctx_extend ctx v Variable t)) dummy_sinfo in
let tct = arg_loop args ctx in
tct
| Case (_l, _e, ret, _branches, _default) -> ret
@@ -1081,29 +1082,29 @@ and get_type ctx e =
let rec indtype fargs start_index =
match fargs with
| [] -> []
- | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) sinfo)
+ | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_sinfo)
:: indtype fargs (start_index - 1) in
let rec fieldargs ftypes =
match ftypes with
| [] -> let nargs = List.length fieldtypes + List.length fargs in
- mkCall (mkSusp t (S.shift nargs) sinfo,
- indtype fargs (nargs - 1)) sinfo
+ mkCall (mkSusp t (S.shift nargs) dummy_sinfo,
+ indtype fargs (nargs - 1)) dummy_sinfo
| (ak, vd, ftype) :: ftypes
-> mkArrow (ak, vd, ftype, lexp_location ftype,
- fieldargs ftypes) sinfo in
+ fieldargs ftypes) dummy_sinfo in
let rec buildtype fargs =
match fargs with
| [] -> fieldargs fieldtypes
| (_ak, ((l,_) as vd), atype) :: fargs
-> mkArrow (P.Aerasable, vd, atype, l,
- buildtype fargs) sinfo in
+ buildtype fargs) dummy_sinfo in
buildtype fargs
- with Not_found -> DB.type_int)
- | _ -> DB.type_int)
+ with Not_found -> DB.type_int )
+ | _ -> DB.type_int )
| Metavar (idx, s, _)
-> (match metavar_lookup idx with
- | MVal e -> get_type ctx (push_susp e s)
- | MVar (_, t, _) -> push_susp t s)
+ | MVal e -> get_type ctx (push_susp e s dummy_sinfo)
+ | MVar (_, t, _) -> push_susp t s dummy_sinfo)
(* FIXME: Remove the mutual recursion between `lexp_whnf` and
`get_type`, and move this closer to the `lexp_whnf`. *)
@@ -1148,7 +1149,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =
| L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)
| L.Lambda (P.Aerasable, _, _, body)
- -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy))
+ -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) dummy_sinfo)
| L.Lambda (_, vdef, ty, body)
-> let lctx' = DB.lctx_extend lctx vdef Variable ty in
@@ -1166,7 +1167,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =
let ebranches = clean_branch_map lctx branches in
E.Case (location, etarget, ebranches, clean_default lctx default)
- | L.Susp (l, s) -> erase_type lctx (L.push_susp l s)
+ | L.Susp (l, s) -> erase_type lctx (L.push_susp l s dummy_sinfo)
(* To be thrown out *)
| L.Arrow _ -> E.Type lxp
@@ -1177,7 +1178,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =
| L.Inductive (_, _, _, _) -> E.Type lxp
| L.Metavar (idx, s, _)
-> (match metavar_lookup idx with
- | MVal e -> erase_type lctx (push_susp e s)
+ | MVal e -> erase_type lctx (push_susp e s dummy_sinfo)
| MVar _ -> Log.internal_error "Metavar in erase_type")
and clean_arg lctx = function
@@ -1194,7 +1195,7 @@ and clean_decls
and clean_default lctx lxp =
match lxp with
| Some (v, lxp)
- -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) in
+ -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) dummy_sinfo in
Some (v, erase_type lctx lxp')
| None -> None
@@ -1208,12 +1209,12 @@ and clean_branch_map lctx cases =
| (_, var) :: tl
-> (* Keep the variable and sink the substitution. *)
let lctx' = DB.lctx_extend lctx var Variable erasure_dummy in
- clean_arg_list tl (var :: acc) (ssink var subst) lctx'
+ clean_arg_list tl (var :: acc) (ssink dummy_sinfo var subst) lctx'
| [] -> (List.rev acc, subst, lctx)
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))
+ (l, eargs, erase_type lctx' (L.push_susp expr subst dummy_sinfo))
in
SMap.map clean_branch cases
@@ -1278,16 +1279,16 @@ let ctx2tup ctx nctx =
* let-binding i.s.o the tuple
* field (which would be both
* equivalent and preferable). *)
- mkSusp t (S.shift offset) sinfo))
+ mkSusp t (S.shift offset) dummy_sinfo))
types)
- SMap.empty) sinfo,
- cons_label) sinfo,
+ SMap.empty) dummy_sinfo,
+ cons_label) dummy_sinfo,
List.mapi (fun i (oname, _t)
- -> (P.Aimplicit, mkVar (oname, offset - i - 1) sinfo))
- types) sinfo
+ -> (P.Aimplicit, mkVar (oname, offset - i - 1) dummy_sinfo))
+ types) dummy_sinfo
| (DB.CVlet (name, LetDef (_, e), t, _) :: blocs)
- -> mkLet (loc, [(name, mkSusp e (S.shift 1) sinfo, t)],
- mk_lets_and_tup blocs ((name, t) :: types)) sinfo
+ -> mkLet (loc, [(name, mkSusp e (S.shift 1) dummy_sinfo, t)],
+ mk_lets_and_tup blocs ((name, t) :: types)) dummy_sinfo
| (DB.CVfix (defs, _) :: blocs)
-> mkLet (loc, defs,
mk_lets_and_tup blocs (List.append
@@ -1295,7 +1296,7 @@ let ctx2tup ctx nctx =
(List.map (fun (oname, _, t)
-> (oname, t))
defs))
- types)) sinfo
+ types)) dummy_sinfo
| _ -> assert false in
mk_lets_and_tup (get_blocs nctx []) []
=====================================
src/positivity.ml
=====================================
@@ -108,7 +108,7 @@ and positive' index lexp =
| Lexp.Lambda (_, _, _, e) -> positive index e
- | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s)
+ | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s dummy_sinfo)
| Lexp.Var _
(*
=====================================
src/sexp.ml
=====================================
@@ -41,7 +41,6 @@ type token = sexp
let epsilon l = Symbol (l, "")
let dummy_epsilon = epsilon dummy_location
-let dummy_sinfo : sexp list = []
(********************** Sexp tests **********************)
let pred_symbol s pred =
=====================================
src/unification.ml
=====================================
@@ -135,10 +135,10 @@ let common_subset ctx s1 s2 =
let o2 = o2 + o2' in
(* FIXME: We should check if le1 and le2 are *unifiable* instead! *)
if not (le1 = impossible || le1 = impossible)
- && OL.conv_p ctx (mkSusp le1 (S.shift o1) sinfo) (mkSusp le2 (S.shift o2) sinfo)
+ && OL.conv_p ctx (mkSusp le1 (S.shift o1) dummy_sinfo) (mkSusp le2 (S.shift o2) dummy_sinfo)
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) sinfo,
+ | s' -> S.Cons (mkVar ((lexp_location le1, None), 0) dummy_sinfo,
s', o)
else loop s1' s2' o1 o2 (o + 1)
(* If one of them reached `Identity`, unroll it, knowing that
@@ -146,11 +146,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) sinfo,
+ -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo,
S.Identity 1, o2'))
o1 o2 o
| (S.Identity o1', S.Cons _)
- -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) sinfo,
+ -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo,
S.Identity 1, o1'))
s2 o1 o2 o
| (S.Identity o1', S.Identity o2')
@@ -215,8 +215,8 @@ and unify' (e1: lexp) (e2: lexp)
(* Then, we handle metavariables (aka. flexible-flexible and
Flexible-Rigid Equations). Reminder: WHNF implies that the
metavariables are not already instanciated. *)
- | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1'
- | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2'
+ | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' dummy_sinfo
+ | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' dummy_sinfo
(* Otherwise, the equation is rigid-rigid. Let's start with the
cases that can leave residuals: 1. Variables, since they could
@@ -292,14 +292,14 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
- metavar , metavar -> inverse subst (try both sides)
- metavar , lexp -> inverse subst
*)
-and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
+and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) sinfo
: return_type =
let unif idx s lxp =
let t = match metavar_lookup idx with
| MVal _ -> Log.internal_error
"`lexp_whnf` returned an instantiated metavar!!"
- | MVar (_, t, _) -> push_susp t s in
- match Inverse_subst.apply_inv_subst lxp s with
+ | MVar (_, t, _) -> push_susp t s sinfo in
+ match Inverse_subst.apply_inv_subst lxp s sinfo with
| exception Inverse_subst.Not_invertible
-> log_info
"Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n"
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c6bb08e5de48ddc898604b095af141e4e…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c6bb08e5de48ddc898604b095af141e4e…
You're receiving this email because of your account on gitlab.com.
1
0
Bonjour,
Dans le but de s'assurer que les exemples de code Typer (sous `typer/samples/`) demeurent actuels, j'ai ajouté un test qui tente simplement de les exécuter. Certains exemples doivent encore être rafraîchis, alors pour le moment, j'ai explicitement listé les fichiers à vérifier.
Le commit se trouve ici: https://gitlab.com/monnier/typer/-/commit/f69dd1f0
Je suis ouvert à vos commentaires avant d'intégrer ces changements. D'ailleurs, je ne suis pas certain de ce qui est mieux entre une liste d'inclusions vs. d'exclusions. Je vous inviterais également à y ajouter vos exemples de code Typer.
Jean-Alexandre
2
1
[Git][monnier/typer] Pushed new branch keep-samples-alive
by Jean-Alexandre Barszcz (@jabarszcz) 12 Mar '22
by Jean-Alexandre Barszcz (@jabarszcz) 12 Mar '22
12 Mar '22
Jean-Alexandre Barszcz pushed new branch keep-samples-alive at Stefan / Typer
--
View it on GitLab: https://gitlab.com/monnier/typer/-/tree/keep-samples-alive
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][master] * shell.nix : Set the Ocaml version to 4.11
by Jean-Alexandre Barszcz (@jabarszcz) 12 Mar '22
by Jean-Alexandre Barszcz (@jabarszcz) 12 Mar '22
12 Mar '22
Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer
Commits:
a072f995 by Jean-Alexandre Barszcz at 2022-03-12T13:34:42-05:00
* shell.nix : Set the Ocaml version to 4.11
- - - - -
1 changed file:
- shell.nix
Changes:
=====================================
shell.nix
=====================================
@@ -2,7 +2,7 @@
pkgs.mkShell {
name = "typer";
buildInputs =
- with pkgs.ocamlPackages; [
+ with pkgs.ocaml-ng.ocamlPackages_4_11; [
pkgs.gnumake ocaml dune_2 findlib utop # tooling
zarith # ocaml libraries
merlin # for emacs
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a072f9955b7cea2318c36652702db8de2…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a072f9955b7cea2318c36652702db8de2…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] 2 commits: update highlight and references
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 12 Mar '22
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 12 Mar '22
12 Mar '22
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
17cc8120 by Soilih at 2022-03-11T19:55:55-05:00
update highlight and references
- - - - -
928ea462 by Soilih at 2022-03-11T19:56:17-05:00
Merge branch 'soilih-test-avec-ast' into soilih
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -890,8 +890,7 @@ let tup_browse_defs_in_ctx (lctx: Debruijn.lexp_context) lxp (vn : vname) (curso
else foo tl str rlst
in foo lctx_l str []
-
-let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname) ret =
+let rec find_references (lxp: Lexp.lexp) (vr: vname) idx_vr ret =
match Lexp.lexp_lexp' lxp with
| Imm (Float (_, _))
| Imm (Integer (_, _))
@@ -904,28 +903,20 @@ let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname)
| Sort (_, StypeLevel) -> ret
| Sort (_, StypeOmega) -> ret
| Builtin (_, t) -> ret
- | Var ((vn, idx) as v)
- -> let (vn_ret,_,_) = Debruijn.lctx_lookup ctx v in
- let (_,vrn) = vr in
- let stri = try Option.get vrn
- with exe -> failwith "Our Var doesn't have a string"
- in
- let (_, vn_ret') = vn_ret in
- let str = try Option.get vn_ret'
- with exe -> failwith "Our Reference doesn't have a string"
- in
- if (String.equal str stri) then vn::ret
- else ret
+ | Var (vn, idx)
+ -> if (Int.equal idx idx_vr) then
+ vn::ret
+ else ret
| Arrow (ak, v, t1, l, t2)
- -> find_references ctx t2 vr ret
+ -> find_references t2 vr idx_vr ret
| Lambda (ak, v, t, e)
- -> find_references ctx e vr (find_references ctx t vr ret)
+ -> find_references e vr idx_vr (find_references t vr idx_vr ret)
| Call (f, args) -> ret
- | Let (l, defs, el) -> find_references ctx el vr ret
+ | Let (l, defs, el) -> find_references el vr idx_vr ret
| Inductive (l, _label, args, cases)
->
(
- let rec arg_loop ctx args =
+ let rec arg_loop args =
match args with
(*| Inductive of U.location * label
* ((arg_kind * vname * ltype) list) (* formal Args *)
@@ -934,17 +925,16 @@ let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname)
-> let lst =
SMap.fold
(fun _ case (lst: vname list) ->
- let (_, ret_list) =
+ let ret_list =
List.fold_left
(
- fun (ictx, tab) (ak, v, t) ->
+ fun tab (ak, v, t) ->
(
- let nctx = Debruijn.lctx_extend ictx v Variable t in
- (Debruijn.lctx_extend ictx v Variable t,
- (List.append tab (find_references nctx t vr ret)))
+
+ (List.append tab (find_references t vr idx_vr ret))
)
)
- (ctx, [] )
+ []
case
in
ret_list
@@ -953,20 +943,19 @@ let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname)
lst
| (ak, v, t)::args
- -> let ctx' = Debruijn.lctx_extend ctx v Variable t in
- find_references ctx' t vr (find_references ctx' t vr ret)
- in
- arg_loop ctx args
+ -> find_references t vr idx_vr (find_references t vr idx_vr ret)
+ in
+ arg_loop args
)
(*
| Case of U.location * lexp
- * ltype (* The type of the return value of all branches *)
- * (U.location * (arg_kind * vname) list * lexp) SMap.t
- * (vname * lexp) option (* Default. *)
+ * ltype (* The type of the return value of all branches *)
+ * (U.location * (arg_kind * vname) list * lexp) SMap.t
+ * (vname * lexp) option (* Default. *)
*)
| _ -> ret
-
-let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.Location.t) : (Debruijn.lexp_context * Lexp.lexp * vname) option =
+
+let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.Location.t) : (Lexp.lexp * vname * int) option =
match Lexp.lexp_lexp' lxp with
@@ -988,25 +977,24 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.L
List.fold_left (fun ctx (v, _e, t)
-> (Debruijn.lctx_extend ctx v ForwardRef t))
ctx defs in
- let rec foo ctx' (ctx_list: Debruijn.env_elem list) cursor =
+ let rec foo (ctx_list: Debruijn.env_elem list) cursor comp =
match ctx_list with
| [] -> failwith "No Variable in the cursor"
| ((l, (Some vn) as v),_,_)::tl
- -> if (vn_on_the_cursor v cursor) then Some (ctx', el, v)
- else foo ctx' tl cursor
- | _::tl -> foo ctx' tl cursor
+ -> if (vn_on_the_cursor v cursor) then Some (el, v, comp)
+ else foo tl cursor (comp + 1)
+ | _::tl -> foo tl cursor (comp + 1)
in
let ctx_list = Myers.list ctx' in
- foo ctx' ctx_list cursor
+ foo ctx_list cursor 0
| Arrow (ak, v, t1, l, t2)
- -> let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
- if (vn_on_the_cursor v cursor) then
- Some (nctx, t2, v)
+ -> if (vn_on_the_cursor v cursor) then
+ Some (t2, v, 0)
else None
- | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in
- if (vn_on_the_cursor v cursor) then Some (ctx', e, v)
+ | Lambda (ak, ((l,_) as 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 None
| Call (f, args) -> None
@@ -1018,88 +1006,41 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.L
match Lexp.lexp_lexp' e with
| Call (f, args) -> (f, args)
| _ -> (e,[]) in
- (* candidats := (browse_lexp ctx e cursor):: !candidats;*)
- let etype = Opslexp.get_type ctx e in
- (* FIXME save the type in the case lexp instead of recomputing
- it over and over again *)
- let ekind = Opslexp.get_type ctx etype in
- let elvl = match Opslexp.lexp'_whnf ekind ctx with
- | Sort (_, Stype l) -> l
- | _ -> Debruijn.level0 in
- let erased = Debruijn.set_empty in
+ let etype = Opslexp.get_type ctx e in
let it, aargs = call_split etype in
(
match Opslexp.lexp'_whnf it ctx, aargs with
-
| Inductive (_, _, fargs, constructors), aargs ->
- let rec mksubst s fargs aargs =
- match fargs, aargs with
- | [], [] -> s
- | _farg::fargs, (_ak, aarg)::aargs
- (* We don't check aarg's type, because we assume that `check`
- * returns a valid type. *)
- -> mksubst (Subst.cons aarg s) fargs aargs
- | _,_ -> s in
- let s = mksubst Subst.identity fargs aargs in
- let ctx_extend_with_eq ctx subst hlxp =
- let tlxp = Lexp.mkSusp e subst in
- let tltp = Lexp.mkSusp etype subst in
- let tlvl = Lexp.mkSusp elvl subst in
- let eqty = Lexp.mkCall (Debruijn.type_eq,
- [(Lexp.Aerasable, tlvl); (* Typelevel *)
- (Lexp.Aerasable, tltp); (* Inductive type *)
- (Lexp.Anormal, hlxp); (* Lexp of the branch head *)
- (Lexp.Anormal, tlxp)]) in (* Target lexp *)
- (* The eq proof is erasable. *)
- let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in
- (erased, nctx) in
-
- let brch = SMap.bindings branches in
- let _ =
- List.map
- (
- fun (name, (l, vdefs, branch))
- -> let fieldtypes = SMap.find name constructors in
- let rec mkctx erased ctx s hlxp vdefs fieldtypes =
- match vdefs, fieldtypes with
- | [], [] -> (erased, ctx, hlxp)
- (* FIXME: If ak is Aerasable, make sure the var only
- * appears in type annotations. *)
- | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes
- -> candidats := ((Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)), vdef)::!candidats;
- mkctx (Opslexp.dbset_push ak erased)
- (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s))
- (Lexp.ssink vdef s)
- (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))]))
- vdefs fieldtypes
- | _,_ -> (erased, ctx, hlxp) in
- let hctor =
- Lexp.mkCall (Lexp.mkCons (it, (l, name)),
- List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in
- let (nerased, nctx, hlxp) =
- mkctx erased ctx s hctor vdefs fieldtypes in
- let subst = Subst.shift (List.length vdefs) in
- ignore(ctx_extend_with_eq nctx subst hlxp)
- )
- brch
- in
- ()
-
- | _,_ -> () ;
+ let vn_lst = SMap.fold
+ (fun name (l, vdefs, branch) (lst: (vname * Lexp.lexp * int) list)
+ -> let fieldtypes = SMap.find name constructors in
+ let collect vdefs fieldtypes comp =
+ match vdefs, fieldtypes with
+ | [], [] -> lst
+ | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes
+ -> (vdef, branch, comp)::(_vdef', branch, comp)::lst
+ | _,_ -> lst in
+ collect vdefs fieldtypes 0
+ )
+ branches []
+ in
+ candidats := vn_lst
+
+ | _,_ -> failwith "Case on a non-inductive type!" ;
);
- let rec cands (lst: (Debruijn.lexp_context * vname) list) =
+ let rec cands (lst: (vname * Lexp.lexp * int) list) =
match lst with
| [] -> failwith "No Valid Candidate"
- | hd::tl -> let (ctx,(l,s)) = hd in
+ | hd::tl -> let ((l,s), lxp, comp) = hd in
if (l.start_column <= cursor.start_column
&& l.end_column >= cursor.end_column
)
then hd
else cands tl
in
- let (lctx,vn) = cands !candidats in
- Some (lctx, e, vn)
+ let (vn, lxp, comp) = cands !candidats in
+ Some (lxp, vn, comp)
| Cons (t, (_l, name))
-> None
@@ -1107,6 +1048,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.L
-> None
+
let construct_highlights (lst: vname list) : Lsp.Types.DocumentHighlight.t list =
List.map ( fun (x: vname) ->
let (l,_) = x in
@@ -1720,15 +1662,8 @@ class lsp_server =
match Hashtbl.find buffers params.textDocument.uri with
| state_after_processing -> let (_,ast,cur) = state_after_processing in
cur := Some (params.position.line,params.position.character);
- let (list_list, _) = Option.get ast in
+ let (list_list, _) = ast in
let typer_loc = typer_pos_of_lsp_pos params.position in
- let typer_loc' = {
- typer_loc
- with
- start_line = typer_loc.start_line + 1;
- end_line = typer_loc.end_line + 1
- }
- in
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
(*
let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in
@@ -1736,10 +1671,10 @@ class lsp_server =
(Debruijn.lexp_context * Lexp.lexp * vname)
*)
let lexp = trans_list_in_list_to_let list_list in
- let (l_ctx,lxp,vn) = try Option.get (browse_defs ctx lexp typer_loc')
- with exe -> failwith "No highlight found !!!"
+ let (lxp, vn, idx) = try Option.get (browse_defs ctx lexp typer_loc)
+ with exe -> failwith "No highlight found !!!"
in
- let ret = find_references l_ctx lxp vn [vn] in
+ let ret = find_references lxp vn idx [vn] in
let r = construct_highlights ret in
let e = Some r in
let f = Linol_lwt.return e in f
@@ -1749,15 +1684,8 @@ class lsp_server =
match Hashtbl.find buffers params.textDocument.uri with
| state_after_processing -> let (_,ast,cur) = state_after_processing in
cur := Some (params.position.line,params.position.character);
- let (list_list, _) = Option.get ast in
+ let (list_list, _) = ast in
let typer_loc = typer_pos_of_lsp_pos params.position in
- let typer_loc' = {
- typer_loc
- with
- start_line = typer_loc.start_line + 1;
- end_line = typer_loc.end_line + 1
- }
- in
(*failwith ("(" ^ (string_of_int typer_loc.start_line) ^ "," ^ (string_of_int typer_loc.start_column) ^ ")");*)
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
(*
@@ -1765,10 +1693,10 @@ class lsp_server =
let (_,lexp,_) = vx in
*)
let lexp = trans_list_in_list_to_let list_list in
- let (l_ctx,lxp,vn) = try Option.get (browse_defs ctx lexp typer_loc')
- with exe -> failwith "No reference found !!!"
+ let (lxp, vn, idx) = try Option.get (browse_defs ctx lexp typer_loc)
+ with exe -> failwith "No reference found !!!"
in
- let ret = find_references l_ctx lxp vn [vn] in
+ let ret = find_references lxp vn idx [vn] in
let r = construct_references params.textDocument.uri ret in
let e = Some r in
let f = Linol_lwt.return e in f
@@ -1776,6 +1704,7 @@ class lsp_server =
| _ -> super#on_request_unhandled ~notify_back ~id req
)
in f req
+
*)
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/61db9bef0a3b061fbbc0599ea97800db…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/61db9bef0a3b061fbbc0599ea97800db…
You're receiving this email because of your account on gitlab.com.
1
0
11 Mar '22
Soilihi BEN SOILIHI BOINA pushed new branch soilih at Stefan / Typer
--
View it on GitLab: https://gitlab.com/monnier/typer/-/tree/soilih
You're receiving this email because of your account on gitlab.com.
1
0
11 Mar '22
Soilihi BEN SOILIHI BOINA deleted branch soilih at Stefan / Typer
--
You're receiving this email because of your account on gitlab.com.
1
0