seems to work

i'm honestly rather disappointed in myself for not implementing a comonadic algo J.
cross my heart i'll come back to this and return stronger!
in the mean time, i really need to get this thing into a presentable state...

.ghci

@@ -1,5 +1,9 @@
+-- repl extensions
 :set -XOverloadedStrings
 
+--------------------------------------------------------------------------------
+
+-- happy/alex: override :r to rebuild parsers
 :set -package process
 
 :{
@@ -16,3 +20,5 @@ _reload_and_make _ = do
 
 :def! r _reload_and_make
 
+--------------------------------------------------------------------------------
+

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.cl)
 
 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

@@ -3,6 +3,10 @@
 `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/)
@@ -18,21 +22,40 @@ $ cabal test --test-show-details=direct
 ```
 
 ### Use
+
+#### TLDR
+
 ```sh
-# Compile and evaluate examples/factorial.hs, with evaluation info dumped to stderr
-$ rlpc -ddump-eval examples/factorial.hs
-# Compile and evaluate t.hs, with evaluation info dumped to t.log
-$ rlpc -ddump-eval -l t.log t.hs
-# Print the raw structure describing the compiler options
-# (option parsing still must succeed in order to print)
-$ rlpc -ddump-opts t.hs
+# 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
-- [ ] Higher-kinded types
+- [x] Higher-kinded types
 - [ ] Typeclasses
 - [x] Parametric polymorphism
 - [x] Hindley-Milner type inference
@@ -42,6 +65,14 @@ Listed in order of importance.
 ### 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
@@ -57,9 +88,8 @@ Listed in order of importance.
         - [x] Garbage Collection
     - [ ] Emitter
         - [ ] Code-gen (target yet to be decided)
-        - [ ] Core language emitter
-    - [ ] Core linter (Type-checker)
-    - [ ] Core2Core pass
+    - [x] Core linter (Type-checker)
+    - [ ] Core2Core pass (optimisations and misc. preprocessing)
         - [x] GM prep
             - [x] Non-strict case-floating
         - [ ] Let-floating
@@ -70,7 +100,7 @@ Listed in order of importance.
         - [x] AST
         - [x] Lexer
         - [x] Parser
-    - [ ] Translation to the core language
+    - [x] Translation to the core language
         - [ ] Constraint solver
         - [ ] `do`-notation
     - [x] CLI
@@ -98,29 +128,38 @@ Listed in order of importance.
     - [x] Garbage Collection
 - [ ] Stable documentation for the evaluation model
 
-### January Release Plan
-- [ ] Beta rl' to Core
-- [ ] UX improvements
-    - [ ] Actual compiler errors -- no more unexceptional `error` calls
-    - [ ] Better CLI dump flags
-    - [ ] Annotate the AST with token positions for errors
-- [ ] More examples
+### ~~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
-- [ ] GM to LLVM
+- [ ] Choose a target. LLVM, JS, C, and WASM are currently top contenders
+- [ ] https://proglangdesign.net/wiki/challenges
 

app/CoreDriver.hs

@@ -5,6 +5,8 @@ module CoreDriver
 --------------------------------------------------------------------------------
 import Compiler.RLPC
 import Control.Monad
+import Data.Text                    qualified as T
+import Control.Lens.Combinators
 
 import Core.Lex
 import Core.Parse
@@ -15,3 +17,8 @@ driver :: RLPCIO ()
 driver = forFiles_ $ \f ->
     withSource f (lexCoreR >=> parseCoreProgR >=> evalProgR)
 
+driverSource :: T.Text -> RLPCIO ()
+driverSource = lexCoreR >=> parseCoreProgR >=> evalProgR >=> printRes
+    where
+        printRes = liftIO . print . view _1
+

app/Main.hs

@@ -1,7 +1,9 @@
 {-# LANGUAGE BlockArguments, LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 module Main where
 ----------------------------------------------------------------------------------
 import Compiler.RLPC
+import Compiler.RlpcError
 import Control.Exception
 import Options.Applicative      hiding (ParseError)
 import Control.Monad
@@ -11,12 +13,13 @@ import Data.Text                (Text)
 import Data.Text                qualified as T
 import Data.Text.IO             qualified as TIO
 import Data.List
+import Data.Maybe               (listToMaybe)
 import System.IO
 import System.Exit              (exitSuccess)
 import Core
 import TI
 import GM
-import Lens.Micro.Mtl
+import Control.Lens.Combinators hiding (argument)
 
 import CoreDriver               qualified
 import RlpDriver                qualified
@@ -65,9 +68,11 @@ options = RLPCOptions
                 \triggering the garbage collector"
         <> value 50
         )
-    <*> option languageReader
+    <*> optional # option languageReader
         (  long "language"
         <> short 'x'
+        <> metavar "rlp|core"
+        <> help "the language to be compiled -- see README"
         )
     <*> some (argument str $ metavar "FILES...")
     where
@@ -78,6 +83,8 @@ languageReader :: ReadM Language
 languageReader = maybeReader $ \case
     "rlp"   -> Just LanguageRlp
     "core"  -> Just LanguageCore
+    "rl"    -> Just LanguageRlp
+    "cr"    -> Just LanguageCore
     _       -> Nothing
 
 debugFlagReader :: ReadM DebugFlag
@@ -100,10 +107,34 @@ mmany v = liftA2 (<>) v (mmany v)
 main :: IO ()
 main = do
     opts <- execParser optParser
-    void $ evalRLPCIO opts driver
+    void $ evalRLPCIO opts dispatch
+
+dispatch :: RLPCIO ()
+dispatch = getLang >>= \case
+    Just LanguageCore -> CoreDriver.driver
+    Just LanguageRlp  -> RlpDriver.driver
+    Nothing           -> addFatal err
+        where
+            -- TODO: why didn't i make the srcspan optional LOL
+            err = errorMsg (SrcSpan 0 0 0 0) $ Text
+                [ "Could not determine source language from filetype."
+                , "Possible Solutions:\n\
+                  \  Suffix the file with `.cr' for Core, or `.rl' for rl'\n\
+                  \  Specify a language with `rlpc -x core' or `rlpc -x rlp'"
+                ]
+  where
+    getLang = liftA2 (<|>)
+        (view rlpcLanguage)
+        -- TODO: we only check the first file lol
+        ((listToMaybe >=> inferLanguage) <$> view rlpcInputFiles)
+
 
 driver :: RLPCIO ()
-driver = view rlpcLanguage >>= \case
-    LanguageCore -> CoreDriver.driver
-    LanguageRlp  -> RlpDriver.driver
+driver = undefined
+
+inferLanguage :: FilePath -> Maybe Language
+inferLanguage fp
+    | ".rl" `isSuffixOf` fp     = Just LanguageRlp
+    | ".cr" `isSuffixOf` fp     = Just LanguageCore
+    | otherwise                 = Nothing
 

app/RlpDriver.hs

@@ -1,11 +1,19 @@
+{-# LANGUAGE OverloadedStrings #-}
 module RlpDriver
     ( driver
     )
     where
 --------------------------------------------------------------------------------
 import Compiler.RLPC
+import Control.Monad
+
+import Rlp.Lex
+import Rlp.Parse
+import Rlp2Core
+import GM
 --------------------------------------------------------------------------------
 
 driver :: RLPCIO ()
-driver = undefined
+driver = forFiles_ $ \f ->
+    withSource f (parseRlpProgR >=> desugarRlpProgR >=> evalProgR)
 

doc/src/commentary/gm.rst

@@ -63,52 +63,13 @@ an assembly target. The goal of our new G-Machine is to compile a *linear
 sequence of instructions* which, **when executed**, build up a graph
 representing the code.
 
-**************************
-Trees and Vines, in Theory
-**************************
-
-Rather than instantiating an expression at runtime -- traversing the AST and
-building a graph -- we want to compile all expressions at compile-time,
-generating a linear sequence of instructions which may be executed to build the
-graph.
-
-**************************
-Evaluation: Slurping Vines
-**************************
-
-WIP.
-
-Laziness
---------
-
-WIP.
-
-* Instead of :code:`Slide (n+1); Unwind`, do :code:`Update n; Pop n; Unwind`
-
-****************************
-Compilation: Squashing Trees
-****************************
-
-WIP.
-
-Notice that we do not keep a (local) environment at run-time. The environment
-only exists at compile-time to map local names to stack indices. When compiling
-a supercombinator, the arguments are enumerated from zero (the top of the
-stack), and passed to :code:`compileR` as an environment.
+*************
+The G-Machine
+*************
 
 .. literalinclude:: /../../src/GM.hs
    :dedent:
-   :start-after: -- >> [ref/compileSc]
-   :end-before: -- << [ref/compileSc]
-   :caption: src/GM.hs
-
-Of course, variables being indexed relative to the top of the stack means that
-they will become inaccurate the moment we push or pop the stack a single time.
-The way around this is quite simple: simply offset the stack when w
-
-.. literalinclude:: /../../src/GM.hs
-   :dedent:
-   :start-after: -- >> [ref/compileC]
-   :end-before: -- << [ref/compileC]
+   :start-after: -- >> [ref/Instr]
+   :end-before: -- << [ref/Instr]
    :caption: src/GM.hs
 

doc/src/commentary/layout-lexing.rst

@@ -62,159 +62,6 @@ braces and semicolons. In developing our *layout* rules, we will follow in the
 pattern of translating the whitespace-sensitive source language to an explicitly
 sectioned language.
 
-But What About Haskell?
-***********************
-
-Parsing Haskell -- and thus rl' -- is only slightly more complex than Python,
-but the design is certainly more sensitive. 
-
-.. code-block:: haskell
-
-   -- line folds
-   something = this is a
-       single expression
-
-   -- an extremely common style found in haskell
-   data Some = Data
-       { is    :: Presented
-       , in    :: This
-       , silly :: Style
-       }
-
-   -- another style oddity
-   -- note that this is not a single
-   -- continued line! `look at`,
-   -- `this odd`, and `alignment` are all
-   -- discrete items!
-   anotherThing = do look at
-                     this odd
-                     alignment
-
-But enough fear, lets actually think about implementation. Firstly, some
-formality: what do we mean when we say layout? We will define layout as the
-rules we apply to an implicitly-sectioned language in order to yield one that is
-explicitly-sectioned. We will also define indentation of a lexeme as the column
-number of its first character.
-
-Thankfully for us, our entry point is quite clear; layouts only appear after a
-select few keywords, (with a minor exception; TODO: elaborate) being :code:`let`
-(followed by supercombinators), :code:`where` (followed by supercombinators),
-:code:`do` (followed by expressions), and :code:`of` (followed by alternatives)
-(TODO: all of these terms need linked glossary entries). In order to manage the
-cascade of layout contexts, our lexer will record a stack for which each element
-is either :math:`\varnothing`, denoting an explicit layout written with braces
-and semicolons, or a :math:`\langle n \rangle`, denoting an implicitly laid-out
-layout where the start of each item belonging to the layout is indented
-:math:`n` columns.
-
-.. code-block:: haskell
-
-    -- layout stack: []
-    module M where -- layout stack: [∅]
-
-    f x = let -- layout keyword; remember indentation of next token
-              y = w * w -- layout stack: [∅, <10>]
-              w = x + x
-              -- layout ends here
-          in do -- layout keyword; next token is a brace!
-              { -- layout stack: [∅]
-                  print y;
-                  print x;
-              }
-
-Finally, we also need the concept of "virtual" brace tokens, which as far as
-we're concerned at this moment are exactly like normal brace tokens, except
-implicitly inserted by the compiler. With the presented ideas in mind, we may
-begin to introduce a small set of informal rules describing the lexer's handling
-of layouts, the first being:
-
-1. If a layout keyword is followed by the token '{', push :math:`\varnothing`
-   onto the layout context stack. Otherwise, push :math:`\langle n \rangle` onto
-   the layout context stack where :math:`n` is the indentation of the token
-   following the layout keyword. Additionally, the lexer is to insert a virtual
-   opening brace after the token representing the layout keyword.
-
-Consider the following observations from that previous code sample:
-
-* Function definitions should belong to a layout, each of which may start at
-  column 1.
-
-* A layout can enclose multiple bodies, as seen in the :code:`let`-bindings and
-  the :code:`do`-expression.
-
-* Semicolons should *terminate* items, rather than *separate* them.
-
-Our current focus is the semicolons. In an implicit layout, items are on
-separate lines each aligned with the previous. A naïve implementation would be
-to insert the semicolon token when the EOL is reached, but this proves unideal
-when you consider the alignment requirement. In our implementation, our lexer
-will wait until the first token on a new line is reached, then compare
-indentation and insert a semicolon if appropriate. This comparison -- the
-nondescript measurement of "more, less, or equal indentation" rather than a
-numeric value -- is referred to as *offside* by myself internally and the
-Haskell report describing layouts. We informally formalise this rule as follows:
-
-2. When the first token on a line is preceeded only by whitespace, if the
-   token's first grapheme resides on a column number :math:`m` equal to the
-   indentation level of the enclosing context -- i.e. the :math:`\langle n
-   \rangle` on top of the layout stack. Should no such context exist on the
-   stack, assume :math:`m > n`.
-
-We have an idea of how to begin layouts, delimit the enclosed items, and last
-we'll need to end layouts. This is where the distinction between virtual and
-non-virtual brace tokens comes into play. The lexer needs only partial concern
-towards closing layouts; the complete responsibility is shared with the parser.
-This will be elaborated on in the next section. For now, we will be content with
-naïvely inserting a virtual closing brace when a token is indented right of the
-layout.
-
-3. Under the same conditions as rule 2., when :math:`m < n` the lexer shall
-   insert a virtual closing brace and pop the layout stack.
-
-This rule covers some cases including the top-level, however, consider
-tokenising the :code:`in` in a :code:`let`-expression. If our lexical analysis
-framework only allows for lexing a single token at a time, we cannot return both
-a virtual right-brace and a :code:`in`. Under this model, the lexer may simply
-pop the layout stack and return the :code:`in` token. As we'll see in the next
-section, as long as the lexer keeps track of its own context (i.e. the stack),
-the parser will cope just fine without the virtual end-brace.
-
-Parsing Lonely Braces
-*********************
-
-When viewed in the abstract, parsing and tokenising are near-identical tasks yet
-the two are very often decomposed into discrete systems with very different
-implementations. Lexers operate on streams of text and tokens, while parsers
-are typically far less linear, using a parse stack or recursing top-down. A
-big reason for this separation is state management: the parser aims to be as
-context-free as possible, while the lexer tends to burden the necessary
-statefulness. Still, the nature of a stream-oriented lexer makes backtracking
-difficult and quite inelegant.
-
-However, simply declaring a parse error to be not an error at all
-counterintuitively proves to be an elegant solution our layout problem which
-minimises backtracking and state in both the lexer and the parser. Consider the
-following definitions found in rlp's BNF:
-
-.. productionlist:: rlp
-   VOpen   : `vopen`
-   VClose  : `vclose` | `error`
-
-A parse error is recovered and treated as a closing brace. Another point of note
-in the BNF is the difference between virtual and non-virtual braces (TODO: i
-don't like that the BNF is formatted without newlines :/):
-
-.. productionlist:: rlp
-   LetExpr : `let` VOpen Bindings VClose `in` Expr | `let` `{` Bindings `}` `in` Expr
-
-This ensures that non-virtual braces are closed explicitly.
-
-This set of rules is adequete enough to satisfy our basic concerns about line
-continations and layout lists. For a more pedantic description of the layout
-system, see `chapter 10
-<https://www.haskell.org/onlinereport/haskell2010/haskellch10.html>`_ of the
-2010 Haskell Report, which I heavily referenced here.
-
 References
 ----------
 

examples/Core/constDivZero.cr

@@ -0,0 +1,3 @@
+k x y = x;
+main = k 3 (/# 1 0);
+

examples/Core/factorial.cr

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

examples/Core/sumList.cr

@@ -0,0 +1,12 @@
+{-# PackData Nil  0 0 #-}
+{-# PackData Cons 1 2 #-}
+
+foldr f z l = case l of
+    { Nil       -> z
+    ; Cons x xs -> f x (foldr f z xs)
+    };
+
+list = Cons 1 (Cons 2 (Cons 3 Nil));
+
+main = foldr (+#) 0 list;
+

examples/constDivZero.hs

@@ -1,3 +0,0 @@
-k x y = x;
-main = k 3 ((/#) 1 0);
-

examples/factorial.hs

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

examples/rlp/QuickSort.rl

@@ -0,0 +1,31 @@
+data List a = Nil | Cons a (List a)
+
+data Bool = False | True
+
+filter :: (a -> Bool) -> List a -> List a
+filter p l = case l of
+    Nil -> Nil
+    Cons a as ->
+        case p a of
+            True -> Cons a (filter p as)
+            False -> filter p as
+
+append :: List a -> List a -> List a
+append p q = case p of
+    Nil -> q
+    Cons a as -> Cons a (append as q)
+
+qsort :: List Int# -> List Int#
+qsort l = case l of
+    Nil -> Nil
+    Cons a as ->
+        let lesser = filter (>=# a) as
+            greater = filter (<# a) as
+        in append (append (qsort lesser) (Cons a Nil)) (qsort greater)
+
+list :: List Int#
+list = Cons 9 (Cons 2 (Cons 3 (Cons 2
+            (Cons 5 (Cons 2 (Cons 12 (Cons 89 Nil)))))))
+
+main = print# (qsort list)
+

examples/rlp/SumList.rl

@@ -0,0 +1,11 @@
+data List a = Nil | Cons a (List a)
+
+foldr :: (a -> b -> b) -> b -> List a -> b
+foldr f z l = case l of
+    Nil -> z
+    Cons a as -> f a (foldr f z as)
+
+list = Cons 1 (Cons 2 (Cons 3 Nil))
+
+main = print# (foldr (+#) 0 list)
+

examples/sumList.hs

@@ -1,9 +0,0 @@
-nil = Pack{0 0};
-cons x y = Pack{1 2} x y;
-list = cons 1 (cons 2 (cons 3 nil));
-sum l = case l of
-    { <0>      -> 0
-    ; <1> x xs -> (+#) x (sum xs)
-    };
-main = sum list;
-

find-build.cl

@@ -0,0 +1,8 @@
+#!/usr/bin/env sbcl --script
+
+(let* ((paths (directory "dist-newstyle/build/*/*/rlp-*/build/"))
+       (n (length paths)))
+  (cond ((< 1 n) (error ">1 build directories found. run `cabal clean`."))
+        ((< n 1) (error "no build directories found. this shouldn't happen lol"))
+        (t       (format t "~A" (car paths)))))
+

rlp.cabal

@@ -32,18 +32,31 @@ library
                     , Core.HindleyMilner
                     , Control.Monad.Errorful
                     , Rlp.Syntax
+                    , Rlp.AltSyntax
+                    , Rlp.AltParse
+                    , Rlp.HindleyMilner
+                    , Rlp.HindleyMilner.Types
+                    , Rlp.Syntax.Backstage
+                    , Rlp.Syntax.Types
+                    , Rlp.Syntax.Good
                     -- , Rlp.Parse.Decls
                     , Rlp.Parse
                     , Rlp.Parse.Associate
                     , Rlp.Lex
                     , Rlp.Parse.Types
+                    , Rlp.TH
                     , Compiler.Types
                     , Data.Heap
                     , Data.Pretty
                     , Core.Parse
+                    , Core.Parse.Types
                     , Core.Lex
                     , Core2Core
+                    , Rlp2Core
                     , Control.Monad.Utils
+                    , Misc
+                    , Misc.Lift1
+                    , Core.SystemF
 
     build-tool-depends: happy:happy, alex:alex
 
@@ -58,21 +71,22 @@ library
                     , 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.1
-                    , megaparsec >= 9.6.1 && < 9.7
-                    , microlens >= 0.4.13 && < 0.5
-                    , microlens-mtl >= 0.2.0 && < 0.3
-                    , microlens-platform >= 0.4.3 && < 0.5
-                    , microlens-th >= 0.4.3 && < 0.5
+                    , 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
                     , utf8-string >= 1.0.2 && < 1.1
-                    , extra >= 1.7.0 && < 2
-                    , semigroupoids
-                    , comonad
-                    , lens
-                    , text-ansi
+                    , extra >= 1.7.0 && <2
+                    , semigroupoids >=6.0 && <6.1
+                    , comonad >=5.0.0 && <6
+                    , lens >=5.2.3 && <6.0
+                    , text-ansi >=0.2.0 && <0.4
+                    , effectful-core ^>=2.3.0.0
+                    , deriving-compat ^>=0.6.0
+                    , these >=0.2 && <2.0
+                    , free >=5.2
+                    , bifunctors >=5.2
 
     hs-source-dirs:   src
     default-language: GHC2021
@@ -81,6 +95,12 @@ library
         OverloadedStrings
         TypeFamilies
         LambdaCase
+        ViewPatterns
+        DataKinds
+        DerivingVia
+        StandaloneDeriving
+        DerivingStrategies
+        BlockArguments
 
 executable rlpc
     import:           warnings
@@ -91,11 +111,10 @@ executable rlpc
     build-depends: base >=4.17.0.0 && <4.20.0.0
                  , rlp
                  , optparse-applicative >= 0.18.1 && < 0.19
-                 , microlens >= 0.4.13 && < 0.5
-                 , microlens-mtl >= 0.2.0 && < 0.3
                  , mtl >= 2.3.1 && < 2.4
                  , unordered-containers >= 0.2.20 && < 0.3
-                 , text >= 2.0.2 && < 2.1
+                 , lens >=5.2.3 && <6.0
+                 , text >= 2.0.2 && < 2.2
 
     hs-source-dirs:   app
     default-language: GHC2021
@@ -112,8 +131,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
 

rlpc.drawio

@@ -0,0 +1,253 @@
+<mxfile host="app.diagrams.net" modified="2024-02-08T07:33:52.268Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:122.0) Gecko/20100101 Firefox/122.0" etag="_2ex2NLQLCDMU70EmKFT" version="23.0.2" type="device">
+  <diagram name="Page-1" id="ijVUcW-Be2043inOeyM6">
+    <mxGraphModel dx="1629" dy="2189" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="827" pageHeight="1169" math="0" shadow="0">
+      <root>
+        <mxCell id="0" />
+        <mxCell id="1" parent="0" />
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-64" value="&lt;div&gt;&lt;font face=&quot;Helvetica&quot;&gt;rl&#39; source code&lt;/font&gt;&lt;/div&gt;" style="rounded=0;whiteSpace=wrap;html=1;fillColor=#fff2cc;strokeColor=#d6b656;fontFamily=Courier New;" parent="1" vertex="1">
+          <mxGeometry x="10" y="154.92" width="120" height="60" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-72" value="" style="group;fontFamily=Courier New;" parent="1" vertex="1" connectable="0">
+          <mxGeometry x="150" y="-60" width="1440" height="780" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-2" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-72" vertex="1">
+          <mxGeometry width="1440" height="780" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-3" value="&lt;div&gt;&lt;font face=&quot;Helvetica&quot;&gt;RLPC&lt;/font&gt;&lt;/div&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-2" vertex="1">
+          <mxGeometry width="1440" height="76.09756097560975" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-56" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-2" vertex="1">
+          <mxGeometry x="38.4" y="68.42" width="431.6" height="221.58" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-57" value="&lt;div&gt;&lt;font face=&quot;Helvetica&quot;&gt;Parser&lt;/font&gt;&lt;/div&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-56" vertex="1">
+          <mxGeometry width="431.6" height="27.6975" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-58" value="Rlp.Parse&lt;br&gt;&lt;div&gt;(src/Rlp/Parse.y)&lt;/div&gt;" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;whiteSpace=wrap;points=[];strokeColor=#6c8ebf;fillColor=#dae8fc;glass=0;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-56" vertex="1">
+          <mxGeometry x="26.980533333333334" y="27.6975" width="371.43053333333336" height="55.395" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-59" value="&lt;div&gt;Rlp.Lex&lt;/div&gt;&lt;div&gt;&lt;br&gt;&lt;/div&gt;&lt;div&gt;(src/Rlp/Lex.x)&lt;br&gt;&lt;/div&gt;" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-56" vertex="1">
+          <mxGeometry x="26.98606666666666" y="147.72" width="170.33402285714286" height="55.395" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-61" value="" style="endArrow=classic;html=1;rounded=0;fontFamily=Courier New;exitX=0.25;exitY=0;exitDx=0;exitDy=0;" parent="l7NxJpuHm0Jx_7flO9iA-56" edge="1" source="l7NxJpuHm0Jx_7flO9iA-59">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="111.49666666666668" y="147.72" as="sourcePoint" />
+            <mxPoint x="69.26631355932203" y="83.84879190161169" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-62" value="&lt;div&gt;RlpToken&lt;/div&gt;" style="edgeLabel;resizable=0;html=1;align=center;verticalAlign=middle;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-61" connectable="0" vertex="1">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="-33" y="5" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-74" value="&lt;div&gt;Rlp.Parse.Associate&lt;/div&gt;" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-56" vertex="1">
+          <mxGeometry x="244.26979047619054" y="147.72" width="154.14285714285714" height="55.395" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-75" value="" style="endArrow=classic;html=1;rounded=0;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-56" source="l7NxJpuHm0Jx_7flO9iA-58" target="l7NxJpuHm0Jx_7flO9iA-74" edge="1">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="271.29142857142864" y="175.4175" as="sourcePoint" />
+            <mxPoint x="394.60571428571427" y="175.4175" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-77" value="&lt;div&gt;RlpProgram&#39; RlpcPs&lt;/div&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-75" vertex="1" connectable="0">
+          <mxGeometry x="0.0677" y="5" relative="1" as="geometry">
+            <mxPoint x="39" y="6" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-3" value="" style="endArrow=classic;html=1;rounded=0;exitX=0.368;exitY=1.014;exitDx=0;exitDy=0;exitPerimeter=0;entryX=0.811;entryY=-0.021;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-56" source="l7NxJpuHm0Jx_7flO9iA-58" target="l7NxJpuHm0Jx_7flO9iA-59">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="168.70805084745763" y="201.9041131288017" as="sourcePoint" />
+            <mxPoint x="225.8584745762712" y="152.71439595080588" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-4" value="&lt;p style=&quot;line-height: 60%;&quot;&gt;&lt;font style=&quot;font-size: 7px;&quot;&gt;(lexer &amp;amp; parser threaded w/ CPS)&lt;/font&gt;&lt;/p&gt;" style="text;html=1;strokeColor=none;fillColor=none;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-56">
+          <mxGeometry x="88.69745762711862" y="103.52467877281002" width="68.58050847457626" height="29.513830306797498" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-69" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-2" vertex="1">
+          <mxGeometry x="38.4" y="531.8231578947368" width="431.6" height="230.4557894736842" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-70" value="&lt;div&gt;&lt;font face=&quot;Helvetica&quot;&gt;Desugarer&lt;/font&gt;&lt;/div&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" parent="l7NxJpuHm0Jx_7flO9iA-69" vertex="1">
+          <mxGeometry width="431.6" height="46.091157894736845" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-1" value="&lt;div&gt;Rlp2Core&lt;/div&gt;" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-69">
+          <mxGeometry x="22.122266666666665" y="46.088669843028626" width="387.34440000000006" height="159.17559608494923" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-6" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-2">
+          <mxGeometry x="904" y="68.42105263157895" width="186.6" height="697.8947368421053" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-7" value="&lt;font face=&quot;Helvetica&quot;&gt;Evaluation Model&lt;br&gt;&lt;/font&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-6">
+          <mxGeometry width="186.6" height="107.07065060420568" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-8" value="GM" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-6">
+          <mxGeometry x="9.568013810372213" y="356.90796215152363" width="167.46559322033886" height="82.98740890928475" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-9" value="TM" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-6">
+          <mxGeometry x="9.562261652542377" y="263.9548629430177" width="167.46559322033886" height="82.98740890928475" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-10" value="TIM" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-6">
+          <mxGeometry x="9.56226165254238" y="168.9311122835313" width="167.46559322033886" height="82.98740890928475" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-11" value="STG" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-6">
+          <mxGeometry x="9.56720338983051" y="73.90736162404495" width="167.46559322033886" height="82.98740890928475" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-12" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-2">
+          <mxGeometry x="530" y="68.42" width="281.6" height="314.74" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-13" value="&lt;div&gt;&lt;font face=&quot;Helvetica&quot;&gt;Preprocessing&lt;/font&gt;&lt;/div&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-12">
+          <mxGeometry width="281.5999999999999" height="24.68549019607843" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-15" value="Core2Core" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;verticalAlign=top;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-12">
+          <mxGeometry x="22.25077720207253" y="49.37098039215686" width="237.09844559585483" height="259.1976470588235" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-16" value="&lt;font face=&quot;Courier New&quot;&gt;tagData&lt;/font&gt;" style="rounded=1;whiteSpace=wrap;html=1;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-12">
+          <mxGeometry x="31.36994818652857" y="74.0564705882353" width="218.860103626943" height="37.02823529411765" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-18" value="&lt;font face=&quot;Courier New&quot;&gt;defineData&lt;/font&gt;" style="rounded=1;whiteSpace=wrap;html=1;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-12">
+          <mxGeometry x="31.36994818652857" y="160.45568627450984" width="218.860103626943" height="37.02823529411765" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-17" value="&lt;font face=&quot;Courier New&quot;&gt;liftNonStrictCases&lt;/font&gt;" style="rounded=1;whiteSpace=wrap;html=1;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-12">
+          <mxGeometry x="31.369948186528582" y="118.66932274509804" width="218.860103626943" height="37.02823529411765" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-20" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-2">
+          <mxGeometry x="1240" y="68.42105263157895" width="186.6" height="697.8947368421053" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-21" value="&lt;font face=&quot;Helvetica&quot;&gt;Some target&lt;br&gt;&lt;/font&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-20">
+          <mxGeometry width="186.6" height="107.07065060420568" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-27" value="" style="endArrow=classic;html=1;rounded=0;entryX=-0.019;entryY=0.844;entryDx=0;entryDy=0;entryPerimeter=0;exitX=0.98;exitY=0.066;exitDx=0;exitDy=0;exitPerimeter=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-2" source="MMc0v0DIyy0xya0iXp__-1" target="MMc0v0DIyy0xya0iXp__-12">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="450" y="684.2105263157895" as="sourcePoint" />
+            <mxPoint x="500" y="615.7894736842105" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-28" value="&lt;font face=&quot;Courier New&quot;&gt;Program&#39;&lt;/font&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];" vertex="1" connectable="0" parent="MMc0v0DIyy0xya0iXp__-27">
+          <mxGeometry x="-0.1473" y="1" relative="1" as="geometry">
+            <mxPoint x="7" y="1" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-30" value="" style="endArrow=classic;html=1;rounded=0;entryX=-0.013;entryY=0.321;entryDx=0;entryDy=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryPerimeter=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-2" source="MMc0v0DIyy0xya0iXp__-12" target="MMc0v0DIyy0xya0iXp__-6">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="810" y="588.421052631579" as="sourcePoint" />
+            <mxPoint x="860" y="520" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-31" value="&lt;font face=&quot;Courier New&quot;&gt;Program&#39;&lt;/font&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];" vertex="1" connectable="0" parent="MMc0v0DIyy0xya0iXp__-30">
+          <mxGeometry x="0.0097" y="-1" relative="1" as="geometry">
+            <mxPoint x="-1" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-32" value="" style="endArrow=classic;html=1;rounded=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-2" source="MMc0v0DIyy0xya0iXp__-6" target="MMc0v0DIyy0xya0iXp__-20">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="810" y="588.421052631579" as="sourcePoint" />
+            <mxPoint x="860" y="520" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-33" value="&lt;font face=&quot;Courier New&quot;&gt;[Instr]&lt;/font&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];" vertex="1" connectable="0" parent="MMc0v0DIyy0xya0iXp__-32">
+          <mxGeometry x="0.0406" y="1" relative="1" as="geometry">
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-35" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-2">
+          <mxGeometry x="530" y="630" width="281.6" height="131.32" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-36" value="&lt;font face=&quot;Helvetica&quot;&gt;Core Parser&lt;br&gt;&lt;/font&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-35">
+          <mxGeometry width="281.59999999999997" height="10.299607843137254" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-41" value="Core.Lex" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-35">
+          <mxGeometry x="10.140518134715029" y="16.369019607843132" width="87.1306390328152" height="106.24535947712415" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-42" value="Core.Parse" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-35">
+          <mxGeometry x="182.3834196891192" y="16.369019607843146" width="87.1306390328152" height="106.24535947712415" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-43" value="&lt;font face=&quot;Courier New&quot;&gt;CoreToken&lt;/font&gt;" style="endArrow=classic;html=1;rounded=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;" edge="1" parent="MMc0v0DIyy0xya0iXp__-35" source="MMc0v0DIyy0xya0iXp__-41" target="MMc0v0DIyy0xya0iXp__-42">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="-72.95336787564769" y="39.35921568627452" as="sourcePoint" />
+            <mxPoint x="-12.15889464594128" y="1.0422222222222326" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-51" value="" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-2">
+          <mxGeometry x="530" y="440" width="281.6" height="131.32" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-52" value="&lt;font face=&quot;Helvetica&quot;&gt;Core Type-checker&lt;br&gt;&lt;/font&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-51">
+          <mxGeometry width="281.59999999999997" height="10.299607843137254" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-46" value="(currently unimplemented)" style="rounded=1;absoluteArcSize=1;html=1;arcSize=10;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-72">
+          <mxGeometry x="40" y="360" width="431.6" height="90.46" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-47" value="&lt;font face=&quot;Verdana&quot;&gt;Type-checker&lt;/font&gt;" style="html=1;shape=mxgraph.er.anchor;whiteSpace=wrap;fontFamily=Courier New;" vertex="1" parent="MMc0v0DIyy0xya0iXp__-46">
+          <mxGeometry width="431.6" height="18.092000000000002" as="geometry" />
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-80" value="" style="endArrow=classic;html=1;rounded=0;" parent="l7NxJpuHm0Jx_7flO9iA-72" source="l7NxJpuHm0Jx_7flO9iA-74" target="MMc0v0DIyy0xya0iXp__-46" edge="1">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="537.6" y="424.2105263157895" as="sourcePoint" />
+            <mxPoint x="-40" y="490" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-81" value="&lt;font face=&quot;Courier New&quot;&gt;RlpProgram&#39; RlpcPs&lt;br&gt;&lt;/font&gt;" style="edgeLabel;resizable=0;html=1;align=center;verticalAlign=middle;" parent="l7NxJpuHm0Jx_7flO9iA-80" connectable="0" vertex="1">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="6" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-49" value="" style="endArrow=classic;html=1;rounded=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-72" source="MMc0v0DIyy0xya0iXp__-46" target="l7NxJpuHm0Jx_7flO9iA-69">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="352" y="282" as="sourcePoint" />
+            <mxPoint x="295" y="370" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-50" value="&lt;font face=&quot;Courier New&quot;&gt;RlpProgram&#39; RlpcTc&lt;/font&gt;" style="edgeLabel;resizable=0;html=1;align=center;verticalAlign=middle;" connectable="0" vertex="1" parent="MMc0v0DIyy0xya0iXp__-49">
+          <mxGeometry relative="1" as="geometry">
+            <mxPoint x="6" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-57" value="Core.HindleyMilner" style="rounded=1;arcSize=10;whiteSpace=wrap;html=1;align=center;fillColor=#dae8fc;strokeColor=#6c8ebf;fontFamily=Courier New;" vertex="1" parent="l7NxJpuHm0Jx_7flO9iA-72">
+          <mxGeometry x="540" y="460" width="260" height="106.24" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-58" value="" style="endArrow=classic;html=1;rounded=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-72" source="MMc0v0DIyy0xya0iXp__-42" target="MMc0v0DIyy0xya0iXp__-57">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="530" y="550" as="sourcePoint" />
+            <mxPoint x="580" y="500" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-59" value="Program&#39;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontFamily=Courier New;" vertex="1" connectable="0" parent="MMc0v0DIyy0xya0iXp__-58">
+          <mxGeometry x="-0.0188" y="-3" relative="1" as="geometry">
+            <mxPoint y="-1" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-60" value="" style="endArrow=classic;html=1;rounded=0;" edge="1" parent="l7NxJpuHm0Jx_7flO9iA-72" source="MMc0v0DIyy0xya0iXp__-57" target="MMc0v0DIyy0xya0iXp__-15">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="741" y="656" as="sourcePoint" />
+            <mxPoint x="704" y="576" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-61" value="Program&#39;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];fontFamily=Courier New;" vertex="1" connectable="0" parent="MMc0v0DIyy0xya0iXp__-60">
+          <mxGeometry x="-0.0188" y="-3" relative="1" as="geometry">
+            <mxPoint y="-1" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="l7NxJpuHm0Jx_7flO9iA-65" value="" style="endArrow=classic;html=1;rounded=0;fontFamily=Courier New;" parent="1" source="l7NxJpuHm0Jx_7flO9iA-64" target="l7NxJpuHm0Jx_7flO9iA-59" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="290" y="400" as="sourcePoint" />
+            <mxPoint x="340" y="350" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-26" value="&lt;font face=&quot;Helvetica&quot;&gt;Core source code&lt;br&gt;&lt;/font&gt;" style="rounded=0;whiteSpace=wrap;html=1;fillColor=#fff2cc;strokeColor=#d6b656;fontFamily=Courier New;" vertex="1" parent="1">
+          <mxGeometry x="673.7099999999999" y="740" width="120" height="60" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-29" value="&lt;div&gt;&lt;font face=&quot;Helvetica&quot;&gt;???&lt;/font&gt;&lt;/div&gt;" style="rounded=0;whiteSpace=wrap;html=1;fillColor=#fff2cc;strokeColor=#d6b656;fontFamily=Courier New;" vertex="1" parent="1">
+          <mxGeometry x="1420" y="730" width="120" height="60" as="geometry" />
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-34" value="" style="endArrow=classic;html=1;rounded=0;exitX=0.5;exitY=0;exitDx=0;exitDy=0;" edge="1" parent="1" source="MMc0v0DIyy0xya0iXp__-26" target="MMc0v0DIyy0xya0iXp__-41">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="960" y="370" as="sourcePoint" />
+            <mxPoint x="690" y="570" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="MMc0v0DIyy0xya0iXp__-62" value="" style="endArrow=classic;html=1;rounded=0;" edge="1" parent="1" source="MMc0v0DIyy0xya0iXp__-20" target="MMc0v0DIyy0xya0iXp__-29">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="1060" y="650" as="sourcePoint" />
+            <mxPoint x="1110" y="600" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+      </root>
+    </mxGraphModel>
+  </diagram>
+</mxfile>

src/Compiler/JustRun.hs

@@ -8,39 +8,69 @@ that use Prelude types such as @Either@ and @String@ rather than more complex
 types such as @RLPC@ or @Text@.
 -}
 module Compiler.JustRun
-    ( justLexSrc
-    , justParseSrc
-    , justTypeCheckSrc
+    ( 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                    ((>=>))
+import Control.Monad                    ((>=>), void)
+import Control.Comonad
+import Control.Lens
 import Data.Text                        qualified as T
 import Data.Function                    ((&))
+import System.IO
 import GM
+import Rlp2Core
+import Data.Pretty
+
+import Rlp.AltParse
+import Rlp.AltSyntax                    qualified as Rlp
 ----------------------------------------------------------------------------------
 
-justLexSrc :: String -> Either [MsgEnvelope RlpcError] [CoreToken]
-justLexSrc s = lexCoreR (T.pack s)
-             & fmap (map $ \ (Located _ _ _ t) -> t)
-             & rlpcToEither
+justHdbg :: String -> IO GmState
+justHdbg = undefined
+-- justHdbg s = do
+--     p <- evalRLPCIO def (parseRlpProgR >=> desugarRlpProgR $ T.pack s)
+--     withFile "/tmp/t.log" WriteMode $ hdbgProg p
 
-justParseSrc :: String -> Either [MsgEnvelope RlpcError] Program'
-justParseSrc s = parse (T.pack s)
+justLexCore :: String -> Either [MsgEnvelope RlpcError] [CoreToken]
+justLexCore s = lexCoreR (T.pack s)
+              & mapped . each %~ extract
+              & rlpcToEither
+
+justParseCore :: String -> Either [MsgEnvelope RlpcError] (Program Var)
+justParseCore s = parse (T.pack s)
+                & rlpcToEither
+    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 = lexCoreR >=> parseCoreProgR
+    where parse = parseRlpProgR @Identity
 
-justTypeCheckSrc :: String -> Either [MsgEnvelope RlpcError] Program'
-justTypeCheckSrc s = typechk (T.pack s)
-                   & rlpcToEither
+justTypeCheckCore :: String -> Either [MsgEnvelope RlpcError] Program'
+justTypeCheckCore s = typechk (T.pack s)
+                    & rlpcToEither
     where typechk = lexCoreR >=> parseCoreProgR >=> checkCoreProgR
 
+makeItPretty :: (Pretty a) => Either e a -> Either e Doc
+makeItPretty = fmap pretty
+
+makeItPretty' :: (Pretty (WithTerseBinds a)) => Either e a -> Either e Doc
+makeItPretty' = fmap (pretty . WithTerseBinds)
+
 rlpcToEither :: RLPC a -> Either [MsgEnvelope RlpcError] a
 rlpcToEither r = case evalRLPC def r of
     (Just a,   _) -> Right a

src/Compiler/RLPC.hs

@@ -10,7 +10,6 @@ errors and the family of RLPC monads.
 {-# LANGUAGE TemplateHaskell #-}
 -- only used for mtl instances
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE DeriveGeneric, DerivingStrategies, DerivingVia #-}
 {-# LANGUAGE BlockArguments, ViewPatterns #-}
 module Compiler.RLPC
     (
@@ -18,6 +17,7 @@ module Compiler.RLPC
       RLPCT(RLPCT),
     -- ** Special cases
       RLPC, RLPCIO
+    , liftIO
     -- ** Running
     , runRLPCT
     , evalRLPCT, evalRLPCIO, evalRLPC
@@ -27,7 +27,7 @@ module Compiler.RLPC
     -- ** Lenses
     , rlpcLogFile, rlpcDFlags, rlpcEvaluator, rlpcInputFiles, rlpcLanguage
     -- * Misc. MTL-style functions
-    , liftErrorful, hoistRlpcT
+    , liftErrorful, liftMaybe, hoistRlpcT
     -- * Misc. Rlpc Monad -related types
     , RLPCOptions(RLPCOptions), IsRlpcError(..), RlpcError(..)
     , MsgEnvelope(..), Severity(..)
@@ -61,10 +61,11 @@ import Data.Coerce
 import Data.Text                (Text)
 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 Lens.Micro.Platform
-import Lens.Micro.Platform.Internal
+import Control.Lens
+import Data.Text.Lens           (packed, unpacked, IsText)
 import System.Exit
 ----------------------------------------------------------------------------------
 
@@ -84,7 +85,11 @@ type RLPC = RLPCT Identity
 
 type RLPCIO = RLPCT IO
 
+instance MonadTrans RLPCT where
+    lift = RLPCT . lift . lift
+
 instance (MonadIO m) => MonadIO (RLPCT m) where
+    liftIO = lift . liftIO
 
 evalRLPC :: RLPCOptions
          -> RLPC a
@@ -103,6 +108,9 @@ 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, [])
+
 hoistRlpcT :: (forall a. m a -> n a)
          -> RLPCT m a -> RLPCT n a
 hoistRlpcT f rma = RLPCT $ ReaderT $ \opt ->
@@ -114,7 +122,7 @@ data RLPCOptions = RLPCOptions
     , _rlpcFFlags      :: HashSet CompilerFlag
     , _rlpcEvaluator   :: Evaluator
     , _rlpcHeapTrigger :: Int
-    , _rlpcLanguage    :: Language
+    , _rlpcLanguage    :: Maybe Language
     , _rlpcInputFiles  :: [FilePath]
     }
     deriving Show
@@ -135,7 +143,7 @@ instance Default RLPCOptions where
         , _rlpcEvaluator = EvaluatorGM
         , _rlpcHeapTrigger = 200
         , _rlpcInputFiles = []
-        , _rlpcLanguage = LanguageRlp
+        , _rlpcLanguage = Nothing
         }
 
 -- debug flags are passed with -dFLAG
@@ -175,14 +183,23 @@ evalRLPCIO opt r = do
         Nothing -> die "Failed, no code compiled."
 
 putRlpcErrs :: RLPCOptions -> [MsgEnvelope RlpcError] -> IO ()
-putRlpcErrs opts = filter byTag
-               >>> traverse_ (putStrLn . ('\n':) . prettyRlpcMsg)
+putRlpcErrs opt es = case opt ^. rlpcLogFile of
+    Just lf -> withFile lf WriteMode putter
+    Nothing -> putter stderr
+  where
+    putter h = hPutStrLn h `traverse_` renderRlpcErrs opt es
+
+renderRlpcErrs :: RLPCOptions -> [MsgEnvelope RlpcError] -> [String]
+renderRlpcErrs opts = (if don'tBother then id else filter byTag)
+                  >>> fmap prettyRlpcMsg
     where
         dflags = opts ^. rlpcDFlags
+        don'tBother = "ALL" `S.member` (opts ^. rlpcDFlags)
 
         byTag :: MsgEnvelope RlpcError -> Bool
         byTag (view msgSeverity -> SevDebug t) =
             t `S.member` dflags
+        byTag _ = True
 
 prettyRlpcMsg :: MsgEnvelope RlpcError -> String
 prettyRlpcMsg m@(view msgSeverity -> SevDebug _) = prettyRlpcDebugMsg m
@@ -206,9 +223,9 @@ docRlpcErr msg = header
                 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 ":"

src/Compiler/RlpcError.hs

@@ -14,6 +14,9 @@ module Compiler.RlpcError
     -- * Located Comonad
     , Located(..)
     , SrcSpan(..)
+
+    -- * Common error messages
+    , undefinedVariableErr
     )
     where
 ----------------------------------------------------------------------------------
@@ -21,8 +24,7 @@ import Control.Monad.Errorful
 import Data.Text                (Text)
 import Data.Text                qualified as T
 import GHC.Exts                 (IsString(..))
-import Lens.Micro.Platform
-import Lens.Micro.Platform.Internal
+import Control.Lens
 import Compiler.Types
 ----------------------------------------------------------------------------------
 
@@ -34,7 +36,7 @@ data MsgEnvelope e = MsgEnvelope
    deriving (Functor, Show)
 
 newtype RlpcError = Text [Text]
-    deriving Show
+               deriving Show
 
 instance IsString RlpcError where
     fromString = Text . pure . T.pack
@@ -47,7 +49,7 @@ instance IsRlpcError RlpcError where
 
 data Severity = SevWarning
               | SevError
-              | SevDebug Text
+              | SevDebug Text -- ^ Tag
               deriving Show
 
 makeLenses ''MsgEnvelope
@@ -75,3 +77,8 @@ debugMsg tag e = MsgEnvelope
     , _msgSeverity = SevDebug tag
     }
 
+undefinedVariableErr :: Text -> RlpcError
+undefinedVariableErr n = Text
+    [ "Variable not in scope: `" <> n <> "'."
+    ]
+

src/Compiler/Types.hs

@@ -1,25 +1,79 @@
+{-# 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
+    , 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 Control.Comonad.Trans.Cofree qualified as Trans.Cofree
+import Control.Comonad.Trans.Cofree (CofreeF)
 import Data.Functor.Apply
 import Data.Functor.Bind
-import Control.Lens             hiding ((<<~))
+import Data.Functor.Compose
+import Data.Functor.Foldable
+import Data.Semigroup.Foldable
+import Data.Fix                     hiding (cata, ana)
+import Data.Kind
+import Control.Lens                 hiding ((<<~), (:<))
+
+import Data.List.NonEmpty           (NonEmpty)
+import Data.Function                (on)
 --------------------------------------------------------------------------------
 
 -- | Token wrapped with a span (line, column, absolute, length)
 data Located a = Located SrcSpan a
-    deriving (Show, Functor)
+    deriving (Show, Lift, Functor)
+
+pattern (:<$) :: a -> f b -> Trans.Cofree.CofreeF f a b
+pattern a :<$ b = a Trans.Cofree.:< b
+
+(<~>) :: 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)
@@ -39,40 +93,137 @@ data SrcSpan = SrcSpan
     !Int -- ^ Column
     !Int -- ^ Absolute
     !Int -- ^ Length
-    deriving Show
+    deriving (Show, Eq, Lift)
 
-tupling :: Iso' SrcSpan (Int, Int, Int, Int)
-tupling = iso (\ (SrcSpan a b c d) -> (a,b,c,d))
+_SrcSpan :: Iso' SrcSpan (Int, Int, Int, Int)
+_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 = tupling . _1
-srcspanColumn = tupling . _2
-srcspanAbs = tupling . _3
-srcspanLen = tupling . _4
+srcSpanLine, srcSpanColumn, srcSpanAbs, srcSpanLen :: Lens' SrcSpan Int
+srcSpanLine = _SrcSpan . _1
+srcSpanColumn = _SrcSpan . _2
+srcSpanAbs = _SrcSpan . _3
+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)
-            GT -> max sb (aa + la - ab)
+            LT -> max sa (ab + sb - aa)
+            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
-mc <~> ma = mc >>- \f -> ma =>> f
+data GetSetLens (k :: GetOrSet) s t a b :: Type where
+    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
+
+class HasLocation k s | s -> k where
+    -- location :: (Access k f, Functor f) => LensLike' f s SrcSpan
+    getSetLocation :: GetSetLens' k s SrcSpan
+
+type family Access (k :: GetOrSet) f where
+    Access GetSet f = Functor f
+    Access Set f = Settable f
+    Access Get f = (Functor f, Contravariant f)
+
+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

@@ -8,18 +8,21 @@ module Control.Monad.Errorful
     , errorful
     , runErrorful
     , mapErrorful
+    , hoistErrorfulT
     , MonadErrorful(..)
     )
     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
 import Data.HashSet                 (HashSet)
 import Data.HashSet                 qualified as H
-import Lens.Micro
+import Control.Lens
 ----------------------------------------------------------------------------------
 
 newtype ErrorfulT e m a = ErrorfulT { runErrorfulT :: m (Maybe a, [e]) }
@@ -50,7 +53,7 @@ instance (MonadIO m) => MonadIO (ErrorfulT e m) where
     liftIO = lift . liftIO
 
 instance (Functor m) => Functor (ErrorfulT e m) where
-    fmap f (ErrorfulT m) = ErrorfulT (m & mapped . _1 . _Just %~ f)
+    fmap f (ErrorfulT m) = ErrorfulT (m <&> _1 . _Just %~ f)
 
 instance (Applicative m) => Applicative (ErrorfulT e m) where
     pure a = ErrorfulT . pure $ (Just a, [])
@@ -63,17 +66,20 @@ instance (Monad m) => Monad (ErrorfulT e m) where
     ErrorfulT m >>= k = ErrorfulT $ do
         (a,es) <- m
         case a of
-            Just x      -> runErrorfulT (k x)
+            Just x      -> runErrorfulT (k x) <&> _2 %~ (es<>)
             Nothing     -> pure (Nothing, es)
 
 mapErrorful :: (Functor m) => (e -> e') -> ErrorfulT e m a -> ErrorfulT e' m a
 mapErrorful f (ErrorfulT m) = ErrorfulT $
-    m & mapped . _2 . mapped %~ f
+    m <&> _2 . mapped %~ f
 
 -- when microlens-pro drops we can write this as
 --    mapErrorful f = coerced . mapped . _2 . mapped %~ f
 -- lol
 
+hoistErrorfulT :: (forall a. m a -> n a) -> ErrorfulT e m a -> ErrorfulT e n a
+hoistErrorfulT nt (ErrorfulT m) = ErrorfulT (nt m)
+
 --------------------------------------------------------------------------------
 -- daily dose of n^2 instances
 
@@ -81,3 +87,16 @@ instance (Monad m, MonadErrorful e m) => MonadErrorful e (ReaderT r m) where
     addWound = lift . addWound
     addFatal = lift . addFatal
 
+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 (Monoid w, Monad m, MonadAccum w m)
+      => MonadAccum w (ErrorfulT e m) where
+    accum = lift . accum
+

src/Control/Monad/Utils.hs

@@ -1,10 +1,15 @@
 module Control.Monad.Utils
     ( mapAccumLM
+    , Kendo(..)
+    , generalise
     )
     where
 ----------------------------------------------------------------------------------
 import Data.Tuple               (swap)
+import Data.Coerce
+import Data.Functor.Identity
 import Control.Monad.State
+import Control.Monad
 ----------------------------------------------------------------------------------
 
 -- | Monadic variant of @mapAccumL@
@@ -19,3 +24,14 @@ mapAccumLM k s t = swap <$> runStateT (traverse k' t) s
         k' :: a -> StateT s m b
         k' a = StateT $ fmap swap <$> flip k a
 
+newtype Kendo m a = Kendo { appKendo :: a -> m a }
+
+instance (Monad m) => Semigroup (Kendo m a) where
+    Kendo f <> Kendo g = Kendo (f <=< g)
+
+instance (Monad m) => Monoid (Kendo m a) where
+    mempty = Kendo pure
+
+generalise :: (Monad m) => Identity a -> m a
+generalise (Identity a) = pure a
+

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
--- sumList = undefined
--- constDivZero = undefined
--- idCase = undefined
+letRecExample = undefined
 
----
+{--
 
 letrecExample :: Program'
 letrecExample = [coreProg|
@@ -76,12 +73,12 @@ negExample3 = [coreProg|
 
 arithExample1 :: Program'
 arithExample1 = [coreProg|
-    main = (+#) 3 (negate# 2);
+    main = +# 3 (negate# 2);
 |]
 
 arithExample2 :: Program'
 arithExample2 = [coreProg|
-    main = negate# ((+#) 2 ((*#) 5 3));
+    main = negate# (+# 2 (*# 5 3));
 |]
 
 ifExample1 :: Program'
@@ -96,7 +93,7 @@ ifExample2 = [coreProg|
 
 facExample :: Program'
 facExample = [coreProg|
-    fac n = if# ((==#) n 0) 1 ((*#) n (fac ((-#) n 1)));
+    fac n = if# (==# n 0) 1 (*# n (fac (-# n 1)));
     main = fac 3;
 |]
 
@@ -149,14 +146,14 @@ caseBool1 = [coreProg|
     false = Pack{0 0};
     true = Pack{1 0};
 
-    main = _if false ((+#) 2 3) ((*#) 4 5);
+    main = _if false (+# 2 3) (*# 4 5);
 |]
 
 fac3 :: Program'
 fac3 = [coreProg|
-    fac n = case (==#) n 0 of
+    fac n = case ==# n 0 of
         { <1> -> 1
-        ; <0> -> (*#) n (fac ((-#) n 1))
+        ; <0> -> *# n (fac (-# n 1))
         };
 
     main = fac 3;
@@ -171,7 +168,7 @@ sumList = [coreProg|
         list = cons 1 (cons 2 (cons 3 nil));
         sum l = case l of
             { <0>      -> 0
-            ; <1> x xs -> (+#) x (sum xs)
+            ; <1> x xs -> +# x (sum xs)
             };
         main = sum list;
     |]
@@ -179,7 +176,7 @@ sumList = [coreProg|
 constDivZero :: Program'
 constDivZero = [coreProg|
         k x y = x;
-        main = k 3 ((/#) 1 0);
+        main = k 3 (/# 1 0);
     |]
 
 idCase :: Program'
@@ -187,7 +184,7 @@ idCase = [coreProg|
         id x = x;
 
         main = id (case Pack{1 0} of
-            { <1> -> (+#) 2 3
+            { <1> -> +# 2 3
             })
     |]
 
@@ -197,7 +194,7 @@ namedBoolCase :: Program'
 namedBoolCase = [coreProg|
         {-# PackData True 1 0 #-}
         {-# PackData False 0 0 #-}
-        main = case (==#) 1 1 of
+        main = case ==# 1 1 of
             { True -> 123
             ; False -> 456
             }
@@ -207,8 +204,6 @@ namedConsCase :: Program'
 namedConsCase = [coreProg|
         {-# PackData Nil  0 0 #-}
         {-# PackData Cons 1 2 #-}
-        Nil = Pack{0 0};
-        Cons = Pack{1 2};
         foldr f z l = case l of
             { Nil       -> z
             ; Cons x xs -> f x (foldr f z xs)
@@ -245,3 +240,4 @@ namedConsCase = [coreProg|
 --         ]
 
 --}
+

src/Core/HindleyMilner.hs

@@ -10,27 +10,37 @@ module Core.HindleyMilner
     , check
     , checkCoreProg
     , checkCoreProgR
+    , checkCoreExprR
     , TypeError(..)
     , HMError
     )
     where
 ----------------------------------------------------------------------------------
-import Lens.Micro
-import Lens.Micro.Mtl
-import Lens.Micro.Platform
+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 Compiler.RlpcError
 import Control.Monad            (foldM, void, forM)
-import Control.Monad.Errorful   (Errorful, addFatal)
+import Control.Monad.Errorful
 import Control.Monad.State
-import Control.Monad.Utils      (mapAccumLM)
+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)]
@@ -38,8 +48,6 @@ type Context b = [(b, Type)]
 -- | Unannotated typing context, AKA our beloved Γ.
 type Context' = Context Name
 
--- TODO: Errorful monad?
-
 -- | Type error enum.
 data TypeError
     -- | Two types could not be unified
@@ -56,25 +64,23 @@ instance IsRlpcError TypeError where
         -- todo: use anti-parser instead of show
         TyErrCouldNotUnify t u -> Text
             [ T.pack $ printf "Could not match type `%s` with `%s`."
-                              (show t) (show u)
-            , "Expected: " <> tshow t
-            , "Got: " <> tshow u
+                              (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 error lol"
+            [ T.pack $ printf "Recursive type: `%s' occurs in `%s'"
+                              (rpretty @String t) (rpretty @String x)
             ]
 
-        where tshow = T.pack . show
-
 -- | 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
 
--- TODO: better errors. Errorful-esque, with cummulative errors instead of
--- instantly dying.
+{--
 
 -- | Assert that an expression unifies with a given type
 --
@@ -93,7 +99,7 @@ check g t1 e = do
 -- in the mean time all top-level binders must have a type annotation.
 checkCoreProg :: Program' -> HMError ()
 checkCoreProg p = scDefs
-            & traverse_ k
+                & traverse_ k
     where
         scDefs = p ^. programScDefs
         g = gatherTypeSigs p
@@ -105,10 +111,17 @@ checkCoreProg p = scDefs
              where scname = sc ^. _lhs._1
 
 -- | @checkCoreProgR p@ returns @p@ if @p@ successfully typechecks.
-checkCoreProgR :: (Applicative m) => Program' -> RLPCT m Program'
-checkCoreProgR p = undefined
+checkCoreProgR :: forall m. (Monad m) => Program' -> RLPCT m Program'
+checkCoreProgR p = (hoistRlpcT generalise . liftE . checkCoreProg $ p)
+                $> p
+    where
+        liftE = liftErrorful . mapErrorful (errorMsg (SrcSpan 0 0 0 0))
 
-{-# WARNING checkCoreProgR "unimpl" #-}
+checkCoreExprR :: (Monad m) => Context' -> Expr' -> RLPCT m Expr'
+checkCoreExprR g e = (hoistRlpcT generalise . liftE . infer g $ e)
+                  $> e
+    where
+        liftE = liftErrorful . mapErrorful (errorMsg (SrcSpan 0 0 0 0))
 
 -- | Infer the type of an expression under some context.
 --
@@ -271,9 +284,4 @@ demoContext =
     , ("False", TyCon "Bool")
     ]
 
-pprintType :: Type -> String
-pprintType (s :-> t) = "(" <> pprintType s <> " -> " <> pprintType t <> ")"
-pprintType TyFun = "(->)"
-pprintType (TyVar x) = x ^. unpacked
-pprintType (TyCon t) = t ^. unpacked
-
+--}

src/Core/Lex.x

@@ -23,10 +23,10 @@ import Data.String          (IsString(..))
 import Data.Functor.Identity
 import Core.Syntax
 import Compiler.RLPC
+import Compiler.Types
 -- TODO: unify Located definitions
-import Compiler.RlpcError   hiding (Located(..))
-import Lens.Micro
-import Lens.Micro.TH
+import Compiler.RlpcError
+import Control.Lens
 }
 
 %wrapper "monad-strict-text"
@@ -78,7 +78,7 @@ rlp :-
     "{"                     { constTok TokenLBrace }
     "}"                     { constTok TokenRBrace }
     ";"                     { constTok TokenSemicolon }
-    "::"                    { constTok TokenHasType }
+    ":"                     { constTok TokenHasType }
     "@"                     { constTok TokenTypeApp }
     "{-#"                   { constTok TokenLPragma `andBegin` pragma }
 
@@ -120,11 +120,9 @@ rlp :-
 }
 
 {
-data Located a = Located Int Int Int a
-    deriving Show
 
 constTok :: t -> AlexInput -> Int -> Alex (Located t)
-constTok t (AlexPn _ y x,_,_,_) l = pure $ Located y x l t
+constTok t (AlexPn _ y x,_,_,_) l = pure $ nolo t
 
 data CoreToken = TokenLet
                | TokenLetrec
@@ -171,7 +169,7 @@ data SrcErrorType = SrcErrLexical String
 type Lexer = AlexInput -> Int -> Alex (Located CoreToken)
 
 lexWith :: (Text -> CoreToken) -> Lexer
-lexWith f (AlexPn _ y x,_,_,s) l = pure $ Located y x l (f $ T.take l s)
+lexWith f (AlexPn _ y x,_,_,s) l = pure . nolo . f . T.take l $ s
 
 -- | The main lexer driver.
 lexCore :: Text -> RLPC [Located CoreToken]
@@ -191,14 +189,14 @@ lexCoreR = hoistRlpcT generalise . lexCore
 -- debugging
 lexCore' :: Text -> RLPC [CoreToken]
 lexCore' s = fmap f <$> lexCore s
-    where f (Located _ _ _ t) = t
+    where f (Located _ t) = t
 
 lexStream :: Alex [Located CoreToken]
 lexStream = do
     l <- alexMonadScan
     case l of
-        Located _ _ _ TokenEOF  -> pure [l]
-        _                       -> (l:) <$> lexStream
+        Located _ TokenEOF -> pure [l]
+        _                  -> (l:) <$> lexStream
 
 data ParseError = ParErrLexical String
                 | ParErrParse
@@ -214,7 +212,7 @@ instance IsRlpcError ParseError where
 
 alexEOF :: Alex (Located CoreToken)
 alexEOF = Alex $ \ st@(AlexState { alex_pos = AlexPn _ y x }) ->
-    Right (st, Located y x 0 TokenEOF)
+    Right (st, nolo $ TokenEOF)
 
 }
 

src/Core/Lex.x.old

@@ -1,315 +0,0 @@
-{
--- TODO: layout semicolons are not inserted at EOf.
-{-# LANGUAGE TemplateHaskell #-}
-module Core.Lex
-    ( lexCore
-    , lexCore'
-    , CoreToken(..)
-    , ParseError(..)
-    , Located(..)
-    , AlexPosn(..)
-    )
-    where
-import Data.Char (chr)
-import Debug.Trace
-import Core.Syntax
-import Compiler.RLPC
-import Lens.Micro
-import Lens.Micro.TH
-}
-
-%wrapper "monadUserState"
-
-$whitechar = [ \t\n\r\f\v]
-$special   = [\(\)\,\;\[\]\{\}]
-
-$digit     = 0-9
-
-$ascsymbol = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~]
-$unisymbol = [] -- TODO
-$symbol    = [$ascsymbol $unisymbol] # [$special \_\:\"\']
-
-$large     = [A-Z \xc0-\xd6 \xd8-\xde]
-$small     = [a-z \xdf-\xf6 \xf8-\xff \_]
-$alpha     = [$small $large]
-
-$graphic   = [$small $large $symbol $digit $special \:\"\']
-
-$octit     = 0-7
-$hexit     = [0-9 A-F a-f]
-$namechar  = [$alpha $digit \' \#]
-$symchar   = [$symbol \:]
-$nl        = [\n\r]
-$white_no_nl = $white # $nl
-
-@reservedid = 
-    case|data|do|import|in|let|letrec|module|of|where
-
-@reservedop =
-    "=" | \\ | "->"
-
-@varname   = $small $namechar*
-@conname   = $large $namechar*
-@varsym    = $symbol $symchar*
-@consym    = \: $symchar*
-
-@decimal = $digit+
-
-rlp :-
-
--- everywhere: skip whitespace
-$white_no_nl+           { skip }
-
--- TODO: `--` could begin an operator
-"--"[^$nl]*             { skip }
-"--"\-*[^$symbol].*     { skip }
-
-"{-"                        { nestedComment }
-
--- syntactic symbols
-<0>
-{
-    "("                     { constTok TokenLParen }
-    ")"                     { constTok TokenRParen }
-    "{"                     { lbrace }
-    "}"                     { rbrace }
-    ";"                     { constTok TokenSemicolon }
-    ","                     { constTok TokenComma }
-}
-
--- keywords
--- see commentary on the layout system
-<0>
-{
-    "let"                   { constTok TokenLet `andBegin` layout }
-    "letrec"                { constTok TokenLetrec `andBegin` layout }
-    "of"                    { constTok TokenOf `andBegin` layout }
-    "case"                  { constTok TokenCase }
-    "module"                { constTok TokenModule }
-    "in"                    { letin }
-    "where"                 { constTok TokenWhere `andBegin` layout }
-}
-
--- reserved symbols
-<0>
-{
-    "="                     { constTok TokenEquals }
-    "->"                    { constTok TokenArrow }
-}
-
--- identifiers
-<0>
-{
-    -- TODO: qualified names
-    @varname                { lexWith TokenVarName }
-    @conname                { lexWith TokenConName }
-    @varsym                 { lexWith TokenVarSym }
-}
-
--- literals
-<0>
-{
-    @decimal                { lexWith (TokenLitInt . read @Int) }
-}
-
-<0> \n                      { begin bol }
-
-<initial>
-{
-    $white                  { skip }
-    \n                      { skip }
-    ()                      { topLevelOff `andBegin` 0 }
-}
-
-<bol>
-{
-    \n                      { skip }
-    ()                      { doBol `andBegin` 0 }
-}
-
-<layout>
-{
-    $white                  { skip }
-    \{                      { lbrace `andBegin` 0 }
-    ()                      { noBrace `andBegin` 0 }
-}
-
-{
-data Located a = Located Int Int Int a
-    deriving Show
-
-constTok :: t -> AlexInput -> Int -> Alex (Located t)
-constTok t (AlexPn _ y x,_,_,_) l = pure $ Located y x l t
-
-data CoreToken = TokenLet
-               | TokenLetrec
-               | TokenIn
-               | TokenModule
-               | TokenWhere
-               | TokenComma
-               | TokenCase
-               | TokenOf
-               | TokenLambda
-               | TokenArrow
-               | TokenLitInt Int
-               | TokenVarName Name
-               | TokenConName Name
-               | TokenVarSym Name
-               | TokenConSym Name
-               | TokenEquals
-               | TokenLParen
-               | TokenRParen
-               | TokenLBrace
-               | TokenRBrace
-               | TokenLBraceV -- virtual brace inserted by layout
-               | TokenRBraceV -- virtual brace inserted by layout
-               | TokenIndent Int
-               | TokenDedent Int
-               | TokenSemicolon
-               | TokenEOF
-               deriving Show
-
-data LayoutContext = Layout Int
-                   | NoLayout
-                   deriving Show
-
-data AlexUserState = AlexUserState
-    { _ausContext :: [LayoutContext]
-    }
-
-ausContext :: Lens' AlexUserState [LayoutContext]
-ausContext f (AlexUserState ctx)
-  = fmap
-      (\a -> AlexUserState a) (f ctx)
-{-# INLINE ausContext #-}
-
-pushContext :: LayoutContext -> Alex ()
-pushContext c = do
-    st <- alexGetUserState
-    alexSetUserState $ st { _ausContext = c : _ausContext st }
-
-popContext :: Alex ()
-popContext = do
-    st <- alexGetUserState
-    alexSetUserState $ st { _ausContext = drop 1 (_ausContext st) }
-
-getContext :: Alex [LayoutContext]
-getContext = do
-    st <- alexGetUserState
-    pure $ _ausContext st
-
-type Lexer = AlexInput -> Int -> Alex (Located CoreToken)
-
-alexInitUserState :: AlexUserState
-alexInitUserState = AlexUserState []
-
-nestedComment :: Lexer
-nestedComment _ _ = undefined
-
-lexStream :: Alex [Located CoreToken]
-lexStream = do
-    l <- alexMonadScan
-    case l of
-        Located _ _ _ TokenEOF  -> pure [l]
-        _                       -> (l:) <$> lexStream
-
--- | The main lexer driver.
-lexCore :: String -> RLPC ParseError [Located CoreToken]
-lexCore s = case m of
-    Left e   -> addFatal err
-        where err = SrcError
-                { _errSpan       = (0,0,0) -- TODO: location
-                , _errSeverity   = Error
-                , _errDiagnostic = ParErrLexical e
-                }
-    Right ts -> pure ts
-    where
-        m = runAlex s (alexSetStartCode initial *> lexStream)
-
--- | @lexCore@, but the tokens are stripped of location info. Useful for
--- debugging
-lexCore' :: String -> RLPC ParseError [CoreToken]
-lexCore' s = fmap f <$> lexCore s
-    where f (Located _ _ _ t) = t
-
-data ParseError = ParErrLexical String
-                | ParErrParse
-                deriving Show
-
-lexWith :: (String -> CoreToken) -> Lexer
-lexWith f (AlexPn _ y x,_,_,s) l = pure $ Located y x l (f $ take l s)
-
-lexToken :: Alex (Located CoreToken)
-lexToken = alexMonadScan
-
-getSrcCol :: Alex Int
-getSrcCol = Alex $ \ st ->
-    let AlexPn _ _ col = alex_pos st
-    in Right (st, col)
-
-lbrace :: Lexer
-lbrace (AlexPn _ y x,_,_,_) l = do
-    pushContext NoLayout
-    pure $ Located y x l TokenLBrace
-
-rbrace :: Lexer
-rbrace (AlexPn _ y x,_,_,_) l = do
-    popContext
-    pure $ Located y x l TokenRBrace
-
-insRBraceV :: AlexPosn -> Alex (Located CoreToken)
-insRBraceV (AlexPn _ y x) = do
-    popContext
-    pure $ Located y x 0 TokenRBraceV
-
-insSemi  :: AlexPosn -> Alex (Located CoreToken)
-insSemi (AlexPn _ y x) = do
-    pure $ Located y x 0 TokenSemicolon
-
-modifyUst :: (AlexUserState -> AlexUserState) -> Alex ()
-modifyUst f = do
-    st <- alexGetUserState
-    alexSetUserState $ f st
-
-getUst :: Alex AlexUserState
-getUst = alexGetUserState
-
-newLayoutContext :: Lexer
-newLayoutContext (p,_,_,_) _ = do
-    undefined
-
-noBrace :: Lexer
-noBrace (AlexPn _ y x,_,_,_) l = do
-    col <- getSrcCol
-    pushContext (Layout col)
-    pure $ Located y x l TokenLBraceV
-
-getOffside :: Alex Ordering
-getOffside = do
-    ctx <- getContext
-    m <- getSrcCol
-    case ctx of
-        Layout n : _ -> pure $ m `compare` n
-        _            -> pure GT
-
-doBol :: Lexer
-doBol (p,c,_,s) _ = do
-    off <- getOffside
-    case off of
-        LT      -> insRBraceV p
-        EQ      -> insSemi p
-        _       -> lexToken
-
-letin :: Lexer
-letin (AlexPn _ y x,_,_,_) l = do
-    popContext
-    pure $ Located y x l TokenIn
-
-topLevelOff :: Lexer
-topLevelOff = noBrace
-
-alexEOF :: Alex (Located CoreToken)
-alexEOF = Alex $ \ st@(AlexState { alex_pos = AlexPn _ y x }) ->
-    Right (st, Located y x 0 TokenEOF)
-
-}

src/Core/Parse.y

@@ -5,24 +5,24 @@ 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
 
 import Control.Monad        ((>=>))
+import Control.Monad.Utils  (generalise)
 import Data.Foldable        (foldl')
 import Data.Functor.Identity
 import Core.Syntax
 import Core.Lex
 import Compiler.RLPC
 import Control.Monad
-import Lens.Micro
+import Control.Lens         hiding (snoc)
 import Data.Default.Class   (def)
 import Data.Hashable        (Hashable)
 import Data.List.Extra
@@ -30,65 +30,63 @@ 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 }
-      pack            { Located _ _ _ TokenPack } -- temp
-      in              { Located _ _ _ TokenIn }
-      litint          { Located _ _ _ (TokenLitInt $$) }
-      varname         { Located _ _ _ (TokenVarName $$) }
-      varsym          { Located _ _ _ (TokenVarSym $$) }
-      conname         { Located _ _ _ (TokenConName $$) }
-      consym          { Located _ _ _ (TokenConSym $$) }
-      alttag          { Located _ _ _ (TokenAltTag $$) }
-      word            { Located _ _ _ (TokenWord $$) }
-      'λ'             { Located _ _ _ TokenLambda }
-      '->'            { Located _ _ _ TokenArrow }
-      '='             { Located _ _ _ TokenEquals }
-      '@'             { Located _ _ _ TokenTypeApp }
-      '('             { Located _ _ _ TokenLParen }
-      ')'             { Located _ _ _ TokenRParen }
-      '{'             { Located _ _ _ TokenLBrace }
-      '}'             { Located _ _ _ TokenRBrace }
-      '{-#'           { Located _ _ _ TokenLPragma }
-      '#-}'           { Located _ _ _ TokenRPragma }
-      ';'             { Located _ _ _ TokenSemicolon }
-      '::'            { Located _ _ _ TokenHasType }
-      eof             { Located _ _ _ TokenEOF }
+      let             { Located _ TokenLet }
+      letrec          { Located _ TokenLetrec }
+      where           { Located _ TokenWhere }
+      case            { Located _ TokenCase }
+      of              { Located _ TokenOf }
+      pack            { Located _ TokenPack } -- temp
+      in              { Located _ TokenIn }
+      litint          { Located _ (TokenLitInt $$) }
+      varname         { Located _ (TokenVarName $$) }
+      varsym          { Located _ (TokenVarSym $$) }
+      conname         { Located _ (TokenConName $$) }
+      consym          { Located _ (TokenConSym $$) }
+      alttag          { Located _ (TokenAltTag $$) }
+      word            { Located _ (TokenWord $$) }
+      'λ'             { Located _ TokenLambda }
+      '->'            { Located _ TokenArrow }
+      '='             { Located _ TokenEquals }
+      '@'             { Located _ TokenTypeApp }
+      '('             { Located _ TokenLParen }
+      ')'             { Located _ TokenRParen }
+      '{'             { Located _ TokenLBrace }
+      '}'             { Located _ TokenRBrace }
+      '{-#'           { Located _ TokenLPragma }
+      '#-}'           { Located _ TokenRPragma }
+      ';'             { Located _ TokenSemicolon }
+      ':'             { 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         : ScTypeSig ';' Program         { insTypeSig $1 $3 }
-                | ScTypeSig OptSemi             { singletonTypeSig $1 }
-                | ScDef     ';' Program         { insScDef $1 $3 }
-                | ScDef     OptSemi             { singletonScDef $1 }
-                | TLPragma  Program             {% doTLPragma $1 $2 }
-                | TLPragma                      {% doTLPragma $1 mempty }
+Program         :: { Program Var }
+                : TypedScDef ';' Program    { $3 & insTypeSig (fst $1)
+                                                 & insScDef (snd $1) }
+                | TypedScDef OptSemi        { mempty & insTypeSig (fst $1)
+                                                     & insScDef (snd $1) }
+                | TLPragma Program          {% doTLPragma $1 $2 }
+                | TLPragma                  {% doTLPragma $1 mempty }
 
 TLPragma        :: { Pragma }
                 : '{-#' Words '#-}'             { Pragma $2 }
@@ -102,140 +100,152 @@ OptSemi         : ';'                           { () }
                 | {- epsilon -}                 { () }
 
 ScTypeSig       :: { (Name, Type) }
-ScTypeSig       : Var '::' Type                 { ($1,$3) }
+ScTypeSig       : Id ':' Type                   { ($1, $3) }
 
-ScDefs          :: { [ScDef Name] }
-ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
-                | ScDef ';'                     { [$1] }
-                | ScDef                         { [$1] }
+TypedScDef      :: { (Var, ScDef Var) }
+                : Id ':' Type ';' Id ParList '=' Expr
+                            { (MkVar $1 $3, mkTypedScDef $1 $3 $5 $6 $8) }
 
-ScDef           :: { ScDef Name }
-ScDef           : Var ParList '=' Expr          { ScDef $1 $2 $4 }
-                -- hack to allow constructors to be compiled into scs
-                | Con ParList '=' Expr          { ScDef $1 $2 $4 }
+-- ScDefs          :: { [ScDef PsName] }
+-- ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
+--                 | ScDef ';'                     { [$1] }
+--                 | 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         : Var ParList                   { $1 : $2 }
-                | {- epsilon -}                 { [] }
+ParList      :: { [Name] }
+ParList      : varname ParList            { $1 : $2 }
+             | {- 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     : Expr1 AppArgs                { foldl' App $1 $2 }
+Application     :: { Expr Var }
+Application     : Application AppArg           { App $1 $2 }
+                | Expr1       AppArg           { App $1 $2 }
 
-AppArgs         :: { [Expr Name] }
-AppArgs         : Expr1 AppArgs                 { $1 : $2 }
-                | Expr1                         { [$1] }
+AppArg          :: { Expr Var }
+                : '@' Type1                     { Type $2 }
+                | 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           : alttag ParList '->' Expr      { Alter (AltTag  $1) $2 $4 }
-                | Con    ParList '->' Expr      { Alter (AltData $1) $2 $4 }
+Alter           :: { Alter Var }
+Alter           : alttag  AltParList '->' Expr     { Alter (AltTag  $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 }
-                | Con                                { $1 }
-
-Var             :: { Name }
-Var             : '(' varsym ')'                    { $2 }
-                | varname                           { $1 }
-
-Con             :: { Name }
-Con             : '(' consym ')'                    { $2 }
+                : varname                           { $1 }
                 | conname                           { $1 }
 
+Var             :: { Var }
+Var             : '(' varname ':' Type ')'          { MkVar $2 $4 }
+
 {
 
-parseError :: [Located CoreToken] -> RLPC a
-parseError (Located y x l t : _) =
-    error $ show y <> ":" <> show x
+parseError :: [Located CoreToken] -> P a
+parseError (Located _ t : _) =
+    error $ "<line>" <> ":" <> "<col>"
          <> ": parse error at token `" <> show t <> "'"
 
-{-# WARNING parseError "unimpl" #-}
-
-exprPragma :: [String] -> RLPC (Expr Name)
+exprPragma :: [String] -> RLPC (Expr Var)
 exprPragma ("AST" : e) = undefined
 exprPragma _           = undefined
 
-{-# WARNING exprPragma "unimpl" #-}
-
-astPragma :: [String] -> RLPC (Expr Name)
+astPragma :: [String] -> RLPC (Expr Var)
 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 ts = programTypeSigs %~ uncurry H.insert ts
+insTypeSig :: Var -> Program Var -> Program Var
+insTypeSig w@(MkVar _ t) = programTypeSigs %~ H.insert w t
 
-singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
-singletonTypeSig ts = insTypeSig ts mempty
+-- singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
+-- 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 sc = insScDef sc mempty
+-- singletonScDef :: (Hashable b) => ScDef b -> Program b
+-- singletonScDef sc = insScDef sc mempty
 
-parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m Program'
-parseCoreProgR = ddumpast <=< (hoistRlpcT generalise . parseCoreProg)
-    where
-        generalise :: forall a. Identity a -> m a
-        generalise (Identity a) = pure a
+parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m (Expr Var)
+parseCoreExprR = liftMaybe . snd . flip runP def . parseCoreExpr
 
-        ddumpast :: Program' -> RLPCT m Program'
-        ddumpast p = do
-            addDebugMsg "dump-ast" . show $ p
-            pure p
+parseCoreProgR :: forall m. (Monad m)
+               => [Located CoreToken] -> RLPCT m (Program Var)
+parseCoreProgR s = do
+    let p = runP (parseCoreProg s) def
+    case p of
+        (st, Just a) -> do
+            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
@@ -243,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.y.old

@@ -1,159 +0,0 @@
-{
-module Core.Parse
-    ( parseCore
-    , parseCoreExpr
-    , parseCoreProg
-    , module Core.Lex -- temp convenience
-    , parseTmp
-    , SrcError
-    , ParseError
-    , Module
-    )
-    where
-
-import Control.Monad        ((>=>))
-import Data.Foldable        (foldl')
-import Core.Syntax
-import Core.Lex
-import Compiler.RLPC
-import Data.Default.Class   (def)
-}
-
-%name parseCore Module
-%name parseCoreExpr StandaloneExpr
-%name parseCoreProg StandaloneProgram
-%tokentype { Located CoreToken }
-%error { parseError }
-%monad { RLPC ParseError }
-
-%token
-      let             { Located _ _ _ TokenLet }
-      letrec          { Located _ _ _ TokenLetrec }
-      module          { Located _ _ _ TokenModule }
-      where           { Located _ _ _ TokenWhere }
-      ','             { Located _ _ _ TokenComma }
-      in              { Located _ _ _ TokenIn }
-      litint          { Located _ _ _ (TokenLitInt $$) }
-      varname         { Located _ _ _ (TokenVarName $$) }
-      varsym          { Located _ _ _ (TokenVarSym $$) }
-      conname         { Located _ _ _ (TokenConName $$) }
-      consym          { Located _ _ _ (TokenConSym $$) }
-      'λ'             { Located _ _ _ TokenLambda }
-      '->'            { Located _ _ _ TokenArrow }
-      '='             { Located _ _ _ TokenEquals }
-      '('             { Located _ _ _ TokenLParen }
-      ')'             { Located _ _ _ TokenRParen }
-      '{'             { Located _ _ _ TokenLBrace }
-      '}'             { Located _ _ _ TokenRBrace }
-      vl              { Located _ _ _ TokenLBraceV }
-      vr              { Located _ _ _ TokenRBraceV }
-      ';'             { Located _ _ _ TokenSemicolon }
-      eof             { Located _ _ _ TokenEOF }
-
-%%
-
-Module          :: { Module }
-Module          : module conname where Program Eof { Module (Just ($2, [])) $4 }
-                | Program Eof                      { Module Nothing $1 }
-
-Eof             :: { () }
-Eof             : eof           { () }
-                | error         { () }
-
-StandaloneProgram :: { Program }
-StandaloneProgram : Program eof                 { $1 }
-
-Program         :: { Program }
-Program         : VOpen ScDefs VClose           { Program $2 }
-                | '{'   ScDefs '}'              { Program $2 }
-
-VOpen           :: { () }
-VOpen           : vl                            { () }
-
-VClose          :: { () }
-VClose          : vr                            { () }
-                | error                         { () }
-
-ScDefs          :: { [ScDef] }
-ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
-                | {- epsilon -}                 { [] }
-
-ScDef           :: { ScDef }
-ScDef           : Var ParList '=' Expr          { ScDef $1 $2 $4 }
-
-ParList         :: { [Name] }
-ParList         : Var ParList                   { $1 : $2 }
-                | {- epsilon -}                 { [] }
-
-StandaloneExpr  :: { Expr }
-StandaloneExpr  : Expr eof                      { $1 }
-
-Expr            :: { Expr }
-Expr            : LetExpr                       { $1 }
-                | 'λ' Binders '->' Expr         { Lam $2 $4 }
-                | Application                   { $1 }
-                | Expr1                         { $1 }
-
-LetExpr         :: { Expr }
-LetExpr         : let    VOpen Bindings VClose in Expr { Let NonRec $3 $6 }
-                | letrec VOpen Bindings VClose in Expr { Let Rec $3 $6 }
-                | let    '{'   Bindings '}'    in Expr { Let NonRec $3 $6 }
-                | letrec '{'   Bindings '}'    in Expr { Let Rec $3 $6 }
-
-Binders         :: { [Name] }
-Binders         : Var Binders                  { $1 : $2 }
-                | Var                          { [$1] }
-
-Application     :: { Expr }
-Application     : Expr1 AppArgs                 { foldl' App $1 $2 }
-
--- TODO: Application can probably be written as a single rule, without AppArgs
-AppArgs         :: { [Expr] }
-AppArgs         : Expr1 AppArgs                 { $1 : $2 }
-                | Expr1                         { [$1] }
-
-Expr1           :: { Expr }
-Expr1           : litint                        { IntE $1 }
-                | Id                            { Var $1 }
-                | '(' Expr ')'                  { $2 }
-
-Bindings        :: { [Binding] }
-Bindings        : Binding ';' Bindings          { $1 : $3 }
-                | Binding ';'                   { [$1] }
-                | Binding                       { [$1] }
-
-Binding         :: { Binding }
-Binding         : Var '=' Expr                  { $1 := $3 }
-
-Id              :: { Name }
-Id              : Var                                { $1 }
-                | Con                                { $1 }
-
-Var             :: { Name }
-Var             : '(' varsym ')'                    { $2 }
-                | varname                           { $1 }
-
-Con             :: { Name }
-Con             : '(' consym ')'                    { $2 }
-                | conname                           { $1 }
-
-{
-parseError :: [Located CoreToken] -> RLPC ParseError a
-parseError (Located y x l _ : _) = addFatal err
-    where err = SrcError
-            { _errSpan       = (y,x,l)
-            , _errSeverity   = Error
-            , _errDiagnostic = ParErrParse
-            }
-
-parseTmp :: IO Module
-parseTmp = do
-    s <- readFile "/tmp/t.hs"
-    case parse s of
-        Left e -> error (show e)
-        Right (ts,_) -> pure ts
-    where
-        parse = evalRLPC def . (lexCore >=> parseCore)
-
-}
-

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

@@ -5,42 +5,41 @@ Description : Core ASTs and the like
 {-# LANGUAGE PatternSynonyms, OverloadedStrings #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE DerivingStrategies, DerivingVia #-}
 -- for recursion-schemes
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable
-  , TemplateHaskell, TypeFamilies #-}
+{-# LANGUAGE DeriveTraversable, TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 module Core.Syntax
-    ( Expr(..)
-    , ExprF(..)
-    , ExprF'(..)
-    , Type(..)
-    , pattern TyInt
-    , Lit(..)
-    , pattern (:$)
-    , pattern (:@)
-    , pattern (:->)
-    , Binding(..)
-    , AltCon(..)
-    , pattern (:=)
-    , Rec(..)
-    , Alter(..)
-    , Name
-    , Tag
-    , ScDef(..)
-    , Module(..)
-    , Program(..)
-    , Program'
+    (
+    -- * Core AST
+      ExprF(..), ExprF'
+    , ScDef(..), ScDef'
+    , Program(..), Program'
+    , Type(..), Kind, pattern (:->), pattern TyInt
+    , AlterF(..), Alter(..), Alter', AltCon(..)
+    , pattern Binding, pattern Alter
+    , Rec(..), Lit(..)
     , Pragma(..)
-    , unliftScDef
-    , programScDefs
-    , programTypeSigs
-    , programDataTags
-    , Expr'
-    , ScDef'
-    , Alter'
-    , Binding'
-    , HasRHS(_rhs)
-    , HasLHS(_lhs)
+    -- ** Variables and identifiers
+    , Name, Var(..), Tag, pattern (:^)
+    , Binding, BindingF(..), pattern (:=), pattern (:$)
+    , type Binding'
+    -- ** Working with the fixed point of ExprF
+    , Expr, Expr'
+    , pattern Con, pattern Var, pattern App, pattern Lam, pattern Let
+    , pattern Case, pattern Type, pattern Lit
+
+    -- * Pretty-printing
+    , Pretty(pretty), WithTerseBinds(..)
+
+    -- * Optics
+    , HasArrowSyntax(..)
+    , programScDefs, programTypeSigs, programDataTags, programTyCons
+    , formalising, lambdaLifting
+    , HasRHS(_rhs), HasLHS(_lhs)
+    , _BindingF, _MkVar, _ScDef
+    -- ** Classy optics
+    , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
     )
     where
 ----------------------------------------------------------------------------------
@@ -48,163 +47,736 @@ 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 GHC.Generics
+import Data.These
+import GHC.Generics                 (Generic, Generic1, Generically(..))
+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 Lens.Micro.TH                (makeLenses)
-import Lens.Micro
+import Misc
+import Misc.Lift1
+import Control.Lens
 ----------------------------------------------------------------------------------
 
-data Expr b = Var Name
-            | Con Tag Int -- ^ Con Tag Arity
-            | Case (Expr b) [Alter b]
-            | Lam [b] (Expr b)
-            | Let Rec [Binding b] (Expr b)
-            | App (Expr b) (Expr b)
-            | Lit Lit
-            deriving (Show, Read, Lift)
+data ExprF b a = VarF Name
+               | ConF Tag Int -- ^ Con Tag Arity
+               | CaseF a [AlterF b a]
+               | LamF [b] a
+               | LetF Rec [BindingF b a] a
+               | AppF a a
+               | LitF Lit
+               | 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)
+
+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 :$
-pattern (:$) :: Expr b -> Expr b -> Expr b 
-pattern f :$ x = App f x
+class HasArrowSyntax s a b | s -> a b where
+    _arrowSyntax :: Prism' s (a, b)
 
-infixl 2 :@
-pattern (:@) :: Type -> Type -> Type
-pattern f :@ x = TyApp f x
+instance HasArrowSyntax Type Type Type where
+    _arrowSyntax = prism make unmake where
+        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 a :-> b = TyApp (TyApp TyFun a) b
+pattern (:->) :: HasArrowSyntax s 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 #-}
-{-# COMPLETE (:=) :: Binding #-}
-data Binding b = Binding b (Expr b)
-    deriving (Show, Read, Lift)
+data BindingF b a = BindingF b (ExprF b a)
+    deriving (Functor, Foldable, Traversable)
 
-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)
-    deriving (Show, Read, Lift)
+infixl 2 :$
+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
-            | Default
-            deriving (Show, Read, Eq, Lift)
+            | AltDefault
+            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 _ as e) = Lam as e
+-- unliftScDef :: ScDef b -> Expr b
+-- 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
-    -- map constructors to their tag and arity
-    , _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.
+programTypeSigsP :: (Hashable b) => Prism' (Program b) (HashMap b Type)
+programTypeSigsP = prism
+    (\b -> mempty & programTypeSigs .~ b)
+    (Right . view programTypeSigs)
+
 type ExprF' = ExprF Name
 
 type Program' = Program Name
 type Expr' = Expr Name
 type ScDef' = ScDef Name
-type Alter' = Alter Name
-type Binding' = Binding Name
+-- type Alter' = Alter Name
+-- type Binding' = Binding Name
 
-instance IsString (Expr b) where
-    fromString = Var . fromString
+-- instance IsString (Expr b) where
+--     fromString = Var . fromString
 
-instance IsString Type where
-    fromString "" = error "IsString Type string may not be empty"
-    fromString s
-        | isUpper c     = TyCon . fromString $ s
-        | otherwise     = TyVar . fromString $ s
-        where (c:_) = s
+lambdaLifting :: Iso (ScDef b) (ScDef b') (b, Expr b) (b', Expr b')
+lambdaLifting = iso sa bt where
+    sa (ScDef n as e) = (n, e') where
+        e' = Lam as e
+
+    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)
-        (\ (Alter t as _) e' -> Alter t as e')
+        (\ (AlterF _ _ e) -> 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
-    _rhs = lens
-        (\ (_ := e) -> e)
-        (\ (k := _) e' -> k := e')
+instance HasRHS (BindingF b a) (BindingF b' a') (ExprF b a) (ExprF b' a')
 
 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
-    _lhs = lens
-        (\ (k := _) -> k)
-        (\ (_ := e) k' -> k' := e)
+-- instance HasLHS (Binding b) (Binding b) b b where
+    -- _lhs = lens
+    --     (\ (k := _) -> k)
+    --     (\ (_ := 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
+
+--------------------------------------------------------------------------------
+
+newtype WithTerseBinds a = WithTerseBinds a
+
+class MakeTerse a where
+    type AsTerse a :: Data.Kind.Type
+    asTerse :: a -> AsTerse a
+
+instance MakeTerse Var where
+    type AsTerse Var = Name
+    asTerse (MkVar n _) = n
+
+instance (Hashable b, Pretty b, Pretty (AsTerse b), MakeTerse b)
+      => Pretty (WithTerseBinds (Program b)) where
+    pretty (WithTerseBinds p)
+            = (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
+                `u` foldMapOf programScDefs thatSc p
+              where u = H.unionWith unionThese
+
+            thisTs = ifoldMap @b @(HashMap b)
+                (\n t -> H.singleton n (This (n,t)))
+            thatSc = foldMap $ \sc ->
+                H.singleton (sc ^. _lhs . _1) (That sc)
+
+            prettyGroup :: These (b, Type) (ScDef b) -> Doc
+            prettyGroup = bifoldr vs vs mempty
+                        . bimap (uncurry prettyTySig')
+                                (pretty . WithTerseBinds)
+                where vs = vsepTerm ";"
+
+            cataDataTag n (t,a) acc = prettyDataTag n t a $+$ acc
+
+instance (Hashable b, Pretty b) => Pretty (Program b) where
+    pretty p = (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
+                `u` foldMapOf programScDefs thatSc p
+              where u = H.unionWith unionThese
+
+            thisTs = ifoldMap @b @(HashMap b)
+                (\n t -> H.singleton n (This (n,t)))
+            thatSc = foldMap $ \sc ->
+                H.singleton (sc ^. _lhs . _1) (That sc)
+
+            prettyGroup :: These (b, Type) (ScDef b) -> Doc
+            prettyGroup = bifoldr vs vs mempty
+                        . bimap (uncurry prettyTySig) pretty
+                where vs = vsepTerm ";"
+
+            cataDataTag n (t,a) acc = prettyDataTag n t a $+$ acc
+
+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 :: (Pretty n, Pretty t, Pretty a)
+              => n -> t -> a -> Doc
+prettyDataTag n t a =
+    hsep ["{-#", "PackData", ttext n, ttext t, ttext a, "#-}"]
+
+prettyTySig :: (Pretty n, Pretty t) => n -> t -> Doc
+prettyTySig n t = hsep [ttext n, ":", pretty t]
+
+prettyTySig' :: (MakeTerse n, Pretty (AsTerse n), Pretty t) => n -> t -> Doc
+prettyTySig' n t = hsep [ttext (asTerse n), ":", pretty t]
+
+-- Pretty Type
+-- TyApp | appPrec   | left
+-- (:->) | appPrec-1 | right
+
+instance Pretty Type where
+    prettyPrec _ (TyVar n)   = ttext n
+    prettyPrec _ TyFun       = "(->)"
+    prettyPrec _ (TyCon n)   = ttext n
+    prettyPrec p (a :-> b)   = maybeParens (p>appPrec-1) $
+        hsep [prettyPrec appPrec a, "->", prettyPrec (appPrec-1) b]
+    prettyPrec p (TyApp f x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    prettyPrec p (TyForall a m) = maybeParens (p>appPrec-2) $
+        "∀" <+> (prettyPrec appPrec1 a <> ".") <+> pretty m
+    prettyPrec _ TyKindType = "Type"
+
+instance (Pretty b, Pretty (AsTerse b), MakeTerse b)
+      => Pretty (WithTerseBinds (ScDef b)) where
+    pretty (WithTerseBinds sc) = hsep [name, as, "=", hang empty 1 e]
+        where
+            name = ttext $ sc ^. _lhs . _1 . to asTerse
+            as = sc & hsepOf (_lhs . _2 . each . to asTerse . to ttext)
+            e = pretty $ sc ^. _rhs
+
+instance (Pretty b) => Pretty (ScDef b) where
+    pretty sc = hsep [name, as, "=", hang empty 1 e]
+        where
+            name = ttext $ sc ^. _lhs . _1
+            as = sc & hsepOf (_lhs . _2 . each . to ttext)
+            e = pretty $ sc ^. _rhs
+
+-- Pretty Expr
+-- LamF | appPrec1 | right
+-- AppF | appPrec  | left
+
+instance (Pretty b, Pretty a) => Pretty (ExprF b a) where
+    prettyPrec = prettyPrec1
+
+    -- prettyPrec _ (VarF n) = ttext n
+    -- prettyPrec _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
+    -- prettyPrec p (LamF bs e) = maybeParens (p>0) $
+    --     hsep ["λ", hsep (prettyPrec appPrec1 <$> bs), "->", pretty e]
+    -- prettyPrec p (LetF r bs e) = maybeParens (p>0)
+    --                            $ hsep [pretty r, explicitLayout bs]
+    --                          $+$ hsep ["in", pretty e]
+    -- prettyPrec p (AppF f x) = maybeParens (p>appPrec) $
+    --     prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    -- prettyPrec p (LitF l) = prettyPrec p l
+    -- prettyPrec p (CaseF e as) = maybeParens (p>0) $
+    --     "case" <+> pretty e <+> "of"
+    --     $+$ nest 2 (explicitLayout as)
+    -- prettyPrec p (TypeF t) = "@" <> prettyPrec appPrec1 t
+
+instance (Pretty b) => Pretty1 (ExprF b) where
+    liftPrettyPrec pr _ (VarF n) = ttext n
+    liftPrettyPrec pr _ (ConF t a) = "Pack{" <> (ttext t <+> ttext a) <> "}"
+    liftPrettyPrec pr p (LamF bs e) = maybeParens (p>0) $
+        hsep ["λ", hsep (prettyPrec appPrec1 <$> bs), "->", pr 0 e]
+    liftPrettyPrec pr p (LetF r bs e) = maybeParens (p>0)
+                               $ hsep [pretty r, bs']
+                             $+$ hsep ["in", pr 0 e]
+        where bs' = liftExplicitLayout (liftPrettyPrec pr 0) bs
+    liftPrettyPrec pr p (AppF f x) = maybeParens (p>appPrec) $
+        pr appPrec f <+> pr appPrec1 x
+    liftPrettyPrec pr p (LitF l) = prettyPrec p l
+    liftPrettyPrec pr p (CaseF e as) = maybeParens (p>0) $
+            "case" <+> pr 0 e <+> "of"
+            $+$ nest 2 as'
+        where as' = liftExplicitLayout (liftPrettyPrec pr 0) as
+    liftPrettyPrec pr p (TypeF t) = "@" <> prettyPrec appPrec1 t
+
+instance Pretty Rec where
+    pretty Rec = "letrec"
+    pretty NonRec = "let"
+
+instance (Pretty b, Pretty a) => Pretty (AlterF b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (AlterF b) where
+    liftPrettyPrec pr _ (AlterF c as e) =
+        hsep [pretty c, hsep (pretty <$> as), "->", liftPrettyPrec pr 0 e]
+
+instance Pretty AltCon where
+    pretty (AltData n) = ttext n
+    pretty (AltLit l) = pretty l
+    pretty (AltTag t) = "<" <> ttext t <> ">"
+    pretty AltDefault = "_"
+
+instance Pretty Lit where
+    pretty (IntL n) = ttext n
+
+instance (Pretty b, Pretty a) => Pretty (BindingF b a) where
+    prettyPrec = prettyPrec1
+
+instance Pretty b => Pretty1 (BindingF b) where
+    liftPrettyPrec pr _ (BindingF k v) = hsep [pretty k, "=", liftPrettyPrec pr 0 v]
+
+liftExplicitLayout :: (a -> Doc) -> [a] -> Doc
+liftExplicitLayout pr as = vcat inner <+> "}" where
+    inner = zipWith (<+>) delims (pr <$> as)
+    delims = "{" : repeat ";"
+
+explicitLayout :: (Pretty a) => [a] -> Doc
+explicitLayout as = vcat inner <+> "}" where
+    inner = zipWith (<+>) delims (pretty <$> as)
+    delims = "{" : repeat ";"
+
+instance Pretty Var where
+    prettyPrec p (MkVar n t) = maybeParens (p>0) $
+        hsep [pretty n, ":", pretty 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)
 

src/Core/SystemF.hs

@@ -0,0 +1,268 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE OverloadedLists #-}
+module Core.SystemF
+    ( lintCoreProgR
+    )
+    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
+
+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 = undefined
+
+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'"
+                                   (pretty k) (pretty k')
+                 ]
+        SystemFErrorCouldNotMatch t t' ->
+            Text [ T.pack $ printf "Could not match type `%s' with `%s'"
+                                   (pretty t) (pretty t')
+                 ]
+
+justLintCoreExpr = fmap (fmap (prettyPrec 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,7 +5,8 @@ Description : Core quasiquoters
 module Core.TH
     ( coreExpr
     , coreProg
-    , coreProgT
+    -- , coreExprT
+    -- , coreProgT
     )
     where
 ----------------------------------------------------------------------------------
@@ -22,20 +23,30 @@ import Data.Text                    qualified as T
 import Core.Parse
 import Core.Lex
 import Core.Syntax
-import Core.HindleyMilner           (checkCoreProgR)
+import Core.HindleyMilner           (checkCoreProgR, checkCoreExprR)
 ----------------------------------------------------------------------------------
 
 coreProg :: QuasiQuoter
 coreProg = mkqq $ lexCoreR >=> parseCoreProgR
 
 coreExpr :: QuasiQuoter
-coreExpr = mkqq $ lexCoreR >=> parseCoreExpr
+coreExpr = mkqq $ lexCoreR >=> parseCoreExprR
 
 -- | Type-checked @coreProg@
-coreProgT :: QuasiQuoter
-coreProgT = mkqq $ lexCoreR >=> parseCoreProgR >=> checkCoreProgR
+-- coreProgT :: QuasiQuoter
+-- coreProgT = mkqq $ lexCoreR >=> parseCoreProgR >=> checkCoreProgR
 
-mkqq :: (Lift a) => (Text -> RLPC a) -> QuasiQuoter
+-- coreExprT :: QuasiQuoter
+-- coreExprT = mkqq $ lexCoreR >=> parseCoreExprR >=> checkCoreExprR g
+--     where
+--         g = [ ("+#", TyInt :-> TyInt :-> TyInt)
+--             , ("id", TyForall (MkVar "a" TyKindType) $
+--                     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
     { quoteExp = mkq p
     , quotePat = error "core quasiquotes may only be used in expressions"
@@ -43,8 +54,6 @@ mkqq p = QuasiQuoter
     , quoteDec = error "core quasiquotes may only be used in expressions"
     }
 
-mkq :: (Lift a) => (Text -> RLPC a) -> String -> Q Exp
-mkq parse s = case evalRLPC def (parse $ T.pack s) of
-    (Just a,  _) -> lift a
-    (Nothing, _) -> error "todo: aaahhbbhjhbdjhabsjh"
+mkq :: (Lift a) => (Text -> RLPCIO a) -> String -> Q Exp
+mkq parse s = liftIO $ evalRLPCIO def (parse $ T.pack s) >>= lift
 

src/Core/Utils.hs

@@ -2,8 +2,6 @@ module Core.Utils
     ( programRhss
     , programGlobals
     , isAtomic
-    -- , insertModule
-    , extractProgram
     , freeVariables
     )
     where
@@ -13,7 +11,7 @@ import Data.Functor.Foldable
 import Data.Set                     (Set)
 import Data.Set                     qualified as S
 import Core.Syntax
-import Lens.Micro
+import Control.Lens
 import GHC.Exts                     (IsList(..))
 ----------------------------------------------------------------------------------
 
@@ -30,34 +28,29 @@ isAtomic _        = False
 
 ----------------------------------------------------------------------------------
 
--- TODO: export list awareness
--- insertModule :: Module b -> Program b -> Program b
--- insertModule (Module _ p) = programScDefs %~ (<>m)
+freeVariables :: Expr b -> Set b
+freeVariables = undefined
 
-extractProgram :: Module b -> Program b
-extractProgram (Module _ p) = p
+-- freeVariables :: Expr' -> Set Name
+-- 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
 
-----------------------------------------------------------------------------------
-
-freeVariables :: Expr' -> Set Name
-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
-                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
+--         go (CaseF e as)     = e `S.union` asFree
+--             where
+--                 -- asFree = foldMap id $ freeVariables <$> (fmap altToLam as)
+--                 asFree = foldMap (freeVariables . 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

@@ -1,5 +1,4 @@
 {-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE LambdaCase #-}
 module Core2Core
     ( core2core
     , gmPrep
@@ -15,27 +14,53 @@ import Data.Maybe               (fromJust)
 import Data.Set                 (Set)
 import Data.Set                 qualified as S
 import Data.List
+import Data.Foldable
 import Control.Monad.Writer
 import Control.Monad.State.Lazy
 import Control.Arrow            ((>>>))
 import Data.Text                qualified as T
 import Data.HashMap.Strict      (HashMap)
 import Numeric                  (showHex)
-import Lens.Micro.Platform
+
+import Data.Pretty
+import Compiler.RLPC
+import Control.Lens
 import Core.Syntax
 import Core.Utils
 ----------------------------------------------------------------------------------
 
+-- | General optimisations
+
 core2core :: Program' -> Program'
 core2core p = undefined
 
+gmPrepR :: (Monad m) => Program' -> RLPCT m Program'
+gmPrepR p = do
+    let p' = gmPrep p
+    addDebugMsg "dump-gm-preprocessed" $ render . pretty $ p'
+    pure p'
+
+-- | G-machine-specific preprocessing.
+
 gmPrep :: Program' -> Program'
 gmPrep p = p & appFloater (floatNonStrictCases globals)
              & tagData
+             & defineData
     where
         globals = p ^.. programScDefs . each . _lhs . _1
                 & S.fromList
 
+-- | Define concrete supercombinators for all datatags defined via pragmas (or
+-- desugaring)
+
+defineData :: Program' -> Program'
+defineData p = p & programScDefs <>~ defs
+    where
+        defs = p ^. programDataTags
+             . to (ifoldMap (\k (t,a) -> [ScDef k [] (Con t a)]))
+
+-- | Substitute all pattern matches on named constructors for matches on tags
+
 tagData :: Program' -> Program'
 tagData p = let ?dt = p ^. programDataTags
             in p & programRhss %~ cata go where
@@ -44,7 +69,7 @@ tagData p = let ?dt = p ^. programDataTags
     go x                = embed x
 
     tagAlts :: (?dt :: HashMap Name (Tag, Int)) => Alter' -> Alter'
-    tagAlts (Alter (AltData c) bs e) = Alter (AltTag tag) bs e
+    tagAlts (Alter (AltData c) bs e) = Alter (AltTag tag) bs (cata go e)
         where tag = case ?dt ^. at c of
                 Just (t,_) -> t
                 -- TODO: errorful
@@ -59,6 +84,7 @@ appFloater fl p = p & traverseOf programRhss fl
                     & runFloater
                     & \ (me,floats) -> me & programScDefs %~ (<>floats)
 
+-- TODO: move NameSupply from Rlp2Core into a common module to share here
 runFloater :: Floater a -> (a, [ScDef'])
 runFloater = flip evalStateT ns >>> runWriter
     where
@@ -88,23 +114,23 @@ floatNonStrictCases g = goE
                 altBodies = (\(Alter _ _ b) -> b) <$> as
             tell [sc]
             goE e
-            traverse goE altBodies
+            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)
         goC (Var k)             = pure (Var k)
         goC (Con t as)          = pure (Con t as)
 
-        name = state (fromJust . uncons)
+        name = state (fromJust . Data.List.uncons)
 
         -- 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
-                    & traverse goC
-                    & const (pure bs)
+        travBs c bs = undefined
+        -- ^ ??? 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/Heap.hs

@@ -27,6 +27,7 @@ import Debug.Trace
 import Data.Map.Strict              qualified as M
 import Data.List                    (intersect)
 import GHC.Stack                    (HasCallStack)
+import Control.Lens
 ----------------------------------------------------------------------------------
 
 data Heap a = Heap [Addr] (Map Addr a)
@@ -34,6 +35,21 @@ data Heap a = Heap [Addr] (Map Addr a)
 
 type Addr = Int
 
+type instance Index (Heap a) = Addr
+type instance IxValue (Heap a) = a
+
+instance Ixed (Heap a) where
+    ix a k (Heap as m) = Heap as <$> M.alterF k' a m where
+        k' (Just v) = Just <$> k v
+        k' Nothing = pure Nothing
+
+instance At (Heap a) where
+    at ma k (Heap as m) = Heap as <$> M.alterF k ma m
+
+instance FoldableWithIndex Addr Heap where
+    ifoldr fi z (Heap _ m) = ifoldr fi z m
+    ifoldMap iam (Heap _ m) = ifoldMap iam m
+
 instance Semigroup (Heap a) where
     Heap ua ma <> Heap ub mb = Heap u m
         where
@@ -54,7 +70,7 @@ instance Foldable Heap where
     length (Heap _ m) = M.size m
 
 instance Traversable Heap where
-    traverse t (Heap u m) = Heap u <$> (traverse t m)
+    traverse t (Heap u m) = Heap u <$> traverse t m
 
 ----------------------------------------------------------------------------------
 

src/Data/Pretty.hs

@@ -1,80 +1,113 @@
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
 module Data.Pretty
-    ( Pretty(..)
-    , ISeq(..)
-    , precPretty
-    , prettyPrint
-    , prettyShow
-    , iShow
-    , iBracket
-    , withPrec
-    , bracketPrec
+    ( Pretty(..), Pretty1(..)
+    , prettyPrec1
+    , rpretty
+    , ttext
+    , Showing(..)
+    -- * Pretty-printing lens combinators
+    , hsepOf, vsepOf, vcatOf, vlinesOf, vsepTerm
+    , vsep
+    , module Text.PrettyPrint
+    , maybeParens
+    , appPrec
+    , appPrec1
     )
     where
 ----------------------------------------------------------------------------------
-import Data.String      (IsString(..))
+import Text.PrettyPrint             hiding ((<>))
+import Text.PrettyPrint.HughesPJ    hiding ((<>))
+import Text.Printf
+import Data.String                  (IsString(..))
+import Data.Text.Lens               hiding ((:<))
+import Data.Monoid                  hiding (Sum)
+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
-    pretty :: a -> ISeq
-    prettyPrec :: a -> Int -> ISeq
+    pretty :: a -> Doc
+    prettyPrec :: Int -> a -> Doc
 
     {-# MINIMAL pretty | prettyPrec #-}
-    pretty a = prettyPrec a 0
-    prettyPrec a _ = iBracket (pretty a)
+    pretty = prettyPrec 0
+    prettyPrec = const pretty
 
-precPretty :: (Pretty a) => Int -> a -> ISeq
-precPretty = flip prettyPrec
+rpretty :: (IsString s, Pretty a) => a -> s
+rpretty = fromString . render . pretty
 
-prettyPrint :: (Pretty a) => a -> IO ()
-prettyPrint = putStr . squash . pretty
+instance Pretty String where
+    pretty = Text.PrettyPrint.text
 
-prettyShow :: (Pretty a) => a -> String
-prettyShow = squash . pretty
+instance Pretty T.Text where
+    pretty = Text.PrettyPrint.text . view unpacked
 
-data ISeq where
-    INil :: ISeq
-    IStr :: String -> ISeq
-    IAppend :: ISeq -> ISeq -> ISeq
-    IIndent :: ISeq -> ISeq
-    IBreak :: ISeq
+newtype Showing a = Showing a
 
-instance IsString ISeq where
-    fromString = IStr
+instance (Show a) => Pretty (Showing a) where
+    prettyPrec p (Showing a) = fromString $ showsPrec p a ""
 
-instance Semigroup ISeq where
-    (<>) = IAppend
+deriving via Showing Int instance Pretty Int
 
-instance Monoid ISeq where
-    mempty = INil
+class (forall a. Pretty a => Pretty (f a)) => Pretty1 f where
+    liftPrettyPrec :: (Int -> a -> Doc) -> Int -> f a -> Doc
 
-squash :: ISeq -> String
-squash a = flatten 0 [(a,0)]
+prettyPrec1 :: (Pretty1 f, Pretty a) => Int -> f a -> Doc
+prettyPrec1 = liftPrettyPrec prettyPrec
 
-flatten :: Int -> [(ISeq, Int)] -> String
-flatten _ []                      = ""
-flatten c ((INil,        i) : ss) = flatten c ss
-flatten c ((IStr s,      i) : ss) = s ++ flatten (c + length s) ss
-flatten c ((IAppend r s, i) : ss) = flatten c ((r,i) : (s,i) : ss)
-flatten _ ((IBreak,      i) : ss) = '\n' : replicate i ' ' ++ flatten i ss
-flatten c ((IIndent s,   i) : ss) = flatten c ((s,c) : ss)
+instance (Pretty1 f, Pretty1 g, Pretty a) => Pretty (Sum f g a) where
+    prettyPrec p (InL fa) = prettyPrec1 p fa
+    prettyPrec p (InR ga) = prettyPrec1 p ga
 
-iBracket :: ISeq -> ISeq
-iBracket s = IStr "(" <> s <> IStr ")"
+instance (Pretty1 f, Pretty1 g) => Pretty1 (Sum f g) where
+    liftPrettyPrec pr p (InL fa) = liftPrettyPrec pr p fa
+    liftPrettyPrec pr p (InR ga) = liftPrettyPrec pr p ga
 
-withPrec :: Int -> ISeq -> Int -> ISeq
-withPrec n s p
-    | p > n     = iBracket s
-    | otherwise =          s
+instance (Pretty (f (Fix f))) => Pretty (Fix f) where
+    prettyPrec d (Fix f) = prettyPrec d f
 
-bracketPrec :: Int -> Int -> ISeq -> ISeq
-bracketPrec n p s = withPrec n s p
+-- instance (Pretty1 f) => Pretty (Fix f) where
+--     prettyPrec d (Fix f) = prettyPrec1 d f
 
-iShow :: (Show a) => a -> ISeq
-iShow = IStr . show
+--------------------------------------------------------------------------------
 
-----------------------------------------------------------------------------------
+ttext :: Pretty t => t -> Doc
+ttext = pretty
+
+hsepOf :: Getting (Endo Doc) s Doc -> s -> Doc
+hsepOf l = foldrOf l (<+>) mempty
+
+vsepOf :: Getting (Endo Doc) s Doc -> s -> Doc
+vsepOf l = foldrOf l ($+$) mempty
+
+vcatOf :: Getting (Endo Doc) s Doc -> s -> Doc
+vcatOf l = foldrOf l ($$) mempty
+
+vlinesOf :: Getting (Endo Doc) s Doc -> s -> Doc
+vlinesOf l = foldrOf l (\a b -> a $+$ "" $+$ b) mempty
+-- hack(?) to separate chunks with a blankline
+
+vsepTerm :: Doc -> Doc -> Doc -> Doc
+vsepTerm term a b = (a <> term) $+$ b
+
+vsep :: [Doc] -> Doc
+vsep = foldr ($+$) mempty
+
+--------------------------------------------------------------------------------
+
+appPrec, appPrec1 :: Int
+appPrec  = 10
+appPrec1 = 11
+
+instance PrintfArg Doc where
+    formatArg d fmt
+        | fmtChar (vFmt 'D' fmt) == 'D' = formatString (render d) fmt'
+        | otherwise                     = errorBadFormat $ fmtChar fmt
+      where
+        fmt' = fmt { fmtChar = 's', fmtPrecision = Nothing }
 
-instance (Pretty a) => Pretty (Maybe a) where
-    prettyPrec (Just a) p = prettyPrec a p
-    prettyPrec Nothing  p = "<Nothing>"

src/GM.hs

@@ -9,8 +9,12 @@ module GM
     ( hdbgProg
     , evalProg
     , evalProgR
+    , GmState(..)
+    , gmCode, gmStack, gmDump, gmHeap, gmEnv, gmStats
     , Node(..)
+    , showState
     , gmEvalProg
+    , Stats(..)
     , finalStateOf
     , resultOf
     , resultOfExpr
@@ -22,16 +26,18 @@ import Data.List                    (mapAccumL)
 import Data.Maybe                   (fromMaybe, mapMaybe)
 import Data.Monoid                  (Endo(..))
 import Data.Tuple                   (swap)
-import Lens.Micro
-import Lens.Micro.Extras            (view)
-import Lens.Micro.TH
-import Lens.Micro.Platform          (packed, unpacked)
-import Lens.Micro.Platform.Internal (IsText(..))
+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 System.IO                    (Handle, hPutStrLn)
+-- TODO: an actual output system
+-- TODO: an actual output system
+-- TODO: an actual output system
+-- TODO: an actual output system
+import System.IO.Unsafe             (unsafePerformIO)
 import Data.String                  (IsString)
 import Data.Heap
 import Debug.Trace
@@ -40,6 +46,15 @@ import Core2Core
 import Core
 ----------------------------------------------------------------------------------
 
+tag_Unit_unit :: Int
+tag_Unit_unit = 0
+
+tag_Bool_True :: Int
+tag_Bool_True = 1
+
+tag_Bool_False :: Int
+tag_Bool_False = 0
+
 {-}
 
 hdbgProg = undefined
@@ -75,6 +90,7 @@ data Key = NameKey Name
          | ConstrKey Tag Int
          deriving (Show, Eq)
 
+-- >> [ref/Instr]
 data Instr = Unwind
            | PushGlobal Name
            | PushConstr Tag Int
@@ -89,12 +105,14 @@ data Instr = Unwind
            -- arith
            | Neg | Add | Sub | Mul | Div
            -- comparison
-           | Equals
+           | Equals | Lesser | GreaterEq
            | Pack Tag Int -- Pack Tag Arity
            | CaseJump [(Tag, Code)]
            | Split Int
+           | Print
            | Halt
            deriving (Show, Eq)
+-- << [ref/Instr]
 
 data Node = NNum Int
           | NAp Addr Addr
@@ -137,7 +155,7 @@ evalProg p = res <&> (,sts)
         resAddr = final ^. gmStack ^? _head
         res = resAddr >>= flip hLookup h
 
-hdbgProg :: Program' -> Handle -> IO (Node, Stats)
+hdbgProg :: Program' -> Handle -> IO GmState
 hdbgProg p hio = do
     (renderOut . showState) `traverse_` states
     -- TODO: i'd like the statistics to be at the top of the file, but `sts`
@@ -145,7 +163,7 @@ hdbgProg p hio = do
     -- *can't* get partial logs in the case of a crash. this is in opposition to
     -- the above traversal which *will* produce partial logs. i love laziness :3
     renderOut . showStats $ sts
-    pure (res, sts)
+    pure final
     where
         renderOut r = hPutStrLn hio $ render r ++ "\n"
 
@@ -195,29 +213,55 @@ isFinal st = null $ st ^. gmCode
 
 step :: GmState -> GmState
 step st = case head (st ^. gmCode) of
-    Unwind         -> unwindI        
+    Unwind         -> unwindI
     PushGlobal n   -> pushGlobalI   n
     PushConstr t n -> pushConstrI t n
     PushInt    n   -> pushIntI      n
     Push       n   -> pushI         n
-    MkAp           -> mkApI          
+    MkAp           -> mkApI
     Slide      n   -> slideI        n
     Pop        n   -> popI          n
     Update     n   -> updateI       n
     Alloc      n   -> allocI        n
-    Eval           -> evalI          
-    Neg            -> negI           
-    Add            -> addI           
-    Sub            -> subI           
-    Mul            -> mulI           
-    Div            -> divI           
-    Equals         -> equalsI           
+    Eval           -> evalI
+    Neg            -> negI
+    Add            -> addI
+    Sub            -> subI
+    Mul            -> mulI
+    Div            -> divI
+    Equals         -> equalsI
+    Lesser         -> lesserI
+    GreaterEq      -> greaterEqI
     Split      n   -> splitI        n
     Pack       t n -> packI       t n
     CaseJump    as -> caseJumpI    as
+    Print          -> printI
     Halt           -> haltI
     where
 
+        printI :: GmState
+        printI = case hLookupUnsafe a h of
+            NNum n       -> (evilTempPrinter `seq` st)
+                          & gmCode .~ i
+                          & gmStack .~ s
+                where
+                    -- TODO: an actual output system
+                    -- TODO: an actual output system
+                    -- TODO: an actual output system
+                    -- TODO: an actual output system
+                    evilTempPrinter = unsafePerformIO (print n)
+            NConstr _ as -> st
+                          & gmCode .~ i' ++ i
+                          & gmStack .~ s'
+                where
+                    i' = mconcat $ replicate n [Eval,Print]
+                    n = length as
+                    s' = as ++ s
+          where
+            h = st ^. gmHeap
+            (a:s) = st ^. gmStack
+            Print : i = st ^. gmCode
+
         -- nuke the state
         haltI :: GmState
         haltI = error "halt#"
@@ -411,8 +455,10 @@ step st = case head (st ^. gmCode) of
         mulI = primitive2 boxInt unboxInt (*) st
         divI = primitive2 boxInt unboxInt div st
 
-        equalsI :: GmState
+        lesserI, greaterEqI, equalsI :: GmState
         equalsI = primitive2 boxBool unboxInt (==) st
+        lesserI = primitive2 boxBool unboxInt (<) st
+        greaterEqI = primitive2 boxBool unboxInt (>=) st
 
         splitI :: Int -> GmState
         splitI n = st
@@ -554,12 +600,13 @@ boxBool st p = st
     where
         h = st ^. gmHeap
         (h',a) = alloc h (NConstr p' [])
-        p' = if p then 1 else 0
+        p' = if p then tag_Bool_True else tag_Bool_False
 
 unboxBool :: Addr -> GmState -> Bool
 unboxBool a st = case hLookup a h of
-        Just (NConstr 1 []) -> True
-        Just (NConstr 0 []) -> False
+        Just (NConstr t [])
+            | t == tag_Bool_True  -> True
+            | t == tag_Bool_False -> False
         Just _              -> error "unboxInt received a non-int"
         Nothing             -> error "unboxInt received an invalid address"
     where h = st ^. gmHeap
@@ -595,6 +642,10 @@ compiledPrims =
     , binop "*#" Mul
     , binop "/#" Div
     , binop "==#" Equals
+    , binop "<#" Lesser
+    , binop ">=#" GreaterEq
+    , ("print#", 1, [ Push 0, Eval, Print, Pack tag_Unit_unit 0, Update 1, Pop 1
+                    , Unwind ])
     ]
     where
         unop k i = (k, 1, [Push 0, Eval, i, Update 1, Pop 1, Unwind])
@@ -698,14 +749,12 @@ buildInitialHeap (view programScDefs -> ss) = mapAccumL allocateSc mempty compil
                 mconcat binders <> compileE g' e <> [Slide d]
             where
                 d = length bs
-                (g',binders) = mapAccumL compileBinder (argOffset d g) addressed
-                -- kinda gross. revisit this
-                addressed = bs `zip` reverse [0 .. d-1]
+                (g',binders) = mapAccumL compileBinder g bs
 
-                compileBinder :: Env -> (Binding', Int) -> (Env, Code)
-                compileBinder m (k := v, a) = (m',c)
+                compileBinder :: Env -> Binding' -> (Env, Code)
+                compileBinder m (k := v) = (m',c)
                     where
-                        m' = (NameKey k, a) : m
+                        m' = (NameKey k, 0) : argOffset 1 m
                         -- make note that we use m rather than m'!
                         c = compileC m v
 
@@ -733,13 +782,15 @@ buildInitialHeap (view programScDefs -> ss) = mapAccumL allocateSc mempty compil
         compileE g ("*#" :$ a :$ b)  = inlineOp2 g Mul    a b
         compileE g ("/#" :$ a :$ b)  = inlineOp2 g Div    a b
         compileE g ("==#" :$ a :$ b) = inlineOp2 g Equals a b
+        compileE g ("<#" :$ a :$ b)  = inlineOp2 g Lesser a b
+        compileE g (">=#" :$ a :$ b)  = inlineOp2 g GreaterEq a b
 
         compileE g (Case e as) = compileE g e <> [CaseJump (compileD g as)]
 
         compileE g e = compileC g e ++ [Eval]
 
         compileD :: Env -> [Alter'] -> [(Tag, Code)]
-        compileD g as = fmap (compileA g) as
+        compileD g = fmap (compileA g)
 
         compileA :: Env -> Alter' -> (Tag, Code)
         compileA g (Alter (AltTag t) as e) = (t, [Split n] <> c <> [Slide n])

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/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,232 @@
+{
+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 }
+
+%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 }
+
+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 }
+
+AppE                :: { RlpExpr PsName }
+                    : AppE Expr1            { Finl $ Core.AppF $1 $2 }
+                    | Expr1                 { $1 }
+
+VarE                :: { RlpExpr PsName }
+                    : Var                   { 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)  : '{' layout_list0(';',p) '}'   { $2 }
+            | VL  layout_list0(VS,p)  VR    { $2 }
+
+-- 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) 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 = error "explode"
+
+extractName = view $ to extract . singular _TokenVarName
+
+}

src/Rlp/AltSyntax.hs

@@ -0,0 +1,219 @@
+{-# LANGUAGE TemplateHaskell, PatternSynonyms #-}
+module Rlp.AltSyntax
+    (
+    -- * AST
+      Program(..), Decl(..), ExprF(..), Pat(..)
+    , RlpExprF, RlpExpr, Binding(..), Alter(..)
+    , DataCon(..), Type(..)
+    , pattern IntT
+
+    , TypeF(..)
+
+    , Core.Name, PsName
+    , pattern (Core.:->)
+
+    -- * Optics
+    , programDecls
+    , _VarP, _FunB, _VarB
+
+    -- * Functor-related tools
+    , Fix(..), Cofree(..), Sum(..), pattern Finl, pattern Finr
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Functor.Sum
+import Control.Comonad.Cofree
+import Data.Fix
+import Data.Function            (fix)
+import GHC.Generics             (Generic, Generic1)
+import Data.Hashable
+import Data.Hashable.Lifted
+import GHC.Exts                 (IsString)
+import Control.Lens
+
+import Data.Functor.Foldable.TH
+import Text.Show.Deriving
+import Data.Eq.Deriving
+import Data.Text                qualified as T
+import Data.Pretty
+import Misc.Lift1
+
+import Compiler.Types
+import Core.Syntax              qualified as Core
+--------------------------------------------------------------------------------
+
+type PsName = T.Text
+
+newtype Program b a = Program [Decl b a]
+    deriving Show
+
+programDecls :: Lens' (Program b a) [Decl b a]
+programDecls = lens (\ (Program ds) -> ds) (const Program)
+
+data Decl b a = FunD b [Pat b] a
+              | DataD b [b] [DataCon b]
+              | TySigD b (Type b)
+              deriving Show
+
+data DataCon b = DataCon b [Type b]
+    deriving (Show, Generic)
+
+data Type b = VarT b
+            | ConT b
+            | AppT (Type b) (Type b)
+            | FunT
+            | ForallT b (Type b)
+            deriving (Show, Eq, Generic, Functor, Foldable, Traversable)
+
+instance (Hashable b) => Hashable (Type b)
+
+pattern IntT :: (IsString b, Eq b) => Type b
+pattern IntT = ConT "Int#"
+
+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)
+
+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 (Pretty b, Pretty a) => Pretty (ExprF b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b, Pretty a) => Pretty (Alter b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (Alter b) where
+    liftPrettyPrec pr _ (Alter p e) =
+        hsep [ pretty p, "->", pr 0 e]
+
+instance Pretty b => Pretty1 (ExprF b) where
+    liftPrettyPrec pr p (InfixEF o a b) = maybeParens (p>0) $
+        pr 1 a <+> pretty o <+> pr 1 b
+    liftPrettyPrec pr p (CaseEF e as) = maybeParens (p>0) $
+        hsep [ "case", pr 0 e, "of" ]
+        $+$ nest 2 (vcat $ liftPrettyPrec pr 0 <$> as)
+
+instance (Pretty b, Pretty a) => Pretty (Decl b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (Decl b) where
+    liftPrettyPrec pr _ (FunD f as e) =
+        hsep [ ttext f, hsep (prettyPrec appPrec1 <$> as)
+             , "=", pr 0 e ]
+
+    liftPrettyPrec _ _ (DataD f as []) =
+        hsep [ "data", ttext f, hsep (pretty <$> as) ]
+
+    liftPrettyPrec _ _ (DataD f as ds) =
+        hsep [ "data", ttext f, hsep (pretty <$> as), cons ]
+      where
+        cons = vcat $ zipWith (<+>) delims (pretty <$> ds)
+        delims = "=" : repeat "|"
+
+    liftPrettyPrec _ _ (TySigD n t) =
+        hsep [ ttext n, ":", pretty t ]
+
+instance (Pretty b) => Pretty (DataCon b) where
+    pretty (DataCon n as) = ttext n <+> hsep (prettyPrec appPrec1 <$> as)
+
+-- (->) is given prec `appPrec-1`
+instance (Pretty b) => Pretty (Type b) where
+    prettyPrec _ (VarT n) = ttext n
+    prettyPrec _ (ConT n) = ttext n
+    prettyPrec p (s Core.:-> t) = maybeParens (p>appPrec-1) $
+        hsep [ prettyPrec appPrec s, "->", prettyPrec (appPrec-1) t ]
+    prettyPrec p (AppT f x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec f <+> prettyPrec appPrec1 x
+    prettyPrec p FunT = maybeParens (p>0) "->"
+
+instance (Pretty b) => Pretty (Pat b) where
+    prettyPrec p (VarP b) = prettyPrec p b
+    prettyPrec p (ConP b) = prettyPrec p b
+    prettyPrec p (AppP c x) = maybeParens (p>appPrec) $
+        prettyPrec appPrec c <+> prettyPrec appPrec1 x
+
+instance (Pretty a, Pretty b) => Pretty (Program b a) where
+    prettyPrec = prettyPrec1
+
+instance (Pretty b) => Pretty1 (Program b) where
+    liftPrettyPrec pr p (Program ds) = vsep $ liftPrettyPrec pr p <$> ds
+
+makePrisms ''Pat
+makePrisms ''Binding
+
+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
+

src/Rlp/HindleyMilner.hs

@@ -0,0 +1,161 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE OverloadedLists #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.HindleyMilner
+    ( typeCheckRlpProgR
+    , solve
+    , TypeError(..)
+    , runHM'
+    , HM
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Lens             hiding (Context', Context, (:<), para)
+import Control.Monad.Errorful
+import Control.Monad.State
+import Control.Monad.Accum
+import Control.Monad
+import Control.Arrow            ((>>>))
+import Control.Monad.Writer.Strict
+import Data.Text                qualified as T
+import Data.Pretty
+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 Data.Maybe               (fromMaybe)
+import Data.Traversable
+import GHC.Generics             (Generic(..), Generically(..))
+
+import Data.Functor
+import Data.Functor.Foldable
+import Data.Fix                 hiding (cata, para)
+import Control.Comonad.Cofree
+import Control.Comonad
+
+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
+--------------------------------------------------------------------------------
+
+fixCofree :: (Functor f, Functor g)
+          => Iso (Fix f) (Fix g) (Cofree f ()) (Cofree g b)
+fixCofree = iso sa bt where
+    sa = foldFix (() :<)
+    bt (_ :< as) = Fix $ bt <$> as
+
+lookupVar :: PsName -> Context -> HM (Type PsName)
+lookupVar n g = case g ^. contextVars . at n of
+    Just t -> pure t
+    Nothing -> addFatal $ TyErrUntypedVariable n
+
+gather :: RlpExpr PsName -> HM (Type PsName, PartialJudgement)
+gather e = look >>= (H.lookup e >>> maybe memoise pure)
+    where
+        memoise = do
+            r <- gather' e
+            add (H.singleton e r)
+            pure r
+
+gather' :: RlpExpr PsName -> HM (Type PsName, PartialJudgement)
+gather' = \case
+    Finl (LitF (IntL _)) -> pure (IntT, mempty)
+
+    Finl (VarF n) -> do
+        t <- freshTv
+        let j = mempty & assumptions .~ H.singleton n [t]
+        pure (t,j)
+
+    Finl (AppF f x) -> do
+        tfx <- freshTv
+        (tf,jf) <- gather f
+        (tx,jx) <- gather x
+        let jtfx = mempty & constraints .~ [Equality tf (tx :-> tfx)]
+        pure (tfx, jf <> jx <> jtfx)
+
+    Finl (LamF [b] e) -> do
+        tb <- freshTv
+        (te,je) <- gather e
+        let cs = maybe [] (fmap $ Equality tb) (je ^. assumptions . at b)
+            as = je ^. assumptions & at b .~ Nothing
+            j = mempty & constraints .~ cs & assumptions .~ as
+            t = tb :-> te
+        pure (t,j)
+
+unify :: [Constraint] -> HM Context
+
+unify [] = pure mempty
+
+unify (Equality (sx :-> sy) (tx :-> ty) : cs) =
+    unify $ Equality sx tx : Equality sy ty : cs
+
+-- elim
+unify (Equality (ConT s) (ConT t) : cs) | s == t = unify cs
+unify (Equality (VarT s) (VarT t) : cs) | s == t = unify cs
+
+unify (Equality (VarT s) t : cs)
+    | occurs s t = addFatal $ TyErrRecursiveType s t
+    | otherwise  = unify cs' <&> contextVars . at s ?~ t
+  where
+    cs' = cs & each . constraintTypes %~ subst s t
+
+-- swap
+unify (Equality s (VarT t) : cs) = unify (Equality (VarT t) s : cs)
+
+unify (Equality s t : _) = addFatal $ TyErrCouldNotUnify s t
+
+annotate :: RlpExpr PsName
+         -> HM (Cofree (RlpExprF PsName) (Type PsName, PartialJudgement))
+annotate = sequenceA . fixtend (gather . wrapFix)
+
+solveTree :: Cofree (RlpExprF PsName) (Type PsName, PartialJudgement)
+          -> HM (Type PsName)
+solveTree e = undefined
+
+infer1 :: RlpExpr PsName -> HM (Type PsName)
+infer1 e = do
+    ((t,j) :< _) <- annotate e
+    g <- unify (j ^. constraints)
+    pure $ ifoldrOf (contextVars . itraversed) subst t g
+
+solve = undefined
+-- solve g e = do
+--     (t,j) <- gather e
+--     g' <- unify cs
+--     pure $ ifoldrOf (contextVars . itraversed) subst t g'
+
+occurs :: PsName -> Type PsName -> Bool
+occurs n = cata \case
+    VarTF m | n == m -> True
+    t                -> or t
+
+subst :: PsName -> Type PsName -> Type PsName -> Type PsName
+subst n t' = para \case
+    VarTF m | n == m -> t'
+    -- shadowing
+    ForallTF x (pre,post) | x == n    -> ForallT x pre
+                          | otherwise -> ForallT x post
+    t -> embed $ t <&> view _2
+
+prettyHM :: (Pretty a)
+         => Either [TypeError] (a, [Constraint])
+         -> Either [TypeError] (String, [String])
+prettyHM = over (mapped . _1) rpretty
+         . over (mapped . _2 . each) rpretty
+
+fixtend :: Functor f => (f (Fix f) -> b) -> Fix f -> Cofree f b
+fixtend c (Fix f) = c f :< fmap (fixtend c) f
+
+infer :: RlpExpr PsName -> HM (Cofree (RlpExprF PsName) (Type PsName))
+infer = undefined
+
+typeCheckRlpProgR :: (Monad m)
+                  => Program PsName (RlpExpr PsName)
+                  -> RLPCT m (Program PsName
+                      (Cofree (RlpExprF PsName) (Type PsName)))
+typeCheckRlpProgR = undefined
+

src/Rlp/HindleyMilner/Types.hs

@@ -0,0 +1,162 @@
+{-# 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 Control.Monad.Writer
+import Control.Monad.Accum
+import Control.Monad.Trans.Accum
+import Control.Monad.Errorful
+import Control.Monad.State
+import Text.Printf
+import Data.Pretty
+import Data.Function
+
+import Control.Lens             hiding (Context', Context)
+
+import Compiler.RlpcError
+import Rlp.AltSyntax
+--------------------------------------------------------------------------------
+
+newtype Context = Context
+    { _contextVars      :: HashMap PsName (Type PsName)
+    }
+    deriving (Show, Generic)
+    deriving (Semigroup, Monoid)
+        via Generically Context
+
+data Constraint = Equality (Type PsName) (Type PsName)
+    deriving (Eq, Generic, Show)
+
+data PartialJudgement = PartialJudgement
+    { _constraints :: [Constraint]
+    , _assumptions :: HashMap PsName [Type PsName]
+    }
+    deriving (Generic, Show)
+    deriving (Monoid)
+        via Generically PartialJudgement
+
+instance Semigroup PartialJudgement where
+    a <> b = PartialJudgement
+        { _constraints = ((<>) `on` _constraints) a b
+        , _assumptions = (H.unionWith (<>) `on` _assumptions) a b
+        }
+
+instance Hashable Constraint
+
+type Memo = HashMap (RlpExpr PsName) (Type PsName, PartialJudgement)
+
+type HM = ErrorfulT TypeError (StateT Int (Accum Memo))
+
+-- | Type error enum.
+data TypeError
+    -- | Two types could not be unified
+    = TyErrCouldNotUnify (Type Name) (Type Name)
+    -- | @x@ could not be unified with @t@ because @x@ occurs in @t@
+    | TyErrRecursiveType Name (Type Name)
+    -- | 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`."
+                              (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)
+            ]
+
+-- type Memo t = HashMap t (Type PsName, PartialJudgement)
+
+-- newtype HM t a = HM { unHM :: Int -> Memo t -> (a, Int, Memo t) }
+
+-- runHM :: (Hashable t) => HM t a -> (a, Memo t)
+-- runHM hm = let (a,_,m) = unHM hm 0 mempty in (a,m)
+
+-- instance Functor (HM t) where
+--     fmap f (HM h) = HM \n m -> h n m & _1 %~ f
+
+-- instance Applicative (HM t) where
+--     pure a = HM \n m -> (a,n,m)
+--     HM hf <*> HM ha = HM \n m ->
+--         let (f',n',m') = hf n m
+--             (a,n'',m'') = ha n' m'
+--         in (f' a, n'', m'')
+
+-- instance Monad (HM t) where
+--     HM ha >>= k = HM \n m ->
+--         let (a,n',m') = ha n m
+--             (a',n'',m'') = unHM (k a) n' m'
+--         in (a',n'', m'')
+
+-- instance Hashable t => MonadWriter (Memo t) (HM t) where
+--     -- IMPORTAN! (<>) is left-biased for HashMap! append `w` to the RIGHt!
+--     writer (a,w) = HM \n m -> (a,n,m <> w)
+--     listen ma = HM \n m ->
+--         let (a,n',m') = unHM ma n m
+--         in ((a,m'),n',m')
+--     pass maww = HM \n m ->
+--         let ((a,ww),n',m') = unHM maww n m
+--         in (a,n',ww m')
+
+-- instance MonadState Int (HM t) where
+--     state f = HM \n m ->
+--         let (a,n') = f n
+--         in (a,n',m)
+
+freshTv :: HM (Type PsName)
+freshTv = do
+    n <- get
+    modify succ
+    pure . VarT $ "$a" <> T.pack (show n)
+
+runHM' :: HM a -> Either [TypeError] a
+runHM' e = maybe (Left es) Right ma
+    where
+        ((ma,es),m) = (`runAccum` mempty) . (`evalStateT` 0) . runErrorfulT $ e
+
+-- addConstraint :: Constraint -> HM ()
+-- addConstraint = tell . pure
+
+makePrisms ''PartialJudgement
+makeLenses ''PartialJudgement
+makeLenses ''Context
+makePrisms ''Constraint
+makePrisms ''TypeError
+
+supplement :: [(PsName, Type PsName)] -> Context -> Context
+supplement bs = contextVars %~ (H.fromList bs <>)
+
+demoContext :: Context
+demoContext = Context
+    { _contextVars =
+        [ ("+#", IntT :-> IntT :-> IntT)
+        ]
+    }
+
+constraintTypes :: Traversal' Constraint (Type PsName)
+constraintTypes k (Equality s t) = Equality <$> k s <*> k t
+
+instance Pretty Constraint where
+    pretty (Equality s t) =
+        hsep [prettyPrec appPrec1 s, "~", prettyPrec appPrec1 t]
+

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)
@@ -27,9 +29,9 @@ import Data.Text                (Text)
 import Data.Text                qualified as T
 import Data.Word
 import Data.Default
-import Lens.Micro.Mtl
-import Lens.Micro
+import Control.Lens
 
+import Compiler.Types
 import Debug.Trace
 import Rlp.Parse.Types
 }
@@ -60,7 +62,7 @@ $asciisym       = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~\:]
     |infixr|infixl|infix
 
 @reservedop =
-    "=" | \\ | "->" | "|" | "::"
+    "=" | \\ | "->" | "|" | ":"
 
 rlp :-
     
@@ -85,6 +87,8 @@ $white_no_nl+       ;
 <0>
 {
     "let"               { constToken TokenLet `thenBeginPush` layout_let }
+    "letrec"            { constToken TokenLetrec `thenBeginPush` layout_let }
+    "of"                { constToken TokenOf `thenBeginPush` layout_of }
 }
 
 -- scan various identifiers and reserved words. order is important here!
@@ -124,18 +128,25 @@ $white_no_nl+       ;
     ()                  { doBol }
 }
 
-<layout_let>
-{
-    \n                  { beginPush bol }
-    "{"                 { explicitLBrace }
-    "in"                { constToken TokenIn `thenDo` (popLexState *> popLayout) }
-    ()                  { doLayout }
-}
-
 <layout_top>
 {
     \n                  ;
     "{"                 { explicitLBrace `thenDo` popLexState }
+}
+
+<layout, layout_let, layout_of>
+{
+    \n                  { beginPush bol }
+    "{"                 { explicitLBrace `thenDo` popLexState }
+}
+
+<layout_let>
+{
+    "in"                { constToken TokenIn `thenDo` (popLexState *> popLayout) }
+}
+
+<layout, layout_top, layout_let, layout_of>
+{
     ()                  { doLayout }
 }
 
@@ -147,16 +158,21 @@ lexReservedName = \case
     "case"      -> TokenCase
     "of"        -> TokenOf
     "let"       -> TokenLet
+    "letrec"    -> TokenLetrec
     "in"        -> TokenIn
     "infix"     -> TokenInfix
     "infixl"    -> TokenInfixL
     "infixr"    -> TokenInfixR
+    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
 --   /after/ the action
@@ -262,11 +278,12 @@ lexCont :: (Located RlpToken -> P a) -> P a
 lexCont = (lexToken >>=)
 
 lexStream :: P [RlpToken]
-lexStream = do
-    t <- lexToken
-    case t of
-        Located _ TokenEOF -> pure [TokenEOF]
-        Located _ t        -> (t:) <$> lexStream
+lexStream = fmap extract <$> lexStream'
+
+lexStream' :: P [Located RlpToken]
+lexStream' = lexToken >>= \case
+    t@(Located _ TokenEOF) -> pure [t]
+    t        -> (t:) <$> lexStream'
 
 lexDebug :: (Located RlpToken -> P a) -> P a
 lexDebug k = do
@@ -322,18 +339,19 @@ doBol :: LexerAction (Located RlpToken)
 doBol inp l = do
     off <- cmpLayout
     i <- indentLevel
-    traceM $ "i: " <> show i
+    -- traceM $ "i: " <> show i
     -- important that we pop the lex state lest we find our lexer diverging
-    popLexState
     case off of
         -- the line is aligned with the previous. it therefore belongs to the
         -- same list
-        EQ -> insertSemicolon
+        EQ -> popLexState *> insertSemicolon
         -- the line is indented further than the previous, so we assume it is a
         -- line continuation. ignore it and move on!
-        GT -> lexToken
+        GT -> popLexState *> lexToken
         -- the line is indented less than the previous, pop the layout stack and
-        -- insert a closing brace.
+        -- insert a closing brace. make VERY good note of the fact that we do not
+        -- pop the lex state! this means doBol is called until indentation is EQ
+        -- GT. so if multiple layouts are closed at once, this catches that.
         LT -> popLayout >> insertRBrace
 
 thenDo :: LexerAction a -> P b -> LexerAction a

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 Lens.Micro.Platform
+import Control.Lens                 hiding (snoc, (.>), (<.), (<<~), (:<))
 import Data.List.Extra
 import Data.Fix
 import Data.Functor.Const
@@ -25,6 +27,7 @@ import Data.Semigroup.Traversable
 import Data.Text                    (Text)
 import Data.Text                    qualified as T
 import Data.Void
+import Compiler.Types
 }
 
 %name parseRlpProg StandaloneProgram
@@ -42,6 +45,8 @@ import Data.Void
     consym          { Located _ (TokenConSym _) }
     varsym          { Located _ (TokenVarSym _) }
     data            { Located _ TokenData }
+    case            { Located _ TokenCase }
+    of              { Located _ TokenOf }
     litint          { Located _ (TokenLitInt _) }
     '='             { Located _ TokenEquals }
     '|'             { Located _ TokenPipe }
@@ -59,6 +64,7 @@ import Data.Void
     infixr          { Located _ TokenInfixR }
     infix           { Located _ TokenInfix }
     let             { Located _ TokenLet }
+    letrec          { Located _ TokenLetrec }
     in              { Located _ TokenIn }
 
 %nonassoc '='
@@ -67,139 +73,205 @@ import Data.Void
 
 %%
 
-StandaloneProgram   :: { RlpProgram RlpcPs }
-StandaloneProgram   : '{' Decls  '}'        {% mkProgram $2 }
-                    | VL  DeclsV VR         {% mkProgram $2 }
+StandaloneProgram   :: { Program RlpcPs SrcSpan }
+StandaloneProgram   : layout0(Decl)         {% mkProgram $1 }
 
-StandaloneExpr      :: { RlpExpr RlpcPs }
-                    : VL Expr VR            { extract $2 }
+StandaloneExpr      :: { Expr' RlpcPs SrcSpan }
+                    : VL Expr VR            { $2 }
 
 VL  :: { () }
 VL  : vlbrace       { () }
 
 VR  :: { () }
 VR  : vrbrace       { () }
-    | error         { () }
+    | error         {% void popLayout }
 
-Decls               :: { [Decl' RlpcPs] }
-Decls               : Decl ';' Decls        { $1 : $3 }
-                    | Decl ';'              { [$1] }
-                    | Decl                  { [$1] }
+VS                  :: { () }
+VS                  : ';'                   { () }
+                    | vsemi                 { () }
 
-DeclsV              :: { [Decl' RlpcPs] }
-DeclsV              : Decl VS Decls         { $1 : $3 }
-                    | Decl VS               { [$1] }
-                    | Decl                  { [$1] }
-                    | {- epsilon -}         { [] }
-
-VS                  :: { Located RlpToken }
-VS                  : ';'                   { $1 }
-                    | vsemi                 { $1 }
-
-Decl        :: { Decl' RlpcPs }
+Decl        :: { Decl RlpcPs SrcSpan }
             : FunDecl                   { $1 }
             | TySigDecl                 { $1 }
             | DataDecl                  { $1 }
             | InfixDecl                 { $1 }
 
-TySigDecl   :: { Decl' RlpcPs }
-            : Var '::' Type             { (\e -> TySigD [extract e]) <<~ $1 <~> $3 }
+TySigDecl   :: { Decl RlpcPs SrcSpan }
+            : Var '::' Type             { TySigD [$1] $3 }
 
-InfixDecl   :: { Decl' RlpcPs }
-            : InfixWord litint InfixOp  { $1 =>> \w ->
-                                          InfixD (extract $1) (extractInt $ extract $2)
-                                          (extract $3) }
+InfixDecl   :: { Decl RlpcPs SrcSpan }
+            : InfixWord litint InfixOp  {% mkInfixD $1 ($2 ^. _litint) $3 }
 
-InfixWord   :: { Located Assoc }
-            : infixl                    { $1 \$> InfixL }
-            | infixr                    { $1 \$> InfixR }
-            | infix                     { $1 \$> Infix  }
+InfixWord   :: { Assoc }
+            : infixl                    { InfixL }
+            | infixr                    { InfixR }
+            | infix                     { Infix }
 
-DataDecl    :: { Decl' RlpcPs }
-            : data Con TyParams '=' DataCons    { $1 \$> DataD (extract $2) $3 $5 }
+DataDecl    :: { Decl RlpcPs SrcSpan }
+            : 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) }
-            | varname                   { fmap VarT (mkPsName $1) }
+            | conname                   { ConT (extractName $1) }
+            | varname                   { VarT (extractName $1) }
 
-Type        :: { RlpType' RlpcPs }
-            : Type '->' Type            { FunT <<~ $1 <~> $3 }
-            | Type1                     { $1 }
+Type        :: { Ty RlpcPs }
+            : Type '->' Type            { FunT $1 $3 }
+            | TypeApp                   { $1 }
 
-FunDecl     :: { Decl' RlpcPs }
-FunDecl     : Var Params '=' Expr       { $4 =>> \e ->
-                                          FunD (extract $1) $2 e Nothing }
+TypeApp     :: { Ty RlpcPs }
+            : Type1                     { $1 }
+            | TypeApp Type1             { AppT $1 $2 }
 
-Params      :: { [Pat' RlpcPs] }
+FunDecl     :: { Decl RlpcPs SrcSpan }
+FunDecl     : Var Params '=' Expr       { FunD $1 $2 $4 Nothing }
+
+Params      :: { [Pat RlpcPs] }
 Params      : {- epsilon -}             { [] }
             | Params Pat1               { $1 `snoc` $2 }
 
-Pat1        :: { Pat' RlpcPs }
-            : Var                       { fmap VarP $1 }
-            | Lit                       { LitP <<= $1 }
+Pat         :: { Pat RlpcPs }
+            : Con Pat1s                 { ConP $1 $2 }
+            | Pat1                      { $1 }
 
-Expr        :: { RlpExpr' RlpcPs }
-            : Expr1 InfixOp Expr        { $2 =>> \o ->
-                                          OAppE (extract o) $1 $3 }
-            | Expr1                     { $1 }
+Pat1s       :: { [Pat RlpcPs] }
+            : Pat1s Pat1                { $1 `snoc` $2 }
+            | Pat1                      { [$1] }
+
+Pat1        :: { Pat RlpcPs }
+            : Con                       { ConP $1 [] }
+            | Var                       { VarP $1 }
+            | Lit                       { LitP $1 }
+            | '(' Pat ')'               { $2 }
+
+Expr        :: { Expr' RlpcPs SrcSpan }
+            -- infixities delayed till next release :(
+            -- : Expr1 InfixOp Expr        { undefined }
+            : AppExpr                   { $1 }
+            | TempInfixExpr             { $1 }
             | LetExpr                   { $1 }
+            | CaseExpr                  { $1 }
 
-LetExpr     :: { RlpExpr' RlpcPs }
-            : let layout1(Binding) in Expr { $1 \$> LetE $2 $4 }
+TempInfixExpr :: { Expr' RlpcPs SrcSpan }
+TempInfixExpr : Expr1 InfixOp TempInfixExpr {% tempInfixExprErr $1 $3 }
+              | Expr1 InfixOp Expr1         { nolo' $ InfixEF $2 $1 $3 }
 
+AppExpr     :: { Expr' RlpcPs SrcSpan }
+            : Expr1                     { $1 }
+            | AppExpr Expr1             { comb2 AppEF $1 $2 }
+
+LetExpr     :: { Expr' RlpcPs SrcSpan }
+            : let layout1(Binding) in Expr      { nolo' $ LetEF NonRec $2 $4 }
+            | letrec layout1(Binding) in Expr   { nolo' $ LetEF Rec $2 $4 }
+
+CaseExpr    :: { Expr' RlpcPs SrcSpan }
+            : case Expr of layout0(Alt)     { nolo' $ CaseEF $2 $4 }
+
+-- TODO: where-binds
+Alt         :: { Alt' RlpcPs SrcSpan }
+            : Pat '->' Expr                 { AltA $1 (view _unwrap $3) Nothing }
+
+-- layout0(p : β) :: [β]
+layout0(p)  : '{' layout_list0(';',p) '}'   { $2 }
+            | VL  layout_list0(VS,p)  VR    { $2 }
+
+-- 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) VR     { $2 }
 
+-- layout_list1(sep : α, p : β) :: [β]
 layout_list1(sep,p) : p                          { [$1] }
                     | layout_list1(sep,p) sep p  { $1 `snoc` $3 }
 
-Binding     :: { Binding' RlpcPs }
-            : Pat1 '=' Expr              { PatB <<~ $1 <~> $3 }
+Binding     :: { Binding' RlpcPs SrcSpan }
+            : Pat '=' Expr              { PatB $1 (view _unwrap $3) }
 
-Expr1       :: { RlpExpr' RlpcPs }
-            : '(' Expr ')'              { $1 .> $2 <. $3 }
-            | Lit                       { fmap LitE $1 }
-            | Var                       { fmap VarE $1 }
+Expr1       :: { Expr' RlpcPs SrcSpan }
+            : '(' Expr ')'              { $2 }
+            | Lit                       { nolo' $ LitEF $1 }
+            | Var                       { case $1 of Located ss _ -> ss :< VarEF $1 }
+            | Con                       { case $1 of Located ss _ -> ss :< VarEF $1 }
 
-InfixOp     :: { Located PsName }
-            : consym                    { mkPsName $1 }
-            | varsym                    { mkPsName $1 }
+InfixOp     :: { PsName }
+            : consym                    { extractName $1 }
+            | varsym                    { extractName $1 }
 
 -- TODO: microlens-pro save me microlens-pro (rewrite this with prisms)
-Lit         :: { Lit' RlpcPs }
-            : litint                    { $1 <&> (IntL . (\ (TokenLitInt n) -> n)) }
+Lit         :: { Lit RlpcPs }
+            : litint                    { $1 ^. to extract
+                                              . singular _TokenLitInt
+                                              . to IntL }
 
-Var         :: { Located PsName }
-Var         : varname                   { mkPsName $1 }
+Var         :: { PsName }
+Var         : varname                   { $1 <&> view (singular _TokenVarName) }
+            | varsym                    { $1 <&> view (singular _TokenVarSym) }
 
-Con         :: { Located PsName }
-            : conname                   { mkPsName $1 }
+Con         :: { PsName }
+            : conname                   { $1 <&> view (singular _TokenConName) }
 
 {
 
-parseRlpExprR = undefined
+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
 
-parseRlpProgR :: (Monad m) => Text -> RLPCT m (RlpProgram RlpcPs)
-parseRlpProgR s = liftErrorful $ pToErrorful parseRlpProg st
+parseRlpExprR :: (Monad m) => Text -> RLPCT m (Expr' RlpcPs SrcSpan)
+parseRlpExprR s = liftErrorful $ pToErrorful parseRlpExpr st
     where
         st = programInitState s
 
+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
+    pure a
+  where
+        st = programInitState s
+
 mkPsName :: Located RlpToken -> Located PsName
 mkPsName = fmap extractName
 
@@ -215,30 +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)
+
+intOfToken :: Located RlpToken -> Int
+intOfToken (Located _ (TokenLitInt n)) = n
+
+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)
 
-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
-
 }
 

src/Rlp/Parse/Associate.hs

@@ -1,19 +1,37 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PatternSynonyms, ViewPatterns, ImplicitParams #-}
 module Rlp.Parse.Associate
-    {-# WARNING "temporarily unimplemented" #-}
+    {-# WARNING "unimplemented" #-}
     ( associate
     )
     where
 --------------------------------------------------------------------------------
 import Data.HashMap.Strict              qualified as H
 import Data.Functor.Foldable
+import Data.Functor.Foldable.TH
 import Data.Functor.Const
-import Lens.Micro
+import Data.Functor
+import Data.Text                        qualified as T
+import Text.Printf
+import Control.Lens
 import Rlp.Parse.Types
 import Rlp.Syntax
 --------------------------------------------------------------------------------
 
-associate x y = y
-{-# WARNING associate "temporarily undefined" #-}
+associate :: OpTable -> Decl RlpcPs a -> Decl RlpcPs a
+associate _ p = p
+
+{-# WARNING associate "unimplemented" #-}
+
+examplePrecTable :: OpTable
+examplePrecTable = H.fromList
+    [ ("+",    (InfixL,6))
+    , ("*",    (InfixL,7))
+    , ("^",    (InfixR,8))
+    , (".",    (InfixR,7))
+    , ("~",    (Infix, 9))
+    , ("=",    (Infix, 4))
+    , ("&&",   (Infix, 3))
+    , ("||",   (Infix, 2))
+    , ("$",    (InfixR,0))
+    , ("&",    (InfixL,0))
+    ]
 

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
@@ -17,10 +18,9 @@ module Rlp.Parse.Types
     , RlpToken(..), AlexInput(..), Position(..), spanFromPos, LexerAction
     , Located(..), PsName
     -- ** Lenses
+    , _TokenLitInt, _TokenVarName, _TokenConName, _TokenVarSym, _TokenConSym
     , aiPrevChar, aiSource, aiBytes, aiPos, posLine, posColumn
 
-    , (<<~), (<~>)
-
     -- * Error handling
     , MsgEnvelope(..), RlpcError(..), RlpParseError(..)
     , addFatal, addWound, addFatalHere, addWoundHere
@@ -28,10 +28,13 @@ 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
+import Control.Comonad              (extract)
 import Compiler.RlpcError
+import Language.Haskell.TH.Syntax   (Lift)
 import Data.Text                    (Text)
 import Data.Maybe
 import Data.Fix
@@ -42,8 +45,7 @@ import Data.HashMap.Strict          qualified as H
 import Data.Void
 import Data.Word                    (Word8)
 import Data.Text                    qualified as T
-import Lens.Micro.TH
-import Lens.Micro
+import Control.Lens                 hiding ((<<~))
 import Rlp.Syntax
 import Compiler.Types
 --------------------------------------------------------------------------------
@@ -52,26 +54,9 @@ import Compiler.Types
 
 data RlpcPs
 
-type instance XRec RlpcPs f = Located (f RlpcPs)
-type instance IdP RlpcPs = PsName
+type instance NameP RlpcPs = PsName
 
-type instance XFunD RlpcPs = ()
-type instance XDataD RlpcPs = ()
-type instance XInfixD RlpcPs = ()
-type instance XTySigD RlpcPs = ()
-type instance XXDeclD RlpcPs = ()
-
-type instance XLetE 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 PsName = Text
+type PsName = Located Text
 
 --------------------------------------------------------------------------------
 
@@ -109,15 +94,16 @@ data RlpToken
     -- literals
     = TokenLitInt Int
     -- identifiers
-    | TokenVarName Name
-    | TokenConName Name
-    | TokenVarSym Name
-    | TokenConSym Name
+    | TokenVarName Text
+    | TokenConName Text
+    | TokenVarSym Text
+    | TokenConSym Text
     -- reserved words
     | TokenData
     | TokenCase
     | TokenOf
     | TokenLet
+    | TokenLetrec
     | TokenIn
     | TokenInfixL
     | TokenInfixR
@@ -142,6 +128,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)
@@ -191,12 +202,11 @@ data Layout = Explicit
 type OpTable = H.HashMap Name OpInfo
 type OpInfo = (Assoc, Int)
 
--- data WithLocation a = WithLocation [String] a
-
 data RlpParseError = RlpParErrOutOfBoundsPrecedence Int
                    | RlpParErrDuplicateInfixD Name
                    | RlpParErrLexical
                    | RlpParErrUnexpectedToken RlpToken [String]
+                   | RlpParErrOther [Text]
                    deriving (Show)
 
 instance IsRlpcError RlpParseError where
@@ -215,6 +225,8 @@ instance IsRlpcError RlpParseError where
             Text [ "Unexpected token " <> tshow t
                  , "Expected: " <> tshow exp
                  ]
+        RlpParErrOther ts ->
+            Text ts
         where
             tshow :: (Show a) => a -> T.Text
             tshow = T.pack . show
@@ -265,6 +277,19 @@ initAlexInput s = AlexInput
     { _aiPrevChar   = '\0'
     , _aiSource     = s
     , _aiBytes      = []
-    , _aiPos        = (1,1,0)
+    , _aiPos        = (1,0,0)
     }
 
+--------------------------------------------------------------------------------
+
+
+-- deriving instance Lift (Program RlpcPs)
+-- deriving instance Lift (Decl RlpcPs)
+-- deriving instance Lift (Pat RlpcPs)
+-- deriving instance Lift (Lit RlpcPs)
+-- deriving instance Lift (Expr RlpcPs)
+-- deriving instance Lift (Binding RlpcPs)
+-- deriving instance Lift (Ty RlpcPs)
+-- deriving instance Lift (Alt RlpcPs)
+-- deriving instance Lift (ConAlt RlpcPs)
+

src/Rlp/Syntax.hs

@@ -1,244 +1,10 @@
--- recursion-schemes
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable
-  , TemplateHaskell, TypeFamilies #-}
-{-# LANGUAGE OverloadedStrings, PatternSynonyms #-}
-{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
-{-# LANGUAGE UndecidableInstances, ImpredicativeTypes #-}
 module Rlp.Syntax
-    (
-    -- * AST
-      RlpProgram(..)
-    , Decl(..), Decl', RlpExpr(..), RlpExpr'
-    , Pat(..), Pat'
-    , Assoc(..)
-    , Lit(..), Lit'
-    , RlpType(..), RlpType'
-    , ConAlt(..)
-    , Binding(..), Binding'
-
-    -- * Trees That Grow boilerplate
-    -- ** Extension points
-    , IdP, XRec, UnXRec(..), MapXRec(..)
-    -- *** Decl
-    , XFunD, XTySigD, XInfixD, XDataD, XXDeclD
-    -- *** RlpExpr
-    , XLetE, XVarE, XLamE, XCaseE, XIfE, XAppE, XLitE
-    , XParE, XOAppE, XXRlpExprE
-    -- ** Pattern synonyms
-    -- *** Decl
-    , pattern FunD, pattern TySigD, pattern InfixD, pattern DataD
-    -- *** RlpExpr
-    , pattern LetE, pattern VarE, pattern LamE, pattern CaseE, pattern IfE
-    , pattern AppE, pattern LitE, pattern ParE, pattern OAppE
-    , pattern XRlpExprE
+    ( module Rlp.Syntax.Backstage
+    , module Rlp.Syntax.Types
     )
     where
-----------------------------------------------------------------------------------
-import Data.Text                    (Text)
-import Data.Text                    qualified as T
-import Data.String                  (IsString(..))
-import Data.Functor.Foldable.TH     (makeBaseFunctor)
-import Data.Functor.Classes
-import Data.Kind                    (Type)
-import Lens.Micro
-import Lens.Micro.TH
-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), Show (XRec p RlpExpr)
-    , Show (XRec p Lit), Show (IdP p)
-    , Show (XRec p RlpType)
-    , Show (XRec p Binding)
-    )
-
-newtype RlpProgram p = RlpProgram [Decl' p]
-
-deriving instance (PhaseShow p, Show (XRec p Decl)) => 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
-
-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' ()
-
-type Decl' p = XRec p Decl
-
-data Assoc = InfixL
-           | InfixR
-           | Infix
-           deriving (Show)
-
-data ConAlt p = ConAlt (IdP p) [RlpType' p]
-
-deriving instance (Show (IdP p), Show (XRec p RlpType)) => Show (ConAlt p)
-
-data RlpExpr p = LetE'  (XLetE 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)
-
-type family XLetE 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 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 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 (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
-
-class UnXRec p where
-    unXRec :: XRec p f -> f p
-
-class MapXRec p where
-    mapXRec :: (f p -> f' p') -> XRec p f -> XRec p' f'
-
-type family XRec p (f :: Type -> Type) = (r :: Type) | r -> p f
-
-type family 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
-
-deriving instance (Show (XRec p Pat), Show (XRec p RlpExpr), Show (IdP p)
-                  ) => Show (Binding p)
-
-data Pat p = VarP (IdP p)
-           | LitP (Lit' p)
-           | ConP (IdP p) [Pat' p]
-
-deriving instance (PhaseShow p) => Show (Pat p)
-
-type Pat' p = XRec p Pat
-
-data Lit p = IntL Int
-           | CharL Char
-           | ListL [RlpExpr' p]
-
-deriving instance (PhaseShow p) => Show (Lit p)
-
-type Lit' p = XRec p Lit
-
--- 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
-
+--------------------------------------------------------------------------------
+import Rlp.Syntax.Backstage
+import Rlp.Syntax.Types
 --------------------------------------------------------------------------------
 
-makeLenses ''RlpModule
-

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/Good.hs

@@ -0,0 +1,56 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Rlp.Syntax.Good
+    ( Decl(..), Program(..)
+    , programDecls
+    , Mistake(..)
+    )
+    where
+--------------------------------------------------------------------------------
+import Data.Kind
+import Control.Lens
+import Rlp.Syntax.Types (NameP)
+import Rlp.Syntax.Types qualified as Rlp
+--------------------------------------------------------------------------------
+
+data Program b a = Program
+    { _programDecls :: [Decl b a]
+    }
+
+data Decl p a = FunD   (NameP p) [Rlp.Pat p] a
+              | TySigD [NameP p] (Rlp.Ty p)
+              | DataD  (NameP p) [NameP p] [Rlp.ConAlt p]
+              | InfixD Rlp.Assoc Int (NameP p)
+
+type Where p a = [Binding p a]
+
+data Binding p a = PatB (Rlp.Pat p) a
+    deriving (Functor, Foldable, Traversable)
+
+makeLenses ''Program
+
+class Mistake a where
+    type family Ammend a :: Type
+    ammendMistake :: a -> Ammend a
+
+instance Mistake (Rlp.Program p a) where
+    type Ammend (Rlp.Program p a) = Program p (Rlp.Expr' p a)
+
+    ammendMistake p = Program
+        { _programDecls = ammendMistake <$> Rlp._programDecls p
+        }
+
+instance Mistake (Rlp.Decl p a) where
+    type Ammend (Rlp.Decl p a) = Decl p (Rlp.Expr' p a)
+
+    ammendMistake = \case
+        Rlp.FunD n as e _  -> FunD n as e
+        Rlp.TySigD ns t    -> TySigD ns t
+        Rlp.DataD n as cs  -> DataD n as cs
+        Rlp.InfixD ass p n -> InfixD ass p n
+
+instance Mistake (Rlp.Binding p a) where
+    type Ammend (Rlp.Binding p a) = Binding p (Rlp.ExprF p a)
+
+    ammendMistake = \case
+        Rlp.PatB k v -> PatB k v
+

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

@@ -0,0 +1,36 @@
+module Rlp.TH
+    ( rlpProg
+    , rlpExpr
+    )
+    where
+--------------------------------------------------------------------------------
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+import Language.Haskell.TH.Quote
+import Data.Text                        (Text)
+import Data.Text                        qualified as T
+import Control.Monad.IO.Class
+import Control.Monad
+
+import Compiler.RLPC
+import Rlp.AltParse
+--------------------------------------------------------------------------------
+
+rlpProg :: QuasiQuoter
+rlpProg = mkqq parseRlpProgR
+
+rlpExpr :: QuasiQuoter
+rlpExpr = mkqq parseRlpExprR
+
+mkq :: (Lift a) => (Text -> RLPCIO a) -> String -> Q Exp
+mkq parse = evalAndParse >=> lift where
+    evalAndParse = liftIO . evalRLPCIO def . parse . T.pack
+
+mkqq :: (Lift a) => (Text -> RLPCIO a) -> QuasiQuoter
+mkqq p = QuasiQuoter
+    { quoteExp = mkq p
+    , quotePat = error "rlp quasiquotes may only be used in expressions"
+    , quoteType = error "rlp quasiquotes may only be used in expressions"
+    , quoteDec = error "rlp quasiquotes may only be used in expressions"
+    }
+

src/Rlp2Core.hs

@@ -0,0 +1,107 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveTraversable #-}
+module Rlp2Core
+    ( desugarRlpProgR
+    , desugarRlpProg
+    , desugarRlpExpr
+    )
+    where
+--------------------------------------------------------------------------------
+import Control.Monad
+import Control.Monad.Writer.CPS
+import Control.Monad.Utils
+import Control.Arrow
+import Control.Applicative
+import Control.Comonad
+import Control.Lens
+import Compiler.RLPC
+import Data.List                        (mapAccumL, partition)
+import Data.Text                        (Text)
+import Data.Text                        qualified as T
+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 Effectful.State.Static.Local
+import Effectful.Labeled
+import Effectful
+import Text.Show.Deriving
+
+import Core.Syntax                      as Core
+import Rlp.AltSyntax                    as Rlp
+import Compiler.Types
+import Data.Pretty                      (render, pretty)
+--------------------------------------------------------------------------------
+
+type Tree a = Either Name (Name, Branch a)
+
+-- | Rose tree branch representing "nested" "patterns" in the Core language. That
+-- is, a constructor with children that are either a normal binder (Left (Given)
+-- name) or an indirection to another pattern (Right (Generated name) (Pattern))
+
+data Branch a = Branch Name [Tree a]
+    deriving (Show, Functor, Foldable, Traversable)
+
+-- | The actual rose tree.
+-- @type Rose = 'Data.Fix.Fix' 'Branch'@
+
+type Rose = Fix Branch
+
+deriveShow1 ''Branch
+
+--------------------------------------------------------------------------------
+
+desugarRlpProgR :: forall m a. (Monad m)
+                => Rlp.Program PsName a
+                -> RLPCT m Core.Program'
+desugarRlpProgR p = do
+    let p' = desugarRlpProg p
+    addDebugMsg "dump-desugared" $ render (pretty p')
+    pure p'
+
+desugarRlpProg = undefined
+
+desugarRlpExpr = undefined
+
+runNameSupply :: Text -> Eff (NameSupply ': es) a -> Eff es a
+runNameSupply pre = undefined -- evalState [ pre <> "_" <> tshow name | name <- [0..] ]
+
+-- the rl' program is desugared by desugaring each declaration as a separate
+-- program, and taking the monoidal product of the lot :3
+
+rlpProgToCore :: Rlp.Program PsName (RlpExpr PsName) -> Program'
+rlpProgToCore = foldMapOf (programDecls . each) declToCore
+
+declToCore :: Rlp.Decl PsName (RlpExpr PsName) -> Program'
+
+-- assume all arguments are VarP's for now
+declToCore (FunD b as e) = mempty & programScDefs .~ [ScDef b as' e']
+    where
+        as' = as ^.. each . singular _VarP
+        e' = runPureEff . runNameSupply b . exprToCore $ e
+
+type NameSupply = State [Name]
+
+exprToCore :: (NameSupply :> es)
+           => RlpExpr PsName -> Eff es Core.Expr'
+exprToCore = foldFixM \case
+    InL e -> pure $ Fix e
+    InR e -> rlpExprToCore e
+
+rlpExprToCore :: (NameSupply :> es)
+           => Rlp.ExprF PsName Core.Expr' -> Eff es Core.Expr'
+
+-- assume all binders are simple variable patterns for now
+rlpExprToCore (LetEF r bs e) = pure $ Let r bs' e
+  where
+    bs' = b2b <$> bs
+    b2b (VarB (VarP k) v) = Binding k v
+

src/TI.hs

@@ -20,8 +20,7 @@ import System.IO                (Handle, hPutStr)
 import Text.Printf              (printf, hPrintf)
 import Data.Proxy               (Proxy(..))
 import Data.Monoid              (Endo(..))
-import Lens.Micro
-import Lens.Micro.TH
+import Control.Lens
 import Data.Pretty
 import Data.Heap
 import Core.Examples

tst/Arith.hs

@@ -41,6 +41,7 @@ evalArith (a ::* b)   = evalArith a * evalArith b
 evalArith (a ::- b)   = evalArith a - evalArith b
 
 instance Arbitrary ArithExpr where
+    -- TODO: implement shrink
     arbitrary = gen 4
         where
             gen :: Int -> Gen ArithExpr

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
+