src/HOL/Tools/SMT/smt_translate.ML
changeset 41059 d2b1fc1b8e19
parent 41057 8dbc951a291c
child 41123 3bb9be510a9d
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 06 16:54:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Dec 07 14:53:12 2010 +0100
     1.3 @@ -17,17 +17,6 @@
     1.4  
     1.5    (* configuration options *)
     1.6    type prefixes = {sort_prefix: string, func_prefix: string}
     1.7 -  type header = Proof.context -> term list -> string list
     1.8 -  type strict = {
     1.9 -    is_builtin_conn: string * typ -> bool,
    1.10 -    is_builtin_pred: Proof.context -> string * typ -> bool,
    1.11 -    is_builtin_distinct: bool}
    1.12 -  type builtins = {
    1.13 -    builtin_typ: Proof.context -> typ -> string option,
    1.14 -    builtin_num: Proof.context -> typ -> int -> string option,
    1.15 -    builtin_fun: Proof.context -> string * typ -> term list ->
    1.16 -      (string * term list) option,
    1.17 -    has_datatypes: bool }
    1.18    type sign = {
    1.19      header: string list,
    1.20      sorts: string list,
    1.21 @@ -35,9 +24,9 @@
    1.22      funcs: (string * (string list * string)) list }
    1.23    type config = {
    1.24      prefixes: prefixes,
    1.25 -    header: header,
    1.26 -    strict: strict option,
    1.27 -    builtins: builtins,
    1.28 +    header: Proof.context -> term list -> string list,
    1.29 +    is_fol: bool,
    1.30 +    has_datatypes: bool,
    1.31      serialize: string list -> sign -> sterm list -> string }
    1.32    type recon = {
    1.33      typs: typ Symtab.table,
    1.34 @@ -53,6 +42,7 @@
    1.35  struct
    1.36  
    1.37  structure U = SMT_Utils
    1.38 +structure B = SMT_Builtin
    1.39  
    1.40  
    1.41  (* intermediate term structure *)
    1.42 @@ -73,20 +63,6 @@
    1.43  
    1.44  type prefixes = {sort_prefix: string, func_prefix: string}
    1.45  
    1.46 -type header = Proof.context -> term list -> string list
    1.47 -
    1.48 -type strict = {
    1.49 -  is_builtin_conn: string * typ -> bool,
    1.50 -  is_builtin_pred: Proof.context -> string * typ -> bool,
    1.51 -  is_builtin_distinct: bool}
    1.52 -
    1.53 -type builtins = {
    1.54 -  builtin_typ: Proof.context -> typ -> string option,
    1.55 -  builtin_num: Proof.context -> typ -> int -> string option,
    1.56 -  builtin_fun: Proof.context -> string * typ -> term list ->
    1.57 -    (string * term list) option,
    1.58 -  has_datatypes: bool }
    1.59 -
    1.60  type sign = {
    1.61    header: string list,
    1.62    sorts: string list,
    1.63 @@ -95,9 +71,9 @@
    1.64  
    1.65  type config = {
    1.66    prefixes: prefixes,
    1.67 -  header: header,
    1.68 -  strict: strict option,
    1.69 -  builtins: builtins,
    1.70 +  header: Proof.context -> term list -> string list,
    1.71 +  is_fol: bool,
    1.72 +  has_datatypes: bool,
    1.73    serialize: string list -> sign -> sterm list -> string }
    1.74  
    1.75  type recon = {
    1.76 @@ -152,13 +128,20 @@
    1.77  
    1.78  
    1.79  
    1.80 -(* enforce a strict separation between formulas and terms *)
    1.81 +(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *)
    1.82  
    1.83 -val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
    1.84 +val tboolT = @{typ SMT.term_bool}
    1.85 +val term_true = Const (@{const_name True}, tboolT)
    1.86 +val term_false = Const (@{const_name False}, tboolT)
    1.87  
    1.88 -val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
    1.89 -val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
    1.90 -
    1.91 +val term_bool = @{lemma "True ~= False" by simp}
    1.92 +val term_bool_prop =
    1.93 +  let
    1.94 +    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
    1.95 +      | replace @{const True} = term_true
    1.96 +      | replace @{const False} = term_false
    1.97 +      | replace t = t
    1.98 +  in Term.map_aterms replace (prop_of term_bool) end
    1.99  
   1.100  val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
   1.101      Const (@{const_name Let}, _) => true
   1.102 @@ -171,63 +154,57 @@
   1.103    @{lemma "P = True == P" by (rule eq_reflection) simp},
   1.104    @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
   1.105  
   1.106 -fun rewrite ctxt = Simplifier.full_rewrite
   1.107 -  (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
   1.108 +fun rewrite ctxt ct =
   1.109 +  Conv.top_sweep_conv (fn ctxt' =>
   1.110 +    Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct
   1.111  
   1.112  fun normalize ctxt thm =
   1.113    if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
   1.114  
   1.115 -val unfold_rules = term_eq_rewr :: rewrite_rules
   1.116 -
   1.117 +fun revert_typ @{typ SMT.term_bool} = @{typ bool}
   1.118 +  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
   1.119 +  | revert_typ T = T
   1.120  
   1.121 -val revert_types =
   1.122 -  let
   1.123 -    fun revert @{typ prop} = @{typ bool}
   1.124 -      | revert (Type (n, Ts)) = Type (n, map revert Ts)
   1.125 -      | revert T = T
   1.126 -  in Term.map_types revert end
   1.127 +val revert_types = Term.map_types revert_typ
   1.128  
   1.129 -
   1.130 -fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
   1.131 +fun folify ctxt =
   1.132    let
   1.133 -    fun is_builtin_conn' (@{const_name True}, _) = false
   1.134 -      | is_builtin_conn' (@{const_name False}, _) = false
   1.135 -      | is_builtin_conn' c = is_builtin_conn c
   1.136 +    fun is_builtin_conn (@{const_name True}, _) _ = false
   1.137 +      | is_builtin_conn (@{const_name False}, _) _ = false
   1.138 +      | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts
   1.139  
   1.140 -    fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
   1.141 -          is_builtin_distinct andalso can HOLogic.dest_list t
   1.142 -      | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
   1.143 +    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
   1.144  
   1.145 -    val propT = @{typ prop} and boolT = @{typ bool}
   1.146 -    val as_propT = (fn @{typ bool} => propT | T => T)
   1.147 +    fun as_tbool @{typ bool} = tboolT
   1.148 +      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
   1.149 +      | as_tbool T = T
   1.150      fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
   1.151 -    fun conn (n, T) = (n, mapTs as_propT as_propT T)
   1.152 -    fun pred (n, T) = (n, mapTs I as_propT T)
   1.153 +    fun predT T = mapTs as_tbool I T
   1.154 +    fun funcT T = mapTs as_tbool as_tbool T
   1.155 +    fun func (n, T) = Const (n, funcT T)
   1.156  
   1.157 -    val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
   1.158 -    fun as_term t = Const term_eq $ t $ @{const True}
   1.159 -
   1.160 -    val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
   1.161 -    fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
   1.162 +    fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->)
   1.163 +    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
   1.164 +    fun wrap_in_if t = if_term $ t $ term_true $ term_false
   1.165  
   1.166      fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
   1.167  
   1.168      fun in_term t =
   1.169        (case Term.strip_comb t of
   1.170 -        (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
   1.171 -          c $ in_form t1 $ in_term t2 $ in_term t3
   1.172 -      | (h as Const c, ts) =>
   1.173 -          if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
   1.174 +        (Const (c as @{const_name If}, T), [t1, t2, t3]) =>
   1.175 +          Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
   1.176 +      | (Const c, ts) =>
   1.177 +          if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts
   1.178            then wrap_in_if (in_form t)
   1.179 -          else Term.list_comb (h, map in_term ts)
   1.180 -      | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
   1.181 +          else Term.list_comb (func c, map in_term ts)
   1.182 +      | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts)
   1.183        | _ => t)
   1.184  
   1.185      and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
   1.186        | in_weight t = in_form t 
   1.187  
   1.188 -    and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
   1.189 -      | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
   1.190 +    and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t
   1.191 +      | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t
   1.192        | in_pat t = raise TERM ("in_pat", [t])
   1.193  
   1.194      and in_pats ps =
   1.195 @@ -239,23 +216,23 @@
   1.196      and in_form t =
   1.197        (case Term.strip_comb t of
   1.198          (q as Const (qn, _), [Abs (n, T, t')]) =>
   1.199 -          if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
   1.200 +          if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t')
   1.201            else as_term (in_term t)
   1.202 -      | (Const (c as (@{const_name distinct}, T)), [t']) =>
   1.203 -          if is_builtin_distinct andalso can HOLogic.dest_list t' then
   1.204 -            Const (pred c) $ in_list T in_term t'
   1.205 +      | (Const (c as (n as @{const_name distinct}, T)), [t']) =>
   1.206 +          if B.is_builtin_fun ctxt c [t'] then
   1.207 +            Const (n, predT T) $ in_list T in_term t'
   1.208            else as_term (in_term t)
   1.209 -      | (Const c, ts) =>
   1.210 -          if is_builtin_conn (conn c)
   1.211 -          then Term.list_comb (Const (conn c), map in_form ts)
   1.212 -          else if is_builtin_pred ctxt (pred c)
   1.213 -          then Term.list_comb (Const (pred c), map in_term ts)
   1.214 +      | (Const (c as (n, T)), ts) =>
   1.215 +          if B.is_builtin_conn ctxt c ts
   1.216 +          then Term.list_comb (Const c, map in_form ts)
   1.217 +          else if B.is_builtin_pred ctxt c ts
   1.218 +          then Term.list_comb (Const (n, predT T), map in_term ts)
   1.219            else as_term (in_term t)
   1.220        | _ => as_term (in_term t))
   1.221    in
   1.222      map (apsnd (normalize ctxt)) #> (fn irules =>
   1.223 -    ((unfold_rules, (~1, term_bool') :: irules),
   1.224 -     map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
   1.225 +    ((rewrite_rules, (~1, term_bool) :: irules),
   1.226 +     term_bool_prop :: map (in_form o prop_of o snd) irules))
   1.227    end
   1.228  
   1.229  
   1.230 @@ -280,10 +257,12 @@
   1.231  fun string_of_index pre i = pre ^ string_of_int i
   1.232  
   1.233  fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
   1.234 -  let val s = string_of_index sort_prefix Tidx
   1.235 -  in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
   1.236 +  let
   1.237 +    val s = string_of_index sort_prefix Tidx
   1.238 +    val U = revert_typ T
   1.239 +  in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end
   1.240  
   1.241 -fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
   1.242 +fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ
   1.243  
   1.244  fun fresh_typ T f cx =
   1.245    (case lookup_typ cx T of
   1.246 @@ -297,7 +276,7 @@
   1.247    in (f, (Tidx, typs, dtyps, idx+1, terms')) end
   1.248  
   1.249  fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
   1.250 -  (case Termtab.lookup terms t of
   1.251 +  (case Termtab.lookup terms (revert_types t) of
   1.252      SOME (f, _) => (f, cx)
   1.253    | NONE => new_fun func_prefix t ss cx)
   1.254  
   1.255 @@ -335,15 +314,15 @@
   1.256    in ((make_sign (header ts) context, us), make_recon ths context) end
   1.257  
   1.258  
   1.259 -fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
   1.260 +fun translate config ctxt comments =
   1.261    let
   1.262 +    val {prefixes, is_fol, header, has_datatypes, serialize} = config
   1.263      val {sort_prefix, func_prefix} = prefixes
   1.264 -    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
   1.265  
   1.266      fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
   1.267        | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
   1.268        | transT (T as Type (n, Ts)) =
   1.269 -          (case builtin_typ ctxt T of
   1.270 +          (case B.builtin_typ ctxt T of
   1.271              SOME n => pair n
   1.272            | NONE => fresh_typ T (fn _ => fn cx =>
   1.273                if not has_datatypes then new_typ sort_prefix true T cx
   1.274 @@ -387,17 +366,14 @@
   1.275            transT T ##>> trans t1 ##>> trans t2 #>>
   1.276            (fn ((U, u1), u2) => SLet (U, u1, u2))
   1.277        | (h as Const (c as (@{const_name distinct}, T)), ts) =>
   1.278 -          (case builtin_fun ctxt c ts of
   1.279 +          (case B.builtin_fun ctxt c ts of
   1.280              SOME (n, ts) => fold_map trans ts #>> app n
   1.281            | NONE => transs h T ts)
   1.282        | (h as Const (c as (_, T)), ts) =>
   1.283 -          (case try HOLogic.dest_number t of
   1.284 -            SOME (T, i) =>
   1.285 -              (case builtin_num ctxt T i of
   1.286 -                SOME n => pair (SApp (n, []))
   1.287 -              | NONE => transs t T [])
   1.288 +          (case B.builtin_num ctxt t of
   1.289 +            SOME n => pair (SApp (n, []))
   1.290            | NONE =>
   1.291 -              (case builtin_fun ctxt c ts of
   1.292 +              (case B.builtin_fun ctxt c ts of
   1.293                  SOME (n, ts') => fold_map trans ts' #>> app n
   1.294                | NONE => transs h T ts))
   1.295        | (h as Free (_, T), ts) => transs h T ts
   1.296 @@ -414,7 +390,7 @@
   1.297          fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
   1.298        end
   1.299    in
   1.300 -    (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
   1.301 +    (if is_fol then folify ctxt else relaxed) #>
   1.302      with_context (header ctxt) trans #>> uncurry (serialize comments)
   1.303    end
   1.304