src/Pure/section_utils.ML
author wenzelm
Mon Nov 09 15:40:26 1998 +0100 (1998-11-09)
changeset 5838 a4122945d638
parent 4938 c8bbbf3c59fa
child 6039 01f67f5f8dd0
permissions -rw-r--r--
added metacuts_tac;
     1 (*  Title: 	Pure/section_utils.ML
     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 
    17 (*Read an assumption in the given theory*)
    18 fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT));
    19 
    20 (*Read a term from string "b", with expected type T*)
    21 fun readtm sign T b = 
    22     read_cterm sign (b,T) |> term_of
    23     handle ERROR => error ("The error(s) above occurred for " ^ b);
    24 
    25 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    26 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    27   | tryres (th, []) = raise THM("tryres", 0, [th]);
    28 
    29 fun gen_make_elim elim_rls rl = 
    30       standard (tryres (rl, elim_rls @ [revcut_rl]));
    31 
    32 (** String manipulation **)
    33 
    34 (*Skipping initial blanks, find the first identifier*)	(* FIXME *)
    35 fun scan_to_id s = 
    36     s |> Symbol.explode
    37     |> Scan.error (Scan.finite Symbol.stopper
    38       (!! (fn _ => "Expected to find an identifier in " ^ s)
    39         (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    40     |> #1;
    41 
    42 fun is_backslash c = c = "\\";
    43 
    44 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3
    45   Does not handle the \ddd form;  no error checking*)
    46 fun escape [] = []
    47   | escape cs = (case take_prefix (not o is_backslash) cs of
    48 	 (front, []) => front
    49        | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
    50        | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
    51        | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
    52        | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
    53        | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
    54        | (front, b::c::rest) => 
    55 	   if Symbol.is_blank c   (*remove any further blanks and the following \ *)
    56 	   then front @ escape (tl (snd (take_prefix Symbol.is_blank rest)))
    57 	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    58 
    59 (*Remove the first and last charaters -- presumed to be quotes*)
    60 val trim = implode o escape o rev o tl o rev o tl o Symbol.explode;