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

[Git][monnier/typer] Pushed new branch minimal-server
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

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

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

[Git][monnier/typer][track-sexp-lexp] Introduce sinfo
by Ismaila FALL (＠Fallismaila) 17 Mar '22

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

Un test pour les "samples"
by Jean-Alexandre Barszcz 15 Mar '22

15 Mar '22

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

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

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) 11 Mar '22

11 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

[Git][monnier/typer] Pushed new branch soilih
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 11 Mar '22

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

[Git][monnier/typer] Deleted branch soilih
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 11 Mar '22

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mars 2022