Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 28 insertions, 26 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 570d113d..ffedcfff 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 8997 2006-07-03 16:40:20Z herbelin $ *)
+(* $Id: constrextern.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -295,9 +295,6 @@ let same_rawconstr c d =
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
-let make_current_scopes (scopt,scopes) = 
-  option_fold_right push_scope scopt scopes
-
 let has_curly_brackets ntn =
   String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
     String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
@@ -401,14 +398,14 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
   List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
 
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
-let rec extern_cases_pattern_in_scope scopes vars pat =
+let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
-    match availability_of_prim_token sc (make_current_scopes scopes) with
+    match availability_of_prim_token sc scopes with
     | None -> raise No_match
     | Some key ->
-      let loc = pattern_loc pat in
+      let loc = cases_pattern_loc pat in
       insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
   try 
@@ -440,17 +437,15 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	(* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (sc,ntn) ->
-	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes = make_current_scopes (scopt, scopes) in
+	          let scopes' = option_cons scopt scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
-		      extern_cases_pattern_in_scope 
-		        (scopt,List.fold_right push_scope scl scopes) vars c)
+		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
                       subst in
 		  insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
           | SynDefRule kn ->
@@ -460,7 +455,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	  No_match -> extern_symbol_pattern allscopes vars t rules
 
 let extern_cases_pattern vars p = 
-  extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p
+  extern_cases_pattern_in_scope (None,[]) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -607,7 +602,7 @@ let rec share_fix_binders n rbl ty def =
 let extern_possible_prim_token scopes r =
   try
     let (sc,n) = uninterp_prim_token r in
-    match availability_of_prim_token sc (make_current_scopes scopes) with
+    match availability_of_prim_token sc scopes with
     | None -> None
     | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
   with No_match ->
@@ -754,11 +749,16 @@ let rec extern inctx scopes vars r =
 
   | RDynamic (loc,d) -> CDynamic (loc,d)
 
-and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes)
+and extern_typ (_,scopes) = 
+  extern true (Some Notation.type_scope,scopes)
 
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
-and factorize_prod scopes vars aty = function
+and factorize_prod scopes vars aty c =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    ([],extern_symbol scopes vars c (uninterp_notations c))
+  with No_match -> match c with
   | RProd (loc,(Name id as na),ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
@@ -766,7 +766,11 @@ and factorize_prod scopes vars aty = function
            ((loc,Name id)::nal,c)
   | c -> ([],extern_typ scopes vars c)
 
-and factorize_lambda inctx scopes vars aty = function
+and factorize_lambda inctx scopes vars aty c =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    ([],extern_symbol scopes vars c (uninterp_notations c))
+  with No_match -> match c with
   | RLambda (loc,na,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
@@ -817,17 +821,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
         let e =
           match keyrule with
           | NotationRule (sc,ntn) ->
-	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes = make_current_scopes (scopt, scopes) in
+	          let scopes' = option_cons scopt scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern (* assuming no overloading: *) true
-		        (scopt,List.fold_right push_scope scl scopes) vars c)
+		        (scopt,scl@scopes') vars c)
                       subst in
 	          insert_delimiters (make_notation loc ntn l) key)
           | SynDefRule kn ->
@@ -847,10 +850,10 @@ and extern_recursion_order scopes vars = function
 
 
 let extern_rawconstr vars c =
-  extern false (None,Notation.current_scopes()) vars c
+  extern false (None,[]) vars c
 
 let extern_rawtype vars c =
-  extern_typ (None,Notation.current_scopes()) vars c
+  extern_typ (None,[]) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -861,7 +864,7 @@ let extern_constr_gen at_top scopt env t =
   let avoid = if at_top then ids_of_context env else [] in
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   let vars = vars_of_env env in
-  extern (not at_top) (scopt,Notation.current_scopes()) vars r
+  extern (not at_top) (scopt,[]) vars r
 
 let extern_constr_in_scope at_top scope env t =
   extern_constr_gen at_top (Some scope) env t
@@ -962,5 +965,4 @@ and raw_of_eqn env constr construct_nargs branch =
   buildrec [] [] env construct_nargs branch
 
 let extern_constr_pattern env pat =
-  extern true (None,Notation.current_scopes()) Idset.empty
-    (raw_of_pat env pat)
+  extern true (None,[]) Idset.empty (raw_of_pat env pat)