src/HOL/Tools/SMT/smt_datatypes.ML
author blanchet
Wed Sep 17 17:32:27 2014 +0200 (2014-09-17)
changeset 58361 7f2b3b6f6ad1
parent 58360 dee1fd1cc631
child 58362 cf32eb8001b8
permissions -rw-r--r--
added codatatype support for CVC4
     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 =
    19   Variable.variant_fixes (replicate (length Ts) "select")
    20   #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    21 
    22 
    23 (* free constructor type declarations *)
    24 
    25 fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    26   let
    27     fun mk_constr ctr0 =
    28       let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
    29         mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
    30       end
    31   in
    32     fold_map mk_constr ctrs ctxt
    33     |>> (pair T #> single)
    34   end
    35 
    36 
    37 (* typedef declarations *)
    38 
    39 fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
    40     : Typedef.info) T Ts =
    41   if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
    42     let
    43       val env = snd (Term.dest_Type abs_type) ~~ Ts
    44       val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    45 
    46       val constr = Const (Abs_name, instT (rep_type --> abs_type))
    47       val select = Const (Rep_name, instT (abs_type --> rep_type))
    48     in [(T, [(constr, [select])])] end
    49   else
    50     []
    51 
    52 
    53 (* collection of declarations *)
    54 
    55 fun declared declss T = exists (exists (equal T o fst)) declss
    56 fun declared' dss T = exists (exists (equal T o fst) o snd) dss
    57 
    58 (* Simplification: We assume that every type that is not a codatatype is a datatype (or a
    59    record). *)
    60 fun fp_kind_of ctxt n =
    61   (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
    62     SOME {fp, ...} => fp
    63   | NONE => BNF_Util.Least_FP)
    64 
    65 fun get_decls fp T n Ts ctxt =
    66   let
    67     fun fallback () =
    68       (case Typedef.get_info ctxt n of
    69         [] => ([], ctxt)
    70       | info :: _ => (get_typedef_decl info T Ts, ctxt))
    71   in
    72     (case Ctr_Sugar.ctr_sugar_of ctxt n of
    73       SOME ctr_sugar =>
    74       if fp_kind_of ctxt n = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else fallback ()
    75     | NONE => fallback ())
    76   end
    77 
    78 fun add_decls fp T (declss, ctxt) =
    79   let
    80     fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
    81 
    82     fun add (TFree _) = I
    83       | add (TVar _) = I
    84       | add (T as Type (@{type_name fun}, _)) =
    85           fold add (Term.body_type T :: Term.binder_types T)
    86       | add @{typ bool} = I
    87       | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
    88           if declared declss T orelse declared' dss T then (dss, ctxt1)
    89           else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
    90           else
    91             (case get_decls fp T n Ts ctxt1 of
    92               ([], _) => (dss, ctxt1)
    93             | (ds, ctxt2) =>
    94                 let
    95                   val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
    96                   val Us = fold (union (op =) o Term.binder_types) constrTs []
    97 
    98                   fun ins [] = [(Us, ds)]
    99                     | ins ((Uds as (Us', _)) :: Udss) =
   100                         if depends Us' ds then (Us, ds) :: Uds :: Udss
   101                         else Uds :: ins Udss
   102             in fold add Us (ins dss, ctxt2) end))
   103   in add T ([], ctxt) |>> append declss o map snd end
   104 
   105 end;