20
(* 1. gappa syntax trees and output *)
22
module Constant = struct
26
type t = { mantissa : bigint; base : int; exp : bigint }
28
let create (b, m, e) =
29
{ mantissa = m; base = b; exp = e }
32
{ mantissa = x; base = 1; exp = zero }
34
let print fmt x = match x.base with
35
| 1 -> fprintf fmt "%s" (to_string x.mantissa)
36
| 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp)
37
| 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp)
42
type binop = Bminus | Bplus | Bmult | Bdiv
44
type unop = Usqrt | Uabs | Uopp
46
type rounding_mode = string
49
| Tconst of Constant.t
51
| Tbinop of binop * term * term
52
| Tunop of unop * term
53
| Tround of rounding_mode * term
56
| Pin of term * Constant.t * Constant.t
58
let rec print_term fmt = function
59
| Tconst c -> Constant.print fmt c
60
| Tvar s -> pp_print_string fmt s
61
| Tbinop (op, t1, t2) ->
62
let op = match op with
63
| Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/"
65
fprintf fmt "(%a %s %a)" print_term t1 op print_term t2
67
fprintf fmt "|%a|" print_term t
68
| Tunop (Uopp | Usqrt as op, t) ->
70
| Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false
72
fprintf fmt "(%s(%a))" s print_term t
74
fprintf fmt "(%s(%a))" m print_term t
76
let print_pred fmt = function
78
fprintf fmt "%a in [%a, %a]"
79
print_term t Constant.print c1 Constant.print c2
81
let temp_file f = if !debug then f else Filename.temp_file f ".v"
82
let remove_file f = if not !debug then try Sys.remove f with _ -> ()
84
let read_gappa_proof f =
85
let buf = Buffer.create 1024 in
86
Buffer.add_char buf '(';
87
let cin = open_in f in
88
let rec skip_space () =
89
let c = input_char cin in if c = ' ' then skip_space () else c
91
while input_char cin <> '=' do () done;
94
let c = skip_space () in
95
if c = ':' then raise Exit;
96
Buffer.add_char buf c;
97
let s = input_line cin in
98
Buffer.add_string buf s;
99
Buffer.add_char buf '\n';
105
Buffer.add_char buf ')';
108
exception GappaFailed
109
exception GappaProofFailed
111
let patch_gappa_proof fin fout =
112
let cin = open_in fin in
113
let cout = open_out fout in
114
let fmt = formatter_of_out_channel cout in
119
let s = input_line cin in
121
fprintf fmt "Defined.@\n"
124
try Scanf.sscanf s "Lemma %s "
125
(fun n -> defs := n ^ " " ^ !defs; last := n)
126
with Scanf.Scan_failure _ ->
127
try Scanf.sscanf s "Definition %s "
128
(fun n -> defs := n ^ " " ^ !defs)
129
with Scanf.Scan_failure _ ->
132
fprintf fmt "%s@\n" s
137
fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last;
140
let call_gappa hl p =
141
let gappa_in = temp_file "gappa_input" in
142
let c = open_out gappa_in in
143
let fmt = formatter_of_out_channel c in
145
List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl;
146
fprintf fmt "%a }@]@." print_pred p;
148
let gappa_out = temp_file "gappa_output" in
149
let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in
150
let out = Sys.command cmd in
151
if out <> 0 then raise GappaFailed;
152
remove_file gappa_in;
153
let gappa_out2 = temp_file "gappa2" in
154
patch_gappa_proof gappa_out gappa_out2;
155
remove_file gappa_out;
156
let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out2 in
157
let out = Sys.command cmd in
158
if out <> 0 then raise GappaProofFailed;
159
let gappa_out3 = temp_file "gappa3" in
160
let c = open_out gappa_out3 in
161
let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in
163
"Require \"%s\". Set Printing Depth 999999. Print %s.proof."
164
(Filename.chop_suffix gappa_out2 ".v") gappa2;
166
let lambda = temp_file "gappa_lambda" in
167
let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out3 ^ " > " ^ lambda in
168
let out = Sys.command cmd in
169
if out <> 0 then raise GappaProofFailed;
170
remove_file gappa_out2; remove_file gappa_out3;
171
remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o");
172
read_gappa_proof lambda
174
(* 2. coq -> gappa translation *)
178
let logic_dir = ["Coq";"Logic";"Decidable"]
180
init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
181
@ [["Coq"; "ZArith"; "BinInt"];
182
["Coq"; "Reals"; "Rdefinitions"];
183
["Coq"; "Reals"; "Raxioms";];
184
["Coq"; "Reals"; "Rbasic_fun";];
185
["Coq"; "Reals"; "R_sqrt";];
186
["Coq"; "Reals"; "Rfunctions";];
187
["Gappa"; "Gappa_tactic";];
188
["Gappa"; "Gappa_fixed";];
189
["Gappa"; "Gappa_float";];
190
["Gappa"; "Gappa_round_def";];
191
["Gappa"; "Gappa_pred_bnd";];
192
["Gappa"; "Gappa_definitions";];
195
let constant = gen_constant_in_modules "gappa" coq_modules
197
let coq_refl_equal = lazy (constant "refl_equal")
198
let coq_Rle = lazy (constant "Rle")
199
let coq_R = lazy (constant "R")
201
let coq_Rplus = lazy (constant "Rplus")
202
let coq_Rminus = lazy (constant "Rminus")
203
let coq_Rmult = lazy (constant "Rmult")
204
let coq_Rdiv = lazy (constant "Rdiv")
205
let coq_powerRZ = lazy (constant "powerRZ")
206
let coq_R1 = lazy (constant "R1")
207
let coq_Ropp = lazy (constant "Ropp")
208
let coq_Rabs = lazy (constant "Rabs")
209
let coq_sqrt = lazy (constant "sqrt")
212
let coq_convert = lazy (constant "convert")
213
let coq_reUnknown = lazy (constant "reUnknown")
214
let coq_reFloat2 = lazy (constant "reFloat2")
215
let coq_reFloat10 = lazy (constant "reFloat10")
216
let coq_reInteger = lazy (constant "reInteger")
217
let coq_reBinary = lazy (constant "reBinary")
218
let coq_reUnary = lazy (constant "reUnary")
219
let coq_reRound = lazy (constant "reRound")
220
let coq_roundDN = lazy (constant "roundDN")
221
let coq_roundUP = lazy (constant "roundUP")
222
let coq_roundNE = lazy (constant "roundNE")
223
let coq_roundZR = lazy (constant "roundZR")
224
let coq_rounding_fixed = lazy (constant "rounding_fixed")
225
let coq_rounding_float = lazy (constant "rounding_float")
226
let coq_boAdd = lazy (constant "boAdd")
227
let coq_boSub = lazy (constant "boSub")
228
let coq_boMul = lazy (constant "boMul")
229
let coq_boDiv = lazy (constant "boDiv")
230
let coq_uoAbs = lazy (constant "uoAbs")
231
let coq_uoNeg = lazy (constant "uoNeg")
232
let coq_uoSqrt = lazy (constant "uoSqrt")
233
let coq_subset = lazy (constant "subset")
234
let coq_makepairF = lazy (constant "makepairF")
236
let coq_true = lazy (constant "true")
237
let coq_false = lazy (constant "false")
239
let coq_Z0 = lazy (constant "Z0")
240
let coq_Zpos = lazy (constant "Zpos")
241
let coq_Zneg = lazy (constant "Zneg")
242
let coq_xH = lazy (constant "xH")
243
let coq_xI = lazy (constant "xI")
244
let coq_xO = lazy (constant "xO")
245
let coq_IZR = lazy (constant "IZR")
247
(* translates a closed Coq term p:positive into a FOL term of type int *)
248
let rec tr_positive p = match kind_of_term p with
249
| Term.Construct _ when p = Lazy.force coq_xH ->
251
| Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
252
2 * (tr_positive a) + 1
253
| Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
255
| Term.Cast (p, _, _) ->
260
(* translates a closed Coq term t:Z into a term of type int *)
261
let rec tr_arith_constant t = match kind_of_term t with
262
| Term.Construct _ when t = Lazy.force coq_Z0 -> 0
263
| Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a
264
| Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a)
265
| Term.Cast (t, _, _) -> tr_arith_constant t
266
| _ -> raise NotGappa
268
(* translates a closed Coq term p:positive into a FOL term of type bigint *)
269
let rec tr_bigpositive p = match kind_of_term p with
270
| Term.Construct _ when p = Lazy.force coq_xH ->
272
| Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
273
Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a))
274
| Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
275
(Bigint.mult_2 (tr_bigpositive a))
276
| Term.Cast (p, _, _) ->
281
(* translates a closed Coq term t:Z into a term of type bigint *)
282
let rec tr_arith_bigconstant t = match kind_of_term t with
283
| Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero
284
| Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a
285
| Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
286
Bigint.neg (tr_bigpositive a)
287
| Term.Cast (t, _, _) -> tr_arith_bigconstant t
288
| _ -> raise NotGappa
291
let c, args = decompose_app c in
294
let tr_bool c = match decompose_app c with
295
| c, [] when c = Lazy.force coq_true -> true
296
| c, [] when c = Lazy.force coq_false -> false
297
| _ -> raise NotGappa
300
(b, tr_arith_bigconstant m, tr_arith_bigconstant e)
302
let tr_binop c = match decompose_app c with
303
| c, [] when c = Lazy.force coq_boAdd -> Bplus
304
| c, [] when c = Lazy.force coq_boSub -> Bminus
305
| c, [] when c = Lazy.force coq_boMul -> Bmult
306
| c, [] when c = Lazy.force coq_boDiv -> Bdiv
309
let tr_unop c = match decompose_app c with
310
| c, [] when c = Lazy.force coq_uoNeg -> Uopp
311
| c, [] when c = Lazy.force coq_uoSqrt -> Usqrt
312
| c, [] when c = Lazy.force coq_uoAbs -> Uabs
313
| _ -> raise NotGappa
315
let tr_var c = match decomp c with
316
| Var x, [] -> string_of_id x
319
let tr_mode c = match decompose_app c with
320
| c, [] when c = Lazy.force coq_roundDN -> "dn"
321
| c, [] when c = Lazy.force coq_roundNE -> "ne"
322
| c, [] when c = Lazy.force coq_roundUP -> "up"
323
| c, [] when c = Lazy.force coq_roundZR -> "zr"
324
| _ -> raise NotGappa
326
let tr_rounding_mode c = match decompose_app c with
327
| c, [a;b] when c = Lazy.force coq_rounding_fixed ->
329
let b = tr_arith_constant b in
330
sprintf "fixed<%d,%s>" b a
331
| c, [a;p;e] when c = Lazy.force coq_rounding_float ->
333
let p = tr_positive p in
334
let e = tr_arith_constant e in
335
sprintf "float<%d,%d,%s>" p (-e) a
341
let c, args = decompose_app c0 in
342
match kind_of_term c, args with
343
| _, [a] when c = Lazy.force coq_reUnknown ->
345
| _, [a; b] when c = Lazy.force coq_reFloat2 ->
346
Tconst (Constant.create (tr_float 2 a b))
347
| _, [a; b] when c = Lazy.force coq_reFloat10 ->
348
Tconst (Constant.create (tr_float 10 a b))
349
| _, [a] when c = Lazy.force coq_reInteger ->
350
Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero))
351
| _, [op;a;b] when c = Lazy.force coq_reBinary ->
352
Tbinop (tr_binop op, tr_term a, tr_term b)
353
| _, [op;a] when c = Lazy.force coq_reUnary ->
354
Tunop (tr_unop op, tr_term a)
355
| _, [op;a] when c = Lazy.force coq_reRound ->
356
Tround (tr_rounding_mode op, tr_term a)
358
msgnl (str "tr_term: " ++ Printer.pr_constr c0);
362
let c, args = decompose_app c in
363
match kind_of_term c, args with
364
| _, [a;b] when c = Lazy.force coq_Rle ->
365
begin match decompose_app a, decompose_app b with
366
| (ac, [at]), (bc, [bt])
367
when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert ->
376
let c, args = decompose_app c in
377
match kind_of_term c, args with
378
| _, [a;b] when c = build_coq_and () ->
379
begin match tr_rle a, tr_rle b with
380
| (c1, t1), (t2, c2) when t1 = t2 ->
381
begin match tr_term c1, tr_term c2 with
382
| Tconst c1, Tconst c2 ->
383
Pin (tr_term t1, c1, c2)
393
let is_R c = match decompose_app c with
394
| c, [] when c = Lazy.force coq_R -> true
399
(fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) []
401
let constr_of_string gl s =
402
let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
403
Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
405
let var_name = function
407
let s = string_of_id id in
408
let s = String.sub s 1 (String.length s - 1) in
409
mkVar (id_of_string s)
413
let build_proof_term c0 =
414
let bl,c = decompose_lam c0 in
417
mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |]))
420
let gappa_internal gl =
422
let c = tr_pred (pf_concl gl) in
423
let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in
424
let pf = constr_of_string gl s in
425
let pf = build_proof_term pf in
426
Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl
428
| NotGappa -> error "not a gappa goal"
429
| GappaFailed -> error "gappa failed"
430
| GappaProofFailed -> error "incorrect gappa proof term"
433
let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
434
lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
437
Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
438
Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl
442
compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt"
added
removed
contrib/dp/dp_gappa.ml
