diff --git a/grin/grin.cabal b/grin/grin.cabal
index 9156ccc3..995a6858 100644
--- a/grin/grin.cabal
+++ b/grin/grin.cabal
@@ -66,6 +66,18 @@ library
     Grin.PrimOpsPrelude
     Grin.Nametable
     Grin.Research
+    Grin.ExtendedSyntax.Syntax
+    Grin.ExtendedSyntax.SyntaxDefs
+    Grin.ExtendedSyntax.Grin
+    Grin.ExtendedSyntax.EffectMap
+    Grin.ExtendedSyntax.Parse
+    Grin.ExtendedSyntax.Parse.AST
+    Grin.ExtendedSyntax.Parse.Basic
+    Grin.ExtendedSyntax.Parse.TypeEnv
+    Grin.ExtendedSyntax.Pretty
+    Grin.ExtendedSyntax.TH
+    Grin.ExtendedSyntax.TypeEnv
+    Grin.ExtendedSyntax.TypeEnvDefs
     Pipeline.Eval
     Pipeline.Optimizations
     Pipeline.Pipeline
@@ -85,6 +97,9 @@ library
     Test.IO
     Test.Test
     Test.Util
+    Test.ExtendedSyntax.Assertions
+    Test.ExtendedSyntax.Old.Grammar
+    Test.ExtendedSyntax.Old.Test
     Transformations.BindNormalisation
     Transformations.CountVariableUse
     Transformations.EffectMap
@@ -94,6 +109,7 @@ library
     Transformations.StaticSingleAssignment
     Transformations.UnitPropagation
     Transformations.Util
+    Transformations.ExtendedSyntax.Conversion
     Transformations.Optimising.ArityRaising
     Transformations.Optimising.CaseCopyPropagation
     Transformations.Optimising.CaseHoisting
@@ -225,6 +241,8 @@ test-suite grin-test
                      , inline-c
 
   other-modules:
+                     ExtendedSyntax.ParserSpec
+                     Transformations.ExtendedSyntax.ConversionSpec
                      Transformations.Simplifying.RegisterIntroductionSpec
                      Transformations.Simplifying.CaseSimplificationSpec
                      Transformations.Simplifying.SplitFetchSpec
diff --git a/grin/src/Grin/ExtendedSyntax/EffectMap.hs b/grin/src/Grin/ExtendedSyntax/EffectMap.hs
new file mode 100644
index 00000000..0531344e
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/EffectMap.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, TemplateHaskell #-}
+module Grin.ExtendedSyntax.EffectMap
+  ( EffectMap(..)
+  , Effects(..)
+  , hasPossibleSideEffect
+  , storesEff
+  , primopEff
+  , updatesEff
+  , hasTrueSideEffect
+  ) where
+
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Monoid
+
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+
+import Lens.Micro.Platform
+
+import Grin.ExtendedSyntax.Grin
+
+-- | Contains the name of all the effectful primops used by the function,
+-- and a list of heap locations updated by it.
+data Effects
+  = Effects
+  { _effectfulPrimops :: Set Name
+  , _updateLocs       :: Set Int
+  , _storeLocs        :: Set Int
+  }
+  deriving (Eq, Ord, Show)
+
+instance Semigroup Effects where
+  (<>) (Effects primops1 updateLocs1 storeLocs1) (Effects primops2 updateLocs2 storeLocs2)
+    = Effects (primops1 <> primops2) (updateLocs1 <> updateLocs2) (storeLocs1 <> storeLocs2)
+
+instance Monoid Effects where
+  mempty = Effects mempty mempty mempty
+
+
+
+-- | Mapping of function names to their respective side effects.
+newtype EffectMap = EffectMap { _effects :: Map Name Effects }
+  deriving (Eq, Ord, Show, Semigroup, Monoid)
+
+concat <$> mapM makeLenses [''Effects, '' EffectMap]
+
+
+primopEff :: Name -> Effects
+primopEff f = Effects (Set.singleton f) mempty mempty
+
+updatesEff :: [Int] -> Effects
+updatesEff locs = Effects mempty (Set.fromList locs) mempty
+
+storesEff :: [Int] -> Effects
+storesEff locs = Effects mempty mempty (Set.fromList locs)
+
+
+hasSomeEffect :: (Effects -> Set a) -> Name -> EffectMap -> Bool
+hasSomeEffect selectEff f (EffectMap effMap)
+  | Just effects <- Map.lookup f effMap
+  = not . null . selectEff $ effects
+  | otherwise = False
+
+hasSideEffectingPrimop :: Name -> EffectMap -> Bool
+hasSideEffectingPrimop = hasSomeEffect _effectfulPrimops
+
+hasUpdates :: Name -> EffectMap -> Bool
+hasUpdates = hasSomeEffect _updateLocs
+
+hasStores :: Name -> EffectMap -> Bool
+hasStores = hasSomeEffect _storeLocs
+
+-- | Checks whether a function has a true side effect
+-- , meaning it calls a side-effecting primop.
+hasTrueSideEffect :: Name -> EffectMap -> Bool
+hasTrueSideEffect = hasSideEffectingPrimop
+
+-- | Checks whether a function has a possible side effect
+-- , meaning it either has a true side effect
+-- , or it updates a location, which can cause a side effect.
+hasPossibleSideEffect :: Name -> EffectMap -> Bool
+hasPossibleSideEffect f effMap = hasTrueSideEffect f effMap || hasUpdates f effMap
diff --git a/grin/src/Grin/ExtendedSyntax/Grin.hs b/grin/src/Grin/ExtendedSyntax/Grin.hs
new file mode 100644
index 00000000..67e2b10b
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Grin.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE FlexibleInstances, DeriveFunctor, RankNTypes, LambdaCase #-}
+module Grin.ExtendedSyntax.Grin
+  ( module Grin.ExtendedSyntax.Grin
+  , module Grin.ExtendedSyntax.Syntax
+  ) where
+
+import Data.Functor.Foldable as Foldable
+import Debug.Trace (trace)
+import Lens.Micro.Platform
+import Data.Maybe
+import Data.Text (pack, unpack)
+import Data.List (nub)
+
+import Grin.ExtendedSyntax.Syntax
+import Grin.ExtendedSyntax.TypeEnvDefs
+
+class FoldNames n where
+  foldNames :: (Monoid m) => (Name -> m) -> n -> m
+
+instance FoldNames Val where
+  foldNames f = \case
+    ConstTagNode  _tag vals -> foldMap f vals
+    Var name                -> f name
+    _                       -> mempty
+
+instance FoldNames BPat where
+  foldNames f = \case
+    VarPat v    -> f v
+    AsPat v val -> f v <> foldNames f val
+
+
+instance FoldNames CPat where
+  foldNames f = \case
+    NodePat _ names -> foldMap f names
+    LitPat _        -> mempty
+    DefaultPat      -> mempty
+
+instance FoldNames n => FoldNames [n] where
+  foldNames f = foldMap (foldNames f)
+
+dCoAlg :: (a -> String) -> (a -> ExpF b) -> (a -> ExpF b)
+dCoAlg dbg f = f . (\x -> trace (dbg x) x)
+
+dAlg :: (b -> String) -> (ExpF a -> b) -> (ExpF a -> b)
+dAlg dbg f = (\x -> trace (dbg x) x) . f
+
+match :: Traversal' a b -> a -> Bool
+match t x = isJust $ x ^? t
+
+isLit :: Val -> Bool
+isLit = match _Lit
+
+_Lit :: Traversal' Val Lit
+_Lit f (Lit l) = Lit <$> f l
+_Lit _ rest    = pure rest
+
+_Var :: Traversal' Val Name
+_Var f (Var name) = Var <$> f name
+_Var _ rest       = pure rest
+
+_CNode :: Traversal' Val (Tag, [Name])
+_CNode f (ConstTagNode tag params) = uncurry ConstTagNode <$> f (tag, params)
+_CNode _ rest = pure rest
+
+isBasicCPat :: CPat -> Bool
+isBasicCPat = \case
+  LitPat _ -> True
+  _        -> False
+
+isBasicValue :: Val -> Bool
+isBasicValue Unit{}   = True
+isBasicValue Lit{}    = True
+isBasicValue _'       = True
+
+isPrimitiveExp :: Exp -> Bool
+isPrimitiveExp = \case
+  SApp    _ _ -> True
+  SReturn _   -> True
+  SStore  _   -> True
+  SFetch  _   -> True
+  SUpdate _ _ -> True
+  _           -> False
+
+isSimpleExp :: Exp -> Bool
+isSimpleExp e | isPrimitiveExp e = True
+isSimpleExp e = case e of
+  SBlock  _   -> True
+  _           -> False
+
+unpackName :: Name -> String
+unpackName (NM name) = unpack name
+
+packName :: String -> Name
+packName = NM . pack
+
+showTS :: Show a => a -> Name
+showTS = packName . show
+
+concatPrograms :: [Program] -> Program
+concatPrograms prgs = Program (nub $ concat exts) (concat defs) where
+  (exts, defs) = unzip [(e, d) | Program e d <- prgs]
+
+-- NOTE: @ is no longer an allowed special (due to as-patterns)
+-- indetifier rules for parser and pretty printer
+allowedSpecial :: String
+allowedSpecial = "._':!-"
+
+allowedInitial :: String
+allowedInitial = "._" ++ ['a'..'z'] ++ ['A'..'Z']
diff --git a/grin/src/Grin/ExtendedSyntax/Parse.hs b/grin/src/Grin/ExtendedSyntax/Parse.hs
new file mode 100644
index 00000000..2a076550
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Parse.hs
@@ -0,0 +1,18 @@
+module Grin.ExtendedSyntax.Parse
+  ( module Grin.ExtendedSyntax.Parse.AST
+  , module Grin.ExtendedSyntax.Parse.TypeEnv
+  , module Grin.ExtendedSyntax.Parse
+  ) where
+
+import Data.Void
+import Data.Text
+import Text.Megaparsec
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.TypeEnvDefs
+
+import Grin.ExtendedSyntax.Parse.AST
+import Grin.ExtendedSyntax.Parse.TypeEnv
+
+parseGrinWithTypes :: String -> Text -> Either (ParseError Char Void) (TypeEnv, Exp)
+parseGrinWithTypes filename content = (,) <$> parseMarkedTypeEnv filename content <*> parseGrin filename content
diff --git a/grin/src/Grin/ExtendedSyntax/Parse/AST.hs b/grin/src/Grin/ExtendedSyntax/Parse/AST.hs
new file mode 100644
index 00000000..0287277c
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Parse/AST.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE TupleSections, LambdaCase, OverloadedStrings #-}
+
+module Grin.ExtendedSyntax.Parse.AST
+  ( parseGrin
+  , parseProg
+  , parseDef
+  , parseExpr
+  ) where
+
+import Data.Char
+import Data.Void
+import Data.Text (Text)
+import qualified Data.Text as T
+
+import Control.Applicative (empty)
+import Control.Monad (void, mzero)
+import Text.Megaparsec
+import qualified Text.Megaparsec.Char.Lexer as L
+import Text.Megaparsec.Char as C
+import qualified Data.Set as Set
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.Parse.Basic
+import Grin.ExtendedSyntax.Parse.TypeEnv
+
+-- grin syntax
+
+def :: Parser Def
+def = Def <$> try (L.indentGuard sc EQ pos1 *> var) <*> many var <* op "=" <*> (L.indentGuard sc GT pos1 >>= expr)
+
+expr :: Pos -> Parser Exp
+expr i = L.indentGuard sc EQ i >>
+  try ((\pat e b -> EBind e pat b) <$> try (bindingPat <* op "<-") <*> simpleExp i <*> expr i ) <|>
+  ifThenElse i <|>
+  simpleExp i
+
+ifThenElse :: Pos -> Parser Exp
+ifThenElse i = do
+  kw "if"
+  b <- var
+  kw "then"
+  t <- (L.indentGuard sc GT i >>= expr)
+  L.indentGuard sc EQ i
+  kw "else"
+  e <- (L.indentGuard sc GT i >>= expr)
+  return $ ECase b [ Alt (LitPat (LBool True))  t
+                   , Alt (LitPat (LBool False)) e
+                   ]
+
+simpleExp :: Pos -> Parser SimpleExp
+simpleExp i = SReturn <$ kw "pure" <*> value <|>
+              ECase <$ kw "case" <*> var <* kw "of" <*> (L.indentGuard sc GT i >>= some . alternative) <|>
+              SStore <$ kw "store" <*> var <|>
+              SFetch <$ kw "fetch" <*> var <|>
+              SUpdate <$ kw "update" <*> var <*> var <|>
+              SBlock <$ kw "do" <*> (L.indentGuard sc GT i >>= expr) <|>
+
+              -- FIXME: remove '$' from app syntax, fix 'value' parser with using 'lineFold' instead
+              SApp <$> primNameOrDefName <* (optional $ op "$") <*> many var
+
+primNameOrDefName :: Parser Name
+primNameOrDefName = nMap ("_"<>) <$ char '_' <*> var <|> var
+
+alternative :: Pos -> Parser Alt
+alternative i = Alt <$> try (L.indentGuard sc EQ i *> altPat) <* op "->" <*> (L.indentGuard sc GT i >>= expr)
+
+-- NOTE: The parser `value` already handles the parentheses around "complex" values,
+-- and we don't want to parenthesize variables, literals and units.
+bindingPat :: Parser BPat
+bindingPat =
+  try (AsPat <$> (var <* char '@') <*> {- parens -} value) <|>
+  VarPat <$> var
+
+
+altPat :: Parser CPat
+altPat = parens (NodePat <$> tag <*> many var) <|>
+         DefaultPat <$ kw "#default" <|>
+         LitPat <$> literal
+
+-- #undefined can hold simple types as well as node types
+value :: Parser Val
+value = Lit <$> literal <|>
+        Var <$> var <|>
+        try (parens $ ConstTagNode <$> tag <*> many var) <|>
+        try (Unit <$ op "()") <|>
+        Undefined <$> parens (kw "#undefined" *> op "::" *> typeAnnot)
+
+literal :: Parser Lit
+literal = (try $ LFloat . realToFrac <$> signedFloat) <|>
+          (try $ LWord64 . fromIntegral <$> lexeme (L.decimal <* C.char 'u')) <|>
+          (try $ LInt64 . fromIntegral <$> signedInteger) <|>
+          (try $ LBool <$> (True <$ kw "#True" <|> False <$ kw "#False")) <|>
+          (try $ LString <$> lexeme (C.char '#' *> quotedString)) <|>
+          (try $ LChar <$> lexeme (C.string "#'" *> (escaped <|> anyChar) <* C.char '\''))
+
+satisfyM :: (a -> Bool) -> Parser a -> Parser a
+satisfyM pred parser = do
+  x <- parser
+  if pred x
+    then pure x
+    else mzero
+
+-- externals
+
+externalBlock = do
+  L.indentGuard sc EQ pos1
+  ext <- const PrimOp <$> kw "primop" <|> const FFI <$> kw "ffi"
+  eff <- const False <$> kw "pure" <|> const True <$> kw "effectful"
+  i <- L.indentGuard sc GT pos1
+  some $ try (external ext eff i)
+
+external :: ExternalKind -> Bool -> Pos -> Parser External
+external ext eff i = do
+  L.indentGuard sc EQ i
+  name <- var
+  L.indentGuard sc GT i >> op "::"
+  ty <- reverse <$> sepBy1 (L.indentGuard sc GT i >> L.lexeme sc tyP ) (L.indentGuard sc GT i >> op "->")
+  let (retTy:argTyRev) = ty
+  pure External
+    { eName       = name
+    , eRetType    = retTy
+    , eArgsType   = reverse argTyRev
+    , eEffectful  = eff
+    , eKind       = ext
+    }
+
+tyP :: Parser Ty
+tyP =
+  TyVar <$ C.char '%' <*> var <|>
+  braces (TyCon <$> var <*> many tyP) <|>
+  TySimple <$> try simpleType
+
+-- top-level API
+
+grinModule :: Parser Exp
+grinModule = Program <$> (concat <$> many (try externalBlock)) <*> many def <* sc <* eof
+
+parseGrin :: String -> Text -> Either (ParseError Char Void) Exp
+parseGrin filename content = runParser grinModule filename (withoutTypeAnnots content)
+
+parseProg :: Text -> Exp
+parseProg src = either (error . parseErrorPretty' src) id . parseGrin "" $ withoutTypeAnnots src
+
+parseDef :: Text -> Exp
+parseDef src = either (error . parseErrorPretty' src) id . runParser def "" $ withoutTypeAnnots src
+
+parseExpr :: Text -> Exp
+parseExpr src = either (error . parseErrorPretty' src) id . runParser (expr pos1) "" $ withoutTypeAnnots src
+
+
+withoutTypeAnnots :: Text -> Text
+withoutTypeAnnots = T.unlines
+                  . map skipIfAnnot
+                  . T.lines
+  where skipIfAnnot line
+          | Just ('%',_) <- T.uncons . T.dropWhile isSpace $ line = ""
+          | otherwise = line
diff --git a/grin/src/Grin/ExtendedSyntax/Parse/Basic.hs b/grin/src/Grin/ExtendedSyntax/Parse/Basic.hs
new file mode 100644
index 00000000..9ae50edd
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Parse/Basic.hs
@@ -0,0 +1,155 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Grin.ExtendedSyntax.Parse.Basic where
+
+import Data.Set (Set)
+import Data.Vector (Vector)
+import qualified Data.Set    as Set
+
+import qualified Data.Vector as Vec
+
+import Data.String (fromString)
+import Data.Text (Text)
+import Data.Void
+
+import Control.Monad (void)
+import Text.Megaparsec
+import qualified Text.Megaparsec.Char.Lexer as L
+import Text.Megaparsec.Char
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.TypeEnvDefs
+
+type Parser = Parsec Void Text
+
+keywords = Set.fromList
+  [ "case", "of"
+  , "fetch", "store", "update"
+  , "if", "then", "else"
+  , "do", "pure"
+  , "#True", "#False"
+  , "#undefined"
+  , "primop", "effectful"
+  ] `Set.union` simpleTypes
+
+simpleTypes = Set.fromList
+  [ "T_Int64", "T_Word64", "T_Float"
+  , "T_Bool",  "T_Unit"
+  , "T_Location", "T_Dead"
+  , "T_String", "T_Char"
+  ]
+
+lineComment :: Parser ()
+lineComment = L.skipLineComment "--"
+
+blockComment :: Parser ()
+blockComment = L.skipBlockComment "{-" "-}"
+
+sc :: Parser ()
+sc = L.space (void spaceChar) lineComment blockComment
+
+sc' :: Parser ()
+sc' = L.space (void $ oneOf (" \t" :: String)) lineComment blockComment
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme sc'
+
+symbol = L.symbol sc'
+
+parens = between (symbol "(") (symbol ")")
+
+brackets = between (symbol "[") (symbol "]")
+
+braces = between (symbol "{") (symbol "}")
+
+kw w = lexeme $ string w
+
+op w = L.symbol sc' w
+
+int :: Parser Int
+int = lexeme L.decimal
+
+integer = lexeme L.decimal
+signedInteger = L.signed sc' integer
+
+float = lexeme L.float
+signedFloat = L.signed sc' float
+
+list :: Parser a -> Parser [a]
+list p = brackets (sepBy p (op ","))
+
+list1 :: Parser a -> Parser [a]
+list1 p = brackets (sepBy1 p (op ","))
+
+vec :: Parser a -> Parser (Vector a)
+vec p = Vec.fromList <$> list p
+
+vec1 :: Parser a -> Parser (Vector a)
+vec1 p = Vec.fromList <$> list1 p
+
+bracedList :: Parser a -> Parser [a]
+bracedList p = braces (sepBy p (op ","))
+
+set :: Ord a => Parser a -> Parser (Set a)
+set p = Set.fromList <$> bracedList p
+
+set1 :: Ord a => Parser a -> Parser (Set a)
+set1 p = Set.fromList <$> bracedList p
+
+anySingle :: MonadParsec e s m => m (Token s)
+anySingle = satisfy (const True)
+
+anySingleBut :: MonadParsec e s m => Token s -> m (Token s)
+anySingleBut t = satisfy (/= t)
+
+
+-- grin syntax
+
+escaped :: Parser Char
+escaped = string "\\\"" >> pure '"'
+
+quotedVar :: Parser Name
+quotedVar = packName <$ char '"' <*> someTill (escaped <|> anyChar) (char '"')
+
+escapedStringChar :: Parser Char
+escapedStringChar =
+  (string "\\\"" >> pure '"') <|>
+  (string "\\\\" >> pure '\\') <|>
+  (string "\\a" >> pure '\a') <|>
+  (string "\\b" >> pure '\b') <|>
+  (string "\\f" >> pure '\f') <|>
+  (string "\\n" >> pure '\n') <|>
+  (string "\\r" >> pure '\r') <|>
+  (string "\\t" >> pure '\t') <|>
+  (string "\\v" >> pure '\v')
+
+quotedString :: Parser Text
+quotedString = fromString <$> (char '"' *> manyTill (escapedStringChar <|> anyChar) (char '"'))
+
+simpleVar :: Parser Name
+simpleVar = (\c s -> packName $ c : s) <$> oneOf allowedInitial <*> many (alphaNumChar <|> oneOf allowedSpecial)
+
+-- TODO: allow keywords in quotes
+var :: Parser Name
+var = try $ lexeme (quotedVar <|> simpleVar) >>= \x@(NM x') -> case Set.member x' keywords of
+  True -> fail $ "keyword: " ++ unpackName x
+  False -> return x
+
+tag :: Parser Tag
+tag = Tag C <$ char 'C' <*> var <|>
+      Tag F <$ char 'F' <*> var <|>
+      Tag <$> (P <$ char 'P' <*> L.decimal) <*> var
+
+-- type syntax
+
+simpleType :: Parser SimpleType
+simpleType =
+  T_Int64 <$ kw "T_Int64" <|>
+  T_Word64 <$ kw "T_Word64" <|>
+  T_Float <$ kw "T_Float" <|>
+  T_Bool <$ kw "T_Bool" <|>
+  T_Unit <$ kw "T_Unit" <|>
+  T_UnspecifiedLocation <$ kw "#ptr" <|>
+  T_Location <$> bracedList int <|>
+  T_String <$ kw "T_String" <|>
+  T_Char <$ kw "T_Char" <|>
+  T_Dead <$ kw "T_Dead"
diff --git a/grin/src/Grin/ExtendedSyntax/Parse/TypeEnv.hs b/grin/src/Grin/ExtendedSyntax/Parse/TypeEnv.hs
new file mode 100644
index 00000000..7ccc9638
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Parse/TypeEnv.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE LambdaCase, OverloadedStrings #-}
+module Grin.ExtendedSyntax.Parse.TypeEnv
+  ( typeAnnot
+  , parseTypeEnv
+  , parseMarkedTypeEnv
+  , parseMarkedTypeEnv'
+  ) where
+
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Vector (Vector)
+import qualified Data.Map    as Map
+import qualified Data.Set    as Set
+import qualified Data.Vector as Vec
+
+import Data.List
+import Data.Char
+import Data.Void
+import Data.Monoid
+import Data.Text (Text)
+import qualified Data.Text as T
+
+import Control.Monad (void)
+
+import Lens.Micro.Platform
+
+import Text.Megaparsec
+import qualified Text.Megaparsec.Char.Lexer as L
+import Text.Megaparsec.Char as C
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.TypeEnvDefs hiding (location, nodeSet, simpleType)
+import qualified Grin.ExtendedSyntax.TypeEnvDefs as Env
+import Grin.ExtendedSyntax.Parse.Basic
+
+import Control.Monad.State
+
+
+data TypeEnvEntry
+  = Location Int NodeSet
+  | Variable Name Type
+  | Function Name (Type, Vector Type)
+  deriving (Eq, Ord, Show)
+
+nodeType :: Parser (Tag, Vector SimpleType)
+nodeType = (,) <$> tag <*> vec simpleType
+
+nodeSet :: Parser NodeSet
+nodeSet = Map.fromList <$> bracedList nodeType
+
+typeAnnot :: Parser Type
+typeAnnot = try (T_SimpleType <$> simpleType) <|>
+            T_NodeSet <$> nodeSet
+
+functionTypeAnnot :: Parser (Type, Vector Type)
+functionTypeAnnot = toPair <$> sepBy1 typeAnnot (op "->")
+  where toPair ts = (last ts, Vec.fromList . init $ ts)
+
+
+location :: Parser TypeEnvEntry
+location = Location <$> int <* op "->" <*> nodeSet
+
+varType :: Parser TypeEnvEntry
+varType = Variable <$> var <* op "->" <*> typeAnnot
+
+functionType :: Parser TypeEnvEntry
+functionType = Function <$> var <* op "::" <*> functionTypeAnnot
+
+typeEnvEntry :: Parser TypeEnvEntry
+typeEnvEntry = location <|> try varType <|> functionType
+
+markedTypeEnvEntry :: Parser TypeEnvEntry
+markedTypeEnvEntry = op "%" *> typeEnvEntry
+
+typeEnvEntries :: Parser [TypeEnvEntry]
+typeEnvEntries = many $ typeEnvEntry <* sc
+
+markedTypeEnvEntries :: Parser [TypeEnvEntry]
+markedTypeEnvEntries = many $ markedTypeEnvEntry <* sc
+
+typeEnv :: Parser TypeEnv
+typeEnv = entriesToTypeEnv <$>
+            (sc *> header "Location" *> many' location) <>
+                  (header "Variable" *> many' (try varType)) <>
+                  (header "Function" *> many' functionType)
+            <* eof
+  where header w = L.lexeme sc $ string w
+        many'  p = many $ L.lexeme sc p
+
+markedTypeEnv :: Parser TypeEnv
+markedTypeEnv = entriesToTypeEnv <$> (sc *> markedTypeEnvEntries <* eof)
+
+
+filterSortLocEntries :: [TypeEnvEntry] -> [TypeEnvEntry]
+filterSortLocEntries = sortBy cmpLoc . filter isLoc
+  where isLoc (Location _ _) = True
+        isLoc _ = False
+
+        cmpLoc (Location n _) (Location m _) = compare n m
+
+locEntriesToHeapMap :: [TypeEnvEntry] -> Vector NodeSet
+locEntriesToHeapMap entries = flip execState mempty $ forM entries' $
+  \(Location _ t) -> modify $ flip Vec.snoc t
+  where entries' = filterSortLocEntries entries
+
+entriesToTypeEnv :: [TypeEnvEntry] -> TypeEnv
+entriesToTypeEnv xs = flip execState emptyTypeEnv $ do
+  Env.location .= locEntriesToHeapMap xs
+  forM_ xs $ \case
+    Variable n t  -> variable %= Map.insert n t
+    Function n ts -> function %= Map.insert n ts
+    Location _ _  -> pure ()
+
+-- parses a type environment (without code)
+parseTypeEnv :: Text -> TypeEnv
+parseTypeEnv src = either (error . parseErrorPretty' src) id
+                 . runParser typeEnv ""
+                 $ src
+
+-- parses type marked type annotations (even interleaved with code)
+parseMarkedTypeEnv' :: Text -> TypeEnv
+parseMarkedTypeEnv' src = either (error . parseErrorPretty' src) id $ parseMarkedTypeEnv "" src
+
+parseMarkedTypeEnv :: String -> Text -> Either (ParseError Char Void) TypeEnv
+parseMarkedTypeEnv filename src = runParser markedTypeEnv filename (withoutCodeLines src)
+
+withoutCodeLines :: Text -> Text
+withoutCodeLines = T.unlines
+                 . map skipIfCode
+                 . T.lines
+  where skipIfCode line
+          | Just ('%',_) <- T.uncons . T.dropWhile isSpace $ line = line
+          | otherwise = ""
+
diff --git a/grin/src/Grin/ExtendedSyntax/Pretty.hs b/grin/src/Grin/ExtendedSyntax/Pretty.hs
new file mode 100644
index 00000000..ee2431a9
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Pretty.hs
@@ -0,0 +1,229 @@
+{-# LANGUAGE LambdaCase, RecordWildCards, OverloadedStrings #-}
+module Grin.ExtendedSyntax.Pretty
+  ( pretty
+  , printGrin
+  , PP(..)
+  , WPP(..)
+  , RenderingOption(..)
+  , prettyProgram
+  , prettyHighlightExternals
+  , prettyKeyValue
+  , prettyBracedList
+  , prettySimplePair
+  , prettyFunction
+  , Pretty
+  , showName
+  , showWidth
+  , showWide
+  ) where
+
+import Data.Char
+import Data.Set (Set)
+import Data.List (groupBy)
+import qualified Data.Set as Set
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+
+import Data.Vector (Vector)
+import qualified Data.Vector as V
+
+import Data.Text (unpack)
+
+import Data.Functor.Foldable as Foldable
+import Text.PrettyPrint.ANSI.Leijen
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.TypeEnvDefs
+import Grin.ExtendedSyntax.EffectMap
+
+import Grin.ExtendedSyntax.Parse
+
+showWidth :: Int -> Doc -> String
+showWidth w x = displayS (renderPretty 0.4 w x) ""
+
+showWide :: Doc -> String
+showWide = showWidth 156
+
+printGrin :: Exp -> IO ()
+printGrin = putStrLn . showWide . pretty
+
+-- plain wrappers ; remove colors
+
+-- Pretty Show instance wrapper ; i.e. useful for hspec tests
+newtype PP a = PP a deriving Eq
+instance Pretty a => Show (PP a ) where
+  show (PP a) = showWide . plain . pretty $ a
+
+-- Wide pretty printing, useful for reparsing pretty-printed ASTs
+newtype WPP a = WPP a deriving Eq
+instance Pretty a => Show (WPP a ) where
+  show (WPP a) = showWide . plain . pretty $ a
+
+
+keyword :: String -> Doc
+keyword = yellow . text
+
+keywordR = red . text
+
+showName :: Name -> String
+showName n = case unpackName n of
+  []    -> ""
+  str@(c:s)
+    | c `elem` allowedInitial && all (\a -> isAlphaNum a || elem a allowedSpecial) s -> str
+    | otherwise -> '"' : go str
+    where
+      go [] = ['"']
+      go ('"':xs) = '\\' : '"' : go xs
+      go (a : xs) = a : go xs
+
+instance Pretty Name where
+  pretty = text . showName
+
+data RenderingOption
+  = Simple
+  | WithExternals
+  deriving (Eq, Ord, Show, Read)
+
+prettyProgram :: RenderingOption -> Exp -> Doc
+prettyProgram Simple          (Program exts e) = prettyHighlightExternals exts (Program [] e)
+prettyProgram WithExternals p@(Program exts _) = prettyHighlightExternals exts p
+prettyProgram _             p                  = prettyHighlightExternals [] p
+
+-- TODO
+--  nice colors for syntax highlight
+--  better node type syntax (C | F | P)
+
+-- | Print a given expression with highlighted external functions.
+prettyHighlightExternals :: [External] -> Exp -> Doc
+prettyHighlightExternals externals exp = cata prettyExpAlgebra exp where
+
+  prettyExpAlgebra :: ExpF Doc -> Doc
+  prettyExpAlgebra = \case
+    ProgramF exts defs  -> vcat (prettyExternals exts : defs)
+    DefF name args exp  -> hsep (pretty name : map pretty args) <+> text "=" <$$> indent 2 exp <> line
+    -- Exp
+    EBindF lhs bpat rhs     -> pretty bpat <+> text "<-" <+> lhs <$$> rhs
+    ECaseF scrutinee alts   -> keyword "case" <+> pretty scrutinee <+> keyword "of" <$$> indent 2 (vsep alts)
+    -- Simple Expr
+    SAppF f args
+      | isExternalName externals f -> hsep ((dullyellow $ pretty f) : text "$" : map pretty args)
+      | otherwise                  -> hsep ((cyan       $ pretty f) : text "$" : map pretty args)
+    SReturnF val            -> keyword "pure" <+> pretty val
+    SStoreF v               -> keywordR "store" <+> pretty v
+    SFetchF p               -> keywordR "fetch" <+> pretty p
+    SUpdateF name v         -> keywordR "update" <+> pretty name <+> pretty v
+    SBlockF exp             -> text "do" <$$> indent 2 exp
+    -- Alt
+    AltF cpat exp     -> pretty cpat <+> text "->" <$$> indent 2 exp
+
+
+instance Pretty Exp where
+  pretty = prettyProgram Simple
+
+instance Pretty Val where
+  pretty = \case
+    ConstTagNode tag args -> parens $ hsep (pretty tag : map pretty args)
+    Unit         -> parens empty
+    -- simple val
+    Lit lit      -> pretty lit
+    Var name     -> pretty name
+    Undefined ty -> parens $ text "#undefined" <+> text "::" <+> pretty ty
+
+instance Pretty Lit where
+  pretty = \case
+    LInt64 a   -> integer $ fromIntegral a
+    LWord64 a  -> integer (fromIntegral a) <> text "u"
+    LFloat a   -> float a
+    LBool a    -> text "#" <> text (show a)
+    LString a  -> text "#" <> text (show a)
+    LChar a    -> text "#" <> text (show a)
+
+instance Pretty BPat where
+  pretty = \case
+    VarPat v    -> pretty v
+    AsPat v val -> pretty v <> pretty '@' <> pretty '(' <> pretty val <> pretty ')'
+
+instance Pretty CPat where
+  pretty = \case
+    NodePat tag vars  -> parens $ hsep (pretty tag : map pretty vars)
+    LitPat  lit       -> pretty lit
+    DefaultPat        -> keyword "#default"
+
+instance Pretty TagType where
+  pretty = green . \case
+    C   -> text "C"
+    F   -> text "F"
+    P i -> text "P" <> int i
+
+instance Pretty Tag where
+  pretty (Tag tagtype name) = pretty tagtype <> pretty name
+
+-- generic ; used by HPTResult and TypeEnv
+
+instance Pretty a => Pretty (Set a) where
+  pretty s = encloseSep lbrace rbrace comma (map pretty $ Set.toList s)
+
+prettyKeyValue :: (Pretty k, Pretty v) => [(k,v)] -> Doc
+prettyKeyValue kvList = vsep [fill 6 (pretty k) <+> text "->" <+> pretty v | (k,v) <- kvList]
+
+-- type env
+
+instance Pretty SimpleType where
+  pretty = \case
+    T_UnspecifiedLocation -> red $ text "#ptr"
+    T_Location l -> encloseSep lbrace rbrace comma $ map (cyan . int) l
+    ty -> red $ text $ show ty
+
+prettyNode :: (Tag, Vector SimpleType) -> Doc
+prettyNode (tag, args) = pretty tag <> list (map pretty $ V.toList args)
+
+instance Pretty Type where
+  pretty = \case
+    T_SimpleType ty -> pretty ty
+    T_NodeSet ns    -> encloseSep lbrace rbrace comma (map prettyNode (Map.toList ns))
+
+instance Pretty TypeEnv where
+  pretty TypeEnv{..} = vsep
+    [ yellow (text "Location") <$$> indent 4 (prettyKeyValue $ zip [(0 :: Int)..] $ map T_NodeSet $ V.toList _location)
+    , yellow (text "Variable") <$$> indent 4 (prettyKeyValue $ Map.toList _variable)
+    , yellow (text "Function") <$$> indent 4 (vsep $ map prettyFunction $ Map.toList _function)
+    ]
+
+instance Pretty Effects where
+  pretty (Effects priomps updateLocs storeLocs) = align . vsep $
+    [ green (text "effectful") <+> (semiBraces . map (red . pretty) . Set.toList $ priomps)
+    , green (text "updates")   <+> prettyLocSet updateLocs
+    , green (text "stores")    <+> prettyLocSet storeLocs
+    ]
+
+instance Pretty EffectMap where
+  pretty (EffectMap effects) = yellow (text "EffectMap") <$$>
+    indent 4 (prettyKeyValue $ Map.toList effects)
+
+prettyExternals :: [External] -> Doc
+prettyExternals exts = vcat (map prettyExtGroup $ groupBy (\a b -> eEffectful a == eEffectful b && eKind a == eKind b) exts) where
+  prettyExtGroup [] = mempty
+  prettyExtGroup l@(a : _) = keyword "primop" <+> (if eEffectful a then keyword "effectful" else keyword "pure") <$$> indent 2
+    (vsep [prettyFunction (eName, (eRetType, V.fromList eArgsType)) | External{..} <- l] <> line)
+
+instance Pretty Ty where
+  pretty = \case
+    TyCon name tys      -> braces . hsep $ (green $ pretty name) : map pretty tys
+    TyVar name          -> text "%" <> cyan (pretty name)
+    TySimple simpleType -> pretty simpleType
+
+prettyBracedList :: [Doc] -> Doc
+prettyBracedList = encloseSep lbrace rbrace comma
+
+prettySimplePair :: (Pretty a, Pretty b) => (a, b) -> Doc
+prettySimplePair (x, y) = pretty x <> pretty y
+
+prettyFunction :: (Pretty a, Pretty name) => (name, (a, Vector a)) -> Doc
+prettyFunction (name, (ret, args)) = pretty name <> align (encloseSep (text " :: ") empty (text " -> ") (map pretty $ (V.toList args) ++ [ret]))
+
+prettyLocSet :: Set Loc -> Doc
+prettyLocSet = semiBraces . map (cyan . int) . Set.toList
diff --git a/grin/src/Grin/ExtendedSyntax/Syntax.hs b/grin/src/Grin/ExtendedSyntax/Syntax.hs
new file mode 100644
index 00000000..3becc721
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/Syntax.hs
@@ -0,0 +1,179 @@
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, DeriveAnyClass, DeriveFunctor, TypeFamilies #-}
+{-# LANGUAGE DeriveFoldable, DeriveTraversable, PatternSynonyms #-}
+{-# LANGUAGE TemplateHaskell, StandaloneDeriving, OverloadedStrings #-}
+{-# LANGUAGE LambdaCase #-}
+module Grin.ExtendedSyntax.Syntax
+  ( module Grin.ExtendedSyntax.Syntax
+  , module Grin.ExtendedSyntax.SyntaxDefs
+  ) where
+
+import Data.Data
+import Control.DeepSeq
+import Data.Binary
+import Data.Functor.Foldable.TH
+import Data.Int
+import Data.Text (Text, isPrefixOf)
+import Data.Vector
+import Data.Word
+import GHC.Generics (Generic)
+import Lens.Micro.Platform
+import qualified Data.ByteString.Short as B
+
+import Grin.ExtendedSyntax.SyntaxDefs
+import Grin.ExtendedSyntax.TypeEnvDefs
+
+-- * GRIN Externals, i.e. primops and foreign functions
+
+data Ty
+  = TyCon     Name [Ty]
+  | TyVar     Name
+  | TySimple  SimpleType
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+data ExternalKind
+  = PrimOp -- ^ Implemented in the internal code generator
+  | FFI    -- ^ Implemented in C and linked during the linker phase
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+data External
+  = External
+  { eName       :: Name
+  , eRetType    :: Ty
+  , eArgsType   :: [Ty]
+  , eEffectful  :: Bool
+  , eKind       :: ExternalKind
+  }
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+isExternalName :: [External] -> Name -> Bool
+isExternalName es n = n `Prelude.elem` (eName <$> es)
+
+-- * GRIN Literal
+
+-- QUESTION: Now #undefined can be pattern matched on.
+-- Should the linter warn about this?
+data Lit
+  = LInt64  Int64
+  | LWord64 Word64
+  | LFloat  Float
+  | LBool   Bool
+  | LString Text
+  | LChar   Char
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+-- * GRIN Value
+
+data Val
+  = ConstTagNode  Tag  [Name]
+  | Unit
+  -- simple val
+  | Lit Lit
+  | Var Name
+  | Undefined     Type
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+-- See: https://github.com/ekmett/recursion-schemes/blob/master/Data/Functor/Foldable/TH.hs#L31
+makeBaseFunctor ''Val
+
+-- * Case Pattern
+
+data CPat
+  = NodePat Tag [Name]  -- HIGH level GRIN
+  | LitPat  Lit         -- HIGH level GRIN
+  | DefaultPat          -- HIGH level GRIN
+  deriving (Generic, Data, NFData, Binary, Eq, Show, Ord)
+
+
+-- * Binding pattern
+
+data BPat
+  = VarPat { _bPatVar :: Name }
+  | AsPat  { _bPatVar :: Name
+           , _bPatVal :: Val
+           }
+  deriving (Generic, Data, NFData, Binary, Eq, Show, Ord)
+
+makeLenses ''BPat
+
+-- * GRIN Expression
+
+type SimpleExp = Exp
+type Alt = Exp
+type Def = Exp
+type Program = Exp
+
+data Exp
+  = Program     [External] [Def]
+  | Def         Name [Name] Exp
+  -- Exp
+  | EBind       SimpleExp BPat Exp
+  | ECase       Name [Alt]
+  -- Simple Exp
+  | SApp        Name [Name]
+  | SReturn     Val
+  | SStore      Name
+  | SFetch      Name
+  | SUpdate     Name Name
+  | SBlock      Exp
+  -- Alt
+  | Alt CPat Exp
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+externals :: Exp -> [External]
+externals = \case
+  Program es _ -> es
+  _            -> []
+
+-- See: https://github.com/ekmett/recursion-schemes/blob/master/Data/Functor/Foldable/TH.hs#L31
+makeBaseFunctor ''Exp
+
+deriving instance Show a  => Show (ExpF a)
+deriving instance Eq a    => Eq   (ExpF a)
+deriving instance Ord a   => Ord  (ExpF a)
+
+
+pattern BoolPat b = LitPat (LBool b)
+
+_AltCPat :: Traversal' Exp CPat
+_AltCPat f (Alt p e) = (`Alt` e) <$> f p
+_AltCPat _ other     = pure other
+
+_AltFCPat :: Traversal' (ExpF a) CPat
+_AltFCPat f (AltF p e) = (`AltF` e) <$> f p
+_AltFCPat _ other      = pure other
+
+_ValVar :: Traversal' Val Name
+_ValVar f (Var name) = Var <$> f name
+_ValVar _ other      = pure other
+
+_OnlyVarPat :: Traversal' BPat Name
+_OnlyVarPat f (VarPat v) = VarPat <$> f v
+_OnlyVarPat _ other      = pure other
+
+_BPatVar :: Traversal' BPat Name
+_BPatVar f (AsPat v val) = AsPat <$> f v <*> pure val
+_BPatVar f (VarPat v)    = VarPat <$> f v
+
+_CPatNodeTag :: Traversal' CPat Tag
+_CPatNodeTag f (NodePat tag args) = (`NodePat` args) <$> f tag
+_CPatNodeTag _ other              = pure other
+
+_CPatLit :: Traversal' CPat Lit
+_CPatLit f (LitPat lit) = LitPat <$> f lit
+_CPatLit _ other        = pure other
+
+_CPatDefault :: Traversal' CPat ()
+_CPatDefault f DefaultPat = const DefaultPat <$> f ()
+_CPatDefault _ other      = pure other
+
+_TyCon :: Traversal' Ty (Name, [Ty])
+_TyCon f (TyCon n ts) = uncurry TyCon <$> f (n, ts)
+_TyCon _ other        = pure other
+
+_TyVar :: Traversal' Ty Name
+_TyVar f (TyVar n) = TyVar <$> f n
+_TyVar _ other     = pure other
+
+_TySimple :: Traversal' Ty SimpleType
+_TySimple f (TySimple t) = TySimple <$> f t
+_TySimple _ other        = pure other
diff --git a/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs b/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs
new file mode 100644
index 00000000..5f40c516
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/SyntaxDefs.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, DeriveAnyClass, StandaloneDeriving, LambdaCase #-}
+module Grin.ExtendedSyntax.SyntaxDefs where
+
+import Data.Text (Text, unpack)
+import Data.Binary
+import Control.DeepSeq
+import GHC.Generics (Generic)
+import Data.Data
+import Data.String
+import Text.Printf
+import Lens.Micro.Platform
+
+-- Names are stored in NM form when we do program generation. NI is only used
+-- when we seralize the Exp
+data Name
+  = NM { unNM :: !Text }
+  | NI !Int
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+nMap :: (Text -> Text) -> Name -> Name
+nMap f (NM n) = NM (f n)
+
+instance Semigroup Name where
+  (NM n1) <> (NM n2) = NM (n1 <> n2)
+
+instance Monoid Name where
+  mempty = NM mempty
+
+instance IsString Name where
+  fromString = NM . fromString
+
+instance PrintfArg Name where
+  formatArg = formatString . unpack . unNM
+
+nameString :: Name -> String
+nameString = \case
+  NM n -> unpack n
+  _    -> error "Name index found." -- This could have left in the AST after a problematic deserialisation.
+
+-- * GRIN Tag
+
+data TagType = C | F | P Int {-missing parameter count-}
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+data Tag = Tag
+  { tagType :: TagType
+  , tagName :: Name
+  }
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+-- * GRIN Type System
+
+type Loc = Int
+
+data SimpleType
+  = T_Int64
+  | T_Word64
+  | T_Float
+  | T_Bool
+  | T_Unit
+  | T_Location {_locations :: [Loc]}
+  | T_UnspecifiedLocation
+  | T_Dead
+  | T_String
+  | T_Char
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+-- * Traversals
+
+_NM :: Traversal' Name Text
+_NM f (NM n) = NM <$> f n
+_NM _ other  = pure other
+
+_NI :: Traversal' Name Int
+_NI f (NI i) = NI <$> f i
+_NI _ other  = pure other
diff --git a/grin/src/Grin/ExtendedSyntax/TH.hs b/grin/src/Grin/ExtendedSyntax/TH.hs
new file mode 100644
index 00000000..43908732
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/TH.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Grin.ExtendedSyntax.TH
+  ( text
+  , progConst
+  , prog
+  , def
+  , expr
+  ) where
+
+import Data.List (sort)
+import Data.Char
+import Data.Data
+import Data.Maybe
+import NeatInterpolation
+import Text.Megaparsec
+
+import qualified Grin.ExtendedSyntax.Parse as P
+import qualified Data.Text as T
+
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+import Language.Haskell.TH.Quote
+
+prog :: QuasiQuoter
+prog = text { quoteExp = applyParseProg . quoteExp text }
+
+applyParseProg:: Q Exp -> Q Exp
+applyParseProg q = appE [|P.parseProg|] q
+
+def :: QuasiQuoter
+def = text { quoteExp = applyParseDef . quoteExp text }
+
+applyParseDef :: Q Exp -> Q Exp
+applyParseDef q = appE [|P.parseDef|] q
+
+expr :: QuasiQuoter
+expr = text { quoteExp = applyParseExpr . quoteExp text }
+
+applyParseExpr :: Q Exp -> Q Exp
+applyParseExpr q = appE [|P.parseExpr|] q
+
+liftText :: T.Text -> Q Exp
+liftText txt = AppE (VarE 'T.pack) <$> lift (T.unpack txt)
+
+liftDataWithText :: Data a => a -> Q Exp
+liftDataWithText = dataToExpQ (\a -> liftText <$> cast a)
+
+-- NOTE: does not support metavariables
+progConst :: QuasiQuoter
+progConst = QuasiQuoter
+  { quoteExp = \input -> do
+      let src = T.pack $ normalizeQQInput input
+      case P.parseGrin "" src of
+        Left  e -> fail $ parseErrorPretty' src e
+        Right p -> liftDataWithText p
+  , quotePat  = undefined
+  , quoteType = undefined
+  , quoteDec  = undefined
+  }
+
+--
+-- NOTE: copy-paste utility from NeatInterpolation.String hidden module
+--
+normalizeQQInput :: [Char] -> [Char]
+normalizeQQInput = trim . unindent' . tabsToSpaces
+  where
+    unindent' :: [Char] -> [Char]
+    unindent' s =
+      case lines s of
+        head:tail ->
+          let
+            unindentedHead = dropWhile (== ' ') head
+            minimumTailIndent = minimumIndent . unlines $ tail
+            unindentedTail = case minimumTailIndent of
+              Just indent -> map (drop indent) tail
+              Nothing -> tail
+          in unlines $ unindentedHead : unindentedTail
+        [] -> []
+
+trim :: [Char] -> [Char]
+trim = dropWhileRev isSpace . dropWhile isSpace
+
+dropWhileRev :: (a -> Bool) -> [a] -> [a]
+dropWhileRev p = foldr (\x xs -> if p x && null xs then [] else x:xs) []
+
+unindent :: [Char] -> [Char]
+unindent s =
+  case minimumIndent s of
+    Just indent -> unlines . map (drop indent) . lines $ s
+    Nothing -> s
+
+tabsToSpaces :: [Char] -> [Char]
+tabsToSpaces ('\t':tail) = "    " ++ tabsToSpaces tail
+tabsToSpaces (head:tail) = head : tabsToSpaces tail
+tabsToSpaces [] = []
+
+minimumIndent :: [Char] -> Maybe Int
+minimumIndent =
+  listToMaybe . sort . map lineIndent
+    . filter (not . null . dropWhile isSpace) . lines
+
+-- | Amount of preceding spaces on first line
+lineIndent :: [Char] -> Int
+lineIndent = length . takeWhile (== ' ')
diff --git a/grin/src/Grin/ExtendedSyntax/TypeEnv.hs b/grin/src/Grin/ExtendedSyntax/TypeEnv.hs
new file mode 100644
index 00000000..6a920218
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/TypeEnv.hs
@@ -0,0 +1,187 @@
+{-# LANGUAGE LambdaCase, RecordWildCards #-}
+module Grin.ExtendedSyntax.TypeEnv
+  ( module Grin.ExtendedSyntax.TypeEnv
+  , module Grin.ExtendedSyntax.TypeEnvDefs
+  , module Grin.ExtendedSyntax.SyntaxDefs
+  ) where
+
+import Text.Printf
+import Data.Int
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Vector (Vector)
+import qualified Data.Map as Map
+import qualified Data.Set as Set (fromList, toList)
+import qualified Data.Vector as Vector (fromList, toList, map)
+import Data.Bifunctor (bimap)
+import Data.Monoid
+import Data.Maybe (fromMaybe)
+import Data.Functor.Infix ((<$$>))
+import Control.Applicative (liftA2)
+import Control.Monad (join)
+
+import Lens.Micro.Platform
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.Pretty
+import Grin.ExtendedSyntax.TypeEnvDefs
+import Grin.ExtendedSyntax.SyntaxDefs
+
+
+dead_t :: Type
+dead_t = T_SimpleType T_Dead
+
+unit_t :: Type
+unit_t = T_SimpleType T_Unit
+
+int64_t :: Type
+int64_t = T_SimpleType T_Int64
+
+bool_t :: Type
+bool_t = T_SimpleType T_Bool
+
+float_t :: Type
+float_t = T_SimpleType T_Float
+
+location_t :: [Int] -> Type
+location_t = T_SimpleType . T_Location
+
+fun_t :: Name -> [Type] -> Type -> Map Name (Type, Vector Type)
+fun_t name params ret = Map.singleton name (ret, Vector.fromList params)
+
+cnode_t :: Name -> [SimpleType] -> NodeSet
+cnode_t name params = Map.singleton (Tag C name) (Vector.fromList params)
+
+-- * Prism
+
+_T_NodeSet :: Traversal' Type NodeSet
+_T_NodeSet f (T_NodeSet ns) = T_NodeSet <$> f ns
+_T_NodeSet _ rest           = pure rest
+
+_T_SimpleType :: Traversal' Type SimpleType
+_T_SimpleType f (T_SimpleType s) = T_SimpleType <$> f s
+_T_SimpleType _ rest             = pure rest
+
+_T_Location :: Traversal' SimpleType [Int]
+_T_Location f (T_Location ls) = T_Location <$> f ls
+_T_Location _ rest            = pure rest
+
+_T_String :: Traversal' SimpleType ()
+_T_String f T_String = const T_String <$> f ()
+_T_String _ rest     = pure rest
+
+_T_Float :: Traversal' SimpleType ()
+_T_Float f T_Float = const T_Float <$> f ()
+_T_Float _ rest    = pure rest
+
+_T_Unit :: Traversal' SimpleType ()
+_T_Unit f T_Unit = const T_Unit <$> f ()
+_T_Unit _ rest   = pure rest
+
+_ReturnType :: Traversal' (Type, Vector Type) Type
+_ReturnType = _1
+
+_T_OnlyOneTag :: Traversal' NodeSet NodeSet
+_T_OnlyOneTag f nodeSet
+  | (Map.size nodeSet == 1) = f nodeSet
+  | otherwise = pure nodeSet
+
+newVar :: Name -> Type -> Endo TypeEnv
+newVar n t = Endo (variable %~ (Map.insert n t))
+
+newFun :: Name -> Type -> [Type] -> Endo TypeEnv
+newFun n t a = Endo (function %~ (Map.insert n (t, Vector.fromList a)))
+
+create :: Endo TypeEnv -> TypeEnv
+create (Endo c) = c emptyTypeEnv
+
+extend :: TypeEnv -> Endo TypeEnv -> TypeEnv
+extend t (Endo c) = c t
+
+variableType :: TypeEnv -> Name -> Type
+variableType TypeEnv{..} name = case Map.lookup name _variable of
+  Nothing -> error $ printf "variable %s is missing from type environment" (unNM name)
+  Just t -> t
+
+functionType :: TypeEnv -> Name -> (Type, Vector Type)
+functionType TypeEnv{..} name = case Map.lookup name _function of
+  Nothing -> error $ printf "function %s is missing from type environment" name
+  Just t -> t
+
+typeOfLit :: Lit -> Type
+typeOfLit = T_SimpleType . typeOfLitST
+
+typeOfLitST :: Lit -> SimpleType
+typeOfLitST lit = case lit of
+  LInt64{}  -> T_Int64
+  LWord64{} -> T_Word64
+  LFloat{}  -> T_Float
+  LBool{}   -> T_Bool
+  LString{} -> T_String
+  LChar{}   -> T_Char
+
+-- Type of literal like values
+typeOfVal :: Val -> Type
+typeOfVal = \case
+  ConstTagNode  tag [] ->
+    T_NodeSet
+      $ Map.singleton tag
+      $ mempty
+
+  Unit    -> T_SimpleType T_Unit
+  Lit lit -> typeOfLit lit
+
+  bad -> error (show bad)
+
+typeOfValTE :: TypeEnv -> Val -> Type
+typeOfValTE typeEnv val = fromMaybe (error $ show val) $ mTypeOfValTE typeEnv val
+
+mTypeOfValTE :: TypeEnv -> Val -> Maybe Type
+mTypeOfValTE typeEnv@TypeEnv{..} = \case
+  Undefined t -> Just t
+
+  ConstTagNode tag args -> do
+    tys <- mapM (`Map.lookup` _variable) args
+    let sTys = map _simpleType $ tys
+    pure . T_NodeSet . Map.singleton tag . Vector.fromList $ sTys
+
+  Unit      -> Just $ T_SimpleType T_Unit
+  Lit lit   -> Just $ typeOfLit lit
+  Var name  -> typeEnv ^. variable . at name
+
+  bad -> Nothing
+
+-- | Sort locations, remove duplication from set like things.
+normalizeTypeEnv :: TypeEnv -> TypeEnv
+normalizeTypeEnv (TypeEnv locations variables functions) =
+  TypeEnv
+    (Vector.map normalizeNodeSet locations)
+    (Map.map normalizeType variables)
+    (Map.map (bimap normalizeType (Vector.map normalizeType)) functions)
+
+normalizeSimpleType :: SimpleType -> SimpleType
+normalizeSimpleType = \case
+  T_Location ls -> T_Location $ Set.toList $ Set.fromList ls
+  rest          -> rest
+
+normalizeNodeSet :: NodeSet -> NodeSet
+normalizeNodeSet = Map.map (Vector.map normalizeSimpleType)
+
+normalizeType :: Type -> Type
+normalizeType = \case
+  T_SimpleType st -> T_SimpleType $ normalizeSimpleType st
+  T_NodeSet    ns -> T_NodeSet $ normalizeNodeSet ns
+  rest            -> rest
+
+-- | Compare types, return Nothing if types are incomparable: Dead or UnspecifiedLocation
+sameType :: Type -> Type -> Maybe Bool
+sameType (T_SimpleType T_Dead) _                = Nothing
+sameType _ (T_SimpleType T_Dead)                = Nothing
+sameType (T_SimpleType T_UnspecifiedLocation) _ = Nothing
+sameType _ (T_SimpleType T_UnspecifiedLocation) = Nothing
+sameType t1 t2 = Just $ t1 == t2
+
+ptrLocations :: TypeEnv -> Name -> [Loc]
+ptrLocations te p = case variableType te p of
+  T_SimpleType (T_Location locs) -> locs
+  ty -> error $ "Variable " ++ show (PP p) ++ " should be a pointer, but instead it has type: " ++ show (PP ty)
diff --git a/grin/src/Grin/ExtendedSyntax/TypeEnvDefs.hs b/grin/src/Grin/ExtendedSyntax/TypeEnvDefs.hs
new file mode 100644
index 00000000..a844db7d
--- /dev/null
+++ b/grin/src/Grin/ExtendedSyntax/TypeEnvDefs.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE DeriveDataTypeable, DeriveAnyClass, DeriveGeneric #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Grin.ExtendedSyntax.TypeEnvDefs where
+
+import Data.Binary
+
+import Data.Data
+import Data.Map (Map)
+import Data.Vector (Vector)
+
+import qualified Data.Vector as V (fromList, toList)
+
+import Data.Monoid
+
+import Control.DeepSeq
+import GHC.Generics (Generic)
+
+import Lens.Micro.Platform
+
+import Grin.ExtendedSyntax.SyntaxDefs
+
+-- TODO: put orphan instances into a separate module
+instance Binary a => Binary (Vector a) where
+  get = V.fromList <$> get
+  put = put . V.toList
+
+type NodeSet = Map Tag (Vector SimpleType)
+
+data Type
+  = T_SimpleType  {_simpleType  :: SimpleType}
+  | T_NodeSet     {_nodeSet     :: NodeSet}
+  deriving (Generic, Data, NFData, Binary, Eq, Ord, Show)
+
+data TypeEnv
+  = TypeEnv
+  { _location :: Vector NodeSet
+  , _variable :: Map Name Type
+  , _function :: Map Name (Type, Vector Type)
+  }
+  deriving (Eq, Show)
+
+concat <$> mapM makeLenses [''TypeEnv, ''Type, ''SimpleType]
+
+emptyTypeEnv :: TypeEnv
+emptyTypeEnv = TypeEnv mempty mempty mempty
diff --git a/grin/src/Test/ExtendedSyntax/Assertions.hs b/grin/src/Test/ExtendedSyntax/Assertions.hs
new file mode 100644
index 00000000..70d00637
--- /dev/null
+++ b/grin/src/Test/ExtendedSyntax/Assertions.hs
@@ -0,0 +1,51 @@
+module Test.ExtendedSyntax.Assertions where
+
+import Test.Hspec
+
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.Pretty
+import Grin.ExtendedSyntax.TypeEnv
+
+-- import AbstractInterpretation.CreatedBy.Pretty
+-- import AbstractInterpretation.CreatedBy.Result (ProducerMap,ProducerGraph(..))
+-- import AbstractInterpretation.LiveVariable.Pretty
+-- import AbstractInterpretation.LiveVariable.Result (LVAResult)
+-- import AbstractInterpretation.HeapPointsTo.Result (HPTResult)
+-- import AbstractInterpretation.EffectTracking.Pretty
+-- import AbstractInterpretation.EffectTracking.Result (ETResult)
+import Transformations.Names
+
+
+class SameAs a where
+  sameAs :: a -> a -> IO ()
+
+instance SameAs TypeEnv where
+  sameAs found expected = found `shouldBe` expected
+
+-- instance SameAs ProducerMap where
+--   sameAs found expected = (PP found) `shouldBe` (PP expected)
+
+-- instance SameAs HPTResult where
+--   sameAs found expected = (PP found) `shouldBe` (PP expected)
+
+-- instance SameAs LVAResult where
+--   sameAs found expected = (PP found) `shouldBe` (PP expected)
+
+-- instance SameAs ETResult where
+--   sameAs found expected = (PP found) `shouldBe` (PP expected)
+
+-- instance SameAs ProducerGraph where
+--   sameAs found expected = (PP found) `shouldBe` (PP expected)
+
+-- instance SameAs ExpChanges where
+--   sameAs found expected = found `shouldBe` expected
+
+instance (SameAs a, SameAs b) => SameAs (a, b) where
+  sameAs (f1, f2) (e1, e2) = do
+    f1 `sameAs` e1
+    f2 `sameAs` e2
+
+instance SameAs Exp where
+  -- | Check if the two expression are the same, if not renders them
+  -- in a pretty printed form.
+  sameAs found expected = (PP found) `shouldBe` (PP expected)
diff --git a/grin/src/Test/ExtendedSyntax/Old/Grammar.hs b/grin/src/Test/ExtendedSyntax/Old/Grammar.hs
new file mode 100644
index 00000000..c2be5c94
--- /dev/null
+++ b/grin/src/Test/ExtendedSyntax/Old/Grammar.hs
@@ -0,0 +1,112 @@
+{-# LANGUAGE StandaloneDeriving, DeriveGeneric, LambdaCase #-}
+module Test.ExtendedSyntax.Old.Grammar where
+
+import qualified Grin.Grin as Grin
+import Test.QuickCheck (NonEmptyList(..))
+import GHC.Generics
+
+-- NOTE: Still generates stuff convertible to OLD AST!!
+
+data Name = Name { unName :: Grin.Name }
+  deriving (Eq, Generic, Show)
+
+deriving instance Generic (NonEmptyList a)
+
+data Prog = Prog (NonEmptyList Def)
+  deriving (Generic, Show)
+
+data Def = Def Name [Name] Exp
+  deriving (Generic, Show)
+
+data Exp
+  = EBind SExp LPat Exp
+  | ECase Val (NonEmptyList Alt)
+  | SExp SExp
+  deriving (Generic, Show)
+
+data Alt = Alt Grin.CPat Exp
+  deriving (Generic, Show)
+
+data SExp
+  = SApp     Name [SimpleVal]
+  | SReturn  Val
+  | SStore   Val
+  | SFetch   Name
+  | SUpdate  Name Val
+  | SBlock   Exp
+  deriving (Generic, Show)
+
+data Val
+  = ConstTagNode  Grin.Tag [SimpleVal]
+  | Unit
+  | SimpleVal SimpleVal
+  deriving (Eq, Generic, Show)
+
+data SimpleVal
+  = Lit Grin.Lit
+  | Var Name
+  deriving (Eq, Generic, Show)
+
+data LPat
+  = LPatVal  Val
+  | LPatSVal SimpleVal
+  deriving (Generic, Show)
+
+type Loc = Int
+
+data ExtraVal
+  = Loc Loc
+  deriving (Eq, Generic, Show)
+
+
+toName (Name n) = n
+
+class AsVal t where
+  asVal :: t -> Grin.Val
+
+instance AsVal Val where
+  asVal = \case
+    ConstTagNode  tag  simpleVals -> Grin.ConstTagNode tag (asVal <$> simpleVals)
+    Unit                          -> Grin.Unit
+    SimpleVal     simpleVal       -> asVal simpleVal
+
+instance AsVal SimpleVal where
+  asVal = \case
+    Lit lit  -> Grin.Lit lit
+    Var name -> Grin.Var (toName name)
+
+instance AsVal LPat where
+  asVal = \case
+    LPatVal  val  -> asVal val
+    LPatSVal sval -> asVal sval
+
+
+class AsExp t where
+  asExp :: t -> Grin.Exp
+
+instance AsExp Prog where
+  asExp = \case
+    Prog defs -> Grin.Program [] (asExp <$> getNonEmpty defs)
+
+instance AsExp Def where
+  asExp = \case
+    Def name params exp -> Grin.Def (toName name) (toName <$> params) (asExp exp)
+
+instance AsExp SExp where
+  asExp = \case
+    SApp     name simpleVals -> Grin.SApp (toName name) (asVal <$> simpleVals)
+    SReturn  val -> Grin.SReturn (asVal val)
+    SStore   val -> Grin.SStore (asVal val)
+    SFetch   name -> Grin.SFetchI (toName name) Nothing
+    SUpdate  name val -> Grin.SUpdate (toName name) (asVal val)
+    SBlock   exp -> Grin.SBlock (asExp exp)
+
+instance AsExp Exp where
+  asExp = \case
+    EBind sexp lpat exp -> Grin.EBind (asExp sexp) (asVal lpat) (asExp exp)
+    ECase val alts      -> Grin.ECase (asVal val) (asExp <$> getNonEmpty alts)
+    SExp sexp           -> asExp sexp
+
+instance AsExp Alt where
+  asExp = \case
+    Alt cpat exp -> Grin.Alt cpat (asExp exp)
diff --git a/grin/src/Test/ExtendedSyntax/Old/Test.hs b/grin/src/Test/ExtendedSyntax/Old/Test.hs
new file mode 100644
index 00000000..571b090f
--- /dev/null
+++ b/grin/src/Test/ExtendedSyntax/Old/Test.hs
@@ -0,0 +1,943 @@
+{-# LANGUAGE DeriveGeneric, LambdaCase, TypeApplications, StandaloneDeriving, RankNTypes #-}
+{-# LANGUAGE QuasiQuotes, ViewPatterns, OverloadedStrings #-}
+module Test.ExtendedSyntax.Old.Test where
+
+import Prelude hiding (GT)
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Extra (loopM)
+import Control.Monad.Logic
+import Control.Monad.Trans (lift)
+import Control.Monad.Identity
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.State
+import Control.Monad.Trans.Reader
+import qualified Control.Monad.State.Class as CMS
+import qualified Control.Monad.Reader.Class as CMR
+import Data.Bifunctor
+import Data.Functor.Infix
+import Data.Functor.Foldable
+import Data.List ((\\))
+import Data.Maybe (fromJust, maybeToList)
+import Data.Semigroup
+import Data.String (fromString)
+import qualified Data.Text as Text
+import GHC.Generics
+import Grin.Grin hiding (Def)
+import qualified Grin.Grin as Grin
+import qualified Grin.TypeEnvDefs as Grin
+import qualified Grin.PrimOpsPrelude as PrimOps'
+import Test.QuickCheck
+import Test.QuickCheck.Instances.Vector
+import Generic.Random
+import Lens.Micro
+import Lens.Micro.Mtl
+import qualified Test.ExtendedSyntax.Old.Grammar as G
+
+import Data.Set (Set); import qualified Data.Set as Set
+import Data.Map (Map); import qualified Data.Map as Map
+import Data.List
+
+import Debug.Trace
+import Data.Text (pack)
+import Grin.ExtendedSyntax.Pretty (PP(..))
+import Grin.TH
+import Grin.ExtendedSyntax.TypeEnv (TypeEnv, emptyTypeEnv)  -- NOTE: might become problematic later
+import Test.Hspec
+import Control.Monad
+import Data.List
+
+import Transformations.Optimising.SimpleDeadFunctionElimination
+import Transformations.Optimising.SimpleDeadParameterElimination
+import Transformations.StaticSingleAssignment
+import Grin.PrimOpsPrelude
+
+-- NOTE: Still generates stuff convertible to OLD AST!!
+
+type SpecWithProg = Exp -> Spec
+
+type TestExpContext = (String, (TypeEnv, Exp) -> (TypeEnv, Exp))
+
+testExprContext :: (((TypeEnv, Exp) -> (TypeEnv, Exp)) -> Spec) -> Spec
+testExprContext mkSpec = forM_ contexts $ \(label, ctx) -> describe (concat ["(", label, ")"]) $ mkSpec ctx
+
+testExprContextIn :: [TestExpContext] -> (((TypeEnv, Exp) -> (TypeEnv, Exp)) -> Spec) -> Spec
+testExprContextIn ctxs mkSpec = forM_ ctxs $ \(label, ctx) -> describe (concat ["(", label, ")"]) $ mkSpec ctx
+
+testExprContextE :: ((Exp -> Exp) -> Spec) -> Spec
+testExprContextE mkSpec =
+  forM_ contexts $ \(label, ctx) ->
+    describe (concat ["(", label, ")"]) $ mkSpec (\e -> snd $ ctx (emptyTypeEnv, e))
+
+stressTest
+  :: ((TypeEnv, Exp) -> (TypeEnv, Exp))
+  -> (TypeEnv, Exp)
+  -> (TypeEnv, Exp)
+  -> Spec
+stressTest f before after = it "Stress test" $ forAllShrink (listOf1 arbitrary) shrink $ \ctx ->
+  let c = createExpr ctx
+  in (f (c before)) == (c after)
+
+data ExpContext
+  = EmptyCtx
+  | LastBindR
+  | BindL
+  | LastBindL
+  | FirstAlt
+  | MiddleAlt
+  | LastAlt
+  deriving (Eq, Show, Generic)
+
+instance Arbitrary ExpContext where arbitrary = genericArbitraryU
+
+createExpr :: [ExpContext] -> (TypeEnv, Exp) -> (TypeEnv, Exp)
+createExpr xs te = foldl' combine te (xs `zip` [0..]) where
+  combine te (ctx, n) =
+    (case ctx of
+      EmptyCtx   -> snd emptyCtx
+      LastBindR  -> snd lastBindR
+      BindL      -> snd $ bindL n
+      LastBindL  -> snd $ lastBindL n
+      FirstAlt   -> snd firstAlt
+      MiddleAlt  -> snd middleAlt
+      LastAlt    -> snd lastAlt)
+    $ te
+
+contexts :: [TestExpContext]
+contexts =
+  [ emptyCtx
+  , lastBindR
+  , bindL 0
+  , lastBindL 0
+  , firstAlt
+  , middleAlt
+  , lastAlt
+  ]
+
+contexts1 :: [TestExpContext]
+contexts1 =
+  [ middleBindR
+  ]
+
+emptyCtx :: TestExpContext
+emptyCtx = ("empty", id)
+
+exprText = pack . show . PP
+
+firstBindR1 :: TestExpContext
+firstBindR1 = ("first bind right", second tr) where
+  tr (exprText -> e) = [expr|
+      $e
+      _prim_int_print 1
+    |]
+
+changeLast :: Exp -> Exp -> Exp
+changeLast e (EBind l p r) = EBind l p (changeLast e r)
+changeLast e r@(ECase{})   = EBind (SBlock r) (Var "cl") e
+changeLast e r             = EBind r (Var "cl") e
+
+firstBindR :: TestExpContext
+firstBindR = ("first bind right", second tr) where
+  tr e = changeLast (SReturn (Lit (LInt64 1))) e
+
+middleBindR :: TestExpContext
+middleBindR = ("middle bind right", second tr) where
+  tr (exprText -> e) = [expr|
+      _prim_int_print 42
+      $e
+      _prim_int_print 1
+    |]
+
+lastBindR :: TestExpContext
+lastBindR = ("last bind right", second tr) where
+  tr (exprText -> e) = [expr|
+      _prim_int_print 42
+      $e
+    |]
+
+bindL :: Int -> TestExpContext
+bindL (pack . show -> n) = ("bind left", second tr) where
+  tr (exprText -> e) = [expr|
+      fb$n <- do
+        $e
+      _prim_int_print 1
+    |]
+
+lastBindL :: Int -> TestExpContext
+lastBindL (pack . show -> n) = ("last bind left", second tr) where
+  tr (exprText -> e) = [expr|
+      md$n <- do
+        _prim_int_print 42
+        $e
+      _prim_int_print 1
+    |]
+
+firstAlt :: TestExpContext
+firstAlt = ("first alt", second tr) where
+  tr (exprText -> e) = [expr|
+      case 1 of
+        1 -> _prim_int_print 42
+             $e
+        2 -> _prim_int_print 1
+        3 -> _prim_int_print 1
+    |]
+
+middleAlt :: TestExpContext
+middleAlt = ("middle alt", second tr) where
+  tr (exprText -> e) = [expr|
+      case 1 of
+        1 -> _prim_int_print 1
+        2 -> _prim_int_print 1
+             $e
+        3 -> _prim_int_print 1
+    |]
+
+lastAlt :: TestExpContext
+lastAlt = ("last alt", second tr) where
+  tr (exprText -> e) = [expr|
+      case 1 of
+        1 -> _prim_int_print 1
+        2 -> _prim_int_print 1
+        3 -> _prim_int_print 1
+             $e
+    |]
+
+
+
+programGenerators :: [(String, Gen Exp)]
+programGenerators =
+  [ ("Semantically incorrect programs", semanticallyIncorrectPrograms)
+  , ("Semantically correct programs", genProg)
+  ]
+
+semanticallyIncorrectPrograms :: Gen Exp
+semanticallyIncorrectPrograms = resize 1 (G.asExp <$> arbitrary @G.Prog)
+
+
+downScale :: Gen a -> Gen a
+downScale = scale (`div` 2)
+
+instance Arbitrary Name where arbitrary = NM <$> arbitrary
+instance Arbitrary Text.Text where arbitrary = Text.pack <$> arbitrary
+
+instance Arbitrary G.Prog where arbitrary = genericArbitraryU
+instance Arbitrary G.Def where arbitrary = genericArbitraryU
+instance Arbitrary G.Exp where arbitrary = downScale genericArbitraryU
+instance Arbitrary G.Alt where arbitrary = genericArbitraryU
+instance Arbitrary Val where arbitrary = genericArbitraryU
+instance Arbitrary Lit where arbitrary = genericArbitraryU
+instance Arbitrary TagType where arbitrary =genericArbitraryU
+instance Arbitrary G.Val where arbitrary = genericArbitraryU
+instance Arbitrary G.SimpleVal where arbitrary = genericArbitraryU
+instance Arbitrary G.ExtraVal where arbitrary = genericArbitraryU
+instance Arbitrary G.LPat where arbitrary = genericArbitraryU
+
+instance Arbitrary G.SExp where
+  arbitrary = genericArbitraryU `suchThat` validStoreOp
+    where
+      isNode = \case
+        G.ConstTagNode  _ _ -> True
+        _                   -> False
+
+      validStoreOp = \case
+        G.SStore  val   -> isNode val
+        G.SUpdate _ val -> isNode val
+        _               -> True
+
+instance Arbitrary CPat where
+  arbitrary = oneof
+    [ NodePat <$> arbitrary <*> (G.unName <$$> listOf1 arbitrary)
+    , LitPat  <$> arbitrary
+    , pure DefaultPat
+    ]
+
+instance Arbitrary Tag where
+  arbitrary = Tag
+    <$> arbitrary
+    <*> (G.unName <$> arbitrary)
+
+instance Arbitrary G.Name where
+  arbitrary = G.Name . packName . concat <$> listOf1 hiragana
+
+-- | Increase the size parameter until the generator succeds.
+suchThatIncreases :: Gen a -> (a -> Bool) -> Gen a
+suchThatIncreases g p =
+  resize 1 $ flip loopM () $ \() -> do
+    scale (+1)
+      $ fmap (maybe (Left ()) Right)
+      $ suchThatMaybe g p
+
+hiragana :: Gen String
+hiragana = elements $
+  ( [ c ++ v
+    | v <- ["a",  "e",  "i",  "o",  "u"]
+    , c <- ["", "k", "s", "t", "n", "h", "m", "y", "r", "w"]
+    ] \\ ["yi", "ye", "wu"]) ++ ["n"]
+
+data Env
+  = Env
+    { vars :: Map Name Type
+    , funs :: Map Name ([Type], Type, [Eff])
+    , adts :: Set Type -- The collection of user defined types.
+    }
+  deriving (Eq, Show)
+
+adtsL :: Lens' Env (Set Type)
+adtsL = lens adts (\e a -> e { adts = a})
+
+funsL :: Lens' Env (Map Name ([Type], Type, [Eff]))
+funsL = lens funs (\e f -> e { funs = f })
+
+instance Semigroup  Env where (Env v0 f0 a0) <> (Env v1 f1 a1) = Env (Map.unionWith (<>) v0 v1) (f0 <> f1) (a0 <> a1)
+instance Monoid     Env where mempty = Env mempty mempty mempty
+insertVar :: Name -> Either G.Val G.ExtraVal -> Env -> Env
+insertVar name val (Env vars funs adts) = Env (Map.singleton name (typeOf val) <> vars) funs adts
+
+insertVarT :: Name -> Type -> Env -> Env
+insertVarT name ttype (Env vars funs adts) = Env (Map.singleton name ttype <> vars) funs adts
+
+insertVars :: [(Name, Type)] -> Env -> Env
+insertVars vars' (Env vars funs adts) = Env ((Map.fromList vars') <> vars) funs adts
+
+insertFun :: (Name, [Type], Type, [Eff]) -> Env -> Env
+insertFun (fname, params, rtype, effs) (Env vars funs adts) =
+    Env vars funs' adts
+  where
+    funs' = Map.insert fname (params, rtype, effs) funs
+
+data Store = Store (Map G.Loc (G.Val, Type))
+  deriving (Eq, Show)
+
+instance Semigroup  Store where (Store s0) <> (Store s1) = Store (s0 <> s1)
+instance Monoid     Store where mempty = Store mempty
+
+data Eff
+  = NoEff          -- Generate a value returning expression of the given type
+  | NewLoc    Type -- Store a value of a given type
+  | ReadLoc   Type -- Read a location with a given type
+  | UpdateLoc Type -- Update a location with a given type
+  deriving (Eq, Generic, Ord, Show)
+
+getSExpTypeInEff :: Eff -> Maybe Type
+getSExpTypeInEff = \case
+  NoEff       -> mzero
+  NewLoc    t -> pure (TLoc t)
+  ReadLoc   t -> pure t
+  UpdateLoc t -> pure TUnit
+
+instance Arbitrary Eff where arbitrary = genericArbitraryU
+
+-- TODO: Remove
+data Type
+  = TUnit -- TODO: Rename
+  | TInt
+  | TFloat
+  | TBool
+  | TWord
+  | TLoc Type
+  | TTag Name [Type] -- Only constant tags, only simple types, or variables with location info
+  | TUnion (Set Type)
+  | TString
+  | TChar
+  deriving (Eq, Generic, Ord, Show)
+
+instance Arbitrary Type where arbitrary = genericArbitraryU
+instance Arbitrary Grin.SimpleType where arbitrary = genericArbitraryU
+
+instance Arbitrary Grin.Type where
+  arbitrary = oneof
+    [ Grin.T_SimpleType <$> arbitrary
+    , Grin.T_NodeSet <$> arbitrary
+    ]
+
+  shrink = genericShrink
+
+simpleType :: GoalM Type
+simpleType = melements
+  [ TInt
+  , TFloat
+  , TWord
+  , TUnit
+  , TBool
+  , TString
+  , TChar
+  ]
+
+primitiveType :: GoalM Type
+primitiveType = melements
+  [ TInt
+  , TFloat
+  , TWord
+  , TBool
+  , TString
+  , TChar
+  ]
+
+
+instance Semigroup Type where
+  (TUnion as) <> (TUnion bs) = TUnion (as `Set.union` bs)
+  (TUnion as) <> a = TUnion (Set.insert a as)
+  a <> (TUnion as) = TUnion (Set.insert a as)
+  a <> b = TUnion $ Set.fromList [a,b]
+
+class TypeOf t where
+  typeOf :: t -> Type
+
+instance TypeOf G.SimpleVal where
+  typeOf = \case
+    G.Lit (LInt64 _)  -> TInt
+    G.Lit (LWord64 _) -> TWord
+    G.Lit (LFloat _)  -> TFloat
+    G.Lit (LBool _)   -> TBool
+    G.Lit (LString _) -> TString
+    G.Lit (LChar _)   -> TChar
+    bad              -> error $ "typeOf @G.SimpleVal got:" ++ show bad
+
+instance TypeOf G.Val where
+  typeOf = \case
+    G.ConstTagNode  tag vals -> TTag (tagName tag) (typeOf <$> vals)
+    G.Unit                   -> TUnit
+    G.SimpleVal val          -> typeOf val
+    bad -> error $ "typeOf got:" ++ show bad
+
+instance TypeOf G.ExtraVal where
+  typeOf = \case
+    G.Loc _ -> TLoc TInt -- TODO: More types...
+
+instance (TypeOf l, TypeOf r) => TypeOf (Either l r) where
+  typeOf = either typeOf typeOf
+
+data Context = Context
+  { _ctxEnv    :: Env
+  , _ctxStore  :: Store
+  , _ctxExpGen :: GoalM G.Exp
+  }
+
+ctxEnv :: Lens' Context Env
+ctxEnv = lens _ctxEnv (\c e -> c { _ctxEnv = e })
+
+ctxExpGen :: Lens' Context (GoalM G.Exp)
+ctxExpGen = lens _ctxExpGen (\c e -> c { _ctxExpGen = e })
+
+getADTs :: GoalM (Set Type)
+getADTs = view (ctxEnv . adtsL)
+
+-- ctxStore = _2
+
+data Goal
+  = Exp [Eff] Type
+  | SExp Eff Type
+  | GVal Type
+  | Prog
+  deriving (Eq, Ord, Show)
+
+-- NOTE: entry point
+genProg :: Gen Exp
+genProg = genProgWith mzero
+
+-- generate one sample
+sampleProg :: IO ()
+sampleProg = sample $ fmap PP $ genProg
+
+-- TODO: add liveness info, or use simples DPE
+genProgWith :: GoalM G.Exp -> Gen Exp
+genProgWith gexp =
+  fmap (simpleDeadFunctionElimination . simpleDeadParameterElimination . staticSingleAssignment . head) $
+  G.asExp <$$>
+  (runGoalM gexp $
+    withADTs 10 $
+    solve @G.Prog Prog)
+
+sampleGoalM :: Show a => GoalM a -> IO ()
+sampleGoalM g = sample $ runGoalM mzero g
+
+type GoalM a = ReaderT Context (LogicT Gen) a
+
+initContext :: GoalM G.Exp -> Context
+initContext expGen = Context (Env mempty primitives mempty) mempty expGen
+  where
+    primitives = Map.fromList [ (eName p, (tyToType <$> eArgsType p, tyToType $ eRetType p, [])) | p <- preludePurePrimOps ]
+    tyToType = \case
+      TySimple ty -> case ty of
+        T_Int64  -> TInt
+        T_Word64 -> TWord
+        T_Float  -> TFloat
+        T_Bool   -> TBool
+        T_Unit   -> TUnit
+        T_String -> TString
+        T_Char   -> TChar
+      ty -> error $ "Unsupported type when testing: " ++ show ty
+
+{-
+  = TUnit -- TODO: Rename
+  | TInt
+  | TFloat
+  | TBool
+  | TWord
+  | TLoc Type
+  | TTag Name [Type] -- Only constant tags, only simple types, or variables with location info
+  | TUnion (Set Type)
+  | TString
+  | TChar
+
+
+  = External
+  { eName       :: Name
+  , eRetType    :: Ty
+  , eArgsType   :: [Ty]
+  , eEffectful  :: Bool
+  }
+
+    primitives = Map.map (\(params, ret) -> (convPrimTypes <$> params, convPrimTypes ret, [])) PrimOps.primOps
+    primitives = primPrelude
+    convPrimTypes = \case
+      PrimOps.TInt   -> TInt
+      PrimOps.TWord  -> TWord
+      PrimOps.TFloat -> TFloat
+      PrimOps.TBool  -> TBool
+      PrimOps.TUnit  -> TUnit
+-}
+
+runGoalM :: GoalM G.Exp -> GoalM a -> Gen [a]
+runGoalM expGen = observeManyT 1 . flip runReaderT (initContext expGen)
+
+runGoalUnsafe :: GoalM a -> Gen a
+runGoalUnsafe = fmap checkSolution . runGoalM mzero
+  where
+    checkSolution [] = error "No solution is found."
+    checkSolution xs = head xs
+
+gen :: Gen a -> GoalM a
+gen = lift . lift
+
+tagNames :: Type -> [Name]
+tagNames (TTag name _)  = [name]
+tagNames (TUnion types) = concatMap tagNames (Set.toList types)
+tagNames _              = []
+
+newName :: GoalM Name
+newName = do
+  (Env vars funs adts) <- view ctxEnv
+  let names = Map.keys vars <> Map.keys funs <> (concatMap tagNames $ Set.toList adts)
+  gen $ ((G.unName <$> arbitrary) `suchThatIncreases` (`notElem` names))
+
+newNames :: Int -> GoalM [Name]
+newNames = go [] where
+  go names 0 = pure names
+  go names n = do
+    name <- newName `mSuchThat` (`notElem` names)
+    go (name:names) (n-1)
+
+newVar :: Type -> (Name -> GoalM a) -> GoalM a
+newVar t k = do
+  (Env vars funs adts) <- view ctxEnv
+  name <- newName
+  CMR.local (ctxEnv %~ insertVarT name t) $ do
+    k name
+
+withVars :: [(Name, Type)] -> GoalM a -> GoalM a
+withVars vars = CMR.local (ctxEnv %~ insertVars vars)
+
+type GBool = Type
+
+adt :: GoalM Type
+adt = do
+  constructors <- newNames =<< gen (choose (1, 5))
+  fmap (TUnion . Set.fromList) $ forM constructors $ \name -> do
+    fields <- gen $ choose (0, 5)
+    TTag name <$> replicateM fields primitiveType
+
+-- | Select a variable from a context which has a given type.
+gEnv :: Type -> GoalM Name
+gEnv t = do
+  (Env vars funs adts) <- view ctxEnv
+  melements . Map.keys $ Map.filter (==t) vars
+
+gLiteral :: Type -> GoalM G.SimpleVal
+gLiteral = fmap G.Lit . \case
+  TInt   -> LInt64  <$> gen arbitrary
+  TFloat -> LFloat  <$> gen arbitrary
+  TWord  -> LWord64 <$> gen arbitrary
+  TBool  -> LBool   <$> gen arbitrary
+  TString -> LString . fromString <$> gen (listOf alphaNumChar)
+  TChar   -> LChar <$> gen alphaNumChar
+  _      -> mzero
+  where
+    alphaNumChar = elements $ ['a' .. 'z'] ++ ['0' .. '9']
+
+varFromEnv :: Type -> GoalM G.SimpleVal
+varFromEnv t = (G.Var . G.Name <$> gEnv t)
+
+gSimpleVal :: Type -> GoalM G.SimpleVal
+gSimpleVal = \case
+  TInt   -> varFromEnv TInt `mplus` gLiteral TInt
+  TFloat -> varFromEnv TFloat `mplus` gLiteral TFloat
+  TWord  -> varFromEnv TWord `mplus` gLiteral TWord
+  TBool  -> varFromEnv TBool `mplus` gLiteral TBool
+  TString  -> varFromEnv TString `mplus` gLiteral TString
+  TChar  -> varFromEnv TChar `mplus` gLiteral TChar
+  (TLoc t) -> varFromEnv (TLoc t) -- Locations have no literals
+  _      -> mzero
+
+gNodeValue :: Type -> GoalM G.Val
+gNodeValue = \case
+  TTag tag types ->
+    (G.SimpleVal <$> varFromEnv (TTag tag types)) `mplus`
+    (G.ConstTagNode (Tag C tag) <$> mapM gSimpleVal types)
+  _ -> mzero
+
+gValue :: Type -> GoalM G.Val
+gValue = \case
+  TUnit          -> pure G.Unit
+  TInt            -> G.SimpleVal <$> gSimpleVal TInt
+  TFloat          -> G.SimpleVal <$> gSimpleVal TFloat
+  TWord           -> G.SimpleVal <$> gSimpleVal TWord
+  TLoc t        -> G.SimpleVal <$> gSimpleVal (TLoc t)
+  TBool           -> G.SimpleVal <$> gSimpleVal TBool
+  TString         -> G.SimpleVal <$> gSimpleVal TString
+  TChar           -> G.SimpleVal <$> gSimpleVal TChar
+  TTag tag types  -> gNodeValue $ TTag tag types
+  TUnion types    -> do
+    t <- melements (Set.toList types)
+    solve (GVal t)
+  -- NOTE: type driven value generator, add undef here
+
+gPureFunction :: (Name -> Bool) -> Type -> GoalM (Name, [Type])
+gPureFunction p t = do
+  (Env vars funs adts) <- view ctxEnv
+  funs <- gen $ shuffle $ filter (p . fst) $ Map.toList $ Map.filter (\(_, r, eff) -> r == t && eff == []) funs
+  (name, (params, ret, _)) <- melements funs
+  pure (name, params)
+
+preludePurePrimOps :: [External]
+preludePurePrimOps = filter (not . eEffectful) es where
+  (Program es _) = primPrelude
+
+gPureNonPrimFun :: Type -> GoalM (Name, [Type])
+gPureNonPrimFun = gPureFunction (not . isExternalName preludePurePrimOps)
+
+gPurePrimFun :: Type -> GoalM (Name, [Type])
+gPurePrimFun = gPureFunction (isExternalName preludePurePrimOps)
+
+mGetSize :: GoalM Int
+mGetSize = gen $ sized pure
+
+gSExp :: Eff -> Type -> GoalM G.SExp
+gSExp e t = do
+  s <- mGetSize
+  gSExpSized s t e
+
+gFunctionCall :: Type -> GoalM G.SExp
+gFunctionCall t =
+  do (funName, paramTypes) <- (gPureNonPrimFun t `mplus` gPurePrimFun t)
+     G.SApp (G.Name funName) <$> forM paramTypes gSimpleVal
+
+gSExpSized :: Int -> Type -> Eff -> GoalM G.SExp
+gSExpSized s t = \case
+  NoEff ->
+    case s of
+      0 -> moneof
+            [ gFunctionCall t
+            , G.SReturn <$> solve (GVal t)
+            ]
+      n -> mfreq
+            [ (45, gFunctionCall t)
+            , (45, G.SReturn <$> solve (GVal t))
+            , (10, fmap G.SBlock $ solve (Exp [] t))
+            ]
+
+  NewLoc t' -> case t of
+    TLoc t0 -> G.SStore <$> solve (GVal t0) -- TODO: Add a block
+    _        -> mzero
+
+  -- find a name that contains the location and the given type.
+  ReadLoc t' -> varFromEnv (TLoc t') >>= \case
+    G.Var name -> pure $ G.SFetch name
+    t -> error $ "var expected, but got: " ++ show t
+
+  UpdateLoc t' -> varFromEnv (TLoc t') >>= \case
+    G.Var name -> G.SUpdate name <$> solve (GVal t') -- fing a name that contains the location and generate  value of a given type
+    t -> error $ "var expected, but got: " ++ show t
+
+tryout :: [GoalM a] -> GoalM a
+tryout gs = do
+  (g, gs') <- select gs
+  g `mplus` tryout gs'
+
+selectF :: [(Int, a)] -> GoalM ((Int, a), [(Int, a)])
+selectF []  = mzero
+selectF [a] = pure (a, [])
+selectF gs  = do
+  let s = sum $ map fst gs
+  n <- gen $ choose (0, s)
+  pure $ go n gs []
+  where
+    go n [] _   = error "selectF: impossible"
+    go n [a] rs = (a, [])
+    go n (a@(m, _):rest) skipped
+      | (n - m) <= 0 = (a, skipped ++ rest)-- in range
+      | otherwise    = go (n - m) rest (a:skipped)
+
+tryoutF :: [(Int, GoalM a)] -> GoalM a
+tryoutF []       = mzero
+tryoutF [(_, g)] = g
+tryoutF gs = do
+  gs0 <- gen $ shuffle gs
+  ((_, g), gs1) <- selectF gs0
+  g `mplus` tryoutF gs1
+
+moneof :: [GoalM a] -> GoalM a
+moneof [] = mzero
+moneof gs = join $ fmap fst $ select gs
+
+mfreq :: [(Int, GoalM a)] -> GoalM a
+mfreq gs = join $ fmap (snd . fst) $ selectF gs
+
+
+-- TODO: Limit the number of retries
+mSuchThat :: GoalM a -> (a -> Bool) -> GoalM a
+mSuchThat g p = go 100 where
+  go 0 = mzero
+  go n = do
+    x <- g
+    if (p x) then pure x else go (n - 1)
+
+melements :: [a] -> GoalM a
+melements [] = mzero
+melements es = gen $ elements es
+
+select :: [a] -> GoalM (a, [a])
+select []  = mzero
+select [a] = pure (a, [])
+select xs  = do
+  n <- gen $ choose (0, length xs - 1)
+  case (splitAt n xs) of
+    ([]    , [])     -> mzero
+    ((a:as), [])     -> pure (a, as)
+    ([]    , (b:bs)) -> pure (b, bs)
+    (as    , (b:bs)) -> pure (b, as ++ bs)
+
+definedAdt :: GoalM Type
+definedAdt = do
+  (Env funs vars adts) <- view ctxEnv
+  melements $ Set.toList adts
+
+retry :: Int -> GoalM a -> GoalM a
+retry n _ | n < 0 = mzero
+retry 0 g = g
+retry n g = g `mplus` retry (n-1) g
+
+liftGenTr :: (forall r . Gen r -> Gen r) -> GoalM a -> GoalM a
+liftGenTr fg (ReaderT g) =
+  ReaderT $ \ctx ->
+    let l' = unLogicT (g ctx)
+    in (LogicT (\f g1 -> fg $ l' (\a g0 -> (f a g0)) g1))
+
+mresize :: Int -> GoalM a -> GoalM a
+mresize n = liftGenTr (resize n)
+
+mscale :: (Int -> Int) -> GoalM a -> GoalM a
+mscale f = liftGenTr (scale f)
+
+gEffs :: GoalM [Eff]
+gEffs = do
+  adts <- Set.toList <$> definedAdts
+  moneof
+    [ pure []
+    , gen $ do
+        n <- choose (0, 3)
+        let noeffs = replicate n NoEff
+        adt <- elements adts
+        rest <- listOf1 $ elements [NoEff, NewLoc adt, ReadLoc adt, UpdateLoc adt]
+        pure $ noeffs ++ [NewLoc adt] ++ rest
+    ]
+
+-- TODO: Effects
+-- TODO: Always succeeds with a trivial function
+-- TODO: Self Recursive
+gDef :: Type -> GoalM (G.Def, ([Type], Type, [Eff]))
+gDef retType = do
+  effs <- gEffs
+  n <- gen $ choose (1, 5)
+  ptypes <- replicateM n $ mfreq [ (90, simpleType), (10, definedAdt) ]
+  nl <- newNames n
+  let (fname:pnames) = nl
+  CMR.local
+--    TODO: Self recursive: Generate eval creates in infinite loop
+--    kahe ya = kahe ya
+--    (ctxEnv %~ (insertFun (fname, ptypes, retType, effs) .
+--                insertVars (pnames `zip` ptypes))
+    (ctxEnv %~ insertVars (pnames `zip` ptypes)
+    ) $ do
+        body <- solve (Exp effs retType)
+        pure $
+          ( G.Def (G.Name fname) (map G.Name pnames) body
+          , (ptypes, retType, effs)
+          )
+
+gExp :: Type -> [Eff] -> GoalM G.Exp
+gExp t es = do
+  s <- mGetSize
+  gExpSized s t es
+
+-- TODO: Generate values for effects
+-- TODO: Limit exp generation by values
+-- TODO: Use size parameter to limit the generation of programs.
+gExpSized :: Int -> Type -> [Eff] -> GoalM G.Exp
+gExpSized n t = \case
+  [] -> case n of
+    0 -> G.SExp <$> (solve (SExp NoEff t))
+    _ -> tryoutF
+          [ -- (10, G.SExp <$> (solve (SExp (NoEff t))))
+            (80, do (t', se) <-
+                      tryout
+                        [ do t' <- tryout [simpleType, definedAdt]
+                             se <- (solve (SExp NoEff t'))
+                             pure (t', se)
+                        , do se <- fmap G.SBlock $ join $ view ctxExpGen
+                             pure (TUnit, se)
+                        ]
+                    newVar t' $ \n -> do -- TODO: Gen LPat
+                      rest <- solve (Exp [] t)
+                      pure (G.EBind se (G.LPatSVal (G.Var (G.Name n))) rest))
+          , (20, gCase [] t)
+          ]
+  (e:es) -> case n of
+    0 -> G.SExp <$> (solve (SExp NoEff t)) -- TODO: Consume all effects
+    _ -> tryoutF
+            [ -- (10, G.SExp <$> (solve (SExp (NoEff t))))
+              (80, do t' <- maybe (tryout [simpleType, definedAdt]) pure
+                            $ getSExpTypeInEff e
+                      se <- (solve (SExp e t'))
+                      newVar t' $ \n -> do -- TODO: Gen LPat
+                        rest <- solve (Exp es t)
+                        pure (G.EBind se (G.LPatSVal (G.Var (G.Name n))) rest))
+            , (20, gCase (e:es) t)
+            ]
+
+gCase :: [Eff] -> Type -> GoalM G.Exp
+gCase eff t = tryout
+  [ -- Make variable for the case
+    do t'   <- tryout [simpleType, definedAdt]
+       se   <- gFunctionCall t'
+       newVar t' $ \n -> do
+         alts <- gAlts eff Nothing t' t
+         pure
+           $ G.EBind se (G.LPatSVal (G.Var (G.Name n)))
+           $ G.ECase (G.SimpleVal (G.Var (G.Name n))) $ NonEmpty alts
+    -- Try to lookup variable or make a value
+  , do t'   <- tryout [simpleType, definedAdt]
+       val  <- gValue t'
+       alts <- gAlts eff (Just val) t' t
+       mDefAlt <- moneof [pure Nothing, (Just . G.Alt DefaultPat <$> (solve (Exp eff t)))]
+       pure $ G.ECase val $ NonEmpty (alts ++ maybeToList mDefAlt)
+  ]
+
+-- TODO: Effects
+-- TODO: Remove overlappings
+-- TODO: Mix values and variables in tags
+gAlts :: [Eff] -> Maybe G.Val -> Type -> Type -> GoalM [G.Alt]
+gAlts eff val typeOfVal typeOfExp = case typeOfVal of
+  TTag name params -> do
+    names <- newNames (length params)
+    pure . G.Alt (NodePat (Tag C name) names)
+      <$> withVars (names `zip` params) (solve (Exp eff typeOfExp))
+  TUnion types -> fmap concat . forM (Set.toList types) $ \typOfV ->
+    gAlts eff val typOfV typeOfExp
+  _ -> case val of
+        (Just (G.SimpleVal (G.Lit lit))) -> do
+          n <- gen $ choose (0, 5)
+          alts0 <- replicateM n $ do
+            lit0P <- gLiteral typeOfVal
+            let G.Lit lit0 = lit0P
+            G.Alt (LitPat lit0) <$> (solve (Exp eff typeOfExp))
+          matching <- G.Alt (LitPat lit) <$> (solve (Exp eff typeOfExp))
+          let alts = Map.elems $
+                     Map.fromList $
+                     map (\v@(G.Alt pat body) -> (pat, v)) $
+                     matching:alts0
+          gen $ shuffle alts
+        _ -> mzero
+
+gMain :: GoalM G.Def
+gMain =
+  fmap (G.Def (G.Name "grinMain") [])
+  $ mresize 20
+  $ do effs <- gEffs
+       solve (Exp effs TUnit)
+
+-- | Generate n functions and extend the context with the definitions,
+-- run the final computation.
+gDefs :: [Type] -> ([G.Def] -> GoalM a) -> GoalM a
+gDefs n f = go n f [] where
+  go [] f defs = f defs
+  go (t:ts) f defs = do
+    (def@(G.Def (G.Name name) _ _), (ptypes, rtype, effs)) <- mresize 20 $ gDef t
+    CMR.local (ctxEnv %~ insertFun (name, ptypes, rtype, effs)) $
+      -- TODO: Make this as a config parameter
+      go ts f (def:defs)
+
+definedAdts :: GoalM (Set Type)
+definedAdts = do
+  (Env _ _ adts) <- view ctxEnv
+  pure adts
+
+gProg :: GoalM G.Prog
+gProg = retry 10 $ do
+  n <- gen $ choose (0, 10)
+  adts <- Set.toList <$> definedAdts
+  ts <- replicateM n $ moneof [simpleType, definedAdt]
+  gDefs (ts ++ adts) $ \defs -> do
+    m <- gMain
+    defs1 <- gen $ shuffle defs
+    pure $ G.Prog $ NonEmpty (defs1 ++ [m])
+
+-- | Generate the given number of ADTs, and register them
+-- in the context, running the computation with the new context.
+withADTs :: Int -> GoalM a -> GoalM a
+withADTs n g = do
+  k <- foldM combine id [1 .. n]
+  k g
+  where
+    combine :: (GoalM a -> GoalM a) -> Int -> GoalM (GoalM a -> GoalM a)
+    combine k _ = do
+      x <- adt
+      return (k . (CMR.local ((ctxEnv . adtsL) %~ (Set.union (Set.singleton x)))))
+
+class Solve t where
+  solve' :: Goal -> GoalM t
+
+-- TODO: Remove debug...
+solve :: Solve t => Goal -> GoalM t
+solve g = do
+--  (Env vars funs adts) <- view _1
+--  traceShowM adts
+--  traceShowM (Map.keys funs)
+--  s <- gen $ sized pure
+--  traceShowM s
+--  traceShowM ("Solve", g)
+  mscale (\x -> if x > 0 then x - 1 else 0) $ solve' g
+
+instance Solve G.Val where
+  solve' = \case
+    GVal e -> gValue e
+    _      -> mzero
+
+instance Solve G.SExp where
+  solve' = \case
+    SExp e t -> gSExp e t
+    _        -> mzero
+
+instance Solve G.Exp where
+  solve' = \case
+    Exp es t -> gExp t es
+    _        -> mzero
+
+instance Solve G.Prog where
+  solve' = \case
+    Prog -> gProg
+    _    -> mzero
+
+changed :: (Testable prop) => Exp -> Exp -> prop -> Property
+changed old new = cover (old /= new) 1 "Transformation has effect"
diff --git a/grin/src/Transformations/ExtendedSyntax/Conversion.hs b/grin/src/Transformations/ExtendedSyntax/Conversion.hs
new file mode 100644
index 00000000..ee26e03f
--- /dev/null
+++ b/grin/src/Transformations/ExtendedSyntax/Conversion.hs
@@ -0,0 +1,302 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+module Transformations.ExtendedSyntax.Conversion where
+
+import Data.String
+import Data.Text (Text(..))
+import Data.Functor.Foldable as Foldable
+
+import qualified Data.Map    as M
+import qualified Data.Vector as V
+
+import Control.Monad
+
+import Lens.Micro.Extra
+import Lens.Micro.Platform
+
+import Grin.Grin
+import Grin.Pretty
+import Grin.Syntax
+import Grin.SyntaxDefs
+import Grin.TypeEnvDefs
+import qualified Grin.ExtendedSyntax.Pretty as New
+import qualified Grin.ExtendedSyntax.Grin as New
+import qualified Grin.ExtendedSyntax.Syntax as New
+import qualified Grin.ExtendedSyntax.SyntaxDefs as New
+import qualified Grin.ExtendedSyntax.TypeEnvDefs as New
+
+import Transformations.Names
+import Transformations.BindNormalisation
+import Transformations.Simplifying.ProducerNameIntroduction
+import Transformations.Simplifying.BindingPatternSimplification
+
+-- TODO: remove these
+import Test.QuickCheck
+import Test.ExtendedSyntax.Old.Test()
+import qualified Test.ExtendedSyntax.Old.Grammar as OG
+
+class Convertible a b where
+  convert :: a -> b
+
+instance Convertible TagType New.TagType where
+  convert = \case
+    C   -> New.C
+    F   -> New.F
+    P n -> New.P n
+
+instance Convertible Name New.Name where
+  convert = \case
+    NM name -> New.NM name
+    NI n    -> New.NI n
+
+instance Convertible Tag New.Tag where
+  convert Tag{..} = New.Tag (convert tagType) (convert tagName)
+
+instance Convertible Lit New.Lit where
+  convert = \case
+    LInt64 n  -> New.LInt64 n
+    LWord64 n -> New.LWord64 n
+    LFloat f  -> New.LFloat f
+    LBool b   -> New.LBool b
+    LString s -> New.LString s
+    LChar c   -> New.LChar c
+
+instance Convertible SimpleType New.SimpleType where
+  convert = \case
+    T_Int64               -> New.T_Int64
+    T_Word64              -> New.T_Word64
+    T_Float               -> New.T_Float
+    T_Bool                -> New.T_Bool
+    T_Unit                -> New.T_Unit
+    T_Location locs       -> New.T_Location locs
+    T_UnspecifiedLocation -> New.T_UnspecifiedLocation
+    T_Dead                -> New.T_Dead
+    T_String              -> New.T_String
+    T_Char                -> New.T_Char
+
+instance Convertible Type New.Type where
+  convert = \case
+    T_SimpleType st -> New.T_SimpleType (convert st)
+    T_NodeSet ns    -> New.T_NodeSet
+      $ M.mapKeysMonotonic convert
+      . M.map (V.map convert)
+      $ ns
+    _ -> error "convert: Dependent type constructors are not supported in the new syntax."
+
+instance Convertible Ty New.Ty where
+  convert = \case
+    TyCon name tys -> New.TyCon (convert name) (map convert tys)
+    TyVar name     -> New.TyVar (convert name)
+    TySimple st    -> New.TySimple (convert st)
+
+instance Convertible ExternalKind New.ExternalKind where
+  convert = \case
+    PrimOp -> New.PrimOp
+    FFI    -> New.FFI
+
+instance Convertible External New.External where
+  convert External{..} = New.External
+    (convert eName)
+    (convert eRetType)
+    (map convert eArgsType)
+    eEffectful
+    (convert eKind)
+
+instance Convertible CPat New.CPat where
+  convert = \case
+    NodePat t args -> New.NodePat (convert t) (map convert args)
+    LitPat l       -> New.LitPat (convert l)
+    DefaultPat     -> New.DefaultPat
+    TagPat _ -> error "covnert: Tag patterns are not supported in the new syntax."
+
+instance Convertible Val New.Val where
+  convert n@(ConstTagNode t vals)
+    | any (isn't _Var) [] = error $ "ConstTagNode " ++ show (PP n) ++ " has a non-variable argument."
+    | otherwise           = New.ConstTagNode (convert t) (map (convert . view _Var) vals)
+  convert v@(VarTagNode _ _) = error $ "Cannot transform VarTagNode to new syntax: " ++ show (PP v)
+  convert v@(ValTag _)       = error $ "Cannot transform ValTag to new syntax: " ++ show (PP v)
+  convert Unit          = New.Unit
+  convert (Lit l)       = New.Lit (convert l)
+  convert (Var v)       = New.Var (convert v)
+  convert (Undefined t) = New.Undefined (convert t)
+
+instance Convertible Exp New.Exp where
+  convert (Program exts defs)  = New.Program (map convert exts) (map convert defs)
+  convert (Def name args body) = New.Def (convert name) (map convert args) (convert body)
+  {- NOTE: we assume Binding Pattern Simplification has been run
+    v.0 <- pure <value>
+    <non-var pat> <- pure v.0
+    <rhs2>
+  -}
+  convert (EBind lhs1 (Var var) rhs1)
+    | EBind (SReturn (Var var')) pat rhs2 <- rhs1
+    , isn't _Var pat
+    , var == var'
+    = New.EBind (convert lhs1) (New.AsPat (convert var) (convert pat)) (convert rhs2)
+  convert (EBind lhs (Var var) rhs)
+    = New.EBind (convert lhs) (New.VarPat $ convert var) (convert rhs)
+  convert (ECase scrut alts)
+    | isn't _Var scrut   = error $ "Non-variable pattern in case scrutinee: " ++ show (PP scrut)
+    | (Var var) <- scrut = New.ECase (convert var) (map convert alts)
+  convert e@(SApp f vals)
+    | any (isn't _Var) vals = error $ "Non-variable value in application: " ++ show (PP e)
+    | otherwise             = New.SApp (convert f) $ map (convert . view _Var) vals
+  convert e@(SStore val)
+    | isn't _Var val   = error $ "Non-variable value in store: " ++ show (PP e)
+    | (Var var) <- val = New.SStore (convert var)
+  convert e@(SFetchI ptr mIx)
+    | Nothing <- mIx = New.SFetch (convert ptr)
+    | otherwise      = error $ "Indexed fetch is no longer supported: " ++ show (PP e)
+  convert e@(SUpdate ptr val)
+    | isn't _Var val   = error $ "Non-variable value in update: " ++ show (PP e)
+    | (Var var) <- val = New.SUpdate (convert ptr) (convert var)
+  convert (SReturn val)  = New.SReturn (convert val)
+  convert (SBlock exp)   = New.SBlock (convert exp)
+  convert (Alt cpat exp) = New.Alt (convert cpat) (convert exp)
+
+instance Convertible New.TagType TagType where
+  convert = \case
+    New.C   -> C
+    New.F   -> F
+    New.P n -> P n
+
+instance Convertible New.Name Name where
+  convert = \case
+    New.NM name -> NM name
+    New.NI n    -> NI n
+
+instance Convertible New.Tag Tag where
+  convert New.Tag{..} = Tag (convert tagType) (convert tagName)
+
+instance Convertible New.Lit Lit where
+  convert = \case
+    New.LInt64 n  -> LInt64 n
+    New.LWord64 n -> LWord64 n
+    New.LFloat f  -> LFloat f
+    New.LBool b   -> LBool b
+    New.LString s -> LString s
+    New.LChar c   -> LChar c
+
+instance Convertible New.SimpleType SimpleType where
+  convert = \case
+    New.T_Int64               -> T_Int64
+    New.T_Word64              -> T_Word64
+    New.T_Float               -> T_Float
+    New.T_Bool                -> T_Bool
+    New.T_Unit                -> T_Unit
+    New.T_Location locs       -> T_Location locs
+    New.T_UnspecifiedLocation -> T_UnspecifiedLocation
+    New.T_Dead                -> T_Dead
+    New.T_String              -> T_String
+    New.T_Char                -> T_Char
+
+instance Convertible New.Type Type where
+  convert = \case
+    New.T_SimpleType st -> T_SimpleType (convert st)
+    New.T_NodeSet ns    -> T_NodeSet
+      $ M.mapKeysMonotonic convert
+      . M.map (V.map convert)
+      $ ns
+
+instance Convertible New.Ty Ty where
+  convert = \case
+    New.TyCon name tys -> TyCon (convert name) (map convert tys)
+    New.TyVar name     -> TyVar (convert name)
+    New.TySimple st    -> TySimple (convert st)
+
+instance Convertible New.ExternalKind ExternalKind where
+  convert = \case
+    New.PrimOp -> PrimOp
+    New.FFI    -> FFI
+
+instance Convertible New.External External where
+  convert New.External{..} = External
+    (convert eName)
+    (convert eRetType)
+    (map convert eArgsType)
+    eEffectful
+    (convert eKind)
+
+instance Convertible New.CPat CPat where
+  convert = \case
+    New.NodePat t args -> NodePat (convert t) (map convert args)
+    New.LitPat l       -> LitPat (convert l)
+    New.DefaultPat     -> DefaultPat
+
+instance Convertible New.Val Val where
+  convert (New.ConstTagNode t vars) = ConstTagNode (convert t) $ map (Var . convert) vars
+  convert (New.Unit)  = Unit
+  convert (New.Lit l) = Lit (convert l)
+  convert (New.Var v) = Var (convert v)
+  convert (New.Undefined t) = Undefined (convert t)
+
+instance Convertible New.Exp Exp where
+  convert (New.Program exts defs)  = Program (map convert exts) (map convert defs)
+  convert (New.Def name args body) = Def (convert name) (map convert args) (convert body)
+  convert e@(New.EBind lhs pat rhs)
+    | (New.VarPat v)      <- pat = EBind (convert lhs) (Var $ convert v) (convert rhs)
+    | (New.AsPat  v pat') <- pat -- condition
+    , rhs' <- EBind (SReturn (Var $ convert v)) (convert pat') (convert rhs) -- helper
+    = EBind (convert lhs) (Var $ convert v) rhs'
+  convert e@(New.ECase scrut alts) = ECase (Var $ convert scrut) (map convert alts)
+  convert (New.SApp f vars)        = SApp (convert f) $ map (Var . convert) vars
+  convert (New.SStore var)         = SStore (Var $ convert var)
+  convert (New.SFetch ptr)         = SFetchI (convert ptr) Nothing
+  convert (New.SUpdate ptr var)    = SUpdate (convert ptr) (Var $ convert var)
+  convert (New.SReturn val)        = SReturn (convert val)
+  convert (New.SBlock exp)         = SBlock (convert exp)
+  convert (New.Alt cpat exp)       = Alt (convert cpat) (convert exp)
+
+convertToNew :: Exp -> New.Exp
+convertToNew = convert . nameEverything
+
+nameEverything :: Exp -> Exp
+nameEverything = nodeArgumentNaming
+               . bindNormalisation
+               . appArgumentNaming
+               . bindNormalisation
+               . fst . bindingPatternSimplification
+               . bindNormalisation
+               . fst . producerNameIntroduction
+               . bindNormalisation
+
+appArgumentNaming :: Exp -> Exp
+appArgumentNaming e = fst . evalNameM e . cata alg $ e where
+  alg :: ExpF (NameM Exp) -> NameM Exp
+  alg e = case e of
+    SAppF f args -> bindFunArgs f args
+    expf -> fmap embed . sequence $ expf
+
+  bindFunArgs :: Name -> [Val] -> NameM Exp
+  bindFunArgs f args = do
+    varArgs <- forM [1..length args] $ \_ ->
+      Var <$> newArgName
+    let g exp (arg, var) = EBind (SReturn arg) var exp
+        boundApp = foldl g (SApp f varArgs) $ zip args varArgs
+    pure $ SBlock boundApp
+
+  newArgName :: NameM Name
+  newArgName = deriveNewName "x"
+
+-- NOTE: we can ssume tha Producer Name Introduction
+-- & Binding Pattern Simplification has already been run
+-- ConstTagNodes can only appear in SReturns
+nodeArgumentNaming :: Exp -> Exp
+nodeArgumentNaming e = fst . evalNameM e . cata alg $ e where
+  alg :: ExpF (NameM Exp) -> NameM Exp
+  alg e = case e of
+    SReturnF (ConstTagNode tag args) -> bindNodeArgs tag args
+    expf -> fmap embed . sequence $ expf
+
+  bindNodeArgs :: Tag -> [Val] -> NameM Exp
+  bindNodeArgs tag args = do
+    varArgs <- forM [1..length args] $ \_ ->
+      Var <$> newArgName
+    let g exp (arg, var) = EBind (SReturn arg) var exp
+        boundApp = foldl g (SReturn $ ConstTagNode tag varArgs) $ zip args varArgs
+    pure $ SBlock boundApp
+
+  newArgName :: NameM Name
+  newArgName = deriveNewName "y"
diff --git a/grin/test/ExtendedSyntax/ParserSpec.hs b/grin/test/ExtendedSyntax/ParserSpec.hs
new file mode 100644
index 00000000..0fdeff20
--- /dev/null
+++ b/grin/test/ExtendedSyntax/ParserSpec.hs
@@ -0,0 +1,459 @@
+{-# LANGUAGE LambdaCase, QuasiQuotes, OverloadedStrings #-}
+module ExtendedSyntax.ParserSpec where
+
+import qualified Data.Text as Text
+import Test.Hspec
+import Test.QuickCheck
+
+import Grin.ExtendedSyntax.Pretty
+import Grin.ExtendedSyntax.Grin
+import Grin.ExtendedSyntax.TH
+import Grin.ExtendedSyntax.Parse
+
+import Test.ExtendedSyntax.Old.Test
+import Test.ExtendedSyntax.Assertions
+
+import Transformations.ExtendedSyntax.Conversion
+
+runTests :: IO ()
+runTests = hspec spec
+
+spec :: Spec
+spec = do
+  describe "quoted names" $ do
+    it "basic" $ do
+      let before = [prog|
+        "GHC.Tuple.()" = pure (C"GHC.Tuple.()")
+        |]
+      let after = Program []
+            [ Def "GHC.Tuple.()" [] $ SReturn $ ConstTagNode (Tag C "GHC.Tuple.()") []
+            ]
+      before `sameAs` after
+
+    it "special symbols" $ do
+      let before = [prog|
+        "extreme name with \" and ~ ! @ # $ % ^ & * ( ) | : > < > ? , . / " = pure ()
+        |]
+      let after = Program []
+            [ Def "extreme name with \" and ~ ! @ # $ % ^ & * ( ) | : > < > ? , . / " [] $ SReturn Unit
+            ]
+      before `sameAs` after
+
+    it "parse . pretty == id" $ do
+      let exp = Program []
+            [ Def "extreme name with \" and ~ ! @ # $ % ^ & * ( ) | : > < > ? , . / " [] $ SReturn Unit
+            ]
+      let Right parsedExp = parseGrin "" (Text.pack $ show $ PP exp)
+      parsedExp `sameAs` exp
+
+  describe "simple" $ do
+    it "var-pat" $ do
+      let before = [prog|
+        grinMain =
+          v <- pure ()
+          pure v
+        |]
+      let after = Program []
+            [ Def "grinMain" [] $
+                EBind (SReturn Unit) (VarPat "v") (SReturn $ Var "v")
+            ]
+      before `sameAs` after
+
+    it "as-pat-unit" $ do
+      let before = [prog|
+        grinMain =
+          v@() <- pure ()
+          pure v
+        |]
+      let after = Program []
+            [ Def "grinMain" [] $
+                EBind (SReturn Unit) (AsPat "v" Unit) (SReturn $ Var "v")
+            ]
+      before `sameAs` after
+
+    it "as-pat-lit" $ do
+      let before = [prog|
+        grinMain =
+          v@5 <- pure ()
+          pure v
+        |]
+      let after = Program []
+            [ Def "grinMain" [] $
+                EBind (SReturn Unit) (AsPat "v" (Lit $ LInt64 5)) (SReturn $ Var "v")
+            ]
+      before `sameAs` after
+
+    it "as-pat-nullary-node" $ do
+      let before = [prog|
+        grinMain =
+          v@(CNil) <- pure ()
+          pure v
+        |]
+      let after = Program []
+            [ Def "grinMain" [] $
+                EBind (SReturn Unit) (AsPat "v" (ConstTagNode (Tag C "Nil") [])) (SReturn $ Var "v")
+            ]
+      before `sameAs` after
+
+    it "as-pat-node" $ do
+      let before = [prog|
+        grinMain =
+          v@(CCons x xs) <- pure ()
+          pure v
+        |]
+      let after = Program []
+            [ Def "grinMain" [] $
+                EBind (SReturn Unit) (AsPat "v" (ConstTagNode (Tag C "Cons") ["x", "xs"])) (SReturn $ Var "v")
+            ]
+      before `sameAs` after
+
+    it "case" $ do
+      let before = [prog|
+        test p =
+          _unit@() <- case p of
+            #default ->
+              pure ()
+          case p of
+            #default ->
+              pure p
+        |]
+      let after = Program []
+            [ Def "test"[ "p" ]
+              ( EBind ( ECase "p" [ Alt DefaultPat ( SReturn Unit ) ] ) (AsPat "_unit" Unit)
+                ( ECase "p" [ Alt DefaultPat ( SReturn (Var "p") ) ] )
+              )
+            ]
+      before `sameAs` after
+
+    it "literal - bind" $ do
+      let before = [prog|
+        grinMain =
+          x0 <- pure 13.1415
+          x1 <- pure +13.1415
+          x2 <- pure -13.1415
+          x3 <- pure 42
+          x4 <- pure +42
+          x5 <- pure -42
+          x6 <- pure 64u
+          x7 <- pure #True
+          x8 <- pure #False
+          x9 <- pure ()
+          pure (CNode x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
+        |]
+      let after = Program []
+            [ Def "grinMain" [] $
+                EBind ( SReturn ( Lit ( LFloat 13.1415 ) ) )    (VarPat "x0") $
+                EBind ( SReturn ( Lit ( LFloat 13.1415 ) ) )    (VarPat "x1") $
+                EBind ( SReturn ( Lit ( LFloat (-13.1415) ) ) ) (VarPat "x2") $
+                EBind ( SReturn ( Lit ( LInt64 42 ) ) )         (VarPat "x3") $
+                EBind ( SReturn ( Lit ( LInt64 42 ) ) )         (VarPat "x4") $
+                EBind ( SReturn ( Lit ( LInt64 (-42) ) ) )      (VarPat "x5") $
+                EBind ( SReturn ( Lit ( LWord64 64 ) ) )        (VarPat "x6") $
+                EBind ( SReturn ( Lit ( LBool True ) ) )        (VarPat "x7") $
+                EBind ( SReturn ( Lit ( LBool False ) ) )       (VarPat "x8") $
+                EBind ( SReturn Unit )                          (VarPat "x9") $
+                SReturn (ConstTagNode (Tag C "Node") ["x0", "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8", "x9"])
+
+
+            ]
+      before `sameAs` after
+
+    it "literal - case" $ do
+      let before = [prog|
+        grinMain =
+          case scrut of
+            13.1415   -> pure ()
+            +14.1415  -> pure ()
+            -14.1415  -> pure ()
+            42        -> pure ()
+            +43       -> pure ()
+            -42       -> pure ()
+            64u       -> pure ()
+            (CNode a1 a2 a3 a4 a5) -> pure ()
+            #default  -> pure ()
+            #True     -> pure ()
+            #False    -> pure ()
+        |]
+      let after = Program []
+            [ Def "grinMain"[]
+                ( ECase "scrut"
+                    [ Alt ( LitPat ( LFloat 13.1415 ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LFloat 14.1415 ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LFloat ( -14.1415 ) ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LInt64 42 ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LInt64 43 ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LInt64 ( -42 ) ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LWord64 64 ) ) ( SReturn Unit )
+                    , Alt
+                        ( NodePat
+                            ( Tag
+                                { tagType = C
+                                , tagName = "Node"
+                                }
+                            )
+                            [ "a1"
+                            , "a2"
+                            , "a3"
+                            , "a4"
+                            , "a5"
+                            ]
+                        ) ( SReturn Unit )
+                    , Alt DefaultPat ( SReturn Unit )
+                    , Alt ( LitPat ( LBool True ) ) ( SReturn Unit )
+                    , Alt ( LitPat ( LBool False ) ) ( SReturn Unit )
+                    ]
+                )
+            ]
+      before `sameAs` after
+
+    xit "bind case on left hand side" $ do
+      let before = [expr|
+          x <-
+            case y of
+              1 -> pure 2
+          pure x
+      |]
+      let after =
+            EBind
+              (ECase "y"
+                [ Alt (LitPat (LInt64 1)) $ SReturn $ Lit $ LInt64 2
+                ])
+              (VarPat "x") $
+            SReturn (Var "x")
+      before `shouldBe` after
+
+  it "interleaved typeenv" $ do
+    let exp = [text|
+            % grinMain :: T_Int64
+            grinMain =
+              % a -> T_Int64
+              a <- pure 5
+              % n -> {CInt[T_Int64]}
+              n <- pure (CInt a)
+              % 0 -> {CInt[T_Int64]}
+              % p -> {0}
+              p <- store n
+              pure 5
+        |]
+    let env = parseMarkedTypeEnv' exp
+    env `sameAs` (parseTypeEnv . Text.pack . show . WPP $ env)
+
+  it "pure undefined ast" $ do
+    let exp = [prog|
+            grinMain =
+              x0 <- pure (#undefined :: T_Int64)
+              x1 <- pure (#undefined :: T_Word64)
+              x4 <- pure (#undefined :: T_Float)
+              x2 <- pure (#undefined :: T_Bool)
+              x3 <- pure (#undefined :: T_Unit)
+              p0 <- pure (#undefined :: #ptr)
+              p1 <- pure (#undefined :: {0})
+              p2 <- pure (#undefined :: {0,1})
+              n0 <- pure (#undefined :: {CInt[T_Int64]})
+              n1 <- pure (#undefined :: {CPair[T_Int64, T_Bool]})
+              n2 <- pure (#undefined :: {CPair[T_Int64, {0}]})
+              n3 <- pure (#undefined :: {CPair[T_Int64, {0,1}]})
+              n4 <- pure (#undefined :: {CPair[T_Int64, #ptr]})
+              n5 <- pure (#undefined :: {CTriplet[T_Int64, {0,1}, #ptr]})
+              pure 0
+        |]
+    exp `sameAs` (parseProg . Text.pack . show . WPP $ exp)
+
+  it "store undefined" $ do
+    pendingWith "store can only be applied to names in the new syntax"
+    let exp = [prog|
+            grinMain =
+              p0 <- store (#undefined :: {CInt[T_Int64]})
+              p1 <- store (#undefined :: {CPair[T_Int64, T_Bool]})
+              p2 <- store (#undefined :: {CPair[T_Int64, {0}]})
+              p3 <- store (#undefined :: {CPair[T_Int64, {0,1}]})
+              p4 <- store (#undefined :: {CPair[T_Int64, #ptr]})
+              p5 <- store (#undefined :: {CTriplet[T_Int64, {0,1}, #ptr]})
+              pure 0
+          |]
+    exp `sameAs` (parseProg . Text.pack . show . WPP $ exp)
+
+  it "update undefined" $ do
+    pendingWith "update can only be applied to names in the new syntax"
+    let exp = [prog|
+            grinMain p =
+              update p (#undefined :: {CInt[T_Int64]})
+              update p (#undefined :: {CPair[T_Int64, T_Bool]})
+              update p (#undefined :: {CPair[T_Int64, {0}]})
+              update p (#undefined :: {CPair[T_Int64, {0,1}]})
+              update p (#undefined :: {CPair[T_Int64, #ptr]})
+              update p (#undefined :: {CTriplet[T_Int64, {0,1}, #ptr]})
+              pure 0
+        |]
+    exp `sameAs` (parseProg . Text.pack . show . WPP $ exp)
+
+  it "string literal" $ do
+    let before = [prog|
+          grinMain =
+            v1 <- pure #""
+            v2 <- pure #"a"
+            v3 <- case v1 of
+              #"" -> pure 1
+              #"a" -> pure 2
+              #default -> pure 3
+            _x@#"a" <- pure v2
+            pure ()
+        |]
+    let after = Program []
+          [Def "grinMain" [] $
+            EBind (SReturn (Lit (LString ""))) (VarPat "v1") $
+            EBind (SReturn (Lit (LString "a"))) (VarPat "v2") $
+            EBind (ECase "v1" $
+              [Alt (LitPat (LString "")) (SReturn (Lit (LInt64 1)))
+              ,Alt (LitPat (LString "a")) (SReturn (Lit (LInt64 2)))
+              ,Alt DefaultPat (SReturn (Lit (LInt64 3)))
+              ]) (VarPat "v3") $
+            EBind (SReturn $ Var "v2") (AsPat "_x" $ (Lit (LString "a"))) $
+            SReturn Unit
+          ]
+    before `sameAs` after
+
+  it "char literals" $ do
+    let before = [prog|
+          grinMain =
+            v2 <- pure #'a'
+            v3 <- case v2 of
+              #'b' -> pure 1
+              #'c' -> pure 2
+              #default -> pure 3
+            _c@#'a' <- pure v2
+            pure ()
+        |]
+    let after = Program []
+          [Def "grinMain" [] $
+            EBind (SReturn (Lit (LChar 'a'))) (VarPat "v2") $
+            EBind (ECase "v2" $
+              [Alt (LitPat (LChar 'b')) (SReturn (Lit (LInt64 1)))
+              ,Alt (LitPat (LChar 'c')) (SReturn (Lit (LInt64 2)))
+              ,Alt DefaultPat (SReturn (Lit (LInt64 3)))
+              ]) (VarPat "v3") $
+            EBind (SReturn $ Var "v2") (AsPat "_c" $ Lit (LChar 'a')) $
+            SReturn Unit
+          ]
+    before `shouldBe` after
+
+  describe "external defintions" $ do
+    it "primop" $ do
+      let before = [prog|
+        primop effectful
+          _prim_string_print  :: T_String -> T_Unit
+          _prim_read_string   :: T_String
+
+          "newArrayArray#" :: {"Int#"} -> {"State#" %s} -> {"GHC.Prim.Unit#" {"MutableArrayArray#" %s}}
+
+        primop pure
+          _prim_string_concat   :: T_String -> T_String -> T_String
+
+        ffi pure
+          newArrayArray :: {Int} -> {State %s} -> {GHC.Prim.Unit {MutableArrayArray %s}}
+
+        grinMain = pure ()
+        |]
+      let after = Program
+
+            [ External
+                { eName = "_prim_string_print"
+                , eRetType = TySimple T_Unit
+                , eArgsType = [ TySimple T_String ]
+                , eEffectful = True
+                , eKind = PrimOp
+                }
+            , External
+                { eName = "_prim_read_string"
+                , eRetType = TySimple T_String
+                , eArgsType = []
+                , eEffectful = True
+                , eKind = PrimOp
+                }
+            , External
+                { eName = "newArrayArray#"
+                , eRetType = TyCon "GHC.Prim.Unit#"
+                    [ TyCon "MutableArrayArray#" [ TyVar "s" ] ]
+                , eArgsType =
+                    [ TyCon "Int#" []
+                    , TyCon "State#" [ TyVar "s" ]
+                    ]
+                , eEffectful = True
+                , eKind = PrimOp
+                }
+            , External
+                { eName = "_prim_string_concat"
+                , eRetType = TySimple T_String
+                , eArgsType =
+                    [ TySimple T_String
+                    , TySimple T_String
+                    ]
+                , eEffectful = False
+                , eKind = PrimOp
+                }
+            , External
+                { eName = "newArrayArray"
+                , eRetType = TyCon "GHC.Prim.Unit"
+                    [ TyCon "MutableArrayArray" [ TyVar "s" ] ]
+                , eArgsType =
+                    [ TyCon "Int" []
+                    , TyCon "State" [ TyVar "s" ]
+                    ]
+                , eEffectful = False
+                , eKind = FFI
+                }
+            ]
+            [ Def "grinMain" [] ( SReturn Unit ) ]
+      before `sameAs` after
+
+    it "indentation" $ do
+      let before = [prog|
+        primop pure
+          -- comment
+          _primA :: T_String
+                 -> T_String
+                 -> T_String
+          {-
+            comment
+          -}
+          _primB
+           :: T_String
+           -> T_String
+
+          -- comment
+          {-
+            comment
+          -}
+        |]
+      let after =
+            Program
+              [ External
+                  { eName = NM { unNM = "_primA" }
+                  , eRetType = TySimple T_String
+                  , eArgsType =
+                      [ TySimple T_String
+                      , TySimple T_String
+                      ]
+                  , eEffectful = False
+                  , eKind = PrimOp
+                  }
+              , External
+                  { eName = NM { unNM = "_primB" }
+                  , eRetType = TySimple T_String
+                  , eArgsType = [ TySimple T_String ]
+                  , eEffectful = False
+                  , eKind = PrimOp
+                  }
+              ] []
+
+      before `sameAs` after
+
+  -- TODO: Kind of hack for now. Now, we generate an old AST,
+  -- convert it to the new syntax, then test for the property.
+  -- We will need to fix Test.ExtendedSyntax.New.Test.
+  describe "generated" $ do
+    it "parse . pretty print == id" $ property $
+      forAll (convertToNew <$> genProg) $ \newAst -> do
+        let newAst' = either (error "Couldn't parse pretty printed AST, see generated NEW AST below.") id $
+              parseGrin "" (Text.pack . show . WPP $ newAst)
+        newAst' `sameAs` newAst
diff --git a/grin/test/TestSpec.hs b/grin/test/TestSpec.hs
index 4e7c4c37..9b8d7fc1 100644
--- a/grin/test/TestSpec.hs
+++ b/grin/test/TestSpec.hs
@@ -1,6 +1,6 @@
 module TestSpec where
 
-import Test.Test
+import Test.ExtendedSyntax.Old.Test
 import Test.Hspec
 import Test.QuickCheck
 import Test.QuickCheck.Monadic
@@ -26,8 +26,7 @@ spec = do
       uniqueValues
 
   it "withGADTs generate unique tags as constructors" $ do
-    pending
-    -- NOTE: commented out due type error
+    pendingWith "commented out due type error"
     {-
     property $ forAll
       (do n <- abs <$> arbitrary
diff --git a/grin/test/Transformations/ExtendedSyntax/ConversionSpec.hs b/grin/test/Transformations/ExtendedSyntax/ConversionSpec.hs
new file mode 100644
index 00000000..05b75379
--- /dev/null
+++ b/grin/test/Transformations/ExtendedSyntax/ConversionSpec.hs
@@ -0,0 +1,38 @@
+module Transformations.ExtendedSyntax.ConversionSpec where
+
+import Control.DeepSeq
+
+import Grin.Grin
+import Grin.Syntax (Exp)
+import qualified Grin.ExtendedSyntax.Syntax as New (Exp)
+import Transformations.ExtendedSyntax.Conversion
+
+import Test.Hspec
+import Test.QuickCheck
+import Test.Hspec.QuickCheck
+
+import Test.Assertions
+import Test.ExtendedSyntax.Old.Test()
+import qualified Test.ExtendedSyntax.Old.Grammar as G
+
+runTests :: IO ()
+runTests = hspec spec
+
+spec :: Spec
+spec = describe "Syntax transformation QuickCheck tests" $ do
+         prop "Old is always convertible to New" $
+           convertibleToNew
+         prop "Old is always convertible to New then back to Old" $
+           roundtripConvertibleOld
+
+-- NOTE: The conversion itself is the proof that it is convertible
+-- QUESTION: There must be a better way to do this
+-- ANSWER: The conversion function could an Either
+convertibleToNew :: G.Exp -> Bool
+convertibleToNew exp = force (convertToNew $ G.asExp exp) `seq` True
+
+roundtripConvertibleOld :: G.Exp -> Bool
+roundtripConvertibleOld exp = force (convertToOld $ convertToNew $ G.asExp exp) `seq` True where
+
+  convertToOld :: New.Exp -> Exp
+  convertToOld = convert