Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 66 insertions, 94 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f58a12c6..390b884c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml,v 1.24.2.2 2004/11/26 17:51:52 herbelin Exp $ *)
+(* $Id: pattern.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
 
 open Util
 open Names
@@ -17,18 +17,13 @@ open Rawterm
 open Environ
 open Nametab
 open Pp
+open Mod_subst
 
 (* Metavariables *)
 
 type patvar_map = (patvar * constr) list
-let patvar_of_int n =
-  let p = if !Options.v7 & not (Options.do_translate ()) then "?" else "X"
-  in
-  Names.id_of_string (p ^ string_of_int n)
 let pr_patvar = pr_id
 
-let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n)
-
 (* Patterns *)
 
 type constr_pattern =
@@ -62,57 +57,6 @@ let rec occur_meta_pattern = function
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
-let rec subst_pattern subst pat = match pat with
-  | PRef ref ->
-      let ref' = subst_global subst ref in
-	if ref' == ref then pat else 
-	  PRef ref'
-  | PVar _ 
-  | PEvar _
-  | PRel _ -> pat
-  | PApp (f,args) ->
-      let f' = subst_pattern subst f in 
-      let args' = array_smartmap (subst_pattern subst) args in
-	if f' == f && args' == args then pat else
-	  PApp (f',args')
-  | PSoApp (i,args) ->
-      let args' = list_smartmap (subst_pattern subst) args in
-	if args' == args then pat else
-	  PSoApp (i,args')
-  | PLambda (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PLambda (name,c1',c2')
-  | PProd (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PProd (name,c1',c2')
-  | PLetIn (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PLetIn (name,c1',c2')
-  | PSort _ 
-  | PMeta _ -> pat
-  | PCase (cs,typ, c, branches) -> 
-      let typ' = option_smartmap (subst_pattern subst) typ in 
-      let c' = subst_pattern subst c in
-      let branches' = array_smartmap (subst_pattern subst) branches in
-	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(cs,typ', c', branches') 
-  | PFix fixpoint ->
-      let cstr = mkFix fixpoint in
-      let fixpoint' = destFix (subst_mps subst cstr) in
-	if fixpoint' == fixpoint then pat else
-	  PFix fixpoint'
-  | PCoFix cofixpoint ->
-      let cstr = mkCoFix cofixpoint in
-      let cofixpoint' = destCoFix (subst_mps subst cstr) in
-	if cofixpoint' == cofixpoint then pat else
-	  PCoFix cofixpoint'
-
 type constr_label =
   | ConstNode of constant
   | IndNode of inductive
@@ -121,33 +65,14 @@ type constr_label =
 
 exception BoundPattern;;
 
-let label_of_ref = function
-  | ConstRef sp     -> ConstNode sp
-  | IndRef sp       -> IndNode sp
-  | ConstructRef sp -> CstrNode sp
-  | VarRef id       -> VarNode id
-
-let ref_of_label = function
-  | ConstNode sp     -> ConstRef sp
-  | IndNode sp       -> IndRef sp
-  | CstrNode sp      -> ConstructRef sp
-  | VarNode id       -> VarRef id
-
-let subst_label subst cstl = 
-  let ref = ref_of_label cstl in
-  let ref' = subst_global subst ref in
-    if ref' == ref then cstl else
-      label_of_ref ref'
-      
-  
 let rec head_pattern_bound t =
   match t with
     | PProd (_,_,b)  -> head_pattern_bound b 
     | PLetIn (_,_,b) -> head_pattern_bound b 
     | PApp (c,args)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
-    | PRef r         -> label_of_ref r
-    | PVar id        -> VarNode id
+    | PRef r         -> r
+    | PVar id        -> VarRef id
     | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
@@ -155,10 +80,10 @@ let rec head_pattern_bound t =
     | PCoFix _ -> anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
-  | Const sp -> ConstNode sp
-  | Construct sp -> CstrNode sp
-  | Ind sp -> IndNode sp
-  | Var id -> VarNode id
+  | Const sp -> ConstRef sp
+  | Construct sp -> ConstructRef sp
+  | Ind sp -> IndRef sp
+  | Var id -> VarRef id
   | _ -> anomaly "Not a rigid reference"
 
 let rec pattern_of_constr t =
@@ -168,7 +93,7 @@ let rec pattern_of_constr t =
     | Var id -> PVar id
     | Sort (Prop c) -> PSort (RProp c)
     | Sort (Type _) -> PSort (RType None)
-    | Cast (c,_)      -> pattern_of_constr c
+    | Cast (c,_,_)      -> pattern_of_constr c
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
@@ -198,9 +123,61 @@ let rec inst lvar = function
   (* Non recursive *)
   | (PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x 
   (* Bound to terms *)
-  | (PFix _ | PCoFix _ as r) ->
+  | (PFix _ | PCoFix _) ->
       error ("Not instantiable pattern")
 
+let rec subst_pattern subst pat = match pat with
+  | PRef ref ->
+      let ref',t = subst_global subst ref in
+	if ref' == ref then pat else
+	 pattern_of_constr t
+  | PVar _ 
+  | PEvar _
+  | PRel _ -> pat
+  | PApp (f,args) ->
+      let f' = subst_pattern subst f in 
+      let args' = array_smartmap (subst_pattern subst) args in
+	if f' == f && args' == args then pat else
+	  PApp (f',args')
+  | PSoApp (i,args) ->
+      let args' = list_smartmap (subst_pattern subst) args in
+	if args' == args then pat else
+	  PSoApp (i,args')
+  | PLambda (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PLambda (name,c1',c2')
+  | PProd (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PProd (name,c1',c2')
+  | PLetIn (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PLetIn (name,c1',c2')
+  | PSort _ 
+  | PMeta _ -> pat
+  | PCase (cs,typ, c, branches) -> 
+      let typ' = option_smartmap (subst_pattern subst) typ in 
+      let c' = subst_pattern subst c in
+      let branches' = array_smartmap (subst_pattern subst) branches in
+	if typ' == typ && c' == c && branches' == branches then pat else
+	  PCase(cs,typ', c', branches') 
+  | PFix fixpoint ->
+      let cstr = mkFix fixpoint in
+      let fixpoint' = destFix (subst_mps subst cstr) in
+	if fixpoint' == fixpoint then pat else
+	  PFix fixpoint'
+  | PCoFix cofixpoint ->
+      let cstr = mkCoFix cofixpoint in
+      let cofixpoint' = destCoFix (subst_mps subst cstr) in
+	if cofixpoint' == cofixpoint then pat else
+	  PCoFix cofixpoint'
+
+
 let instantiate_pattern = inst
 
 let rec pat_of_raw metas vars = function
@@ -230,30 +207,25 @@ let rec pat_of_raw metas vars = function
       PSort s
   | RHole _ ->
       PMeta None
-  | RCast (_,c,t) ->
+  | RCast (_,c,_,t) ->
       Options.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
-  | ROrderedCase (_,st,po,c,br,_) ->
-      PCase ((None,st),option_app (pat_of_raw metas vars) po,
-             pat_of_raw metas vars c,
-             Array.map (pat_of_raw metas vars) br)
   | RIf (_,c,(_,None),b1,b2) ->
       PCase ((None,IfStyle),None, pat_of_raw metas vars c,
              [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
-  | RCases (loc,(po,_),[c,_],brs) ->
+  | RCases (loc,None,[c,_],brs) ->
       let sp =
 	match brs with
 	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	  | _ -> None in
-      (* When po disappears: switch to rtn type *)
-      PCase ((sp,Term.RegularStyle),option_app (pat_of_raw metas vars) po,
+      PCase ((sp,Term.RegularStyle),None,
              pat_of_raw metas vars c,
              Array.init (List.length brs)
 	       (pat_of_raw_branch loc metas vars sp brs))
   | r ->
       let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern")
+      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
 
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter