From 31e590b693fa38241e82d822e9676fa803f22df4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 6 Jun 2024 16:48:46 +0200 Subject: [PATCH] Avoid retypechecking repeated subterms in typeops --- kernel/constr.ml | 6 +- kernel/constr.mli | 9 ++ kernel/hConstr.ml | 370 +++++++++++++++++++++++++++++++++++++++++++++ kernel/hConstr.mli | 59 ++++++++ kernel/typeops.ml | 143 ++++++++++-------- 5 files changed, 526 insertions(+), 61 deletions(-) create mode 100644 kernel/hConstr.ml create mode 100644 kernel/hConstr.mli diff --git a/kernel/constr.ml b/kernel/constr.ml index 171849f15affe..8face8549fc37 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1147,8 +1147,8 @@ let invert_eqeq iv1 iv2 = let hasheq_ctx (nas1, c1) (nas2, c2) = array_eqeq nas1 nas2 && c1 == c2 -let hasheq t1 t2 = - match kind t1, kind t2 with +let hasheq_kind t1 t2 = + match t1, t2 with | Rel n1, Rel n2 -> n1 == n2 | Meta m1, Meta m2 -> m1 == m2 | Var id1, Var id2 -> id1 == id2 @@ -1189,6 +1189,8 @@ let hasheq t1 t2 = | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ | CoFix _ | Int _ | Float _ | String _ | Array _), _ -> false +let hasheq t1 t2 = hasheq_kind (kind t1) (kind t2) + (** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *) diff --git a/kernel/constr.mli b/kernel/constr.mli index 7eff1eb44f364..f1d480724039f 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -630,6 +630,9 @@ val case_info_hash : case_info -> int val hcons : constr -> constr +val hasheq_kind : (_ kind_of_term as 'k) -> 'k -> bool +(** Checks physical equality of every immediate element (goes inside tuples and arrays) *) + val debug_print : constr -> Pp.t val debug_print_fix : ('a -> Pp.t) -> ('a, 'a, 'r) pfixpoint -> Pp.t @@ -641,3 +644,9 @@ val mkInd : inductive -> constr val mkConstruct : constructor -> constr [@@deprecated "Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]"] + +val hcons_annot : Name.t binder_annot -> Name.t binder_annot + +val hcons_caseinfo : case_info -> case_info + +val hash_cast_kind : cast_kind -> int diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml new file mode 100644 index 0000000000000..1b77f1a35e75b --- /dev/null +++ b/kernel/hConstr.ml @@ -0,0 +1,370 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* not a rel, otherwise unique identifier of that binder *); + hash : int; + mutable refcount : int; +} + +let equal a b = + a.isRel == b.isRel + && hasheq_kind a.kind b.kind + +let hash x = x.hash + +end + +include Self + +let self x = x.self + +let refcount x = x.refcount + +module Tbl = struct + type key = t + + (* We expose the API of Hashtbl but implemented using Int.Map ref. + For unclear reasons this is dramatically faster on an artificial example + (balanced binary tree whose leaves are all different primitive ints, + such that there is no sharing). + It is a bit slower in the real world. + It seems that hashtbl produces overly large buckets which then need to be linearly scanned. + hconsing doesn't seem to have this problem, + perhaps because of differences between hashtbl and our hashset implementation. *) + type 'a t = (key * 'a) list Int.Map.t ref + + let create _ = ref Int.Map.empty + + let add tbl key v = + tbl := Int.Map.update key.hash (function + | None -> Some [(key,v)] + | Some l -> Some ((key,v)::l)) + !tbl + + let find_opt tbl key = + match Int.Map.find_opt key.hash !tbl with + | None -> None + | Some l -> + List.find_map (fun (k',v) -> + if equal key k' then Some v else None) + l + + type stats = { + hashes : int; + bindings : int; + most_collisions : int; + } + + let empty_stats = { + hashes = 0; + bindings = 0; + most_collisions = 0; + } + + let stats tbl = + Int.Map.fold (fun _ l acc -> + let len = List.length l in + { + hashes = acc.hashes + 1; + bindings = acc.bindings + len; + most_collisions = max acc.most_collisions len; + } + ) + !tbl + empty_stats + +end + +type local_env = { + (* unique identifiers for each binder crossed *) + rels : int Range.t; + (* global counter *) + cnt : int ref; + assum_uids : int Tbl.t; + (* the surrounding table is for the body, the inner table for the type *) + letin_uids : int Tbl.t Tbl.t; +} + +let empty_env () = { + rels = Range.empty; + cnt = ref 0; + assum_uids = Tbl.create 47; + letin_uids = Tbl.create 47; +} + +let push_unknown_rel env = + incr env.cnt; + { env with rels = Range.cons !(env.cnt) env.rels } + +let push_assum t env = + let uid = match Tbl.find_opt env.assum_uids t with + | Some uid -> uid + | None -> + incr env.cnt; + let uid = !(env.cnt) in + Tbl.add env.assum_uids t uid; + uid + in + { env with rels = Range.cons uid env.rels } + +let push_letin ~body ~typ env = + let uid = match Tbl.find_opt env.letin_uids body with + | Some tbl -> begin match Tbl.find_opt tbl typ with + | Some uid -> uid + | None -> + incr env.cnt; + let uid = !(env.cnt) in + Tbl.add tbl typ uid; + uid + end + | None -> + incr env.cnt; + let uid = !(env.cnt) in + let tbl = Tbl.create 3 in + Tbl.add tbl typ uid; + Tbl.add env.letin_uids body tbl; + uid + in + { env with rels = Range.cons uid env.rels } + +let hash_annot = hash_annot Name.hash + +let hash_array hashf a = Array.fold_left (fun hash x -> Hashset.Combine.combine hash (hashf x)) 0 a + +let hash_kind = let open Hashset.Combine in function + | Var i -> combinesmall 1 (Id.hash i) + | Sort s -> combinesmall 2 (Sorts.hash s) + | Cast (c,k,t) -> combinesmall 3 (combine3 c.hash (hash_cast_kind k) t.hash) + | Prod (na,t,c) -> combinesmall 4 (combine3 (hash_annot na) t.hash c.hash) + | Lambda (na,t,c) -> combinesmall 5 (combine3 (hash_annot na) t.hash c.hash) + | LetIn (na,b,t,c) -> combinesmall 6 (combine4 (hash_annot na) b.hash t.hash c.hash) + | App (h,args) -> combinesmall 7 (Array.fold_left (fun hash c -> combine hash c.hash) h.hash args) + | Evar _ -> assert false + | Const (c,u) -> combinesmall 9 (combine (Constant.SyntacticOrd.hash c) (UVars.Instance.hash u)) + | Ind (ind,u) -> combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) (UVars.Instance.hash u)) + | Construct (c,u) -> combinesmall 11 (combine (Construct.SyntacticOrd.hash c) (UVars.Instance.hash u)) + | Case (_,u,pms,(p,_),_,c,bl) -> + let hash_ctx (bnd,c) = + Array.fold_left (fun hash na -> combine (hash_annot na) hash) c.hash bnd + in + let hpms = hash_array hash pms in + let hbl = hash_array hash_ctx bl in + let h = combine5 (UVars.Instance.hash u) + c.hash hpms (hash_ctx p) hbl + in + combinesmall 12 h + | Fix (_,(lna,tl,bl)) -> + combinesmall 13 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl)) + | CoFix (_,(lna,tl,bl)) -> + combinesmall 14 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl)) + | Meta _ -> assert false + | Rel n -> combinesmall 16 n + | Proj (p,_,c) -> combinesmall 17 (combine (Projection.SyntacticOrd.hash p) c.hash) + | Int i -> combinesmall 18 (Uint63.hash i) + | Float f -> combinesmall 19 (Float64.hash f) + | String s -> combinesmall 20 (Pstring.hash s) + | Array (u,t,def,ty) -> combinesmall 21 (combine4 (UVars.Instance.hash u) (hash_array hash t) def.hash ty.hash) + +let kind_to_constr = function + | Rel n -> mkRel n + | Var i -> mkVar i + | Meta _ | Evar _ -> assert false + | Sort s -> mkSort s + | Cast (c,k,t) -> mkCast (c.self,k,t.self) + | Prod (na,t,c) -> mkProd (na,t.self,c.self) + | Lambda (na,t,c) -> mkLambda (na,t.self,c.self) + | LetIn (na,b,t,c) -> mkLetIn (na,b.self,t.self,c.self) + | App (h,args) -> mkApp (h.self, Array.map self args) + | Const cu -> mkConstU cu + | Ind iu -> mkIndU iu + | Construct cu -> mkConstructU cu + | Case (ci,u,pms,(p,r),iv,c,bl) -> + let to_ctx (bnd,c) = bnd, c.self in + let iv = match iv with + | NoInvert -> NoInvert + | CaseInvert x -> CaseInvert {indices=Array.map self x.indices} + in + mkCase (ci,u,Array.map self pms,(to_ctx p,r),iv,c.self,Array.map to_ctx bl) + | Fix (ln,(lna,tl,bl)) -> + mkFix (ln,(lna,Array.map self tl,Array.map self bl)) + | CoFix (ln,(lna,tl,bl)) -> + mkCoFix (ln,(lna,Array.map self tl,Array.map self bl)) + | Proj (p,r,c) -> mkProj (p,r,c.self) + | Int i -> mkInt i + | Float f -> mkFloat f + | String s -> mkString s + | Array (u,t,def,ty) -> mkArray (u,Array.map self t,def.self,ty.self) + +let hcons_inplace f a = Array.iteri (fun i x -> Array.unsafe_set a i (f x)) a + +let of_kind_nohashcons = function + | App (c, [||]) -> c + | kind -> + let self = kind_to_constr kind in + let hash = hash_kind kind in + let () = match kind with + | Rel _ -> assert false + | _ -> () + in + { self; kind; hash; isRel = 0; refcount = 1 } + +let rec of_constr tbl local_env c = + let c = + let kind = of_constr_aux tbl local_env c in + let self = kind_to_constr kind in + let self = if hasheq_kind (Constr.kind self) (Constr.kind c) then c else self in + let hash = hash_kind kind in + let isRel, hash = match kind with + | Rel n -> + let uid = Range.get local_env.rels (n-1) in + assert (uid <> 0); + uid, Hashset.Combine.combine uid hash + | _ -> 0, hash + in + { self; kind; hash; isRel; refcount = 1 } + in + match Tbl.find_opt tbl c with + | Some c' -> c'.refcount <- c'.refcount + 1; c' + | None -> Tbl.add tbl c c; c + +and of_constr_aux tbl local_env c = + match kind c with + | Var i -> + let i = Id.hcons i in + Var i + | Rel _ as t -> t + | Sort s -> + let s = Sorts.hcons s in + Sort s + | Cast (c,k,t) -> + let c = of_constr tbl local_env c in + let t = of_constr tbl local_env t in + Cast (c, k, t) + | Prod (na,t,c) -> + let na = hcons_annot na in + let t = of_constr tbl local_env t in + let c = of_constr tbl (push_assum t local_env) c in + Prod (na, t, c) + | Lambda (na, t, c) -> + let na = hcons_annot na in + let t = of_constr tbl local_env t in + let c = of_constr tbl (push_assum t local_env) c in + Lambda (na,t,c) + | LetIn (na,b,t,c) -> + let na = hcons_annot na in + let b = of_constr tbl local_env b in + let t = of_constr tbl local_env t in + let c = of_constr tbl (push_letin ~body:b ~typ:t local_env) c in + LetIn (na,b,t,c) + | App (h,args) -> + let h = of_constr tbl local_env h in + let args = Array.map (of_constr tbl local_env) args in + App (h, args) + | Evar _ -> CErrors.anomaly Pp.(str "evar in typeops") + | Meta _ -> CErrors.anomaly Pp.(str "meta in typeops") + | Const (c,u) -> + let c = hcons_con c in + let u = UVars.Instance.hcons u in + Const (c,u) + | Ind (ind,u) -> + let ind = hcons_ind ind in + let u = UVars.Instance.hcons u in + Ind (ind,u) + | Construct (c,u) -> + let c = hcons_construct c in + let u = UVars.Instance.hcons u in + Construct (c,u) + | Case (ci,u,pms,(p,r),iv,c,bl) -> + let of_ctx (bnd, c) = + let () = hcons_inplace hcons_annot bnd in + let local_env = Array.fold_left (fun local_env _ -> push_unknown_rel local_env) local_env bnd in + let c = of_constr tbl local_env c in + bnd, c + in + let ci = hcons_caseinfo ci in + let u = UVars.Instance.hcons u in + let pms = Array.map (of_constr tbl local_env) pms in + let p = of_ctx p in + let iv = match iv with + | NoInvert -> NoInvert + | CaseInvert {indices} -> CaseInvert {indices=Array.map (of_constr tbl local_env) indices} + in + let c = of_constr tbl local_env c in + let bl = Array.map of_ctx bl in + Case (ci,u,pms,(p,r),iv,c,bl) + | Fix (ln,(lna,tl,bl)) -> + let () = hcons_inplace hcons_annot lna in + let tl = Array.map (of_constr tbl local_env) tl in + let body_env = Array.fold_left (fun env t -> push_assum t env) local_env tl in + let bl = Array.map (of_constr tbl body_env) bl in + Fix (ln,(lna,tl,bl)) + | CoFix (ln,(lna,tl,bl)) -> + let () = hcons_inplace hcons_annot lna in + let tl = Array.map (of_constr tbl local_env) tl in + let body_env = Array.fold_left (fun env t -> push_assum t env) local_env tl in + let bl = Array.map (of_constr tbl body_env) bl in + CoFix (ln,(lna,tl,bl)) + | Proj (p,r,c) -> + let p = Projection.hcons p in + let c = of_constr tbl local_env c in + Proj (p,r,c) + | Int _ as t -> t + | Float _ as t -> t + | String _ as t -> t + | Array (u,t,def,ty) -> + let u = UVars.Instance.hcons u in + let t = Array.map (of_constr tbl local_env) t in + let def = of_constr tbl local_env def in + let ty = of_constr tbl local_env ty in + Array (u,t,def,ty) + +let dbg = CDebug.create ~name:"hconstr" () + +let of_constr env c = + let local_env = empty_env () in + let local_env = iterate push_unknown_rel (Environ.nb_rel env) local_env in + let tbl = Tbl.create 57 in + let c = of_constr tbl local_env c in + dbg Pp.(fun () -> + let stats = Tbl.stats tbl in + v 0 ( + str "hashes = " ++ int stats.Tbl.hashes ++ spc() ++ + str "bindings = " ++ int stats.Tbl.bindings ++ spc() ++ + str "most_collisions = " ++ int stats.Tbl.most_collisions + ) + ); + c + +let of_constr env c = NewProfile.profile "HConstr.of_constr" (fun () -> of_constr env c) () + +let kind x = x.kind diff --git a/kernel/hConstr.mli b/kernel/hConstr.mli new file mode 100644 index 0000000000000..08c4c12f1ef3d --- /dev/null +++ b/kernel/hConstr.mli @@ -0,0 +1,59 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* x] and [fun x : nat => x] are different + (and have different hashes modulo accidental collision) + and the [x] subterms in [fun (y:nat) (x:bool) => x] and [fun (x:bool) (y:nat) => x] are different + (one is [Rel 1], the other is [Rel 2]) + but the [x] subterms in [fun (y:nat) (x:bool) => x] and [fun (y:bool) (x:bool) => x] are shared. + + This allows using it as a cache key while typechecking. + + Hashconsing information of subterms is also kept. *) + +val self : t -> constr + +val kind : t -> (t,t,Sorts.t,UVars.Instance.t,Sorts.relevance) kind_of_term + +val refcount : t -> int +(** How many times this term appeared as a subterm of the argument to [of_constr]. *) + +val of_constr : Environ.env -> constr -> t + +(* May not be used on Rel! (subterms can be rels) *) +val of_kind_nohashcons : (t,t,Sorts.t,UVars.Instance.t,Sorts.relevance) kind_of_term -> t +(** Build a [t] without hashconsing. Its refcount may be 1 even if + an identical term was already seen. + + May not be used to build [Rel]. + + This is intended for the reconstruction of the inductive type when checking CaseInvert. *) + +module Tbl : sig + (** Imperative tables indexed by [HConstr.t]. + The interfaces exposed are the same as [Hashtbl] + but are not guaranteed to be implemented by [Hashtbl]. *) + + type key = t + + type 'a t + + val find_opt : 'a t -> key -> 'a option + + val add : 'a t -> key -> 'a -> unit + + val create : int -> 'a t +end diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b22216083ef93..f218a48fb66d1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -618,13 +618,25 @@ let check_let_annot env s x c t = then () else error_bad_binder_relevance env r' (RelDecl.LocalDef (x, c, t)) +let push_rec_types (lna,typarray,_) env = + let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in + Array.fold_left (fun e assum -> push_rel assum e) env ctxt + (* The typing machine. *) - (* ATTENTION : faudra faire le typage du contexte des Const, - Ind et Constructsi un jour cela devient des constructions - arbitraires et non plus des variables *) -let rec execute env cstr = +let rec execute tbl env cstr = + if Int.equal (HConstr.refcount cstr) 1 then execute_aux tbl env cstr + else begin match HConstr.Tbl.find_opt tbl cstr with + | Some v -> v + | None -> + let v = execute_aux tbl env cstr in + HConstr.Tbl.add tbl cstr v; + v + end + +and execute_aux tbl env cstr = let open Context.Rel.Declaration in - match kind cstr with + let self = HConstr.self in + match HConstr.kind cstr with (* Atomic terms *) | Sort s -> let () = match s with @@ -643,52 +655,55 @@ let rec execute env cstr = type_of_constant env c | Proj (p, r, c) -> - let ct = execute env c in - let r', ty = type_of_projection env p c ct in + let ct = execute tbl env c in + let r', ty = type_of_projection env p (self c) ct in assert (Sorts.relevance_equal r r'); ty (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array env args in + let argst = execute_array tbl env args in + let args = snd @@ destApp (self cstr) in let ft = - match kind f with + match HConstr.kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> type_of_inductive_knowing_parameters env ind args argst | _ -> (* No template polymorphism *) - execute env f + execute tbl env f in - type_of_apply env f ft args argst + type_of_apply env (self f) ft args argst | Lambda (name,c1,c2) -> - let s = execute_is_type env c1 in - let () = check_assum_annot env s name c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - type_of_abstraction env name c1 c2t + let s = execute_is_type tbl env c1 in + let () = check_assum_annot env s name (self c1) in + let env1 = push_rel (LocalAssum (name,self c1)) env in + let c2t = execute tbl env1 c2 in + type_of_abstraction env name (self c1) c2t | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let () = check_assum_annot env vars name c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in + let vars = execute_is_type tbl env c1 in + let () = check_assum_annot env vars name (self c1) in + let env1 = push_rel (LocalAssum (name,self c1)) env in + let vars' = execute_is_type tbl env1 c2 in type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let c2s = execute_is_type env c2 in + let c1t = execute tbl env c1 in + let c2s = execute_is_type tbl env c2 in + let c1 = self c1 in + let c2 = self c2 in let () = check_let_annot env c2s name c1 c2 in let () = check_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in + let c3t = execute tbl env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute env c in - let _ts : Sorts.t = execute_is_type env t in - let () = check_cast env c ct k t in - t + let ct = execute tbl env c in + let _ts : Sorts.t = execute_is_type tbl env t in + let () = check_cast env (self c) ct k (self t) in + self t (* Inductive types *) | Ind ind -> @@ -697,15 +712,18 @@ let rec execute env cstr = | Construct c -> type_of_constructor env c - | Case (ci, u, pms, (p,rp), iv, c, lf) -> - let ct = execute env c in + | Case (ci, u, pms, (p,_), iv, c, lf) -> + let ct = execute tbl env c in let () = match iv with | NoInvert -> () | CaseInvert {indices} -> let args = Array.append pms indices in - let ct' = mkApp (mkIndU (ci.ci_ind,u), args) in - let _ : Sorts.t = execute_is_type env ct' in - match conv_leq env ct ct' with + let ct' = + let mk = HConstr.of_kind_nohashcons in + mk @@ App (mk @@ Ind (ci.ci_ind,u), args) + in + let _ : Sorts.t = execute_is_type tbl env ct' in + match conv_leq env ct (self ct') with | Result.Ok () -> () | Result.Error () -> error_bad_invert env (* TODO: more informative message *) @@ -713,10 +731,11 @@ let rec execute env cstr = let mib, mip = Inductive.lookup_mind_specif env ci.ci_ind in let cst = Inductive.instantiate_inductive_constraints mib u in let () = check_constraints cst env in - let pmst = execute_array env pms in + let pmst = execute_array tbl env pms in + let pms = Array.map self pms in let paramsubst = try type_of_parameters env mib.mind_params_ctxt u pms pmst - with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) c None + with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) (self c) None in let (pctx, pt) = let (nas, p) = p in @@ -729,16 +748,16 @@ let rec execute env cstr = let realdecls = LocalAssum (Context.make_annot Anonymous mip.mind_relevance, self) :: realdecls in let realdecls = try instantiate_context u paramsubst nas realdecls - with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) c None + with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) (HConstr.self c) None in let p_env = Environ.push_rel_context realdecls env in - let pt = execute p_env p in + let pt = execute tbl p_env p in (realdecls, pt) in let () = let nbranches = Array.length mip.mind_nf_lc in if not (Int.equal (Array.length lf) nbranches) then - error_number_branches env (make_judge c ct) nbranches + error_number_branches env (make_judge (self c) ct) nbranches in let build_one_branch i (nas, br) = let (ctx, cty) = mip.mind_nf_lc.(i) in @@ -747,24 +766,26 @@ let rec execute env cstr = try instantiate_context u paramsubst nas ctx with ArgumentsMismatch -> (* Despite the name, the toplevel message is reasonable *) - error_elim_arity env (ci.ci_ind, u) c None + error_elim_arity env (ci.ci_ind, u) (self c) None in let br_env = Environ.push_rel_context ctx env in - let brt = execute br_env br in + let brt = execute tbl br_env br in let cty = esubst u (Esubst.subs_liftn mip.mind_consnrealdecls.(i) paramsubst) cty in (ctx, brt, cty) in let lft = Array.mapi build_one_branch lf in + (* easier than mapping self over various shapes of arrays *) + let (ci, u, pms, (p,rp), iv, c, lf) = destCase (self cstr) in type_of_case env (mib, mip) ci u pms (pctx, fst p, snd p, rp, pt) iv c ct lf lft - | Fix ((_,i),recdef as fix) -> - let fix_ty = execute_recdef env recdef i in - check_fix env fix; + | Fix ((_,i),recdef) -> + let fix_ty = execute_recdef tbl env recdef i in + check_fix env (destFix @@ self cstr); fix_ty - | CoFix (i,recdef as cofix) -> - let fix_ty = execute_recdef env recdef i in - check_cofix env cofix; + | CoFix (i,recdef) -> + let fix_ty = execute_recdef tbl env recdef i in + check_cofix env (destCoFix @@ self cstr); fix_ty (* Primitive types *) @@ -777,14 +798,15 @@ let rec execute env cstr = | [||], [|u|] -> u | _ -> assert false in - let tyty = execute env ty in + let tyty = execute tbl env ty in + let ty = self ty in check_cast env ty tyty DEFAULTcast (mkType (Universe.make ulev)); - let def_ty = execute env def in - check_cast env def def_ty DEFAULTcast ty; + let def_ty = execute tbl env def in + check_cast env (self def) def_ty DEFAULTcast ty; let ta = type_of_array env u in let () = Array.iter (fun x -> - let xt = execute env x in - check_cast env x xt DEFAULTcast ty) + let xt = execute tbl env x in + check_cast env (self x) xt DEFAULTcast ty) t in mkApp(ta, [|ty|]) @@ -796,23 +818,26 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables.") -and execute_is_type env constr = - let t = execute env constr in - check_type env constr t +and execute_is_type tbl env constr = + let t = execute tbl env constr in + check_type env (HConstr.self constr) t -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in +and execute_recdef tbl env (names,lar,vdef) i = + let lart = execute_array tbl env lar in + let lar = Array.map HConstr.self lar in let () = Array.iteri (fun i na -> check_assumption env na lar.(i) lart.(i)) names in let env1 = push_rec_types (names,lar,vdef) env in (* vdef is ignored *) - let vdeft = execute_array env1 vdef in + let vdeft = execute_array tbl env1 vdef in + let vdef = Array.map HConstr.self vdef in let () = check_fixpoint env1 names lar vdef vdeft in lar.(i) -and execute_array env cs = - Array.map (fun c -> execute env c) cs +and execute_array tbl env cs = + Array.map (fun c -> execute tbl env c) cs let execute env c = - NewProfile.profile "Typeops.infer" (fun () -> execute env c) () + let c = HConstr.of_constr env c in + NewProfile.profile "Typeops.execute" (fun () -> execute (HConstr.Tbl.create 57) env c) () (* Derived functions *)