1(* Title: HOL/Tools/hologic.ML 2 Author: Lawrence C Paulson and Markus Wenzel 3 4Abstract syntax operations for HOL. 5*) 6 7signature HOLOGIC = 8sig 9 val id_const: typ -> term 10 val mk_comp: term * term -> term 11 val boolN: string 12 val boolT: typ 13 val mk_obj_eq: thm -> thm 14 val Trueprop: term 15 val mk_Trueprop: term -> term 16 val dest_Trueprop: term -> term 17 val Trueprop_conv: conv -> conv 18 val mk_induct_forall: typ -> term 19 val mk_setT: typ -> typ 20 val dest_setT: typ -> typ 21 val Collect_const: typ -> term 22 val mk_Collect: string * typ * term -> term 23 val mk_mem: term * term -> term 24 val dest_mem: term -> term * term 25 val mk_set: typ -> term list -> term 26 val dest_set: term -> term list 27 val mk_UNIV: typ -> term 28 val conj_intr: Proof.context -> thm -> thm -> thm 29 val conj_elim: Proof.context -> thm -> thm * thm 30 val conj_elims: Proof.context -> thm -> thm list 31 val conj: term 32 val disj: term 33 val imp: term 34 val Not: term 35 val mk_conj: term * term -> term 36 val mk_disj: term * term -> term 37 val mk_imp: term * term -> term 38 val mk_not: term -> term 39 val dest_conj: term -> term list 40 val conjuncts: term -> term list 41 val dest_disj: term -> term list 42 val disjuncts: term -> term list 43 val dest_imp: term -> term * term 44 val dest_not: term -> term 45 val conj_conv: conv -> conv -> conv 46 val eq_const: typ -> term 47 val mk_eq: term * term -> term 48 val dest_eq: term -> term * term 49 val eq_conv: conv -> conv -> conv 50 val all_const: typ -> term 51 val mk_all: string * typ * term -> term 52 val list_all: (string * typ) list * term -> term 53 val exists_const: typ -> term 54 val mk_exists: string * typ * term -> term 55 val choice_const: typ -> term 56 val class_equal: string 57 val mk_binop: string -> term * term -> term 58 val mk_binrel: string -> term * term -> term 59 val dest_bin: string -> typ -> term -> term * term 60 val unitT: typ 61 val is_unitT: typ -> bool 62 val unit: term 63 val is_unit: term -> bool 64 val mk_prodT: typ * typ -> typ 65 val dest_prodT: typ -> typ * typ 66 val pair_const: typ -> typ -> term 67 val mk_prod: term * term -> term 68 val dest_prod: term -> term * term 69 val mk_fst: term -> term 70 val mk_snd: term -> term 71 val case_prod_const: typ * typ * typ -> term 72 val mk_case_prod: term -> term 73 val flatten_tupleT: typ -> typ list 74 val tupled_lambda: term -> term -> term 75 val mk_tupleT: typ list -> typ 76 val strip_tupleT: typ -> typ list 77 val mk_tuple: term list -> term 78 val strip_tuple: term -> term list 79 val mk_ptupleT: int list list -> typ list -> typ 80 val strip_ptupleT: int list list -> typ -> typ list 81 val flat_tupleT_paths: typ -> int list list 82 val mk_ptuple: int list list -> typ -> term list -> term 83 val strip_ptuple: int list list -> term -> term list 84 val flat_tuple_paths: term -> int list list 85 val mk_ptupleabs: int list list -> typ -> typ -> term -> term 86 val strip_ptupleabs: term -> term * typ list * int list list 87 val natT: typ 88 val zero: term 89 val is_zero: term -> bool 90 val mk_Suc: term -> term 91 val dest_Suc: term -> term 92 val Suc_zero: term 93 val mk_nat: int -> term 94 val dest_nat: term -> int 95 val class_size: string 96 val size_const: typ -> term 97 val intT: typ 98 val one_const: term 99 val bit0_const: term 100 val bit1_const: term 101 val mk_numeral: int -> term 102 val dest_numeral: term -> int 103 val numeral_const: typ -> term 104 val add_numerals: term -> (term * typ) list -> (term * typ) list 105 val mk_number: typ -> int -> term 106 val dest_number: term -> typ * int 107 val code_integerT: typ 108 val code_naturalT: typ 109 val realT: typ 110 val charT: typ 111 val mk_char: int -> term 112 val dest_char: term -> int 113 val listT: typ -> typ 114 val nil_const: typ -> term 115 val cons_const: typ -> term 116 val mk_list: typ -> term list -> term 117 val dest_list: term -> term list 118 val stringT: typ 119 val mk_string: string -> term 120 val dest_string: term -> string 121 val literalT: typ 122 val mk_literal: string -> term 123 val dest_literal: term -> string 124 val mk_typerep: typ -> term 125 val termT: typ 126 val term_of_const: typ -> term 127 val mk_term_of: typ -> term -> term 128 val reflect_term: term -> term 129 val mk_valtermify_app: string -> (string * typ) list -> typ -> term 130 val mk_return: typ -> typ -> term -> term 131 val mk_ST: ((term * typ) * (string * typ) option) list -> term -> typ -> typ option * typ -> term 132 val mk_random: typ -> term -> term 133end; 134 135structure HOLogic: HOLOGIC = 136struct 137 138(* functions *) 139 140fun id_const T = Const ("Fun.id", T --> T); 141 142fun mk_comp (f, g) = 143 let 144 val fT = fastype_of f; 145 val gT = fastype_of g; 146 val compT = fT --> gT --> domain_type gT --> range_type fT; 147 in Const ("Fun.comp", compT) $ f $ g end; 148 149 150(* bool and set *) 151 152val boolN = "HOL.bool"; 153val boolT = Type (boolN, []); 154 155fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT); 156 157fun mk_setT T = Type ("Set.set", [T]); 158 159fun dest_setT (Type ("Set.set", [T])) = T 160 | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); 161 162fun mk_set T ts = 163 let 164 val sT = mk_setT T; 165 val empty = Const ("Orderings.bot_class.bot", sT); 166 fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u; 167 in fold_rev insert ts empty end; 168 169fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T); 170 171fun dest_set (Const ("Orderings.bot_class.bot", _)) = [] 172 | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u 173 | dest_set t = raise TERM ("dest_set", [t]); 174 175fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T); 176fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T) t; 177 178fun mk_mem (x, A) = 179 let val setT = fastype_of A in 180 Const ("Set.member", dest_setT setT --> setT --> boolT) $ x $ A 181 end; 182 183fun dest_mem (Const ("Set.member", _) $ x $ A) = (x, A) 184 | dest_mem t = raise TERM ("dest_mem", [t]); 185 186 187(* logic *) 188 189fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq}; 190 191val Trueprop = Const (\<^const_name>\<open>Trueprop\<close>, boolT --> propT); 192 193fun mk_Trueprop P = Trueprop $ P; 194 195fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P 196 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 197 198fun Trueprop_conv cv ct = 199 (case Thm.term_of ct of 200 Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => Conv.arg_conv cv ct 201 | _ => raise CTERM ("Trueprop_conv", [ct])) 202 203 204fun conj_intr ctxt thP thQ = 205 let 206 val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ) 207 handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); 208 val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); 209 in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; 210 211fun conj_elim ctxt thPQ = 212 let 213 val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ)) 214 handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]); 215 val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); 216 val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ; 217 val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ; 218 in (thP, thQ) end; 219 220fun conj_elims ctxt th = 221 let val (th1, th2) = conj_elim ctxt th 222 in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th]; 223 224val conj = \<^term>\<open>HOL.conj\<close> 225and disj = \<^term>\<open>HOL.disj\<close> 226and imp = \<^term>\<open>implies\<close> 227and Not = \<^term>\<open>Not\<close>; 228 229fun mk_conj (t1, t2) = conj $ t1 $ t2 230and mk_disj (t1, t2) = disj $ t1 $ t2 231and mk_imp (t1, t2) = imp $ t1 $ t2 232and mk_not t = Not $ t; 233 234fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t' 235 | dest_conj t = [t]; 236 237(*Like dest_conj, but flattens conjunctions however nested*) 238fun conjuncts_aux (Const ("HOL.conj", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) 239 | conjuncts_aux t conjs = t::conjs; 240 241fun conjuncts t = conjuncts_aux t []; 242 243fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t' 244 | dest_disj t = [t]; 245 246(*Like dest_disj, but flattens disjunctions however nested*) 247fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs) 248 | disjuncts_aux t disjs = t::disjs; 249 250fun disjuncts t = disjuncts_aux t []; 251 252fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B) 253 | dest_imp t = raise TERM ("dest_imp", [t]); 254 255fun dest_not (Const ("HOL.Not", _) $ t) = t 256 | dest_not t = raise TERM ("dest_not", [t]); 257 258 259fun conj_conv cv1 cv2 ct = 260 (case Thm.term_of ct of 261 Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => 262 Conv.combination_conv (Conv.arg_conv cv1) cv2 ct 263 | _ => raise CTERM ("conj_conv", [ct])); 264 265 266fun eq_const T = Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> boolT); 267 268fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; 269 270fun dest_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (lhs, rhs) 271 | dest_eq t = raise TERM ("dest_eq", [t]) 272 273fun eq_conv cv1 cv2 ct = 274 (case Thm.term_of ct of 275 Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct 276 | _ => raise CTERM ("eq_conv", [ct])); 277 278 279fun all_const T = Const ("HOL.All", (T --> boolT) --> boolT); 280fun mk_all (x, T, P) = all_const T $ absfree (x, T) P; 281fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t; 282 283fun exists_const T = Const ("HOL.Ex", (T --> boolT) --> boolT); 284fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P; 285 286fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T); 287 288val class_equal = "HOL.equal"; 289 290 291(* binary operations and relations *) 292 293fun mk_binop c (t, u) = 294 let val T = fastype_of t 295 in Const (c, T --> T --> T) $ t $ u end; 296 297fun mk_binrel c (t, u) = 298 let val T = fastype_of t 299 in Const (c, T --> T --> boolT) $ t $ u end; 300 301(*destruct the application of a binary operator. The dummyT case is a crude 302 way of handling polymorphic operators.*) 303fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = 304 if c = c' andalso (T=T' orelse T=dummyT) then (t, u) 305 else raise TERM ("dest_bin " ^ c, [tm]) 306 | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); 307 308 309(* unit *) 310 311val unitT = Type ("Product_Type.unit", []); 312 313fun is_unitT (Type ("Product_Type.unit", [])) = true 314 | is_unitT _ = false; 315 316val unit = Const ("Product_Type.Unity", unitT); 317 318fun is_unit (Const ("Product_Type.Unity", _)) = true 319 | is_unit _ = false; 320 321 322(* prod *) 323 324fun mk_prodT (T1, T2) = Type ("Product_Type.prod", [T1, T2]); 325 326fun dest_prodT (Type ("Product_Type.prod", [T1, T2])) = (T1, T2) 327 | dest_prodT T = raise TYPE ("dest_prodT", [T], []); 328 329fun pair_const T1 T2 = Const ("Product_Type.Pair", T1 --> T2 --> mk_prodT (T1, T2)); 330 331fun mk_prod (t1, t2) = 332 let val T1 = fastype_of t1 and T2 = fastype_of t2 in 333 pair_const T1 T2 $ t1 $ t2 334 end; 335 336fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2) 337 | dest_prod t = raise TERM ("dest_prod", [t]); 338 339fun mk_fst p = 340 let val pT = fastype_of p in 341 Const ("Product_Type.prod.fst", pT --> fst (dest_prodT pT)) $ p 342 end; 343 344fun mk_snd p = 345 let val pT = fastype_of p in 346 Const ("Product_Type.prod.snd", pT --> snd (dest_prodT pT)) $ p 347 end; 348 349fun case_prod_const (A, B, C) = 350 Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C); 351 352fun mk_case_prod t = 353 (case Term.fastype_of t of 354 T as (Type ("fun", [A, Type ("fun", [B, C])])) => 355 Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t 356 | _ => raise TERM ("mk_case_prod: bad body type", [t])); 357 358(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) 359fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2 360 | flatten_tupleT T = [T]; 361 362(*abstraction over nested tuples*) 363fun tupled_lambda (x as Free _) b = lambda x b 364 | tupled_lambda (x as Var _) b = lambda x b 365 | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b = 366 mk_case_prod (tupled_lambda u (tupled_lambda v b)) 367 | tupled_lambda (Const ("Product_Type.Unity", _)) b = 368 Abs ("x", unitT, b) 369 | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]); 370 371 372(* tuples with right-fold structure *) 373 374fun mk_tupleT [] = unitT 375 | mk_tupleT Ts = foldr1 mk_prodT Ts; 376 377fun strip_tupleT (Type ("Product_Type.unit", [])) = [] 378 | strip_tupleT (Type ("Product_Type.prod", [T1, T2])) = T1 :: strip_tupleT T2 379 | strip_tupleT T = [T]; 380 381fun mk_tuple [] = unit 382 | mk_tuple ts = foldr1 mk_prod ts; 383 384fun strip_tuple (Const ("Product_Type.Unity", _)) = [] 385 | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2 386 | strip_tuple t = [t]; 387 388 389(* tuples with specific arities 390 391 an "arity" of a tuple is a list of lists of integers, 392 denoting paths to subterms that are pairs 393*) 394 395fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []); 396 397fun mk_ptupleT ps = 398 let 399 fun mk p Ts = 400 if member (op =) ps p then 401 let 402 val (T, Ts') = mk (1::p) Ts; 403 val (U, Ts'') = mk (2::p) Ts' 404 in (mk_prodT (T, U), Ts'') end 405 else (hd Ts, tl Ts) 406 in fst o mk [] end; 407 408fun strip_ptupleT ps = 409 let 410 fun factors p T = if member (op =) ps p then (case T of 411 Type ("Product_Type.prod", [T1, T2]) => 412 factors (1::p) T1 @ factors (2::p) T2 413 | _ => ptuple_err "strip_ptupleT") else [T] 414 in factors [] end; 415 416val flat_tupleT_paths = 417 let 418 fun factors p (Type ("Product_Type.prod", [T1, T2])) = 419 p :: factors (1::p) T1 @ factors (2::p) T2 420 | factors p _ = [] 421 in factors [] end; 422 423fun mk_ptuple ps = 424 let 425 fun mk p T ts = 426 if member (op =) ps p then (case T of 427 Type ("Product_Type.prod", [T1, T2]) => 428 let 429 val (t, ts') = mk (1::p) T1 ts; 430 val (u, ts'') = mk (2::p) T2 ts' 431 in (pair_const T1 T2 $ t $ u, ts'') end 432 | _ => ptuple_err "mk_ptuple") 433 else (hd ts, tl ts) 434 in fst oo mk [] end; 435 436fun strip_ptuple ps = 437 let 438 fun dest p t = if member (op =) ps p then (case t of 439 Const ("Product_Type.Pair", _) $ t $ u => 440 dest (1::p) t @ dest (2::p) u 441 | _ => ptuple_err "strip_ptuple") else [t] 442 in dest [] end; 443 444val flat_tuple_paths = 445 let 446 fun factors p (Const ("Product_Type.Pair", _) $ t $ u) = 447 p :: factors (1::p) t @ factors (2::p) u 448 | factors p _ = [] 449 in factors [] end; 450 451(*In mk_ptupleabs ps S T u, term u expects separate arguments for the factors of S, 452 with result type T. The call creates a new term expecting one argument 453 of type S.*) 454fun mk_ptupleabs ps T T3 u = 455 let 456 fun ap ((p, T) :: pTs) = 457 if member (op =) ps p then (case T of 458 Type ("Product_Type.prod", [T1, T2]) => 459 case_prod_const (T1, T2, map snd pTs ---> T3) $ 460 ap ((1::p, T1) :: (2::p, T2) :: pTs) 461 | _ => ptuple_err "mk_ptupleabs") 462 else Abs ("x", T, ap pTs) 463 | ap [] = 464 let val k = length ps 465 in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end 466 in ap [([], T)] end; 467 468val strip_ptupleabs = 469 let 470 fun strip [] qs Ts t = (t, rev Ts, qs) 471 | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) = 472 strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t 473 | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t 474 | strip (p :: ps) qs Ts t = strip ps qs 475 (hd (binder_types (fastype_of1 (Ts, t))) :: Ts) 476 (incr_boundvars 1 t $ Bound 0) 477 in strip [[]] [] [] end; 478 479 480(* nat *) 481 482val natT = Type ("Nat.nat", []); 483 484val zero = Const ("Groups.zero_class.zero", natT); 485 486fun is_zero (Const ("Groups.zero_class.zero", _)) = true 487 | is_zero _ = false; 488 489fun mk_Suc t = Const ("Nat.Suc", natT --> natT) $ t; 490 491fun dest_Suc (Const ("Nat.Suc", _) $ t) = t 492 | dest_Suc t = raise TERM ("dest_Suc", [t]); 493 494val Suc_zero = mk_Suc zero; 495 496fun mk_nat n = 497 let 498 fun mk 0 = zero 499 | mk n = mk_Suc (mk (n - 1)); 500 in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end; 501 502fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0 503 | dest_nat (Const ("Nat.Suc", _) $ t) = dest_nat t + 1 504 | dest_nat t = raise TERM ("dest_nat", [t]); 505 506val class_size = "Nat.size"; 507 508fun size_const T = Const ("Nat.size_class.size", T --> natT); 509 510 511(* binary numerals and int *) 512 513val numT = Type ("Num.num", []); 514val intT = Type ("Int.int", []); 515 516val one_const = Const ("Num.num.One", numT) 517and bit0_const = Const ("Num.num.Bit0", numT --> numT) 518and bit1_const = Const ("Num.num.Bit1", numT --> numT); 519 520fun mk_numeral i = 521 let 522 fun mk 1 = one_const 523 | mk i = 524 let 525 val (q, r) = Integer.div_mod i 2 526 in (if r = 0 then bit0_const else bit1_const) $ mk q end 527 in 528 if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, []) 529 end 530 531fun dest_numeral (Const ("Num.num.One", _)) = 1 532 | dest_numeral (Const ("Num.num.Bit0", _) $ bs) = 2 * dest_numeral bs 533 | dest_numeral (Const ("Num.num.Bit1", _) $ bs) = 2 * dest_numeral bs + 1 534 | dest_numeral t = raise TERM ("dest_num", [t]); 535 536fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T); 537 538fun add_numerals (Const ("Num.numeral_class.numeral", Type (_, [_, T])) $ t) = cons (t, T) 539 | add_numerals (t $ u) = add_numerals t #> add_numerals u 540 | add_numerals (Abs (_, _, t)) = add_numerals t 541 | add_numerals _ = I; 542 543fun mk_number T 0 = Const ("Groups.zero_class.zero", T) 544 | mk_number T 1 = Const ("Groups.one_class.one", T) 545 | mk_number T i = 546 if i > 0 then numeral_const T $ mk_numeral i 547 else Const ("Groups.uminus_class.uminus", T --> T) $ mk_number T (~ i); 548 549fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0) 550 | dest_number (Const ("Groups.one_class.one", T)) = (T, 1) 551 | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) = 552 (T, dest_numeral t) 553 | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", _)) $ t) = 554 apsnd (op ~) (dest_number t) 555 | dest_number t = raise TERM ("dest_number", [t]); 556 557 558(* code target numerals *) 559 560val code_integerT = Type ("Code_Numeral.integer", []); 561 562val code_naturalT = Type ("Code_Numeral.natural", []); 563 564 565(* real *) 566 567val realT = Type ("Real.real", []); 568 569 570(* list *) 571 572fun listT T = Type ("List.list", [T]); 573 574fun nil_const T = Const ("List.list.Nil", listT T); 575 576fun cons_const T = 577 let val lT = listT T 578 in Const ("List.list.Cons", T --> lT --> lT) end; 579 580fun mk_list T ts = 581 let 582 val lT = listT T; 583 val Nil = Const ("List.list.Nil", lT); 584 fun Cons t u = Const ("List.list.Cons", T --> lT --> lT) $ t $ u; 585 in fold_rev Cons ts Nil end; 586 587fun dest_list (Const ("List.list.Nil", _)) = [] 588 | dest_list (Const ("List.list.Cons", _) $ t $ u) = t :: dest_list u 589 | dest_list t = raise TERM ("dest_list", [t]); 590 591 592(* booleans as bits *) 593 594fun mk_bit b = if b = 0 then \<^term>\<open>False\<close> 595 else if b = 1 then \<^term>\<open>True\<close> 596 else raise TERM ("mk_bit", []); 597 598fun mk_bits len = map mk_bit o Integer.radicify 2 len; 599 600fun dest_bit \<^term>\<open>False\<close> = 0 601 | dest_bit \<^term>\<open>True\<close> = 1 602 | dest_bit _ = raise TERM ("dest_bit", []); 603 604val dest_bits = Integer.eval_radix 2 o map dest_bit; 605 606 607(* char *) 608 609val charT = Type ("String.char", []); 610 611val Char_const = Const ("String.char.Char", replicate 8 boolT ---> charT); 612 613fun mk_char i = 614 if 0 <= i andalso i <= 255 615 then list_comb (Char_const, mk_bits 8 i) 616 else raise TERM ("mk_char", []) 617 618fun dest_char (Const ("String.char.Char", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ b7) = 619 dest_bits [b0, b1, b2, b3, b4, b5, b6, b7] 620 | dest_char t = raise TERM ("dest_char", [t]); 621 622 623(* string *) 624 625val stringT = listT charT; 626 627val mk_string = mk_list charT o map (mk_char o ord) o raw_explode; 628val dest_string = implode o map (chr o dest_char) o dest_list; 629 630 631(* literal *) 632 633val literalT = Type ("String.literal", []); 634 635val Literal_const = Const ("String.Literal", replicate 7 boolT ---> literalT --> literalT); 636 637fun mk_literal s = 638 let 639 fun mk [] = 640 Const ("Groups.zero_class.zero", literalT) 641 | mk (c :: cs) = 642 list_comb (Literal_const, mk_bits 7 c) $ mk cs; 643 val cs = map ord (raw_explode s); 644 in 645 if forall (fn c => c < 128) cs 646 then mk cs 647 else raise TERM ("mk_literal", []) 648 end; 649 650val dest_literal = 651 let 652 fun dest (Const ("Groups.zero_class.zero", Type ("String.literal", []))) = [] 653 | dest (Const ("String.Literal", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) = 654 chr (dest_bits [b0, b1, b2, b3, b4, b5, b6]) :: dest t 655 | dest t = raise TERM ("dest_literal", [t]); 656 in implode o dest end; 657 658 659(* typerep and term *) 660 661val typerepT = Type ("Typerep.typerep", []); 662 663fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep", 664 literalT --> listT typerepT --> typerepT) $ mk_literal tyco 665 $ mk_list typerepT (map mk_typerep Ts) 666 | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep", 667 Term.itselfT T --> typerepT) $ Logic.mk_type T; 668 669val termT = Type ("Code_Evaluation.term", []); 670 671fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT); 672 673fun mk_term_of T t = term_of_const T $ t; 674 675fun reflect_term (Const (c, T)) = 676 Const ("Code_Evaluation.Const", literalT --> typerepT --> termT) 677 $ mk_literal c $ mk_typerep T 678 | reflect_term (t1 $ t2) = 679 Const ("Code_Evaluation.App", termT --> termT --> termT) 680 $ reflect_term t1 $ reflect_term t2 681 | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t) 682 | reflect_term t = t; 683 684fun mk_valtermify_app c vs T = 685 let 686 fun termifyT T = mk_prodT (T, unitT --> termT); 687 fun valapp T T' = Const ("Code_Evaluation.valapp", 688 termifyT (T --> T') --> termifyT T --> termifyT T'); 689 fun mk_fTs [] _ = [] 690 | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T; 691 val Ts = map snd vs; 692 val t = Const (c, Ts ---> T); 693 val tt = mk_prod (t, Abs ("u", unitT, reflect_term t)); 694 fun app (fT, (v, T)) t = valapp T fT $ t $ Free (v, termifyT T); 695 in fold app (mk_fTs Ts T ~~ vs) tt end; 696 697 698(* open state monads *) 699 700fun mk_return T U x = pair_const T U $ x; 701 702fun mk_ST clauses t U (someT, V) = 703 let 704 val R = case someT of SOME T => mk_prodT (T, V) | NONE => V 705 fun mk_clause ((t, U), SOME (v, T)) (t', U') = 706 (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R) 707 $ t $ lambda (Free (v, T)) t', U) 708 | mk_clause ((t, U), NONE) (t', U') = 709 (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R) 710 $ t $ t', U) 711 in fold_rev mk_clause clauses (t, U) |> fst end; 712 713 714(* random seeds *) 715 716val random_seedT = mk_prodT (code_naturalT, code_naturalT); 717 718fun mk_random T t = Const ("Quickcheck_Random.random_class.random", code_naturalT 719 --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t; 720 721end; 722