author  wenzelm 
Thu, 03 Mar 2016 11:59:03 +0100  
changeset 62503  19afb533028e 
parent 62387  ad3eb2889f9a 
child 62663  bea354f6ff21 
permissions  rwrr 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
43791
diff
changeset

1 
(* Title: Pure/ML/install_pp_polyml.ML 
38327  2 
Author: Makarius 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

3 

62356  4 
ML toplevel prettyprinting for Poly/ML. 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

5 
*) 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

6 

62356  7 
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T => 
62503  8 
ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>"))); 
62356  9 

10 
PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon => 

62503  11 
ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon))); 
62356  12 

13 
PolyML.addPrettyPrinter (fn _ => fn _ => fn task => 

62503  14 
ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task)))); 
62356  15 

16 
PolyML.addPrettyPrinter (fn _ => fn _ => fn group => 

62503  17 
ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group)))); 
62356  18 

19 
PolyML.addPrettyPrinter (fn _ => fn _ => fn pos => 

62503  20 
ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos))); 
62356  21 

22 
PolyML.addPrettyPrinter (fn _ => fn _ => fn binding => 

62503  23 
ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding))); 
62356  24 

25 
PolyML.addPrettyPrinter (fn _ => fn _ => fn th => 

62503  26 
ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th))); 
62356  27 

28 
PolyML.addPrettyPrinter (fn _ => fn _ => fn ct => 

62503  29 
ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct))); 
62356  30 

31 
PolyML.addPrettyPrinter (fn _ => fn _ => fn cT => 

62503  32 
ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT))); 
62356  33 

34 
PolyML.addPrettyPrinter (fn _ => fn _ => fn T => 

62503  35 
ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T))); 
62356  36 

37 
PolyML.addPrettyPrinter (fn _ => fn _ => fn thy => 

62503  38 
ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy))); 
62356  39 

40 
PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt => 

62503  41 
ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt))); 
62356  42 

43 
PolyML.addPrettyPrinter (fn _ => fn _ => fn ast => 

62503  44 
ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast))); 
62356  45 

46 
PolyML.addPrettyPrinter (fn _ => fn _ => fn path => 

62503  47 
ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path))); 
62356  48 

49 
PolyML.addPrettyPrinter (fn _ => fn _ => fn digest => 

62503  50 
ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest))))); 
62356  51 

52 
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state => 

62503  53 
ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>"))); 
62356  54 

55 
PolyML.addPrettyPrinter (fn _ => fn _ => fn st => 

62503  56 
ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st))); 
62356  57 

58 
PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism => 

62503  59 
ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism))); 
62356  60 

41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

61 
PolyML.addPrettyPrinter (fn depth => fn _ => fn str => 
62503  62 
ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str))); 
41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

63 

43791  64 
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => 
62503  65 
ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree))); 
43791  66 

33767  67 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => 
68 
pretty (Synchronized.value var, depth)); 

69 

31318  70 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

71 
(case Future.peek x of 
31318  72 
NONE => PolyML.PrettyString "<future>" 
73 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset

74 
 SOME (Exn.Res y) => pretty (y, depth))); 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

75 

31318  76 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

77 
(case Lazy.peek x of 
31318  78 
NONE => PolyML.PrettyString "<lazy>" 
79 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset

80 
 SOME (Exn.Res y) => pretty (y, depth))); 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

81 

52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

82 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

83 
local 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

84 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

85 
open PolyML; 
62503  86 
val from_ML = Pretty.from_ML o ML_Pretty.from_polyml; 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

87 
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

88 
fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

89 

62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62356
diff
changeset

90 
fun prt_term parens (dp: FixedInt.int) t = 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

91 
if dp <= 0 then Pretty.str "..." 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

92 
else 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

93 
(case t of 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

94 
_ $ _ => 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

95 
op :: (strip_comb t) 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62356
diff
changeset

96 
> map_index (fn (i, u) => prt_term true (dp  FixedInt.fromInt i  1) u) 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

97 
> Pretty.separate " $" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

98 
> (if parens then Pretty.enclose "(" ")" else Pretty.block) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

99 
 Abs (a, T, b) => 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

100 
prt_apps "Abs" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

101 
[from_ML (prettyRepresentation (a, dp  1)), 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

102 
from_ML (prettyRepresentation (T, dp  2)), 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

103 
prt_term false (dp  3) b] 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

104 
 Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

105 
 Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

106 
 Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

107 
 Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp  1)))); 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

108 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

109 
in 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

110 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

111 
val _ = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

112 
PolyML.addPrettyPrinter (fn depth => fn _ => fn t => 
62503  113 
ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t))); 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

114 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

115 
local 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

116 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

117 
fun prt_proof parens dp prf = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

118 
if dp <= 0 then Pretty.str "..." 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

119 
else 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

120 
(case prf of 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

121 
_ % _ => prt_proofs parens dp prf 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

122 
 _ %% _ => prt_proofs parens dp prf 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

123 
 Abst (a, T, b) => 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

124 
prt_apps "Abst" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

125 
[from_ML (prettyRepresentation (a, dp  1)), 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

126 
from_ML (prettyRepresentation (T, dp  2)), 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

127 
prt_proof false (dp  3) b] 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

128 
 AbsP (a, t, b) => 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

129 
prt_apps "AbsP" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

130 
[from_ML (prettyRepresentation (a, dp  1)), 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

131 
from_ML (prettyRepresentation (t, dp  2)), 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

132 
prt_proof false (dp  3) b] 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

133 
 Hyp t => prt_app "Hyp" (prt_term true (dp  1) t) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

134 
 MinProof => Pretty.str "MinProof" 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

135 
 PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

136 
 PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

137 
 OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

138 
 Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

139 
 Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp  1))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

140 
 PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp  1)))) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

141 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

142 
and prt_proofs parens dp prf = 
33545
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

143 
let 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

144 
val (head, args) = strip_proof prf []; 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62356
diff
changeset

145 
val prts = 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62356
diff
changeset

146 
head (dp  1) :: flat (map_index (fn (i, prt) => prt (dp  FixedInt.fromInt i  2)) args); 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

147 
in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

148 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

149 
and strip_proof (p % t) res = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

150 
strip_proof p 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

151 
((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

152 
 strip_proof (p %% q) res = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

153 
strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res) 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

154 
 strip_proof p res = (fn d => prt_proof true d p, res); 
33545
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

155 

52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

156 
in 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

157 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

158 
val _ = 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

159 
PolyML.addPrettyPrinter (fn depth => fn _ => fn prf => 
62503  160 
ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf))); 
52426
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

161 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

162 
end; 
81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

163 

81e27230a8b7
ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents:
52425
diff
changeset

164 
end; 