Merge PR #486: Make some functions on terms more robust w.r.t new term constructs.

4 files changed, 67 insertions, 31 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index e1b086b753..fa12e54068 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -480,7 +480,8 @@ let rec lft_fconstr n ft =
     | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
     | FLIFT(k,m) -> lft_fconstr (n+k) m
     | FLOCKED -> assert false
-    | _ -> {norm=ft.norm; term=FLIFT(n,ft)}
+    | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+      | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
@@ -958,7 +959,10 @@ let rec knr info m stk =
       (match evar_value info.i_cache ev with
           Some c -> knit info env c stk
         | None -> (m,stk))
-  | _ -> (m,stk)
+  | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+    | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
+    | FCLOS _ -> (m, stk)
+
 
 (* Computes the weak head normal form of a term *)
 and kni info m stk =
@@ -1034,7 +1038,8 @@ and norm_head info m =
           mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
       | FProj (p,c) ->
           mkProj (p, kl info c)
-      | t -> term_of_fconstr m
+      | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+        | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index be59f93414..5930cfadc6 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -674,6 +674,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
   | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2
   | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2
+  (* Why do we suddenly make a special case for Cast here? *)
   | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
   | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
   | App (c1,l1), App (c2,l2) ->
@@ -691,7 +692,9 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
       && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
       Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
-  | _ -> false
+  | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
+     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
+     | CoFix _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -811,9 +814,6 @@ let always_true _ _ = true
 let rec eq_constr_nounivs m n =
   (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n
 
-(** We only use this function over blocks! *)
-let tag t = Obj.tag (Obj.repr t)
-
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
     let c = f i1 i2 in
@@ -825,35 +825,50 @@ let constr_ord_int f t1 t2 =
     ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
   in
   match kind t1, kind t2 with
+    | Cast (c1,_,_), _ -> f c1 t2
+    | _, Cast (c2,_,_) -> f t1 c2
+    (* Why this special case? *)
+    | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
+    | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
     | Rel n1, Rel n2 -> Int.compare n1 n2
-    | Meta m1, Meta m2 -> Int.compare m1 m2
+    | Rel _, _ -> -1 | _, Rel _ -> 1
     | Var id1, Var id2 -> Id.compare id1 id2
+    | Var _, _ -> -1 | _, Var _ -> 1
+    | Meta m1, Meta m2 -> Int.compare m1 m2
+    | Meta _, _ -> -1 | _, Meta _ -> 1
+    | Evar (e1,l1), Evar (e2,l2) ->
+        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+    | Evar _, _ -> -1 | _, Evar _ -> 1
     | Sort s1, Sort s2 -> Sorts.compare s1 s2
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
+    | Sort _, _ -> -1 | _, Sort _ -> 1
     | Prod (_,t1,c1), Prod (_,t2,c2)
     | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
         (f =? f) t1 t2 c1 c2
+    | Prod _, _ -> -1 | _, Prod _ -> 1
+    | Lambda _, _ -> -1 | _, Lambda _ -> 1
     | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
         ((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
-    | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
+    | LetIn _, _ -> -1 | _, LetIn _ -> 1
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
-    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
-    | Evar (e1,l1), Evar (e2,l2) ->
-        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+    | App _, _ -> -1 | _, App _ -> 1
     | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2
+    | Const _, _ -> -1 | _, Const _ -> 1
     | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2
+    | Ind _, _ -> -1 | _, Ind _ -> 1
     | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2
+    | Construct _, _ -> -1 | _, Construct _ -> 1
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
         ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
+    | Case _, _ -> -1 | _, Case _ -> 1
     | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
         ((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
         ln1 ln2 tl1 tl2 bl1 bl2
+    | Fix _, _ -> -1 | _, Fix _ -> 1
     | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
         ((Int.compare =? (Array.compare f)) ==? (Array.compare f))
         ln1 ln2 tl1 tl2 bl1 bl2
-    | t1, t2 -> Int.compare (tag t1) (tag t2)
+    | CoFix _, _ -> -1 | _, CoFix _ -> 1
+    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
 
 let rec compare m n=
   constr_ord_int compare m n
@@ -937,7 +952,9 @@ let hasheq t1 t2 =
       && array_eqeq lna1 lna2
       && array_eqeq tl1 tl2
       && array_eqeq bl1 bl2
-    | _ -> false
+    | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
+      | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
+      | Fix _ | CoFix _), _ -> 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 *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0782ea820d..62aa9a2d7b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -809,8 +809,11 @@ let rec subterm_specif renv stack t =
 	| Dead_code -> Dead_code
 	| Not_subterm -> Not_subterm)
 
+    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+      | Construct _ | CoFix _ -> Not_subterm
+
+
       (* Other terms are not subterms *)
-    | _ -> Not_subterm
 
 and lazy_subterm_specif renv stack t =
   lazy (subterm_specif renv stack t)
@@ -1193,8 +1196,8 @@ let check_one_cofix env nbfix def deftype =
 	| Meta _ -> ()
         | Evar _ ->
 	    List.iter (check_rec_call env alreadygrd n tree vlra) args
-
-	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+        | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
+          | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let ((mind, _),_) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bf998933e3..41d6c05eb5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -57,7 +57,9 @@ let compare_stack_shape stk1 stk2 =
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-    | (_,_) -> false in
+    | [], _ :: _
+    | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false
+  in
   compare_rec 0 stk1 stk2
 
 type lft_constr_stack_elt =
@@ -122,14 +124,17 @@ let nf_betaiota env t =
 
 let whd_betaiotazeta env x =
   match kind x with
-    | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
+  | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
-      | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+      | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+        | Case _ | Fix _ | CoFix _ | Proj _ ->
+         whd_val (create_clos_infos betaiotazeta env) (inject x)
       end
-    | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+    | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
+        whd_val (create_clos_infos betaiotazeta env) (inject x)
 
 let whd_all env t =
   match kind t with
@@ -138,9 +143,12 @@ let whd_all env t =
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ -> t
-      | _ -> whd_val (create_clos_infos all env) (inject t)
+      | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+        | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
+         whd_val (create_clos_infos all env) (inject t)
       end
-    | _ -> whd_val (create_clos_infos all env) (inject t)
+    | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
+        whd_val (create_clos_infos all env) (inject t)
 
 let whd_allnolet env t =
   match kind t with
@@ -149,9 +157,12 @@ let whd_allnolet env t =
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
-      | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+      | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
+        | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
+         whd_val (create_clos_infos allnolet env) (inject t)
       end
-    | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+    | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
+        whd_val (create_clos_infos allnolet env) (inject t)
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -578,10 +589,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
-       | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
+       | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
 
-     (* In all other cases, terms are not convertible *)
-     | _ -> raise NotConvertible
+     | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
+        | FProd _ | FEvar _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks