author  wenzelm 
Fri, 18 Mar 2016 16:26:35 +0100  
changeset 62663  bea354f6ff21 
parent 62503  19afb533028e 
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 

62663  7 
PolyML.addPrettyPrinter 
8 
(fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); 

62356  9 

62663  10 
PolyML.addPrettyPrinter 
11 
(fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory); 

62356  12 

62663  13 
PolyML.addPrettyPrinter 
14 
(fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory); 

62356  15 

62663  16 
PolyML.addPrettyPrinter 
17 
(fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory); 

33767  18 

62663  19 
PolyML.addPrettyPrinter 
20 
(fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory); 

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

21 

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

22 

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

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

24 

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

25 
open PolyML; 
62503  26 
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

27 
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

28 
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

29 

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

30 
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

31 
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

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

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

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

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

36 
> 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

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

38 
> (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

39 
 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

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

41 
[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

42 
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

43 
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

44 
 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

45 
 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

46 
 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

47 
 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

48 

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

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

50 

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

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

52 
PolyML.addPrettyPrinter (fn depth => fn _ => fn t => 
62503  53 
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

54 

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

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

56 

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

57 
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

58 
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

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

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

61 
_ % _ => 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

62 
 _ %% _ => 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

63 
 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

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

65 
[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

66 
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

67 
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

68 
 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

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

70 
[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

71 
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

72 
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

73 
 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

74 
 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

75 
 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

76 
 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

77 
 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

78 
 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

79 
 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

80 
 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

81 

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

82 
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

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

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

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

86 
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

87 
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

88 

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

89 
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

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

91 
((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

92 
 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

93 
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

94 
 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

95 

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

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

97 

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

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

99 
PolyML.addPrettyPrinter (fn depth => fn _ => fn prf => 
62503  100 
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

101 

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

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

103 

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

104 
end; 