author | Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> |
Mon, 22 Aug 2022 06:27:28 +0200 | |
changeset 75956 | 1e2a9d2251b0 |
parent 75561 | b6239ed66b94 |
child 76183 | 8089593a364a |
permissions | -rw-r--r-- |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/Lethe_Proof.ML |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
2 |
Author: Mathias Fleury, ENS Rennes |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
3 |
Author: Sascha Boehme, TU Muenchen |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
4 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
5 |
Lethe proofs: parsing and abstract syntax tree. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
6 |
*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
7 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
8 |
signature LETHE_PROOF = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
9 |
sig |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
10 |
(*proofs*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
11 |
datatype lethe_step = Lethe_Step of { |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
12 |
id: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
13 |
rule: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
14 |
prems: string list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
15 |
proof_ctxt: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
16 |
concl: term, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
17 |
fixes: string list} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
18 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
19 |
datatype lethe_replay_node = Lethe_Replay_Node of { |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
20 |
id: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
21 |
rule: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
22 |
args: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
23 |
prems: string list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
24 |
proof_ctxt: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
25 |
concl: term, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
26 |
bounds: (string * typ) list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
27 |
declarations: (string * term) list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
28 |
insts: term Symtab.table, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
29 |
subproof: (string * typ) list * term list * term list * lethe_replay_node list} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
30 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
31 |
val mk_replay_node: string -> string -> term list -> string list -> term list -> |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
32 |
term -> (string * typ) list -> term Symtab.table -> (string * term) list -> |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
33 |
(string * typ) list * term list * term list * lethe_replay_node list -> lethe_replay_node |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
34 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
35 |
(*proof parser*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
36 |
val parse: typ Symtab.table -> term Symtab.table -> string list -> |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
37 |
Proof.context -> lethe_step list * Proof.context |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
38 |
val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
39 |
Proof.context -> lethe_replay_node list * Proof.context |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
40 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
41 |
val step_prefix : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
42 |
val input_rule: string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
43 |
val keep_app_symbols: string -> bool |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
44 |
val keep_raw_lifting: string -> bool |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
45 |
val normalized_input_rule: string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
46 |
val la_generic_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
47 |
val rewrite_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
48 |
val simp_arith_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
49 |
val lethe_deep_skolemize_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
50 |
val lethe_def : string |
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75561
diff
changeset
|
51 |
val is_lethe_def : string -> bool |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
52 |
val subproof_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
53 |
val local_input_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
54 |
val not_not_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
55 |
val contract_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
56 |
val ite_intro_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
57 |
val eq_congruent_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
58 |
val eq_congruent_pred_rule : string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
59 |
val skolemization_steps : string list |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
60 |
val theory_resolution2_rule: string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
61 |
val equiv_pos2_rule: string |
75561
b6239ed66b94
fix veriT reconstruction for and_pos and lambda-lifting
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75299
diff
changeset
|
62 |
val and_pos_rule: string |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
63 |
val th_resolution_rule: string |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
64 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
65 |
val is_skolemization: string -> bool |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
66 |
val is_skolemization_step: lethe_replay_node -> bool |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
67 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
68 |
val number_of_steps: lethe_replay_node list -> int |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
69 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
70 |
end; |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
71 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
72 |
structure Lethe_Proof: LETHE_PROOF = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
73 |
struct |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
74 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
75 |
open SMTLIB_Proof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
76 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
77 |
datatype raw_lethe_node = Raw_Lethe_Node of { |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
78 |
id: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
79 |
rule: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
80 |
args: SMTLIB.tree, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
81 |
prems: string list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
82 |
concl: SMTLIB.tree, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
83 |
declarations: (string * SMTLIB.tree) list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
84 |
subproof: raw_lethe_node list} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
85 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
86 |
fun mk_raw_node id rule args prems declarations concl subproof = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
87 |
Raw_Lethe_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
88 |
concl = concl, subproof = subproof} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
89 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
90 |
datatype lethe_node = Lethe_Node of { |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
91 |
id: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
92 |
rule: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
93 |
prems: string list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
94 |
proof_ctxt: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
95 |
concl: term} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
96 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
97 |
fun mk_node id rule prems proof_ctxt concl = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
98 |
Lethe_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
99 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
100 |
datatype lethe_replay_node = Lethe_Replay_Node of { |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
101 |
id: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
102 |
rule: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
103 |
args: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
104 |
prems: string list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
105 |
proof_ctxt: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
106 |
concl: term, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
107 |
bounds: (string * typ) list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
108 |
insts: term Symtab.table, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
109 |
declarations: (string * term) list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
110 |
subproof: (string * typ) list * term list * term list * lethe_replay_node list} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
111 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
112 |
fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
113 |
Lethe_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
114 |
concl = concl, bounds = bounds, insts = insts, declarations = declarations, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
115 |
subproof = subproof} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
116 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
117 |
datatype lethe_step = Lethe_Step of { |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
118 |
id: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
119 |
rule: string, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
120 |
prems: string list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
121 |
proof_ctxt: term list, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
122 |
concl: term, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
123 |
fixes: string list} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
124 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
125 |
fun mk_step id rule prems proof_ctxt concl fixes = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
126 |
Lethe_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
127 |
fixes = fixes} |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
128 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
129 |
val step_prefix = ".c" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
130 |
val input_rule = "input" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
131 |
val la_generic_rule = "la_generic" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
132 |
val normalized_input_rule = "__normalized_input" (*arbitrary*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
133 |
val rewrite_rule = "__rewrite" (*arbitrary*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
134 |
val subproof_rule = "subproof" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
135 |
val local_input_rule = "__local_input" (*arbitrary*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
136 |
val simp_arith_rule = "simp_arith" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
137 |
val lethe_def = "__skolem_definition" (*arbitrary*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
138 |
val not_not_rule = "not_not" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
139 |
val contract_rule = "contraction" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
140 |
val eq_congruent_pred_rule = "eq_congruent_pred" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
141 |
val eq_congruent_rule = "eq_congruent" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
142 |
val ite_intro_rule = "ite_intro" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
143 |
val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
144 |
val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
145 |
val equiv_pos2_rule = "equiv_pos2" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
146 |
val th_resolution_rule = "th_resolution" |
75561
b6239ed66b94
fix veriT reconstruction for and_pos and lambda-lifting
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75299
diff
changeset
|
147 |
val and_pos_rule = "and_pos" |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
148 |
|
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75561
diff
changeset
|
149 |
val is_lethe_def = String.isSuffix lethe_def |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
150 |
val skolemization_steps = ["sko_forall", "sko_ex"] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
151 |
val is_skolemization = member (op =) skolemization_steps |
75561
b6239ed66b94
fix veriT reconstruction for and_pos and lambda-lifting
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75299
diff
changeset
|
152 |
val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule] |
b6239ed66b94
fix veriT reconstruction for and_pos and lambda-lifting
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75299
diff
changeset
|
153 |
val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule] |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
154 |
val is_SH_trivial = member (op =) [not_not_rule, contract_rule] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
155 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
156 |
fun is_skolemization_step (Lethe_Replay_Node {id, ...}) = is_skolemization id |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
157 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
158 |
(* Even the lethe developers do not know if the following rule can still appear in proofs: *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
159 |
val lethe_deep_skolemize_rule = "deep_skolemize" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
160 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
161 |
fun number_of_steps [] = 0 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
162 |
| number_of_steps ((Lethe_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
163 |
1 + number_of_steps subproof + number_of_steps pf |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
164 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
165 |
(* proof parser *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
166 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
167 |
fun node_of p cx = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
168 |
([], cx) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
169 |
||>> `(with_fresh_names (term_of p)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
170 |
|>> snd |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
171 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
172 |
fun synctactic_var_subst old_name new_name (u $ v) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
173 |
(synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
174 |
| synctactic_var_subst old_name new_name (Abs (v, T, u)) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
175 |
Abs (if String.isPrefix old_name v then new_name else v, T, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
176 |
synctactic_var_subst old_name new_name u) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
177 |
| synctactic_var_subst old_name new_name (Free (v, T)) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
178 |
if String.isPrefix old_name v then Free (new_name, T) else Free (v, T) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
179 |
| synctactic_var_subst _ _ t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
180 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
181 |
fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
182 |
Const(\<^const_name>\<open>HOL.eq\<close>, T) $ synctactic_var_subst old_name new_name t1 $ t2 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
183 |
| synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>Trueprop\<close>, T) $ t1) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
184 |
Const(\<^const_name>\<open>Trueprop\<close>, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
185 |
| synctatic_rew_in_lhs_subst _ _ t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
186 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
187 |
fun add_bound_variables_to_ctxt cx = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
188 |
fold (update_binding o |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
189 |
(fn (s, SOME typ) => (s, Term (Free (s, type_of cx typ))))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
190 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
191 |
local |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
192 |
fun extract_symbols bds = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
193 |
bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
194 |
|> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => [([x, y], typ)] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
195 |
| t => raise (Fail ("match error " ^ @{make_string} t))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
196 |
|> flat |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
197 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
198 |
(* onepoint can bind a variable to another variable or to a constant *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
199 |
fun extract_qnt_symbols cx bds = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
200 |
bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
201 |
|> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
202 |
(case node_of (SMTLIB.Sym y) cx of |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
203 |
((_, []), _) => [([x], typ)] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
204 |
| _ => [([x, y], typ)]) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
205 |
| (SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _), typ) => [([x], typ)] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
206 |
| t => raise (Fail ("match error " ^ @{make_string} t))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
207 |
|> flat |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
208 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
209 |
fun extract_symbols_map bds = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
210 |
bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
211 |
|> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _], typ) => [([x], typ)]) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
212 |
|> flat |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
213 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
214 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
215 |
fun declared_csts _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [(x, typ)] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
216 |
| declared_csts _ "__skolem_definition" t = raise (Fail ("unrecognized skolem_definition " ^ @{make_string} t)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
217 |
| declared_csts _ _ _ = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
218 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
219 |
fun skolems_introduced_by_rule (SMTLIB.S bds) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
220 |
fold (fn (SMTLIB.S [SMTLIB.Sym "=", _, SMTLIB.Sym y]) => curry (op ::) y) bds [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
221 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
222 |
(*FIXME there is probably a way to use the information given by onepoint*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
223 |
fun bound_vars_by_rule _ "bind" (bds) = extract_symbols bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
224 |
| bound_vars_by_rule cx "onepoint" bds = extract_qnt_symbols cx bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
225 |
| bound_vars_by_rule _ "sko_forall" bds = extract_symbols_map bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
226 |
| bound_vars_by_rule _ "sko_ex" bds = extract_symbols_map bds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
227 |
| bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [([x], SOME typ)] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
228 |
| bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [_, SMTLIB.Sym x, _], _)] = [([x], NONE)] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
229 |
| bound_vars_by_rule _ _ _ = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
230 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
231 |
(* Lethe adds "?" before some variables. *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
232 |
fun remove_all_qm (SMTLIB.Sym v :: l) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
233 |
SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
234 |
| remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
235 |
| remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
236 |
| remove_all_qm (v :: l) = v :: remove_all_qm l |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
237 |
| remove_all_qm [] = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
238 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
239 |
fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
240 |
| remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
241 |
| remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
242 |
| remove_all_qm2 v = v |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
243 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
244 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
245 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
246 |
datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
247 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
248 |
fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) : |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
249 |
(raw_lethe_node list * SMTLIB.tree list * name_bindings) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
250 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
251 |
fun rotate_pair (a, (b, c)) = ((a, b), c) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
252 |
fun step_kind [] = (NO_STEP, SMTLIB.S [], []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
253 |
| step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
254 |
| step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
255 |
| step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
256 |
| step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
257 |
| step_kind p = raise (Fail ("step_kind unrec: " ^ @{make_string} p)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
258 |
fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
259 |
SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
260 |
(*replace the name binding by the constant instead of the full term in order to reduce |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
261 |
the size of the generated terms and therefore the reconstruction time*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
262 |
let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
263 |
|> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
264 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
265 |
(mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
266 |
(SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
267 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
268 |
| parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S l]) cx = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
269 |
let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
270 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
271 |
(mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
272 |
(SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
273 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
274 |
| parse_skolem t _ = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
275 |
fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
276 |
| get_id_cx t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
277 |
fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
278 |
| get_id t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
279 |
fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
280 |
(SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
281 |
| parse_source (l, cx) = (NONE, (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
282 |
fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
283 |
| parse_rule t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
284 |
fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
285 |
| parse_anchor_step t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
286 |
fun parse_args (SMTLIB.Key "args" :: args :: l, cx) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
287 |
let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
288 |
in (args, (l, cx)) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
289 |
| parse_args (l, cx) = (SMTLIB.S [], (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
290 |
fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
291 |
(SMTLIB.Sym "false", (l, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
292 |
| parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
293 |
let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
294 |
in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
295 |
| parse_and_clausify_conclusion t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
296 |
val parse_normal_step = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
297 |
get_id_cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
298 |
##> parse_and_clausify_conclusion |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
299 |
#> rotate_pair |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
300 |
##> parse_rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
301 |
#> rotate_pair |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
302 |
##> parse_source |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
303 |
#> rotate_pair |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
304 |
##> parse_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
305 |
#> rotate_pair |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
306 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
307 |
fun to_raw_node subproof ((((id, concl), rule), prems), args) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
308 |
mk_raw_node id rule args (the_default [] prems) [] concl subproof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
309 |
fun at_discharge NONE _ = false |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
310 |
| at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
311 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
312 |
case step_kind ls of |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
313 |
(NO_STEP, _, _) => ([],[], cx) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
314 |
| (NORMAL_STEP, p, l) => |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
315 |
if at_discharge limit p then ([], ls, cx) else |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
316 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
317 |
(*ignores content of "discharge": Isabelle is keeping track of it via the context*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
318 |
val (s, (_, cx)) = (p, cx) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
319 |
|> parse_normal_step |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
320 |
|>> (to_raw_node []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
321 |
val (rp, rl, cx) = parse_raw_proof_steps limit l cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
322 |
in (s :: rp, rl, cx) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
323 |
| (ASSUME, p, l) => |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
324 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
325 |
val (id, t :: []) = p |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
326 |
|> get_id |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
327 |
val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
328 |
val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
329 |
val (rp, rl, cx) = parse_raw_proof_steps limit l cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
330 |
in (s :: rp, rl, cx) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
331 |
| (ANCHOR, p, l) => |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
332 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
333 |
val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
334 |
val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
335 |
val (curss, (_, cx)) = parse_normal_step (discharge_step, cx) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
336 |
val s = to_raw_node subproof (fst curss, anchor_args) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
337 |
val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
338 |
in (s :: rp, rl, cx) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
339 |
| (SKOLEM, p, l) => |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
340 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
341 |
val (s, cx) = parse_skolem p cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
342 |
val (rp, rl, cx) = parse_raw_proof_steps limit l cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
343 |
in (s :: rp, rl, cx) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
344 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
345 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
346 |
fun proof_ctxt_of_rule "bind" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
347 |
| proof_ctxt_of_rule "sko_forall" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
348 |
| proof_ctxt_of_rule "sko_ex" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
349 |
| proof_ctxt_of_rule "let" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
350 |
| proof_ctxt_of_rule "onepoint" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
351 |
| proof_ctxt_of_rule _ _ = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
352 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
353 |
fun args_of_rule "bind" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
354 |
| args_of_rule "la_generic" t = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
355 |
| args_of_rule _ _ = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
356 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
357 |
fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
358 |
| insts_of_forall_inst _ _ = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
359 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
360 |
fun id_of_last_step prems = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
361 |
if null prems then [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
362 |
else |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
363 |
let val Lethe_Replay_Node {id, ...} = List.last prems in [id] end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
364 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
365 |
fun extract_assumptions_from_subproof subproof = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
366 |
let fun extract_assumptions_from_subproof (Lethe_Replay_Node {rule, concl, ...}) assms = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
367 |
if rule = local_input_rule then concl :: assms else assms |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
368 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
369 |
fold extract_assumptions_from_subproof subproof [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
370 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
371 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
372 |
fun normalized_rule_name id rule = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
373 |
(case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
374 |
(true, true) => normalized_input_rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
375 |
| (true, _) => local_input_rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
376 |
| _ => rule) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
377 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
378 |
fun is_assm_repetition id rule = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
379 |
rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
380 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
381 |
fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
382 |
| extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
383 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
384 |
(* The preprocessing takes care of: |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
385 |
1. unfolding the shared terms |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
386 |
2. extract the declarations of skolems to make sure that there are not unfolded |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
387 |
*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
388 |
fun preprocess compress step = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
389 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
390 |
fun expand_assms cs = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
391 |
map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
392 |
fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
393 |
| expand_lonely_arguments (x as SMTLIB.S [SMTLIB.Sym var, _]) = [SMTLIB.S [SMTLIB.Sym "=", x, SMTLIB.Sym var]] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
394 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
395 |
fun preprocess (Raw_Lethe_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
396 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
397 |
val (skolem_names, stripped_args) = args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
398 |
|> (fn SMTLIB.S args => args) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
399 |
|> map |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
400 |
(fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
401 |
| x => x) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
402 |
|> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
403 |
|> `(if rule = lethe_def then single o extract_skolem else K []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
404 |
||> SMTLIB.S |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
405 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
406 |
val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
407 |
val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
408 |
(* declare variables in the context *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
409 |
val declarations = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
410 |
if rule = lethe_def |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
411 |
then skolem_names |> map (fn (name, _, choice) => (name, choice)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
412 |
else [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
413 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
414 |
if compress andalso rule = "or" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
415 |
then ([], (cx, remap_assms)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
416 |
else ([Raw_Lethe_Node {id = id, rule = rule, args = stripped_args, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
417 |
prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}], |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
418 |
(cx, remap_assms)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
419 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
420 |
in preprocess step end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
421 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
422 |
fun filter_split _ [] = ([], []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
423 |
| filter_split f (a :: xs) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
424 |
(if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
425 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
426 |
fun extract_types_of_args (SMTLIB.S [var, typ, t as SMTLIB.S [SMTLIB.Sym "choice", _, _]]) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
427 |
(SMTLIB.S [var, typ, t], SOME typ) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
428 |
|> single |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
429 |
| extract_types_of_args (SMTLIB.S t) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
430 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
431 |
fun extract_types_of_arg (SMTLIB.S [eq, SMTLIB.S [var, typ], t]) = (SMTLIB.S [eq, var, t], SOME typ) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
432 |
| extract_types_of_arg t = (t, NONE) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
433 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
434 |
t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
435 |
|> map extract_types_of_arg |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
436 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
437 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
438 |
fun collect_skolem_defs (Raw_Lethe_Node {rule, subproof = subproof, args, ...}) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
439 |
(if is_skolemization rule then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule args) else []) @ |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
440 |
flat (map collect_skolem_defs subproof) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
441 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
442 |
(*The postprocessing does: |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
443 |
1. translate the terms to Isabelle syntax, taking care of free variables |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
444 |
2. remove the ambiguity in the proof terms: |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
445 |
x \<leadsto> y |- x = x |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
446 |
means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
447 |
by: |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
448 |
xy \<leadsto> y |- xy = x. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
449 |
This is now does not have an ambiguity and we can safely move the "xy \<leadsto> y" to the proof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
450 |
assumptions. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
451 |
*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
452 |
fun postprocess_proof compress ctxt step cx = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
453 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
454 |
fun postprocess (Raw_Lethe_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
455 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
456 |
val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
457 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
458 |
val args = extract_types_of_args args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
459 |
val globally_bound_vars = declared_csts cx rule args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
460 |
val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ))))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
461 |
globally_bound_vars cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
462 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
463 |
(*find rebound variables specific to the LHS of the equivalence symbol*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
464 |
val bound_vars = bound_vars_by_rule cx rule args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
465 |
val bound_vars_no_typ = map fst bound_vars |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
466 |
val rhs_vars = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
467 |
fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars_no_typ [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
468 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
469 |
fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
470 |
not (member (op =) rhs_vars t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
471 |
val (shadowing_vars, rebound_lhs_vars) = bound_vars |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
472 |
|> filter_split (fn ([t, _], typ) => not_already_bound cx t | _ => true) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
473 |
|>> map (apfst (hd)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
474 |
|>> (fn vars => vars @ flat (map (fn ([_, t], typ) => [(t, typ)] | _ => []) bound_vars)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
475 |
val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t')) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
476 |
(map fst rebound_lhs_vars) rew |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
477 |
val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t') |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
478 |
subproof_rew |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
479 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
480 |
val ((concl, bounds), cx') = node_of concl cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
481 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
482 |
val extra_lhs_vars = map (fn ([a,b], typ) => (a, a^b, typ)) rebound_lhs_vars |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
483 |
val old_lhs_vars = map (fn (a, _, typ) => (a, typ)) extra_lhs_vars |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
484 |
val new_lhs_vars = map (fn (_, newvar, typ) => (newvar, typ)) extra_lhs_vars |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
485 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
486 |
(* postprocess conclusion *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
487 |
val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
488 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
489 |
val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
490 |
val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx', |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
491 |
"bound_vars =", bound_vars)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
492 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
493 |
val bound_tvars = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
494 |
map (fn (s, SOME typ) => (s, type_of cx typ)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
495 |
(shadowing_vars @ new_lhs_vars) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
496 |
val subproof_cx = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
497 |
add_bound_variables_to_ctxt cx (shadowing_vars @ new_lhs_vars) cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
498 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
499 |
fun could_unify (Bound i, Bound j) = i = j |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
500 |
| could_unify (Var v, Var v') = v = v' |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
501 |
| could_unify (Free v, Free v') = v = v' |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
502 |
| could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty' |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
503 |
| could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy') |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
504 |
| could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v') |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
505 |
| could_unify _ = false |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
506 |
fun is_alpha_renaming t = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
507 |
t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
508 |
|> HOLogic.dest_Trueprop |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
509 |
|> HOLogic.dest_eq |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
510 |
|> could_unify |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
511 |
handle TERM _ => false |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
512 |
val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
513 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
514 |
val can_remove_subproof = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
515 |
compress andalso (is_skolemization rule orelse alpha_conversion) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
516 |
val (fixed_subproof : lethe_replay_node list, _) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
517 |
fold_map postprocess (if can_remove_subproof then [] else subproof) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
518 |
(subproof_cx, subproof_rew) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
519 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
520 |
val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
521 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
522 |
(* postprocess assms *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
523 |
val stripped_args = map fst args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
524 |
val sanitized_args = proof_ctxt_of_rule rule stripped_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
525 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
526 |
val arg_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ old_lhs_vars) subproof_cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
527 |
val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
528 |
val normalized_args = map unsk_and_rewrite termified_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
529 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
530 |
val subproof_assms = proof_ctxt_of_rule rule normalized_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
531 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
532 |
(* postprocess arguments *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
533 |
val rule_args = args_of_rule rule stripped_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
534 |
val (termified_args, _) = fold_map term_of rule_args subproof_cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
535 |
val normalized_args = map unsk_and_rewrite termified_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
536 |
val rule_args = map subproof_rewriter normalized_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
537 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
538 |
val raw_insts = insts_of_forall_inst rule stripped_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
539 |
fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
540 |
val (termified_args, _) = fold_map termify_term raw_insts subproof_cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
541 |
val insts = Symtab.empty |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
542 |
|> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
543 |
|> Symtab.map (K unsk_and_rewrite) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
544 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
545 |
(* declarations *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
546 |
val (declarations, _) = fold_map termify_term declarations cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
547 |
|> apfst (map (apsnd unsk_and_rewrite)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
548 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
549 |
(* fix step *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
550 |
val _ = if bounds <> [] then raise (Fail "found dangling variable in concl") else () |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
551 |
val skolem_defs = (if is_skolemization rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
552 |
then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule (SMTLIB.S (map fst args))) else []) |
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75561
diff
changeset
|
553 |
val skolems_of_subproof = (if compress andalso is_skolemization rule |
75299
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
554 |
then flat (map collect_skolem_defs subproof) else []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
555 |
val fixed_prems = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
556 |
prems @ (if is_assm_repetition id rule then [id] else []) @ |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
557 |
skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
558 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
559 |
(* fix subproof *) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
560 |
val normalized_rule = normalized_rule_name id rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
561 |
|> (if compress andalso alpha_conversion then K "refl" else I) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
562 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
563 |
val extra_assms2 = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
564 |
(if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
565 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
566 |
val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
567 |
[] insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
568 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
569 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
570 |
(step, (cx', rew)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
571 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
572 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
573 |
postprocess step (cx, []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
574 |
|> (fn (step, (cx, _)) => (step, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
575 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
576 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
577 |
fun combine_proof_steps ((step1 : lethe_replay_node) :: step2 :: steps) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
578 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
579 |
val (Lethe_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
580 |
proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
581 |
declarations = declarations1, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
582 |
subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
583 |
val (Lethe_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
584 |
proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
585 |
declarations = declarations2, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
586 |
subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
587 |
val goals1 = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
588 |
(case concl1 of |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
589 |
_ $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
590 |
(Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.Not\<close>, _) $a) $ b)) => [a,b] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
591 |
| _ => []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
592 |
val goal2 = (case concl2 of _ $ a => a) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
593 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
594 |
if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
595 |
andalso member (op =) goals1 goal2 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
596 |
then |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
597 |
mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
598 |
proof_ctxt2 concl2 bounds2 insts2 declarations2 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
599 |
(bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) :: |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
600 |
combine_proof_steps steps |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
601 |
else |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
602 |
mk_replay_node id1 rule1 args1 prems1 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
603 |
proof_ctxt1 concl1 bounds1 insts1 declarations1 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
604 |
(bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) :: |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
605 |
combine_proof_steps (step2 :: steps) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
606 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
607 |
| combine_proof_steps steps = steps |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
608 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
609 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
610 |
val linearize_proof = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
611 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
612 |
fun map_node_concl f (Lethe_Node {id, rule, prems, proof_ctxt, concl}) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
613 |
mk_node id rule prems proof_ctxt (f concl) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
614 |
fun linearize (Lethe_Replay_Node {id = id, rule = rule, args = _, prems = prems, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
615 |
proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
616 |
subproof = (bounds', assms, inputs, subproof)}) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
617 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
618 |
val bounds = distinct (op =) bounds |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
619 |
val bounds' = distinct (op =) bounds' |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
620 |
fun mk_prop_of_term concl = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
621 |
concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close> |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
622 |
fun remove_assumption_id assumption_id prems = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
623 |
filter_out (curry (op =) assumption_id) prems |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
624 |
fun add_assumption assumption concl = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
625 |
\<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close> |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
626 |
fun inline_assumption assumption assumption_id |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
627 |
(Lethe_Node {id, rule, prems, proof_ctxt, concl}) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
628 |
mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
629 |
(add_assumption assumption concl) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
630 |
fun find_input_steps_and_inline [] = [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
631 |
| find_input_steps_and_inline |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
632 |
(Lethe_Node {id = id', rule, prems, concl, ...} :: steps) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
633 |
if rule = input_rule then |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
634 |
find_input_steps_and_inline (map (inline_assumption concl id') steps) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
635 |
else |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
636 |
mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
637 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
638 |
fun free_bounds bounds (concl) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
639 |
fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
640 |
val subproof = subproof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
641 |
|> flat o map linearize |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
642 |
|> map (map_node_concl (fold add_assumption (assms @ inputs))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
643 |
|> map (map_node_concl (free_bounds (bounds @ bounds'))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
644 |
|> find_input_steps_and_inline |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
645 |
val concl = free_bounds bounds concl |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
646 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
647 |
subproof @ [mk_node id rule prems proof_ctxt concl] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
648 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
649 |
in linearize end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
650 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
651 |
fun rule_of (Lethe_Replay_Node {rule,...}) = rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
652 |
fun subproof_of (Lethe_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
653 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
654 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
655 |
(* Massage Skolems for Sledgehammer. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
656 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
657 |
We have to make sure that there is an "arrow" in the graph for skolemization steps. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
658 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
659 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
660 |
A. The normal easy case |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
661 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
662 |
This function detects the steps of the form |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
663 |
P \<longleftrightarrow> Q :skolemization |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
664 |
Q :resolution with P |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
665 |
and replace them by |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
666 |
Q :skolemization |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
667 |
Throwing away the step "P \<longleftrightarrow> Q" completely. This throws away a lot of information, but it does not |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
668 |
matter too much for Sledgehammer. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
669 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
670 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
671 |
B. Skolems in subproofs |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
672 |
Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
673 |
does not support more features like definitions. lethe is able to generate proofs with skolemization |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
674 |
happening in subproofs inside the formula. |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
675 |
(assume "A \<or> P" |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
676 |
... |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
677 |
P \<longleftrightarrow> Q :skolemization in the subproof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
678 |
...) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
679 |
hence A \<or> P \<longrightarrow> A \<or> Q :lemma |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
680 |
... |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
681 |
R :something with some rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
682 |
and replace them by |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
683 |
R :skolemization with some rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
684 |
Without any subproof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
685 |
*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
686 |
fun remove_skolem_definitions_proof steps = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
687 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
688 |
fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\<open>HOL.eq\<close>, typ) $ arg1) $ arg2)) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
689 |
judgement $ ((Const(\<^const_name>\<open>HOL.implies\<close>, typ) $ arg1) $ arg2) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
690 |
| replace_equivalent_by_imp a = a (*This case is probably wrong*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
691 |
fun remove_skolem_definitions (Lethe_Replay_Node {id = id, rule = rule, args = args, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
692 |
prems = prems, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
693 |
proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
694 |
declarations = declarations, |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
695 |
subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
696 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
697 |
val prems = prems |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
698 |
|> filter_out (member (op =) prems_to_remove) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
699 |
val trivial_step = is_SH_trivial rule |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
700 |
fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
701 |
else fold has_skolem_substep (subproof_of st) NONE |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
702 |
| has_skolem_substep _ a = a |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
703 |
val promote_to_skolem = exists (fn t => member (op =) skolems t) prems |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
704 |
val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
705 |
val promote_step = promote_to_skolem orelse promote_from_assms |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
706 |
val skolem_step_to_skip = is_skolemization rule orelse |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
707 |
(promote_from_assms andalso length prems > 1) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
708 |
val is_skolem = is_skolemization rule orelse promote_step |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
709 |
val prems = prems |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
710 |
|> filter_out (fn t => member (op =) skolems t) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
711 |
|> is_skolem ? filter_out (String.isPrefix id) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
712 |
val rule = (if promote_step then default_skolem_rule else rule) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
713 |
val subproof = subproof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
714 |
|> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
715 |
|> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems))) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
716 |
(*no new definitions in subproofs*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
717 |
|> flat |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
718 |
val concl = concl |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
719 |
|> is_skolem ? replace_equivalent_by_imp |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
720 |
val step = (if skolem_step_to_skip orelse rule = lethe_def orelse trivial_step then [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
721 |
else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
722 |
(vars, assms', extra_assms', subproof) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
723 |
|> single) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
724 |
val defs = (if rule = lethe_def orelse trivial_step then id :: prems_to_remove |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
725 |
else prems_to_remove) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
726 |
val skolems = (if skolem_step_to_skip then id :: skolems else skolems) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
727 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
728 |
(step, (defs, skolems)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
729 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
730 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
731 |
fold_map remove_skolem_definitions steps ([], []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
732 |
|> fst |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
733 |
|> flat |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
734 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
735 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
736 |
local |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
737 |
(*TODO useful?*) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
738 |
fun remove_pattern (SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.S _])) = t |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
739 |
| remove_pattern (SMTLIB.S xs) = SMTLIB.S (map remove_pattern xs) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
740 |
| remove_pattern p = p |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
741 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
742 |
fun import_proof_and_post_process typs funs lines ctxt = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
743 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
744 |
val compress = SMT_Config.compress_verit_proofs ctxt |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
745 |
val smtlib_lines_without_qm = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
746 |
lines |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
747 |
|> map single |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
748 |
|> map SMTLIB.parse |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
749 |
|> map remove_all_qm2 |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
750 |
|> map remove_pattern |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
751 |
val (raw_steps, _, _) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
752 |
parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
753 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
754 |
fun process step (cx, cx') = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
755 |
let fun postprocess step (cx, cx') = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
756 |
let val (step, cx) = postprocess_proof compress ctxt step cx |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
757 |
in (step, (cx, cx')) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
758 |
in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
759 |
val step = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
760 |
(empty_context ctxt typs funs, []) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
761 |
|> fold_map process raw_steps |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
762 |
|> (fn (steps, (cx, _)) => (flat steps, cx)) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
763 |
|> compress? apfst combine_proof_steps |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
764 |
in step end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
765 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
766 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
767 |
fun parse typs funs lines ctxt = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
768 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
769 |
val (u, env) = import_proof_and_post_process typs funs lines ctxt |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
770 |
val t = u |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
771 |
|> remove_skolem_definitions_proof |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
772 |
|> flat o (map linearize_proof) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
773 |
fun node_to_step (Lethe_Node {id, rule, prems, concl, ...}) = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
774 |
mk_step id rule prems [] concl [] |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
775 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
776 |
(map node_to_step t, ctxt_of env) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
777 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
778 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
779 |
fun parse_replay typs funs lines ctxt = |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
780 |
let |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
781 |
val (u, env) = import_proof_and_post_process typs funs lines ctxt |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
782 |
val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
783 |
in |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
784 |
(u, ctxt_of env) |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
785 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
786 |
end |
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
787 |
|
da591621d6ae
split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
788 |
end; |