Alice de Berny pushed to branch alice at Stefan / Typer

Commits: 50177654 by irradiee at 2020-06-24T10:40:07-04:00 add dependency between subst and lexp & hash sharing counter

- - - - -

8 changed files:

- src/REPL.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/lexp_type.ml - src/subst.ml - src/unification.ml - src/util.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -232,8 +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) - | "%lcollisions" | "%cl" -> (get_stats (WHC.stats hc_table)) - | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table)) + | "%lcollisions" | "%cl" -> (get_stats (WHC.stats hc_table) !lshrct !sshrct) + | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table) !lshrct !sshrct)

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

===================================== src/elab.ml ===================================== @@ -395,7 +395,7 @@ let rec meta_to_var ids (e : lexp) = *)

(* `o` is the binding offset until the root. *) - let rec adjust_subst o (s : lsubst) = match S.subst_subst' s with + let rec adjust_subst o (s : subst) = match S.subst_subst' s with | Identity n -> let o' = o - n in if o' < 0 then

===================================== src/inverse_subst.ml ===================================== @@ -57,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: lsubst) : substIR option = - let rec transfo (s: lsubst) (off_acc: int) (idx: int) (imp_cnt : int) +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 *) let v' = lexp_lexp' v in @@ -106,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): lsubst option = - let rec genDummyVar (beg_: int) (end_: int) (l: lsubst): lsubst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: subst): subst = (* 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: lsubst) (nbVar: int): lsubst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: subst) (nbVar: int): subst 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): lsubst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None

@@ -144,8 +144,8 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): lsubst option = | None -> None | Some s -> fill_before l s nbVar

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

<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: lsubst) : lsubst option = +let inverse (s: subst) : subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -182,7 +182,7 @@ let inverse (s: lsubst) : lsubst 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: lsubst) : bool = match S.subst_subst' s with +let rec invertible (s: subst) : bool = match S.subst_subst' s with | Identity _ -> true | Cons (e, s, _) -> (let e' = lexp_lexp' e in @@ -193,7 +193,7 @@ exception Not_invertible exception Ambiguous

(* Lookup variable i in s⁻¹ *) -let rec lookup_inv_subst (i : db_index) (s : lsubst) : db_index +let rec lookup_inv_subst (i : db_index) (s : subst) : db_index = match S.subst_subst' s with | (Identity o | Cons (_, _, o)) when i < o -> raise Not_invertible | Identity o -> i - o @@ -240,7 +240,7 @@ 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' : lsubst) (s : lsubst) = match S.subst_subst' s' with +let rec compose_inv_subst (s' : subst) (s : subst) = 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? *) @@ -254,7 +254,7 @@ let rec compose_inv_subst (s' : lsubst) (s : lsubst) = match S.subst_subst' s' w * 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 : lsubst) : lexp = +and apply_inv_subst (e : lexp) (s : subst) : lexp = let e' = lexp_lexp' e in match e' with | Imm _ -> e

===================================== src/lexp.ml ===================================== @@ -42,10 +42,28 @@ open Grammar

let lexp_lexp' (e, h) = e

- let rec apply_lxor (map : int list) : int = - match map with - | [] -> 31 - | e :: l -> (e * 31) lxor (apply_lxor l) +let rec apply_lxor (map : int list) : int = + match map with + | [] -> 31 + | e :: l -> (e * 31) lxor (apply_lxor l) + +let attributemap_combine_hash (k: (int * string)) (v: lexp) (p: int) : int = +shrct_inc lshrct 1; + (p * 31) lxor (((Hashtbl.hash k) * 31) lxor (lexp_hash v)) + +let ind_stringmap_combine_hash (k: string) (v: ((arg_kind * vname * ltype) list)) (p: int) : int = + (p * 31) lxor ((Hashtbl.hash k) * 31) lxor + (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in + shrct_inc lshrct 1; + (U.combine_hash (Hashtbl.hash ak) + (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) v)) + +let case_stringmap_combine_hash (k: string) (v: (U.location * (arg_kind * vname) list * lexp)) (p: int) : int = + shrct_inc lshrct 1; + let (loc, li, lp) = v in + (p * 31) lxor ((Hashtbl.hash k) * 31) lxor + (Hashtbl.hash loc) lxor (Hashtbl.hash li) lxor (lexp_hash lp) +

(* Hashtbl.hash for not lexp types * TODO: - find something else @@ -56,51 +74,67 @@ open Grammar | SortLevel l -> U.combine_hash 2 (match l with | SLz -> Hashtbl.hash l - | SLsucc lp -> lexp_hash lp - | SLlub (lp1, lp2) -> U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) + | SLsucc lp -> shrct_inc lshrct 1; lexp_hash lp + | SLlub (lp1, lp2) + -> shrct_inc lshrct 2; U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) | Sort (l, s) -> U.combine_hash 3 (U.combine_hash (Hashtbl.hash l) (match s with - | Stype lp -> lexp_hash lp + | Stype lp -> shrct_inc lshrct 1; lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) as e -> U.combine_hash 4 (Hashtbl.hash e) + | Builtin (v, t, m) + -> shrct_inc lshrct 1; U.combine_hash 4 (U.combine_hash + (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) + (match m with + | Some m -> (AttributeMap.fold attributemap_combine_hash + m 31) + | None -> 404)) | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) - -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) + -> shrct_inc lshrct 1; + 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 + shrct_inc lshrct 2; (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) - -> 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)))) + -> shrct_inc lshrct 2; + 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) - -> 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))) + -> shrct_inc lshrct 2; + 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) -> 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) + shrct_inc lshrct 1; + (U.combine_hash (Hashtbl.hash ak) (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) - (Hashtbl.hash cs))) - | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) + (SMap.fold ind_stringmap_combine_hash + cs 21))) + | Cons (t, n) -> shrct_inc lshrct 1; U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) - -> 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) + -> shrct_inc lshrct 2; + 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 + (SMap.fold case_stringmap_combine_hash bs 21) (match d with - | Some (n, lp) -> U.combine_hash (Hashtbl.hash n) (lexp_hash lp) + | Some (n, lp) -> shrct_inc lshrct 1; U.combine_hash (Hashtbl.hash n) (lexp_hash lp) | _ -> 0)))) | Metavar (id, s, v) - -> 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 - (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 - let (y', h2) = y in - compare h1 h2 = 0 + -> shrct_inc sshrct 1; + U.combine_hash 12 (U.combine_hash id + (U.combine_hash (S.subst_hash s) (Hashtbl.hash v))) + | Call (e, args) + -> shrct_inc lshrct 1; U.combine_hash 13 (U.combine_hash (lexp_hash e) + (apply_lxor (List.map (fun e -> let (ak, lp) = e in + shrct_inc lshrct 1; + (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) + | Susp (lp, subst) + -> shrct_inc lshrct 1; shrct_inc sshrct 1; + U.combine_hash 14 (U.combine_hash (lexp_hash lp) (S.subst_hash subst))

let hc_eq e1 e2 = e1 == e2 || @@ -241,7 +275,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. *)

-let hcs_table : ((lexp * lexp subst), lexp) Hashtbl.t = Hashtbl.create 1000 +let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000

(* When computing the type of "load"ed modules * we end up building substitutions of the form

===================================== src/lexp_type.ml ===================================== @@ -1,3 +1,25 @@ +(* lexp_type.ml --- Lambda-expressions: the core language. + +Copyright (C) 2011-2020 Free Software Foundation, Inc. + +Author: Stefan Monnier monnier@iro.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/. *) + module U = Util module L = List module SMap = U.SMap @@ -16,38 +38,6 @@ 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: @@ -64,7 +54,6 @@ type 'a subst = 'a subst' * int * 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, ... *) @@ -72,7 +61,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype * lexp AttributeMap.t option | Var of vref - | Susp of lexp * lsubst (* Lazy explicit substitution: e[σ]. *) + | 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 @@ -88,7 +77,7 @@ type ltype = lexp * (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 + | Metavar of meta_id * subst * vname (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -123,12 +112,43 @@ type ltype = lexp | SLsucc of lexp | SLlub of lexp * lexp

+ (* 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. + *) + + and db_index = int (* DeBruijn index. *) + and db_offset = int (* DeBruijn index offset. *) + + (* Substitution, i.e. a mapping from db_index to lexp *) + and subst = subst' * int + and subst' = + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of lexp * subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * lexp 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) *) + + 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. @@ -172,3 +192,10 @@ 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!" + +(* counter for lexp sharing *) +let lshrct = ref 0 + +(* counter for subst sharing *) +let sshrct = ref 0 +let shrct_inc e acc = e := !e + acc

===================================== src/subst.ml ===================================== @@ -122,30 +122,31 @@ open Lexp_type -> lp1 == lp2 && lps1 == lps2 && off1 = off2 | _ -> false

- let subst'_hash (sb : 'a subst') : int = + let subst'_hash (sb : 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 + -> shrct_inc lshrct 1; shrct_inc sshrct 1; + 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 + module WHCSB = Weak.Make (struct type t = subst let equal x y = hcsb_eq x y let hash = subst_hash end)

let hcsb_table : WHCSB.t = WHCSB.create 1000

- let hcsb (s : lexp subst') : lexp subst = + let hcsb (s : subst') : 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 = + (s: subst) (l : 'b) (v:db_index) : 'a = + let rec lookup' (o:db_offset) (s: subst) (v:db_index) : 'a = match subst_subst' s with | Identity o' -> mkVar l (v + o + o') (* Use Myers's fastlane when applicable: @@ -165,11 +166,11 @@ let mkShift s (m:db_offset) = (* 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) : 'a subst = hcsb (Identity m) +let shift (m:db_offset) : subst = hcsb (Identity m)

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

(* The trivial substitution which doesn't do anything. *) let identity = hcsb (Identity 0) @@ -179,12 +180,12 @@ 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₂) *) -let compose (mkSusp : 'a -> 'a subst -> 'a) - (s1: 'a subst) (s2: 'a subst) : 'a subst = +let compose (mkSusp : 'a -> subst -> 'a) + (s1: subst) (s2: subst) : subst = (* There is a bit of flexibility in what we return, in the sense * 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 = + let rec compose' (s1: subst) (s2: subst) : subst = match subst_subst' s1 with | Identity o1 -> let rec compose_id o1 s o = match subst_subst' s with @@ -213,7 +214,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * I.e. take a substitution from Δs to Δₜ and return a substitution * from Δs,x to Δₜ,x. * Also known as `lift`. *) -let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = +let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:subst) = cons (mkVar l 0) (mkShift s 1)

(* Return a substitution which replaces #0 with `e`. *)

===================================== src/unification.ml ===================================== @@ -132,8 +132,8 @@ 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 : lsubst) (s2 : lsubst) = - let rec loop (s1 : lsubst) (s2 : lsubst) o1 o2 o = +let common_subset ctx (s1 : subst) (s2 : subst) = + let rec loop (s1 : subst) (s2 : subst) 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 @@ -166,7 +166,7 @@ let common_subset ctx (s1 : lsubst) (s2 : lsubst) = (* 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 : lsubst) = match S.subst_subst' s with +let rec s_offset (s : subst) = match S.subst_subst' s with | Identity o -> o | Cons (_, s', o) -> o - 1 + s_offset s'

===================================== src/util.ml ===================================== @@ -117,13 +117,15 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = | None -> None | Some x -> Some (fn x)

-let combine_hash e1 e2 = (e1 * 31) lxor e2 +let combine_hash (e1: int) (e2: int) : int = (e1 * 31) lxor e2

-let get_stats stats = +let get_stats stats lshrct sshrct = 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 + biggest bucket length: %i\n + lexp sharing counter: %i\n + subst sharing counter: %i\n" tl ne sumb smallb medianb bigb lshrct sshrct;

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