Simon Génier pushed to branch simon--pp-print-lctx at Stefan / Typer

Commits: 62f468a7 by Simon Génier at 2023-03-24T16:31:56-04:00 Move the index set to its own module.

I want to separate the lexp context to its own module, but it depends on the index set in Debruijn. Debruijn will depend on this new Lctx module so splitting the index set is necessary to avoid circular dependencies.

- - - - - 77d866bd by Simon Génier at 2023-03-24T16:33:33-04:00 Implement IdxSet in terms of Set instead of Map.

It probably ends up also using a map internally, but it makes the code more concise by not having all these () to ignore.

- - - - - af3d981d by Simon Génier at 2023-03-24T16:33:38-04:00 Add a fold for IdxSet.

- - - - - a49395a8 by Simon Génier at 2023-03-24T16:33:38-04:00 Move the lexp context to its own module.

- - - - - 99576918 by Simon Génier at 2023-03-24T16:33:38-04:00 Merge the try and the match in Lctx.lookup.

- - - - - 800d040d by Simon Génier at 2023-03-24T16:33:38-04:00 Print the lexp context with the format module.

This patch introduces two important changes to the way lexp contexts are printed.

- The lexp context is now formatted as a list of definitions instead of a table. This leaves more horizontal room to print the expressions themselves. For example,

% index = 1, offset = 0 case_return_ : Macro; case_return_ = (__.__ (depelim) case_return_);

- We leverage the recent changes to the printing of lexps to limit the size of the expressions we print. We get this for free by setting a "box" limit on the formatter. Note that this limit only applies when dumping the context: the full expression is printed when inspecting single value.

Elab_arg-pos = (lambda (a : ##String) -> (lambda (b : ##String) -> (lambda … -> …)));

- - - - -

16 changed files:

- debug_util.ml - + src/IdxSet.ml - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - + src/lctx.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml - src/util.ml - tests/instargs_test.ml - typer.ml

Changes:

===================================== debug_util.ml ===================================== @@ -145,7 +145,7 @@ let main () = print_string "\n";));

(if (get_p_option "lctx") then( - print_lexp_ctx (ectx_to_lctx nctx); print_string "\n")); + Lctx.print (ectx_to_lctx nctx); print_string "\n"));

(* Type erasure *) let _, clean_lxp =

===================================== src/IdxSet.ml ===================================== @@ -0,0 +1,64 @@ +(* Copyright (C) 2023 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@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 Util + +(** Sets of DeBruijn indices. + + It is implemented by a set, but a global offset is stored alongside. This + makes shifting very efficient. *) +type t = db_offset * ISet.t + +let empty : t = (0, ISet.empty) + +let mem (i : db_offset) (o, m : t) : bool = + ISet.mem (i - o) m + +let set (i : db_offset) (o, m : t) : t = + (o, ISet.add (i - o) m) + +let reset (i : db_offset) (o, m : t) : t = + (o, ISet.remove (i - o) m) + +let singleton (i : db_offset) = + (0, ISet.singleton i) + +(** Adjust a set for use in a deeper scope with `o` additional bindings. *) +let sink (o : db_offset) (o', m : t) : t = + (o + o', m) + +(** Adjust a set for use in a higher scope with `o` fewer bindings. *) +let hoist (o : db_offset) (o', m : t) : t = + let newo = o' - o in + let (_, _, newm) = ISet.split (-1 - newo) m + in (newo, newm) + +let union (o1, m1 : t) (o2, m2 : t) : t = + if o1 = o2 + then (o1, ISet.union m1 m2) + else + let o = o2 - o1 in + (o1, ISet.fold (fun i2 m1 -> ISet.add (i2 + o) m1) m2 m1) + +let ascending_seq (o, m : t) : int Seq.t = + ISet.to_seq m |> Seq.map (fun x -> x + o) + +let fold (type a) (f : db_offset -> a -> a) (o, m : t) (x : a) : a = + ISet.fold (fun i x -> f (o + i) x) m x

===================================== src/REPL.ml ===================================== @@ -180,8 +180,8 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) = ectx | "%info"::args | "%i"::args -> let _ = match args with - | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) - | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + | ["all"] -> Lctx.dump (ectx_to_lctx ectx) + | _ -> Lctx.print (ectx_to_lctx ectx) in ectx

| cmd::_

===================================== src/debruijn.ml ===================================== @@ -32,50 +32,13 @@ * * ---------------------------------------------------------------------------*)

-open Fmt open Lexp open Sexp open Util

-module M = Myers - let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt

-(** Sets of DeBruijn indices **) - -type set = db_offset * unit IMap.t - -let set_empty = (0, IMap.empty) - -let set_mem i (o, m) = IMap.mem (i - o) m - -let set_set i (o, m) = (o, IMap.add (i - o) () m) -let set_reset i (o, m) = (o, IMap.remove (i - o) m) - -let set_singleton i = (0, IMap.singleton i ()) - -(* Adjust a set for use in a deeper scope with `o` additional bindings. *) -let set_sink o (o', m) = (o + o', m) - -(* Adjust a set for use in a higher scope with `o` fewer bindings. *) -let set_hoist o (o', m) = - let newo = o' - o in - let (_, _, newm) = IMap.split (-1 - newo) m - in (newo, newm) - -let set_union (o1, m1) (o2, m2) : set = - if o1 = o2 then - (o1, IMap.merge (fun _k _ _ -> Some ()) m1 m2) - else - let o = o2 - o1 in - (o1, IMap.fold (fun i2 () m1 - -> IMap.add (i2 + o) () m1) - m2 m1) - -let set_ascending_seq ((o, m) : set) : int Seq.t = - IMap.to_seq m |> Seq.map (fun x -> fst x + o) - (* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. * @@ -159,10 +122,6 @@ let eq_refl = Anormal, mkVar (xv, 0)])))))

-(* easier to debug with type annotations *) -type env_elem = (vname * varbind * ltype) -type lexp_context = env_elem M.myers - type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)

(* Map variable name to its distance in the context *) @@ -180,18 +139,18 @@ type typeclass_ctx = (ltype * lctx_length) list (* the list of type classes *) * bool (* true if new bindings are instances (used to implement (dont-)bind-instances) *) - * set (* The set of bindings that are instances *) + * IdxSet.t (* The set of bindings that are instances *)

(* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.t * senv_type * lexp_context * meta_scope * typeclass_ctx + = Grammar.t * senv_type * Lctx.t * meta_scope * typeclass_ctx

(* Elab context getters *)

let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in - assert (n = M.length lctx); n + assert (n = Myers.length lctx); n

let ectx_get_grammar (ectx : elab_context) : Grammar.t = let (grm,_, _, _, _) = ectx in grm @@ -200,7 +159,7 @@ let ectx_get_senv (ectx : elab_context) : senv_type = let (_,senv, _, _, _) = ectx in senv

(* Extract the lexp context from the context used during elaboration. *) -let ectx_to_lctx (ectx : elab_context) : lexp_context = +let ectx_to_lctx (ectx : elab_context) : Lctx.t = let (_,_, lctx, _, _) = ectx in lctx

let ectx_get_scope (ectx : elab_context) : meta_scope = @@ -225,7 +184,7 @@ let ectx_set_senv (senv : senv_type) (ectx : elab_context) : elab_context = let (grm, _, lctx, sl, tcctx) = ectx in (grm, senv, lctx, sl, tcctx)

-let ectx_set_lctx (lctx : lexp_context) (ectx : elab_context) : elab_context = +let ectx_set_lctx (lctx : Lctx.t) (ectx : elab_context) : elab_context = let (grm, senv, _, sl, tcctx) = ectx in (grm, senv, lctx, sl, tcctx)

@@ -241,11 +200,10 @@ let ectx_set_tcctx (tcctx : typeclass_ctx) (ectx : elab_context) : elab_context * ---------------------------------- *)

let empty_senv = (0, SMap.empty) -let empty_lctx = M.nil -let empty_tcctx = ([], false, set_empty) +let empty_tcctx = ([], false, IdxSet.empty)

let empty_elab_context : elab_context - = (Grammar.default_grammar, empty_senv, empty_lctx, + = (Grammar.default_grammar, empty_senv, Lctx.empty, (0, 0, ref SMap.empty), empty_tcctx)

(* senv_lookup caller were using Not_found exception *) @@ -273,33 +231,15 @@ let senv_lookup (name: string) (ctx: elab_context): int =

senv_lookup_fail (get_related_names n name map)

-let lexp_ctx_cons (ctx : lexp_context) d v t = - assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in - offset >= 0 - && (ctx = M.nil - || match M.car ctx with - | (_, LetDef (previous_offset, _), _) - -> previous_offset >= 0 (* General constraint. *) - (* Either `ctx` is self-standing (doesn't depend on us), - * or it depends on us (and maybe other bindings to come), in - * which case we have to depend on the exact same bindings. *) - && (previous_offset <= 1 - || previous_offset = 1 + offset) - | _ -> true)); - M.cons (d, v, t) ctx - -let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = - lexp_ctx_cons ctx def v t - let tcctx_extend ((tcs, inst_def, insts) : typeclass_ctx) = - let insts = set_sink 1 insts in - tcs, inst_def, if inst_def then set_set 0 insts else insts + let insts = IdxSet.sink 1 insts in + tcs, inst_def, if inst_def then IdxSet.set 0 insts else insts

let tcctx_extend_rec (n : int) ((tcs, inst_def, insts) : typeclass_ctx) = let rec set_set_n n s = if n = 0 then s else - set_set_n (n - 1) (set_set (n - 1) s) in - let insts = set_sink n insts in + set_set_n (n - 1) (IdxSet.set (n - 1) s) in + let insts = IdxSet.sink n insts in tcs, inst_def, if inst_def then set_set_n n insts else insts

let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = @@ -307,20 +247,11 @@ let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (n, map) = ectx_get_senv ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in ctx |> ectx_set_senv (n + 1, nmap) - |> ectx_set_lctx (lexp_ctx_cons (ectx_to_lctx ctx) def v t) + |> ectx_set_lctx (Lctx.cons (ectx_to_lctx ctx) def v t) |> ectx_set_tcctx (tcctx_extend (ectx_to_tcctx ctx))

let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t

-let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = - let (ctx, _) = - List.fold_left - (fun (ctx, recursion_offset) (def, e, t) -> - lexp_ctx_cons ctx def (LetDef (recursion_offset, e)) t, - recursion_offset - 1) - (ctx, List.length defs) defs in - ctx - let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = let (n, senv) = ectx_get_senv ctx in let len = List.length defs in @@ -331,7 +262,7 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = i + 1) (senv, n) defs in ctx |> ectx_set_senv (n + len, senv') - |> ectx_set_lctx (lctx_extend_rec (ectx_to_lctx ctx) defs) + |> ectx_set_lctx (Lctx.extend (ectx_to_lctx ctx) defs) |> ectx_set_tcctx (tcctx_extend_rec len (ectx_to_tcctx ctx))

let ectx_new_scope (ectx : elab_context) : elab_context = @@ -339,12 +270,9 @@ let ectx_new_scope (ectx : elab_context) : elab_context = let (scope, _, rmmap) = ectx_get_scope ectx in ectx_set_meta_scope (scope + 1, Myers.length lctx, ref (!rmmap)) ectx

-let env_lookup_by_index index (ctx: lexp_context): env_elem = +let env_lookup_by_index index (ctx: Lctx.t): Lctx.elem = Myers.nth index ctx

-let env_lookup_set (s : set) (lctx : lexp_context) : (db_index * env_elem) Seq.t = - M.nthsi lctx (set_ascending_seq s) - let ectx_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = let (tcs, inst_def, insts) = ectx_to_tcctx ectx in ectx_set_tcctx ((t, get_size ectx) :: tcs, inst_def, insts) ectx @@ -352,154 +280,23 @@ let ectx_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = let ectx_set_inst (ectx : elab_context) (index : int) (inst : bool) : elab_context = let (tcs, inst_def, insts) = ectx_to_tcctx ectx in - let ninsts = if inst then set_set index insts else set_reset index insts in + let ninsts = if inst then IdxSet.set index insts else IdxSet.reset index insts in ectx_set_tcctx (tcs, inst_def, ninsts) ectx

let ectx_set_inst_def (ectx : elab_context) (inst_def : bool) : elab_context = let (tcs, _, insts) = ectx_to_tcctx ectx in ectx_set_tcctx (tcs, inst_def, insts) ectx

-let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = - print_string (make_title " LEXP CONTEXT "); - - make_rheader - [(Some ('l', 7), "INDEX"); - (Some ('l', 4), "OFF"); - (Some ('l', 10), "NAME"); - (Some ('l', 42), "VALUE : TYPE")]; - - print_string (make_sep '-'); - - let prefix = " | | | | " in - - let print i = - try - let r, name, lexp, ty = - match env_lookup_by_index i ctx with - | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty - | ((_, name), _, ty) -> 0, name, None, ty - in - let name' = maybename name in - let short_name = - if String.length name' > 10 - then - String.sub name' 0 9 ^ "…" - else name' - in - Printf.printf " | %-7d | %-4d | %-10s | " i r short_name; - (match lexp with - | None -> print_string "<var>" - | Some lexp - -> (let str = Lexp.to_string lexp in - let strs = - match String.split_on_char '\n' str with - | hd :: tl -> print_string hd; tl - | [] -> [] - in - List.iter - (fun elem -> - print_newline (); - print_string prefix; - print_string elem) - strs)); - print_string " : "; - Lexp.print ty; - print_newline () - with - | Not_found - -> print_endline " | %-7d | Not_found |" - in - - let rec print_range lower i = - let i' = i - 1 in - if i' >= lower - then - (print i'; - print_range lower i') - in - - let rec print_ranges = function - | [] -> () - | (lower, upper) :: ranges' - -> (print_range lower upper; - print_ranges ranges') - in - - print_ranges ranges; - print_string (make_sep '=') - -(* Only print user defined variables *) -let print_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_n lctx [(0, M.length lctx - !builtin_size)] - -(* Dump the whole context *) -let dump_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_n lctx [(0, M.length lctx)] - -let summarize_lctx (lctx : lexp_context) (at : int) : unit = - let ranges = - if at < 7 - then [(0, min (max (at + 2) 5) (M.length lctx))] - else [(at - 2, min (at + 2) (M.length lctx)); (0, 5)] - in - print_lexp_ctx_n lctx ranges; - print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full." - -let log_full_lctx = ref false - -(* generic lookup *) -let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = - let ((loc, oename), dbi) = v in - try - let ret = Myers.nth dbi ctx in - let _ = match (ret, oename) with - | (((_, Some name), _, _), Some ename) - -> (* Check if names match *) - if not (ename = name) then - let print_action = - if !log_full_lctx - then fun () -> (print_lexp_ctx ctx; print_newline ()) - else fun () -> summarize_lctx ctx dbi - in - fatal - ~loc:(Sexp.location loc) ~print_action - ({|DeBruijn index %d refers to wrong name. |} - ^^ {|Expected: "%s" got "%s"|}) - dbi ename name - | _ -> () in - - ret - with - | Not_found - -> fatal - ~loc:(Sexp.location loc) - "DeBruijn index %d of `%s` out of bounds" - dbi - (maybename oename) - -let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = - let (_, i) = vref in - let (_, _, t) = lctx_lookup ctx vref in - mkSusp t (S.shift (i + 1)) - -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))) - | _ -> None - let env_lookup_type ctx (v : vref): lexp = - lctx_lookup_type (ectx_to_lctx ctx) v - - (* mkSusp ltp (S.shift (idx + 1)) *) + Lctx.lookup_type (ectx_to_lctx ctx) v

let env_lookup_expr ctx (v : vref): lexp option = - lctx_lookup_value (ectx_to_lctx ctx) v + Lctx.lookup_value (ectx_to_lctx ctx) v

type lct_view = | CVempty - | CVlet of vname * varbind * ltype * lexp_context - | CVfix of (vname * lexp * ltype) list * lexp_context + | CVlet of vname * varbind * ltype * Lctx.t + | CVfix of (vname * lexp * ltype) list * Lctx.t

let lctx_view lctx = match lctx with

===================================== src/elab.ml ===================================== @@ -164,7 +164,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var = | _ -> info ~print_action:(fun _ -> - print_lexp_ctx (ectx_to_lctx ctx); print_newline () + Lctx.print (ectx_to_lctx ctx); print_newline () ) ~loc:(Lexp.location ltp) {|Exception while checking type "%s"%s|} @@ -185,7 +185,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = info ~print_action:(fun _ -> lexp_print_details lxp (); - print_lexp_ctx (ectx_to_lctx ctx); + Lctx.print (ectx_to_lctx ctx); print_newline () ) ~loc:(Sexp.location loc) @@ -276,7 +276,7 @@ let ctx_define_rec (ctx: elab_context) decls = * definitions) as well as when we fill implicit arguments. *)

-let newMetavar (ctx : lexp_context) sl name t = +let newMetavar (ctx : Lctx.t) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name)

@@ -305,7 +305,7 @@ let newShiftedInstanceMetavar (ctx : elab_context) name t = let new_n = n - ctx_shift in (new_n, SMap.filter (fun _ n' -> n' <= new_n) senv_map) in let shift_tcctx (tcs, inst_def, insts) = - (tcs, inst_def, DB.set_hoist ctx_shift insts) in + (tcs, inst_def, IdxSet.hoist ctx_shift insts) in let nctx = ctx |> ectx_set_senv (shift_senv (ectx_get_senv ctx)) |> ectx_set_lctx octx @@ -314,10 +314,10 @@ let newShiftedInstanceMetavar (ctx : elab_context) name t = Inst.save_metavar_resolution_ctxt meta nctx (fst name); mkMetavar (meta, subst, name)

-let newMetalevel (ctx : lexp_context) sl loc = +let newMetalevel (ctx : Lctx.t) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level

-let newMetatype (ctx : lexp_context) sl loc +let newMetatype (ctx : Lctx.t) sl loc = newMetavar ctx sl (loc, Some "τ") (mkSort (loc, Stype (newMetalevel ctx sl loc)))

===================================== src/eval.ml ===================================== @@ -1123,27 +1123,26 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps

-module CMap - (* Memoization table. FIXME: Ideally the keys should be "weak", but - * I haven't found any such functionality in OCaml's libs. *) - = Hashtbl.Make - (struct type t = lexp_context let hash = Hashtbl.hash let equal = (==) end) +(* Memoization table. FIXME: Ideally the keys should be "weak", but I haven't + found any such functionality in OCaml's libs. *) +module CMap = Hashtbl.Make(Lctx) let ctx_memo = CMap.create 1000

-let not_closed rctx ((o, vm) : DB.set) = - IMap.fold (fun i () nc -> let i = i + o in - let (_, rc) = Myers.nth i rctx in - match !rc with Vundefined -> i::nc | _ -> nc) - vm [] +let not_closed rctx (indices : IdxSet.t) : db_offset list = + let f i nc = + let (_, rc) = Myers.nth i rctx in + match !rc with Vundefined -> i::nc | _ -> nc + in + IdxSet.fold f indices []

let closed_p rctx (fvs, (mvs, _)) = not_closed rctx fvs = [] (* FIXME: Handle metavars! *) && IMap.is_empty mvs

-let from_lctx (lctx: lexp_context): runtime_env = +let from_lctx (lctx : Lctx.t) : runtime_env = (* FIXME: `eval` with a disabled IO.run. *) - let rec from_lctx' (lctx: lexp_context): runtime_env = + let rec from_lctx' (lctx : Lctx.t) : runtime_env = match lctx_view lctx with | CVempty -> Myers.nil | CVlet (loname, def, _, lctx) @@ -1172,7 +1171,7 @@ let from_lctx (lctx: lexp_context): runtime_env = let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) - let lctx' = DB.lctx_extend_rec lctx defs in + let lctx' = Lctx.extend 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 else () in

===================================== src/fmt.ml ===================================== @@ -118,6 +118,7 @@ let formatter_of_out_channel (chan : out_channel) : Format.formatter = print_close_stag = Fun.const (); } in - Format.pp_set_formatter_stag_functions f stag_fns; - Format.pp_set_tags f true; + pp_set_formatter_stag_functions f stag_fns; + pp_set_tags f true; + pp_set_ellipsis_text f "…"; f

===================================== src/gambit.ml ===================================== @@ -18,7 +18,6 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see http://www.gnu.org/licenses/. *)

-open Debruijn open Elexp open Lexp open Printf @@ -136,7 +135,7 @@ module ScmContext = struct

let nil : t = Myers.nil

- let of_lctx (lctx : lexp_context) : t = + let of_lctx (lctx : Lctx.t) : t = let f ((_, name), _, _) = Option.get name in Myers.map f lctx

===================================== src/instargs.ml ===================================== @@ -77,7 +77,7 @@ let in_typeclass_set (ectx : DB.elab_context) (t : L.ltype) : bool =

(** Get the head of a call. For instance, the call of `(Monoid α)` is `Monoid`. *) -let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = +let get_head (lctx : Lctx.t) (t : L.ltype) : L.ltype = let whnft = OL.lexp_whnf t lctx in match L.lexp_lexp' whnft with | L.Call (_, head, _) -> head @@ -136,8 +136,8 @@ let search_instance return the applied expression (ex: `(nil (t := Int))` for a `(List Int)`). The expression is tupled with the index and env_elem, for convenience. *) - let env_elem_match (i, elem : U.db_index * DB.env_elem) - : (int * DB.env_elem * L.lexp) option = + let env_elem_match (i, elem : U.db_index * Lctx.elem) + : (int * Lctx.elem * L.lexp) option = let ((_, namopt), _, t') = elem in let var = L.mkVar ((sinfo, namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in @@ -166,7 +166,7 @@ let search_instance None | Match -> Some (i, elem, e) in

- let candidates = DB.env_lookup_set insts lctx + let candidates = Lctx.lookup_set insts lctx |> Seq.filter_map env_elem_match in

if !debug_list_all_candidates then

===================================== src/lctx.ml ===================================== @@ -0,0 +1,165 @@ +(* Copyright (C) 2023 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@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 Lexp +open Sexp +open Util + +let fatal ?print_action ?loc fmt = + Log.log_fatal ~section:"LCTX" ?print_action ?loc fmt + +type elem = vname * varbind * ltype + +type t = elem Myers.myers + +let empty = Myers.nil + +let cons (ctx : t) d v t = + assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in + offset >= 0 + && (ctx = Myers.nil + || match Myers.car ctx with + | (_, LetDef (previous_offset, _), _) + -> previous_offset >= 0 (* General constraint. *) + (* Either `ctx` is self-standing (doesn't depend on us), + * or it depends on us (and maybe other bindings to come), in + * which case we have to depend on the exact same bindings. *) + && (previous_offset <= 1 + || previous_offset = 1 + offset) + | _ -> true)); + Myers.cons (d, v, t) ctx + +let extend (ctx : t) (defs: (vname * lexp * ltype) list) : t = + let (ctx, _) = + List.fold_left + (fun (ctx, recursion_offset) (def, e, t) -> + cons ctx def (LetDef (recursion_offset, e)) t, + recursion_offset - 1) + (ctx, List.length defs) defs in + ctx + +let lookup_by_index index (ctx: t) : elem = + Myers.nth index ctx + +let lookup_set (s : IdxSet.t) (lctx : t) : (db_index * elem) Seq.t = + Myers.nthsi lctx (IdxSet.ascending_seq s) + +let pp_print_elem + (f : Format.formatter) + (i : db_index) + (r : db_offset) + (name : vname) + (e : lexp option) + (ty : ltype) + : unit = + + let open Format in + let name_text = string_of_vname name in + fprintf f "%% index = @{<green>%d@}, offset = @{<green>%d@}@." i r; + fprintf f "@[<hov 2>%s :@ %a;@]@." name_text Lexp.pp_print ty; + match e with + | Some e + -> let max_boxes = pp_get_max_boxes f () in + pp_set_max_boxes f 6; + fprintf f "@[<hov 2>%s =@ %a;@]@." name_text Lexp.pp_print e; + pp_set_max_boxes f max_boxes + | None -> () + +let pp_print_ranges + (f : Format.formatter) ~(ranges : (int * int) list) (lctx : t) + : unit = + + let open Format in + let print_range (lower, upper) = + for i = upper - 1 downto lower do + match lookup_by_index i lctx with + | (name, LetDef (r, exp), ty) -> pp_print_elem f i r name (Some exp) ty + | (name, _, ty) -> pp_print_elem f i 0 name None ty + | exception Not_found -> fatal "Missing variable at index %d" i + done + in + pp_print_string f (Fmt.make_title "Lexp Context"); + List.iter print_range ranges; + pp_print_string f (Fmt.make_sep '='); + pp_print_cut f () + +(** Print a summary of the context around a given offset, plus a few of the most + recently defined variables. *) +let summarize ~(around : int) (lctx : t) : unit = + let ranges = + if around < 7 + then [(0, min (max (around + 2) 5) (Myers.length lctx))] + else [(around - 2, min (around + 2) (Myers.length lctx)); (0, 5)] + in + let f = Fmt.formatter_of_out_channel stdout in + Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx; + print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full." + +(** Only print user defined variables *) +let print (lctx : t) : unit = + let ranges = [(0, Myers.length lctx - !builtin_size)] in + let f = Fmt.formatter_of_out_channel stdout in + Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx + +(** Print the whole context, including builtins. *) +let dump (lctx : t) : unit = + let ranges = [(0, Myers.length lctx)] in + let f = Fmt.formatter_of_out_channel stdout in + Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx + +let log_full = ref false + +(** Lookup a variable by reference. *) +let lookup (ctx : t) ((sinfo, oename), dbi : vref) : elem = + match Myers.nth dbi ctx, oename with + | exception Not_found + -> fatal + ~loc:(Sexp.location sinfo) + "DeBruijn index %d of `%s` out of bounds" + dbi + (maybename oename) + + (* Check if names match *) + | ((_, Some name), _, _), Some ename when name <> ename + -> let print_action = + if !log_full + then fun () -> print ctx + else fun () -> summarize ~around:dbi ctx + in + fatal + ~loc:(Sexp.location sinfo) ~print_action + {|DeBruijn index %d refers to wrong name. Expected "%s", but got "%s"|} + dbi ename name + + | ret, _ -> ret + +let lookup_type (ctx : t) ((_, i) as vref : vref) : lexp = + let (_, _, t) = lookup ctx vref in + mkSusp t (S.shift (i + 1)) + +let lookup_value (ctx : t) ((_, i) as vref : vref) : lexp option = + match lookup ctx vref with + | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) + | _ -> None + +(** Two contexts are equal if they have the same identity. *) +let equal : t -> t -> bool = (==) + +let hash : t -> int = Hashtbl.hash

===================================== src/opslexp.ml ===================================== @@ -61,7 +61,7 @@ module LMap (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end)

let reducible_builtins - = ref (SMap.empty : (DB.lexp_context + = ref (SMap.empty : (Lctx.t -> (P.arg_kind * lexp) list (* The builtin's args *) -> lexp option) SMap.t)

@@ -88,8 +88,8 @@ let impredicative_universe_poly = true (* Assume arg is TypeLevel.z when erasabl

(* Lexp context *)

-let lookup_type = DB.lctx_lookup_type -let lookup_value = DB.lctx_lookup_value +let lookup_type = Lctx.lookup_type +let lookup_value = Lctx.lookup_value

(** Extend a substitution S with a (mutually recursive) set * of definitions DEFS. @@ -171,7 +171,7 @@ 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 e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf e (ctx : Lctx.t) : lexp = match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e @@ -284,7 +284,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp =

| _elem -> e

-and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = +and lexp'_whnf e (ctx : Lctx.t) : lexp' = lexp_lexp' (lexp_whnf e ctx)

and eq_cast_whnf ctx args = @@ -355,7 +355,7 @@ and level_leq (c1, m1) (c2, m2) = m1

(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = +and conv_p' (ctx : Lctx.t) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in e1' == e2' || @@ -384,11 +384,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Arrow (_, ak1, vd1, t11, t12), Arrow (_, ak2, _vd2, t21, t22)) -> ak1 == ak2 && conv_p t11 t21 - && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') + && conv_p' (Lctx.cons ctx vd1 Variable t11) (set_shift vs') t12 (srename vd1 t22) | (Lambda (ak1, l1, t1, e1), Lambda (ak2, _l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) - && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) + && conv_p' (Lctx.cons ctx l1 Variable t1) (set_shift vs') e1 e2 | (Call (_, f1, args1), Call (_, f2, args2)) @@ -406,7 +406,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | ([], []) -> true | ((ak1,vd1,t1)::fields1, (ak2,_vd2,t2)::fields2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) + && conv_fields (Lctx.cons ctx vd1 Variable t1) (set_shift vs) fields1 fields2 | _,_ -> false in @@ -418,7 +418,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = SMap.equal (conv_fields ctx vs) cases1 cases2 | ((ak1,l1,t1)::args1, (ak2,_l2,t2)::args2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) + && conv_args (Lctx.cons ctx l1 Variable t1) (set_shift vs) args1 args2 | _,_ -> false in @@ -465,7 +465,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (Pexp.Aerasable, tltp); (* Inductive type *) (Pexp.Anormal, hlxp); (* Lexp of the branch head *) (Pexp.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (dsinfo, None) Variable eqty in + Lctx.cons ctx (dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types from the inductive. Instead, we work with the lists of @@ -481,7 +481,7 @@ 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)) + (Lctx.cons ctx vdef1 Variable (mkSusp ftype s)) ((ak1, (mkVar (vdef1, i)))::args) (ssink vdef1 s) (i - 1) @@ -507,7 +507,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = ) && (match (def1, def2) with | (Some (v1, e1), Some (_v2, e2)) -> - let nctx = DB.lctx_extend ctx v1 Variable etype in + let nctx = Lctx.cons ctx v1 Variable etype in let subst = S.shift 1 in let hlxp = mkVar ((dsinfo, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in @@ -520,7 +520,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = subst_eq s1 s2 | (_, _) -> false

-and conv_p (ctx : DB.lexp_context) e1 e2 +and conv_p (ctx : Lctx.t) e1 e2 = if e1 == e2 then true else conv_p' ctx set_empty e1 e2

@@ -582,8 +582,8 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = | (_, _) -> SortK1NotType

and dbset_push ak erased = - let nerased = DB.set_sink 1 erased in - if ak = P.Aerasable then DB.set_set 0 nerased else nerased + let nerased = IdxSet.sink 1 erased in + if ak = P.Aerasable then IdxSet.set 0 nerased else nerased

and nerased_let defs erased = (* Let bindings are not erasable, with the important exception of @@ -593,7 +593,7 @@ and nerased_let defs erased = * to pay attention to whether the var is erasable or not. *) (* FIXME: Maybe allow more cases of erasable let-bindings. *) - let nerased = DB.set_sink (List.length defs) erased in + let nerased = IdxSet.sink (List.length defs) erased in let es = List.map (fun (_v, e, _t) -> (* Look for `x = y` where `y` is an erasable var. @@ -601,7 +601,7 @@ and nerased_let defs erased = * will be non-erasable, so in `let x = z; y = x ...` * where `z` is erasable, `x` will be found * to be erasable, but not `y`. *) - match lexp_lexp' e with Var (_, idx) -> DB.set_mem idx nerased + match lexp_lexp' e with Var (_, idx) -> IdxSet.mem idx nerased | _ -> false) defs in if not (List.mem true es) then nerased else @@ -659,11 +659,11 @@ and check'' erased ctx e = * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t) - -> let _ = check_type DB.set_empty Myers.nil t in + -> let _ = check_type IdxSet.empty Myers.nil t in t (* FIXME: Check recursive references. *) | Var (((loc, name), idx) as v) - -> if DB.set_mem idx erased then + -> if IdxSet.mem idx erased then log_tc_error ~loc:(Sexp.location loc) {|Var `%s` can't be used here, because it's erasable|} @@ -673,17 +673,17 @@ and check'' erased ctx e = | Let (l, defs, e) -> let _ = List.fold_left (fun ctx (v, _e, t) - -> (let _ = check_type DB.set_empty ctx t in - DB.lctx_extend ctx v ForwardRef t)) + -> (let _ = check_type IdxSet.empty ctx t in + Lctx.cons ctx v ForwardRef t)) ctx defs in let nerased = nerased_let defs erased in - let nctx = DB.lctx_extend_rec ctx defs in + let nctx = Lctx.extend ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (_v, e, t) -> assert_type nctx e - (check (if DB.set_mem (n - 1) nerased - then DB.set_empty + (check (if IdxSet.mem (n - 1) nerased + then IdxSet.empty else nerased) nctx e) (push_susp t (S.shift n)); @@ -693,8 +693,8 @@ and check'' erased ctx e = (lexp_defs_subst l S.identity defs) | Arrow (loc, ak, v, t1, t2) -> (let k1 = check_type erased ctx t1 in - let nctx = DB.lexp_ctx_cons ctx v Variable t1 in - let k2 = check_type (DB.set_sink 1 erased) nctx t2 in + let nctx = Lctx.cons ctx v Variable t1 in + let k2 = check_type (IdxSet.sink 1 erased) nctx t2 in match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid @@ -707,16 +707,16 @@ and check'' erased ctx e = -> log_tc_error ~loc:(Lexp.location t2) "Not a proper type"; mkSort (loc, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) - -> (let _k = check_type DB.set_empty ctx t in + -> (let _k = check_type IdxSet.empty ctx t in mkArrow (l, ak, v, t, check (dbset_push ak erased) - (DB.lctx_extend ctx v Variable t) + (Lctx.cons ctx v Variable t) e)) | Call (_, f, args) -> let ft = check erased ctx f in List.fold_left (fun ft (ak,arg) - -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) + -> let at = check (if ak = P.Aerasable then IdxSet.empty else erased) ctx arg in match lexp'_whnf ft ctx with | Arrow (_l, ak', _v, t1, t2) @@ -761,12 +761,12 @@ and check'' erased ctx e = -> log_tc_error ~loc:(Lexp.location t) ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline ()) + Lctx.print ictx; print_newline ()) "Field type %s is not a Type! (%s)" (Lexp.to_string t) (Lexp.to_string lwhnf); level), - DB.lctx_extend ictx v Variable t, - DB.set_sink 1 erased, + Lctx.cons ictx v Variable t, + IdxSet.sink 1 erased, (* The final type(level) cannot refer * to the fields! *) S.cons @@ -781,9 +781,9 @@ and check'' erased ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> let _k = check_type DB.set_empty ctx t in + -> let _k = check_type IdxSet.empty ctx t in mkArrow (lexp_sinfo t, ak, v, t, - arg_loop (DB.lctx_extend ctx v Variable t) + arg_loop (Lctx.cons ctx v Variable t) (dbset_push ak erased) args) in let tct = arg_loop ctx erased args in @@ -872,7 +872,7 @@ and check'' erased ctx e = (Pexp.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) let nerased = dbset_push Pexp.Aerasable nerased in - let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in + let nctx = Lctx.cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter (fun name (l, vdefs, branch) @@ -884,7 +884,7 @@ and check'' erased ctx e = * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) + (Lctx.cons ctx vdef Variable (mkSusp ftype s)) (ssink vdef s) (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes @@ -907,8 +907,8 @@ and check'' erased ctx e = | Some (v, d) -> if diff <= 0 then log_tc_warning ~loc:(Sexp.location l) "Redundant default clause"; - let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - let nerased = DB.set_sink 1 erased in + let nctx = (Lctx.cons ctx v (LetDef (0, e)) etype) in + let nerased = IdxSet.sink 1 erased in let subst = S.shift 1 in let hlxp = mkVar ((l, None), 0) in let (nerased, nctx) = @@ -962,7 +962,7 @@ and check'' erased ctx e = | MVar (_, t, _) -> push_susp t s)

and check' ctx e = - let res = check'' DB.set_empty ctx e in + let res = check'' IdxSet.empty ctx e in (Log.stop_on_error (); res)

and check ctx e = check' ctx e @@ -995,14 +995,14 @@ and mv_set_erase (ms, _nes) = (ms, IMap.empty)

and fv_memo = LMap.create 1000

-and fv_empty = (DB.set_empty, mv_set_empty) +and fv_empty = (IdxSet.empty, mv_set_empty) and fv_union (fv1, mv1) (fv2, mv2) - = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) -and fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) -and fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) + = (IdxSet.union fv1 fv2, mv_set_union mv1 mv2) +and fv_sink n (fvs, mvs) = (IdxSet.sink n fvs, mvs) +and fv_hoist n (fvs, mvs) = (IdxSet.hoist n fvs, mvs) and fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)

-and fv (e : lexp) : (DB.set * mv_set) = +and fv (e : lexp) : IdxSet.t * mv_set = let fv' e = match lexp_lexp' e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty @@ -1011,7 +1011,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, Stype e) -> fv e | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty - | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Var (_, i) -> (IdxSet.singleton i, mv_set_empty) | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) @@ -1151,19 +1151,19 @@ and get_type ctx e = etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) - -> let nctx = DB.lctx_extend_rec ctx defs in + -> let nctx = Lctx.extend ctx defs in mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) | Arrow (l, ak, v, t1, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in - let nctx = DB.lexp_ctx_cons ctx v Variable t1 in + let nctx = Lctx.cons ctx v Variable t1 in let k2 = get_type nctx t2 in match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (l, ak, v, t, - get_type (DB.lctx_extend ctx v Variable t) + get_type (Lctx.cons ctx v Variable t) e)) | Call (_l, f, args) -> let ft = get_type ctx f in @@ -1194,7 +1194,7 @@ and get_type ctx e = -> mkSLlub ctx level (mkSusp level' subst) | _tt -> level), - DB.lctx_extend ictx v Variable t, + Lctx.cons ictx v Variable t, (* The final type(level) cannot refer * to the fields! *) S.cons @@ -1209,7 +1209,7 @@ and get_type ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> mkArrow (lexp_sinfo t, ak, v, t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in + arg_loop args (Lctx.cons ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret @@ -1258,7 +1258,7 @@ let _ = register_reducible_builtins () let erasure_dummy = DB.type0

let arity_of_cons - (lctx : DB.lexp_context) + (lctx : Lctx.t) (ty : lexp) (location, name : symbol) : int = @@ -1319,7 +1319,7 @@ let pos_of_label lctx label e : int = 0

-let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = +let rec erase_type (lctx : Lctx.t) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) @@ -1333,7 +1333,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy))

| L.Lambda (_, vdef, ty, body) - -> let lctx' = DB.lctx_extend lctx vdef Variable ty in + -> let lctx' = Lctx.cons lctx vdef Variable ty in E.Lambda (vdef, erase_type lctx' body)

| L.Let (l, decls, body) @@ -1367,10 +1367,10 @@ and clean_arg lctx = function | (_, lexp) -> Some (erase_type lctx lexp)

and clean_decls - (lctx : DB.lexp_context) + (lctx : Lctx.t) (decls : ldecl list) - : DB.lexp_context * (vname * E.elexp) list = - let lctx' = DB.lctx_extend_rec lctx decls in + : Lctx.t * (vname * E.elexp) list = + let lctx' = Lctx.extend lctx decls in (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls)

and clean_default lctx lxp = @@ -1389,7 +1389,7 @@ and clean_branch_map lctx cases = clean_arg_list tl acc (S.cons erasure_dummy subst) lctx | (_, var) :: tl -> (* Keep the variable and sink the substitution. *) - let lctx' = DB.lctx_extend lctx var Variable erasure_dummy in + let lctx' = Lctx.cons lctx var Variable erasure_dummy in clean_arg_list tl (var :: acc) (ssink var subst) lctx' | [] -> (List.rev acc, subst, lctx) in @@ -1418,11 +1418,11 @@ let erase_type lctx lxp = (* Textually identical to the previous definition of `clean_decls`, but calls the new `erase_type`, which checks for metavars. *) let clean_decls - (lctx : DB.lexp_context) + (lctx : Lctx.t) (decls : ldecl list) - : DB.lexp_context * (vname * E.elexp) list = + : Lctx.t * (vname * E.elexp) list =

- let lctx' = DB.lctx_extend_rec lctx decls in + let lctx' = Lctx.extend lctx decls in (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls)

(** Turning a set of declarations into an object. **)

===================================== src/positivity.ml ===================================== @@ -50,7 +50,7 @@ open Util (* Computes if the judgement x ∉ fv(τ) holds. *) let absent index lexp = let fv, _ = Opslexp.fv lexp in - not (Debruijn.set_mem index fv) + not (IdxSet.mem index fv)

let rec absent_in_bindings index bindings = match bindings with

===================================== src/unification.ml ===================================== @@ -37,7 +37,7 @@ let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int) (!metavar_table); idx

-let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) +let create_metavar (ctx : Lctx.t) (sl : scope_level) (t : ltype) = create_metavar_1 sl t (Myers.length ctx)

let dloc = DB.dloc @@ -50,7 +50,7 @@ type constraint_kind = (* FIXME: Each constraint should additionally come with a description of how it relates to its "top-level" or some other info which might let us fix the problem (e.g. by introducing coercions). *) -type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list +type constraints = (constraint_kind * Lctx.t * lexp * lexp) list

type return_type = constraints

@@ -215,12 +215,12 @@ let matching_instantiation_check *) let rec unify ?(matching : scope_level option) (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) + (ctx : Lctx.t) : return_type = unify' e1 e2 ctx OL.set_empty matching

and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_plexp) + (ctx : Lctx.t) (vs : OL.set_plexp) (msl : scope_level option) (* matching mode optional scope level *) : return_type = if e1 == e2 then [] else @@ -290,7 +290,7 @@ and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 (srename v1 lexp2) - (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (Lctx.cons ctx v1 Variable ltype1) (OL.set_shift vs) matching) else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)] @@ -308,7 +308,7 @@ and unify_lambda (matching : scope_level option) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (Lctx.cons ctx v1 Variable ltype1) (OL.set_shift vs) matching) else [(CKimpossible, ctx, lambda, lxp)] | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] @@ -626,7 +626,7 @@ and unify_inductive' (matching : scope_level option) ctx vs (ctx, vs, [(CKimpossible, ctx, e1, e2)]) else List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, _v2, t2)) - -> (DB.lexp_ctx_cons ctx v1 Variable t1, + -> (Lctx.cons ctx v1 Variable t1, OL.set_shift vs, if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] else (unify' t1 t2 ctx vs matching) @ residue))

===================================== src/util.ml ===================================== @@ -22,6 +22,7 @@ this program. If not, see http://www.gnu.org/licenses/. *)

module SMap = Map.Make(String) module IMap = Map.Make(Int) +module ISet = Set.Make(Int)

type location = Source.Location.t let dummy_location = Source.Location.dummy

===================================== tests/instargs_test.ml ===================================== @@ -88,7 +88,7 @@ instance d; match L.lexp_lexp' (lexp_from_str lstr ctx) with | L.Var (_,idx) -> add_test ("is `" ^ lstr ^ "` an instance ?") (fun _ -> - expect_equal_bool (DB.set_mem idx insts) b + expect_equal_bool (IdxSet.mem idx insts) b ) | _ -> failwith "Impossible" ) [("a", true); ("b", false); ("c", false); ("d", true)])

===================================== typer.ml ===================================== @@ -39,7 +39,7 @@ let arg_defs = ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity");

("-Vfull-lctx", - Arg.Set Debruijn.log_full_lctx, + Arg.Set Lctx.log_full, "Print the full lexp context on error");

("-Vmacro-expansion",

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/54bdd38af3aad1ebc85ebcd709792aa68...