this sucks lol

unparsers

README.md

@@ -12,14 +12,15 @@ $ cabal build       # Build the rlpc compiler
 $ cabal install     # Install rlpc to $PATH
 $ cabal haddock     # Build the API docs w/ Haddock
 $ make -C doc html  # Build the primary docs w/ Sphinx
+
+# run the test suite
+$ cabal test --test-show-details=direct
 ```
 
 ### Use
 ```sh
-# Compile and evaluate t.hs
+# Compile and evaluate examples/factorial.hs, with evaluation info dumped to stderr
-$ rlpc t.hs
+$ rlpc -ddump-eval examples/factorial.hs
-# Compile and evaluate t.hs, with evaluation info dumped to stderr
-$ rlpc -ddump-eval t.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 and die
@@ -80,7 +81,7 @@ Listed in order of importance.
     - [ ] Tail call optimisation
     - [x] Parsing rlp
 - [ ] Tests
-    - [ ] Generic example programs
+    - [x] Generic example programs
     - [ ] Parser
 
 ### December Release Plan

app/Main.hs

@@ -7,6 +7,9 @@ import Options.Applicative      hiding (ParseError)
 import Control.Monad
 import Control.Monad.Reader
 import Data.HashSet             qualified as S
+import Data.Text                (Text)
+import Data.Text                qualified as T
+import Data.Text.IO             qualified as TIO
 import System.IO
 import System.Exit              (exitSuccess)
 import Core
@@ -102,7 +105,7 @@ dshowFlags = whenFlag flagDDumpOpts do
 ddumpAST :: RLPCIO CompilerError ()
 ddumpAST = whenFlag flagDDumpAST $ forFiles_ \o f -> do
     liftIO $ withFile f ReadMode $ \h -> do
-        s <- hGetContents h
+        s <- TIO.hGetContents h
         case parseProg o s of
             Right (a,_) -> hPutStrLn stderr $ show a
             Left e -> error "todo errors lol"
@@ -110,10 +113,10 @@ ddumpAST = whenFlag flagDDumpAST $ forFiles_ \o f -> do
 ddumpEval :: RLPCIO CompilerError ()
 ddumpEval = whenFlag flagDDumpEval do
     fs <- view rlpcInputFiles
-    forM_ fs $ \f -> liftIO (readFile f) >>= doProg
+    forM_ fs $ \f -> liftIO (TIO.readFile f) >>= doProg
 
     where
-        doProg :: String -> RLPCIO CompilerError ()
+        doProg :: Text -> RLPCIO CompilerError ()
         doProg s = ask >>= \o -> case parseProg o s of
             -- TODO: error handling
             Left e -> addFatal . CompilerError $ show e
@@ -133,7 +136,7 @@ ddumpEval = whenFlag flagDDumpEval do
             where v f p h = f p h *> pure ()
 
 parseProg :: RLPCOptions
-          -> String
+          -> Text
           -> Either SrcError (Program', [SrcError])
 parseProg o = evalRLPC o . (lexCore >=> parseCoreProg)
 

doc/src/commentary/gm.rst

@@ -1,16 +1,24 @@
 The *G-Machine*
 ===============
 
+The G-Machine (graph machine) is the current heart of rlpc, until we potentially
+move onto a STG (spineless tagless graph machine) or a TIM (three-instruction
+machine). rl' source code is desugared into Core; a dumbed-down subset of rl',
+and then compiled to G-Machine code, which is then finally translated to the
+desired target.
+
 **********
 Motivation
 **********
 
-Our initial model, the *Template Instantiator* (TI) was a very
+Our initial model, the *Template Instantiator* (TI) was a very straightforward
-straightforward solution to compilation, but its core design has a major
+solution to compilation, but its core design has a major Achilles' heel, being
-Achilles' heel, being that Compilation is interleaved with evaluation -- The
+that compilation is interleaved with evaluation -- The heap nodes for
-heap nodes for supercombinators hold uninstantiated expressions, i.e. raw ASTs
+supercombinators hold uninstantiated expressions, i.e. raw ASTs straight from
-straight from the parser. When a supercombinator is found on the stack during
+the parser. When a supercombinator is found on the stack during evaluation, the
-evaluation, the template expression is instantiated (compiled) on the spot.
+template expression is instantiated (compiled) on the spot. This makes
+translation to an assembly difficult, undermining the point of an intermediate
+language.
 
 .. math::
    \transrule
@@ -31,7 +39,7 @@ evaluation, the template expression is instantiated (compiled) on the spot.
    \text{where } h' = \mathtt{instantiateU} \; e \; a_n \; h \; g
    }
 
-The process of instantiating a supercombinator goes something like this
+The process of instantiating a supercombinator goes something like this:
 
 1. Augment the environment with bindings to the arguments.
 
@@ -52,13 +60,17 @@ The process of instantiating a supercombinator goes something like this
 Instantiating the supercombinator's body in this way is the root of our
 Achilles' heel. Traversing a tree structure is a very non-linear task unfit for
 an assembly target. The goal of our new G-Machine is to compile a *linear
-sequence of instructions* which instantiate the expression at execution.
+sequence of instructions* which, **when executed**, build up a graph
+representing the code.
 
 **************************
 Trees and Vines, in Theory
 **************************
 
-WIP.
+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

doc/src/commentary/ti.rst

@@ -1,6 +0,0 @@
-The *Template Instantiator*
-====================================
-
-WIP. This will hopefully be expanded into a thorough walkthrough of the state
-machine.
-

doc/src/conf.py

@@ -13,7 +13,7 @@ author = 'madeleine sydney slaga'
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration
 
-extensions = ['sphinx.ext.imgmath']
+extensions = ['sphinx.ext.imgmath', 'sphinx.ext.graphviz']
 
 # templates_path = ['_templates']
 exclude_patterns = []

examples/constDivZero.hs

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

examples/factorial.hs

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

examples/sumList.hs

@@ -0,0 +1,9 @@
+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;
+

rlp.cabal

@@ -22,17 +22,21 @@ library
                     , TI
                     , GM
                     , Compiler.RLPC
+                    , Compiler.RlpcError
+                    , Compiler.JustRun
                     , Core.Syntax
                     , Core.Examples
                     , Core.Utils
                     , Core.TH
+                    , Core.HindleyMilner
+                    , Control.Monad.Errorful
 
     other-modules:    Data.Heap
                     , Data.Pretty
                     , Core.Parse
                     , Core.Lex
-                    , Control.Monad.Errorful
                     , Core2Core
+                    , Control.Monad.Utils
                     , RLP.Syntax
 
     build-tool-depends: happy:happy, alex:alex
@@ -41,7 +45,9 @@ library
     build-depends:    base ^>=4.18.0.0
                     , containers
                     , microlens
+                    , microlens-mtl
                     , microlens-th
+                    , microlens-platform
                     , mtl
                     , template-haskell
                     -- required for happy
@@ -50,6 +56,8 @@ library
                     , unordered-containers
                     , hashable
                     , pretty
+                    -- TODO: either learn recursion-schemes, or stop depending
+                    -- on it.
                     , recursion-schemes
                     , megaparsec
                     , text
@@ -69,6 +77,7 @@ executable rlpc
                  , microlens-mtl
                  , mtl
                  , unordered-containers
+                 , text
 
     hs-source-dirs:   app
     default-language: GHC2021
@@ -81,10 +90,20 @@ test-suite rlp-test
     hs-source-dirs: tst
     main-is: Main.hs
     build-depends: base ^>=4.18.0.0
+                 , unordered-containers
                  , rlp
                  , QuickCheck
                  , hspec            ==2.*
+                 , microlens
+                 , text
+                 , pretty
+                 , microlens-platform
+
     other-modules: Arith
                  , GMSpec
+                 , CoreSyntax
+                 , Core.HindleyMilnerSpec
+                 , Core.ParseSpec
+
     build-tool-depends: hspec-discover:hspec-discover
 

src/Compiler/JustRun.hs

@@ -0,0 +1,48 @@
+{-|
+Module      : Compiler.JustRun
+Description : No-BS, high-level wrappers for major pipeline pieces.
+
+A collection of wrapper functions to demo processes such as lexing, parsing,
+type-checking, and evaluation. This module intends to export "no-BS" functions
+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
+    , RlpcError
+    , Program'
+    )
+    where
+----------------------------------------------------------------------------------
+import Core.Lex
+import Core.Parse
+import Core.HindleyMilner
+import Core.Syntax                      (Program')
+import Compiler.RLPC
+import Control.Arrow                    ((>>>))
+import Control.Monad                    ((>=>))
+import Data.Text                        qualified as T
+import Data.Function                    ((&))
+import GM
+----------------------------------------------------------------------------------
+
+justLexSrc :: String -> Either RlpcError [CoreToken]
+justLexSrc s = lexCoreR (T.pack s)
+             & fmap (map $ \ (Located _ _ _ t) -> t)
+             & rlpcToEither
+
+justParseSrc :: String -> Either RlpcError Program'
+justParseSrc s = parse (T.pack s)
+               & rlpcToEither
+    where parse = lexCoreR >=> parseCoreProgR
+
+justTypeCheckSrc :: String -> Either RlpcError Program'
+justTypeCheckSrc s = typechk (T.pack s)
+                   & rlpcToEither
+    where typechk = lexCoreR >=> parseCoreProgR >=> checkCoreProgR
+
+rlpcToEither :: RLPC e a -> Either e a
+rlpcToEither = evalRLPC def >>> fmap fst
+

src/Compiler/RLPC.hs

@@ -13,9 +13,12 @@ errors and the family of RLPC monads.
 {-# LANGUAGE DeriveGeneric, DerivingStrategies, DerivingVia #-}
 module Compiler.RLPC
     ( RLPC
-    , RLPCT
+    , RLPCT(..)
     , RLPCIO
     , RLPCOptions(RLPCOptions)
+    , RlpcError(..)
+    , IsRlpcError(..)
+    , rlpc
     , addFatal
     , addWound
     , MonadErrorful
@@ -24,6 +27,9 @@ module Compiler.RLPC
     , evalRLPCT
     , evalRLPCIO
     , evalRLPC
+    , addRlpcWound
+    , addRlpcFatal
+    , liftRlpcErrs
     , rlpcLogFile
     , rlpcDebugOpts
     , rlpcEvaluator
@@ -42,6 +48,7 @@ import Control.Exception
 import Control.Monad.Reader
 import Control.Monad.State      (MonadState(state))
 import Control.Monad.Errorful
+import Compiler.RlpcError
 import Data.Functor.Identity
 import Data.Default.Class
 import GHC.Generics             (Generic)
@@ -94,7 +101,6 @@ evalRLPCIO o m = do
         Left e -> throwIO e
         Right a -> pure a
 
-
 data RLPCOptions = RLPCOptions
     { _rlpcLogFile     :: Maybe FilePath
     , _rlpcDebugOpts   :: DebugOpts
@@ -115,13 +121,24 @@ data Severity = Error
 -- temporary until we have a new doc building system
 type ErrorDoc = String
 
-class Diagnostic e where
-    errorDoc :: e -> ErrorDoc
-
 instance (Monad m) => MonadErrorful e (RLPCT e m) where
     addWound = RLPCT . lift . addWound
     addFatal = RLPCT . lift . addFatal
 
+liftRlpcErrs :: (IsRlpcError e, Monad m)
+             => RLPCT e m a -> RLPCT RlpcError m a
+liftRlpcErrs m = RLPCT . ReaderT $ \r ->
+    mapErrors liftRlpcErr $ runRLPCT >>> (`runReaderT` r) $ m
+
+addRlpcWound :: (IsRlpcError e, Monad m) => e -> RLPCT RlpcError m ()
+addRlpcWound = addWound . liftRlpcErr
+
+addRlpcFatal :: (IsRlpcError e, Monad m) => e -> RLPCT RlpcError m ()
+addRlpcFatal = addWound . liftRlpcErr
+
+rlpc :: (Monad m) => ErrorfulT e m a -> RLPCT e m a
+rlpc = RLPCT . ReaderT . const
+
 ----------------------------------------------------------------------------------
 
 instance Default RLPCOptions where

src/Compiler/RlpcError.hs

@@ -0,0 +1,15 @@
+module Compiler.RlpcError
+    ( RlpcError(..)
+    , IsRlpcError(..)
+    )
+    where
+----------------------------------------------------------------------------------
+import Control.Monad.Errorful
+----------------------------------------------------------------------------------
+
+data RlpcError = RlpcErr String -- temp
+    deriving (Show, Eq)
+
+class IsRlpcError a where
+    liftRlpcErr :: a -> RlpcError
+

src/Control/Monad/Errorful.hs

@@ -6,6 +6,7 @@ module Control.Monad.Errorful
     , runErrorfulT
     , Errorful
     , runErrorful
+    , mapErrors
     , MonadErrorful(..)
     )
     where
@@ -63,3 +64,10 @@ instance (Monad m) => Monad (ErrorfulT e m) where
             Right (a,es) -> runErrorfulT (k a)
             Left e       -> pure (Left e)
 
+mapErrors :: (Monad m) => (e -> e') -> ErrorfulT e m a -> ErrorfulT e' m a
+mapErrors f m = ErrorfulT $ do
+    x <- runErrorfulT m
+    case x of
+        Left  e      -> pure . Left  $ f e
+        Right (a,es) -> pure . Right $ (a, f <$> es)
+

src/Control/Monad/Utils.hs

@@ -0,0 +1,21 @@
+module Control.Monad.Utils
+    ( mapAccumLM
+    )
+    where
+----------------------------------------------------------------------------------
+import Data.Tuple               (swap)
+import Control.Monad.State
+----------------------------------------------------------------------------------
+
+-- | Monadic variant of @mapAccumL@
+
+mapAccumLM :: forall m t s a b. (Monad m, Traversable t)
+           => (s -> a -> m (s, b))
+           -> s
+           -> t a
+           -> m (s, t b)
+mapAccumLM k s t = swap <$> runStateT (traverse k' t) s
+    where
+        k' :: a -> StateT s m b
+        k' a = StateT $ fmap swap <$> flip k a
+

src/Core/Examples.hs

@@ -8,14 +8,13 @@ module Core.Examples
     ( fac3
     , sumList
     , constDivZero
+    , idCase
     ) where
 ----------------------------------------------------------------------------------
 import Core.Syntax
 import Core.TH
 ----------------------------------------------------------------------------------
 
--- TODO: my shitty lexer isn't inserting semicolons
-
 letrecExample :: Program'
 letrecExample = [coreProg|
     pair x y f = f x y;
@@ -181,30 +180,39 @@ constDivZero = [coreProg|
         main = k 3 ((/#) 1 0);
     |]
 
-corePrelude :: Module Name
+idCase :: Program'
-corePrelude = Module (Just ("Prelude", [])) $
+idCase = [coreProg|
-    -- non-primitive defs
-    [coreProg|
         id x = x;
-        k x y = x;
+
-        k1 x y = y;
+        main = id (case Pack{1 0} of
-        s f g x = f x (g x);
+            { 1 -> (+#) 2 3
-        compose f g x = f (g x);
+            })
-        twice f x = f (f x);
+    |]
-        fst p = casePair# p k;
+
-        snd p = casePair# p k1;
+-- corePrelude :: Module Name
-        head l = caseList# l abort# k;
+-- corePrelude = Module (Just ("Prelude", [])) $
-        tail l = caseList# l abort# k1;
+--     -- non-primitive defs
-        _length_cc x xs = (+#) 1 (length xs);
+--     [coreProg|
-        length l = caseList# l 0 length_cc;
+--         id x = x;
-    |]
+--         k x y = x;
-    <>
+--         k1 x y = y;
-    -- primitive constructors need some specialised wiring:
+--         s f g x = f x (g x);
-    Program
+--         compose f g x = f (g x);
-        [ ScDef "False" [] $ Con 0 0
+--         twice f x = f (f x);
-        , ScDef "True" [] $ Con 1 0
+--         fst p = casePair# p k;
-        , ScDef "MkPair" [] $ Con 0 2
+--         snd p = casePair# p k1;
-        , ScDef "Nil" [] $ Con 1 0
+--         head l = caseList# l abort# k;
-        , ScDef "Cons" [] $ Con 2 2
+--         tail l = caseList# l abort# k1;
-        ]
+--         _length_cc x xs = (+#) 1 (length xs);
+--         length l = caseList# l 0 length_cc;
+--     |]
+--     <>
+--     -- primitive constructors need some specialised wiring:
+--     Program
+--         [ ScDef "False" [] $ Con 0 0
+--         , ScDef "True" [] $ Con 1 0
+--         , ScDef "MkPair" [] $ Con 0 2
+--         , ScDef "Nil" [] $ Con 1 0
+--         , ScDef "Cons" [] $ Con 2 2
+--         ]
 

src/Core/HindleyMilner.hs

@@ -0,0 +1,220 @@
+{-|
+Module      : Core.HindleyMilner
+Description : Hindley-Milner type system
+-}
+{-# LANGUAGE LambdaCase #-}
+module Core.HindleyMilner
+    ( Context'
+    , infer
+    , check
+    , checkCoreProg
+    , checkCoreProgR
+    , TypeError(..)
+    , HMError
+    )
+    where
+----------------------------------------------------------------------------------
+import Lens.Micro
+import Lens.Micro.Mtl
+import Data.Maybe               (fromMaybe)
+import Data.Text                qualified as T
+import Data.HashMap.Strict      qualified as H
+import Data.Foldable            (traverse_)
+import Compiler.RLPC
+import Control.Monad            (foldM, void)
+import Control.Monad.Errorful   (Errorful, addFatal)
+import Control.Monad.State
+import Control.Monad.Utils      (mapAccumLM)
+import Core.Syntax
+----------------------------------------------------------------------------------
+
+-- | Annotated typing context -- I have a feeling we're going to want this in the
+-- future.
+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
+    = TyErrCouldNotUnify Type Type
+    -- | @x@ could not be unified with @t@ because @x@ occurs in @t@
+    | TyErrRecursiveType Name Type
+    -- | Untyped, potentially undefined variable
+    | TyErrUntypedVariable Name
+    | TyErrMissingTypeSig Name
+    deriving (Show, Eq)
+
+-- TODO:
+instance IsRlpcError TypeError where
+    liftRlpcErr = RlpcErr . 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
+--
+-- >>> let e = [coreProg|3|]
+-- >>> check [] (TyCon "Bool") e
+-- Left (TyErrCouldNotUnify (TyCon "Bool") (TyCon "Int#"))
+-- >>> check [] (TyCon "Int#") e
+-- Right ()
+
+check :: Context' -> Type -> Expr' -> HMError ()
+check g t1 e = do
+    t2 <- infer g e
+    void $ unify [(t1,t2)]
+
+-- | Typecheck program. I plan to allow for *some* inference in the future, but
+-- in the mean time all top-level binders must have a type annotation.
+checkCoreProg :: Program' -> HMError ()
+checkCoreProg p = scDefs
+            & traverse_ k
+    where
+        scDefs = p ^. programScDefs
+        g = gatherTypeSigs p
+
+        k :: ScDef' -> HMError ()
+        k sc = case lookup scname g of
+             Just t  -> check g t (sc ^. _rhs)
+             Nothing -> addFatal $ TyErrMissingTypeSig scname
+             where scname = sc ^. _lhs._1
+
+-- | @checkCoreProgR p@ returns @p@ if @p@ successfully typechecks.
+checkCoreProgR :: Program' -> RLPC RlpcError Program'
+checkCoreProgR p = do
+    liftRlpcErrs . rlpc . checkCoreProg $ p
+    pure p
+
+-- | Infer the type of an expression under some context.
+--
+-- >>> let g1 = [("id", TyVar "a" :-> TyVar "a")]
+-- >>> let g2 = [("id", (TyVar "a" :-> TyVar "a") :-> TyVar "a" :-> TyVar "a")]
+-- >>> infer g1 [coreExpr|id 3|]
+-- Right TyInt
+-- >>> infer g2 [coreExpr|id 3|]
+-- Left (TyErrCouldNotUnify (TyVar "a" :-> TyVar "a") TyInt)
+
+infer :: Context' -> Expr' -> HMError Type
+infer g e = do
+    (t,cs) <- gather g e
+    -- apply all unified constraints
+    foldr (uncurry subst) t <$> unify cs
+
+-- | A @Constraint@ between two types describes the requirement that the pair
+-- must unify
+type Constraint = (Type, Type)
+
+-- | Type of an expression under some context, and gather the constraints
+-- necessary to unify. Note that this is not the same as @infer@, as the
+-- expression will likely be given a fresh type variable along with a
+-- constraint, rather than the solved type.
+--
+-- For example, if the context says "@id@ has type a -> a," in an application of
+-- @id 3@, the whole application is assigned type @$a0@ and the constraint that
+-- @id@ must unify with type @Int -> $a0@ is generated.
+--
+-- >>> gather [("id", TyVar "a" :-> TyVar "a")] [coreExpr|id 3|]
+-- (TyVar "$a0",[(TyVar "a" :-> TyVar "a",TyInt :-> TyVar "$a0")])
+
+gather :: Context' -> Expr' -> HMError (Type, [Constraint])
+gather = \g e -> runStateT (go g e) ([],0) <&> \ (t,(cs,_)) -> (t,cs) where
+    go :: Context' -> Expr' -> StateT ([Constraint], Int) HMError Type
+    go g = \case
+        Lit (IntL _)  -> pure TyInt
+        Var k         -> lift $ maybe e pure $ lookup k g
+            where e = addFatal $ TyErrUntypedVariable k
+        App f x       -> do
+            tf <- go g f
+            tx <- go g x
+            tfx <- uniqueVar
+            addConstraint tf (tx :-> tfx)
+            pure tfx
+        Let NonRec bs e -> do
+            g' <- buildLetContext g bs
+            go g' e
+        -- TODO letrec, lambda, case
+
+    buildLetContext :: Context' -> [Binding']
+                    -> StateT ([Constraint], Int) HMError Context'
+    buildLetContext = foldM k where
+        k :: Context' -> Binding' -> StateT ([Constraint], Int) HMError Context'
+        k g (x := y) = do
+            ty <- go g y
+            pure ((x,ty) : g)
+
+uniqueVar :: StateT ([Constraint], Int) HMError Type
+uniqueVar = do
+    n <- use _2
+    _2 %= succ
+    pure (TyVar . T.pack $ '$' : 'a' : show n)
+
+addConstraint :: Type -> Type -> StateT ([Constraint], Int) HMError ()
+addConstraint t u = _1 %= ((t, u):)
+
+-- | Unify a list of constraints, meaning that pairs between types are turned
+-- into pairs of type variables and types. A useful thought model is to think of
+-- it as solving an equation such that the unknown variable is the left-hand
+-- side.
+
+unify :: [Constraint] -> HMError Context'
+unify = go mempty where
+    go :: Context' -> [Constraint] -> HMError Context'
+
+    -- nothing left! return accumulated context
+    go g [] = pure g
+
+    go g (c:cs) = case c of
+        -- primitives may of course unify with themselves
+        (TyInt,   TyInt)            -> go g cs
+
+        -- `x` unifies with `x`
+        (TyVar t, TyVar u) | t == u -> go g cs
+
+        -- a type variable `x` unifies with an arbitrary type `t` if `t` does
+        -- not reference `x`
+        (TyVar x, t)                -> unifyTV g x t cs
+        (t, TyVar x)                -> unifyTV g x t cs
+
+        -- two functions may be unified if their domain and codomain unify
+        (a :-> b, x :-> y)          -> go g $ (a,x) : (b,y) : cs
+
+        -- anything else is a failure :(
+        (t,u)                       -> addFatal $ TyErrCouldNotUnify t u
+
+    unifyTV :: Context' -> Name -> Type -> [Constraint] -> HMError Context'
+    unifyTV g x t cs | occurs t   = addFatal $ TyErrRecursiveType x t
+                     | otherwise  = go g' substed
+        where
+            g' = (x,t) : g
+            substed = cs & each . both %~ subst x t
+
+            occurs (a :-> b) = occurs a || occurs b
+            occurs (TyVar y)
+                | x == y     = True
+            occurs _         = False
+
+gatherTypeSigs :: Program b -> Context b
+gatherTypeSigs p = p ^. programTypeSigs
+                 & H.toList
+
+-- | The expression @subst x t e@ substitutes all occurences of @x@ in @e@ with
+-- @t@
+--
+-- >>> subst "a" (TyCon "Int") (TyVar "a")
+-- TyCon "Int"
+-- >>> subst "a" (TyCon "Int") (TyVar "a" :-> TyVar "a")
+-- TyCon "Int" :-> TyCon "Int"
+
+subst :: Name -> Type -> Type -> Type
+subst x t (TyVar y) | x == y  = t
+subst x t (a :-> b)           = subst x t a :-> subst x t b
+subst _ _ e                   = e
+

src/Core/Lex.x

@@ -3,8 +3,10 @@
 Module      : Core.Lex
 Description : Lexical analysis for the core language
 -}
+{-# LANGUAGE OverloadedStrings #-}
 module Core.Lex
     ( lexCore
+    , lexCoreR
     , lexCore'
     , CoreToken(..)
     , SrcError(..)
@@ -15,13 +17,17 @@ module Core.Lex
     where
 import Data.Char (chr)
 import Debug.Trace
+import Data.Text            (Text)
+import Data.Text            qualified as T
+import Data.String          (IsString(..))
 import Core.Syntax
 import Compiler.RLPC
+import Compiler.RlpcError
 import Lens.Micro
 import Lens.Micro.TH
 }
 
-%wrapper "monad"
+%wrapper "monad-strict-text"
 
 $whitechar = [ \t\n\r\f\v]
 $special   = [\(\)\,\;\[\]\{\}]
@@ -68,6 +74,7 @@ rlp :-
     "{"                     { constTok TokenLBrace }
     "}"                     { constTok TokenRBrace }
     ";"                     { constTok TokenSemicolon }
+    "::"                    { constTok TokenHasType }
     "@"                     { constTok TokenTypeApp }
     "{-#"                   { constTok TokenLPragma `andBegin` pragma }
 
@@ -80,7 +87,7 @@ rlp :-
     "where"                 { constTok TokenWhere }
     "Pack"                  { constTok TokenPack } -- temp
 
-    "\\"                    { constTok TokenLambda }
+    "\"                     { constTok TokenLambda }
     "λ"                     { constTok TokenLambda }
     "="                     { constTok TokenEquals }
     "->"                    { constTok TokenArrow }
@@ -90,12 +97,14 @@ rlp :-
     @varsym                 { lexWith TokenVarSym }
     @consym                 { lexWith TokenConSym }
 
-    @decimal                { lexWith (TokenLitInt . read @Int) }
+    @decimal                { lexWith (TokenLitInt . read @Int . T.unpack) }
 
     $white                  { skip }
     \n                      { skip }
 }
 
+-- TODO: negative literals
+
 <pragma>
 {
     "#-}"                   { constTok TokenRPragma `andBegin` 0 }
@@ -134,10 +143,11 @@ data CoreToken = TokenLet
                | TokenLBrace
                | TokenRBrace
                | TokenSemicolon
+               | TokenHasType
                | TokenTypeApp
                | TokenLPragma
                | TokenRPragma
-               | TokenWord String
+               | TokenWord Text
                | TokenEOF
                deriving Show
 
@@ -155,11 +165,11 @@ data SrcErrorType = SrcErrLexical String
 
 type Lexer = AlexInput -> Int -> Alex (Located CoreToken)
 
-lexWith :: (String -> CoreToken) -> Lexer
+lexWith :: (Text -> CoreToken) -> Lexer
-lexWith f (AlexPn _ y x,_,_,s) l = pure $ Located y x l (f $ take l s)
+lexWith f (AlexPn _ y x,_,_,s) l = pure $ Located y x l (f $ T.take l s)
 
 -- | The main lexer driver.
-lexCore :: String -> RLPC SrcError [Located CoreToken]
+lexCore :: Text -> RLPC SrcError [Located CoreToken]
 lexCore s = case m of
     Left e   -> addFatal err
         where err = SrcError
@@ -171,9 +181,12 @@ lexCore s = case m of
     where
         m = runAlex s lexStream
 
+lexCoreR :: Text -> RLPC RlpcError [Located CoreToken]
+lexCoreR = liftRlpcErrs . lexCore
+
 -- | @lexCore@, but the tokens are stripped of location info. Useful for
 -- debugging
-lexCore' :: String -> RLPC SrcError [CoreToken]
+lexCore' :: Text -> RLPC SrcError [CoreToken]
 lexCore' s = fmap f <$> lexCore s
     where f (Located _ _ _ t) = t
 
@@ -188,6 +201,14 @@ data ParseError = ParErrLexical String
                 | ParErrParse
                 deriving Show
 
+-- TODO:
+instance IsRlpcError SrcError where
+    liftRlpcErr = RlpcErr . show
+
+-- TODO:
+instance IsRlpcError ParseError where
+    liftRlpcErr = RlpcErr . show
+
 alexEOF :: Alex (Located CoreToken)
 alexEOF = Alex $ \ st@(AlexState { alex_pos = AlexPn _ y x }) ->
     Right (st, Located y x 0 TokenEOF)

src/Core/Parse.y

@@ -3,10 +3,12 @@
 Module : Core.Parse
 Description : Parser for the Core language
 -}
+{-# LANGUAGE OverloadedStrings #-}
 module Core.Parse
     ( parseCore
     , parseCoreExpr
     , parseCoreProg
+    , parseCoreProgR
     , module Core.Lex -- temp convenience
     , parseTmp
     , SrcError
@@ -19,7 +21,12 @@ import Data.Foldable        (foldl')
 import Core.Syntax
 import Core.Lex
 import Compiler.RLPC
+import Lens.Micro
 import Data.Default.Class   (def)
+import Data.Hashable        (Hashable)
+import Data.Text.IO         qualified as TIO
+import Data.Text            qualified as T
+import Data.HashMap.Strict  qualified as H
 }
 
 %name parseCore Module
@@ -55,6 +62,7 @@ import Data.Default.Class   (def)
       '{-#'           { Located _ _ _ TokenLPragma }
       '#-}'           { Located _ _ _ TokenRPragma }
       ';'             { Located _ _ _ TokenSemicolon }
+      '::'            { Located _ _ _ TokenHasType }
       eof             { Located _ _ _ TokenEOF }
 
 %%
@@ -69,9 +77,20 @@ Eof             : eof           { () }
 
 StandaloneProgram :: { Program Name }
 StandaloneProgram : Program eof                 { $1 }
+                  | eof                         { mempty }
 
 Program         :: { Program Name }
-Program         : ScDefs                        { Program $1 }
+Program         : ScTypeSig ';' Program         { insTypeSig $1 $3 }
+                | ScTypeSig OptSemi             { singletonTypeSig $1 }
+                | ScDef     ';' Program         { insScDef $1 $3 }
+                | ScDef     OptSemi             { singletonScDef $1 }
+
+OptSemi         :: { () }
+OptSemi         : ';'                           { () }
+                | {- epsilon -}                 { () }
+
+ScTypeSig       :: { (Name, Type) }
+ScTypeSig       : Var '::' Type                 { ($1,$3) }
 
 ScDefs          :: { [ScDef Name] }
 ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
@@ -82,6 +101,16 @@ ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
 ScDef           :: { ScDef Name }
 ScDef           : Var ParList '=' Expr          { ScDef $1 $2 $4 }
 
+Type            :: { Type }
+Type            : Type1                         { $1 }
+
+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 }
+
 ParList         :: { [Name] }
 ParList         : Var ParList                   { $1 : $2 }
                 | {- epsilon -}                 { [] }
@@ -119,11 +148,12 @@ Alters          : Alter ';' Alters              { $1 : $3 }
                 | Alter ';'                     { [$1] }
                 | Alter                         { [$1] }
 
+-- TODO: tags should be wrapped in <n> to allow matching against literals
 Alter           :: { Alter Name }
 Alter           : litint ParList '->' Expr      { Alter (AltData $1) $2 $4 }
 
 Expr1           :: { Expr Name }
-Expr1           : litint                        { LitE $ IntL $1 }
+Expr1           : litint                        { Lit $ IntL $1 }
                 | Id                            { Var $1 }
                 | PackCon                       { $1 }
                 | ExprPragma                    { $1 }
@@ -133,8 +163,8 @@ ExprPragma      :: { Expr Name }
 ExprPragma      : '{-#' Words '#-}'      {% exprPragma $2 }
 
 Words           :: { [String] }
-Words           : word Words                    { $1 : $2 }
+Words           : word Words                    { T.unpack $1 : $2 }
-                | word                          { [$1] }
+                | word                          { [T.unpack $1] }
 
 PackCon         :: { Expr Name }
 PackCon         : pack '{' litint litint '}'    { Con $3 $4 }
@@ -171,7 +201,7 @@ parseError (Located y x l _ : _) = addFatal err
 
 parseTmp :: IO (Module Name)
 parseTmp = do
-    s <- readFile "/tmp/t.hs"
+    s <- TIO.readFile "/tmp/t.hs"
     case parse s of
         Left e -> error (show e)
         Right (ts,_) -> pure ts
@@ -190,5 +220,20 @@ exprPragma _           = addFatal err
 astPragma :: [String] -> RLPC SrcError (Expr Name)
 astPragma = pure . read . unwords
 
+insTypeSig :: (Hashable b) => (b, Type) -> Program b -> Program b
+insTypeSig ts = programTypeSigs %~ uncurry H.insert ts
+
+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
+
+parseCoreProgR :: [Located CoreToken] -> RLPC RlpcError Program'
+parseCoreProgR = liftRlpcErrs . parseCoreProg
+
 }
 

src/Core/Syntax.hs

@@ -4,11 +4,15 @@ Description : Core ASTs and the like
 -}
 {-# LANGUAGE PatternSynonyms, OverloadedStrings #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TemplateHaskell #-}
 module Core.Syntax
     ( Expr(..)
     , Type(..)
-    , Literal(..)
+    , pattern TyInt
+    , Lit(..)
     , pattern (:$)
+    , pattern (:@)
+    , pattern (:->)
     , Binding(..)
     , AltCon(..)
     , pattern (:=)
@@ -20,7 +24,9 @@ module Core.Syntax
     , Module(..)
     , Program(..)
     , Program'
+    , unliftScDef
     , programScDefs
+    , programTypeSigs
     , Expr'
     , ScDef'
     , Alter'
@@ -32,82 +38,95 @@ module Core.Syntax
 ----------------------------------------------------------------------------------
 import Data.Coerce
 import Data.Pretty
-import GHC.Generics
 import Data.List                    (intersperse)
 import Data.Function                ((&))
 import Data.String
+import Data.HashMap.Strict          qualified as H
+import Data.Hashable
+import Data.Text                    qualified as T
+import Data.Char
 -- Lift instances for the Core quasiquoters
 import Language.Haskell.TH.Syntax   (Lift)
+import Lens.Micro.TH                (makeLenses)
 import Lens.Micro
 ----------------------------------------------------------------------------------
 
 data Expr b = Var Name
-            | Con Tag Int -- Con Tag Arity
+            | 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)
-            | LitE Literal
+            | Lit Lit
-            | Type Type
+            deriving (Show, Eq, Read, Lift)
-            deriving (Show, Read, Lift)
 
-deriving instance (Eq b) => Eq (Expr b)
+-- deriving instance (Eq b) => Eq (Expr b)
 
-data Type = TyInt
+data Type = TyFun
-          | TyFun
           | TyVar Name
           | TyApp Type Type
-          | TyConApp TyCon [Type]
+          | TyCon Name
           deriving (Show, Read, Lift, Eq)
 
-type TyCon = Name
+pattern TyInt :: Type
+pattern TyInt = TyCon "Int#"
 
 infixl 2 :$
 pattern (:$) :: Expr b -> Expr b -> Expr b 
 pattern f :$ x = App f x
 
+infixl 2 :@
+pattern (:@) :: Type -> Type -> Type
+pattern f :@ x = TyApp f x
+
+infixr 1 :->
+pattern (:->) :: Type -> Type -> Type
+pattern a :-> b = TyApp (TyApp TyFun a) b
+
 {-# COMPLETE Binding :: Binding #-}
 {-# COMPLETE (:=) :: Binding #-}
 data Binding b = Binding b (Expr b)
-    deriving (Show, Read, Lift)
+    deriving (Show, Read, Eq, Lift)
-
-deriving instance (Eq b) => Eq (Binding b)
 
 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)
+    deriving (Show, Read, Eq, Lift)
-
-deriving instance (Eq b) => Eq (Alter b)
 
 data Rec = Rec
          | NonRec
          deriving (Show, Read, Eq, Lift)
 
 data AltCon = AltData Tag
-            | AltLiteral Literal
+            | AltLit Lit
             | Default
             deriving (Show, Read, Eq, Lift)
 
-data Literal = IntL Int
+data Lit = IntL Int
     deriving (Show, Read, Eq, Lift)
 
-type Name = String
+type Name = T.Text
 type Tag = Int
 
 data ScDef b = ScDef b [b] (Expr b)
-    deriving (Show, Lift)
+    deriving (Show, Eq, Lift)
+
+unliftScDef :: ScDef b -> Expr b
+unliftScDef (ScDef _ as e) = Lam as e
 
 data Module b = Module (Maybe (Name, [Name])) (Program b)
     deriving (Show, Lift)
 
-newtype Program b = Program [ScDef b]
+data Program b = Program
-    deriving (Show, Lift)
+    { _programScDefs   :: [ScDef b]
+    , _programTypeSigs :: H.HashMap b Type
+    }
+    deriving (Show, Eq, Lift)
 
-programScDefs :: Lens' (Program b) [ScDef b]
+makeLenses ''Program
-programScDefs = lens coerce (const coerce)
+pure []
 
 type Program' = Program Name
 type Expr' = Expr Name
@@ -116,13 +135,20 @@ type Alter' = Alter Name
 type Binding' = Binding Name
 
 instance IsString (Expr b) where
-    fromString = Var
+    fromString = Var . fromString
 
-instance Semigroup (Program b) where
+instance IsString Type where
-    (<>) = coerce $ (<>) @[ScDef b] 
+    fromString "" = error "IsString Type string may not be empty"
+    fromString s
+        | isUpper c     = TyCon . fromString $ s
+        | otherwise     = TyVar . fromString $ s
+        where (c:_) = s
 
-instance Monoid (Program b) where
+instance (Hashable b) => Semigroup (Program b) where
-    mempty = Program []
+    (<>) = undefined
+
+instance (Hashable b) => Monoid (Program b) where
+    mempty = Program mempty mempty
 
 ----------------------------------------------------------------------------------
 

src/Core/TH.hs

@@ -5,6 +5,7 @@ Description : Core quasiquoters
 module Core.TH
     ( coreExpr
     , coreProg
+    , coreProgT
     , core
     )
     where
@@ -15,10 +16,14 @@ import Language.Haskell.TH.Quote
 import Control.Monad                ((>=>))
 import Compiler.RLPC
 import Data.Default.Class           (def)
+import Data.Text                    qualified as T
 import Core.Parse
 import Core.Lex
+import Core.HindleyMilner           (checkCoreProgR)
 ----------------------------------------------------------------------------------
 
+-- TODO: write in terms of a String -> QuasiQuoter
+
 core :: QuasiQuoter
 core = QuasiQuoter
     { quoteExp = qCore
@@ -43,24 +48,40 @@ coreExpr = QuasiQuoter
     , quoteDec = error "core quasiquotes may only be used in expressions"
     }
 
+-- | Type-checked @coreProg@
+coreProgT :: QuasiQuoter
+coreProgT = QuasiQuoter
+    { quoteExp = qCoreProgT
+    , quotePat = error "core quasiquotes may only be used in expressions"
+    , quoteType = error "core quasiquotes may only be used in expressions"
+    , quoteDec = error "core quasiquotes may only be used in expressions"
+    }
+
 qCore :: String -> Q Exp
-qCore s = case parse s of
+qCore s = case parse (T.pack s) of
     Left e       -> error (show e)
     Right (m,ts) -> lift m
     where
         parse = evalRLPC def . (lexCore >=> parseCore)
 
 qCoreExpr :: String -> Q Exp
-qCoreExpr s = case parseExpr s of
+qCoreExpr s = case parseExpr (T.pack s) of
     Left e       -> error (show e)
     Right (m,ts) -> lift m
     where
         parseExpr = evalRLPC def . (lexCore >=> parseCoreExpr)
 
 qCoreProg :: String -> Q Exp
-qCoreProg s = case parseProg s of
+qCoreProg s = case parse (T.pack s) of
     Left e       -> error (show e)
     Right (m,ts) -> lift m
     where
-        parseProg = evalRLPC def . (lexCore >=> parseCoreProg)
+        parse = evalRLPC def . (lexCoreR >=> parseCoreProgR)
+
+qCoreProgT :: String -> Q Exp
+qCoreProgT s = case parse (T.pack s) of
+    Left e      -> error (show e)
+    Right (m,_) -> lift m
+    where
+        parse = evalRLPC def . (lexCoreR >=> parseCoreProgR >=> checkCoreProgR)
 

src/Core/Utils.hs

@@ -7,7 +7,7 @@ module Core.Utils
     ( bindersOf
     , rhssOf
     , isAtomic
-    , insertModule
+    -- , insertModule
     , extractProgram
     , freeVariables
     , ExprF(..)
@@ -19,6 +19,7 @@ import Data.Functor.Foldable
 import Data.Set                     (Set)
 import Data.Set                     qualified as S
 import Core.Syntax
+import Lens.Micro
 import GHC.Exts                     (IsList(..))
 ----------------------------------------------------------------------------------
 
@@ -32,14 +33,14 @@ rhssOf = fromList . fmap f
 
 isAtomic :: Expr b -> Bool
 isAtomic (Var _)  = True
-isAtomic (LitE _) = True
+isAtomic (Lit _)  = True
 isAtomic _        = False
 
 ----------------------------------------------------------------------------------
 
 -- TODO: export list awareness
-insertModule :: Module b -> Program b -> Program b
+-- insertModule :: Module b -> Program b -> Program b
-insertModule (Module _ m) p = p <> m
+-- insertModule (Module _ p) = programScDefs %~ (<>m)
 
 extractProgram :: Module b -> Program b
 extractProgram (Module _ p) = p

src/Core2Core.hs

@@ -17,6 +17,7 @@ import Data.List
 import Control.Monad.Writer
 import Control.Monad.State
 import Control.Arrow            ((>>>))
+import Data.Text                qualified as T
 import Numeric                  (showHex)
 import Lens.Micro
 import Core.Syntax
@@ -27,7 +28,7 @@ core2core :: Program' -> Program'
 core2core p = undefined
 
 gmPrep :: Program' -> Program'
-gmPrep p = p' <> Program caseScs
+gmPrep p = p' & programScDefs %~ (<>caseScs)
     where
         rhss :: Applicative f => (Expr z -> f (Expr z)) -> Program z -> f (Program z)
         rhss = programScDefs . each . _rhs
@@ -46,8 +47,7 @@ type Floater = StateT [Name] (Writer [ScDef'])
 runFloater :: Floater a -> (a, [ScDef'])
 runFloater = flip evalStateT ns >>> runWriter
     where
-        -- TODO: safer, uncapturable names
+        ns = [ T.pack $ "$nonstrict_case_" ++ showHex n "" | n <- [0..] ]
-        ns = [ "nonstrict_case_" ++ showHex n "" | n <- [0..] ]
 
 -- TODO: formally define a "strict context" and reference that here
 -- the returned ScDefs are guaranteed to be free of non-strict cases.
@@ -56,7 +56,7 @@ floatNonStrictCases g = goE
     where
         goE :: Expr' -> Floater Expr'
         goE (Var k)             = pure (Var k)
-        goE (LitE l)            = pure (LitE l)
+        goE (Lit l)             = pure (Lit l)
         goE (Case e as)         = pure (Case e as)
         goE (Let Rec bs e)      = Let Rec <$> bs' <*> goE e
             where bs' = travBs goE bs
@@ -78,7 +78,7 @@ floatNonStrictCases g = goE
         goC (f :$ x)            = (:$) <$> goC f <*> goC x
         goC (Let r bs e)        = Let r <$> bs' <*> goE e
             where bs' = travBs goC bs
-        goC (LitE l)            = pure (LitE l)
+        goC (Lit l)             = pure (Lit l)
         goC (Var k)             = pure (Var k)
         goC (Con t as)          = pure (Con t as)
 

src/GM.hs

@@ -22,7 +22,10 @@ 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 Text.Printf
 import Text.PrettyPrint             hiding ((<>))
 import Text.PrettyPrint.HughesPJ    (maybeParens)
@@ -281,7 +284,7 @@ step st = case head (st ^. gmCode) of
                 m = st ^. gmEnv
                 s = st ^. gmStack
                 h = st ^. gmHeap
-                n' = show n
+                n' = show n ^. packed
 
         -- Core Rule 2. (no sharing)
         -- pushIntI :: Int -> GmState
@@ -582,7 +585,7 @@ compiledPrims =
         binop k i = (k, 2, [Push 1, Eval, Push 1, Eval, i, Update 2, Pop 2, Unwind])
 
 buildInitialHeap :: Program' -> (GmHeap, Env)
-buildInitialHeap (Program ss) = mapAccumL allocateSc mempty compiledScs
+buildInitialHeap (view programScDefs -> ss) = mapAccumL allocateSc mempty compiledScs
     where
         compiledScs = fmap compileSc ss <> compiledPrims
 
@@ -612,12 +615,13 @@ buildInitialHeap (Program ss) = mapAccumL allocateSc mempty compiledScs
             | k `elem` domain  = [Push n]
             | otherwise        = [PushGlobal k]
             where
-                n = fromMaybe (error $ "undeclared var: " <> k) $ lookupN k g
+                n = fromMaybe err $ lookupN k g
+                err = error $ "undeclared var: " <> (k ^. unpacked)
                 domain = f `mapMaybe` g
                 f (NameKey n, _) = Just n
                 f _              = Nothing
 
-        compileC _ (LitE l)  = compileCL l
+        compileC _ (Lit l)   = compileCL l
 
         -- >> [ref/compileC]
         compileC g (App f x) = compileC g x
@@ -661,16 +665,16 @@ buildInitialHeap (Program ss) = mapAccumL allocateSc mempty compiledScs
 
         compileC _ _ = error "yet to be implemented!"
 
-        compileCL :: Literal -> Code
+        compileCL :: Lit -> Code
         compileCL (IntL n) = [PushInt n]
 
-        compileEL :: Literal -> Code
+        compileEL :: Lit -> Code
         compileEL (IntL n) = [PushInt n]
 
         -- compile an expression in a strict context such that a pointer to the
         -- expression is left on top of the stack in WHNF
         compileE :: Env -> Expr' -> Code
-        compileE _ (LitE l) = compileEL l
+        compileE _ (Lit l) = compileEL l
         compileE g (Let NonRec bs e) =
                 -- we use compileE instead of compileC
                 mconcat binders <> compileE g' e <> [Slide d]
@@ -738,8 +742,8 @@ buildInitialHeap (Program ss) = mapAccumL allocateSc mempty compiledScs
         argOffset :: Int -> Env -> Env
         argOffset n = each . _2 %~ (+n)
 
-idPack :: Tag -> Int -> String
+showCon :: (IsText a) => Tag -> Int -> a
-idPack t n = printf "Pack{%d %d}" t n
+showCon t n = printf "Pack{%d %d}" t n ^. packed
 
 ----------------------------------------------------------------------------------
 
@@ -855,12 +859,12 @@ showNodeAt = showNodeAtP 0
 showNodeAtP :: Int -> GmState -> Addr -> Doc
 showNodeAtP p st a = case hLookup a h of
     Just (NNum n)        -> int n <> "#"
-    Just (NGlobal _ _)   -> text name
+    Just (NGlobal _ _)   -> textt name
         where
             g = st ^. gmEnv
             name = case lookup a (swap <$> g) of
                 Just (NameKey n)     -> n
-                Just (ConstrKey t n) -> idPack t n
+                Just (ConstrKey t n) -> showCon t n
                 _                    -> errTxtInvalidAddress
     -- TODO: left-associativity
     Just (NAp f x)       -> pprec $ showNodeAtP (p+1) st f
@@ -877,7 +881,7 @@ showNodeAtP p st a = case hLookup a h of
         pprec = maybeParens (p > 0)
 
 showSc :: GmState -> (Name, Addr) -> Doc
-showSc st (k,a) = "Supercomb " <> qquotes (text k) <> colon
+showSc st (k,a) = "Supercomb " <> qquotes (textt k) <> colon
                $$ code
     where
         code = case hLookup a (st ^. gmHeap) of
@@ -900,6 +904,9 @@ showInstr (CaseJump alts) = "CaseJump" $$ nest pprTabstop alternatives
         alternatives = foldr (\a acc -> showAlt a $$ acc) mempty alts
 showInstr i = text $ show i
 
+textt :: (IsText a) => a -> Doc
+textt t = t ^. unpacked & text
+
 ----------------------------------------------------------------------------------
 
 lookupN :: Name -> Env -> Maybe Addr
@@ -975,7 +982,8 @@ resultOf p = do
         h = st ^. gmHeap
 
 resultOfExpr :: Expr' -> Maybe Node
-resultOfExpr e = resultOf $ Program
+resultOfExpr e = resultOf $
+    mempty & programScDefs .~
                 [ ScDef "main" [] e
                 ]
 

tst/Arith.hs

@@ -6,6 +6,7 @@ module Arith
     ) where
 ----------------------------------------------------------------------------------
 import Data.Functor.Classes             (eq1)
+import Lens.Micro
 import Core.Syntax
 import GM
 import Test.QuickCheck
@@ -48,7 +49,7 @@ instance Arbitrary ArithExpr where
                     -- i don't feel like dealing with division at the moment
                     [ IntA <$> int
                     , NegateA <$> arbitrary
-                    -- , IdA <$> arbitrary
+                    , IdA <$> arbitrary
                     , b (:+)
                     , b (:-)
                     , b (:*)
@@ -70,13 +71,13 @@ instance Arbitrary ArithExpr where
 --         coreResult  = evalCore (toCore e)
 
 toCore :: ArithExpr -> Program'
-toCore expr = Program
+toCore expr = mempty & programScDefs .~
         [ ScDef "id" ["x"] $ Var "x"
         , ScDef "main" [] $ go expr
         ]
     where
         go :: ArithExpr -> Expr'
-        go (IntA n)    = LitE (IntL n)
+        go (IntA n)    = Lit (IntL n)
         go (NegateA e) = "negate#" :$ go e
         go (IdA e)     = "id" :$ go e
         go (a :+ b)    = f "+#" a b

tst/Core/HindleyMilnerSpec.hs

@@ -0,0 +1,46 @@
+{-# LANGUAGE QuasiQuotes, OverloadedStrings #-}
+module Core.HindleyMilnerSpec
+    ( spec
+    )
+    where
+----------------------------------------------------------------------------------
+import Core.Syntax
+import Core.TH                  (coreExpr)
+import Core.HindleyMilner
+import Control.Monad.Errorful
+import Data.Either              (isLeft)
+import Test.Hspec
+----------------------------------------------------------------------------------
+
+-- TODO: more tests. preferrably property-based. lol.
+spec :: Spec
+spec = do
+    it "should infer `id 3` :: Int" $
+        let g = [ ("id", "a" :-> "a") ]
+        in infer' g [coreExpr|id 3|] `shouldBe` Right TyInt
+
+    it "should not infer `id 3` when `id` is specialised to `a -> a`" $
+        let g = [ ("id", ("a" :-> "a") :-> "a" :-> "a") ]
+        in infer' g [coreExpr|id 3|] `shouldSatisfy` isLeft
+
+    -- TODO: property-based tests for let
+    it "should infer `let x = 3 in id x` :: Int" $
+        let g = [ ("id", "a" :-> "a") ]
+            e = [coreExpr|let {x = 3} in id x|]
+        in infer' g e `shouldBe` Right TyInt
+
+    it "should infer `let x = 3; y = 2 in (+#) x y` :: Int" $
+        let g = [ ("+#", TyInt :-> TyInt :-> TyInt) ]
+            e = [coreExpr|let {x=3;y=2} in (+#) x y|]
+        in infer' g e `shouldBe` Right TyInt
+    
+    it "should find `3 :: Bool` contradictory" $
+        let e = [coreExpr|3|]
+        in check' [] (TyCon "Bool") e `shouldSatisfy` isLeft
+
+infer' :: Context' -> Expr' -> Either TypeError Type
+infer' g e = fmap fst . runErrorful $ infer g e
+
+check' :: Context' -> Type -> Expr' -> Either TypeError ()
+check' g t e = fmap fst . runErrorful $ check g t e
+

tst/Core/ParseSpec.hs

@@ -0,0 +1,40 @@
+module Core.ParseSpec
+    ( spec
+    )
+    where
+----------------------------------------------------------------------------------
+import CoreSyntax
+import Core.Syntax
+import Compiler.JustRun
+import Compiler.RlpcError
+import Control.Monad                ((<=<))
+import Data.Coerce
+import Data.Text                    qualified as T
+import Data.Functor.Classes         (Eq1(..))
+import Test.Hspec
+import Test.QuickCheck
+----------------------------------------------------------------------------------
+
+spec :: Spec
+spec = do
+    it "should be a right-inverse to the unparser \
+        \up to source code congruency" $
+        withMaxSuccess 20 $ property $
+            \p -> (unparse <=< parse) p ~== Right p
+
+    -- TODO: abitrary ASTs
+    -- it "should be a right-inverse to the unparser\
+    --     \up to source code congruency" $
+    --     property $ \p -> (parse <=< unparse) p == Right p
+
+(~==) :: (Eq1 f) => f ProgramSrc -> f ProgramSrc -> Bool
+(~==) = liftEq congruentSrc
+
+infix 4 ~==
+
+parse :: ProgramSrc -> Either RlpcError Program'
+parse (ProgramSrc s) = justParseSrc (T.unpack s)
+
+unparse :: Program' -> Either RlpcError ProgramSrc
+unparse = Right . unparseCoreProg
+

tst/CoreSyntax.hs

@@ -0,0 +1,303 @@
+{-# LANGUAGE OverloadedStrings, LambdaCase, GeneralisedNewtypeDeriving #-}
+module CoreSyntax
+    ( ProgramSrc(..)
+    , congruentSrc
+    , unparseCoreProg
+    )
+    where
+----------------------------------------------------------------------------------
+import Core.Syntax
+import Compiler.JustRun             (justParseSrc)
+import Control.Arrow                ((>>>), (&&&))
+import Control.Monad
+import Data.List                    (intersperse)
+import Data.Coerce                  (coerce)
+import Data.Text                    (Text)
+import Data.Text                    qualified as T
+import Data.HashMap.Strict          qualified as H
+import Test.QuickCheck
+import Text.PrettyPrint             hiding ((<>))
+import Data.Functor                 ((<&>))
+import Data.Function                ((&), on)
+import Data.String                  (IsString(..))
+import Lens.Micro.Platform
+import Lens.Micro.Platform.Internal (IsText(..))
+----------------------------------------------------------------------------------
+
+newtype ProgramSrc = ProgramSrc Text
+    deriving (Show, Read, Eq, Semigroup, Monoid, IsString)
+
+instance Arbitrary ProgramSrc where
+    arbitrary = sized genProg where
+
+        genProg :: Int -> Gen ProgramSrc
+        genProg n = do
+            -- in generating a program, we create a random list of sc names and
+            -- assign them type signatures and definitions in random order.
+            ns <- replicateM n genName
+               -- generate a typesig and def for each name
+            ns & each %~ (genTySig &&& genScDef)
+               -- [(typesig, scdef)] -> [typesigs and scdefs]
+               & uncurry (++) . unzip
+               -- [Gen Text] -> Gen [Text]
+               & sequenceA
+               -- shuffle order of tysigs and scdefs
+               >>= shuffle
+               -- terminate each tysig and scdef with a semicolon with a blank
+               -- line for legibility
+               <&> intersperse ";\n\n"
+               -- mconcat into a single body of text
+               <&> mconcat
+               -- she's done! put a bow on her! :D
+               <&> ProgramSrc
+
+        genTySig :: Name -> Gen Text
+        genTySig n = conseq [pure n, ws, pure "::", ws, genTy]
+
+        genScDef :: Name -> Gen Text
+        genScDef n = conseq [pure n, ws, pure "=", ws, genExpr]
+
+        genExpr :: Gen Text
+        genExpr = gen 4 0 where
+            gen 0 _ = oneof
+                [ genVar
+                , genLit
+                ]
+            gen n p = oneof
+                [ gen 0 p
+                , wrapParens <$> gen n' 0
+                , genApp n p
+                , genLet n p
+                -- , genLam n p
+                -- , genCase n p
+                ]
+                where n' = next n
+
+            genVar = oneof
+                [ genName
+                , genCon
+                , wrapParens <$> genSymName
+                , wrapParens <$> genSymCon
+                ]
+
+            genCase n p = conseq [ pure "case", ws1, gen n' 0, ws1, pure "of"
+                                 , pure "{", alts, pure "}"
+                                 ]
+                        <&> pprec 0 p
+                where
+                    n' = next n
+                    alts = chooseSize (1,6) (listOf1 alt)
+                         <&> intersperse ";"
+                         <&> mconcat
+                    alt = conseq [ tag, ws, pure "->", ws1, gen n' 0 ]
+                    tag = T.pack . show <$> chooseInt (0,maxBound)
+
+            genLit = T.pack . show <$> chooseInt (0,maxBound)
+
+            genApp n p = chooseSize (2,10) (listOf1 (gen n' 1))
+                     <&> pprec 0 p . mconcat . intersperse " "
+                where
+                    n' = next n
+
+            genLet n p = conseq [ letw, ws, pure "{", ws, binds
+                                , ws, pure "}", ws, pure "in"
+                                , ws1, gen n' 0
+                                ]
+                where
+                    letw = arbitrary <&> \case
+                        Rec    -> "letrec"
+                        NonRec -> "let"
+                    binds = chooseSize (1,6) (listOf1 bind)
+                        <&> intersperse ";"
+                        <&> mconcat
+                    bind = conseq [var, ws, pure "=", ws, gen n' 0]
+                    var = oneof [genName, wrapParens <$> genSymName]
+                    n' = next n
+
+            genLam n p = conseq [l, ws, bs, ws, pure "->", ws, gen n' 0]
+                     <&> pprec 0 p
+                where
+                    -- whitespace because reserved op shenanigans :3
+                    l = elements [" \\ ", "λ"]
+                    n' = next n
+                    bs = chooseSize (0,6) (listOf1 genName)
+                     <&> mconcat
+
+            next = (`div` 2)
+
+        genTy :: Gen Text
+        genTy = gen 4 where
+            gen 0 = genCon
+            gen n = oneof
+                [ gen 0
+                -- function types
+                , conseq [gen n', ws, pure "->", ws, gen n']
+                -- TODO: type applications (remember precedence lol)
+                ]
+                where n' = n `div` 2
+
+instance Arbitrary Rec where
+    arbitrary = elements [Rec,NonRec]
+
+chooseSize :: (Int, Int) -> Gen a -> Gen a
+chooseSize (a,b) g = do
+    n <- chooseInt (a,b)
+    resize n g
+
+-- | @pprec q p s@ wraps @s@ with parens when @p <= q@
+pprec :: (IsString a, Monoid a) => Int -> Int -> a -> a
+pprec maxp p
+    | p <= maxp = id
+    | otherwise = wrapParens
+
+wrapParens :: (IsString a, Monoid a) => a -> a
+wrapParens t = "(" <> t <> ")"
+
+conseq :: (Applicative f, Monoid m, Traversable t)
+       => t (f m)
+       -> f m
+conseq tfm = sequenceA tfm <&> the_cool_kid's_concat
+    -- me when `concat` is generalised in the container but specialised in the
+    -- value, and `mconcat` is specialised in the container but generalised in
+    -- the value. shoutout `foldMap id`
+    where the_cool_kid's_concat = foldMap id
+
+genName :: Gen Name
+genName = T.pack <$> liftA2 (:) small namechars where
+    small = elements ['a'..'z']
+
+genCon :: Gen Name
+genCon = T.pack <$> liftA2 (:) large namechars where
+    large = elements ['A'..'Z']
+
+genSymName :: Gen Name
+genSymName = T.pack <$> liftA2 (:) symbol symchars where
+    symbol = elements nameSymbols
+
+genSymCon :: Gen Name
+genSymCon = T.pack . (':' :) <$> symchars
+
+namechars :: Gen String
+namechars = liftArbitrary namechar where
+    namechar :: Gen Char
+    namechar = elements $ ['a'..'z'] <> ['A'..'Z'] <> ['0'..'9'] <> "'"
+
+nameSymbols :: [Char]
+nameSymbols = "!#$%&*+./<=>?@^|-~"
+
+symchars :: Gen String
+symchars = liftArbitrary symchar where
+    symchar = elements $ ':' : nameSymbols
+
+txt :: (IsText t) => t -> Doc
+txt t = t ^. unpacked & text
+
+ws :: (IsString a) => Gen a
+ws = elements [""," ", "  "]
+
+ws1 :: (IsString a) => Gen a
+ws1 = elements [" ", "  "]
+
+----------------------------------------------------------------------------------
+
+-- | Two bodies of source code are considered congruent iff the parser produces
+-- identical ASTs for both.
+congruentSrc :: ProgramSrc -> ProgramSrc -> Bool
+congruentSrc = (==) `on` (justParseSrc . T.unpack . coerce)
+
+----------------------------------------------------------------------------------
+
+-- TODO: unparseCoreProg :: Program -> [CoreToken]
+-- womp womp.
+
+-- TODO: implement shrink
+
+-- | @unparseCoreProg@ should be inverse to @parseCoreProg@ up to source code
+-- congruency, newtype coercion and errors handling.
+unparseCoreProg :: Program' -> ProgramSrc
+unparseCoreProg p = unparseTypeSigs (p ^. programTypeSigs)
+                 <> unparseScDefs (p ^. programScDefs)
+
+unparseTypeSigs :: H.HashMap Name Type -> ProgramSrc
+unparseTypeSigs = H.foldrWithKey f mempty
+    where f k v a = unparseTypeSig k v <> ";\n\n" <> a
+
+unparseTypeSig :: Name -> Type -> ProgramSrc
+unparseTypeSig n t = unparseName n <> " :: " <> unparseType t
+
+unparseName :: Name -> ProgramSrc
+unparseName n
+    | T.head n `elem` (':' : nameSymbols)   = coerce $ wrapParens n
+    | otherwise                             = coerce n
+
+unparseType :: Type -> ProgramSrc
+unparseType = go 0 where
+    go :: Int -> Type -> ProgramSrc
+    -- (:->) is a special case of TyApp, but we want the infix syntax
+    go p (a :-> b)          = a : assocFun b
+                            <&> go 1
+                            & coerce (T.intercalate " -> ")
+                            & pprec 0 p
+    go p a@(TyApp f x)      = assocApp a
+                            <&> go 1
+                            & coerce (T.intercalate " ")
+                            & pprec 1 p
+    go _ TyFun              = "(->)"
+    go _ (TyCon a)          = unparseName a
+    go _ (TyVar a)          = unparseName a
+
+    assocFun :: Type -> [Type]
+    assocFun (a :-> b) = a : assocFun b
+    assocFun x         = [x]
+
+    assocApp :: Type -> [Type]
+    assocApp (TyApp f x) = assocApp f ++ [x]
+    assocApp x           = [x]
+
+unparseScDefs :: [ScDef'] -> ProgramSrc
+unparseScDefs = foldr f mempty where
+    f sc a = unparseScDef sc <> ";\n\n" <> a
+
+unparseScDef :: ScDef' -> ProgramSrc
+unparseScDef (ScDef n as e) = (unparseName <$> (n:as)) <> ["=", unparseExpr e]
+                            & coerce (T.intercalate " ")
+
+unparseExpr :: Expr' -> ProgramSrc
+unparseExpr = go 0 where
+    go :: Int -> Expr' -> ProgramSrc
+    go _ (Var n)        = unparseName n
+    go _ (Con t a)      = mconcat ["Pack{",srcShow t," ",srcShow a,"}"]
+    go _ (Lit l)        = unparseLit l
+    go p a@(App _ _)    = srci " " (go 1 <$> assocApp a)
+                        & pprec 0 p
+    go p (Lam bs e)     = "λ" <> srci " " (unparseName <$> bs)
+                              <> " -> " <> go 0 e
+                        & pprec 0 p
+    go p (Let r bs e)   = mconcat [lw," { ",bs'," } in ",go 0 e]
+                        & pprec 0 p
+        where
+            lw = case r of { NonRec -> "let"; Rec -> "letrec" }
+            bs' = srci "; " $ unparseBinding <$> bs
+    go p (Case e as)    = mconcat ["case ",go 0 e," of {",as',"}"]
+                        & pprec 0 p
+        where as' = srci "; " (unparseAlter <$> as)
+
+    assocApp (App f x) = assocApp f ++ [x]
+    assocApp f         = [f]
+
+    srci :: ProgramSrc -> [ProgramSrc] -> ProgramSrc
+    srci = coerce T.intercalate
+
+unparseBinding :: Binding' -> ProgramSrc
+unparseBinding (k := v) = mconcat [unparseName k, " = ", unparseExpr v]
+
+unparseLit :: Lit -> ProgramSrc
+unparseLit (IntL n) = srcShow n
+
+srcShow :: (Show a) => a -> ProgramSrc
+srcShow = coerce . T.pack . show
+
+unparseAlter :: Alter' -> ProgramSrc
+unparseAlter (Alter (AltData t) as e)   = srcShow t <> " " <> coerce (T.unwords as)
+                                       <> " -> " <> unparseExpr e
+

tst/GMSpec.hs

@@ -21,7 +21,7 @@ spec = do
         resultOf [coreProg|id x = x; main = (id (-#)) 3 2;|] `shouldBe` Just (NNum 1)
 
     it "should correctly evaluate arbitrary arithmetic" $ do
-        property $ \e ->
+        withMaxSuccess 40 $ property $ \e ->
             let arithRes = Just (evalArith e)
                 coreRes  = evalCore e
             in coreRes `shouldBe` arithRes
@@ -36,3 +36,6 @@ spec = do
         it "k 3 ((/#) 1 0)" $ do
             resultOf Ex.constDivZero `shouldBe` Just (NNum 3)
 
+        it "id (case ... of { ... })" $ do
+            resultOf Ex.idCase `shouldBe` Just (NNum 5)
+