1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Declare
open Impargs
type locality = Discharge | Global of Declare.import_status
(* Hooks naturally belong here as they apply to both definitions and lemmas *)
module Hook = struct
module S = struct
type t =
{ uctx : UState.t
(** [ustate]: universe constraints obtained when the term was closed *)
; obls : (Names.Id.t * Constr.t) list
(** [(n1,t1),...(nm,tm)]: association list between obligation
name and the corresponding defined term (might be a constant,
but also an arbitrary term in the Expand case of obligations) *)
; scope : locality
(** [locality]: Locality of the original declaration *)
; dref : Names.GlobRef.t
(** [ref]: identifier of the original declaration *)
}
end
type t = (S.t -> unit) CEphemeron.key
let make hook = CEphemeron.create hook
let call ?hook ?fix_exn x =
try Option.iter (fun hook -> CEphemeron.get hook x) hook
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
let e = Option.cata (fun fix -> fix e) e fix_exn in
Exninfo.iraise e
end
(* Locality stuff *)
let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
let fix_exn = Declare.Internal.get_fix_exn ce in
let should_suggest = ce.Declare.proof_entry_opaque &&
Option.is_empty ce.Declare.proof_entry_secctx in
let dref = match scope with
| Discharge ->
let () = declare_variable ~name ~kind (SectionLocalDef ce) in
if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
Names.GlobRef.VarRef name
| Global local ->
let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
let gr = Names.GlobRef.ConstRef kn in
if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
let () = DeclareUniv.declare_univ_binders gr ubind in
gr
in
let () = maybe_declare_manual_implicits false dref impargs in
let () = definition_message name in
begin
match hook_data with
| None -> ()
| Some (hook, uctx, obls) ->
Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref }
end;
dref
let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes =
match possible_indexes with
| Some possible_indexes ->
let env = Global.env() in
let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixnames in
vars, fixdecls, Some indexes
| None ->
let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in
let vars = Vars.universes_of_constr (List.hd fixdecls) in
vars, fixdecls, None
let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixnames fixtypes fiximps =
let vars, fixdecls, indexes =
mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
let ubind, univs =
(* XXX: Note that obligations don't do this, is that a bug? *)
if restrict_ucontext
then
let evd = Evd.from_ctx uctx in
let evd = Evd.restrict_universe_context evd vars in
let univs = Evd.check_univ_decl ~poly evd udecl in
Evd.universe_binders evd, univs
else
let univs = UState.univ_entry ~poly uctx in
UnivNames.empty_binders, univs
in
let csts = CList.map4
(fun name body types impargs ->
let ce = Declare.definition_entry ~opaque ~types ~univs body in
declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
fixnames fixdecls fixtypes fiximps
in
let isfix = Option.is_empty possible_indexes in
Declare.recursive_message isfix indexes fixnames;
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
csts
let warn_let_as_axiom =
CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
spc () ++ strbrk "declared as an axiom.")
let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
let local = match scope with
| Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
| Global local -> local
in
let kind = Decls.(IsAssumption Conjectural) in
let decl = Declare.ParameterEntry pe in
let kn = Declare.declare_constant ~name ~local ~kind decl in
let dref = Names.GlobRef.ConstRef kn in
let () = Impargs.maybe_declare_manual_implicits false dref impargs in
let () = Declare.assumption_message name in
let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in
let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in
dref
(* Preparing proof entries *)
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma =
check_definition_evars ~allow_evars sigma;
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
sigma (fun nf -> nf body, Option.map nf types)
in
let univs = Evd.check_univ_decl ~poly sigma udecl in
sigma, definition_entry ?opaque ?inline ?types ~univs body
let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
check_definition_evars ~allow_evars sigma;
let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
sigma (fun nf -> nf types)
in
let univs = Evd.check_univ_decl ~poly sigma udecl in
sigma, (None(*proof using*), (typ, univs), None(*inline*))
|
