src/HOL/Tools/SMT/smt_translate.ML
changeset 36899 bcd6fce5bf06
parent 36898 8e55aa1306c5
child 37124 fe22fc54b876
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed May 12 23:54:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed May 12 23:54:04 2010 +0200
     1.3 @@ -17,21 +17,23 @@
     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: string * typ -> bool,
    1.11 +    is_builtin_pred: Proof.context -> string * typ -> bool,
    1.12      is_builtin_distinct: bool}
    1.13    type builtins = {
    1.14 -    builtin_typ: typ -> string option,
    1.15 -    builtin_num: typ -> int -> string option,
    1.16 -    builtin_fun: string * typ -> term list -> (string * term list) option }
    1.17 -  datatype smt_theory = Integer | Real | Bitvector
    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    type sign = {
    1.23 -    theories: smt_theory list,
    1.24 +    header: string list,
    1.25      sorts: string list,
    1.26      funcs: (string * (string list * string)) list }
    1.27    type config = {
    1.28      prefixes: prefixes,
    1.29 +    header: header,
    1.30      strict: strict option,
    1.31      builtins: builtins,
    1.32      serialize: string list -> sign -> sterm list -> string }
    1.33 @@ -39,7 +41,7 @@
    1.34      typs: typ Symtab.table,
    1.35      terms: term Symtab.table,
    1.36      unfolds: thm list,
    1.37 -    assms: thm list option }
    1.38 +    assms: thm list }
    1.39  
    1.40    val translate: config -> Proof.context -> string list -> thm list ->
    1.41      string * recon
    1.42 @@ -66,25 +68,27 @@
    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: string * typ -> bool,
    1.51 +  is_builtin_pred: Proof.context -> string * typ -> bool,
    1.52    is_builtin_distinct: bool}
    1.53  
    1.54  type builtins = {
    1.55 -  builtin_typ: typ -> string option,
    1.56 -  builtin_num: typ -> int -> string option,
    1.57 -  builtin_fun: string * typ -> term list -> (string * term list) option }
    1.58 -
    1.59 -datatype smt_theory = Integer | Real | Bitvector
    1.60 +  builtin_typ: Proof.context -> typ -> string option,
    1.61 +  builtin_num: Proof.context -> typ -> int -> string option,
    1.62 +  builtin_fun: Proof.context -> string * typ -> term list ->
    1.63 +    (string * term list) option }
    1.64  
    1.65  type sign = {
    1.66 -  theories: smt_theory list,
    1.67 +  header: string list,
    1.68    sorts: string list,
    1.69    funcs: (string * (string list * string)) list }
    1.70  
    1.71  type config = {
    1.72    prefixes: prefixes,
    1.73 +  header: header,
    1.74    strict: strict option,
    1.75    builtins: builtins,
    1.76    serialize: string list -> sign -> sterm list -> string }
    1.77 @@ -93,7 +97,7 @@
    1.78    typs: typ Symtab.table,
    1.79    terms: term Symtab.table,
    1.80    unfolds: thm list,
    1.81 -  assms: thm list option }
    1.82 +  assms: thm list }
    1.83  
    1.84  
    1.85  
    1.86 @@ -175,7 +179,6 @@
    1.87  
    1.88  fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
    1.89    let
    1.90 -
    1.91      fun is_builtin_conn' (@{const_name True}, _) = false
    1.92        | is_builtin_conn' (@{const_name False}, _) = false
    1.93        | is_builtin_conn' c = is_builtin_conn c
    1.94 @@ -199,7 +202,7 @@
    1.95          (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
    1.96            c $ in_form t1 $ in_term t2 $ in_term t3
    1.97        | (h as Const c, ts) =>
    1.98 -          if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c)
    1.99 +          if is_builtin_conn' (conn c) orelse is_builtin_pred ctxt (pred c)
   1.100            then wrap_in_if (in_form t)
   1.101            else Term.list_comb (h, map in_term ts)
   1.102        | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
   1.103 @@ -227,7 +230,7 @@
   1.104        | (Const c, ts) =>
   1.105            if is_builtin_conn (conn c)
   1.106            then Term.list_comb (Const (conn c), map in_form ts)
   1.107 -          else if is_builtin_pred (pred c)
   1.108 +          else if is_builtin_pred ctxt (pred c)
   1.109            then Term.list_comb (Const (pred c), map in_term ts)
   1.110            else as_term (in_term t)
   1.111        | _ => as_term (in_term t))
   1.112 @@ -240,62 +243,53 @@
   1.113  
   1.114  (* translation from Isabelle terms into SMT intermediate terms *)
   1.115  
   1.116 -val empty_context = (1, Typtab.empty, 1, Termtab.empty, [])
   1.117 +val empty_context = (1, Typtab.empty, 1, Termtab.empty)
   1.118  
   1.119 -fun make_sign (_, typs, _, terms, thys) = {
   1.120 -  theories = thys,
   1.121 +fun make_sign header (_, typs, _, terms) = {
   1.122 +  header = header,
   1.123    sorts = Typtab.fold (cons o snd) typs [],
   1.124    funcs = Termtab.fold (cons o snd) terms [] }
   1.125  
   1.126 -fun make_recon (unfolds, assms) (_, typs, _, terms, _) = {
   1.127 +fun make_recon (unfolds, assms) (_, typs, _, terms) = {
   1.128    typs = Symtab.make (map swap (Typtab.dest typs)),
   1.129    terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
   1.130    unfolds = unfolds,
   1.131 -  assms = SOME assms }
   1.132 +  assms = assms }
   1.133  
   1.134  fun string_of_index pre i = pre ^ string_of_int i
   1.135  
   1.136 -fun add_theory T (Tidx, typs, idx, terms, thys) =
   1.137 -  let
   1.138 -    fun add @{typ int} = insert (op =) Integer
   1.139 -      | add @{typ real} = insert (op =) Real
   1.140 -      | add (Type (@{type_name word}, _)) = insert (op =) Bitvector
   1.141 -      | add (Type (_, Ts)) = fold add Ts
   1.142 -      | add _ = I
   1.143 -  in (Tidx, typs, idx, terms, add T thys) end
   1.144 -
   1.145 -fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) =
   1.146 +fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms)) =
   1.147    (case Typtab.lookup typs T of
   1.148      SOME s => (s, cx)
   1.149    | NONE =>
   1.150        let
   1.151          val s = string_of_index sort_prefix Tidx
   1.152          val typs' = Typtab.update (T, s) typs
   1.153 -      in (s, (Tidx+1, typs', idx, terms, thys)) end)
   1.154 +      in (s, (Tidx+1, typs', idx, terms)) end)
   1.155  
   1.156 -fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) =
   1.157 +fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms)) =
   1.158    (case Termtab.lookup terms t of
   1.159      SOME (f, _) => (f, cx)
   1.160    | NONE =>
   1.161        let
   1.162          val f = string_of_index func_prefix idx
   1.163          val terms' = Termtab.update (revert_types t, (f, ss)) terms
   1.164 -      in (f, (Tidx, typs, idx+1, terms', thys)) end)
   1.165 +      in (f, (Tidx, typs, idx+1, terms')) end)
   1.166  
   1.167  fun relaxed thms = (([], thms), map prop_of thms)
   1.168  
   1.169 -fun with_context f (ths, ts) =
   1.170 +fun with_context header f (ths, ts) =
   1.171    let val (us, context) = fold_map f ts empty_context
   1.172 -  in ((make_sign context, us), make_recon ths context) end
   1.173 +  in ((make_sign (header ts) context, us), make_recon ths context) end
   1.174  
   1.175  
   1.176 -fun translate {prefixes, strict, builtins, serialize} ctxt comments =
   1.177 +fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
   1.178    let
   1.179      val {sort_prefix, func_prefix} = prefixes
   1.180      val {builtin_typ, builtin_num, builtin_fun} = builtins
   1.181  
   1.182 -    fun transT T = add_theory T #>
   1.183 -      (case builtin_typ T of
   1.184 +    fun transT T =
   1.185 +      (case builtin_typ ctxt T of
   1.186          SOME n => pair n
   1.187        | NONE => fresh_typ sort_prefix T)
   1.188  
   1.189 @@ -313,18 +307,18 @@
   1.190            transT T ##>> trans t1 ##>> trans t2 #>>
   1.191            (fn ((U, u1), u2) => SLet (U, u1, u2))
   1.192        | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
   1.193 -          (case builtin_fun c (HOLogic.dest_list t1) of
   1.194 -            SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n
   1.195 +          (case builtin_fun ctxt c (HOLogic.dest_list t1) of
   1.196 +            SOME (n, ts) => fold_map trans ts #>> app n
   1.197            | NONE => transs h T [t1])
   1.198        | (h as Const (c as (_, T)), ts) =>
   1.199            (case try HOLogic.dest_number t of
   1.200              SOME (T, i) =>
   1.201 -              (case builtin_num T i of
   1.202 -                SOME n => add_theory T #> pair (SApp (n, []))
   1.203 +              (case builtin_num ctxt T i of
   1.204 +                SOME n => pair (SApp (n, []))
   1.205                | NONE => transs t T [])
   1.206            | NONE =>
   1.207 -              (case builtin_fun c ts of
   1.208 -                SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n
   1.209 +              (case builtin_fun ctxt c ts of
   1.210 +                SOME (n, ts') => fold_map trans ts' #>> app n
   1.211                | NONE => transs h T ts))
   1.212        | (h as Free (_, T), ts) => transs h T ts
   1.213        | (Bound i, []) => pair (SVar i)
   1.214 @@ -337,8 +331,8 @@
   1.215          fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
   1.216        end
   1.217    in
   1.218 -    (if is_some strict then strictify (the strict) ctxt else relaxed) #>
   1.219 -    with_context trans #>> uncurry (serialize comments)
   1.220 +    (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
   1.221 +    with_context (header ctxt) trans #>> uncurry (serialize comments)
   1.222    end
   1.223  
   1.224  end