Motifs recursifs de notations: prise en compte de l'associativite et des notations de pattern de filtrage

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

4 files changed, 48 insertions, 23 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ddd9ef044..2ccd2f69c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -389,8 +389,18 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
+let decode_patlist_value = function
+  | CPatCstr (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let rec subst_pat_iterator y t = function
+  | PatVar (_,id) as x ->
+      if id = Name y then t else x
+  | PatCstr (loc,id,l,alias) ->
+      PatCstr (loc,id,List.map (subst_pat_iterator y t) l,alias)
+
 let subst_cases_pattern loc aliases intern subst scopes a =
-  let rec aux aliases = function
+  let rec aux aliases subst = function
   | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
@@ -399,7 +409,8 @@ let subst_cases_pattern loc aliases intern subst scopes a =
 	  let (a,(scopt,subscopes)) = List.assoc id subst in
 	  intern (subscopes@scopes) ([],[]) scopt a
 	with Not_found -> 
-	  anomaly "Unbound pattern notation variable"
+	  if id = ldots_var then [[],[]], PatVar (loc,Name id) else
+	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
 	  (*
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
 	  if aliases <> ([],[]) then
@@ -412,10 +423,24 @@ let subst_cases_pattern loc aliases intern subst scopes a =
   | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
       let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
       let _,args = list_chop nparams args in
-      let (idsl,pl) = List.split (List.map (aux ([],[])) args) in
+      let (idsl,pl) = List.split (List.map (aux ([],[]) subst) args) in
       aliases::List.flatten idsl, PatCstr (loc,c,pl,alias_of aliases)
+  | AList (x,y,iter,terminator,lassoc) ->
+      (try 
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (a,(scopt,subscopes)) = List.assoc x subst in
+        let idslt,termin = aux ([],[]) subst terminator in
+        let l = decode_patlist_value a in
+        let idsl,v =
+	  List.fold_right (fun a (allidsl,t) -> 
+            let idsl,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in
+            idsl::allidsl, subst_pat_iterator y t u)
+            (if lassoc then List.rev l else l) ([idslt],termin) in
+        aliases::List.flatten idsl, v
+      with Not_found -> 
+          anomaly "Inconsistent substitution of recursive notation")
   | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
-  in aux aliases a
+  in aux aliases subst a
 
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
@@ -655,7 +680,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
 	  RVar (loc,id)
       end
-  | AList (x,y,iter,terminator) ->
+  | AList (x,y,iter,terminator,lassoc) ->
       (try 
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (a,(scopt,subscopes)) = List.assoc x subst in
@@ -668,7 +693,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
             (subst_aconstr_in_rawconstr loc interp 
               ((x,(a,(scopt,subscopes)))::subst)
               (ids,None,scopes) iter))
-            l termin
+            (if lassoc then List.rev l else l) termin
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
   | t ->
diff --git a/interp/symbols.ml b/interp/symbols.ml
index eb2e60d0d..7a2f2e3c9 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -175,7 +175,7 @@ let cases_pattern_key = function
 
 let aconstr_key = function
   | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
-  | AList (_,_,AApp (ARef ref,args),_) -> RefKey ref, Some (List.length args)
+  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
   | ARef ref -> RefKey ref, Some 0
   | _ -> Oth, None
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 832a6ab68..f0011af06 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -23,14 +23,14 @@ open Term
 
 (* For AList: first constr is iterator, second is terminator;
    first id is place of n-th argument in iterator and snd id is recursive
-   place in iterator *)
+   place in iterator; boolean is associativity *)
 
 type aconstr =
   (* Part common to rawconstr and cases_pattern *)
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
-  | AList of identifier * identifier * aconstr * aconstr
+  | AList of identifier * identifier * aconstr * aconstr * bool
   (* Part only in rawconstr *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
@@ -110,10 +110,10 @@ let rec subst_aconstr subst raw =
 	if r' == r && rl' == rl then raw else
 	  AApp(r',rl')
 
-  | AList (id1,id2,r1,r2) -> 
+  | AList (id1,id2,r1,r2,b) -> 
       let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  AList (id1,id2,r1',r2')
+	  AList (id1,id2,r1',r2',b)
 
   | ALambda (n,r1,r2) -> 
       let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
@@ -223,9 +223,9 @@ let discriminate_patterns nl l1 l2 =
   let diff = ref None in
   let rec aux n c1 c2 = match c1,c2 with
   | RVar (_,v1), RVar (_,v2) when v1<>v2 ->
-      if !diff = None then (diff := Some (v1,v2,(n<nl)); true)
+      if !diff = None then (diff := Some (v1,v2,(n>=nl)); true)
       else 
-        !diff = Some (v1,v2,(n<nl)) or !diff = Some (v2,v1,(n>=nl))
+        !diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n<nl))
         or (error
           "Both ends of the recursive pattern differ in more than one place")
   | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
@@ -292,17 +292,17 @@ allowed in abbreviatable expressions"
         then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
         found := id::!found) [x;y];
       let iter =
-        if order then RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1)
-        else RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2) in
-      (if order then x else y), ldots_var, aux iter, aux t
+        if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
+        else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
+      (if order then y else x), ldots_var, aux iter, aux t, order
   | _ -> error "One end of the recursive pattern is not an application"
     
   and make_aconstr_list f args =
     let rec find_patterns acc = function
       | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
           (* We've found the recursive part *)
-	  let x,y,iter,terminator = terminator_of_pat f (List.rev acc) l c in
-	  AList (x,y,iter,terminator)
+	  let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
+	  AList (x,y,iter,term,lassoc)
       | a::l -> find_patterns (a::acc) l
       | [] -> error "Ill-formed recursive notation"
     in find_patterns [] args
@@ -355,9 +355,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
   | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
       List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
-  | RApp (_,f1,l1), AList (x,y,(AApp (f2,l2) as iter),termin) 
+  | RApp (_,f1,l1), AList (x,y,(AApp (f2,l2) as iter),termin,lassoc) 
       when List.length l1 = List.length l2 ->
-      match_alist alp metas sigma (f1::l1) (f2::l2) x y iter termin
+      match_alist alp metas sigma (f1::l1) (f2::l2) x y iter termin lassoc
   | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
      match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
   | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
@@ -383,7 +383,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | (RDynamic _ | RRec _ | REvar _), _ 
   | _,_ -> raise No_match
 
-and match_alist alp metas sigma l1 l2 x y iter termin =
+and match_alist alp metas sigma l1 l2 x y iter termin lassoc =
   (* match the iterator at least once *)
   let sigma = List.fold_left2 (match_ alp (y::metas)) sigma l1 l2 in
   (* Recover the recursive position *)
@@ -402,7 +402,7 @@ and match_alist alp metas sigma l1 l2 x y iter termin =
     with No_match ->
       List.rev acc, match_ alp metas sigma rest termin in
   let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
-  (x,encode_list_value tl)::sigma
+  (x,encode_list_value (if lassoc then List.rev tl else tl))::sigma
 
 and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
   | (Name id1,Name id2) when List.mem id2 metas ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1fe1f95cd..8803cb959 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -27,7 +27,7 @@ type aconstr =
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
-  | AList of identifier * identifier * aconstr * aconstr
+  | AList of identifier * identifier * aconstr * aconstr * bool
   (* Part only in rawconstr *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr