Make some functions on terms more robust w.r.t new term constructs.

Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.

4 files changed, 67 insertions, 31 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index e1b086b75..fa12e5406 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 cec00c04b..892414e45 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -513,6 +513,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) ->
@@ -530,7 +531,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,
@@ -650,9 +653,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
@@ -664,35 +664,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
@@ -776,7 +791,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 cb03a4d6b..aad12207e 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 bf998933e..41d6c05eb 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