From b185065fb0d89cee5cdce5835b47da26e02d5539 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 16 Nov 2024 12:01:48 -0800
Subject: [PATCH] Port Prettier.idr to newt

---
 TODO.md                |   2 +
 newt/IO.newt           |  44 -------
 newt/Prelude.newt      | 215 ++++++++++++++++++++++++++++++++-
 port/Prelude.newt      | 264 +++++++++++++++++++++++++++++++++++++++++
 port/Prettier.newt     | 156 ++++++++++++++++++++++++
 port/TestPrettier.newt |  19 +++
 src/Lib/Elab.idr       |   1 +
 7 files changed, 654 insertions(+), 47 deletions(-)
 delete mode 100644 newt/IO.newt
 create mode 100644 port/Prelude.newt
 create mode 100644 port/Prettier.newt
 create mode 100644 port/TestPrettier.newt

diff --git a/TODO.md b/TODO.md
index c1774d3..4f6bc0a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,8 @@
 
 ## TODO
 
+- [ ] accepting DCon for another type (skipping case, but should be an error)
+- [ ] don't allow (or dot) duplicate names on LHS
 - [ ] improve test driver
   - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
diff --git a/newt/IO.newt b/newt/IO.newt
deleted file mode 100644
index 61437fb..0000000
--- a/newt/IO.newt
+++ /dev/null
@@ -1,44 +0,0 @@
-module IO
-
-import Prelude
-
-data Foo : U where
-  MkFoo : Nat -> Nat -> Foo
-
-data World : U where
-
-data IORes : U -> U where
-  MkIORes : {a : U} -> a -> World -> IORes a
-
-IO : U -> U
-IO a = World -> IORes a
-
--- TODO - if I move w to the left, I get "extra pattern variable"
--- because I'm not looking instide the IO b type, probably should force it.
-iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
-iobind ma mab = \ w => case ma w of
-  (MkIORes a w) => mab a w
-
-iopure : {a : U} -> a -> IO a
-iopure a = \ w => MkIORes a w
-
-IOMonad : Monad IO
-IOMonad = MkMonad iobind iopure
-
-data Unit : U where
-  MkUnit : Unit
-
-ptype String
-
-pfunc log : String -> IO Unit := "(s) => (w) => MkIORes(console.log(s),w)"
-
--- this version wraps with IO, but leaves this plog in scope
-pfunc plog : String -> Unit := "(s) => console.log(s)"
-
-log2 : String -> IO Unit
-log2 s = pure $ plog s
-
-main : IO Unit
-main = do
-  log "woot"
-  log2 "line 2"
diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index 906165a..f75dc9e 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -1,5 +1,20 @@
 module Prelude
 
+
+data Bool : U where
+  True False : Bool
+
+not : Bool → Bool
+not True = False
+not False = True
+
+-- In Idris, this is lazy in the second arg, we're not doing
+-- magic laziness for now, it's messy
+infixr 4 _||_
+_||_ : Bool → Bool → Bool
+True || _ = True
+False || b = b
+
 data Nat : U where
   Z : Nat
   S : Nat -> Nat
@@ -8,22 +23,64 @@ data Maybe : U -> U where
   Just : {a : U} -> a -> Maybe a
   Nothing : {a : U} -> Maybe a
 
+fromMaybe : {a} → a → Maybe a → a
+fromMaybe a Nothing = a
+fromMaybe _ (Just a) = a
+
 data Either : U -> U -> U where
   Left : {a b : U} -> a -> Either a b
   Right : {a b : U} -> b -> Either a b
 
+infixr 7 _::_
+data List : U -> U where
+  Nil : {A} → List A
+  _::_ : {A} → A → List A → List A
+
+
+infixl 7 _:<_
+data SnocList : U → U where
+  Lin : {A} → SnocList A
+  _:<_ : {A} → SnocList A → A → SnocList A
+
+-- 'chips'
+infixr 6 _<>>_
+_<>>_ : {a} → SnocList a → List a → List a
+Lin <>> ys = ys
+(xs :< x) <>> ys = xs <>> x :: ys
+
 -- TODO this is special cased in some languages, maybe for easier
 -- inference? Figure out why.
-
+-- Currently very noisy in generated code (if nothing else, optimize it out?)
 infixr 0 _$_
-
--- Currently very noisy in generated code
 _$_ : {a b : U} -> (a -> b) -> a -> b
 f $ a = f a
 
+infixr 8 _×_
+infixr 2 _,_
+data _×_ : U → U → U where
+  _,_ : {A B} → A → B → A × B
+
+
+infixl 6 _<_
+data Ord : U → U where
+  MkOrd : {A} → (A → A → Bool) → Ord A
+
+_<_ : {A} {{Ord A}} → A → A → Bool
+_<_ {{MkOrd cmp}} a b = cmp a b
+
+cmpNat : Nat → Nat → Bool
+cmpNat Z Z = True
+cmpNat Z m = False
+cmpNat n Z = True
+cmpNat (S n) (S m) = True
+
+OrdNat : Ord Nat
+OrdNat = MkOrd cmpNat
 
 -- Monad
 
+-- TODO sugar for if then else (mixfix is too eager)
+
 -- TODO stack with Applicative, etc?
 
 data Monad : (U -> U) -> U where
@@ -42,6 +99,8 @@ ma >> mb = mb
 pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
 pure {_} {_} {{MkMonad _ pure'}} a = pure' a
 
+-- Equality
+
 infixl 1 _≡_
 data _≡_ : {A : U} -> A -> A -> U where
   Refl :  {A : U} -> {a : A} -> a ≡ a
@@ -53,3 +112,153 @@ cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
 
 sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
 sym Refl = Refl
+
+-- Functor
+data Functor : (U → U) → U where
+  MkFunctor : {m : U → U} → ({a b : U} → (a → b) → m a → m b) → Functor m
+
+map : {m} {{Functor m}} → {a b} → (a → b) → m a → m b
+map {{MkFunctor f}} ma = f ma
+
+infixr 4 _<$>_
+_<$>_ : {f : U → U} {{Functor f}} {a b} → (a → b) → f a → f b
+f <$> ma = map f ma
+
+
+mapMaybe : {a b} → (a → b) → Maybe a → Maybe b
+mapMaybe f Nothing = Nothing
+mapMaybe f (Just a) = Just (f a)
+
+FunctorMaybe : Functor Maybe
+FunctorMaybe = MkFunctor mapMaybe
+
+
+
+-- Idris is lazy in second arg, we don't have that.
+data Alternative : (U → U) → U where
+  MkAlt : {m : U → U} →
+          ({a} → m a → m a → m a) →
+          Alternative m
+
+infixr 2 _<|>_
+_<|>_ : {m : U → U} {{Alternative m}} → {a} → m a → m a → m a
+_<|>_ {m} {{MkAlt f}} {a} x y = f x y
+
+altMaybe : {a} → Maybe a → Maybe a → Maybe a
+altMaybe Nothing x = x
+altMaybe (Just x) _ = Just x
+
+AltMaybe : Alternative Maybe
+AltMaybe = MkAlt altMaybe
+
+-- Semigroup
+
+infixl 8 _<+>_
+data Semigroup : U → U where
+  MkSemi : {a} → (a → a → a) → Semigroup a
+
+_<+>_ : {a} {{Semigroup a}} → a → a → a
+_<+>_ {{MkSemi op}} x y = op x y
+
+
+infixl 7 _+_
+data Add : U → U where
+  MkAdd : {A} → (A → A → A) → Add A
+
+_+_ : {A} {{Add A}} → A → A → A
+_+_ {{MkAdd add}} x y  = add x y
+
+infixl 8 _*_
+data Mul : U → U where
+  MkMul : {A} →
+          (A → A → A) →
+          Mul A
+
+_*_ : {A} {{Mul A}} → A → A → A
+_*_ {{MkMul mul}} x y  = mul x y
+
+
+-- TODO codata/copatterns might be nice here?
+-- AddNat : AddNat
+-- AddNat .add Z m = m
+-- AddNat .add (S n) m = S (self .add n m)
+
+addNat : Nat → Nat → Nat
+addNat Z m = m
+addNat (S n) m = S (addNat n m)
+
+AddNat : Add Nat
+AddNat = MkAdd addNat
+
+mulNat : Nat → Nat → Nat
+mulNat Z _ = Z
+mulNat (S n) m = m + mulNat n m
+
+MulNat : Mul Nat
+MulNat = MkMul mulNat
+
+
+-- TODO Sub
+infixl 7 _-_
+_-_ : Nat -> Nat -> Nat
+Z - m = Z
+n - Z = n
+S n - S m = n - m
+
+
+ptype String
+ptype Int
+ptype Char
+
+-- probably want to switch to Int or implement magic Nat
+pfunc length : String → Nat := "(s) => {
+  let rval = Z
+  for (let i = 0; i < s.length; s++) rval = S(rval)
+  return rval
+}"
+
+data Unit : U where
+  MkUnit : Unit
+
+ptype Array : U → U
+pfunc listToArray : {a : U} -> List a -> Array a := "
+(a, l) => {
+  let rval = []
+  while (l.tag !== 'Nil') {
+    rval.push(l.h1)
+    l = l.h2
+  }
+  return rval
+}
+"
+pfunc alen : {a : U} -> Array a -> Int := "(a,arr) => arr.length"
+pfunc aget : {a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]"
+pfunc aempty : {a : U} -> Unit -> Array a := "() => []"
+
+
+pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')"
+pfunc replicate : Nat -> Char → String := "() => abort('FIXME replicate')"
+
+
+
+ptype World
+
+data IORes : U -> U where
+  MkIORes : {a : U} -> a -> World -> IORes a
+
+IO : U -> U
+IO a = World -> IORes a
+
+-- TODO - if I move w to the left, I get "extra pattern variable"
+-- because I'm not looking instide the IO b type, probably should force it.
+iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
+iobind ma mab = \ w => case ma w of
+  (MkIORes a w) => mab a w
+
+iopure : {a : U} -> a -> IO a
+iopure a = \ w => MkIORes a w
+
+IOMonad : Monad IO
+IOMonad = MkMonad iobind iopure
+
+pfunc putStrLn : String -> IO Unit := "(s) => (w) => console.log(s)"
diff --git a/port/Prelude.newt b/port/Prelude.newt
new file mode 100644
index 0000000..f75dc9e
--- /dev/null
+++ b/port/Prelude.newt
@@ -0,0 +1,264 @@
+module Prelude
+
+
+data Bool : U where
+  True False : Bool
+
+not : Bool → Bool
+not True = False
+not False = True
+
+-- In Idris, this is lazy in the second arg, we're not doing
+-- magic laziness for now, it's messy
+infixr 4 _||_
+_||_ : Bool → Bool → Bool
+True || _ = True
+False || b = b
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+fromMaybe : {a} → a → Maybe a → a
+fromMaybe a Nothing = a
+fromMaybe _ (Just a) = a
+
+data Either : U -> U -> U where
+  Left : {a b : U} -> a -> Either a b
+  Right : {a b : U} -> b -> Either a b
+
+infixr 7 _::_
+data List : U -> U where
+  Nil : {A} → List A
+  _::_ : {A} → A → List A → List A
+
+
+infixl 7 _:<_
+data SnocList : U → U where
+  Lin : {A} → SnocList A
+  _:<_ : {A} → SnocList A → A → SnocList A
+
+-- 'chips'
+infixr 6 _<>>_
+_<>>_ : {a} → SnocList a → List a → List a
+Lin <>> ys = ys
+(xs :< x) <>> ys = xs <>> x :: ys
+
+-- TODO this is special cased in some languages, maybe for easier
+-- inference? Figure out why.
+-- Currently very noisy in generated code (if nothing else, optimize it out?)
+infixr 0 _$_
+_$_ : {a b : U} -> (a -> b) -> a -> b
+f $ a = f a
+
+infixr 8 _×_
+infixr 2 _,_
+data _×_ : U → U → U where
+  _,_ : {A B} → A → B → A × B
+
+
+infixl 6 _<_
+data Ord : U → U where
+  MkOrd : {A} → (A → A → Bool) → Ord A
+
+_<_ : {A} {{Ord A}} → A → A → Bool
+_<_ {{MkOrd cmp}} a b = cmp a b
+
+cmpNat : Nat → Nat → Bool
+cmpNat Z Z = True
+cmpNat Z m = False
+cmpNat n Z = True
+cmpNat (S n) (S m) = True
+
+OrdNat : Ord Nat
+OrdNat = MkOrd cmpNat
+
+-- Monad
+
+-- TODO sugar for if then else (mixfix is too eager)
+
+-- TODO stack with Applicative, etc?
+
+data Monad : (U -> U) -> U where
+  MkMonad : { M : U -> U } ->
+            (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
+            (pure : {A : U} -> A -> M A) ->
+            Monad M
+
+infixl 1 _>>=_ _>>_
+_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
+_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb
+
+_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
+ma >> mb = mb
+
+pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
+pure {_} {_} {{MkMonad _ pure'}} a = pure' a
+
+-- Equality
+
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+  Refl :  {A : U} -> {a : A} -> a ≡ a
+
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
+sym Refl = Refl
+
+-- Functor
+data Functor : (U → U) → U where
+  MkFunctor : {m : U → U} → ({a b : U} → (a → b) → m a → m b) → Functor m
+
+map : {m} {{Functor m}} → {a b} → (a → b) → m a → m b
+map {{MkFunctor f}} ma = f ma
+
+infixr 4 _<$>_
+_<$>_ : {f : U → U} {{Functor f}} {a b} → (a → b) → f a → f b
+f <$> ma = map f ma
+
+
+mapMaybe : {a b} → (a → b) → Maybe a → Maybe b
+mapMaybe f Nothing = Nothing
+mapMaybe f (Just a) = Just (f a)
+
+FunctorMaybe : Functor Maybe
+FunctorMaybe = MkFunctor mapMaybe
+
+
+
+-- Idris is lazy in second arg, we don't have that.
+data Alternative : (U → U) → U where
+  MkAlt : {m : U → U} →
+          ({a} → m a → m a → m a) →
+          Alternative m
+
+infixr 2 _<|>_
+_<|>_ : {m : U → U} {{Alternative m}} → {a} → m a → m a → m a
+_<|>_ {m} {{MkAlt f}} {a} x y = f x y
+
+altMaybe : {a} → Maybe a → Maybe a → Maybe a
+altMaybe Nothing x = x
+altMaybe (Just x) _ = Just x
+
+AltMaybe : Alternative Maybe
+AltMaybe = MkAlt altMaybe
+
+-- Semigroup
+
+infixl 8 _<+>_
+data Semigroup : U → U where
+  MkSemi : {a} → (a → a → a) → Semigroup a
+
+_<+>_ : {a} {{Semigroup a}} → a → a → a
+_<+>_ {{MkSemi op}} x y = op x y
+
+
+infixl 7 _+_
+data Add : U → U where
+  MkAdd : {A} → (A → A → A) → Add A
+
+_+_ : {A} {{Add A}} → A → A → A
+_+_ {{MkAdd add}} x y  = add x y
+
+infixl 8 _*_
+data Mul : U → U where
+  MkMul : {A} →
+          (A → A → A) →
+          Mul A
+
+_*_ : {A} {{Mul A}} → A → A → A
+_*_ {{MkMul mul}} x y  = mul x y
+
+
+-- TODO codata/copatterns might be nice here?
+-- AddNat : AddNat
+-- AddNat .add Z m = m
+-- AddNat .add (S n) m = S (self .add n m)
+
+addNat : Nat → Nat → Nat
+addNat Z m = m
+addNat (S n) m = S (addNat n m)
+
+AddNat : Add Nat
+AddNat = MkAdd addNat
+
+mulNat : Nat → Nat → Nat
+mulNat Z _ = Z
+mulNat (S n) m = m + mulNat n m
+
+MulNat : Mul Nat
+MulNat = MkMul mulNat
+
+
+-- TODO Sub
+infixl 7 _-_
+_-_ : Nat -> Nat -> Nat
+Z - m = Z
+n - Z = n
+S n - S m = n - m
+
+
+ptype String
+ptype Int
+ptype Char
+
+-- probably want to switch to Int or implement magic Nat
+pfunc length : String → Nat := "(s) => {
+  let rval = Z
+  for (let i = 0; i < s.length; s++) rval = S(rval)
+  return rval
+}"
+
+data Unit : U where
+  MkUnit : Unit
+
+ptype Array : U → U
+pfunc listToArray : {a : U} -> List a -> Array a := "
+(a, l) => {
+  let rval = []
+  while (l.tag !== 'Nil') {
+    rval.push(l.h1)
+    l = l.h2
+  }
+  return rval
+}
+"
+pfunc alen : {a : U} -> Array a -> Int := "(a,arr) => arr.length"
+pfunc aget : {a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]"
+pfunc aempty : {a : U} -> Unit -> Array a := "() => []"
+
+
+pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')"
+pfunc replicate : Nat -> Char → String := "() => abort('FIXME replicate')"
+
+
+
+ptype World
+
+data IORes : U -> U where
+  MkIORes : {a : U} -> a -> World -> IORes a
+
+IO : U -> U
+IO a = World -> IORes a
+
+-- TODO - if I move w to the left, I get "extra pattern variable"
+-- because I'm not looking instide the IO b type, probably should force it.
+iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
+iobind ma mab = \ w => case ma w of
+  (MkIORes a w) => mab a w
+
+iopure : {a : U} -> a -> IO a
+iopure a = \ w => MkIORes a w
+
+IOMonad : Monad IO
+IOMonad = MkMonad iobind iopure
+
+pfunc putStrLn : String -> IO Unit := "(s) => (w) => console.log(s)"
diff --git a/port/Prettier.newt b/port/Prettier.newt
new file mode 100644
index 0000000..05d4b5b
--- /dev/null
+++ b/port/Prettier.newt
@@ -0,0 +1,156 @@
+-- A prettier printer, Philip Wadler
+-- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
+module Prettier
+
+import Prelude
+
+-- `Doc` is a pretty printing document.  Constructors are private, use
+-- methods below.  `Alt` in particular has some invariants on it, see paper
+-- for details. (Something along the lines of "the first line of left is not
+-- bigger than the first line of the right".)
+
+
+-- data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
+data Doc : U where
+  Empty Line : Doc
+  Text : String -> Doc
+  Nest : Nat -> Doc -> Doc
+  Seq : Doc -> Doc -> Doc
+  Alt : Doc -> Doc -> Doc
+
+
+-- The original paper had a List-like structure Doc (the above was DOC) which
+-- had Empty and a tail on Text and Line.
+-- data Item = TEXT String | LINE Nat
+data Item : U where
+  TEXT :  String -> Item
+  LINE : Nat -> Item
+
+empty : Doc
+empty = Empty
+
+flatten : Doc -> Doc
+flatten Empty = Empty
+flatten (Seq x y) = Seq (flatten x) (flatten y)
+flatten (Nest i x) = flatten x
+flatten Line = Text " "
+flatten (Text str) = Text str
+flatten (Alt x y) = flatten x
+
+group : Doc -> Doc
+group x = Alt (flatten x) x
+
+-- TODO - we can accumulate snoc and cat all at once
+layout : List Item -> SnocList String -> String
+layout Nil acc = fastConcat $ acc <>> Nil
+layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate k ' ')
+layout (TEXT str :: x) acc = layout x (acc :< str)
+
+-- Whether a documents first line fits.
+fits : Nat -> List Item -> Bool
+fits 0 x = False
+fits w ((TEXT s) :: xs) = fits (w - length s) xs
+fits w _ = True
+
+-- vs Wadler, we're collecting the left side as a SnocList to prevent
+-- blowing out the stack on the Text case.  The original had DOC as
+-- a Linked-List like structure (now List Item)
+
+-- I've now added a `fit` boolean to indicate if we should cut when we hit the line length
+-- Wadler was relying on laziness to stop the first branch before LINE if necessary
+be : Bool -> SnocList Item -> Nat -> Nat -> List (Nat × Doc) -> Maybe (List Item)
+be fit acc w k Nil = Just (acc <>> Nil)
+be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs
+be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs)
+be fit acc w k ((i, (Text s)) :: xs) =
+  case not fit || (k + length s < w) of
+    True => (be fit (acc :< TEXT s) w (k + length s) xs)
+    False => Nothing
+be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x):: xs)
+be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs)
+be fit acc w k ((i, (Alt x y)) :: xs) =
+  (_<>>_ acc) <$> (be True Lin w k ((i,x) :: xs) <|> be fit Lin w k ((i, y) :: xs))
+
+best : Nat -> Nat -> Doc -> List Item
+best w k x = fromMaybe Nil $ be False Lin w k ((Z,x) :: Nil)
+
+-- interface Pretty a where
+--   pretty : a -> Doc
+
+data Pretty : U -> U where
+  MkPretty : {a} → (a → Doc) → Pretty a
+
+pretty : {a} {{Pretty a}} → a → Doc
+pretty {{MkPretty p}} x = p x
+
+render : Nat -> Doc -> String
+render w x = layout (best w Z x) Lin
+
+SemigroupDoc : Semigroup Doc
+SemigroupDoc = MkSemi (\ x y => Seq x (Seq (Text " ") y))
+
+-- Match System.File so we don't get warnings
+
+line : Doc
+line = Line
+
+text : String -> Doc
+text = Text
+
+nest : Nat -> Doc -> Doc
+nest = Nest
+
+infixl 7 _++_
+_++_ : Doc -> Doc -> Doc
+x ++ y = Seq x y
+
+infixl 5 _</>_
+_</>_ : Doc -> Doc -> Doc
+x </> y = x ++ line ++ y
+
+-- fold, but doesn't emit extra nil
+folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc
+folddoc f Nil = Empty
+folddoc f (x :: Nil) = x
+folddoc f (x :: xs) = f x (folddoc f xs)
+
+-- separate with space
+spread : List Doc -> Doc
+spread = folddoc _<+>_
+
+-- separate with new lines
+stack : List Doc -> Doc
+stack = folddoc _</>_
+
+-- bracket x with l and r, indenting contents on new line
+bracket : String -> Doc -> String -> Doc
+bracket l x r = group (text l ++ nest (S (S Z)) (line ++ x) ++ line ++ text r)
+
+infixl 5 _<+/>_
+
+-- Either space or newline
+
+_<+/>_ : Doc -> Doc -> Doc
+x <+/> y = x ++ Alt (text " ") line ++ y
+
+-- Reformat some docs to fill. Not sure if I want this precise behavior or not.
+fill : List Doc -> Doc
+fill Nil = Empty
+fill (x :: Nil) = x
+fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
+
+-- separate with space
+commaSep : List Doc -> Doc
+commaSep = folddoc (\a b => a ++ text "," <+/> b)
+
+/-
+
+FromString Doc where
+  fromString = text
+
+-- If we stick Doc into a String, try to avoid line-breaks via `flatten`
+
+Interpolation Doc where
+  interpolate = render 80 . flatten
+
+-/
diff --git a/port/TestPrettier.newt b/port/TestPrettier.newt
new file mode 100644
index 0000000..cdabe69
--- /dev/null
+++ b/port/TestPrettier.newt
@@ -0,0 +1,19 @@
+module TestPrettier
+
+import Prettier
+
+five : Nat
+five = S (S (S (S (S Z))))
+
+fifty : Nat
+fifty = five * five * S (S Z)
+
+doc : Doc
+doc = text "x" <+> text "+" <+> text "y"
+
+foo : String
+foo = render fifty doc
+
+main : IO Unit
+main = do
+  putStrLn foo
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 06101bb..1795a62 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -1013,5 +1013,6 @@ infer ctx (RImplicit fc) = do
 
 infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String"))
 infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), !(primType fc "Int"))
+infer ctx (RLit fc (LChar c)) = pure (Lit fc (LChar c), !(primType fc "Char"))
 
 infer ctx tm = error (getFC tm) "Implement infer \{show tm}"