Skip to content

Commit a5c233e

Browse files
gilithgilith
committed
Clearer printing of let/conditional/infix operators
1 parent 9e6e251 commit a5c233e

File tree

2 files changed

+87
-84
lines changed

2 files changed

+87
-84
lines changed

‎doc/axioms.txt

+65-65
Original file line numberDiff line numberDiff line change
@@ -1,83 +1,83 @@
11
----------------------------------------------------------------------------------------------------------------------------------------------------------------
22
Axiom of Extensionality
33

4-
|- let a <- \d. (\e. d e) = d in a = \b. (\c. c) = \c. c
4+
|- let a <- (\d. (\e. d e) = d) in a = \b. (\c. c) = \c. c
55

66
----------------------------------------------------------------------------------------------------------------------------------------------------------------
77
Axiom of Choice
88

99
|- let a <-
10-
\d.
11-
let e <-
12-
\g.
13-
(let h <- d g in
14-
\i.
15-
(let j <- h in
16-
\k. (\l. l j k) = \m. m ((\c. c) = \c. c) ((\c. c) = \c. c)) i <=>
17-
h) (d (select d)) in
18-
e = \f. (\c. c) = \c. c in
10+
(\d.
11+
let e <-
12+
(\g.
13+
(let h <- d g in
14+
\i.
15+
(let j <- h in
16+
\k. (\l. l j k) = \m. m ((\c. c) = \c. c) ((\c. c) = \c. c)) i <=>
17+
h) (d (select d))) in
18+
e = \f. (\c. c) = \c. c) in
1919
a = \b. (\c. c) = \c. c
2020

2121
----------------------------------------------------------------------------------------------------------------------------------------------------------------
2222
Axiom of Infinity
2323

2424
|- let a <-
25-
\p.
26-
(let h <-
27-
let q <-
28-
\s.
29-
let q <-
30-
\t.
31-
(let f <- p s = p t in
32-
\g.
33-
(let h <- f in
34-
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
35-
f) (s = t) in
36-
q = \r. (\d. d) = \d. d in
37-
q = \r. (\d. d) = \d. d in
38-
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) (let u <-
39-
let q <-
40-
\v.
41-
let w <- \z. v = p z in
42-
let b <-
43-
\x.
44-
(let f <-
45-
let q <-
46-
\y.
47-
(let f <- w y in
48-
\g.
49-
(let h <- f in
50-
\i.
51-
(\j. j h i) =
52-
\k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
53-
f) x in
54-
q = \r. (\d. d) = \d. d in
55-
\g.
56-
(let h <- f in
57-
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
58-
f) x in
59-
b = \c. (\d. d) = \d. d in
60-
q = \r. (\d. d) = \d. d in
61-
(let f <- u in
62-
\g.
63-
(let h <- f in
64-
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
65-
f) (let b <- \d. d in b = \c. (\d. d) = \d. d)) in
25+
(\p.
26+
(let h <-
27+
(let q <-
28+
(\s.
29+
let q <-
30+
(\t.
31+
(let f <- p s = p t in
32+
\g.
33+
(let h <- f in
34+
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
35+
f) (s = t)) in
36+
q = \r. (\d. d) = \d. d) in
37+
q = \r. (\d. d) = \d. d) in
38+
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) (let u <-
39+
(let q <-
40+
(\v.
41+
let w <- (\z. v = p z) in
42+
let b <-
43+
(\x.
44+
(let f <-
45+
(let q <-
46+
(\y.
47+
(let f <- w y in
48+
\g.
49+
(let h <- f in
50+
\i.
51+
(\j. j h i) =
52+
\k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
53+
f) x) in
54+
q = \r. (\d. d) = \d. d) in
55+
\g.
56+
(let h <- f in
57+
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
58+
f) x) in
59+
b = \c. (\d. d) = \d. d) in
60+
q = \r. (\d. d) = \d. d) in
61+
(let f <- u in
62+
\g.
63+
(let h <- f in
64+
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
65+
f) (let b <- (\d. d) in b = \c. (\d. d) = \d. d))) in
6666
let b <-
67-
\e.
68-
(let f <-
69-
let l <-
70-
\n.
71-
(let f <- a n in
72-
\g.
73-
(let h <- f in
74-
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
75-
f) e in
76-
l = \m. (\d. d) = \d. d in
77-
\g.
78-
(let h <- f in
79-
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
80-
f) e in
67+
(\e.
68+
(let f <-
69+
(let l <-
70+
(\n.
71+
(let f <- a n in
72+
\g.
73+
(let h <- f in
74+
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
75+
f) e) in
76+
l = \m. (\d. d) = \d. d) in
77+
\g.
78+
(let h <- f in
79+
\i. (\j. j h i) = \k. k ((\d. d) = \d. d) ((\d. d) = \d. d)) g <=>
80+
f) e) in
8181
b = \c. (\d. d) = \d. d
8282

8383
----------------------------------------------------------------------------------------------------------------------------------------------------------------

‎src/HOL/Print.hs

+22-19
Original file line numberDiff line numberDiff line change
@@ -89,9 +89,10 @@ data Assoc =
8989

9090
type InfixOp = (Prec, Assoc, PP.Doc -> PP.Doc)
9191

92-
ppInfixOps :: (a -> Maybe (InfixOp,a,a)) -> (Bool -> a -> PP.Doc) -> a -> PP.Doc
92+
ppInfixOps :: (a -> Maybe (InfixOp,a,a)) -> (Bool -> a -> PP.Doc) ->
93+
Bool -> a -> PP.Doc
9394
ppInfixOps dest pp =
94-
go Nothing True
95+
go Nothing
9596
where
9697
go mprec rightmost a =
9798
case dest a of
@@ -217,7 +218,7 @@ instance Printable Type where
217218
OpType t [x] -> basic False x <+> toDoc t
218219
OpType t xs -> normals xs <+> toDoc t
219220

220-
normal = ppInfixOps destInfix basic
221+
normal = ppInfixOps destInfix basic True
221222

222223
normals = PP.parens . PP.fsep . PP.punctuate PP.comma . map normal
223224

@@ -325,19 +326,21 @@ instance Printable Term where
325326
([],_) -> binder rightmost tm
326327
(ns,t) -> ppPrefixOps ns $ binder rightmost t
327328

328-
letterm rightmost tm =
329-
case stripLet tm of
330-
([],_) -> negation rightmost tm
331-
(ves,t) -> if not rightmost then parens tm
332-
else ppLet application normal ves t
329+
infixTerm = ppInfixOps destInfix negation
333330

334331
conditional rightmost tm =
335332
case stripCond tm of
336-
([],_) -> letterm rightmost tm
337-
((c,t) : cts, e) -> if not rightmost then parens tm
338-
else ppCond normal c t cts e
333+
([],_) -> infixTerm rightmost tm
334+
((c,t) : cts, e) -> ppCond (infixTerm False)
335+
(infixTerm rightmost) c t cts e
336+
337+
letTerm rightmost tm =
338+
case stripLet tm of
339+
([],_) -> conditional rightmost tm
340+
(ves,t) -> ppLet application (conditional False)
341+
(conditional rightmost) ves t
339342

340-
normal = ppInfixOps destInfix conditional
343+
normal = letTerm True
341344

342345
parens = PP.parens . normal
343346

@@ -616,9 +619,9 @@ instance Printable Term where
616619
Just (c,t,u) -> ((c,t) : cts, e) where (cts,e) = stripCond u
617620
Nothing -> ([],tm)
618621

619-
ppCond :: (Term -> PP.Doc) -> Term -> Term -> [(Term,Term)] -> Term ->
620-
PP.Doc
621-
ppCond pp =
622+
ppCond :: (Term -> PP.Doc) -> (Term -> PP.Doc) ->
623+
Term -> Term -> [(Term,Term)] -> Term -> PP.Doc
624+
ppCond pp ppe =
622625
\c t cts e ->
623626
PP.sep (ifThen c t : map elseIfThen cts ++ [elseBranch e])
624627
where
@@ -629,7 +632,7 @@ instance Printable Term where
629632
PP.text "else" <+> PP.sep [PP.text "if" <+> pp c,
630633
PP.text "then" <+> pp t]
631634

632-
elseBranch e = PP.text "else" <+> pp e
635+
elseBranch e = PP.text "else" <+> ppe e
633636

634637
-------------------------------------------------------------------------
635638
-- Lets
@@ -650,15 +653,15 @@ instance Printable Term where
650653
Just (v,e,u) -> ((v,e) : ves, t) where (ves,t) = stripLet u
651654
Nothing -> ([],tm)
652655

653-
ppLet :: (Term -> PP.Doc) -> (Term -> PP.Doc) ->
656+
ppLet :: (Term -> PP.Doc) -> (Term -> PP.Doc) -> (Term -> PP.Doc) ->
654657
[(Term,Term)] -> Term -> PP.Doc
655-
ppLet ppv pp =
658+
ppLet ppv ppe pp =
656659
\ves t ->
657660
PP.sep (map letBind ves ++ [pp t])
658661
where
659662
letBind (v,e) =
660663
PP.text "let" <+> PP.sep [ppv v <+> PP.text "<-",
661-
pp e <+> PP.text "in"]
664+
ppe e <+> PP.text "in"]
662665

663666
-------------------------------------------------------------------------
664667
-- Numerals

0 commit comments

Comments
 (0)