|
1 (* Title: HOL/hologic.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson and Markus Wenzel |
|
4 |
|
5 Abstract syntax operations for HOL. |
|
6 *) |
|
7 |
|
8 signature HOLOGIC = |
|
9 sig |
|
10 val typeS: sort |
|
11 val typeT: typ |
|
12 val boolN: string |
|
13 val boolT: typ |
|
14 val true_const: term |
|
15 val false_const: term |
|
16 val mk_setT: typ -> typ |
|
17 val dest_setT: typ -> typ |
|
18 val Trueprop: term |
|
19 val mk_Trueprop: term -> term |
|
20 val dest_Trueprop: term -> term |
|
21 val conj_intr: thm -> thm -> thm |
|
22 val conj_elim: thm -> thm * thm |
|
23 val conj_elims: thm -> thm list |
|
24 val conj: term |
|
25 val disj: term |
|
26 val imp: term |
|
27 val Not: term |
|
28 val mk_conj: term * term -> term |
|
29 val mk_disj: term * term -> term |
|
30 val mk_imp: term * term -> term |
|
31 val mk_not: term -> term |
|
32 val dest_conj: term -> term list |
|
33 val dest_disj: term -> term list |
|
34 val disjuncts: term -> term list |
|
35 val dest_imp: term -> term * term |
|
36 val dest_not: term -> term |
|
37 val eq_const: typ -> term |
|
38 val mk_eq: term * term -> term |
|
39 val dest_eq: term -> term * term |
|
40 val all_const: typ -> term |
|
41 val mk_all: string * typ * term -> term |
|
42 val list_all: (string * typ) list * term -> term |
|
43 val exists_const: typ -> term |
|
44 val mk_exists: string * typ * term -> term |
|
45 val choice_const: typ -> term |
|
46 val Collect_const: typ -> term |
|
47 val mk_Collect: string * typ * term -> term |
|
48 val class_eq: string |
|
49 val mk_mem: term * term -> term |
|
50 val dest_mem: term -> term * term |
|
51 val mk_UNIV: typ -> term |
|
52 val mk_binop: string -> term * term -> term |
|
53 val mk_binrel: string -> term * term -> term |
|
54 val dest_bin: string -> typ -> term -> term * term |
|
55 val unitT: typ |
|
56 val is_unitT: typ -> bool |
|
57 val unit: term |
|
58 val is_unit: term -> bool |
|
59 val mk_prodT: typ * typ -> typ |
|
60 val dest_prodT: typ -> typ * typ |
|
61 val pair_const: typ -> typ -> term |
|
62 val mk_prod: term * term -> term |
|
63 val dest_prod: term -> term * term |
|
64 val mk_fst: term -> term |
|
65 val mk_snd: term -> term |
|
66 val split_const: typ * typ * typ -> term |
|
67 val mk_split: term -> term |
|
68 val prodT_factors: typ -> typ list |
|
69 val mk_tuple: typ -> term list -> term |
|
70 val dest_tuple: term -> term list |
|
71 val ap_split: typ -> typ -> term -> term |
|
72 val prod_factors: term -> int list list |
|
73 val dest_tuple': int list list -> term -> term list |
|
74 val prodT_factors': int list list -> typ -> typ list |
|
75 val ap_split': int list list -> typ -> typ -> term -> term |
|
76 val mk_tuple': int list list -> typ -> term list -> term |
|
77 val mk_tupleT: int list list -> typ list -> typ |
|
78 val strip_split: term -> term * typ list * int list list |
|
79 val natT: typ |
|
80 val zero: term |
|
81 val is_zero: term -> bool |
|
82 val mk_Suc: term -> term |
|
83 val dest_Suc: term -> term |
|
84 val Suc_zero: term |
|
85 val mk_nat: int -> term |
|
86 val dest_nat: term -> int |
|
87 val class_size: string |
|
88 val size_const: typ -> term |
|
89 val indexT: typ |
|
90 val intT: typ |
|
91 val pls_const: term |
|
92 val min_const: term |
|
93 val bit0_const: term |
|
94 val bit1_const: term |
|
95 val mk_bit: int -> term |
|
96 val dest_bit: term -> int |
|
97 val mk_numeral: int -> term |
|
98 val dest_numeral: term -> int |
|
99 val number_of_const: typ -> term |
|
100 val add_numerals: term -> (term * typ) list -> (term * typ) list |
|
101 val mk_number: typ -> int -> term |
|
102 val dest_number: term -> typ * int |
|
103 val realT: typ |
|
104 val nibbleT: typ |
|
105 val mk_nibble: int -> term |
|
106 val dest_nibble: term -> int |
|
107 val charT: typ |
|
108 val mk_char: int -> term |
|
109 val dest_char: term -> int |
|
110 val listT: typ -> typ |
|
111 val nil_const: typ -> term |
|
112 val cons_const: typ -> term |
|
113 val mk_list: typ -> term list -> term |
|
114 val dest_list: term -> term list |
|
115 val stringT: typ |
|
116 val mk_string: string -> term |
|
117 val dest_string: term -> string |
|
118 end; |
|
119 |
|
120 structure HOLogic: HOLOGIC = |
|
121 struct |
|
122 |
|
123 (* HOL syntax *) |
|
124 |
|
125 val typeS: sort = ["HOL.type"]; |
|
126 val typeT = TypeInfer.anyT typeS; |
|
127 |
|
128 |
|
129 (* bool and set *) |
|
130 |
|
131 val boolN = "bool"; |
|
132 val boolT = Type (boolN, []); |
|
133 |
|
134 val true_const = Const ("True", boolT); |
|
135 val false_const = Const ("False", boolT); |
|
136 |
|
137 fun mk_setT T = T --> boolT; |
|
138 |
|
139 fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T |
|
140 | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []); |
|
141 |
|
142 |
|
143 (* logic *) |
|
144 |
|
145 val Trueprop = Const ("Trueprop", boolT --> propT); |
|
146 |
|
147 fun mk_Trueprop P = Trueprop $ P; |
|
148 |
|
149 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
|
150 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
|
151 |
|
152 fun conj_intr thP thQ = |
|
153 let |
|
154 val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ) |
|
155 handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); |
|
156 val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); |
|
157 in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; |
|
158 |
|
159 fun conj_elim thPQ = |
|
160 let |
|
161 val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ)) |
|
162 handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]); |
|
163 val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); |
|
164 val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ; |
|
165 val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ; |
|
166 in (thP, thQ) end; |
|
167 |
|
168 fun conj_elims th = |
|
169 let val (th1, th2) = conj_elim th |
|
170 in conj_elims th1 @ conj_elims th2 end handle THM _ => [th]; |
|
171 |
|
172 val conj = @{term "op &"} |
|
173 and disj = @{term "op |"} |
|
174 and imp = @{term "op -->"} |
|
175 and Not = @{term "Not"}; |
|
176 |
|
177 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
|
178 and mk_disj (t1, t2) = disj $ t1 $ t2 |
|
179 and mk_imp (t1, t2) = imp $ t1 $ t2 |
|
180 and mk_not t = Not $ t; |
|
181 |
|
182 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t' |
|
183 | dest_conj t = [t]; |
|
184 |
|
185 fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t' |
|
186 | dest_disj t = [t]; |
|
187 |
|
188 (*Like dest_disj, but flattens disjunctions however nested*) |
|
189 fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs) |
|
190 | disjuncts_aux t disjs = t::disjs; |
|
191 |
|
192 fun disjuncts t = disjuncts_aux t []; |
|
193 |
|
194 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) |
|
195 | dest_imp t = raise TERM ("dest_imp", [t]); |
|
196 |
|
197 fun dest_not (Const ("Not", _) $ t) = t |
|
198 | dest_not t = raise TERM ("dest_not", [t]); |
|
199 |
|
200 fun eq_const T = Const ("op =", [T, T] ---> boolT); |
|
201 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
|
202 |
|
203 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs) |
|
204 | dest_eq t = raise TERM ("dest_eq", [t]) |
|
205 |
|
206 fun all_const T = Const ("All", [T --> boolT] ---> boolT); |
|
207 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P); |
|
208 fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t; |
|
209 |
|
210 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT); |
|
211 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P); |
|
212 |
|
213 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T); |
|
214 |
|
215 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T); |
|
216 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t); |
|
217 |
|
218 val class_eq = "HOL.eq"; |
|
219 |
|
220 fun mk_mem (x, A) = |
|
221 let val setT = fastype_of A in |
|
222 Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A |
|
223 end; |
|
224 |
|
225 fun dest_mem (Const ("op :", _) $ x $ A) = (x, A) |
|
226 | dest_mem t = raise TERM ("dest_mem", [t]); |
|
227 |
|
228 fun mk_UNIV T = Const ("UNIV", mk_setT T); |
|
229 |
|
230 |
|
231 (* binary operations and relations *) |
|
232 |
|
233 fun mk_binop c (t, u) = |
|
234 let val T = fastype_of t in |
|
235 Const (c, [T, T] ---> T) $ t $ u |
|
236 end; |
|
237 |
|
238 fun mk_binrel c (t, u) = |
|
239 let val T = fastype_of t in |
|
240 Const (c, [T, T] ---> boolT) $ t $ u |
|
241 end; |
|
242 |
|
243 (*destruct the application of a binary operator. The dummyT case is a crude |
|
244 way of handling polymorphic operators.*) |
|
245 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = |
|
246 if c = c' andalso (T=T' orelse T=dummyT) then (t, u) |
|
247 else raise TERM ("dest_bin " ^ c, [tm]) |
|
248 | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); |
|
249 |
|
250 |
|
251 (* unit *) |
|
252 |
|
253 val unitT = Type ("Product_Type.unit", []); |
|
254 |
|
255 fun is_unitT (Type ("Product_Type.unit", [])) = true |
|
256 | is_unitT _ = false; |
|
257 |
|
258 val unit = Const ("Product_Type.Unity", unitT); |
|
259 |
|
260 fun is_unit (Const ("Product_Type.Unity", _)) = true |
|
261 | is_unit _ = false; |
|
262 |
|
263 |
|
264 (* prod *) |
|
265 |
|
266 fun mk_prodT (T1, T2) = Type ("*", [T1, T2]); |
|
267 |
|
268 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2) |
|
269 | dest_prodT T = raise TYPE ("dest_prodT", [T], []); |
|
270 |
|
271 fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2)); |
|
272 |
|
273 fun mk_prod (t1, t2) = |
|
274 let val T1 = fastype_of t1 and T2 = fastype_of t2 in |
|
275 pair_const T1 T2 $ t1 $ t2 |
|
276 end; |
|
277 |
|
278 fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2) |
|
279 | dest_prod t = raise TERM ("dest_prod", [t]); |
|
280 |
|
281 fun mk_fst p = |
|
282 let val pT = fastype_of p in |
|
283 Const ("fst", pT --> fst (dest_prodT pT)) $ p |
|
284 end; |
|
285 |
|
286 fun mk_snd p = |
|
287 let val pT = fastype_of p in |
|
288 Const ("snd", pT --> snd (dest_prodT pT)) $ p |
|
289 end; |
|
290 |
|
291 fun split_const (A, B, C) = |
|
292 Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C); |
|
293 |
|
294 fun mk_split t = |
|
295 (case Term.fastype_of t of |
|
296 T as (Type ("fun", [A, Type ("fun", [B, C])])) => |
|
297 Const ("split", T --> mk_prodT (A, B) --> C) $ t |
|
298 | _ => raise TERM ("mk_split: bad body type", [t])); |
|
299 |
|
300 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) |
|
301 fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2 |
|
302 | prodT_factors T = [T]; |
|
303 |
|
304 (*Makes a nested tuple from a list, following the product type structure*) |
|
305 fun mk_tuple (Type ("*", [T1, T2])) tms = |
|
306 mk_prod (mk_tuple T1 tms, |
|
307 mk_tuple T2 (Library.drop (length (prodT_factors T1), tms))) |
|
308 | mk_tuple T (t::_) = t; |
|
309 |
|
310 fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u |
|
311 | dest_tuple t = [t]; |
|
312 |
|
313 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
|
314 with result type T. The call creates a new term expecting one argument |
|
315 of type S.*) |
|
316 fun ap_split T T3 u = |
|
317 let |
|
318 fun ap (T :: Ts) = |
|
319 (case T of |
|
320 Type ("*", [T1, T2]) => |
|
321 split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts) |
|
322 | _ => Abs ("x", T, ap Ts)) |
|
323 | ap [] = |
|
324 let val k = length (prodT_factors T) |
|
325 in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end |
|
326 in ap [T] end; |
|
327 |
|
328 |
|
329 (* operations on tuples with specific arities *) |
|
330 (* |
|
331 an "arity" of a tuple is a list of lists of integers |
|
332 ("factors"), denoting paths to subterms that are pairs |
|
333 *) |
|
334 |
|
335 fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []); |
|
336 |
|
337 fun prod_factors t = |
|
338 let |
|
339 fun factors p (Const ("Pair", _) $ t $ u) = |
|
340 p :: factors (1::p) t @ factors (2::p) u |
|
341 | factors p _ = [] |
|
342 in factors [] t end; |
|
343 |
|
344 fun dest_tuple' ps = |
|
345 let |
|
346 fun dest p t = if p mem ps then (case t of |
|
347 Const ("Pair", _) $ t $ u => |
|
348 dest (1::p) t @ dest (2::p) u |
|
349 | _ => prod_err "dest_tuple'") else [t] |
|
350 in dest [] end; |
|
351 |
|
352 fun prodT_factors' ps = |
|
353 let |
|
354 fun factors p T = if p mem ps then (case T of |
|
355 Type ("*", [T1, T2]) => |
|
356 factors (1::p) T1 @ factors (2::p) T2 |
|
357 | _ => prod_err "prodT_factors'") else [T] |
|
358 in factors [] end; |
|
359 |
|
360 (*In ap_split' ps S T u, term u expects separate arguments for the factors of S, |
|
361 with result type T. The call creates a new term expecting one argument |
|
362 of type S.*) |
|
363 fun ap_split' ps T T3 u = |
|
364 let |
|
365 fun ap ((p, T) :: pTs) = |
|
366 if p mem ps then (case T of |
|
367 Type ("*", [T1, T2]) => |
|
368 split_const (T1, T2, map snd pTs ---> T3) $ |
|
369 ap ((1::p, T1) :: (2::p, T2) :: pTs) |
|
370 | _ => prod_err "ap_split'") |
|
371 else Abs ("x", T, ap pTs) |
|
372 | ap [] = |
|
373 let val k = length ps |
|
374 in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end |
|
375 in ap [([], T)] end; |
|
376 |
|
377 fun mk_tuple' ps = |
|
378 let |
|
379 fun mk p T ts = |
|
380 if p mem ps then (case T of |
|
381 Type ("*", [T1, T2]) => |
|
382 let |
|
383 val (t, ts') = mk (1::p) T1 ts; |
|
384 val (u, ts'') = mk (2::p) T2 ts' |
|
385 in (pair_const T1 T2 $ t $ u, ts'') end |
|
386 | _ => prod_err "mk_tuple'") |
|
387 else (hd ts, tl ts) |
|
388 in fst oo mk [] end; |
|
389 |
|
390 fun mk_tupleT ps = |
|
391 let |
|
392 fun mk p Ts = |
|
393 if p mem ps then |
|
394 let |
|
395 val (T, Ts') = mk (1::p) Ts; |
|
396 val (U, Ts'') = mk (2::p) Ts' |
|
397 in (mk_prodT (T, U), Ts'') end |
|
398 else (hd Ts, tl Ts) |
|
399 in fst o mk [] end; |
|
400 |
|
401 fun strip_split t = |
|
402 let |
|
403 fun strip [] qs Ts t = (t, Ts, qs) |
|
404 | strip (p :: ps) qs Ts (Const ("split", _) $ t) = |
|
405 strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t |
|
406 | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t |
|
407 | strip (p :: ps) qs Ts t = strip ps qs |
|
408 (hd (binder_types (fastype_of1 (Ts, t))) :: Ts) |
|
409 (incr_boundvars 1 t $ Bound 0) |
|
410 in strip [[]] [] [] t end; |
|
411 |
|
412 |
|
413 (* nat *) |
|
414 |
|
415 val natT = Type ("nat", []); |
|
416 |
|
417 val zero = Const ("HOL.zero_class.zero", natT); |
|
418 |
|
419 fun is_zero (Const ("HOL.zero_class.zero", _)) = true |
|
420 | is_zero _ = false; |
|
421 |
|
422 fun mk_Suc t = Const ("Suc", natT --> natT) $ t; |
|
423 |
|
424 fun dest_Suc (Const ("Suc", _) $ t) = t |
|
425 | dest_Suc t = raise TERM ("dest_Suc", [t]); |
|
426 |
|
427 val Suc_zero = mk_Suc zero; |
|
428 |
|
429 fun mk_nat n = |
|
430 let |
|
431 fun mk 0 = zero |
|
432 | mk n = mk_Suc (mk (n - 1)); |
|
433 in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end; |
|
434 |
|
435 fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0 |
|
436 | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1 |
|
437 | dest_nat t = raise TERM ("dest_nat", [t]); |
|
438 |
|
439 val class_size = "Nat.size"; |
|
440 |
|
441 fun size_const T = Const ("Nat.size_class.size", T --> natT); |
|
442 |
|
443 |
|
444 (* index *) |
|
445 |
|
446 val indexT = Type ("Code_Index.index", []); |
|
447 |
|
448 |
|
449 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *) |
|
450 |
|
451 val intT = Type ("Int.int", []); |
|
452 |
|
453 val pls_const = Const ("Int.Pls", intT) |
|
454 and min_const = Const ("Int.Min", intT) |
|
455 and bit0_const = Const ("Int.Bit0", intT --> intT) |
|
456 and bit1_const = Const ("Int.Bit1", intT --> intT); |
|
457 |
|
458 fun mk_bit 0 = bit0_const |
|
459 | mk_bit 1 = bit1_const |
|
460 | mk_bit _ = raise TERM ("mk_bit", []); |
|
461 |
|
462 fun dest_bit (Const ("Int.Bit0", _)) = 0 |
|
463 | dest_bit (Const ("Int.Bit1", _)) = 1 |
|
464 | dest_bit t = raise TERM ("dest_bit", [t]); |
|
465 |
|
466 fun mk_numeral 0 = pls_const |
|
467 | mk_numeral ~1 = min_const |
|
468 | mk_numeral i = |
|
469 let val (q, r) = Integer.div_mod i 2; |
|
470 in mk_bit r $ mk_numeral q end; |
|
471 |
|
472 fun dest_numeral (Const ("Int.Pls", _)) = 0 |
|
473 | dest_numeral (Const ("Int.Min", _)) = ~1 |
|
474 | dest_numeral (Const ("Int.Bit0", _) $ bs) = 2 * dest_numeral bs |
|
475 | dest_numeral (Const ("Int.Bit1", _) $ bs) = 2 * dest_numeral bs + 1 |
|
476 | dest_numeral t = raise TERM ("dest_numeral", [t]); |
|
477 |
|
478 fun number_of_const T = Const ("Int.number_class.number_of", intT --> T); |
|
479 |
|
480 fun add_numerals (Const ("Int.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T) |
|
481 | add_numerals (t $ u) = add_numerals t #> add_numerals u |
|
482 | add_numerals (Abs (_, _, t)) = add_numerals t |
|
483 | add_numerals _ = I; |
|
484 |
|
485 fun mk_number T 0 = Const ("HOL.zero_class.zero", T) |
|
486 | mk_number T 1 = Const ("HOL.one_class.one", T) |
|
487 | mk_number T i = number_of_const T $ mk_numeral i; |
|
488 |
|
489 fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0) |
|
490 | dest_number (Const ("HOL.one_class.one", T)) = (T, 1) |
|
491 | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) = |
|
492 (T, dest_numeral t) |
|
493 | dest_number t = raise TERM ("dest_number", [t]); |
|
494 |
|
495 |
|
496 (* real *) |
|
497 |
|
498 val realT = Type ("RealDef.real", []); |
|
499 |
|
500 |
|
501 (* nibble *) |
|
502 |
|
503 val nibbleT = Type ("List.nibble", []); |
|
504 |
|
505 fun mk_nibble n = |
|
506 let val s = |
|
507 if 0 <= n andalso n <= 9 then chr (n + ord "0") |
|
508 else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10) |
|
509 else raise TERM ("mk_nibble", []) |
|
510 in Const ("List.nibble.Nibble" ^ s, nibbleT) end; |
|
511 |
|
512 fun dest_nibble t = |
|
513 let fun err () = raise TERM ("dest_nibble", [t]) in |
|
514 (case try (unprefix "List.nibble.Nibble" o fst o Term.dest_Const) t of |
|
515 NONE => err () |
|
516 | SOME c => |
|
517 if size c <> 1 then err () |
|
518 else if "0" <= c andalso c <= "9" then ord c - ord "0" |
|
519 else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10 |
|
520 else err ()) |
|
521 end; |
|
522 |
|
523 |
|
524 (* char *) |
|
525 |
|
526 val charT = Type ("List.char", []); |
|
527 |
|
528 fun mk_char n = |
|
529 if 0 <= n andalso n <= 255 then |
|
530 Const ("List.char.Char", nibbleT --> nibbleT --> charT) $ |
|
531 mk_nibble (n div 16) $ mk_nibble (n mod 16) |
|
532 else raise TERM ("mk_char", []); |
|
533 |
|
534 fun dest_char (Const ("List.char.Char", _) $ t $ u) = |
|
535 dest_nibble t * 16 + dest_nibble u |
|
536 | dest_char t = raise TERM ("dest_char", [t]); |
|
537 |
|
538 |
|
539 (* list *) |
|
540 |
|
541 fun listT T = Type ("List.list", [T]); |
|
542 |
|
543 fun nil_const T = Const ("List.list.Nil", listT T); |
|
544 |
|
545 fun cons_const T = |
|
546 let val lT = listT T |
|
547 in Const ("List.list.Cons", T --> lT --> lT) end; |
|
548 |
|
549 fun mk_list T ts = |
|
550 let |
|
551 val lT = listT T; |
|
552 val Nil = Const ("List.list.Nil", lT); |
|
553 fun Cons t u = Const ("List.list.Cons", T --> lT --> lT) $ t $ u; |
|
554 in fold_rev Cons ts Nil end; |
|
555 |
|
556 fun dest_list (Const ("List.list.Nil", _)) = [] |
|
557 | dest_list (Const ("List.list.Cons", _) $ t $ u) = t :: dest_list u |
|
558 | dest_list t = raise TERM ("dest_list", [t]); |
|
559 |
|
560 |
|
561 (* string *) |
|
562 |
|
563 val stringT = Type ("List.string", []); |
|
564 |
|
565 val mk_string = mk_list charT o map (mk_char o ord) o explode; |
|
566 val dest_string = implode o map (chr o dest_char) o dest_list; |
|
567 |
|
568 end; |