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