Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 46 insertions, 37 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index efb6c853..f99af68e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 (*i*)
 open Pp
@@ -190,8 +190,9 @@ let rec check_same_type ty1 ty2 =
       check_same_type b1 b2
   | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
       check_same_type a1 a2
-  | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
-      List.iter2 check_same_type e1 e2
+  | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+      List.iter2 check_same_type e1 e2;
+      List.iter2 (List.iter2 check_same_type) el1 el2
   | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
   | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
       check_same_type e1 e2
@@ -298,7 +299,7 @@ and spaces ntn n =
   if n = String.length ntn then []
   else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
 
-let expand_curly_brackets loc mknot ntn l =
+let expand_curly_brackets loc mknot ntn (l,ll) =
   let ntn' = ref ntn in
   let rec expand_ntn i =
     function
@@ -311,12 +312,12 @@ let expand_curly_brackets loc mknot ntn l =
             ntn' := 
               String.sub !ntn' 0 p ^ "_" ^ 
               String.sub !ntn' (p+5) (String.length !ntn' -p-5);
-            mknot (loc,"{ _ }",[a]) end
+            mknot (loc,"{ _ }",([a],[])) end
           else a in
         a' :: expand_ntn (i+1) l in
   let l = expand_ntn 0 l in
   (* side effect *)
-  mknot (loc,!ntn',l)
+  mknot (loc,!ntn',(l,ll))
 
 let destPrim = function CPrim(_,t) -> Some t | _ -> None
 let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -324,18 +325,18 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
   then expand_curly_brackets loc mknot ntn l
-  else match ntn,List.map destprim l with
+  else match ntn,List.map destprim (fst l),(snd l) with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
-    | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
-        mknot (loc,ntn,[mknot (loc,"( _ )",l)])
+    | "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
+        mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
     | _ -> 
 	match decompose_notation_key ntn, l with
-	| [Terminal "-"; Terminal x], [] ->
+	| [Terminal "-"; Terminal x], ([],[]) ->
 	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
- 	     with _ -> mknot (loc,ntn,[]))
-	| [Terminal x], [] ->
+ 	     with _ -> mknot (loc,ntn,([],[])))
+	| [Terminal x], ([],[]) ->
 	    (try mkprim (loc, Numeral (Bigint.of_string x))
- 	     with _ -> mknot (loc,ntn,[]))
+ 	     with _ -> mknot (loc,ntn,([],[])))
 	| _ ->
 	    mknot (loc,ntn,l)
 
@@ -351,13 +352,13 @@ let make_pat_notation loc ntn l =
     (fun (loc,p) -> CPatPrim (loc,p))
     destPatPrim l
 
-let bind_env sigma var v =
+let bind_env (sigma,sigmalist as fullsigma) var v =
   try
     let vvar = List.assoc var sigma in
-    if v=vvar then sigma else raise No_match
+    if v=vvar then fullsigma else raise No_match
   with Not_found ->
     (* TODO: handle the case of multiple occs in different scopes *)
-    (var,v)::sigma
+    (var,v)::sigma,sigmalist
 
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
@@ -378,15 +379,18 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
         (* All parameters must be _ *)
         List.iter (function AHole _ -> () | _ -> raise No_match) p2;
 	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+  (* TODO: use recursive notations *)
   | _ -> raise No_match
 
-let match_aconstr_cases_pattern c (metas_scl,pat) =
-  let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in
+let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
+  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+  let subst,substlist = match_cases_pattern vars ([],[]) c pat in
   (* Reorder canonically the substitution *)
   let find x subst =
-    try List.assoc x subst
+    try List.assoc x subst 
     with Not_found -> anomaly "match_aconstr_cases_pattern" in
-  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
+  List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
 
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -424,7 +428,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	  | PatCstr (loc,_,_,na),_ -> loc,na
 	  | PatVar (loc,na),_ -> loc,na in
 	(* Try matching ... *)
-	let subst = match_aconstr_cases_pattern t pat in
+	let subst,substlist = match_aconstr_cases_pattern t pat in
 	(* Try availability of interpretation ... *)
 	let p = match keyrule with
           | NotationRule (sc,ntn) ->
@@ -438,7 +442,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
                       subst in
-		  insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
+		  let ll =
+		    List.map (fun (c,(scopt,scl)) ->
+		      let subscope = (scopt,scl@scopes') in
+		      List.map (extern_cases_pattern_in_scope subscope vars) c)
+                      substlist in
+		  insert_pat_delimiters loc 
+		    (make_pat_notation loc ntn (l,ll)) key)
           | SynDefRule kn ->
 	      let qid = shortest_qualid_of_syndef vars kn in
               CPatAtom (loc,Some (Qualid (loc, qid))) in
@@ -544,15 +554,10 @@ let rec remove_coercions inctx = function
 	      (* We skip a coercion *) 
 	      let l = list_skipn n args in
 	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
-	      let (a,l) =
-                (* Recursively remove the head coercions *)
-                match remove_coercions true a with
-                  | RApp (_,a,l') -> a,l'@l
-                  | a -> a,l in
-              if l = [] then a
-              else
-                (* Recursively remove coercions in arguments *)
-                RApp (loc,a,List.map (remove_coercions true) l)
+              (* Recursively remove the head coercions *)
+              (match remove_coercions true a with
+              | RApp (_,a,l') -> RApp (loc,a,l'@l)
+              | a -> RApp (loc,a,l))
 	  | _ -> c
       with Not_found -> c)
   | c -> c
@@ -671,7 +676,7 @@ let rec extern inctx scopes vars r =
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
-
+	
   | RCases (loc,sty,rtntypopt,tml,eqns) ->
       let vars' = 
 	List.fold_right (name_fold Idset.add)
@@ -694,7 +699,7 @@ let rec extern inctx scopes vars r =
 	    | Name id -> RVar (dummy_loc,id)) nal in
 	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
-      let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in 
+      let eqns = List.map (extern_eqn inctx scopes vars) eqns in 
       CCases (loc,sty,rtntypopt',tml,eqns)
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
@@ -702,13 +707,13 @@ let rec extern inctx scopes vars r =
         (Option.map (fun _ -> na) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
-        extern false scopes (List.fold_left add_vname vars nal) b)
+        extern inctx scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
         (Option.map (fun _ -> na) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
-        sub_extern false scopes vars b1, sub_extern false scopes vars b2)
+        sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
   | RRec (loc,fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Idset.add idv vars in
@@ -822,7 +827,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
           | _, None -> t,[]
           | _ -> raise No_match in
 	(* Try matching ... *)
-	let subst = match_aconstr t pat in
+	let subst,substlist = match_aconstr t pat in
 	(* Try availability of interpretation ... *)
         let e =
           match keyrule with
@@ -838,7 +843,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 		      extern (* assuming no overloading: *) true
 		        (scopt,scl@scopes') vars c)
                       subst in
-	          insert_delimiters (make_notation loc ntn l) key)
+		  let ll =
+		    List.map (fun (c,(scopt,scl)) ->
+		      List.map (extern true (scopt,scl@scopes') vars) c)
+                      substlist in
+	          insert_delimiters (make_notation loc ntn (l,ll)) key)
           | SynDefRule kn ->
 	      let l =
 		List.map (fun (c,(scopt,scl)) ->