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