# HG changeset patch # User wenzelm # Date 781976338 -3600 # Node ID 49fc43cd6a35acc01694ef3bb9b5ba85f550ebea # Parent b26753b92f98ad322d3fbbe3d0226481f9e2e215 add_defs: improved error messages; installed new print_goals with nice 'env mode'; diff -r b26753b92f98 -r 49fc43cd6a35 src/Pure/drule.ML --- a/src/Pure/drule.ML Wed Oct 12 16:34:52 1994 +0100 +++ b/src/Pure/drule.ML Wed Oct 12 16:38:58 1994 +0100 @@ -147,29 +147,36 @@ val (c, ty) = dest_Const head handle TERM _ => err "Head of lhs not a constant"; - fun occs_const (Const c_ty') = clash_consts (c, ty) c_ty' + fun occs_const (Const (c', _)) = (c = c') | occs_const (Abs (_, _, t)) = occs_const t | occs_const (t $ u) = occs_const t orelse occs_const u | occs_const _ = false; + + val show_frees = commas_quote o map (fst o dest_Free); + val show_tfrees = commas_quote o map fst; + + val lhs_dups = duplicates args; + val rhs_extras = gen_rems (op =) (term_frees rhs, args); + val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); in if not (forall is_Free args) then err "Arguments of lhs have to be variables" - else if not (null (duplicates args)) then - err "Duplicate variables on lhs" - else if not (term_frees rhs subset args) then - err "Extra variables on rhs" - else if not (term_tfrees rhs subset typ_tfrees ty) then - err "Extra type variables on rhs" + else if not (null lhs_dups) then + err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) + else if not (null rhs_extras) then + err ("Extra variables on rhs: " ^ show_frees rhs_extras) + else if not (null rhs_extrasT) then + err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) else if occs_const rhs then - err "Constant to be defined clashes with occurrence(s) on rhs" + err ("Constant " ^ quote c ^ " occurs on rhs") else (c, ty) end; (* check_defn *) -fun err_in_axm name msg = - (writeln msg; error ("The error(s) above occurred in axiom " ^ quote name)); +fun err_in_defn name msg = + (writeln msg; error ("The error(s) above occurred in definition " ^ quote name)); fun check_defn sign (axms, (name, tm)) = let @@ -180,11 +187,11 @@ fun show_defns c = commas o map (show_defn c); val (c, ty) = dest_defn tm - handle TERM (msg, _) => err_in_axm name msg; + handle TERM (msg, _) => err_in_defn name msg; val defns = clash_defns (c, ty) axms; in if not (null defns) then - err_in_axm name ("Definition of " ^ show_const (c, ty) ^ + err_in_defn name ("Definition of " ^ show_const (c, ty) ^ " clashes with " ^ show_defns c defns) else (name, tm) :: axms end; @@ -323,35 +330,96 @@ (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **) -fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es))); +(* get type_env, sort_env of term *) + +local + open Syntax; + + fun ins_entry (x, y) [] = [(x, [y])] + | ins_entry (x, y) ((pair as (x', ys')) :: pairs) = + if x = x' then (x', y ins ys') :: pairs + else pair :: ins_entry (x, y) pairs; + + fun add_type_env (Free (x, T), env) = ins_entry (T, x) env + | add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env + | add_type_env (Abs (_, _, t), env) = add_type_env (t, env) + | add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env)) + | add_type_env (_, env) = env; + + fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env) + | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env + | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env; + + val sort = map (apsnd sort_strings); +in + fun type_env t = sort (add_type_env (t, [])); + fun sort_env t = rev (sort (it_term_types add_sort_env (t, []))); +end; + + +(* print_goals *) + +fun print_goals maxgoals state = + let + open Syntax; + + val {sign, prop, ...} = rep_thm state; + + val pretty_term = Sign.pretty_term sign; + val pretty_typ = Sign.pretty_typ sign; + val pretty_sort = Sign.pretty_sort; + + fun pretty_vars prtf (X, vs) = Pretty.block + [Pretty.block (Pretty.commas (map Pretty.str vs)), + Pretty.str " ::", Pretty.brk 1, prtf X]; -fun print_goals maxgoals th : unit = -let val {sign, hyps, prop,...} = rep_thm th; - fun printgoals (_, []) = () - | printgoals (n, A::As) = - let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". "); - val prettyA = Sign.pretty_term sign A - in prettyprints[prettyn,prettyA]; - printgoals (n+1,As) - end; - fun prettypair(t,u) = - Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1, - Sign.pretty_term sign u]); - fun printff [] = () - | printff tpairs = - writeln("\nFlex-flex pairs:\n" ^ - Pretty.string_of(Pretty.lst("","") (map prettypair tpairs))) - val (tpairs,As,B) = Logic.strip_horn(prop); - val ngoals = length As -in - writeln (Sign.string_of_term sign B); - if ngoals=0 then writeln"No subgoals!" - else if ngoals>maxgoals - then (printgoals (1, take(maxgoals,As)); - writeln("A total of " ^ string_of_int ngoals ^ " subgoals...")) - else printgoals (1, As); - printff tpairs -end; + fun print_list _ _ [] = () + | print_list name prtf lst = + (writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst))); + + + fun print_goals (_, []) = () + | print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0, + [Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A])); + print_goals (n + 1, As)); + + val print_ffpairs = + print_list "Flex-flex pairs:" (pretty_term o Logic.mk_flexpair); + + val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env; + val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env; + + + val (tpairs, As, B) = Logic.strip_horn prop; + val ngoals = length As; + + val orig_no_freeTs = ! show_no_free_types; + val orig_sorts = ! show_sorts; + + fun restore () = + (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts); + in + (show_no_free_types := true; show_sorts := false; + + Pretty.writeln (pretty_term B); + + if ngoals = 0 then writeln "No subgoals!" + else if ngoals > maxgoals then + (print_goals (1, take (maxgoals, As)); + writeln ("A total of " ^ string_of_int ngoals ^ " subgoals...")) + else print_goals (1, As); + + print_ffpairs tpairs; + + if orig_sorts then + (print_types prop; print_sorts prop) + else if ! show_types then + print_types prop + else ()) + handle exn => (restore (); raise exn); + restore () + end; + (*"hook" for user interfaces: allows print_goals to be replaced*) val print_goals_ref = ref print_goals;