renamePrettily

whole-program inference

whole-program inference

whole-program inference

.ghci

@@ -1,5 +1,6 @@
 -- repl extensions
 :set -XOverloadedStrings
+:set -XQuasiQuotes
 
 --------------------------------------------------------------------------------
 

Makefile_happysrcs

@@ -1,19 +1,24 @@
+GHC_VERSION = $(shell ghc --numeric-version)
 HAPPY = happy
 HAPPY_OPTS = -a -g -c -i/tmp/t.info
 ALEX = alex
 ALEX_OPTS = -g
 
 SRC = src
-CABAL_BUILD = dist-newstyle/build/x86_64-osx/ghc-9.6.2/rlp-0.1.0.0/build
+CABAL_BUILD = $(shell ./find-build.clj)
 
 all: parsers lexers
 
-parsers: $(CABAL_BUILD)/Rlp/Parse.hs $(CABAL_BUILD)/Core/Parse.hs
+parsers: $(CABAL_BUILD)/Rlp/Parse.hs $(CABAL_BUILD)/Core/Parse.hs \
+		$(CABAL_BUILD)/Rlp/AltParse.hs
 lexers: $(CABAL_BUILD)/Rlp/Lex.hs $(CABAL_BUILD)/Core/Lex.hs
 
 $(CABAL_BUILD)/Rlp/Parse.hs: $(SRC)/Rlp/Parse.y
 	$(HAPPY) $(HAPPY_OPTS) $< -o $@
 
+$(CABAL_BUILD)/Rlp/AltParse.hs: $(SRC)/Rlp/AltParse.y
+	$(HAPPY) $(HAPPY_OPTS) $< -o $@
+
 $(CABAL_BUILD)/Rlp/Lex.hs: $(SRC)/Rlp/Lex.x
 	$(ALEX) $(ALEX_OPTS) $< -o $@
 

README.md

@@ -1,165 +0,0 @@
-# rl'
-
-`rlp` (ruelang') will be a lazily-evaluated purely-functional language heavily
-imitating Haskell.
-
-### Architecture
-
-![rlpc architecture diagram](/rlpc.drawio.svg)
-
-### Build Info
-* rlp is built using [Cabal](https://www.haskell.org/ghcup/)
-* rlp's documentation is built using [Sphinx](https://www.sphinx-doc.org/en/master/)
-
-```sh
-$ cabal build       # Build the rlpc compiler
-$ cabal install     # Install rlpc to $PATH
-$ cabal haddock     # Build the API docs w/ Haddock
-$ make -C doc html  # Build the primary docs w/ Sphinx
-
-# run the test suite
-$ cabal test --test-show-details=direct
-```
-
-### Use
-
-#### TLDR
-
-```sh
-# Compile and evaluate examples/rlp/QuickSort.rl
-$ rlpc examples/QuickSort.rl
-# Compile and evaluate t.cr, with evaluation info dumped to t.log
-$ rlpc -ddump-eval -l t.log t.cr
-# Compile and evaluate t.rl, dumping the desugared Core
-$ rlpc -ddump-desugared t.rl
-# Compile and evaluate t.rl with all compiler messages enabled
-$ rlpc -dALL t.rl
-```
-
-#### Options
-
-```sh
-Usage: rlpc [-l|--log FILE] [-d DEBUG FLAG] [-f COMPILATION FLAG] 
-            [-e|--evaluator gm|ti] [--heap-trigger INT] [-x|--language rlp|core]
-            FILES...
-```
-
-Available debug flags include:
-* `-ddump-desugared`: dump Core generated from rl'
-* `-ddump-parsed-core`: dump raw Core AST
-* `-ddump-parsed`: dump raw rl' AST
-* `-ddump-eval`: dump evaluation logs
-* `-dALL`: disable debug message filtering. enables **all** debug messages
-
-### Potential Features
-Listed in order of importance.
-- [x] ADTs
-- [x] First-class functions
-- [x] Higher-kinded types
-- [ ] Typeclasses
-- [x] Parametric polymorphism
-- [x] Hindley-Milner type inference
-- [ ] Newtype coercion
-- [ ] Parallelism
-
-### Milestones
-(This list is incomplete.)
-
-Items are marked off not as they are 100% implemented, but rather once I
-consider them stable enough that completion is soley a matter of getting
-around to it -- no tough design decisions, theorising, etc. remain. For
-example, as of writing this, the rl' frontend parser is not fully featured,
-yet it is marked off on this list; finishing it would require cranking out
-the remaining grammatical rules, and no work on complex tasks like layout
-parsing remains.
-
-- [ ] Backend
-    - [x] Core language
-        - [x] AST
-    - [x] Low-level execution model (TI)
-        - [x] Arithmetic
-        - [x] Conditionals
-        - [x] Structured data
-        - [x] Garbage collection
-    - [x] Low-level execution model (GM)
-        - [x] Arithmetic
-        - [x] Conditionals
-        - [x] Structured data
-        - [x] Garbage Collection
-    - [ ] Emitter
-        - [ ] Code-gen (target yet to be decided)
-    - [x] Core linter (Type-checker)
-    - [ ] Core2Core pass (optimisations and misc. preprocessing)
-        - [x] GM prep
-            - [x] Non-strict case-floating
-        - [ ] Let-floating
-        - [ ] TCO
-        - [ ] DCE
-- [ ] Frontend
-    - [x] High-level language
-        - [x] AST
-        - [x] Lexer
-        - [x] Parser
-    - [x] Translation to the core language
-        - [ ] Constraint solver
-        - [ ] `do`-notation
-    - [x] CLI
-- [ ] Documentation
-    - [x] State transition rules
-    - [ ] How does the evaluation model work?
-    - [ ] The Hindley-Milner type system
-    - [ ] CLI usage
-    - [ ] Tail call optimisation
-    - [ ] Parsing rlp
-    - [ ] Trees That Grow
-- [ ] Tests
-    - [x] Generic example programs
-    - [ ] Parser
-
-### ~~December Release Plan~~
-- [x] Tests
-    - [ ] Core lexer
-    - [ ] Core parser
-    - [x] Evaluation model
-- [ ] Benchmarks
-- [x] Stable Core lexer
-- [x] Stable Core parser
-- [x] Stable evaluation model
-    - [x] Garbage Collection
-- [ ] Stable documentation for the evaluation model
-
-### ~~February Release Plan~~
-- [x] Beta rl' to Core
-- [x] UX improvements
-    - [x] Actual compiler errors -- no more unexceptional `error` calls
-    - [x] Better CLI dump flags
-    - [x] Annotate the AST with token positions for errors (NOTE: As of Feb. 1,
-      this has been done, but the locational info is not yet used in error messages)
-- [x] Compiler architecture diagram
-- [x] More examples
-
-### March Release Plan
-- [ ] Tests
-    - [ ] rl' parser
-    - [ ] rl' lexer
-- [ ] Ditch TTG in favour of a simpler AST focusing on extendability via Fix, Free, 
-  Cofree, etc. rather than boilerplate-heavy type families
-
-### Indefinite Release Plan
-
-This list is more concrete than the milestones, but likely further in the future
-than the other release plans.
-
-- [ ] Overall codebase cleaning
-    - [ ] Complete all TODOs
-    - [ ] Replace mtl with effectful
-- [ ] rl' type-checker
-- [ ] Stable rl' to Core
-- [ ] Core polish
-    - [ ] Better, stable parser
-    - [ ] Better, stable lexer
-    - [ ] Less hacky handling of named data
-    - [ ] Less hacky pragmas
-- [ ] Choose a target. LLVM, JS, C, and WASM are currently top contenders
-- [ ] https://proglangdesign.net/wiki/challenges
-

README.org

@@ -0,0 +1,188 @@
+#+title: rl'
+#+author: Madeleine Sydney Slaga
+
+~rl'~ will be a lazily-evaluated, purely-functional, statically-typed language
+heavily imitating Haskell.
+
+* Architecture
+
+[[file:rlpc.drawio.svg]]
+
+* Build Info
+
+- ~rlpc~ is built using [[https://www.haskell.org/ghcup/][Cabal]]
+- ~rlpc~'s documentation is built using
+  [[https://www.sphinx-doc.org/en/master/][Sphinx]]
+
+#+BEGIN_SRC sh
+$ cabal build       # Build the rlpc compiler
+$ cabal install     # Install rlpc to $PATH
+$ cabal haddock     # Build the API docs w/ Haddock
+$ make -C doc html  # Build the primary docs w/ Sphinx
+
+# run the test suite
+$ cabal test --test-show-details=direct
+#+END_SRC
+
+* Use
+
+** TLDR
+#+begin_src sh
+# Compile and evaluate examples/rlp/QuickSort.rl
+$ rlpc examples/QuickSort.rl
+# Compile and evaluate t.cr, with evaluation info dumped to t.log
+$ rlpc -ddump-eval -l t.log t.cr
+# Compile and evaluate t.rl, dumping the desugared Core
+$ rlpc -ddump-desugared t.rl
+# Compile and evaluate t.rl with all compiler messages enabled
+$ rlpc -dALL t.rl
+#+end_src
+
+** Options
+#+begin_src sh
+Usage: rlpc [-l|--log FILE] [-d DEBUG FLAG] [-f COMPILATION FLAG]
+            [-e|--evaluator gm|ti] [--heap-trigger INT] [-x|--language rlp|core]
+            FILES...
+#+end_src
+
+Available debug flags include:
+- ~-ddump-desugared~: dump Core generated from rl'
+- ~-ddump-parsed-core~: dump raw Core AST
+- ~-ddump-parsed~: dump raw rl' AST
+- ~-ddump-eval~: dump evaluation logs
+- ~-dALL~: disable debug message filtering. enables *all* debug messages
+
+* Demos
+
+[TODO: add hmvis video here]
+
+* To-do List
+
+** TODO rlp to core desugaring                                         :feature:
+
+** DONE [#A] HM memoisation prevents shadowing                             :bug:
+   CLOSED: [2024-04-04 Thu 12:29]
+Example:
+#+begin_src haskell
+-- >>> runHM' $ infer1 [rlpExpr|let f = \x -> x in f (let f = 2 in f)|]
+-- Left [TyErrCouldNotUnify
+--         (ConT "Int#")
+--         (AppT (AppT FunT (ConT "Int#")) (VarT "$a2"))]
+-- >>> :t let f = \x -> x in f (let f = 2 in f)
+-- let f = \x -> x in f (let f = 2 in f) :: Int
+#+end_src
+For the time being, I just disabled the memoisation. This is very, very bad.
+*** Closing Remarks
+    Fixed by entirely rewriting the type inference algorithm :P. Memoisation is
+    no longer required; the bottom-up inference a la Algorithm M was previously
+    hacked together using a comonadic extend with a catamorphism, which, for each
+    node, would fold the entire subtree and memoise the result, which would then
+    be retrieved when parent nodes attempted to infer children nodes. This sucks!
+    It's not "bottom-up" at all! I replaced it with a gorgeous hand-rolled
+    recursion scheme which truly works from the bottom upwards. A bonus
+    specialisation is that it annotates each node with the result of a
+    catamorphism from that node downwards via the cofree comonad.
+    #+begin_src haskell
+    dendroscribe :: (Functor f, Base t ~ f, Recursive t)
+                => (f (Cofree f a) -> a) -> t -> Cofree f a
+    dendroscribe c (project -> f) = c f' :< f'
+         where f' = dendroscribe c <$> f
+
+    dendroscribeM :: (Traversable f, Monad m, Base t ~ f, Recursive t)
+                  => (f (Cofree f a) -> m a) -> t -> m (Cofree f a)
+    dendroscribeM c (project -> f) = do
+         as <- dendroscribeM c `traverse` f
+         a <- c as
+         pure (a :< as)
+    #+end_src
+
+** DONE README.md -> README.org                                           :docs:
+   CLOSED: [2024-03-28 Thu 10:44]
+
+** TODO ~case~ inference                                               :feature:
+
+** DONE ADT support in Rlp/HindleyMilner.hs                            :feature:
+   CLOSED: [2024-03-28 Thu 11:55]
+
+** DONE whole-program inference (wrap top-level in a ~letrec~)         :feature:
+   CLOSED: [2024-04-04 Thu 12:42]
+   shadowing issue sucks. i'm going to have to rewrite the whole type inference
+   system later. and i never learn, so i'm gonna use a chronomorphism :3.
+*** Closing Remarks
+    I don't know how a fucking chronomorphism works. None of the experts can
+    think of a single example of how to use it. The rewrite uses a bottom-up
+    recursion scheme I've dubbed ~dendroscribe~.
+
+** TODO user-supplied annotation support in Rlp/HindleyMilner.hs       :feature:
+
+** TODO update architecture diagram                                       :docs:
+
+** TODO pattern support; everywhere [0%]                                :feature:
+   - [ ] in the type-checker
+   - [ ] in the desugarer
+
+** TODO G-machine visualiser                                              :docs:
+
+** TODO lambda calculus visualiser                                        :docs:
+
+** TODO hmvis does not reload when redefining expressions                  :bug:
+   To recreate:
+   1. enter
+      #+begin_src haskell
+      x = 2
+      #+end_src
+   2. hit "type-check"
+   3. edit source to
+      #+begin_src haskell
+      x = \x -> x
+      #+end_src
+   4. hit "type-check"
+
+** DONE in Rlp/HindleyMilner.hs, fix ~listenFreshTvNames~         :housekeeping:
+   CLOSED: [2024-04-04 Thu 13:17]
+   it /does/ work in its current state, however it captures an unreasonably
+   excessive amount of names, even for a heuristic.
+*** Closing Remarks
+    Fixed with the proper Algorithm M rewrite. The original purpose of
+    ~listenFreshTvNames~ (tracking monomorphic type variables) has been solved
+    much more cleanly via the (non-monadic!) ~monomorphise~ function paired with
+    the new ~ImplicitInstance~ constraint.
+
+** TODO up-to-date examples [0/2]                                         :docs:
+- [ ] quicksort (core and rlp)
+- [ ] factorial (core and rlp)
+
+* Releases
+
+** +December Release+
+- [X] Tests
+    - [ ] Core lexer
+    - [ ] Core parser
+    - [X] Evaluation model
+- [ ] Benchmarks
+- [X] Stable Core lexer
+- [X] Stable Core parser
+- [X] Stable evaluation model
+    - [X] Garbage Collection
+- [ ] Stable documentation for the evaluation model
+
+** +February Release Plan+
+- [X] Beta rl' to Core
+- [X] UX improvements
+    - [X] Actual compiler errors -- no more unexceptional `error` calls
+    - [X] Better CLI dump flags
+    - [X] Annotate the AST with token positions for errors (NOTE: As of Feb. 1,
+      this has been done, but the locational info is not yet used in error messages)
+- [X] Compiler architecture diagram
+- [X] More examples
+
+** March Release Plan
+- [ ] Tests
+    - [ ] rl' parser
+    - [ ] Type inference
+- [X] Ditch TTG in favour of a simpler AST focusing on extendability via Fix, Free, 
+  Cofree, etc. rather than boilerplate-heavy type families
+- [X] rl' type inference
+- [X] Core type checking
+
+

app/CoreDriver.hs

@@ -10,15 +10,17 @@ import Control.Lens.Combinators
 
 import Core.Lex
 import Core.Parse
+import Core.SystemF
 import GM
 --------------------------------------------------------------------------------
 
 driver :: RLPCIO ()
 driver = forFiles_ $ \f ->
-    withSource f (lexCoreR >=> parseCoreProgR >=> evalProgR)
+    withSource f (lexCoreR >=> parseCoreProgR >=> lintCoreProgR >=> evalProgR)
 
 driverSource :: T.Text -> RLPCIO ()
-driverSource = lexCoreR >=> parseCoreProgR >=> evalProgR >=> printRes
+driverSource = lexCoreR >=> parseCoreProgR
+           >=> lintCoreProgR >=> evalProgR >=> printRes
     where
         printRes = liftIO . print . view _1
 

app/Main.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Main where
 ----------------------------------------------------------------------------------
+import Control.Lens             hiding (argument)
 import Compiler.RLPC
 import Compiler.RlpcError
 import Control.Exception
@@ -23,6 +24,7 @@ import Control.Lens.Combinators hiding (argument)
 
 import CoreDriver               qualified
 import RlpDriver                qualified
+import Server                   qualified
 ----------------------------------------------------------------------------------
 
 optParser :: ParserInfo RLPCOptions
@@ -74,7 +76,11 @@ options = RLPCOptions
         <> metavar "rlp|core"
         <> help "the language to be compiled -- see README"
         )
-    <*> some (argument str $ metavar "FILES...")
+    <*> switch
+        (  long "server"
+        <> short 's'
+        )
+    <*> many (argument str $ metavar "FILES...")
     where
         infixr 9 #
         f # x = f x
@@ -107,7 +113,9 @@ mmany v = liftA2 (<>) v (mmany v)
 main :: IO ()
 main = do
     opts <- execParser optParser
-    void $ evalRLPCIO opts dispatch
+    if opts ^. rlpcServer
+    then Server.server
+    else void $ evalRLPCIO opts dispatch
 
 dispatch :: RLPCIO ()
 dispatch = getLang >>= \case

app/RlpDriver.hs

@@ -15,5 +15,5 @@ import GM
 
 driver :: RLPCIO ()
 driver = forFiles_ $ \f ->
-    withSource f (parseRlpProgR >=> desugarRlpProgR >=> evalProgR)
+    withSource f (parseRlpProgR >=> undefined >=> desugarRlpProgR >=> evalProgR)
 

app/Server.hs

@@ -0,0 +1,115 @@
+{-# LANGUAGE LambdaCase, BlockArguments #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE OverloadedStrings #-}
+module Server
+    ( server
+    )
+    where
+--------------------------------------------------------------------------------
+import GHC.Generics                 (Generic, Generically(..))
+import Data.Text.Encoding           qualified as T
+import Data.Text                    (Text)
+import Data.Text                    qualified as T
+import Data.Text.IO                 qualified as T
+import Data.Pretty                  hiding (annotate)
+import Data.Aeson
+import Data.Function
+import Control.Arrow
+import Control.Applicative
+import Control.Monad
+import Control.Concurrent
+import Network.WebSockets           qualified as WS
+import Control.Exception
+import GHC.IO
+import Control.Lens                 hiding ((.=))
+
+import Control.Comonad
+import Data.Functor.Foldable
+
+import Compiler.RLPC
+
+import Misc.CofreeF
+import Rlp.AltSyntax
+import Rlp.HindleyMilner
+import Rlp.AltParse
+--------------------------------------------------------------------------------
+
+server :: IO ()
+server = do
+    T.putStrLn "rlpc server started at 127.0.0.1:9002"
+    WS.runServer "127.0.0.1" 9002 application
+
+application :: WS.ServerApp
+application pending = do
+    WS.acceptRequest pending >>= talk
+
+data Command = Annotate Text
+             | PartiallyAnnotate Text
+    deriving Show
+
+instance FromJSON Command where
+    parseJSON = withObject "command object" $ \v -> do
+        cmd :: Text <- v .: "command"
+        case cmd of
+            "annotate"           -> Annotate <$> v .: "source"
+            "partially-annotate" -> PartiallyAnnotate <$> v .: "source"
+            _          -> empty
+
+data Response = Annotated Value
+              | PartiallyAnnotated Value
+    deriving (Generic)
+    deriving (ToJSON)
+        via Generically Response
+
+talk :: WS.Connection -> IO ()
+talk conn = (`catchAny` print) . forever $ do
+    msg <- WS.receiveData @Text conn
+    T.putStrLn $ "received: " <> msg
+    doCommand conn `traverse` decodeStrictText msg
+
+doCommand :: WS.Connection -> Command -> IO ()
+doCommand conn c = do
+    putStr "sending: "
+    let r = encode . respond $ c
+    print r
+    WS.sendTextData conn r
+
+respond :: Command -> Response
+respond (Annotate s)
+    = s & (parseRlpProgR >=> typeCheckRlpProgR)
+        & fmap (\p -> p ^.. funDs
+           <&> serialiseSc)
+        & runRLPCJsonDef
+        & Annotated
+
+showPartialAnn = undefined
+
+funDs :: Traversal' (Program b a) (b, [Pat b], a)
+funDs = programDecls . each . _FunD
+
+serialiseSc :: (PsName, [Pat PsName], Cofree (RlpExprF PsName) (Type PsName))
+            -> Value
+serialiseSc (n,as,e) = object
+    [ "name" .= n
+    , "args" .= as
+    , "body" .= let root = extract e
+                in serialiseAnnotated (e <&> renamePrettily root)
+    ]
+
+serialiseAnnotated :: Cofree (RlpExprF PsName) (Type PsName)
+                   -> Value
+serialiseAnnotated = cata \case
+    t :<$ e -> object [ "e" .= e, "type" .= rout @Text t ]
+
+runRLPCJsonWithDef :: (a -> Value) -> RLPC a -> Value
+runRLPCJsonWithDef f = runRLPCJsonWith f def
+
+runRLPCJsonDef :: (ToJSON a) => RLPC a -> Value
+runRLPCJsonDef = runRLPCJsonWith toJSON def
+
+runRLPCJsonWith :: (a -> Value) -> RLPCOptions -> RLPC a -> Value
+runRLPCJsonWith f o r = object
+    [ "errors" .= es
+    , "result" .= (f <$> ma) ]
+  where (ma,es) = evalRLPC o r
+

examples/Core/factorial.cr

@@ -1,7 +1,9 @@
+fac : Int# -> Int#
 fac n = case (==#) n 0 of
     { <1> -> 1
     ; <0> -> *# n (fac (-# n 1))
     };
 
+main : IO ()
 main = fac 3;
 

find-build.clj

@@ -0,0 +1,13 @@
+#!/usr/bin/env bb
+
+(defn die [& msgs]
+  (binding [*out* *err*]
+    (run! println msgs))
+  (System/exit 1))
+
+(let [paths (map str (fs/glob "." "dist-newstyle/build/*/*/rlp-*/build"))
+      n (count paths)]
+  (cond (< 1 n) (die ">1 build directories found. run `cabal clean`.")
+        (< n 1) (die "no build directories found. this shouldn't happen lol")
+        :else   (-> paths first fs/real-path str println)))
+

rlp.cabal

@@ -16,6 +16,7 @@ tested-with:        GHC==9.6.2
 
 common warnings
 --    ghc-options: -Wall -Wno-incomplete-uni-patterns -Wno-unused-top-binds
+    ghc-options: -fdefer-typed-holes
 
 library
     import:           warnings
@@ -32,6 +33,13 @@ library
                     , Core.HindleyMilner
                     , Control.Monad.Errorful
                     , Rlp.Syntax
+                    , Rlp.AltSyntax
+                    , Rlp.AltParse
+                    , Rlp.HindleyMilner
+                    , Rlp.HindleyMilner.Visual
+                    , Rlp.HindleyMilner.Types
+                    , Rlp.Syntax.Backstage
+                    , Rlp.Syntax.Types
                     -- , Rlp.Parse.Decls
                     , Rlp.Parse
                     , Rlp.Parse.Associate
@@ -42,10 +50,15 @@ library
                     , Data.Heap
                     , Data.Pretty
                     , Core.Parse
+                    , Core.Parse.Types
                     , Core.Lex
                     , Core2Core
                     , Rlp2Core
                     , Control.Monad.Utils
+                    , Misc
+                    , Misc.Lift1
+                    , Misc.CofreeF
+                    , Core.SystemF
 
     build-tool-depends: happy:happy, alex:alex
 
@@ -54,13 +67,14 @@ library
                     -- required for happy
                     , array >= 0.5.5 && < 0.6
                     , containers >= 0.6.7 && < 0.7
-                    , template-haskell >= 2.20.0 && < 2.23
+                    , template-haskell >= 2.20.0 && < 2.22
-                    , pretty >= 1.1.3 && < 1.2
+                    , prettyprinter
                     , data-default >= 0.7.1 && < 0.8
                     , data-default-class >= 0.1.2 && < 0.2
                     , hashable >= 1.4.3 && < 1.5
                     , mtl >= 2.3.1 && < 2.4
-                    , text >= 2.0.2 && < 2.3
+                    , transformers
+                    , text >= 2.0.2 && < 2.2
                     , unordered-containers >= 0.2.20 && < 0.3
                     , recursion-schemes >= 5.2.2 && < 5.3
                     , data-fix >= 0.3.2 && < 0.4
@@ -73,6 +87,10 @@ library
                     , effectful-core ^>=2.3.0.0
                     , deriving-compat ^>=0.6.0
                     , these >=0.2 && <2.0
+                    , free >=5.2
+                    , bifunctors >=5.2
+                    , aeson >=2.2.1.0 && <2.3.1.0
+                    , lens-aeson
 
     hs-source-dirs:   src
     default-language: GHC2021
@@ -86,12 +104,14 @@ library
         DerivingVia
         StandaloneDeriving
         DerivingStrategies
+        BlockArguments
 
 executable rlpc
     import:           warnings
     main-is:          Main.hs
     other-modules:    RlpDriver
                     , CoreDriver
+                    , Server
 
     build-depends: base >=4.17.0.0 && <4.20.0.0
                  , rlp
@@ -99,7 +119,11 @@ executable rlpc
                  , mtl >= 2.3.1 && < 2.4
                  , unordered-containers >= 0.2.20 && < 0.3
                  , lens >=5.2.3 && <6.0
-                 , text >= 2.0.2 && < 2.3
+                 , text >= 2.0.2 && < 2.2
+                 , websockets
+                 , aeson
+                 , recursion-schemes >= 5.2.2 && < 5.3
+                 , comonad
 
     hs-source-dirs:   app
     default-language: GHC2021
@@ -116,8 +140,10 @@ test-suite rlp-test
                  , QuickCheck
                  , hspec            ==2.*
                  , microlens
+                 , lens >=5.2.3 && <6.0
     other-modules: Arith
                  , GMSpec
                  , Core.HindleyMilnerSpec
+                 , Compiler.TypesSpec
     build-tool-depends: hspec-discover:hspec-discover
 

src/Compiler/JustRun.hs

@@ -10,15 +10,17 @@ types such as @RLPC@ or @Text@.
 module Compiler.JustRun
     ( justLexCore
     , justParseCore
+    , justParseRlp
     , justTypeCheckCore
     , justHdbg
+    , makeItPretty, makeItPretty'
     )
     where
 ----------------------------------------------------------------------------------
 import Core.Lex
 import Core.Parse
 import Core.HindleyMilner
-import Core.Syntax                      (Program')
+import Core.Syntax
 import Compiler.RLPC
 import Control.Arrow                    ((>>>))
 import Control.Monad                    ((>=>), void)
@@ -28,30 +30,47 @@ import Data.Text                        qualified as T
 import Data.Function                    ((&))
 import System.IO
 import GM
-import Rlp.Parse
 import Rlp2Core
+import Data.Pretty
+
+import Rlp.AltParse
+import Rlp.AltSyntax                    qualified as Rlp
 ----------------------------------------------------------------------------------
 
 justHdbg :: String -> IO GmState
-justHdbg s = do
+justHdbg = undefined
-    p <- evalRLPCIO def (parseRlpProgR >=> desugarRlpProgR $ T.pack s)
+-- justHdbg s = do
-    withFile "/tmp/t.log" WriteMode $ hdbgProg p
+--     p <- evalRLPCIO def (parseRlpProgR >=> desugarRlpProgR $ T.pack s)
+--     withFile "/tmp/t.log" WriteMode $ hdbgProg p
 
 justLexCore :: String -> Either [MsgEnvelope RlpcError] [CoreToken]
 justLexCore s = lexCoreR (T.pack s)
               & mapped . each %~ extract
               & rlpcToEither
 
-justParseCore :: String -> Either [MsgEnvelope RlpcError] Program'
+justParseCore :: String -> Either [MsgEnvelope RlpcError] (Program Var)
 justParseCore s = parse (T.pack s)
                 & rlpcToEither
-    where parse = lexCoreR >=> parseCoreProgR
+    where parse = lexCoreR @Identity >=> parseCoreProgR
+
+justParseRlp :: String
+             -> Either [MsgEnvelope RlpcError]
+                       (Rlp.Program Name (Rlp.RlpExpr Name))
+justParseRlp s = parse (T.pack s)
+               & rlpcToEither
+    where parse = parseRlpProgR @Identity
 
 justTypeCheckCore :: String -> Either [MsgEnvelope RlpcError] Program'
 justTypeCheckCore s = typechk (T.pack s)
                     & rlpcToEither
     where typechk = lexCoreR >=> parseCoreProgR >=> checkCoreProgR
 
+makeItPretty :: (Out a) => Either e a -> Either e (Doc ann)
+makeItPretty = fmap out
+
+makeItPretty' :: (Out (WithTerseBinds a)) => Either e a -> Either e (Doc ann)
+makeItPretty' = fmap (out . WithTerseBinds)
+
 rlpcToEither :: RLPC a -> Either [MsgEnvelope RlpcError] a
 rlpcToEither r = case evalRLPC def r of
     (Just a,   _) -> Right a

src/Compiler/RLPC.hs

@@ -26,8 +26,9 @@ module Compiler.RLPC
     , DebugFlag(..), CompilerFlag(..)
     -- ** Lenses
     , rlpcLogFile, rlpcDFlags, rlpcEvaluator, rlpcInputFiles, rlpcLanguage
+    , rlpcServer
     -- * Misc. MTL-style functions
-    , liftErrorful, hoistRlpcT
+    , liftErrorful, liftEither, liftMaybe, hoistRlpcT
     -- * Misc. Rlpc Monad -related types
     , RLPCOptions(RLPCOptions), IsRlpcError(..), RlpcError(..)
     , MsgEnvelope(..), Severity(..)
@@ -54,6 +55,7 @@ import Data.Default.Class
 import Data.Foldable
 import GHC.Generics             (Generic)
 import Data.Maybe
+import Data.Pretty
 import Data.Hashable            (Hashable)
 import Data.HashSet             (HashSet)
 import Data.HashSet             qualified as S
@@ -63,7 +65,6 @@ import Data.Text                qualified as T
 import Data.Text.IO             qualified as T
 import System.IO
 import Text.ANSI                qualified as Ansi
-import Text.PrettyPrint         hiding ((<>))
 import Control.Lens
 import Data.Text.Lens           (packed, unpacked, IsText)
 import System.Exit
@@ -108,6 +109,16 @@ evalRLPCT opt r = runRLPCT r
 liftErrorful :: (Monad m, IsRlpcError e) => ErrorfulT (MsgEnvelope e) m a -> RLPCT m a
 liftErrorful e = RLPCT $ lift (fmap liftRlpcError `mapErrorful` e)
 
+liftMaybe :: (Monad m) => Maybe a -> RLPCT m a
+liftMaybe m = RLPCT . lift . ErrorfulT . pure $ (m, [])
+
+liftEither :: (Monad m, IsRlpcError e)
+           => Either [e] a -> RLPCT m a
+liftEither = RLPCT . lift . ErrorfulT . pure . f where
+    f (Left es) = (Nothing, errorMsg s . liftRlpcError <$> es)
+        where s = SrcSpan 0 0 0 0
+    f (Right a) = (Just a, [])
+
 hoistRlpcT :: (forall a. m a -> n a)
          -> RLPCT m a -> RLPCT n a
 hoistRlpcT f rma = RLPCT $ ReaderT $ \opt ->
@@ -120,6 +131,7 @@ data RLPCOptions = RLPCOptions
     , _rlpcEvaluator   :: Evaluator
     , _rlpcHeapTrigger :: Int
     , _rlpcLanguage    :: Maybe Language
+    , _rlpcServer      :: Bool
     , _rlpcInputFiles  :: [FilePath]
     }
     deriving Show
@@ -140,6 +152,7 @@ instance Default RLPCOptions where
         , _rlpcEvaluator = EvaluatorGM
         , _rlpcHeapTrigger = 200
         , _rlpcInputFiles = []
+        , _rlpcServer = False
         , _rlpcLanguage = Nothing
         }
 
@@ -200,7 +213,7 @@ renderRlpcErrs opts = (if don'tBother then id else filter byTag)
 
 prettyRlpcMsg :: MsgEnvelope RlpcError -> String
 prettyRlpcMsg m@(view msgSeverity -> SevDebug _) = prettyRlpcDebugMsg m
-prettyRlpcMsg m                                  = render $ docRlpcErr m
+prettyRlpcMsg m                                  = show $ docRlpcErr m
 
 prettyRlpcDebugMsg :: MsgEnvelope RlpcError -> String
 prettyRlpcDebugMsg msg =
@@ -210,29 +223,28 @@ prettyRlpcDebugMsg msg =
         Text ts = msg ^. msgDiagnostic
         SevDebug tag = msg ^. msgSeverity
 
-docRlpcErr :: MsgEnvelope RlpcError -> Doc
+docRlpcErr :: MsgEnvelope RlpcError -> Doc ann
-docRlpcErr msg = header
+docRlpcErr msg = vcat [ header
-                 $$ nest 2 bullets
+                      , nest 2 bullets
-                 $$ source
+                      , source ]
     where
         source = vcat $ zipWith (<+>) rule srclines
             where
                 rule = repeat (ttext . Ansi.blue . Ansi.bold $ "|")
                 srclines = ["", "<problematic source code>", ""]
         filename = msgColour "<input>"
-        pos = msgColour $ tshow (msg ^. msgSpan . srcspanLine)
+        pos = msgColour $ tshow (msg ^. msgSpan . srcSpanLine)
                        <> ":"
-                       <> tshow (msg ^. msgSpan . srcspanColumn)
+                       <> tshow (msg ^. msgSpan . srcSpanColumn)
 
         header = ttext $ filename <> msgColour ":" <> pos <> msgColour ": "
                         <> errorColour "error" <> msgColour ":"
 
         bullets = let Text ts = msg ^. msgDiagnostic
-                  in vcat $ hang "•" 2 . ttext . msgColour <$> ts
+                  in vcat $ ("•" <>) . hang 2 . ttext . msgColour <$> ts
 
         msgColour = Ansi.white . Ansi.bold
         errorColour = Ansi.red . Ansi.bold
-        ttext = text . T.unpack
         tshow :: (Show a) => a -> Text
         tshow = T.pack . show
 

src/Compiler/RlpcError.hs

@@ -14,6 +14,9 @@ module Compiler.RlpcError
     -- * Located Comonad
     , Located(..)
     , SrcSpan(..)
+
+    -- * Common error messages
+    , undefinedVariableErr
     )
     where
 ----------------------------------------------------------------------------------
@@ -21,8 +24,11 @@ import Control.Monad.Errorful
 import Data.Text                (Text)
 import Data.Text                qualified as T
 import GHC.Exts                 (IsString(..))
-import Control.Lens
+import GHC.Generics
+import Control.Lens             hiding ((.=))
 import Compiler.Types
+
+import Data.Aeson
 ----------------------------------------------------------------------------------
 
 data MsgEnvelope e = MsgEnvelope
@@ -32,8 +38,17 @@ data MsgEnvelope e = MsgEnvelope
    }
    deriving (Functor, Show)
 
+instance (ToJSON e) => ToJSON (MsgEnvelope e) where
+    toJSON msg = object
+        [ "span" .= _msgSpan msg
+        , "severity" .= _msgSeverity msg
+        , "diagnostic" .= _msgDiagnostic msg
+        ]
+
 newtype RlpcError = Text [Text]
-               deriving Show
+    deriving (Show, Generic)
+    deriving (ToJSON)
+        via Generically [Text]
 
 instance IsString RlpcError where
     fromString = Text . pure . T.pack
@@ -47,7 +62,9 @@ instance IsRlpcError RlpcError where
 data Severity = SevWarning
               | SevError
               | SevDebug Text -- ^ Tag
-              deriving Show
+              deriving (Show, Generic)
+              deriving (ToJSON)
+                via Generically Severity
 
 makeLenses ''MsgEnvelope
 
@@ -74,3 +91,8 @@ debugMsg tag e = MsgEnvelope
     , _msgSeverity = SevDebug tag
     }
 
+undefinedVariableErr :: Text -> RlpcError
+undefinedVariableErr n = Text
+    [ "Variable not in scope: `" <> n <> "'."
+    ]
+

src/Compiler/Types.hs

@@ -1,33 +1,84 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances, QuantifiedConstraints #-}
+{-# LANGUAGE PatternSynonyms #-}
 module Compiler.Types
     ( SrcSpan(..)
-    , srcspanLine, srcspanColumn, srcspanAbs, srcspanLen
+    , srcSpanLine, srcSpanColumn, srcSpanAbs, srcSpanLen
+    , pattern (:<$)
     , Located(..)
+    , HasLocation(..)
     , _Located
-    , located
+    , nolo, nolo'
-    , nolo
+
-    , (<<~), (<~>), (<#>)
+    , (<~>), (~>), (~~>), (<~~)
+
+    , comb2, comb3, comb4
+    , lochead
 
     -- * Re-exports
-    , Comonad
+    , Comonad(extract)
     , Apply
     , Bind
     )
     where
 --------------------------------------------------------------------------------
+import Language.Haskell.TH.Syntax   (Lift)
+
 import Control.Comonad
+import Control.Comonad.Cofree
 import Data.Functor.Apply
 import Data.Functor.Bind
-import Control.Lens             hiding ((<<~))
+import Data.Functor.Compose
-import Language.Haskell.TH.Syntax   (Lift)
+import Data.Functor.Foldable
+import Data.Semigroup.Foldable
+import Data.Fix                     hiding (cata, ana)
+
+import Data.Kind
+import Data.Aeson
+import Control.Lens                 hiding ((<<~), (:<), (.=))
+
+import Data.List.NonEmpty           (NonEmpty)
+import Data.Function                (on)
+import Misc.CofreeF
 --------------------------------------------------------------------------------
 
 -- | Token wrapped with a span (line, column, absolute, length)
 data Located a = Located SrcSpan a
     deriving (Show, Lift, Functor)
 
-located :: Lens (Located a) (Located b) a b
+instance ToJSON SrcSpan where
-located = lens extract ($>)
+    toJSON (SrcSpan l c a s) = object
+        [ "line" .= l
+        , "column" .= c
+        , "abs" .= a
+        , "length" .= s]
+
+(<~>) :: a -> b -> SrcSpan
+(<~>) = undefined
+
+infixl 5 <~>
+
+(~>) :: (CanGet k, CanSet k', HasLocation k a, HasLocation k' b)
+     => a -> b -> b
+a ~> b = b & fromSet getSetLocation .~ (a ^. fromGet getSetLocation)
+-- (~>) = undefined
+
+infixl 4 ~>
+
+-- (~~>) :: (CanGet k, HasLocation k a, CanSet k', HasLocation k' b)
+--       => (a -> b) -> a -> b
+-- (~~>) :: (f SrcSpan -> b) -> Cofree f SrcSpan -> Cofree f SrcSpan
+-- f ~~> (ss :< as) = ss :< f as
+(~~>) = undefined
+
+infixl 3 ~~>
+
+-- (<~~) :: (GetLocation a, HasLocation b) => (a -> b) -> a -> b
+-- a <~~ b = a b & location <>~ srcspan b
+(<~~) = undefined
+
+infixr 2 <~~
 
 instance Apply Located where
     liftF2 f (Located sa p) (Located sb q)
@@ -47,53 +98,137 @@ data SrcSpan = SrcSpan
     !Int -- ^ Column
     !Int -- ^ Absolute
     !Int -- ^ Length
-    deriving (Show, Lift)
+    deriving (Show, Eq, Lift)
 
-tupling :: Iso' SrcSpan (Int, Int, Int, Int)
+_SrcSpan :: Iso' SrcSpan (Int, Int, Int, Int)
-tupling = iso (\ (SrcSpan a b c d) -> (a,b,c,d))
+_SrcSpan = iso (\ (SrcSpan a b c d) -> (a,b,c,d))
               (\ (a,b,c,d) -> SrcSpan a b c d)
 
-srcspanLine, srcspanColumn, srcspanAbs, srcspanLen :: Lens' SrcSpan Int
+srcSpanLine, srcSpanColumn, srcSpanAbs, srcSpanLen :: Lens' SrcSpan Int
-srcspanLine = tupling . _1
+srcSpanLine = _SrcSpan . _1
-srcspanColumn = tupling . _2
+srcSpanColumn = _SrcSpan . _2
-srcspanAbs = tupling . _3
+srcSpanAbs = _SrcSpan . _3
-srcspanLen = tupling . _4
+srcSpanLen = _SrcSpan . _4
 
 -- | debug tool
 nolo :: a -> Located a
 nolo = Located (SrcSpan 0 0 0 0)
 
+nolo' :: f (Cofree f SrcSpan) -> Cofree f SrcSpan
+nolo' as = SrcSpan 0 0 0 0 :< as
+
 instance Semigroup SrcSpan where
+    -- multiple identities? what are the consequences of this...?
+    SrcSpan _ _ _ 0 <> SrcSpan l c a s = SrcSpan l c a s
+    SrcSpan l c a s <> SrcSpan _ _ _ 0 = SrcSpan l c a s
+
     SrcSpan la ca aa sa <> SrcSpan lb cb ab sb = SrcSpan l c a s where
         l = min la lb
         c = min ca cb
         a = min aa ab
         s = case aa `compare` ab of
             EQ -> max sa sb
-            LT -> max sa (ab + lb - aa)
+            LT -> max sa (ab + sb - aa)
-            GT -> max sb (aa + la - ab)
+            GT -> max sb (aa + sa - ab)
 
--- | A synonym for '(<<=)' with a tighter precedence and left-associativity for
+--------------------------------------------------------------------------------
--- use with '(<~>)' in a sort of, comonadic pseudo-applicative style.
 
-(<<~) :: (Comonad w) => (w a -> b) -> w a -> w b
+data GetOrSet = Get | Set | GetSet
-(<<~) = (<<=)
 
-infixl 4 <<~
+class CanGet (k :: GetOrSet)
+class CanSet (k :: GetOrSet) where
 
--- | Similar to '(<*>)', but with a cokleisli arrow.
+instance CanGet Get
+instance CanGet GetSet
+instance CanSet Set
+instance CanSet GetSet
 
-(<~>) :: (Comonad w, Bind w) => w (w a -> b) -> w a -> w b
+data GetSetLens (k :: GetOrSet) s t a b :: Type where
-mc <~> ma = mc >>- \f -> ma =>> f
+    Getter_      :: (s -> a)             -> GetSetLens Get s t a b
+    Setter_      :: ((a -> b) -> s -> t) -> GetSetLens Set s t a b
+    GetterSetter :: (CanGet k', CanSet k')
+                 => (s -> a) -> (s -> b -> t) -> GetSetLens k' s t a b
 
-infixl 4 <~>
+type GetSetLens' k s a = GetSetLens k s s a a
 
--- this is getting silly
+class HasLocation k s | s -> k where
+    -- location :: (Access k f, Functor f) => LensLike' f s SrcSpan
+    getSetLocation :: GetSetLens' k s SrcSpan
 
-(<#>) :: (Functor f) => f (a -> b) -> a -> f b
+type family Access (k :: GetOrSet) f where
-fab <#> a = fmap ($ a) fab
+    Access GetSet f = Functor f
+    Access Set f = Settable f
+    Access Get f = (Functor f, Contravariant f)
 
-infixl 4 <#>
+instance HasLocation GetSet SrcSpan where
+    getSetLocation = GetterSetter id (flip const)
+    -- location = fromGetSetLens getSetLocation
+
+instance (CanSet k, HasLocation k a) => HasLocation Set (r -> a) where
+    getSetLocation = Setter_ $ \ss ra r -> ra r & fromSet getSetLocation %~ ss
+    -- location = fromSet getSetLocation
+
+instance (HasLocation k a) => HasLocation k (Cofree f a) where
+    getSetLocation = case getSetLocation @_ @a of
+        Getter_ sa -> Getter_ $ \ (s :< _) -> sa s
+        Setter_ abst -> Setter_ $ \ss (s :< as) -> abst ss s :< as
+        GetterSetter sa sbt -> GetterSetter sa' sbt' where
+            sa' (s :< _) = sa s
+            sbt' (s :< as) b = sbt s b :< as
+
+location :: (Access k f, Functor f, HasLocation k s)
+         => LensLike' f s SrcSpan
+location = fromGetSetLens getSetLocation
+
+fromGetSetLens :: (Access k f, Functor f) => GetSetLens' k s a -> LensLike' f s a
+fromGetSetLens gsl = case gsl of
+    Getter_ sa          -> to sa
+    Setter_ abst        -> setting abst
+    GetterSetter sa sbt -> lens sa sbt
+
+fromGet :: (CanGet k) => GetSetLens k s t a b -> Getter s a
+fromGet (Getter_ sa)        = to sa
+fromGet (GetterSetter sa _) = to sa
+
+fromSet :: (CanSet k) => GetSetLens k s t a b -> Setter s t a b
+fromSet (Setter_ abst)        = setting abst
+fromSet (GetterSetter sa sbt) = lens sa sbt
+
+fromGetSet :: (CanGet k, CanSet k) => GetSetLens k s t a b -> Lens s t a b
+fromGetSet (GetterSetter sa sbt) = lens sa sbt
+
+--------------------------------------------------------------------------------
+
+comb2 :: (Functor f, Semigroup m)
+      => (Cofree f m -> Cofree f m -> f (Cofree f m))
+      -> Cofree f m -> Cofree f m -> Cofree f m
+comb2 f a b = ss :< f a b
+    where ss = a `mextract` b
+
+comb3 :: (Functor f, Semigroup m)
+      => (Cofree f m -> Cofree f m -> Cofree f m -> f (Cofree f m))
+      -> Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m
+comb3 f a b c = ss :< f a b c
+    where ss = a `mapply` b `mextract` c
+
+comb4 :: (Functor f, Semigroup m)
+      => (Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m
+         -> f (Cofree f m))
+      -> Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m -> Cofree f m
+comb4 f a b c d = ss :< f a b c d
+    where ss = a `mapply` b `mapply` c `mextract` d
+
+mextract :: (Comonad w, Semigroup m) => w m -> w m -> m
+mextract = (<>) `on` extract
+
+mapply :: (Comonad w, Semigroup m) => w m -> w m -> w m
+mapply a b = b <&> (<> extract a)
+
+lochead :: Functor f
+        => (f SrcSpan -> f SrcSpan) -> Located (f SrcSpan) -> Cofree f SrcSpan
+lochead afs (Located ss fss) = ss :< unwrap (lochead afs $ Located ss fss)
+
+--------------------------------------------------------------------------------
 
 makePrisms ''Located
 

src/Control/Monad/Errorful.hs

@@ -14,7 +14,9 @@ module Control.Monad.Errorful
     where
 ----------------------------------------------------------------------------------
 import Control.Monad.State.Strict
+import Control.Monad.Writer
 import Control.Monad.Reader
+import Control.Monad.Accum
 import Control.Monad.Trans
 import Data.Functor.Identity
 import Data.Coerce
@@ -39,10 +41,15 @@ runErrorful m = coerce (runErrorfulT m)
 class (Applicative m) => MonadErrorful e m | m -> e where
     addWound :: e -> m ()
     addFatal :: e -> m a
+    -- | Turn any wounds into fatals
+    bleedOut :: m a -> m a
 
 instance (Applicative m) => MonadErrorful e (ErrorfulT e m) where
     addWound e = ErrorfulT $ pure (Just (), [e])
     addFatal e = ErrorfulT $ pure (Nothing, [e])
+    bleedOut m = ErrorfulT $ runErrorfulT m <&> \case
+        (a, []) -> (a, [])
+        (_, es) -> (Nothing, es)
 
 instance MonadTrans (ErrorfulT e) where
     lift m = ErrorfulT ((\x -> (Just x,[])) <$> m)
@@ -84,4 +91,22 @@ hoistErrorfulT nt (ErrorfulT m) = ErrorfulT (nt m)
 instance (Monad m, MonadErrorful e m) => MonadErrorful e (ReaderT r m) where
     addWound = lift . addWound
     addFatal = lift . addFatal
+    bleedOut = mapReaderT bleedOut
+
+instance (Monad m, MonadState s m) => MonadState s (ErrorfulT e m) where
+    state = lift . state
+
+instance (Monoid w, Monad m, MonadWriter w m) => MonadWriter w (ErrorfulT e m) where
+    tell = lift . tell
+    listen (ErrorfulT m) = ErrorfulT $ listen m <&> \ ((ma,es),w) ->
+        ((,w) <$> ma, es)
+    pass (ErrorfulT m) = undefined
+
+instance (Monad m, MonadReader r m) => MonadReader r (ErrorfulT e m) where
+    ask      = lift ask
+    local rr = hoistErrorfulT (local rr)
+
+instance (Monoid w, Monad m, MonadAccum w m)
+      => MonadAccum w (ErrorfulT e m) where
+    accum = lift . accum
 

src/Core.hs

@@ -1,6 +1,5 @@
 module Core
     ( module Core.Syntax
-    , parseCore
     , parseCoreProg
     , parseCoreExpr
     , lexCore

src/Core/Examples.hs

@@ -10,12 +10,9 @@ import Core.Syntax
 import Core.TH
 ----------------------------------------------------------------------------------
 
--- fac3 = undefined
+letRecExample = undefined
--- sumList = undefined
--- constDivZero = undefined
--- idCase = undefined
 
----
+{--
 
 letrecExample :: Program'
 letrecExample = [coreProg|

src/Core/HindleyMilner.hs

@@ -16,25 +16,18 @@ module Core.HindleyMilner
     )
     where
 ----------------------------------------------------------------------------------
-import Control.Lens             hiding (Context', Context)
-import Data.Maybe               (fromMaybe)
-import Data.Text                qualified as T
-import Data.Pretty              (rpretty)
-import Data.HashMap.Strict      qualified as H
-import Data.Foldable            (traverse_)
-import Data.Functor
-import Data.Functor.Identity
 import Compiler.RLPC
-import Compiler.Types
+import Data.Text qualified as T
-import Compiler.RlpcError
-import Control.Monad            (foldM, void, forM)
 import Control.Monad.Errorful
-import Control.Monad.State
-import Control.Monad.Utils      (mapAccumLM, generalise)
-import Text.Printf
 import Core.Syntax
 ----------------------------------------------------------------------------------
 
+infer = undefined
+check = undefined
+checkCoreProg = undefined
+checkCoreProgR = undefined
+checkCoreExprR = undefined
+
 -- | Annotated typing context -- I have a feeling we're going to want this in the
 -- future.
 type Context b = [(b, Type)]
@@ -54,26 +47,14 @@ data TypeError
     deriving (Show, Eq)
 
 instance IsRlpcError TypeError where
-    liftRlpcError = \case
+    liftRlpcError = undefined
-        -- todo: use anti-parser instead of show
-        TyErrCouldNotUnify t u -> Text
-            [ T.pack $ printf "Could not match type `%s` with `%s`."
-                              (rpretty @String t) (rpretty @String u)
-            , "Expected: " <> rpretty t
-            , "Got: " <> rpretty u
-            ]
-        TyErrUntypedVariable n -> Text
-            [ "Untyped (likely undefined) variable `" <> n <> "`"
-            ]
-        TyErrRecursiveType t x -> Text
-            [ T.pack $ printf "Recursive type: `%s' occurs in `%s'"
-                              (rpretty @String t) (rpretty @String x)
-            ]
 
 -- | Synonym for @Errorful [TypeError]@. This means an @HMError@ action may
 -- throw any number of fatal or nonfatal errors. Run with @runErrorful@.
 type HMError = Errorful TypeError
 
+{--
+
 -- | Assert that an expression unifies with a given type
 --
 -- >>> let e = [coreProg|3|]
@@ -276,3 +257,4 @@ demoContext =
     , ("False", TyCon "Bool")
     ]
 
+--}

src/Core/Lex.x

@@ -78,7 +78,7 @@ rlp :-
     "{"                     { constTok TokenLBrace }
     "}"                     { constTok TokenRBrace }
     ";"                     { constTok TokenSemicolon }
-    "::"                    { constTok TokenHasType }
+    ":"                     { constTok TokenHasType }
     "@"                     { constTok TokenTypeApp }
     "{-#"                   { constTok TokenLPragma `andBegin` pragma }
 

src/Core/Parse.y

@@ -5,14 +5,12 @@ Description : Parser for the Core language
 -}
 {-# LANGUAGE OverloadedStrings, ViewPatterns #-}
 module Core.Parse
-    ( parseCore
+    ( parseCoreExpr
-    , parseCoreExpr
     , parseCoreExprR
     , parseCoreProg
     , parseCoreProgR
     , module Core.Lex -- temp convenience
     , SrcError
-    , Module
     )
     where
 
@@ -32,19 +30,19 @@ import Data.Text.IO         qualified as TIO
 import Data.Text            (Text)
 import Data.Text            qualified as T
 import Data.HashMap.Strict  qualified as H
+
+import Core.Parse.Types
 }
 
-%name parseCore Module
 %name parseCoreExpr StandaloneExpr
 %name parseCoreProg StandaloneProgram
 %tokentype { Located CoreToken }
 %error { parseError }
-%monad { RLPC } { happyBind } { happyPure }
+%monad { P }
 
 %token
       let             { Located _ TokenLet }
       letrec          { Located _ TokenLetrec }
-      module          { Located _ TokenModule }
       where           { Located _ TokenWhere }
       case            { Located _ TokenCase }
       of              { Located _ TokenOf }
@@ -68,29 +66,27 @@ import Data.HashMap.Strict  qualified as H
       '{-#'           { Located _ TokenLPragma }
       '#-}'           { Located _ TokenRPragma }
       ';'             { Located _ TokenSemicolon }
-      '::'            { Located _ TokenHasType }
+      ':'             { Located _ TokenHasType }
       eof             { Located _ TokenEOF }
 
-%%
+%right '->'
 
-Module          :: { Module Name }
+%%
-Module          : module conname where Program Eof { Module (Just ($2, [])) $4 }
-                | Program Eof                      { Module Nothing $1 }
 
 Eof             :: { () }
 Eof             : eof           { () }
                 | error         { () }
 
-StandaloneProgram :: { Program Name }
+StandaloneProgram :: { Program Var }
 StandaloneProgram : Program eof                 { $1 }
 
-Program         :: { Program Name }
+Program         :: { Program Var }
-Program         : ScTypeSig ';' Program         { insTypeSig $1 $3 }
+                : TypedScDef ';' Program    { $3 & insTypeSig (fst $1)
-                | ScTypeSig OptSemi             { singletonTypeSig $1 }
+                                                 & insScDef (snd $1) }
-                | ScDef     ';' Program         { insScDef $1 $3 }
+                | TypedScDef OptSemi        { mempty & insTypeSig (fst $1)
-                | ScDef     OptSemi             { singletonScDef $1 }
+                                                     & insScDef (snd $1) }
-                | TLPragma  Program             {% doTLPragma $1 $2 }
+                | TLPragma Program          {% doTLPragma $1 $2 }
-                | TLPragma                      {% doTLPragma $1 mempty }
+                | TLPragma                  {% doTLPragma $1 mempty }
 
 TLPragma        :: { Pragma }
                 : '{-#' Words '#-}'             { Pragma $2 }
@@ -104,140 +100,152 @@ OptSemi         : ';'                           { () }
                 | {- epsilon -}                 { () }
 
 ScTypeSig       :: { (Name, Type) }
-ScTypeSig       : Var '::' Type                 { ($1,$3) }
+ScTypeSig       : Id ':' Type                   { ($1, $3) }
 
-ScDefs          :: { [ScDef Name] }
+TypedScDef      :: { (Var, ScDef Var) }
-ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
+                : Id ':' Type ';' Id ParList '=' Expr
-                | ScDef ';'                     { [$1] }
+                            { (MkVar $1 $3, mkTypedScDef $1 $3 $5 $6 $8) }
-                | ScDef                         { [$1] }
 
-ScDef           :: { ScDef Name }
+-- ScDefs          :: { [ScDef PsName] }
-ScDef           : Var ParList '=' Expr          { ScDef $1 $2 $4 }
+-- ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
-                -- hack to allow constructors to be compiled into scs
+--                 | ScDef ';'                     { [$1] }
-                | Con ParList '=' Expr          { ScDef $1 $2 $4 }
+--                 | ScDef                         { [$1] }
+-- 
+-- ScDef           :: { ScDef PsName }
+-- ScDef           : Id ParList '=' Expr   { ScDef (Left $1) $2
+--                                                 ($4 & binders %~ Right) }
 
 Type            :: { Type }
-Type            : Type1                         { $1 }
+                : TypeApp '->' TypeApp              { $1 :-> $3 }
+                | TypeApp                         { $1 }
+
+TypeApp         :: { Type }
+                : TypeApp Type1                 { TyApp $1 $2 }
+                | Type1                         { $1 }
+
+-- do we want to allow symbolic names for tyvars and tycons?
 
 Type1           :: { Type }
 Type1           : '(' Type ')'                  { $2 }
-                | Type1 '->' Type               { $1 :-> $3 }
-                -- do we want to allow symbolic names for tyvars and tycons?
                 | varname                       { TyVar $1 }
-                | conname                       { TyCon $1 }
+                | conname                       { if $1 == "Type"
+                                                    then TyKindType else TyCon $1 }
 
-ParList         :: { [Name] }
+ParList      :: { [Name] }
-ParList         : Var ParList                   { $1 : $2 }
+ParList      : varname ParList            { $1 : $2 }
-                | {- epsilon -}                 { [] }
+             | {- epsilon -}                 { [] }
 
-StandaloneExpr  :: { Expr Name }
+StandaloneExpr  :: { Expr Var }
 StandaloneExpr  : Expr eof                      { $1 }
 
-Expr            :: { Expr Name }
+Expr            :: { Expr Var }
 Expr            : LetExpr                       { $1 }
                 | 'λ' Binders '->' Expr         { Lam $2 $4 }
                 | Application                   { $1 }
                 | CaseExpr                      { $1 }
                 | Expr1                         { $1 }
 
-LetExpr         :: { Expr Name }
+LetExpr         :: { Expr Var }
 LetExpr         : let    '{'   Bindings '}'    in Expr { Let NonRec $3 $6 }
                 | letrec '{'   Bindings '}'    in Expr { Let Rec $3 $6 }
 
-Binders         :: { [Name] }
+Binders         :: { [Var] }
 Binders         : Var Binders                  { $1 : $2 }
                 | Var                          { [$1] }
 
-Application     :: { Expr Name }
+Application     :: { Expr Var }
-Application     : Expr1 AppArgs                { foldl' App $1 $2 }
+Application     : Application AppArg           { App $1 $2 }
+                | Expr1       AppArg           { App $1 $2 }
 
-AppArgs         :: { [Expr Name] }
+AppArg          :: { Expr Var }
-AppArgs         : Expr1 AppArgs                 { $1 : $2 }
+                : '@' Type1                     { Type $2 }
-                | Expr1                         { [$1] }
+                | Expr1                         { $1 }
 
-CaseExpr        :: { Expr Name }
+CaseExpr        :: { Expr Var }
 CaseExpr        : case Expr of '{' Alters '}'   { Case $2 $5 }
 
-Alters          :: { [Alter Name] }
+Alters          :: { [Alter Var] }
 Alters          : Alter ';' Alters              { $1 : $3 }
                 | Alter ';'                     { [$1] }
                 | Alter                         { [$1] }
 
-Alter           :: { Alter Name }
+Alter           :: { Alter Var }
-Alter           : alttag ParList '->' Expr      { Alter (AltTag  $1) $2 $4 }
+Alter           : alttag  AltParList '->' Expr     { Alter (AltTag  $1) $2 $4 }
-                | Con    ParList '->' Expr      { Alter (AltData $1) $2 $4 }
+                | conname AltParList '->' Expr     { Alter (AltData $1) $2 $4 }
 
-Expr1           :: { Expr Name }
+AltParList      :: { [Var] }
+                : Var AltParList                { $1 : $2 }
+                | {- epsilon -}                 { [] }
+
+Expr1           :: { Expr Var }
 Expr1           : litint                        { Lit $ IntL $1 }
                 | Id                            { Var $1 }
                 | PackCon                       { $1 }
                 | '(' Expr ')'                  { $2 }
 
-PackCon         :: { Expr Name }
+PackCon         :: { Expr Var }
 PackCon         : pack '{' litint litint '}'    { Con $3 $4 }
 
-Bindings        :: { [Binding Name] }
+Bindings        :: { [Binding Var] }
 Bindings        : Binding ';' Bindings          { $1 : $3 }
                 | Binding ';'                   { [$1] }
                 | Binding                       { [$1] }
 
-Binding         :: { Binding Name }
+Binding         :: { Binding Var }
 Binding         : Var '=' Expr                  { $1 := $3 }
 
 Id              :: { Name }
-Id              : Var                                { $1 }
+                : varname                           { $1 }
-                | Con                                { $1 }
+                | conname                           { $1 }
 
-Var             :: { Name }
+Var             :: { Var }
-Var             : varname                           { $1 }
+Var             : '(' varname ':' Type ')'          { MkVar $2 $4 }
-                | varsym                            { $1 }
-
-Con             :: { Name }
-Con             : conname                           { $1 }
-                | consym                            { $1 }
 
 {
 
-parseError :: [Located CoreToken] -> RLPC a
+parseError :: [Located CoreToken] -> P a
 parseError (Located _ t : _) =
     error $ "<line>" <> ":" <> "<col>"
          <> ": parse error at token `" <> show t <> "'"
 
-{-# WARNING parseError "unimpl" #-}
+exprPragma :: [String] -> RLPC (Expr Var)
-
-exprPragma :: [String] -> RLPC (Expr Name)
 exprPragma ("AST" : e) = undefined
 exprPragma _           = undefined
 
-{-# WARNING exprPragma "unimpl" #-}
+astPragma :: [String] -> RLPC (Expr Var)
-
-astPragma :: [String] -> RLPC (Expr Name)
 astPragma _ = undefined
 
-{-# WARNING astPragma "unimpl" #-}
+-- insTypeSig :: (Hashable b) => (b, Type) -> Program b -> Program b
+-- insTypeSig ts = programTypeSigs %~ uncurry H.insert ts
 
-insTypeSig :: (Hashable b) => (b, Type) -> Program b -> Program b
+insTypeSig :: Var -> Program Var -> Program Var
-insTypeSig ts = programTypeSigs %~ uncurry H.insert ts
+insTypeSig w@(MkVar _ t) = programTypeSigs %~ H.insert w t
 
-singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
+-- singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
-singletonTypeSig ts = insTypeSig ts mempty
+-- singletonTypeSig ts = insTypeSig ts mempty
 
 insScDef :: (Hashable b) => ScDef b -> Program b -> Program b
 insScDef sc = programScDefs %~ (sc:)
 
-singletonScDef :: (Hashable b) => ScDef b -> Program b
+-- singletonScDef :: (Hashable b) => ScDef b -> Program b
-singletonScDef sc = insScDef sc mempty
+-- singletonScDef sc = insScDef sc mempty
 
-parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m Expr'
+parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m (Expr Var)
-parseCoreExprR = hoistRlpcT generalise . parseCoreExpr
+parseCoreExprR = liftMaybe . snd . flip runP def . parseCoreExpr
 
-parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m Program'
+parseCoreProgR :: forall m. (Monad m)
-parseCoreProgR = ddumpast <=< (hoistRlpcT generalise . parseCoreProg)
+               => [Located CoreToken] -> RLPCT m (Program Var)
-    where
+parseCoreProgR s = do
-        ddumpast :: Program' -> RLPCT m Program'
+    let p = runP (parseCoreProg s) def
-        ddumpast p = do
+    case p of
-            addDebugMsg "dump-parsed-core" . show $ p
+        (st, Just a) -> do
-            pure p
+            ddumpast a
+            pure a
+  where
+    ddumpast :: Show a => Program a -> RLPCT m (Program a)
+    ddumpast p = do
+        addDebugMsg "dump-parsed-core" . show $ p
+        pure p
 
 happyBind :: RLPC a -> (a -> RLPC b) -> RLPC b
 happyBind m k = m >>= k
@@ -245,7 +253,7 @@ happyBind m k = m >>= k
 happyPure :: a -> RLPC a
 happyPure a = pure a
 
-doTLPragma :: Pragma -> Program' -> RLPC Program'
+doTLPragma :: Pragma -> Program Var -> P (Program Var)
 -- TODO: warn unrecognised pragma
 doTLPragma (Pragma []) p = pure p
 

src/Core/Parse/Types.hs

@@ -0,0 +1,62 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Core.Parse.Types
+    ( P(..)
+    , psTyVars
+    , def
+    , PsName
+    , mkTypedScDef
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State
+import Data.Default
+import Data.Maybe
+import Data.Tuple               (swap)
+
+import Control.Lens
+
+import Core.Syntax
+--------------------------------------------------------------------------------
+
+newtype P a = P { runP :: PState -> (PState, Maybe a) }
+    deriving Functor
+
+data PState = PState
+    { _psTyVars :: [(Name, Kind)]
+    }
+
+instance Applicative P where
+    pure a = P (, Just a)
+
+    P pf <*> P pa = P \st ->
+        let (st',mf) = pf st
+            (st'',ma) = pa st'
+        in (st'', mf <*> ma)
+
+instance Monad P where
+    P pa >>= k = P \st ->
+        let (st',ma) = pa st
+        in case ma of
+            Just a -> runP (k a) st'
+            Nothing -> (st', Nothing)
+
+instance MonadState PState P where
+    state = P . fmap ((_2 %~ Just) . review swapped)
+
+instance Default PState where
+    def = undefined
+
+makeLenses ''PState
+
+type PsName = Either Name Var
+
+--------------------------------------------------------------------------------
+
+mkTypedScDef :: Name -> Type -> Name -> [Name] -> Expr Var -> ScDef Var
+mkTypedScDef nt tt n as e | nt == n = ScDef n' as' e
+    where
+        n' = MkVar n tt
+        as' = zipWith MkVar as (tt ^.. arrowStops)
+

src/Core/Syntax.hs

@@ -7,39 +7,39 @@ Description : Core ASTs and the like
 {-# LANGUAGE TemplateHaskell #-}
 -- for recursion-schemes
 {-# LANGUAGE DeriveTraversable, TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 module Core.Syntax
-    ( Expr(..)
+    (
-    , ExprF(..)
+    -- * Core AST
-    , ExprF'(..)
+      ExprF(..), ExprF'
-    , Type(..)
+    , ScDef(..), ScDef'
-    , pattern TyInt
+    , Program(..), Program'
-    , Lit(..)
+    , Type(..), Kind, pattern (:->), pattern TyInt
-    , pattern (:$)
+    , AlterF(..), Alter(..), Alter', AltCon(..)
-    , pattern (:@)
+    , pattern Binding, pattern Alter
-    , pattern (:->)
+    , Rec(..), Lit(..)
-    , Binding(..)
-    , AltCon(..)
-    , pattern (:=)
-    , Rec(..)
-    , Alter(..)
-    , Name
-    , Tag
-    , ScDef(..)
-    , Module(..)
-    , Program(..)
-    , Program'
     , Pragma(..)
-    , unliftScDef
+    -- ** Variables and identifiers
-    , programScDefs
+    , Name, Var(..), Tag, pattern (:^)
-    , programTypeSigs
+    , Binding, BindingF(..), pattern (:=), pattern (:$)
-    , programDataTags
+    , type Binding'
-    , Expr'
+    -- ** Working with the fixed point of ExprF
-    , ScDef'
+    , Expr, Expr'
-    , Alter'
+    , pattern Con, pattern Var, pattern App, pattern Lam, pattern Let
-    , Binding'
+    , pattern Case, pattern Type, pattern Lit
-    , HasRHS(_rhs)
+
-    , HasLHS(_lhs)
+    -- * pretty-printing
-    , Pretty(pretty)
+    , Out(out), WithTerseBinds(..)
+
+    -- * Optics
+    , HasArrowSyntax(..)
+    , programScDefs, programTypeSigs, programDataTags, programTyCons
+    , formalising, lambdaLifting
+    , HasRHS(_rhs), HasLHS(_lhs)
+    , _BindingF, _MkVar, _ScDef
+    -- ** Classy optics
+    , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
     )
     where
 ----------------------------------------------------------------------------------
@@ -47,109 +47,201 @@ import Data.Coerce
 import Data.Pretty
 import Data.List                    (intersperse)
 import Data.Function                ((&))
-import Data.Functor.Foldable
-import Data.Functor.Foldable.TH     (makeBaseFunctor)
 import Data.String
 import Data.HashMap.Strict          (HashMap)
 import Data.HashMap.Strict          qualified as H
 import Data.Hashable
+import Data.Hashable.Lifted
+import Data.Foldable                (traverse_)
+import Data.Functor
+import Data.Monoid
+import Data.Functor.Classes
 import Data.Text                    qualified as T
 import Data.Char
 import Data.These
-import Data.Bifoldable              (bifoldr)
+import Data.Aeson
-import GHC.Generics                 (Generic, Generically(..))
+import GHC.Generics                 ( Generic, Generic1
+                                    , Generically(..), Generically1(..))
+import Text.Show.Deriving
+import Data.Eq.Deriving
+import Data.Kind                    qualified
+
+import Data.Fix                     hiding (cata, ana)
+import Data.Bifunctor               (Bifunctor(..))
+import Data.Bifoldable              (bifoldr, Bifoldable(..))
+import Data.Bifunctor.TH
+import Data.Bitraversable
+import Data.Functor.Foldable
+import Data.Functor.Foldable.TH     (makeBaseFunctor)
+
 -- Lift instances for the Core quasiquoters
-import Language.Haskell.TH.Syntax   (Lift)
+import Misc
+import Misc.Lift1
 import Control.Lens
 ----------------------------------------------------------------------------------
 
-data Expr b = Var Name
+data ExprF b a = VarF Name
-            | Con Tag Int -- ^ Con Tag Arity
+               | ConF Tag Int -- ^ Con Tag Arity
-            | Case (Expr b) [Alter b]
+               | CaseF a [AlterF b a]
-            | Lam [b] (Expr b)
+               | LamF [b] a
-            | Let Rec [Binding b] (Expr b)
+               | LetF Rec [BindingF b a] a
-            | App (Expr b) (Expr b)
+               | AppF a a
-            | Lit Lit
+               | LitF Lit
-            deriving (Show, Read, Lift)
+               | TypeF Type
+               deriving (Functor, Foldable, Traversable)
 
-deriving instance (Eq b) => Eq (Expr b)
+type Expr b = Fix (ExprF b)
+
+instance IsString (ExprF b a) where
+    fromString = VarF . fromString
+
+instance (IsString (f (Fix f))) => IsString (Fix f) where
+    fromString = Fix . fromString
 
 data Type = TyFun
           | TyVar Name
           | TyApp Type Type
           | TyCon Name
-          deriving (Show, Read, Lift, Eq)
+          | TyForall Var Type
+          | TyKindType
+          deriving (Show, Eq, Lift)
+
+type Kind = Type
+
+-- data TyCon = MkTyCon Name Kind
+--     deriving (Eq, Show, Lift)
+
+data Var = MkVar Name Type
+    deriving (Eq, Show, Lift, Generic)
+
+pattern (:^) :: Name -> Type -> Var
+pattern n :^ t = MkVar n t
+
+instance Hashable Var where
+    hashWithSalt s (MkVar n _) = hashWithSalt s n
+
+pattern Con :: Tag -> Int -> Expr b
+pattern Con t a = Fix (ConF t a)
+
+pattern Var :: Name -> Expr b
+pattern Var b = Fix (VarF b)
+
+pattern App :: Expr b -> Expr b -> Expr b
+pattern App f x = Fix (AppF f x)
+
+pattern Lam :: [b] -> Expr b -> Expr b
+pattern Lam bs e = Fix (LamF bs e)
+
+pattern Let :: Rec -> [Binding b] -> Expr b -> Expr b
+pattern Let r bs e = Fix (LetF r bs e)
+
+pattern Case :: Expr b -> [Alter b] -> Expr b
+pattern Case e as = Fix (CaseF e as)
+
+pattern Type :: Type -> Expr b
+pattern Type t = Fix (TypeF t)
+
+pattern Lit :: Lit -> Expr b
+pattern Lit t = Fix (LitF t)
 
 pattern TyInt :: Type
 pattern TyInt = TyCon "Int#"
 
-infixl 2 :$
+class HasArrowSyntax s a b | s -> a b where
-pattern (:$) :: Expr b -> Expr b -> Expr b 
+    _arrowSyntax :: Prism' s (a, b)
-pattern f :$ x = App f x
 
-infixl 2 :@
+instance HasArrowSyntax Type Type Type where
-pattern (:@) :: Type -> Type -> Type
+    _arrowSyntax = prism make unmake where
-pattern f :@ x = TyApp f x
+        make (s,t) = TyFun `TyApp` s `TyApp` t
+
+        unmake (TyFun `TyApp` s `TyApp` t) = Right (s,t)
+        unmake s                           = Left s
 
 infixr 1 :->
-pattern (:->) :: Type -> Type -> Type
+pattern (:->) :: HasArrowSyntax s a b
-pattern a :-> b = TyApp (TyApp TyFun a) b
+              => a -> b -> s
+-- pattern (:->) :: Type -> Type -> Type
+pattern a :-> b <- (preview _arrowSyntax -> Just (a, b))
+    where a :-> b = _arrowSyntax # (a, b)
 
-{-# COMPLETE Binding :: Binding #-}
+data BindingF b a = BindingF b (ExprF b a)
-{-# COMPLETE (:=) :: Binding #-}
+    deriving (Functor, Foldable, Traversable)
-data Binding b = Binding b (Expr b)
-    deriving (Show, Read, Lift)
 
-deriving instance (Eq b) => Eq (Binding b)
+type Binding b = BindingF b (Fix (ExprF b))
+
+type Binding' = Binding Name
+
+-- collapse = foldFix embed
+
+pattern Binding :: b -> Expr b -> Binding b
+pattern Binding k v <- BindingF k (wrapFix -> v)
+    where Binding k v = BindingF k (unwrapFix v)
+
+{-# COMPLETE (:=) #-}
+{-# COMPLETE Binding #-}
 
 infixl 1 :=
 pattern (:=) :: b -> Expr b -> Binding b
 pattern k := v = Binding k v
 
-data Alter b = Alter AltCon [b] (Expr b)
+infixl 2 :$
-    deriving (Show, Read, Lift)
+pattern (:$) :: Expr b -> Expr b -> Expr b
+pattern f :$ x = App f x
 
-deriving instance (Eq b) => Eq (Alter b)
+data AlterF b a = AlterF AltCon [b] (ExprF b a)
+    deriving (Functor, Foldable, Traversable)
+
+pattern Alter :: AltCon -> [b] -> Expr b -> Alter b
+pattern Alter con bs e <- AlterF con bs (wrapFix -> e)
+    where Alter con bs e = AlterF con bs (unwrapFix e)
+
+type Alter b = AlterF b (Fix (ExprF b))
+
+type Alter' = Alter Name
+
+-- pattern Alter :: AltCon -> [b] -> Expr b -> Alter b
+-- pattern Alter con bs e <- Fix (AlterF con bs (undefined -> e))
+--     where Alter con bs e = Fix (AlterF con bs undefined)
 
 newtype Pragma = Pragma [T.Text]
 
 data Rec = Rec
          | NonRec
-         deriving (Show, Read, Eq, Lift)
+         deriving (Show, Eq, Lift)
 
 data AltCon = AltData Name
             | AltTag Tag
             | AltLit Lit
             | AltDefault
-            deriving (Show, Read, Eq, Lift)
+            deriving (Show, Eq, Lift)
 
 newtype Lit = IntL Int
-    deriving (Show, Read, Eq, Lift)
+    deriving (Show, Eq, Lift)
 
 type Name = T.Text
 type Tag = Int
 
 data ScDef b = ScDef b [b] (Expr b)
-    deriving (Show, Lift)
 
-unliftScDef :: ScDef b -> Expr b
+-- unliftScDef :: ScDef b -> Expr b
-unliftScDef (ScDef _ as e) = Lam as e
+-- unliftScDef (ScDef _ as e) = Lam as e
 
 data Module b = Module (Maybe (Name, [Name])) (Program b)
-    deriving (Show, Lift)
 
 data Program b = Program
     { _programScDefs   :: [ScDef b]
     , _programTypeSigs :: HashMap b Type
-    , _programDataTags :: HashMap b (Tag, Int)
+    , _programDataTags :: HashMap Name (Tag, Int)
     -- ^ map constructors to their tag and arity
+    , _programTyCons   :: HashMap Name Kind
+    -- ^ map type constructors to their kind
     }
-    deriving (Show, Lift, Generic)
+    deriving (Generic)
     deriving (Semigroup, Monoid)
         via Generically (Program b)
 
 makeLenses ''Program
-makeBaseFunctor ''Expr
+-- makeBaseFunctor ''Expr
 pure []
 
 -- this is a weird optic, stronger than Lens and Prism, but weaker than Iso.
@@ -163,65 +255,97 @@ type ExprF' = ExprF Name
 type Program' = Program Name
 type Expr' = Expr Name
 type ScDef' = ScDef Name
-type Alter' = Alter Name
+-- type Alter' = Alter Name
-type Binding' = Binding Name
+-- type Binding' = Binding Name
 
-instance IsString (Expr b) where
+-- instance IsString (Expr b) where
-    fromString = Var . fromString
+--     fromString = Var . fromString
 
-instance IsString Type where
+lambdaLifting :: Iso (ScDef b) (ScDef b') (b, Expr b) (b', Expr b')
-    fromString "" = error "IsString Type string may not be empty"
+lambdaLifting = iso sa bt where
-    fromString s
+    sa (ScDef n as e) = (n, e') where
-        | isUpper c     = TyCon . fromString $ s
+        e' = Lam as e
-        | otherwise     = TyVar . fromString $ s
+
-        where (c:_) = s
+    bt (n, Lam as e) = ScDef n as e
+    bt (n, e)        = ScDef n [] e
 
 ----------------------------------------------------------------------------------
 
 class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
     _rhs :: Lens s t a b
 
-instance HasRHS (Alter b) (Alter b) (Expr b) (Expr b) where
+instance HasRHS (AlterF b a) (AlterF b a') (ExprF b a) (ExprF b a') where
     _rhs = lens
-        (\ (Alter _ _ e) -> e)
+        (\ (AlterF _ _ e) -> e)
-        (\ (Alter t as _) e' -> Alter t as e')
+        (\ (AlterF t as _) e' -> AlterF t as e')
 
 instance HasRHS (ScDef b) (ScDef b) (Expr b) (Expr b) where
     _rhs = lens
         (\ (ScDef _ _ e) -> e)
         (\ (ScDef n as _) e' -> ScDef n as e')
 
-instance HasRHS (Binding b) (Binding b) (Expr b) (Expr b) where
+instance HasRHS (BindingF b a) (BindingF b' a') (ExprF b a) (ExprF b' a')
-    _rhs = lens
-        (\ (_ := e) -> e)
-        (\ (k := _) e' -> k := e')
 
 class HasLHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
     _lhs :: Lens s t a b
 
-instance HasLHS (Alter b) (Alter b) (AltCon, [b]) (AltCon, [b]) where
-    _lhs = lens
-        (\ (Alter a bs _) -> (a,bs))
-        (\ (Alter _ _ e) (a',bs') -> Alter a' bs' e)
-
 instance HasLHS (ScDef b) (ScDef b) (b, [b]) (b, [b]) where
     _lhs = lens
         (\ (ScDef n as _) -> (n,as))
         (\ (ScDef _ _ e) (n',as') -> ScDef n' as' e)
 
-instance HasLHS (Binding b) (Binding b) b b where
+-- instance HasLHS (Binding b) (Binding b) b b where
-    _lhs = lens
+    -- _lhs = lens
-        (\ (k := _) -> k)
+    --     (\ (k := _) -> k)
-        (\ (_ := e) k' -> k' := e)
+    --     (\ (_ := e) k' -> k' := e)
+
+-- | This is not a valid isomorphism for expressions containing lambdas whose
+-- bodies are themselves lambdas with multiple arguments:
+--
+-- >>> [coreExpr|\x -> \y z -> x|] ^. from (from formalising)
+-- Lam ["x"] (Lam ["y"] (Lam ["z"] (Var "x")))
+-- >>> [coreExpr|\x -> \y z -> x|]
+-- Lam ["x"] (Lam ["y","z"] (Var "x"))
+--
+-- For this reason, it's best to consider 'formalising' as if it were two
+-- unrelated unidirectional getters.
+
+formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b)
+formalising = iso sa bt where
+    sa :: Expr a -> Expr a
+    sa = ana \case
+        Lam [b] e      -> LamF [b] e
+        Lam (b:bs) e   -> LamF [b] (Lam bs e)
+        Let r (b:bs) e -> LetF r [b] (Let r bs e)
+        x              -> project x
+
+    bt :: Expr b -> Expr b
+    bt = cata \case
+        LamF [b] (Lam bs e)                -> Lam (b:bs) e
+        LetF r [b] (Let r' bs e) | r == r' -> Let r (b:bs) e
+        x                                  -> embed x
 
 --------------------------------------------------------------------------------
 
--- TODO: print type sigs with corresponding scdefs
+newtype WithTerseBinds a = WithTerseBinds a
--- TODO: emit pragmas for datatags
+
-instance (Hashable b, Pretty b) => Pretty (Program b) where
+class MakeTerse a where
-    pretty p = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
+    type AsTerse a :: Data.Kind.Type
-           $+$ vlinesOf (programJoinedDefs . to prettyGroup) p
+    asTerse :: a -> AsTerse a
+
+instance MakeTerse Var where
+    type AsTerse Var = Name
+    asTerse (MkVar n _) = n
+
+instance (Hashable b, Out b, Out (AsTerse b), MakeTerse b)
+      => Out (WithTerseBinds (Program b)) where
+    out (WithTerseBinds p)
+            = vsep [ (datatags <> "\n")
+                   , defs ]
         where
+            datatags = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
+            defs = vlinesOf (programJoinedDefs . to prettyGroup) p
+
             programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b))
             programJoinedDefs = folding $ \p ->
                 foldMapOf programTypeSigs thisTs p
@@ -233,68 +357,431 @@ instance (Hashable b, Pretty b) => Pretty (Program b) where
             thatSc = foldMap $ \sc ->
                 H.singleton (sc ^. _lhs . _1) (That sc)
 
-            prettyGroup :: These (b, Type) (ScDef b) -> Doc
+            prettyGroup :: These (b, Type) (ScDef b) -> Doc ann
-            prettyGroup = bifoldr ($$) ($$) mempty . bimap prettyTySig pretty
+            prettyGroup = bifoldr vs vs mempty
+                        . bimap (uncurry prettyTySig')
+                                (out . WithTerseBinds)
+                where vs a b = a <> ";" <> line <> b
 
-            prettyTySig (n,t) = hsep [ttext n, "::", pretty t]
+            cataDataTag n (t,a) acc = prettyDataTag n t a <> line <> acc
 
-            unionThese (This a) (That b) = These a b
+instance (Hashable b, Out b) => Out (Program b) where
-            unionThese (That b) (This a) = These a b
+    out p = vsep [ datatags <> "\n"
-            unionThese (These a b) _     = These a b
+                 , defs ]
+        where
+            datatags = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
+            defs = vlinesOf (programJoinedDefs . to prettyGroup) p
 
-            cataDataTag n (t,a) acc = prettyDataTag n t a $+$ acc
+            programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b))
+            programJoinedDefs = folding $ \p ->
+                foldMapOf programTypeSigs thisTs p
+                `u` foldMapOf programScDefs thatSc p
+              where u = H.unionWith unionThese
 
-            prettyDataTag n t a =
+            thisTs = ifoldMap @b @(HashMap b)
-                hsep ["{-#", "PackData", ttext n, ttext t, ttext a, "#-}"]
+                (\n t -> H.singleton n (This (n,t)))
+            thatSc = foldMap $ \sc ->
+                H.singleton (sc ^. _lhs . _1) (That sc)
 
-instance Pretty Type where
+            prettyGroup :: These (b, Type) (ScDef b) -> Doc ann
-    prettyPrec _ (TyVar n) = ttext n
+            prettyGroup = bifoldr vs vs mempty
-    prettyPrec _ TyFun = "(->)"
+                        . bimap (uncurry prettyTySig) out
-    prettyPrec _ (TyCon n) = ttext n
+                where vs a b = a <> ";" <> line <> b
-    prettyPrec p (a :-> b) = maybeParens (p>0) $
-        hsep [prettyPrec 1 a, "->", prettyPrec 0 b]
-    prettyPrec p (TyApp f x) = maybeParens (p>1) $
-        prettyPrec 1 f <+> prettyPrec 2 x
 
-instance (Pretty b) => Pretty (ScDef b) where
+            cataDataTag n (t,a) acc = prettyDataTag n t a <> line <> acc
-    pretty sc = hsep [name, as, "=", hang empty 1 e, ";"]
+
+unionThese :: These a b -> These a b -> These a b
+unionThese (This a) (That b) = These a b
+unionThese (That b) (This a) = These a b
+unionThese (These a b) _     = These a b
+
+prettyDataTag :: (Out n, Out t, Out a)
+              => n -> t -> a -> Doc ann
+prettyDataTag n t a =
+    hsep ["{-#", "PackData", ttext n, ttext t, ttext a, "#-}"]
+
+prettyTySig :: (Out n, Out t) => n -> t -> Doc ann
+prettyTySig n t = hsep [ttext n, ":", out t]
+
+prettyTySig' :: (MakeTerse n, Out (AsTerse n), Out t) => n -> t -> Doc ann
+prettyTySig' n t = hsep [ttext (asTerse n), ":", out t]
+
+-- out Type
+-- TyApp | appPrec   | left
+-- (:->) | appPrec-1 | right
+
+instance Out Type where
+    outPrec _ (TyVar n)   = ttext n
+    outPrec _ TyFun       = "(->)"
+    outPrec _ (TyCon n)   = ttext n
+    outPrec p (a :-> b)   = maybeParens (p>appPrec-1) $
+        hsep [outPrec appPrec a, "->", outPrec (appPrec-1) b]
+    outPrec p (TyApp f x) = maybeParens (p>appPrec) $
+        outPrec appPrec f <+> outPrec appPrec1 x
+    outPrec p (TyForall a m) = maybeParens (p>appPrec-2) $
+        "∀" <+> (outPrec appPrec1 a <> ".") <+> out m
+    outPrec _ TyKindType = "Type"
+
+instance (Out b, Out (AsTerse b), MakeTerse b)
+      => Out (WithTerseBinds (ScDef b)) where
+    out (WithTerseBinds sc) = hsep [name, as, "=", hang 1 e]
+        where
+            name = ttext $ sc ^. _lhs . _1 . to asTerse
+            as = sc & hsepOf (_lhs . _2 . each . to asTerse . to ttext)
+            e = out $ sc ^. _rhs
+
+instance (Out b) => Out (ScDef b) where
+    out sc = hsep [name, as, "=", hang 1 e]
         where
             name = ttext $ sc ^. _lhs . _1
             as = sc & hsepOf (_lhs . _2 . each . to ttext)
-            e = pretty $ sc ^. _rhs
+            e = out $ sc ^. _rhs
 
-instance (Pretty b) => Pretty (Expr b) where
+-- out Expr
-    prettyPrec _ (Var n)      = ttext n
+-- LamF | appPrec1 | right
-    prettyPrec _ (Con t a)    = "Pack{" <> (ttext t <+> ttext a) <> "}"
+-- AppF | appPrec  | left
-    prettyPrec _ (Lam bs e)   = hsep ["λ", hsep (prettyPrec 1 <$> bs), "->", pretty e]
-    prettyPrec _ (Let r bs e) = hsep [word, explicitLayout bs]
-                            $+$ hsep ["in", pretty e]
-        where word = if r == Rec then "letrec" else "let"
-    prettyPrec p (App f x)    = maybeParens (p>0) $
-        prettyPrec 0 f <+> prettyPrec 1 x
-    prettyPrec _ (Lit l)      = pretty l
-    prettyPrec p (Case e as)  = maybeParens (p>0) $
-        "case" <+> pretty e <+> "of"
-        $+$ nest 2 (explicitLayout as)
 
-instance (Pretty b) => Pretty (Alter b) where
+instance (Out b, Out a) => Out (ExprF b a) where
-    pretty (Alter c as e) =
+    outPrec = outPrec1
-        hsep [pretty c, hsep (pretty <$> as), "->", pretty e]
 
-instance Pretty AltCon where
+instance (Out b) => Out1 (ExprF b) where
-    pretty (AltData n) = ttext n
+    liftOutPrec pr _ (VarF n) = ttext n
-    pretty (AltLit l) = pretty l
+    liftOutPrec pr _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
-    pretty (AltTag t) = ttext t
+    liftOutPrec pr p (LamF bs e) = maybeParens (p>0) $
-    pretty AltDefault = "_"
+        hsep ["λ", hsep (outPrec appPrec1 <$> bs), "->", pr 0 e]
+    liftOutPrec pr p (LetF r bs e) = maybeParens (p>0)
+                               $ vsep [ hsep [out r, bs']
+                                      , hsep ["in", pr 0 e] ]
+        where bs' = liftExplicitLayout (liftOutPrec pr 0) bs
+    liftOutPrec pr p (AppF f x) = maybeParens (p>appPrec) $
+        pr appPrec f <+> pr appPrec1 x
+    liftOutPrec pr p (LitF l) = outPrec p l
+    liftOutPrec pr p (CaseF e as) = maybeParens (p>0) $
+            vsep [ "case" <+> pr 0 e <+> "of"
+                 , nest 2 as' ]
+        where as' = liftExplicitLayout (liftOutPrec pr 0) as
+    liftOutPrec pr p (TypeF t) = "@" <> outPrec appPrec1 t
 
-instance Pretty Lit where
+instance Out Rec where
-    pretty (IntL n) = ttext n
+    out Rec = "letrec"
+    out NonRec = "let"
 
-instance (Pretty b) => Pretty (Binding b) where
+instance (Out b, Out a) => Out (AlterF b a) where
-    pretty (k := v) = hsep [pretty k, "=", pretty v]
+    outPrec = outPrec1
 
-explicitLayout :: (Pretty a) => [a] -> Doc
+instance (Out b) => Out1 (AlterF b) where
-explicitLayout as = vcat inner <+> "}" where
+    liftOutPrec pr _ (AlterF c as e) =
-    inner = zipWith (<+>) delims (pretty <$> as)
+        hsep [out c, hsep (out <$> as), "->", liftOutPrec pr 0 e]
+
+instance Out AltCon where
+    out (AltData n) = ttext n
+    out (AltLit l) = out l
+    out (AltTag t) = "<" <> ttext t <> ">"
+    out AltDefault = "_"
+
+instance Out Lit where
+    out (IntL n) = ttext n
+
+instance (Out b, Out a) => Out (BindingF b a) where
+    outPrec = outPrec1
+
+instance Out b => Out1 (BindingF b) where
+    liftOutPrec pr _ (BindingF k v) = hsep [out k, "=", liftOutPrec pr 0 v]
+
+liftExplicitLayout :: (a -> Doc ann) -> [a] -> Doc ann
+liftExplicitLayout pr as = vcat inner <+> "}" where
+    inner = zipWith (<+>) delims (pr <$> as)
     delims = "{" : repeat ";"
 
+explicitLayout :: (Out a) => [a] -> Doc ann
+explicitLayout as = vcat inner <+> "}" where
+    inner = zipWith (<+>) delims (out <$> as)
+    delims = "{" : repeat ";"
+
+instance Out Var where
+    outPrec p (MkVar n t) = maybeParens (p>0) $
+        hsep [out n, ":", out t]
+
+--------------------------------------------------------------------------------
+
+-- instance Functor Alter where
+--     fmap f (Alter con bs e) = Alter con (f <$> bs) e'
+--         where
+--             e' = foldFix (embed . bimap' f id) e
+--             bimap' = $(makeBimap ''ExprF)
+
+-- instance Foldable Alter where
+-- instance Traversable Alter where
+-- instance Functor Binding where
+-- instance Foldable Binding where
+-- instance Traversable Binding where
+
+liftShowsPrecExpr :: (Show b)
+                  => (Int -> a -> ShowS)
+                  -> ([a] -> ShowS)
+                  -> Int -> ExprF b a -> ShowS
+liftShowsPrecExpr = $(makeLiftShowsPrec ''ExprF)
+
+showsPrec1Expr :: (Show b, Show a)
+               => Int -> ExprF b a -> ShowS
+showsPrec1Expr = $(makeShowsPrec1 ''ExprF)
+
+instance (Show b) => Show1 (AlterF b) where
+    liftShowsPrec sp spl d (AlterF con bs e) =
+        showsTernaryWith showsPrec showsPrec (liftShowsPrecExpr sp spl)
+                         "AlterF" d con bs e
+
+instance (Show b) => Show1 (BindingF b) where
+    liftShowsPrec sp spl d (BindingF k v) =
+        showsBinaryWith showsPrec (liftShowsPrecExpr sp spl)
+                        "BindingF" d k v
+
+instance (Show b, Show a) => Show (BindingF b a) where
+    showsPrec d (BindingF k v)
+        = showParen (d > 10)
+        $ showString "BindingF" . showChar ' '
+        . showsPrec 11 k . showChar ' '
+        . showsPrec1Expr 11 v
+
+instance (Show b, Show a) => Show (AlterF b a) where
+    showsPrec d (AlterF con bs e)
+        = showParen (d > 10)
+        $ showString "AlterF" . showChar ' '
+        . showsPrec 11 con . showChar ' '
+        . showsPrec 11 bs . showChar ' '
+        . showsPrec1Expr 11 e
+
+deriveShow1 ''ExprF
+
+deriving instance (Show b, Show a) => Show (ExprF b a)
+-- deriving instance (Show b, Show a) => Show (BindingF b a)
+-- deriving instance (Show b, Show a) => Show (AlterF b a)
+deriving instance Show b => Show (ScDef b)
+deriving instance Show b => Show (Program b)
+
+bimapExpr :: (b -> b') -> (a -> a')
+          -> ExprF b a -> ExprF b' a'
+bimapExpr = $(makeBimap ''ExprF)
+
+bifoldrExpr :: (b -> c -> c)
+            -> (a -> c -> c)
+            -> c -> ExprF b a -> c
+bifoldrExpr = $(makeBifoldr ''ExprF)
+
+bitraverseExpr :: Applicative f
+               => (b -> f b')
+               -> (a -> f a')
+               -> ExprF b a -> f (ExprF b' a')
+bitraverseExpr = $(makeBitraverse ''ExprF)
+
+instance Bifunctor AlterF where
+    bimap f g (AlterF con bs e) = AlterF con (f <$> bs) (bimapExpr f g e)
+
+instance Bifunctor BindingF where
+    bimap f g (BindingF k v) = BindingF (f k) (bimapExpr f g v)
+
+instance Bifoldable AlterF where
+    bifoldr f g z (AlterF con bs e) = bifoldrExpr f g z' e where
+        z' = foldr f z bs
+
+instance Bitraversable AlterF where
+    bitraverse f g (AlterF con bs e) =
+        AlterF con <$> traverse f bs <*> bitraverseExpr f g e
+
+instance Bifoldable BindingF where
+    bifoldr f g z (BindingF k v) = bifoldrExpr f g (f k z) v
+
+instance Bitraversable BindingF where
+    bitraverse f g (BindingF k v) =
+        BindingF <$> f k <*> bitraverseExpr f g v
+
+deriveBifunctor ''ExprF
+deriveBifoldable ''ExprF
+deriveBitraversable ''ExprF
+
+instance Lift b => Lift1 (BindingF b) where
+    liftLift lf (BindingF k v) = liftCon2 'BindingF (lift k) (liftLift lf v)
+
+instance Lift b => Lift1 (AlterF b) where
+    liftLift lf (AlterF con bs e) =
+        liftCon3 'AlterF (lift con) (lift1 bs) (liftLift lf e)
+
+instance Lift b => Lift1 (ExprF b) where
+    liftLift lf (VarF k)      = liftCon 'VarF (lift k)
+    liftLift lf (AppF f x)    = liftCon2 'AppF (lf f) (lf x)
+    liftLift lf (LamF b e)    = liftCon2 'LamF (lift b) (lf e)
+    liftLift lf (LetF r bs e) = liftCon3 'LetF (lift r) bs' (lf e)
+        where bs' = liftLift (liftLift lf) bs
+    liftLift lf (CaseF e as)  = liftCon2 'CaseF (lf e) as'
+        where as' = liftLift (liftLift lf) as
+    liftLift lf (TypeF t)     = liftCon 'TypeF (lift t)
+    liftLift lf (LitF l)      = liftCon 'LitF (lift l)
+    liftLift lf (ConF t a)    = liftCon2 'ConF (lift t) (lift a)
+
+deriving instance (Lift b, Lift a) => Lift (ExprF b a)
+deriving instance (Lift b, Lift a) => Lift (BindingF b a)
+deriving instance (Lift b, Lift a) => Lift (AlterF b a)
+deriving instance Lift b => Lift (ScDef b)
+deriving instance Lift b => Lift (Program b)
+
+--------------------------------------------------------------------------------
+
+class HasApplicants1 s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    applicants1 :: Traversal s t a b
+
+class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    applicants :: Traversal s t a b
+
+instance HasApplicants1 Type Type Type Type where
+    applicants1 k (TyApp f x) = TyApp <$> applicants1 k f <*> k x
+    applicants1 k x           = k x
+
+instance HasApplicants Type Type Type Type where
+    applicants k (TyApp f x) = TyApp <$> applicants k f <*> k x
+    applicants k x           = pure x
+
+-- instance HasArguments (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
+--                        (Fix (ExprF b)) (Fix (ExprF b)) where
+--     arguments k (AppF f x) = AppF <$> arguments k f <*> k x
+--     arguments k x          = unwrapFix <$> k (wrapFix x)
+
+-- instance HasArguments (f (Fix f)) (f (Fix f)) (Fix f) (Fix f)
+--       => HasArguments (Fix f) (Fix f) (Fix f) (Fix f) where
+--     arguments :: forall g. Applicative g
+--                => LensLike' g (Fix f) (Fix f)
+--     arguments k (Fix f) = Fix <$> arguments k f
+
+-- arguments :: Traversal' (Expr b) (Expr b)
+-- arguments k (App f x) = App <$> arguments k f <*> k x
+-- arguments k x         = k x
+
+class HasBinders s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    binders :: Traversal s t a b
+
+instance HasBinders (ScDef b) (ScDef b') b b' where
+    binders k (ScDef b as e) = ScDef <$> k b <*> traverse k as <*> binders k e
+
+instance (Hashable b, Hashable b')
+      => HasBinders (Program b) (Program b') b b' where
+    binders :: forall f. (Applicative f)
+            => LensLike f (Program b) (Program b') b b'
+    binders k p
+        = Program
+        <$> traverse (binders k) (_programScDefs p)
+        <*> (getAp . ifoldMap toSingleton $ _programTypeSigs p)
+        <*> pure (_programDataTags p)
+        <*> pure (_programTyCons p)
+      where
+        toSingleton :: b -> Type -> Ap f (HashMap b' Type)
+        toSingleton b t = Ap $ (`H.singleton` t) <$> k b
+
+instance HasBinders a a' b b'
+    => HasBinders (ExprF b a) (ExprF b' a') b b' where
+    binders :: forall f. (Applicative f)
+                    => LensLike f (ExprF b a) (ExprF b' a') b b'
+    binders k = go where
+        go :: ExprF b a -> f (ExprF b' a')
+        go (LamF bs e)   = LamF <$> traverse k bs <*> binders k e
+        go (CaseF e as)  = CaseF <$> binders k e <*> eachbind as
+        go (LetF r bs e) = LetF r <$> eachbind bs <*> binders k e
+        go f             = bitraverse k (binders k) f
+
+        eachbind :: forall p. Bitraversable p => [p b a] -> f [p b' a']
+        eachbind bs = bitraverse k (binders k) `traverse` bs
+
+instance HasBinders a a b b'
+      => HasBinders (AlterF b a) (AlterF b' a) b b' where
+    binders k (AlterF con bs e) =
+        AlterF con <$> traverse k bs <*> traverseOf binders k e
+
+instance HasBinders a a b b'
+      => HasBinders (BindingF b a) (BindingF b' a) b b' where
+    binders k (BindingF b v) = BindingF <$> k b <*> binders k v
+
+instance (HasBinders (f b (Fix (f b))) (f b' (Fix (f b'))) b b')
+      => HasBinders (Fix (f b)) (Fix (f b')) b b' where
+    binders k (Fix f) = Fix <$> binders k f
+
+class HasArrowStops s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    arrowStops :: Traversal s t a b
+
+instance HasArrowStops Type Type Type Type where
+    arrowStops k (s :-> t) = (:->) <$> k s <*> arrowStops k t
+    arrowStops k t         = k t
+
+--------------------------------------------------------------------------------
+
+liftEqExpr :: (Eq b)
+           => (a -> a' -> Bool)
+           -> ExprF b a -> ExprF b a' -> Bool
+liftEqExpr = $(makeLiftEq ''ExprF)
+
+instance (Eq b, Eq a) => Eq (BindingF b a) where
+    BindingF ka va == BindingF kb vb =
+        ka == kb && va `eq` vb
+      where eq = liftEqExpr (==)
+
+instance (Eq b, Eq a) => Eq (AlterF b a) where
+    AlterF cona bsa ea == AlterF conb bsb eb =
+        cona == conb && bsa == bsb && ea `eq` eb
+      where eq = liftEqExpr (==)
+
+instance (Eq b) => Eq1 (AlterF b) where
+    liftEq f (AlterF cona bsa ea) (AlterF conb bsb eb) =
+        cona == conb && bsa == bsb && ea `eq` eb
+      where eq = liftEqExpr f
+
+instance (Eq b) => Eq1 (BindingF b) where
+    liftEq f (BindingF ka va) (BindingF kb vb) =
+        ka == kb && va `eq` vb
+      where eq = liftEqExpr f
+
+deriveEq1 ''ExprF
+
+deriving instance (Eq b, Eq a) => Eq (ExprF b a)
+
+makePrisms ''BindingF
+makePrisms ''Var
+makePrisms ''ScDef
+
+deriving instance Generic (ExprF b a)
+deriving instance Generic1 (ExprF b)
+deriving instance Generic1 (AlterF b)
+deriving instance Generic1 (BindingF b)
+deriving instance Generic (AlterF b a)
+deriving instance Generic (BindingF b a)
+deriving instance Generic AltCon
+deriving instance Generic Lit
+deriving instance Generic Rec
+deriving instance Generic Type
+
+instance Hashable Lit
+instance Hashable AltCon
+instance Hashable Rec
+instance Hashable Type
+instance (Hashable b, Hashable a) => Hashable (BindingF b a)
+instance (Hashable b, Hashable a) => Hashable (AlterF b a)
+instance (Hashable b, Hashable a) => Hashable (ExprF b a)
+
+instance Hashable b => Hashable1 (AlterF b)
+instance Hashable b => Hashable1 (BindingF b)
+instance Hashable b => Hashable1 (ExprF b)
+
+deriving via (Generically Rec)
+    instance ToJSON Rec
+deriving via (Generically Lit)
+    instance ToJSON Lit
+deriving via (Generically AltCon)
+    instance ToJSON AltCon
+deriving via (Generically Type)
+    instance ToJSON Type
+deriving via (Generically Var)
+    instance ToJSON Var
+
+deriving via (Generically1 (BindingF b))
+    instance ToJSON b => ToJSON1 (BindingF b)
+deriving via (Generically1 (AlterF b))
+    instance ToJSON b => ToJSON1 (AlterF b)
+deriving via (Generically1 (ExprF b))
+    instance ToJSON b => ToJSON1 (ExprF b)
+

src/Core/SystemF.hs

@@ -0,0 +1,269 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE OverloadedLists #-}
+module Core.SystemF
+    ( lintCoreProgR
+    , kindOf
+    )
+    where
+--------------------------------------------------------------------------------
+import GHC.Generics                 (Generic, Generically(..))
+import Data.HashMap.Strict          (HashMap)
+import Data.HashMap.Strict          qualified as H
+import Data.Function                (on)
+import Data.Traversable
+import Data.Foldable
+import Data.List.Extra
+import Control.Monad.Utils
+import Control.Monad
+import Data.Text                    qualified as T
+import Data.Pretty
+import Text.Printf
+
+import Control.Comonad
+import Control.Comonad.Cofree
+import Data.Fix
+import Data.Functor                 hiding (unzip)
+
+import Control.Lens                 hiding ((:<))
+import Control.Lens.Unsound
+
+import Compiler.RLPC
+import Compiler.RlpcError
+import Core
+--------------------------------------------------------------------------------
+
+data Gamma = Gamma
+    { _gammaVars   :: HashMap Name Type
+    , _gammaTyVars :: HashMap Name Kind
+    , _gammaTyCons :: HashMap Name Kind
+    }
+    deriving (Generic)
+    deriving (Semigroup, Monoid)
+        via (Generically Gamma)
+
+makeLenses ''Gamma
+
+lintCoreProgR :: (Monad m) => Program Var -> RLPCT m (Program Name)
+lintCoreProgR = liftEither . (_Left %~ pure) . lint
+
+lintDontCheck :: Program Var -> Program Name
+lintDontCheck = binders %~ view (_MkVar . _1)
+
+lint :: Program Var -> SysF (Program Name)
+lint p = do
+    scs <- traverse (lintScDef g0) $ p ^. programScDefs
+    pure $ lintDontCheck p & programScDefs .~ scs
+  where
+    g0 = mempty & gammaVars .~ typeSigs
+                & gammaTyCons .~ p ^. programTyCons
+    -- 'p' stores the type signatures as 'HashMap Var Type',
+    -- while our typechecking context demands a 'HashMap Name Type'.
+    -- This conversion is perfectly safe, as the 'Hashable' instance for
+    -- 'Var' hashes exactly the internal 'Name'. i.e.
+    -- `hash (MkVar n t) = hash n`.
+    typeSigs = p ^. programTypeSigs
+             & H.mapKeys (view $ _MkVar . _1)
+
+lintScDef :: Gamma -> ScDef Var -> SysF (ScDef Name)
+lintScDef g = traverseOf lambdaLifting $ \ (MkVar n t, e) -> do
+    e'@(t' :< _) <- lintE g e
+    assertUnify t t'
+    let e'' = stripVars . stripTypes $ e'
+    pure (n, e'')
+
+stripTypes :: ET -> Expr Var
+stripTypes (_ :< as) = Fix (stripTypes <$> as)
+
+stripVars :: Expr Var -> Expr Name
+stripVars = binders %~ view (_MkVar . _1)
+
+type ET = Cofree (ExprF Var) Type
+
+type SysF = Either SystemFError
+
+data SystemFError = SystemFErrorUndefinedVariable Name
+                  | SystemFErrorKindMismatch Kind Kind
+                  | SystemFErrorCouldNotMatch Type Type
+                  deriving Show
+
+instance IsRlpcError SystemFError where
+    liftRlpcError = \case
+        SystemFErrorUndefinedVariable n ->
+            undefinedVariableErr n
+        SystemFErrorKindMismatch k k' ->
+            Text [ T.pack $ printf "Could not match kind `%s' with `%s'"
+                                   (out k) (out k')
+                 ]
+        SystemFErrorCouldNotMatch t t' ->
+            Text [ T.pack $ printf "Could not match type `%s' with `%s'"
+                                   (out t) (out t')
+                 ]
+
+justLintCoreExpr = fmap (fmap (outPrec appPrec1)) . lintE demoContext
+
+lintE :: Gamma -> Expr Var -> SysF ET
+lintE g = \case
+    Var n -> lookupVar g n <&> (:< VarF n)
+    Lit (IntL n) -> pure $ TyInt :< LitF (IntL n)
+
+    Type t -> kindOf g t <&> (:< TypeF t)
+
+    App f x
+        -- type application
+        | Right (TyForall (a :^ k) m :< f') <- lintE g f
+        , Right (k' :< TypeF t) <- lintE g x
+        , k == k'
+        -> pure $ subst a t m :< f'
+
+        -- value application
+        | Right fw@((s :-> t) :< _) <- lintE g f
+        , Right xw@(s' :< _) <- lintE g x
+        , s == s'
+        -> pure $ t :< AppF fw xw
+
+    Lam bs e -> do
+        e'@(t :< _) <- lintE g' e
+        pure $ foldr arrowify t bs :< LamF bs e'
+      where
+        g' = foldMap suppl bs <> g
+
+        suppl (MkVar n t)
+            | isKind t  = mempty & gammaTyVars %~ H.insert n t
+            | otherwise = mempty & gammaVars %~ H.insert n t
+
+        arrowify (MkVar n s) s'
+            | isKind s  = TyForall (n :^ s) s'
+            | otherwise = s :-> s'
+
+    Let Rec bs e -> do
+        e'@(t :< _) <- lintE g' e
+        bs' <- (uncurry checkBind . (_2 %~ wrapFix)) `traverse` binds
+        pure $ t :< LetF Rec bs' e'
+      where
+        binds = bs ^.. each . _BindingF
+        vs = binds ^.. each . _1 . _MkVar
+        g' = supplementVars vs g
+        checkBind v@(MkVar n t) e = case lintE g' e of
+            Right (t' :< e') | t == t'   -> Right (BindingF v e')
+                             | otherwise -> Left (SystemFErrorCouldNotMatch t t')
+            Left e -> Left e
+    Let NonRec bs e -> do
+        (g',bs') <- mapAccumLM checkBind g bs
+        e'@(t :< _) <- lintE g' e
+        pure $ t :< LetF NonRec bs' e'
+      where
+        checkBind :: Gamma -> BindingF Var (Expr Var)
+                  -> SysF (Gamma, BindingF Var ET)
+        checkBind g (BindingF v@(n :^ t) e) = case lintE g (wrapFix e) of
+            Right (t' :< e')
+                | t == t'   -> Right (supplementVar n t g, BindingF v e')
+                | otherwise -> Left (SystemFErrorCouldNotMatch t t')
+            Left e -> Left e
+
+    Case e as -> do
+        e'@(et :< _) <- lintE g e
+        (ts,as') <- unzip <$> checkAlt et `traverse` as
+        case allUnify ts of
+            Just err -> Left err
+            Nothing  -> pure $ head ts :< CaseF e' as'
+      where
+        checkAlt :: Type -> Alter Var -> SysF (Type, AlterF Var ET)
+        checkAlt scrutineeType (AlterF (AltData con) bs e) = do
+            ct <- lookupVar g con
+            ct' <- foldrMOf applicants (elimForall g) ct scrutineeType
+            zipWithM_ fzip bs (ct' ^.. arrowStops)
+            (t :< e') <- lintE (supplementVars (varsToPairs bs) g) (wrapFix e)
+            pure (t, AlterF (AltData con) bs e')
+          where
+            fzip (MkVar _ t) t'
+                | t == t'   = Right ()
+                | otherwise = Left (SystemFErrorCouldNotMatch t t')
+
+assertUnify :: Type -> Type -> SysF ()
+assertUnify t t'
+    | t == t'   = pure ()
+    | otherwise = Left (SystemFErrorCouldNotMatch t t')
+
+allUnify :: [Type] -> Maybe SystemFError
+allUnify [] = Nothing
+allUnify [t] = Nothing
+allUnify (t:t':ts)
+    | t == t'   = allUnify ts
+    | otherwise = Just (SystemFErrorCouldNotMatch t t')
+
+elimForall :: Gamma -> Type -> Type -> SysF Type
+elimForall g t (TyForall (n :^ k) m) = do
+    k' <- kindOf g t
+    case k == k' of
+        True -> pure $ subst n t m
+        False -> Left $ SystemFErrorKindMismatch k k'
+elimForall _ m _ = pure m
+ 
+varsToPairs :: [Var] -> [(Name, Type)]
+varsToPairs = toListOf (each . _MkVar)
+
+checkAgainst :: Gamma -> Var -> Expr Var -> SysF ET
+checkAgainst g v@(MkVar n t) e = case lintE g e of
+    Right e'@(t' :< _) | t == t'      -> Right e'
+                       | otherwise    -> Left (SystemFErrorCouldNotMatch t t')
+    Left a -> Left a
+
+supplementVars :: [(Name, Type)] -> Gamma -> Gamma
+supplementVars vs = gammaVars <>~ H.fromList vs
+
+supplementVar :: Name -> Type -> Gamma -> Gamma
+supplementVar n t = gammaVars %~ H.insert n t
+
+supplementTyVar :: Name -> Kind -> Gamma -> Gamma
+supplementTyVar n t = gammaTyVars %~ H.insert n t
+
+subst :: Name -> Type -> Type -> Type
+subst k v (TyVar n) | k == n = v
+subst k v (TyForall (MkVar n k') t)
+    | k /= n                 = TyForall (MkVar n k') (subst k v t)
+    | otherwise              = TyForall (MkVar n k') t
+subst k v (TyApp f x)        = (TyApp `on` subst k v) f x
+subst _ _ x                  = x
+
+isKind :: Type -> Bool
+isKind (s :-> t)  = isKind s && isKind t
+isKind TyKindType = True
+isKind _          = False
+
+kindOf :: Gamma -> Type -> SysF Kind
+kindOf g (TyVar n)  = lookupTyVar g n
+kindOf _ TyKindType = pure TyKindType
+kindOf g (TyCon n)  = lookupCon g n
+kindOf _ e          = error (show e)
+
+lookupCon :: Gamma -> Name -> SysF Kind
+lookupCon g n = case g ^. gammaTyCons . at n of
+    Just k  -> Right k
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
+
+lookupVar :: Gamma -> Name -> SysF Type
+lookupVar g n = case g ^. gammaVars . at n of
+    Just t -> Right t
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
+
+lookupTyVar :: Gamma -> Name -> SysF Kind
+lookupTyVar g n = case g ^. gammaTyVars . at n of
+    Just k -> Right k
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
+
+demoContext :: Gamma
+demoContext = Gamma
+    { _gammaVars =
+        [ ("id", TyForall ("a" :^ TyKindType) $ TyVar "a" :-> TyVar "a")
+        , ("Just", TyForall ("a" :^ TyKindType) $
+            TyVar "a" :-> (TyCon "Maybe" `TyApp` TyVar "a"))
+        , ("Nothing", TyForall ("a" :^ TyKindType) $
+            TyCon "Maybe" `TyApp` TyVar "a")
+        ]
+    , _gammaTyVars = []
+    , _gammaTyCons =
+        [ ("Int#", TyKindType)
+        , ("Maybe", TyKindType :-> TyKindType)
+        ]
+    }
+

src/Core/TH.hs

@@ -5,8 +5,8 @@ Description : Core quasiquoters
 module Core.TH
     ( coreExpr
     , coreProg
-    , coreExprT
+    -- , coreExprT
-    , coreProgT
+    -- , coreProgT
     )
     where
 ----------------------------------------------------------------------------------
@@ -33,16 +33,18 @@ coreExpr :: QuasiQuoter
 coreExpr = mkqq $ lexCoreR >=> parseCoreExprR
 
 -- | Type-checked @coreProg@
-coreProgT :: QuasiQuoter
+-- coreProgT :: QuasiQuoter
-coreProgT = mkqq $ lexCoreR >=> parseCoreProgR >=> checkCoreProgR
+-- coreProgT = mkqq $ lexCoreR >=> parseCoreProgR >=> checkCoreProgR
 
-coreExprT :: QuasiQuoter
+-- coreExprT :: QuasiQuoter
-coreExprT = mkqq $ lexCoreR >=> parseCoreExprR >=> checkCoreExprR g
+-- coreExprT = mkqq $ lexCoreR >=> parseCoreExprR >=> checkCoreExprR g
-    where
+--     where
-        g = [ ("+#", TyCon "Int#" :-> TyCon "Int#" :-> TyCon "Int#")
+--         g = [ ("+#", TyInt :-> TyInt :-> TyInt)
-            , ("id", TyCon "a" :-> TyCon "a")
+--             , ("id", TyForall (MkVar "a" TyKindType) $
-            , ("fix", (TyCon "a" :-> TyCon "a") :-> TyCon "a")
+--                     TyVar "a" :-> TyVar "a")
-            ]
+--             , ("fix", TyForall (MkVar "a" TyKindType) $
+--                     (TyVar "a" :-> TyVar "a") :-> TyVar "a")
+--             ]
 
 mkqq :: (Lift a) => (Text -> RLPCIO a) -> QuasiQuoter
 mkqq p = QuasiQuoter

src/Core/Utils.hs

@@ -2,8 +2,6 @@ module Core.Utils
     ( programRhss
     , programGlobals
     , isAtomic
-    -- , insertModule
-    , extractProgram
     , freeVariables
     )
     where
@@ -30,34 +28,29 @@ isAtomic _        = False
 
 ----------------------------------------------------------------------------------
 
--- TODO: export list awareness
+freeVariables :: Expr b -> Set b
--- insertModule :: Module b -> Program b -> Program b
+freeVariables = undefined
--- insertModule (Module _ p) = programScDefs %~ (<>m)
 
-extractProgram :: Module b -> Program b
+-- freeVariables :: Expr' -> Set Name
-extractProgram (Module _ p) = p
+-- freeVariables = cata go
+--     where
+--         go :: ExprF Name (Set Name) -> Set Name
+--         go (VarF k)         = S.singleton k
+--         -- TODO: collect free vars in rhss of bs
+--         go (LetF _ bs e)    = (e `S.union` esFree) `S.difference` ns
+--             where
+--                 es = bs ^.. each . _rhs :: [Expr']
+--                 ns = S.fromList $ bs ^.. each . _lhs
+--                 -- TODO: this feels a little wrong. maybe a different scheme is
+--                 -- appropriate
+--                 esFree = foldMap id $ freeVariables <$> es
 
-----------------------------------------------------------------------------------
+--         go (CaseF e as)     = e `S.union` asFree
-
+--             where
-freeVariables :: Expr' -> Set Name
+--                 -- asFree = foldMap id $ freeVariables <$> (fmap altToLam as)
-freeVariables = cata go
+--                 asFree = foldMap (freeVariables . altToLam) as
-    where
+--                 -- we map alts to lambdas to avoid writing a 'freeVariablesAlt'
-        go :: ExprF Name (Set Name) -> Set Name
+--                 altToLam (Alter _ ns e) = Lam ns e
-        go (VarF k)         = S.singleton k
+--         go (LamF bs e)      = e `S.difference` (S.fromList bs)
-        -- TODO: collect free vars in rhss of bs
+--         go e                = foldMap id e
-        go (LetF _ bs e)    = (e `S.union` esFree) `S.difference` ns
-            where
-                es = bs ^.. each . _rhs :: [Expr']
-                ns = S.fromList $ bs ^.. each . _lhs
-                -- TODO: this feels a little wrong. maybe a different scheme is
-                -- appropriate
-                esFree = foldMap id $ freeVariables <$> es
-
-        go (CaseF e as)     = e `S.union` asFree
-            where
-                asFree = foldMap id $ freeVariables <$> (fmap altToLam as)
-                -- we map alts to lambdas to avoid writing a 'freeVariablesAlt'
-                altToLam (Alter _ ns e) = Lam ns e
-        go (LamF bs e)      = e `S.difference` (S.fromList bs)
-        go e                = foldMap id e
 

src/Core2Core.hs

@@ -37,7 +37,7 @@ core2core p = undefined
 gmPrepR :: (Monad m) => Program' -> RLPCT m Program'
 gmPrepR p = do
     let p' = gmPrep p
-    addDebugMsg "dump-gm-preprocessed" $ render . pretty $ p'
+    addDebugMsg "dump-gm-preprocessed" $ show . out $ p'
     pure p'
 
 -- | G-machine-specific preprocessing.
@@ -116,7 +116,7 @@ floatNonStrictCases g = goE
             goE e
             traverse_ goE altBodies
             pure e'
-        goC (f :$ x)            = (:$) <$> goC f <*> goC x
+        goC (App f x)           = App <$> goC f <*> goC x
         goC (Let r bs e)        = Let r <$> bs' <*> goE e
             where bs' = travBs goC bs
         goC (Lit l)             = pure (Lit l)
@@ -128,10 +128,9 @@ floatNonStrictCases g = goE
         -- extract the right-hand sides of a list of bindings, traverse each
         -- one, and return the original list of bindings
         travBs :: (Expr' -> Floater Expr') -> [Binding'] -> Floater [Binding']
-        travBs c bs = bs ^.. each . _rhs
+        travBs c bs = undefined
-                    & traverse goC
-                    & const (pure bs)
         -- ^ ??? what the fuck?
+        -- ^ 24/02/22: what is this shit lol?
 
 -- when provided with a case expr, floatCase will float the case into a
 -- supercombinator of its free variables. the sc is returned along with an

src/Data/Pretty.hs

@@ -1,65 +1,110 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
 module Data.Pretty
-    ( Pretty(..)
+    ( Out(..), Out1(..)
-    , rpretty
+    , outPrec1
+    , rout
     , ttext
-    -- * Pretty-printing lens combinators
+    , Showing(..)
-    , hsepOf, vsepOf
+    -- * Out-printing lens combinators
-    , vcatOf
+    , hsepOf, vsepOf, vcatOf, vlinesOf
-    , vlinesOf
+    , module Prettyprinter
-    , module Text.PrettyPrint
     , maybeParens
+    , appPrec
+    , appPrec1
     )
     where
 ----------------------------------------------------------------------------------
-import Text.PrettyPrint             hiding ((<>))
+import Prettyprinter
-import Text.PrettyPrint.HughesPJ    hiding ((<>))
 import Text.Printf
 import Data.String                  (IsString(..))
-import Data.Text.Lens
+import Data.Text.Lens               hiding ((:<))
-import Data.Monoid
+import Data.Monoid                  hiding (Sum)
-import Data.Text                    qualified as T
+import Data.Bool
 import Control.Lens
+
+-- instances
+import Control.Comonad.Cofree
+import Data.Text                    qualified as T
+import Data.Functor.Sum
+import Data.Fix                     (Fix(..))
 ----------------------------------------------------------------------------------
 
-class Pretty a where
+class Out a where
-    pretty :: a -> Doc
+    out :: a -> Doc ann
-    prettyPrec :: Int -> a -> Doc
+    outPrec :: Int -> a -> Doc ann
 
-    {-# MINIMAL pretty | prettyPrec #-}
+    {-# MINIMAL out | outPrec #-}
-    pretty = prettyPrec 0
+    out = outPrec 0
-    prettyPrec a _ = pretty a
+    outPrec = const out
 
-rpretty :: (IsString s, Pretty a) => a -> s
+rout :: (IsString s, Out a) => a -> s
-rpretty = fromString . render . pretty
+rout = fromString . show . out
 
-instance Pretty String where
+-- instance Out (Doc ann) where
-    pretty = Text.PrettyPrint.text
+--     out = id
 
-instance Pretty T.Text where
+instance Out String where
-    pretty = Text.PrettyPrint.text . view unpacked
+    out = pretty
+
+instance Out T.Text where
+    out = pretty
 
 newtype Showing a = Showing a
 
-instance (Show a) => Pretty (Showing a) where
+instance (Show a) => Out (Showing a) where
-    prettyPrec p (Showing a) = fromString $ showsPrec p a ""
+    outPrec p (Showing a) = fromString $ showsPrec p a ""
 
-deriving via Showing Int instance Pretty Int
+deriving via Showing Int instance Out Int
+
+class (forall a. Out a => Out (f a)) => Out1 f where
+    liftOutPrec :: (Int -> a -> Doc ann) -> Int -> f a -> Doc ann
+
+outPrec1 :: (Out1 f, Out a) => Int -> f a -> Doc ann
+outPrec1 = liftOutPrec outPrec
+
+instance (Out1 f, Out1 g, Out a) => Out (Sum f g a) where
+    outPrec p (InL fa) = outPrec1 p fa
+    outPrec p (InR ga) = outPrec1 p ga
+
+instance (Out1 f, Out1 g) => Out1 (Sum f g) where
+    liftOutPrec pr p (InL fa) = liftOutPrec pr p fa
+    liftOutPrec pr p (InR ga) = liftOutPrec pr p ga
+
+instance (Out (f (Fix f))) => Out (Fix f) where
+    outPrec d (Fix f) = outPrec d f
 
 --------------------------------------------------------------------------------
 
-ttext :: Pretty t => t -> Doc
+ttext :: Out t => t -> Doc ann
-ttext = pretty
+ttext = out
 
-hsepOf :: Getting (Endo Doc) s Doc -> s -> Doc
+hsepOf :: Getting (Endo (Doc ann)) s (Doc ann) -> s -> Doc ann
 hsepOf l = foldrOf l (<+>) mempty
 
-vsepOf :: Getting (Endo Doc) s Doc -> s -> Doc
+vsepOf :: _ -> s -> Doc ann
-vsepOf l = foldrOf l ($+$) mempty
+vsepOf l = vsep . toListOf l
 
-vcatOf :: Getting (Endo Doc) s Doc -> s -> Doc
+vcatOf :: _ -> s -> Doc ann
-vcatOf l = foldrOf l ($$) mempty
+vcatOf l = vcat . toListOf l
 
-vlinesOf :: Getting (Endo Doc) s Doc -> s -> Doc
+vlinesOf :: Getting (Endo (Doc ann)) s (Doc ann) -> s -> Doc ann
-vlinesOf l = foldrOf l (\a b -> a $+$ "" $+$ b) mempty
+vlinesOf l = foldrOf l (\a b -> a <> line <> b) mempty
 -- hack(?) to separate chunks with a blankline
 
+--------------------------------------------------------------------------------
+
+maybeParens :: Bool -> Doc ann -> Doc ann
+maybeParens = bool id parens
+
+appPrec, appPrec1 :: Int
+appPrec  = 10
+appPrec1 = 11
+
+instance PrintfArg (Doc ann) where
+    formatArg d fmt
+        | fmtChar (vFmt 'D' fmt) == 'D' = formatString (show d) fmt'
+        | otherwise                     = errorBadFormat $ fmtChar fmt
+      where
+        fmt' = fmt { fmtChar = 's', fmtPrecision = Nothing }
+

src/GM.hs

@@ -29,9 +29,9 @@ import Data.Tuple                   (swap)
 import Control.Lens
 import Data.Text.Lens               (IsText, packed, unpacked)
 import Text.Printf
-import Text.PrettyPrint             hiding ((<>))
-import Text.PrettyPrint.HughesPJ    (maybeParens)
 import Data.Foldable                (traverse_)
+import Prettyprinter
+import Data.Pretty
 import System.IO                    (Handle, hPutStrLn)
 -- TODO: an actual output system
 -- TODO: an actual output system
@@ -165,7 +165,7 @@ hdbgProg p hio = do
     renderOut . showStats $ sts
     pure final
     where
-        renderOut r = hPutStrLn hio $ render r ++ "\n"
+        renderOut r = hPutStrLn hio $ show r ++ "\n"
 
         states = eval $ compile p
         final = last states
@@ -182,7 +182,7 @@ evalProgR p = do
     renderOut . showStats $ sts
     pure (res, sts)
     where
-        renderOut r = addDebugMsg "dump-eval" $ render r ++ "\n"
+        renderOut r = addDebugMsg "dump-eval" $ show r ++ "\n"
         states = eval . compile $ p
         final = last states
 
@@ -823,13 +823,13 @@ showCon t n = printf "Pack{%d %d}" t n ^. packed
 pprTabstop :: Int
 pprTabstop = 4
 
-qquotes :: Doc -> Doc
+qquotes :: Doc ann -> Doc ann
 qquotes d = "`" <> d <> "'"
 
-showStats :: Stats -> Doc
+showStats :: Stats -> Doc ann
-showStats sts = "==== Stats ============" $$ stats
+showStats sts = "==== Stats ============" <> line <> stats
     where
-        stats = text $ printf
+        stats = textt @String $ printf
             "Reductions      : %5d\n\
             \Prim Reductions : %5d\n\
             \Allocations     : %5d\n\
@@ -839,10 +839,10 @@ showStats sts = "==== Stats ============" $$ stats
             (sts ^. stsAllocations)
             (sts ^. stsGCCycles)
 
-showState :: GmState -> Doc
+showState :: GmState -> Doc ann
 showState st = vcat
         [ "==== GmState " <> int stnum <> " "
-            <> text (replicate (28 - 13 - 1 - digitalWidth stnum) '=')
+            <> textt (replicate (28 - 13 - 1 - digitalWidth stnum) '=')
         , "-- Next instructions -------"
         , info $ showCodeShort c
         , "-- Stack -------------------"
@@ -859,23 +859,23 @@ showState st = vcat
         -- indent data
         info = nest pprTabstop
 
-showCodeShort :: Code -> Doc
+showCodeShort :: Code -> Doc ann
 showCodeShort c = braces c'
     where
         c' | length c > 3 = list (showInstr <$> take 3 c) <> "; ..."
            | otherwise    = list (showInstr <$> c)
         list = hcat . punctuate "; "
 
-showStackShort :: Stack -> Doc
+showStackShort :: Stack -> Doc ann
 showStackShort s = brackets s'
     where
            -- no access to heap, otherwise we'd use showNodeAt
         s' | length s > 3 = list (showEntry <$> take 3 s) <> ", ..."
            | otherwise    = list (showEntry <$> s)
         list = hcat . punctuate ", "
-        showEntry = text . show
+        showEntry = textt . show
 
-showStack :: GmState -> Doc
+showStack :: GmState -> Doc ann
 showStack st = vcat $ uncurry showEntry <$> si
     where
         h = st ^. gmHeap
@@ -887,10 +887,9 @@ showStack st = vcat $ uncurry showEntry <$> si
         w = maxWidth (addresses h)
         showIndex n = padInt w n <> ": "
 
-        showEntry :: Int -> Addr -> Doc
         showEntry n a = showIndex n <> showNodeAt st a
 
-showDump :: GmState -> Doc
+showDump :: GmState -> Doc ann
 showDump st = vcat $ uncurry showEntry <$> di
     where
         d = st ^. gmDump
@@ -899,14 +898,13 @@ showDump st = vcat $ uncurry showEntry <$> di
         showIndex n = padInt w n <> ": "
         w = maxWidth (fst <$> di)
 
-        showEntry :: Int -> (Code, Stack) -> Doc
         showEntry n (c,s) = showIndex n <> nest pprTabstop entry
             where
-                entry = ("Stack : " <> showCodeShort c)
+                entry = vsep [ "Stack : " <> showCodeShort c
-                     $$ ("Code  : " <> showStackShort s)
+                             , "Code  : " <> showStackShort s ]
 
-padInt :: Int -> Int -> Doc
+padInt :: Int -> Int -> Doc ann
-padInt m n = text (replicate (m - digitalWidth n) ' ') <> int n
+padInt m n = textt (replicate (m - digitalWidth n) ' ') <> int n
 
 maxWidth :: [Int] -> Int
 maxWidth ns = digitalWidth $ maximum ns
@@ -914,7 +912,7 @@ maxWidth ns = digitalWidth $ maximum ns
 digitalWidth :: Int -> Int
 digitalWidth = length . show
 
-showHeap :: GmState -> Doc
+showHeap :: GmState -> Doc ann
 showHeap st = vcat $ showEntry <$> addrs
     where
         showAddr n = padInt w n <> ": "
@@ -923,13 +921,12 @@ showHeap st = vcat $ showEntry <$> addrs
         h = st ^. gmHeap
         addrs = addresses h
 
-        showEntry :: Addr -> Doc
         showEntry a = showAddr a <> showNodeAt st a
 
-showNodeAt :: GmState -> Addr -> Doc
+showNodeAt :: GmState -> Addr -> Doc ann
 showNodeAt = showNodeAtP 0
 
-showNodeAtP :: Int -> GmState -> Addr -> Doc
+showNodeAtP :: Int -> GmState -> Addr -> Doc ann
 showNodeAtP p st a = case hLookup a h of
     Just (NNum n)        -> int n <> "#"
     Just (NGlobal _ _)   -> textt name
@@ -953,9 +950,9 @@ showNodeAtP p st a = case hLookup a h of
         h = st ^. gmHeap
         pprec = maybeParens (p > 0)
 
-showSc :: GmState -> (Name, Addr) -> Doc
+showSc :: GmState -> (Name, Addr) -> Doc ann
-showSc st (k,a) = "Supercomb " <> qquotes (textt k) <> colon
+showSc st (k,a) = vcat [ "Supercomb " <> qquotes (textt k) <> colon
-               $$ code
+                       , code ]
     where
         code = case hLookup a (st ^. gmHeap) of
             Just (NGlobal _ c) -> showCode c
@@ -966,19 +963,21 @@ errTxtInvalidObject, errTxtInvalidAddress :: (IsString a) => a
 errTxtInvalidObject = "<invalid object>"
 errTxtInvalidAddress = "<invalid address>"
 
-showCode :: Code -> Doc
+showCode :: Code -> Doc ann
 showCode c = "Code" <+> braces instrs
     where instrs = vcat $ showInstr <$> c
 
-showInstr :: Instr -> Doc
+showInstr :: Instr -> Doc ann
-showInstr (CaseJump alts) = "CaseJump" $$ nest pprTabstop alternatives
+showInstr (CaseJump alts) = vcat [ "CaseJump", nest pprTabstop alternatives ]
     where
         showAlt (t,c) = "<" <> int t <> ">" <> showCodeShort c
-        alternatives = foldr (\a acc -> showAlt a $$ acc) mempty alts
+        alternatives = foldr (\a acc -> showAlt a <> line <> acc) mempty alts
-showInstr i = text $ show i
+showInstr i = textt $ show i
 
-textt :: (IsText a) => a -> Doc
+int = pretty
-textt t = t ^. unpacked & text
+
+textt :: (Pretty a) => a -> Doc ann
+textt = pretty
 
 ----------------------------------------------------------------------------------
 

src/Misc.hs

@@ -0,0 +1,17 @@
+module Misc where
+--------------------------------------------------------------------------------
+import Data.Functor.Classes
+--------------------------------------------------------------------------------
+
+
+showsTernaryWith :: (Int -> a -> ShowS)
+                 -> (Int -> b -> ShowS)
+                 -> (Int -> c -> ShowS)
+                 -> String -> Int -> a -> b -> c -> ShowS
+showsTernaryWith sp1 sp2 sp3 name d x y z
+    = showParen (d > 10)
+    $ showString name . showChar ' '
+    . sp1 11 x . showChar ' '
+    . sp2 11 y . showChar ' '
+    . sp3 11 z
+

src/Misc/CofreeF.hs

@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms #-}
+module Misc.CofreeF
+    ( pattern (:<$)
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Comonad.Trans.Cofree qualified as Trans.Cofree
+import Control.Comonad.Trans.Cofree (CofreeF)
+--------------------------------------------------------------------------------
+
+pattern (:<$) :: a -> f b -> Trans.Cofree.CofreeF f a b
+pattern a :<$ b = a Trans.Cofree.:< b
+

src/Misc/Lift1.hs

@@ -0,0 +1,54 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Misc.Lift1
+    ( Lift1(..), lift1
+    , liftCon, liftCon2, liftCon3
+    , Lift(..)
+    )
+    where
+--------------------------------------------------------------------------------
+import Language.Haskell.TH              hiding (Type, Name)
+import Language.Haskell.TH.Syntax       hiding (Type, Name)
+import Language.Haskell.TH.Syntax       qualified as TH
+import Language.Haskell.TH.Quote
+import Data.Kind                        qualified
+import GHC.Generics
+
+-- instances
+import Data.Fix
+import Data.Functor.Sum
+--------------------------------------------------------------------------------
+
+class Lift1 (f :: Data.Kind.Type -> Data.Kind.Type) where
+    -- lift1 :: (Quote m, Lift t) => f t -> m Exp
+    liftLift :: (Quote m) => (a -> m Exp) -> f a -> m Exp
+
+lift1 :: (Lift1 f, Lift a, Quote m) => f a -> m Exp
+lift1 = liftLift lift
+
+liftCon :: Quote m => TH.Name -> m Exp -> m Exp
+liftCon n = fmap (AppE (ConE n))
+
+liftCon2 :: Quote m => TH.Name -> m Exp -> m Exp -> m Exp
+liftCon2 n a b = do
+    a' <- a
+    b' <- b
+    pure $ ConE n `AppE` a' `AppE` b'
+
+liftCon3 :: Quote m => TH.Name -> m Exp -> m Exp -> m Exp -> m Exp
+liftCon3 n a b c = do
+    a' <- a
+    b' <- b
+    c' <- c
+    pure $ ConE n `AppE` a' `AppE` b' `AppE` c'
+
+instance Lift1 f => Lift (Fix f) where
+    lift (Fix f) = AppE (ConE 'Fix) <$> lift1 f
+
+instance Lift1 [] where
+    liftLift lf []     = pure $ ConE '[]
+    liftLift lf (a:as) = liftCon2 '(:) (lf a) (liftLift lf as)
+
+instance (Lift1 f, Lift1 g) => Lift1 (Sum f g) where
+    liftLift lf (InL fa) = liftCon 'InL $ liftLift lf fa
+    liftLift lf (InR ga) = liftCon 'InR $ liftLift lf ga
+

src/Rlp/AltParse.y

@@ -0,0 +1,243 @@
+{
+module Rlp.AltParse
+    ( parseRlpProg
+    , parseRlpProgR
+    , parseRlpExprR
+    , runP'
+    )
+    where
+import Data.List.Extra
+import Data.Text                (Text)
+
+import Control.Comonad
+import Control.Comonad.Cofree
+import Control.Lens             hiding (snoc)
+
+import Compiler.RlpcError
+import Compiler.RLPC
+import Control.Monad.Errorful
+
+import Rlp.Lex
+import Rlp.AltSyntax
+import Rlp.Parse.Types          hiding (PsName)
+import Core.Syntax              qualified as Core
+}
+
+%name parseRlpProg StandaloneProgram
+%name parseRlpExpr StandaloneExpr
+
+%monad { P }
+%lexer { lexCont } { Located _ TokenEOF }
+%error { parseError }
+%errorhandlertype explist
+%tokentype { Located RlpToken }
+
+%token
+    varname         { Located _ (TokenVarName _) }
+    conname         { Located _ (TokenConName _) }
+    consym          { Located _ (TokenConSym _) }
+    varsym          { Located _ (TokenVarSym _) }
+    data            { Located _ TokenData }
+    case            { Located _ TokenCase }
+    of              { Located _ TokenOf }
+    litint          { Located _ (TokenLitInt _) }
+    '='             { Located _ TokenEquals }
+    '|'             { Located _ TokenPipe }
+    '::'            { Located _ TokenHasType }
+    ';'             { Located _ TokenSemicolon }
+    'λ'             { Located _ TokenLambda }
+    '('             { Located _ TokenLParen }
+    ')'             { Located _ TokenRParen }
+    '->'            { Located _ TokenArrow }
+    vsemi           { Located _ TokenSemicolonV }
+    '{'             { Located _ TokenLBrace }
+    '}'             { Located _ TokenRBrace }
+    vlbrace         { Located _ TokenLBraceV }
+    vrbrace         { Located _ TokenRBraceV }
+    infixl          { Located _ TokenInfixL }
+    infixr          { Located _ TokenInfixR }
+    infix           { Located _ TokenInfix }
+    let             { Located _ TokenLet }
+    letrec          { Located _ TokenLetrec }
+    in              { Located _ TokenIn }
+    forall          { Located _ TokenForall }
+
+%nonassoc '='
+%right '->'
+%right in
+
+%%
+
+StandaloneProgram :: { Program Name (RlpExpr PsName) }
+                  : layout0(Decl)       { Program $1 }
+
+
+StandaloneExpr :: { RlpExpr PsName }
+               : VL Expr VR             { $2 }
+
+VL  :: { () }
+VL  : vlbrace       { () }
+
+VR  :: { () }
+VR  : vrbrace       { () }
+    | error         { () }
+
+VS                  :: { () }
+VS                  : ';'                   { () }
+                    | vsemi                 { () }
+
+Decl                :: { Decl PsName (RlpExpr PsName) }
+                    : FunD                  { $1 }
+                    | DataD                 { $1 }
+                    | TySigD                { $1 }
+
+TySigD              :: { Decl PsName (RlpExpr PsName) }
+                    : Var '::' Type         { TySigD $1 $3 }
+
+DataD               :: { Decl PsName (RlpExpr PsName) }
+                    : data Con TyVars               { DataD $2 $3 [] }
+                    | data Con TyVars '=' DataCons  { DataD $2 $3 $5 }
+
+DataCons            :: { [DataCon PsName] }
+                    : DataCon '|' DataCons  { $1 : $3 }
+                    | DataCon               { [$1] }
+
+DataCon             :: { DataCon PsName }
+                    : Con list0(Type1)      { DataCon $1 $2 }
+
+Type1               :: { Type PsName }
+                    : varname               { VarT $ extractVarName $1 }
+                    | Con                   { ConT $1 }
+                    | '(' Type ')'          { $2 }
+
+Type                :: { Type PsName }
+                    : Type '->' Type        { $1 :-> $3 }
+                    | AppT                  { $1 }
+
+AppT                :: { Type PsName }
+                    : Type1                 { $1 }
+                    | AppT Type1            { AppT $1 $2 }
+
+TyVars              :: { [PsName] }
+                    : list0(varname)     { $1 <&> view ( to extract
+                                                       . singular _TokenVarName ) }
+
+FunD                :: { Decl PsName (RlpExpr PsName) }
+                    : Var Pat1s '=' Expr    { FunD $1 $2 $4 }
+
+Expr                :: { RlpExpr PsName }
+                    : AppE                  { $1 }
+                    | LetE                  { $1 }
+                    | CaseE                 { $1 }
+                    | LamE                  { $1 }
+
+LamE                :: { RlpExpr PsName }
+                    : 'λ' list0(varname) '->' Expr { Finl $ Core.LamF (fmap extractName $2) $4 }
+
+CaseE               :: { RlpExpr PsName }
+                    : case Expr of CaseAlts { Finr $ CaseEF $2 $4 }
+
+CaseAlts            :: { [Alter PsName (RlpExpr PsName)] }
+                    : layout1(CaseAlt)      { $1 }
+
+CaseAlt             :: { Alter PsName (RlpExpr PsName) }
+                    : Pat '->' Expr    { Alter $1 $3 }
+
+LetE                :: { RlpExpr PsName }
+                    : let layout1(Binding) in Expr
+                        { Finr $ LetEF Core.NonRec $2 $4 }
+                    | letrec layout1(Binding) in Expr
+                        { Finr $ LetEF Core.Rec $2 $4 }
+
+Binding             :: { Binding PsName (RlpExpr PsName) }
+                    : Pat '=' Expr          { VarB $1 $3 }
+
+Expr1               :: { RlpExpr PsName }
+                    : VarE                  { $1 }
+                    | litint                { $1 ^. to extract
+                                                  . singular _TokenLitInt
+                                                  . to (Finl . Core.LitF . Core.IntL) }
+                    | '(' Expr ')'          { $2 }
+                    | ConE                  { $1 }
+
+AppE                :: { RlpExpr PsName }
+                    : AppE Expr1            { Finl $ Core.AppF $1 $2 }
+                    | Expr1                 { $1 }
+
+VarE                :: { RlpExpr PsName }
+                    : Var                   { Finl $ Core.VarF $1 }
+
+ConE                :: { RlpExpr PsName }
+                    : Con                   { Finl $ Core.VarF $1 }
+
+Pat1s               :: { [Pat PsName] }
+                    : list0(Pat1)           { $1 }
+
+Pat1                :: { Pat PsName }
+                    : Var                   { VarP $1 }
+                    | Con                   { ConP $1 }
+                    | '(' Pat ')'           { $2 }
+
+Pat                 :: { Pat PsName }
+                    : AppP                  { $1 }
+
+AppP                :: { Pat PsName }
+                    : Pat1                  { $1 }
+                    | AppP Pat1             { $1 `AppP` $2 }
+
+Con                 :: { PsName }
+                    : conname               { $1 ^. to extract
+                                                  . singular _TokenConName }
+                    | '(' consym ')'        { $1 ^. to extract
+                                                  . singular _TokenConSym }
+
+Var                 :: { PsName }
+                    : varname               { $1 ^. to extract
+                                                  . singular _TokenVarName }
+                    | '(' varsym ')'        { $2 ^. to extract
+                                                  . singular _TokenVarSym }
+
+-- list0(p : α) : [α]
+list0(p) : {- epsilon -}            { [] }
+         | list0(p) p             { $1 `snoc` $2 }
+
+-- layout0(p : β) :: [β]
+layout0(p)  : '{' '}'                   { [] }
+            | VL  VR                    { [] }
+            | layout1(p)                { $1 }
+
+-- layout_list0(sep : α, p : β) :: [β]
+layout_list0(sep,p) : p                          { [$1] }
+                    | layout_list1(sep,p) sep p  { $1 `snoc` $3 }
+                    | {- epsilon -}              { [] }
+
+-- layout1(p : β) :: [β]
+layout1(p)  : '{' layout_list1(';',p) '}'   { $2 }
+            | VL  layout_list1(VS,p) VS VR  { $2 }
+            | VL  layout_list1(VS,p) VR     { $2 }
+
+-- layout_list1(sep : α, p : β) :: [β]
+layout_list1(sep,p) : p                          { [$1] }
+                    | layout_list1(sep,p) sep p  { $1 `snoc` $3 }
+
+{
+
+extractVarName = view $ to extract . singular _TokenVarName
+
+parseRlpProgR :: (Monad m) => Text -> RLPCT m (Program Name (RlpExpr PsName))
+parseRlpProgR s = liftErrorful $ errorful (ma,es)
+    where
+        (_,es,ma) = runP' parseRlpProg s
+
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (RlpExpr PsName)
+parseRlpExprR s = liftErrorful $ errorful (ma,es)
+    where
+        (_,es,ma) = runP' parseRlpExpr s
+
+parseError :: (Located RlpToken, [String]) -> P a
+parseError (Located ss t,ts) = addFatalHere (ss ^. srcSpanLen) $
+    RlpParErrUnexpectedToken t ts
+
+extractName = view $ to extract . singular _TokenVarName
+
+}

src/Rlp/AltSyntax.hs

@@ -0,0 +1,301 @@
+{-# LANGUAGE TemplateHaskell, PatternSynonyms #-}
+module Rlp.AltSyntax
+    (
+    -- * AST
+      Program(..), Decl(..), ExprF(..), Pat(..)
+    , RlpExprF, RlpExpr, Binding(..), Alter(..)
+    , RlpExpr', RlpExprF', AnnotatedRlpExpr', Type'
+    , DataCon(..), Type(..), Kind
+    , pattern IntT, pattern TypeT
+    , Core.Rec(..)
+
+    , AnnotatedRlpExpr, TypedRlpExpr
+    , TypeF(..)
+
+    , Core.Name, PsName
+    , pattern (Core.:->)
+
+    -- * Optics
+    , programDecls
+    , _VarP, _FunB, _VarB
+    , _TySigD, _FunD
+    , _LetEF
+    , Core.applicants1, Core.arrowStops
+
+    -- * Functor-related tools
+    , Fix(..), Cofree(..), Sum(..), pattern Finl, pattern Finr
+
+    -- * Misc
+    , serialiseCofree
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Functor.Sum
+import Control.Comonad.Cofree
+import Data.Fix                 hiding (cata)
+import Data.Functor.Foldable
+import Data.Function            (fix)
+import GHC.Generics             ( Generic, Generic1
+                                , Generically(..), Generically1(..))
+import Data.Hashable
+import Data.Hashable.Lifted
+import GHC.Exts                 (IsString)
+import Control.Lens             hiding ((.=))
+
+import Data.Functor.Extend
+import Data.Functor.Foldable.TH
+import Text.Show.Deriving
+import Data.Eq.Deriving
+import Data.Text                qualified as T
+import Data.Aeson
+import Data.Pretty
+import Misc.Lift1
+
+import Compiler.Types
+import Core.Syntax              qualified as Core
+--------------------------------------------------------------------------------
+
+type RlpExpr' = RlpExpr PsName
+type RlpExprF' = RlpExprF PsName
+type AnnotatedRlpExpr' = Cofree (RlpExprF PsName)
+type Type' = Type PsName
+
+type AnnotatedRlpExpr b = Cofree (RlpExprF b)
+
+type TypedRlpExpr b = Cofree (RlpExprF b) (Type b)
+
+type PsName = T.Text
+
+newtype Program b a = Program [Decl b a]
+    deriving (Show, Functor, Foldable, Traversable)
+
+instance Extend (Decl b) where
+    extended c w@(FunD n as a) = FunD n as (c w)
+    extended _ (DataD n as cs) = DataD n as cs
+    extended _ (TySigD n t)    = TySigD n t
+
+programDecls :: Iso (Program b a) (Program b' a') [Decl b a] [Decl b' a']
+programDecls = iso sa bt where
+    sa (Program ds) = ds
+    bt = Program
+
+data Decl b a = FunD b [Pat b] a
+              | DataD Core.Name [Core.Name] [DataCon b]
+              | TySigD Core.Name (Type b)
+              deriving (Show, Functor, Foldable, Traversable)
+
+data DataCon b = DataCon Core.Name [Type b]
+    deriving (Show, Generic)
+
+data Type b = VarT Core.Name
+            | ConT Core.Name
+            | AppT (Type b) (Type b)
+            | FunT
+            | ForallT b (Type b)
+            deriving (Show, Eq, Generic, Functor, Foldable, Traversable)
+
+instance Core.HasApplicants1 (Type b) (Type b) (Type b) (Type b) where
+    applicants1 k (AppT f x) = AppT <$> Core.applicants1 k f <*> k x
+    applicants1 k t          = k t
+
+instance (Hashable b) => Hashable (Type b)
+
+pattern IntT :: (IsString b, Eq b) => Type b
+pattern IntT = ConT "Int#"
+
+type Kind = Type
+
+pattern TypeT :: (IsString b, Eq b) => Type b
+pattern TypeT = ConT "Type"
+
+instance Core.HasArrowSyntax (Type b) (Type b) (Type b) where
+    _arrowSyntax = prism make unmake where
+        make (s,t) = FunT `AppT` s `AppT` t
+
+        unmake (FunT `AppT` s `AppT` t) = Right (s,t)
+        unmake s                        = Left s
+
+data ExprF b a = InfixEF b a a
+               | LetEF Core.Rec [Binding b a] a
+               | CaseEF a [Alter b a]
+               deriving (Functor, Foldable, Traversable)
+               deriving (Eq, Generic, Generic1)
+
+data Alter b a = Alter (Pat b) a
+               deriving (Show, Functor, Foldable, Traversable)
+               deriving (Eq, Generic, Generic1)
+
+data Binding b a = FunB b [Pat b] a
+                 | VarB (Pat b) a
+                 deriving (Show, Functor, Foldable, Traversable)
+                 deriving (Eq, Generic, Generic1)
+
+-- type Expr b = Cofree (ExprF b)
+
+type RlpExprF b = Sum (Core.ExprF b) (ExprF b)
+
+type RlpExpr b = Fix (RlpExprF b)
+
+data Pat b = VarP b
+           | ConP b
+           | AppP (Pat b) (Pat b)
+           deriving (Eq, Show, Generic, Generic1)
+
+deriveShow1 ''Alter
+deriveShow1 ''Binding
+deriveShow1 ''ExprF
+deriving instance (Show b, Show a) => Show (ExprF b a)
+
+pattern Finl :: f (Fix (Sum f g)) -> Fix (Sum f g)
+pattern Finl fa = Fix (InL fa)
+
+pattern Finr :: g (Fix (Sum f g)) -> Fix (Sum f g)
+pattern Finr ga = Fix (InR ga)
+
+--------------------------------------------------------------------------------
+
+instance (Out b, Out a) => Out (ExprF b a) where
+    outPrec = outPrec1
+
+instance (Out b, Out a) => Out (Alter b a) where
+    outPrec = outPrec1
+
+instance (Out b) => Out1 (Alter b) where
+    liftOutPrec pr _ (Alter p e) =
+        hsep [ out p, "->", pr 0 e]
+
+instance Out b => Out1 (ExprF b) where
+    liftOutPrec pr p (InfixEF o a b) = maybeParens (p>0) $
+        pr 1 a <+> out o <+> pr 1 b
+    liftOutPrec pr p (CaseEF e as) = maybeParens (p>0) $
+        vsep [ hsep [ "case", pr 0 e, "of" ]
+             , nest 2 (vcat $ liftOutPrec pr 0 <$> as) ]
+    liftOutPrec pr p (LetEF r bs e) = maybeParens (p>0) $
+        vsep [ hsep [ letword r, "<bs>" ]
+             , nest 2 (hsep [ "in", pr 0 e ]) ]
+      where
+        letword Core.Rec = "letrec"
+        letword Core.NonRec = "let"
+
+instance (Out b, Out a) => Out (Decl b a) where
+    outPrec = outPrec1
+
+instance (Out b) => Out1 (Decl b) where
+    liftOutPrec pr _ (FunD f as e) =
+        hsep [ ttext f, hsep (outPrec appPrec1 <$> as)
+             , "=", pr 0 e ]
+
+    liftOutPrec _ _ (DataD f as []) =
+        hsep [ "data", ttext f, hsep (out <$> as) ]
+
+    liftOutPrec _ _ (DataD f as ds) =
+        hsep [ "data", ttext f, hsep (out <$> as), cons ]
+      where
+        cons = vcat $ zipWith (<+>) delims (out <$> ds)
+        delims = "=" : repeat "|"
+
+    liftOutPrec _ _ (TySigD n t) =
+        hsep [ ttext n, ":", out t ]
+
+instance (Out b) => Out (DataCon b) where
+    out (DataCon n as) = ttext n <+> hsep (outPrec appPrec1 <$> as)
+
+collapseForalls :: Prism' (Type b) ([b], Type b)
+collapseForalls = prism' up down where
+    up (bs,m) = foldr ForallT m bs
+    down (ForallT x m) = case down m of
+        Just (xs,m') -> Just (x : xs, m')
+        Nothing      -> Just ([x],m)
+    down _ = Nothing
+
+-- (->) is given prec `appPrec-1`
+instance (Out b) => Out (Type b) where
+    outPrec _ (VarT n) = ttext n
+    outPrec _ (ConT n) = ttext n
+    outPrec p (s Core.:-> t) = maybeParens (p>arrPrec) $
+        hsep [ outPrec arrPrec1 s, "->", outPrec arrPrec t ]
+      where arrPrec = appPrec-1
+            arrPrec1 = appPrec
+    outPrec p (AppT f x) = maybeParens (p>appPrec) $
+        outPrec appPrec f <+> outPrec appPrec1 x
+    outPrec p FunT = maybeParens (p>0) "->"
+    outPrec p t@(ForallT _ _) = maybeParens (p>0) $
+        t ^. singular collapseForalls & \(bs,m) ->
+            let bs' = "∀" <> (hsep $ outPrec appPrec1 <$> bs) <> "."
+            in bs' <+> outPrec 0 m
+
+instance (Out b) => Out (Pat b) where
+    outPrec p (VarP b) = outPrec p b
+    outPrec p (ConP b) = outPrec p b
+    outPrec p (AppP c x) = maybeParens (p>appPrec) $
+        outPrec appPrec c <+> outPrec appPrec1 x
+
+instance (Out a, Out b) => Out (Program b a) where
+    outPrec = outPrec1
+
+instance (Out b) => Out1 (Program b) where
+    liftOutPrec pr p (Program ds) = vsep $ liftOutPrec pr p <$> ds
+
+makePrisms ''ExprF
+makePrisms ''Pat
+makePrisms ''Binding
+makePrisms ''Decl
+
+deriving instance (Lift b, Lift a) => Lift (Program b a)
+deriving instance (Lift b, Lift a) => Lift (Decl b a)
+deriving instance (Lift b) => Lift (Pat b)
+deriving instance (Lift b) => Lift (DataCon b)
+deriving instance (Lift b) => Lift (Type b)
+
+instance Lift b => Lift1 (Binding b) where
+    liftLift lf (VarB b a) = liftCon2 'VarB (lift b) (lf a)
+
+instance Lift b => Lift1 (Alter b) where
+    liftLift lf (Alter b a) = liftCon2 'Alter (lift b) (lf a)
+
+instance Lift b => Lift1 (ExprF b) where
+    liftLift lf (InfixEF o a b) =
+        liftCon3 'InfixEF (lift o) (lf a) (lf b)
+    liftLift lf (LetEF r bs e) =
+        liftCon3 'LetEF (lift r) bs' (lf e)
+      where bs' = liftLift (liftLift lf) bs
+    liftLift lf (CaseEF e as) =
+        liftCon2 'CaseEF (lf e) as'
+      where as' = liftLift (liftLift lf) as
+
+deriveEq1 ''Binding
+deriveEq1 ''Alter
+deriveEq1 ''ExprF
+
+instance (Hashable b) => Hashable (Pat b)
+instance (Hashable b, Hashable a) => Hashable (Binding b a)
+instance (Hashable b, Hashable a) => Hashable (Alter b a)
+instance (Hashable b, Hashable a) => Hashable (ExprF b a)
+instance (Hashable b) => Hashable1 (Alter b)
+instance (Hashable b) => Hashable1 (Binding b)
+instance (Hashable b) => Hashable1 (ExprF b)
+
+makeBaseFunctor ''Type
+
+instance Core.HasArrowStops (Type b) (Type b) (Type b) (Type b) where
+    arrowStops k (s Core.:-> t) = (Core.:->) <$> k s <*> Core.arrowStops k t
+    arrowStops k t         = k t
+
+deriving via (Generically1 Pat)
+    instance ToJSON1 Pat
+deriving via (Generically (Pat b))
+    instance ToJSON b => ToJSON (Pat b)
+deriving via (Generically1 (Alter b))
+    instance ToJSON b => ToJSON1 (Alter b)
+deriving via (Generically1 (Binding b))
+    instance ToJSON b => ToJSON1 (Binding b)
+deriving via (Generically1 (ExprF b))
+    instance ToJSON b => ToJSON1 (ExprF b)
+deriving via (Generically1 (RlpExprF b))
+    instance ToJSON b => ToJSON1 (RlpExprF b)
+
+serialiseCofree :: (Functor f, ToJSON1 f, ToJSON a) => Cofree f a -> Value
+serialiseCofree = cata \case
+    ann :<$ e -> object [ "ann" .= ann
+                        , "val" .= toJSON1 e ]
+

src/Rlp/HindleyMilner.hs

@@ -0,0 +1,324 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.HindleyMilner
+    ( typeCheckRlpProgR
+    , TypeError(..)
+    , renamePrettily
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Lens             hiding (Context', Context, (:<), para, uncons)
+import Control.Lens.Unsound
+import Control.Lens.Extras
+import Control.Monad.Errorful
+import Control.Monad.State
+import Control.Monad.Accum
+import Control.Monad.Reader
+import Control.Monad
+import Control.Monad.Extra
+import Control.Arrow            ((>>>))
+import Control.Monad.Writer.Strict
+
+import Data.List
+import Data.Monoid
+import Data.Text                qualified as T
+import Data.Foldable            (fold)
+import Data.Function
+import Data.Foldable
+import Data.Pretty              hiding (annotate)
+import Data.Maybe
+import Data.Hashable
+import Data.HashMap.Strict      (HashMap)
+import Data.HashMap.Strict      qualified as H
+import Data.HashSet             (HashSet)
+import Data.HashSet.Lens
+import Data.HashSet             qualified as S
+import Data.Maybe               (fromMaybe)
+import Data.Traversable
+import GHC.Generics             (Generic, Generically(..))
+import Debug.Trace
+
+import Data.Functor             hiding (unzip)
+import Data.Functor.Extend
+import Data.Functor.Foldable    hiding (fold)
+import Data.Fix                 hiding (cata, para, cataM)
+import Control.Comonad.Cofree
+import Control.Comonad
+
+import Effectful
+
+import Compiler.RLPC
+import Compiler.RlpcError
+import Rlp.AltSyntax            as Rlp
+import Core.Syntax              qualified as Core
+import Core.Syntax              (ExprF(..), Lit(..))
+import Rlp.HindleyMilner.Types
+--------------------------------------------------------------------------------
+
+-- | Annotate a structure with the result of a catamorphism at each level.
+--
+--   Pretentious etymology: 'dendr-' means 'tree'
+
+dendroscribe :: (Functor f, Base t ~ f, Recursive t)
+           => (f (Cofree f a) -> a) -> t -> Cofree f a
+dendroscribe c (project -> f) = c f' :< f'
+    where f' = dendroscribe c <$> f
+
+dendroscribeM :: (Traversable f, Monad m, Base t ~ f, Recursive t)
+            => (f (Cofree f a) -> m a) -> t -> m (Cofree f a)
+dendroscribeM c (project -> f) = do
+    as <- dendroscribeM c `traverse` f
+    a <- c as
+    pure (a :< as)
+
+--------------------------------------------------------------------------------
+
+assume :: Name -> Type' -> Judgement
+assume n t = mempty & assumptions .~ H.singleton n [t]
+
+equal :: Type' -> Type' -> Judgement
+equal a b = mempty & constraints .~ [Equality a b]
+
+elim :: Name -> Type' -> Judgement -> Judgement
+elim n t j = j & assumptions %~ H.delete n
+               & constraints <>~ cs
+    where
+        cs = j & foldMapOf (assumptions . at n . each . each) \t' ->
+            [Equality t t']
+
+elimGenerally :: Name -> Type' -> Judgement -> Judgement
+elimGenerally n t j = j & assumptions %~ H.delete n
+                        & constraints <>~ cs
+    where
+        cs = j & foldMapOf (assumptions . at n . each . each) \t' ->
+            [ImplicitInstance mempty t' t]
+
+monomorphise :: Type' -> Judgement -> Judgement
+monomorphise n = constraints . each . _ImplicitInstance . _1 %~ S.insert n
+
+withoutPatterns :: [Binding b a] -> [(b, a)]
+withoutPatterns bs = bs ^.. each . singular _VarB
+                          & each . _1 %~ view (singular _VarP)
+
+--------------------------------------------------------------------------------
+
+gather :: (Unique :> es)
+       => RlpExprF' (Type', Judgement) -> Eff es (Type', Judgement)
+gather (InL (LitF (IntL _))) = pure (IntT, mempty)
+
+gather (InL (VarF n)) = do
+    t <- freshTv
+    pure (t, assume n t)
+
+gather (InL (AppF (tf,jf) (tx,jx))) = do
+    tfx <- freshTv
+    pure (tfx, jf <> jx <> equal tf (tx :-> tfx))
+
+gather (InL (LamF xs (te,je))) = do
+    bs <- for xs (\x -> (x,) <$> freshTv)
+    let j = je & forBinds elim bs
+               & forBinds (const monomorphise) bs
+        t = foldr (:->) te (bs ^.. each . _2)
+    pure (t, j)
+  where
+    elimBind (x,tx) j1 = elim x tx j1
+
+gather (InR (LetEF NonRec (withoutPatterns -> bs) (te,je))) = do
+    let j = foldr elimBind je bs
+    pure (te, j)
+  where
+    elimBind (x,(tx,jx)) j1 = elimGenerally x tx (jx <> j1)
+
+gather (InR (LetEF Rec (withoutPatterns -> bs) (te,je))) = do
+    let j = foldOf (each . _2 . _2) bs
+        j' = foldr elimRecBind j bs
+    pure (te, j' <> foldr elimBind je bs)
+  where
+    elimRecBind (x,(tx,_)) j = elim x tx j
+    elimBind (x,(tx,_)) j = elimGenerally x tx j
+
+forBinds :: (PsName -> Type' -> Judgement -> Judgement)
+         -> [(PsName, Type')] -> Judgement -> Judgement
+forBinds f bs j = foldr (uncurry f) j bs
+
+unify :: (Unique :> es)
+      => [Constraint] -> ErrorfulT TypeError (Eff es) Subst
+unify [] = pure id
+unify (c:cs) = case c of
+
+    Equality (ConT a) (ConT b)
+        | a == b
+        -> unify cs
+
+    Equality (VarT a) (VarT b)
+        | a == b
+        -> unify cs
+
+    Equality (VarT a) t
+        | a `occurs` t
+        -> error "recursive type"
+        | otherwise
+        -> unify (subst a t <$> cs) <&> (. subst a t)
+
+    Equality t (VarT a)
+        -> unify (Equality (VarT a) t : cs)
+
+    Equality (s :-> t) (s' :-> t')
+        -> unify (Equality s s' : Equality t t' : cs)
+
+    ImplicitInstance m s t
+        | null $ (freeTvs t `S.difference` freeTvs m)
+                    `S.intersection` activeTvs cs
+        -> unify $ ExplicitInstance s (generalise (freeTvs m) t) : cs
+
+    ExplicitInstance s t -> do
+        t' <- lift $ instantiate t
+        unify $ Equality s t' : cs
+
+    Equality a b
+        -> addFatal $ TyErrCouldNotUnify a b
+
+    _ -> error $ "explode (typecheckr explsiong): " <> show c
+
+activeTvs :: [Constraint] -> HashSet Name
+activeTvs = foldMap \case
+    Equality s t           -> freeTvs s <> freeTvs t
+    ImplicitInstance m s t -> freeTvs s <> (freeTvs m `S.intersection` freeTvs t)
+    ExplicitInstance s t   -> freeTvs s <> freeTvs t
+
+instantiate :: (Unique :> es) => Scheme -> Eff es Type'
+instantiate (ForallT x t) = do
+    x' <- freshTv
+    subst x x' <$> instantiate t
+instantiate t = pure t
+
+generalise :: HashSet Name -> Type' -> Scheme
+generalise m t = foldr ForallT t as
+    where as = S.toList $ freeTvs t `S.difference` m
+
+occurs :: (HasTypes a) => Name -> a -> Bool
+occurs x t = x `elem` freeTvs t
+
+--------------------------------------------------------------------------------
+
+annotate :: (Unique :> es)
+         => RlpExpr' -> Eff es (Cofree RlpExprF' (Type', Judgement))
+annotate = dendroscribeM (gather . fmap extract)
+
+orderConstraints :: [Constraint] -> [Constraint]
+orderConstraints cs = a <> b
+    where (a,b) = partition (isn't _ImplicitInstance) cs
+
+finalJudgement :: Cofree RlpExprF' (Type', Judgement) -> Judgement
+finalJudgement = snd . extract
+
+solveTree :: (Unique :> es)
+          => Cofree RlpExprF' (Type', Judgement)
+          -> ErrorfulT TypeError (Eff es) (Cofree RlpExprF' Type')
+solveTree e = do
+    sub <- unify (orderConstraints $ finalJudgement e ^. constraints . reversed)
+    pure $ sub . view _1 <$> e
+
+solveJudgement :: (Unique :> es)
+               => Judgement
+               -> ErrorfulT TypeError (Eff es) Subst
+solveJudgement j = unify (orderConstraints $ j ^. constraints . reversed)
+
+typeCheckRlpProgR :: Monad m
+                  => Program PsName RlpExpr'
+                  -> RLPCT m (Program PsName (Cofree RlpExprF' Type'))
+typeCheckRlpProgR
+    = liftErrorful
+    . hoistErrorfulT (pure . runPureEff . runUnique)
+    . mapErrorful (errorMsg (SrcSpan 0 0 0 0))
+    . inferProg
+
+finallyGeneralise :: Cofree RlpExprF' Type' -> Cofree RlpExprF' Type'
+finallyGeneralise = _extract %~ generalise mempty
+
+inferProg :: (Unique :> es)
+          => Program PsName RlpExpr'
+          -> ErrorfulT TypeError (Eff es)
+              (Program PsName (Cofree RlpExprF' Type'))
+inferProg p = do
+    p' <- lift $ annotateProg (etaExpandProg p)
+    sub <- solveJudgement (foldOf (folded . _extract . _2) p')
+    pure $ p' & traversed . traversed %~ sub . view _1
+              & traversed %~ finallyGeneralise
+
+etaExpandProg :: Program PsName RlpExpr' -> Program PsName RlpExpr'
+etaExpandProg = programDecls . each %~ etaExpand where
+    etaExpand (FunD n [] e) = FunD n [] e
+    etaExpand (FunD n as e) = FunD n [] $ Finl (LamF as' e)
+        where as' = as ^.. each . singular _VarP
+    etaExpand x = x
+
+infer :: (Unique :> es)
+      => RlpExpr'
+      -> ErrorfulT TypeError (Eff es)
+            (Cofree RlpExprF' Type')
+infer e = do
+    e' <- solveTree <=< (lift . annotate) $ e
+    pure $ finallyGeneralise e'
+
+annotateDefs :: (Unique :> es)
+             => Program PsName RlpExpr'
+             -> Eff es (Program PsName
+                         (Cofree RlpExprF' (Type', Judgement)))
+annotateDefs = traverseOf (programDefs . _2) annotate
+
+annotateProg :: (Unique :> es)
+             => Program PsName RlpExpr'
+             -> Eff es (Program PsName
+                         (Cofree RlpExprF' (Type', Judgement)))
+annotateProg p = do
+    p' <- annotateDefs p
+    let bs = p' ^.. programDefs & each . _2 %~ (fst . extract)
+        p'' = p' & programDefs . _2 . traversed . _2
+            %~ forBinds elimGenerally bs
+    pure p''
+
+programDefs :: Traversal (Program b a) (Program b a') (b, a) (b, a')
+programDefs k (Program ds) = Program <$> go k ds where
+    go k [] = pure []
+    go k (FunD n as e : ds) = (:) <$> refun as (k (n,e)) <*> go k ds
+    refun as kne = uncurry (\a b -> FunD a as b) <$> kne
+
+--------------------------------------------------------------------------------
+
+renamePrettily' :: Type PsName -> Type PsName
+renamePrettily' = join renamePrettily
+
+-- | for some type, compute a substitution which will rename all free variables
+-- for aesthetic purposes
+
+renamePrettily :: Type PsName -> Type PsName -> Type PsName
+renamePrettily root = (`evalState` alphabetNames) . (renameFree <=< renameBound)
+  where
+    renameBound :: Type PsName -> State [PsName] (Type PsName)
+    renameBound = cata \case
+        ForallTF x m -> do
+            n <- getName
+            ForallT n <$> (subst x (VarT n) <$> m)
+        t -> embed <$> sequenceA t
+
+    renameFree :: Type PsName -> State [PsName] (Type PsName)
+    renameFree t = do
+        subs <- forM (freeVariablesLTR root) $ \v -> do
+            n <- getName
+            pure $ Endo (subst v (VarT n))
+        pure . appEndo (fold subs) $ t
+
+    getName :: State [PsName] PsName
+    getName = state (fromJust . uncons)
+
+alphabetNames :: [PsName]
+alphabetNames = alphabet ++ concatMap appendAlphabet alphabetNames
+    where alphabet = [ T.pack [c] | c <- ['a'..'z'] ]
+          appendAlphabet c = [ c <> c' | c' <- alphabet ]
+
+freeVariablesLTR :: Type PsName -> [PsName]
+freeVariablesLTR = nub . cata \case
+    VarTF x -> [x]
+    ForallTF x m -> m \\ [x]
+    vs -> concat vs
+

src/Rlp/HindleyMilner/Types.hs

@@ -0,0 +1,175 @@
+{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.HindleyMilner.Types
+    where
+--------------------------------------------------------------------------------
+import Data.Hashable
+import Data.HashMap.Strict      (HashMap)
+import Data.HashMap.Strict      qualified as H
+import Data.HashSet             (HashSet)
+import Data.HashSet             qualified as S
+import GHC.Generics             (Generic(..), Generically(..))
+import Data.Kind                qualified
+import Data.Text                qualified as T
+import Effectful.State.Static.Local
+import Effectful.Labeled
+import Effectful
+import Text.Printf
+import Data.Pretty
+import Data.Function
+
+import Control.Lens             hiding (Context', Context, para)
+
+import Data.Functor.Foldable    hiding (fold)
+import Data.Foldable
+
+import Compiler.RlpcError
+import Rlp.AltSyntax
+--------------------------------------------------------------------------------
+
+-- | A polymorphic type
+
+type Scheme = Type'
+
+type Subst = Type' -> Type'
+
+data Constraint = Equality Type' Type'
+                | ImplicitInstance (HashSet Type') Type' Type'
+                | ExplicitInstance Type' Scheme
+                deriving Show
+
+instance Out Constraint where
+    out (Equality s t) =
+        hsep [outPrec appPrec1 s, "~", outPrec appPrec1 t]
+
+--------------------------------------------------------------------------------
+
+-- | Type error enum.
+data TypeError
+    -- | Two types could not be unified
+    = TyErrCouldNotUnify Type' Type'
+    -- | @x@ could not be unified with @t@ because @x@ occurs in @t@
+    | TyErrRecursiveType Name Type'
+    -- | Untyped, potentially undefined variable
+    | TyErrUntypedVariable Name
+    | TyErrMissingTypeSig Name
+    | TyErrNonHomogenousCaseAlternatives (RlpExpr PsName)
+    deriving (Show)
+
+instance IsRlpcError TypeError where
+    liftRlpcError = \case
+        -- todo: use anti-parser instead of show
+        TyErrCouldNotUnify t u -> Text
+            [ T.pack $ printf "Could not match type `%s` with `%s`."
+                              (rout @String t) (rout @String u)
+            , "Expected: " <> rout t
+            , "Got: " <> rout u
+            ]
+        TyErrUntypedVariable n -> Text
+            [ "Untyped (likely undefined) variable `" <> n <> "`"
+            ]
+        TyErrRecursiveType t x -> Text
+            [ T.pack $ printf "Recursive type: `%s' occurs in `%s'"
+                              (rout @String t) (rout @String x)
+            ]
+
+--------------------------------------------------------------------------------
+
+type Unique = State Int
+
+runUnique :: Eff (Unique : es) a -> Eff es a
+runUnique = evalState 0
+
+freshTv :: (Unique :> es) => Eff es (Type PsName)
+freshTv = do
+    n <- get
+    modify @Int succ
+    pure (VarT $ tvNameOfInt n)
+
+tvNameOfInt :: Int -> PsName
+tvNameOfInt n = "$a" <> T.pack (show n)
+
+--------------------------------------------------------------------------------
+
+-- | A 'Judgement' is a sort of "co-context" used in bottom-up inference. The
+--   typical algorithms J, W, and siblings pass some context Γ to the inference
+--   algorithm which is used to lookup variables and such. Here in rlpc we
+--   infer a type under zero context; inference returns the assumptions made of
+--   a variable which may be later eliminated and solved.
+
+data Judgement = Judgement
+    { _constraints :: [Constraint]
+    , _assumptions :: Assumptions
+    }
+    deriving (Show)
+
+type Assumptions = HashMap PsName [Type PsName]
+
+instance Semigroup Judgement where
+    a <> b = Judgement
+        { _constraints = ((<>) `on` _constraints) a b
+        , _assumptions = (H.unionWith (<>) `on` _assumptions) a b
+        }
+
+instance Monoid Judgement where
+    mempty = Judgement
+        { _constraints = mempty
+        , _assumptions = mempty
+        }
+
+--------------------------------------------------------------------------------
+
+class HasTypes a where
+    types :: Traversal' a Type'
+    freeTvs :: a -> HashSet PsName
+    boundTvs :: a -> HashSet PsName
+    subst :: Name -> Type' -> a -> a
+
+    freeTvs = foldMapOf types $ cata \case
+        VarTF n -> S.singleton n
+        t       -> fold t
+
+    boundTvs = const mempty
+
+    subst k v = types %~ cata \case
+        VarTF n | k == n -> v
+        t                -> embed t
+
+instance HasTypes Constraint where
+    types k (Equality s t) = Equality <$> types k s <*> types k t
+    types k (ImplicitInstance m s t) =
+        ImplicitInstance <$> types k m <*> types k s <*> types k t
+    types k (ExplicitInstance s t) =
+        ExplicitInstance <$> types k s <*> types k t
+
+instance (Hashable a, HasTypes a) => HasTypes (HashSet a) where
+    types k = traverseHashSetBad (types k)
+
+instance HasTypes Type' where
+    types = id
+    freeTvs = cata \case
+        VarTF n -> S.singleton n
+        ForallTF x t -> S.delete x t
+        t -> fold t
+    boundTvs = cata \case
+        ForallTF x t -> S.insert x t
+        t -> fold t
+    subst k v = para \case
+        VarTF n | k == n -> v
+        ForallTF x (pre,post)
+            | k == x -> ForallT x pre
+        t -> embed $ snd <$> t
+
+-- illegal traversal
+traverseHashSetBad :: (Hashable a, Hashable b)
+                   => Traversal (HashSet a) (HashSet b) a b
+traverseHashSetBad k s = fmap S.fromList $ traverse k (S.toList s)
+
+
+--------------------------------------------------------------------------------
+
+makePrisms ''Judgement
+makeLenses ''Judgement
+makePrisms ''Constraint
+makePrisms ''TypeError
+

src/Rlp/HindleyMilner/Visual.hs

@@ -0,0 +1,30 @@
+{-# LANGUAGE LexicalNegation #-}
+module Rlp.HindleyMilner.Visual
+    (
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Monad
+import System.IO
+import Data.Text                        (Text)
+import Data.Text                        qualified as T
+import Data.Text.IO                     qualified as T
+import Data.Pretty                      hiding (annotate)
+import Data.String                      (IsString(..))
+import Data.Foldable
+import Misc.CofreeF
+import Control.Exception
+
+import Data.Functor.Foldable
+
+import Data.Aeson
+
+import Core.Syntax                      as Core
+import Rlp.AltSyntax                    as Rlp
+import Rlp.HindleyMilner
+
+import Prelude hiding ((**))
+--------------------------------------------------------------------------------
+
+type AnnExpr = Cofree (RlpExprF PsName)
+

src/Rlp/Lex.x

@@ -8,11 +8,13 @@ module Rlp.Lex
     , Located(..)
     , lexToken
     , lexStream
+    , lexStream'
     , lexDebug
     , lexCont
     , popLexState
     , programInitState
     , runP'
+    , popLayout
     )
     where
 import Codec.Binary.UTF8.String (encodeChar)
@@ -29,6 +31,7 @@ import Data.Word
 import Data.Default
 import Control.Lens
 
+import Compiler.Types
 import Debug.Trace
 import Rlp.Parse.Types
 }
@@ -56,10 +59,10 @@ $asciisym       = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~\:]
 
 @reservedname = 
     case|data|do|import|in|let|letrec|module|of|where
-    |infixr|infixl|infix
+    |infixr|infixl|infix|forall
 
 @reservedop =
-    "=" | \\ | "->" | "|" | "::"
+    "=" | \\ | "->" | "|" | ":"
 
 rlp :-
     
@@ -160,14 +163,16 @@ lexReservedName = \case
     "infix"     -> TokenInfix
     "infixl"    -> TokenInfixL
     "infixr"    -> TokenInfixR
+    "forall"    -> TokenForall
     s           -> error (show s)
 
 lexReservedOp :: Text -> RlpToken
 lexReservedOp = \case
     "="     -> TokenEquals
-    "::"    -> TokenHasType
+    ":"     -> TokenHasType
     "|"     -> TokenPipe
     "->"    -> TokenArrow
+    "\\"    -> TokenLambda
     s       -> error (show s)
 
 -- | @andBegin@, with the subtle difference that the start code is set
@@ -274,11 +279,12 @@ lexCont :: (Located RlpToken -> P a) -> P a
 lexCont = (lexToken >>=)
 
 lexStream :: P [RlpToken]
-lexStream = do
+lexStream = fmap extract <$> lexStream'
-    t <- lexToken
+
-    case t of
+lexStream' :: P [Located RlpToken]
-        Located _ TokenEOF -> pure [TokenEOF]
+lexStream' = lexToken >>= \case
-        Located _ t        -> (t:) <$> lexStream
+    t@(Located _ TokenEOF) -> pure [t]
+    t                      -> (t:) <$> lexStream'
 
 lexDebug :: (Located RlpToken -> P a) -> P a
 lexDebug k = do
@@ -325,6 +331,7 @@ insertRBrace    = {- traceM "inserting rbrace" >> -} insertToken TokenRBraceV
 cmpLayout :: P Ordering
 cmpLayout = do
     i <- indentLevel
+    -- traceM $ "i: " <> show i
     ctx <- preuse (psLayoutStack . _head)
     case ctx of
         Just (Implicit n) -> pure (i `compare` n)
@@ -333,8 +340,6 @@ cmpLayout = do
 doBol :: LexerAction (Located RlpToken)
 doBol inp l = do
     off <- cmpLayout
-    i <- indentLevel
-    -- traceM $ "i: " <> show i
     -- important that we pop the lex state lest we find our lexer diverging
     case off of
         -- the line is aligned with the previous. it therefore belongs to the

src/Rlp/Parse.y

@@ -5,15 +5,17 @@ module Rlp.Parse
     , parseRlpProgR
     , parseRlpExpr
     , parseRlpExprR
+    , runP'
     )
     where
 import Compiler.RlpcError
 import Compiler.RLPC
+import Control.Comonad.Cofree
 import Rlp.Lex
 import Rlp.Syntax
 import Rlp.Parse.Types
 import Rlp.Parse.Associate
-import Control.Lens                 hiding (snoc, (.>), (<.), (<<~))
+import Control.Lens                 hiding (snoc, (.>), (<.), (<<~), (:<))
 import Data.List.Extra
 import Data.Fix
 import Data.Functor.Const
@@ -71,139 +73,118 @@ import Compiler.Types
 
 %%
 
-StandaloneProgram   :: { RlpProgram RlpcPs }
+StandaloneProgram   :: { Program RlpcPs SrcSpan }
-StandaloneProgram   : '{' Decls  '}'        {% mkProgram $2 }
+StandaloneProgram   : layout0(Decl)         {% mkProgram $1 }
-                    | VL  DeclsV VR         {% mkProgram $2 }
 
-StandaloneExpr      :: { RlpExpr RlpcPs }
+StandaloneExpr      :: { Expr' RlpcPs SrcSpan }
-                    : VL Expr VR            { extract $2 }
+                    : VL Expr VR            { $2 }
 
 VL  :: { () }
 VL  : vlbrace       { () }
 
 VR  :: { () }
 VR  : vrbrace       { () }
-    | error         { () }
+    | error         {% void popLayout }
 
-Decls               :: { [Decl' RlpcPs] }
+VS                  :: { () }
-Decls               : Decl ';' Decls        { $1 : $3 }
+VS                  : ';'                   { () }
-                    | Decl ';'              { [$1] }
+                    | vsemi                 { () }
-                    | Decl                  { [$1] }
 
-DeclsV              :: { [Decl' RlpcPs] }
+Decl        :: { Decl RlpcPs SrcSpan }
-DeclsV              : Decl VS DeclsV        { $1 : $3 }
-                    | Decl VS               { [$1] }
-                    | Decl                  { [$1] }
-
-VS                  :: { Located RlpToken }
-VS                  : ';'                   { $1 }
-                    | vsemi                 { $1 }
-
-Decl        :: { Decl' RlpcPs }
             : FunDecl                   { $1 }
             | TySigDecl                 { $1 }
             | DataDecl                  { $1 }
             | InfixDecl                 { $1 }
 
-TySigDecl   :: { Decl' RlpcPs }
+TySigDecl   :: { Decl RlpcPs SrcSpan }
-            : Var '::' Type             { (\e -> TySigD [extract e]) <<~ $1 <~> $3 }
+            : Var '::' Type             { TySigD [$1] $3 }
 
-InfixDecl   :: { Decl' RlpcPs }
+InfixDecl   :: { Decl RlpcPs SrcSpan }
-            : InfixWord litint InfixOp  { $1 =>> \w ->
+            : InfixWord litint InfixOp  {% mkInfixD $1 ($2 ^. _litint) $3 }
-                                          InfixD (extract $1) (extractInt $ extract $2)
-                                          (extract $3) }
 
-InfixWord   :: { Located Assoc }
+InfixWord   :: { Assoc }
-            : infixl                    { $1 \$> InfixL }
+            : infixl                    { InfixL }
-            | infixr                    { $1 \$> InfixR }
+            | infixr                    { InfixR }
-            | infix                     { $1 \$> Infix  }
+            | infix                     { Infix }
 
-DataDecl    :: { Decl' RlpcPs }
+DataDecl    :: { Decl RlpcPs SrcSpan }
-            : data Con TyParams '=' DataCons    { $1 \$> DataD (extract $2) $3 $5 }
+            : data Con TyParams '=' DataCons    { DataD $2 $3 $5 }
 
 TyParams    :: { [PsName] }
             : {- epsilon -}             { [] }
-            | TyParams varname          { $1 `snoc` (extractName . extract $ $2) }
+            | TyParams varname          { $1 `snoc` extractName $2 }
 
 DataCons    :: { [ConAlt RlpcPs] }
             : DataCons '|' DataCon      { $1 `snoc` $3 }
             | DataCon                   { [$1] }
 
 DataCon     :: { ConAlt RlpcPs }
-            : Con Type1s                { ConAlt (extract $1) $2 }
+            : Con Type1s                { ConAlt $1 $2 }
 
-Type1s      :: { [RlpType' RlpcPs] }
+Type1s      :: { [Ty RlpcPs] }
             : {- epsilon -}             { [] }
             | Type1s Type1              { $1 `snoc` $2 }
 
-Type1       :: { RlpType' RlpcPs }
+Type1       :: { Ty RlpcPs }
             : '(' Type ')'              { $2 }
-            | conname                   { fmap ConT (mkPsName $1) }
+            | conname                   { ConT (extractName $1) }
-            | varname                   { fmap VarT (mkPsName $1) }
+            | varname                   { VarT (extractName $1) }
 
-Type        :: { RlpType' RlpcPs }
+Type        :: { Ty RlpcPs }
-            : Type '->' Type            { FunT <<~ $1 <~> $3 }
+            : Type '->' Type            { FunT $1 $3 }
             | TypeApp                   { $1 }
 
-TypeApp     :: { RlpType' RlpcPs }
+TypeApp     :: { Ty RlpcPs }
             : Type1                     { $1 }
-            | TypeApp Type1             { AppT <<~ $1 <~> $2 }
+            | TypeApp Type1             { AppT $1 $2 }
 
-FunDecl     :: { Decl' RlpcPs }
+FunDecl     :: { Decl RlpcPs SrcSpan }
-FunDecl     : Var Params '=' Expr       { $4 =>> \e ->
+FunDecl     : Var Params '=' Expr       { FunD $1 $2 $4 Nothing }
-                                          FunD (extract $1) $2 e Nothing }
 
-Params      :: { [Pat' RlpcPs] }
+Params      :: { [Pat RlpcPs] }
 Params      : {- epsilon -}             { [] }
             | Params Pat1               { $1 `snoc` $2 }
 
-Pat         :: { Pat' RlpcPs }
+Pat         :: { Pat RlpcPs }
-            : Con Pat1s                 { $1 =>> \cn ->
+            : Con Pat1s                 { ConP $1 $2 }
-                                          ConP (extract $1) $2 }
             | Pat1                      { $1 }
 
-Pat1s       :: { [Pat' RlpcPs] }
+Pat1s       :: { [Pat RlpcPs] }
             : Pat1s Pat1                { $1 `snoc` $2 }
             | Pat1                      { [$1] }
 
-Pat1        :: { Pat' RlpcPs }
+Pat1        :: { Pat RlpcPs }
-            : Con                       { fmap (`ConP` []) $1 }
+            : Con                       { ConP $1 [] }
-            | Var                       { fmap VarP $1 }
+            | Var                       { VarP $1 }
-            | Lit                       { LitP <<= $1 }
+            | Lit                       { LitP $1 }
-            | '(' Pat ')'               { $1 .> $2 <. $3 }
+            | '(' Pat ')'               { $2 }
 
-Expr        :: { RlpExpr' RlpcPs }
+Expr        :: { Expr' RlpcPs SrcSpan }
             -- infixities delayed till next release :(
-            -- : Expr1 InfixOp Expr        { $2 =>> \o ->
+            -- : Expr1 InfixOp Expr        { undefined }
-            --                              OAppE (extract o) $1 $3 }
+            : AppExpr                   { $1 }
-            : TempInfixExpr             { $1 }
+            | TempInfixExpr             { $1 }
             | LetExpr                   { $1 }
             | CaseExpr                  { $1 }
-            | AppExpr                   { $1 }
 
-TempInfixExpr :: { RlpExpr' RlpcPs }
+TempInfixExpr :: { Expr' RlpcPs SrcSpan }
 TempInfixExpr : Expr1 InfixOp TempInfixExpr {% tempInfixExprErr $1 $3 }
-              | Expr1 InfixOp Expr1 { $2 =>> \o ->
+              | Expr1 InfixOp Expr1         { nolo' $ InfixEF $2 $1 $3 }
-                                      OAppE (extract o) $1 $3 }
 
-AppExpr     :: { RlpExpr' RlpcPs }
+AppExpr     :: { Expr' RlpcPs SrcSpan }
             : Expr1                     { $1 }
-            | AppExpr Expr1             { AppE <<~ $1 <~> $2 }
+            | AppExpr Expr1             { comb2 AppEF $1 $2 }
 
-LetExpr     :: { RlpExpr' RlpcPs }
+LetExpr     :: { Expr' RlpcPs SrcSpan }
-            : let layout1(Binding) in Expr      { $1 \$> LetE $2 $4 }
+            : let layout1(Binding) in Expr      { nolo' $ LetEF NonRec $2 $4 }
-            | letrec layout1(Binding) in Expr   { $1 \$> LetrecE $2 $4 }
+            | letrec layout1(Binding) in Expr   { nolo' $ LetEF Rec $2 $4 }
 
-CaseExpr    :: { RlpExpr' RlpcPs }
+CaseExpr    :: { Expr' RlpcPs SrcSpan }
-            : case Expr of layout0(CaseAlt)
+            : case Expr of layout0(Alt)     { nolo' $ CaseEF $2 $4 }
-                { CaseE <<~ $2 <#> $4 }
 
 -- TODO: where-binds
-CaseAlt     :: { (Alt RlpcPs, Where RlpcPs) }
+Alt         :: { Alt' RlpcPs SrcSpan }
-            : Alt                           { ($1, []) }
+            : Pat '->' Expr                 { AltA $1 (view _unwrap $3) Nothing }
-
-Alt         :: { Alt RlpcPs }
-            : Pat '->' Expr                 { AltA $1 $3 }
 
 -- layout0(p : β) :: [β]
 layout0(p)  : '{' layout_list0(';',p) '}'   { $2 }
@@ -222,38 +203,68 @@ layout1(p)  : '{' layout_list1(';',p) '}'   { $2 }
 layout_list1(sep,p) : p                          { [$1] }
                     | layout_list1(sep,p) sep p  { $1 `snoc` $3 }
 
-Binding     :: { Binding' RlpcPs }
+Binding     :: { Binding' RlpcPs SrcSpan }
-            : Pat '=' Expr              { PatB <<~ $1 <~> $3 }
+            : Pat '=' Expr              { PatB $1 (view _unwrap $3) }
 
-Expr1       :: { RlpExpr' RlpcPs }
+Expr1       :: { Expr' RlpcPs SrcSpan }
-            : '(' Expr ')'              { $1 .> $2 <. $3 }
+            : '(' Expr ')'              { $2 }
-            | Lit                       { fmap LitE $1 }
+            | Lit                       { nolo' $ LitEF $1 }
-            | Var                       { fmap VarE $1 }
+            | Var                       { case $1 of Located ss _ -> ss :< VarEF $1 }
-            | Con                       { fmap VarE $1 }
+            | Con                       { case $1 of Located ss _ -> ss :< VarEF $1 }
 
-InfixOp     :: { Located PsName }
+InfixOp     :: { PsName }
-            : consym                    { mkPsName $1 }
+            : consym                    { extractName $1 }
-            | varsym                    { mkPsName $1 }
+            | varsym                    { extractName $1 }
 
 -- TODO: microlens-pro save me microlens-pro (rewrite this with prisms)
-Lit         :: { Lit' RlpcPs }
+Lit         :: { Lit RlpcPs }
-            : litint                    { $1 <&> (IntL . (\ (TokenLitInt n) -> n)) }
+            : litint                    { $1 ^. to extract
+                                              . singular _TokenLitInt
+                                              . to IntL }
 
-Var         :: { Located PsName }
+Var         :: { PsName }
-Var         : varname                   { mkPsName $1 }
+Var         : varname                   { $1 <&> view (singular _TokenVarName) }
-            | varsym                    { mkPsName $1 }
+            | varsym                    { $1 <&> view (singular _TokenVarSym) }
 
-Con         :: { Located PsName }
+Con         :: { PsName }
-            : conname                   { mkPsName $1 }
+            : conname                   { $1 <&> view (singular _TokenConName) }
 
 {
 
-parseRlpExprR :: (Monad m) => Text -> RLPCT m (RlpExpr RlpcPs)
+parseRlpProgR :: (Monad m) => Text -> RLPCT m (Program RlpcPs SrcSpan)
+parseRlpProgR s = do
+    a <- liftErrorful $ pToErrorful parseRlpProg st
+    addDebugMsg @_ @String "dump-parsed" $ show a
+    pure a
+  where
+    st = programInitState s
+
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (Expr' RlpcPs SrcSpan)
 parseRlpExprR s = liftErrorful $ pToErrorful parseRlpExpr st
     where
         st = programInitState s
 
-parseRlpProgR :: (Monad m) => Text -> RLPCT m (RlpProgram RlpcPs)
+mkInfixD :: Assoc -> Int -> PsName -> P (Decl RlpcPs SrcSpan)
+mkInfixD a p ln@(Located ss n) = do
+    let opl :: Lens' ParseState (Maybe OpInfo)
+        opl = psOpTable . at n
+    opl <~ (use opl >>= \case
+        Just o  -> addWoundHere l e >> pure (Just o) where
+            e = RlpParErrDuplicateInfixD n
+            l = T.length n
+        Nothing -> pure (Just (a,p))
+        )
+    pos <- use (psInput . aiPos)
+    pure $ InfixD a p ln
+
+{--
+
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (Expr RlpcPs)
+parseRlpExprR s = liftErrorful $ pToErrorful parseRlpExpr st
+    where
+        st = programInitState s
+
+parseRlpProgR :: (Monad m) => Text -> RLPCT m (Program RlpcPs)
 parseRlpProgR s = do
     a <- liftErrorful $ pToErrorful parseRlpProg st
     addDebugMsg @_ @String "dump-parsed" $ show a
@@ -276,37 +287,48 @@ extractInt :: RlpToken -> Int
 extractInt (TokenLitInt n) = n
 extractInt _ = error "extractInt: ugh"
 
-mkProgram :: [Decl' RlpcPs] -> P (RlpProgram RlpcPs)
+mkProgram :: [Decl RlpcPs SrcSpan] -> P (Program RlpcPs SrcSpan)
 mkProgram ds = do
     pt <- use psOpTable
-    pure $ RlpProgram (associate pt <$> ds)
+    pure $ Program (associate pt <$> ds)
-
-parseError :: (Located RlpToken, [String]) -> P a
-parseError ((Located ss t), exp) = addFatal $
-    errorMsg ss (RlpParErrUnexpectedToken t exp)
-
-mkInfixD :: Assoc -> Int -> PsName -> P (Decl' RlpcPs)
-mkInfixD a p n = do
-    let opl :: Lens' ParseState (Maybe OpInfo)
-        opl = psOpTable . at n
-    opl <~ (use opl >>= \case
-        Just o  -> addWoundHere l e >> pure (Just o) where
-            e = RlpParErrDuplicateInfixD n
-            l = T.length n
-        Nothing -> pure (Just (a,p))
-        )
-    pos <- use (psInput . aiPos)
-    pure $ Located (spanFromPos pos 0) (InfixD a p n)
 
 intOfToken :: Located RlpToken -> Int
 intOfToken (Located _ (TokenLitInt n)) = n
 
-tempInfixExprErr :: RlpExpr' RlpcPs -> RlpExpr' RlpcPs -> P a
+tempInfixExprErr :: Expr RlpcPs -> Expr RlpcPs -> P a
 tempInfixExprErr (Located a _) (Located b _) =
     addFatal $ errorMsg (a <> b) $ RlpParErrOther
         [ "The rl' frontend is currently in beta. Support for infix expressions is minimal, sorry! :("
         , "In the mean time, don't mix any infix operators."
         ]
 
+--}
+
+_litint :: Getter (Located RlpToken) Int
+_litint = to extract
+        . singular _TokenLitInt
+
+tempInfixExprErr :: Expr' RlpcPs SrcSpan -> Expr' RlpcPs SrcSpan -> P a
+tempInfixExprErr (a :< _) (b :< _) =
+    addFatal $ errorMsg (a <> b) $ RlpParErrOther
+        [ "The rl' frontend is currently in beta. Support for infix expressions is minimal, sorry! :("
+        , "In the mean time, don't mix any infix operators."
+        ]
+
+mkProgram :: [Decl RlpcPs SrcSpan] -> P (Program RlpcPs SrcSpan)
+mkProgram ds = do
+    pt <- use psOpTable
+    pure $ Program (associate pt <$> ds)
+
+extractName :: Located RlpToken -> PsName
+extractName (Located ss (TokenVarSym n)) = Located ss n
+extractName (Located ss (TokenVarName n)) = Located ss n
+extractName (Located ss (TokenConName n)) = Located ss n
+extractName (Located ss (TokenConSym n)) = Located ss n
+
+parseError :: (Located RlpToken, [String]) -> P a
+parseError ((Located ss t), exp) = addFatal $
+    errorMsg ss (RlpParErrUnexpectedToken t exp)
+
 }
 

src/Rlp/Parse/Associate.hs

@@ -16,7 +16,7 @@ import Rlp.Parse.Types
 import Rlp.Syntax
 --------------------------------------------------------------------------------
 
-associate :: OpTable -> Decl' RlpcPs -> Decl' RlpcPs
+associate :: OpTable -> Decl RlpcPs a -> Decl RlpcPs a
 associate _ p = p
 
 {-# WARNING associate "unimplemented" #-}

src/Rlp/Parse/Types.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE ImplicitParams, ViewPatterns, PatternSynonyms #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Rlp.Parse.Types
     (
     -- * Trees That Grow
@@ -16,11 +17,11 @@ module Rlp.Parse.Types
     -- * Other parser types
     , RlpToken(..), AlexInput(..), Position(..), spanFromPos, LexerAction
     , Located(..), PsName
+    , srcSpanLen
     -- ** Lenses
+    , _TokenLitInt, _TokenVarName, _TokenConName, _TokenVarSym, _TokenConSym
     , aiPrevChar, aiSource, aiBytes, aiPos, posLine, posColumn
 
-    , (<<~), (<~>)
-
     -- * Error handling
     , MsgEnvelope(..), RlpcError(..), RlpParseError(..)
     , addFatal, addWound, addFatalHere, addWoundHere
@@ -28,6 +29,7 @@ module Rlp.Parse.Types
     where
 --------------------------------------------------------------------------------
 import Core.Syntax                  (Name)
+import Text.Show.Deriving
 import Control.Monad
 import Control.Monad.State.Strict
 import Control.Monad.Errorful
@@ -53,34 +55,9 @@ import Compiler.Types
 
 data RlpcPs
 
-type instance XRec RlpcPs a = Located a
+type instance NameP RlpcPs = PsName
-type instance IdP RlpcPs = PsName
 
-type instance XFunD RlpcPs = ()
+type PsName = Located Text
-type instance XDataD RlpcPs = ()
-type instance XInfixD RlpcPs = ()
-type instance XTySigD RlpcPs = ()
-type instance XXDeclD RlpcPs = ()
-
-type instance XLetE RlpcPs = ()
-type instance XLetrecE RlpcPs = ()
-type instance XVarE RlpcPs = ()
-type instance XLamE RlpcPs = ()
-type instance XCaseE RlpcPs = ()
-type instance XIfE RlpcPs = ()
-type instance XAppE RlpcPs = ()
-type instance XLitE RlpcPs = ()
-type instance XParE RlpcPs = ()
-type instance XOAppE RlpcPs = ()
-type instance XXRlpExprE RlpcPs = ()
-
-type PsName = Text
-
-instance MapXRec RlpcPs where
-    mapXRec = fmap
-
-instance UnXRec RlpcPs where
-    unXRec = extract
 
 --------------------------------------------------------------------------------
 
@@ -118,10 +95,10 @@ data RlpToken
     -- literals
     = TokenLitInt Int
     -- identifiers
-    | TokenVarName Name
+    | TokenVarName Text
-    | TokenConName Name
+    | TokenConName Text
-    | TokenVarSym Name
+    | TokenVarSym Text
-    | TokenConSym Name
+    | TokenConSym Text
     -- reserved words
     | TokenData
     | TokenCase
@@ -132,6 +109,7 @@ data RlpToken
     | TokenInfixL
     | TokenInfixR
     | TokenInfix
+    | TokenForall
     -- reserved ops
     | TokenArrow
     | TokenPipe
@@ -152,6 +130,31 @@ data RlpToken
     | TokenEOF
     deriving (Show)
 
+_TokenLitInt :: Prism' RlpToken Int
+_TokenLitInt = prism TokenLitInt $ \case
+    TokenLitInt n -> Right n
+    x             -> Left x
+
+_TokenVarName :: Prism' RlpToken Text
+_TokenVarName = prism TokenVarName $ \case
+    TokenVarName n -> Right n
+    x              -> Left x
+
+_TokenVarSym :: Prism' RlpToken Text
+_TokenVarSym = prism TokenVarSym $ \case
+    TokenVarSym n -> Right n
+    x              -> Left x
+
+_TokenConName :: Prism' RlpToken Text
+_TokenConName = prism TokenConName $ \case
+    TokenConName n -> Right n
+    x              -> Left x
+
+_TokenConSym :: Prism' RlpToken Text
+_TokenConSym = prism TokenConSym $ \case
+    TokenConSym n -> Right n
+    x              -> Left x
+
 newtype P a = P {
         runP :: ParseState
              -> (ParseState, [MsgEnvelope RlpParseError], Maybe a)
@@ -281,13 +284,14 @@ initAlexInput s = AlexInput
 
 --------------------------------------------------------------------------------
 
-deriving instance Lift (RlpProgram RlpcPs)
+
-deriving instance Lift (Decl RlpcPs)
+-- deriving instance Lift (Program RlpcPs)
-deriving instance Lift (Pat RlpcPs)
+-- deriving instance Lift (Decl RlpcPs)
-deriving instance Lift (Lit RlpcPs)
+-- deriving instance Lift (Pat RlpcPs)
-deriving instance Lift (RlpExpr RlpcPs)
+-- deriving instance Lift (Lit RlpcPs)
-deriving instance Lift (Binding RlpcPs)
+-- deriving instance Lift (Expr RlpcPs)
-deriving instance Lift (RlpType RlpcPs)
+-- deriving instance Lift (Binding RlpcPs)
-deriving instance Lift (Alt RlpcPs)
+-- deriving instance Lift (Ty RlpcPs)
-deriving instance Lift (ConAlt RlpcPs)
+-- deriving instance Lift (Alt RlpcPs)
+-- deriving instance Lift (ConAlt RlpcPs)
 

src/Rlp/Syntax.hs

@@ -1,362 +1,10 @@
--- recursion-schemes
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable
-  , TemplateHaskell, TypeFamilies #-}
-{-# LANGUAGE OverloadedStrings, PatternSynonyms, ViewPatterns #-}
-{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
-{-# LANGUAGE UndecidableInstances, ImpredicativeTypes #-}
 module Rlp.Syntax
-    (
+    ( module Rlp.Syntax.Backstage
-    -- * AST
+    , module Rlp.Syntax.Types
-      RlpProgram(..)
-    , progDecls
-    , Decl(..), Decl', RlpExpr(..), RlpExpr', RlpExprF(..)
-    , Pat(..), Pat'
-    , Alt(..), Where
-    , Assoc(..)
-    , Lit(..), Lit'
-    , RlpType(..), RlpType'
-    , ConAlt(..)
-    , Binding(..), Binding'
-
-    , _PatB, _FunB
-    , _VarP, _LitP, _ConP
-
-    -- * Trees That Grow boilerplate
-    -- ** Extension points
-    , IdP, IdP', XRec, UnXRec(..), MapXRec(..)
-    -- *** Decl
-    , XFunD, XTySigD, XInfixD, XDataD, XXDeclD
-    -- *** RlpExpr
-    , XLetE, XLetrecE, XVarE, XLamE, XCaseE, XIfE, XAppE, XLitE
-    , XParE, XOAppE, XXRlpExprE
-    -- ** Pattern synonyms
-    -- *** Decl
-    , pattern FunD, pattern TySigD, pattern InfixD, pattern DataD
-    , pattern FunD'', pattern TySigD'', pattern InfixD'', pattern DataD''
-    -- *** RlpExpr
-    , pattern LetE, pattern LetrecE, pattern VarE, pattern LamE, pattern CaseE
-    , pattern IfE , pattern AppE, pattern LitE, pattern ParE, pattern OAppE
-    , pattern XRlpExprE
-    -- *** RlpType
-    , pattern FunConT'', pattern FunT'', pattern AppT'', pattern VarT''
-    , pattern ConT''
-    -- *** Pat
-    , pattern VarP'', pattern LitP'', pattern ConP''
-    -- *** Binding
-    , pattern PatB''
     )
     where
-----------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
-import Data.Text                    (Text)
+import Rlp.Syntax.Backstage
-import Data.Text                    qualified as T
+import Rlp.Syntax.Types
-import Data.String                  (IsString(..))
-import Data.Functor.Foldable
-import Data.Functor.Foldable.TH     (makeBaseFunctor)
-import Data.Functor.Classes
-import Data.Functor.Identity
-import Data.Kind                    (Type)
-import GHC.Generics
-import Language.Haskell.TH.Syntax   (Lift)
-import Control.Lens
-import Core.Syntax                  hiding (Lit, Type, Binding, Binding')
-import Core                         (HasRHS(..), HasLHS(..))
-----------------------------------------------------------------------------------
-
-data RlpModule p = RlpModule
-    { _rlpmodName       :: Text
-    , _rlpmodProgram    :: RlpProgram p
-    }
-
--- | dear god.
-type PhaseShow p =
-    ( Show (XRec p (Pat p)), Show (XRec p (RlpExpr p))
-    , Show (XRec p (Lit p)), Show (IdP p)
-    , Show (XRec p (RlpType p))
-    , Show (XRec p (Binding p))
-    )
-
-newtype RlpProgram p = RlpProgram [Decl' p]
-
-progDecls :: Lens' (RlpProgram p) [Decl' p]
-progDecls = lens
-    (\ (RlpProgram ds) -> ds)
-    (const RlpProgram)
-
-deriving instance (PhaseShow p, Show (XRec p (Decl p))) => Show (RlpProgram p)
-
-data RlpType p = FunConT
-               | FunT (RlpType' p) (RlpType' p)
-               | AppT (RlpType' p) (RlpType' p)
-               | VarT (IdP p)
-               | ConT (IdP p)
-
-type RlpType' p = XRec p (RlpType p)
-
-pattern FunConT'' :: (UnXRec p) => RlpType' p
-pattern FunT''    :: (UnXRec p) => RlpType' p -> RlpType' p -> RlpType' p
-pattern AppT''    :: (UnXRec p) => RlpType' p -> RlpType' p -> RlpType' p
-pattern VarT''    :: (UnXRec p) => IdP p -> RlpType' p
-pattern ConT''    :: (UnXRec p) => IdP p -> RlpType' p
-
-pattern FunConT''     <- (unXRec -> FunConT)
-pattern FunT''    s t <- (unXRec -> FunT s t)
-pattern AppT''    s t <- (unXRec -> AppT s t)
-pattern VarT''    n   <- (unXRec -> VarT n)
-pattern ConT''    n   <- (unXRec -> ConT n)
-
-deriving instance (PhaseShow p)
-                  => Show (RlpType p)
-
-data Decl p = FunD'   (XFunD p)    (IdP p) [Pat' p] (RlpExpr' p) (Maybe (Where p))
-            | TySigD' (XTySigD p)  [IdP p] (RlpType' p)
-            | DataD'  (XDataD p)   (IdP p) [IdP p] [ConAlt p]
-            | InfixD' (XInfixD p)  Assoc Int (IdP p)
-            | XDeclD' !(XXDeclD p)
-
-deriving instance
-    ( Show (XFunD p), Show (XTySigD p)
-    , Show (XDataD p), Show (XInfixD p)
-    , Show (XXDeclD p)
-    , PhaseShow p
-    ) 
-    => Show (Decl p)
-
-type family XFunD p
-type family XTySigD p
-type family XDataD p
-type family XInfixD p
-type family XXDeclD p
-
-pattern FunD   :: (XFunD p ~ ())
-               => IdP p -> [Pat' p] -> RlpExpr' p -> Maybe (Where p)
-               -> Decl p
-pattern TySigD :: (XTySigD p ~ ()) => [IdP p] -> RlpType' p -> Decl p
-pattern DataD  :: (XDataD p ~ ()) => IdP p -> [IdP p] -> [ConAlt p] -> Decl p
-pattern InfixD :: (XInfixD p ~ ()) => Assoc -> Int -> IdP p -> Decl p
-pattern XDeclD :: (XXDeclD p ~ ()) => Decl p
-
-pattern FunD n as e wh = FunD' () n as e wh
-pattern TySigD ns t    = TySigD' () ns t
-pattern DataD n as cs  = DataD' () n as cs
-pattern InfixD a p n   = InfixD' () a p n
-pattern XDeclD         = XDeclD' ()
-
-pattern FunD''   :: (UnXRec p)
-                 => IdP p -> [Pat' p] -> RlpExpr' p -> Maybe (Where p)
-                 -> Decl' p
-pattern TySigD'' :: (UnXRec p)
-                 => [IdP p] -> RlpType' p -> Decl' p
-pattern DataD''  :: (UnXRec p)
-                 => IdP p -> [IdP p] -> [ConAlt p] -> Decl' p
-pattern InfixD'' :: (UnXRec p)
-                 => Assoc -> Int -> IdP p -> Decl' p
-
-pattern FunD''   n as e wh <- (unXRec -> FunD' _ n as e wh)
-pattern TySigD'' ns t      <- (unXRec -> TySigD' _ ns t)
-pattern DataD''  n as ds   <- (unXRec -> DataD' _ n as ds)
-pattern InfixD'' a p n     <- (unXRec -> InfixD' _ a p n)
-
-type Decl' p = XRec p (Decl p)
-
-data Assoc = InfixL
-           | InfixR
-           | Infix
-           deriving (Show, Lift)
-
-data ConAlt p = ConAlt (IdP p) [RlpType' p]
-
-deriving instance (Show (IdP p), Show (XRec p (RlpType p))) => Show (ConAlt p)
-
-data RlpExpr p = LetE'      (XLetE p) [Binding' p] (RlpExpr' p)
-               | LetrecE'   (XLetrecE p) [Binding' p] (RlpExpr' p)
-               | VarE'      (XVarE p) (IdP p)
-               | LamE'      (XLamE p) [Pat p] (RlpExpr' p)
-               | CaseE'     (XCaseE p) (RlpExpr' p) [(Alt p, Where p)]
-               | IfE'       (XIfE p) (RlpExpr' p) (RlpExpr' p) (RlpExpr' p)
-               | AppE'      (XAppE p) (RlpExpr' p) (RlpExpr' p)
-               | LitE'      (XLitE p) (Lit p)
-               | ParE'      (XParE p) (RlpExpr' p)
-               | OAppE'     (XOAppE p) (IdP p) (RlpExpr' p) (RlpExpr' p)
-               | XRlpExprE' !(XXRlpExprE p)
-               deriving (Generic)
-
-type family XLetE p
-type family XLetrecE p
-type family XVarE p
-type family XLamE p
-type family XCaseE p
-type family XIfE p
-type family XAppE p
-type family XLitE p
-type family XParE p
-type family XOAppE p
-type family XXRlpExprE p
-
-pattern LetE :: (XLetE p ~ ()) => [Binding' p] -> RlpExpr' p -> RlpExpr p
-pattern LetrecE :: (XLetrecE p ~ ()) => [Binding' p] -> RlpExpr' p -> RlpExpr p
-pattern VarE :: (XVarE p ~ ()) => IdP p -> RlpExpr p
-pattern LamE :: (XLamE p ~ ()) => [Pat p] -> RlpExpr' p -> RlpExpr p
-pattern CaseE :: (XCaseE p ~ ()) => RlpExpr' p -> [(Alt p, Where p)] -> RlpExpr p
-pattern IfE :: (XIfE p ~ ()) => RlpExpr' p -> RlpExpr' p -> RlpExpr' p -> RlpExpr p
-pattern AppE :: (XAppE p ~ ()) => RlpExpr' p -> RlpExpr' p -> RlpExpr p
-pattern LitE :: (XLitE p ~ ()) => Lit p -> RlpExpr p
-pattern ParE :: (XParE p ~ ()) => RlpExpr' p -> RlpExpr p
-pattern OAppE :: (XOAppE p ~ ()) => IdP p -> RlpExpr' p -> RlpExpr' p -> RlpExpr p
-pattern XRlpExprE :: (XXRlpExprE p ~ ()) => RlpExpr p
-
-pattern LetE bs e = LetE' () bs e
-pattern LetrecE bs e = LetrecE' () bs e
-pattern VarE n = VarE' () n
-pattern LamE as e = LamE' () as e
-pattern CaseE e as = CaseE' () e as
-pattern IfE c a b = IfE' () c a b
-pattern AppE f x = AppE' () f x
-pattern LitE l = LitE' () l
-pattern ParE e = ParE' () e
-pattern OAppE n a b = OAppE' () n a b
-pattern XRlpExprE = XRlpExprE' ()
-
-deriving instance
-    ( Show (XLetE p), Show (XLetrecE p), Show (XVarE p)
-    , Show (XLamE p), Show (XCaseE p), Show (XIfE p)
-    , Show (XAppE p), Show (XLitE p), Show (XParE p)
-    , Show (XOAppE p), Show (XXRlpExprE p)
-    , PhaseShow p
-    ) => Show (RlpExpr p)
-
-type RlpExpr' p = XRec p (RlpExpr p)
-
-class UnXRec p where
-    unXRec :: XRec p a -> a
-
-class WrapXRec p where
-    wrapXRec :: a -> XRec p a
-
-class MapXRec p where
-    mapXRec :: (a -> b) -> XRec p a -> XRec p b
-
--- old definition:
--- type family XRec p (f :: Type -> Type) = (r :: Type) | r -> p f
-type family XRec p a = (r :: Type) | r -> p a
-
-type family IdP p
-
-type IdP' p = XRec p (IdP p)
-
-type Where p = [Binding p]
-
--- do we want guards?
-data Alt p = AltA (Pat' p) (RlpExpr' p)
-
-deriving instance (PhaseShow p) => Show (Alt p)
-
-data Binding p = PatB (Pat' p) (RlpExpr' p)
-               | FunB (IdP p) [Pat' p] (RlpExpr' p)
-
-type Binding' p = XRec p (Binding p)
-
-pattern PatB'' :: (UnXRec p) => Pat' p -> RlpExpr' p -> Binding' p
-pattern PatB'' p e <- (unXRec -> PatB p e)
-
-deriving instance (Show (XRec p (Pat p)), Show (XRec p (RlpExpr p)), Show (IdP p)
-                  ) => Show (Binding p)
-
-data Pat p = VarP (IdP p)
-           | LitP (Lit' p)
-           | ConP (IdP p) [Pat' p]
-
-pattern VarP'' :: (UnXRec p) => IdP p -> Pat' p
-pattern LitP'' :: (UnXRec p) => Lit' p -> Pat' p
-pattern ConP'' :: (UnXRec p) => IdP p -> [Pat' p] -> Pat' p
-
-pattern VarP'' n    <- (unXRec -> VarP n)
-pattern LitP'' l    <- (unXRec -> LitP l)
-pattern ConP'' c as <- (unXRec -> ConP c as)
-
-deriving instance (PhaseShow p) => Show (Pat p)
-
-type Pat' p = XRec p (Pat p)
-
-data Lit p = IntL Int
-           | CharL Char
-           | ListL [RlpExpr' p]
-
-deriving instance (PhaseShow p) => Show (Lit p)
-
-type Lit' p = XRec p (Lit p)
-
--- instance HasLHS Alt Alt Pat Pat where
---     _lhs = lens
---         (\ (AltA p _) -> p)
---         (\ (AltA _ e) p' -> AltA p' e)
-
--- instance HasRHS Alt Alt RlpExpr RlpExpr where
---     _rhs = lens
---         (\ (AltA _ e) -> e)
---         (\ (AltA p _) e' -> AltA p e')
-
--- makeBaseFunctor ''RlpExpr
-
--- showsTernaryWith :: (Int -> x -> ShowS)
---                  -> (Int -> y -> ShowS)
---                  -> (Int -> z -> ShowS)
---                  -> String -> Int
---                  -> x -> y -> z
---                  -> ShowS
--- showsTernaryWith sa sb sc name p a b c = showParen (p > 10)
---     $ showString name
---     . showChar ' ' . sa 11 a 
---     . showChar ' ' . sb 11 b
---     . showChar ' ' . sc 11 c
-
 --------------------------------------------------------------------------------
 
-makeLenses ''RlpModule
-makePrisms ''Pat
-makePrisms ''Binding
-
---------------------------------------------------------------------------------
-
-data RlpExprF p a = LetE'F  (XLetE p) [Binding' p] a
-                  | LetrecE'F  (XLetrecE p) [Binding' p] a
-                  | VarE'F  (XVarE p) (IdP p)
-                  | LamE'F  (XLamE p) [Pat p] a
-                  | CaseE'F (XCaseE p) a [(Alt p, Where p)]
-                  | IfE'F   (XIfE p) a a a
-                  | AppE'F  (XAppE p) a a
-                  | LitE'F  (XLitE p) (Lit p)
-                  | ParE'F  (XParE p) a
-                  | OAppE'F (XOAppE p) (IdP p) a a
-                  | XRlpExprE'F !(XXRlpExprE p)
-                  deriving (Functor, Foldable, Traversable, Generic)
-
-type instance Base (RlpExpr p) = RlpExprF p
-
-instance (UnXRec p) => Recursive (RlpExpr p) where
-    project = \case
-        LetE' xx bs e   -> LetE'F xx bs (unXRec e)
-        LetrecE' xx bs e   -> LetrecE'F xx bs (unXRec e)
-        VarE' xx n      -> VarE'F xx n
-        LamE' xx ps e   -> LamE'F xx ps (unXRec e)
-        CaseE' xx e as  -> CaseE'F xx (unXRec e) as
-        IfE' xx a b c   -> IfE'F xx (unXRec a) (unXRec b) (unXRec c)
-        AppE' xx f x    -> AppE'F xx (unXRec f) (unXRec x)
-        LitE' xx l      -> LitE'F xx l
-        ParE' xx e      -> ParE'F xx (unXRec e)
-        OAppE' xx f a b -> OAppE'F xx f (unXRec a) (unXRec b)
-        XRlpExprE' xx   -> XRlpExprE'F xx
-
-instance (WrapXRec p) => Corecursive (RlpExpr p) where
-    embed = \case
-        LetE'F xx bs e   -> LetE' xx bs (wrapXRec e)
-        LetrecE'F xx bs e   -> LetrecE' xx bs (wrapXRec e)
-        VarE'F xx n      -> VarE' xx n
-        LamE'F xx ps e   -> LamE' xx ps (wrapXRec e)
-        CaseE'F xx e as  -> CaseE' xx (wrapXRec e) as
-        IfE'F xx a b c   -> IfE' xx (wrapXRec a) (wrapXRec b) (wrapXRec c)
-        AppE'F xx f x    -> AppE' xx (wrapXRec f) (wrapXRec x)
-        LitE'F xx l      -> LitE' xx l
-        ParE'F xx e      -> ParE' xx (wrapXRec e)
-        OAppE'F xx f a b -> OAppE' xx f (wrapXRec a) (wrapXRec b)
-        XRlpExprE'F xx   -> XRlpExprE' xx
-

src/Rlp/Syntax/Backstage.hs

@@ -0,0 +1,35 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Rlp.Syntax.Backstage
+    ( strip
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Fix                     hiding (cata)
+import Data.Functor.Classes
+import Data.Functor.Foldable
+import Rlp.Syntax.Types
+import Text.Show.Deriving
+import Language.Haskell.TH.Syntax   (Lift)
+--------------------------------------------------------------------------------
+
+-- oprhan instances because TH
+
+instance (Show (NameP p)) => Show1 (Alt p) where
+    liftShowsPrec = $(makeLiftShowsPrec ''Alt)
+
+instance (Show (NameP p)) => Show1 (Binding p) where
+    liftShowsPrec = $(makeLiftShowsPrec ''Binding)
+
+instance (Show (NameP p)) => Show1 (ExprF p) where
+    liftShowsPrec = $(makeLiftShowsPrec ''ExprF)
+
+deriving instance (Lift (NameP p), Lift a) => Lift (Expr' p a)
+deriving instance (Lift (NameP p), Lift a) => Lift (Decl p a)
+deriving instance (Show (NameP p), Show a) => Show (Decl p a)
+
+deriving instance (Show (NameP p), Show a) => Show (Program p a)
+
+strip :: Functor f => Cofree f a -> Fix f
+strip (_ :< as) = Fix $ strip <$> as
+

src/Rlp/Syntax/Types.hs

@@ -0,0 +1,145 @@
+-- recursion-schemes
+{-# LANGUAGE DeriveTraversable, TemplateHaskell, TypeFamilies #-}
+{-# LANGUAGE OverloadedStrings, PatternSynonyms, ViewPatterns #-}
+{-# LANGUAGE UndecidableInstances, ImpredicativeTypes #-}
+module Rlp.Syntax.Types
+    (
+      NameP
+    , SimpleP
+    , Assoc(..)
+    , ConAlt(..)
+    , Alt(..), Alt'
+    , Ty(..)
+    , Binding(..), Binding'
+    , Expr', ExprF(..)
+    , Rec(..)
+    , Lit(..)
+    , Pat(..)
+    , Decl(..), Decl'
+    , Program(..)
+    , Where
+
+    -- * Re-exports
+    , Cofree(..)
+    , Trans.Cofree.CofreeF
+    , SrcSpan(..)
+
+    , programDecls
+    )
+    where
+----------------------------------------------------------------------------------
+import Data.Text                    (Text)
+import Data.Text                    qualified as T
+import Data.String                  (IsString(..))
+import Data.Functor.Classes
+import Data.Functor.Identity
+import Data.Functor.Compose
+import Data.Fix
+import Data.Kind                    (Type)
+import GHC.Generics
+import Language.Haskell.TH.Syntax   (Lift)
+import Control.Lens                 hiding ((:<))
+
+import Control.Comonad.Trans.Cofree qualified as Trans.Cofree
+import Control.Comonad.Cofree
+import Data.Functor.Foldable
+import Data.Functor.Foldable.TH     (makeBaseFunctor)
+
+import Compiler.Types               (SrcSpan(..), Located(..))
+import Core.Syntax                  qualified as Core
+import Core                         (Rec(..), HasRHS(..), HasLHS(..))
+----------------------------------------------------------------------------------
+
+data SimpleP
+
+type instance NameP SimpleP = String
+
+type family NameP p
+
+data ExprF p a = LetEF   Rec [Binding p a] a
+               | VarEF   (NameP p)
+               | LamEF   [Pat p] a
+               | CaseEF  a [Alt p a]
+               | IfEF    a a a
+               | AppEF   a a
+               | LitEF   (Lit p)
+               | ParEF   a
+               | InfixEF (NameP p) a a
+               deriving (Functor, Foldable, Traversable)
+
+data ConAlt p = ConAlt (NameP p) [Ty p]
+
+deriving instance (Lift (NameP p)) => Lift (ConAlt p)
+deriving instance (Show (NameP p)) => Show (ConAlt p)
+
+data Ty p = ConT (NameP p)
+          | VarT (NameP p)
+          | FunT (Ty p) (Ty p)
+          | AppT (Ty p) (Ty p)
+
+deriving instance (Show (NameP p)) => Show (Ty p)
+deriving instance (Lift (NameP p)) => Lift (Ty p)
+
+data Pat p = VarP (NameP p)
+           | LitP (Lit p)
+           | ConP (NameP p) [Pat p]
+
+deriving instance (Lift (NameP p)) => Lift (Pat p)
+deriving instance (Show (NameP p)) => Show (Pat p)
+
+data Lit p = IntL Int
+    deriving Show
+
+deriving instance (Lift (NameP p)) => Lift (Lit p)
+
+data Assoc = InfixL | InfixR | Infix
+    deriving (Lift, Show)
+
+deriving instance (Show (NameP p), Show a) => Show (ExprF p a)
+deriving instance (Lift (NameP p), Lift a) => Lift (ExprF p a)
+
+data Binding p a = PatB (Pat p) (ExprF p a)
+    deriving (Functor, Foldable, Traversable)
+
+deriving instance (Lift (NameP p), Lift a) => Lift (Binding p a)
+deriving instance (Show (NameP p), Show a) => Show (Binding p a)
+
+type Binding' p a = Binding p (Cofree (ExprF p) a)
+
+type Where p a = [Binding p a]
+
+data Alt p a = AltA (Pat p) (ExprF p a) (Maybe (Where p a))
+    deriving (Functor, Foldable, Traversable)
+
+deriving instance (Show (NameP p), Show a) => Show (Alt p a)
+deriving instance (Lift (NameP p), Lift a) => Lift (Alt p a)
+
+type Expr p = Fix (ExprF p)
+
+type Alt' p a = Alt p (Cofree (ExprF p) a)
+
+--------------------------------------------------------------------------------
+
+data Program p a = Program
+    { _programDecls :: [Decl p a]
+    }
+
+data Decl p a = FunD   (NameP p) [Pat p] (Expr' p a) (Maybe (Where p a))
+              | TySigD [NameP p] (Ty p)
+              | DataD  (NameP p) [NameP p] [ConAlt p]
+              | InfixD Assoc Int (NameP p)
+
+type Decl' p a = Decl p (Cofree (ExprF p) a)
+
+type Expr' p = Cofree (ExprF p)
+
+makeLenses ''Program
+
+loccof :: Iso' (Cofree f SrcSpan) (Located (f (Cofree f SrcSpan)))
+loccof = iso sa bt where
+    sa :: Cofree f SrcSpan -> Located (f (Cofree f SrcSpan))
+    sa (ss :< as) = Located ss as
+
+    bt :: Located (f (Cofree f SrcSpan)) -> Cofree f SrcSpan
+    bt (Located ss as) = ss :< as
+

src/Rlp/TH.hs

@@ -13,7 +13,7 @@ import Control.Monad.IO.Class
 import Control.Monad
 
 import Compiler.RLPC
-import Rlp.Parse
+import Rlp.AltParse
 --------------------------------------------------------------------------------
 
 rlpProg :: QuasiQuoter

src/Rlp2Core.hs

@@ -12,8 +12,7 @@ import Control.Monad.Writer.CPS
 import Control.Monad.Utils
 import Control.Arrow
 import Control.Applicative
-import Control.Comonad
+import Control.Lens                     hiding ((:<))
-import Control.Lens
 import Compiler.RLPC
 import Data.List                        (mapAccumL, partition)
 import Data.Text                        (Text)
@@ -22,12 +21,16 @@ import Data.HashMap.Strict              qualified as H
 import Data.Monoid                      (Endo(..))
 import Data.Either                      (partitionEithers)
 import Data.Foldable
-import Data.Fix
 import Data.Maybe                       (fromJust, fromMaybe)
-import Data.Functor.Bind
 import Data.Function                    (on)
 import GHC.Stack
 import Debug.Trace
+import Numeric
+
+import Data.Fix                         hiding (cata, para, cataM)
+import Data.Functor.Bind
+import Data.Functor.Foldable
+import Control.Comonad
 
 import Effectful.State.Static.Local
 import Effectful.Labeled
@@ -35,10 +38,9 @@ import Effectful
 import Text.Show.Deriving
 
 import Core.Syntax                      as Core
+import Rlp.AltSyntax                    as Rlp
 import Compiler.Types
-import Data.Pretty                      (render, pretty)
+import Data.Pretty
-import Rlp.Syntax                       as Rlp
-import Rlp.Parse.Types                  (RlpcPs, PsName)
 --------------------------------------------------------------------------------
 
 type Tree a = Either Name (Name, Branch a)
@@ -59,178 +61,64 @@ deriveShow1 ''Branch
 
 --------------------------------------------------------------------------------
 
-desugarRlpProgR :: forall m. (Monad m) => RlpProgram RlpcPs -> RLPCT m Program'
+-- desugarRlpProgR :: forall m a. (Monad m)
-desugarRlpProgR p = do
+--                 => Rlp.Program PsName (TypedRlpExpr PsName)
-    let p' = desugarRlpProg p
+--                 -> RLPCT m (Core.Program Var)
-    addDebugMsg "dump-desugared" $ render (pretty p')
+-- desugarRlpProgR p = do
-    pure p'
+--     let p' = desugarRlpProg p
+--     addDebugMsg "dump-desugared" $ show (out p')
+--     pure p'
 
-desugarRlpProg :: RlpProgram RlpcPs -> Program'
+desugarRlpProgR = undefined
+
+desugarRlpProg :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var
 desugarRlpProg = rlpProgToCore
 
-desugarRlpExpr :: RlpExpr RlpcPs -> Expr'
+desugarRlpExpr = undefined
-desugarRlpExpr = runPureEff . runNameSupply "anon" . exprToCore
+
+type NameSupply = Labeled "NameSupply" (State [Name])
+
+runNameSupply :: Text -> Eff (NameSupply ': es) a -> Eff es a
+runNameSupply pre = runLabeled $ evalState [ pre <> "_" <> tshow name | name <- [0..] ]
+    where tshow = T.pack . show
 
 -- the rl' program is desugared by desugaring each declaration as a separate
 -- program, and taking the monoidal product of the lot :3
 
-rlpProgToCore :: RlpProgram RlpcPs -> Program'
+rlpProgToCore :: Rlp.Program PsName (TypedRlpExpr PsName) -> Core.Program Var
-rlpProgToCore = foldMapOf (progDecls . each) declToCore
+rlpProgToCore = foldMapOf (programDecls . each) declToCore
 
-declToCore :: Decl' RlpcPs -> Program'
+declToCore :: Rlp.Decl PsName (TypedRlpExpr PsName) -> Core.Program Var
 
-declToCore (TySigD'' ns t) = mempty &
+-- assume full eta-expansion for now
-    programTypeSigs .~ H.fromList [ (n, typeToCore t) | n <- ns ]
+declToCore (FunD b [] e) = mempty & programScDefs .~ [ScDef b' [] undefined]
-
-declToCore (DataD'' n as ds) = fold . getZipList $
-    constructorToCore t' <$> ZipList [0..] <*> ZipList ds
     where
-        -- create the appropriate type from the declared constructor and its
+        b' = MkVar b (typeToCore $ extract e)
-        -- arguments
+        e' = runPureEff . runNameSupply b . exprToCore $ e
-        t' = foldl TyApp (TyCon n) (TyVar . dsNameToName <$> as)
 
--- TODO: where-binds
+typeToCore :: Rlp.Type PsName -> Core.Type
-declToCore fd@(FunD'' n as e _) = mempty & programScDefs .~ [ScDef n' as' e']
+typeToCore (VarT n) = TyVar n
-    where
-        n' = dsNameToName n
-        e' = runPureEff . runNameSupply n . exprToCore . unXRec $ e
-        as' = as <&> \case
-            (unXRec -> VarP k) -> dsNameToName k
-            _                  -> error "no patargs yet"
 
-type NameSupply = Labeled NameSupplyLabel (State [IdP RlpcPs])
+exprToCore :: (NameSupply :> es)
-type NameSupplyLabel = "expr-name-supply"
+           => TypedRlpExpr PsName
+           -> Eff es (Cofree (Core.ExprF Var) Core.Type)
+exprToCore = undefined
 
-exprToCore :: forall es. (NameSupply :> es) => RlpExpr RlpcPs -> Eff es Expr'
+annotateVar :: Core.Type -> Core.ExprF PsName a -> Core.ExprF Var a
 
-exprToCore (VarE n) = pure $ Var (dsNameToName n)
+-- fixed points:
+annotateVar _ (VarF n)   = VarF n
+annotateVar _ (ConF t a) = ConF t a
+annotateVar _ (AppF f x) = AppF f x
+annotateVar _ (LitF l)   = LitF l
+annotateVar _ (TypeF t)  = TypeF t
 
-exprToCore (AppE a b) = (liftA2 App `on` exprToCore . unXRec) a b
+rlpExprToCore :: (NameSupply :> es)
+              => Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr'
 
-exprToCore (OAppE f a b) = (liftA2 mkApp `on` exprToCore . unXRec) a b
+-- assume all binders are simple variable patterns for now
-    where
+rlpExprToCore (LetEF r bs e) = pure $ Let r bs' e
-        mkApp s t = (Var f `App` s) `App` t
-
-exprToCore (CaseE (unXRec -> e) as) = do
-    e' <- exprToCore e
-    Case e' <$> caseAltToCore `traverse` as
-
-exprToCore (LetE bs e) = letToCore NonRec bs e
-exprToCore (LetrecE bs e) = letToCore Rec bs e
-
-exprToCore (LitE l) = litToCore l
-
-letToCore :: forall es. (NameSupply :> es)
-          => Rec -> [Rlp.Binding' RlpcPs] -> RlpExpr' RlpcPs -> Eff es Expr'
-letToCore r bs e = do
-    -- TODO: preserve binder order.
-    (bs',as) <- getParts
-    let insbs | null bs'  = pure
-              | otherwise = pure . Let r bs'
-    appKendo (foldMap Kendo (as `snoc` insbs)) <=< exprToCore $ unXRec e
   where
-    -- partition & map the list of binders into:
+    bs' = b2b <$> bs
-    --  bs'   : the let-binds that may be directly translated to Core
+    b2b (VarB (VarP k) v) = Binding k v
-    --          let-binds (we do exactly that). this is all the binders that
-    --          are a simple variable rather than a pattern match.
-    -- and as : the let-binds that may **not** be directly translated to
-    --          Core let-exprs. they get turned into case alternates.
-    getParts = traverse f bs <&> partitionEithers
-
-    f :: Rlp.Binding' RlpcPs
-      -> Eff es (Either Core.Binding' (Expr' -> Eff es Expr'))
-    f (PatB'' (VarP'' n) e) = Left . (n :=) <$> exprToCore (unXRec e)
-    f (PatB'' p          e) = pure $ Right (caseify p e)
-
-litToCore :: (NameSupply :> es) => Rlp.Lit RlpcPs -> Eff es Expr'
-litToCore (Rlp.IntL n) = pure . Lit $ Core.IntL n
-
-{-
-let C x = y
-in e
-
-case y of
-    C x -> e
- -}
-
-caseify :: (NameSupply :> es)
-        => Pat' RlpcPs -> RlpExpr' RlpcPs -> Expr' -> Eff es Expr'
-caseify p (unXRec -> e) i =
-    Case <$> exprToCore e <*> ((:[]) <$> alt)
-  where
-    alt = conToRose (unXRec p) <&> foldFix (branchToCore i)
-
--- TODO: where-binds
-caseAltToCore :: (HasCallStack, NameSupply :> es)
-              => (Alt RlpcPs, Where RlpcPs) -> Eff es Alter'
-caseAltToCore (AltA (unXRec -> p) e, wh) = do
-    e' <- exprToCore . unXRec $ e
-    conToRose p <&> foldFix (branchToCore e')
-
-altToCore :: (NameSupply :> es)
-          => Alt RlpcPs -> Eff es Alter'
-altToCore (AltA p e) = altToCore' p e
-
-altToCore' :: (NameSupply :> es)
-           => Pat' RlpcPs -> RlpExpr' RlpcPs -> Eff es Alter'
-altToCore' (unXRec -> p) (unXRec -> e) = do
-    e' <- exprToCore e
-    conToRose p <&> foldFix (branchToCore e')
-
-conToRose :: forall es. (HasCallStack, NameSupply :> es) => Pat RlpcPs -> Eff es Rose
-conToRose (ConP cn as) = Fix . Branch cn <$> patToForrest `traverse` as
-    where
-        patToForrest :: Pat' RlpcPs -> Eff es (Tree Rose)
-        patToForrest (VarP'' x) = pure $ Left (dsNameToName x)
-        patToForrest p@(ConP'' _ _) =
-            Right <$> liftA2 (,) uniqueName br
-          where
-            br = unwrapFix <$> conToRose (unXRec p)
-conToRose s = error $ "conToRose: not a ConP!: " <> show s
-
-branchToCore :: Expr' -> Branch Alter' -> Alter'
-branchToCore e (Branch cn as) = Alter (AltData cn) myBinds e'
-    where
-        -- gather binders for the /current/ pattern, and build an expression
-        -- matching subpatterns
-        (e', myBinds) = mapAccumL f e as
-
-        f :: Expr' -> Tree Alter' -> (Expr', Name)
-        f e (Left n)       = (e, dsNameToName n)
-        f e (Right (n,cs)) = (e', dsNameToName n) where
-            e' = Case (Var $ dsNameToName n) [branchToCore e cs]
-
-runNameSupply :: IdP RlpcPs -> Eff (NameSupply ': es) a -> Eff es a
-runNameSupply n = runLabeled @NameSupplyLabel (evalState ns) where
-    ns = [ "$" <> n <> "_" <> T.pack (show k) | k <- [0..] ]
-
--- | debug helper
-
-nameSupply :: [IdP RlpcPs]
-nameSupply = [ T.pack $ "$x_" <> show n | n <- [0..] ]
-
-uniqueName :: (NameSupply :> es) => Eff es (IdP RlpcPs)
-uniqueName = labeled @NameSupplyLabel @(State [IdP RlpcPs]) $
-    state @[IdP RlpcPs] (fromMaybe err . uncons)
-  where
-    err = error "NameSupply ran out of names! This shound never happen.\
-                \ The caller of runNameSupply is responsible."
-
-constructorToCore :: Type -> Tag -> ConAlt RlpcPs -> Program'
-constructorToCore t tag (ConAlt cn as) =
-    mempty & programTypeSigs . at cn ?~ foldr (:->) t as'
-           & programDataTags . at cn ?~ (tag, length as)
-    where
-        as' = typeToCore <$> as
-
-typeToCore :: RlpType' RlpcPs -> Type
-typeToCore FunConT''    = TyFun
-typeToCore (FunT'' s t) = typeToCore s :-> typeToCore t
-typeToCore (AppT'' s t) = TyApp (typeToCore s) (typeToCore t)
-typeToCore (ConT'' n)   = TyCon (dsNameToName n)
-typeToCore (VarT'' x)   = TyVar (dsNameToName x)
-
--- | Forwards-compatiblity if IdP RlpDs is changed
-dsNameToName :: IdP RlpcPs -> Name
-dsNameToName = id
 

tst/Compiler/TypesSpec.hs

@@ -0,0 +1,67 @@
+{-# LANGUAGE ParallelListComp #-}
+module Compiler.TypesSpec
+    ( spec
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Lens.Combinators
+import Data.Function            ((&))
+
+import Test.QuickCheck
+import Test.Hspec
+
+import Compiler.Types           (SrcSpan(..), srcSpanAbs, srcSpanLen)
+--------------------------------------------------------------------------------
+
+spec :: Spec
+spec = do
+    describe "SrcSpan" $ do
+        -- it "associates under closure"
+        --     prop_SrcSpan_mul_associative
+        it "commutes under closure"
+            prop_SrcSpan_mul_commutative
+        it "equals itself when squared"
+            prop_SrcSpan_mul_square_eq
+
+prop_SrcSpan_mul_associative :: Property
+prop_SrcSpan_mul_associative = property $ \a b c ->
+    -- very crudely approximate when overflow will occur; bail we think it
+    -- will
+    (([a,b,c] :: [SrcSpan]) & allOf (each . (srcSpanAbs <> srcSpanLen))
+                                    (< (maxBound @Int `div` 3)))
+    ==> (a <> b) <> c === a <> (b <> c :: SrcSpan)
+
+prop_SrcSpan_mul_commutative :: Property
+prop_SrcSpan_mul_commutative = property $ \a b ->
+    a <> b === (b <> a :: SrcSpan)
+
+prop_SrcSpan_mul_square_eq :: Property
+prop_SrcSpan_mul_square_eq = property $ \a ->
+    a <> a === (a :: SrcSpan)
+
+instance Arbitrary SrcSpan where
+    arbitrary = do
+        l <- chooseInt (1, maxBound)
+        c <- chooseInt (1, maxBound)
+        a <- chooseInt (0, maxBound)
+            `suchThat` (\n -> n >= pred l + pred c)
+        s <- chooseInt (0, maxBound)
+        pure $ SrcSpan l c a s
+
+    shrink (SrcSpan l c a s) =
+        [ SrcSpan l' c' a' s'
+        | (l',c',a',s') <- shrinkParts
+        , l' >= 1
+        , c' >= 1
+        , a' >= pred l' + pred c'
+        ]
+      where
+        -- shfl as = unsafePerformIO (generate $ shuffle as)
+        shrinkParts = 
+            [ (l',c',a',s')
+            | l' <- shrinkIntegral l
+            | c' <- shrinkIntegral c
+            | a' <- shrinkIntegral a
+            | s' <- shrinkIntegral s
+            ]
+

tst/Rlp/HindleyMilnerSpec.hs

@@ -0,0 +1,14 @@
+{-# LANGUAGE TemplateHaskell, QuasiQuotes #-}
+module Rlp.HindleyMilnerSpec
+    ( spec
+    )
+    where
+--------------------------------------------------------------------------------
+import Test.Hspec
+import Rlp.TH
+import Rlp.HindleyMilner
+--------------------------------------------------------------------------------
+
+spec :: Spec
+spec = undefined
+

visualisers/hmvis/.gitignore

@@ -0,0 +1,8 @@
+/public/js
+/node_modules
+/target
+/.shadow-cljs
+/*.iml
+/.nrepl-port
+/.idea
+

visualisers/hmvis/package.json

@@ -0,0 +1,11 @@
+{
+  "devDependencies": {
+    "shadow-cljs": "^2.26.2"
+  },
+  "dependencies": {
+    "ace-builds": "^1.32.7",
+    "react": "16.13.0",
+    "react-ace": "^10.1.0",
+    "react-dom": "16.13.0"
+  }
+}

visualisers/hmvis/public/css/main.css

@@ -0,0 +1,99 @@
+@import "solarized.css";
+
+html, body
+{ height: 100%
+}
+
+body {
+    font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif;
+    overflow: hidden;
+}
+
+.editor-container
+{ position: relative
+; height: 80vh
+}
+
+#editor
+{ width: 100%;
+; height: 100%
+; position: relative
+}
+
+#type-check-button {
+    position: fixed;
+    top: 0;
+    left: 50%;
+    z-index: 2;
+    /* margin: 0 auto; */
+    transform: translateX(-50%);
+}
+
+#type-check-output
+{ background: green
+; width: 100%
+; height: 100%
+}
+
+.main-view-container
+{ columns: 2 auto;
+
+}
+
+.split {
+    height: 100%;
+    width: 50%;
+    position: fixed;
+    z-index: 1;
+    top: 0;
+    overflow-x: hidden;
+    padding-top: 20px;
+}
+
+.left {
+    left: 0;
+}
+
+.right {
+    right: 0;
+}
+
+.annotation-wrapper
+{ display: inline-flex
+; flex-direction: column
+/* ; border-style: solid */
+/* ; border-width: 0 0 0.45em 0 */
+}
+
+.typed-wrapper
+{ display: inline-block
+}
+
+.annotation-wrapper .annotation
+{ position: relative
+; bottom: 0
+; min-height: 0.60em
+}
+
+.annotation-text
+{ display: none
+}
+
+.annotation.hovering > .annotation-text
+{ display: inline-block
+}
+
+.code-wrapper
+{ display: inline-block
+}
+
+code
+{ font-family: monospace
+; font-size: 1em
+}
+
+/* .typed-wrapper.hovering > .code-wrapper */
+/* { border-width: 0.2em */
+/* ; border-style: solid */
+/* } */
+

visualisers/hmvis/public/css/solarized.css

@@ -0,0 +1,303 @@
+@import url(http://fonts.googleapis.com/css?family=PT+Sans);
+@import url(http://fonts.googleapis.com/css?family=PT+Sans+Narrow:400,700);
+article,
+aside,
+details,
+figcaption,
+figure,
+footer,
+header,
+hgroup,
+nav,
+section,
+summary {
+  display: block;
+}
+audio,
+canvas,
+video {
+  display: inline-block;
+}
+audio:not([controls]) {
+  display: none;
+  height: 0;
+}
+[hidden] {
+  display: none;
+}
+html {
+  font-family: sans-serif;
+  -webkit-text-size-adjust: 100%;
+  -ms-text-size-adjust: 100%;
+}
+body {
+  margin: 0;
+}
+a:focus {
+  outline: thin dotted;
+}
+a:active,
+a:hover {
+  outline: 0;
+}
+h1 {
+  font-size: 2em;
+}
+abbr[title] {
+  border-bottom: 1px dotted;
+}
+b,
+strong {
+  font-weight: bold;
+}
+dfn {
+  font-style: italic;
+}
+mark {
+  background: #ff0;
+  color: #000;
+}
+code,
+kbd,
+pre,
+samp {
+  font-family: monospace, serif;
+  font-size: 1em;
+}
+pre {
+  white-space: pre-wrap;
+  word-wrap: break-word;
+}
+q {
+  quotes: "\201C" "\201D" "\2018" "\2019";
+}
+small {
+  font-size: 80%;
+}
+sub,
+sup {
+  font-size: 75%;
+  line-height: 0;
+  position: relative;
+  vertical-align: baseline;
+}
+sup {
+  top: -0.5em;
+}
+sub {
+  bottom: -0.25em;
+}
+img {
+  border: 0;
+}
+svg:not(:root) {
+  overflow: hidden;
+}
+figure {
+  margin: 0;
+}
+fieldset {
+  border: 1px solid #c0c0c0;
+  margin: 0 2px;
+  padding: 0.35em 0.625em 0.75em;
+}
+legend {
+  border: 0;
+  padding: 0;
+}
+button,
+input,
+select,
+textarea {
+  font-family: inherit;
+  font-size: 100%;
+  margin: 0;
+}
+button,
+input {
+  line-height: normal;
+}
+button,
+html input[type="button"],
+input[type="reset"],
+input[type="submit"] {
+  -webkit-appearance: button;
+  cursor: pointer;
+}
+button[disabled],
+input[disabled] {
+  cursor: default;
+}
+input[type="checkbox"],
+input[type="radio"] {
+  box-sizing: border-box;
+  padding: 0;
+}
+input[type="search"] {
+  -webkit-appearance: textfield;
+  -moz-box-sizing: content-box;
+  -webkit-box-sizing: content-box;
+  box-sizing: content-box;
+}
+input[type="search"]::-webkit-search-cancel-button,
+input[type="search"]::-webkit-search-decoration {
+  -webkit-appearance: none;
+}
+button::-moz-focus-inner,
+input::-moz-focus-inner {
+  border: 0;
+  padding: 0;
+}
+textarea {
+  overflow: auto;
+  vertical-align: top;
+}
+table {
+  border-collapse: collapse;
+  border-spacing: 0;
+}
+html {
+  font-family: 'PT Sans', sans-serif;
+}
+pre,
+code {
+  font-family: 'Inconsolata', sans-serif;
+}
+h1,
+h2,
+h3,
+h4,
+h5,
+h6 {
+  font-family: 'PT Sans Narrow', sans-serif;
+  font-weight: 700;
+}
+html {
+  background-color: #eee8d5;
+  color: #657b83;
+  margin: 1em;
+}
+body {
+  background-color: #fdf6e3;
+  margin: 0 auto;
+  max-width: 23cm;
+  border: 1pt solid #93a1a1;
+  padding: 1em;
+}
+code {
+  background-color: #eee8d5;
+  padding: 2px;
+}
+a {
+  color: #b58900;
+}
+a:visited {
+  color: #cb4b16;
+}
+a:hover {
+  color: #cb4b16;
+}
+h1 {
+  color: #d33682;
+}
+h2,
+h3,
+h4,
+h5,
+h6 {
+  color: #859900;
+}
+pre {
+  background-color: #fdf6e3;
+  color: #657b83;
+  border: 1pt solid #93a1a1;
+  padding: 1em;
+  box-shadow: 5pt 5pt 8pt #eee8d5;
+}
+pre code {
+  background-color: #fdf6e3;
+}
+h1 {
+  font-size: 2.8em;
+}
+h2 {
+  font-size: 2.4em;
+}
+h3 {
+  font-size: 1.8em;
+}
+h4 {
+  font-size: 1.4em;
+}
+h5 {
+  font-size: 1.3em;
+}
+h6 {
+  font-size: 1.15em;
+}
+.tag {
+  background-color: #eee8d5;
+  color: #d33682;
+  padding: 0 0.2em;
+}
+.todo,
+.next,
+.done {
+  color: #fdf6e3;
+  background-color: #dc322f;
+  padding: 0 0.2em;
+}
+.tag {
+  -webkit-border-radius: 0.35em;
+  -moz-border-radius: 0.35em;
+  border-radius: 0.35em;
+}
+.TODO {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #2aa198;
+}
+.NEXT {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #268bd2;
+}
+.ACTIVE {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #268bd2;
+}
+.DONE {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #859900;
+}
+.WAITING {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #cb4b16;
+}
+.HOLD {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #d33682;
+}
+.NOTE {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #d33682;
+}
+.CANCELLED {
+  -webkit-border-radius: 0.2em;
+  -moz-border-radius: 0.2em;
+  border-radius: 0.2em;
+  background-color: #859900;
+}
+

visualisers/hmvis/public/index.html

@@ -0,0 +1,22 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+  <meta charset="UTF-8">
+  <meta http-equiv="X-UA-Compatible" content="IE=edge">
+  <meta name="viewport" content="width=device-width, initial-scale=1.0">
+  <link rel="stylesheet" href="/css/main.css">
+  <title>Hindley-Milner</title>
+
+  <style type="text/css" media="screen">
+  </style>
+</head>
+<body>
+
+    <div id="mount">
+        <div id="editor">
+        </div>
+    </div>
+  <script src="/js/main.js"></script>
+</body>
+</html>
+

visualisers/hmvis/shadow-cljs.edn

@@ -0,0 +1,27 @@
+;; shadow-cljs configuration
+{:source-paths
+ ["src/"]
+
+ :dependencies
+ [[cider/cider-nrepl "0.24.0"]
+  [nilenso/wscljs "0.2.0"]
+  [org.clojure/core.match "1.1.0"]
+  [binaryage/oops "0.7.2"]
+  [reagent "0.10.0"]
+  [cljsjs/react "17.0.2-0"]
+  [cljsjs/react-dom "17.0.2-0"]
+  [cljsx "1.0.0"]]
+
+ :dev-http
+ {8020 "public"}
+
+ :builds
+ {:app
+  {:target :browser
+   :output-dir "public/js"
+   :asset-path "/js"
+
+   :modules
+   {:main ; becomes public/js/main.js
+    {:init-fn main/init}}}}}
+

visualisers/hmvis/src/hmvis/annotated.cljs

@@ -0,0 +1,142 @@
+(ns hmvis.annotated
+  (:require [cljs.core.match :refer-macros [match]]
+            [cljsx.core :refer [jsx> react> defcomponent]]
+            [react :as react]
+            [react-dom :as react-dom]
+            [reagent.core :as r]
+            [reagent.dom :as rdom]
+            [clojure.pprint :refer [cl-format]]
+            [hmvis.ppr :as ppr]
+            [clojure.pprint :refer [pprint]]
+            [clojure.string :as str]))
+
+(defonce tc-input (r/atom nil))
+
+(defonce current-annotation-text (r/atom nil))
+
+(defn unicodify [s]
+  (str/replace s #"->" "→"))
+
+(defn punctuate [p & as]
+  (match as
+         [] ""
+         _  (reduce #(str %1 p %2) as)))
+
+(defn hsep [& as]
+  (apply punctuate " " as))
+
+(defn maybe-parens [c s]
+  (if c
+      [:<> "(" s ")"]
+      s))
+
+(defn formatln [fs & rest]
+  (apply cl-format true (str fs "~%") rest))
+
+(def nesting-rainbow (cycle ["red" "orange" "yellow"
+                             "green" "blue" "purple"]))
+
+(defn text-colour-by-background [colour]
+  (match colour
+         "yellow" "black"
+         _        "white"))
+
+(defn Annotation [colour text hovering?]
+  [:div {:class (if @hovering?
+                    "annotation hovering"
+                    "annotation")
+         :on-mouse-enter #(reset! hovering? true)
+         :on-mouse-leave #(reset! hovering? false)
+         :style {:background colour
+                 :color (text-colour-by-background colour)}}
+   [:div {:class "annotation-text"}
+    text]])
+
+(defn Typed [colour t child]
+  (let [hovering? (r/atom false)]
+    (fn []
+        [:div {:class "annotation-wrapper"}
+         [:div {:class (if @hovering?
+                           "typed-wrapper hovering"
+                           "typed-wrapper")
+                }
+          [:div {:class "code-wrapper"} child]]
+         [Annotation colour (unicodify t) hovering?]])))
+
+(declare Expr)
+
+(defn LambdaExpr [colours binds body]
+  [:<>
+    [:code
+      (hsep "λ" (apply hsep binds) "-> ")]
+    [Expr colours 0 body]])
+
+(defn VarExpr [var-id]
+  [:code var-id])
+
+(defn AppExpr [colours f x]
+  [:<> [Expr colours ppr/app-prec f]
+       " "
+       [Expr colours ppr/app-prec1 x]])
+
+(defn let-or-letrec [rec]
+  (match rec
+         "Rec"    "letrec"
+         "NonRec" "let"))
+
+(defn Pat [colours p {:keys [tag contents]}]
+  (match tag
+         "VarP" contents))
+
+(defn Binding [colours {:keys [tag contents]}]
+  (match tag
+         "VarB" (let [[p v] contents]
+                  [:<> [Pat colours 0 p] " = " [Expr colours 0 v]])))
+
+(defn LetExpr [colours rec bs e]
+  [:<> (let-or-letrec rec)
+       " "
+       (apply punctuate "; " (map (partial Binding colours) bs))
+       " in "
+       (Expr colours 0 e)])
+
+(defn LitExpr [_ l]
+  [:code (str l)])
+
+(defn Expr [[c & colours] p {e :e t :type}]
+  (match e
+    {:InL {:tag "LamF" :contents [bs body & _]}}
+      (maybe-parens (< ppr/app-prec1 p)
+                    [Typed c t [LambdaExpr colours bs body]])
+    {:InL {:tag "VarF" :contents var-id}}
+      [Typed c t [VarExpr var-id]]
+    {:InL {:tag "AppF" :contents [f x]}}
+      (maybe-parens (< ppr/app-prec p)
+                    [Typed c t [AppExpr colours f x]])
+    {:InR {:tag "LetEF" :contents [r bs body]}}
+      (maybe-parens (< ppr/app-prec1 p)
+                    [Typed c t [LetExpr colours r bs body]])
+    {:InL {:tag "LitF" :contents l}}
+      [Typed c t [LitExpr colours l]]
+    :else [:code "<expr>"]))
+
+(def rainbow-cycle (cycle ["red"
+                           "orange"
+                           "yellow"
+                           "green"
+                           "blue"
+                           "violet"]))
+
+(defn render-decl [{name :name body :body}]
+  [:code {:key name :display "block"}
+           (str name " = ") [Expr rainbow-cycle 0 body] #_ (render-expr body)
+           [:br]])
+
+(defn TypeChecker []
+  [:div
+   (map render-decl (or @tc-input []))])
+
+; (defn init []
+;   (rdom/render [type-checker]
+;                (js/document.querySelector "#output")))
+

visualisers/hmvis/src/hmvis/ppr.cljs

@@ -0,0 +1,41 @@
+(ns hmvis.ppr
+    (:require [cljs.core.match :refer-macros [match]]))
+
+(def app-prec  10)
+(def app-prec1 11)
+
+(defn- maybe-parens [c s]
+  (if c
+      (str "(" s ")")
+      s))
+
+(defn- hsep [& as]
+  (let [f (fn [a b] (str a " " b))]
+    (reduce f as)))
+
+(declare expr)
+
+(defn lambda-expr [binds body]
+  (hsep "λ" (apply hsep binds) "->" (expr body)))
+
+(defn app-expr [f x]
+  (hsep (expr app-prec f) (expr app-prec1 x)))
+
+(defn var-expr [var-id]
+  var-id)
+
+(defn expr
+  ([exp] (expr 0 exp))
+
+  ([p {e :e}]
+    (match e
+           {:InL {:tag "LamF" :contents [bs body & _]}}
+           (maybe-parens (< app-prec1 p)
+                         (lambda-expr bs body))
+           {:InL {:tag "VarF" :contents var-id}}
+           (var-expr var-id)
+           {:InL {:tag "AppF" :contents [f x]}}
+           (maybe-parens (< app-prec p)
+                         (app-expr f x))
+           :else [:code "<expr>"])))
+

visualisers/hmvis/src/main.cljs

@@ -0,0 +1,103 @@
+(ns main
+  (:require [clojure.spec.alpha :as s]
+            ["react-ace$default" :as AceEditor]
+            ["ace-builds/src-noconflict/mode-haskell"]
+            ["ace-builds/src-noconflict/theme-solarized_light"]
+            ["ace-builds/src-noconflict/keybinding-vim"]
+            [wscljs.client :as ws]
+            [wscljs.format :as fmt]
+            [cljs.core.match :refer-macros [match]]
+            [hmvis.annotated :as annotated]
+            [reagent.core :as r]
+            [reagent.dom :as rdom]))
+
+; (def *editor
+;   (doto (js/ace.edit "editor")
+;         (.setTheme "ace/theme/solarized_light")
+;         (.setKeyboardHandler "ace/keyboard/vim")
+;         (.setOption "mode" "ace/mode/haskell")))
+
+(def *output (.querySelector js/document "#output"))
+
+(defn display-errors [es]
+  (doseq [{{e :contents} :diagnostic} es]
+         (let [fmte (map #(str "  • " % "\n") e)]
+           (js/console.warn (apply str "message from rlpc:\n" fmte)))))
+
+(defn with-success [f ma]
+  (match ma
+    {:errors es :result nil} (display-errors es)
+    {:errors es :result a}   (do (display-errors es)
+                                 (f a))))
+
+(defn on-message [e]
+  (let [r (js->clj (js/JSON.parse (.-data e)) :keywordize-keys true)]
+    (match r
+           {:tag "Annotated" :contents c}
+             (with-success #(reset! annotated/tc-input %) c)
+           :else
+             (js/console.warn "unrecognisable response from rlp"))))
+
+(defonce *socket (ws/create "ws://127.0.0.1:9002"
+                            {:on-message on-message
+                             :on-open #(println "socket opened")
+                             :on-close #(println "socket closed")
+                             :on-error #(println "error: " %)}))
+
+(defn send [msg]
+  (ws/send *socket msg fmt/json))
+
+(defonce *editor nil)
+
+(defn TypeCheckButton []
+  [:button {:id "type-check-button"
+            :on-click #(send {:command "annotate"
+                              :source (.getValue *editor)})}
+   "type-check"])
+
+(defn Editor []
+  [:div {:class "editor-container"}
+    [(r/adapt-react-class AceEditor)
+     {:mode "haskell"
+      :theme "solarized_light"
+      :keyboardHandler "vim"
+      :defaultValue (str "id = \\x -> x\n"
+                         "flip f x y = f y x\n"
+                         "fix f = letrec x = f x in x")
+      :style {:width "100%"
+              :height "100%"}
+      :on-load (fn [editor]
+                 (set! *editor editor)
+                 (set! (.. editor -container -style -resize) "both")
+                 (js/document.addEventListener
+                   "mouseup"
+                   #(.resize editor)))
+      :name "editor"} ]])
+
+(defn Main []
+  [:<>
+    [:div {:class "main-view-container"}
+     [TypeCheckButton]
+     [Editor]
+     [annotated/TypeChecker]
+     #_ [:div {:id "type-check-output"}
+      "doge soge quoge"]]
+   #_ [annotated/TypeChecker]])
+
+;; start is called by init and after code reloading finishes
+(defn ^:dev/after-load start []
+  (rdom/render [Main]
+               (js/document.getElementById "mount"))
+  (js/console.log "start"))
+
+(defn init []
+  ;; init is called ONCE when the page loads
+  ;; this is called in the index.html and must be exported
+  ;; so it is available even in :advanced release builds
+  (js/console.log "init")
+  (start))
+
+;; this is called before any code is reloaded
+(defn ^:dev/before-load stop []
+  (js/console.log "stop"))
+