src/Pure/section_utils.ML
changeset 579 08f465e23dc5
child 613 f9eb0f819642
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/section_utils.ML	Thu Aug 25 12:21:00 1994 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +(*  Title: 	Pure/section-utils
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +Utilities for writing new theory sections
    1.10 +*)
    1.11 +
    1.12 +fun ap t u = t$u;
    1.13 +fun app t (u1,u2) = t $ u1 $ u2;
    1.14 +
    1.15 +(*Make distinct individual variables a1, a2, a3, ..., an. *)
    1.16 +fun mk_frees a [] = []
    1.17 +  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
    1.18 +
    1.19 +(*Make a definition lhs==rhs*)
    1.20 +fun mk_defpair (lhs, rhs) = 
    1.21 +  let val Const(name, _) = head_of lhs
    1.22 +  in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
    1.23 +
    1.24 +fun get_def thy s = get_axiom thy (s^"_def");
    1.25 +
    1.26 +fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    1.27 +
    1.28 +
    1.29 +(*Read an assumption in the given theory*)
    1.30 +fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    1.31 +
    1.32 +fun readtm sign T a = 
    1.33 +    read_cterm sign (a,T) |> term_of
    1.34 +    handle ERROR => error ("The error above occurred for " ^ a);
    1.35 +
    1.36 +(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    1.37 +fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    1.38 +  | tryres (th, []) = raise THM("tryres", 0, [th]);
    1.39 +
    1.40 +fun gen_make_elim elim_rls rl = 
    1.41 +      standard (tryres (rl, elim_rls @ [revcut_rl]));
    1.42 +
    1.43 +(** String manipulation **)
    1.44 +
    1.45 +(*Skipping initial blanks, find the first identifier*)
    1.46 +fun scan_to_id s = 
    1.47 +    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
    1.48 +    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
    1.49 +
    1.50 +fun is_backslash c = c = "\\";
    1.51 +
    1.52 +(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
    1.53 +  Does not handle the \ddd form;  no error checking*)
    1.54 +fun escape [] = []
    1.55 +  | escape cs = (case take_prefix (not o is_backslash) cs of
    1.56 +	 (front, []) => front
    1.57 +       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
    1.58 +       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
    1.59 +       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
    1.60 +       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
    1.61 +       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
    1.62 +       | (front, b::c::rest) => 
    1.63 +	   if is_blank c   (*remove any further blanks and the following \ *)
    1.64 +	   then front @ escape (tl (snd (take_prefix is_blank rest)))
    1.65 +	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    1.66 +
    1.67 +(*Remove the first and last charaters -- presumed to be quotes*)
    1.68 +val trim = implode o escape o rev o tl o rev o tl o explode;