src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58061 3d060f43accb
parent 57229 489083abce44
child 58360 dee1fd1cc631
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -0,0 +1,93 @@
     1.4 +(*  Title:      HOL/Tools/SMT/smt_datatypes.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Collector functions for common type declarations and their representation
     1.8 +as algebraic datatypes.
     1.9 +*)
    1.10 +
    1.11 +signature SMT_DATATYPES =
    1.12 +sig
    1.13 +  val add_decls: typ ->
    1.14 +    (typ * (term * term list) list) list list * Proof.context ->
    1.15 +    (typ * (term * term list) list) list list * Proof.context
    1.16 +end;
    1.17 +
    1.18 +structure SMT_Datatypes: SMT_DATATYPES =
    1.19 +struct
    1.20 +
    1.21 +fun mk_selectors T Ts =
    1.22 +  Variable.variant_fixes (replicate (length Ts) "select")
    1.23 +  #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
    1.24 +
    1.25 +
    1.26 +(* free constructor type declarations *)
    1.27 +
    1.28 +fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
    1.29 +  let
    1.30 +    fun mk_constr ctr0 =
    1.31 +      let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in
    1.32 +        mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr
    1.33 +      end
    1.34 +  in
    1.35 +    fold_map mk_constr ctrs ctxt
    1.36 +    |>> (pair T #> single)
    1.37 +  end
    1.38 +
    1.39 +
    1.40 +(* typedef declarations *)
    1.41 +
    1.42 +fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
    1.43 +    : Typedef.info) T Ts =
    1.44 +  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
    1.45 +    let
    1.46 +      val env = snd (Term.dest_Type abs_type) ~~ Ts
    1.47 +      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    1.48 +
    1.49 +      val constr = Const (Abs_name, instT (rep_type --> abs_type))
    1.50 +      val select = Const (Rep_name, instT (abs_type --> rep_type))
    1.51 +    in [(T, [(constr, [select])])] end
    1.52 +  else
    1.53 +    []
    1.54 +
    1.55 +
    1.56 +(* collection of declarations *)
    1.57 +
    1.58 +fun declared declss T = exists (exists (equal T o fst)) declss
    1.59 +fun declared' dss T = exists (exists (equal T o fst) o snd) dss
    1.60 +
    1.61 +fun get_decls T n Ts ctxt =
    1.62 +  (case Ctr_Sugar.ctr_sugar_of ctxt n of
    1.63 +    SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt
    1.64 +  | NONE =>
    1.65 +      (case Typedef.get_info ctxt n of
    1.66 +        [] => ([], ctxt)
    1.67 +      | info :: _ => (get_typedef_decl info T Ts, ctxt)))
    1.68 +
    1.69 +fun add_decls T (declss, ctxt) =
    1.70 +  let
    1.71 +    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
    1.72 +
    1.73 +    fun add (TFree _) = I
    1.74 +      | add (TVar _) = I
    1.75 +      | add (T as Type (@{type_name fun}, _)) =
    1.76 +          fold add (Term.body_type T :: Term.binder_types T)
    1.77 +      | add @{typ bool} = I
    1.78 +      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
    1.79 +          if declared declss T orelse declared' dss T then (dss, ctxt1)
    1.80 +          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
    1.81 +          else
    1.82 +            (case get_decls T n Ts ctxt1 of
    1.83 +              ([], _) => (dss, ctxt1)
    1.84 +            | (ds, ctxt2) =>
    1.85 +                let
    1.86 +                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
    1.87 +                  val Us = fold (union (op =) o Term.binder_types) constrTs []
    1.88 +
    1.89 +                  fun ins [] = [(Us, ds)]
    1.90 +                    | ins ((Uds as (Us', _)) :: Udss) =
    1.91 +                        if depends Us' ds then (Us, ds) :: Uds :: Udss
    1.92 +                        else Uds :: ins Udss
    1.93 +            in fold add Us (ins dss, ctxt2) end))
    1.94 +  in add T ([], ctxt) |>> append declss o map snd end
    1.95 +
    1.96 +end;