aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_command.ml2
-rw-r--r--interp/constrintern.ml40
-rw-r--r--interp/constrintern.mli16
-rw-r--r--library/impargs.ml7
-rw-r--r--library/impargs.mli12
-rw-r--r--parsing/g_constr.ml437
-rw-r--r--theories/Init/Wf.v2
-rw-r--r--theories/Program/Wf.v2
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/command.ml82
-rw-r--r--toplevel/command.mli12
-rw-r--r--toplevel/record.ml2
12 files changed, 153 insertions, 63 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b06880bd3e..9c40c861e1 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -374,7 +374,7 @@ let interp_recursive fixkind l boxed =
let env_rec = push_named_context rec_sign env in
(* Get interpretation metadatas *)
- let impls = Command.compute_interning_datas env [] fixnames fixtypes in
+ let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in
let notations = List.fold_right Option.List.cons ntnl [] in
(* Interp bodies with rollback because temp use of notations/implicit *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 156d155667..49b719bdb5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1144,17 +1144,36 @@ let intern_pattern env patt =
let intern_ltac isarity ltacvars sigma env c =
intern_gen isarity sigma env ~ltacvars:ltacvars c
+type manual_implicits = (explicitation * (bool * bool)) list
+
+let implicits_of_rawterm l =
+ let rec aux i c =
+ match c with
+ RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
+ let rest = aux (succ i) b in
+ if bk = Implicit then
+ let name =
+ match na with
+ Name id -> Some id
+ | Anonymous -> None
+ in
+ (ExplByPos (i, name), (true, true)) :: rest
+ else rest
+ | RLetIn (loc, na, t, b) -> aux i b
+ | _ -> []
+ in aux 1 l
+
(*********************************************************************)
(* Functions to parse and interpret constructions *)
let interp_gen kind sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
- Default.understand_gen kind sigma env
- (intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c)
+ let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
+ Default.understand_gen kind sigma env c
let interp_constr sigma env c =
- interp_gen (OfType None) sigma env c
+ interp_gen (OfType None) sigma env c
let interp_type sigma env ?(impls=([],[])) c =
interp_gen IsType sigma env ~impls c
@@ -1168,9 +1187,20 @@ let interp_open_constr sigma env c =
let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
+let interp_constr_evars_gen_impls evdref env ?(impls=([],[])) kind c =
+ let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+ let imps = implicits_of_rawterm c in
+ Default.understand_tcc_evars evdref env kind c, imps
+
let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
- Default.understand_tcc_evars evdref env kind
- (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
+ let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+ Default.understand_tcc_evars evdref env kind c
+
+let interp_casted_constr_evars_impls evdref env ?(impls=([],[])) c typ =
+ interp_constr_evars_gen_impls evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars_impls evdref env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls evdref env IsType ~impls c
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f4272a2b19..9f3a815ee0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,6 +45,8 @@ type var_internalisation_data =
type implicits_env = (identifier * var_internalisation_data) list
type full_implicits_env = identifier list * implicits_env
+type manual_implicits = (explicitation * (bool * bool)) list
+
type ltac_sign = identifier list * unbound_ltac_var_map
(*s Internalisation performs interpretation of global names and notations *)
@@ -74,14 +76,22 @@ val interp_gen : typing_constraint -> evar_map -> env ->
val interp_constr : evar_map -> env ->
constr_expr -> constr
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
- constr_expr -> types -> constr
-
val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+ constr_expr -> types -> constr
+
+(* Accepting evars and giving back the manual implicits in addition. *)
+
+val interp_casted_constr_evars_impls : evar_defs ref -> env ->
+ ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+
+val interp_type_evars_impls : evar_defs ref -> env -> ?impls:full_implicits_env ->
+ constr_expr -> types * manual_implicits
+
val interp_casted_constr_evars : evar_defs ref -> env ->
?impls:full_implicits_env -> constr_expr -> types -> constr
diff --git a/library/impargs.ml b/library/impargs.ml
index 081bb58c10..9ffd103deb 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -471,9 +471,10 @@ let rebuild_implicits (req,l) =
| ImplAuto -> [ref,compute_global_implicits flags ref]
| ImplManual l ->
let auto = compute_global_implicits flags ref in
+ let auto = if flags.main then auto else List.map (fun _ -> None) auto in
let l' = merge_impls auto l in [ref,l']
in (req,l')
-
+
let (inImplicits, _) =
declare_object {(default_object "IMPLICITS") with
@@ -530,6 +531,10 @@ let declare_manual_implicits local ref enriching l =
in
add_anonymous_leaf (inImplicits (req,[ref,l']))
+let maybe_declare_manual_implicits local ref enriching l =
+ if l = [] then ()
+ else declare_manual_implicits local ref enriching l
+
(*s Registration as global tables *)
let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index a9e6ccb91f..e7b05f4223 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -57,7 +57,7 @@ val compute_implicits : env -> types -> implicits_list
(* A [manual_explicitation] is a tuple of a positional or named explicitation with
maximal insertion and forcing flags. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool)
+type manual_explicitation = Topconstr.explicitation * (bool * bool)
val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
@@ -69,8 +69,16 @@ val declare_mib_implicits : mutual_inductive -> unit
val declare_implicits : bool -> global_reference -> unit
-(* Manual declaration of which arguments are expected implicit *)
+(* [declare_manual_implicits local ref enriching l]
+ Manual declaration of which arguments are expected implicit.
+ Unsets implicits if [l] is empty. *)
+
val declare_manual_implicits : bool -> global_reference -> bool ->
manual_explicitation list -> unit
+(* If the list is empty, do nothing, otherwise declare the implicits. *)
+
+val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
+ manual_explicitation list -> unit
+
val implicits_of_global : global_reference -> implicits_list
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 68389c54a4..423ade8b6d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -103,13 +103,16 @@ let impl_ident =
Gram.Entry.of_parser "impl_ident"
(fun strm ->
match Stream.npeek 1 strm with
- | [("IDENT",("wf"|"struct"|"measure"))] ->
- raise Stream.Failure
- | [("IDENT",s)] ->
- Stream.junk strm;
- Names.id_of_string s
+ | [(_,"{")] ->
+ (match Stream.npeek 2 strm with
+ | [_;("IDENT",("wf"|"struct"|"measure"))] ->
+ raise Stream.Failure
+ | [_;("IDENT",s)] ->
+ Stream.junk strm; Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
-
+
let ident_eq =
Gram.Entry.of_parser "ident_eq"
(fun strm ->
@@ -356,10 +359,26 @@ GEXTEND Gram
ctx @ bl
| cl = LIST0 binder_let -> cl ] ]
;
+ binder_assum:
+ [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
+ | idl=LIST1 name; ":"; c=lconstr; "}" ->
+ (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
+ | idl=LIST1 name; "}" ->
+ (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)))
+ | ":"; c=lconstr; "}" ->
+ (fun id -> LocalRawAssum ([id],Default Implicit,c))
+ ] ]
+ ;
+ fixannot:
+ [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
+ | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
+ | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
+ ] ]
+ ;
binders_let_fixannot:
- [ [ "{"; IDENT "struct"; id=name; "}" -> [], (Some id, CStructRec)
- | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> [], (id, CWfRec rel)
- | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> [], (id, CMeasureRec rel)
+ [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
+ (assum (loc, Name id) :: fst bl), snd bl
+ | f = fixannot -> [], f
| b = binder_let; bl = binders_let_fixannot ->
b :: fst bl, snd bl
| -> [], (None, CStructRec)
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 024b32af4a..39df213281 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -157,7 +157,7 @@ Section Well_founded_2.
P x x' :=
F
(fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
- Acc_iter_2 (x:=y) (x':=y') (Acc_inv a h)).
+ Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
End Acc_iter_2.
Hypothesis Rwf : well_founded R.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 98b18f9030..bf37c8f231 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -2,6 +2,8 @@ Require Import Coq.Init.Wf.
Require Import Coq.Program.Utils.
Require Import ProofIrrelevance.
+Implicit Arguments Enriching Acc_inv [y].
+
(** Reformulation of the Wellfounded module using subsets where possible. *)
Section Well_founded.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4af59ff621..3896f02dda 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -183,7 +183,7 @@ let declare_structure env id idbuild params arity fields =
mind_entry_record = true;
mind_entry_finite = true;
mind_entry_inds = [mie_ind] } in
- let kn = Command.declare_mutual_with_eliminations true mie in
+ let kn = Command.declare_mutual_with_eliminations true mie [] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 327fe904ec..b5c9cb59bd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,8 +139,7 @@ let red_constant_entry bl ce = function
let declare_global_definition ident ce local imps =
let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
let gr = ConstRef kn in
- if Impargs.is_implicit_args () || imps <> [] then
- declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
if local = Local && Flags.is_verbose() then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
@@ -192,8 +191,7 @@ let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) =
let kn =
declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
let gr = ConstRef kn in
- if Impargs.is_implicit_args () || imps <> [] then
- declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
assumption_message ident;
if local=Local & Flags.is_verbose () then
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -459,18 +457,18 @@ let declare_eliminations sp =
(* 3b| Mutual inductive definitions *)
-let compute_interning_datas env l nal typl =
- let mk_interning_data na typ =
+let compute_interning_datas env l nal typl impll =
+ let mk_interning_data na typ impls =
let idl, impl =
- if is_implicit_args() then
- let impl = compute_implicits env typ in
- let sub_impl,_ = list_chop (List.length l) impl in
- let sub_impl' = List.filter is_status_implicit sub_impl in
+ let impl =
+ compute_implicits_with_manual env typ (is_implicit_args ()) impls
+ in
+ let sub_impl,_ = list_chop (List.length l) impl in
+ let sub_impl' = List.filter is_status_implicit sub_impl in
(List.map name_of_implicit sub_impl', impl)
- else
- ([],[]) in
- (na, (idl, impl, compute_arguments_scope typ)) in
- (l, List.map2 mk_interning_data nal typl)
+ in
+ (na, (idl, impl, compute_arguments_scope typ)) in
+ (l, list_map3 mk_interning_data nal typl impll)
let declare_interning_data (_,impls) (df,c,scope) =
silently (Metasyntax.add_notation_interpretation df impls c) scope
@@ -521,13 +519,14 @@ let interp_cstrs evdref env impls mldata arity ind =
(* Complete conclusions of constructor types if given in ML-style syntax *)
let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
(* Interpret the constructor types *)
- let ctyps'' = List.map (interp_type_evars evdref env ~impls) ctyps' in
- (cnames, ctyps'')
+ let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
+ (cnames, ctyps'', cimpls)
let interp_mutual paramsl indl notations finite =
check_all_names_different indl;
let env0 = Global.env() in
let evdref = ref (Evd.create_evar_defs Evd.empty) in
+ let userimpls = Implicit_quantifiers.implicits_of_binders paramsl in
let env_params, ctx_params = interp_context_evars evdref env0 paramsl in
let indnames = List.map (fun ind -> ind.ind_name) indl in
@@ -542,7 +541,8 @@ let interp_mutual paramsl indl notations finite =
let env_ar_params = push_rel_context ctx_params env_ar in
(* Compute interpretation metadatas *)
- let impls = compute_interning_datas env0 params indnames fullarities in
+ let indimpls = List.map (fun _ -> userimpls) fullarities in
+ let impls = compute_interning_datas env0 params indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
let constructors =
@@ -556,17 +556,17 @@ let interp_mutual paramsl indl notations finite =
(* Instantiate evars and check all are resolved *)
let evd,_ = consider_remaining_unif_problems env_params !evdref in
let sigma = evars_of evd in
- let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in
+ let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
let arities = List.map (nf_evar sigma) arities in
List.iter (check_evars env_params Evd.empty evd) arities;
Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
- List.iter (fun (_,ctyps) ->
+ List.iter (fun (_,ctyps,_) ->
List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
constructors;
(* Build the inductive entries *)
- let entries = list_map3 (fun ind arity (cnames,ctypes) -> {
+ let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> {
mind_entry_typename = ind.ind_name;
mind_entry_arity = arity;
mind_entry_consnames = cnames;
@@ -577,7 +577,7 @@ let interp_mutual paramsl indl notations finite =
{ mind_entry_params = List.map prepare_param ctx_params;
mind_entry_record = false;
mind_entry_finite = finite;
- mind_entry_inds = entries }
+ mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors)
let eq_constr_expr c1 c2 =
try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
@@ -630,21 +630,36 @@ let _ =
optwrite = (fun b -> elim_flag := b) }
-let declare_mutual_with_eliminations isrecord mie =
+let lift_implicits n =
+ List.map (fun x ->
+ match fst x with
+ ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
+ | _ -> x)
+
+let declare_mutual_with_eliminations isrecord mie impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
- let (_,kn) = declare_mind isrecord mie in
- if_verbose ppnl (minductive_message names);
- if !elim_flag then declare_eliminations kn;
- kn
+ let params = List.length mie.mind_entry_params in
+ let (_,kn) = declare_mind isrecord mie in
+ list_iter_i (fun i (indimpls, constrimpls) ->
+ let ind = (kn,i) in
+ list_iter_i
+ (fun j impls ->
+ maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
+ (is_implicit_args()) (indimpls @ (lift_implicits params impls)))
+ constrimpls)
+ impls;
+ if_verbose ppnl (minductive_message names);
+ if !elim_flag then declare_eliminations kn;
+ kn
let build_mutual l finite =
let indl,ntnl = List.split l in
let paramsl = extract_params indl in
let coes = extract_coercions indl in
let notations,indl = prepare_inductive ntnl indl in
- let mie = interp_mutual paramsl indl notations finite in
+ let mie,impls = interp_mutual paramsl indl notations finite in
(* Declare the mutual inductive block with its eliminations *)
- ignore (declare_mutual_with_eliminations false mie);
+ ignore (declare_mutual_with_eliminations false mie impls);
(* Declare the possible notations of inductive types *)
List.iter (declare_interning_data ([],[])) notations;
(* Declare the coercions *)
@@ -785,11 +800,9 @@ let declare_fix boxed kind f def t imps =
} in
let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
let gr = ConstRef kn in
- if Impargs.is_implicit_args () || imps <> [] then
- declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
gr
-
-
+
let prepare_recursive_declaration fixnames fixtypes fixdefs =
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
let names = List.map (fun id -> Name id) fixnames in
@@ -828,7 +841,7 @@ let interp_recursive fixkind l boxed =
let env_rec = push_named_types env fixnames fixtypes in
(* Get interpretation metadatas *)
- let impls = compute_interning_datas env [] fixnames fixtypes in
+ let impls = compute_interning_datas env [] fixnames fixtypes fiximps in
let notations = List.fold_right Option.List.cons ntnl [] in
(* Interp bodies with rollback because temp use of notations/implicit *)
@@ -1043,8 +1056,7 @@ let start_proof_com sopt kind (bl,t) hook =
let j = Default.understand_judgment sigma env ib in
start_proof id kind j.uj_val
(fun str cst ->
- if Impargs.is_implicit_args () || imps <> [] then
- declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
hook str cst)
let check_anonymity id save_ident =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d67daa83a6..a6a403c035 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -57,16 +57,20 @@ val compute_interning_datas : Environ.env ->
'a list ->
'b list ->
Term.types list ->
- 'a list *
+ Impargs.manual_explicitation list list ->
+ 'a list *
('b *
- (Names.identifier list * Impargs.implicits_list *
- Topconstr.scope_name option list))
+ (Names.identifier list * Impargs.implicits_list *
+ Topconstr.scope_name option list))
list
val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
val declare_mutual_with_eliminations :
- bool -> Entries.mutual_inductive_entry -> mutual_inductive
+ bool -> Entries.mutual_inductive_entry ->
+ (Impargs.manual_explicitation list *
+ Impargs.manual_explicitation list list) list ->
+ mutual_inductive
type fixpoint_kind =
| IsFixpoint of (int option * recursion_order_expr) list
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b045573045..57a7e63b34 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -223,7 +223,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
mind_entry_record = true;
mind_entry_finite = not declare_as_coind;
mind_entry_inds = [mie_ind] } in
- let kn = declare_mutual_with_eliminations true mie in
+ let kn = declare_mutual_with_eliminations true mie [] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let kinds,sp_projs = declare_projections rsp coers fields in
let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 03:52:46 +0000