src/HOL/Library/Old_SMT/old_smt_builtin.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 58058 1a0b18176548
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Library/Old_SMT/old_smt_builtin.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Tables of types and terms directly supported by SMT solvers.
     5 *)
     6 
     7 signature OLD_SMT_BUILTIN =
     8 sig
     9   (*for experiments*)
    10   val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
    11 
    12   (*built-in types*)
    13   val add_builtin_typ: Old_SMT_Utils.class ->
    14     typ * (typ -> string option) * (typ -> int -> string option) ->
    15     Context.generic -> Context.generic
    16   val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
    17     Context.generic
    18   val dest_builtin_typ: Proof.context -> typ -> string option
    19   val is_builtin_typ_ext: Proof.context -> typ -> bool
    20 
    21   (*built-in numbers*)
    22   val dest_builtin_num: Proof.context -> term -> (string * typ) option
    23   val is_builtin_num: Proof.context -> term -> bool
    24   val is_builtin_num_ext: Proof.context -> term -> bool
    25 
    26   (*built-in functions*)
    27   type 'a bfun = Proof.context -> typ -> term list -> 'a
    28   type bfunr = string * int * term list * (term list -> term)
    29   val add_builtin_fun: Old_SMT_Utils.class ->
    30     (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
    31   val add_builtin_fun': Old_SMT_Utils.class -> term * string -> Context.generic ->
    32     Context.generic
    33   val add_builtin_fun_ext: (string * typ) * term list bfun ->
    34     Context.generic -> Context.generic
    35   val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
    36   val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
    37   val dest_builtin_fun: Proof.context -> string * typ -> term list ->
    38     bfunr option
    39   val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
    40   val dest_builtin_pred: Proof.context -> string * typ -> term list ->
    41     bfunr option
    42   val dest_builtin_conn: Proof.context -> string * typ -> term list ->
    43     bfunr option
    44   val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
    45   val dest_builtin_ext: Proof.context -> string * typ -> term list ->
    46     term list option
    47   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
    48   val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
    49 end
    50 
    51 structure Old_SMT_Builtin: OLD_SMT_BUILTIN =
    52 struct
    53 
    54 
    55 (* built-in tables *)
    56 
    57 datatype ('a, 'b) kind = Ext of 'a | Int of 'b
    58 
    59 type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) Old_SMT_Utils.dict 
    60 
    61 fun typ_ord ((T, _), (U, _)) =
    62   let
    63     fun tord (TVar _, Type _) = GREATER
    64       | tord (Type _, TVar _) = LESS
    65       | tord (Type (n, Ts), Type (m, Us)) =
    66           if n = m then list_ord tord (Ts, Us)
    67           else Term_Ord.typ_ord (T, U)
    68       | tord TU = Term_Ord.typ_ord TU
    69   in tord (T, U) end
    70 
    71 fun insert_ttab cs T f =
    72   Old_SMT_Utils.dict_map_default (cs, [])
    73     (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
    74 
    75 fun merge_ttab ttabp =
    76   Old_SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
    77 
    78 fun lookup_ttab ctxt ttab T =
    79   let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
    80   in
    81     get_first (find_first match)
    82       (Old_SMT_Utils.dict_lookup ttab (Old_SMT_Config.solver_class_of ctxt))
    83   end
    84 
    85 type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
    86 
    87 fun insert_btab cs n T f =
    88   Symtab.map_default (n, []) (insert_ttab cs T f)
    89 
    90 fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
    91 
    92 fun lookup_btab ctxt btab (n, T) =
    93   (case Symtab.lookup btab n of
    94     NONE => NONE
    95   | SOME ttab => lookup_ttab ctxt ttab T)
    96 
    97 type 'a bfun = Proof.context -> typ -> term list -> 'a
    98 
    99 type bfunr = string * int * term list * (term list -> term)
   100 
   101 structure Builtins = Generic_Data
   102 (
   103   type T =
   104     (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
   105     (term list bfun, bfunr option bfun) btab
   106   val empty = ([], Symtab.empty)
   107   val extend = I
   108   fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
   109 )
   110 
   111 fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst)))
   112 
   113 fun filter_builtins keep_T =
   114   Context.proof_map (Builtins.map (fn (ttab, btab) =>
   115     (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab)))
   116 
   117 
   118 (* built-in types *)
   119 
   120 fun add_builtin_typ cs (T, f, g) =
   121   Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
   122 
   123 fun add_builtin_typ_ext (T, f) =
   124   Builtins.map (apfst (insert_ttab Old_SMT_Utils.basicC T (Ext f)))
   125 
   126 fun lookup_builtin_typ ctxt =
   127   lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
   128 
   129 fun dest_builtin_typ ctxt T =
   130   (case lookup_builtin_typ ctxt T of
   131     SOME (_, Int (f, _)) => f T
   132   | _ => NONE) 
   133 
   134 fun is_builtin_typ_ext ctxt T =
   135   (case lookup_builtin_typ ctxt T of
   136     SOME (_, Int (f, _)) => is_some (f T)
   137   | SOME (_, Ext f) => f T
   138   | NONE => false)
   139 
   140 
   141 (* built-in numbers *)
   142 
   143 fun dest_builtin_num ctxt t =
   144   (case try HOLogic.dest_number t of
   145     NONE => NONE
   146   | SOME (T, i) =>
   147       if i < 0 then NONE else
   148         (case lookup_builtin_typ ctxt T of
   149           SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
   150         | _ => NONE))
   151 
   152 val is_builtin_num = is_some oo dest_builtin_num
   153 
   154 fun is_builtin_num_ext ctxt t =
   155   (case try HOLogic.dest_number t of
   156     NONE => false
   157   | SOME (T, _) => is_builtin_typ_ext ctxt T)
   158 
   159 
   160 (* built-in functions *)
   161 
   162 fun add_builtin_fun cs ((n, T), f) =
   163   Builtins.map (apsnd (insert_btab cs n T (Int f)))
   164 
   165 fun add_builtin_fun' cs (t, n) =
   166   let
   167     val c as (m, T) = Term.dest_Const t
   168     fun app U ts = Term.list_comb (Const (m, U), ts)
   169     fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
   170   in add_builtin_fun cs (c, bfun) end
   171 
   172 fun add_builtin_fun_ext ((n, T), f) =
   173   Builtins.map (apsnd (insert_btab Old_SMT_Utils.basicC n T (Ext f)))
   174 
   175 fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
   176 
   177 fun add_builtin_fun_ext'' n context =
   178   let val thy = Context.theory_of context
   179   in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
   180 
   181 fun lookup_builtin_fun ctxt =
   182   lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt)))
   183 
   184 fun dest_builtin_fun ctxt (c as (_, T)) ts =
   185   (case lookup_builtin_fun ctxt c of
   186     SOME (_, Int f) => f ctxt T ts
   187   | _ => NONE)
   188 
   189 fun dest_builtin_eq ctxt t u =
   190   let
   191     val aT = TFree (Name.aT, @{sort type})
   192     val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
   193     fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
   194   in
   195     dest_builtin_fun ctxt c []
   196     |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
   197   end
   198 
   199 fun special_builtin_fun pred ctxt (c as (_, T)) ts =
   200   if pred (Term.body_type T, Term.binder_types T) then
   201     dest_builtin_fun ctxt c ts
   202   else NONE
   203 
   204 fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
   205 
   206 fun dest_builtin_conn ctxt =
   207   special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
   208 
   209 fun dest_builtin ctxt c ts =
   210   let val t = Term.list_comb (Const c, ts)
   211   in
   212     (case dest_builtin_num ctxt t of
   213       SOME (n, _) => SOME (n, 0, [], K t)
   214     | NONE => dest_builtin_fun ctxt c ts)
   215   end
   216 
   217 fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
   218   (case lookup_builtin_fun ctxt c of
   219     SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
   220   | SOME (_, Ext f) => SOME (f ctxt T ts)
   221   | NONE => NONE)
   222 
   223 fun dest_builtin_ext ctxt c ts =
   224   if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
   225   else dest_builtin_fun_ext ctxt c ts
   226 
   227 fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
   228 
   229 fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
   230 
   231 end