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
|
(************************************************************************)
(* * 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 Names
let declare id entry =
let _ : Constant.t =
Declare.declare_constant ~name:id ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry)
in
Flags.if_verbose Feedback.msg_info Pp.(Id.print id ++ str " is declared")
let do_primitive id udecl prim typopt =
if Global.sections_are_opened () then
CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
let loc = id.CAst.loc in
let id = id.CAst.v in
match typopt with
| None ->
if Option.has_some udecl then
CErrors.user_err ?loc
Pp.(strbrk "Cannot use a universe declaration without a type when declaring primitives.");
declare id {Entries.prim_entry_type = None; prim_entry_content = prim}
| Some typ ->
let env = Global.env () 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
let evd, (typ,impls) =
Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env)
env evd typ
in
let evd = try Evarconv.unify_delay env evd typ expected_typ
with Evarconv.UnableToUnify (evd,e) as exn ->
let _, info = Exninfo.capture exn in
Exninfo.iraise (Pretype_errors.(
PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info))
in
Pretyping.check_evars_are_solved ~program_mode:false env evd;
let evd = Evd.minimize_universes evd in
let uvars = EConstr.universes_of_constr evd typ in
let evd = Evd.restrict_universe_context evd uvars in
let typ = EConstr.to_constr evd typ in
let univs = Evd.check_univ_decl ~poly:(not (Univ.AUContext.is_empty auctx)) evd udecl in
let entry = {
Entries.prim_entry_type = Some (typ,univs);
prim_entry_content = prim;
}
in
declare id entry
|
