aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml47
-rw-r--r--interp/constrintern.ml45
-rw-r--r--interp/notation.ml29
-rw-r--r--interp/notation.mli15
-rw-r--r--interp/topconstr.ml6
-rw-r--r--interp/topconstr.mli9
6 files changed, 93 insertions, 58 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 44f4baee60..8c81e066ad 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -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
@@ -363,6 +360,9 @@ let make_pat_notation loc ntn l =
(fun (loc,p) -> CPatPrim (loc,p))
destPatPrim l
+let find_arguments_scope ref =
+ List.map (option_map (fun sc -> LightTmpScope sc)) (find_arguments_scope ref)
+
let bind_env sigma var v =
try
let vvar = List.assoc var sigma in
@@ -401,11 +401,11 @@ 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
@@ -440,17 +440,17 @@ 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' =
+ if (* recursive *) false then option_cons scopt scopes
+ else 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 +460,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 +607,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,7 +754,8 @@ 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 (LightTmpScope (Notation.type_scope)),scopes)
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
@@ -817,17 +818,18 @@ 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' =
+ if (* recursive *) false then option_cons scopt scopes
+ else 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 +849,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,10 +863,10 @@ 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
+ extern_constr_gen at_top (Some (ExplicitTmpScope scope)) env t
let extern_constr at_top env t =
extern_constr_gen at_top None env t
@@ -962,5 +964,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)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index bdd9fa32da..95fcf0d9a8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -221,7 +221,18 @@ let contract_pat_notation ntn l =
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
-let make_current_scope (scopt,scopes) = option_cons scopt scopes
+let make_light_tmp_scope = function
+ | Some sc -> Some (LightTmpScope sc)
+ | None -> None
+
+let make_current_scope (tmp_scope,scopes) =
+ let scopes = if (* recursive *) false then scopes else [] in
+ match tmp_scope with
+ | Some (ExplicitTmpScope sc) -> sc :: scopes
+ | _ -> scopes
+
+let find_arguments_scope ref =
+ List.map make_light_tmp_scope (find_arguments_scope ref)
let set_var_scope loc id (_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
@@ -231,7 +242,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
user_err_loc (loc,"set_var_scope",
pr_id id ++ str " already occurs in a different scope")
else
- idscopes := Some (scopt,scopes)
+ idscopes := Some (scopt,if (* recursive *) false then scopes else [])
(**********************************************************************)
(* Discriminating between bound variables and global references *)
@@ -247,7 +258,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
let l,impl,argsc = List.assoc id impls in
let l = List.map
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
- RVar (loc,id), impl, argsc, l
+ RVar (loc,id), impl, List.map make_light_tmp_scope argsc, l
with Not_found ->
(* Is [id] bound in current env or is an ltac var bound to constr *)
if Idset.mem id env or List.mem id vars1
@@ -558,21 +569,20 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
intern_cases_pattern genv scopes aliases tmp_scope a
| CPatNotation (loc, ntn, args) ->
let ntn,args = contract_pat_notation ntn args in
- let scopes = option_cons tmp_scope scopes in
- let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+ let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
if !dump then dump_notation_location (patntn_loc loc args ntn) df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes
c
| CPatPrim (loc, p) ->
- let scopes = option_cons tmp_scope scopes in
let a = alias_of aliases in
- let (c,df) = Notation.interp_prim_token_cases_pattern loc p a scopes in
+ let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
+ (tmp_scope,scopes) in
if !dump then dump_notation_location (fst (unloc loc)) df;
(ids,[subst,c])
| CPatDelimiters (loc, key, e) ->
- intern_cases_pattern genv (find_delimiters_scope loc key::scopes)
- aliases None e
+ intern_cases_pattern genv scopes aliases
+ (Some (ExplicitTmpScope (find_delimiters_scope loc key))) e
| CPatAtom (loc, Some head) ->
(match maybe_constructor head with
| ConstrPat (c,args) ->
@@ -747,14 +757,13 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) =
let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
let ntn,args = contract_notation ntn args in
- let scopes = option_cons tmp_scope scopes in
- let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+ let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
if !dump then dump_notation_location (ntn_loc loc args ntn) df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
subst_aconstr_in_rawconstr loc intern subst env c
let set_type_scope (ids,tmp_scope,scopes) =
- (ids,Some Notation.type_scope,scopes)
+ (ids,Some (LightTmpScope Notation.type_scope),scopes)
let reset_tmp_scope (ids,tmp_scope,scopes) =
(ids,None,scopes)
@@ -849,12 +858,12 @@ let internalise sigma globalenv env allow_soapp lvar c =
| CNotation (loc,ntn,args) ->
intern_notation intern env loc ntn args
| CPrim (loc, p) ->
- let scopes = option_cons tmp_scope scopes in
- let c,df = Notation.interp_prim_token loc p scopes in
+ let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
if !dump then dump_notation_location (fst (unloc loc)) df;
c
| CDelimiters (loc, key, e) ->
- intern (ids,None,find_delimiters_scope loc key::scopes) e
+ let tmp_scope = ExplicitTmpScope (find_delimiters_scope loc key) in
+ intern (ids,Some tmp_scope,scopes) e
| CAppExpl (loc, (isproj,ref), args) ->
let (f,_,args_scopes,_) = intern_reference env lvar ref in
check_projection isproj (List.length args) f;
@@ -918,8 +927,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
| CDynamic (loc,d) -> RDynamic (loc,d)
- and intern_type (ids,_,scopes) =
- intern (ids,Some Notation.type_scope,scopes)
+ and intern_type env = intern (set_type_scope env)
and intern_local_binder ((ids,ts,sc as env),bl) = function
| LocalRawAssum(nal,ty) ->
@@ -1068,7 +1076,8 @@ let extract_ids env =
let intern_gen isarity sigma env
?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
c =
- let tmp_scope = if isarity then Some Notation.type_scope else None in
+ let tmp_scope =
+ if isarity then Some (LightTmpScope Notation.type_scope) else None in
internalise sigma env (extract_ids env, tmp_scope,[])
allow_soapp (ltacvars,Environ.named_context env, [], impls) c
diff --git a/interp/notation.ml b/interp/notation.ml
index 00aa7fb6c7..0e6f02c52c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -130,6 +130,17 @@ let push_scope sc scopes = Scope sc :: scopes
let push_scopes = List.fold_right push_scope
+type local_scopes = tmp_scope_name option * scope_name list
+
+let make_current_scopes (tmp_scope,scopes) =
+ match tmp_scope with
+ | Some (ExplicitTmpScope sc) ->
+ if (* recursive *) false
+ then push_scope sc (push_scopes scopes !scope_stack)
+ else [Scope sc]
+ | Some (LightTmpScope sc) -> push_scope sc (push_scopes scopes !scope_stack)
+ | None -> push_scopes scopes !scope_stack
+
(**********************************************************************)
(* Delimiters *)
@@ -146,7 +157,7 @@ let declare_delimiters scope key =
scope_map := Gmap.add scope sc !scope_map;
if Gmap.mem key !delimiters_map then begin
let oldsc = Gmap.find key !delimiters_map in
- Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+ Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
end;
delimiters_map := Gmap.add key scope !delimiters_map
@@ -336,9 +347,9 @@ let find_prim_token g loc p sc =
check_required_module loc sc spdir;
g (interp ()), (dirpath (fst spdir),"")
-let interp_prim_token_gen g loc p scopes =
- let all_scopes = push_scopes scopes !scope_stack in
- try find_interpretation (find_prim_token g loc p) all_scopes
+let interp_prim_token_gen g loc p local_scopes =
+ let scopes = make_current_scopes local_scopes in
+ try find_interpretation (find_prim_token g loc p) scopes
with Not_found ->
user_err_loc (loc,"interp_prim_token",
(match p with
@@ -351,8 +362,9 @@ let interp_prim_token =
let interp_prim_token_cases_pattern loc p name =
interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p
-let rec interp_notation loc ntn scopes =
- try find_interpretation (find_notation ntn) (push_scopes scopes !scope_stack)
+let rec interp_notation loc ntn local_scopes =
+ let scopes = make_current_scopes local_scopes in
+ try find_interpretation (find_notation ntn) scopes
with Not_found ->
user_err_loc
(loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
@@ -366,7 +378,7 @@ let uninterp_cases_pattern_notations c =
let availability_of_notation (ntn_scope,ntn) scopes =
let f scope =
Gmap.mem ntn (Gmap.find scope !scope_map).notations in
- find_without_delimiters f (ntn_scope,Some ntn) scopes
+ find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
let uninterp_prim_token c =
try
@@ -387,8 +399,9 @@ let uninterp_prim_token_cases_pattern c =
| Some n -> (na,sc,n)
with Not_found -> raise No_match
-let availability_of_prim_token printer_scope scopes =
+let availability_of_prim_token printer_scope local_scopes =
let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+ let scopes = make_current_scopes local_scopes in
option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
(* Miscellaneous *)
diff --git a/interp/notation.mli b/interp/notation.mli
index d4c36d9e74..9822905c20 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -32,12 +32,15 @@ type delimiters = string
type scope
type scopes (* = [scope_name list] *)
+type local_scopes = tmp_scope_name option * scope_name list
+
val type_scope : scope_name
val declare_scope : scope_name -> unit
+val current_scopes : unit -> scopes
+
(* Open scope *)
-val current_scopes : unit -> scopes
val open_close_scope :
(* locality *) bool * (* open *) bool * scope_name -> unit
@@ -76,10 +79,10 @@ val declare_string_interpreter : scope_name -> required_module ->
(* Return the [term]/[cases_pattern] bound to a primitive token in a
given scope context*)
-val interp_prim_token : loc -> prim_token -> scope_name list ->
+val interp_prim_token : loc -> prim_token -> local_scopes ->
rawconstr * (notation_location * scope_name option)
val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
- scope_name list -> cases_pattern * (notation_location * scope_name option)
+ local_scopes -> cases_pattern * (notation_location * scope_name option)
(* Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
@@ -90,7 +93,7 @@ val uninterp_prim_token_cases_pattern :
cases_pattern -> name * scope_name * prim_token
val availability_of_prim_token :
- scope_name -> scopes -> delimiters option option
+ scope_name -> local_scopes -> delimiters option option
(*s Declare and interpret back and forth a notation *)
@@ -105,7 +108,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
val declare_uninterpretation : interp_rule -> interpretation -> unit
(* Return the interpretation bound to a notation *)
-val interp_notation : loc -> notation -> scope_name list ->
+val interp_notation : loc -> notation -> local_scopes ->
interpretation * (notation_location * scope_name option)
(* Return the possible notations for a given term *)
@@ -117,7 +120,7 @@ val uninterp_cases_pattern_notations : cases_pattern ->
(* Test if a notation is available in the scopes *)
(* context [scopes]; if available, the result is not None; the first *)
(* argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> scopes ->
+val availability_of_notation : scope_name option * notation -> local_scopes ->
(scope_name option * delimiters option) option
(*s Declare and test the level of a (possibly uninterpreted) notation *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c613bf0dbe..c9ae593afd 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -480,8 +480,12 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (_,patl2,rhs2) =
type scope_name = string
+type tmp_scope_name =
+ | LightTmpScope of scope_name
+ | ExplicitTmpScope of scope_name
+
type interpretation =
- (identifier * (scope_name option * scope_name list)) list * aconstr
+ (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
let match_aconstr c (metas_scl,pat) =
let subst = match_ [] (List.map fst metas_scl) [] c pat in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index e1d35bb274..0d428e8fa3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -60,11 +60,16 @@ val eq_rawconstr : rawconstr -> rawconstr -> bool
exception No_match
type scope_name = string
+
+type tmp_scope_name =
+ | LightTmpScope of scope_name
+ | ExplicitTmpScope of scope_name
+
type interpretation =
- (identifier * (scope_name option * scope_name list)) list * aconstr
+ (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
val match_aconstr : rawconstr -> interpretation ->
- (rawconstr * (scope_name option * scope_name list)) list
+ (rawconstr * (tmp_scope_name option * scope_name list)) list
(*s Concrete syntax for terms *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:44:22 +0000