author | boehmes |
Wed, 12 May 2010 23:54:01 +0200 | |
changeset 36897 | 6d1ecdb81ff0 |
parent 36893 | 48cf03469dc6 |
permissions | -rw-r--r-- |
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/SMT/Tools/smt_translate.ML |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
3 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
4 |
Translate theorems into an SMT intermediate format and serialize them. |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
5 |
*) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
6 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
7 |
signature SMT_TRANSLATE = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
8 |
sig |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
9 |
(* intermediate term structure *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
10 |
datatype squant = SForall | SExists |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
11 |
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
12 |
datatype sterm = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
13 |
SVar of int | |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
14 |
SApp of string * sterm list | |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
15 |
SLet of string * sterm * sterm | |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
16 |
SQua of squant * string list * sterm spattern list * sterm |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
17 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
18 |
(* configuration options *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
19 |
type prefixes = {sort_prefix: string, func_prefix: string} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
20 |
type strict = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
21 |
is_builtin_conn: string * typ -> bool, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
22 |
is_builtin_pred: string * typ -> bool, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
23 |
is_builtin_distinct: bool} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
24 |
type builtins = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
25 |
builtin_typ: typ -> string option, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
26 |
builtin_num: typ -> int -> string option, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
27 |
builtin_fun: string * typ -> term list -> (string * term list) option } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
28 |
datatype smt_theory = Integer | Real | Bitvector |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
29 |
type sign = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
30 |
theories: smt_theory list, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
31 |
sorts: string list, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
32 |
funcs: (string * (string list * string)) list } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
33 |
type config = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
34 |
prefixes: prefixes, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
35 |
strict: strict option, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
36 |
builtins: builtins, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
37 |
serialize: sign -> sterm list -> string } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
38 |
type recon = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
39 |
typs: typ Symtab.table, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
40 |
terms: term Symtab.table, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
41 |
unfolds: thm list, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
42 |
assms: thm list option } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
43 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
44 |
val translate: config -> Proof.context -> thm list -> string * recon |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
45 |
end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
46 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
47 |
structure SMT_Translate: SMT_TRANSLATE = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
48 |
struct |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
49 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
50 |
(* intermediate term structure *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
51 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
52 |
datatype squant = SForall | SExists |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
53 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
54 |
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
55 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
56 |
datatype sterm = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
57 |
SVar of int | |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
58 |
SApp of string * sterm list | |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
59 |
SLet of string * sterm * sterm | |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
60 |
SQua of squant * string list * sterm spattern list * sterm |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
61 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
62 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
63 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
64 |
(* configuration options *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
65 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
66 |
type prefixes = {sort_prefix: string, func_prefix: string} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
67 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
68 |
type strict = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
69 |
is_builtin_conn: string * typ -> bool, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
70 |
is_builtin_pred: string * typ -> bool, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
71 |
is_builtin_distinct: bool} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
72 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
73 |
type builtins = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
74 |
builtin_typ: typ -> string option, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
75 |
builtin_num: typ -> int -> string option, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
76 |
builtin_fun: string * typ -> term list -> (string * term list) option } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
77 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
78 |
datatype smt_theory = Integer | Real | Bitvector |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
79 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
80 |
type sign = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
81 |
theories: smt_theory list, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
82 |
sorts: string list, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
83 |
funcs: (string * (string list * string)) list } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
84 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
85 |
type config = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
86 |
prefixes: prefixes, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
87 |
strict: strict option, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
88 |
builtins: builtins, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
89 |
serialize: sign -> sterm list -> string } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
90 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
91 |
type recon = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
92 |
typs: typ Symtab.table, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
93 |
terms: term Symtab.table, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
94 |
unfolds: thm list, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
95 |
assms: thm list option } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
96 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
97 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
98 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
99 |
(* utility functions *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
100 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
101 |
val dest_funT = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
102 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
103 |
fun dest Ts 0 T = (rev Ts, T) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
104 |
| dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
105 |
| dest _ _ T = raise TYPE ("dest_funT", [T], []) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
106 |
in dest [] end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
107 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
108 |
val quantifier = (fn |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
109 |
@{const_name All} => SOME SForall |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
110 |
| @{const_name Ex} => SOME SExists |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
111 |
| _ => NONE) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
112 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
113 |
fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
114 |
if q = qname then group_quant qname (T :: Ts) u else (Ts, t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
115 |
| group_quant _ Ts t = (Ts, t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
116 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
117 |
fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts)) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
118 |
| dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts)) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
119 |
| dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
120 |
| dest_pat _ t = raise TERM ("dest_pat", [t]) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
121 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
122 |
fun dest_trigger (@{term trigger} $ tl $ t) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
123 |
(map (dest_pat []) (HOLogic.dest_list tl), t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
124 |
| dest_trigger t = ([], t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
125 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
126 |
fun dest_quant qn T t = quantifier qn |> Option.map (fn q => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
127 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
128 |
val (Ts, u) = group_quant qn [T] t |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
129 |
val (ps, b) = dest_trigger u |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
130 |
in (q, rev Ts, ps, b) end) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
131 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
132 |
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
133 |
| fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
134 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
135 |
fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
136 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
137 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
138 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
139 |
(* enforce a strict separation between formulas and terms *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
140 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
141 |
val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
142 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
143 |
val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
144 |
val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
145 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
146 |
|
36897
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
147 |
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
148 |
Const (@{const_name Let}, _) => true |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
149 |
| @{term "op = :: bool => _"} $ _ $ @{term True} => true |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
150 |
| Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true |
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
151 |
| _ => false) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
152 |
|
36897
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
153 |
val rewrite_rules = [ |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
154 |
Let_def, |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
155 |
@{lemma "P = True == P" by (rule eq_reflection) simp}, |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
156 |
@{lemma "if P then True else False == P" by (rule eq_reflection) simp}] |
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
157 |
|
36897
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
158 |
fun rewrite ctxt = Simplifier.full_rewrite |
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
159 |
(Simplifier.context ctxt empty_ss addsimps rewrite_rules) |
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
160 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
161 |
fun normalize ctxt thm = |
36897
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
162 |
if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm |
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
163 |
|
36897
6d1ecdb81ff0
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
boehmes
parents:
36893
diff
changeset
|
164 |
val unfold_rules = term_eq_rewr :: rewrite_rules |
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
165 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
166 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
167 |
val revert_types = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
168 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
169 |
fun revert @{typ prop} = @{typ bool} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
170 |
| revert (Type (n, Ts)) = Type (n, map revert Ts) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
171 |
| revert T = T |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
172 |
in Term.map_types revert end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
173 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
174 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
175 |
fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
176 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
177 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
178 |
fun is_builtin_conn' (@{const_name True}, _) = false |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
179 |
| is_builtin_conn' (@{const_name False}, _) = false |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
180 |
| is_builtin_conn' c = is_builtin_conn c |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
181 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
182 |
val propT = @{typ prop} and boolT = @{typ bool} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
183 |
val as_propT = (fn @{typ bool} => propT | T => T) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
184 |
fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
185 |
fun conn (n, T) = (n, mapTs as_propT as_propT T) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
186 |
fun pred (n, T) = (n, mapTs I as_propT T) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
187 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
188 |
val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
189 |
fun as_term t = Const term_eq $ t $ @{term True} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
190 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
191 |
val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
192 |
fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False} |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
193 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
194 |
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
195 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
196 |
fun in_term t = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
197 |
(case Term.strip_comb t of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
198 |
(c as Const (@{const_name If}, _), [t1, t2, t3]) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
199 |
c $ in_form t1 $ in_term t2 $ in_term t3 |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
200 |
| (h as Const c, ts) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
201 |
if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
202 |
then wrap_in_if (in_form t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
203 |
else Term.list_comb (h, map in_term ts) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
204 |
| (h as Free _, ts) => Term.list_comb (h, map in_term ts) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
205 |
| _ => t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
206 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
207 |
and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
208 |
| in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
209 |
| in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
210 |
c $ in_pat p $ in_term t |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
211 |
| in_pat t = raise TERM ("in_pat", [t]) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
212 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
213 |
and in_pats p = in_list @{typ pattern} in_pat p |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
214 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
215 |
and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
216 |
| in_trig t = in_form t |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
217 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
218 |
and in_form t = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
219 |
(case Term.strip_comb t of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
220 |
(q as Const (qn, _), [Abs (n, T, t')]) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
221 |
if is_some (quantifier qn) then q $ Abs (n, T, in_trig t') |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
222 |
else as_term (in_term t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
223 |
| (Const (c as (@{const_name distinct}, T)), [t']) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
224 |
if is_builtin_distinct then Const (pred c) $ in_list T in_term t' |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
225 |
else as_term (in_term t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
226 |
| (Const c, ts) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
227 |
if is_builtin_conn (conn c) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
228 |
then Term.list_comb (Const (conn c), map in_form ts) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
229 |
else if is_builtin_pred (pred c) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
230 |
then Term.list_comb (Const (pred c), map in_term ts) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
231 |
else as_term (in_term t) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
232 |
| _ => as_term (in_term t)) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
233 |
in |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
234 |
map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms), |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
235 |
map (in_form o prop_of) (term_bool :: thms))) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
236 |
end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
237 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
238 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
239 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
240 |
(* translation from Isabelle terms into SMT intermediate terms *) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
241 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
242 |
val empty_context = (1, Typtab.empty, 1, Termtab.empty, []) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
243 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
244 |
fun make_sign (_, typs, _, terms, thys) = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
245 |
theories = thys, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
246 |
sorts = Typtab.fold (cons o snd) typs [], |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
247 |
funcs = Termtab.fold (cons o snd) terms [] } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
248 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
249 |
fun make_recon (unfolds, assms) (_, typs, _, terms, _) = { |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
250 |
typs = Symtab.make (map swap (Typtab.dest typs)), |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
251 |
terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)), |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
252 |
unfolds = unfolds, |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
253 |
assms = SOME assms } |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
254 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
255 |
fun string_of_index pre i = pre ^ string_of_int i |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
256 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
257 |
fun add_theory T (Tidx, typs, idx, terms, thys) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
258 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
259 |
fun add @{typ int} = insert (op =) Integer |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
260 |
| add @{typ real} = insert (op =) Real |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
261 |
| add (Type (@{type_name word}, _)) = insert (op =) Bitvector |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
262 |
| add (Type (_, Ts)) = fold add Ts |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
263 |
| add _ = I |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
264 |
in (Tidx, typs, idx, terms, add T thys) end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
265 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
266 |
fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
267 |
(case Typtab.lookup typs T of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
268 |
SOME s => (s, cx) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
269 |
| NONE => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
270 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
271 |
val s = string_of_index sort_prefix Tidx |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
272 |
val typs' = Typtab.update (T, s) typs |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
273 |
in (s, (Tidx+1, typs', idx, terms, thys)) end) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
274 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
275 |
fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
276 |
(case Termtab.lookup terms t of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
277 |
SOME (f, _) => (f, cx) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
278 |
| NONE => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
279 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
280 |
val f = string_of_index func_prefix idx |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
281 |
val terms' = Termtab.update (revert_types t, (f, ss)) terms |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
282 |
in (f, (Tidx, typs, idx+1, terms', thys)) end) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
283 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
284 |
fun relaxed thms = (([], thms), map prop_of thms) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
285 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
286 |
fun with_context f (ths, ts) = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
287 |
let val (us, context) = fold_map f ts empty_context |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
288 |
in ((make_sign context, us), make_recon ths context) end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
289 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
290 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
291 |
fun translate {prefixes, strict, builtins, serialize} ctxt = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
292 |
let |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
293 |
val {sort_prefix, func_prefix} = prefixes |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
294 |
val {builtin_typ, builtin_num, builtin_fun} = builtins |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
295 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
296 |
fun transT T = add_theory T #> |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
297 |
(case builtin_typ T of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
298 |
SOME n => pair n |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
299 |
| NONE => fresh_typ sort_prefix T) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
300 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
301 |
fun app n ts = SApp (n, ts) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
302 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
303 |
fun trans t = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
304 |
(case Term.strip_comb t of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
305 |
(Const (qn, _), [Abs (_, T, t1)]) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
306 |
(case dest_quant qn T t1 of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
307 |
SOME (q, Ts, ps, b) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
308 |
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
309 |
trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
310 |
| NONE => raise TERM ("intermediate", [t])) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
311 |
| (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
312 |
transT T ##>> trans t1 ##>> trans t2 #>> |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
313 |
(fn ((U, u1), u2) => SLet (U, u1, u2)) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
314 |
| (h as Const (c as (@{const_name distinct}, T)), [t1]) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
315 |
(case builtin_fun c (HOLogic.dest_list t1) of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
316 |
SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
317 |
| NONE => transs h T [t1]) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
318 |
| (h as Const (c as (_, T)), ts) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
319 |
(case try HOLogic.dest_number t of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
320 |
SOME (T, i) => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
321 |
(case builtin_num T i of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
322 |
SOME n => add_theory T #> pair (SApp (n, [])) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
323 |
| NONE => transs t T []) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
324 |
| NONE => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
325 |
(case builtin_fun c ts of |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
326 |
SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
327 |
| NONE => transs h T ts)) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
328 |
| (h as Free (_, T), ts) => transs h T ts |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
329 |
| (Bound i, []) => pair (SVar i) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
330 |
| _ => raise TERM ("intermediate", [t])) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
331 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
332 |
and transs t T ts = |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
333 |
let val (Us, U) = dest_funT (length ts) T |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
334 |
in |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
335 |
fold_map transT Us ##>> transT U #-> (fn Up => |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
336 |
fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp) |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
337 |
end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
338 |
in |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
339 |
(if is_some strict then strictify (the strict) ctxt else relaxed) #> |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
340 |
with_context trans #>> uncurry serialize |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
341 |
end |
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
342 |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
343 |
end |