--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/section_utils.ML Thu Aug 25 12:21:00 1994 +0200
@@ -0,0 +1,65 @@
+(* Title: Pure/section-utils
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Utilities for writing new theory sections
+*)
+
+fun ap t u = t$u;
+fun app t (u1,u2) = t $ u1 $ u2;
+
+(*Make distinct individual variables a1, a2, a3, ..., an. *)
+fun mk_frees a [] = []
+ | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
+
+(*Make a definition lhs==rhs*)
+fun mk_defpair (lhs, rhs) =
+ let val Const(name, _) = head_of lhs
+ in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
+
+fun get_def thy s = get_axiom thy (s^"_def");
+
+fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
+
+
+(*Read an assumption in the given theory*)
+fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
+
+fun readtm sign T a =
+ read_cterm sign (a,T) |> term_of
+ handle ERROR => error ("The error above occurred for " ^ a);
+
+(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
+fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
+ | tryres (th, []) = raise THM("tryres", 0, [th]);
+
+fun gen_make_elim elim_rls rl =
+ standard (tryres (rl, elim_rls @ [revcut_rl]));
+
+(** String manipulation **)
+
+(*Skipping initial blanks, find the first identifier*)
+fun scan_to_id s =
+ s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
+ handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
+
+fun is_backslash c = c = "\\";
+
+(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
+ Does not handle the \ddd form; no error checking*)
+fun escape [] = []
+ | escape cs = (case take_prefix (not o is_backslash) cs of
+ (front, []) => front
+ | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
+ | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
+ | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
+ | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
+ | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
+ | (front, b::c::rest) =>
+ if is_blank c (*remove any further blanks and the following \ *)
+ then front @ escape (tl (snd (take_prefix is_blank rest)))
+ else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
+
+(*Remove the first and last charaters -- presumed to be quotes*)
+val trim = implode o escape o rev o tl o rev o tl o explode;