Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 411 insertions, 316 deletions

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     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* This module instantiates the structure of generic deBruijn terms to Coq *)
+(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
+(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)
+(* Extension to mutual inductive constructions by Christine Paulin for
+   Coq V5.10.2 *)
+(* Extension to co-inductive constructions by Eduardo Gimenez *)
+(* Optimization of substitution functions by Chet Murthy *)
+(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
+(* Hash-consing by Bruno Barras in Feb 1998 *)
+(* Restructuration of Coq of the type-checking kernel by Jean-Christophe 
+   Filliâtre, 1999 *)
+(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+
+(* This file defines the internal syntax of the Calculus of
+   Inductive Constructions (CIC) terms together with constructors,
+   destructors, iterators and basic functions *)
 
 open Util
 open Pp
@@ -16,12 +29,14 @@ open Names
 open Univ
 open Esubst
 
-(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
 type existential_key = int
 type metavariable = int
 
 (* This defines the strategy to use for verifiying a Cast *)
+(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *)
+(* come after the vo-exported cast_kind so as to be compatible with coqchk *)
+type cast_kind = VMcast | DEFAULTcast | REVERTcast
 
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
@@ -31,7 +46,7 @@ type case_printing =
 type case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
-    ci_cstr_nargs : int array; (* number of real args of each constructor *)
+    ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
     ci_pp_info    : case_printing (* not interpreted by the kernel *)
   }
 
@@ -58,8 +73,6 @@ let family_of_sort = function
 (*       Constructions as implemented                               *)
 (********************************************************************)
 
-type cast_kind = VMcast | DEFAULTcast
-
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type 'constr pexistential = existential_key * 'constr array
@@ -90,24 +103,6 @@ type ('constr, 'types) kind_of_term =
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
 
-(* Experimental *)
-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
-
-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"
-
 (* 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<n & n<=16 then rels.(n-1) else Rel n
 
-(* Constructs an existential variable named "?n" *)
-let mkMeta  n =  Meta n
-
-(* Constructs a Variable named id *)
-let mkVar id = Var id
-
 (* Construct a type *)
-let mkSort s = Sort s
+let mkProp   = Sort prop_sort
+let mkSet    = Sort set_sort
+let mkType u = Sort (Type u)
+let mkSort   = function
+  | Prop Null -> 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 <p>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 <p>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 *)