src/Pure/display.ML
changeset 12081 f9735aad76dc
parent 12067 b2f5fbb39f14
child 12418 753054ec8e88
     1.1 --- a/src/Pure/display.ML	Tue Nov 06 23:51:16 2001 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Nov 06 23:52:23 2001 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  signature BASIC_DISPLAY =
     1.6  sig
     1.7 +  val goals_limit: int ref
     1.8    val show_hyps: bool ref
     1.9    val show_tags: bool ref
    1.10    val string_of_thm: thm -> string
    1.11 @@ -27,7 +28,7 @@
    1.12  signature DISPLAY =
    1.13  sig
    1.14    include BASIC_DISPLAY
    1.15 -  val pretty_thm_aux: (sort -> Pretty.T) -> (term -> Pretty.T) -> bool -> thm -> Pretty.T
    1.16 +  val pretty_thm_aux: (sort -> Pretty.T) * (term -> Pretty.T) -> bool -> thm -> Pretty.T
    1.17    val pretty_thm_no_quote: thm -> Pretty.T
    1.18    val pretty_thm: thm -> Pretty.T
    1.19    val pretty_thms: thm list -> Pretty.T
    1.20 @@ -42,10 +43,9 @@
    1.21    val pprint_theory: theory -> pprint_args -> unit
    1.22    val pretty_full_theory: theory -> Pretty.T list
    1.23    val pretty_name_space: string * NameSpace.T -> Pretty.T
    1.24 -  val pretty_goals_marker: string -> int -> thm -> Pretty.T list
    1.25 +  val pretty_goals_aux: (sort -> Pretty.T) * (typ -> Pretty.T) * (term -> Pretty.T)
    1.26 +    -> string -> bool * bool -> int -> thm -> Pretty.T list
    1.27    val pretty_goals: int -> thm -> Pretty.T list
    1.28 -  val pretty_sub_goals: bool -> int -> thm -> Pretty.T list
    1.29 -  val print_goals_marker: string -> int -> thm -> unit
    1.30    val print_goals: int -> thm -> unit
    1.31    val current_goals_markers: (string * string * string) ref
    1.32    val print_current_goals_default: (int -> int -> thm -> unit)
    1.33 @@ -58,13 +58,14 @@
    1.34  
    1.35  (** print thm **)
    1.36  
    1.37 +val goals_limit = ref 10;       (*max number of goals to print -- set by user*)
    1.38  val show_hyps = ref true;       (*false: print meta-hypotheses as dots*)
    1.39  val show_tags = ref false;      (*false: suppress tags*)
    1.40  
    1.41  fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
    1.42  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.43  
    1.44 -fun pretty_thm_aux pretty_sort pretty_term quote th =
    1.45 +fun pretty_thm_aux (pretty_sort, pretty_term) quote th =
    1.46    let
    1.47      val {hyps, prop, der = (ora, _), ...} = rep_thm th;
    1.48      val xshyps = Thm.extra_shyps th;
    1.49 @@ -88,7 +89,7 @@
    1.50  
    1.51  fun gen_pretty_thm quote th =
    1.52    let val sg = Thm.sign_of_thm th
    1.53 -  in pretty_thm_aux (Sign.pretty_sort sg) (Sign.pretty_term sg) quote th end;
    1.54 +  in pretty_thm_aux (Sign.pretty_sort sg, Sign.pretty_term sg) quote th end;
    1.55  
    1.56  val pretty_thm = gen_pretty_thm true;
    1.57  val pretty_thm_no_quote = gen_pretty_thm false;
    1.58 @@ -252,105 +253,99 @@
    1.59  
    1.60  local
    1.61  
    1.62 -  (* utils *)
    1.63 +fun ins_entry (x, y) [] = [(x, [y])]
    1.64 +  | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
    1.65 +      if x = x' then (x', y ins ys') :: pairs
    1.66 +      else pair :: ins_entry (x, y) pairs;
    1.67 +
    1.68 +fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
    1.69 +  | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
    1.70 +  | add_consts (Abs (_, _, t), env) = add_consts (t, env)
    1.71 +  | add_consts (_, env) = env;
    1.72  
    1.73 -  fun ins_entry (x, y) [] = [(x, [y])]
    1.74 -    | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
    1.75 -        if x = x' then (x', y ins ys') :: pairs
    1.76 -        else pair :: ins_entry (x, y) pairs;
    1.77 +fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
    1.78 +  | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
    1.79 +  | add_vars (Abs (_, _, t), env) = add_vars (t, env)
    1.80 +  | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
    1.81 +  | add_vars (_, env) = env;
    1.82  
    1.83 -  fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
    1.84 -    | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
    1.85 -    | add_consts (Abs (_, _, t), env) = add_consts (t, env)
    1.86 -    | add_consts (_, env) = env;
    1.87 +fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
    1.88 +  | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
    1.89 +  | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
    1.90  
    1.91 -  fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
    1.92 -    | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
    1.93 -    | add_vars (Abs (_, _, t), env) = add_vars (t, env)
    1.94 -    | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
    1.95 -    | add_vars (_, env) = env;
    1.96 +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    1.97 +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    1.98 +
    1.99 +fun consts_of t = sort_cnsts (add_consts (t, []));
   1.100 +fun vars_of t = sort_idxs (add_vars (t, []));
   1.101 +fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   1.102 +
   1.103 +in
   1.104  
   1.105 -  fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
   1.106 -    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   1.107 -    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   1.108 +fun pretty_goals_aux (prt_sort, prt_typ, prt_term) begin_goal (msg, main) maxgoals state =
   1.109 +  let
   1.110 +    fun prt_atoms prt prtT (X, xs) = Pretty.block
   1.111 +      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   1.112 +        Pretty.brk 1, prtT X];
   1.113  
   1.114 -  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   1.115 -  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   1.116 +    fun prt_var (x, ~1) = prt_term (Syntax.free x)
   1.117 +      | prt_var xi = prt_term (Syntax.var xi);
   1.118 +
   1.119 +    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   1.120 +      | prt_varT xi = prt_typ (TVar (xi, []));
   1.121 +
   1.122 +    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   1.123 +    val prt_vars = prt_atoms prt_var prt_typ;
   1.124 +    val prt_varsT = prt_atoms prt_varT prt_sort;
   1.125  
   1.126  
   1.127 -  (* prepare atoms *)
   1.128 -
   1.129 -  fun consts_of t = sort_cnsts (add_consts (t, []));
   1.130 -  fun vars_of t = sort_idxs (add_vars (t, []));
   1.131 -  fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   1.132 -
   1.133 -  fun pretty_goals_marker_aux begin_goal print_msg print_goal maxgoals state =
   1.134 -    let
   1.135 -      val {sign, ...} = rep_thm state;
   1.136 -
   1.137 -      val prt_term = Sign.pretty_term sign;
   1.138 -      val prt_typ = Sign.pretty_typ sign;
   1.139 -      val prt_sort = Sign.pretty_sort sign;
   1.140 +    fun pretty_list _ _ [] = []
   1.141 +      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   1.142  
   1.143 -      fun prt_atoms prt prtT (X, xs) = Pretty.block
   1.144 -        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   1.145 -          Pretty.brk 1, prtT X];
   1.146 -
   1.147 -      fun prt_var (x, ~1) = prt_term (Syntax.free x)
   1.148 -        | prt_var xi = prt_term (Syntax.var xi);
   1.149 +    fun pretty_subgoal (n, A) =
   1.150 +      Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
   1.151 +    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   1.152  
   1.153 -      fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   1.154 -        | prt_varT xi = prt_typ (TVar (xi, []));
   1.155 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
   1.156  
   1.157 -      val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   1.158 -      val prt_vars = prt_atoms prt_var prt_typ;
   1.159 -      val prt_varsT = prt_atoms prt_varT prt_sort;
   1.160 +    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   1.161 +    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   1.162 +    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   1.163  
   1.164  
   1.165 -      fun pretty_list _ _ [] = []
   1.166 -        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   1.167 -
   1.168 -      fun pretty_subgoal (n, A) =
   1.169 -        Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
   1.170 -      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   1.171 -
   1.172 -      val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
   1.173 -
   1.174 -      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   1.175 -      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   1.176 -      val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   1.177 -
   1.178 -
   1.179 -      val {prop, ...} = rep_thm state;
   1.180 -      val (tpairs, As, B) = Logic.strip_horn prop;
   1.181 -      val ngoals = length As;
   1.182 +    val {prop, ...} = rep_thm state;
   1.183 +    val (tpairs, As, B) = Logic.strip_horn prop;
   1.184 +    val ngoals = length As;
   1.185  
   1.186 -      fun pretty_gs (types, sorts) =
   1.187 -        (if print_goal then [prt_term B] else []) @
   1.188 -         (if ngoals = 0 then [Pretty.str "No subgoals!"]
   1.189 -          else if ngoals > maxgoals then
   1.190 -            pretty_subgoals (take (maxgoals, As)) @
   1.191 -            (if print_msg then
   1.192 -                [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   1.193 -             else [])
   1.194 -          else pretty_subgoals As) @
   1.195 -        pretty_ffpairs tpairs @
   1.196 -        (if ! show_consts then pretty_consts prop else []) @
   1.197 -        (if types then pretty_vars prop else []) @
   1.198 -        (if sorts then pretty_varsT prop else []);
   1.199 -    in
   1.200 -      setmp show_no_free_types true
   1.201 -        (setmp show_types (! show_types orelse ! show_sorts)
   1.202 -          (setmp show_sorts false pretty_gs))
   1.203 -     (! show_types orelse ! show_sorts, ! show_sorts)
   1.204 +    fun pretty_gs (types, sorts) =
   1.205 +      (if main then [prt_term B] else []) @
   1.206 +       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   1.207 +        else if ngoals > maxgoals then
   1.208 +          pretty_subgoals (take (maxgoals, As)) @
   1.209 +          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   1.210 +           else [])
   1.211 +        else pretty_subgoals As) @
   1.212 +      pretty_ffpairs tpairs @
   1.213 +      (if ! show_consts then pretty_consts prop else []) @
   1.214 +      (if types then pretty_vars prop else []) @
   1.215 +      (if sorts then pretty_varsT prop else []);
   1.216 +  in
   1.217 +    setmp show_no_free_types true
   1.218 +      (setmp show_types (! show_types orelse ! show_sorts)
   1.219 +        (setmp show_sorts false pretty_gs))
   1.220 +   (! show_types orelse ! show_sorts, ! show_sorts)
   1.221    end;
   1.222  
   1.223 -in
   1.224 -  fun pretty_goals_marker bg = pretty_goals_marker_aux bg true true;
   1.225 -  val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
   1.226 -  val pretty_sub_goals = pretty_goals_marker_aux "" false;
   1.227 -  val pretty_goals = pretty_goals_marker "";
   1.228 -  val print_goals = print_goals_marker "";
   1.229 +fun pretty_goals_marker bg n th =
   1.230 +  let val sg = Thm.sign_of_thm th in
   1.231 +    pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg)
   1.232 +      bg (true, true) n th
   1.233 +  end;
   1.234 +
   1.235 +val pretty_goals = pretty_goals_marker "";
   1.236 +val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
   1.237 +val print_goals = print_goals_marker "";
   1.238 +
   1.239  end;
   1.240  
   1.241