src/HOL/Tools/SMT/smt_datatypes.ML
author blanchet
Wed Sep 24 15:46:24 2014 +0200 (2014-09-24)
changeset 58428 e4e34dfc3e68
parent 58427 cc1bab5558b0
child 58429 0b94858325a5
permissions -rw-r--r--
rule out nested (co)recursion for SMT (co)datatypes
     1 (*  Title:      HOL/Tools/SMT/smt_datatypes.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Collector functions for common type declarations and their representation
     5 as (co)algebraic datatypes.
     6 *)
     7 
     8 signature SMT_DATATYPES =
     9 sig
    10   val add_decls: BNF_Util.fp_kind -> typ ->
    11     (typ * (term * term list) list) list list * Proof.context ->
    12     (typ * (term * term list) list) list list * Proof.context
    13 end;
    14 
    15 structure SMT_Datatypes: SMT_DATATYPES =
    16 struct
    17 
    18 fun mk_selectors T Ts sels =
    19   if null sels then
    20     Variable.variant_fixes (replicate (length Ts) "select")
    21     #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    22   else
    23     pair sels
    24 
    25 
    26 (* free constructor type declarations *)
    27 
    28 fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    29   let
    30     fun mk_constr ctr0 sels0 =
    31       let
    32         val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
    33         val ctr = Ctr_Sugar.mk_ctr Ts ctr0
    34         val binder_Ts = binder_types (fastype_of ctr)
    35       in
    36         mk_selectors T binder_Ts sels #>> pair ctr
    37       end
    38 
    39     val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
    40   in
    41     Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
    42     |>> (pair T #> single)
    43   end
    44 
    45 
    46 (* typedef declarations *)
    47 
    48 fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
    49     : Typedef.info) T Ts =
    50   if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
    51     let
    52       val env = snd (Term.dest_Type abs_type) ~~ Ts
    53       val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    54 
    55       val constr = Const (Abs_name, instT (rep_type --> abs_type))
    56       val select = Const (Rep_name, instT (abs_type --> rep_type))
    57     in [(T, [(constr, [select])])] end
    58   else
    59     []
    60 
    61 
    62 (* collection of declarations *)
    63 
    64 val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *)
    65 
    66 fun get_decls fp T n Ts ctxt =
    67   let
    68     fun maybe_typedef () =
    69       (case Typedef.get_info ctxt n of
    70         [] => ([], ctxt)
    71       | info :: _ => (get_typedef_decl info T Ts, ctxt))
    72   in
    73     (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
    74       SOME {fp = fp', fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
    75       if fp' = fp then
    76         let
    77           val ns = map (fst o dest_Type) fp_Ts
    78           val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
    79           val Xs = map #X mutual_fp_sugars
    80           val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
    81 
    82           fun is_nested_co_recursive (T as Type _) =
    83               BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
    84             | is_nested_co_recursive _ = false
    85         in
    86           if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef ()
    87           else get_ctr_sugar_decl ctr_sugar T Ts ctxt
    88         end
    89       else
    90         ([], ctxt)
    91     | NONE =>
    92       if fp = BNF_Util.Least_FP then
    93         if String.isSuffix extN n then
    94           (* for records (FIXME: hack) *)
    95           (case Ctr_Sugar.ctr_sugar_of ctxt n of
    96             SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    97           | NONE => maybe_typedef ())
    98         else
    99           maybe_typedef ()
   100       else
   101         ([], ctxt))
   102   end
   103 
   104 fun add_decls fp T (declss, ctxt) =
   105   let
   106     fun declared T = exists (exists (equal T o fst))
   107     fun declared' T = exists (exists (equal T o fst) o snd)
   108     fun depends ds = exists (member (op =) (map fst ds))
   109 
   110     fun add (TFree _) = I
   111       | add (TVar _) = I
   112       | add (T as Type (@{type_name fun}, _)) =
   113           fold add (Term.body_type T :: Term.binder_types T)
   114       | add @{typ bool} = I
   115       | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
   116           if declared T declss orelse declared' T dss then (dss, ctxt1)
   117           else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
   118           else
   119             (case get_decls fp T n Ts ctxt1 of
   120               ([], _) => (dss, ctxt1)
   121             | (ds, ctxt2) =>
   122                 let
   123                   val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
   124                   val Us = fold (union (op =) o Term.binder_types) constrTs []
   125 
   126                   fun ins [] = [(Us, ds)]
   127                     | ins ((Uds as (Us', _)) :: Udss) =
   128                         if depends ds Us' then (Us, ds) :: Uds :: Udss else Uds :: ins Udss
   129             in fold add Us (ins dss, ctxt2) end))
   130   in add T ([], ctxt) |>> append declss o map snd end
   131 
   132 end;