From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- kernel/term.ml | 727 ++++++++++++++++++++++++++++++++------------------------- 1 file changed, 411 insertions(+), 316 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 1894417c..dcb63cf7 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,14 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* SortType s - | Cast (c,_,t) -> CastType (c, t) - | Prod (na,t,c) -> ProdType (na, t, c) - | LetIn (na,b,t,c) -> LetInType (na, b, t, c) - | App (c,l) -> AtomicType (c, l) - | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Case _ | Fix _ | CoFix _ | Ind _ as c) - -> AtomicType (c,[||]) - | (Lambda _ | Construct _) -> failwith "Not a type" - (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type constr = (constr,constr) kind_of_term @@ -117,82 +112,10 @@ type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration -(***************************) -(* hash-consing functions *) -(***************************) -let comp_term t1 t2 = - match t1, t2 with - | Rel n1, Rel n2 -> n1 = n2 - | Meta m1, Meta m2 -> m1 == m2 - | Var id1, Var id2 -> id1 == id2 - | Sort s1, Sort s2 -> s1 == s2 - | Cast (c1,_,t1), Cast (c2,_,t2) -> c1 == c2 & t1 == t2 - | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 - | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 - | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> - n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2 - | App (c1,l1), App (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 (==) l1 l2 - | Const c1, Const c2 -> c1 == c2 - | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 & i1 = i2 - | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) -> - sp1 == sp2 & i1 = i2 & j1 = j2 - | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> - ci1 == ci2 & p1 == p2 & c1 == c2 & array_for_all2 (==) bl1 bl2 - | Fix (ln1,(lna1,tl1,bl1)), Fix (ln2,(lna2,tl2,bl2)) -> - ln1 = ln2 - & array_for_all2 (==) lna1 lna2 - & array_for_all2 (==) tl1 tl2 - & array_for_all2 (==) bl1 bl2 - | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) -> - ln1 = ln2 - & array_for_all2 (==) lna1 lna2 - & array_for_all2 (==) tl1 tl2 - & array_for_all2 (==) bl1 bl2 - | _ -> false - -let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t = - match t with - | Rel _ -> t - | Meta x -> Meta x - | Var x -> Var (sh_id x) - | Sort s -> Sort (sh_sort s) - | Cast (c, k, t) -> Cast (sh_rec c, k, (sh_rec t)) - | Prod (na,t,c) -> Prod (sh_na na, sh_rec t, sh_rec c) - | Lambda (na,t,c) -> Lambda (sh_na na, sh_rec t, sh_rec c) - | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c) - | App (c,l) -> App (sh_rec c, Array.map sh_rec l) - | Evar (e,l) -> Evar (e, Array.map sh_rec l) - | Const c -> Const (sh_con c) - | Ind (kn,i) -> Ind (sh_kn kn,i) - | Construct ((kn,i),j) -> Construct ((sh_kn kn,i),j) - | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *) - Case (ci, sh_rec p, sh_rec c, Array.map sh_rec bl) - | Fix (ln,(lna,tl,bl)) -> - Fix (ln,(Array.map sh_na lna, - Array.map sh_rec tl, - Array.map sh_rec bl)) - | CoFix(ln,(lna,tl,bl)) -> - CoFix (ln,(Array.map sh_na lna, - Array.map sh_rec tl, - Array.map sh_rec bl)) - -module Hconstr = - Hashcons.Make( - struct - type t = constr - type u = (constr -> constr) * - ((sorts -> sorts) * (constant -> constant) * - (mutual_inductive -> mutual_inductive) * (name -> name) * - (identifier -> identifier)) - let hash_sub = hash_term - let equal = comp_term - let hash = Hashtbl.hash - end) - -let hcons_term (hsorts,hcon,hkn,hname,hident) = - Hashcons.recursive_hcons Hconstr.f (hsorts,hcon,hkn,hname,hident) +(*********************) +(* Term constructors *) +(*********************) (* Constructs a DeBrujin index with number n *) let rels = @@ -201,21 +124,20 @@ let rels = let mkRel n = if 0 mkProp (* Easy sharing *) + | Prop Pos -> mkSet + | s -> Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) -(* (that means t2 is declared as the type of t1) - [s] is the strategy to use when *) +(* (that means t2 is declared as the type of t1) *) let mkCast (t1,k2,t2) = match t1 with - | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2) + | Cast (c,k1, _) when k1 = VMcast & k1 = k2 -> Cast (c,k1,t2) | _ -> Cast (t1,k2,t2) (* Constructs the product (x:t1)t2 *) @@ -236,16 +158,13 @@ let mkApp (f, a) = | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) - (* Constructs a constant *) -(* The array of terms correspond to the variables introduced in the section *) let mkConst c = Const c (* Constructs an existential variable *) let mkEvar e = Evar e (* Constructs the ith (co)inductive type of the block named kn *) -(* The array of terms correspond to the variables introduced in the section *) let mkInd m = Ind m (* Constructs the jth constructor of the ith (co)inductive type of the @@ -256,12 +175,48 @@ let mkConstruct c = Construct c (* Constructs the term

Case c of c1 | c2 .. | cn end *) let mkCase (ci, p, c, ac) = Case (ci, p, c, ac) +(* If recindxs = [|i1,...in|] + funnames = [|f1,...fn|] + typarray = [|t1,...tn|] + bodies = [|b1,...bn|] + then + + mkFix ((recindxs,i),(funnames,typarray,bodies)) + + constructs the ith function of the block + + Fixpoint f1 [ctx1] : t1 := b1 + with f2 [ctx2] : t2 := b2 + ... + with fn [ctxn] : tn := bn. + + where the lenght of the jth context is ij. +*) + let mkFix fix = Fix fix -let mkCoFix cofix = CoFix cofix +(* If funnames = [|f1,...fn|] + typarray = [|t1,...tn|] + bodies = [|b1,...bn|] + then + + mkCoFix (i,(funnames,typsarray,bodies)) + + constructs the ith function of the block + + CoFixpoint f1 : t1 := b1 + with f2 : t2 := b2 + ... + with fn : tn := bn. +*) +let mkCoFix cofix= CoFix cofix + +(* Constructs an existential variable named "?n" *) +let mkMeta n = Meta n + +(* Constructs a Variable named id *) +let mkVar id = Var id -let kind_of_term c = c -let kind_of_term2 c = c (************************************************************************) (* kind_of_term = constructions as seen by the user *) @@ -271,15 +226,25 @@ let kind_of_term2 c = c least one argument and the function is not itself an applicative term *) -let kind_of_term = kind_of_term +let kind_of_term c = c +(* Experimental, used in Presburger contrib *) +type ('constr, 'types) kind_of_type = + | SortType of sorts + | CastType of 'types * 'types + | ProdType of name * 'types * 'types + | LetInType of name * 'constr * 'types * 'types + | AtomicType of 'constr * 'constr array -(* En vue d'un kind_of_type : constr -> hnftype ??? *) -type hnftype = - | HnfSort of sorts - | HnfProd of name * constr * constr - | HnfAtom of constr - | HnfInd of inductive * constr array +let kind_of_type = function + | Sort s -> SortType s + | Cast (c,_,t) -> CastType (c, t) + | Prod (na,t,c) -> ProdType (na, t, c) + | LetIn (na,b,t,c) -> LetInType (na, b, t, c) + | App (c,l) -> AtomicType (c, l) + | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Case _ | Fix _ | CoFix _ | Ind _ as c) + -> AtomicType (c,[||]) + | (Lambda _ | Construct _) -> failwith "Not a type" (**********************************************************************) (* Non primitive term destructors *) @@ -334,18 +299,12 @@ let rec is_Type c = match kind_of_term c with | Cast (c,_,_) -> is_Type c | _ -> false -let isType = function - | Type _ -> true - | _ -> false - let is_small = function | Prop _ -> true | _ -> false let iskind c = isprop c or is_Type c -let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2) - (* Tests if an evar *) let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false @@ -366,6 +325,7 @@ let isRel c = match kind_of_term c with Rel _ -> true | _ -> false (* Tests if a variable *) let isVar c = match kind_of_term c with Var _ -> true | _ -> false +let isVarId id c = match kind_of_term c with Var id' -> id = id' | _ -> false (* Tests if an inductive *) let isInd c = match kind_of_term c with Ind _ -> true | _ -> false @@ -387,7 +347,7 @@ let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false (* Destructs the let [x:=b:t1]t2 *) let destLetIn c = match kind_of_term c with | LetIn (x,b,t1,t2) -> (x,b,t1,t2) - | _ -> invalid_arg "destProd" + | _ -> invalid_arg "destLetIn" let isLetIn c = match kind_of_term c with LetIn _ -> true | _ -> false @@ -412,10 +372,6 @@ let destEvar c = match kind_of_term c with | Evar (kn, a as r) -> r | _ -> invalid_arg "destEvar" -let num_of_evar c = match kind_of_term c with - | Evar (n, _) -> n - | _ -> anomaly "num_of_evar called with bad args" - (* Destructs a (co)inductive type named kn *) let destInd c = match kind_of_term c with | Ind (kn, a as r) -> r @@ -485,18 +441,6 @@ let decompose_app c = | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[]) -(* strips head casts and flattens head applications *) -let rec strip_head_cast c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = match kind_of_term f with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) - in - collapse_rec f cl - | Cast (c,_,_) -> strip_head_cast c - | _ -> c - (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) @@ -621,15 +565,11 @@ let compare_constr f t1 t2 = | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 + | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 + | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2)) | App (c1,l1), App (c2,l2) -> - if Array.length l1 = Array.length l2 then - f c1 c2 & array_for_all2 f l1 l2 - else - let (h1,l1) = decompose_app t1 in - let (h2,l2) = decompose_app t2 in - if List.length l1 = List.length l2 then - f h1 h2 & List.for_all2 f l1 l2 - else false + Array.length l1 = Array.length l2 && + f c1 c2 && array_for_all2 f l1 l2 | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 | Const c1, Const c2 -> eq_constant c1 c2 | Ind c1, Ind c2 -> eq_ind c1 c2 @@ -642,6 +582,62 @@ let compare_constr f t1 t2 = ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 | _ -> false +(*******************************) +(* alpha conversion functions *) +(*******************************) + +(* alpha conversion : ignore print names and casts *) + +let rec eq_constr m n = + (m==n) or + compare_constr eq_constr m n + +let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) + +let constr_ord_int f t1 t2 = + let (=?) f g i1 i2 j1 j2= + let c=f i1 i2 in + if c=0 then g j1 j2 else c in + let (==?) fg h i1 i2 j1 j2 k1 k2= + let c=fg i1 i2 j1 j2 in + if c=0 then h k1 k2 else c in + match kind_of_term t1, kind_of_term t2 with + | Rel n1, Rel n2 -> n1 - n2 + | Meta m1, Meta m2 -> m1 - m2 + | Var id1, Var id2 -> id_ord id1 id2 + | Sort s1, Sort s2 -> Pervasives.compare s1 s2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + (f =? f) t1 t2 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> + ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 + | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 + | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2)) + | App (c1,l1), App (c2,l2) -> (f =? (array_compare f)) c1 c2 l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> + ((-) =? (array_compare f)) e1 e2 l1 l2 + | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2) + | Ind (spx, ix), Ind (spy, iy) -> + let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c + | Construct ((spx, ix), jx), Construct ((spy, iy), jy) -> + let c = jx - jy in if c = 0 then + (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) + else c + | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> + ((f =? f) ==? (array_compare f)) p1 p2 c1 c2 bl1 bl2 + | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (array_compare f)) ==? (array_compare f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (array_compare f)) ==? (array_compare f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | t1, t2 -> Pervasives.compare t1 t2 + +let rec constr_ord m n= + constr_ord_int constr_ord m n + (***************************************************************************) (* Type of assumptions *) (***************************************************************************) @@ -659,6 +655,18 @@ let map_rel_declaration = map_named_declaration let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) let fold_rel_declaration = fold_named_declaration +let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty +let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty + +let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty +let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty + +let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = + id_ord i1 i2 = 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 + +let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = + n1 = n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 + (***************************************************************************) (* Type of local contexts (telescopes) *) (***************************************************************************) @@ -762,12 +770,12 @@ let rec exliftn el c = match kind_of_term c with (* Lifting the binding depth across k bindings *) -let liftn k n = - match el_liftn (pred n) (el_shft k ELID) with +let liftn n k = + match el_liftn (pred k) (el_shft n el_id) with | ELID -> (fun c -> c) | el -> exliftn el -let lift k = liftn k 1 +let lift n = liftn n 1 (*********************) (* Substituting *) @@ -814,12 +822,12 @@ let substnl laml n = let substl laml = substnl laml 0 let subst1 lam = substl [lam] -let substnl_decl laml k (id,bodyopt,typ) = - (id,Option.map (substnl laml k) bodyopt,substnl laml k typ) +let substnl_decl laml k = map_rel_declaration (substnl laml k) let substl_decl laml = substnl_decl laml 0 let subst1_decl lam = substl_decl [lam] -let subst1_named_decl = subst1_decl +let substnl_named laml k = map_named_declaration (substnl laml k) let substl_named_decl = substl_decl +let subst1_named_decl = subst1_decl (* (thin_val sigma) removes identity substitutions from sigma *) @@ -858,44 +866,12 @@ let substn_vars p vars = let subst_vars = substn_vars 1 -(*********************) -(* Term constructors *) -(*********************) - -(* Constructs a DeBrujin index with number n *) -let mkRel = mkRel - -(* Constructs an existential variable named "?n" *) -let mkMeta = mkMeta - -(* Constructs a Variable named id *) -let mkVar = mkVar - -(* Construct a type *) -let mkProp = mkSort prop_sort -let mkSet = mkSort set_sort -let mkType u = mkSort (Type u) -let mkSort = function - | Prop Null -> mkProp (* Easy sharing *) - | Prop Pos -> mkSet - | s -> mkSort s - -(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) -(* (that means t2 is declared as the type of t1) *) -let mkCast = mkCast +(***************************) +(* Other term constructors *) +(***************************) -(* Constructs the product (x:t1)t2 *) -let mkProd = mkProd let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c) -let mkProd_string s t c = mkProd (Name (id_of_string s), t, c) - -(* Constructs the abstraction [x:t1]t2 *) -let mkLambda = mkLambda let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c) -let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) - -(* Constructs [x=c_1:t]c_2 *) -let mkLetIn = mkLetIn let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2) (* Constructs either [(x:t)c] or [[x=b:t]c] *) @@ -909,17 +885,6 @@ let mkNamedProd_or_LetIn (id,body,t) c = | None -> mkNamedProd id t c | Some b -> mkNamedLetIn id b t c -(* Constructs either [[x:t]c] or [[x=b:t]c] *) -let mkLambda_or_LetIn (na,body,t) c = - match body with - | None -> mkLambda (na, t, c) - | Some b -> mkLetIn (na, b, t, c) - -let mkNamedLambda_or_LetIn (id,body,t) c = - match body with - | None -> mkNamedLambda id t c - | Some b -> mkNamedLetIn id b t c - (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) let mkProd_wo_LetIn (na,body,t) c = match body with @@ -934,83 +899,16 @@ let mkNamedProd_wo_LetIn (id,body,t) c = (* non-dependent product t1 -> t2 *) let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) -(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) -(* We ensure applicative terms have at most one arguments and the - function is not itself an applicative term *) -let mkApp = mkApp - -let mkAppA v = - let l = Array.length v in - if l=0 then anomaly "mkAppA received an empty array" - else mkApp (v.(0), Array.sub v 1 (Array.length v -1)) - -(* Constructs a constant *) -(* The array of terms correspond to the variables introduced in the section *) -let mkConst = mkConst - -(* Constructs an existential variable *) -let mkEvar = mkEvar - -(* Constructs the ith (co)inductive type of the block named kn *) -(* The array of terms correspond to the variables introduced in the section *) -let mkInd = mkInd - -(* Constructs the jth constructor of the ith (co)inductive type of the - block named kn. The array of terms correspond to the variables - introduced in the section *) -let mkConstruct = mkConstruct - -(* Constructs the term

Case c of c1 | c2 .. | cn end *) -let mkCase = mkCase -let mkCaseL (ci, p, c, ac) = mkCase (ci, p, c, Array.of_list ac) - -(* If recindxs = [|i1,...in|] - funnames = [|f1,...fn|] - typarray = [|t1,...tn|] - bodies = [|b1,...bn|] - then - - mkFix ((recindxs,i),(funnames,typarray,bodies)) - - constructs the ith function of the block - - Fixpoint f1 [ctx1] : t1 := b1 - with f2 [ctx2] : t2 := b2 - ... - with fn [ctxn] : tn := bn. - - where the lenght of the jth context is ij. -*) - -let mkFix = mkFix - -(* If funnames = [|f1,...fn|] - typarray = [|t1,...tn|] - bodies = [|b1,...bn|] - then - - mkCoFix (i,(funnames,typsarray,bodies)) - - constructs the ith function of the block - - CoFixpoint f1 : t1 := b1 - with f2 : t2 := b2 - ... - with fn : tn := bn. -*) -let mkCoFix = mkCoFix - -(* Construct an implicit *) -let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0)) -let mkImplicit = mkSort implicit_sort - -(***************************) -(* Other term constructors *) -(***************************) +(* Constructs either [[x:t]c] or [[x=b:t]c] *) +let mkLambda_or_LetIn (na,body,t) c = + match body with + | None -> mkLambda (na, t, c) + | Some b -> mkLetIn (na, b, t, c) -let abs_implicit c = mkLambda (Anonymous, mkImplicit, c) -let lambda_implicit a = mkLambda (Name(id_of_string"y"), mkImplicit, a) -let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a) +let mkNamedLambda_or_LetIn (id,body,t) c = + match body with + | None -> mkNamedLambda id t c + | Some b -> mkNamedLetIn id b t c (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) let prodn n env b = @@ -1252,37 +1150,216 @@ let rec isArity c = | Sort _ -> true | _ -> false -(*******************************) -(* alpha conversion functions *) -(*******************************) - -(* alpha conversion : ignore print names and casts *) - -let rec eq_constr m n = - (m==n) or - compare_constr eq_constr m n - -let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) - (*******************) (* hash-consing *) (*******************) -module Htype = - Hashcons.Make( - struct - type t = types - type u = (constr -> constr) * (sorts -> sorts) -(* - let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ} - let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ +(* Hash-consing of [constr] does not use the module [Hashcons] because + [Hashcons] is not efficient on deep tree-like data + structures. Indeed, [Hashcons] is based the (very efficient) + generic hash function [Hashtbl.hash], which computes the hash key + through a depth bounded traversal of the data structure to be + hashed. As a consequence, for a deep [constr] like the natural + number 1000 (S (S (... (S O)))), the same hash is assigned to all + the sub [constr]s greater than the maximal depth handled by + [Hashtbl.hash]. This entails a huge number of collisions in the + hash table and leads to cubic hash-consing in this worst-case. + + In order to compute a hash key that is independent of the data + structure depth while being constant-time, an incremental hashing + function must be devised. A standard implementation creates a cache + of the hashing function by decorating each node of the hash-consed + data structure with its hash key. In that case, the hash function + can deduce the hash key of a toplevel data structure by a local + computation based on the cache held on its substructures. + Unfortunately, this simple implementation introduces a space + overhead that is damageable for the hash-consing of small [constr]s + (the most common case). One can think of an heterogeneous + distribution of caches on smartly chosen nodes, but this is forbidden + by the use of generic equality in Coq source code. (Indeed, this forces + each [constr] to have a unique canonical representation.) + + Given that hash-consing proceeds inductively, we can nonetheless + computes the hash key incrementally during hash-consing by changing + a little the signature of the hash-consing function: it now returns + both the hash-consed term and its hash key. This simple solution is + implemented in the following code: it does not introduce a space + overhead in [constr], that's why the efficiency is unchanged for + small [constr]s. Besides, it does handle deep [constr]s without + introducing an unreasonable number of collisions in the hash table. + Some benchmarks make us think that this implementation of + hash-consing is linear in the size of the hash-consed data + structure for our daily use of Coq. *) -(**) - let hash_sub (hc,hs) j = hc j - let equal j1 j2 = j1==j2 -(**) - let hash = Hashtbl.hash - end) + +let array_eqeq t1 t2 = + t1 == t2 || + (Array.length t1 = Array.length t2 && + let rec aux i = + (i = Array.length t1) || (t1.(i) == t2.(i) && aux (i + 1)) + in aux 0) + +let equals_constr t1 t2 = + match t1, t2 with + | Rel n1, Rel n2 -> n1 == n2 + | Meta m1, Meta m2 -> m1 == m2 + | Var id1, Var id2 -> id1 == id2 + | Sort s1, Sort s2 -> s1 == s2 + | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 & k1 == k2 & t1 == t2 + | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 + | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 + | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> + n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2 + | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_eqeq l1 l2 + | Const c1, Const c2 -> c1 == c2 + | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 & i1 = i2 + | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) -> + sp1 == sp2 & i1 = i2 & j1 = j2 + | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> + ci1 == ci2 & p1 == p2 & c1 == c2 & array_eqeq bl1 bl2 + | Fix (ln1,(lna1,tl1,bl1)), Fix (ln2,(lna2,tl2,bl2)) -> + ln1 = ln2 + & array_eqeq lna1 lna2 + & array_eqeq tl1 tl2 + & array_eqeq bl1 bl2 + | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) -> + ln1 = ln2 + & array_eqeq lna1 lna2 + & array_eqeq tl1 tl2 + & array_eqeq bl1 bl2 + | _ -> false + +(** 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 *) + +module H = Hashtbl_alt.Make(struct type t = constr let equals = equals_constr end) + +open Hashtbl_alt.Combine + +(* [hcons_term hash_consing_functions constr] computes an hash-consed + representation for [constr] using [hash_consing_functions] on + leaves. *) +let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = + + (* Note : we hash-cons constr arrays *in place* *) + + let rec hash_term_array t = + let accu = ref 0 in + for i = 0 to Array.length t - 1 do + let x, h = sh_rec t.(i) in + accu := combine !accu h; + t.(i) <- x + done; + !accu + + and hash_term t = + match t with + | Var i -> + (Var (sh_id i), combinesmall 1 (Hashtbl.hash i)) + | Sort s -> + (Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s)) + | Cast (c, k, t) -> + let c, hc = sh_rec c in + let t, ht = sh_rec t in + (Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht)) + | Prod (na,t,c) -> + let t, ht = sh_rec t + and c, hc = sh_rec c in + (Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc)) + | Lambda (na,t,c) -> + let t, ht = sh_rec t + and c, hc = sh_rec c in + (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc)) + | LetIn (na,b,t,c) -> + let b, hb = sh_rec b in + let t, ht = sh_rec t in + let c, hc = sh_rec c in + (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc)) + | App (c,l) -> + let c, hc = sh_rec c in + let hl = hash_term_array l in + (App (c, l), combinesmall 7 (combine hl hc)) + | Evar (e,l) -> + let hl = hash_term_array l in + (* since the array have been hashed in place : *) + (t, combinesmall 8 (combine (Hashtbl.hash e) hl)) + | Const c -> + (Const (sh_con c), combinesmall 9 (Hashtbl.hash c)) + | Ind ((kn,i) as ind) -> + (Ind (sh_ind ind), combinesmall 9 (combine (Hashtbl.hash kn) i)) + | Construct (((kn,i),j) as c)-> + (Construct (sh_construct c), combinesmall 10 (combine3 (Hashtbl.hash kn) i j)) + | Case (ci,p,c,bl) -> + let p, hp = sh_rec p + and c, hc = sh_rec c in + let hbl = hash_term_array bl in + let hbl = combine (combine hc hp) hbl in + (Case (sh_ci ci, p, c, bl), combinesmall 11 hbl) + | Fix (ln,(lna,tl,bl)) -> + let hbl = hash_term_array bl in + let htl = hash_term_array tl in + Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; + (* since the three arrays have been hashed in place : *) + (t, combinesmall 13 (combine (Hashtbl.hash lna) (combine hbl htl))) + | CoFix(ln,(lna,tl,bl)) -> + let hbl = hash_term_array bl in + let htl = hash_term_array tl in + Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; + (* since the three arrays have been hashed in place : *) + (t, combinesmall 14 (combine (Hashtbl.hash lna) (combine hbl htl))) + | Meta n -> + (t, combinesmall 15 n) + | Rel n -> + (t, combinesmall 16 n) + + and sh_rec t = + let (y, h) = hash_term t in + (* [h] must be positive. *) + let h = h land 0x3FFFFFFF in + (H.may_add_and_get h y, h) + + in + (* Make sure our statically allocated Rels (1 to 16) are considered + as canonical, and hence hash-consed to themselves *) + ignore (hash_term_array rels); + + fun t -> fst (sh_rec t) + +(* Exported hashing fonction on constr, used mainly in plugins. + Appears to have slight differences from [snd (hash_term t)] above ? *) + +let rec hash_constr t = + match kind_of_term t with + | Var i -> combinesmall 1 (Hashtbl.hash i) + | Sort s -> combinesmall 2 (Hashtbl.hash s) + | Cast (c, _, _) -> hash_constr c + | Prod (_, t, c) -> combinesmall 4 (combine (hash_constr t) (hash_constr c)) + | Lambda (_, t, c) -> combinesmall 5 (combine (hash_constr t) (hash_constr c)) + | LetIn (_, b, t, c) -> + combinesmall 6 (combine3 (hash_constr b) (hash_constr t) (hash_constr c)) + | App (c,l) when isCast c -> hash_constr (mkApp (pi1 (destCast c),l)) + | App (c,l) -> + combinesmall 7 (combine (hash_term_array l) (hash_constr c)) + | Evar (e,l) -> + combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l)) + | Const c -> + combinesmall 9 (Hashtbl.hash c) (* TODO: proper hash function for constants *) + | Ind (kn,i) -> + combinesmall 9 (combine (Hashtbl.hash kn) i) + | Construct ((kn,i),j) -> + combinesmall 10 (combine3 (Hashtbl.hash kn) i j) + | Case (_ , p, c, bl) -> + combinesmall 11 (combine3 (hash_constr c) (hash_constr p) (hash_term_array bl)) + | Fix (ln ,(_, tl, bl)) -> + combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) + | CoFix(ln, (_, tl, bl)) -> + combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) + | Meta n -> combinesmall 15 n + | Rel n -> combinesmall 16 n + +and hash_term_array t = + Array.fold_left (fun acc t -> combine (hash_constr t) acc) 0 t module Hsorts = Hashcons.Make( @@ -1300,16 +1377,34 @@ module Hsorts = let hash = Hashtbl.hash end) -let hsort = Hsorts.f +module Hcaseinfo = + Hashcons.Make( + struct + type t = case_info + type u = inductive -> inductive + let hash_sub hind ci = { ci with ci_ind = hind ci.ci_ind } + let equal ci ci' = + ci.ci_ind == ci'.ci_ind && + ci.ci_npar = ci'.ci_npar && + ci.ci_cstr_ndecls = ci'.ci_cstr_ndecls && (* we use (=) on purpose *) + ci.ci_pp_info = ci'.ci_pp_info (* we use (=) on purpose *) + let hash = Hashtbl.hash + end) -let hcons_constr (hcon,hkn,hdir,hname,hident,hstr) = - let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in - let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in - let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in - (hcci,htcci) +let hcons_sorts = Hashcons.simple_hcons Hsorts.f hcons_univ +let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.f hcons_ind -let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names()) +let hcons_constr = + hcons_term + (hcons_sorts, + hcons_caseinfo, + hcons_construct, + hcons_ind, + hcons_con, + hcons_name, + hcons_ident) +let hcons_types = hcons_constr (*******) (* Type of abstract machine values *) -- cgit v1.2.3