src/Pure/display.ML
changeset 11883 7b9522995a78
parent 11501 3b6415035d1a
child 12067 b2f5fbb39f14
     1.1 --- a/src/Pure/display.ML	Mon Oct 22 17:58:56 2001 +0200
     1.2 +++ b/src/Pure/display.ML	Mon Oct 22 17:59:39 2001 +0200
     1.3 @@ -6,45 +6,59 @@
     1.4  Printing of theories, theorems, etc.
     1.5  *)
     1.6  
     1.7 +signature BASIC_DISPLAY =
     1.8 +sig
     1.9 +  val show_hyps: bool ref
    1.10 +  val show_tags: bool ref
    1.11 +  val string_of_thm: thm -> string
    1.12 +  val print_thm: thm -> unit
    1.13 +  val print_thms: thm list -> unit
    1.14 +  val prth: thm -> thm
    1.15 +  val prthq: thm Seq.seq -> thm Seq.seq
    1.16 +  val prths: thm list -> thm list
    1.17 +  val string_of_ctyp: ctyp -> string
    1.18 +  val print_ctyp: ctyp -> unit
    1.19 +  val string_of_cterm: cterm -> string
    1.20 +  val print_cterm: cterm -> unit
    1.21 +  val print_syntax: theory -> unit
    1.22 +  val show_consts: bool ref
    1.23 +end;
    1.24 +
    1.25  signature DISPLAY =
    1.26  sig
    1.27 -  val show_hyps		: bool ref
    1.28 -  val show_tags		: bool ref
    1.29 +  include BASIC_DISPLAY
    1.30    val pretty_thm_no_quote: thm -> Pretty.T
    1.31 -  val pretty_thm	: thm -> Pretty.T
    1.32 -  val pretty_thms	: thm list -> Pretty.T
    1.33 -  val pretty_thm_sg     : Sign.sg -> thm -> Pretty.T
    1.34 -  val pretty_thms_sg    : Sign.sg -> thm list -> Pretty.T
    1.35 -  val string_of_thm	: thm -> string
    1.36 -  val pprint_thm	: thm -> pprint_args -> unit
    1.37 -  val print_thm		: thm -> unit
    1.38 -  val print_thms	: thm list -> unit
    1.39 -  val prth		: thm -> thm
    1.40 -  val prthq		: thm Seq.seq -> thm Seq.seq
    1.41 -  val prths		: thm list -> thm list
    1.42 -  val pretty_ctyp	: ctyp -> Pretty.T
    1.43 -  val pprint_ctyp	: ctyp -> pprint_args -> unit
    1.44 -  val string_of_ctyp	: ctyp -> string
    1.45 -  val print_ctyp	: ctyp -> unit
    1.46 -  val pretty_cterm	: cterm -> Pretty.T
    1.47 -  val pprint_cterm	: cterm -> pprint_args -> unit
    1.48 -  val string_of_cterm	: cterm -> string
    1.49 -  val print_cterm	: cterm -> unit
    1.50 -  val pretty_theory	: theory -> Pretty.T
    1.51 -  val pprint_theory	: theory -> pprint_args -> unit
    1.52 -  val print_syntax	: theory -> unit
    1.53 +  val pretty_thm: thm -> Pretty.T
    1.54 +  val pretty_thms: thm list -> Pretty.T
    1.55 +  val pretty_thm_sg: Sign.sg -> thm -> Pretty.T
    1.56 +  val pretty_thms_sg: Sign.sg -> thm list -> Pretty.T
    1.57 +  val pprint_thm: thm -> pprint_args -> unit
    1.58 +  val pretty_ctyp: ctyp -> Pretty.T
    1.59 +  val pprint_ctyp: ctyp -> pprint_args -> unit
    1.60 +  val pretty_cterm: cterm -> Pretty.T
    1.61 +  val pprint_cterm: cterm -> pprint_args -> unit
    1.62 +  val pretty_theory: theory -> Pretty.T
    1.63 +  val pprint_theory: theory -> pprint_args -> unit
    1.64    val pretty_full_theory: theory -> Pretty.T list
    1.65 -  val pretty_name_space : string * NameSpace.T -> Pretty.T
    1.66 -  val show_consts	: bool ref
    1.67 +  val pretty_name_space: string * NameSpace.T -> Pretty.T
    1.68 +  val pretty_goals_marker: string -> int -> thm -> Pretty.T list
    1.69 +  val pretty_goals: int -> thm -> Pretty.T list
    1.70 +  val pretty_sub_goals: bool -> int -> thm -> Pretty.T list
    1.71 +  val print_goals_marker: string -> int -> thm -> unit
    1.72 +  val print_goals: int -> thm -> unit
    1.73 +  val current_goals_markers: (string * string * string) ref
    1.74 +  val print_current_goals_default: (int -> int -> thm -> unit)
    1.75 +  val print_current_goals_fn : (int -> int -> thm -> unit) ref
    1.76  end;
    1.77  
    1.78  structure Display: DISPLAY =
    1.79  struct
    1.80  
    1.81 +
    1.82  (** print thm **)
    1.83  
    1.84 -val show_hyps = ref true;	(*false: print meta-hypotheses as dots*)
    1.85 -val show_tags = ref false;	(*false: suppress tags*)
    1.86 +val show_hyps = ref true;       (*false: print meta-hypotheses as dots*)
    1.87 +val show_tags = ref false;      (*false: suppress tags*)
    1.88  
    1.89  local
    1.90  
    1.91 @@ -153,8 +167,7 @@
    1.92    end;
    1.93  
    1.94  
    1.95 -
    1.96 -(* print theory *)
    1.97 +(* pretty_full_theory *)
    1.98  
    1.99  fun pretty_full_theory thy =
   1.100    let
   1.101 @@ -227,10 +240,142 @@
   1.102    end;
   1.103  
   1.104  
   1.105 +
   1.106 +(** print_goals **)
   1.107 +
   1.108 +(* print_goals etc. *)
   1.109 +
   1.110  (*show consts with types in proof state output?*)
   1.111  val show_consts = ref false;
   1.112  
   1.113  
   1.114 +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
   1.115 +
   1.116 +local
   1.117 +
   1.118 +  (* utils *)
   1.119 +
   1.120 +  fun ins_entry (x, y) [] = [(x, [y])]
   1.121 +    | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   1.122 +        if x = x' then (x', y ins ys') :: pairs
   1.123 +        else pair :: ins_entry (x, y) pairs;
   1.124 +
   1.125 +  fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
   1.126 +    | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
   1.127 +    | add_consts (Abs (_, _, t), env) = add_consts (t, env)
   1.128 +    | add_consts (_, env) = env;
   1.129 +
   1.130 +  fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
   1.131 +    | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
   1.132 +    | add_vars (Abs (_, _, t), env) = add_vars (t, env)
   1.133 +    | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
   1.134 +    | add_vars (_, env) = env;
   1.135 +
   1.136 +  fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
   1.137 +    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   1.138 +    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   1.139 +
   1.140 +  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   1.141 +  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   1.142 +
   1.143 +
   1.144 +  (* prepare atoms *)
   1.145 +
   1.146 +  fun consts_of t = sort_cnsts (add_consts (t, []));
   1.147 +  fun vars_of t = sort_idxs (add_vars (t, []));
   1.148 +  fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   1.149 +
   1.150 +  fun pretty_goals_marker_aux begin_goal print_msg print_goal maxgoals state =
   1.151 +    let
   1.152 +      val {sign, ...} = rep_thm state;
   1.153 +
   1.154 +      val prt_term = Sign.pretty_term sign;
   1.155 +      val prt_typ = Sign.pretty_typ sign;
   1.156 +      val prt_sort = Sign.pretty_sort sign;
   1.157 +
   1.158 +      fun prt_atoms prt prtT (X, xs) = Pretty.block
   1.159 +        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   1.160 +          Pretty.brk 1, prtT X];
   1.161 +
   1.162 +      fun prt_var (x, ~1) = prt_term (Syntax.free x)
   1.163 +        | prt_var xi = prt_term (Syntax.var xi);
   1.164 +
   1.165 +      fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   1.166 +        | prt_varT xi = prt_typ (TVar (xi, []));
   1.167 +
   1.168 +      val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   1.169 +      val prt_vars = prt_atoms prt_var prt_typ;
   1.170 +      val prt_varsT = prt_atoms prt_varT prt_sort;
   1.171 +
   1.172 +
   1.173 +      fun pretty_list _ _ [] = []
   1.174 +        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   1.175 +
   1.176 +      fun pretty_subgoal (n, A) =
   1.177 +        Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
   1.178 +      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   1.179 +
   1.180 +      val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
   1.181 +
   1.182 +      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   1.183 +      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   1.184 +      val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   1.185 +
   1.186 +
   1.187 +      val {prop, ...} = rep_thm state;
   1.188 +      val (tpairs, As, B) = Logic.strip_horn prop;
   1.189 +      val ngoals = length As;
   1.190 +
   1.191 +      fun pretty_gs (types, sorts) =
   1.192 +        (if print_goal then [prt_term B] else []) @
   1.193 +         (if ngoals = 0 then [Pretty.str "No subgoals!"]
   1.194 +          else if ngoals > maxgoals then
   1.195 +            pretty_subgoals (take (maxgoals, As)) @
   1.196 +            (if print_msg then
   1.197 +                [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   1.198 +             else [])
   1.199 +          else pretty_subgoals As) @
   1.200 +        pretty_ffpairs tpairs @
   1.201 +        (if ! show_consts then pretty_consts prop else []) @
   1.202 +        (if types then pretty_vars prop else []) @
   1.203 +        (if sorts then pretty_varsT prop else []);
   1.204 +    in
   1.205 +      setmp show_no_free_types true
   1.206 +        (setmp show_types (! show_types orelse ! show_sorts)
   1.207 +          (setmp show_sorts false pretty_gs))
   1.208 +     (! show_types orelse ! show_sorts, ! show_sorts)
   1.209 +  end;
   1.210 +
   1.211 +in
   1.212 +  fun pretty_goals_marker bg = pretty_goals_marker_aux bg true true;
   1.213 +  val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
   1.214 +  val pretty_sub_goals = pretty_goals_marker_aux "" false;
   1.215 +  val pretty_goals = pretty_goals_marker "";
   1.216 +  val print_goals = print_goals_marker "";
   1.217  end;
   1.218  
   1.219 -open Display;
   1.220 +
   1.221 +(* print_current_goals *)
   1.222 +
   1.223 +val current_goals_markers = ref ("", "", "");
   1.224 +
   1.225 +fun print_current_goals_default n max th =
   1.226 +  let
   1.227 +    val ref (begin_state, end_state, begin_goal) = current_goals_markers;
   1.228 +    val ngoals = nprems_of th;
   1.229 +  in
   1.230 +    if begin_state = "" then () else writeln begin_state;
   1.231 +    writeln ("Level " ^ string_of_int n ^
   1.232 +      (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
   1.233 +        (if ngoals <> 1 then "s" else "") ^ ")"
   1.234 +      else ""));
   1.235 +    print_goals_marker begin_goal max th;
   1.236 +    if end_state = "" then () else writeln end_state
   1.237 +  end;
   1.238 +
   1.239 +val print_current_goals_fn = ref print_current_goals_default;
   1.240 +
   1.241 +end;
   1.242 +
   1.243 +structure BasicDisplay: BASIC_DISPLAY = Display;
   1.244 +open BasicDisplay;