src/HOL/Tools/SMT/smt_datatypes.ML
author blanchet
Thu Jun 12 01:00:49 2014 +0200 (2014-06-12)
changeset 57226 c22ad39c3b4b
parent 57213 9daec42f6784
permissions -rw-r--r--
use 'ctr_sugar' abstraction in SMT(2)
boehmes@41426
     1
(*  Title:      HOL/Tools/SMT/smt_datatypes.ML
boehmes@41426
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@41426
     3
boehmes@41426
     4
Collector functions for common type declarations and their representation
boehmes@41426
     5
as algebraic datatypes.
boehmes@41426
     6
*)
boehmes@41426
     7
boehmes@41426
     8
signature SMT_DATATYPES =
boehmes@41426
     9
sig
boehmes@41426
    10
  val add_decls: typ ->
boehmes@41426
    11
    (typ * (term * term list) list) list list * Proof.context ->
boehmes@41426
    12
    (typ * (term * term list) list) list list * Proof.context
boehmes@41426
    13
end
boehmes@41426
    14
boehmes@41426
    15
structure SMT_Datatypes: SMT_DATATYPES =
boehmes@41426
    16
struct
boehmes@41426
    17
boehmes@41426
    18
val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
boehmes@41426
    19
blanchet@57226
    20
fun mk_selectors T Ts =
blanchet@57226
    21
  Variable.variant_fixes (replicate (length Ts) "select")
blanchet@57226
    22
  #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
boehmes@41426
    23
boehmes@41426
    24
blanchet@57226
    25
(* free constructor type declarations *)
boehmes@41426
    26
blanchet@57226
    27
fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
boehmes@41426
    28
  let
blanchet@57226
    29
    fun mk_constr ctr0 =
blanchet@57226
    30
      let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
blanchet@57226
    31
        mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
blanchet@57226
    32
      end
blanchet@57226
    33
  in
blanchet@57226
    34
    fold_map mk_constr ctrs ctxt
blanchet@57226
    35
    |>> (pair T #> single)
blanchet@57226
    36
  end
boehmes@41426
    37
boehmes@41426
    38
boehmes@41426
    39
(* typedef declarations *)
boehmes@41426
    40
blanchet@57213
    41
fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
blanchet@57213
    42
    : Typedef.info) T Ts =
blanchet@57213
    43
  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
blanchet@57213
    44
    let
blanchet@57213
    45
      val env = snd (Term.dest_Type abs_type) ~~ Ts
blanchet@57213
    46
      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
boehmes@41426
    47
blanchet@57213
    48
      val constr = Const (Abs_name, instT (rep_type --> abs_type))
blanchet@57213
    49
      val select = Const (Rep_name, instT (abs_type --> rep_type))
blanchet@57213
    50
    in [(T, [(constr, [select])])] end
blanchet@57213
    51
  else
blanchet@57213
    52
    []
boehmes@41426
    53
boehmes@41426
    54
boehmes@41426
    55
(* collection of declarations *)
boehmes@41426
    56
boehmes@41426
    57
fun declared declss T = exists (exists (equal T o fst)) declss
boehmes@43385
    58
fun declared' dss T = exists (exists (equal T o fst) o snd) dss
boehmes@41426
    59
boehmes@41426
    60
fun get_decls T n Ts ctxt =
blanchet@57226
    61
  (case Ctr_Sugar.ctr_sugar_of ctxt n of
blanchet@57226
    62
    SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
blanchet@57226
    63
  | NONE =>
blanchet@57226
    64
      (case Typedef.get_info ctxt n of
blanchet@57226
    65
        [] => ([], ctxt)
blanchet@57226
    66
      | info :: _ => (get_typedef_decl info T Ts, ctxt)))
boehmes@41426
    67
boehmes@41426
    68
fun add_decls T (declss, ctxt) =
boehmes@41426
    69
  let
boehmes@43385
    70
    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
boehmes@43385
    71
boehmes@41426
    72
    fun add (TFree _) = I
boehmes@41426
    73
      | add (TVar _) = I
boehmes@41426
    74
      | add (T as Type (@{type_name fun}, _)) =
boehmes@41426
    75
          fold add (Term.body_type T :: Term.binder_types T)
boehmes@41426
    76
      | add @{typ bool} = I
boehmes@41426
    77
      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
boehmes@43385
    78
          if declared declss T orelse declared' dss T then (dss, ctxt1)
boehmes@41426
    79
          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
boehmes@41426
    80
          else
boehmes@41426
    81
            (case get_decls T n Ts ctxt1 of
boehmes@41426
    82
              ([], _) => (dss, ctxt1)
boehmes@41426
    83
            | (ds, ctxt2) =>
boehmes@41426
    84
                let
boehmes@41426
    85
                  val constrTs =
boehmes@41426
    86
                    maps (map (snd o Term.dest_Const o fst) o snd) ds
boehmes@41426
    87
                  val Us = fold (union (op =) o Term.binder_types) constrTs []
boehmes@43385
    88
boehmes@43385
    89
                  fun ins [] = [(Us, ds)]
boehmes@43385
    90
                    | ins ((Uds as (Us', _)) :: Udss) =
boehmes@43385
    91
                        if depends Us' ds then (Us, ds) :: Uds :: Udss
boehmes@43385
    92
                        else Uds :: ins Udss
boehmes@43385
    93
            in fold add Us (ins dss, ctxt2) end))
boehmes@43385
    94
  in add T ([], ctxt) |>> append declss o map snd end
boehmes@43385
    95
boehmes@41426
    96
end