Changement des named_context

Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 45 insertions, 37 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 8bd079ce5f..f59ba5d66f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -21,6 +21,8 @@ open Esubst
 type existential_key = int
 type metavariable = int
 
+(* This defines the strategy to use for verifiying a Cast *)
+
 (* This defines Cases annotations *)
 type pattern_source = DefaultPat of int | RegularPat
 type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
@@ -56,6 +58,8 @@ 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
@@ -74,7 +78,7 @@ type ('constr, 'types) kind_of_term =
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
-  | Cast      of 'constr * 'types
+  | Cast      of 'constr * cast_kind * 'types
   | Prod      of name * 'types * 'types
   | Lambda    of name * 'types * 'constr
   | LetIn     of name * 'constr * 'types * 'constr
@@ -89,14 +93,14 @@ type ('constr, 'types) kind_of_term =
 (* Experimental *)
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
-  | CastType   of 'types * 'types
+  | 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)
+  | 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)
@@ -123,7 +127,7 @@ let comp_term t1 t2 =
   | 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
+  | 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) ->
@@ -154,7 +158,7 @@ let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t =
   | Meta x -> Meta x
   | Var x -> Var (sh_id x)
   | Sort s -> Sort (sh_sort s)
-  | Cast (c,t) -> Cast (sh_rec c, sh_rec t)
+  | 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)
@@ -207,11 +211,12 @@ let mkVar id = Var id
 let mkSort 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) *)
-let mkCast (t1,t2) =
+(* (that means t2 is declared as the type of t1) 
+   [s] is the strategy to use when *)
+let mkCast (t1,k2,t2) =
   match t1 with
-    | Cast (t,_) -> Cast (t,t2)
-    | _ -> Cast (t1,t2)
+  | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2)
+  | _ -> Cast (t1,k2,t2)
 
 (* Constructs the product (x:t1)t2 *)
 let mkProd (x,t1,t2) = Prod (x,t1,t2)
@@ -310,22 +315,22 @@ let destSort c = match kind_of_term c with
 
 let rec isprop c = match kind_of_term c with
   | Sort (Prop _) -> true
-  | Cast (c,_) -> isprop c
+  | Cast (c,_,_) -> isprop c
   | _ -> false
 
 let rec is_Prop c = match kind_of_term c with
   | Sort (Prop Null) -> true
-  | Cast (c,_) -> is_Prop c
+  | Cast (c,_,_) -> is_Prop c
   | _ -> false
 
 let rec is_Set c = match kind_of_term c with
   | Sort (Prop Pos) -> true
-  | Cast (c,_) -> is_Set c
+  | Cast (c,_,_) -> is_Set c
   | _ -> false
 
 let rec is_Type c = match kind_of_term c with
   | Sort (Type _) -> true
-  | Cast (c,_) -> is_Type c
+  | Cast (c,_,_) -> is_Type c
   | _ -> false
 
 let isType = function
@@ -345,10 +350,11 @@ let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false
 
 (* Destructs a casted term *)
 let destCast c = match kind_of_term c with 
-  | Cast (t1, t2) -> (t1,t2)
+  | Cast (t1,k,t2) -> (t1,k,t2)
   | _ -> invalid_arg "destCast"
 
-let isCast c = match kind_of_term c with Cast (_,_) -> true | _ -> false
+let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
+
 
 (* Tests if a de Bruijn index *)
 let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
@@ -434,7 +440,7 @@ let rec collapse_appl 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,_) when isApp c -> collapse_rec c cl2
+	| Cast (c,_,_) when isApp c -> collapse_rec c cl2
 	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
@@ -450,11 +456,11 @@ 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
+	| Cast (c,_,_) -> collapse_rec c cl2
 	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
-  | Cast (c,t) -> strip_head_cast c
+  | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
 
 (****************************************************************************)
@@ -468,7 +474,7 @@ let rec strip_head_cast c = match kind_of_term c with
 let fold_constr f acc c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
-  | Cast (c,t) -> f (f acc c) t
+  | Cast (c,_,t) -> f (f acc c) t
   | Prod (_,t,c) -> f (f acc t) c
   | Lambda (_,t,c) -> f (f acc t) c
   | LetIn (_,b,t,c) -> f (f (f acc b) t) c
@@ -489,7 +495,7 @@ let fold_constr f acc c = match kind_of_term c with
 let iter_constr f c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
-  | Cast (c,t) -> f c; f t
+  | Cast (c,_,t) -> f c; f t
   | Prod (_,t,c) -> f t; f c
   | Lambda (_,t,c) -> f t; f c
   | LetIn (_,b,t,c) -> f b; f t; f c
@@ -508,7 +514,7 @@ let iter_constr f c = match kind_of_term c with
 let iter_constr_with_binders g f n c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
-  | Cast (c,t) -> f n c; f n t
+  | Cast (c,_,t) -> f n c; f n t
   | Prod (_,t,c) -> f n t; f (g n) c
   | Lambda (_,t,c) -> f n t; f (g n) c
   | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
@@ -529,7 +535,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
 let map_constr f c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
-  | Cast (c,t) -> mkCast (f c, f t)
+  | Cast (c,k,t) -> mkCast (f c, k, f t)
   | Prod (na,t,c) -> mkProd (na, f t, f c)
   | Lambda (na,t,c) -> mkLambda (na, f t, f c)
   | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
@@ -550,7 +556,7 @@ let map_constr f c = match kind_of_term c with
 let map_constr_with_binders g f l c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
-  | Cast (c,t) -> mkCast (f l c, f l t)
+  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
   | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c)
   | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
   | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
@@ -575,8 +581,8 @@ let compare_constr f t1 t2 =
   | Meta m1, Meta m2 -> m1 = m2
   | Var id1, Var id2 -> id1 = id2
   | Sort s1, Sort s2 -> s1 = s2
-  | Cast (c1,_), _ -> f c1 t2
-  | _, Cast (c2,_) -> f t1 c2
+  | Cast (c1,_,_), _ -> f c1 t2
+  | _, Cast (c2,_,_) -> f t1 c2
   | 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
@@ -607,6 +613,8 @@ let compare_constr f t1 t2 =
 
 type types = constr
 
+type strategy = types option 
+
 let type_app f tt = f tt
 
 let body_of_type ty = ty
@@ -673,7 +681,7 @@ let noccur_with_meta n m term =
     | Rel p -> if n<=p & p<n+m then raise LocalOccur
     | App(f,cl) ->
 	(match kind_of_term f with
-           | Cast (c,_) when isMeta c -> ()
+           | Cast (c,_,_) when isMeta c -> ()
            | Meta _ -> ()
 	   | _ -> iter_constr_with_binders succ occur_rec n c)
     | Evar (_, _) -> ()
@@ -942,17 +950,17 @@ let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0))
 let mkImplicit = mkSort implicit_sort
 
 let rec strip_outer_cast c = match kind_of_term c with
-  | Cast (c,_) -> strip_outer_cast c
+  | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
 
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
 
 let under_outer_cast f c =  match kind_of_term c with
-  | Cast (b,t) -> mkCast (f b,f t)
+  | Cast (b,k,t) -> mkCast (f b, k, f t)
   | _ -> f c
 
 let rec under_casts f c = match kind_of_term c with
-  | Cast (c,t) -> mkCast (under_casts f c, t)
+  | Cast (c,k,t) -> mkCast (under_casts f c, k, t)
   | _            -> f c
 
 (***************************)
@@ -1003,7 +1011,7 @@ let rec to_lambda n prod =
   else 
     match kind_of_term prod with 
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
-      | Cast (c,_) -> to_lambda n c
+      | Cast (c,_,_) -> to_lambda n c
       | _   -> errorlabstrm "to_lambda" (mt ())                      
 
 let rec to_prod n lam =
@@ -1012,7 +1020,7 @@ let rec to_prod n lam =
   else   
     match kind_of_term lam with 
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
-      | Cast (c,_) -> to_prod n c
+      | Cast (c,_,_) -> to_prod n c
       | _   -> errorlabstrm "to_prod" (mt ())                      
 	    
 (* pseudo-reduction rule:
@@ -1042,7 +1050,7 @@ let prod_applist t nL = List.fold_left prod_app t nL
 let decompose_prod = 
   let rec prodec_rec l c = match kind_of_term c with
     | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
-    | Cast (c,_)   -> prodec_rec l c
+    | Cast (c,_,_)   -> prodec_rec l c
     | _              -> l,c
   in 
   prodec_rec []
@@ -1052,7 +1060,7 @@ let decompose_prod =
 let decompose_lam = 
   let rec lamdec_rec l c = match kind_of_term c with
     | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
-    | Cast (c,_)     -> lamdec_rec l c
+    | Cast (c,_,_)     -> lamdec_rec l c
     | _                -> l,c
   in 
   lamdec_rec []
@@ -1065,7 +1073,7 @@ let decompose_prod_n n =
     if n=0 then l,c 
     else match kind_of_term c with 
       | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
-      | Cast (c,_)   -> prodec_rec l n c
+      | Cast (c,_,_)   -> prodec_rec l n c
       | _ -> error "decompose_prod_n: not enough products"
   in 
   prodec_rec [] n 
@@ -1078,7 +1086,7 @@ let decompose_lam_n n =
     if n=0 then l,c 
     else match kind_of_term c with 
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
-      | Cast (c,_)     -> lamdec_rec l n c
+      | Cast (c,_,_)     -> lamdec_rec l n c
       | _ -> error "decompose_lam_n: not enough abstractions"
   in 
   lamdec_rec [] n 
@@ -1088,7 +1096,7 @@ let decompose_lam_n n =
 let nb_lam = 
   let rec nbrec n c = match kind_of_term c with
     | Lambda (_,_,c) -> nbrec (n+1) c
-    | Cast (c,_) -> nbrec n c
+    | Cast (c,_,_) -> nbrec n c
     | _ -> n
   in 
   nbrec 0
@@ -1097,7 +1105,7 @@ let nb_lam =
 let nb_prod = 
   let rec nbrec n c = match kind_of_term c with
     | Prod (_,_,c) -> nbrec (n+1) c
-    | Cast (c,_) -> nbrec n c
+    | Cast (c,_,_) -> nbrec n c
     | _ -> n
   in 
   nbrec 0