src/Pure/section_utils.ML
author wenzelm
Mon Mar 09 16:09:56 1998 +0100 (1998-03-09)
changeset 4695 6aa25ee18fc4
parent 3974 d3c2159b75fa
child 4848 99c8d95c51d6
permissions -rw-r--r--
adapted to new scanners and baroque chars;
clasohm@1460
     1
(*  Title: 	Pure/section-utils
lcp@579
     2
    ID:         $Id$
clasohm@1460
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@579
     4
    Copyright   1994  University of Cambridge
lcp@579
     5
lcp@579
     6
Utilities for writing new theory sections
lcp@579
     7
*)
lcp@579
     8
lcp@579
     9
fun ap t u = t$u;
lcp@579
    10
fun app t (u1,u2) = t $ u1 $ u2;
lcp@579
    11
lcp@579
    12
(*Make distinct individual variables a1, a2, a3, ..., an. *)
lcp@579
    13
fun mk_frees a [] = []
lcp@579
    14
  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
lcp@579
    15
lcp@579
    16
(*Make a definition lhs==rhs*)
lcp@579
    17
fun mk_defpair (lhs, rhs) = 
lcp@579
    18
  let val Const(name, _) = head_of lhs
wenzelm@3934
    19
  in (Sign.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
lcp@579
    20
lcp@579
    21
fun get_def thy s = get_axiom thy (s^"_def");
lcp@579
    22
lcp@579
    23
lcp@579
    24
(*Read an assumption in the given theory*)
lcp@579
    25
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
lcp@579
    26
paulson@1390
    27
(*Read a term from string "b", with expected type T*)
paulson@1390
    28
fun readtm sign T b = 
paulson@1390
    29
    read_cterm sign (b,T) |> term_of
wenzelm@3536
    30
    handle ERROR => error ("The error(s) above occurred for " ^ b);
lcp@579
    31
lcp@579
    32
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
lcp@579
    33
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
lcp@579
    34
  | tryres (th, []) = raise THM("tryres", 0, [th]);
lcp@579
    35
lcp@579
    36
fun gen_make_elim elim_rls rl = 
lcp@579
    37
      standard (tryres (rl, elim_rls @ [revcut_rl]));
lcp@579
    38
lcp@579
    39
(** String manipulation **)
lcp@579
    40
wenzelm@4695
    41
(*Skipping initial blanks, find the first identifier*)	(* FIXME *)
lcp@579
    42
fun scan_to_id s = 
wenzelm@4695
    43
    s |> Symbol.explode
wenzelm@4695
    44
    |> Scan.error (Scan.finite Symbol.eof
wenzelm@4695
    45
      (!! (fn _ => "Expected to find an identifier in " ^ s)
wenzelm@4695
    46
        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
wenzelm@4695
    47
    |> #1;
lcp@579
    48
lcp@579
    49
fun is_backslash c = c = "\\";
lcp@579
    50
lcp@579
    51
(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
lcp@579
    52
  Does not handle the \ddd form;  no error checking*)
lcp@579
    53
fun escape [] = []
lcp@579
    54
  | escape cs = (case take_prefix (not o is_backslash) cs of
clasohm@1460
    55
	 (front, []) => front
lcp@579
    56
       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
lcp@579
    57
       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
lcp@579
    58
       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
lcp@579
    59
       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
lcp@579
    60
       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
lcp@579
    61
       | (front, b::c::rest) => 
wenzelm@4695
    62
	   if Symbol.is_blank c   (*remove any further blanks and the following \ *)
wenzelm@4695
    63
	   then front @ escape (tl (snd (take_prefix Symbol.is_blank rest)))
clasohm@1460
    64
	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
lcp@579
    65
lcp@579
    66
(*Remove the first and last charaters -- presumed to be quotes*)
wenzelm@4695
    67
val trim = implode o escape o rev o tl o rev o tl o Symbol.explode;
wenzelm@654
    68
wenzelm@654
    69
wenzelm@654
    70
(*Check for some named theory*)
wenzelm@654
    71
fun require_thy thy name sect =
wenzelm@3974
    72
  if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
paulson@2863
    73
  else error ("Need theory " ^ quote name ^ " as an ancestor for " ^ sect);