|
1 (* Title: HOL/Tools/SMT2/verit_proof.ML |
|
2 Author: Mathias Fleury, ENS Rennes |
|
3 Author: Sascha Boehme, TU Muenchen |
|
4 |
|
5 VeriT proofs: parsing and abstract syntax tree. |
|
6 *) |
|
7 |
|
8 signature VERIT_PROOF = |
|
9 sig |
|
10 (*proofs*) |
|
11 datatype veriT_step = VeriT_Step of { |
|
12 id: int, |
|
13 rule: string, |
|
14 prems: string list, |
|
15 concl: term, |
|
16 fixes: string list} |
|
17 |
|
18 (*proof parser*) |
|
19 val parse: typ Symtab.table -> term Symtab.table -> string list -> |
|
20 Proof.context -> veriT_step list * Proof.context |
|
21 |
|
22 val verit_step_prefix : string |
|
23 val verit_proof_input_rule: string |
|
24 val verit_rewrite : string |
|
25 end; |
|
26 |
|
27 structure VeriT_Proof: VERIT_PROOF = |
|
28 struct |
|
29 |
|
30 open SMTLIB2_Proof |
|
31 |
|
32 (* proof rules *) |
|
33 |
|
34 datatype veriT_node = VeriT_Node of { |
|
35 id: int, |
|
36 rule: string, |
|
37 prems: string list, |
|
38 concl: term, |
|
39 bounds: string list} |
|
40 |
|
41 fun mk_node id rule prems concl bounds = |
|
42 VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} |
|
43 |
|
44 (*two structures needed*) |
|
45 datatype veriT_step = VeriT_Step of { |
|
46 id: int, |
|
47 rule: string, |
|
48 prems: string list, |
|
49 concl: term, |
|
50 fixes: string list} |
|
51 |
|
52 fun mk_step id rule prems concl fixes = |
|
53 VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} |
|
54 |
|
55 val verit_step_prefix = ".c" |
|
56 val verit_proof_input_rule = "input" |
|
57 val verit_rewrite = "rewrite" |
|
58 |
|
59 (* proof parser *) |
|
60 |
|
61 fun node_of p cx = |
|
62 ([], cx) |
|
63 ||>> with_fresh_names (term_of p) |
|
64 ||>> next_id |
|
65 |>> (fn ((prems, (t, ns)), id) => mk_node id verit_proof_input_rule prems t ns) |
|
66 |
|
67 (*in order to get Z3-style quantification*) |
|
68 fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) = |
|
69 let |
|
70 val (quantified_vars, t) = split_last (map fix_quantification l) |
|
71 in |
|
72 SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: []) |
|
73 end |
|
74 | fix_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) = |
|
75 let val (quantified_vars, t) = split_last (map fix_quantification l) |
|
76 in |
|
77 SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) |
|
78 end |
|
79 | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) |
|
80 | fix_quantification x = x |
|
81 |
|
82 fun parse_proof cx = |
|
83 let |
|
84 fun rotate_pair (a, (b, c)) = ((a, b), c) |
|
85 fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) |
|
86 | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) |
|
87 fun change_id_to_number x = (unprefix verit_step_prefix #> Int.fromString #> the) x |
|
88 fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) |
|
89 fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = |
|
90 (SOME (map (fn (SMTLIB2.Sym id) => id) source), l) |
|
91 | parse_source l = (NONE, l) |
|
92 fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l |
|
93 | skip_args l = l |
|
94 |
|
95 fun parse_conclusion [SMTLIB2.Key "conclusion", SMTLIB2.S concl] = concl |
|
96 |
|
97 fun make_or_from_clausification l = |
|
98 foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => (HOLogic.mk_disj (concl1, concl2), |
|
99 bounds1 @ bounds2)) l |
|
100 (*the conclusion is empty, ie no false*) |
|
101 fun to_node ((((id, rule), prems), ([], cx))) = (mk_node id rule (the_default [] prems) |
|
102 @{const False} [], cx) |
|
103 | to_node ((((id, rule), prems), (concls, cx))) = |
|
104 let val (concl, bounds) = make_or_from_clausification concls in |
|
105 (mk_node id rule (the_default [] prems) concl bounds, cx) end |
|
106 in |
|
107 get_id |
|
108 #>> change_id_to_number |
|
109 ##> parse_rule |
|
110 #> rotate_pair |
|
111 ##> parse_source |
|
112 #> rotate_pair |
|
113 ##> skip_args |
|
114 ##> parse_conclusion |
|
115 ##> map fix_quantification |
|
116 ##> (fn terms => fold_map (fn t => fn cx => node_of t cx) terms cx) |
|
117 ##> apfst (map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds))) |
|
118 #> to_node |
|
119 end |
|
120 |
|
121 |
|
122 (* overall proof parser *) |
|
123 fun parse typs funs lines ctxt = |
|
124 let |
|
125 val (u, env) = |
|
126 fold_map (fn l => fn cx => parse_proof cx l) (map (fn f => SMTLIB2.parse [f]) lines) |
|
127 (empty_context ctxt typs funs) |
|
128 val t = |
|
129 map (fn (VeriT_Node {id, rule, prems, concl, bounds, ...}) => |
|
130 mk_step id rule prems concl bounds) u |
|
131 in |
|
132 (t, ctxt_of env) |
|
133 end |
|
134 |
|
135 end; |