From b37fa56c70b99101957e418e0f9e8f6701d0db0d Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 11 Jul 2024 22:17:29 -0700
Subject: [PATCH] fix issue in prettier

---
 README.md            |  5 ++---
 newt/zoo3.newt       | 36 ++++++++++++++++++++++++++++--------
 src/Lib/Prettier.idr |  5 +++--
 src/Main.idr         |  1 -
 4 files changed, 33 insertions(+), 14 deletions(-)

diff --git a/README.md b/README.md
index ca4f88a..6bd9b4f 100644
--- a/README.md
+++ b/README.md
@@ -22,10 +22,9 @@ I'd kinda like to see array run in js...
 
 Idris does a common array for metas and defs. 
 
+Prettier was missing a Lazy.
 
-
-Something exponential is going on with zoo3.newt.  Adding code makes it quickly worse. 
-
+Zoo3, mostly runs aside from eqTest. 
 
 Parser:
 - [x] unify broken for zoo3 `cons`
diff --git a/newt/zoo3.newt b/newt/zoo3.newt
index 3bbe8b5..8276dad 100644
--- a/newt/zoo3.newt
+++ b/newt/zoo3.newt
@@ -33,19 +33,39 @@ refl = \ A x p px => px
 list1 : List Bool
 list1 = cons _ true (cons _ false (nil _))
 
--- 9 sec
-
-
 Nat : U
 Nat = (N : U) -> (N -> N) -> N -> N
 
--- 30 sec
+five : Nat
+five = \ N s z => s (s (s (s (s z))))
 
--- five : Nat
--- five = \ N s z => s (s (s (s (s z))))
+add : Nat -> Nat -> Nat
+add = \ a b N s z => a N s (b N s z)
 
--- add : Nat -> Nat -> Nat
--- add = \ a b N s z => a N s (b N s z)
+mul : Nat -> Nat -> Nat
+mul = \a b N s z => a N (b N s) z
+
+ten : Nat
+ten = add five five
+
+hundred : Nat
+hundred = mul ten ten
+
+thousand : Nat
+thousand = mul ten hundred
+
+-- All of these fail, but are they funext?
+-- works for zoo3, but maybe I'm expanding stuff too eagerly
+
+-- eq : Eq _ true true
+-- eq = refl
+
+-- eqTest2 : Eq _ five five
+-- eqTest2 = refl
+
+-- -- This one breaks
+-- eqTest : Eq _ hundred hundred
+-- -- eqTest = refl _ _
 
 -- Add the rest
 
diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr
index 23f0247..b01212a 100644
--- a/src/Lib/Prettier.idr
+++ b/src/Lib/Prettier.idr
@@ -35,12 +35,13 @@ layout (TEXT str x) = str ++ layout x
 
 ||| Whether a documents first line fits.
 fits : Nat -> DOC -> Bool
-fits w x = if w < 0 then False else case x of
+fits w x = if w == 0 then False else case x of
             EMPTY => True
             (LINE k x) => True
             (TEXT s x) => fits (w `minus` length s) x
 
-better : Nat -> Nat -> DOC -> DOC -> DOC
+-- The lazy is important
+better : Nat -> Nat -> DOC -> Lazy DOC -> DOC
 better w k x y = if fits (w `minus` k) x then x else y
 
 be : Nat -> Nat -> List (Nat, Doc) -> DOC
diff --git a/src/Main.idr b/src/Main.idr
index 243fc93..366bf74 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -55,7 +55,6 @@ processDecl (TypeSig nm tm) = do
 
 -- FIXME - this should be in another file
 processDecl (Def nm raw) = do
-  let m : MonadError Error M := %search
   putStrLn "def \{show nm}"
   ctx <- get
   let pos = case raw of