1(* Title: HOL/Tools/SMT/smt_datatypes.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Collector functions for common type declarations and their representation 5as (co)algebraic datatypes. 6*) 7 8signature SMT_DATATYPES = 9sig 10 val add_decls: BNF_Util.fp_kind list -> typ -> 11 (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context -> 12 (BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context 13end; 14 15structure SMT_Datatypes: SMT_DATATYPES = 16struct 17 18fun 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 28fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = 29 let 30 val selss = map (map (Ctr_Sugar.mk_disc_or_sel Ts)) selss0 31 val ctrs = map (Ctr_Sugar.mk_ctr Ts) ctrs0 32 33 fun mk_constr ctr sels = 34 mk_selectors T (binder_types (fastype_of ctr)) sels #>> pair ctr 35 36 val selss' = 37 (if has_duplicates (op aconv) (flat selss) orelse 38 exists (exists (can (dest_funT o range_type o fastype_of))) selss then 39 [] 40 else 41 selss) 42 |> Ctr_Sugar_Util.pad_list [] (length ctrs) 43 in 44 @{fold_map 2} mk_constr ctrs selss' ctxt 45 |>> (pair T #> single) 46 end 47 48 49(* typedef declarations *) 50 51fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...}) 52 : Typedef.info) T Ts = 53 if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then 54 let 55 val env = snd (Term.dest_Type abs_type) ~~ Ts 56 val instT = Term.map_atyps (perhaps (AList.lookup (op =) env)) 57 58 val constr = Const (Abs_name, instT (rep_type --> abs_type)) 59 val select = Const (Rep_name, instT (abs_type --> rep_type)) 60 in [(T, [(constr, [select])])] end 61 else 62 [] 63 64 65(* collection of declarations *) 66 67val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *) 68 69fun get_decls fps T n Ts ctxt = 70 let 71 fun maybe_typedef () = 72 (case Typedef.get_info ctxt n of 73 [] => ([], ctxt) 74 | info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt)) 75 in 76 (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of 77 SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} => 78 if member (op =) fps fp then 79 let 80 val ns = map (fst o dest_Type) fp_Ts 81 val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns 82 val Xs = map #X mutual_fp_sugars 83 val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars 84 85 (* Datatypes nested through datatypes and codatatypes nested through codatatypes are 86 allowed. So are mutually (co)recursive (co)datatypes. *) 87 fun is_same_fp s = 88 (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of 89 SOME {fp = fp', ...} => fp' = fp 90 | NONE => false) 91 fun is_homogenously_nested_co_recursive (Type (s, Ts)) = 92 forall (if is_same_fp s then is_homogenously_nested_co_recursive 93 else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts 94 | is_homogenously_nested_co_recursive _ = true 95 96 val Type (_, As) :: _ = fp_Ts 97 val substAs = Term.typ_subst_atomic (As ~~ Ts); 98 in 99 (* TODO/FIXME: The "bool" check is there to work around a CVC4 bug 100 (http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=597). It should be removed once 101 the bug is fixed. *) 102 if forall (forall (forall (is_homogenously_nested_co_recursive))) ctrXs_Tsss andalso 103 forall (forall (forall (curry (op <>) \<^typ>\<open>bool\<close>))) 104 (map (map (map substAs)) ctrXs_Tsss) then 105 get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp) 106 else 107 maybe_typedef () 108 end 109 else 110 ([], ctxt) 111 | NONE => 112 if String.isSuffix extN n then 113 (* for records (FIXME: hack) *) 114 (case Ctr_Sugar.ctr_sugar_of ctxt n of 115 SOME ctr_sugar => 116 get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair (hd fps)) 117 | NONE => maybe_typedef ()) 118 else 119 maybe_typedef ()) 120 end 121 122fun add_decls fps T (declss, ctxt) = 123 let 124 fun declared T = exists (exists (equal T o fst o snd)) 125 fun declared' T = exists (exists (equal T o fst o snd) o snd) 126 fun depends ds = exists (member (op =) (map (fst o snd) ds)) 127 128 fun add (TFree _) = I 129 | add (TVar _) = I 130 | add (T as Type (\<^type_name>\<open>fun\<close>, _)) = 131 fold add (Term.body_type T :: Term.binder_types T) 132 | add \<^typ>\<open>bool\<close> = I 133 | add (T as Type (n, Ts)) = (fn (dss, ctxt1) => 134 if declared T declss orelse declared' T dss then 135 (dss, ctxt1) 136 else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then 137 (dss, ctxt1) 138 else 139 (case get_decls fps T n Ts ctxt1 of 140 ([], _) => (dss, ctxt1) 141 | (ds, ctxt2) => 142 let 143 val constrTs = maps (map (snd o Term.dest_Const o fst) o snd o snd) ds 144 val Us = fold (union (op =) o Term.binder_types) constrTs [] 145 146 fun ins [] = [(Us, ds)] 147 | ins ((Uds as (Us', _)) :: Udss) = 148 if depends ds Us' then (Us, ds) :: Uds :: Udss else Uds :: ins Udss 149 in fold add Us (ins dss, ctxt2) end)) 150 in add T ([], ctxt) |>> append declss o map snd end 151 152end; 153