From 4598da7e213c889d63fe8de0d1de74fd39ece44f Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:26:51 -0400
Subject: [PATCH 01/13] Define prettify direct-recursively.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This uses fromScope to recur, and accumulates a continuation for the variables to avoid n² fmaps.
---
 semantic-core/src/Data/Core/Pretty.hs | 108 +++++++++++++-------------
 1 file changed, 55 insertions(+), 53 deletions(-)

diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs
index 70cc97197a..cbb7dc295b 100644
--- a/semantic-core/src/Data/Core/Pretty.hs
+++ b/semantic-core/src/Data/Core/Pretty.hs
@@ -11,7 +11,6 @@ module Data.Core.Pretty
 import           Control.Effect.Reader
 import           Data.Core
 import           Data.File
-import           Data.Functor.Const
 import           Data.Name
 import           Data.Scope
 import           Data.Term
@@ -56,57 +55,62 @@ inParens amount go = do
   body <- with amount go
   pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body)
 
-prettify :: (Member (Reader [AnsiDoc]) sig, Member (Reader Prec) sig, Carrier sig m)
+prettify :: (Member (Reader Prec) sig, Carrier sig m)
          => Style
-         -> Core (Const (m AnsiDoc)) a
+         -> Term Core User
          -> m AnsiDoc
-prettify style = \case
-  Let a -> pure $ keyword "let" <+> name a
-  Const a :>> Const b -> do
-    prec <- ask @Prec
-    fore <- with 12 a
-    aft  <- with 12 b
-
-    let open  = symbol ("{" <> softline)
-        close = symbol (softline <> "}")
-        separator = ";" <> Pretty.line
-        body = fore <> separator <> aft
-
-    pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
-
-  Lam n f -> inParens 11 $ do
-    (x, body) <- bind n f
-    pure (lambda <> x <+> arrow <+> body)
-
-  Frame    -> pure $ primitive "frame"
-  Unit     -> pure $ primitive "unit"
-  Bool b   -> pure $ primitive (if b then "true" else "false")
-  String s -> pure . strlit $ Pretty.viaShow s
-
-  Const f :$ Const x -> inParens 11 $ (<+>) <$> f <*> x
-
-  If (Const con) (Const tru) (Const fal) -> do
-    con' <- "if"   `appending` con
-    tru' <- "then" `appending` tru
-    fal' <- "else" `appending` fal
-    pure $ Pretty.sep [con', tru', fal']
-
-  Load (Const p)   -> "load" `appending` p
-  Edge Lexical (Const n) -> "lexical" `appending` n
-  Edge Import (Const n) -> "import" `appending` n
-  Const item :. Const body   -> inParens 4 $ do
-    f <- item
-    g <- body
-    pure (f <> symbol "." <> g)
-
-  Const lhs := Const rhs -> inParens 3 $ do
-    f <- lhs
-    g <- rhs
-    pure (f <+> symbol "=" <+> g)
-
-  -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
-  Ann _ (Const c) -> c
-  where bind (Ignored x) f = let x' = name x in (,) x' <$> local (x':) (getConst (unScope f))
+prettify style = go (pure . name)
+  where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) ->  Term Core a -> m AnsiDoc
+        go var = \case
+          Var v -> var v
+          Term t -> case t of
+            Let a -> pure $ keyword "let" <+> name a
+            a :>> b -> do
+              prec <- ask @Prec
+              fore <- with 12 a
+              aft  <- with 12 b
+
+              let open  = symbol ("{" <> softline)
+                  close = symbol (softline <> "}")
+                  separator = ";" <> Pretty.line
+                  body = fore <> separator <> aft
+
+              pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
+
+            Lam n f -> inParens 11 $ do
+              (x, body) <- bind n f
+              pure (lambda <> x <+> arrow <+> body)
+
+            Frame    -> pure $ primitive "frame"
+            Unit     -> pure $ primitive "unit"
+            Bool b   -> pure $ primitive (if b then "true" else "false")
+            String s -> pure . strlit $ Pretty.viaShow s
+
+            f :$ x -> inParens 11 $ (<+>) <$> go var f <*> go var x
+
+            If con tru fal -> do
+              con' <- "if"   `appending` go var con
+              tru' <- "then" `appending` go var tru
+              fal' <- "else" `appending` go var fal
+              pure $ Pretty.sep [con', tru', fal']
+
+            Load p   -> "load" `appending` go var p
+            Edge Lexical n -> "lexical" `appending` go var n
+            Edge Import n -> "import" `appending` go var n
+            item :. body   -> inParens 4 $ do
+              f <- go var item
+              g <- go var body
+              pure (f <> symbol "." <> g)
+
+            lhs := rhs -> inParens 3 $ do
+              f <- go var lhs
+              g <- go var rhs
+              pure (f <+> symbol "=" <+> g)
+
+            -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
+            Ann _ c -> go var c
+          where with n m = local (const (n :: Prec)) (go var m)
+                bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f)
         lambda = case style of
           Unicode -> symbol "λ"
           Ascii   -> symbol "\\"
@@ -119,6 +123,4 @@ appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
 appending k item = (keyword k <+>) <$> item
 
 prettyCore :: Style -> Term Core User -> AnsiDoc
-prettyCore s = run . runReader @Prec 0 . runReader @[AnsiDoc] [] . cata id (prettify s) bound (pure . name)
-  where bound (Z _) = asks (head @AnsiDoc)
-        bound (S n) = local (tail @AnsiDoc) n
+prettyCore s = run . runReader @Prec 0 . prettify s

From d7e4f2129dd0acc39997ccb90452d987cf4218cf Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:28:12 -0400
Subject: [PATCH 02/13] Combine prettyCore & prettify.

---
 semantic-core/src/Data/Core/Pretty.hs | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs
index cbb7dc295b..ac59ea06f3 100644
--- a/semantic-core/src/Data/Core/Pretty.hs
+++ b/semantic-core/src/Data/Core/Pretty.hs
@@ -55,11 +55,8 @@ inParens amount go = do
   body <- with amount go
   pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body)
 
-prettify :: (Member (Reader Prec) sig, Carrier sig m)
-         => Style
-         -> Term Core User
-         -> m AnsiDoc
-prettify style = go (pure . name)
+prettyCore :: Style -> Term Core User -> AnsiDoc
+prettyCore style = run . runReader @Prec 0 . go (pure . name)
   where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) ->  Term Core a -> m AnsiDoc
         go var = \case
           Var v -> var v
@@ -121,6 +118,3 @@ prettify style = go (pure . name)
 
 appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
 appending k item = (keyword k <+>) <$> item
-
-prettyCore :: Style -> Term Core User -> AnsiDoc
-prettyCore s = run . runReader @Prec 0 . prettify s

From fbb5688bd4da571b62ad01f5bcb535cb5ba47cd9 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:29:57 -0400
Subject: [PATCH 03/13] Use the top-level definition of with.

---
 semantic-core/src/Data/Core/Pretty.hs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs
index ac59ea06f3..ecff6b0dfa 100644
--- a/semantic-core/src/Data/Core/Pretty.hs
+++ b/semantic-core/src/Data/Core/Pretty.hs
@@ -64,8 +64,8 @@ prettyCore style = run . runReader @Prec 0 . go (pure . name)
             Let a -> pure $ keyword "let" <+> name a
             a :>> b -> do
               prec <- ask @Prec
-              fore <- with 12 a
-              aft  <- with 12 b
+              fore <- with 12 (go var a)
+              aft  <- with 12 (go var b)
 
               let open  = symbol ("{" <> softline)
                   close = symbol (softline <> "}")
@@ -106,8 +106,7 @@ prettyCore style = run . runReader @Prec 0 . go (pure . name)
 
             -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
             Ann _ c -> go var c
-          where with n m = local (const (n :: Prec)) (go var m)
-                bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f)
+          where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f)
         lambda = case style of
           Unicode -> symbol "λ"
           Ascii   -> symbol "\\"

From e6e580d0a216bfedc02f24c55df7785d7ab547d7 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:30:20 -0400
Subject: [PATCH 04/13] Spacing.

---
 semantic-core/src/Data/Core/Pretty.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs
index ecff6b0dfa..57e70c7cb4 100644
--- a/semantic-core/src/Data/Core/Pretty.hs
+++ b/semantic-core/src/Data/Core/Pretty.hs
@@ -57,7 +57,7 @@ inParens amount go = do
 
 prettyCore :: Style -> Term Core User -> AnsiDoc
 prettyCore style = run . runReader @Prec 0 . go (pure . name)
-  where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) ->  Term Core a -> m AnsiDoc
+  where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) -> Term Core a -> m AnsiDoc
         go var = \case
           Var v -> var v
           Term t -> case t of

From 4cbc23b76de5874812f10b241ddb39afdc6e6eea Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:34:16 -0400
Subject: [PATCH 05/13] :fire: cata.

---
 semantic-core/src/Data/Term.hs | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/semantic-core/src/Data/Term.hs b/semantic-core/src/Data/Term.hs
index 0557116a13..fe93858d4b 100644
--- a/semantic-core/src/Data/Term.hs
+++ b/semantic-core/src/Data/Term.hs
@@ -3,15 +3,12 @@ module Data.Term
 ( Term(..)
 , Syntax(..)
 , iter
-, cata
 , interpret
 ) where
 
 import Control.Effect.Carrier
 import Control.Monad (ap)
 import Control.Monad.Module
-import Data.Coerce (coerce)
-import Data.Functor.Const
 import Data.Scope
 
 data Term sig a
@@ -79,15 +76,6 @@ iter var alg bound = go
           Var a -> var (free a)
           Term t -> alg (foldSyntax go bound free t)
 
-cata :: Syntax sig
-     => (a -> b)
-     -> (forall a . sig (Const b) a -> b)
-     -> (Incr () b -> a)
-     -> (x -> a)
-     -> Term sig x
-     -> b
-cata var alg k h = getConst . iter (coerce var) (Const . alg) (coerce k) (Const . h)
-
 
 interpret :: (Carrier sig m, Member eff sig, Syntax eff) => (forall a . Incr () (m a) -> m (Incr () (m a))) -> (a -> m b) -> Term eff a -> m b
 interpret = iter id send

From 97320176dc2a0f1a2554bef04763104863847f04 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:34:44 -0400
Subject: [PATCH 06/13] :fire: interpret.

---
 semantic-core/src/Data/Term.hs | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/semantic-core/src/Data/Term.hs b/semantic-core/src/Data/Term.hs
index fe93858d4b..fbaadf6e46 100644
--- a/semantic-core/src/Data/Term.hs
+++ b/semantic-core/src/Data/Term.hs
@@ -3,7 +3,6 @@ module Data.Term
 ( Term(..)
 , Syntax(..)
 , iter
-, interpret
 ) where
 
 import Control.Effect.Carrier
@@ -75,7 +74,3 @@ iter var alg bound = go
         go free = \case
           Var a -> var (free a)
           Term t -> alg (foldSyntax go bound free t)
-
-
-interpret :: (Carrier sig m, Member eff sig, Syntax eff) => (forall a . Incr () (m a) -> m (Incr () (m a))) -> (a -> m b) -> Term eff a -> m b
-interpret = iter id send

From aa1e36bc93c6852929827d78406aad95343f3f7c Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:37:19 -0400
Subject: [PATCH 07/13] Define stripAnnotations directly.

---
 semantic-core/src/Data/Core.hs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs
index 1bb9934af1..60697634ea 100644
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@@ -195,9 +195,10 @@ annWith callStack = maybe id (fmap send . Ann) (stackLoc callStack)
 
 
 stripAnnotations :: (Member Core sig, Syntax sig) => Term sig a -> Term sig a
-stripAnnotations = iter id alg Var Var
-  where alg t | Just c <- prj t, Ann _ b <- c = b
-              | otherwise                     = Term t
+stripAnnotations (Var v)  = Var v
+stripAnnotations (Term t)
+  | Just c <- prj t, Ann _ b <- c = b
+  | otherwise                     = Term (hmap stripAnnotations t)
 
 
 instance Syntax Core where

From 9eae24ecc16a2d22bf68b4f0e288b1d71e192340 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:39:20 -0400
Subject: [PATCH 08/13] Recur through annotations.

---
 semantic-core/src/Data/Core.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs
index 60697634ea..2453397ab2 100644
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@@ -197,7 +197,7 @@ annWith callStack = maybe id (fmap send . Ann) (stackLoc callStack)
 stripAnnotations :: (Member Core sig, Syntax sig) => Term sig a -> Term sig a
 stripAnnotations (Var v)  = Var v
 stripAnnotations (Term t)
-  | Just c <- prj t, Ann _ b <- c = b
+  | Just c <- prj t, Ann _ b <- c = stripAnnotations b
   | otherwise                     = Term (hmap stripAnnotations t)
 
 

From 2f8126875d66bbfc625e1db8af9fe8ef2234d617 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:41:04 -0400
Subject: [PATCH 09/13] Generalize stripAnnotations.

---
 semantic-core/src/Data/Core.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs
index 2453397ab2..be8ac5f5fa 100644
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@@ -194,7 +194,7 @@ annWith :: (Carrier sig m, Member Core sig) => CallStack -> m a -> m a
 annWith callStack = maybe id (fmap send . Ann) (stackLoc callStack)
 
 
-stripAnnotations :: (Member Core sig, Syntax sig) => Term sig a -> Term sig a
+stripAnnotations :: (Member Core sig, HFunctor sig, forall g . Functor g => Functor (sig g)) => Term sig a -> Term sig a
 stripAnnotations (Var v)  = Var v
 stripAnnotations (Term t)
   | Just c <- prj t, Ann _ b <- c = stripAnnotations b

From 49baa468f9413541544b6ea7c98c63f0fda724a8 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:43:25 -0400
Subject: [PATCH 10/13] :fire: iter.

---
 semantic-core/src/Data/Term.hs | 16 ----------------
 1 file changed, 16 deletions(-)

diff --git a/semantic-core/src/Data/Term.hs b/semantic-core/src/Data/Term.hs
index fbaadf6e46..e5ecf1ff5f 100644
--- a/semantic-core/src/Data/Term.hs
+++ b/semantic-core/src/Data/Term.hs
@@ -2,7 +2,6 @@
 module Data.Term
 ( Term(..)
 , Syntax(..)
-, iter
 ) where
 
 import Control.Effect.Carrier
@@ -59,18 +58,3 @@ instance Syntax (Scope ()) where
 instance (Syntax l, Syntax r) => Syntax (l :+: r) where
   foldSyntax go bound free (L l) = L (foldSyntax go bound free l)
   foldSyntax go bound free (R r) = R (foldSyntax go bound free r)
-
-
-iter :: forall m n sig a b
-     .  Syntax sig
-     => (forall a . m a -> n a)
-     -> (forall a . sig n a -> n a)
-     -> (forall a . Incr () (n a) -> m (Incr () (n a)))
-     -> (a -> m b)
-     -> Term sig a
-     -> n b
-iter var alg bound = go
-  where go :: forall x y . (x -> m y) -> Term sig x -> n y
-        go free = \case
-          Var a -> var (free a)
-          Term t -> alg (foldSyntax go bound free t)

From 2743895e782270f8dc617a38e0c03c85b091aca8 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:44:10 -0400
Subject: [PATCH 11/13] :fire: the Syntax instance for Core.

---
 semantic-core/src/Data/Core.hs | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs
index be8ac5f5fa..e3a6d8c270 100644
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@@ -199,21 +199,3 @@ stripAnnotations (Var v)  = Var v
 stripAnnotations (Term t)
   | Just c <- prj t, Ann _ b <- c = stripAnnotations b
   | otherwise                     = Term (hmap stripAnnotations t)
-
-
-instance Syntax Core where
-  foldSyntax go k h = \case
-    Let a -> Let a
-    a :>> b -> go h a :>> go h b
-    Lam u b -> Lam u (foldSyntax go k h b)
-    a :$ b -> go h a :$ go h b
-    Unit -> Unit
-    Bool b -> Bool b
-    If c t e -> If (go h c) (go h t) (go h e)
-    String s -> String s
-    Load t -> Load (go h t)
-    Edge e t -> Edge e (go h t)
-    Frame -> Frame
-    a :. b -> go h a :. go h b
-    a := b -> go h a := go h b
-    Ann loc t -> Ann loc (go h t)

From 70f67c0165dc3ed73a0738169c72711e2391bb7d Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:44:36 -0400
Subject: [PATCH 12/13] :fire: the Syntax class.

---
 semantic-core/src/Data/Term.hs | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/semantic-core/src/Data/Term.hs b/semantic-core/src/Data/Term.hs
index e5ecf1ff5f..caf2ac49c0 100644
--- a/semantic-core/src/Data/Term.hs
+++ b/semantic-core/src/Data/Term.hs
@@ -1,13 +1,11 @@
 {-# LANGUAGE DeriveTraversable, FlexibleInstances, LambdaCase, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeOperators, UndecidableInstances #-}
 module Data.Term
 ( Term(..)
-, Syntax(..)
 ) where
 
 import Control.Effect.Carrier
 import Control.Monad (ap)
 import Control.Monad.Module
-import Data.Scope
 
 data Term sig a
   = Var a
@@ -43,18 +41,3 @@ instance RightModule sig => Monad (Term sig) where
 
 instance RightModule sig => Carrier sig (Term sig) where
   eff = Term
-
-
-class (HFunctor sig, forall g . Functor g => Functor (sig g)) => Syntax sig where
-  foldSyntax :: (forall x y . (x -> m y) -> f x -> n y)
-             -> (forall a . Incr () (n a) -> m (Incr () (n a)))
-             -> (a -> m b)
-             -> sig f a
-             -> sig n b
-
-instance Syntax (Scope ()) where
-  foldSyntax go bound free = Scope . go (bound . fmap (go free)) . unScope
-
-instance (Syntax l, Syntax r) => Syntax (l :+: r) where
-  foldSyntax go bound free (L l) = L (foldSyntax go bound free l)
-  foldSyntax go bound free (R r) = R (foldSyntax go bound free r)

From 05a309745b756ad6842603f83ec918c6f9e70917 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Thu, 18 Jul 2019 14:45:30 -0400
Subject: [PATCH 13/13] Tidy up the language extensions.

---
 semantic-core/src/Data/Term.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/semantic-core/src/Data/Term.hs b/semantic-core/src/Data/Term.hs
index caf2ac49c0..f7e9695d9f 100644
--- a/semantic-core/src/Data/Term.hs
+++ b/semantic-core/src/Data/Term.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveTraversable, FlexibleInstances, LambdaCase, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-}
 module Data.Term
 ( Term(..)
 ) where