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.ml37
-rw-r--r--interp/constrintern.ml169
-rw-r--r--interp/constrintern.mli18
-rw-r--r--interp/dumpglob.ml5
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/notation.ml95
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli2
-rw-r--r--interp/syntax_def.ml9
11 files changed, 197 insertions, 153 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..d5a5bde616 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
@@ -435,13 +435,10 @@ let extern_record_pattern cstrsp args =
let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
- let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+ let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
- match availability_of_prim_token p sc scopes with
- | None -> raise No_match
- | Some key ->
let loc = cases_pattern_loc pat in
insert_pat_coercion ?loc coercion
(insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
@@ -453,7 +450,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 +613,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))
@@ -843,13 +845,11 @@ let same_binder_type ty nal c =
(* one with no delimiter if possible) *)
let extern_possible_prim_token (custom,scopes) r =
- let (sc,n) = uninterp_prim_token r in
+ let (n,key) = uninterp_prim_token r scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| 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)
+ 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 +931,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 +1082,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 +1280,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 +1294,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..f82783f47d 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 *)
@@ -1416,62 +1428,28 @@ let inductive_of_record loc record =
let sort_fields ~complete loc fields completer =
match fields with
| [] -> None
- | (first_field_ref, first_field_value):: other_fields ->
+ | (first_field_ref, _):: _ ->
let (first_field_glob_ref, record) =
try
let gr = locate_reference first_field_ref in
+ Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
(gr, Recordops.find_projection gr)
with Not_found ->
- raise (InternalizationError(loc, NotAProjection first_field_ref))
+ raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
(* the reference constructor of the record *)
- let base_constructor =
- let global_record_id = GlobRef.ConstructRef record.Recordops.s_CONST in
- try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
- with Not_found ->
- anomaly (str "Environment corruption for records.") in
+ let base_constructor = GlobRef.ConstructRef record.Recordops.s_CONST in
let () = check_duplicate ?loc fields in
- let (end_index, (* one past the last field index *)
- first_field_index, (* index of the first field of the record *)
- proj_list) (* list of projections *)
- =
- (* eliminate the first field from the projections,
- but keep its index *)
- let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
- match projs with
- | [] -> (idx, acc_first_idx, acc)
- | (Some field_glob_id) :: projs ->
- let field_glob_ref = GlobRef.ConstRef field_glob_id in
- let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
- begin match proj_kinds with
- | [] -> anomaly (Pp.str "Number of projections mismatch.")
- | { Recordops.pk_true_proj = regular } :: proj_kinds ->
- (* "regular" is false when the field is defined
- by a let-in in the record declaration
- (its value is fixed from other fields). *)
- if first_field && not regular && complete then
- user_err ?loc (str "No local fields allowed in a record construction.")
- else if first_field then
- build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
- else if not regular && complete then
- (* skip non-regular fields *)
- build_proj_list projs proj_kinds idx ~acc_first_idx acc
- else
- build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
- ((idx, field_glob_id) :: acc)
- end
- | None :: projs ->
- if complete then
- (* we don't want anonymous fields *)
- user_err ?loc (str "This record contains anonymous fields.")
- else
- (* anonymous arguments don't appear in proj_kinds *)
- build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
- in
- build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 []
- in
+ let build_proj idx proj kind =
+ if proj = None && complete then
+ (* we don't want anonymous fields *)
+ user_err ?loc (str "This record contains anonymous fields.")
+ else
+ (idx, proj, kind.Recordops.pk_true_proj) in
+ let proj_list =
+ List.map2_i build_proj 1 record.Recordops.s_PROJ record.Recordops.s_PROJKIND in
(* now we want to have all fields assignments indexed by their place in
the constructor *)
let rec index_fields fields remaining_projs acc =
@@ -1479,34 +1457,43 @@ let sort_fields ~complete loc fields completer =
| (field_ref, field_value) :: fields ->
let field_glob_ref = try locate_reference field_ref
with Not_found ->
- user_err ?loc ~hdr:"intern"
+ user_err ?loc:field_ref.CAst.loc ~hdr:"intern"
(str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
- let this_field_record = try Recordops.find_projection field_glob_ref
- with Not_found ->
- let inductive_ref = inductive_of_record loc record in
- raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref)))
- in
- let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) in
+ let remaining_projs, (field_index, _, regular) =
+ let the_proj = function
+ | (idx, Some glob_id, _) -> GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id)
+ | (idx, None, _) -> false in
try CList.extract_first the_proj remaining_projs
with Not_found ->
- let ind1 = inductive_of_record loc record in
- let ind2 = inductive_of_record loc this_field_record in
+ let floc = field_ref.CAst.loc in
+ let this_field_record =
+ try Recordops.find_projection field_glob_ref
+ with Not_found ->
+ let inductive_ref = inductive_of_record floc record in
+ raise (InternalizationError(floc, NotAProjectionOf (field_ref, inductive_ref))) in
+ let ind1 = inductive_of_record floc record in
+ let ind2 = inductive_of_record floc this_field_record in
raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
in
+ if not regular && complete then
+ (* "regular" is false when the field is defined
+ by a let-in in the record declaration
+ (its value is fixed from other fields). *)
+ user_err ?loc (str "No local fields allowed in a record construction.");
+ Dumpglob.add_glob ?loc:field_ref.CAst.loc field_glob_ref;
index_fields fields remaining_projs ((field_index, field_value) :: acc)
| [] ->
- (* the order does not matter as we sort them next,
- List.rev_* is just for efficiency *)
let remaining_fields =
- let complete_field (idx, field_ref) = (idx,
- completer idx field_ref record.Recordops.s_CONST) in
- List.rev_map complete_field remaining_projs in
+ let complete_field (idx, field_ref, regular) =
+ if not regular && complete then
+ (* For terms, we keep only regular fields *)
+ None
+ else
+ Some (idx, completer idx field_ref record.Recordops.s_CONST) in
+ List.map_filter complete_field remaining_projs in
List.rev_append remaining_fields acc
in
- let unsorted_indexed_fields =
- index_fields other_fields proj_list
- [(first_field_index, first_field_value)] in
+ let unsorted_indexed_fields = index_fields fields proj_list [] in
let sorted_indexed_fields =
let cmp_by_index (i, _) (j, _) = Int.compare i j in
List.sort cmp_by_index unsorted_indexed_fields in
@@ -1665,9 +1652,9 @@ let drop_notations_pattern looked_for genv =
if get_asymmetric_patterns () then pl else
let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
List.rev_append pars pl in
- match drop_syndef top scopes head pl with
- | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
- | None -> raise (InternalizationError (loc,NotAConstructor head))
+ let (_,argscs) = find_remaining_scopes [] pl head in
+ let pats = List.map2 (in_pat_sc scopes) argscs pl in
+ DAst.make ?loc @@ RCPatCstr(head, [], pats)
end
| CPatCstr (head, None, pl) ->
begin
@@ -2052,7 +2039,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(fun _idx fieldname constructorname ->
let open Evar_kinds in
let fieldinfo : Evar_kinds.record_field =
- {fieldname=fieldname; recordname=inductive_of_constructor constructorname}
+ {fieldname=Option.get fieldname; recordname=inductive_of_constructor constructorname}
in
CAst.make ?loc @@ CHole (Some
(Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with
@@ -2064,10 +2051,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
match fields with
| None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
| Some (n, constrname, args) ->
+ let args_scopes = find_arguments_scope constrname in
let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in
- let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
- intern env app
- end
+ let args = intern_args env args_scopes (List.rev_append pars args) in
+ let hd = DAst.make @@ GRef (constrname,None) in
+ DAst.make ?loc @@ GApp (hd, args)
+ end
| CCases (sty, rtnpo, tms, eqns) ->
let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
(Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na))
@@ -2084,7 +2073,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 +2111,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..7761606f11 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 }
@@ -932,7 +932,7 @@ let prim_token_interp_infos =
(* Table from global_reference to backtrack-able informations about
prim_token uninterpretation (in particular uninterpreter unique id). *)
let prim_token_uninterp_infos =
- ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t)
+ ref (GlobRef.Map.empty : ((scope_name * (prim_token_interp_info * bool)) list) GlobRef.Map.t)
let hashtbl_check_and_set allow_overwrite uid f h eq =
match Hashtbl.find h uid with
@@ -968,10 +968,13 @@ let cache_prim_token_interpretation (_,infos) =
check_scope ~tolerant:true sc;
prim_token_interp_infos :=
String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
- List.iter (fun r -> prim_token_uninterp_infos :=
- GlobRef.Map.add r (sc,ptii,infos.pt_in_match)
- !prim_token_uninterp_infos)
- infos.pt_refs
+ let add_uninterp r =
+ let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
+ let l = List.remove_assoc_f String.equal sc l in
+ prim_token_uninterp_infos :=
+ GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
+ !prim_token_uninterp_infos in
+ List.iter add_uninterp infos.pt_refs
let subst_prim_token_interpretation (subs,infos) =
{ infos with
@@ -980,9 +983,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}
@@ -1321,27 +1327,6 @@ let entry_has_ident = function
| InCustomEntryLevel (s,n) ->
try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
-let uninterp_prim_token c =
- match glob_prim_constr_key c with
- | None -> raise Notation_ops.No_match
- | Some r ->
- try
- let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
- let uninterp = match info with
- | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
- | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
- | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
- in
- match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
- | None -> raise Notation_ops.No_match
- | Some n -> (sc,n)
- with Not_found -> raise Notation_ops.No_match
-
-let uninterp_prim_token_cases_pattern c =
- match glob_constr_of_closed_cases_pattern (Global.env()) c with
- | exception Not_found -> raise Notation_ops.No_match
- | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
-
let availability_of_prim_token n printer_scope local_scopes =
let f scope =
try
@@ -1363,6 +1348,60 @@ let availability_of_prim_token n printer_scope local_scopes =
let scopes = make_current_scopes local_scopes in
Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
+let rec find_uninterpretation need_delim def find = function
+ | [] ->
+ List.find_map
+ (fun (sc,_,_) -> try Some (find need_delim sc) with Not_found -> None)
+ def
+ | OpenScopeItem scope :: scopes ->
+ (try find need_delim scope
+ with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+ | LonelyNotationItem ntn::scopes ->
+ find_uninterpretation (ntn::need_delim) def find scopes
+
+let uninterp_prim_token c local_scopes =
+ match glob_prim_constr_key c with
+ | None -> raise Notation_ops.No_match
+ | Some r ->
+ let uninterp (sc,(info,_)) =
+ try
+ let uninterp = match info with
+ | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
+ | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+ | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
+ in
+ match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
+ | None -> None
+ | Some n -> Some (sc,n)
+ with Not_found -> None in
+ let add_key (sc,n) =
+ Option.map (fun k -> sc,n,k) (availability_of_prim_token n sc local_scopes) in
+ let l =
+ try GlobRef.Map.find r !prim_token_uninterp_infos
+ with Not_found -> raise Notation_ops.No_match in
+ let l = List.map_filter uninterp l in
+ let l = List.map_filter add_key l in
+ let find need_delim sc =
+ let _,n,k = List.find (fun (sc',_,_) -> String.equal sc' sc) l in
+ if k <> None then n,k else
+ let hidden =
+ List.exists
+ (fun n' -> notation_eq n' (notation_of_prim_token n))
+ need_delim in
+ if not hidden then n,k else
+ match (String.Map.find sc !scope_map).delimiters with
+ | Some k -> n,Some k
+ | None -> raise Not_found
+ in
+ let scopes = make_current_scopes local_scopes in
+ try find_uninterpretation [] l find scopes
+ with Not_found -> match l with (_,n,k)::_ -> n,k | [] -> raise Notation_ops.No_match
+
+let uninterp_prim_token_cases_pattern c local_scopes =
+ match glob_constr_of_closed_cases_pattern (Global.env()) c with
+ | exception Not_found -> raise Notation_ops.No_match
+ | na,c -> let (sc,n) = uninterp_prim_token c local_scopes in (na,sc,n)
+
(* Miscellaneous *)
let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
diff --git a/interp/notation.mli b/interp/notation.mli
index 892eba8d11..842f2b1458 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -206,9 +206,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) ->
raise [No_match] if no such token *)
val uninterp_prim_token :
- 'a glob_constr_g -> scope_name * prim_token
+ 'a glob_constr_g -> subscopes -> prim_token * delimiters option
val uninterp_prim_token_cases_pattern :
- 'a cases_pattern_g -> Name.t * scope_name * prim_token
+ 'a cases_pattern_g -> subscopes -> Name.t * prim_token * delimiters option
val availability_of_prim_token :
prim_token -> scope_name -> subscopes -> delimiters option option
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 492671fff0..d5f104b7f8 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -42,6 +42,8 @@ let wit_var =
let wit_ref = make0 "ref"
+let wit_smart_global = make0 ~dyn:(val_tag (topwit wit_ref)) "smart_global"
+
let wit_sort_family = make0 "sort_family"
let wit_constr =
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 35de3693cb..89bdd78c70 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -39,6 +39,8 @@ val wit_var : (lident, lident, Id.t) genarg_type
val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_smart_global : (qualid or_by_notation, GlobRef.t located or_var, GlobRef.t) genarg_type
+
val wit_sort_family : (Sorts.family, unit, unit) genarg_type
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
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-05-03 10:38:43 +0000