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