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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open Entries
open Coqlib
(* Constr generation and manipulation *)
type id = Names.identifier
let mkId = Names.id_of_string
type name = Names.name
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.string_of_id id
| _ -> failwith "unnamed rel"
type constr = Term.constr
type types = Term.types
let eq_constr = Term.eq_constr
let hash_constr = Term.hash_constr
let mkProp = Term.mkProp
let mkConst = Term.mkConst
let mkVar = Term.mkVar
let mkRel = Term.mkRel
let isRel = Term.isRel
let destRel = Term.destRel
let lift = Term.lift
let mkApp = Term.mkApp
let decompose_app = Term.decompose_app
let mkLambda = Term.mkLambda
let mkProd = Term.mkProd
let mkLetIn = Term.mkLetIn
let pr_constr_env = Printer.pr_constr_env
let pr_constr = Printer.pr_constr
let dummy_loc = Pp.dummy_loc
let mkUConst c =
{ const_entry_body = c;
const_entry_type = None;
const_entry_secctx = None;
const_entry_opaque = false;
const_entry_inline_code = false}
let mkTConst c _ ty =
{ const_entry_body = c;
const_entry_type = Some ty;
const_entry_secctx = None;
const_entry_opaque = false;
const_entry_inline_code = false}
(* TODO : Set -> Type *)
let declare_new_type t =
Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) Term.mkSet [] false None (dummy_loc, t);
Term.mkVar t
let declare_new_variable v constr_t =
Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
Term.mkVar v
let declare_constant n c =
Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
type cast_kind = Term.cast_kind
let vmcast = Term.VMcast
let mkCast = Term.mkCast
(* EConstr *)
type econstr = Term.constr
let econstr_of_constr e = e
(* Modules *)
let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
(* Int63 *)
let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
let mkInt : int -> Term.constr =
fun i -> Term.mkInt (Uint63.of_int i)
let cint = gen_constant int63_modules "int"
(* PArray *)
let parray_modules = [["Coq";"Array";"PArray"]]
let max_array_size : int =
Parray.trunc_size (Uint63.of_int 4194303)
let mkArray : Term.types * Term.constr array -> Term.constr =
Term.mkArray
(* Traces *)
(* WARNING: side effect on r! *)
let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
let max = max_array_size - 1 in
let q,r1 = size / max, size mod max in
let trace =
let len = if r1 = 0 then q + 1 else q + 2 in
Array.make len (mkArray (step, [|def_step|])) in
for j = 0 to q - 1 do
let tracej = Array.make max_array_size def_step in
for i = 0 to max - 1 do
r := next !r;
tracej.(i) <- step_to_coq !r;
done;
trace.(j) <- mkArray (step, tracej)
done;
if r1 <> 0 then (
let traceq = Array.make (r1 + 1) def_step in
for i = 0 to r1-1 do
r := next !r;
traceq.(i) <- step_to_coq !r;
done;
trace.(q) <- mkArray (step, traceq)
);
mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace)
(* Micromega *)
module Micromega_plugin_Micromega = Micromega
module Micromega_plugin_Mutils = Mutils
module Micromega_plugin_Certificate = Certificate
module Micromega_plugin_Coq_micromega = Coq_micromega
let micromega_coq_proofTerm =
Coq_micromega.M.coq_proofTerm
let micromega_dump_proof_term p =
Coq_micromega.dump_proof_term p
(* Tactics *)
type tactic = Proof_type.tactic
let tclTHEN = Tacticals.tclTHEN
let tclTHENLAST = Tacticals.tclTHENLAST
let assert_before = Tactics.assert_tac
let vm_cast_no_check = Tactics.vm_cast_no_check
let mk_tactic tac gl =
let env = Tacmach.pf_env gl in
let sigma = Tacmach.project gl in
let t = Tacmach.pf_concl gl in
tac env sigma t gl
let set_evars_tac _ = Tacticals.tclIDTAC
(* Other differences between the two versions of Coq *)
type constr_expr = Topconstr.constr_expr
let error = Errors.error
let warning _ s = Pp.warning s
let extern_constr = Constrextern.extern_constr true Environ.empty_env
let destruct_rel_decl (n, _, t) = n, t
let interp_constr env sigma = Constrintern.interp_constr sigma env
let ppconstr_lsimpleconstr = Ppconstr.lsimple
let constrextern_extern_constr =
let env = Global.env () in
Constrextern.extern_constr false env
let get_rel_dec_name = fun _ -> Names.Anonymous
(* Eta-expanded to get rid of optional arguments *)
let retyping_get_type_of env = Retyping.get_type_of env
let vm_conv = Reduction.vm_conv
let cbv_vm = Vnorm.cbv_vm
|
