Alice de Berny pushed to branch alice at Stefan / Typer

Commits: ab6585a3 by irradiee at 2020-06-16T05:54:24-04:00 hash consing of substitutions

- - - - -

15 changed files:

- src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - + src/lexp_type.ml - src/opslexp.ml - src/sexp.ml - src/subst.ml - src/unification.ml - src/util.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -44,6 +44,7 @@ open Prelexer open Lexer open Sexp open Pexp +open Lexp_type open Lexp

open Eval @@ -231,7 +232,8 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%collisions" | "%cl" -> (get_stats hc_table) + | "%lcollisions" | "%cl" -> (get_stats (WHC.stats hc_table)) + | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table))

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> (

===================================== src/builtin.ml ===================================== @@ -57,7 +57,7 @@ open Util

open Sexp (* Integer/Float *) open Pexp (* arg_kind *) -module L = Lexp +open Lexp_type module OL = Opslexp open Lexp

===================================== src/debruijn.ml ===================================== @@ -35,8 +35,10 @@ module Str = Str

open Util + +open Lexp_type open Lexp -module L = Lexp + module M = Myers open Fmt

@@ -300,7 +302,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start =

(* Only print user defined variables *) let print_lexp_ctx (ctx : lexp_context) = - print_lexp_ctx_n ctx !L.builtin_size + print_lexp_ctx_n ctx !builtin_size

(* Dump the whole context *) let dump_lexp_ctx (ctx : lexp_context) =

===================================== src/elab.ml ===================================== @@ -45,6 +45,7 @@ open Lexer

open Sexp open Pexp +open Lexp_type open Lexp

open Env @@ -394,23 +395,23 @@ let rec meta_to_var ids (e : lexp) = *)

(* `o` is the binding offset until the root. *) - let rec adjust_subst o s = match s with - | S.Identity n + let rec adjust_subst o (s : lsubst) = match S.subst_subst' s with + | Identity n -> let o' = o - n in if o' < 0 then (* This metavar's original context is outside of our scope * (case (B) above), so don't let it refer to the new vars. *) - S.Identity (n + count) + S.hcsb (Identity (n + count)) else - Identity n - | S.Cons (e, s', n) + S.hcsb (Identity n) + | Cons (e, s', n) -> let o' = o - n in if o' < 0 then (* This metavar's original context is outside of our scope * (case (B) above), so don't let it refer to the new vars. *) - S.Cons (e, s', n + count) + S.hcsb (Cons (e, s', n + count)) else - S.Cons (loop o' e, adjust_subst o' s', n) + S.hcsb (Cons (loop o' e, adjust_subst o' s', n))

(* `o` is the binding depth at which we are relative to the "root" * of the expression (i.e. where the new vars will be inserted). *)

===================================== src/elexp.ml ===================================== @@ -35,6 +35,7 @@ open Sexp (* Sexp type *) open Pexp (* Anormal *)

module U = Util +module LT = Lexp_type module L = Lexp

type vname = U.vname @@ -77,7 +78,7 @@ type elexp =

(* A Type expression. There's no useful operation we can apply to it, * but they can appear in the code. *) - | Type of L.lexp + | Type of LT.lexp

let rec elexp_location e = match e with

===================================== src/env.ml ===================================== @@ -36,6 +36,7 @@ open Sexp

open Elexp module M = Myers +module LT = Lexp_type module L = Lexp module BI = Z (* Was Big_int *) module DB = Debruijn @@ -58,7 +59,7 @@ type value_type = | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined - | Vtype of L.lexp (* The lexp value can't be trusted. *) + | Vtype of LT.lexp (* The lexp value can't be trusted. *) | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) @@ -241,7 +242,7 @@ let print_rte_ctx_n (ctx: runtime_env) start =

(* Only print user defined variables *) let print_rte_ctx ctx = - print_rte_ctx_n ctx (!L.builtin_size) + print_rte_ctx_n ctx (!LT.builtin_size)

(* Dump the whole context *) let dump_rte_ctx ctx =

===================================== src/eval.ml ===================================== @@ -35,6 +35,7 @@ open Fmt

open Sexp open Pexp (* Arg_kind *) +open Lexp_type open Lexp (* Varbind *)

open Elexp

===================================== src/inverse_subst.ml ===================================== @@ -39,6 +39,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) * So either left or right inverse can be used! *)

+open Lexp_type open Lexp open Util module S = Subst @@ -56,8 +57,8 @@ 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: Lexp.subst) : substIR option = - let rec transfo (s: Lexp.subst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: lsubst) : substIR option = + let rec transfo (s: lsubst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) let v' = lexp_lexp' v in @@ -68,8 +69,8 @@ let transfo (s: Lexp.subst) : substIR option = let shiftVar (var: lexp) (offset: int): int = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in - match s with - | S.Cons ((Var _ as v, h), s, o) -> + match S.subst_subst' s with + | Cons ((Var _ as v, h), s, o) -> let off_acc = off_acc + o in (match transfo s off_acc (idx + 1) imp_cnt with | Some (tail, off, imp) @@ -77,15 +78,15 @@ let transfo (s: Lexp.subst) : substIR option = in if newVar >= off then None (* Error *) else Some (((shiftVar (v, h) off_acc), idx)::tail, off, imp) | None -> None) - | S.Cons ((Imm (Sexp.Symbol (_, "")), _), s, o) + | Cons ((Imm (Sexp.Symbol (_, "")), _), s, o) -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) - | S.Identity o -> Some ([], (o + off_acc), imp_cnt) + | Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) in transfo s 0 0 0

(* Inverse *)

-(** Returns the number of element in a sequence of S.Cons +(** Returns the number of element in a sequence of Cons *) let rec sizeOf (s: (int * int) list): int = List.length s

@@ -94,7 +95,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Lexp.mkVar ((U.dummy_location, None), idx) + mkVar ((U.dummy_location, None), idx)

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -105,18 +106,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: Lexp.subst): Lexp.subst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = + let rec genDummyVar (beg_: int) (end_: int) (l: lsubst): lsubst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: Lexp.subst) (nbVar: int): Lexp.subst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: lsubst) (nbVar: int): lsubst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None

@@ -143,11 +144,11 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = | None -> None | Some s -> fill_before l s nbVar

-let is_identity s = - let rec is_identity s acc = - match s with - | S.Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) - | S.Identity o -> acc = o +let is_identity (s : lsubst) = + let rec is_identity (s : lsubst) acc = + match S.subst_subst' s with + | Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0

@@ -155,7 +156,7 @@ let is_identity s =

<code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: Lexp.subst) : Lexp.subst option = +let inverse (s: lsubst) : lsubst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -181,9 +182,9 @@ let inverse (s: Lexp.subst) : Lexp.subst option = (* Returns false if the application of the inverse substitution is not * possible. This happens when the substitution replaces some variables * with non-variables, in which case the "inverse" is ambiguous. *) -let rec invertible (s: subst) : bool = match s with - | S.Identity _ -> true - | S.Cons (e, s, _) +let rec invertible (s: lsubst) : bool = match S.subst_subst' s with + | Identity _ -> true + | Cons (e, s, _) -> (let e' = lexp_lexp' e in match e' with Var _ -> true | _ -> e = impossible) && invertible s @@ -192,16 +193,16 @@ exception Not_invertible exception Ambiguous

(* Lookup variable i in s⁻¹ *) -let rec lookup_inv_subst (i : db_index) (s : subst) : db_index - = match s with - | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible - | S.Identity o -> i - o - | S.Cons ((Var (_, i'), _), s, o) when i' = i - o +let rec lookup_inv_subst (i : db_index) (s : lsubst) : db_index + = match S.subst_subst' s with + | (Identity o | Cons (_, _, o)) when i < o -> raise Not_invertible + | Identity o -> i - o + | Cons ((Var (_, i'), _), s, o) when i' = i - o -> (try let i'' = lookup_inv_subst i' s in assert (i'' != 0); raise Ambiguous with Not_invertible -> 0) - | S.Cons (e, s, o) + | Cons (e, s, o) -> assert (let e' = lexp_lexp' e in match e' with Var _ -> true | _ -> e = impossible); @@ -239,12 +240,12 @@ let shift_inv_subst n s * One way to do it is to compute s⁻¹ and then pass it to `compose`. * But we can try and do it more directly. *) -let rec compose_inv_subst (s' : subst) (s : subst) = match s' with - | S.Cons (e, s', o) -> +let rec compose_inv_subst (s' : lsubst) (s : lsubst) = match S.subst_subst' s' with + | 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.Identity o -> (match inverse (shift_inv_subst o s) with + | Identity o -> (match inverse (shift_inv_subst o s) with | Some s -> s (* FIXME: could also be Ambiguous, depending on `s`. *) | None -> raise Not_invertible) @@ -253,7 +254,7 @@ 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 : lsubst) : lexp = let e' = lexp_lexp' e in match e' with | Imm _ -> e

===================================== src/lexp.ml ===================================== @@ -20,161 +20,25 @@ 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/. *)

-module U = Util -module L = List -module SMap = U.SMap +(* open Unify *) +module S = Subst + open Fmt

open Sexp open Pexp

+open Lexp_type + open Myers open Grammar

-(* open Unify *) -module S = Subst - -type vname = U.vname -type vref = U.vref -type meta_id = int (* Identifier of a meta variable. *) - -type label = symbol - -type attribute_key = (int * string) (* rev_dbi * Var name *) -module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) - -(*************** Elaboration to Lexp *********************) - -(* The scoping of `Let` is tricky: - * - * Since it's a recursive let, the definition part of each binding is - * valid in the "final" scope which includes all the new bindings. - * - * But the type of each binding is not defined in that same scope. Instead - * it's defined in the scope of all the previous bindings. - * - * For exemple the type of the second binding of such a Let is defined in - * the scope of the surrounded context extended with the first binding. - * And the type of the 3rd binding is defined in the scope of the - * surrounded context extended with the first and the second bindings. *) - -type ltype = lexp -and subst = subst' * int - and subst' = lexp S.subst - and lexp = lexp' * int - and lexp' = - | Imm of sexp (* Used for strings, ... *) - | SortLevel of sort_level - | Sort of U.location * sort - | Builtin of symbol * ltype * lexp AttributeMap.t option - | Var of vref - | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) - (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype - | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t - | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp - * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t - * (vname * lexp) option (* Default. *) - (* The `subst` will be applied to the the metavar's value when it - * gets instantiated. *) - | Metavar of meta_id * subst * vname - (* (* For logical metavars, there's no substitution. *) - * | Metavar of (U.location * string) * metakind * metavar ref - * and metavar = - * (* An uninstantiated var, along with a venv (stipulating over which vars - * * it should be closed), and its type. - * * If its type is not given, it implies its type should be a sort. *) - * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level - * | MetaSet of lexp - * and metakind = - * | MetaGraft of subst - * (* Forward reference or Free var: Not known yet, but not instantiable by - * * unification. *) - * | MetaFoF - * and subst = lexp VMap.t *) - (* - * The PTS I'm imagining looks like: - * - * S = { TypeLevel, TypeOmega, Type ℓ } - * A = { Level : TypeLevel, Z : Level, S : Level → Level, - * Type : (ℓ : Level) → Type (S ℓ) } - * R = { (TypeLevel, Type ℓ, TypeOmega), - * (TypeLevel, TypeOmega, TypeOmega), - * (Type ℓ, TypeOmega, TypeOmega), - * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } - *) - and sort = - | Stype of lexp - | StypeOmega - | StypeLevel - and sort_level = - | SLz - | SLsucc of lexp - | SLlub of lexp * lexp - -type varbind = - | Variable - | ForwardRef - | LetDef of U.db_offset * lexp - -(* For metavariables, we give each metavar a (hopefully) unique integer - * and then we store its corresponding info into the `metavar_table` - * global map. - * - * Instead of this single ref-cell holding an IntMap, we could use many - * ref-cells, and do away with the unique integer. The reasons why we - * do it this way are: - * - for printing purposes, we want to have a printable unique identifier - * for each metavar. OCaml does not offer any way to turn a ref-cell - * into some kind of printable identifier (can't get a hash of the address, - * no `eq` hash-tables, ...). - * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: - * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique - * integer in order to produce a hash anyway (and we'd have to write the hash - * function by hand, tho that might be a good idea anyway). - *) - -(* Scope level is used to detect "out of scope" metavars. - * See http://okmij.org/ftp/ML/generalization.html - * The ctx_length keeps track of the length of the lctx in which the - * metavar is meant to be defined. *) -type scope_level = int -type ctx_length = int - -type metavar_info = - | MVal of lexp (* Exp to which the var is instantiated. *) - | MVar of scope_level (* Outermost scope in which the var appears. *) - * ltype (* Expected type. *) - (* We'd like to keep the lexp_content in which the type is to be - * understood, but lexp_context is not yet defined here, - * so we just keep the length of the lexp_context. *) - * ctx_length -type meta_subst = metavar_info U.IMap.t - -let dummy_scope_level = 0 - -let builtin_size = ref 0 - -let metavar_table = ref (U.IMap.empty : meta_subst) -let metavar_lookup (id : meta_id) : metavar_info - = try U.IMap.find id (!metavar_table) - with Not_found - -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" - (********************** Hash-consing **********************)

-(* let hc_table : (lexp, lexp) Hashtbl.t = Hashtbl.create 1000 - * let hc (e : lexp) : lexp = - * try Hashtbl.find hc_table e - * with Not_found -> Hashtbl.add hc_table e e; e *) - let lexp_hash (e, h) = h + (** hash-consing test ** + * with: Hashtbl.hash - lexp'_hash + * median bucket length: 7 - 7 + * biggest bucket length: 205 - 22 *)

let lexp_lexp' (e, h) = e

@@ -183,57 +47,55 @@ let metavar_lookup (id : meta_id) : metavar_info | [] -> 31 | e :: l -> (e * 31) lxor (apply_lxor l)

-let combine_hash e1 e2 = (e1 * 31) lxor e2 - (* Hashtbl.hash for not lexp types * TODO: - find something else * - extract the first arg of 2 arg types ? (SMap) *) let lexp'_hash (expr : lexp') = match expr with - | Imm s -> combine_hash 1 (Hashtbl.hash s) + | Imm s -> U.combine_hash 1 (Hashtbl.hash s) | SortLevel l - -> combine_hash 2 (match l with + -> U.combine_hash 2 (match l with | SLz -> Hashtbl.hash l | SLsucc lp -> lexp_hash lp - | SLlub (lp1, lp2) -> combine_hash (lexp_hash lp1) (lexp_hash lp2)) + | SLlub (lp1, lp2) -> U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) | Sort (l, s) - -> combine_hash 3 (combine_hash (Hashtbl.hash l) + -> U.combine_hash 3 (U.combine_hash (Hashtbl.hash l) (match s with | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) as e -> combine_hash 4 (Hashtbl.hash e) - | Var v -> combine_hash 5 (Hashtbl.hash v) + | Builtin (v, t, m) as e -> U.combine_hash 4 (Hashtbl.hash e) + | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) - -> combine_hash 6 (combine_hash (Hashtbl.hash l) - (combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in - (combine_hash (Hashtbl.hash n) (combine_hash (lexp_hash lp) (lexp_hash lt)))) + -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in + (U.combine_hash (Hashtbl.hash n) (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) | Arrow (k, v, t1, l, t2) - -> combine_hash 7 (combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (combine_hash (lexp_hash t1) (combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + -> U.combine_hash 7 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t1) (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) | Lambda (k, v, t, e) - -> combine_hash 8 (combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (combine_hash (lexp_hash t) (lexp_hash e))) + -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t) (lexp_hash e))) | Inductive (l, n, a, cs) - -> combine_hash 9 (combine_hash (combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) - (combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in - (combine_hash (Hashtbl.hash ak) - (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) + -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) + (U.combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in + (U.combine_hash (Hashtbl.hash ak) + (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) (Hashtbl.hash cs))) - | Cons (t, n) -> combine_hash 10 (combine_hash (lexp_hash t) (Hashtbl.hash n)) + | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) - -> combine_hash 11 (combine_hash (combine_hash (Hashtbl.hash l) (lexp_hash e)) - (combine_hash (lexp_hash rt) (combine_hash (Hashtbl.hash bs) + -> U.combine_hash 11 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (lexp_hash e)) + (U.combine_hash (lexp_hash rt) (U.combine_hash (Hashtbl.hash bs) (match d with - | Some (n, lp) -> combine_hash (Hashtbl.hash n) (lexp_hash lp) + | Some (n, lp) -> U.combine_hash (Hashtbl.hash n) (lexp_hash lp) | _ -> 0)))) | Metavar (id, s, v) - -> combine_hash 12 (Hashtbl.hash expr) - | Call (e, args) -> combine_hash 13 (combine_hash (lexp_hash e) + -> U.combine_hash 12 (Hashtbl.hash expr) + | Call (e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (apply_lxor (List.map (fun e -> let (ak, lp) = e in - (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) - | Susp (lp, subst) -> combine_hash 14 (combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) + | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst))

let compare_hash x y = let (x', h1) = x in @@ -256,6 +118,7 @@ let hc_eq e1 e2 = | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 + (* TODO: == via hcs ? *) | ((Susp (e1, s1) as e), _) -> compare e (lexp_lexp' e2) = 0 | (_, (Susp (e2, s2) as e)) -> compare (lexp_lexp' e1) e = 0 | (Let (_, defs1, e1), Let (_, defs2, e2)) @@ -306,15 +169,6 @@ let hc_table : WHC.t = WHC.create 1000 let hc (e : lexp') : lexp = let lp = (e, lexp'_hash e) in WHC.merge hc_table lp

-let get_stats table = - let (tl, ne, sumb, smallb, medianb, bigb) = WHC.stats table in - Printf.printf "\n\ttable length: %i\n - number of entries: %i\n - sum of bucket lengths: %i\n - smallest bucket length: %i\n - median bucket length: %i\n - biggest bucket length: %i\n" tl ne sumb smallb medianb bigb - let impossible = hc (Imm Sexp.dummy_epsilon)

let mkImm s = hc (Imm s) @@ -387,41 +241,7 @@ let mkSLsucc e = * but Weak.Make doesn't cut it because we need to index with a pair * that is transient and hence immediately GC'd. *)

-(* try... *) -type subst_pair = ((lexp * subst) * lexp) - -let subst_hash (s, h) = h - - let hcs_eq sb1 sb2 = - sb1 == sb2 || - match (sb1, sb2) with - | (((l1, S.Identity off), l2), ((l1', S.Identity off'), l2')) - -> l1 == l1' && off = off' && l2 == l2' - | (((l1, S.Cons (lp1, lps1, off1)), l2), ((l1', S.Cons (lp2, lps2, off2)), l2')) - -> l1 == l1' && lp1 == lp2 && lps1 == lps2 && off1 = off2 && l2 == l2' - | _ -> false - - let subst'_hash sb : int = - match sb with - | ((l1, S.Identity off), l2) - -> combine_hash 1 (combine_hash (lexp_hash l1) - (combine_hash (Hashtbl.hash off) (lexp_hash l2))) - | ((l1, S.Cons (lp, sb, off)), l2) - -> combine_hash 2 (combine_hash (lexp_hash l1) - (combine_hash (combine_hash (lexp_hash lp) (subst_hash sb)) - (combine_hash (Hashtbl.hash off) (lexp_hash l2)))) - - module WHCS = Hashtbl.Make (struct type t = subst_pair - let equal x y = hcs_eq x y - let hash = subst_hash - end) - -let hcs_table : WHCS.t = WHCS.create 1000 - -(* let hcs (s : subst') : subst = - let sb = (s, subst'_hash s) in WHCS.merge hcsb_table sb *) - -(******) +let hcs_table : ((lexp * lexp subst), lexp) Hashtbl.t = Hashtbl.create 1000

(* When computing the type of "load"ed modules * we end up building substitutions of the form @@ -799,10 +619,10 @@ let rec lexp_unparse lxp = (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp)

-and subst_string s = match s with - | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s - | S.Cons (l, s, o) +and subst_string s = match S.subst_subst' s with + | Identity o -> "↑" ^ string_of_int o + | Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s + | Cons (l, s, o) -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"

and lexp_name e = @@ -1185,9 +1005,9 @@ let rec eq e1 e2 =

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)) + match (S.subst_subst' s1, S.subst_subst' s2) with + | (Identity o1, Identity o2) -> o1 = o2 + | (Cons (e1, s1, o1), Cons (e2, s2, o2)) -> if o1 = o2 then eq e1 e2 && subst_eq s1 s2 else if o1 > o2 then

===================================== src/lexp_type.ml ===================================== @@ -0,0 +1,174 @@ +module U = Util +module L = List +module SMap = U.SMap + + +open Sexp +open Pexp + + +type vname = U.vname +type vref = U.vref +type meta_id = int (* Identifier of a meta variable. *) + +type label = symbol + +type attribute_key = (int * string) (* rev_dbi * Var name *) +module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) + +(* We define here substitutions which take a variable within a source context + * Δₛ and should return an expression valid in target context Δₜ. + * + * The current implementation only handles a very limited subset of such + * substitutions. One of the many limitations is that we can only encode + * substitutions which map variables to variables. + *) + +type db_index = int (* DeBruijn index. *) +type db_offset = int (* DeBruijn index offset. *) + +(* Substitution, i.e. a mapping from db_index to 'a + * In practice, 'a is always lexp, but we keep it as a parameter: + * - for better modularity of the code. + * - to break a mutual dependency between the Lexp and the Subst modules. *) +type 'a subst = 'a subst' * int + and 'a subst' = (* lexp subst *) + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * 'a subst * db_offset *) +(* Lift (n,m) increases indices≥N by M. + * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination + * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) + (* | Lift of db_index * db_offset *) + +(* Build Myers's "stack" element. *) +(* let mkCons e s o = match s with + * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 + * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) + * | _ -> Cons (e, s, o, 1, s, o) *) + +(*************** Elaboration to Lexp *********************) + +(* The scoping of `Let` is tricky: + * + * Since it's a recursive let, the definition part of each binding is + * valid in the "final" scope which includes all the new bindings. + * + * But the type of each binding is not defined in that same scope. Instead + * it's defined in the scope of all the previous bindings. + * + * For exemple the type of the second binding of such a Let is defined in + * the scope of the surrounded context extended with the first binding. + * And the type of the 3rd binding is defined in the scope of the + * surrounded context extended with the first and the second bindings. *) + +type ltype = lexp + and lsubst = lexp subst + and lexp = lexp' * int + and lexp' = + | Imm of sexp (* Used for strings, ... *) + | SortLevel of sort_level + | Sort of U.location * sort + | Builtin of symbol * ltype * lexp AttributeMap.t option + | Var of vref + | Susp of lexp * lsubst (* Lazy explicit substitution: e[σ]. *) + (* This "Let" allows recursion. *) + | Let of U.location * (vname * lexp * ltype) list * lexp + | Arrow of arg_kind * vname * ltype * U.location * ltype + | Lambda of arg_kind * vname * ltype * lexp + | Call of lexp * (arg_kind * lexp) list (* Curried call. *) + | Inductive of U.location * label + * ((arg_kind * vname * ltype) list) (* formal Args *) + * ((arg_kind * vname * ltype) list) SMap.t + | Cons of lexp * symbol (* = Type info * ctor_name *) + | Case of U.location * lexp + * ltype (* The type of the return value of all branches *) + * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (vname * lexp) option (* Default. *) + (* The `subst` will be applied to the the metavar's value when it + * gets instantiated. *) + | Metavar of meta_id * lsubst * vname + (* (* For logical metavars, there's no substitution. *) + * | Metavar of (U.location * string) * metakind * metavar ref + * and metavar = + * (* An uninstantiated var, along with a venv (stipulating over which vars + * * it should be closed), and its type. + * * If its type is not given, it implies its type should be a sort. *) + * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level + * | MetaSet of lexp + * and metakind = + * | MetaGraft of subst + * (* Forward reference or Free var: Not known yet, but not instantiable by + * * unification. *) + * | MetaFoF + * and subst = lexp VMap.t *) + (* + * The PTS I'm imagining looks like: + * + * S = { TypeLevel, TypeOmega, Type ℓ } + * A = { Level : TypeLevel, Z : Level, S : Level → Level, + * Type : (ℓ : Level) → Type (S ℓ) } + * R = { (TypeLevel, Type ℓ, TypeOmega), + * (TypeLevel, TypeOmega, TypeOmega), + * (Type ℓ, TypeOmega, TypeOmega), + * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } + *) + and sort = + | Stype of lexp + | StypeOmega + | StypeLevel + and sort_level = + | SLz + | SLsucc of lexp + | SLlub of lexp * lexp + +type varbind = + | Variable + | ForwardRef + | LetDef of U.db_offset * lexp + + let lexp_hash (e, h) = h +(* For metavariables, we give each metavar a (hopefully) unique integer + * and then we store its corresponding info into the `metavar_table` + * global map. + * + * Instead of this single ref-cell holding an IntMap, we could use many + * ref-cells, and do away with the unique integer. The reasons why we + * do it this way are: + * - for printing purposes, we want to have a printable unique identifier + * for each metavar. OCaml does not offer any way to turn a ref-cell + * into some kind of printable identifier (can't get a hash of the address, + * no `eq` hash-tables, ...). + * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: + * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique + * integer in order to produce a hash anyway (and we'd have to write the hash + * function by hand, tho that might be a good idea anyway). + *) + +(* Scope level is used to detect "out of scope" metavars. + * See http://okmij.org/ftp/ML/generalization.html + * The ctx_length keeps track of the length of the lctx in which the + * metavar is meant to be defined. *) +type scope_level = int +type ctx_length = int + +type metavar_info = + | MVal of lexp (* Exp to which the var is instantiated. *) + | MVar of scope_level (* Outermost scope in which the var appears. *) + * ltype (* Expected type. *) + (* We'd like to keep the lexp_content in which the type is to be + * understood, but lexp_context is not yet defined here, + * so we just keep the length of the lexp_context. *) + * ctx_length +type meta_subst = metavar_info U.IMap.t + +let dummy_scope_level = 0 + +let builtin_size = ref 0 + +let metavar_table = ref (U.IMap.empty : meta_subst) +let metavar_lookup (id : meta_id) : metavar_info + = try U.IMap.find id (!metavar_table) + with Not_found + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!"

===================================== src/opslexp.ml ===================================== @@ -30,6 +30,7 @@ module P = Pexp (* open Grammar *) open Lexp module E = Elexp +open Lexp_type module L = Lexp module M = Myers

@@ -933,38 +934,38 @@ let rec get_type ctx e =

(*********** Type erasure, before evaluation. *****************)

-let rec erase_type (lxp: L.lexp): E.elexp = +let rec erase_type (lxp: lexp): E.elexp = let lxp' = lexp_lexp' lxp in match lxp' with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) - | L.Lambda (P.Aerasable, _, _, body) -> + | Imm(s) -> E.Imm(s) + | Builtin(v, _, _) -> E.Builtin(v) + | Var(v) -> E.Var(v) + | Cons(_, s) -> E.Cons(s) + | Lambda (P.Aerasable, _, _, body) -> (* The var shouldn't appear in body, basically, but we need * to adjust the debruijn indices of other vars, hence the subst. *) erase_type (L.push_susp body (S.substitute DB.type0)) - | L.Lambda (_, vdef, _, body) -> + | Lambda (_, vdef, _, body) -> E.Lambda (vdef, erase_type body)

- | L.Let(l, decls, body) -> + | Let(l, decls, body) -> E.Let(l, (clean_decls decls), (erase_type body))

- | L.Call(fct, args) -> + | Call(fct, args) -> E.Call((erase_type fct), (filter_arg_list args))

- | L.Case(l, target, _, cases, default) -> + | Case(l, target, _, cases, default) -> E.Case(l, (erase_type target), (clean_map cases), (clean_maybe default))

- | L.Susp(l, s) -> erase_type (L.push_susp l s) + | Susp(l, s) -> erase_type (L.push_susp l s)

(* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp + | Arrow _ -> E.Type lxp + | SortLevel _ -> E.Type lxp + | Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | Inductive(l, label, _, _) -> E.Type lxp | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s)

===================================== src/sexp.ml ===================================== @@ -258,4 +258,3 @@ and sexp_eq_list ss1 ss2 = match ss1, ss2 with | (s1 :: ss1), (s2 :: ss2) -> sexp_equal s1 s2 && sexp_eq_list ss1 ss2 | _ -> false -

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

module U = Util +open Lexp_type

(* Implementation of the subsitution calculus. * @@ -103,43 +104,49 @@ module U = Util * *)

-(* We define here substitutions which take a variable within a source context - * Δₛ and should return an expression valid in target context Δₜ. - * - * The current implementation only handles a very limited subset of such - * substitutions. One of the many limitations is that we can only encode - * substitutions which map variables to variables. - *) + (********************** Hash-consing **********************) + + (** hash-consing test ** + * with: subst'_hash + * median bucket length: 7 + * biggest bucket length: 22 *) + + let subst_hash (s, h) = h + let subst_subst' (s, h) = s + + let hcsb_eq sb1 sb2 = + sb1 == sb2 || + match (subst_subst' sb1, subst_subst' sb2) with + | (Identity off1, Identity off2) -> off1 = off2 + | (Cons (lp1, lps1, off1), Cons (lp2, lps2, off2)) + -> lp1 == lp2 && lps1 == lps2 && off1 = off2 + | _ -> false + + let subst'_hash (sb : 'a subst') : int = + match sb with + | Identity off + -> U.combine_hash 1 (Hashtbl.hash off) + | Cons (lp, sb, off) + -> U.combine_hash 2 + (U.combine_hash (U.combine_hash + (lexp_hash lp) (subst_hash sb)) (Hashtbl.hash off)) + + module WHCSB = Weak.Make (struct type t = lexp subst + let equal x y = hcsb_eq x y + let hash = subst_hash + end) + + let hcsb_table : WHCSB.t = WHCSB.create 1000

-type db_index = int (* DeBruijn index. *) -type db_offset = int (* DeBruijn index offset. *) - -(* Substitution, i.e. a mapping from db_index to 'a - * In practice, 'a is always lexp, but we keep it as a parameter: - * - for better modularity of the code. - * - to break a mutual dependency between the Lexp and the Subst modules. *) -type 'a subst = (* lexp subst *) - | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) - | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) - (* Myers's extra pointers down the list: - * * int * 'a subst * db_offset *) -(* Lift (n,m) increases indices≥N by M. - * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination - * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - (* | Lift of db_index * db_offset *) - -(* Build Myers's "stack" element. *) -(* let mkCons e s o = match s with - * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 - * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) - * | _ -> Cons (e, s, o, 1, s, o) *) + let hcsb (s : lexp subst') : lexp subst = + let sb = (s, subst'_hash s) in WHCSB.merge hcsb_table sb

(* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a) (mkShift: 'a -> db_offset -> 'a) (s: 'a subst) (l : 'b) (v:db_index) : 'a = let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = - match s with + match subst_subst' s with | Identity o' -> mkVar l (v + o + o') (* Use Myers's fastlane when applicable: * | Cons (_, _, _, sk, s, o') when v >= sk -> lookup' (o + o') s (v - sk) *) @@ -148,26 +155,27 @@ let lookup (mkVar : 'b -> db_index -> 'a) else mkShift e o in lookup' 0 s v

+(* ici *) let mkShift s (m:db_offset) = if m>0 then - match s with Identity o -> Identity (o + m) - | Cons (e, s, o) -> Cons (e, s, o + m) + match subst_subst' s with Identity o -> hcsb (Identity (o + m)) + | Cons (e, s, o) -> hcsb (Cons (e, s, o + m)) else s

(* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) = Identity m +let shift (m:db_offset) : 'a subst = hcsb (Identity m)

(* Return a substitution which replaces #0 with `e` and then applies `s` * to the rest. *) -let cons e s = Cons (e, s, 0) +let cons e s : 'a subst = hcsb (Cons (e, s, 0))

(* The trivial substitution which doesn't do anything. *) -let identity = Identity 0 +let identity = hcsb (Identity 0)

(* Test if a substitution is trivial. The "_p" stands for "predicate". *) -let identity_p s = match s with | Identity o -> o = 0 | _ -> false +let identity_p s = match subst_subst' s with | Identity o -> o = 0 | _ -> false

(* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) @@ -177,27 +185,27 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * that some shifts can be pushed more or less down. Here we * want the shifts to float as far outside as possible. *) let rec compose' (s1: 'a subst) (s2: 'a subst) : 'a subst = - match s1 with + match subst_subst' s1 with | Identity o1 - -> let rec compose_id o1 s o = match s with - | Identity o2 -> Identity (o + o1 + o2) + -> let rec compose_id o1 s o = match subst_subst' s with + | Identity o2 -> hcsb (Identity (o + o1 + o2)) | Cons (e2, s2, o2) (* , sk2, s2', o2' *) -> (* Myers's fastlane: * if o1 >= sk2 then compose_id (o1 - sk2) s2' (o + o2') *) if o1 > 0 then compose_id (o1 - 1) s2 (o + o2) - else Cons (e2, s2, o + o2) + else hcsb (Cons (e2, s2, o + o2)) in compose_id o1 s2 0 | Cons (e1, s1, o1) - -> let rec compose_cons o1 s o = match s with - | Identity o2 -> Cons (e1, s1, o + o1 + o2) + -> let rec compose_cons o1 s o = match subst_subst' s with + | Identity o2 -> hcsb (Cons (e1, s1, o + o1 + o2)) | Cons (e2, s2, o2) (* , sk2, s2', o2' *) -> (* Myers's fastlane: * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) - else + else (* Pull out o2's shift and compose the two Cons. *) let s' = cons e2 s2 in - Cons (mkSusp e1 s', compose' s1 s', o + o2) + hcsb (Cons (mkSusp e1 s', compose' s1 s', o + o2)) in compose_cons o1 s2 0 in compose' s1 s2

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

+open Lexp_type open Lexp + (* open Sexp *) (* open Inverse_subst *) module OL = Opslexp @@ -130,43 +132,43 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with * aka * ?a = ?b[0 => 0 · ↑1] *) -let common_subset ctx s1 s2 = - let rec loop s1 s2 o1 o2 o = - match (s1, s2) with - | (S.Cons (le1, s1', o1'), S.Cons (le2, s2', o2')) +let common_subset ctx (s1 : lsubst) (s2 : lsubst) = + let rec loop (s1 : lsubst) (s2 : lsubst) o1 o2 o = + match (S.subst_subst' s1, S.subst_subst' s2) with + | (Cons (le1, s1', o1'), Cons (le2, s2', o2')) -> let o1 = o1 + o1' in 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)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with - | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), - s', o) + | (Identity 1, _) -> S.hcsb (Identity o) (* Optimization! *) + | (sb, _) as s' -> S.hcsb (Cons (mkVar ((lexp_location le1, None), 0), + s', o)) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that * * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) - | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), - S.Identity 1, o2')) + | (Cons _, Identity o2') + -> loop s1 (S.hcsb (Cons (mkVar ((U.dummy_location, None), 0), + S.hcsb (Identity 1), o2'))) o1 o2 o - | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), - S.Identity 1, o1')) + | (Identity o1', Cons _) + -> loop (S.hcsb (Cons (mkVar ((U.dummy_location, None), 0), + S.hcsb (Identity 1), o1'))) s2 o1 o2 o - | (S.Identity o1', S.Identity o2') + | (Identity o1', Identity o2') -> assert (o1 + o1' = o2 + o2'); - S.Identity o + S.hcsb (Identity o) in loop s1 s2 0 0 0

(* Return the number of vars difference between input and output context. * * Could be returned directly by `common_subset`, but it's pretty easy to * compute it here instead. *) -let rec s_offset s = match s with - | S.Identity o -> o - | S.Cons (_, s', o) -> o - 1 + s_offset s' +let rec s_offset (s : lsubst) = match S.subst_subst' s with + | Identity o -> o + | Cons (_, s', o) -> o - 1 + s_offset s'

(************************** Top level unify **********************************)

@@ -311,7 +313,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | Metavar (idx2, s2, name) -> if idx = idx2 then match common_subset ctx s1 s2 with - | S.Identity 0 -> [] (* Optimization! *) + | (Identity 0, _) -> [] (* Optimization! *) (* ¡ s1 != s2 ! * Create a new metavar that can only refer to those vars * which are mapped identically by `s1` and `s2` @@ -319,7 +321,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) * This metavar doesn't necessarily live exactly in `ctx` * nor even a proper prefix of it, tho :-( !! *) - | s -> + | (sb, _) as s -> (* print_string "Metavar idx-idx s1!=s2\n"; *) assert (not (OL.conv_p ctx lxp1 lxp2)); match (Inverse_subst.inverse s,

===================================== src/util.ml ===================================== @@ -116,3 +116,14 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = match opt with | None -> None | Some x -> Some (fn x) + +let combine_hash e1 e2 = (e1 * 31) lxor e2 + +let get_stats stats = + let (tl, ne, sumb, smallb, medianb, bigb) = stats in + Printf.printf "\n\ttable length: %i\n + number of entries: %i\n + sum of bucket lengths: %i\n + smallest bucket length: %i\n + median bucket length: %i\n + biggest bucket length: %i\n" tl ne sumb smallb medianb bigb

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ab6585a3c7ea5cd7ec35c0b9a7b4ec3ae0...