author | blanchet |
Sat, 25 Apr 2015 09:48:06 +0200 | |
changeset 60201 | 90e88e521e0e |
parent 59582 | 0fbed69ff081 |
child 69205 | 8050734eee3e |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/verit_proof_parse.ML |
57704 | 2 |
Author: Mathias Fleury, TU Muenchen |
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
4 |
||
5 |
VeriT proof parsing. |
|
6 |
*) |
|
7 |
||
8 |
signature VERIT_PROOF_PARSE = |
|
9 |
sig |
|
10 |
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
|
58491 | 11 |
val parse_proof: SMT_Translate.replay_data -> |
57704 | 12 |
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> |
58061 | 13 |
SMT_Solver.parsed_proof |
57704 | 14 |
end; |
15 |
||
16 |
structure VeriT_Proof_Parse: VERIT_PROOF_PARSE = |
|
17 |
struct |
|
18 |
||
19 |
open ATP_Util |
|
20 |
open ATP_Problem |
|
21 |
open ATP_Proof |
|
22 |
open ATP_Proof_Reconstruct |
|
23 |
open VeriT_Isar |
|
24 |
open VeriT_Proof |
|
25 |
||
58492
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
26 |
fun add_used_asserts_in_step (VeriT_Proof.VeriT_Step {prems, ...}) = |
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
27 |
union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems) |
57704 | 28 |
|
58491 | 29 |
fun parse_proof |
58061 | 30 |
({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) |
57704 | 31 |
xfacts prems concl output = |
32 |
let |
|
58492
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
33 |
val num_ll_defs = length ll_defs |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
34 |
|
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
35 |
val id_of_index = Integer.add num_ll_defs |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
36 |
val index_of_id = Integer.add (~ num_ll_defs) |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
37 |
|
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
38 |
fun step_of_assume j (_, th) = |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
39 |
VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j), |
59582 | 40 |
rule = veriT_input_rule, prems = [], concl = Thm.prop_of th, fixes = []} |
58492
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
41 |
|
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
42 |
val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt |
58492
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
43 |
val used_assert_ids = fold add_used_asserts_in_step actual_steps [] |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
44 |
val used_assm_js = |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
45 |
map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end) |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
46 |
used_assert_ids |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
47 |
val used_assms = map (nth assms) used_assm_js |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
48 |
val assm_steps = map2 step_of_assume used_assm_js used_assms |
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
49 |
val steps = assm_steps @ actual_steps |
57704 | 50 |
|
58492
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
51 |
val conjecture_i = 0 |
58488
289d1c39968c
correct indexing in the presence of lambda-lifting
blanchet
parents:
58482
diff
changeset
|
52 |
val prems_i = conjecture_i + 1 |
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
53 |
val num_prems = length prems |
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
54 |
val facts_i = prems_i + num_prems |
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
55 |
val num_facts = length xfacts |
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
56 |
val helpers_i = facts_i + num_facts |
57704 | 57 |
|
58492
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
58 |
val conjecture_id = id_of_index conjecture_i |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
59 |
val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1) |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
60 |
val fact_ids' = |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
61 |
map_filter (fn j => |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
62 |
let val (i, _) = nth assms j in |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
63 |
try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) |
e3ee0cf5cf93
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
blanchet
parents:
58491
diff
changeset
|
64 |
end) used_assm_js |
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
65 |
val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms |
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
66 |
|
57704 | 67 |
val fact_helper_ts = |
59582 | 68 |
map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @ |
69 |
map (fn (_, ((s, _), th)) => (s, Thm.prop_of th)) fact_ids' |
|
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
70 |
val fact_helper_ids' = |
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
71 |
map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids' |
57704 | 72 |
in |
60201 | 73 |
{outcome = NONE, fact_ids = SOME fact_ids', |
57704 | 74 |
atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl |
58482
7836013951e6
simplified and repaired veriT index handling code
blanchet
parents:
58061
diff
changeset
|
75 |
fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps} |
57704 | 76 |
end |
77 |
||
78 |
end; |