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