added pretty_stmt;
authorwenzelm
Tue Mar 14 16:29:36 2006 +0100 (2006-03-14)
changeset 19259196d3b7c8ad1
parent 19258 ada9977f1e98
child 19260 a3d3a4b75c71
added pretty_stmt;
tuned;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Tue Mar 14 16:29:35 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Mar 14 16:29:36 2006 +0100
     1.3 @@ -7,6 +7,11 @@
     1.4  
     1.5  signature ELEMENT =
     1.6  sig
     1.7 +  datatype ('typ, 'term) stmt =
     1.8 +    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
     1.9 +    Obtains of (string * ((string * 'typ option) list * 'term list)) list
    1.10 +  type statement  (*= (string, string) stmt*)
    1.11 +  type statement_i  (*= (typ, term) stmt*)
    1.12    datatype ('typ, 'term, 'fact) ctxt =
    1.13      Fixes of (string * 'typ option * mixfix) list |
    1.14      Constrains of (string * 'typ) list |
    1.15 @@ -20,7 +25,6 @@
    1.16      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
    1.17      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
    1.18    val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
    1.19 -  val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
    1.20    val rename: (string * (string * mixfix option)) list -> string -> string
    1.21    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.22    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.23 @@ -33,16 +37,25 @@
    1.24    val inst_term: typ Symtab.table * term Symtab.table -> term -> term
    1.25    val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
    1.26    val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
    1.27 -  datatype ('typ, 'term) stmt =
    1.28 -    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.29 -    Obtains of (string * ((string * 'typ option) list * 'term list)) list
    1.30 -  type statement  (*= (string, string) stmt*)
    1.31 -  type statement_i  (*= (typ, term) stmt*)
    1.32 +  val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list
    1.33 +  val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
    1.34  end;
    1.35  
    1.36  structure Element: ELEMENT =
    1.37  struct
    1.38  
    1.39 +
    1.40 +(** conclusions **)
    1.41 +
    1.42 +datatype ('typ, 'term) stmt =
    1.43 +  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.44 +  Obtains of (string * ((string * 'typ option) list * 'term list)) list;
    1.45 +
    1.46 +type statement = (string, string) stmt;
    1.47 +type statement_i = (typ, term) stmt;
    1.48 +
    1.49 +
    1.50 +
    1.51  (** context elements **)
    1.52  
    1.53  (* datatype ctxt *)
    1.54 @@ -74,51 +87,6 @@
    1.55      attrib = Args.map_values I typ term thm};
    1.56  
    1.57  
    1.58 -(* pretty_ctxt *)
    1.59 -
    1.60 -fun pretty_ctxt ctxt =
    1.61 -  let
    1.62 -    val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
    1.63 -    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
    1.64 -    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    1.65 -    val prt_atts = Args.pretty_attribs ctxt;
    1.66 -
    1.67 -    fun prt_mixfix mx =
    1.68 -      let val s = Syntax.string_of_mixfix mx
    1.69 -      in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
    1.70 -    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
    1.71 -          prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
    1.72 -      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
    1.73 -    fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn);
    1.74 -
    1.75 -    fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
    1.76 -    fun prt_name_atts (name, atts) sep =
    1.77 -      if name = "" andalso null atts then []
    1.78 -      else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str sep]))];
    1.79 -
    1.80 -    fun prt_asm (a, ts) =
    1.81 -      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
    1.82 -    fun prt_def (a, (t, _)) =
    1.83 -      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
    1.84 -
    1.85 -    fun prt_fact (ths, []) = map prt_thm ths
    1.86 -      | prt_fact (ths, atts) =
    1.87 -          Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts;
    1.88 -    fun prt_note (a, ths) =
    1.89 -      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
    1.90 -
    1.91 -    fun items _ [] = []
    1.92 -      | items prfx (x :: xs) =
    1.93 -          Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items "  and" xs;
    1.94 -  in
    1.95 -    fn Fixes fixes => items "fixes" (map prt_fix fixes)
    1.96 -     | Constrains xs => items "constrains" (map prt_constrain xs)
    1.97 -     | Assumes asms => items "assumes" (map prt_asm asms)
    1.98 -     | Defines defs => items "defines" (map prt_def defs)
    1.99 -     | Notes facts => items "notes" (map prt_note facts)
   1.100 -  end;
   1.101 -
   1.102 -
   1.103  
   1.104  (** logical operations **)
   1.105  
   1.106 @@ -259,13 +227,75 @@
   1.107  
   1.108  
   1.109  
   1.110 -(** concluding statements **)
   1.111 +(** pretty printing **)
   1.112 +
   1.113 +fun pretty_items _ _ _ [] = []
   1.114 +  | pretty_items ctxt sep prfx (x :: xs) =
   1.115 +      Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: pretty_items ctxt sep ("  " ^ sep) xs;
   1.116 +
   1.117 +fun pretty_name_atts ctxt (name, atts) sep =
   1.118 +  if name = "" andalso null atts then []
   1.119 +  else [Pretty.block (Pretty.breaks (Pretty.str (ProofContext.extern_thm ctxt name) ::
   1.120 +    Args.pretty_attribs ctxt atts @ [Pretty.str sep]))];
   1.121 +
   1.122 +
   1.123 +(* pretty_stmt *)
   1.124 +
   1.125 +fun pretty_stmt ctxt =
   1.126 +  let
   1.127 +    val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
   1.128 +    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   1.129 +    val prt_name_atts = pretty_name_atts ctxt;
   1.130 +
   1.131 +    fun prt_show (a, ts) =
   1.132 +      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
   1.133 +
   1.134 +    fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
   1.135 +      | prt_var (x, NONE) = Pretty.str x;
   1.136 +
   1.137 +    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (map prt_term ts))
   1.138 +      | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
   1.139 +          (map prt_var xs @ [Pretty.str "where"] @ map prt_term ts));
   1.140 +  in
   1.141 +    fn Shows shows => pretty_items ctxt "and" "shows" (map prt_show shows)
   1.142 +     | Obtains obtains => pretty_items ctxt "|" "obtains" (map prt_obtain obtains)
   1.143 +  end;
   1.144 +
   1.145  
   1.146 -datatype ('typ, 'term) stmt =
   1.147 -  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
   1.148 -  Obtains of (string * ((string * 'typ option) list * 'term list)) list;
   1.149 +(* pretty_ctxt *)
   1.150 +
   1.151 +fun pretty_ctxt ctxt =
   1.152 +  let
   1.153 +    val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
   1.154 +    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   1.155 +    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
   1.156 +    val prt_name_atts = pretty_name_atts ctxt;
   1.157 +    val prt_items = pretty_items ctxt "and";
   1.158 +
   1.159 +    fun prt_mixfix mx =
   1.160 +      let val s = Syntax.string_of_mixfix mx
   1.161 +      in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
   1.162 +    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
   1.163 +          prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
   1.164 +      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
   1.165 +    fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn);
   1.166  
   1.167 -type statement = (string, string) stmt;
   1.168 -type statement_i = (typ, term) stmt;
   1.169 +    fun prt_asm (a, ts) =
   1.170 +      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
   1.171 +    fun prt_def (a, (t, _)) =
   1.172 +      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
   1.173 +
   1.174 +    fun prt_fact (ths, []) = map prt_thm ths
   1.175 +      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
   1.176 +          (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts;
   1.177 +    fun prt_note (a, ths) =
   1.178 +      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
   1.179 +  in
   1.180 +    fn Fixes fixes => prt_items "fixes" (map prt_fix fixes)
   1.181 +     | Constrains xs => prt_items "constrains" (map prt_constrain xs)
   1.182 +     | Assumes asms => prt_items "assumes" (map prt_asm asms)
   1.183 +     | Defines defs => prt_items "defines" (map prt_def defs)
   1.184 +     | Notes facts => prt_items "notes" (map prt_note facts)
   1.185 +  end;
   1.186  
   1.187  end;