Changed treatment of during type inference internally generated type
variables.
1. They are renamed to 'a, 'b, 'c etc away from a given set of used names.
2. They are either frozen (turned into TFrees) or left schematic (TVars)
depending on a parameter. In goals they are frozen, for instantiations they
are left schematic.
(* Title: Pure/section-utils
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Utilities for writing new theory sections
*)
fun ap t u = t$u;
fun app t (u1,u2) = t $ u1 $ u2;
(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []
| mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
(*Make a definition lhs==rhs*)
fun mk_defpair (lhs, rhs) =
let val Const(name, _) = head_of lhs
in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
fun get_def thy s = get_axiom thy (s^"_def");
(*Read an assumption in the given theory*)
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
fun readtm sign T a =
read_cterm sign (a,T) |> term_of
handle ERROR => error ("The error above occurred for " ^ a);
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
| tryres (th, []) = raise THM("tryres", 0, [th]);
fun gen_make_elim elim_rls rl =
standard (tryres (rl, elim_rls @ [revcut_rl]));
(** String manipulation **)
(*Skipping initial blanks, find the first identifier*)
fun scan_to_id s =
s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
fun is_backslash c = c = "\\";
(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
Does not handle the \ddd form; no error checking*)
fun escape [] = []
| escape cs = (case take_prefix (not o is_backslash) cs of
(front, []) => front
| (front, _::"n"::rest) => front @ ("\n" :: escape rest)
| (front, _::"t"::rest) => front @ ("\t" :: escape rest)
| (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
| (front, _::"\""::rest) => front @ ("\"" :: escape rest)
| (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
| (front, b::c::rest) =>
if is_blank c (*remove any further blanks and the following \ *)
then front @ escape (tl (snd (take_prefix is_blank rest)))
else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
(*Remove the first and last charaters -- presumed to be quotes*)
val trim = implode o escape o rev o tl o rev o tl o explode;
(*Check for some named theory*)
fun require_thy thy name sect =
if exists (equal name o !) (stamps_of_thy thy) then ()
else error ("Need at least theory " ^ quote name ^ " for " ^ sect);