author | wenzelm |
Wed, 06 Dec 2017 20:43:09 +0100 | |
changeset 67149 | e61557884799 |
parent 66738 | 793e7a9c30c5 |
child 74382 | 8d0294d877bd |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smt_translate.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Translate theorems into an SMT intermediate format and serialize them. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
|
58061 | 7 |
signature SMT_TRANSLATE = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
sig |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
(*intermediate term structure*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
datatype squant = SForall | SExists |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
datatype sterm = |
66551 | 13 |
SVar of int * sterm list | |
14 |
SConst of string * sterm list | |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
15 |
SQua of squant * string list * sterm spattern list * sterm |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
(*translation configuration*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
type sign = { |
57238 | 19 |
logic: string, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
sorts: string list, |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
21 |
dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
funcs: (string * (string list * string)) list } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
type config = { |
66551 | 24 |
order: SMT_Util.order, |
57238 | 25 |
logic: term list -> string, |
58360 | 26 |
fp_kinds: BNF_Util.fp_kind list, |
57239 | 27 |
serialize: (string * string) list -> string list -> sign -> sterm list -> string } |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
28 |
type replay_data = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
context: Proof.context, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
typs: typ Symtab.table, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
terms: term Symtab.table, |
57541 | 32 |
ll_defs: term list, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
rewrite_rules: thm list, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
34 |
assms: (int * thm) list } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
(*translation*) |
58061 | 37 |
val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic |
57239 | 38 |
val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list -> |
39 |
string * replay_data |
|
57229 | 40 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
41 |
|
58061 | 42 |
structure SMT_Translate: SMT_TRANSLATE = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
(* intermediate term structure *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
datatype squant = SForall | SExists |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
|
66134
a1fb6beb2731
correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code
blanchet
parents:
61782
diff
changeset
|
50 |
datatype 'a spattern = |
a1fb6beb2731
correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code
blanchet
parents:
61782
diff
changeset
|
51 |
SPat of 'a list | SNoPat of 'a list |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
52 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
datatype sterm = |
66551 | 54 |
SVar of int * sterm list | |
55 |
SConst of string * sterm list | |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
56 |
SQua of squant * string list * sterm spattern list * sterm |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
57 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
59 |
(* translation configuration *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
type sign = { |
57238 | 62 |
logic: string, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
sorts: string list, |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
64 |
dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
funcs: (string * (string list * string)) list } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
66 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
67 |
type config = { |
66551 | 68 |
order: SMT_Util.order, |
57238 | 69 |
logic: term list -> string, |
58360 | 70 |
fp_kinds: BNF_Util.fp_kind list, |
57239 | 71 |
serialize: (string * string) list -> string list -> sign -> sterm list -> string } |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
72 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
73 |
type replay_data = { |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
74 |
context: Proof.context, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
75 |
typs: typ Symtab.table, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
76 |
terms: term Symtab.table, |
57541 | 77 |
ll_defs: term list, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
rewrite_rules: thm list, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
79 |
assms: (int * thm) list } |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
80 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
81 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
82 |
(* translation context *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
83 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
84 |
fun add_components_of_typ (Type (s, Ts)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
86 |
| add_components_of_typ (TFree (s, _)) = cons (perhaps (try (unprefix "'")) s) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
87 |
| add_components_of_typ _ = I; |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
88 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
89 |
fun suggested_name_of_typ T = space_implode "_" (add_components_of_typ T []); |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
90 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
91 |
fun suggested_name_of_term (Const (s, _)) = Long_Name.base_name s |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
92 |
| suggested_name_of_term (Free (s, _)) = s |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
93 |
| suggested_name_of_term _ = Name.uu |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
94 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
95 |
val empty_tr_context = (Name.context, Typtab.empty, Termtab.empty) |
56096
3e717b56e955
avoid names that may clash with Z3's output (e.g. '')
blanchet
parents:
56090
diff
changeset
|
96 |
val safe_suffix = "$" |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
98 |
fun add_typ T proper (cx as (names, typs, terms)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
99 |
(case Typtab.lookup typs T of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
100 |
SOME (name, _) => (name, cx) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
101 |
| NONE => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
102 |
let |
56811 | 103 |
val sugg = Name.desymbolize (SOME true) (suggested_name_of_typ T) ^ safe_suffix |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
104 |
val (name, names') = Name.variant sugg names |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
val typs' = Typtab.update (T, (name, proper)) typs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
106 |
in (name, (names', typs', terms)) end) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
fun add_fun t sort (cx as (names, typs, terms)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
(case Termtab.lookup terms t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
SOME (name, _) => (name, cx) |
57230 | 111 |
| NONE => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
112 |
let |
56811 | 113 |
val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
val (name, names') = Name.variant sugg names |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
115 |
val terms' = Termtab.update (t, (name, sort)) terms |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
in (name, (names', typs, terms')) end) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
118 |
fun sign_of logic dtyps (_, typs, terms) = { |
57238 | 119 |
logic = logic, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
121 |
dtyps = dtyps, |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
|
57541 | 124 |
fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
fun add_typ (T, (n, _)) = Symtab.update (n, T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
val typs' = Typtab.fold add_typ typs Symtab.empty |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
fun add_fun (t, (n, _)) = Symtab.update (n, t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
val terms' = Termtab.fold add_fun terms Symtab.empty |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
in |
57541 | 132 |
{context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules, |
133 |
assms = assms} |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
136 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
(* preprocessing *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
|
58361 | 139 |
(** (co)datatype declarations **) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
140 |
|
58361 | 141 |
fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
142 |
let |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
143 |
val (fp_decls, ctxt') = |
58361 | 144 |
([], ctxt) |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
145 |
|> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds)) ts |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
146 |
|>> flat |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
147 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
148 |
fun is_decl_typ T = exists (equal T o fst o snd) fp_decls |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
150 |
fun add_typ' T proper = |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
151 |
(case SMT_Builtin.dest_builtin_typ ctxt' T of |
66551 | 152 |
SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
153 |
| NONE => add_typ T proper) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
fun tr_select sel = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
156 |
let val T = Term.range_type (Term.fastype_of sel) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
fun tr_constr (constr, selects) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
159 |
add_fun constr NONE ##>> fold_map tr_select selects |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
160 |
fun tr_typ (fp, (T, cases)) = |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
161 |
add_typ' T false ##>> fold_map tr_constr cases #>> pair fp |
58361 | 162 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
163 |
val (fp_decls', tr_context') = fold_map tr_typ fp_decls tr_context |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
164 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
165 |
fun add (constr, selects) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
166 |
Termtab.update (constr, length selects) #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
167 |
fold (Termtab.update o rpair 1) selects |
58361 | 168 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
169 |
val funcs = fold (fold add o snd o snd) fp_decls Termtab.empty |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
170 |
|
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
171 |
in ((funcs, fp_decls', tr_context', ctxt'), ts) end |
58361 | 172 |
(* FIXME: also return necessary (co)datatype theorems *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
174 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
175 |
(** eta-expand quantifiers, let expressions and built-ins *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
176 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
177 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
178 |
fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
179 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
180 |
fun exp f T = eta f (Term.domain_type (Term.domain_type T)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
181 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
182 |
fun exp2 T q = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
let val U = Term.domain_type T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
184 |
in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
185 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
186 |
fun expf k i T t = |
58061 | 187 |
let val Ts = drop i (fst (SMT_Util.dest_funT k T)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
188 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
189 |
Term.incr_boundvars (length Ts) t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
190 |
|> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
191 |
|> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
192 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
193 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
194 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
195 |
fun eta_expand ctxt funcs = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
196 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
197 |
fun exp_func t T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
198 |
(case Termtab.lookup funcs t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
199 |
SOME k => Term.list_comb (t, ts) |> k <> length ts ? expf k (length ts) T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
200 |
| NONE => Term.list_comb (t, ts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
201 |
|
67149 | 202 |
fun expand ((q as Const (\<^const_name>\<open>All\<close>, _)) $ Abs a) = q $ abs_expand a |
203 |
| expand ((q as Const (\<^const_name>\<open>All\<close>, T)) $ t) = q $ exp expand T t |
|
204 |
| expand (q as Const (\<^const_name>\<open>All\<close>, T)) = exp2 T q |
|
205 |
| expand ((q as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs a) = q $ abs_expand a |
|
206 |
| expand ((q as Const (\<^const_name>\<open>Ex\<close>, T)) $ t) = q $ exp expand T t |
|
207 |
| expand (q as Const (\<^const_name>\<open>Ex\<close>, T)) = exp2 T q |
|
208 |
| expand (Const (\<^const_name>\<open>Let\<close>, T) $ t) = |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
209 |
let val U = Term.domain_type (Term.range_type T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
210 |
in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end |
67149 | 211 |
| expand (Const (\<^const_name>\<open>Let\<close>, T)) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
212 |
let val U = Term.domain_type (Term.range_type T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
213 |
in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
214 |
| expand t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
215 |
(case Term.strip_comb t of |
67149 | 216 |
(Const (\<^const_name>\<open>Let\<close>, _), t1 :: t2 :: ts) => |
66136 | 217 |
Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts) |
66134
a1fb6beb2731
correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code
blanchet
parents:
61782
diff
changeset
|
218 |
| (u as Const (c as (_, T)), ts) => |
58061 | 219 |
(case SMT_Builtin.dest_builtin ctxt c ts of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
220 |
SOME (_, k, us, mk) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
221 |
if k = length us then mk (map expand us) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
222 |
else if k < length us then chop k (map expand us) |>> mk |> Term.list_comb |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
223 |
else expf k (length ts) T (mk (map expand us)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
224 |
| NONE => exp_func u T (map expand ts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
225 |
| (u as Free (_, T), ts) => exp_func u T (map expand ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
226 |
| (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
227 |
| (u, ts) => Term.list_comb (u, map expand ts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
228 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
229 |
and abs_expand (n, T, t) = Abs (n, T, expand t) |
57230 | 230 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
231 |
in map expand end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
232 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
233 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
234 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
235 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
236 |
(** introduce explicit applications **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
237 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
238 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
239 |
(* |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
240 |
Make application explicit for functions with varying number of arguments. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
241 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
242 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
243 |
fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
244 |
fun add_type T = apsnd (Typtab.update (T, ())) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
245 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
246 |
fun min_arities t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
247 |
(case Term.strip_comb t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
248 |
(u as Const _, ts) => add u (length ts) #> fold min_arities ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
249 |
| (u as Free _, ts) => add u (length ts) #> fold min_arities ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
250 |
| (Abs (_, T, u), ts) => (can dest_funT T ? add_type T) #> min_arities u #> fold min_arities ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
251 |
| (_, ts) => fold min_arities ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
252 |
|
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
253 |
fun take_vars_into_account types t i = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
254 |
let |
67149 | 255 |
fun find_min j (T as Type (\<^type_name>\<open>fun\<close>, [_, T'])) = |
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
256 |
if j = i orelse Typtab.defined types T then j else find_min (j + 1) T' |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
257 |
| find_min j _ = j |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
258 |
in find_min 0 (Term.type_of t) end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
259 |
|
67149 | 260 |
fun app u (t, T) = (Const (\<^const_name>\<open>fun_app\<close>, T --> T) $ t $ u, Term.range_type T) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
261 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
262 |
fun apply i t T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
263 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
264 |
val (ts1, ts2) = chop i ts |
58061 | 265 |
val (_, U) = SMT_Util.dest_funT i T |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
266 |
in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
267 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
268 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
269 |
fun intro_explicit_application ctxt funcs ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
270 |
let |
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
271 |
val explicit_application = Config.get ctxt SMT_Config.explicit_application |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
272 |
val get_arities = |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
273 |
(case explicit_application of |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
274 |
0 => min_arities |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
275 |
| 1 => min_arities |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
276 |
| 2 => K I |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
277 |
| n => error ("Illegal value for " ^ quote (Config.name_of SMT_Config.explicit_application) ^ |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
278 |
": " ^ string_of_int n)) |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
279 |
|
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
280 |
val (arities, types) = fold get_arities ts (Termtab.empty, Typtab.empty) |
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
281 |
val arities' = arities |> explicit_application = 1 ? Termtab.map (take_vars_into_account types) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
282 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
283 |
fun app_func t T ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
284 |
if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) |
66738
793e7a9c30c5
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
blanchet
parents:
66551
diff
changeset
|
285 |
else apply (the_default 0 (Termtab.lookup arities' t)) t T ts |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
286 |
|
58061 | 287 |
fun in_list T f t = SMT_Util.mk_symb_list T (map f (SMT_Util.dest_symb_list t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
288 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
289 |
fun traverse Ts t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
290 |
(case Term.strip_comb t of |
67149 | 291 |
(q as Const (\<^const_name>\<open>All\<close>, _), [Abs (x, T, u)]) => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
292 |
q $ Abs (x, T, in_trigger (T :: Ts) u) |
67149 | 293 |
| (q as Const (\<^const_name>\<open>Ex\<close>, _), [Abs (x, T, u)]) => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
294 |
q $ Abs (x, T, in_trigger (T :: Ts) u) |
67149 | 295 |
| (q as Const (\<^const_name>\<open>Let\<close>, _), [u1, u2 as Abs _]) => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
296 |
q $ traverse Ts u1 $ traverse Ts u2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
297 |
| (u as Const (c as (_, T)), ts) => |
58061 | 298 |
(case SMT_Builtin.dest_builtin ctxt c ts of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
299 |
SOME (_, k, us, mk) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
300 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
301 |
val (ts1, ts2) = chop k (map (traverse Ts) us) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
302 |
val U = Term.strip_type T |>> snd o chop k |> (op --->) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
303 |
in apply 0 (mk ts1) U ts2 end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
304 |
| NONE => app_func u T (map (traverse Ts) ts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
305 |
| (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
306 |
| (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
307 |
| (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
308 |
| (u, ts) => traverses Ts u ts) |
67149 | 309 |
and in_trigger Ts ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
310 |
| in_trigger Ts t = traverse Ts t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
311 |
and in_pats Ts ps = |
67149 | 312 |
in_list \<^typ>\<open>pattern symb_list\<close> (in_list \<^typ>\<open>pattern\<close> (in_pat Ts)) ps |
313 |
and in_pat Ts ((p as Const (\<^const_name>\<open>pat\<close>, _)) $ t) = p $ traverse Ts t |
|
314 |
| in_pat Ts ((p as Const (\<^const_name>\<open>nopat\<close>, _)) $ t) = p $ traverse Ts t |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
315 |
| in_pat _ t = raise TERM ("bad pattern", [t]) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
316 |
and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
317 |
in map (traverse []) ts end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
318 |
|
57230 | 319 |
val fun_app_eq = mk_meta_eq @{thm fun_app_def} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
320 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
321 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
322 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
323 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
324 |
(** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
325 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
326 |
local |
67149 | 327 |
val is_quant = member (op =) [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
328 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
329 |
val fol_rules = [ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
330 |
Let_def, |
61782
7d754aca6a75
removed needless complication for modern SMT solvers
blanchet
parents:
58429
diff
changeset
|
331 |
@{lemma "P = True == P" by (rule eq_reflection) simp}] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
332 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
333 |
exception BAD_PATTERN of unit |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
334 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
335 |
fun is_builtin_conn_or_pred ctxt c ts = |
58061 | 336 |
is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse |
337 |
is_some (SMT_Builtin.dest_builtin_pred ctxt c ts) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
338 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
339 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
340 |
fun folify ctxt = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
341 |
let |
58061 | 342 |
fun in_list T f t = SMT_Util.mk_symb_list T (map_filter f (SMT_Util.dest_symb_list t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
343 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
344 |
fun in_term pat t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
345 |
(case Term.strip_comb t of |
67149 | 346 |
(\<^const>\<open>True\<close>, []) => t |
347 |
| (\<^const>\<open>False\<close>, []) => t |
|
348 |
| (u as Const (\<^const_name>\<open>If\<close>, _), [t1, t2, t3]) => |
|
56104
fd6e132ee4fb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet
parents:
56096
diff
changeset
|
349 |
if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
350 |
| (Const (c as (n, _)), ts) => |
61782
7d754aca6a75
removed needless complication for modern SMT solvers
blanchet
parents:
58429
diff
changeset
|
351 |
if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then |
7d754aca6a75
removed needless complication for modern SMT solvers
blanchet
parents:
58429
diff
changeset
|
352 |
if pat then raise BAD_PATTERN () else in_form t |
7d754aca6a75
removed needless complication for modern SMT solvers
blanchet
parents:
58429
diff
changeset
|
353 |
else |
7d754aca6a75
removed needless complication for modern SMT solvers
blanchet
parents:
58429
diff
changeset
|
354 |
Term.list_comb (Const c, map (in_term pat) ts) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
355 |
| (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
356 |
| _ => t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
357 |
|
67149 | 358 |
and in_pat ((p as Const (\<^const_name>\<open>pat\<close>, _)) $ t) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
359 |
p $ in_term true t |
67149 | 360 |
| in_pat ((p as Const (\<^const_name>\<open>nopat\<close>, _)) $ t) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
361 |
p $ in_term true t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
362 |
| in_pat t = raise TERM ("bad pattern", [t]) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
363 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
364 |
and in_pats ps = |
67149 | 365 |
in_list \<^typ>\<open>pattern symb_list\<close> (SOME o in_list \<^typ>\<open>pattern\<close> (try in_pat)) ps |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
366 |
|
67149 | 367 |
and in_trigger ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
368 |
| in_trigger t = in_form t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
369 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
370 |
and in_form t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
371 |
(case Term.strip_comb t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
372 |
(q as Const (qn, _), [Abs (n, T, u)]) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
373 |
if is_quant qn then q $ Abs (n, T, in_trigger u) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
374 |
else in_term false t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
375 |
| (Const c, ts) => |
58061 | 376 |
(case SMT_Builtin.dest_builtin_conn ctxt c ts of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
377 |
SOME (_, _, us, mk) => mk (map in_form us) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
378 |
| NONE => |
58061 | 379 |
(case SMT_Builtin.dest_builtin_pred ctxt c ts of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
380 |
SOME (_, _, us, mk) => mk (map (in_term false) us) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
381 |
| NONE => in_term false t)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
382 |
| _ => in_term false t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
383 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
384 |
map in_form #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
385 |
pair (fol_rules, I) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
386 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
387 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
388 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
389 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
390 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
391 |
(* translation into intermediate format *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
392 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
393 |
(** utility functions **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
394 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
395 |
val quantifier = (fn |
67149 | 396 |
\<^const_name>\<open>All\<close> => SOME SForall |
397 |
| \<^const_name>\<open>Ex\<close> => SOME SExists |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
398 |
| _ => NONE) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
399 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
400 |
fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
401 |
if q = qname then group_quant qname (T :: Ts) u else (Ts, t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
402 |
| group_quant _ Ts t = (Ts, t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
403 |
|
67149 | 404 |
fun dest_pat (Const (\<^const_name>\<open>pat\<close>, _) $ t) = (t, true) |
405 |
| dest_pat (Const (\<^const_name>\<open>nopat\<close>, _) $ t) = (t, false) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
406 |
| dest_pat t = raise TERM ("bad pattern", [t]) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
407 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
408 |
fun dest_pats [] = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
409 |
| dest_pats ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
410 |
(case map dest_pat ts |> split_list ||> distinct (op =) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
411 |
(ps, [true]) => cons (SPat ps) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
412 |
| (ps, [false]) => cons (SNoPat ps) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
413 |
| _ => raise TERM ("bad multi-pattern", ts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
414 |
|
67149 | 415 |
fun dest_trigger (\<^const>\<open>trigger\<close> $ tl $ t) = |
58061 | 416 |
(rev (fold (dest_pats o SMT_Util.dest_symb_list) (SMT_Util.dest_symb_list tl) []), t) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
417 |
| dest_trigger t = ([], t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
418 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
419 |
fun dest_quant qn T t = quantifier qn |> Option.map (fn q => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
420 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
421 |
val (Ts, u) = group_quant qn [T] t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
422 |
val (ps, p) = dest_trigger u |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
423 |
in (q, rev Ts, ps, p) end) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
424 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
425 |
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
426 |
| fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
427 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
428 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
429 |
(** translation from Isabelle terms into SMT intermediate terms **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
430 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
431 |
fun intermediate logic dtyps builtin ctxt ts trx = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
432 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
433 |
fun transT (T as TFree _) = add_typ T true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
434 |
| transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
435 |
| transT (T as Type _) = |
58061 | 436 |
(case SMT_Builtin.dest_builtin_typ ctxt T of |
66551 | 437 |
SOME (n, []) => pair n |
438 |
| SOME (n, Ts) => |
|
439 |
fold_map transT Ts |
|
440 |
#>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns))) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
441 |
| NONE => add_typ T true) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
442 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
443 |
fun trans t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
444 |
(case Term.strip_comb t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
445 |
(Const (qn, _), [Abs (_, T, t1)]) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
446 |
(case dest_quant qn T t1 of |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
447 |
SOME (q, Ts, ps, b) => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
448 |
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56811
diff
changeset
|
449 |
trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
450 |
| NONE => raise TERM ("unsupported quantifier", [t])) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
451 |
| (u as Const (c as (_, T)), ts) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
452 |
(case builtin ctxt c ts of |
66551 | 453 |
SOME (n, _, us, _) => fold_map trans us #>> curry SConst n |
454 |
| NONE => trans_applied_fun u T ts) |
|
455 |
| (u as Free (_, T), ts) => trans_applied_fun u T ts |
|
456 |
| (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
457 |
| _ => raise TERM ("bad SMT term", [t])) |
57230 | 458 |
|
66551 | 459 |
and trans_applied_fun t T ts = |
58061 | 460 |
let val (Us, U) = SMT_Util.dest_funT (length ts) T |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
461 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
462 |
fold_map transT Us ##>> transT U #-> (fn Up => |
66551 | 463 |
add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
464 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
465 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
466 |
val (us, trx') = fold_map trans ts trx |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
467 |
in ((sign_of (logic ts) dtyps trx', us), trx') end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
468 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
469 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
470 |
(* translation *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
471 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
472 |
structure Configs = Generic_Data |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
473 |
( |
58061 | 474 |
type T = (Proof.context -> config) SMT_Util.dict |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
475 |
val empty = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
476 |
val extend = I |
58061 | 477 |
fun merge data = SMT_Util.dict_merge fst data |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
478 |
) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
479 |
|
58061 | 480 |
fun add_config (cs, cfg) = Configs.map (SMT_Util.dict_update (cs, cfg)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
481 |
|
57230 | 482 |
fun get_config ctxt = |
58061 | 483 |
let val cs = SMT_Config.solver_class_of ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
484 |
in |
58061 | 485 |
(case SMT_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
486 |
SOME cfg => cfg ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
487 |
| NONE => error ("SMT: no translation configuration found " ^ |
58061 | 488 |
"for solver class " ^ quote (SMT_Util.string_of_class cs))) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
489 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
490 |
|
57239 | 491 |
fun translate ctxt smt_options comments ithms = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
492 |
let |
66551 | 493 |
val {order, logic, fp_kinds, serialize} = get_config ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
494 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
495 |
fun no_dtyps (tr_context, ctxt) ts = |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
496 |
((Termtab.empty, [], tr_context, ctxt), ts) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
497 |
|
58061 | 498 |
val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
499 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
500 |
val ((funcs, dtyps, tr_context, ctxt1), ts2) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
501 |
((empty_tr_context, ctxt), ts1) |
58361 | 502 |
|-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
503 |
|
67149 | 504 |
fun is_binder (Const (\<^const_name>\<open>Let\<close>, _) $ _) = true |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
505 |
| is_binder t = Lambda_Lifting.is_quantifier t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
506 |
|
67149 | 507 |
fun mk_trigger ((q as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (n, T, t)) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
508 |
q $ Abs (n, T, mk_trigger t) |
67149 | 509 |
| mk_trigger (eq as (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lhs $ _)) = |
510 |
Term.domain_type T --> \<^typ>\<open>pattern\<close> |
|
511 |
|> (fn T => Const (\<^const_name>\<open>pat\<close>, T) $ lhs) |
|
512 |
|> SMT_Util.mk_symb_list \<^typ>\<open>pattern\<close> o single |
|
513 |
|> SMT_Util.mk_symb_list \<^typ>\<open>pattern symb_list\<close> o single |
|
514 |
|> (fn t => \<^const>\<open>trigger\<close> $ t $ eq) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
515 |
| mk_trigger t = t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
516 |
|
57541 | 517 |
val (ctxt2, (ts3, ll_defs)) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
518 |
ts2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
519 |
|> eta_expand ctxt1 funcs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
520 |
|> rpair ctxt1 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
521 |
|-> Lambda_Lifting.lift_lambdas NONE is_binder |
57541 | 522 |
|-> (fn (ts', ll_defs) => fn ctxt' => |
66551 | 523 |
let |
524 |
val ts'' = map mk_trigger ll_defs @ ts' |
|
525 |
|> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs |
|
526 |
in |
|
527 |
(ctxt', (ts'', ll_defs)) |
|
528 |
end) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
529 |
val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 |
66551 | 530 |
|>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
531 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
532 |
(ts4, tr_context) |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58361
diff
changeset
|
533 |
|-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 |
57239 | 534 |
|>> uncurry (serialize smt_options comments) |
57541 | 535 |
||> replay_data_of ctxt2 ll_defs rewrite_rules ithms |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
536 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
537 |
|
57229 | 538 |
end; |