boehmes@36898: (* Title: HOL/Tools/SMT/smt_translate.ML boehmes@36898: Author: Sascha Boehme, TU Muenchen boehmes@36898: boehmes@36898: Translate theorems into an SMT intermediate format and serialize them. boehmes@36898: *) boehmes@36898: boehmes@36898: signature SMT_TRANSLATE = boehmes@36898: sig boehmes@36898: (* intermediate term structure *) boehmes@36898: datatype squant = SForall | SExists boehmes@36898: datatype 'a spattern = SPat of 'a list | SNoPat of 'a list boehmes@36898: datatype sterm = boehmes@36898: SVar of int | boehmes@36898: SApp of string * sterm list | boehmes@36898: SLet of string * sterm * sterm | boehmes@36898: SQua of squant * string list * sterm spattern list * sterm boehmes@36898: boehmes@36898: (* configuration options *) boehmes@36898: type prefixes = {sort_prefix: string, func_prefix: string} boehmes@36898: type strict = { boehmes@36898: is_builtin_conn: string * typ -> bool, boehmes@36898: is_builtin_pred: string * typ -> bool, boehmes@36898: is_builtin_distinct: bool} boehmes@36898: type builtins = { boehmes@36898: builtin_typ: typ -> string option, boehmes@36898: builtin_num: typ -> int -> string option, boehmes@36898: builtin_fun: string * typ -> term list -> (string * term list) option } boehmes@36898: datatype smt_theory = Integer | Real | Bitvector boehmes@36898: type sign = { boehmes@36898: theories: smt_theory list, boehmes@36898: sorts: string list, boehmes@36898: funcs: (string * (string list * string)) list } boehmes@36898: type config = { boehmes@36898: prefixes: prefixes, boehmes@36898: strict: strict option, boehmes@36898: builtins: builtins, boehmes@36898: serialize: string list -> sign -> sterm list -> string } boehmes@36898: type recon = { boehmes@36898: typs: typ Symtab.table, boehmes@36898: terms: term Symtab.table, boehmes@36898: unfolds: thm list, boehmes@36898: assms: thm list option } boehmes@36898: boehmes@36898: val translate: config -> Proof.context -> string list -> thm list -> boehmes@36898: string * recon boehmes@36898: end boehmes@36898: boehmes@36898: structure SMT_Translate: SMT_TRANSLATE = boehmes@36898: struct boehmes@36898: boehmes@36898: (* intermediate term structure *) boehmes@36898: boehmes@36898: datatype squant = SForall | SExists boehmes@36898: boehmes@36898: datatype 'a spattern = SPat of 'a list | SNoPat of 'a list boehmes@36898: boehmes@36898: datatype sterm = boehmes@36898: SVar of int | boehmes@36898: SApp of string * sterm list | boehmes@36898: SLet of string * sterm * sterm | boehmes@36898: SQua of squant * string list * sterm spattern list * sterm boehmes@36898: boehmes@36898: boehmes@36898: boehmes@36898: (* configuration options *) boehmes@36898: boehmes@36898: type prefixes = {sort_prefix: string, func_prefix: string} boehmes@36898: boehmes@36898: type strict = { boehmes@36898: is_builtin_conn: string * typ -> bool, boehmes@36898: is_builtin_pred: string * typ -> bool, boehmes@36898: is_builtin_distinct: bool} boehmes@36898: boehmes@36898: type builtins = { boehmes@36898: builtin_typ: typ -> string option, boehmes@36898: builtin_num: typ -> int -> string option, boehmes@36898: builtin_fun: string * typ -> term list -> (string * term list) option } boehmes@36898: boehmes@36898: datatype smt_theory = Integer | Real | Bitvector boehmes@36898: boehmes@36898: type sign = { boehmes@36898: theories: smt_theory list, boehmes@36898: sorts: string list, boehmes@36898: funcs: (string * (string list * string)) list } boehmes@36898: boehmes@36898: type config = { boehmes@36898: prefixes: prefixes, boehmes@36898: strict: strict option, boehmes@36898: builtins: builtins, boehmes@36898: serialize: string list -> sign -> sterm list -> string } boehmes@36898: boehmes@36898: type recon = { boehmes@36898: typs: typ Symtab.table, boehmes@36898: terms: term Symtab.table, boehmes@36898: unfolds: thm list, boehmes@36898: assms: thm list option } boehmes@36898: boehmes@36898: boehmes@36898: boehmes@36898: (* utility functions *) boehmes@36898: boehmes@36898: val dest_funT = boehmes@36898: let boehmes@36898: fun dest Ts 0 T = (rev Ts, T) boehmes@36898: | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U boehmes@36898: | dest _ _ T = raise TYPE ("dest_funT", [T], []) boehmes@36898: in dest [] end boehmes@36898: boehmes@36898: val quantifier = (fn boehmes@36898: @{const_name All} => SOME SForall boehmes@36898: | @{const_name Ex} => SOME SExists boehmes@36898: | _ => NONE) boehmes@36898: boehmes@36898: fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = boehmes@36898: if q = qname then group_quant qname (T :: Ts) u else (Ts, t) boehmes@36898: | group_quant _ Ts t = (Ts, t) boehmes@36898: boehmes@36898: fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts)) boehmes@36898: | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts)) boehmes@36898: | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p boehmes@36898: | dest_pat _ t = raise TERM ("dest_pat", [t]) boehmes@36898: boehmes@36898: fun dest_trigger (@{term trigger} $ tl $ t) = boehmes@36898: (map (dest_pat []) (HOLogic.dest_list tl), t) boehmes@36898: | dest_trigger t = ([], t) boehmes@36898: boehmes@36898: fun dest_quant qn T t = quantifier qn |> Option.map (fn q => boehmes@36898: let boehmes@36898: val (Ts, u) = group_quant qn [T] t boehmes@36898: val (ps, b) = dest_trigger u boehmes@36898: in (q, rev Ts, ps, b) end) boehmes@36898: boehmes@36898: fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat boehmes@36898: | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat boehmes@36898: boehmes@36898: fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm) boehmes@36898: boehmes@36898: boehmes@36898: boehmes@36898: (* enforce a strict separation between formulas and terms *) boehmes@36898: boehmes@36898: val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)} boehmes@36898: boehmes@36898: val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)} boehmes@36898: val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool boehmes@36898: boehmes@36898: boehmes@36898: val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn boehmes@36898: Const (@{const_name Let}, _) => true boehmes@36898: | @{term "op = :: bool => _"} $ _ $ @{term True} => true boehmes@36898: | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true boehmes@36898: | _ => false) boehmes@36898: boehmes@36898: val rewrite_rules = [ boehmes@36898: Let_def, boehmes@36898: @{lemma "P = True == P" by (rule eq_reflection) simp}, boehmes@36898: @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] boehmes@36898: boehmes@36898: fun rewrite ctxt = Simplifier.full_rewrite boehmes@36898: (Simplifier.context ctxt empty_ss addsimps rewrite_rules) boehmes@36898: boehmes@36898: fun normalize ctxt thm = boehmes@36898: if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm boehmes@36898: boehmes@36898: val unfold_rules = term_eq_rewr :: rewrite_rules boehmes@36898: boehmes@36898: boehmes@36898: val revert_types = boehmes@36898: let boehmes@36898: fun revert @{typ prop} = @{typ bool} boehmes@36898: | revert (Type (n, Ts)) = Type (n, map revert Ts) boehmes@36898: | revert T = T boehmes@36898: in Term.map_types revert end boehmes@36898: boehmes@36898: boehmes@36898: fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt = boehmes@36898: let boehmes@36898: boehmes@36898: fun is_builtin_conn' (@{const_name True}, _) = false boehmes@36898: | is_builtin_conn' (@{const_name False}, _) = false boehmes@36898: | is_builtin_conn' c = is_builtin_conn c boehmes@36898: boehmes@36898: val propT = @{typ prop} and boolT = @{typ bool} boehmes@36898: val as_propT = (fn @{typ bool} => propT | T => T) boehmes@36898: fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T) boehmes@36898: fun conn (n, T) = (n, mapTs as_propT as_propT T) boehmes@36898: fun pred (n, T) = (n, mapTs I as_propT T) boehmes@36898: boehmes@36898: val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred boehmes@36898: fun as_term t = Const term_eq $ t $ @{term True} boehmes@36898: boehmes@36898: val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT) boehmes@36898: fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False} boehmes@36898: boehmes@36898: fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) boehmes@36898: boehmes@36898: fun in_term t = boehmes@36898: (case Term.strip_comb t of boehmes@36898: (c as Const (@{const_name If}, _), [t1, t2, t3]) => boehmes@36898: c $ in_form t1 $ in_term t2 $ in_term t3 boehmes@36898: | (h as Const c, ts) => boehmes@36898: if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c) boehmes@36898: then wrap_in_if (in_form t) boehmes@36898: else Term.list_comb (h, map in_term ts) boehmes@36898: | (h as Free _, ts) => Term.list_comb (h, map in_term ts) boehmes@36898: | _ => t) boehmes@36898: boehmes@36898: and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t boehmes@36898: | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t boehmes@36898: | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) = boehmes@36898: c $ in_pat p $ in_term t boehmes@36898: | in_pat t = raise TERM ("in_pat", [t]) boehmes@36898: boehmes@36898: and in_pats p = in_list @{typ pattern} in_pat p boehmes@36898: boehmes@36898: and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t boehmes@36898: | in_trig t = in_form t boehmes@36898: boehmes@36898: and in_form t = boehmes@36898: (case Term.strip_comb t of boehmes@36898: (q as Const (qn, _), [Abs (n, T, t')]) => boehmes@36898: if is_some (quantifier qn) then q $ Abs (n, T, in_trig t') boehmes@36898: else as_term (in_term t) boehmes@36898: | (Const (c as (@{const_name distinct}, T)), [t']) => boehmes@36898: if is_builtin_distinct then Const (pred c) $ in_list T in_term t' boehmes@36898: else as_term (in_term t) boehmes@36898: | (Const c, ts) => boehmes@36898: if is_builtin_conn (conn c) boehmes@36898: then Term.list_comb (Const (conn c), map in_form ts) boehmes@36898: else if is_builtin_pred (pred c) boehmes@36898: then Term.list_comb (Const (pred c), map in_term ts) boehmes@36898: else as_term (in_term t) boehmes@36898: | _ => as_term (in_term t)) boehmes@36898: in boehmes@36898: map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms), boehmes@36898: map (in_form o prop_of) (term_bool :: thms))) boehmes@36898: end boehmes@36898: boehmes@36898: boehmes@36898: boehmes@36898: (* translation from Isabelle terms into SMT intermediate terms *) boehmes@36898: boehmes@36898: val empty_context = (1, Typtab.empty, 1, Termtab.empty, []) boehmes@36898: boehmes@36898: fun make_sign (_, typs, _, terms, thys) = { boehmes@36898: theories = thys, boehmes@36898: sorts = Typtab.fold (cons o snd) typs [], boehmes@36898: funcs = Termtab.fold (cons o snd) terms [] } boehmes@36898: boehmes@36898: fun make_recon (unfolds, assms) (_, typs, _, terms, _) = { boehmes@36898: typs = Symtab.make (map swap (Typtab.dest typs)), boehmes@36898: terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)), boehmes@36898: unfolds = unfolds, boehmes@36898: assms = SOME assms } boehmes@36898: boehmes@36898: fun string_of_index pre i = pre ^ string_of_int i boehmes@36898: boehmes@36898: fun add_theory T (Tidx, typs, idx, terms, thys) = boehmes@36898: let boehmes@36898: fun add @{typ int} = insert (op =) Integer boehmes@36898: | add @{typ real} = insert (op =) Real boehmes@36898: | add (Type (@{type_name word}, _)) = insert (op =) Bitvector boehmes@36898: | add (Type (_, Ts)) = fold add Ts boehmes@36898: | add _ = I boehmes@36898: in (Tidx, typs, idx, terms, add T thys) end boehmes@36898: boehmes@36898: fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) = boehmes@36898: (case Typtab.lookup typs T of boehmes@36898: SOME s => (s, cx) boehmes@36898: | NONE => boehmes@36898: let boehmes@36898: val s = string_of_index sort_prefix Tidx boehmes@36898: val typs' = Typtab.update (T, s) typs boehmes@36898: in (s, (Tidx+1, typs', idx, terms, thys)) end) boehmes@36898: boehmes@36898: fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) = boehmes@36898: (case Termtab.lookup terms t of boehmes@36898: SOME (f, _) => (f, cx) boehmes@36898: | NONE => boehmes@36898: let boehmes@36898: val f = string_of_index func_prefix idx boehmes@36898: val terms' = Termtab.update (revert_types t, (f, ss)) terms boehmes@36898: in (f, (Tidx, typs, idx+1, terms', thys)) end) boehmes@36898: boehmes@36898: fun relaxed thms = (([], thms), map prop_of thms) boehmes@36898: boehmes@36898: fun with_context f (ths, ts) = boehmes@36898: let val (us, context) = fold_map f ts empty_context boehmes@36898: in ((make_sign context, us), make_recon ths context) end boehmes@36898: boehmes@36898: boehmes@36898: fun translate {prefixes, strict, builtins, serialize} ctxt comments = boehmes@36898: let boehmes@36898: val {sort_prefix, func_prefix} = prefixes boehmes@36898: val {builtin_typ, builtin_num, builtin_fun} = builtins boehmes@36898: boehmes@36898: fun transT T = add_theory T #> boehmes@36898: (case builtin_typ T of boehmes@36898: SOME n => pair n boehmes@36898: | NONE => fresh_typ sort_prefix T) boehmes@36898: boehmes@36898: fun app n ts = SApp (n, ts) boehmes@36898: boehmes@36898: fun trans t = boehmes@36898: (case Term.strip_comb t of boehmes@36898: (Const (qn, _), [Abs (_, T, t1)]) => boehmes@36898: (case dest_quant qn T t1 of boehmes@36898: SOME (q, Ts, ps, b) => boehmes@36898: fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> boehmes@36898: trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) boehmes@36898: | NONE => raise TERM ("intermediate", [t])) boehmes@36898: | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => boehmes@36898: transT T ##>> trans t1 ##>> trans t2 #>> boehmes@36898: (fn ((U, u1), u2) => SLet (U, u1, u2)) boehmes@36898: | (h as Const (c as (@{const_name distinct}, T)), [t1]) => boehmes@36898: (case builtin_fun c (HOLogic.dest_list t1) of boehmes@36898: SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n boehmes@36898: | NONE => transs h T [t1]) boehmes@36898: | (h as Const (c as (_, T)), ts) => boehmes@36898: (case try HOLogic.dest_number t of boehmes@36898: SOME (T, i) => boehmes@36898: (case builtin_num T i of boehmes@36898: SOME n => add_theory T #> pair (SApp (n, [])) boehmes@36898: | NONE => transs t T []) boehmes@36898: | NONE => boehmes@36898: (case builtin_fun c ts of boehmes@36898: SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n boehmes@36898: | NONE => transs h T ts)) boehmes@36898: | (h as Free (_, T), ts) => transs h T ts boehmes@36898: | (Bound i, []) => pair (SVar i) boehmes@36898: | _ => raise TERM ("intermediate", [t])) boehmes@36898: boehmes@36898: and transs t T ts = boehmes@36898: let val (Us, U) = dest_funT (length ts) T boehmes@36898: in boehmes@36898: fold_map transT Us ##>> transT U #-> (fn Up => boehmes@36898: fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp) boehmes@36898: end boehmes@36898: in boehmes@36898: (if is_some strict then strictify (the strict) ctxt else relaxed) #> boehmes@36898: with_context trans #>> uncurry (serialize comments) boehmes@36898: end boehmes@36898: boehmes@36898: end