1.1 --- a/src/HOL/SMT/Tools/smt_translate.ML Wed May 12 23:54:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,343 +0,0 @@
1.4 -(* Title: HOL/SMT/Tools/smt_translate.ML
1.5 - Author: Sascha Boehme, TU Muenchen
1.6 -
1.7 -Translate theorems into an SMT intermediate format and serialize them.
1.8 -*)
1.9 -
1.10 -signature SMT_TRANSLATE =
1.11 -sig
1.12 - (* intermediate term structure *)
1.13 - datatype squant = SForall | SExists
1.14 - datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
1.15 - datatype sterm =
1.16 - SVar of int |
1.17 - SApp of string * sterm list |
1.18 - SLet of string * sterm * sterm |
1.19 - SQua of squant * string list * sterm spattern list * sterm
1.20 -
1.21 - (* configuration options *)
1.22 - type prefixes = {sort_prefix: string, func_prefix: string}
1.23 - type strict = {
1.24 - is_builtin_conn: string * typ -> bool,
1.25 - is_builtin_pred: string * typ -> bool,
1.26 - is_builtin_distinct: bool}
1.27 - type builtins = {
1.28 - builtin_typ: typ -> string option,
1.29 - builtin_num: typ -> int -> string option,
1.30 - builtin_fun: string * typ -> term list -> (string * term list) option }
1.31 - datatype smt_theory = Integer | Real | Bitvector
1.32 - type sign = {
1.33 - theories: smt_theory list,
1.34 - sorts: string list,
1.35 - funcs: (string * (string list * string)) list }
1.36 - type config = {
1.37 - prefixes: prefixes,
1.38 - strict: strict option,
1.39 - builtins: builtins,
1.40 - serialize: sign -> sterm list -> string }
1.41 - type recon = {
1.42 - typs: typ Symtab.table,
1.43 - terms: term Symtab.table,
1.44 - unfolds: thm list,
1.45 - assms: thm list option }
1.46 -
1.47 - val translate: config -> Proof.context -> thm list -> string * recon
1.48 -end
1.49 -
1.50 -structure SMT_Translate: SMT_TRANSLATE =
1.51 -struct
1.52 -
1.53 -(* intermediate term structure *)
1.54 -
1.55 -datatype squant = SForall | SExists
1.56 -
1.57 -datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
1.58 -
1.59 -datatype sterm =
1.60 - SVar of int |
1.61 - SApp of string * sterm list |
1.62 - SLet of string * sterm * sterm |
1.63 - SQua of squant * string list * sterm spattern list * sterm
1.64 -
1.65 -
1.66 -
1.67 -(* configuration options *)
1.68 -
1.69 -type prefixes = {sort_prefix: string, func_prefix: string}
1.70 -
1.71 -type strict = {
1.72 - is_builtin_conn: string * typ -> bool,
1.73 - is_builtin_pred: string * typ -> bool,
1.74 - is_builtin_distinct: bool}
1.75 -
1.76 -type builtins = {
1.77 - builtin_typ: typ -> string option,
1.78 - builtin_num: typ -> int -> string option,
1.79 - builtin_fun: string * typ -> term list -> (string * term list) option }
1.80 -
1.81 -datatype smt_theory = Integer | Real | Bitvector
1.82 -
1.83 -type sign = {
1.84 - theories: smt_theory list,
1.85 - sorts: string list,
1.86 - funcs: (string * (string list * string)) list }
1.87 -
1.88 -type config = {
1.89 - prefixes: prefixes,
1.90 - strict: strict option,
1.91 - builtins: builtins,
1.92 - serialize: sign -> sterm list -> string }
1.93 -
1.94 -type recon = {
1.95 - typs: typ Symtab.table,
1.96 - terms: term Symtab.table,
1.97 - unfolds: thm list,
1.98 - assms: thm list option }
1.99 -
1.100 -
1.101 -
1.102 -(* utility functions *)
1.103 -
1.104 -val dest_funT =
1.105 - let
1.106 - fun dest Ts 0 T = (rev Ts, T)
1.107 - | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
1.108 - | dest _ _ T = raise TYPE ("dest_funT", [T], [])
1.109 - in dest [] end
1.110 -
1.111 -val quantifier = (fn
1.112 - @{const_name All} => SOME SForall
1.113 - | @{const_name Ex} => SOME SExists
1.114 - | _ => NONE)
1.115 -
1.116 -fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) =
1.117 - if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
1.118 - | group_quant _ Ts t = (Ts, t)
1.119 -
1.120 -fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts))
1.121 - | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts))
1.122 - | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p
1.123 - | dest_pat _ t = raise TERM ("dest_pat", [t])
1.124 -
1.125 -fun dest_trigger (@{term trigger} $ tl $ t) =
1.126 - (map (dest_pat []) (HOLogic.dest_list tl), t)
1.127 - | dest_trigger t = ([], t)
1.128 -
1.129 -fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
1.130 - let
1.131 - val (Ts, u) = group_quant qn [T] t
1.132 - val (ps, b) = dest_trigger u
1.133 - in (q, rev Ts, ps, b) end)
1.134 -
1.135 -fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
1.136 - | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
1.137 -
1.138 -fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm)
1.139 -
1.140 -
1.141 -
1.142 -(* enforce a strict separation between formulas and terms *)
1.143 -
1.144 -val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)}
1.145 -
1.146 -val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)}
1.147 -val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
1.148 -
1.149 -
1.150 -val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
1.151 - Const (@{const_name Let}, _) => true
1.152 - | @{term "op = :: bool => _"} $ _ $ @{term True} => true
1.153 - | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
1.154 - | _ => false)
1.155 -
1.156 -val rewrite_rules = [
1.157 - Let_def,
1.158 - @{lemma "P = True == P" by (rule eq_reflection) simp},
1.159 - @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
1.160 -
1.161 -fun rewrite ctxt = Simplifier.full_rewrite
1.162 - (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
1.163 -
1.164 -fun normalize ctxt thm =
1.165 - if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
1.166 -
1.167 -val unfold_rules = term_eq_rewr :: rewrite_rules
1.168 -
1.169 -
1.170 -val revert_types =
1.171 - let
1.172 - fun revert @{typ prop} = @{typ bool}
1.173 - | revert (Type (n, Ts)) = Type (n, map revert Ts)
1.174 - | revert T = T
1.175 - in Term.map_types revert end
1.176 -
1.177 -
1.178 -fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
1.179 - let
1.180 -
1.181 - fun is_builtin_conn' (@{const_name True}, _) = false
1.182 - | is_builtin_conn' (@{const_name False}, _) = false
1.183 - | is_builtin_conn' c = is_builtin_conn c
1.184 -
1.185 - val propT = @{typ prop} and boolT = @{typ bool}
1.186 - val as_propT = (fn @{typ bool} => propT | T => T)
1.187 - fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
1.188 - fun conn (n, T) = (n, mapTs as_propT as_propT T)
1.189 - fun pred (n, T) = (n, mapTs I as_propT T)
1.190 -
1.191 - val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
1.192 - fun as_term t = Const term_eq $ t $ @{term True}
1.193 -
1.194 - val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
1.195 - fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
1.196 -
1.197 - fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
1.198 -
1.199 - fun in_term t =
1.200 - (case Term.strip_comb t of
1.201 - (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
1.202 - c $ in_form t1 $ in_term t2 $ in_term t3
1.203 - | (h as Const c, ts) =>
1.204 - if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c)
1.205 - then wrap_in_if (in_form t)
1.206 - else Term.list_comb (h, map in_term ts)
1.207 - | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
1.208 - | _ => t)
1.209 -
1.210 - and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
1.211 - | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
1.212 - | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) =
1.213 - c $ in_pat p $ in_term t
1.214 - | in_pat t = raise TERM ("in_pat", [t])
1.215 -
1.216 - and in_pats p = in_list @{typ pattern} in_pat p
1.217 -
1.218 - and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
1.219 - | in_trig t = in_form t
1.220 -
1.221 - and in_form t =
1.222 - (case Term.strip_comb t of
1.223 - (q as Const (qn, _), [Abs (n, T, t')]) =>
1.224 - if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
1.225 - else as_term (in_term t)
1.226 - | (Const (c as (@{const_name distinct}, T)), [t']) =>
1.227 - if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
1.228 - else as_term (in_term t)
1.229 - | (Const c, ts) =>
1.230 - if is_builtin_conn (conn c)
1.231 - then Term.list_comb (Const (conn c), map in_form ts)
1.232 - else if is_builtin_pred (pred c)
1.233 - then Term.list_comb (Const (pred c), map in_term ts)
1.234 - else as_term (in_term t)
1.235 - | _ => as_term (in_term t))
1.236 - in
1.237 - map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms),
1.238 - map (in_form o prop_of) (term_bool :: thms)))
1.239 - end
1.240 -
1.241 -
1.242 -
1.243 -(* translation from Isabelle terms into SMT intermediate terms *)
1.244 -
1.245 -val empty_context = (1, Typtab.empty, 1, Termtab.empty, [])
1.246 -
1.247 -fun make_sign (_, typs, _, terms, thys) = {
1.248 - theories = thys,
1.249 - sorts = Typtab.fold (cons o snd) typs [],
1.250 - funcs = Termtab.fold (cons o snd) terms [] }
1.251 -
1.252 -fun make_recon (unfolds, assms) (_, typs, _, terms, _) = {
1.253 - typs = Symtab.make (map swap (Typtab.dest typs)),
1.254 - terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
1.255 - unfolds = unfolds,
1.256 - assms = SOME assms }
1.257 -
1.258 -fun string_of_index pre i = pre ^ string_of_int i
1.259 -
1.260 -fun add_theory T (Tidx, typs, idx, terms, thys) =
1.261 - let
1.262 - fun add @{typ int} = insert (op =) Integer
1.263 - | add @{typ real} = insert (op =) Real
1.264 - | add (Type (@{type_name word}, _)) = insert (op =) Bitvector
1.265 - | add (Type (_, Ts)) = fold add Ts
1.266 - | add _ = I
1.267 - in (Tidx, typs, idx, terms, add T thys) end
1.268 -
1.269 -fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) =
1.270 - (case Typtab.lookup typs T of
1.271 - SOME s => (s, cx)
1.272 - | NONE =>
1.273 - let
1.274 - val s = string_of_index sort_prefix Tidx
1.275 - val typs' = Typtab.update (T, s) typs
1.276 - in (s, (Tidx+1, typs', idx, terms, thys)) end)
1.277 -
1.278 -fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) =
1.279 - (case Termtab.lookup terms t of
1.280 - SOME (f, _) => (f, cx)
1.281 - | NONE =>
1.282 - let
1.283 - val f = string_of_index func_prefix idx
1.284 - val terms' = Termtab.update (revert_types t, (f, ss)) terms
1.285 - in (f, (Tidx, typs, idx+1, terms', thys)) end)
1.286 -
1.287 -fun relaxed thms = (([], thms), map prop_of thms)
1.288 -
1.289 -fun with_context f (ths, ts) =
1.290 - let val (us, context) = fold_map f ts empty_context
1.291 - in ((make_sign context, us), make_recon ths context) end
1.292 -
1.293 -
1.294 -fun translate {prefixes, strict, builtins, serialize} ctxt =
1.295 - let
1.296 - val {sort_prefix, func_prefix} = prefixes
1.297 - val {builtin_typ, builtin_num, builtin_fun} = builtins
1.298 -
1.299 - fun transT T = add_theory T #>
1.300 - (case builtin_typ T of
1.301 - SOME n => pair n
1.302 - | NONE => fresh_typ sort_prefix T)
1.303 -
1.304 - fun app n ts = SApp (n, ts)
1.305 -
1.306 - fun trans t =
1.307 - (case Term.strip_comb t of
1.308 - (Const (qn, _), [Abs (_, T, t1)]) =>
1.309 - (case dest_quant qn T t1 of
1.310 - SOME (q, Ts, ps, b) =>
1.311 - fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
1.312 - trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
1.313 - | NONE => raise TERM ("intermediate", [t]))
1.314 - | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
1.315 - transT T ##>> trans t1 ##>> trans t2 #>>
1.316 - (fn ((U, u1), u2) => SLet (U, u1, u2))
1.317 - | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
1.318 - (case builtin_fun c (HOLogic.dest_list t1) of
1.319 - SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n
1.320 - | NONE => transs h T [t1])
1.321 - | (h as Const (c as (_, T)), ts) =>
1.322 - (case try HOLogic.dest_number t of
1.323 - SOME (T, i) =>
1.324 - (case builtin_num T i of
1.325 - SOME n => add_theory T #> pair (SApp (n, []))
1.326 - | NONE => transs t T [])
1.327 - | NONE =>
1.328 - (case builtin_fun c ts of
1.329 - SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n
1.330 - | NONE => transs h T ts))
1.331 - | (h as Free (_, T), ts) => transs h T ts
1.332 - | (Bound i, []) => pair (SVar i)
1.333 - | _ => raise TERM ("intermediate", [t]))
1.334 -
1.335 - and transs t T ts =
1.336 - let val (Us, U) = dest_funT (length ts) T
1.337 - in
1.338 - fold_map transT Us ##>> transT U #-> (fn Up =>
1.339 - fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
1.340 - end
1.341 - in
1.342 - (if is_some strict then strictify (the strict) ctxt else relaxed) #>
1.343 - with_context trans #>> uncurry serialize
1.344 - end
1.345 -
1.346 -end