diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /interp/constrextern.ml | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r-- | interp/constrextern.ml | 54 |
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) |