Ajout de la possibilité d'utiliser fix/cofix dans les notations.

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

5 files changed, 63 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index f6ced6768..f18e1c575 100644
--- a/CHANGES
+++ b/CHANGES
@@ -113,6 +113,7 @@ Notations, coercions, implicit arguments and type inference
 - Support for parametric notations defining constants.
 - Insertion of coercions below product types refrains to unfold
   constants (possible source of incompatibility).
+- New support for fix/cofix in notations.
 
 Tactic Language
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 081c2117b..35b8f075a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -42,6 +42,9 @@ type aconstr =
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+  | ARec of fix_kind * identifier array *
+      (name * aconstr option * aconstr) list array * aconstr array * 
+      aconstr array
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
@@ -102,6 +105,12 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_fold_map g e na in
       RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
+  | ARec (fk,idl,dll,tl,bl) ->
+      let e,idl = array_fold_map g e idl in
+      let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
+	  let e,na = name_fold_map g e na in
+	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
+      RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
   | ACast (c,k) -> RCast (loc,f e c, 
 			  match k with 
 			    | CastConv (k,t) -> CastConv (k,f e t)
@@ -199,6 +208,13 @@ let aconstr_and_vars_of_rawconstr a =
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
       AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
+  | RRec (_,fk,idl,dll,tl,bl) ->
+      Array.iter (fun id -> found := id::!found) idl;
+      let dll = Array.map (List.map (fun (na,bk,oc,b) -> 
+	 if bk <> Explicit then 
+	   error "Binders marked as implicit not allowed in notations";
+	 add_name found na; (na,Option.map aux oc,aux b))) dll in
+      ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | RCast (_,c,k) -> ACast (aux c, 
 			    match k with CastConv (k,t) -> CastConv (k,aux t) 
 			      | CastCoerce -> CastCoerce)
@@ -206,8 +222,8 @@ let aconstr_and_vars_of_rawconstr a =
   | RHole (_,w) -> AHole w
   | RRef (_,r) -> ARef r
   | RPatVar (_,(_,n)) -> APatVar n
-  | RDynamic _ | RRec _ | REvar _ ->
-      error "Fixpoints, cofixpoints and existential variables not allowed in abbreviatable expressions"
+  | RDynamic _ | REvar _ ->
+      error "Existential variables not allowed in notations"
 
   (* Recognizing recursive notations *)
   and terminator_of_pat f1 ll1 lr1 = function
@@ -340,6 +356,17 @@ let rec subst_aconstr subst bound raw =
 	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
 	  AIf (c',(na,po'),b1',b2')
 
+  | ARec (fk,idl,dll,tl,bl) ->
+      let dll' = 
+	array_smartmap (list_smartmap (fun (na,oc,b as x) ->
+	  let oc' =  Option.smartmap (subst_aconstr subst bound) oc in
+	  let b' =  subst_aconstr subst bound b in
+	  if oc' == oc && b' == b then x else (na,oc',b'))) dll in
+      let tl' = array_smartmap (subst_aconstr subst bound) tl in
+      let bl' = array_smartmap (subst_aconstr subst bound) bl in
+      if dll' == dll && tl' == tl && bl' == bl then raw else
+	  ARec (fk,idl,dll',tl',bl')
+
   | APatVar _ | ASort _ -> raw
 
   | AHole (Evd.ImplicitArg (ref,i)) ->
@@ -411,6 +438,14 @@ let bind_env alp sigma var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma
 
+let match_fix_kind fk1 fk2 =
+  match (fk1,fk2) with
+  | RCoFix n1, RCoFix n2 -> n1 = n2
+  | RFix (nl1,n1), RFix (nl2,n2) ->
+      n1 = n2 && 
+      array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
+  | _ -> false
+
 let match_opt f sigma t1 t2 = match (t1,t2) with
   | None, None -> sigma
   | Some t1, Some t2 -> f sigma t1 t2
@@ -465,9 +500,6 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
       let sigma = List.fold_left2 
        (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
       List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
-  | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
-      let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
-      List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
   | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) 
       when List.length nal1 = List.length nal2 ->
       let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
@@ -475,6 +507,22 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
       let (alp,sigma) =
 	List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
       match_ alp metas sigma c1 c2
+  | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
+      let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
+      List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
+  | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) 
+      when match_fix_kind fk1 fk2 & Array.length idl1 =  Array.length idl2 &
+	array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
+	->
+      let alp,sigma = array_fold_left2
+	(List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
+	  let sigma =
+	    match_ alp metas (match_opt (match_ alp metas) sigma oc1 oc2) b1 b2
+	  in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
+      let sigma = array_fold_left2 (match_ alp metas) sigma tl1 tl2 in
+      let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> 
+	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
+      array_fold_left2 (match_ alp metas) sigma bl1 bl2
   | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
   | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index f56550dd5..155ac9ca8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -38,6 +38,9 @@ type aconstr =
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+  | ARec of fix_kind * identifier array *
+      (name * aconstr option * aconstr) list array * aconstr array * 
+      aconstr array
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
diff --git a/lib/util.ml b/lib/util.ml
index af99e2b23..26be66cb9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1056,6 +1056,11 @@ else
   let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
   (v',!e')
 
+let array_fold_map f e v =
+  let e' = ref e in
+  let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in
+  (!e',v')
+
 let array_fold_map2' f v1 v2 e =
   let e' = ref e in
   let v' = 
diff --git a/lib/util.mli b/lib/util.mli
index 17a7af197..0cbd2fa0e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -208,6 +208,7 @@ val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
   'b array * 'd array
 val array_iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
 val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+val array_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
 val array_fold_map2' :
   ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
 val array_distinct : 'a array -> bool