author | fleury |
Wed, 30 Jul 2014 14:03:13 +0200 | |
changeset 57710 | 323a57d7455c |
parent 57709 | 9cda0c64c37a |
child 57712 | 3c4e6bc7455f |
permissions | -rw-r--r-- |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT2/verit_proof.ML |
57704 | 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 |
||
57705 | 22 |
val veriT_step_prefix : string |
23 |
val veriT_input_rule: string |
|
24 |
val veriT_rewrite_rule : string |
|
57704 | 25 |
end; |
26 |
||
27 |
structure VeriT_Proof: VERIT_PROOF = |
|
28 |
struct |
|
29 |
||
30 |
open SMTLIB2_Proof |
|
31 |
||
32 |
datatype veriT_node = VeriT_Node of { |
|
33 |
id: int, |
|
34 |
rule: string, |
|
35 |
prems: string list, |
|
36 |
concl: term, |
|
37 |
bounds: string list} |
|
38 |
||
39 |
fun mk_node id rule prems concl bounds = |
|
40 |
VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} |
|
41 |
||
42 |
(*two structures needed*) |
|
43 |
datatype veriT_step = VeriT_Step of { |
|
44 |
id: int, |
|
45 |
rule: string, |
|
46 |
prems: string list, |
|
47 |
concl: term, |
|
48 |
fixes: string list} |
|
49 |
||
50 |
fun mk_step id rule prems concl fixes = |
|
51 |
VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} |
|
52 |
||
57705 | 53 |
val veriT_step_prefix = ".c" |
54 |
val veriT_input_rule = "input" |
|
55 |
val veriT_rewrite_rule = "__rewrite" (*arbitrary*) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
56 |
val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
57705 | 57 |
val veriT_tmp_skolemize = "tmp_skolemize" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
58 |
val veriT_alpha_conv = "tmp_alphaconv" |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
59 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
60 |
fun mk_string_id id = veriT_step_prefix ^ (string_of_int id) |
57704 | 61 |
|
62 |
(* proof parser *) |
|
63 |
||
64 |
fun node_of p cx = |
|
65 |
([], cx) |
|
66 |
||>> with_fresh_names (term_of p) |
|
67 |
||>> next_id |
|
57705 | 68 |
|>> (fn ((prems, (t, ns)), id) => mk_node id veriT_input_rule prems t ns) |
57704 | 69 |
|
70 |
(*in order to get Z3-style quantification*) |
|
71 |
fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) = |
|
57705 | 72 |
let val (quantified_vars, t) = split_last (map fix_quantification l) |
57704 | 73 |
in |
74 |
SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: []) |
|
75 |
end |
|
76 |
| fix_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) = |
|
77 |
let val (quantified_vars, t) = split_last (map fix_quantification l) |
|
78 |
in |
|
79 |
SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) |
|
80 |
end |
|
81 |
| fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) |
|
82 |
| fix_quantification x = x |
|
83 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
84 |
fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var = |
57705 | 85 |
(case List.find (fn v => String.isPrefix v var) free_var of |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
86 |
NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
87 |
| SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
88 |
| replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
89 |
replace_bound_var_by_free_var v free_vars |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
90 |
| replace_bound_var_by_free_var u _ = u |
57705 | 91 |
|
92 |
fun find_type_in_formula (Abs(v, ty, u)) var_name = |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
93 |
if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name |
57705 | 94 |
| find_type_in_formula (u $ v) var_name = |
95 |
(case find_type_in_formula u var_name of |
|
96 |
NONE => find_type_in_formula v var_name |
|
97 |
| a => a) |
|
98 |
| find_type_in_formula _ _ = NONE |
|
99 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
100 |
fun add_bound_variables_to_ctxt cx bounds concl = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
101 |
fold (fn a => fn b => update_binding a b) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
102 |
(map (fn s => ((s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
103 |
bounds) cx |
57705 | 104 |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
105 |
fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
106 |
if rule = veriT_tmp_ite_elim_rule then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
107 |
(mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl) |
57705 | 108 |
else if rule = veriT_tmp_skolemize then |
109 |
let |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
110 |
val concl' = replace_bound_var_by_free_var concl bounds |
57705 | 111 |
in |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
112 |
(mk_node id rule prems concl' [], add_bound_variables_to_ctxt cx bounds concl) |
57705 | 113 |
end |
114 |
else |
|
115 |
(st, cx) |
|
116 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
117 |
(*FIXME: using a reference would be better to know th numbers of the steps to add*) |
57705 | 118 |
fun fix_subproof_steps number_of_steps ((((id, rule), prems), subproof), ((step_concl, bounds), |
119 |
cx)) = |
|
120 |
let |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
121 |
fun mk_prop_of_term concl = (fastype_of concl = @{typ "bool"} ? |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
122 |
curry (op $) @{term "Trueprop"}) concl |
57705 | 123 |
fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl, |
124 |
bounds}) = |
|
125 |
if List.find (curry (op =) assumption_id) prems <> NONE then |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
126 |
mk_node (id + number_of_steps) rule (filter_out (curry (op =) assumption_id) prems) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
127 |
(Const ("Pure.imp", @{typ "prop"} --> @{typ "prop"} --> @{typ "prop"}) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
128 |
$ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
57705 | 129 |
else |
130 |
st |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
131 |
fun find_input_steps_and_inline [] last_step_number = ([], last_step_number) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
132 |
| find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
133 |
last_step_number = |
57705 | 134 |
if rule = veriT_input_rule then |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
135 |
find_input_steps_and_inline (map (inline_assumption concl (mk_string_id id')) steps) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
136 |
last_step_number |
57705 | 137 |
else |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
138 |
apfst (cons (mk_node (id' + id + number_of_steps) rule prems concl bounds)) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
139 |
(find_input_steps_and_inline steps (id' + id + number_of_steps)) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
140 |
val (subproof', last_step_number) = find_input_steps_and_inline subproof ~1 |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
141 |
val prems' = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
142 |
if last_step_number = ~1 then prems |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
143 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
144 |
(case prems of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
145 |
NONE => SOME [mk_string_id last_step_number] |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
146 |
| SOME l => SOME (string_of_int last_step_number :: l)) |
57705 | 147 |
in |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
148 |
(subproof', (((((id, rule), prems'), step_concl), bounds), cx)) |
57705 | 149 |
end |
150 |
||
151 |
(* |
|
152 |
(set id rule :clauses(...) :args(..) :conclusion (...)). |
|
153 |
or |
|
154 |
(set id subproof (set ...) :conclusion (...)). |
|
155 |
*) |
|
156 |
||
157 |
fun parse_proof_step number_of_steps cx = |
|
57704 | 158 |
let |
159 |
fun rotate_pair (a, (b, c)) = ((a, b), c) |
|
160 |
fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) |
|
161 |
| get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) |
|
57705 | 162 |
fun change_id_to_number x = (unprefix veriT_step_prefix #> Int.fromString #> the) x |
57704 | 163 |
fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) |
164 |
fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = |
|
165 |
(SOME (map (fn (SMTLIB2.Sym id) => id) source), l) |
|
166 |
| parse_source l = (NONE, l) |
|
57705 | 167 |
fun parse_subproof cx ((subproof_step as SMTLIB2.S (SMTLIB2.Sym "set" :: _)) :: l) = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
168 |
let val (subproof_steps, cx') = parse_proof_step number_of_steps cx subproof_step in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
169 |
apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' l) |
57705 | 170 |
end |
171 |
| parse_subproof cx l = (([], cx), l) |
|
57704 | 172 |
fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l |
173 |
| skip_args l = l |
|
57705 | 174 |
fun parse_conclusion (SMTLIB2.Key "conclusion" :: SMTLIB2.S concl :: []) = concl |
57704 | 175 |
fun make_or_from_clausification l = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
176 |
foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
177 |
(HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
178 |
perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l |
57705 | 179 |
fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
180 |
(the_default [] prems) concl bounds, cx) |
57704 | 181 |
in |
182 |
get_id |
|
183 |
#>> change_id_to_number |
|
184 |
##> parse_rule |
|
185 |
#> rotate_pair |
|
186 |
##> parse_source |
|
187 |
#> rotate_pair |
|
188 |
##> skip_args |
|
57705 | 189 |
##> parse_subproof cx |
190 |
#> rotate_pair |
|
57704 | 191 |
##> parse_conclusion |
192 |
##> map fix_quantification |
|
57705 | 193 |
#> (fn ((((id, rule), prems), (subproof, cx)), terms) => |
194 |
(((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) |
|
195 |
##> apfst ((map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds)))) |
|
196 |
(*the conclusion is the empty list, ie no false is written, we have to add it.*) |
|
197 |
##> (apfst (fn [] => (@{const False}, []) |
|
198 |
| concls => make_or_from_clausification concls)) |
|
199 |
#> fix_subproof_steps number_of_steps |
|
200 |
##> to_node |
|
201 |
#> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
202 |
#> (fn (steps, cx) => fold_map update_step_and_cx steps cx) |
57705 | 203 |
end |
204 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
205 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
206 |
(*function related to parsing and general transformation*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
207 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
208 |
(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
209 |
unbalanced on each line*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
210 |
fun seperate_into_steps lines = |
57705 | 211 |
let |
212 |
fun count ("(" :: l) n = count l (n+1) |
|
213 |
| count (")" :: l) n = count l (n-1) |
|
214 |
| count (_ :: l) n = count l n |
|
215 |
| count [] n = n |
|
216 |
fun seperate (line :: l) actual_lines m = |
|
217 |
let val n = count (raw_explode line) 0 in |
|
218 |
if m + n = 0 then |
|
219 |
[actual_lines ^ line] :: seperate l "" 0 |
|
220 |
else seperate l (actual_lines ^ line) (m + n) |
|
221 |
end |
|
222 |
| seperate [] _ 0 = [] |
|
223 |
in |
|
224 |
seperate lines "" 0 |
|
57704 | 225 |
end |
226 |
||
57705 | 227 |
(*VeriT adds @ before every variable.*) |
228 |
fun remove_all_at (SMTLIB2.Sym v :: l) = |
|
229 |
SMTLIB2.Sym (if nth_string v 0 = "@" then String.extract (v, 1, NONE) else v) :: remove_all_at l |
|
230 |
| remove_all_at (SMTLIB2.S l :: l') = SMTLIB2.S (remove_all_at l) :: remove_all_at l' |
|
231 |
| remove_all_at (SMTLIB2.Key v :: l) = SMTLIB2.Key v :: remove_all_at l |
|
232 |
| remove_all_at (v :: l) = v :: remove_all_at l |
|
233 |
| remove_all_at [] = [] |
|
234 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
235 |
fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) = |
57705 | 236 |
(case List.find (fn v => String.isPrefix v var) bounds of |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
237 |
NONE => find_in_which_step_defined var l |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
238 |
| SOME _ => id) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
239 |
| find_in_which_step_defined var _ = raise Fail ("undefined " ^ var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
240 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
241 |
(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
242 |
fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
243 |
(Const ("HOL.eq", _) $ Free (var1, _) $ Free (var2, _) ) $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
244 |
(Const ("HOL.eq", _) $ Free (var3, _) $ Free (var4, _) )) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
245 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
246 |
fun get_number_of_ite_transformed_var var = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
247 |
perhaps (try (unprefix "ite")) var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
248 |
|> Int.fromString |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
249 |
fun is_equal_and_has_correct_substring var var' var'' = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
250 |
if var = var' andalso String.isPrefix "ite" var then SOME var' |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
251 |
else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
252 |
val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4 |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
253 |
val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2 |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
254 |
in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
255 |
(case (var1_introduced_var, var2_introduced_var) of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
256 |
(SOME a, SOME b) => |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
257 |
(*ill-generated case, might be possible when applying the rule to max a a. Only if the |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
258 |
variable have been introduced before. Probably an impossible edge case*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
259 |
(case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
260 |
(SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
261 |
(*Otherwise, it is a name clase between a parameter name and the introduced variable. |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
262 |
Or the name convention has been changed.*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
263 |
| (NONE, SOME _) => var2_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
264 |
| (SOME _, NONE) => var2_introduced_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
265 |
| (_, SOME _) => var2_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
266 |
| (SOME _, _) => var1_introduced_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
267 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
268 |
| find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
269 |
(Const (@{const_name "HOL.eq"}, _) $ Free (var, _) $ _ ) $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
270 |
(Const (@{const_name "HOL.eq"}, _) $ Free (var', _) $ _ )) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
271 |
if var = var' then SOME var else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
272 |
| find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
273 |
(Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var, _)) $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
274 |
(Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var', _))) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
275 |
if var = var' then SOME var else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
276 |
| find_ite_var_in_term (p $ q) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
277 |
(case find_ite_var_in_term p of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
278 |
NONE => find_ite_var_in_term q |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
279 |
| x => x) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
280 |
| find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
281 |
| find_ite_var_in_term _ = NONE |
57705 | 282 |
|
283 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
284 |
fun correct_veriT_step num_of_steps steps (st as VeriT_Node {id, rule, prems, concl, bounds}) = |
57705 | 285 |
if rule = "tmp_ite_elim" then |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
286 |
if bounds = [] then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
287 |
(*if the introduced var has already been defined, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
288 |
adding the definition as a dependency*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
289 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
290 |
val SOME var = find_ite_var_in_term concl |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
291 |
val new_dep = find_in_which_step_defined var steps |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
292 |
in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
293 |
VeriT_Node {id = id, rule = rule, prems = (mk_string_id new_dep) :: prems, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
294 |
concl = concl, bounds = bounds} |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
295 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
296 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
297 |
(*some new variables are created*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
298 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
299 |
val concl' = replace_bound_var_by_free_var concl bounds |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
300 |
in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
301 |
(*FIXME: horrible hackish method, but seems somehow to work. The difference is in the way |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
302 |
sledgehammer reconstructs: without an empty dependency, the skolemization is not done at all. |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
303 |
But if there is, a new step is added: |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
304 |
{fix sk ....} |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
305 |
hence "..sk.." |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
306 |
thus "(if ..)" |
57709 | 307 |
last step does not work: the step before is buggy. Without it, the proof work.*) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
308 |
mk_node id veriT_tmp_skolemize (if null prems then [mk_string_id (~num_of_steps - id)] |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
309 |
else prems) concl' [] |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
310 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
311 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
312 |
st |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
313 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
314 |
(*remove alpha conversion step, that just renames the variables*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
315 |
fun remove_alpha_conversion _ [] = [] |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
316 |
| remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) = |
57705 | 317 |
let |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
318 |
fun correct_dependency prems = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
319 |
map (fn x => perhaps (Symtab.lookup replace_table) x) prems |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
320 |
fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem |
57705 | 321 |
in |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
322 |
if rule = veriT_alpha_conv then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
323 |
remove_alpha_conversion (Symtab.update (mk_string_id id, find_predecessor (hd prems)) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
324 |
replace_table) steps |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
325 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
326 |
VeriT_Node {id = id, rule = rule, prems = correct_dependency prems, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
327 |
concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps |
57705 | 328 |
end |
329 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
330 |
fun correct_veriT_steps steps = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
331 |
steps |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
332 |
|> map (correct_veriT_step (1 + length steps) steps) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
333 |
|> remove_alpha_conversion Symtab.empty |
57704 | 334 |
|
335 |
(* overall proof parser *) |
|
336 |
fun parse typs funs lines ctxt = |
|
337 |
let |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
338 |
val smtlib2_lines_without_at = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
339 |
remove_all_at (map SMTLIB2.parse (seperate_into_steps lines)) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
340 |
val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step (length lines) cx l) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
341 |
smtlib2_lines_without_at (empty_context ctxt typs funs)) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
342 |
val t = correct_veriT_steps u |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
343 |
fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = |
57705 | 344 |
mk_step id rule prems concl bounds |
345 |
in |
|
346 |
(map node_to_step t, ctxt_of env) |
|
57704 | 347 |
end |
348 |
||
349 |
end; |