1(*---------------------------------------------------------------------------* 2 * Building records of facts about datatypes. * 3 *---------------------------------------------------------------------------*) 4 5structure TypeBase :> TypeBase = 6struct 7 8open HolKernel TypeBasePure; 9 10val ERR = mk_HOL_ERR "TypeBase"; 11 12(* ---------------------------------------------------------------------- 13 Functions used to tweak "bare" tyinfo values 14 ---------------------------------------------------------------------- *) 15fun list_compose [] x = x | list_compose (f :: fs) x = list_compose fs (f x); 16 17(* tyinfo values can include references to conversions through the 18 ssfrag database 19*) 20fun resolve_ssfragconvs tyi = 21 let 22 open ThyDataSexp 23 fun apply_extra s tyi = 24 case s of 25 List [Sym tag, String str, Thm th] => 26 if tag = simpfrag.simpfrag_conv_tag then 27 case simpfrag.lookup_simpfrag_conv str of 28 SOME f => SOME (TypeBasePure.add_ssfrag_convs [f th] tyi) 29 | NONE => (HOL_WARNING "TypeBase" "resolve_ssfragconvs" 30 ("No function "^str^" registered"); 31 NONE) 32 else NONE 33 | _ => NONE 34 fun apply_all unapplied extras tyi = 35 case extras of 36 [] => TypeBasePure.put_extra (List.rev unapplied) tyi 37 | e::es => (case apply_extra e tyi of 38 SOME tyi' => apply_all unapplied es tyi' 39 | NONE => apply_all (e::unapplied) es tyi) 40 in 41 apply_all [] (TypeBasePure.extra_of tyi) tyi 42 end 43 44(* tyinfos lacking the "standard simplifications" have those added here. *) 45fun maybe_add_simpls tyi = 46 let 47 open boolSyntax 48 val cc = case_const_of tyi 49 val rwts = #rewrs (simpls_of tyi) |> map Drule.CONJUNCTS |> List.concat 50 |> map (#2 o strip_forall o concl) 51 fun iscasedef t = 52 same_const cc (t |> lhs |> strip_comb |> #1) handle HOL_ERR _ => false 53 in 54 if List.exists iscasedef rwts then tyi else add_std_simpls tyi 55 end handle HOL_ERR _ => tyi 56 57fun tweak_tyi tyi = tyi |> maybe_add_simpls |> resolve_ssfragconvs 58 59(* ---------------------------------------------------------------------- 60 Initial value of the database 61 ---------------------------------------------------------------------- *) 62 63val bool_info = 64 TypeBasePure.mk_datatype_info 65 {ax=ORIG boolTheory.boolAxiom, 66 induction = ORIG boolTheory.bool_INDUCT, 67 case_def = boolTheory.bool_case_thm, 68 case_eq = 69 Prim_rec.prove_case_eq_thm{ 70 case_def = boolTheory.bool_case_thm, 71 nchotomy = boolTheory.BOOL_CASES_AX 72 }, 73 case_cong = boolTheory.COND_CONG, 74 distinct = SOME (CONJUNCT1 boolTheory.BOOL_EQ_DISTINCT), 75 nchotomy = boolTheory.BOOL_CASES_AX, 76 fields = [], accessors = [], updates = [], one_one = NONE, 77 recognizers=[], destructors = [], 78 size = NONE, encode = NONE, lift = NONE} |> tweak_tyi 79 80(* and similarly for the itself type constructor *) 81val [itself_info0] = let 82 open boolTheory 83in 84 TypeBasePure.gen_datatype_info {ax = itself_Axiom, ind = itself_induction, 85 case_defs = [itself_case_thm]} 86end 87val itself_info = tweak_tyi itself_info0 88 89(*--------------------------------------------------------------------------* 90 * Create the database. * 91 *--------------------------------------------------------------------------*) 92 93local 94 val update_fns = ref ([]:(tyinfo -> tyinfo) list) 95in 96 fun register_update_fn f = (update_fns := !update_fns @ [f]) 97 fun apply_update_fns tyi = list_compose (!update_fns) tyi 98end; 99 100fun apply_delta tyi tyb = TypeBasePure.insert tyb (tweak_tyi tyi) 101fun apply_to_global tyi tyb = 102 TypeBasePure.insert tyb (apply_update_fns $ tweak_tyi tyi) 103val initial_tydb = TypeBasePure.empty 104 |> rev_itlist apply_delta [bool_info, itself_info] 105 106val fullresult as {DB = thy_typebase, get_global_value = theTypeBase, 107 record_delta, get_deltas = thy_updates, 108 merge = merge_typebases, update_global_value, ...} = 109 let open TypeBasePure 110 in 111 AncestryData.fullmake{ 112 adinfo = {tag = "TypeBase", initial_values = [("min", initial_tydb)], 113 apply_delta = apply_delta 114 }, 115 uptodate_delta = K true, 116 sexps = { dec = fromSEXP, enc = toSEXP }, 117 globinfo = {apply_to_global = apply_to_global, 118 thy_finaliser = NONE, 119 initial_value = initial_tydb} 120 } 121 end 122 123fun write tyis = update_global_value (rev_itlist apply_to_global tyis) 124fun export tyis = (write tyis; List.app record_delta tyis) 125 126(* various ways to access the global value *) 127fun read {Thy,Tyop} = prim_get (theTypeBase()) (Thy,Tyop); 128fun fetch ty = TypeBasePure.fetch (theTypeBase()) ty; 129val elts = listItems o theTypeBase; 130 131fun print_sp_type ty = 132 let val {Thy,Tyop,Args} = dest_thy_type ty 133 in Thy ^ "$" ^ Tyop 134 end; 135 136fun valOf2 ty t opt = 137 case opt of 138 NONE => raise ERR t ("No "^t^" information for type "^print_sp_type ty) 139 | SOME x => x 140 141fun pfetch s ty = 142 case TypeBasePure.fetch (theTypeBase()) ty 143 of SOME x => x 144 | NONE => raise ERR s 145 ("unable to find "^ 146 Lib.quote (print_sp_type ty)^" in the TypeBase"); 147 148fun axiom_of ty = TypeBasePure.axiom_of (pfetch "axiom_of" ty) 149fun induction_of ty = TypeBasePure.induction_of (pfetch "induction_of" ty) 150fun constructors_of ty = TypeBasePure.constructors_of (pfetch "constructors_of" ty) 151fun destructors_of ty = TypeBasePure.destructors_of (pfetch "destructors_of" ty) 152fun recognizers_of ty = TypeBasePure.recognizers_of (pfetch "recognizers_of" ty) 153fun case_const_of ty = TypeBasePure.case_const_of (pfetch "case_const_of" ty) 154fun case_cong_of ty = TypeBasePure.case_cong_of (pfetch "case_cong_of" ty) 155fun case_def_of ty = TypeBasePure.case_def_of (pfetch "case_def_of" ty) 156fun case_eq_of ty = TypeBasePure.case_eq_of (pfetch "case_eq_of" ty) 157fun nchotomy_of ty = TypeBasePure.nchotomy_of (pfetch "nchotomy_of" ty) 158fun fields_of ty = TypeBasePure.fields_of (pfetch "fields_of" ty) 159fun accessors_of ty = TypeBasePure.accessors_of (pfetch "accessors_of" ty) 160fun updates_of ty = TypeBasePure.updates_of (pfetch "updates_of" ty) 161fun simpls_of ty = TypeBasePure.simpls_of (pfetch "simpls_of" ty) 162fun axiom_of0 ty = TypeBasePure.axiom_of0 (pfetch "axiom_of" ty) 163fun induction_of0 ty = TypeBasePure.induction_of0 (pfetch "induction_of0" ty) 164 165fun distinct_of ty = valOf2 ty "distinct_of" 166 (TypeBasePure.distinct_of (pfetch "distinct_of" ty)) 167fun one_one_of ty = valOf2 ty "one_one_of" 168 (TypeBasePure.one_one_of (pfetch "one_one_of" ty)) 169fun size_of0 ty = TypeBasePure.size_of0 (pfetch "size_of0" ty) 170fun encode_of0 ty = TypeBasePure.encode_of0 (pfetch "encode_of0" ty) 171fun size_of ty = valOf2 ty "size_of" 172 (TypeBasePure.size_of (pfetch "size_of" ty)) 173fun encode_of ty = valOf2 ty "encode_of" 174 (TypeBasePure.encode_of (pfetch "encode_of" ty)) 175 176 177 178 179fun tyi_from_name s = 180 let 181 open type_grammar 182 fun tyi_from_kid thy nm = 183 case Type.op_arity{Tyop=nm,Thy=thy} of 184 NONE => raise ERR "tyi_from_name" ("No such type: "^thy^"$"^nm) 185 | SOME i => 186 let 187 val st = TYOP {Args = List.tabulate(i, PARAM), Thy = thy, Tyop = nm} 188 in 189 case fetch (structure_to_type st) of 190 NONE => raise ERR "tyi_from_name" ("No tyinfo for "^thy^"$"^nm) 191 | SOME tyi => tyi 192 end 193 in 194 case String.fields (equal #"$") s of 195 [nm] => 196 let 197 val tyg = Parse.type_grammar() 198 in 199 case Binarymap.peek(privileged_abbrevs tyg, nm) of 200 NONE => raise ERR "tyi_from_name" 201 ("Ty-grammar doesn't know name: "^nm) 202 | SOME thy => 203 (case Binarymap.peek(parse_map tyg, {Thy = thy, Name = nm}) of 204 NONE => raise ERR "tyi_from_name" 205 ("Ty-grammar has bad abbrev-map for name: "^nm) 206 | SOME (TYOP {Thy,Tyop,...}) => tyi_from_kid Thy Tyop) 207 end 208 | [thy,nm] => tyi_from_kid thy nm 209 | _ => raise ERR "tyi_from_name" ("Malformed tyname: "^s) 210 end 211 212val CaseEq = TypeBasePure.case_eq_of o tyi_from_name 213val CaseEqs = Drule.LIST_CONJ o map CaseEq 214fun AllCaseEqs() = 215 let 216 fun foldthis(ty, tyi, acc) = 217 case Lib.total TypeBasePure.case_eq_of tyi of 218 NONE => acc 219 | SOME th => if aconv (concl acc) boolSyntax.T then th 220 else CONJ th acc 221 in 222 TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase()) 223 end 224 225(* ---------------------------------------------------------------------- * 226 * Install case transformation function for parser * 227 * ---------------------------------------------------------------------- *) 228 229val _ = 230 let fun lookup s = 231 case read s 232 of SOME tyi => SOME {constructors = TypeBasePure.constructors_of tyi, 233 case_const = TypeBasePure.case_const_of tyi} 234 | NONE => NONE 235 open GrammarSpecials 236 in 237 set_case_specials ((fn t => #functional (Pmatch.mk_functional lookup t)), 238 (fn s => 239 case lookup s of 240 NONE => [] 241 | SOME {constructors,...} => constructors)) 242 end 243 244(*---------------------------------------------------------------------------*) 245(* Is a term a constructor for some datatype. *) 246(*---------------------------------------------------------------------------*) 247 248fun is_constructor x = TypeBasePure.is_constructor (theTypeBase()) x; 249 250(*---------------------------------------------------------------------------*) 251(* Syntax operations on case expressions *) 252(*---------------------------------------------------------------------------*) 253 254fun mk_case x = TypeBasePure.mk_case (theTypeBase()) x 255fun dest_case x = TypeBasePure.dest_case (theTypeBase()) x 256fun is_case x = TypeBasePure.is_case (theTypeBase()) x; 257fun strip_case x = TypeBasePure.strip_case (theTypeBase()) x 258 259fun mk_pattern_fn css = 260 let 261 val pmthry = TypeBasePure.toPmatchThry (theTypeBase ()) 262 in 263 Pmatch.mk_pattern_fn pmthry css 264 end 265 266(*---------------------------------------------------------------------------*) 267(* Syntax operations on records *) 268(*---------------------------------------------------------------------------*) 269 270fun mk_record x = TypeBasePure.mk_record (theTypeBase()) x 271fun dest_record x = TypeBasePure.dest_record (theTypeBase()) x 272fun is_record x = TypeBasePure.is_record (theTypeBase()) x; 273 274fun dest_record_type x = TypeBasePure.dest_record_type (theTypeBase()) x; 275fun is_record_type x = TypeBasePure.is_record_type (theTypeBase()) x; 276 277fun ty2knm ty = 278 let 279 val {Thy,Tyop,...} = dest_thy_type ty 280 in 281 {Thy = Thy, Tyop = Tyop} 282 end 283 284fun update_induction th = 285 let 286 open boolSyntax 287 val (Ps, _) = strip_forall (concl th) 288 fun upd1 knm = 289 case read knm of 290 NONE => HOL_WARNING "TypeBase" "update_induction" 291 ("No type corresponding to " ^ 292 #Thy knm ^ "$" ^ #Tyop knm ^ " to update") 293 | SOME tyi => 294 export [TypeBasePure.put_induction (TypeBasePure.ORIG th) tyi] 295 in 296 List.app (fn v => v |> type_of |> dom_rng |> #1 |> ty2knm |> upd1) Ps 297 end 298 299fun update_axiom th = 300 let 301 open boolSyntax 302 val (_, b) = strip_forall (concl th) 303 val (exvs, _) = strip_exists b 304 fun upd1 knm = 305 case read knm of 306 NONE => HOL_WARNING "TypeBase" "update_axiom" 307 ("No type corresponding to " ^ 308 #Thy knm ^ "$" ^ #Tyop knm ^ " to update") 309 | SOME tyi => 310 export [TypeBasePure.put_axiom (TypeBasePure.ORIG th) tyi] 311 in 312 List.app (fn v => v |> type_of |> dom_rng |> #1 |> ty2knm |> upd1) exvs 313 end 314 315(* ---------------------------------------------------------------------- 316 Initialise the case-split munger in the pretty-printer 317 ---------------------------------------------------------------------- *) 318 319(* 320 This is broken because it can re-order rows in the case expression in a semantically significant way 321local 322 fun group_by f = 323 let 324 fun i x [] = [[x]] 325 | i x (y::ys) = 326 if f x (hd y) 327 then ((x::y)::ys) 328 else y::(i x ys) 329 fun g acc [] = acc 330 | g acc (x::xs) = 331 g (i x acc) xs 332 in 333 g [] 334 end 335 fun aconv_snd x y = aconv (snd x) (snd y) 336 fun max x y = if x < y then y else x 337 fun lengths [] n acc = (n,acc) 338 | lengths (l::ls) n acc = 339 let 340 val m = length l 341 in 342 lengths ls (max n m) ((m,l)::acc) 343 end 344in 345 fun pp_strip_case tm = 346 let 347 val (split_on, splits) = strip_case tm 348 val reduced_splits = 349 let 350 val groups = group_by aconv_snd splits 351 (* groups are in order, but each group is reversed *) 352 val (maxl,lgs) = lengths groups 0 [] 353 (* lgs are now reversed *) 354 in 355 case total (pluck (equal maxl o fst)) lgs of 356 SOME ((_,(p,v)::_),lgs) => 357 rev ((mk_var("_",type_of p),v)::flatten (map snd lgs)) 358 | _ => splits 359 end 360 in 361 (split_on, reduced_splits) 362 end 363end 364*) 365 366(* Less ambitious version, which only fires if all (>1) but one row have 367 the same right-hand-side and it doesn't depend on any pattern variables. 368 369 NOTE: This is also broken, since 370 ``case x of 0n => T | 2 => T | _ => F`` 371 is printed as 372 ``case x of v => F | _ => T`` 373 374local 375 fun disjoint x = HOLset.isEmpty (HOLset.intersection x) 376 fun FV tm = FVL [tm] empty_varset 377in 378 fun pp_strip_case tm = 379 let 380 val (split_on, splits) = strip_case tm 381 fun sole_exception (p,v) = 382 let 383 val (l1,l2) = partition (aconv v o snd) splits 384 val v_rest = snd (hd l2) 385 fun good (p,v) = aconv v_rest v andalso disjoint (FV p, FV v) 386 in 387 if length l1 = 1 andalso all good l2 388 then (hd l1, v_rest) 389 else raise Match 390 end 391 val reduced_splits = 392 case splits of 393 [] => splits 394 | [_] => splits 395 | [_,_] => splits 396 | _ => 397 let 398 val (u as (p,_),v_rest) = tryfind sole_exception splits 399 in 400 [u,(mk_var("_",type_of p),v_rest)] 401 end 402 handle HOL_ERR _ => splits 403 in 404 (split_on, reduced_splits) 405 end 406end 407*) 408 409val _ = term_pp.init_casesplit_munger strip_case 410 411end 412