src/HOL/Tools/SMT/smt_translate.ML
changeset 39298 5aefb5bc8a93
parent 37124 fe22fc54b876
child 39435 5d18f4c00c07
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 10 23:56:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Sep 13 06:02:47 2010 +0200
     1.3 @@ -26,10 +26,12 @@
     1.4      builtin_typ: Proof.context -> typ -> string option,
     1.5      builtin_num: Proof.context -> typ -> int -> string option,
     1.6      builtin_fun: Proof.context -> string * typ -> term list ->
     1.7 -      (string * term list) option }
     1.8 +      (string * term list) option,
     1.9 +    has_datatypes: bool }
    1.10    type sign = {
    1.11      header: string list,
    1.12      sorts: string list,
    1.13 +    dtyps: (string * (string * (string * string) list) list) list list,
    1.14      funcs: (string * (string list * string)) list }
    1.15    type config = {
    1.16      prefixes: prefixes,
    1.17 @@ -79,11 +81,13 @@
    1.18    builtin_typ: Proof.context -> typ -> string option,
    1.19    builtin_num: Proof.context -> typ -> int -> string option,
    1.20    builtin_fun: Proof.context -> string * typ -> term list ->
    1.21 -    (string * term list) option }
    1.22 +    (string * term list) option,
    1.23 +  has_datatypes: bool }
    1.24  
    1.25  type sign = {
    1.26    header: string list,
    1.27    sorts: string list,
    1.28 +  dtyps: (string * (string * (string * string) list) list) list list,
    1.29    funcs: (string * (string list * string)) list }
    1.30  
    1.31  type config = {
    1.32 @@ -248,38 +252,67 @@
    1.33  
    1.34  (* translation from Isabelle terms into SMT intermediate terms *)
    1.35  
    1.36 -val empty_context = (1, Typtab.empty, 1, Termtab.empty)
    1.37 +val empty_context = (1, Typtab.empty, [], 1, Termtab.empty)
    1.38  
    1.39 -fun make_sign header (_, typs, _, terms) = {
    1.40 +fun make_sign header (_, typs, dtyps, _, terms) = {
    1.41    header = header,
    1.42 -  sorts = Typtab.fold (cons o snd) typs [],
    1.43 -  funcs = Termtab.fold (cons o snd) terms [] }
    1.44 +  sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
    1.45 +  funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [],
    1.46 +  dtyps = dtyps }
    1.47  
    1.48 -fun make_recon (unfolds, assms) (_, typs, _, terms) = {
    1.49 -  typs = Symtab.make (map swap (Typtab.dest typs)),
    1.50 +fun make_recon (unfolds, assms) (_, typs, _, _, terms) = {
    1.51 +  typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)),
    1.52 +    (*FIXME: don't drop the datatype information! *)
    1.53    terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
    1.54    unfolds = unfolds,
    1.55    assms = assms }
    1.56  
    1.57  fun string_of_index pre i = pre ^ string_of_int i
    1.58  
    1.59 -fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms)) =
    1.60 -  (case Typtab.lookup typs T of
    1.61 -    SOME s => (s, cx)
    1.62 -  | NONE =>
    1.63 -      let
    1.64 -        val s = string_of_index sort_prefix Tidx
    1.65 -        val typs' = Typtab.update (T, s) typs
    1.66 -      in (s, (Tidx+1, typs', idx, terms)) end)
    1.67 +fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
    1.68 +  let val s = string_of_index sort_prefix Tidx
    1.69 +  in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
    1.70 +
    1.71 +fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
    1.72  
    1.73 -fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms)) =
    1.74 +fun fresh_typ T f cx =
    1.75 +  (case lookup_typ cx T of
    1.76 +    SOME (s, _) => (s, cx)
    1.77 +  | NONE => f T cx)
    1.78 +
    1.79 +fun new_fun func_prefix t ss (Tidx, typs, dtyps, idx, terms) =
    1.80 +  let
    1.81 +    val f = string_of_index func_prefix idx
    1.82 +    val terms' = Termtab.update (revert_types t, (f, ss)) terms
    1.83 +  in (f, (Tidx, typs, dtyps, idx+1, terms')) end
    1.84 +
    1.85 +fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
    1.86    (case Termtab.lookup terms t of
    1.87      SOME (f, _) => (f, cx)
    1.88 -  | NONE =>
    1.89 -      let
    1.90 -        val f = string_of_index func_prefix idx
    1.91 -        val terms' = Termtab.update (revert_types t, (f, ss)) terms
    1.92 -      in (f, (Tidx, typs, idx+1, terms')) end)
    1.93 +  | NONE => new_fun func_prefix t ss cx)
    1.94 +
    1.95 +fun inst_const f Ts t =
    1.96 +  let
    1.97 +    val (n, T) = Term.dest_Const (snd (Type.varify_global [] t))
    1.98 +    val inst = map Term.dest_TVar (snd (Term.dest_Type (f T))) ~~ Ts
    1.99 +  in Const (n, Term_Subst.instantiateT inst T) end
   1.100 +
   1.101 +fun inst_constructor Ts = inst_const Term.body_type Ts
   1.102 +fun inst_selector Ts = inst_const Term.domain_type Ts
   1.103 +
   1.104 +fun lookup_datatype ctxt n Ts = (* FIXME: use Datatype/Record.get_info *)
   1.105 +  if n = @{type_name prod}
   1.106 +  then SOME [
   1.107 +    (Type (n, Ts), [
   1.108 +      (inst_constructor Ts @{term Pair},
   1.109 +        map (inst_selector Ts) [@{term fst}, @{term snd}])])]
   1.110 +  else if n = @{type_name list}
   1.111 +  then SOME [
   1.112 +    (Type (n, Ts), [
   1.113 +      (inst_constructor Ts @{term Nil}, []),
   1.114 +      (inst_constructor Ts @{term Cons},
   1.115 +        map (inst_selector Ts) [@{term hd}, @{term tl}])])]
   1.116 +  else NONE
   1.117  
   1.118  fun relaxed thms = (([], thms), map prop_of thms)
   1.119  
   1.120 @@ -291,12 +324,40 @@
   1.121  fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
   1.122    let
   1.123      val {sort_prefix, func_prefix} = prefixes
   1.124 -    val {builtin_typ, builtin_num, builtin_fun} = builtins
   1.125 +    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
   1.126 +
   1.127 +    fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
   1.128 +      | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
   1.129 +      | transT (T as Type (n, Ts)) =
   1.130 +          (case builtin_typ ctxt T of
   1.131 +            SOME n => pair n
   1.132 +          | NONE => fresh_typ T (fn _ => fn cx =>
   1.133 +              if not has_datatypes then new_typ sort_prefix true T cx
   1.134 +              else
   1.135 +                (case lookup_datatype ctxt n Ts of
   1.136 +                  NONE => new_typ sort_prefix true T cx
   1.137 +                | SOME dts =>
   1.138 +                    let val cx' = new_dtyps dts cx 
   1.139 +                    in (fst (the (lookup_typ cx' T)), cx') end)))
   1.140  
   1.141 -    fun transT T =
   1.142 -      (case builtin_typ ctxt T of
   1.143 -        SOME n => pair n
   1.144 -      | NONE => fresh_typ sort_prefix T)
   1.145 +    and new_dtyps dts cx =
   1.146 +      let
   1.147 +        fun new_decl i t =
   1.148 +          let val (Ts, T) = dest_funT i (Term.fastype_of t)
   1.149 +          in
   1.150 +            fold_map transT Ts ##>> transT T ##>>
   1.151 +            new_fun func_prefix t NONE #>> swap
   1.152 +          end
   1.153 +        fun new_dtyp_decl (con, sels) =
   1.154 +          new_decl (length sels) con ##>> fold_map (new_decl 1) sels #>>
   1.155 +          (fn ((con', _), sels') => (con', map (apsnd snd) sels'))
   1.156 +      in
   1.157 +        cx
   1.158 +        |> fold_map (new_typ sort_prefix false o fst) dts
   1.159 +        ||>> fold_map (fold_map new_dtyp_decl o snd) dts
   1.160 +        |-> (fn (ss, decls) => fn (Tidx, typs, dtyps, idx, terms) =>
   1.161 +              (Tidx, typs, (ss ~~ decls) :: dtyps, idx, terms))
   1.162 +      end
   1.163  
   1.164      fun app n ts = SApp (n, ts)
   1.165  
   1.166 @@ -327,13 +388,13 @@
   1.167                | NONE => transs h T ts))
   1.168        | (h as Free (_, T), ts) => transs h T ts
   1.169        | (Bound i, []) => pair (SVar i)
   1.170 -      | _ => raise TERM ("intermediate", [t]))
   1.171 +      | _ => raise TERM ("smt_translate", [t]))
   1.172  
   1.173      and transs t T ts =
   1.174        let val (Us, U) = dest_funT (length ts) T
   1.175        in
   1.176          fold_map transT Us ##>> transT U #-> (fn Up =>
   1.177 -        fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
   1.178 +        fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
   1.179        end
   1.180    in
   1.181      (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>