Skip to content
This repository has been archived by the owner on Apr 2, 2023. It is now read-only.

Make lines Immortal. #431

Merged
merged 11 commits into from
Nov 11, 2017
Merged

Make lines Immortal. #431

Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
6833e0f
Rename PATH_ABS to ABS and PATH_APP to DIM_APP.
favonia Nov 10, 2017
2e0e13b
Implement the Immortal notation. Needs testing.
favonia Nov 10, 2017
4d46372
Printing of line and function types.
favonia Nov 10, 2017
578d12a
Fix the printing of fcom, hcom, coe, com, box and cap.
favonia Nov 10, 2017
fce66db
Add the printing of ghcom and gcom.
favonia Nov 10, 2017
63c0e98
No more braces for dim binders.
favonia Nov 10, 2017
8b20e98
Add missing rules of line types.
favonia Nov 11, 2017
95845b6
Goodbye, TY.
favonia Nov 11, 2017
3eff92f
Name the low-level rules in Coe.
favonia Nov 11, 2017
653355a
Very basic testing of line types.
favonia Nov 11, 2017
2ffe12b
Enable the Immortal printing for line types.
favonia Nov 11, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 3 additions & 8 deletions src/redprl/pretty.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ struct

and printAbs (us, m) =
Atomic.parens @@ expr @@ hvsep @@
[hvsep [text "abs", symBinding us], align @@ ppTerm m]
[hvsep [text "abs", varBinding us], align @@ ppTerm m]

and printDimApp (m, rs) =
Atomic.parens @@ expr @@ hvsep
Expand Down Expand Up @@ -267,10 +267,10 @@ struct

| O.DIM0 $ _ => char #"0"
| O.DIM1 $ _ => char #"1"
| O.MK_TUBE $ [_ \ r1, _ \ r2, [u] \ mu] =>
| O.MK_TUBE $ [_ \ r1, _ \ r2, tube] =>
Atomic.squares @@ hsep
[seq [ppTerm r1, Atomic.equals, ppTerm r2],
nest 1 @@ hvsep [Atomic.braces @@ ppVar u, ppTerm mu]]
nest 1 @@ ppBinder tube]
Copy link
Contributor Author

@favonia favonia Nov 11, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@jonsterling Is Was there a reason not to group them?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't remember

| O.MK_BDRY $ [_ \ r1, _ \ r2, _ \ m] =>
Atomic.squares @@ hsep
[seq [ppTerm r1, Atomic.equals, ppTerm r2],
Expand Down Expand Up @@ -301,11 +301,6 @@ struct
[] => atLevel 10 @@ ppTerm m
| _ => grouped @@ hvsep [varBinding xs, align @@ ppTerm m]

and symBinding us =
unlessEmpty us @@
Atomic.braces @@
hsep @@ List.map ppVar us

and varBinding xs =
unlessEmpty xs @@
Atomic.squares @@
Expand Down