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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open Entries
(* Constr generation and manipulation *)
type id = Names.variable
let mkId = Names.Id.of_string
type name = Names.Name.t
let name_of_id i = Names.Name i
let mkName s =
let id = mkId s in
name_of_id id
let string_of_name = function
Names.Name id -> Names.Id.to_string id
| _ -> failwith "unnamed rel"
type constr = Constr.t
type types = Constr.types
let eq_constr = Constr.equal
let hash_constr = Constr.hash
let mkProp = Constr.mkProp
let mkConst = Constr.mkConst
let mkVar = Constr.mkVar
let mkRel = Constr.mkRel
let isRel = Constr.isRel
let destRel = Constr.destRel
let lift = Vars.lift
let mkApp = Constr.mkApp
let decompose_app = Constr.decompose_app
let mkLambda = Constr.mkLambda
let mkProd = Constr.mkProd
let mkLetIn = Constr.mkLetIn
let pr_constr_env env = Printer.pr_constr_env env Evd.empty
let pr_constr = pr_constr_env Environ.empty_env
let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c ->
let env = Global.env () in
let evd = Evd.from_env env in
let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in
{ Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
Safe_typing.empty_private_constants);
const_entry_secctx = None;
const_entry_feedback = None;
const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
const_entry_universes = Evd.const_univ_entry ~poly:false evd;
const_entry_opaque = false;
const_entry_inline_code = false }
let mkTConst c noc ty =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in
{ const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
Safe_typing.empty_private_constants);
const_entry_secctx = None;
const_entry_feedback = None;
const_entry_type = Some ty;
const_entry_universes = Evd.const_univ_entry ~poly:false evd;
const_entry_opaque = false;
const_entry_inline_code = false }
(* TODO : Set -> Type *)
let declare_new_type t =
let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
Constr.mkVar t
let declare_new_variable v constr_t =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
Constr.mkVar v
let declare_constant n c =
Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
type cast_kind = Constr.cast_kind
let vmcast = Constr.VMcast
let mkCast = Constr.mkCast
(* EConstr *)
type econstr = EConstr.t
let econstr_of_constr = EConstr.of_constr
(* Modules *)
let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n
let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
(* Int63 *)
let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]]
(* 31-bits integers are "called" 63 bits (this is sound) *)
let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]]
let cD0 = gen_constant int31_module "D0"
let cD1 = gen_constant int31_module "D1"
let cI31 = gen_constant int31_module "I31"
let mkInt : int -> constr = fun i ->
let a = Array.make 31 (Lazy.force cD0) in
let j = ref i in
let k = ref 30 in
while !j <> 0 do
if !j land 1 = 1 then a.(!k) <- Lazy.force cD1;
j := !j lsr 1;
decr k
done;
mkApp (Lazy.force cI31, a)
let cint = gen_constant int31_module "int31"
(* PArray *)
let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]]
let cmake = gen_constant parray_modules "make"
let cset = gen_constant parray_modules "set"
let max_array_size : int = 4194302
let mkArray : Constr.types * Constr.t array -> Constr.t =
fun (ty, a) ->
let l = (Array.length a) - 1 in
snd (Array.fold_left (fun (i,acc) c ->
let acc' =
if i = l then
acc
else
mkApp (Lazy.force cset, [|ty; acc; mkInt i; c|]) in
(i+1,acc')
) (0, mkApp (Lazy.force cmake, [|ty; mkInt l; a.(l)|])) a)
(* Traces *)
(* WARNING: side effect on r! *)
let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
let rec mkTrace s =
if s = size then
mkApp (Lazy.force cnil, [|step|])
else (
r := next !r;
let st = step_to_coq !r in
mkApp (Lazy.force ccons, [|step; st; mkTrace (s+1)|])
) in
mkApp (Lazy.force cpair, [|mkApp (Lazy.force clist, [|step|]); step; mkTrace 0; def_step|])
(* Micromega *)
module Micromega_plugin_Micromega = Micromega_plugin.Micromega
module Micromega_plugin_Mutils = Mutils_full
module Micromega_plugin_Certificate = Micromega_plugin.Certificate
module Micromega_plugin_Coq_micromega = Coq_micromega_full
let micromega_coq_proofTerm =
(* Cannot contain evars *)
lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm)))
let micromega_dump_proof_term p =
(* Cannot contain evars *)
EConstr.Unsafe.to_constr (Micromega_plugin_Coq_micromega.dump_proof_term p)
(* Tactics *)
type tactic = unit Proofview.tactic
let tclTHEN = Tacticals.New.tclTHEN
let tclTHENLAST = Tacticals.New.tclTHENLAST
let assert_before n c = Tactics.assert_before n (EConstr.of_constr c)
let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c)
let mk_tactic tac =
Proofview.Goal.nf_enter (fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let t = Proofview.Goal.concl gl in
let t = EConstr.to_constr sigma t in (* The goal should not contain uninstanciated evars *)
tac env sigma t
)
let set_evars_tac noc =
mk_tactic (
fun env sigma _ ->
let sigma, _ = Typing.type_of env sigma (EConstr.of_constr noc) in
Proofview.Unsafe.tclEVARS sigma)
(* Other differences between the two versions of Coq *)
type constr_expr = Constrexpr.constr_expr
let error s = CErrors.user_err (Pp.str s)
let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s
let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
let destruct_rel_decl r = Context.Rel.Declaration.get_name r,
Context.Rel.Declaration.get_type r
(* Cannot contain evars since it comes from a Constr.t *)
let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst |> EConstr.Unsafe.to_constr
let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr
let constrextern_extern_constr c =
let env = Global.env () in
Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c)
let get_rel_dec_name = function
| Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n
let retyping_get_type_of env sigma c =
(* Cannot contain evars since it comes from a Constr.t *)
EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))
let vm_conv = Vconv.vm_conv
(* Cannot contain evars since it comes from a Constr.t *)
let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t))
|
