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
|
{
open Lexing
open Pp
open Util
open Names
open Tacmach
open Dp_why
open Tactics
open Tacticals
let debug = ref false
let set_debug b = debug := b
let buf = Buffer.create 1024
let string_of_global env ref =
Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref)
let axioms = ref []
(* we cannot interpret the terms as we read them (since some lemmas
may need other lemmas to be already interpreted) *)
type lemma = { l_id : string; l_type : string; l_proof : string }
type zenon_proof = lemma list * string
}
let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+
let space = [' ' '\t' '\r']
rule start = parse
| "(* BEGIN-PROOF *)" "\n" { scan lexbuf }
| _ { start lexbuf }
| eof { anomaly "malformed Zenon proof term" }
(* here we read the lemmas and the main proof term;
meanwhile we maintain the set of axioms that were used *)
and scan = parse
| "Let" space (ident as id) space* ":"
{ let t = read_coq_term lexbuf in
let p = read_lemma_proof lexbuf in
let l,pr = scan lexbuf in
{ l_id = id; l_type = t; l_proof = p } :: l, pr }
| "Definition theorem:"
{ let t = read_main_proof lexbuf in [], t }
| _ | eof
{ anomaly "malformed Zenon proof term" }
and read_coq_term = parse
| "." "\n"
{ let s = Buffer.contents buf in Buffer.clear buf; s }
| "coq__" (ident as id) (* a Why keyword renamed *)
{ Buffer.add_string buf id; read_coq_term lexbuf }
| ("dp_axiom__" ['0'-'9']+) as id
{ axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf }
| _ as c
{ Buffer.add_char buf c; read_coq_term lexbuf }
| eof
{ anomaly "malformed Zenon proof term" }
and read_lemma_proof = parse
| "Proof" space
{ read_coq_term lexbuf }
| _ | eof
{ anomaly "malformed Zenon proof term" }
(* skip the main proof statement and then read its term *)
and read_main_proof = parse
| ":=" "\n"
{ read_coq_term lexbuf }
| _
{ read_main_proof lexbuf }
| eof
{ anomaly "malformed Zenon proof term" }
{
let read_zenon_proof f =
Buffer.clear buf;
let c = open_in f in
let lb = from_channel c in
let p = start lb in
close_in c;
if not !debug then begin try Sys.remove f with _ -> () end;
p
let constr_of_string gl s =
let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
(* we are lazy here: we build strings containing Coq terms using a *)
(* pretty-printer Fol -> Coq *)
module Coq = struct
open Format
open Fol
let rec print_list sep print fmt = function
| [] -> ()
| [x] -> print fmt x
| x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
let space fmt () = fprintf fmt "@ "
let comma fmt () = fprintf fmt ",@ "
let rec print_typ fmt = function
| Tvar x -> fprintf fmt "%s" x
| Tid ("int", []) -> fprintf fmt "Z"
| Tid (x, []) -> fprintf fmt "%s" x
| Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t
| Tid (x,tl) ->
fprintf fmt "(%s %a)" x (print_list comma print_typ) tl
let rec print_term fmt = function
| Cst n ->
fprintf fmt "%d" n
| Plus (a, b) ->
fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b
| Moins (a, b) ->
fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b
| Mult (a, b) ->
fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b
| Div (a, b) ->
fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b
| App (id, []) ->
fprintf fmt "%s" id
| App (id, tl) ->
fprintf fmt "@[(%s %a)@]" id print_terms tl
and print_terms fmt tl =
print_list space print_term fmt tl
(* builds the text for "forall vars, f vars = t" *)
let fun_def_axiom f vars t =
let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in
fprintf str_formatter
"@[(forall %a, %s %a = %a)@]@."
(print_list space binder) vars f
(print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars
print_term t;
flush_str_formatter ()
end
let prove_axiom id = match Dp_why.find_proof id with
| Immediate t ->
exact_check t
| Fun_def (f, vars, ty, t) ->
tclTHENS
(fun gl ->
let s = Coq.fun_def_axiom f vars t in
if !debug then Format.eprintf "axiom fun def = %s@." s;
let c = constr_of_string gl s in
assert_tac true (Name (id_of_string id)) c gl)
[tclTHEN intros reflexivity; tclIDTAC]
let exact_string s gl =
let c = constr_of_string gl s in
exact_check c gl
let interp_zenon_proof (ll,p) =
let interp_lemma l gl =
let ty = constr_of_string gl l.l_type in
tclTHENS
(assert_tac true (Name (id_of_string l.l_id)) ty)
[exact_string l.l_proof; tclIDTAC]
gl
in
tclTHEN (tclMAP interp_lemma ll) (exact_string p)
let proof_from_file f =
axioms := [];
msgnl (str "proof_from_file " ++ str f);
let zp = read_zenon_proof f in
msgnl (str "proof term is " ++ str (snd zp));
tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp)
}
|
