src/Pure/display.ML
changeset 3990 a8c80f5fdd16
parent 3936 1954255c29ef
child 4126 c41846a38e20
equal deleted inserted replaced
3989:092ab30c1471 3990:a8c80f5fdd16
   101 val print_syntax = Syntax.print_syntax o syn_of;
   101 val print_syntax = Syntax.print_syntax o syn_of;
   102 val print_data = Sign.print_data o sign_of;
   102 val print_data = Sign.print_data o sign_of;
   103 
   103 
   104 fun print_thy thy =
   104 fun print_thy thy =
   105   let
   105   let
   106     val {sign, new_axioms, oracles, ...} = rep_theory thy;
   106     val {sign, axioms, oracles, ...} = rep_theory thy;
   107     val axioms = Symtab.dest new_axioms;
   107     val axioms = Symtab.dest axioms;
   108     val oras = map fst (Symtab.dest oracles);
   108     val oras = map fst (Symtab.dest oracles);
   109 
   109 
   110     fun prt_axm (a, t) = Pretty.block
   110     fun prt_axm (a, t) = Pretty.block
   111       [Pretty.str (Sign.cond_extern sign Theory.thmK a ^ ":"), Pretty.brk 1,
   111       [Pretty.str (Sign.cond_extern sign Theory.axiomK a ^ ":"), Pretty.brk 1,
   112         Pretty.quote (Sign.pretty_term sign t)];
   112         Pretty.quote (Sign.pretty_term sign t)];
   113   in
   113   in
   114     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
   114     Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm axioms));
   115     Pretty.writeln (Pretty.strs ("oracles:" :: oras))
   115     Pretty.writeln (Pretty.strs ("oracles:" :: oras));
       
   116     print_data thy "theorems"
   116   end;
   117   end;
   117 
   118 
   118 fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);
   119 fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy);
   119 
   120 
   120 
   121 
   132   fun ins_entry (x, y) [] = [(x, [y])]
   133   fun ins_entry (x, y) [] = [(x, [y])]
   133     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   134     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   134         if x = x' then (x', y ins ys') :: pairs
   135         if x = x' then (x', y ins ys') :: pairs
   135         else pair :: ins_entry (x, y) pairs;
   136         else pair :: ins_entry (x, y) pairs;
   136 
   137 
   137   fun add_consts (Const (c, T), env) = ins_entry (T, c) env
   138   fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
   138     | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
   139     | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
   139     | add_consts (Abs (_, _, t), env) = add_consts (t, env)
   140     | add_consts (Abs (_, _, t), env) = add_consts (t, env)
   140     | add_consts (_, env) = env;
   141     | add_consts (_, env) = env;
   141 
   142 
   142   fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
   143   fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
   150     | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   151     | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   151 
   152 
   152   fun less_idx ((x, i):indexname, (y, j):indexname) =
   153   fun less_idx ((x, i):indexname, (y, j):indexname) =
   153     x < y orelse x = y andalso i < j;
   154     x < y orelse x = y andalso i < j;
   154   fun sort_idxs l = map (apsnd (sort less_idx)) l;
   155   fun sort_idxs l = map (apsnd (sort less_idx)) l;
   155   fun sort_strs l = map (apsnd sort_strings) l;
   156   fun sort_cnsts l = map (apsnd (sort_wrt fst)) l;
   156 
   157 
   157 
   158 
   158   (* prepare atoms *)
   159   (* prepare atoms *)
   159 
   160 
   160   fun consts_of t = sort_strs (add_consts (t, []));
   161   fun consts_of t = sort_cnsts (add_consts (t, []));
   161   fun vars_of t = sort_idxs (add_vars (t, []));
   162   fun vars_of t = sort_idxs (add_vars (t, []));
   162   fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   163   fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   163 
   164 
   164 in
   165 in
   165 
   166 
   181         | prt_var xi = prt_term (Syntax.var xi);
   182         | prt_var xi = prt_term (Syntax.var xi);
   182 
   183 
   183       fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   184       fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   184         | prt_varT xi = prt_typ (TVar (xi, []));
   185         | prt_varT xi = prt_typ (TVar (xi, []));
   185 
   186 
   186       val prt_consts = prt_atoms (prt_term o Syntax.const) prt_typ;
   187       val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   187       val prt_vars = prt_atoms prt_var prt_typ;
   188       val prt_vars = prt_atoms prt_var prt_typ;
   188       val prt_varsT = prt_atoms prt_varT prt_sort;
   189       val prt_varsT = prt_atoms prt_varT prt_sort;
   189 
   190 
   190 
   191 
   191       fun print_list _ _ [] = ()
   192       fun print_list _ _ [] = ()