# HG changeset patch # User paulson # Date 818415592 -3600 # Node ID a1d2735f5adeef606ab07e577b1fdb5e19e6ea5f # Parent 73b6b003c6cae70b126c494e6cde92d63e4e7747 New function read_cterms is a combination of read_def_cterm and read_cterm. It reads and simultaneously type-checks a list of strings. cterm_of no longer catches exception TYPE; instead it must be caught later on and a message printed using Sign.exn_type_msg. More informative messages can be printed this way. diff -r 73b6b003c6ca -r a1d2735f5ade src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Dec 08 10:36:36 1995 +0100 +++ b/src/Pure/thm.ML Fri Dec 08 10:39:52 1995 +0100 @@ -27,6 +27,7 @@ val term_of : cterm -> term val cterm_of : Sign.sg -> term -> cterm val read_cterm : Sign.sg -> string * typ -> cterm + val read_cterms : Sign.sg -> string list * typ list -> cterm list val cterm_fun : (term -> term) -> (cterm -> cterm) val dest_cimplies : cterm -> cterm * cterm val read_def_cterm : @@ -191,9 +192,8 @@ (*create a cterm by checking a "raw" term with respect to a signature*) fun cterm_of sign tm = let val (t, T, maxidx) = Sign.certify_term sign tm - in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} - end handle TYPE (msg, _, _) - => raise TERM ("Term not in signature\n" ^ msg, [tm]); + in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} + end; fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); @@ -217,11 +217,31 @@ val (_, t', tye) = Sign.infer_types sign types sorts used freeze (ts, T'); val ct = cterm_of sign t' - handle TERM (msg, _) => error msg; + handle TYPE arg => error (Sign.exn_type_msg sign arg) + | TERM (msg, _) => error msg; in (ct, tye) end; fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; +(*read a list of terms, matching them against a list of expected types. + NO disambiguation of alternative parses via type-checking -- it is just + not practical.*) +fun read_cterms sign (bs, Ts) = + let + val {tsig, syn, ...} = Sign.rep_sg sign + fun read (b,T) = + case Syntax.read syn T b of + [t] => t + | _ => error("Error or ambiguity in parsing of " ^ b) + val (us,_) = Type.infer_types(tsig, Sign.const_type sign, + K None, K None, + [], true, + map (Sign.certify_typ sign) Ts, + map read (bs~~Ts)) + in map (cterm_of sign) us end + handle TYPE arg => error (Sign.exn_type_msg sign arg) + | TERM (msg, _) => error msg; + (*** Meta theorems ***) @@ -484,7 +504,8 @@ fun cert_axm sg (name, raw_tm) = let val Cterm {t, T, ...} = cterm_of sg raw_tm - handle TERM (msg, _) => error msg; + handle TYPE arg => error (Sign.exn_type_msg sg arg) + | TERM (msg, _) => error msg; in assert (T = propT) "Term not of type prop"; (name, no_vars t)