From e67585c2b34559e73771fe27e0cc1f07ae4481bc Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 18 Oct 2024 22:42:38 -0700 Subject: [PATCH] [ fix ] performance issue in Prettier during codegen of Tree.newt --- TODO.md | 3 +-- src/Lib/Prettier.idr | 32 +++++++++++++++++--------------- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/TODO.md b/TODO.md index c94422f..bca2a21 100644 --- a/TODO.md +++ b/TODO.md @@ -1,7 +1,7 @@ ## TODO -- [ ] unsolved meta errors repeat (need to freeze at some point) +- [ ] unsolved meta errors repeat (need to freeze or only report at end) - [x] Sanitize JS idents, e.g. `_+_` - [ ] Generate some programs that do stuff - [x] import @@ -11,7 +11,6 @@ - When printing `Value`, I now print the spine size instead of spine. - [x] eval for case (see order.newt) - [ ] dynamic pattern unification (add test case first) - - Possibly the cause of issue in code commented out in `TestCase4.newt` - [x] switch from commit/mustWork to checking progress - [x] type constructors are no longer generated? And seem to have 0 arity. - [x] raw let is not yet implemented (although define used by case tree building) diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr index c7f189e..65cac2f 100644 --- a/src/Lib/Prettier.idr +++ b/src/Lib/Prettier.idr @@ -4,6 +4,7 @@ module Lib.Prettier import Data.String import Data.Nat +import Data.Maybe ||| `Doc` is a pretty printing document. Constructors are private, use ||| methods below. `Alt` in particular has some invariants on it, see paper @@ -43,26 +44,27 @@ fits 0 x = False fits w ((TEXT s) :: xs) = fits (w `minus` length s) xs fits w _ = True --- The lazy is important -better : Nat -> Nat -> List Item -> Lazy (List Item) -> List Item -better w k x y = if fits (w `minus` k) x then x else y - -- 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) -be : SnocList Item -> Nat -> Nat -> List (Nat, Doc) -> List Item -be acc w k [] = acc <>> [] -be acc w k ((i, Empty) :: xs) = be acc w k xs -be acc w k ((i, Line) :: xs) = (be (acc :< LINE i) w i xs) -be acc w k ((i, (Text s)) :: xs) = (be (acc :< TEXT s) w (k + length s) xs) -be acc w k ((i, (Nest j x)) :: xs) = be acc w k ((i+j,x)::xs) -be acc w k ((i, (Seq x y)) :: xs) = be acc w k ((i,x) :: (i,y) :: xs) --- We're doing extra work here - the first branch should cut if it exhausts w - k before the first LINE -be acc w k ((i, (Alt x y)) :: xs) = acc <>> better w k (be [<] w k ((i,x)::xs)) - (be [<] w k ((i,y)::xs)) + +-- 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 [] = Just (acc <>> []) +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) = + if not fit || (k + length s < w) + then (be fit (acc :< TEXT s) w (k + length s) xs) + else 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 [<] w k ((i,x)::xs) <|> be fit [<] w k ((i,y)::xs)) best : Nat -> Nat -> Doc -> List Item -best w k x = be [<] w k [(0,x)] +best w k x = fromMaybe [] $ be False [<] w k [(0,x)] -- Public interface public export