src/HOL/Tools/SMT/smt_datatypes.ML
author blanchet
Wed Sep 24 15:46:23 2014 +0200 (2014-09-24)
changeset 58427 cc1bab5558b0
parent 58364 efc56d935728
child 58428 e4e34dfc3e68
permissions -rw-r--r--
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/smt_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@58361
     5
as (co)algebraic datatypes.
blanchet@56078
     6
*)
blanchet@56078
     7
blanchet@58061
     8
signature SMT_DATATYPES =
blanchet@56078
     9
sig
blanchet@58360
    10
  val add_decls: BNF_Util.fp_kind -> 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@57229
    13
end;
blanchet@56078
    14
blanchet@58061
    15
structure SMT_Datatypes: SMT_DATATYPES =
blanchet@56078
    16
struct
blanchet@56078
    17
blanchet@58362
    18
fun mk_selectors T Ts sels =
blanchet@58362
    19
  if null sels then
blanchet@58362
    20
    Variable.variant_fixes (replicate (length Ts) "select")
blanchet@58362
    21
    #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
blanchet@58362
    22
  else
blanchet@58362
    23
    pair sels
blanchet@56078
    24
blanchet@56078
    25
blanchet@57226
    26
(* free constructor type declarations *)
blanchet@56078
    27
blanchet@58362
    28
fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
blanchet@56078
    29
  let
blanchet@58362
    30
    fun mk_constr ctr0 sels0 =
blanchet@58362
    31
      let
blanchet@58362
    32
        val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
blanchet@58362
    33
        val ctr = Ctr_Sugar.mk_ctr Ts ctr0
blanchet@58362
    34
        val binder_Ts = binder_types (fastype_of ctr)
blanchet@58362
    35
      in
blanchet@58362
    36
        mk_selectors T binder_Ts sels #>> pair ctr
blanchet@57226
    37
      end
blanchet@58362
    38
blanchet@58362
    39
    val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
blanchet@57226
    40
  in
blanchet@58362
    41
    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
blanchet@57226
    42
    |>> (pair T #> single)
blanchet@57226
    43
  end
blanchet@56078
    44
blanchet@56078
    45
blanchet@56078
    46
(* typedef declarations *)
blanchet@56078
    47
blanchet@57213
    48
fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
blanchet@57213
    49
    : Typedef.info) T Ts =
blanchet@57213
    50
  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
blanchet@57213
    51
    let
blanchet@57213
    52
      val env = snd (Term.dest_Type abs_type) ~~ Ts
blanchet@57213
    53
      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
blanchet@56078
    54
blanchet@57213
    55
      val constr = Const (Abs_name, instT (rep_type --> abs_type))
blanchet@57213
    56
      val select = Const (Rep_name, instT (abs_type --> rep_type))
blanchet@57213
    57
    in [(T, [(constr, [select])])] end
blanchet@57213
    58
  else
blanchet@57213
    59
    []
blanchet@56078
    60
blanchet@56078
    61
blanchet@56078
    62
(* collection of declarations *)
blanchet@56078
    63
blanchet@58427
    64
val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *)
blanchet@58361
    65
blanchet@58361
    66
fun get_decls fp T n Ts ctxt =
blanchet@58361
    67
  let
blanchet@58427
    68
    fun maybe_typedef () =
blanchet@57226
    69
      (case Typedef.get_info ctxt n of
blanchet@57226
    70
        [] => ([], ctxt)
blanchet@58361
    71
      | info :: _ => (get_typedef_decl info T Ts, ctxt))
blanchet@58361
    72
  in
blanchet@58427
    73
    (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
blanchet@58427
    74
      SOME {fp = fp', ctr_sugar, ...} =>
blanchet@58427
    75
      if fp' = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else ([], ctxt)
blanchet@58427
    76
    | NONE =>
blanchet@58427
    77
      if fp = BNF_Util.Least_FP then
blanchet@58427
    78
        if String.isSuffix extN n then
blanchet@58427
    79
          (* for records (FIXME: hack) *)
blanchet@58427
    80
          (case Ctr_Sugar.ctr_sugar_of ctxt n of
blanchet@58427
    81
            SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
blanchet@58427
    82
          | NONE => maybe_typedef ())
blanchet@58427
    83
        else
blanchet@58427
    84
          maybe_typedef ()
blanchet@58427
    85
      else
blanchet@58427
    86
        ([], ctxt))
blanchet@58361
    87
  end
blanchet@56078
    88
blanchet@58360
    89
fun add_decls fp T (declss, ctxt) =
blanchet@56078
    90
  let
blanchet@58364
    91
    fun declared T = exists (exists (equal T o fst))
blanchet@58364
    92
    fun declared' T = exists (exists (equal T o fst) o snd)
blanchet@58364
    93
    fun depends ds = exists (member (op =) (map fst ds))
blanchet@56078
    94
blanchet@56078
    95
    fun add (TFree _) = I
blanchet@56078
    96
      | add (TVar _) = I
blanchet@56078
    97
      | add (T as Type (@{type_name fun}, _)) =
blanchet@56078
    98
          fold add (Term.body_type T :: Term.binder_types T)
blanchet@56078
    99
      | add @{typ bool} = I
blanchet@56078
   100
      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
blanchet@58364
   101
          if declared T declss orelse declared' T dss then (dss, ctxt1)
blanchet@58061
   102
          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
blanchet@56078
   103
          else
blanchet@58361
   104
            (case get_decls fp T n Ts ctxt1 of
blanchet@56078
   105
              ([], _) => (dss, ctxt1)
blanchet@56078
   106
            | (ds, ctxt2) =>
blanchet@56078
   107
                let
blanchet@57226
   108
                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
blanchet@56078
   109
                  val Us = fold (union (op =) o Term.binder_types) constrTs []
blanchet@56078
   110
blanchet@56078
   111
                  fun ins [] = [(Us, ds)]
blanchet@56078
   112
                    | ins ((Uds as (Us', _)) :: Udss) =
blanchet@58364
   113
                        if depends ds Us' then (Us, ds) :: Uds :: Udss else Uds :: ins Udss
blanchet@56078
   114
            in fold add Us (ins dss, ctxt2) end))
blanchet@56078
   115
  in add T ([], ctxt) |>> append declss o map snd end
blanchet@56078
   116
blanchet@57229
   117
end;