src/HOL/Tools/SMT2/smt2_datatypes.ML
author blanchet
Wed Jun 11 11:28:46 2014 +0200 (2014-06-11)
changeset 57213 9daec42f6784
parent 56078 624faeda77b5
child 57226 c22ad39c3b4b
permissions -rw-r--r--
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet@56078
     1
(*  Title:      HOL/Tools/SMT2/smt2_datatypes.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Collector functions for common type declarations and their representation
blanchet@56078
     5
as algebraic datatypes.
blanchet@56078
     6
*)
blanchet@56078
     7
blanchet@56078
     8
signature SMT2_DATATYPES =
blanchet@56078
     9
sig
blanchet@56078
    10
  val add_decls: typ ->
blanchet@56078
    11
    (typ * (term * term list) list) list list * Proof.context ->
blanchet@56078
    12
    (typ * (term * term list) list) list list * Proof.context
blanchet@56078
    13
end
blanchet@56078
    14
blanchet@56078
    15
structure SMT2_Datatypes: SMT2_DATATYPES =
blanchet@56078
    16
struct
blanchet@56078
    17
blanchet@56078
    18
val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
blanchet@56078
    19
blanchet@56078
    20
fun mk_selectors T Ts ctxt =
blanchet@56078
    21
  let
blanchet@57213
    22
    val (sels, ctxt') = Variable.variant_fixes (replicate (length Ts) "select") ctxt
blanchet@56078
    23
  in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
blanchet@56078
    24
blanchet@56078
    25
blanchet@56078
    26
(* datatype declarations *)
blanchet@56078
    27
blanchet@56078
    28
fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt =
blanchet@56078
    29
  let
blanchet@56078
    30
    fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE
blanchet@56078
    31
    val vars = the (get_first get_vars descr) ~~ Ts
blanchet@56078
    32
    val lookup_var = the o AList.lookup (op =) vars
blanchet@56078
    33
blanchet@56078
    34
    fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
blanchet@56078
    35
      | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
blanchet@56078
    36
      | typ_of (Datatype.DtRec i) =
blanchet@56078
    37
          the (AList.lookup (op =) descr i)
blanchet@56078
    38
          |> (fn (m, dts, _) => Type (m, map typ_of dts))
blanchet@56078
    39
blanchet@56078
    40
    fun mk_constr T (m, dts) ctxt =
blanchet@56078
    41
      let
blanchet@56078
    42
        val Ts = map typ_of dts
blanchet@56078
    43
        val constr = Const (m, Ts ---> T)
blanchet@56078
    44
        val (selects, ctxt') = mk_selectors T Ts ctxt
blanchet@56078
    45
      in ((constr, selects), ctxt') end
blanchet@56078
    46
blanchet@56078
    47
    fun mk_decl (i, (_, _, constrs)) ctxt =
blanchet@56078
    48
      let
blanchet@56078
    49
        val T = typ_of (Datatype.DtRec i)
blanchet@56078
    50
        val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
blanchet@56078
    51
      in ((T, css), ctxt') end
blanchet@56078
    52
blanchet@56078
    53
  in fold_map mk_decl descr ctxt end
blanchet@56078
    54
blanchet@56078
    55
blanchet@56078
    56
(* record declarations *)
blanchet@56078
    57
blanchet@56078
    58
val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode
blanchet@56078
    59
blanchet@56078
    60
fun get_record_decl ({ext_def, ...} : Record.info) T ctxt =
blanchet@56078
    61
  let
blanchet@56078
    62
    val (con, _) = Term.dest_Const (lhs_head_of ext_def)
blanchet@56078
    63
    val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T
blanchet@56078
    64
    val fieldTs = map snd fields @ [snd more]
blanchet@56078
    65
blanchet@56078
    66
    val constr = Const (con, fieldTs ---> T)
blanchet@56078
    67
    val (selects, ctxt') = mk_selectors T fieldTs ctxt
blanchet@56078
    68
  in ((T, [(constr, selects)]), ctxt') end
blanchet@56078
    69
blanchet@56078
    70
blanchet@56078
    71
(* typedef declarations *)
blanchet@56078
    72
blanchet@57213
    73
fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
blanchet@57213
    74
    : Typedef.info) T Ts =
blanchet@57213
    75
  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
blanchet@57213
    76
    let
blanchet@57213
    77
      val env = snd (Term.dest_Type abs_type) ~~ Ts
blanchet@57213
    78
      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
blanchet@56078
    79
blanchet@57213
    80
      val constr = Const (Abs_name, instT (rep_type --> abs_type))
blanchet@57213
    81
      val select = Const (Rep_name, instT (abs_type --> rep_type))
blanchet@57213
    82
    in [(T, [(constr, [select])])] end
blanchet@57213
    83
  else
blanchet@57213
    84
    []
blanchet@56078
    85
blanchet@56078
    86
blanchet@56078
    87
(* collection of declarations *)
blanchet@56078
    88
blanchet@56078
    89
fun declared declss T = exists (exists (equal T o fst)) declss
blanchet@56078
    90
fun declared' dss T = exists (exists (equal T o fst) o snd) dss
blanchet@56078
    91
blanchet@56078
    92
fun get_decls T n Ts ctxt =
blanchet@56078
    93
  let val thy = Proof_Context.theory_of ctxt
blanchet@56078
    94
  in
blanchet@56078
    95
    (case Datatype.get_info thy n of
blanchet@56078
    96
      SOME info => get_datatype_decl info n Ts ctxt
blanchet@56078
    97
    | NONE =>
blanchet@56078
    98
        (case Record.get_info thy (record_name_of n) of
blanchet@56078
    99
          SOME info => get_record_decl info T ctxt |>> single
blanchet@56078
   100
        | NONE =>
blanchet@56078
   101
            (case Typedef.get_info ctxt n of
blanchet@56078
   102
              [] => ([], ctxt)
blanchet@57213
   103
            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
blanchet@56078
   104
  end
blanchet@56078
   105
blanchet@56078
   106
fun add_decls T (declss, ctxt) =
blanchet@56078
   107
  let
blanchet@56078
   108
    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
blanchet@56078
   109
blanchet@56078
   110
    fun add (TFree _) = I
blanchet@56078
   111
      | add (TVar _) = I
blanchet@56078
   112
      | add (T as Type (@{type_name fun}, _)) =
blanchet@56078
   113
          fold add (Term.body_type T :: Term.binder_types T)
blanchet@56078
   114
      | add @{typ bool} = I
blanchet@56078
   115
      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
blanchet@56078
   116
          if declared declss T orelse declared' dss T then (dss, ctxt1)
blanchet@56078
   117
          else if SMT2_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
blanchet@56078
   118
          else
blanchet@56078
   119
            (case get_decls T n Ts ctxt1 of
blanchet@56078
   120
              ([], _) => (dss, ctxt1)
blanchet@56078
   121
            | (ds, ctxt2) =>
blanchet@56078
   122
                let
blanchet@56078
   123
                  val constrTs =
blanchet@56078
   124
                    maps (map (snd o Term.dest_Const o fst) o snd) ds
blanchet@56078
   125
                  val Us = fold (union (op =) o Term.binder_types) constrTs []
blanchet@56078
   126
blanchet@56078
   127
                  fun ins [] = [(Us, ds)]
blanchet@56078
   128
                    | ins ((Uds as (Us', _)) :: Udss) =
blanchet@56078
   129
                        if depends Us' ds then (Us, ds) :: Uds :: Udss
blanchet@56078
   130
                        else Uds :: ins Udss
blanchet@56078
   131
            in fold add Us (ins dss, ctxt2) end))
blanchet@56078
   132
  in add T ([], ctxt) |>> append declss o map snd end
blanchet@56078
   133
blanchet@56078
   134
end