aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml8
-rw-r--r--vernac/attributes.mli1
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comAssumption.ml1
-rw-r--r--vernac/comDefinition.ml22
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml25
-rw-r--r--vernac/comFixpoint.mli4
-rw-r--r--vernac/comHints.ml30
-rw-r--r--vernac/comPrimitive.ml2
-rw-r--r--vernac/comProgramFixpoint.ml32
-rw-r--r--vernac/comProgramFixpoint.mli2
-rw-r--r--vernac/comSearch.ml14
-rw-r--r--vernac/declare.ml101
-rw-r--r--vernac/declare.mli8
-rw-r--r--vernac/declaremods.mli2
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/g_proofs.mlg2
-rw-r--r--vernac/g_vernac.mlg4
-rw-r--r--vernac/library.ml4
-rw-r--r--vernac/metasyntax.ml29
-rw-r--r--vernac/prettyp.ml4
-rw-r--r--vernac/proof_using.ml26
-rw-r--r--vernac/proof_using.mli5
-rw-r--r--vernac/record.ml759
-rw-r--r--vernac/record.mli55
-rw-r--r--vernac/search.ml20
-rw-r--r--vernac/vernacentries.ml113
28 files changed, 776 insertions, 507 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fb308fd316..efba6d332a 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -224,3 +224,11 @@ let canonical_field =
enable_attribute ~key:"canonical" ~default:(fun () -> true)
let canonical_instance =
enable_attribute ~key:"canonical" ~default:(fun () -> false)
+
+let uses_parser : string key_parser = fun orig args ->
+ assert_once ~name:"using" orig;
+ match args with
+ | VernacFlagLeaf str -> str
+ | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
+
+let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 51bab79938..1969665082 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -51,6 +51,7 @@ val option_locality : Goptions.option_locality attribute
val deprecation : Deprecation.t option attribute
val canonical_field : bool attribute
val canonical_instance : bool attribute
+val using : string option attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d5509e2697..054addc542 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -57,7 +57,7 @@ let is_local_for_hint i =
let add_instance_base inst =
let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
- add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
+ add_instance_hint (Hints.hint_globref inst.is_impl) [inst.is_impl] ~locality
inst.is_info
let mk_instance cl info glob impl =
@@ -503,7 +503,7 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx'
declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype
let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
- let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
+ let sigma, decl = interp_univ_decl_opt env pl in
let tclass =
if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
else tclass
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 12194ea20c..9e850ff1c7 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -13,7 +13,6 @@ open Util
open Vars
open Names
open Context
-open Constrexpr_ops
open Constrintern
open Impargs
open Pretyping
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c1dbf0a1ea..81154bbea9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -110,32 +110,42 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
evd, (c, tyopt), imps
-let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
let program_mode = false in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
- let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+ let evd, udecl = interp_univ_decl_opt env udecl in
let evd, (body, types), impargs =
interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
in
+ let using = using |> Option.map (fun expr ->
+ let terms = body :: match types with Some x -> [x] | None -> [] in
+ let l = Proof_using.process_expr (Global.env()) evd expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let kind = Decls.IsDefinition kind in
- let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+ let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
let _ : Names.GlobRef.t =
Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
in ()
-let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
let program_mode = true in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
- let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+ let evd, udecl = interp_univ_decl_opt env udecl in
let evd, (body, types), impargs =
interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
in
+ let using = using |> Option.map (fun expr ->
+ let terms = body :: match types with Some x -> [x] | None -> [] in
+ let l = Proof_using.process_expr (Global.env()) evd expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
let pm, _ =
- let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+ let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7420235449..5e1b705ae4 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -31,6 +31,7 @@ val do_definition
-> scope:Locality.locality
-> poly:bool
-> kind:Decls.definition_object_kind
+ -> ?using:Vernacexpr.section_subset_expr
-> universe_decl_expr option
-> local_binder_expr list
-> red_expr option
@@ -45,6 +46,7 @@ val do_definition_program
-> scope:Locality.locality
-> poly:bool
-> kind:Decls.logical_kind
+ -> ?using:Vernacexpr.section_subset_expr
-> universe_decl_expr option
-> local_binder_expr list
-> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 78572c6aa6..dd6c985bf9 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -176,7 +176,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
CErrors.user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
- let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env all_universes in
+ let sigma, decl = interp_univ_decl_opt env all_universes in
let sigma, (fixctxs, fiximppairs, fixannots) =
on_snd List.split3 @@
List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
@@ -251,15 +251,22 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l :
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
-let build_recthms ~indexes fixnames fixtypes fiximps =
+let build_recthms ~indexes ?using fixnames fixtypes fiximps =
let fix_kind, cofix = match indexes with
| Some indexes -> Decls.Fixpoint, false
| None -> Decls.CoFixpoint, true
in
let thms =
List.map3 (fun name typ (ctx,impargs,_) ->
+ let using = using |> Option.map (fun expr ->
+ let terms = [EConstr.of_constr typ] in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
+ let l = Proof_using.process_expr env sigma expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let args = List.map Context.Rel.Declaration.get_name ctx in
- Declare.CInfo.make ~name ~typ ~args ~impargs ()
+ Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
) fixnames fixtypes fiximps
in
fix_kind, cofix, thms
@@ -277,9 +284,9 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
lemma
-let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
(* We shortcut the proof process *)
- let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
+ let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
let fixdefs = List.map Option.get fixdefs in
let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fix_kind = Decls.IsDefinition fix_kind in
@@ -328,9 +335,9 @@ let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
lemma
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~scope ~poly ?using l =
let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
- declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns
+ declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns
let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
@@ -342,6 +349,6 @@ let do_cofixpoint_interactive ~scope ~poly l =
let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
lemma
-let do_cofixpoint ~scope ~poly l =
+let do_cofixpoint ~scope ~poly ?using l =
let cofix, ntns = do_cofixpoint_common l in
- declare_fixpoint_generic ~scope ~poly cofix ntns
+ declare_fixpoint_generic ~scope ~poly ?using cofix ntns
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index aa5446205c..a36aba7672 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,13 +19,13 @@ val do_fixpoint_interactive :
scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
val do_fixpoint :
- scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
+ scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit
val do_cofixpoint_interactive :
scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
val do_cofixpoint :
- scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
+ scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> cofixpoint_expr list -> unit
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 9eac558908..f642411fa4 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -62,7 +62,7 @@ let project_hint ~poly pri l2r r =
cb
in
let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
- (info, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
+ (info, true, Hints.PathAny, Hints.hint_globref (GlobRef.ConstRef c))
let warn_deprecated_hint_constr =
CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
@@ -84,16 +84,6 @@ let soft_evaluable =
let interp_hints ~poly h =
let env = Global.env () in
let sigma = Evd.from_env env in
- let f poly c =
- let evd, c = Constrintern.interp_open_constr env sigma c in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let c, diff = Hints.prepare_hint true env sigma (evd, c) in
- if poly then (Hints.IsConstr (c, Some diff) [@ocaml.warning "-3"])
- else
- let () = DeclareUctx.declare_universe_context ~poly:false diff in
- (Hints.IsConstr (c, None) [@ocaml.warning "-3"])
- in
let fref r =
let gr = Smartlocate.global_with_alias r in
Dumpglob.add_glob ?loc:r.CAst.loc gr;
@@ -106,10 +96,22 @@ let interp_hints ~poly h =
match c with
| HintsReference c ->
let gr = Smartlocate.global_with_alias c in
- (PathHints [gr], IsGlobRef gr)
+ (PathHints [gr], hint_globref gr)
| HintsConstr c ->
let () = warn_deprecated_hint_constr () in
- (PathAny, f poly c)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c, uctx = Constrintern.interp_constr env sigma c in
+ let subst, uctx = UState.normalize_variables uctx in
+ let c = EConstr.Vars.subst_univs_constr subst c in
+ let diff = UState.context_set uctx in
+ let c =
+ if poly then (c, Some diff)
+ else
+ let () = DeclareUctx.declare_universe_context ~poly:false diff in
+ (c, None)
+ in
+ (PathAny, Hints.hint_constr c) [@ocaml.warning "-3"]
in
let fp = Constrintern.intern_constr_pattern env sigma in
let fres (info, b, r) =
@@ -149,7 +151,7 @@ let interp_hints ~poly h =
( empty_hint_info
, true
, PathHints [gr]
- , IsGlobRef gr ))
+ , hint_globref gr ))
in
HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index eaa5271a73..a910cc6e8b 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -30,7 +30,7 @@ let do_primitive id udecl prim typopt =
declare id {Entries.prim_entry_type = None; prim_entry_content = prim}
| Some typ ->
let env = Global.env () in
- let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+ let evd, udecl = Constrintern.interp_univ_decl_opt env udecl in
let auctx = CPrimitives.op_or_type_univs prim in
let evd, u = Evd.with_context_set UState.univ_flexible evd (UnivGen.fresh_instance auctx) in
let expected_typ = EConstr.of_constr @@ Typeops.type_of_prim_or_type env u prim in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 55901fd604..31f91979d3 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,13 +109,13 @@ let telescope env sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let env = Global.env() in
- let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
+ let sigma, udecl = interp_univ_decl_opt env pl in
let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in
let len = List.length binders_rel in
let top_env = push_rel_context binders_rel env in
@@ -259,8 +259,13 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
let evars, _, evars_def, evars_typ =
RetrieveObl.retrieve_obligations env recname sigma 0 def typ
in
+ let using = using |> Option.map (fun expr ->
+ let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
+ let l = Proof_using.process_expr env sigma expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let uctx = Evd.evar_universe_context sigma in
- let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
+ let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
let info = Declare.Info.make ~udecl ~poly ~hook () in
let pm, _ =
Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
@@ -275,7 +280,7 @@ let collect_evars_of_term evd c ty =
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
-let do_program_recursive ~pm ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
let cofix = fixkind = Declare.Obls.IsCoFixpoint in
let (env, rec_sign, udecl, evd), fix, info =
interp_recursive ~cofix ~program_mode:true fixl
@@ -287,13 +292,18 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
let evd = nf_evar_map_undefined evd in
let collect_evars name def typ impargs =
(* Generalize by the recursive prototypes *)
+ let using = using |> Option.map (fun expr ->
+ let terms = [def; typ] in
+ let l = Proof_using.process_expr env evd expr terms in
+ Names.Id.Set.(List.fold_right add l empty))
+ in
let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
RetrieveObl.retrieve_obligations env name evm
(List.length rec_sign) def typ in
- let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+ let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
(cinfo, def, evars)
in
let (fixnames,fixrs,fixdefs,fixtypes) = fix in
@@ -325,13 +335,13 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
-let do_fixpoint ~pm ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly ?using l =
let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
match g, l with
| [Some { CAst.v = CWfRec (n,r) }],
[ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
let recarg = mkIdentC n.CAst.v in
- build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations
| [Some { CAst.v = CMeasureRec (n, m, r) }],
[Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +354,7 @@ let do_fixpoint ~pm ~scope ~poly l =
user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
| _, _ -> r
in
- build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
+ build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
| _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,11 +362,11 @@ let do_fixpoint ~pm ~scope ~poly l =
Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
let fixkind = Declare.Obls.IsFixpoint annots in
let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
- do_program_recursive ~pm ~scope ~poly fixkind l
+ do_program_recursive ~pm ~scope ~poly ?using fixkind l
| _, _ ->
CErrors.user_err ~hdr:"do_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let do_cofixpoint ~pm ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly ?using fixl =
let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
- do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+ do_program_recursive ~pm ~scope ~poly ?using Declare.Obls.IsCoFixpoint fixl
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 7935cf27fb..30bf3ae8f8 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -15,6 +15,7 @@ val do_fixpoint :
pm:Declare.OblState.t
-> scope:Locality.locality
-> poly:bool
+ -> ?using:Vernacexpr.section_subset_expr
-> fixpoint_expr list
-> Declare.OblState.t
@@ -22,5 +23,6 @@ val do_cofixpoint :
pm:Declare.OblState.t
-> scope:Locality.locality
-> poly:bool
+ -> ?using:Vernacexpr.section_subset_expr
-> cofixpoint_expr list
-> Declare.OblState.t
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index 9de8d6fbc3..af51f4fafb 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -53,9 +53,19 @@ let kind_searcher = Decls.(function
let interp_search_item env sigma =
function
| SearchSubPattern ((where,head),pat) ->
- let _,pat = Constrintern.intern_constr_pattern env sigma pat in
+ let expected_type = Pretyping.(if head then IsType else WithoutTypeConstraint) in
+ let pat =
+ try Constrintern.interp_constr_pattern env sigma ~expected_type pat
+ with e when CErrors.noncritical e ->
+ (* We cannot ensure (yet?) that a typable pattern will
+ actually be typed, consider e.g. (forall A, A -> A /\ A)
+ which fails, not seeing that A can be Prop; so we use an
+ untyped pattern as a fallback (i.e w/o no insertion of
+ coercions, no compilation of pattern-matching) *)
+ snd (Constrintern.intern_constr_pattern env sigma ~as_type:head pat) in
GlobSearchSubPattern (where,head,pat)
- | SearchString ((Anywhere,false),s,None) when Id.is_valid s ->
+ | SearchString ((Anywhere,false),s,None)
+ when Id.is_valid_ident_part s && String.equal (String.drop_simple_quotes s) s ->
GlobSearchString s
| SearchString ((where,head),s,sc) ->
(try
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 3a8ceb0e0f..1e8771b641 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -55,11 +55,13 @@ module CInfo = struct
(** Names to pre-introduce *)
; impargs : Impargs.manual_implicits
(** Explicitily declared implicit arguments *)
+ ; using : Names.Id.Set.t option
+ (** Explicit declaration of section variables used by the constant *)
}
- let make ~name ~typ ?(args=[]) ?(impargs=[]) () =
- { name; typ; args; impargs }
+ let make ~name ~typ ?(args=[]) ?(impargs=[]) ?using () =
+ { name; typ; args; impargs; using }
let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
@@ -108,10 +110,10 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
(** [univsbody] are universe-constraints attached to the body-only,
used in vio-delayed opaque constants and private poly universes *)
-let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+let definition_entry_core ?(opaque=false) ?using ?(inline=false) ?feedback_id ?types
?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
{ proof_entry_body = Future.from_val ((body,univsbody), eff);
- proof_entry_secctx = section_vars;
+ proof_entry_secctx = using;
proof_entry_type = types;
proof_entry_universes = univs;
proof_entry_opaque = opaque;
@@ -119,7 +121,7 @@ let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_
proof_entry_inline_code = inline}
let definition_entry =
- definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+ definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None
type 'a constant_entry =
| DefinitionEntry of 'a proof_entry
@@ -236,9 +238,9 @@ let pure_definition_entry ?(opaque=false) ?(inline=false) ?types
proof_entry_feedback = None;
proof_entry_inline_code = inline}
-let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
+let delayed_definition_entry ~opaque ?feedback_id ~using ~univs ?types body =
{ proof_entry_body = body
- ; proof_entry_secctx = section_vars
+ ; proof_entry_secctx = using
; proof_entry_type = types
; proof_entry_universes = univs
; proof_entry_opaque = opaque
@@ -608,8 +610,8 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar
uctx, univs
in
let csts = CList.map2
- (fun CInfo.{ name; typ; impargs } body ->
- let entry = definition_entry ~opaque ~types:typ ~univs body in
+ (fun CInfo.{ name; typ; impargs; using } body ->
+ let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
cinfo fixdecls
in
@@ -660,7 +662,7 @@ let check_evars_are_solved env sigma t =
let evars = Evarutil.undefined_evars_of_term sigma t in
if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars
-let prepare_definition ~info ~opaque ~body ~typ sigma =
+let prepare_definition ~info ~opaque ?using ~body ~typ sigma =
let { Info.poly; udecl; inline; _ } = info in
let env = Global.env () in
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
@@ -669,13 +671,13 @@ let prepare_definition ~info ~opaque ~body ~typ sigma =
Option.iter (check_evars_are_solved env sigma) types;
check_evars_are_solved env sigma body;
let univs = Evd.check_univ_decl ~poly sigma udecl in
- let entry = definition_entry ~opaque ~inline ?types ~univs body in
+ let entry = definition_entry ~opaque ?using ~inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
entry, uctx
let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
- let { CInfo.name; impargs; typ; _ } = cinfo in
- let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
+ let { CInfo.name; impargs; typ; using; _ } = cinfo in
+ let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in
let { Info.scope; kind; hook; _ } = info in
declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
@@ -803,6 +805,7 @@ module ProgramDecl = struct
let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
let get_poly prg = prg.prg_info.Info.poly
let get_obligations prg = prg.prg_obligations
+ let get_using prg = prg.prg_cinfo.CInfo.using
end
end
@@ -1137,7 +1140,7 @@ let declare_mutual_definition ~pm l =
in
let term = EConstr.to_constr sigma term in
let typ = EConstr.to_constr sigma typ in
- let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in
+ let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs, x.prg_cinfo.CInfo.using) in
let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
(def, oblsubst)
in
@@ -1151,11 +1154,11 @@ let declare_mutual_definition ~pm l =
(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixdefs, fixrs, fixtypes, fixitems =
List.fold_right2
- (fun (d, r, typ, impargs) name (a1, a2, a3, a4) ->
+ (fun (d, r, typ, impargs, using) name (a1, a2, a3, a4) ->
( d :: a1
, r :: a2
, typ :: a3
- , CInfo.{name; typ; impargs; args = []} :: a4 ))
+ , CInfo.{name; typ; impargs; args = []; using } :: a4 ))
defs first.prg_deps ([], [], [], [])
in
let fixkind = Option.get first.prg_fixkind in
@@ -1288,7 +1291,7 @@ let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto} =
FIXME: There is duplication of this code with obligation_terminator
and Obligations.admit_obligations *)
-let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref =
+let obligation_admitted_terminator ~pm {name; num; auto} uctx' dref =
let prg = Option.get (State.find pm name) in
let {obls; remaining = rem} = prg.prg_obligations in
let obl = obls.(num) in
@@ -1300,21 +1303,21 @@ let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref =
if not transparent then err_not_transp ()
| _ -> ()
in
- let inst, ctx' =
+ let inst, uctx' =
if not prg.prg_info.Info.poly (* Not polymorphic *) then
(* The universe context was declared globally, we continue
from the new global environment. *)
- let ctx = UState.from_env (Global.env ()) in
- let ctx' = UState.merge_subst ctx (UState.subst ctx') in
- (Univ.Instance.empty, ctx')
+ let uctx = UState.from_env (Global.env ()) in
+ let uctx' = UState.merge_subst uctx (UState.subst uctx') in
+ (Univ.Instance.empty, uctx')
else
(* We get the right order somehow, but surely it could be enforced in a clearer way. *)
- let uctx = UState.context ctx' in
- (Univ.UContext.instance uctx, ctx')
+ let uctx = UState.context uctx' in
+ (Univ.UContext.instance uctx, uctx')
in
let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in
let () = if transparent then add_hint true prg cst in
- update_program_decl_on_defined ~pm prg obls num obl ~uctx:ctx' rem ~auto
+ update_program_decl_on_defined ~pm prg obls num obl ~uctx:uctx' rem ~auto
end
@@ -1376,7 +1379,7 @@ end
type t =
{ endline_tactic : Genarg.glob_generic_argument option
- ; section_vars : Id.Set.t option
+ ; using : Id.Set.t option
; proof : Proof.t
; initial_euctx : UState.t
(** The initial universe context (for the statement) *)
@@ -1435,7 +1438,7 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
{ proof
; endline_tactic = None
- ; section_vars = None
+ ; using = None
; initial_euctx
; pinfo
}
@@ -1458,7 +1461,7 @@ let start_dependent ~info ~name ~proof_ending goals =
let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
{ proof
; endline_tactic = None
- ; section_vars = None
+ ; using = None
; initial_euctx
; pinfo
}
@@ -1523,7 +1526,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
map lemma ~f:(fun p ->
pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)
-let get_used_variables pf = pf.section_vars
+let get_used_variables pf = pf.using
let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
let set_used_variables ps l =
@@ -1547,9 +1550,9 @@ let set_used_variables ps l =
else (ctx, all_safe) in
let ctx, _ =
Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
- if not (Option.is_empty ps.section_vars) then
+ if not (Option.is_empty ps.using) then
CErrors.user_err Pp.(str "Used section variables can be declared only once");
- ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+ ctx, { ps with using = Some (Context.Named.to_vars ctx) }
let get_open_goals ps =
let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
@@ -1624,12 +1627,12 @@ let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
- let universes = UState.restrict uctx used_univs in
- let typus = UState.restrict universes used_univs_typ in
- let utyp = UState.check_univ_decl ~poly typus udecl in
+ let uctx = UState.restrict uctx used_univs in
+ let uctx' = UState.restrict uctx used_univs_typ in
+ let utyp = UState.check_univ_decl ~poly uctx' udecl in
let ubody = Univ.ContextSet.diff
- (UState.context_set universes)
- (UState.context_set typus)
+ (UState.context_set uctx)
+ (UState.context_set uctx')
in
utyp, ubody
@@ -1640,13 +1643,13 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body)
for the typ. We recheck the declaration after restricting with
the actually used universes.
TODO: check if restrict is really necessary now. *)
- let ctx = UState.restrict uctx used_univs in
- let utyp = UState.check_univ_decl ~poly ctx udecl in
+ let uctx = UState.restrict uctx used_univs in
+ let utyp = UState.check_univ_decl ~poly uctx udecl in
utyp, Univ.ContextSet.empty
let close_proof ~opaque ~keep_body_ucst_separate ps =
- let { section_vars; proof; initial_euctx; pinfo } = ps in
+ let { using; proof; initial_euctx; pinfo } = ps in
let { Proof_info.info = { Info.udecl } } = pinfo in
let { Proof.name; poly } = Proof.data proof in
let unsafe_typ = keep_body_ucst_separate && not poly in
@@ -1667,7 +1670,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
then make_univs_private_poly ~poly ~uctx ~udecl t b
else make_univs ~poly ~uctx ~udecl t b
in
- definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+ definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
in
let entries = CList.map make_entry elist in
{ name; entries; uctx }
@@ -1675,7 +1678,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
- let { section_vars; proof; initial_euctx; pinfo } = ps in
+ let { using; proof; initial_euctx; pinfo } = ps in
let { Proof_info.info = { Info.udecl } } = pinfo in
let { Proof.name; poly; entry; sigma } = Proof.data proof in
@@ -1709,10 +1712,10 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
(Vars.universes_of_constr types)
(Vars.universes_of_constr pt)
in
- let univs = UState.restrict uctx used_univs in
- let univs = UState.check_mono_univ_decl univs udecl in
- (pt,univs),eff)
- |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
+ let uctx = UState.restrict uctx used_univs in
+ let uctx = UState.check_mono_univ_decl uctx udecl in
+ (pt,uctx),eff)
+ |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types
in
let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
{ name; entries; uctx = initial_euctx }
@@ -2289,7 +2292,8 @@ let rec solve_obligation prg num tac =
let name = Internal.get_name prg in
Proof_ending.End_obligation {name; num; auto}
in
- let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in
+ let using = Internal.get_using prg in
+ let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) ?using () in
let poly = Internal.get_poly prg in
let info = Info.make ~scope ~kind ~poly () in
let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd in
@@ -2495,7 +2499,12 @@ let admit_obligations ~pm n =
let next_obligation ~pm n tac =
let prg = match n with
- | None -> State.first_pending pm |> Option.get
+ | None ->
+ begin match State.first_pending pm with
+ | Some prg -> prg
+ | None ->
+ Error.no_obligations None
+ end
| Some _ -> get_unique_prog ~pm n
in
let {obls; remaining} = Internal.get_obligations prg in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 1ad79928d5..0520bf8717 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,6 +79,7 @@ module CInfo : sig
-> typ:'constr
-> ?args:Name.t list
-> ?impargs:Impargs.manual_implicits
+ -> ?using:Names.Id.Set.t
-> unit
-> 'constr t
@@ -244,6 +245,12 @@ module Proof : sig
* (w.r.t. type dependencies and let-ins covered by it) *)
val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
+ (** Gets the set of variables declared to be used by the proof. None means
+ no "Proof using" or #[using] was given *)
+ val get_used_variables : t -> Id.Set.t option
+
+ (** Compacts the representation of the proof by pruning all intermediate
+ terms *)
val compact : t -> t
(** Update the proof's universe information typically after a
@@ -333,6 +340,7 @@ type 'a proof_entry
val definition_entry
: ?opaque:bool
+ -> ?using:Names.Id.Set.t
-> ?inline:bool
-> ?types:Constr.types
-> ?univs:Entries.universes_entry
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index 9ca2ca5593..a1b98e4d9c 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -86,7 +86,7 @@ val start_library : library_name -> unit
val end_library :
?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name ->
- Safe_typing.compiled_library * library_objects * Safe_typing.native_library
+ Safe_typing.compiled_library * library_objects * Nativelib.native_library
(** append a function to be executed at end_library *)
val append_end_library_hook : (unit -> unit) -> unit
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 123ea2c24e..efe4e17d0b 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -408,8 +408,8 @@ match e with
| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
| TTBigint ->
begin match forpat with
- | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v)))
- | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v)))
+ | ForConstr -> push_constr subst (CAst.make @@ CPrim (Number (NumTok.Signed.of_int_string v)))
+ | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Number (NumTok.Signed.of_int_string v)))
end
| TTReference ->
begin match forpat with
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index ebec720ce2..5b80ed6794 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -56,6 +56,8 @@ GRAMMAR EXTEND Gram
[ [ IDENT "Goal"; c = lconstr ->
{ VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) }
| IDENT "Proof" -> { VernacProof (None,None) }
+ | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr ->
+ { VernacProof (None,Some l) }
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn }
| IDENT "Proof"; c = lconstr -> { VernacExactProof c }
| IDENT "Abort" -> { VernacAbort None }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3d6a93c888..1c80d71ea5 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -113,7 +113,9 @@ GRAMMAR EXTEND Gram
]
;
attribute:
- [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } ]
+ [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v }
+ (* Required because "ident" is declared a keyword when loading Ltac. *)
+ | IDENT "using" ; v = attr_value -> { "using", v } ]
]
;
attr_value:
diff --git a/vernac/library.ml b/vernac/library.ml
index e580927bfd..8a9b1fd68d 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -160,7 +160,7 @@ let register_loaded_library m =
let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
let f = prefix ^ "cmo" in
let f = Dynlink.adapt_filename f in
- Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
+ Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
| [] ->
@@ -502,7 +502,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
(* Writing native code files *)
if output_native_objects then
let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in
- Nativelib.compile_library dir ast fn
+ Nativelib.compile_library ast fn
let save_library_raw f sum lib univs proofs =
save_library_base f sum lib (Some univs) None proofs
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 185abcf35b..8477870cb4 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1042,6 +1042,13 @@ let interp_non_syntax_modifiers mods =
in
List.fold_left (fun st modif -> Option.bind st @@ set modif) (Some (false,false,InConstrEntry)) mods
+(* Check if an interpretation can be used for printing a cases printing *)
+let has_no_binders_type =
+ List.for_all (fun (_,(_,typ)) ->
+ match typ with
+ | NtnTypeBinder _ | NtnTypeBinderList -> false
+ | NtnTypeConstr | NtnTypeConstrList -> true)
+
(* Compute precedences from modifiers (or find default ones) *)
let set_entry_type from n etyps (x,typ) =
@@ -1226,6 +1233,9 @@ let find_precedence custom lev etyps symbols onlyprint =
| _ ->
user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
+ | (ETPattern _ | ETBinder _), InConstrEntry when not onlyprint ->
+ (* Don't know exactly if we can make sense of this case *)
+ user_err Pp.(str "Binders or patterns not supported in leftmost position.")
| (ETPattern _ | ETBinder _ | ETConstr _), _ ->
(* Give a default ? *)
if Option.is_empty lev then
@@ -1416,6 +1426,7 @@ type notation_obj = {
notobj_deprecation : Deprecation.t option;
notobj_notation : notation * notation_location;
notobj_specific_pp_rules : syntax_printing_extension option;
+ notobj_also_in_cases_pattern : bool;
}
let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
@@ -1438,9 +1449,10 @@ let open_notation i (_, nobj) =
let pat = nobj.notobj_interp in
let deprecation = nobj.notobj_deprecation in
let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+ let also_in_cases_pattern = nobj.notobj_also_in_cases_pattern in
(* Declare the notation *)
(match nobj.notobj_use with
- | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation
+ | Some use -> Notation.declare_notation (scope,ntn) pat df ~use ~also_in_cases_pattern nobj.notobj_coercion deprecation
| None -> ());
(* Declare specific format if any *)
(match nobj.notobj_specific_pp_rules with
@@ -1621,19 +1633,21 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
let interp = make_interpretation_vars sd.recvars (pi2 sd.level) acvars (fst sd.pa_syntax_data) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
+ let vars = List.map_filter map i_vars in (* Order of elements is important here! *)
+ let also_in_cases_pattern = has_no_binders_type vars in
let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in
let notation, location = sd.info in
let use = make_use true onlyparse sd.only_printing in
let notation = {
notobj_local = local;
notobj_scope = scope;
- notobj_interp = (List.map_filter map i_vars, ac);
- (* Order is important here! *)
notobj_use = use;
+ notobj_interp = (vars, ac);
notobj_coercion = coe;
notobj_deprecation = sd.deprecation;
notobj_notation = (notation, location);
notobj_specific_pp_rules = sy_pp_rules;
+ notobj_also_in_cases_pattern = also_in_cases_pattern;
} in
(* Ready to change the global state *)
List.iter (fun f -> f ()) sd.msgs;
@@ -1665,18 +1679,20 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
let plevel = match level with Some (from,level,l) -> level | None (* numeral: irrelevant )*) -> 0 in
let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
+ let vars = List.map_filter map i_vars in (* Order of elements is important here! *)
+ let also_in_cases_pattern = has_no_binders_type vars in
let onlyparse,coe = printability level i_typs onlyparse reversibility ac in
let use = make_use false onlyparse onlyprint in
let notation = {
notobj_local = local;
notobj_scope = scope;
- notobj_interp = (List.map_filter map i_vars, ac);
- (* Order is important here! *)
notobj_use = use;
+ notobj_interp = (vars, ac);
notobj_coercion = coe;
notobj_deprecation = deprecation;
notobj_notation = df';
notobj_specific_pp_rules = pp_sy;
+ notobj_also_in_cases_pattern = also_in_cases_pattern;
} in
Lib.add_anonymous_leaf (inNotation notation);
df'
@@ -1850,8 +1866,9 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in
let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
+ let also_in_cases_pattern = has_no_binders_type vars in
let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in
- Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
+ Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat)
(**********************************************************************)
(* Declaration of custom entry *)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 06f7c32cdc..840754ccc6 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -631,11 +631,11 @@ let print_constant with_values sep sp udecl =
assert(ContextSet.is_empty body_uctxs);
Polymorphic ctx
in
- let ctx =
+ let uctx =
UState.of_binders
(Printer.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
in
- let env = Global.env () and sigma = Evd.from_ctx ctx in
+ let env = Global.env () and sigma = Evd.from_ctx uctx in
let pr_ltype = pr_ltype_env env sigma in
hov 0 (
match val_0 with
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 95680c2a4e..bdb0cabacf 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -18,30 +18,30 @@ module NamedDecl = Context.Named.Declaration
let known_names = Summary.ref [] ~name:"proofusing-nameset"
-let rec close_fwd e s =
+let rec close_fwd env sigma s =
let s' =
List.fold_left (fun s decl ->
let vb = match decl with
| LocalAssum _ -> Id.Set.empty
- | LocalDef (_,b,_) -> global_vars_set e b
+ | LocalDef (_,b,_) -> Termops.global_vars_set env sigma b
in
- let vty = global_vars_set e (NamedDecl.get_type decl) in
+ let vty = Termops.global_vars_set env sigma (NamedDecl.get_type decl) in
let vbty = Id.Set.union vb vty in
if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
- s (named_context e)
+ s (EConstr.named_context env)
in
- if Id.Set.equal s s' then s else close_fwd e s'
+ if Id.Set.equal s s' then s else close_fwd env sigma s'
-let set_of_type env ty =
+let set_of_type env sigma ty =
List.fold_left (fun acc ty ->
- Id.Set.union (global_vars_set env ty) acc)
+ Id.Set.union (Termops.global_vars_set env sigma ty) acc)
Id.Set.empty ty
let full_set env =
List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
-let process_expr env e v_ty =
+let process_expr env sigma e v_ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
| SsType -> v_ty
@@ -49,7 +49,7 @@ let process_expr env e v_ty =
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
- | SsFwdClose e -> close_fwd env (aux e)
+ | SsFwdClose e -> close_fwd env sigma (aux e)
and set_of_id id =
if Id.to_string id = "All" then
full_set env
@@ -59,9 +59,9 @@ let process_expr env e v_ty =
in
aux e
-let process_expr env e ty =
- let v_ty = set_of_type env ty in
- let s = Id.Set.union v_ty (process_expr env e v_ty) in
+let process_expr env sigma e ty =
+ let v_ty = set_of_type env sigma ty in
+ let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in
Id.Set.elements s
let name_set id expr = known_names := (id,expr) :: !known_names
@@ -110,7 +110,7 @@ let suggest_common env ppid used ids_typ skip =
S.empty (named_context env)
in
let all = S.diff all skip in
- let fwd_typ = close_fwd env ids_typ in
+ let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in
if !Flags.debug then begin
print (str "All " ++ pr_set false all);
print (str "Type " ++ pr_set false ids_typ);
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index dfc233e8fa..93dbd33ae4 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -11,7 +11,8 @@
(** Utility code for section variables handling in Proof using... *)
val process_expr :
- Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
+ Environ.env -> Evd.evar_map ->
+ Vernacexpr.section_subset_expr -> EConstr.types list ->
Names.Id.t list
val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
@@ -24,3 +25,5 @@ val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
val proof_using_opt_name : string list
(** For the stm *)
+
+val using_from_string : string -> Vernacexpr.section_subset_expr
diff --git a/vernac/record.ml b/vernac/record.ml
index acc97f61c1..891d7fcebe 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -11,53 +11,40 @@
open Pp
open CErrors
open Term
-open Sorts
open Util
open Names
-open Nameops
open Constr
open Context
-open Vars
open Environ
open Declarations
open Entries
-open Declare
-open Constrintern
open Type_errors
open Constrexpr
open Constrexpr_ops
-open Goptions
open Context.Rel.Declaration
-open Libobject
module RelDecl = Context.Rel.Declaration
(********** definition d'un record (structure) **************)
(** Flag governing use of primitive projections. Disabled by default. *)
-let primitive_flag = ref false
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Primitive";"Projections"];
- optread = (fun () -> !primitive_flag) ;
- optwrite = (fun b -> primitive_flag := b) }
-
-let typeclasses_strict = ref false
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Typeclasses";"Strict";"Resolution"];
- optread = (fun () -> !typeclasses_strict);
- optwrite = (fun b -> typeclasses_strict := b); }
-
-let typeclasses_unique = ref false
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Typeclasses";"Unique";"Instances"];
- optread = (fun () -> !typeclasses_unique);
- optwrite = (fun b -> typeclasses_unique := b); }
+let primitive_flag =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Primitive";"Projections"]
+ ~value:false
+
+let typeclasses_strict =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Typeclasses";"Strict";"Resolution"]
+ ~value:false
+
+let typeclasses_unique =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Typeclasses";"Unique";"Instances"]
+ ~value:false
let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
let _, sigma, impls, newfs, _ =
@@ -81,7 +68,8 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
let impls_env =
match i with
| Anonymous -> impls_env
- | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env
+ | Name id ->
+ Id.Map.add id (Constrintern.compute_internalization_data env sigma id Constrintern.Method t impl) impls_env
in
let d = match b with
| None -> LocalAssum (make_annot i r,t)
@@ -106,7 +94,7 @@ let compute_constructor_level evars env l =
let univ =
if is_local_assum d then
let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
- Univ.sup (univ_of_sort s) univ
+ Univ.sup (Sorts.univ_of_sort s) univ
else univ
in (EConstr.push_rel d env, univ))
l (env, Univ.Universe.sprop)
@@ -116,68 +104,123 @@ let check_anonymous_type ind =
| { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
| _ -> false
-let typecheck_params_and_fields def poly pl ps records =
+let error_parameters_must_be_named bk {CAst.loc; v=name} =
+ match bk, name with
+ | Default _, Anonymous ->
+ CErrors.user_err ?loc ~hdr:"record" (str "Record parameters must be named")
+ | _ -> ()
+
+let check_parameters_must_be_named = function
+ | CLocalDef (b, _, _) ->
+ error_parameters_must_be_named default_binder_kind b
+ | CLocalAssum (ls, bk, ce) ->
+ List.iter (error_parameters_must_be_named bk) ls
+ | CLocalPattern {CAst.loc} ->
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")
+
+(** [DataI.t] contains the information used in record interpretation,
+ it is a strict subset of [Ast.t] thus this should be
+ eventually removed or merged with [Ast.t] *)
+module DataI = struct
+ type t =
+ { name : Id.t
+ ; arity : Constrexpr.constr_expr option
+ (** declared sort for the record *)
+ ; nots : Vernacexpr.decl_notation list list
+ (** notations for fields *)
+ ; fs : Vernacexpr.local_decl_expr list
+ }
+end
+
+type projection_flags = {
+ pf_subclass: bool;
+ pf_canonical: bool;
+}
+
+(** [DataR.t] contains record data after interpretation /
+ type-inference *)
+module DataR = struct
+ type t =
+ { min_univ : Univ.Universe.t
+ ; arity : Constr.t
+ ; implfs : Impargs.manual_implicits list
+ ; fields : Constr.rel_declaration list
+ }
+end
+
+module Data = struct
+ type t =
+ { id : Id.t
+ ; idbuild : Id.t
+ ; is_coercion : bool
+ ; coers : projection_flags list
+ ; rdata : DataR.t
+ }
+end
+
+let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match arity with
+ | None ->
+ let uvarkind = Evd.univ_flexible_alg in
+ let sigma, s = Evd.new_sort_variable uvarkind sigma in
+ (sigma, template), (EConstr.mkSort s, s)
+ | Some t ->
+ let env = EConstr.push_rel_context newps env0 in
+ let poly =
+ match t with
+ | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in
+ let impls = Constrintern.empty_internalization_env in
+ let sigma, s = Constrintern.interp_type_evars ~program_mode:false env sigma ~impls t in
+ let sred = Reductionops.whd_allnolet env sigma s in
+ (match EConstr.kind sigma sred with
+ | Sort s' ->
+ let s' = EConstr.ESorts.kind sigma s' in
+ (if poly then
+ match Evd.is_sort_variable sigma s' with
+ | Some l ->
+ let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
+ (sigma, template), (s, s')
+ | None ->
+ (sigma, false), (s, s')
+ else (sigma, false), (s, s'))
+ | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
+
+type tc_result =
+ bool
+ * Impargs.manual_implicits
+ (* Part relative to closing the definitions *)
+ * UnivNames.universe_binders
+ * Entries.universes_entry
+ * Constr.rel_context
+ * DataR.t list
+
+(* ps = parameter list *)
+let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_result =
let env0 = Global.env () in
(* Special case elaboration for template-polymorphic inductives,
lower bound on introduced universes is Prop so that we do not miss
any Set <= i constraint for universes that might actually be instantiated with Prop. *)
let is_template =
- List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
+ List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
- let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
- let () =
- let error bk {CAst.loc; v=name} =
- match bk, name with
- | Default _, Anonymous ->
- user_err ?loc ~hdr:"record" (str "Record parameters must be named")
- | _ -> ()
- in
- List.iter
- (function CLocalDef (b, _, _) -> error default_binder_kind b
- | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
- | CLocalPattern {CAst.loc} ->
- Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
- in
- let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in
- let fold (sigma, template) (_, t, _, _) = match t with
- | Some t ->
- let env = EConstr.push_rel_context newps env0 in
- let poly =
- match t with
- | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in
- let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in
- let sred = Reductionops.whd_allnolet env sigma s in
- (match EConstr.kind sigma sred with
- | Sort s' ->
- let s' = EConstr.ESorts.kind sigma s' in
- (if poly then
- match Evd.is_sort_variable sigma s' with
- | Some l ->
- let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
- (sigma, template), (s, s')
- | None ->
- (sigma, false), (s, s')
- else (sigma, false), (s, s'))
- | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
- | None ->
- let uvarkind = Evd.univ_flexible_alg in
- let sigma, s = Evd.new_sort_variable uvarkind sigma in
- (sigma, template), (EConstr.mkSort s, s)
- in
- let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in
+ let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in
+ let () = List.iter check_parameters_must_be_named ps in
+ let sigma, (impls_env, ((env1,newps), imps)) =
+ Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in
+ let (sigma, template), typs =
+ List.fold_left_map (build_type_telescope newps env0) (sigma, true) records in
let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in
let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in
- let fold accu (id, _, _, _) arity r =
- EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in
+ let fold accu { DataI.name; _ } arity r =
+ EConstr.push_rel (LocalAssum (make_annot (Name name) r,arity)) accu in
let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
let impls_env =
- let ids = List.map (fun (id, _, _, _) -> id) records in
+ let ids = List.map (fun { DataI.name; _ } -> name) records in
let imps = List.map (fun _ -> imps) arities in
- compute_internalization_env env0 sigma ~impls:impls_env Inductive ids arities imps
+ Constrintern.compute_internalization_env env0 sigma ~impls:impls_env Constrintern.Inductive ids arities imps
in
let ninds = List.length arities in
let nparams = List.length newps in
- let fold sigma (_, _, nots, fs) arity =
+ let fold sigma { DataI.nots; fs; _ } arity =
interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs
in
let (sigma, data) = List.fold_left2_map fold sigma records arities in
@@ -198,12 +241,13 @@ let typecheck_params_and_fields def poly pl ps records =
else sigma, (univ, typ)
in
let (sigma, typs) = List.fold_left2_map fold sigma typs data in
+ (* TODO: Have this use Declaredef.prepare_definition *)
let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf ->
let newps = List.map (RelDecl.map_constr_het nf) newps in
- let map (impls, newfs) (univ, typ) =
- let newfs = List.map (RelDecl.map_constr_het nf) newfs in
- let typ = nf typ in
- (univ, typ, impls, newfs)
+ let map (implfs, fields) (min_univ, typ) =
+ let fields = List.map (RelDecl.map_constr_het nf) fields in
+ let arity = nf typ in
+ { DataR.min_univ; arity; implfs; fields }
in
let ans = List.map2 map data typs in
newps, ans)
@@ -212,7 +256,7 @@ let typecheck_params_and_fields def poly pl ps records =
let ubinders = Evd.universe_binders sigma in
let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
let () = List.iter (iter_constr ce) (List.rev newps) in
- ubinders, univs, template, newps, imps, ans
+ template, imps, ubinders, univs, newps, ans
type record_error =
| MissingProj of Id.t * Id.t list
@@ -293,26 +337,107 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
Termops.substl_rel_context (subst @ subst') fields
-type projection_flags = {
- pf_subclass: bool;
- pf_canonical: bool;
-}
-
(* We build projections *)
-let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields =
+
+(* TODO: refactor the declaration part here; this requires some
+ surgery as Evarutil.finalize is called too early in the path *)
+(** This builds and _declares_ a named projection, the code looks
+ tricky due to the term manipulation. It also handles declaring the
+ implicits parameters, coercion status, etc... of the projection;
+ this could be refactored as noted above by moving to the
+ higher-level declare constant API *)
+let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls
+ paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp =
+ let ccl = subst_projection fid subst ti in
+ let body, p_opt = match decl with
+ | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
+ | LocalAssum ({binder_relevance=rci},_) ->
+ (* [ccl] is defined in context [params;x:rp] *)
+ (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+ if primitive then
+ let p = Projection.Repr.make indsp
+ ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in
+ mkProj (Projection.make p true, mkRel 1), Some p
+ else
+ let ccl' = liftn 1 2 ccl in
+ let p = mkLambda (x, lift 1 rp, ccl') in
+ let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
+ let ci = Inductiveops.make_case_info env indsp rci LetStyle in
+ (* Record projections are always NoInvert because they're at
+ constant relevance *)
+ mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
+ in
+ let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+ let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
+ let entry = Declare.definition_entry ~univs ~types:projtyp proj in
+ let kind = Decls.IsDefinition kind in
+ let kn =
+ try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
+ with Type_errors.TypeError (ctx,te) as exn when not primitive ->
+ let _, info = Exninfo.capture exn in
+ Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info)
+ in
+ Declare.definition_message fid;
+ let term = match p_opt with
+ | Some p ->
+ let _ = DeclareInd.declare_primitive_projection p kn in
+ mkProj (Projection.make p false,mkRel 1)
+ | None ->
+ let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+ match decl with
+ | LocalDef (_,ci,_) when primitive -> body
+ | _ -> applist (mkConstU (kn,uinstance),proj_args)
+ in
+ let refi = GlobRef.ConstRef kn in
+ Impargs.maybe_declare_manual_implicits false refi impls;
+ if flags.pf_subclass then begin
+ let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+ ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+ end;
+ let i = if is_local_assum decl then i+1 else i in
+ (Some kn::sp_projs, i, Projection term::subst)
+
+(** [build_proj] will build a projection for each field, or skip if
+ the field is anonymous, i.e. [_ : t] *)
+let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs
+ (nfi,i,kinds,sp_projs,subst) flags decl impls =
+ let fi = RelDecl.get_name decl in
+ let ti = RelDecl.get_type decl in
+ let (sp_projs,i,subst) =
+ match fi with
+ | Anonymous ->
+ (None::sp_projs,i,NoProjection fi::subst)
+ | Name fid ->
+ try build_named_proj
+ ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid
+ subst sp_projs nfi ti i indsp mib lifted_fields x rp
+ with NotDefinable why as exn ->
+ let _, info = Exninfo.capture exn in
+ warning_or_error ~info flags.pf_subclass indsp why;
+ (None::sp_projs,i,NoProjection fi::subst)
+ in
+ (nfi - 1, i,
+ { Recordops.pk_name = fi
+ ; pk_true_proj = is_local_assum decl
+ ; pk_canonical = flags.pf_canonical } :: kinds
+ , sp_projs, subst)
+
+(** [declare_projections] prepares the common context for all record
+ projections and then calls [build_proj] for each one. *)
+let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
- let u = match ctx with
+ let uinstance = match univs with
| Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
| Monomorphic_entry ctx -> Univ.Instance.empty
in
- let paramdecls = Inductive.inductive_paramdecls (mib, u) in
- let r = mkIndU (indsp,u) in
+ let paramdecls = Inductive.inductive_paramdecls (mib, uinstance) in
+ let r = mkIndU (indsp,uinstance) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
let x = make_annot (Name binder_name) mip.mind_relevance in
- let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
+ let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
let primitive =
match mib.mind_record with
@@ -321,74 +446,44 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
in
let (_,_,kinds,sp_projs,_) =
List.fold_left3
- (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
- let fi = RelDecl.get_name decl in
- let ti = RelDecl.get_type decl in
- let (sp_projs,i,subst) =
- match fi with
- | Anonymous ->
- (None::sp_projs,i,NoProjection fi::subst)
- | Name fid ->
- try
- let ccl = subst_projection fid subst ti in
- let body, p_opt = match decl with
- | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
- | LocalAssum ({binder_relevance=rci},_) ->
- (* [ccl] is defined in context [params;x:rp] *)
- (* [ccl'] is defined in context [params;x:rp;x:rp] *)
- if primitive then
- let p = Projection.Repr.make indsp
- ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in
- mkProj (Projection.make p true, mkRel 1), Some p
- else
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 rp, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
- let ci = Inductiveops.make_case_info env indsp rci LetStyle in
- (* Record projections are always NoInvert because
- they're at constant relevance *)
- mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
- in
- let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
- let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
- let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
- let kind = Decls.IsDefinition kind in
- let kn =
- try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
- with Type_errors.TypeError (ctx,te) as exn when not primitive ->
- let _, info = Exninfo.capture exn in
- Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info)
- in
- Declare.definition_message fid;
- let term = match p_opt with
- | Some p ->
- let _ = DeclareInd.declare_primitive_projection p kn in
- mkProj (Projection.make p false,mkRel 1)
- | None ->
- let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
- match decl with
- | LocalDef (_,ci,_) when primitive -> body
- | _ -> applist (mkConstU (kn,u),proj_args)
- in
- let refi = GlobRef.ConstRef kn in
- Impargs.maybe_declare_manual_implicits false refi impls;
- if flags.pf_subclass then begin
- let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
- ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
- end;
- let i = if is_local_assum decl then i+1 else i in
- (Some kn::sp_projs, i, Projection term::subst)
- with NotDefinable why as exn ->
- let _, info = Exninfo.capture exn in
- warning_or_error ~info flags.pf_subclass indsp why;
- (None::sp_projs,i,NoProjection fi::subst)
- in
- (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+ (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs)
(List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
open Typeclasses
+let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min_univ; fields; _ }; _ } =
+ let template_candidate () =
+ (* we use some dummy values for the arities in the rel_context
+ as univs_of_constr doesn't care about localassums and
+ getting the real values is too annoying *)
+ let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+ let param_levels =
+ List.fold_left (fun levels d -> match d with
+ | LocalAssum _ -> levels
+ | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+ Univ.LSet.empty params
+ in
+ let ctor_levels = List.fold_left
+ (fun univs d ->
+ let univs =
+ RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs
+ in
+ univs)
+ param_levels fields
+ in
+ ComInductive.template_polymorphism_candidate ~ctor_levels univs params
+ (Some (Sorts.sort_of_univ min_univ))
+ in
+ match template with
+ | Some template, _ ->
+ (* templateness explicitly requested *)
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None, template ->
+ (* auto detect template *)
+ ComInductive.should_auto_template id (template && template_candidate ())
+
let load_structure i (_, structure) =
Recordops.register_structure structure
@@ -402,7 +497,8 @@ let discharge_structure (_, x) = Some x
let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s
-let inStruc : Recordops.struc_typ -> obj =
+let inStruc : Recordops.struc_typ -> Libobject.obj =
+ let open Libobject in
declare_object {(default_object "STRUCTURE") with
cache_function = cache_structure;
load_function = load_structure;
@@ -414,7 +510,22 @@ let inStruc : Recordops.struc_typ -> obj =
let declare_structure_entry o =
Lib.add_anonymous_leaf (inStruc o)
-let declare_structure ~cumulative finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data =
+(** Main record declaration part:
+
+ The entry point is [definition_structure], which will match on the
+ declared [kind] and then either follow the regular record
+ declaration path to [declare_structure] or handle the record as a
+ class declaration with [declare_class].
+
+*)
+
+(** [declare_structure] does two principal things:
+
+ - prepares and declares the low-level (mutual) inductive corresponding to [record_data]
+ - prepares and declares the corresponding record projections, mainly taken care of by
+ [declare_projections]
+*)
+let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
let nparams = List.length params in
let poly, ctx =
match univs with
@@ -426,14 +537,14 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let binder_name =
match name with
| None ->
- let map (id, _, _, _, _, _, _, _) =
+ let map { Data.id; _ } =
Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
in
Array.map_of_list map record_data
| Some n -> n
in
let ntypes = List.length record_data in
- let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) =
+ let mk_block i { Data.id; idbuild; rdata = { DataR.min_univ; arity; fields; _ }; _ } =
let nfields = List.length fields in
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
@@ -444,42 +555,10 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
mind_entry_lc = [type_constructor] }
in
let blocks = List.mapi mk_block record_data in
- let check_template (id, _, min_univ, _, _, fields, _, _) =
- let template_candidate () =
- (* we use some dummy values for the arities in the rel_context
- as univs_of_constr doesn't care about localassums and
- getting the real values is too annoying *)
- let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
- let param_levels =
- List.fold_left (fun levels d -> match d with
- | LocalAssum _ -> levels
- | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
- Univ.LSet.empty params
- in
- let ctor_levels = List.fold_left
- (fun univs d ->
- let univs =
- RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs
- in
- univs)
- param_levels fields
- in
- ComInductive.template_polymorphism_candidate ~ctor_levels univs params
- (Some (Sorts.sort_of_univ min_univ))
- in
- match template with
- | Some template, _ ->
- (* templateness explicitly requested *)
- if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
- template
- | None, template ->
- (* auto detect template *)
- ComInductive.should_auto_template id (template && template_candidate ())
- in
- let template = List.for_all check_template record_data in
+ let template = List.for_all (check_template ~template ~univs ~poly ~params) record_data in
let primitive =
- !primitive_flag &&
- List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
+ primitive_flag () &&
+ List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data
in
let mie =
{ mind_entry_params = params;
@@ -493,15 +572,15 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
}
in
let impls = List.map (fun _ -> paramimpls, []) record_data in
- let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
- ~primitive_expected:!primitive_flag
+ let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubind impls
+ ~primitive_expected:(primitive_flag ())
in
- let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
+ let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } =
let rsp = (kn, i) in (* This is ind path of idstruc *)
let cstr = (rsp, 1) in
- let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
+ let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in
let build = GlobRef.ConstructRef cstr in
- let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
+ let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in
let npars = Inductiveops.inductive_nparams (Global.env()) rsp in
let struc = {
Recordops.s_CONST = cstr;
@@ -519,68 +598,103 @@ let implicits_of_context ctx =
List.map (fun name -> CAst.make (Some (name,true)))
(List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
-let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
- template fieldimpls fields ?(kind=Decls.StructureComponent) coers =
- let fieldimpls =
+let build_class_constant ~univs ~rdata field implfs params paramimpls coers binder id proj_name =
+ let class_body = it_mkLambda_or_LetIn field params in
+ let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in
+ let class_entry =
+ Declare.definition_entry ~types:class_type ~univs class_body in
+ let cst = Declare.declare_constant ~name:id
+ (Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
+ in
+ let inst, univs = match univs with
+ | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
+ | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty
+ in
+ let cstu = (cst, inst) in
+ let inst_type = appvectc (mkConstU cstu)
+ (Termops.rel_vect 0 (List.length params)) in
+ let proj_type =
+ it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in
+ let proj_body =
+ it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
+ let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
+ let proj_cst = Declare.declare_constant ~name:proj_name
+ (Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
+ in
+ let cref = GlobRef.ConstRef cst in
+ Impargs.declare_manual_implicits false cref paramimpls;
+ Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs);
+ Classes.set_typeclass_transparency (EvalConstRef cst) false false;
+ let sub = List.hd coers in
+ let m = {
+ meth_name = Name proj_name;
+ meth_info = sub;
+ meth_const = Some proj_cst;
+ } in
+ [cref, [m]]
+
+let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name =
+ let record_data =
+ { Data.id
+ ; idbuild
+ ; is_coercion = false
+ ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields
+ ; rdata
+ } in
+ let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs paramimpls
+ params template ~kind:Decls.Method ~name:[|binder_name|] [record_data]
+ in
+ let map ind =
+ let map decl b y = {
+ meth_name = RelDecl.get_name decl;
+ meth_info = b;
+ meth_const = y;
+ } in
+ let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in
+ GlobRef.IndRef ind, l
+ in
+ List.map map inds
+
+(** [declare_class] will prepare and declare a [Class]. This is done in
+ 2 steps:
+
+ 1. two markely different paths are followed depending on whether the
+ class declaration refers to a constant "definitional classes" or to
+ a record, that is to say:
+
+ Class foo := bar : T.
+
+ which is equivalent to
+
+ Definition foo := T.
+ Definition bar (x:foo) : T := x.
+ Existing Class foo.
+
+ vs
+
+ Class foo := { ... }.
+
+ 2. declare the class, using the information from 1. in the form of [Classes.typeclass]
+
+ *)
+let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params
+ rdata template ?(kind=Decls.StructureComponent) coers =
+ let implfs =
(* Make the class implicit in the projections, and the params if applicable. *)
let impls = implicits_of_context params in
- List.map (fun x -> impls @ x) fieldimpls
+ List.map (fun x -> impls @ x) rdata.DataR.implfs
in
+ let rdata = { rdata with DataR.implfs } in
let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
+ let fields = rdata.DataR.fields in
let data =
match fields with
- | [LocalAssum ({binder_name=Name proj_name} as binder, field)
- | LocalDef ({binder_name=Name proj_name} as binder, _, field)] when def ->
+ | [ LocalAssum ({binder_name=Name proj_name} as binder, field)
+ | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def ->
let binder = {binder with binder_name=Name binder_name} in
- let class_body = it_mkLambda_or_LetIn field params in
- let class_type = it_mkProd_or_LetIn arity params in
- let class_entry =
- Declare.definition_entry ~types:class_type ~univs class_body in
- let cst = Declare.declare_constant ~name:id
- (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
- in
- let inst, univs = match univs with
- | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
- | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty
- in
- let cstu = (cst, inst) in
- let inst_type = appvectc (mkConstU cstu)
- (Termops.rel_vect 0 (List.length params)) in
- let proj_type =
- it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in
- let proj_body =
- it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
- let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
- let proj_cst = Declare.declare_constant ~name:proj_name
- (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
- in
- let cref = GlobRef.ConstRef cst in
- Impargs.declare_manual_implicits false cref paramimpls;
- Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
- Classes.set_typeclass_transparency (EvalConstRef cst) false false;
- let sub = List.hd coers in
- let m = {
- meth_name = Name proj_name;
- meth_info = sub;
- meth_const = Some proj_cst;
- } in
- [cref, [m]]
+ build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name
| _ ->
- let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
- List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
- let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
- params template ~kind:Decls.Method ~name:[|binder_name|] record_data
- in
- let map ind =
- let map decl b y = {
- meth_name = RelDecl.get_name decl;
- meth_info = b;
- meth_const = y;
- } in
- let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in
- GlobRef.IndRef ind, l
- in
- List.map map inds
+ build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name
in
let univs, params, fields =
match univs with
@@ -598,8 +712,8 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
let k =
{ cl_univs = univs;
cl_impl = impl;
- cl_strict = !typeclasses_strict;
- cl_unique = !typeclasses_unique;
+ cl_strict = typeclasses_strict ();
+ cl_unique = typeclasses_unique ();
cl_context = params;
cl_props = fields;
cl_projs = projs }
@@ -610,7 +724,6 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
in
List.map map data
-
let add_constant_class env sigma cst =
let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in
let r = (Environ.lookup_constant cst env).const_relevance in
@@ -623,8 +736,8 @@ let add_constant_class env sigma cst =
cl_context = ctx;
cl_props = [LocalAssum (make_annot Anonymous r, t)];
cl_projs = [];
- cl_strict = !typeclasses_strict;
- cl_unique = !typeclasses_unique
+ cl_strict = typeclasses_strict ();
+ cl_unique = typeclasses_unique ()
}
in
Classes.add_class env sigma tc;
@@ -645,8 +758,8 @@ let add_inductive_class env sigma ind =
cl_context = ctx;
cl_props = [LocalAssum (make_annot Anonymous r, ty)];
cl_projs = [];
- cl_strict = !typeclasses_strict;
- cl_unique = !typeclasses_unique }
+ cl_strict = typeclasses_strict ();
+ cl_unique = typeclasses_unique () }
in
Classes.add_class env sigma k
@@ -667,14 +780,33 @@ let declare_existing_class g =
open Vernacexpr
+module Ast = struct
+ type t =
+ { name : Names.lident
+ ; is_coercion : coercion_flag
+ ; binders: local_binder_expr list
+ ; cfs : (local_decl_expr * record_field_attr) list
+ ; idbuild : Id.t
+ ; sort : constr_expr option
+ }
+
+ let to_datai { name; is_coercion; cfs; idbuild; sort } =
+ let fs = List.map fst cfs in
+ { DataI.name = name.CAst.v
+ ; arity = sort
+ ; nots = List.map (fun (_, { rf_notation }) -> rf_notation) cfs
+ ; fs
+ }
+end
+
let check_unique_names records =
let extract_name acc (rf_decl, _) = match rf_decl with
Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc
| Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc
| _ -> acc in
let allnames =
- List.fold_left (fun acc (_, id, _, cfs, _, _) ->
- id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
+ List.fold_left (fun acc { Ast.name; cfs; _ } ->
+ name.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
in
match List.duplicates Id.equal allnames with
| [] -> ()
@@ -682,19 +814,15 @@ let check_unique_names records =
let check_priorities kind records =
let isnot_class = match kind with Class false -> false | _ -> true in
- let has_priority (_, _, _, cfs, _, _) =
+ let has_priority { Ast.cfs; _ } =
List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
in
if isnot_class && List.exists has_priority records then
user_err Pp.(str "Priorities only allowed for type class substructures")
let extract_record_data records =
- let map (is_coe, id, _, cfs, idbuild, s) =
- let fs = List.map fst cfs in
- id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs
- in
- let data = List.map map records in
- let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
+ let data = List.map Ast.to_datai records in
+ let pss = List.map (fun { Ast.binders; _ } -> binders) records in
let ps = match pss with
| [] -> CErrors.anomaly (str "Empty record block")
| ps :: rem ->
@@ -708,43 +836,66 @@ let extract_record_data records =
in
ps, data
-(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
- list telling if the corresponding fields must me declared as coercions
- or subinstances. *)
-let definition_structure udecl kind ~template ~cumulative ~poly finite records =
+(* declaring structures, common data to refactor *)
+let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def records data =
+ let { Ast.name; cfs; idbuild; _ }, rdata = match records, data with
+ | [r], [d] -> r, d
+ | _, _ ->
+ CErrors.user_err (str "Mutual definitional classes are not handled")
+ in
+ let coers = List.map (fun (_, { rf_subclass; rf_priority }) ->
+ match rf_subclass with
+ | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None}
+ | Vernacexpr.NoInstance -> None)
+ cfs
+ in
+ declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild
+ impargs params rdata template coers
+
+let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data =
+ let adjust_impls impls = impargs @ [CAst.make None] @ impls in
+ let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
+ (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *)
+ let map rdata { Ast.name; is_coercion; cfs; idbuild; _ } =
+ let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
+ { pf_subclass =
+ (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
+ pf_canonical = rf_canonical })
+ cfs
+ in
+ { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers }
+ in
+ let data = List.map2 map data records in
+ let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in
+ List.map (fun ind -> GlobRef.IndRef ind) inds
+
+(** [fs] corresponds to fields and [ps] to parameters; [coers] is a
+ list telling if the corresponding fields must me declared as coercions
+ or subinstances. *)
+let definition_structure udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) =
let () = check_unique_names records in
let () = check_priorities kind records in
let ps, data = extract_record_data records in
- let ubinders, univs, auto_template, params, implpars, data =
+ let auto_template, impargs, ubind, univs, params, data =
+ (* In theory we should be able to use
+ [Notation.with_notation_protection], due to the call to
+ Metasyntax.set_notation_for_interpretation, however something
+ is messing state beyond that.
+ *)
Vernacstate.System.protect (fun () ->
typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
let template = template, auto_template in
match kind with
| Class def ->
- let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with
- | [r], [d] -> r, d
- | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
- in
- let coers = List.map (fun (_, { rf_subclass=coe; rf_priority=pri }) ->
- match coe with
- | Vernacexpr.BackInstance -> Some {hint_priority = pri ; hint_pattern = None}
- | Vernacexpr.NoInstance -> None)
- cfs
- in
- declare_class def cumulative ubinders univs id.CAst.v idbuild
- implpars params univ arity template implfs fields coers
- | _ ->
- let map impls = implpars @ [CAst.make None] @ impls in
- let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
- let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
- let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
- { pf_subclass =
- (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
- pf_canonical = rf_canonical })
- cfs
- in
- id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe
- in
- let data = List.map2 map data records in
- let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in
- List.map (fun ind -> GlobRef.IndRef ind) inds
+ class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data
+ | Inductive_kw | CoInductive | Variant | Record | Structure ->
+ regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data
+
+module Internal = struct
+ type nonrec projection_flags = projection_flags = {
+ pf_subclass: bool;
+ pf_canonical: bool;
+ }
+ let declare_projections = declare_projections
+ let declare_structure_entry = declare_structure_entry
+end
diff --git a/vernac/record.mli b/vernac/record.mli
index 38a622977a..ffcae2975e 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -12,22 +12,16 @@ open Names
open Vernacexpr
open Constrexpr
-val primitive_flag : bool ref
-
-type projection_flags = {
- pf_subclass: bool;
- pf_canonical: bool;
-}
-
-val declare_projections :
- inductive ->
- Entries.universes_entry ->
- ?kind:Decls.definition_object_kind ->
- Id.t ->
- projection_flags list ->
- Impargs.manual_implicits list ->
- Constr.rel_context ->
- Recordops.proj_kind list * Constant.t option list
+module Ast : sig
+ type t =
+ { name : Names.lident
+ ; is_coercion : coercion_flag
+ ; binders: local_binder_expr list
+ ; cfs : (local_decl_expr * record_field_attr) list
+ ; idbuild : Id.t
+ ; sort : constr_expr option
+ }
+end
val definition_structure
: universe_decl_expr option
@@ -36,14 +30,29 @@ val definition_structure
-> cumulative:bool
-> poly:bool
-> Declarations.recursivity_kind
- -> (coercion_flag *
- Names.lident *
- local_binder_expr list *
- (local_decl_expr * record_field_attr) list *
- Id.t * constr_expr option) list
+ -> Ast.t list
-> GlobRef.t list
val declare_existing_class : GlobRef.t -> unit
-(** Used by elpi *)
-val declare_structure_entry : Recordops.struc_typ -> unit
+(* Implementation internals, consult Coq developers before using;
+ current user Elpi, see https://github.com/LPCIC/coq-elpi/pull/151 *)
+module Internal : sig
+ type projection_flags = {
+ pf_subclass: bool;
+ pf_canonical: bool;
+ }
+
+ val declare_projections
+ : Names.inductive
+ -> Entries.universes_entry
+ -> ?kind:Decls.definition_object_kind
+ -> Names.Id.t
+ -> projection_flags list
+ -> Impargs.manual_implicits list
+ -> Constr.rel_context
+ -> Recordops.proj_kind list * Names.Constant.t option list
+
+ val declare_structure_entry : Recordops.struc_typ -> unit
+
+end
diff --git a/vernac/search.ml b/vernac/search.ml
index abefeab779..501e5b1a91 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -216,18 +216,16 @@ let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
let search_filter query gr kind env sigma typ = match query with
| GlobSearchSubPattern (where,head,pat) ->
let open Context.Rel.Declaration in
- let collect_hyps ctx =
- List.fold_left (fun acc d -> match get_value d with
- | None -> get_type d :: acc
- | Some b -> b :: get_type d :: acc) [] ctx in
+ let rec collect env hyps typ =
+ match Constr.kind typ with
+ | LetIn (na,b,t,c) -> collect (push_rel (LocalDef (na,b,t)) env) ((env,b) :: (env,t) :: hyps) c
+ | Prod (na,t,c) -> collect (push_rel (LocalAssum (na,t)) env) ((env,t) :: hyps) c
+ | _ -> (hyps,(env,typ)) in
let typl= match where with
- | InHyp -> collect_hyps (fst (Term.decompose_prod_assum typ))
- | InConcl -> [snd (Term.decompose_prod_assum typ)]
- | Anywhere ->
- if head then
- let ctx, ccl = Term.decompose_prod_assum typ in ccl :: collect_hyps ctx
- else [typ] in
- List.exists (fun typ ->
+ | InHyp -> fst (collect env [] typ)
+ | InConcl -> [snd (collect env [] typ)]
+ | Anywhere -> if head then let hyps, ccl = collect env [] typ in ccl :: hyps else [env,typ] in
+ List.exists (fun (env,typ) ->
let f =
if head then Constr_matching.is_matching_head
else Constr_matching.is_matching_appsubterm ~closed:false in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3ced38d6ea..6a09250627 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,14 +57,16 @@ module DefAttributes = struct
program : bool;
deprecated : Deprecation.t option;
canonical_instance : bool;
+ using : Vernacexpr.section_subset_expr option;
}
let parse f =
let open Attributes in
- let (((locality, deprecated), polymorphic), program), canonical_instance =
- parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
+ let ((((locality, deprecated), polymorphic), program), canonical_instance), using =
+ parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f
in
- { polymorphic; program; locality; deprecated; canonical_instance }
+ let using = Option.map Proof_using.using_from_string using in
+ { polymorphic; program; locality; deprecated; canonical_instance; using }
end
let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -496,6 +498,25 @@ let program_inference_hook env sigma ev =
user_err Pp.(str "The statement obligations could not be resolved \
automatically, write a statement definition first.")
+let vernac_set_used_variables ~pstate e : Declare.Proof.t =
+ let env = Global.env () in
+ let sigma, _ = Declare.Proof.get_current_context pstate in
+ let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
+ let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+ let l = Proof_using.process_expr env sigma e tys in
+ let vars = Environ.named_context env in
+ List.iter (fun id ->
+ if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
+ user_err ~hdr:"vernac_set_used_variables"
+ (str "Unknown variable: " ++ Id.print id))
+ l;
+ let _, pstate = Declare.Proof.set_used_variables pstate l in
+ pstate
+let vernac_set_used_variables_opt ?using pstate =
+ match using with
+ | None -> pstate
+ | Some expr -> vernac_set_used_variables ~pstate expr
+
(* XXX: Interpretation of lemma command, duplication with ComFixpoint
/ ComDefinition ? *)
let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
@@ -525,25 +546,28 @@ let post_check_evd ~udecl ~poly evd =
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
-let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
+let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
let env0 = Global.env () in
let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let decl = fst (List.hd thms) in
- let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
+ let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in
let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
let evd = Evd.minimize_universes evd in
- match mut_analysis with
- | RecLemmas.NonMutual thm ->
- let thm = Declare.CInfo.to_constr evd thm in
- let evd = post_check_evd ~udecl ~poly evd in
- let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
- Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
- | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
- let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
- let evd = post_check_evd ~udecl ~poly evd in
- let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
- Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+ let pstate =
+ match mut_analysis with
+ | RecLemmas.NonMutual thm ->
+ let thm = Declare.CInfo.to_constr evd thm in
+ let evd = post_check_evd ~udecl ~poly evd in
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+ Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
+ | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
+ let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
+ let evd = post_check_evd ~udecl ~poly evd in
+ let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+ Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+ in
+ vernac_set_used_variables_opt ?using pstate
let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
| Coercion ->
@@ -583,7 +607,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let program_mode = atts.program in
let poly = atts.polymorphic in
let name = vernac_definition_name lid local in
- start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
+ start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
@@ -604,7 +628,7 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_
else
let () =
ComDefinition.do_definition ~name:name.v
- ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
+ ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
pm
(* NB: pstate argument to use combinators easily *)
@@ -613,7 +637,7 @@ let vernac_start_proof ~atts kind l =
let scope = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
- start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
+ start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
| Admitted ->
@@ -639,6 +663,8 @@ let vernac_assumption ~atts discharge kind l nl =
match scope with
| Global _ -> Dumpglob.dump_definition lid false "ax"
| Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+ if Option.has_some atts.using then
+ Attributes.unsupported_attributes ["using",VernacFlagEmpty];
ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
let is_polymorphic_inductive_cumulativity =
@@ -689,16 +715,16 @@ let should_treat_as_uniform () =
else ComInductive.NonUniformParameters
let vernac_record ~template udecl ~cumulative k ~poly finite records =
- let map ((coe, id), binders, sort, nameopt, cfs) =
- let const = match nameopt with
- | None -> Nameops.add_prefix "Build_" id.v
+ let map ((is_coercion, name), binders, sort, nameopt, cfs) =
+ let idbuild = match nameopt with
+ | None -> Nameops.add_prefix "Build_" name.v
| Some lid ->
let () = Dumpglob.dump_definition lid false "constr" in
lid.v
in
let () =
if Dumpglob.dump () then
- let () = Dumpglob.dump_definition id false "rec" in
+ let () = Dumpglob.dump_definition name false "rec" in
let iter (x, _) = match x with
| Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
Dumpglob.dump_definition (make ?loc id) false "proj"
@@ -706,7 +732,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records =
in
List.iter iter cfs
in
- coe, id, binders, cfs, const, sort
+ Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort }
in
let records = List.map map records in
ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records)
@@ -842,16 +868,17 @@ let vernac_fixpoint_interactive ~atts discharge l =
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
CErrors.user_err Pp.(str"Program Fixpoint requires a body");
- ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
+ vernac_set_used_variables_opt ?using:atts.using
+ (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l)
let vernac_fixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
(* XXX: Switch to the attribute system and match on ~atts *)
- ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l
+ ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
else
- let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in
+ let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
pm
let vernac_cofixpoint_common ~atts discharge l =
@@ -864,15 +891,16 @@ let vernac_cofixpoint_interactive ~atts discharge l =
let scope = vernac_cofixpoint_common ~atts discharge l in
if atts.program then
CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
- ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
+ vernac_set_used_variables_opt ?using:atts.using
+ (ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l)
let vernac_cofixpoint ~atts ~pm discharge l =
let open DefAttributes in
let scope = vernac_cofixpoint_common ~atts discharge l in
if atts.program then
- ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l
+ ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
else
- let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in
+ let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
pm
let vernac_scheme l =
@@ -957,9 +985,15 @@ let interp_filter_in m = function
let vernac_import export refl =
let import_mod (qid,f) =
- let m = try Nametab.locate_module qid
+ let loc = qid.loc in
+ let m = try
+ let m = Nametab.locate_module qid in
+ let () = if Modops.is_functor (Global.lookup_module m).Declarations.mod_type
+ then CErrors.user_err ?loc Pp.(str "Cannot import functor " ++ pr_qualid qid ++ str".")
+ in
+ m
with Not_found ->
- CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
+ CErrors.user_err ?loc Pp.(str "Cannot find module " ++ pr_qualid qid)
in
let f = interp_filter_in m f in
Declaremods.import_module f ~export m
@@ -1223,21 +1257,6 @@ let vernac_set_end_tac ~pstate tac =
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
Declare.Proof.set_endline_tactic tac pstate
-let vernac_set_used_variables ~pstate e : Declare.Proof.t =
- let env = Global.env () in
- let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
- let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
- let tys = List.map EConstr.Unsafe.to_constr tys in
- let l = Proof_using.process_expr env e tys in
- let vars = Environ.named_context env in
- List.iter (fun id ->
- if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
- user_err ~hdr:"vernac_set_used_variables"
- (str "Unknown variable: " ++ Id.print id))
- l;
- let _, pstate = Declare.Proof.set_used_variables pstate l in
- pstate
-
(*****************************)
(* Auxiliary file management *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 11:58:44 +0000