|
1 (* Title: Pure/section-utils |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Utilities for writing new theory sections |
|
7 *) |
|
8 |
|
9 fun ap t u = t$u; |
|
10 fun app t (u1,u2) = t $ u1 $ u2; |
|
11 |
|
12 (*Make distinct individual variables a1, a2, a3, ..., an. *) |
|
13 fun mk_frees a [] = [] |
|
14 | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts; |
|
15 |
|
16 (*Make a definition lhs==rhs*) |
|
17 fun mk_defpair (lhs, rhs) = |
|
18 let val Const(name, _) = head_of lhs |
|
19 in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end; |
|
20 |
|
21 fun get_def thy s = get_axiom thy (s^"_def"); |
|
22 |
|
23 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a); |
|
24 |
|
25 |
|
26 (*Read an assumption in the given theory*) |
|
27 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT)); |
|
28 |
|
29 fun readtm sign T a = |
|
30 read_cterm sign (a,T) |> term_of |
|
31 handle ERROR => error ("The error above occurred for " ^ a); |
|
32 |
|
33 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*) |
|
34 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |
|
35 | tryres (th, []) = raise THM("tryres", 0, [th]); |
|
36 |
|
37 fun gen_make_elim elim_rls rl = |
|
38 standard (tryres (rl, elim_rls @ [revcut_rl])); |
|
39 |
|
40 (** String manipulation **) |
|
41 |
|
42 (*Skipping initial blanks, find the first identifier*) |
|
43 fun scan_to_id s = |
|
44 s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1 |
|
45 handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s); |
|
46 |
|
47 fun is_backslash c = c = "\\"; |
|
48 |
|
49 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3 |
|
50 Does not handle the \ddd form; no error checking*) |
|
51 fun escape [] = [] |
|
52 | escape cs = (case take_prefix (not o is_backslash) cs of |
|
53 (front, []) => front |
|
54 | (front, _::"n"::rest) => front @ ("\n" :: escape rest) |
|
55 | (front, _::"t"::rest) => front @ ("\t" :: escape rest) |
|
56 | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest) |
|
57 | (front, _::"\""::rest) => front @ ("\"" :: escape rest) |
|
58 | (front, _::"\\"::rest) => front @ ("\\" :: escape rest) |
|
59 | (front, b::c::rest) => |
|
60 if is_blank c (*remove any further blanks and the following \ *) |
|
61 then front @ escape (tl (snd (take_prefix is_blank rest))) |
|
62 else error ("Unrecognized string escape: " ^ implode(b::c::rest))); |
|
63 |
|
64 (*Remove the first and last charaters -- presumed to be quotes*) |
|
65 val trim = implode o escape o rev o tl o rev o tl o explode; |