aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml10
-rw-r--r--interp/constrintern.ml26
-rw-r--r--interp/constrintern.mli7
-rw-r--r--interp/declare.mli5
-rw-r--r--interp/genintern.ml15
-rw-r--r--interp/genintern.mli9
-rw-r--r--interp/interp.mllib2
-rw-r--r--interp/modintern.ml60
8 files changed, 112 insertions, 22 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 601099c6ff..838ef40545 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -480,6 +480,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(make_pat_notation ?loc ntn (l,ll) l2') key)
end
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in
let l1 =
List.rev_map (fun (c,(subentry,(scopt,scl))) ->
@@ -493,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|None -> raise No_match
in
assert (List.is_empty substlist);
- mkPat ?loc qid (List.rev_append l1 l2')
+ insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
@@ -1131,12 +1134,15 @@ and extern_notation (custom,scopes as allscopes) vars t = function
binderlists in
insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
terms in
let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
- CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
+ insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
if List.is_empty args then e
else
let args = fill_arg_scopes args argsscopes allscopes in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c03a5fee90..02db8f6aab 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -737,7 +737,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
try
let gc = intern nenv c in
- Id.Map.add id (gc, Some c) map
+ Id.Map.add id (gc, None) map
with Nametab.GlobalizationError _ -> map
in
let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
@@ -2051,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (ltacvars, ntnvars) = lvar in
(* Preventively declare notation variables in ltac as non-bindings *)
Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars;
- let ntnvars = Id.Map.domain ntnvars in
let extra = ltacvars.ltac_extra in
+ (* We inform ltac that the interning vars and the notation vars are bound *)
+ (* but we could instead rely on the "intern_sign" *)
let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
- let lvars = Id.Set.union lvars ntnvars in
+ let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
let ltacvars = Id.Set.union lvars env.ids in
+ (* Propagating enough information for mutual interning with tac-in-term *)
+ let intern_sign = {
+ Genintern.intern_ids = env.ids;
+ Genintern.notation_variable_status = ntnvars
+ } in
let ist = {
Genintern.genv = globalenv;
ltacvars;
extra;
+ intern_sign;
} in
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
@@ -2344,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
~pattern_mode:true ~ltacvars env sigma c in
pattern_of_glob_constr c
+let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
+ { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
+ let tmp_scope = scope_of_type_kind sigma kind in
+ let impls = empty_internalization_env in
+ internalize env {ids; unb = false; tmp_scope; scopes = []; impls}
+ pattern_mode (ltacvars, vl) c
+
let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
+ let ids = extract_ids env in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
- let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
- tmp_scope = None; scopes = []; impls = impls}
+ let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls}
false (empty_ltac_sign, vl) a in
+ (* Splits variables into those that are binding, bound, or both *)
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a, reversible = notation_constr_of_glob_constr nenv c in
- (* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
let unused = match reversible with NonInjective ids -> ids | _ -> [] in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index dd0944cc48..147a903fe2 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -185,6 +185,13 @@ val interp_notation_constr : env -> ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes) Id.Map.t * notation_constr * reversibility_status
+(** Idem but to glob_constr (weaker check of binders) *)
+
+val intern_core : typing_constraint ->
+ env -> evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+ Genintern.intern_variable_status -> constr_expr ->
+ glob_constr
+
(** Globalization options *)
val parsing_explicit : bool ref
diff --git a/interp/declare.mli b/interp/declare.mli
index 02e73cd66c..468e056909 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Libnames
open Constr
open Entries
open Decl_kinds
@@ -29,7 +28,7 @@ type section_variable_entry =
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
-val declare_variable : variable -> variable_declaration -> object_name
+val declare_variable : variable -> variable_declaration -> Libobject.object_name
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
@@ -69,7 +68,7 @@ val set_declare_scheme :
(** [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : mutual_inductive_entry -> object_name * bool
+val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
(** Declaration messages *)
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d9a0db040a..1b736b7977 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -14,16 +14,31 @@ open Genarg
module Store = Store.Make ()
+type intern_variable_status = {
+ intern_ids : Id.Set.t;
+ notation_variable_status :
+ (bool ref * Notation_term.subscopes option ref *
+ Notation_term.notation_var_internalization_type)
+ Id.Map.t
+}
+
type glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Store.t;
+ intern_sign : intern_variable_status;
+}
+
+let empty_intern_sign = {
+ intern_ids = Id.Set.empty;
+ notation_variable_status = Id.Map.empty;
}
let empty_glob_sign env = {
ltacvars = Id.Set.empty;
genv = env;
extra = Store.empty;
+ intern_sign = empty_intern_sign;
}
(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
diff --git a/interp/genintern.mli b/interp/genintern.mli
index f4f064bcac..4100f39029 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -14,10 +14,19 @@ open Genarg
module Store : Store.S
+type intern_variable_status = {
+ intern_ids : Id.Set.t;
+ notation_variable_status :
+ (bool ref * Notation_term.subscopes option ref *
+ Notation_term.notation_var_internalization_type)
+ Id.Map.t
+}
+
type glob_sign = {
ltacvars : Id.Set.t;
genv : Environ.env;
extra : Store.t;
+ intern_sign : intern_variable_status;
}
val empty_glob_sign : Environ.env -> glob_sign
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 3668455aeb..aa20bda705 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,8 +3,8 @@ Genredexpr
Redops
Tactypes
Stdarg
-Genintern
Notation_term
+Genintern
Notation_ops
Notation
Syntax_def
diff --git a/interp/modintern.ml b/interp/modintern.ml
index c27cc9cc07..51e27299e3 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,13 +61,52 @@ let lookup_module_or_modtype kind qid =
let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
-let transl_with_decl env = function
+let lookup_polymorphism env base kind fqid =
+ let m = match kind with
+ | Module -> (Environ.lookup_module base env).mod_type
+ | ModType -> (Environ.lookup_modtype base env).mod_type
+ | ModAny -> assert false
+ in
+ let rec defunctor = function
+ | NoFunctor m -> m
+ | MoreFunctor (_,_,m) -> defunctor m
+ in
+ let rec aux m fqid =
+ let open Names in
+ match fqid with
+ | [] -> assert false
+ | [id] ->
+ let test (lab,obj) =
+ match Id.equal (Label.to_id lab) id, obj with
+ | false, _ | _, (SFBmodule _ | SFBmodtype _) -> None
+ | true, SFBmind mind -> Some (Declareops.inductive_is_polymorphic mind)
+ | true, SFBconst const -> Some (Declareops.constant_is_polymorphic const)
+ in
+ (try CList.find_map test m with Not_found -> false (* error later *))
+ | id::rem ->
+ let next = function
+ | MoreFunctor _ -> false (* error later *)
+ | NoFunctor body -> aux body rem
+ in
+ let test (lab,obj) =
+ match Id.equal (Label.to_id lab) id, obj with
+ | false, _ | _, (SFBconst _ | SFBmind _) -> None
+ | true, SFBmodule body -> Some (next body.mod_type)
+ | true, SFBmodtype body -> (* XXX is this valid? If not error later *)
+ Some (next body.mod_type)
+ in
+ (try CList.find_map test m with Not_found -> false (* error later *))
+ in
+ aux (defunctor m) fqid
+
+let transl_with_decl env base kind = function
| CWith_Module ({CAst.v=fqid},qid) ->
WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
| CWith_Definition ({CAst.v=fqid},udecl,c) ->
let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
let c, ectx = interp_constr env sigma c in
- begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
+ let poly = lookup_polymorphism env base kind fqid in
+ begin match UState.check_univ_decl ~poly ectx udecl with
| Entries.Polymorphic_const_entry ctx ->
let inst, ctx = Univ.abstract_universes ctx in
let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
@@ -86,23 +125,24 @@ let loc_of_module l = l.CAst.loc
let rec interp_module_ast env kind m cst = match m with
| {CAst.loc;v=CMident qid} ->
let (mp,kind) = lookup_module_or_modtype kind qid in
- (MEident mp, kind, cst)
+ (MEident mp, mp, kind, cst)
| {CAst.loc;v=CMapply (me1,me2)} ->
- let me1',kind1, cst = interp_module_ast env kind me1 cst in
- let me2',kind2, cst = interp_module_ast env ModAny me2 cst in
+ let me1', base, kind1, cst = interp_module_ast env kind me1 cst in
+ let me2', _, kind2, cst = interp_module_ast env ModAny me2 cst in
let mp2 = match me2' with
| MEident mp -> mp
| _ -> error_application_to_not_path (loc_of_module me2) me2'
in
if kind2 == ModType then
error_application_to_module_type (loc_of_module me2);
- (MEapply (me1',mp2), kind1, cst)
+ (MEapply (me1',mp2), base, kind1, cst)
| {CAst.loc;v=CMwith (me,decl)} ->
- let me,kind,cst = interp_module_ast env kind me cst in
+ let me,base,kind,cst = interp_module_ast env kind me cst in
if kind == Module then error_incorrect_with_in_module m.CAst.loc;
- let decl, cst' = transl_with_decl env decl in
+ let decl, cst' = transl_with_decl env base kind decl in
let cst = Univ.ContextSet.union cst cst' in
- (MEwith(me,decl), kind, cst)
+ (MEwith(me,decl), base, kind, cst)
let interp_module_ast env kind m =
- interp_module_ast env kind m Univ.ContextSet.empty
+ let me, _, kind, cst = interp_module_ast env kind m Univ.ContextSet.empty in
+ me, kind, cst
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:33:04 +0000