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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Pp
open Util
open Constr
open Environ
open Entries
open Redexpr
open Declare
open Constrintern
open Pretyping
open Context.Rel.Declaration
(* Commands of the interface: Constant definitions *)
let rec under_binders env sigma f n c =
if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
match Constr.kind c with
| Lambda (x,t,c) ->
mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
| LetIn (x,b,t,c) ->
mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
| _ -> assert false
let red_constant_entry n ce sigma = function
| None -> ce
| Some red ->
let proof_out = ce.const_entry_body in
let env = Global.env () in
let (redfun, _) = reduction_of_red_expr env red in
let redfun env sigma c =
let (_, c) = redfun env sigma c in
EConstr.Unsafe.to_constr c
in
{ ce with const_entry_body = Future.chain proof_out
(fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
let warn_implicits_in_term =
CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
(fun () ->
strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.")
let check_imps ~impsty ~impsbody =
let b =
try
List.for_all (fun (key, (va:bool*bool*bool)) ->
(* Pervasives.(=) is OK for this type *)
Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va)
impsbody
with Not_found -> false
in
if not b then warn_implicits_in_term ()
let interp_definition pl bl poly red_option c ctypopt =
let open EConstr in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
(* Build the parameters *)
let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
(* Build the type *)
let evd, tyopt = Option.fold_left_map
(interp_type_evars_impls ~impls env_bl)
evd ctypopt
in
(* Build the body, and merge implicits from parameters and from type/body *)
let evd, c, imps, tyopt =
match tyopt with
| None ->
let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in
evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
| Some (ty, impsty) ->
let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
check_imps ~impsty ~impsbody;
evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
in
(* universe minimization *)
let evd = Evd.minimize_universes evd in
(* Substitute evars and universes, and add parameters.
Note: in program mode some evars may remain. *)
let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
(* Keep only useful universes. *)
let uvars_fold uvars c =
Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
in
let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
let evd = Evd.restrict_universe_context evd uvars in
(* Check we conform to declared universes *)
let uctx = Evd.check_univ_decl ~poly evd decl in
(* We're done! *)
let ce = definition_entry ?types:tyopt ~univs:uctx c in
(red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
let check_definition (ce, evd, _, imps) =
let env = Global.env () in
let empty_sigma = Evd.from_env env in
check_evars_are_solved env evd empty_sigma;
ce
let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
let (ce, evd, univdecl, imps as def) =
interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
if program_mode then
let env = Global.env () in
let (c,ctx), sideff = Future.force ce.const_entry_body in
assert(Safe_typing.empty_private_constants = sideff);
assert(Univ.ContextSet.is_empty ctx);
let typ = match ce.const_entry_type with
| Some t -> t
| None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
in
Obligations.check_evars env evd;
let obls, _, c, cty =
Obligations.eterm_obligations env ident evd 0 c typ
in
let ctx = Evd.evar_universe_context evd in
let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
ignore(Obligations.add_definition
ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
|
