1structure bagSyntax :> bagSyntax = 2struct 3 4open HolKernel Parse boolLib simpLib boolSimps bagTheory; 5 6val ERR = mk_HOL_ERR "bagLib"; 7 8val num_ty = numSyntax.num 9 10val bag_ty = Type.alpha --> num_ty 11fun is_bag_ty ty = #2 (dom_rng ty) = num_ty handle HOL_ERR _ => false 12 13val BAG_INSERT_tm = mk_const("BAG_INSERT", alpha --> bag_ty --> bag_ty); 14val BAG_UNION_tm = mk_const("BAG_UNION", bag_ty --> bag_ty --> bag_ty); 15val BAG_DIFF_tm = mk_const("BAG_DIFF", bag_ty --> bag_ty --> bag_ty); 16val BAG_CARD_tm = mk_const("BAG_CARD", bag_ty --> num_ty); 17val EMPTY_BAG_tm = mk_const("EMPTY_BAG", bag_ty); 18val SUB_BAG_tm = mk_const("SUB_BAG", bag_ty --> bag_ty --> bool); 19val BAG_EQ_tm = mk_const("=", bag_ty --> bag_ty --> bool); 20val BAG_IMAGE_tm = mk_const("BAG_IMAGE", 21 (Type.alpha --> Type.beta) --> (Type.alpha --> num_ty) --> 22 (Type.beta --> num_ty)); 23val BAG_ALL_DISTINCT_tm = mk_const("BAG_ALL_DISTINCT", bag_ty --> bool); 24val BAG_EVERY_tm = mk_const("BAG_EVERY", 25 (Type.alpha --> bool) --> bag_ty --> bool) 26 27 28fun base_type tm = let 29 val ty = type_of tm 30 val (dom,rng) = dom_rng ty 31in 32 if rng = num_ty then dom 33 else raise ERR "bag_base_type" "term not a bag" 34end 35 36fun mk_union (tm1, tm2) = let 37 val bt = base_type tm1 38 val bu_tm = Term.inst [alpha |-> bt] BAG_UNION_tm 39in 40 list_mk_comb(bu_tm, [tm1, tm2]) 41end 42fun mk_diff(tm1, tm2) = let 43 val bt = base_type tm1 44 val bd_tm = Term.inst [alpha |-> bt] BAG_DIFF_tm 45in 46 list_mk_comb(bd_tm, [tm1, tm2]) 47end 48 49fun dest_binop name callername tm = let 50 val (f, args) = strip_comb tm 51 val _ = length args = 2 orelse raise ERR callername "not a binary term" 52 val (nm, _) = dest_const f 53 val _ = nm = name orelse raise ERR callername ("not a "^name) 54in 55 (hd args, hd (tl args)) 56end 57 58 59val dest_union = dest_binop "BAG_UNION" "dest_union" 60val is_union = can dest_union 61val dest_diff = dest_binop "BAG_DIFF" "dest_diff" 62val is_diff = can dest_diff 63fun mk_every (tm1, tm2) = list_mk_icomb(BAG_EVERY_tm, [tm1, tm2]) 64val dest_every = dest_binop "BAG_EVERY" "dest_every" 65val is_every = can dest_every 66 67fun list_mk_union0 bu_t acc tmlist = 68 case tmlist of 69 [] => acc 70 | (t::ts) => list_mk_union0 bu_t (list_mk_comb(bu_t, [acc,t])) ts 71 72fun list_mk_union [] = raise ERR "list_mk_union" "term list empty" 73 | list_mk_union (t::ts) = 74 list_mk_union0 (Term.inst [alpha |-> base_type t] BAG_UNION_tm) t ts 75 76fun strip_union0 acc t = 77 if is_union t then let 78 val (l,r) = dest_union t 79 in 80 strip_union0 (strip_union0 acc r) l 81 end 82 else t::acc 83 84val strip_union = strip_union0 [] 85 86fun mk_insert (tm1, tm2) = let 87 val bt = base_type tm2 88 val bi = Term.inst [alpha |-> bt] BAG_INSERT_tm 89in 90 list_mk_comb(bi, [tm1, tm2]) 91end 92 93val dest_insert = dest_binop "BAG_INSERT" "dest_insert" 94val is_insert = can dest_insert 95 96fun mk_all_distinct b = mk_icomb (BAG_ALL_DISTINCT_tm, b); 97fun dest_all_distinct tm = let 98 val (f, arg) = dest_comb tm 99 val _ = (aconv f BAG_ALL_DISTINCT_tm) orelse 100 raise ERR "BAG_ALL_DISTINCT" ("not a BAG_ALL_DISTINCT") 101in 102 arg 103end 104val is_all_distinct = can dest_all_distinct 105 106 107fun mk_card tm = 108 mk_icomb(BAG_CARD_tm, tm) 109fun dest_card tm = let 110 val (f, arg) = dest_comb tm 111 val _ = (aconv f BAG_CARD_tm) orelse 112 raise ERR "BAG_CARD" ("not a BAG_CARD") 113in 114 arg 115end 116val is_card = can dest_card 117 118 119fun mk_image (tm1, tm2) = 120 list_mk_icomb(BAG_IMAGE_tm, [tm1, tm2]) 121val dest_image = dest_binop "BAG_IMAGE" "dest_image" 122val is_image = can dest_image 123 124val is_empty = same_const EMPTY_BAG_tm 125 126fun list_mk_insert (tms, t) = 127 case tms of 128 (h::_) => let 129 val cnst = Term.inst [alpha |-> type_of h] BAG_INSERT_tm 130 in 131 List.foldr (fn (i,b) => list_mk_comb(cnst, [i,b])) t tms 132 end 133 | [] => t 134 135fun strip_insert0 acc tm = 136 if is_insert tm then let 137 val (i,b) = dest_insert tm 138 in 139 strip_insert0 (i::acc) b 140 end 141 else (rev acc, tm) 142val strip_insert = strip_insert0 [] 143 144fun mk_sub_bag (tm1, tm2) = let 145 val bt = base_type tm1 146 val sb = Term.inst [alpha |-> bt] SUB_BAG_tm 147in 148 list_mk_comb(sb, [tm1, tm2]) 149end 150val dest_sub_bag = dest_binop "SUB_BAG" "dest_sub_bag" 151val is_sub_bag = can dest_sub_bag 152 153fun mk_bag (tms, ty) = 154 list_mk_insert(tms, Term.inst [alpha |-> ty] EMPTY_BAG_tm) 155 156fun dest_bag tm = let 157 val (els, b) = strip_insert tm 158 val _ = is_const b andalso fst (Term.dest_const b) = "EMPTY_BAG" orelse 159 raise ERR "dest_bag" "Not a bag literal" 160in 161 (els, base_type b) 162end 163 164end 165