Ajout des Fix et CoFix dans les patterns

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

3 files changed, 14 insertions, 7 deletions

diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index a15198a4c3..43e5d4877c 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -18,6 +18,8 @@ type constr_pattern =
   | PSort of rawsort
   | PMeta of int option
   | PCase of constr_pattern option * constr_pattern * constr_pattern array
+  | PFix of fixpoint
+  | PCoFix of cofixpoint
 
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
@@ -29,7 +31,7 @@ let rec occur_meta_pattern = function
       (occur_meta_pattern p) or
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
   | PMeta _ | PSoApp _ -> true
-  | PVar _ | PRef _ | PRel _ | PSort _   -> false
+  | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
 type constr_label =
   | ConstNode of section_path
@@ -58,7 +60,8 @@ let rec head_pattern_bound t =
     | PRef r                -> label_of_ref r
     | PVar id               -> VarNode id
     | PRel _ | PMeta _ | PSoApp _  | PSort _ -> raise BoundPattern
-    | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type"
+    | PBinder(BLambda,_,_,_) | PFix _ | PCoFix _ ->
+      anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
   | IsConst (sp,_) -> ConstNode sp
@@ -179,10 +182,9 @@ let matches_core convert pat c =
 	  (* On ne teste pas le prédicat *)
 	  array_fold_left2 (sorec stk) (sorec stk sigma a1 a2)
 	    br1 br2
-
-      | _,(IsFix _ | IsCoFix _) ->
-	  error "somatch: not implemented"
-
+      (* À faire *)
+      |	PFix f0, IsFix f1 when f0 = f1 -> sigma
+      |	PCoFix c0, IsCoFix c1 when c0 = c1 -> sigma
       | _ -> raise PatternMatchingFailure
 
   in 
@@ -312,7 +314,8 @@ let rec pattern_of_constr t =
     | IsMutCase (ci,p,a,br) ->
 	PCase (Some (pattern_of_constr p),pattern_of_constr a,
 	       Array.map pattern_of_constr br)
-    | IsFix _ | IsCoFix _ ->
+    | IsFix f -> PFix f
+    | IsCoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
     | IsXtra _   -> anomaly "No longer supported"
 
diff --git a/parsing/pattern.mli b/parsing/pattern.mli
index 41ac6108ac..b50f67ed82 100644
--- a/parsing/pattern.mli
+++ b/parsing/pattern.mli
@@ -18,6 +18,8 @@ type constr_pattern =
   | PSort of Rawterm.rawsort
   | PMeta of int option
   | PCase of constr_pattern option * constr_pattern * constr_pattern array
+  | PFix of fixpoint
+  | PCoFix of cofixpoint
 
 val occur_meta_pattern : constr_pattern -> bool
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 1cacd9b3e3..cd708e3040 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -383,6 +383,8 @@ let rec ast_of_pattern env = function
 
   | PMeta (Some n) -> ope("META",[num n])
   | PMeta None -> ope("ISEVAR",[])
+  | PFix f -> ast_of_raw (Detyping.detype [] env (mkFix f))
+  | PCoFix c -> ast_of_raw (Detyping.detype [] env (mkCoFix c))
 	
 and ast_of_patopt env = function
   | None -> (str "SYNTH")