aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml7
-rw-r--r--interp/constrextern.ml28
-rw-r--r--interp/constrintern.ml50
-rw-r--r--interp/constrintern.mli18
-rw-r--r--interp/dumpglob.ml5
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/notation.ml7
-rw-r--r--interp/syntax_def.ml9
8 files changed, 79 insertions, 47 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d4369e9bd1..d6097304ec 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -121,9 +121,10 @@ let rec constr_expr_eq e1 e2 =
constr_expr_eq a1 a2 &&
Option.equal constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
- | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
+ | CAppExpl((proj1,r1,u1),al1), CAppExpl((proj2,r2,u2),al2) ->
Option.equal Int.equal proj1 proj2 &&
qualid_eq r1 r2 &&
+ eq_universes u1 u2 &&
List.equal constr_expr_eq al1 al2
| CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
Option.equal Int.equal proj1 proj2 &&
@@ -158,8 +159,8 @@ let rec constr_expr_eq e1 e2 =
Id.equal id1 id2 && List.equal instance_eq c1 c2
| CSort s1, CSort s2 ->
Glob_ops.glob_sort_eq s1 s2
- | CCast(t1,c1), CCast(t2,c2) ->
- constr_expr_eq t1 t2 && cast_expr_eq c1 c2
+ | CCast(t1,c1), CCast(t2,c2) ->
+ constr_expr_eq t1 t2 && cast_expr_eq c1 c2
| CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
notation_eq n1 n2 &&
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7a14ca3e48..a37bac3275 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -282,9 +282,9 @@ let insert_pat_alias ?loc p = function
| Anonymous -> p
| Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
-let rec insert_coercion ?loc l c = match l with
+let rec insert_entry_coercion ?loc l c = match l with
| [] -> c
- | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[]))
+ | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_entry_coercion ?loc l c],[],[],[]))
let rec insert_pat_coercion ?loc l c = match l with
| [] -> c
@@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
with No_match ->
let loc = pat.CAst.loc in
match DAst.get pat with
- | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+ | PatVar (Name id) when entry_has_global custom || entry_has_ident custom ->
+ CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
| pat ->
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
@@ -615,6 +616,10 @@ let is_projection nargs r =
let is_hole = function CHole _ | CEvar _ -> true | _ -> false
+let isCRef_no_univ = function
+ | CRef (_,None) -> true
+ | _ -> false
+
let is_significant_implicit a =
not (is_hole (a.CAst.v))
@@ -849,7 +854,7 @@ let extern_possible_prim_token (custom,scopes) r =
| Some coercion ->
match availability_of_prim_token n sc scopes with
| None -> raise No_match
- | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+ | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
let filter_enough_applied nargs l =
match nargs with
@@ -931,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r =
match DAst.get r with
| GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
- | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+ | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) ->
+ CAst.make ?loc (extern_var ?loc id)
| c ->
@@ -1081,7 +1087,7 @@ let rec extern inctx ?impargs scopes vars r =
| GFloat f -> extern_float f (snd scopes)
- in insert_coercion coercion (CAst.make ?loc c)
+ in insert_entry_coercion coercion (CAst.make ?loc c)
and extern_typ ?impargs (subentry,(_,scopes)) =
extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes))
@@ -1279,14 +1285,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
binderlists in
let c = make_notation loc specific_ntn (l,ll,bl,bll) in
- let c = insert_coercion coercion (insert_delimiters c key) in
+ let c = insert_entry_coercion coercion (insert_delimiters c key) in
let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
| 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)
@@ -1296,7 +1299,10 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
- insert_coercion coercion c
+ if isCRef_no_univ c.CAst.v && entry_has_global custom then c
+ else match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion -> insert_entry_coercion coercion c
with
No_match -> extern_notation allscopes vars t rules
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 905d9f1e5b..b72802d911 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -53,6 +53,12 @@ type var_internalization_type =
| Method
| Variable
+type var_unique_id = string
+
+let var_uid =
+ let count = ref 0 in
+ fun id -> incr count; Id.to_string id ^ ":" ^ string_of_int !count
+
type var_internalization_data =
(* type of the "free" variable, for coqdoc, e.g. while typing the
constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
@@ -60,7 +66,9 @@ type var_internalization_data =
(* signature of impargs of the variable *)
Impargs.implicit_status list *
(* subscopes of the args of the variable *)
- scope_name option list
+ scope_name option list *
+ (* unique ID for coqdoc links *)
+ var_unique_id
type internalization_env =
(var_internalization_data) Id.Map.t
@@ -177,15 +185,18 @@ let parsing_explicit = ref false
let empty_internalization_env = Id.Map.empty
-let compute_internalization_data env sigma ty typ impl =
+let compute_internalization_data env sigma id ty typ impl =
let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
- (ty, impl, compute_arguments_scope sigma typ)
+ (ty, impl, compute_arguments_scope sigma typ, var_uid id)
let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
List.fold_left3
- (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map)
+ (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma id ty typ impl) map)
impls
+let extend_internalization_data (r, impls, scopes, uid) impl scope =
+ (r, impls@[impl], scopes@[scope], uid)
+
(**********************************************************************)
(* Contracting "{ _ }" in notations *)
@@ -341,7 +352,7 @@ let impls_binder_list =
let impls_type_list n ?(args = []) =
let rec aux acc n c = match DAst.get c with
| GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
- | _ -> (Variable,List.rev acc,[])
+ | _ -> List.rev acc
in aux args n
let impls_term_list n ?(args = []) =
@@ -351,7 +362,7 @@ let impls_term_list n ?(args = []) =
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
aux acc' n bds.(nb)
- |_ -> (Variable,List.rev acc,[])
+ |_ -> List.rev acc
in aux args n
(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
@@ -431,8 +442,9 @@ let push_name_env ntnvars implargs env =
if Id.Map.is_empty ntnvars && Id.equal id ldots_var
then error_ldots_var ?loc;
set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
- Dumpglob.dump_binding ?loc id;
- pure_push_name_env (id,implargs) env
+ let uid = var_uid id in
+ Dumpglob.dump_binding ?loc uid;
+ pure_push_name_env (id,(Variable,implargs,[],uid)) env
let remember_binders_impargs env bl =
List.map_filter (fun (na,_,_,_) ->
@@ -463,7 +475,7 @@ let intern_generalized_binder intern_type ntnvars
let ty' = intern_type {env with ids = ids; unb = true} ty in
let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
let env' = List.fold_left
- (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[])(*?*) env (make ?loc @@ Name x))
+ (fun env {loc;v=x} -> push_name_env ntnvars [](*?*) env (make ?loc @@ Name x))
env fvs in
let b' = check_implicit_meaningful ?loc b' env in
let bl = List.map
@@ -530,7 +542,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
user_err ?loc (str "Unsupported nested \"as\" clause.");
il,disjpat
in
- let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[]) env (make ?loc @@ Name id)) il env in
+ let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
let na = alias_of_pat (List.hd disjpat) in
let ienv = Name.fold_right Id.Set.remove na env.ids in
let id = Namegen.next_name_away_with_default "pat" na ienv in
@@ -586,7 +598,7 @@ let intern_generalization intern env ntnvars loc bk ak c =
GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
in
List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
- let env' = push_name_env ntnvars (Variable,[],[]) env CAst.(make @@ Name id) in
+ let env' = push_name_env ntnvars [] env CAst.(make @@ Name id) in
(env', abs lid acc)) fvs (env,c)
in c'
@@ -677,7 +689,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
if onlyident then
(* Do not try to interpret a variable as a constructor *)
let na = out_patvar pat in
- let env = push_name_env ntnvars (Variable,[],[]) env (make ?loc:pat.loc na) in
+ let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in
(renaming,env), None, na
else
(* Interpret as a pattern *)
@@ -989,7 +1001,7 @@ let string_of_ty = function
| Variable -> "var"
let gvar (loc, id) us = match us with
-| None -> DAst.make ?loc @@ GVar id
+| None | Some [] -> DAst.make ?loc @@ GVar id
| Some _ ->
user_err ?loc (str "Variable " ++ Id.print id ++
str " cannot have a universe instance")
@@ -1004,9 +1016,9 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
else
(* Is [id] registered with implicit arguments *)
try
- let ty,impls,argsc = Id.Map.find id env.impls in
+ let ty,impls,argsc,uid = Id.Map.find id env.impls in
let tys = string_of_ty ty in
- Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
+ Dumpglob.dump_reference ?loc "<>" uid tys;
gvar (loc,id) us, make_implicits_list impls, argsc
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
@@ -2084,7 +2096,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
List.rev_append match_td matchs)
tms ([],Id.Set.empty,Id.Map.empty,[]) in
let env' = Id.Set.fold
- (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var))
+ (fun var bli -> push_name_env ntnvars [] bli (CAst.make @@ Name var))
(Id.Set.union ex_ids as_in_vars)
(restart_lambda_binders env)
in
@@ -2122,17 +2134,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* "in" is None so no match to add *)
let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
- let env'' = push_name_env ntnvars (Variable,[],[]) env'
+ let env'' = push_name_env ntnvars [] env'
(CAst.make na') in
intern_type (slide_binders env'') u) po in
DAst.make ?loc @@
GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
- intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) env nal) c)
+ intern (List.fold_left (push_name_env ntnvars []) env nal) c)
| CIf (c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
- let env'' = push_name_env ntnvars (Variable,[],[]) env
+ let env'' = push_name_env ntnvars [] env
(CAst.make na') in
intern_type (slide_binders env'') p) po in
DAst.make ?loc @@
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9f06f16258..2eb96aad56 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -43,26 +43,28 @@ type var_internalization_type =
| Method
| Variable
-type var_internalization_data =
- var_internalization_type *
- (* type of the "free" variable, for coqdoc, e.g. while typing the
- constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
-
- Impargs.implicit_status list * (* signature of impargs of the variable *)
- Notation_term.scope_name option list (* subscopes of the args of the variable *)
+(** This collects relevant information for interning local variables:
+ - their coqdoc kind (a recursive call in a inductive, fixpoint of class; or a bound variable)
+ e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive
+ - their implicit arguments
+ - their argument scopes *)
+type var_internalization_data
(** A map of free variables to their implicit arguments and scopes *)
type internalization_env = var_internalization_data Id.Map.t
val empty_internalization_env : internalization_env
-val compute_internalization_data : env -> evar_map -> var_internalization_type ->
+val compute_internalization_data : env -> evar_map -> Id.t -> var_internalization_type ->
types -> Impargs.manual_implicits -> var_internalization_data
val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type ->
Id.t list -> types list -> Impargs.manual_implicits list ->
internalization_env
+val extend_internalization_data :
+ var_internalization_data -> Impargs.implicit_status -> scope_name option -> var_internalization_data
+
type ltac_sign = {
ltac_vars : Id.Set.t;
(** Variables of Ltac which may be bound to a term *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index e659a5ac5c..57ec708b07 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -246,8 +246,6 @@ let add_glob_kn ?loc kn =
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
add_glob_gen ?loc sp lib_dp "syndef"
-let dump_binding ?loc id = ()
-
let dump_def ?loc ty secpath id = Option.iter (fun loc ->
if !glob_output = Feedback then
Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty))
@@ -275,3 +273,6 @@ let dump_notation (loc,(df,_)) sc sec = Option.iter (fun loc ->
let location = (Loc.make_loc (i, i+1)) in
dump_def ~loc:location "not" (Names.DirPath.to_string (Lib.current_dirpath sec)) (cook_notation df sc)
) loc
+
+let dump_binding ?loc uid =
+ dump_def ?loc "binder" "<>" uid
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 5409b20472..14e5a81308 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -36,7 +36,7 @@ val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit
val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
val dump_notation_location : (int * int) list -> Constrexpr.notation ->
(Notation.notation_location * Notation_term.scope_name option) -> unit
-val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
+val dump_binding : ?loc:Loc.t -> string -> unit
val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
diff --git a/interp/notation.ml b/interp/notation.ml
index 6291a88bb0..0afbb9cd62 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -206,7 +206,7 @@ let classify_scope (local,_,_ as o) =
let inScope : bool * bool * scope_item -> obj =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
- open_function = open_scope;
+ open_function = simple_open open_scope;
subst_function = subst_scope;
discharge_function = discharge_scope;
classify_function = classify_scope }
@@ -980,9 +980,12 @@ let subst_prim_token_interpretation (subs,infos) =
let classify_prim_token_interpretation infos =
if infos.pt_local then Dispose else Substitute infos
+let open_prim_token_interpretation i o =
+ if Int.equal i 1 then cache_prim_token_interpretation o
+
let inPrimTokenInterp : prim_token_infos -> obj =
declare_object {(default_object "PRIM-TOKEN-INTERP") with
- open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
+ open_function = simple_open open_prim_token_interpretation;
cache_function = cache_prim_token_interpretation;
subst_function = subst_prim_token_interpretation;
classify_function = classify_prim_token_interpretation}
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 767c69e3b6..7184f5ea29 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -67,11 +67,18 @@ let subst_syntax_constant (subst,(local,syndef)) =
let classify_syntax_constant (local,_ as o) =
if local then Dispose else Substitute o
+let filtered_open_syntax_constant f i ((_,kn),_ as o) =
+ let in_f = match f with
+ | Unfiltered -> true
+ | Names ns -> Globnames.(ExtRefSet.mem (SynDef kn) ns)
+ in
+ if in_f then open_syntax_constant i o
+
let in_syntax_constant : (bool * syndef) -> obj =
declare_object {(default_object "SYNDEF") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
- open_function = open_syntax_constant;
+ open_function = filtered_open_syntax_constant;
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 09:35:38 +0000