# HG changeset patch
# User wenzelm
# Date 1004990519 -3600
# Node ID 9b1e67278f07c6256c09f89247e42bacca81148c
# Parent  5b5ed7eec3a8fbd38856ce1c1aa583996edc1e7d
added pretty/print functions with context;
added cert_def;
print_asms covers both fixes and assumes;

diff -r 5b5ed7eec3a8 -r 9b1e67278f07 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Nov 05 21:00:45 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 05 21:01:59 2001 +0100
@@ -13,11 +13,12 @@
   exception CONTEXT of string * context
   val theory_of: context -> theory
   val sign_of: context -> Sign.sg
+  val fixed_names_of: context -> string list
+  val assumptions_of: context -> (cterm list * exporter) list
   val prems_of: context -> thm list
   val print_proof_data: theory -> unit
   val init: theory -> context
-  val assumptions: context -> (cterm list * exporter) list
-  val fixed_names: context -> string list
+  val is_fixed: context -> string -> bool
   val read_typ: context -> string -> typ
   val read_typ_no_norm: context -> string -> typ
   val cert_typ: context -> typ -> typ
@@ -71,7 +72,6 @@
   val get_thm_closure: context -> string -> thm
   val get_thms: context -> string -> thm list
   val get_thms_closure: context -> string -> thm list
-  val get_thms_with_closure: (string -> thm list) -> context -> string -> thm list
   val put_thm: string * thm -> context -> context
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
@@ -81,6 +81,7 @@
       context -> context * (string * thm list) list
   val export_assume: exporter
   val export_presume: exporter
+  val cert_def: context -> term -> term
   val export_def: exporter
   val assume: exporter
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
@@ -99,14 +100,19 @@
   val add_cases: (string * RuleCases.T) list -> context -> context
   val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
   val show_hyps: bool ref
-  val pretty_thm: thm -> Pretty.T
+  val pretty_term: context -> term -> Pretty.T
+  val pretty_typ: context -> typ -> Pretty.T
+  val pretty_sort: context -> sort -> Pretty.T
+  val pretty_thm: context -> thm -> Pretty.T
+  val pretty_thms: context -> thm list -> Pretty.T
+  val string_of_term: context -> term -> string
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_binds: context -> unit
-  val print_thms: context -> unit
+  val print_lthms: context -> unit
   val print_cases: context -> unit
   val prems_limit: int ref
-  val pretty_prems: context -> Pretty.T list
+  val pretty_asms: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
   val setup: (theory -> theory) list
 end;
@@ -158,7 +164,14 @@
 fun theory_of (Context {thy, ...}) = thy;
 val sign_of = Theory.sign_of o theory_of;
 
-fun prems_of (Context {asms = ((_, asms), _), ...}) = flat (map #2 asms);
+fun fixes_of (Context {asms = (_, (fixes, _)), ...}) = fixes;
+val fixed_names_of = map #2 o fixes_of;
+fun is_fixed (Context {asms = (_, (fixes, _)), ...}) x = exists (equal x o #2) fixes;
+fun used_table (Context {defs = (_, _, (_, tab)), ...}) = tab;
+
+fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms;
+fun prems_of (Context {asms = ((_, prems), _), ...}) = flat (map #2 prems);
+
 
 
 (** user data **)
@@ -254,13 +267,6 @@
   end;
 
 
-(* get assumptions *)
-
-fun assumptions (Context {asms = ((asms, _), _), ...}) = asms;
-fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes;
-fun used_table (Context {defs = (_, _, (_, tab)), ...}) = tab;
-
-
 
 (** default sorts and types **)
 
@@ -301,7 +307,6 @@
 
 (* internalize Skolem constants *)
 
-fun fixes_of (Context {asms = (_, (fixes, _)), ...}) = fixes;
 fun lookup_skolem ctxt x = assoc (fixes_of ctxt, x);
 fun get_skolem ctxt x = if_none (lookup_skolem ctxt x) x;
 
@@ -513,6 +518,25 @@
 
 
 
+(** pretty printing **)  (* FIXME observe local syntax *)
+
+val pretty_term = Sign.pretty_term o sign_of;
+val pretty_typ = Sign.pretty_typ o sign_of;
+val pretty_sort = Sign.pretty_sort o sign_of;
+
+val string_of_term = Pretty.string_of oo pretty_term;
+
+val show_hyps = ref false;
+
+fun pretty_thm ctxt thm =
+  if ! show_hyps then setmp Display.show_hyps true Display.pretty_thm_no_quote thm
+  else pretty_term ctxt (#prop (Thm.rep_thm thm));
+
+fun pretty_thms ctxt [th] = pretty_thm ctxt th
+  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
+
+
+
 (** Hindley-Milner polymorphism **)
 
 (* warn_extra_tfrees *)
@@ -551,7 +575,7 @@
 
 fun gen_tfrees inner outer =
   let
-    val extra_fixes = fixed_names inner \\ fixed_names outer;
+    val extra_fixes = fixed_names_of inner \\ fixed_names_of outer;
     fun still_fixed (Free (x, _)) = not (x mem_string extra_fixes)
       | still_fixed _ = false;
     fun add (gen, (a, xs)) =
@@ -579,8 +603,8 @@
 fun export is_goal inner outer =
   let
     val tfrees = gen_tfrees inner outer;
-    val fixes = fixed_names inner \\ fixed_names outer;
-    val asms = Library.drop (length (assumptions outer), assumptions inner);
+    val fixes = fixed_names_of inner \\ fixed_names_of outer;
+    val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   in fn thm =>
     thm
@@ -789,7 +813,6 @@
 val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm;
 val get_thms = retrieve_thms PureThy.get_thms (K I);
 val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I);
-fun get_thms_with_closure closure = retrieve_thms (K closure) (K I);
 
 
 (* put_thm(s) *)
@@ -836,22 +859,38 @@
 fun export_presume _ = export_assume false;
 
 
-fun dest_lhs cprop =
+(* defs *)
+
+fun cert_def ctxt eq =    (* FIXME proper treatment of extra type variables *)
   let
-    val lhs = #1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)));  (*exception TERM*)
-    val (f, xs) = Term.strip_comb lhs;
-    val cf = Thm.cterm_of (Thm.sign_of_cterm cprop) f;
+    fun err msg = raise CONTEXT (msg ^
+      "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt);
+    val (lhs, rhs) = Logic.dest_equals (Term.strip_all_body eq)
+      handle TERM _ => err "Not a meta-equality (==)";
+    val (head, args) = Term.strip_comb lhs;
+
+    fun fixed_free (Free (x, _)) = is_fixed ctxt x
+      | fixed_free _ = false;
   in
-    Term.dest_Free f;  (*exception TERM*)
-    if forall Term.is_Bound xs andalso null (duplicates xs) then cf
-    else raise TERM ("", [])
-  end handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
-    quote (Display.string_of_cterm cprop), []);
+    Term.dest_Free head handle TERM _ =>
+      err "Head of lhs must be a variable (free or fixed)";
+    conditional (not (forall (fixed_free orf is_Bound) args andalso null (duplicates args)))
+      (fn () => err "Arguments of lhs must be distinct variables (free or fixed)");
+    conditional (head mem Term.term_frees rhs)
+      (fn () => err "Element to be defined occurs on rhs");
+    conditional (not (null (filter_out fixed_free (term_frees rhs) \\ args)))
+      (fn () => err "Extra free variables on rhs");
+    Term.list_all_free (mapfilter (try Term.dest_Free) args, eq)
+  end;
+
+fun head_of_def cprop =
+  #1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
+  |> Thm.cterm_of (Thm.sign_of_cterm cprop);
 
 fun export_def _ cprops thm =
   thm
   |> Drule.implies_intr_list cprops
-  |> Drule.forall_intr_list (map dest_lhs cprops)
+  |> Drule.forall_intr_list (map head_of_def cprops)
   |> Drule.forall_elim_vars 0
   |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
 
@@ -958,9 +997,8 @@
 
 fun fix_frees ts ctxt =
   let
-    val frees = foldl (foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs)) ([], ts);
-    val fixed = fixed_names ctxt;
-    fun new (x, T) = if x mem_string fixed then None else Some ([x], Some T);
+    val frees = foldl Drule.add_frees ([], ts);
+    fun new (x, T) = if is_fixed ctxt x then None else Some ([x], Some T);
   in fix_direct (mapfilter new frees) ctxt end;
 
 
@@ -1006,12 +1044,6 @@
 
 (** print context information **)
 
-val show_hyps = ref false;
-
-fun pretty_thm thm =
-  if ! show_hyps then setmp Display.show_hyps true Display.pretty_thm_no_quote thm
-  else Display.pretty_cterm (#prop (Thm.crep_thm thm));
-
 val verbose = ref false;
 fun verb f x = if ! verbose then f (x ()) else [];
 fun verb_single x = verb Library.single x;
@@ -1034,8 +1066,7 @@
 
 fun pretty_binds (ctxt as Context {binds, ...}) =
   let
-    val prt_term = Sign.pretty_term (sign_of ctxt);
-    fun prt_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
+    fun prt_bind (xi, (t, T)) = pretty_term ctxt (Logic.mk_equals (Var (xi, T), t));
     val bs = mapfilter smash_option (Vartab.dest binds);
   in
     if null bs andalso not (! verbose) then []
@@ -1047,10 +1078,10 @@
 
 (* local theorems *)
 
-fun pretty_thms (Context {thms, ...}) =
-  pretty_items pretty_thm "facts:" (mapfilter smash_option (Symtab.dest thms));
+fun pretty_lthms (ctxt as Context {thms, ...}) =
+  pretty_items (pretty_thm ctxt) "facts:" (mapfilter smash_option (Symtab.dest thms));
 
-val print_thms = Pretty.writeln o Pretty.chunks o pretty_thms;
+val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;
 
 
 (* local contexts *)
@@ -1064,7 +1095,8 @@
 
 fun pretty_cases (ctxt as Context {cases, ...}) =
   let
-    val prt_term = Sign.pretty_term (sign_of ctxt);
+    val prt_term = pretty_term ctxt;
+
     fun prt_let (xi, t) = Pretty.block
       [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
         Pretty.quote (prt_term t)];
@@ -1090,43 +1122,46 @@
 val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
 
 
-(* prems *)
+(* core context *)
 
 val prems_limit = ref 10;
 
-fun pretty_prems ctxt =
+fun pretty_asms ctxt =
   let
+    val prt_term = pretty_term ctxt;
+
+    (*fixes*)
+    fun prt_fix (x, x') =
+      if x = x' then Pretty.str x
+      else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
+    fun prt_fixes [] = []
+      | prt_fixes xs = [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
+          Pretty.commas (map prt_fix xs))];
+
+    (*prems*)
     val limit = ! prems_limit;
     val prems = prems_of ctxt;
     val len = length prems;
     val prt_prems =
       (if len <= limit then [] else [Pretty.str "..."]) @
-      map pretty_thm (Library.drop (len - limit, prems));
-  in if null prems then [] else [Pretty.big_list "prems:" prt_prems] end;
+      map (pretty_thm ctxt) (Library.drop (len - limit, prems));
+  in
+    prt_fixes (rev (filter_out (can Syntax.dest_internal o #1) (fixes_of ctxt))) @
+    (if null prems then [] else [Pretty.big_list "prems:" prt_prems])
+  end;
 
 
 (* main context *)
 
-fun pretty_context (ctxt as Context {asms = (_, (fixes, _)), cases,
-    defs = (types, sorts, (used, _)), ...}) =
+fun pretty_context (ctxt as Context {cases, defs = (types, sorts, (used, _)), ...}) =
   let
-    val sign = sign_of ctxt;
-
-    val prt_term = Sign.pretty_term sign;
-    val prt_typ = Sign.pretty_typ sign;
-    val prt_sort = Sign.pretty_sort sign;
+    val prt_term = pretty_term ctxt;
+    val prt_typ = pretty_typ ctxt;
+    val prt_sort = pretty_sort ctxt;
 
     (*theory*)
-    val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
-
-    (*fixes*)
-    fun prt_fix (x, x') =
-      if x = x' then Pretty.str x
-      else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
-
-    fun prt_fixes [] = []
-      | prt_fixes xs = [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
-          Pretty.commas (map prt_fix xs))];
+    val pretty_thy = Pretty.block
+      [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg (sign_of ctxt)];
 
     (*defaults*)
     fun prt_atom prt prtT (x, X) = Pretty.block
@@ -1142,10 +1177,9 @@
     val prt_defS = prt_atom prt_varT prt_sort;
   in
     verb_single (K pretty_thy) @
-    prt_fixes (rev (filter_out (can Syntax.dest_internal o #1) fixes)) @
-    pretty_prems ctxt @
+    pretty_asms ctxt @
     verb pretty_binds (K ctxt) @
-    verb pretty_thms (K ctxt) @
+    verb pretty_lthms (K ctxt) @
     verb pretty_cases (K ctxt) @
     verb_single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb_single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @