src/Pure/section_utils.ML
author wenzelm
Tue Oct 25 13:13:52 1994 +0100 (1994-10-25)
changeset 654 65435e2c6512
parent 613 f9eb0f819642
child 1390 bf523422a3df
permissions -rw-r--r--
added require_thy;
     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 
    24 (*Read an assumption in the given theory*)
    25 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    26 
    27 fun readtm sign T a = 
    28     read_cterm sign (a,T) |> term_of
    29     handle ERROR => error ("The error above occurred for " ^ a);
    30 
    31 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    32 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    33   | tryres (th, []) = raise THM("tryres", 0, [th]);
    34 
    35 fun gen_make_elim elim_rls rl = 
    36       standard (tryres (rl, elim_rls @ [revcut_rl]));
    37 
    38 (** String manipulation **)
    39 
    40 (*Skipping initial blanks, find the first identifier*)
    41 fun scan_to_id s = 
    42     s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
    43     handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
    44 
    45 fun is_backslash c = c = "\\";
    46 
    47 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3
    48   Does not handle the \ddd form;  no error checking*)
    49 fun escape [] = []
    50   | escape cs = (case take_prefix (not o is_backslash) cs of
    51 	 (front, []) => front
    52        | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
    53        | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
    54        | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
    55        | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
    56        | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
    57        | (front, b::c::rest) => 
    58 	   if is_blank c   (*remove any further blanks and the following \ *)
    59 	   then front @ escape (tl (snd (take_prefix is_blank rest)))
    60 	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    61 
    62 (*Remove the first and last charaters -- presumed to be quotes*)
    63 val trim = implode o escape o rev o tl o rev o tl o explode;
    64 
    65 
    66 (*Check for some named theory*)
    67 fun require_thy thy name sect =
    68   if exists (equal name o !) (stamps_of_thy thy) then ()
    69   else error ("Need at least theory " ^ quote name ^ " for " ^ sect);