switch to new compiler

87 files changed, 0 insertions, 4459 deletions

diff --git a/prototypes/CGExp.hs b/prototypes/CGExp.hs
deleted file mode 100644
index 5477e485..00000000
--- a/prototypes/CGExp.hs
+++ /dev/null
@@ -1,332 +0,0 @@
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE RecursiveDo #-}
-module CGExp
-    ( module CGExp
-    , Lit(..), Export(..), ModuleR(..)
-    ) where
-
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Except
-import Control.Monad.Identity
-import Control.Monad.Writer
-import Control.Arrow
-import qualified Data.Set as S
-import qualified Data.Map as M
-import Text.Parsec.Pos
-
-import Pretty
-import qualified Infer as I
-import Infer (SName, Lit(..), Visibility(..), Export(..), ModuleR(..))
-
---------------------------------------------------------------------------------
-
-data Exp_ a
-    = Pi_ Visibility SName a a
-    | Lam_ Visibility Pat a a
-    | Con_ (SName, a) [a]
-    | ELit_ Lit
-    | Fun_ (SName, a) [a]
-    | App_ a a
-    | Var_ SName a
-    | TType_
-    | Let_ Pat a a
-    | EFieldProj_ a SName
-  deriving (Show, Eq, Functor, Foldable, Traversable)
-
-instance PShow Exp where pShowPrec p = text . show
-
-pattern Pi h n a b = Exp (Pi_ h n a b)
-pattern Lam h n a b = Exp (Lam_ h n a b)
-pattern Con a b = Exp (Con_ a b)
-pattern ELit a = Exp (ELit_ a)
-pattern Fun a b = Exp (Fun_ a b)
-pattern EApp a b = Exp (App_ a b)
-pattern Var a b = Exp (Var_ a b)
-pattern TType = Exp TType_
-pattern ELet a b c = Exp (Let_ a b c)
-pattern EFieldProj a b = Exp (EFieldProj_ a b)
-
-newtype Exp = Exp (Exp_ Exp)
-  deriving (Show, Eq)
-
-type ConvM a = StateT [SName] (Reader [SName]) a
-
-newName = gets head <* modify tail
-
-toExp :: I.Exp -> Exp
-toExp = flip runReader [] . flip evalStateT freshTypeVars . f
-  where
-    f = \case
-        I.FunN "swizzvector" [_, _, _, exp, getSwizzVec -> Just (concat -> s)] -> newName >>= \n -> do
-            e <- f exp
-            return $ app' (EFieldProj (Pi Visible n (tyOf e) (TVec (length s) TFloat)) s) e
-        I.FunN "swizzscalar" [_, _, exp, mkSwizzStr -> Just s] -> newName >>= \n -> do
-            e <- f exp
-            return $ app' (EFieldProj (Pi Visible n (tyOf e) TFloat) s) e
-        I.Var i -> asks $ uncurry Var . (!!! i)
-        I.Pi b x y -> newName >>= \n -> do
-            t <- f x
-            Pi b n t <$> local ((n, t):) (f y)
-        I.Lam b x y -> newName >>= \n -> do
-            t <- f x
-            Lam b (PVar t n) t <$> local ((n, t):) (f y)
-        I.Con (I.ConName s _ _ t) xs -> con s <$> f t <*> mapM f xs
-        I.TyCon (I.TyConName s _ _ t _ _) xs -> con s <$> f t <*> mapM f xs
-        I.ELit l -> pure $ ELit l
-        I.Fun (I.FunName s _ t) xs -> fun s <$> f t <*> mapM f xs
-        I.CaseFun (I.CaseFunName s t _) xs -> fun s <$> f t <*> mapM f xs
-        I.App a b -> app' <$> f a <*> f b
-        I.Label x _ -> f x
-        I.TType -> pure TType
-        I.LabelEnd x -> f x
-        z -> error $ "toExp: " ++ show z
-
-getSwizzVec = \case
-    I.VV2 _ (mkSwizzStr -> Just sx) (mkSwizzStr -> Just sy) -> Just [sx, sy]
-    I.VV3 _ (mkSwizzStr -> Just sx) (mkSwizzStr -> Just sy) (mkSwizzStr -> Just sz) -> Just [sx, sy, sz]
-    I.VV4 _ (mkSwizzStr -> Just sx) (mkSwizzStr -> Just sy) (mkSwizzStr -> Just sz) (mkSwizzStr -> Just sw) -> Just [sx, sy, sz, sw]
-    _ -> Nothing
-
-mkSwizzStr = \case
-    I.ConN "Sx" [] -> Just "x"
-    I.ConN "Sy" [] -> Just "y"
-    I.ConN "Sz" [] -> Just "z"
-    I.ConN "Sw" [] -> Just "w"
-    _ -> Nothing
-
-xs !!! i | i < 0 || i >= length xs = error $ show xs ++ " !! " ++ show i
-xs !!! i = xs !! i
-
-untick ('\'': s) = s
-untick s = s
-
-fun s t xs = Fun (untick s, t) xs
-
-con (untick -> s) t xs = Con (s, t) xs
-
-freeVars :: Exp -> S.Set SName
-freeVars = \case
-    Var n _ -> S.singleton n
-    Con _ xs -> S.unions $ map freeVars xs
-    ELit _ -> mempty
-    Fun _ xs -> S.unions $ map freeVars xs
-    EApp a b -> freeVars a `S.union` freeVars b
-    Pi _ n a b -> freeVars a `S.union` (S.delete n $ freeVars b)
-    Lam _ n a b -> freeVars a `S.union` (foldr S.delete (freeVars b) (patVars n))
-    EFieldProj a _ -> freeVars a
-    TType -> mempty
-    ELet n a b -> freeVars a `S.union` (foldr S.delete (freeVars b) (patVars n))
-
-type Ty = Exp
-
-tyOf :: Exp -> Ty
-tyOf = \case
-    Lam h (PVar _ n) t x -> Pi h n t $ tyOf x
-    EApp f x -> app (tyOf f) x
-    Var _ t -> t
-    Pi{} -> Type
-    Con (_, t) xs -> foldl app t xs
-    Fun (_, t) xs -> foldl app t xs
-    ELit l -> toExp $ I.litType l
-    TType -> TType
-    ELet a b c -> tyOf $ EApp (ELam a c) b
-    EFieldProj t s -> t
-    x -> error $ "tyOf: " ++ show x
-  where
-    app (Pi _ n a b) x = substE n x b
-
-substE n x = \case
-    z@(Var n' _) | n' == n -> x
-                 | otherwise -> z 
-    Pi h n' a b | n == n' -> Pi h n' (substE n x a) b
-    Pi h n' a b -> Pi h n' (substE n x a) (substE n x b)
-    Lam h n' a b -> Lam h n' (substE n x a) $ if n `elem` patVars n' then b else substE n x b
-    Con cn xs -> Con cn (map (substE n x) xs)
-    Fun cn xs -> Fun cn (map (substE n x) xs)
-    TType -> TType
-    EApp a b -> app' (substE n x a) (substE n x b)
-    z -> error $ "substE: " ++ show z
-
-app' (Lam _ (PVar _ n) _ x) b = substE n b x
-app' a b = EApp a b
-
---------------------------------------------------------------------------------
-
-data Pat
-    = PVar Exp SName
-    | PTuple [Pat]
-    deriving (Eq, Show)
-
-instance PShow Pat where pShowPrec p = text . show
-
-patVars (PVar _ n) = [n]
-patVars (PTuple ps) = concatMap patVars ps
-
-patTy (PVar t _) = t
-patTy (PTuple ps) = Con ("Tuple" ++ show (length ps), tupTy $ length ps) $ map patTy ps
-
-tupTy n = foldr (:~>) Type $ replicate n Type
-
--------------
-
-pattern EVar n <- Var n _
-pattern TVar t n = Var n t
-
-pattern ELam n b <- Lam Visible n _ b where ELam n b = Lam Visible n (patTy n) b
-
-pattern a :~> b = Pi Visible "" a b
-infixr 1 :~>
-
-pattern PrimN n xs <- Fun (n, t) (filterRelevant (n, 0) t -> xs) where PrimN n xs = Fun (n, hackType n) xs
-pattern Prim1 n a = PrimN n [a]
-pattern Prim2 n a b = PrimN n [a, b]
-pattern Prim3 n a b c <- PrimN n [a, b, c]
-pattern Prim4 n a b c d <- PrimN n [a, b, c, d]
-pattern Prim5 n a b c d e <- PrimN n [a, b, c, d, e]
-
--- todo: remove
-hackType = \case
-    "Output" -> TType
-    "Bool" -> TType
-    "Float" -> TType
-    "Nat" -> TType
-    "Zero" -> TNat
-    "Succ" -> TNat :~> TNat
-    "String" -> TType
-    "Sampler" -> TType
-    "VecS" -> TType :~> TNat :~> TType
---    "EFieldProj" -> Pi Visible "projt" TType $ Pi Visible "projt2" TString $ Pi Visible "projvec" (TVec (error "pn1") TFloat) (TVec (error "pn2") TFloat)
-    n -> error $ "type of " ++ show n
-
-filterRelevant _ _ [] = []
-filterRelevant i (Pi h n t t') (x: xs) = (if h == Visible || exception i then (x:) else id) $ filterRelevant (id *** (+1) $ i) (substE n x t') xs
-  where
-    -- todo: remove
-    exception i = i `elem` [("ColorImage", 0), ("DepthImage", 0), ("StencilImage", 0)]
-
-pattern AN n xs <- Con (n, t) (filterRelevant (n, 0) t -> xs) where AN n xs = Con (n, hackType n) xs
-pattern A0 n = AN n []
-pattern A1 n a = AN n [a]
-pattern A2 n a b = AN n [a, b]
-pattern A3 n a b c <- AN n [a, b, c]
-pattern A4 n a b c d <- AN n [a, b, c, d]
-pattern A5 n a b c d e <- AN n [a, b, c, d, e]
-
-pattern TCon0 n = A0 n
-pattern TCon t n = Con (n, t) []
-
-pattern Type   = TType
-pattern Star   = TType
-pattern TUnit  <- A0 "Tuple0"
-pattern TBool  <- A0 "Bool"
-pattern TWord  <- A0 "Word"
-pattern TInt   <- A0 "Int"
-pattern TNat   = A0 "Nat"
-pattern TFloat = A0 "Float"
-pattern TString = A0 "String"
-pattern TList n <- A1 "List" n
-
-pattern TSampler = A0 "Sampler"
-pattern TFrameBuffer a b <- A2 "FrameBuffer" a b
-pattern Depth n     <- A1 "Depth" n
-pattern Stencil n   <- A1 "Stencil" n
-pattern Color n     <- A1 "Color" n
-
-pattern Zero = A0 "Zero"
-pattern Succ n = A1 "Succ" n
-
-pattern TVec n a = A2 "VecS" a (Nat n)
-pattern TMat i j a <- A3 "Mat" (Nat i) (Nat j) a
-
-pattern Nat n <- (fromNat -> Just n) where Nat n = toNat n
-
-toNat :: Int -> Exp
-toNat 0 = Zero
-toNat n = Succ (toNat $ n-1)
-
-fromNat :: Exp -> Maybe Int
-fromNat Zero = Just 0
-fromNat (Succ n) = (1 +) <$> fromNat n
-
-pattern TTuple xs <- (getTuple -> Just xs)
-pattern ETuple xs <- (getTuple -> Just xs)
-
-getTuple = \case
-    AN "Tuple0" [] -> Just []
-    AN "Tuple2" [a, b] -> Just [a, b]
-    AN "Tuple3" [a, b, c] -> Just [a, b, c]
-    AN "Tuple4" [a, b, c, d] -> Just [a, b, c, d]
-    AN "Tuple5" [a, b, c, d, e] -> Just [a, b, c, d, e]
-    AN "Tuple6" [a, b, c, d, e, f] -> Just [a, b, c, d, e, f]
-    AN "Tuple7" [a, b, c, d, e, f, g] -> Just [a, b, c, d, e, f, g]
-    _ -> Nothing
-
-pattern ERecord a <- (const Nothing -> Just a)
-
---------------------------------------------------------------------------------
-
-showN = id
-show5 = show
-
-pattern ExpN a = a
-
-newtype ErrorMsg = ErrorMsg String
-instance Show ErrorMsg where show (ErrorMsg s) = s
-
-type ErrorT = ExceptT ErrorMsg
-mapError f e = e
-pattern InFile :: String -> ErrorMsg -> ErrorMsg
-pattern InFile s e <- ((,) "?" -> (s, e)) where InFile _ e = e
-
-type Info = (SourcePos, SourcePos, String)
-type Infos = [Info]
-
-type PolyEnv = I.GlobalEnv
-
-joinPolyEnvs :: MonadError ErrorMsg m => Bool -> [PolyEnv] -> m PolyEnv
-joinPolyEnvs _ = return . mconcat
-getPolyEnv = id
-
-type MName = SName
-type VarMT = StateT FreshVars
-type FreshVars = [String]
-freshTypeVars = (flip (:) <$> map show [0..] <*> ['a'..'z'])
-
-throwErrorTCM :: MonadError ErrorMsg m => Doc -> m a
-throwErrorTCM d = throwError $ ErrorMsg $ show d
-
-infos = const []
-
-type EName = SName
-
-parseLC :: MonadError ErrorMsg m => FilePath -> String -> m ModuleR
-parseLC f s = either (throwError . ErrorMsg) return (I.parse f s)
-
-inference_ :: PolyEnv -> ModuleR -> ErrorT (WriterT Infos (VarMT Identity)) PolyEnv
-inference_ pe m = mdo
-    defs <- either (throwError . ErrorMsg) return $ definitions m $ I.mkGlobalEnv' defs `I.joinGlobalEnv'` I.extractGlobalEnv' pe
-    either (throwError . ErrorMsg) return $ I.infer pe defs
-
-reduce = id
-
-type Item = (I.Exp, I.Exp)
-
-tyOfItem :: Item -> Exp
-tyOfItem = toExp . snd
-
-pattern ISubst a b <- ((,) () -> (a, (toExp -> b, tb)))
-
-dummyPos :: SourcePos
-dummyPos = newPos "" 0 0
-
-showErr e = (dummyPos, dummyPos, e)
-
diff --git a/prototypes/CoreToGLSL.hs b/prototypes/CoreToGLSL.hs
deleted file mode 120000
index b9ebdd27..00000000
--- a/prototypes/CoreToGLSL.hs
+++ /dev/null
@@ -1 +0,0 @@
-../CoreToGLSL.hs
\ No newline at end of file
diff --git a/prototypes/CoreToIR.hs b/prototypes/CoreToIR.hs
deleted file mode 120000
index 7f32ac4d..00000000
--- a/prototypes/CoreToIR.hs
+++ /dev/null
@@ -1 +0,0 @@
-../CoreToIR.hs
\ No newline at end of file
diff --git a/prototypes/Driver.hs b/prototypes/Driver.hs
deleted file mode 120000
index 882f3164..00000000
--- a/prototypes/Driver.hs
+++ /dev/null
@@ -1 +0,0 @@
-../Driver.hs
\ No newline at end of file
diff --git a/prototypes/IR.hs b/prototypes/IR.hs
deleted file mode 120000
index ae04b92e..00000000
--- a/prototypes/IR.hs
+++ /dev/null
@@ -1 +0,0 @@
-../IR.hs
\ No newline at end of file
diff --git a/prototypes/Infer.hs b/prototypes/Infer.hs
deleted file mode 100644
index d4cb8775..00000000
--- a/prototypes/Infer.hs
+++ /dev/null
@@ -1,2247 +0,0 @@
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE RecursiveDo #-}
-module Infer
-    ( Binder (..), SName, Lit(..), Visibility(..), FunName(..), CaseFunName(..), ConName(..), TyConName(..), Export(..), ModuleR(..)
-    , Exp (..), GlobalEnv
-    , pattern Var, pattern Fun, pattern CaseFun, pattern App, pattern FunN, pattern ConN, pattern VV2, pattern VV3, pattern VV4, pattern Pi
-    , parse
-    , mkGlobalEnv', joinGlobalEnv', extractGlobalEnv'
-    , litType, infer
-    ) where
-
-import Data.Monoid
-import Data.Maybe
-import Data.List
-import Data.Char
-import Data.String
-import qualified Data.Set as Set
-import qualified Data.Map as Map
-
-import Control.Monad.Except
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Identity
-import Control.Arrow
-import Control.Applicative hiding (optional)
-import Control.Exception hiding (try)
-
-import Text.Parsec hiding (parse, label, Empty, State, (<|>), many, optional)
-import qualified Text.Parsec.Token as Pa
-import Text.Parsec.Pos
-import Text.Parsec.Indentation hiding (Any)
-import Text.Parsec.Indentation.Char
-import Text.Parsec.Indentation.Token
-
-import Debug.Trace
-
-import qualified Pretty as P
-
--------------------------------------------------------------------------------- source data
-
-type SName = String
-
-data Stmt
-    = Let SName MFixity (Maybe SExp) [Visibility]{-source arity-} SExp
-    | Data SName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SName, SExp)]{-constructor names and types-}
-    | Primitive (Maybe Bool{-Just True: type constructor; Just False: constructor; Nothing: function-}) SName SExp{-type-}
-    | PrecDef SName Fixity
-    | ValueDef ([SName], Pat) SExp
-
-    -- eliminated during parsing
-    | TypeAnn SName SExp            -- intermediate
-    | FunAlt SName [((Visibility, SExp), Pat)] (Maybe SExp) SExp
-    deriving (Show)
-
-data SExp
-    = SGlobal SName
-    | SBind Binder SExp SExp
-    | SApp Visibility SExp SExp
-    | SLet SExp SExp    -- let x = e in f   -->  SLet e f{-x is Var 0-}
-    | SVar !Int
-    | STyped ExpType
-  deriving (Eq, Show)
-
-type FixityMap = Map.Map SName Fixity
-type ConsMap = Map.Map SName ((SName{-type name-}, Int{-num of indices-}), [(SName, Int)]{-constructors with arities-})
-type GlobalEnv' = (FixityMap, ConsMap)
-
-type Fixity = (Maybe FixityDir, Int)
-type MFixity = Maybe Fixity
-data FixityDir = FDLeft | FDRight deriving (Show)
-
-data Binder
-    = BPi  Visibility
-    | BLam Visibility
-    | BMeta      -- a metavariable is like a floating hidden lambda
-  deriving (Eq, Show)
-
-data Visibility = Hidden | Visible
-  deriving (Eq, Show)
-
-sLit a = STyped (ELit a, litType a)
-pattern SType  = STyped (TType, TType)
-pattern SPi  h a b = SBind (BPi  h) a b
-pattern SLam h a b = SBind (BLam h) a b
-pattern Wildcard t = SBind BMeta t (SVar 0)
-pattern SAppH a b = SApp Hidden a b
-pattern SAppV a b = SApp Visible a b
-pattern SAnn a t = STyped (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a  --  a :: t ~~> id t a
-pattern TyType a = STyped (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a
-    -- same as  (a :: TType)     --  a :: TType   ~~>   (\(x :: TType) -> x) a
---pattern CheckSame' a b c = SGlobal "checkSame" `SAppV` STyped a `SAppV` STyped b `SAppV` c
-pattern SCstr a b = SGlobal "cstr" `SAppV` a `SAppV` b          --    a ~ b
-pattern SLabelEnd a = SGlobal "labelend" `SAppV` a
-
-isPi (BPi _) = True
-isPi _ = False
-
-infixl 1 `SAppV`, `SAppH`, `App`
-
--------------------------------------------------------------------------------- destination data
-
-data Exp
-    = Bind Binder Exp Exp   -- TODO: prohibit meta binder here;  BLam is not allowed
-    | Lam Visibility Exp Exp
-    | Con ConName [Exp]
-    | TyCon TyConName [Exp]
-    | ELit Lit
-    | Assign !Int Exp Exp       -- De Bruijn index decreasing assign operator, only for metavariables (non-recursive) -- TODO: remove
-    | Label Exp{-function alternatives are obeyed during reduction-} Exp{-functions are treated like constants-}
-            -- label is used also for getting fixity info
-    | LabelEnd Exp
-    | Neut Neutral
-    | TType
-  deriving (Show)
-
-data Neutral
-    = Fun_ FunName [Exp]
-    | CaseFun_ CaseFunName [Exp]
-    | App_ Exp{-todo: Neutral-} Exp
-    | Var_ !Int                 -- De Bruijn variable
-  deriving (Show)
-
-type Type = Exp
-
-data ConName = ConName SName MFixity Int Type
-instance Show ConName where show (ConName n _ _ _) = n
-instance Eq ConName where ConName n _ _ _ == ConName n' _ _ _ = n == n'
-
-conTypeName :: ConName -> TyConName
-conTypeName (ConName _ _ _ t) = case snd (getParams t) of
-    TyCon n _ -> n
-    _ -> error "impossible"
-
-data TyConName = TyConName SName MFixity Int{-num of indices-} Type [ConName]{-constructors-} Type{-case type-}
-instance Show TyConName where show (TyConName n _ _ _ _ _) = n
-instance Eq TyConName where TyConName n _ _ _ _ _ == TyConName n' _ _ _ _ _ = n == n'
-
-data FunName = FunName SName MFixity Type
-instance Show FunName where show (FunName n _ _) = n
-instance Eq FunName where FunName n _ _ == FunName n' _ _ = n == n'
-
-data CaseFunName = CaseFunName SName Type Int{-num of parameters-}
-instance Show CaseFunName where show (CaseFunName n _ _) = n
-instance Eq CaseFunName where CaseFunName n _ _ == CaseFunName n' _ _ = n == n'
-
-caseName (c:cs) = toLower c: cs ++ "Case"
-
-type ExpType = (Exp, Type)
-
-pattern Fun a b = Neut (Fun_ a b)
-pattern CaseFun a b = Neut (CaseFun_ a b)
-pattern FunN a b <- Fun (FunName a _ _) b
-pattern CaseFunN a b <- CaseFun (CaseFunName a _ _) b
-pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b
-pattern TCaseFun a t i b = CaseFun (CaseFunName a t i) b
-pattern App a b = Neut (App_ a b)
-pattern Var a = Neut (Var_ a)
-
-data Lit
-    = LInt !Int
-    | LChar Char
-    | LFloat Double
-    | LString String
-  deriving (Eq)
-
-instance Show Lit where
-    show = \case
-        LFloat x  -> show x
-        LString x -> show x
-        LInt x    -> show x
-        LChar x   -> show x
-
-pattern Lam' b  <- Lam _ _ b
-pattern Pi  h a b = Bind (BPi h) a b
-pattern Meta  a b = Bind BMeta a b
-
-pattern Cstr a b    = TFun "cstr" (TType :~> TType :~> TType){-todo-} [a, b]
-pattern ReflCstr x  = TFun "reflCstr" (TType :~> Cstr (Var 0) (Var 0)) [x]
-pattern Coe a b w x = TFun "coe" (TType :~> TType :~> Cstr (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x]
-
-pattern ConN s a   <- Con (ConName s _ _ _) a
-pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a
-pattern TCon s i t a <- Con (ConName s _ i t) a where TCon s i t a = Con (ConName s Nothing i t) a  -- todo: don't match on type
-pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ error "TTyCon") a
-pattern TTyCon0 s  <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = TyCon (TyConName s Nothing (error "todo: inum2") TType (error "todo: tcn cons 3") $ error "TTyCon0") []
-pattern Sigma a b  <- TyConN "Sigma" [a, Lam' b] where Sigma a b = TTyCon "Sigma" (error "sigmatype") [a, Lam Visible a{-todo: don't duplicate-} b]
-pattern Unit        = TTyCon0 "Unit"
-pattern TT          = TCon "TT" 0 Unit []
-pattern T2 a b      = TFun "T2" (TType :~> TType :~> TType) [a, b]
-pattern T2C a b     = TCon "T2C" (-1) (Unit :~> Unit :~> Unit) [a, b]
-pattern Empty       = TTyCon0 "Empty"
-pattern TInt        = TTyCon0 "Int"
-pattern TNat        = TTyCon0 "Nat"
-pattern TBool       = TTyCon0 "Bool"
-pattern TFloat      = TTyCon0 "Float"
-pattern TString     = TTyCon0 "String"
-pattern TChar       = TTyCon0 "Char"
-pattern TOrdering   = TTyCon0 "'Ordering"
-pattern Zero        = TCon "Zero" 0 TNat []
-pattern Succ n      = TCon "Succ" 1 (TNat :~> TNat) [n]
---pattern TVec a b    = TTyCon "'Vec" (TNat :~> TType :~> TType) [a, b]
-pattern TVec a b    = TTyCon "'VecS" (TType :~> TNat :~> TType) [b, a]
-pattern TFrameBuffer a b = TTyCon "'FrameBuffer" (TNat :~> TType :~> TType) [a, b]
-pattern TRecord a   = TTyCon "'RecordC" TRecordType [a]
-pattern TList a     = TTyCon "'List" (TType :~> TType) [a]
-pattern Tuple2 a b c d = TCon "Tuple2" 0 Tuple2Type [a, b, c, d]
-pattern Tuple0      = TCon "Tuple0" 0 Tuple0Type []
-pattern VV2 t x y   = TCon "V2" 0 V2Type [t, x, y]
-pattern VV3 t x y z = TCon "V3" 1 V3Type [t, x, y, z]
-pattern VV4 t x y z w = TCon "V4" 2 V4Type [t, x, y, z, w]
-pattern CSplit a b c <- FunN "Split" [a, b, c]
-
-pattern Tuple0Type :: Exp
-pattern Tuple0Type  <- _ where Tuple0Type   = TTyCon0 "'Tuple0"
-pattern Tuple2Type :: Exp
-pattern Tuple2Type  <- _ where Tuple2Type   = Pi Hidden TType $ Pi Hidden TType $ Var 1 :~> Var 1 :~> tTuple2 (Var 3) (Var 2)
-pattern V2Type :: Exp
-pattern V2Type  <- _ where V2Type   = Pi Hidden TType $ Var 0 :~> Var 1 :~> TVec (toNatE 2) (Var 2)
-pattern V3Type :: Exp
-pattern V3Type  <- _ where V3Type   = Pi Hidden TType $ Var 0 :~> Var 1 :~> Var 2 :~> TVec (toNatE 3) (Var 3)
-pattern V4Type :: Exp
-pattern V4Type  <- _ where V4Type   = Pi Hidden TType $ Var 0 :~> Var 1 :~> Var 2 :~> Var 3 :~> TVec (toNatE 4) (Var 4)
-pattern TRecordType :: Exp
-pattern TRecordType <- _ where TRecordType  = TList SListEType :~> TType
-pattern NilType :: Exp
-pattern NilType     <- _ where NilType      = Pi Hidden TType $ TList (Var 0)
-pattern ConsType :: Exp
-pattern ConsType    <- _ where ConsType     = Pi Hidden TType $ Var 0 :~> TList (Var 1) :~> TList (Var 2)
-
-pattern VNil        = TCon "Nil" 0 NilType [SListEType]
-pattern VCons a b   = TCon "Cons" 1 ConsType [SListEType, VT2 a, b]
-
-pattern VT2 :: (String, Exp) -> Exp
-pattern VT2 se <- TCon "Tuple2" 0 _ (listT2 -> Just se)  where VT2 (s, e) = Tuple2 TString TType (ELit $ LString s) e
-
-listT2 [_, _, ELit (LString s), e] = Just (s, e)
-listT2 x = Nothing
-
-pattern SListEType :: Exp
-pattern SListEType  <- _ where SListEType   = tTuple2 TString TType
-
-tTuple2 a b = TTyCon "'Tuple2" (TType :~> TType :~> TType) [a, b]
-tTuple3 a b c = TTyCon "'Tuple3" (TType :~> TType :~> TType :~> TType) [a, b, c]
-tMat a b c = TTyCon "'Mat" (TNat :~> TNat :~> TType :~> TType) [a, b, c]
-
-toNatE :: Int -> Exp
-toNatE 0         = Zero
-toNatE n | n > 0 = Succ (toNatE (n - 1))
-
-t2C TT TT = TT
-t2C a b = T2C a b
-
-t2 Unit a = a
-t2 a Unit = a
-t2 Empty _ = Empty
-t2 _ Empty = Empty
-t2 a b = TFun "T2" (TType :~> TType :~> TType) [a, b]
-
-pattern EInt a      = ELit (LInt a)
-pattern EFloat a    = ELit (LFloat a)
-
-mkBool False = TCon "False" 0 TBool []
-mkBool True  = VTrue
-pattern VTrue = TCon "True" 1 TBool []
-
-pattern LCon <- (isCon -> True)
-pattern CFun <- (caseFunName -> True)
-
-pattern a :~> b = Bind (BPi Visible) a b
-
-infixr 1 :~>
-
-caseFunName (Fun f _) = True
-caseFunName (CaseFun f _) = True
-caseFunName _ = False
-
-isCon = \case
-    TType   -> True
-    Con _ _ -> True
-    TyCon _ _ -> True
-    ELit _  -> True
-    _ -> False
-
--------------------------------------------------------------------------------- environments
-
--- SExp + Exp zipper
-data Env
-    = EBind1 Binder Env SExp            -- zoom into first parameter of SBind
-    | EBind2 Binder Exp Env             -- zoom into second parameter of SBind
-    | EApp1 Visibility Env SExp
-    | EApp2 Visibility Exp Env
-    | ELet1 Env SExp
-    | ELet2 ExpType Env
-    | EGlobal GlobalEnv [Stmt]
-    | ELabelEnd Env
-
-    | EBind1' Binder Env Exp            -- todo: move Exp zipper constructor to a separate ADT (if needed)
-    | EPrim SName [Exp] Env [Exp]    -- todo: move Exp zipper constructor to a separate ADT (if needed)
-
-    | EAssign Int Exp Env
-    | CheckType Exp Env
-    | CheckSame Exp Env
-    | CheckAppType Visibility Exp Env SExp
-  deriving Show
-
---pattern CheckAppType h t te b = EApp1 h (CheckType t te) b
-
-type GlobalEnv = Map.Map SName (Exp, Type)
-
-extractEnv :: Env -> GlobalEnv
-extractEnv = either id extractEnv . parent
-
-parent = \case
-    EAssign _ _ x        -> Right x
-    EBind2 _ _ x         -> Right x
-    EBind1 _ x _         -> Right x
-    EBind1' _ x _        -> Right x
-    EApp1 _ x _          -> Right x
-    EApp2 _ _ x          -> Right x
-    ELet1 x _            -> Right x
-    ELet2 _ x            -> Right x
-    CheckType _ x        -> Right x
-    CheckSame _ x        -> Right x
-    CheckAppType _ _ x _ -> Right x
-    EPrim _ _ x _        -> Right x
-    ELabelEnd x          -> Right x
-    EGlobal x _          -> Left x
-
-
-initEnv :: GlobalEnv
-initEnv = Map.fromList
-    [ (,) "Type" (TType, TType)     -- needed?
-    ]
-
--- monad used during elaborating statments -- TODO: use zippers instead
-type ElabStmtM m = StateT GlobalEnv (ExceptT String m)
-
--------------------------------------------------------------------------------- low-level toolbox
-
-getFunName (fst . getApps' -> Fun f _) = Just f
-getFunName _ = Nothing
-
-label x (LabelEnd y) = y
-label x y = Label x y
-
-pattern UBind a b c = {-UnLabel-} (Bind a b c)      -- todo: review
-pattern UApp a b = {-UnLabel-} (App a b)            -- todo: review
-pattern UVar n = Var n
-
-instance Eq Exp where
-    Label a _ == Label a' _ = a == a'
-    Lam' a == Lam' a' = a == a'
-    Bind a b c == Bind a' b' c' = (a, b, c) == (a', b', c')
-    -- Assign a b c == Assign a' b' c' = (a, b, c) == (a', b', c')
-    Fun a b == Fun a' b' = (a, b) == (a', b')
-    CaseFun a b == CaseFun a' b' = (a, b) == (a', b')
-    Con a b == Con a' b' = (a, b) == (a', b')
-    TyCon a b == TyCon a' b' = (a, b) == (a', b')
-    TType == TType = True
-    ELit l == ELit l' = l == l'
-    App a b == App a' b' = (a, b) == (a', b')
-    Var a == Var a' = a == a'
-    LabelEnd a == LabelEnd a' = a == a'  -- ???
-    _ == _ = False
-
-assign :: (Int -> Exp -> Exp -> a) -> (Int -> Exp -> Exp -> a) -> Int -> Exp -> Exp -> a
-assign _ clet i (Var j) b | i > j = clet j (Var (i-1)) $ substE "assign" j (Var (i-1)) $ up1E i b
-assign clet _ i a b = clet i a b
-
-handleLet i j f
-    | i >  j = f (i-1) j
-    | i <= j = f i (j+1)
-
-foldS g f i = \case
-    SApp _ a b -> foldS g f i a <> foldS g f i b
-    SLet a b -> foldS g f i a <> foldS g f (i+1) b
-    SBind _ a b -> foldS g f i a <> foldS g f (i+1) b
-    STyped (e, t) -> foldE f i e <> foldE f i t
-    SVar j -> foldE f i (Var j)
-    SGlobal x -> g i x
-
-foldE f i = \case
-    Label x _ -> foldE f i x
-    Var k -> f i k
-    Lam' b -> {-foldE f i t <>  todo: explain why this is not needed -} foldE f (i+1) b
-    Bind _ a b -> foldE f i a <> foldE f (i+1) b
-    Fun _ as -> foldMap (foldE f i) as
-    CaseFun _ as -> foldMap (foldE f i) as
-    Con _ as -> foldMap (foldE f i) as
-    TyCon _ as -> foldMap (foldE f i) as
-    TType -> mempty
-    ELit _ -> mempty
-    App a b -> foldE f i a <> foldE f i b
-    Assign j x a -> handleLet i j $ \i' j' -> foldE f i' x <> foldE f i' a
-    LabelEnd x -> foldE f i x
-
-freeS = nub . foldS (\_ s -> [s]) mempty 0
-freeE = foldE (\i k -> Set.fromList [k - i | k >= i]) 0
-
-usedS = (getAny .) . foldS mempty ((Any .) . (==))
-usedE = (getAny .) . foldE ((Any .) . (==))
-
-mapS = mapS_ (const SGlobal)
-mapS_ gg ff = mapS__ gg ff $ \i j -> case ff i $ Var j of
-            Var k -> SVar k
-            -- x -> STyped x -- todo
-mapS__ gg f1 f2 h e = g e where
-    g i = \case
-        SApp v a b -> SApp v (g i a) (g i b)
-        SLet a b -> SLet (g i a) (g (h i) b)
-        SBind k a b -> SBind k (g i a) (g (h i) b)
-        STyped (x, t) -> STyped (f1 i x, f1 i t)
-        SVar j -> f2 i j
-        SGlobal x -> gg i x
-
-rearrangeS :: (Int -> Int) -> SExp -> SExp
-rearrangeS f = mapS__ (const SGlobal) (const id) (\i j -> SVar $ if j < i then j else i + f (j - i)) (+1) 0
-
-upS__ i n = mapS (\i -> upE i n) (+1) i
-upS = upS__ 0 1
-
-up1E i = \case
-    Var k -> Var $ if k >= i then k+1 else k
-    Lam h a b -> Lam h (up1E i a) (up1E (i+1) b)
-    Bind h a b -> Bind h (up1E i a) (up1E (i+1) b)
-    Fun s as  -> Fun s $ map (up1E i) as
-    CaseFun s as  -> CaseFun s $ map (up1E i) as
-    Con s as  -> Con s $ map (up1E i) as
-    TyCon s as -> TyCon s $ map (up1E i) as
-    TType -> TType
-    ELit l -> ELit l
-    App a b -> App (up1E i a) (up1E i b)
-    Assign j a b -> handleLet i j $ \i' j' -> assign Assign Assign j' (up1E i' a) (up1E i' b)
-    Label x y -> Label (up1E i x) $ up1E i y
-    LabelEnd x -> LabelEnd $ up1E i x
-
-upE i n e = iterateN n (up1E i) e
-
-substSS :: Int -> SExp -> SExp -> SExp
-substSS k x = mapS__ (const SGlobal) (error "substSS") (\(i, x) j -> case compare j i of
-            EQ -> x
-            GT -> SVar $ j - 1
-            LT -> SVar j
-            ) ((+1) *** upS) (k, x)
-substS j x = mapS (uncurry $ substE "substS") ((+1) *** up1E 0) (j, x)
-substSG j x = mapS_ (\x i -> if i == j then x else SGlobal i) (const id) upS x
-
-substE err = substE_ (error $ "substE: todo: environment required in " ++ err)  -- todo: remove
-
-substE_ :: Env -> Int -> Exp -> Exp -> Exp
-substE_ te i x = \case
-    Label z v -> label (substE "slab" i x z) $ substE_ te{-todo: label env?-} i x v
-    Var k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> x
-    Lam h a b -> let  -- question: is mutual recursion good here?
-            a' = substE_ (EBind1' (BLam h) te b') i x a
-            b' = substE_ (EBind2 (BLam h) a' te) (i+1) (up1E 0 x) b
-        in Lam h a' b'
-    Bind h a b -> let  -- question: is mutual recursion good here?
-            a' = substE_ (EBind1' h te b') i x a
-            b' = substE_ (EBind2 h a' te) (i+1) (up1E 0 x) b
-        in Bind h a' b'
-    Fun s as  -> eval te $ Fun s [substE_ te{-todo: precise env?-} i x a | (xs, a, ys) <- holes as]
-    CaseFun s as  -> eval te $ CaseFun s [substE_ te{-todo: precise env?-} i x a | (xs, a, ys) <- holes as]
-    Con s as  -> Con s [substE_ te{-todo-} i x a | (xs, a, ys) <- holes as]
-    TyCon s as -> TyCon s [substE_ te{-todo-} i x a | (xs, a, ys) <- holes as]
-    TType -> TType
-    ELit l -> ELit l
-    App a b  -> app_ (substE_ te i x a) (substE_ te i x b)  -- todo: precise env?
-    Assign j a b
-        | j > i, Just a' <- downE i a       -> assign Assign Assign (j-1) a' (substE "sa" i (substE "sa" (j-1) a' x) b)
-        | j > i, Just x' <- downE (j-1) x   -> assign Assign Assign (j-1) (substE "sa" i x' a) (substE "sa" i x' b)
-        | j < i, Just a' <- downE (i-1) a   -> assign Assign Assign j a' (substE "sa" (i-1) (substE "sa" j a' x) b)
-        | j < i, Just x' <- downE j x       -> assign Assign Assign j (substE "sa" (i-1) x' a) (substE "sa" (i-1) x' b)
-        | j == i    -> Meta (cstr x a) $ up1E 0 b
-    LabelEnd a -> LabelEnd $ substE_ te i x a
-
-downS t x | usedS t x = Nothing
-          | otherwise = Just $ substS t (error "impossible: downS") x
-downE t x | usedE t x = Nothing
-          | otherwise = Just $ substE_ (error "impossible") t (error "impossible: downE") x
-
-varType :: String -> Int -> Env -> (Binder, Exp)
-varType err n_ env = f n_ env where
-    f n (EAssign i x es) = id *** substE "varType" i x $ f (if n < i then n else n+1) es
-    f n (EBind2 b t es)  = if n == 0 then (b, up1E 0 t) else id *** up1E 0 $ f (n-1) es
-    f n (ELet2 (x, t) es) = if n == 0 then (BLam Visible{-??-}, up1E 0 t) else id *** up1E 0 $ f (n-1) es
-    f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ showEnv env) (f n) $ parent e
-
--------------------------------------------------------------------------------- reduction
-
-infixl 1 `app_`
-
-app_ :: Exp -> Exp -> Exp
-app_ (Lam' x) a = substE "app" 0 a x
-app_ (Con s xs) a = Con s (xs ++ [a])
-app_ (TyCon s xs) a = TyCon s (xs ++ [a])
-app_ (Label x e) a = label (app_ x a) $ app_ e a
-app_ (LabelEnd x) a = LabelEnd (app_ x a)   -- ???
-app_ f a = App f a
-
-eval te = \case
-    App a b -> app_ a b
-    Cstr a b -> cstr a b
-    ReflCstr a -> reflCstr te a
-    Coe a b c d -> coe a b c d
-    CaseFun (CaseFunName n t pars) (drop (pars + 1) -> ps@(last -> Con (ConName _ _ i _) (drop pars -> vs))) | i /= (-1) -> foldl app_ (ps !! i) vs
-    T2 a b -> t2 a b
-    FunN "T2C" [a, b] -> t2C a b
-
-    FunN "primAdd" [EInt i, EInt j] -> EInt (i + j)
-    FunN "primSub" [EInt i, EInt j] -> EInt (i - j)
-    FunN "primMod" [EInt i, EInt j] -> EInt (i `mod` j)
-    FunN "primSqrt" [EInt i] -> EInt $ round $ sqrt $ fromIntegral i
-    FunN "primIntEq" [EInt i, EInt j] -> mkBool (i == j)
-    FunN "primIntLess" [EInt i, EInt j] -> mkBool (i < j)
-
-    FunN "compare" [_,_,EInt x, EInt y] -> mkOrdering $ x `compare` y
-    FunN "primCompareFloat" [EFloat x, EFloat y] -> mkOrdering $ x `compare` y
-    FunN "PrimGreaterThan" [_, _, _, _, _, _, _, EFloat x, EFloat y] -> mkBool $ x > y
-    FunN "PrimSubS" [_, _, _, _, EFloat x, EFloat y] -> EFloat (x - y)
-    FunN "PrimSubS" [_, _, _, _, EInt x, EInt y] -> EInt (x - y)
-    FunN "PrimAddS" [_, _, _, _, EFloat x, EFloat y] -> EFloat (x + y)
-    FunN "PrimMulS" [_, _, _, _, EFloat x, EFloat y] -> EFloat (x * y)
-    FunN "zeroComp" [TVec (fromNatE -> Just 2) t@TFloat, TT] -> VV2 t (EFloat 0) (EFloat 0)
-    FunN "zeroComp" [TVec (fromNatE -> Just 3) t@TFloat, TT] -> VV3 t (EFloat 0) (EFloat 0) (EFloat 0)
-    FunN "zeroComp" [TVec (fromNatE -> Just 4) t@TFloat, TT] -> VV4 t (EFloat 0) (EFloat 0) (EFloat 0) (EFloat 0)
-    FunN "oneComp" [TVec (fromNatE -> Just 2) t@TFloat, TT] -> VV2 t (EFloat 1) (EFloat 1)
-    FunN "oneComp" [TVec (fromNatE -> Just 3) t@TFloat, TT] -> VV3 t (EFloat 1) (EFloat 1) (EFloat 1)
-    FunN "oneComp" [TVec (fromNatE -> Just 4) t@TFloat, TT] -> VV4 t (EFloat 1) (EFloat 1) (EFloat 1) (EFloat 1)
-    FunN "oneComp" [TVec (fromNatE -> Just 2) t@TBool, TT] -> VV2 t VTrue VTrue
-    FunN "oneComp" [TVec (fromNatE -> Just 3) t@TBool, TT] -> VV3 t VTrue VTrue VTrue
-    FunN "oneComp" [TVec (fromNatE -> Just 4) t@TBool, TT] -> VV4 t VTrue VTrue VTrue VTrue
-
--- todo: elim
-    Fun n@(FunName "natElim" _ _) [a, z, s, Succ x] -> let      -- todo: replace let with better abstraction
-                sx = s `app_` x
-            in sx `app_` eval (EApp2 Visible sx te) (Fun n [a, z, s, x])
-    FunN "natElim" [_, z, s, Zero] -> z
-    Fun na@(FunName "finElim" _ _) [m, z, s, n, ConN "FSucc" [i, x]] -> let six = s `app_` i `app_` x-- todo: replace let with better abstraction
-        in six `app_` eval (EApp2 Visible six te) (Fun na [m, z, s, i, x])
-    FunN "finElim" [m, z, s, n, ConN "FZero" [i]] -> z `app_` i
-
-    FunN "matchInt" [t, f, TyConN "Int" []] -> t
-    FunN "matchInt" [t, f, c@LCon] -> f `app_` c
-    FunN "matchList" [t, f, TyConN "List" [a]] -> t `app_` a
-    FunN "matchList" [t, f, c@LCon] -> f `app_` c
-
-    FunN "Component" [TVec (fromNatE -> Just 3) TFloat] -> Unit
-    FunN "Component" [TVec (fromNatE -> Just 4) TBool] -> Unit
-    FunN "Component" [TVec (fromNatE -> Just 4) TFloat] -> Unit
-    FunN "Floating" [TVec (fromNatE -> Just 2) TFloat] -> Unit
-    FunN "Floating" [TVec (fromNatE -> Just 4) TFloat] -> Unit
-    Fun n@(FunName "Eq_" _ _) [TyConN "List" [a]] -> eval te $ Fun n [a]
-    FunN "Eq_" [TInt] -> Unit
-    FunN "Eq_" [LCon] -> Empty
-    FunN "Monad" [TyConN "IO" []] -> Unit
-    FunN "Signed" [TFloat] -> Unit
-    FunN "Num" [TFloat] -> Unit
-    FunN "Num" [TInt] -> Unit
-    FunN "ValidFrameBuffer" [n] -> Unit -- todo
-    FunN "ValidOutput" [n] -> Unit      -- todo
-    FunN "AttributeTuple" [n] -> Unit   -- todo
-    FunN "fromInt" [TInt, _, n@EInt{}] -> n
-
-    FunN "VecScalar" [Succ Zero, t] -> t
-    FunN "VecScalar" [n@(Succ (Succ _)), t] -> TVec n t
-    FunN "TFFrameBuffer" [TyConN "'Image" [n, t]] -> TFrameBuffer n t
-    FunN "TFFrameBuffer" [TyConN "'Tuple2" [TyConN "'Image" [i@(fromNatE -> Just n), t], TyConN "'Image" [fromNatE -> Just n', t']]]
-        | n == n' -> TFrameBuffer i $ tTuple2 t t'      -- todo
-    FunN "TFFrameBuffer" [TyConN "'Tuple3" [TyConN "'Image" [i@(fromNatE -> Just n), t], TyConN "'Image" [fromNatE -> Just n', t'], TyConN "'Image" [fromNatE -> Just n'', t'']]]
-        | n == n' && n == n'' -> TFrameBuffer i $ tTuple3 t t' t''      -- todo
-    FunN "FragOps" [TyConN "'FragmentOperation" [t]] -> t
-    FunN "FragOps" [TyConN "'Tuple2" [TyConN "'FragmentOperation" [t], TyConN "'FragmentOperation" [t']]] -> tTuple2 t t'
-    FunN "FTRepr'" [TyConN "'Tuple2" [TyConN "'Interpolated" [t], TyConN "'Interpolated" [t']]] -> tTuple2 t t'          -- todo
-    FunN "FTRepr'" [TyConN "'Tuple2" [TyConN "'List" [t], TyConN "'List" [t']]] -> tTuple2 t t'          -- todo
-    FunN "FTRepr'" [TyConN "'List" [t]] -> t          -- todo
-    FunN "FTRepr'" [TyConN "'Interpolated" [t]] -> t          -- todo
-    FunN "ColorRepr" [TTuple0] -> TTuple0
-    FunN "ColorRepr" [t@NoTup] -> TTyCon "'Color" (TType :~> TType) [t] -- todo
-    FunN "JoinTupleType" [a@TyConN{}, TTuple0] -> a
-    FunN "JoinTupleType" [a@NoTup, b@NoTup] -> tTuple2 a b             -- todo
-    FunN "TFMat" [TVec i a, TVec j a'] | a == a' -> tMat i j a       -- todo
-    FunN "MatVecElem" [TVec _ a] -> a
-    FunN "MatVecElem" [TyConN "'Mat" [_, _, a]] -> a
-    FunN "MatVecScalarElem" [TVec _ a@TFloat] -> a
-    FunN "MatVecScalarElem" [a] | a `elem` [TFloat, TBool, TInt] -> a
-    FunN "fromInt" [TFloat, _, EInt i] -> EFloat $ fromIntegral i
-    FunN "Split" [TRecord (fromVList -> Just xs), TRecord (fromVList -> Just ys), z] -> t2 (foldr1 t2 [cstr t t' | (n, t) <- xs, (n', t') <- ys, n == n']) $ cstr z (TRecord $ toVList $ filter ((`notElem` map fst ys) . fst) xs)
-    FunN "Split" [TRecord (fromVList -> Just xs), z, TRecord (fromVList -> Just ys)] -> t2 (foldr1 t2 [cstr t t' | (n, t) <- xs, (n', t') <- ys, n == n']) $ cstr z (TRecord $ toVList $ filter ((`notElem` map fst ys) . fst) xs)
-    FunN "Split" [z, TRecord (fromVList -> Just xs), TRecord (fromVList -> Just ys)] -> t2 (foldr1 t2 [cstr t t' | (n, t) <- xs, (n', t') <- ys, n == n']) $ cstr z (TRecord $ toVList $ xs ++ filter ((`notElem` map fst xs) . fst) ys)
-    FunN "project" [_, _, _, ELit (LString s), _, ConN "RecordCons" [fromVList -> Just ns, vs]]
-        | Just i <- elemIndex s $ map fst ns -> tupsToList vs !! i
-    FunN "Vec" [a, b] -> TVec a b
-    FunN "swizzvector" [_, _, _, getVec -> Just (t, vs), getVec' t vs -> Just f] -> f
-    FunN "swizzscalar" [_, _, getVec -> Just (t, vs), getSwizz -> Just i] -> vs !! i
-
-    x -> x
-
-getVec (VV2 t x y) = Just (t, [x, y])
-getVec (VV3 t x y z) = Just (t, [x, y, z])
-getVec (VV4 t x y z w) = Just (t, [x, y, z, w])
-getVec _ = Nothing
-
-getVec' t vs (VV2 _ (getSwizz -> Just sx) (getSwizz -> Just sy)) = Just $ VV2 t (selSwizz sx vs) (selSwizz sy vs)
-getVec' t vs (VV3 _ (getSwizz -> Just sx) (getSwizz -> Just sy) (getSwizz -> Just sz)) = Just $ VV3 t (selSwizz sx vs) (selSwizz sy vs) (selSwizz sz vs)
-getVec' t vs (VV4 _ (getSwizz -> Just sx) (getSwizz -> Just sy) (getSwizz -> Just sz) (getSwizz -> Just sw)) = Just $ VV4 t (selSwizz sx vs) (selSwizz sy vs) (selSwizz sz vs) (selSwizz sw vs)
-getVec' _ _ _ = Nothing
-
-selSwizz i = (!! i)
-
-getSwizz = \case
-    ConN "Sx" [] -> Just 0
-    ConN "Sy" [] -> Just 1
-    ConN "Sz" [] -> Just 2
-    ConN "Sw" [] -> Just 3
-    _ -> Nothing
-
-toVList = foldr VCons VNil
-fromVList :: Exp -> Maybe [(String, Exp)]
-fromVList (VCons a b) = (a:) <$> fromVList b
-fromVList VNil = Just []
-fromVList x = Nothing
-
-tupsToList (Tuple2 _ _ x xs) = x: tupsToList xs
-tupsToList Tuple0 = []
-
-mkOrdering = \case
-    LT -> TCon "LT" 0 TOrdering []
-    EQ -> TCon "EQ" 1 TOrdering []
-    GT -> TCon "GT" 2 TOrdering []
-
-pattern TTuple0 = TTyCon "'Tuple0" TType []
-pattern NoTup <- (noTup -> True)
-
-noTup (TyConN s _) = take 6 s /= "'Tuple" -- todo
-noTup _ = False
-
-fromNatE :: Exp -> Maybe Int
-fromNatE Zero = Just 0
-fromNatE (Succ n) = (1 +) <$> fromNatE n
-
--- todo
-coe a b c d | a == b = d        -- todo
-coe a b c d = Coe a b c d
-
-reflCstr te = \case
-{-
-    Unit -> TT
-    TType -> TT  -- ?
-    Con n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs
-    TyCon n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs
-    x -> {-error $ "reflCstr: " ++ show x-} ReflCstr x
--}
-    x -> TT
-
-cstr = cstr__ []
-  where
-    cstr__ = cstr_
-
-    cstr_ [] a a' | a == a' = Unit
-    cstr_ ns TType TType = Unit
-    cstr_ ns (Con a []) (Con a' []) | a == a' = Unit
-    cstr_ ns (TyCon a []) (TyCon a' []) | a == a' = Unit
-    cstr_ ns (Var i) (Var i') | i == i', i < length ns = Unit
-    cstr_ (_: ns) (downE 0 -> Just a) (downE 0 -> Just a') = cstr__ ns a a'
-    cstr_ ((t, t'): ns) (UApp (downE 0 -> Just a) (UVar 0)) (UApp (downE 0 -> Just a') (UVar 0)) = traceInj2 (a, "V0") (a', "V0") $ cstr__ ns a a'
-    cstr_ ((t, t'): ns) a (UApp (downE 0 -> Just a') (UVar 0)) = traceInj (a', "V0") a $ cstr__ ns (Lam Visible t a) a'
-    cstr_ ((t, t'): ns) (UApp (downE 0 -> Just a) (UVar 0)) a' = traceInj (a, "V0") a' $ cstr__ ns a (Lam Visible t' a')
-    cstr_ ns (Lam h a b) (Lam h' a' b') | h == h' = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
-    cstr_ ns (UBind h a b) (UBind h' a' b') | h == h' = t2 (cstr__ ns a a') (cstr__ ((a, a'): ns) b b')
-    cstr_ ns (unApp -> Just (a, b)) (unApp -> Just (a', b')) = traceInj2 (a, show b) (a', show b') $ t2 (cstr__ ns a a') (cstr__ ns b b')
---    cstr_ ns (Label f xs _) (Label f' xs' _) | f == f' = foldr1 T2 $ zipWith (cstr__ ns) xs xs'
-    cstr_ ns (FunN "VecScalar" [a, b]) (TVec a' b') = t2 (cstr__ ns a a') (cstr__ ns b b')
-    cstr_ ns (FunN "VecScalar" [a, b]) (FunN "VecScalar" [a', b']) = t2 (cstr__ ns a a') (cstr__ ns b b')
-    cstr_ ns (FunN "VecScalar" [a, b]) t@(TTyCon0 n) | isElemTy n = t2 (cstr__ ns a (toNatE 1)) (cstr__ ns b t)
-    cstr_ ns t@(TTyCon0 n) (FunN "VecScalar" [a, b]) | isElemTy n = t2 (cstr__ ns a (toNatE 1)) (cstr__ ns b t)
-    cstr_ ns@[] (FunN "TFMat" [x, y]) (TyConN "'Mat" [i, j, a]) = t2 (cstr__ ns x (TVec i a)) (cstr__ ns y (TVec j a))
-    cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (FunN "JoinTupleType" [x'@NoTup, y']) = t2 (cstr__ ns x x') (cstr__ ns y y')
-    cstr_ ns@[] (TyConN "'Color" [x]) (FunN "ColorRepr" [x']) = cstr__ ns x x'
---    cstr_ ns (TyConN "'FrameBuffer" [a, b]) (FunN "TFFrameBuffer" [TyConN "'Image" [a', b']]) = T2 (cstr__ ns a a') (cstr__ ns b b')
-    cstr_ [] a@App{} a'@App{} = Cstr a a'
-    cstr_ [] a@CFun a'@CFun = Cstr a a'
-    cstr_ [] a@LCon a'@CFun = Cstr a a'
-    cstr_ [] a@LCon a'@App{} = Cstr a a'
-    cstr_ [] a@CFun a'@LCon = Cstr a a'
-    cstr_ [] a@App{} a'@LCon = Cstr a a'
-    cstr_ [] a a' | isVar a || isVar a' = Cstr a a'
-    cstr_ ns a a' = trace_ ("!----------------------------! type error:\n" ++ show ns ++ "\nfst:\n" ++ show a ++ "\nsnd:\n" ++ show a') Empty
-
-    unApp (UApp a b) = Just (a, b)         -- TODO: injectivity check
-    unApp (Con a xs@(_:_)) = Just (Con a (init xs), last xs)
-    unApp (TyCon a xs@(_:_)) = Just (TyCon a (init xs), last xs)
-    unApp _ = Nothing
-
-    isVar UVar{} = True
-    isVar (UApp a b) = isVar a
-    isVar _ = False
-
-    traceInj2 (a, a') (b, b') c | debug && (susp a || susp b) = trace_ ("  inj'?  " ++ show a ++ " : " ++ a' ++ "   ----   " ++ show b ++ " : " ++ b') c
-    traceInj2 _ _ c = c
-    traceInj (x, y) z a | debug && susp x = trace_ ("  inj?  " ++ show x ++ " : " ++ y ++ "    ----    " ++ show z) a
-    traceInj _ _ a = a
-
-    susp Con{} = False
-    susp TyCon{} = False
-    susp _ = True
-
-    isElemTy n = n `elem` ["Bool", "Float", "Int"]
-
-
-cstr' h x y e = EApp2 h (coe (up1E 0 x) (up1E 0 y) (Var 0) (up1E 0 e)) . EBind2 BMeta (cstr x y)
-
--------------------------------------------------------------------------------- simple typing
-
-litType = \case
-    LInt _    -> TInt
-    LFloat _  -> TFloat
-    LString _ -> TString
-    LChar _   -> TChar
-
-expType_ te = \case
-    Lam h t x -> Pi h t $ expType_ (EBind2 (BLam h) t te) x
-    App f x -> app (expType_ te{-todo: precise env-} f) x
-    Var i -> snd $ varType "C" i te
-    Pi{} -> TType
-    Label x _ -> expType_ te x
-    TFun _ t ts -> foldl app t ts
-    TCaseFun _ t _ ts -> foldl app t ts
-    TCon _ _ t ts -> foldl app t ts
-    TTyCon _ t ts -> foldl app t ts
-    TType -> TType
-    ELit l -> litType l
-    Meta{} -> error "meta type"
-    Assign{} -> error "let type"
-    LabelEnd x -> expType_ te x
-  where
-    app (Pi _ a b) x = substE "expType_" 0 x b
-    app t x = error $ "app: " ++ show t
-
--------------------------------------------------------------------------------- inference
-
-type TCM m = ExceptT String m
-
-runTCM = either error id . runExcept
-
--- todo: do only if NoTypeNamespace extension is not on
-lookupName s@('\'':s') m = maybe (Map.lookup s' m) Just $ Map.lookup s m
-lookupName s m = Map.lookup s m
-elemIndex' s@('\'':s') m = maybe (elemIndex s' m) Just $ elemIndex s m
-elemIndex' s m = elemIndex s m
-notElem' s@('\'':s') m = notElem s m && notElem s' m
-notElem' s m = notElem s m
-
-getDef te s = maybe (throwError $ "getDef: can't find: " ++ s) return (lookupName s $ extractEnv te)
-
-both f = f *** f
-
-inferN :: forall m . Monad m => TraceLevel -> Env -> SExp -> TCM m ExpType
-inferN tracelevel = infer  where
-
-    infer :: Env -> SExp -> TCM m ExpType
-    infer te exp = (if tracelevel >= 1 then trace_ ("infer: " ++ showEnvSExp te exp) else id) $ (if debug then fmap (recheck' "infer" te *** id) else id) $ case exp of
-        SLabelEnd x -> infer (ELabelEnd te) x
-        SVar i      -> focus te (Var i)
-        STyped et   -> focus_ te et
-        SGlobal s   -> focus_ te =<< getDef te s
-        SApp  h a b -> infer (EApp1 h te b) a
-        SLet a b    -> infer (ELet1 te b{-in-}) a{-let-} -- infer te (SLam Visible (Wildcard SType) b `SAppV` a)
-        SBind h a b -> infer ((if h /= BMeta then CheckType TType else id) $ EBind1 h te $ (if isPi h then TyType else id) b) a
-
-    checkN :: Env -> SExp -> Exp -> TCM m ExpType
-    checkN te x t = (if tracelevel >= 1 then trace_ $ "check: " ++ showEnvSExpType te x t else id) $ checkN_ te x t
-
-    checkN_ te e t
-        | SLabelEnd x <- e = checkN_ (ELabelEnd te) x t
-        | SApp h a b <- e = infer (CheckAppType h t te b) a
-        | SLam h a b <- e, Pi h' x y <- t, h == h'  = if checkSame te a x then checkN (EBind2 (BLam h) x te) b y else error "checkN"
-        | Pi Hidden a b <- t, notHiddenLam e = checkN (EBind2 (BLam Hidden) a te) (upS e) b
-        | otherwise = infer (CheckType t te) e
-      where
-        -- todo
-        notHiddenLam = \case
-            SLam Visible _ _ -> True
-            SGlobal s | Lam Hidden _ _ <- fst $ fromMaybe (error $ "infer: can't find: " ++ s) $ lookupName s $ extractEnv te -> False
-                            -- todo: use type instead of expr.
-                      | otherwise -> True
-            _ -> False
-
-    -- todo
-    checkSame te (Wildcard _) a = True
-    checkSame te (SBind BMeta SType (STyped (Var 0, _))) a = True
-    checkSame te a b = error $ "checkSame: " ++ show (a, b)
-
-    hArgs (Pi Hidden _ b) = 1 + hArgs b
-    hArgs _ = 0
-
-    focus env e = focus_ env (e, expType_ env e)
-
-    focus_ :: Env -> ExpType -> TCM m ExpType
-    focus_ env (e, et) = (if tracelevel >= 1 then trace_ $ "focus: " ++ showEnvExp env e else id) $ (if debug then fmap (recheck' "focus" env *** id) else id) $ case env of
-        ELabelEnd te -> focus_ te (LabelEnd e, et)
-        CheckSame x te -> focus_ (EBind2 BMeta (cstr x e) te) (up1E 0 e, up1E 0 et)
-        CheckAppType h t te b
-            | Pi h' x (downE 0 -> Just y) <- et, h == h' -> focus_ (EBind2 BMeta (cstr t y) $ EApp1 h te b) (up1E 0 e, up1E 0 et)
-            | otherwise -> focus_ (EApp1 h (CheckType t te) b) (e, et)
-        EApp1 h te b
-            | Pi h' x y <- et, h == h' -> checkN (EApp2 h e te) b x
-            | Pi Hidden x y  <- et, h == Visible -> focus_ (EApp1 Hidden env $ Wildcard $ Wildcard SType) (e, et)  --  e b --> e _ b
-            | otherwise -> infer (CheckType (Var 2) $ cstr' h (upE 0 2 et) (Pi Visible (Var 1) (Var 1)) (upE 0 2 e) $ EBind2 BMeta TType $ EBind2 BMeta TType te) (upS__ 0 3 b)
-        ELet1 te b{-in-} -> replaceMetas "let" Lam e >>= \e' -> infer (ELet2 (addType_ te e'{-let-}) te) b{-in-}
-        ELet2 (x{-let-}, xt) te -> focus_ te (substE "app2" 0 (x{-let-}) (  e{-in-}), et)
-        CheckType t te
-            | hArgs et > hArgs t
-                            -> focus_ (EApp1 Hidden (CheckType t te) $ Wildcard $ Wildcard SType) (e, et)
-            | otherwise     -> focus_ (EBind2 BMeta (cstr t et) te) (up1E 0 e, up1E 0 et)
-        EApp2 h a te        -> focus te $ app_ a e        --  h??
-        EBind1 h te b       -> infer (EBind2 h e te) b
-        EBind2 BMeta tt te
-            | Unit <- tt    -> refocus te $ both (substE_ te 0 TT) (e, et)
-            | Empty <- tt   -> throwError "halt" -- todo: better error msg
-            | T2 x y <- tt -> let
-                    te' = EBind2 BMeta (up1E 0 y) $ EBind2 BMeta x te
-                in focus_ te' $ both (substE_ te' 2 (t2C (Var 1) (Var 0)) . upE 0 2) (e, et)
-            | Cstr a b <- tt, a == b  -> refocus te $ both (substE "inferN2" 0 TT) (e, et)
-            | Cstr a b <- tt, Just r <- cst a b -> r
-            | Cstr a b <- tt, Just r <- cst b a -> r
-            | EBind2 h x te' <- te, h /= BMeta{-todo: remove-}, Just x' <- downE 0 tt, x == x'
-                            -> refocus (EBind2 h x te') $ both (substE "inferN3" 1 (Var 0)) (e, et)
-            | EBind2 h x te' <- te, h /= BMeta, Just b' <- downE 0 tt
-                            -> refocus (EBind2 h (up1E 0 x) $ EBind2 BMeta b' te') $ both (substE "inferN3" 2 (Var 0) . up1E 0) (e, et)
-            | ELet2 (x, xt) te' <- te, Just b' <- downE 0 tt
-                            -> refocus (ELet2 (up1E 0 x, up1E 0 xt) $ EBind2 BMeta b' te') $ both (substE "inferN32" 2 (Var 0) . up1E 0) (e, et)
-            | EBind1 h te' x  <- te -> refocus (EBind1 h (EBind2 BMeta tt te') $ upS__ 1 1 x) (e, et)
-            | ELet1 te' x     <- te, {-usedE 0 e, -} floatLetMeta $ expType_ env $ replaceMetas' Lam $ Bind BMeta tt e --not (tt == TType) {-todo: tweak?-}
-                                    -> refocus (ELet1 (EBind2 BMeta tt te') $ upS__ 1 1 x) (e, et)
-            | CheckAppType h t te' x <- te -> refocus (CheckAppType h (up1E 0 t) (EBind2 BMeta tt te') $ upS x) (e, et)
-            | EApp1 h te' x   <- te -> refocus (EApp1 h (EBind2 BMeta tt te') $ upS x) (e, et)
-            | EApp2 h x te'   <- te -> refocus (EApp2 h (up1E 0 x) $ EBind2 BMeta tt te') (e, et)
-            | CheckType t te' <- te -> refocus (CheckType (up1E 0 t) $ EBind2 BMeta tt te') (e, et)
-            | ELabelEnd te'   <- te -> refocus (ELabelEnd $ EBind2 BMeta tt te') (e, et)
-            | otherwise             -> focus_ te (Bind BMeta tt e, et {-???-})
-          where
-            cst x = \case
-                Var i | fst (varType "X" i te) == BMeta
-                      , Just y <- downE i x
-                      -> Just $ assign'' te i y $ both (substE_ te 0 ({-ReflCstr y-}TT) . substE_ te (i+1) (up1E 0 y)) (e, et)
-                _ -> Nothing
-        EBind2 (BLam h) a te -> focus_ te (Lam h a e, Pi h a e)
-        EBind2 (BPi h) a te -> focus_ te (Bind (BPi h) a e, TType)
-        EAssign i b te -> case te of
-            EBind2 h x te' | i > 0, Just b' <- downE 0 b
-                              -> refocus' (EBind2 h (substE "inferN5" (i-1) b' x) (EAssign (i-1) b' te')) (e, et)
-            ELet2 (x, xt) te' | i > 0, Just b' <- downE 0 b
-                              -> refocus' (ELet2 (substE "inferN51" (i-1) b' x, substE "inferN52" (i-1) b' xt) (EAssign (i-1) b' te')) (e, et)
-            ELet1 te' x       -> refocus' (ELet1 (EAssign i b te') $ substS (i+1) (up1E 0 b) x) (e, et)
-            EBind1 h te' x    -> refocus' (EBind1 h (EAssign i b te') $ substS (i+1) (up1E 0 b) x) (e, et)
-            CheckAppType h t te' x -> refocus' (CheckAppType h (substE "inferN6" i b t) (EAssign i b te') $ substS i b x) (e, et)
-            EApp1 h te' x     -> refocus' (EApp1 h (EAssign i b te') $ substS i b x) (e, et)
-            EApp2 h x te'     -> refocus' (EApp2 h (substE_ te'{-todo: precise env-} i b x) $ EAssign i b te') (e, et)
-            CheckType t te'   -> refocus' (CheckType (substE "inferN8" i b t) $ EAssign i b te') (e, et)
-            ELabelEnd te'     -> refocus' (ELabelEnd $ EAssign i b te') (e, et)
-            EAssign j a te' | i < j
-                              -> focus_ (EAssign (j-1) (substE "ea" i b a) $ EAssign i (upE (j-1) 1 b) te') (e, et)
-            te@EBind2{}       -> maybe (assign' te i b (e, et)) (flip refocus' (e, et)) $ pull i te
-            te@EAssign{}      -> maybe (assign' te i b (e, et)) (flip refocus' (e, et)) $ pull i te
-            -- todo: CheckSame Exp Env
-          where
-            pull i = \case
-                EBind2 BMeta _ te | i == 0 -> Just te
-                EBind2 h x te   -> EBind2 h <$> downE (i-1) x <*> pull (i-1) te
-                EAssign j b te  -> EAssign (if j <= i then j else j-1) <$> downE i b <*> pull (if j <= i then i+1 else i) te
-                _               -> Nothing
-        EGlobal{} -> return (e, et)
-        _ -> error $ "focus: " ++ show env
-      where
-        assign', assign'' :: Env -> Int -> Exp -> ExpType -> TCM m ExpType
-        assign'  te i x (e, t) = assign (\i x e -> focus te (Assign i x e)) (foc te) i x e
-        assign'' te i x (e, t) = assign (foc te) (foc te) i x e
-        foc te i x = focus $ EAssign i x te
-
-        refocus, refocus' :: Env -> ExpType -> TCM m ExpType
-        refocus = refocus_ focus_
-        refocus' = refocus_ refocus'
-
-        refocus_ f e (Bind BMeta x a, t) = f (EBind2 BMeta x e) (a, t)
-        refocus_ _ e (Assign i x a, t) = focus (EAssign i x e) a
-        refocus_ _ e (a, t) = focus e a
-
--------------------------------------------------------------------------------- debug support
-
-type Message = String
-
-recheck :: Message -> Env -> Exp -> Exp
-recheck msg e = if debug_light then recheck' msg e else id
-
-recheck' :: Message -> Env -> Exp -> Exp
-recheck' msg' e x = {-length (showExp e') `seq` -} e'
-  where
-    e' = recheck_ "main" (checkEnv e) x
-    checkEnv = \case
-        e@EGlobal{} -> e
-        EBind1 h e b -> EBind1 h (checkEnv e) b
-        EBind2 h t e -> EBind2 h (recheckEnv e t) $ checkEnv e            --  E [\(x :: t) -> e]    -> check  E [t]
-        ELet1 e b -> ELet1 (checkEnv e) b
-        ELet2 (x, t) e -> ELet2 (recheckEnv e x, recheckEnv e t{-?-}) $ checkEnv e
-        EApp1 h e b -> EApp1 h (checkEnv e) b
-        EApp2 h a e -> EApp2 h (recheckEnv {-(EApp1 h e _)-}e a) $ checkEnv e              --  E [a x]        ->  check  
-        EAssign i x e -> EAssign i (recheckEnv e $ up1E i x) $ checkEnv e                -- __ <i := x>
-        CheckType x e -> CheckType (recheckEnv e x) $ checkEnv e
-        CheckSame x e -> CheckSame (recheckEnv e x) $ checkEnv e
-        CheckAppType h x e y -> CheckAppType h (recheckEnv e x) (checkEnv e) y
-
-    recheckEnv = recheck_ "env"
-
-    recheck_ msg te = \case
-        Var k -> Var k
-        Lam h a b -> Lam h (ch True te{-ok?-} a) $ ch False (EBind2 (BLam h) a te) b
-        Bind h a b -> Bind h (ch (h /= BMeta) te{-ok?-} a) $ ch (isPi h) (EBind2 h a te) b
-        App a b -> appf (recheck'' "app1" te{-ok?-} a) (recheck'' "app2" (EApp2 Visible a te) b)
-        Label z x -> Label (recheck_ msg te z) x
-        ELit l -> ELit l
-        TType -> TType
-        Con s [] -> Con s []
-        Con s as -> reApp $ recheck_ "prim" te $ foldl App (Con s []) as
-        TyCon s [] -> TyCon s []
-        TyCon s as -> reApp $ recheck_ "prim" te $ foldl App (TyCon s []) as
-        CaseFun s [] -> CaseFun s []
-        CaseFun s as -> reApp $ recheck_ "fun" te $ foldl App (CaseFun s []) as
-        Fun s [] -> Fun s []
-        Fun s as -> reApp $ recheck_ "fun" te $ foldl App (Fun s []) as
-        LabelEnd x -> LabelEnd $ recheck_ msg te x
-      where
-        reApp (App f x) = case reApp f of
-            Fun s args -> Fun s $ args ++ [x]
-            CaseFun s args -> CaseFun s $ args ++ [x]
-            Con s args -> Con s $ args ++ [x]
-            TyCon s args -> TyCon s $ args ++ [x]
-        reApp x = x
-
-        -- todo: remove
-        appf' (a, Pi h x y) (b, x')
-            | x == x' = (b: a, substE "recheck" 0 b y)
-            | otherwise = error_ $ "recheck0 " ++ msg ++ "\nexpected: " ++ showEnvExp te x ++ "\nfound: " ++ showEnvExp te x' ++ "\nin term: " ++ showEnvExp te b
-
-        appf (a, Pi h x y) (b, x')
-            | x == x' = app_ a b
-            | otherwise = error_ $ "recheck " ++ msg' ++ "; " ++ msg ++ "\nexpected: " ++ showEnvExp te{-todo-} x ++ "\nfound: " ++ showEnvExp te{-todo-} x' ++ "\nin term: " ++ showEnvExp te (App a b)
-        appf (a, t) (b, x')
-            = error_ $ "recheck " ++ msg' ++ "; " ++ msg ++ "\nnot a pi type: " ++ showEnvExp te{-todo-} t ++ "\n\n" ++ showEnvExp e x
-
-        recheck'' msg te a = (b, expType_ te b) where b = recheck_ msg te a
-
-        ch False te e = recheck_ "ch" te e
-        ch True te e = case recheck'' "check" te e of
-            (e', TType) -> e'
-            _ -> error_ $ "recheck'':\n" ++ showEnvExp te e
-
--------------------------------------------------------------------------------- statements
-
-addParams ps t = foldr (uncurry SPi) t ps
-
-getParamsS (SPi h t x) = ((h, t):) *** id $ getParamsS x
-getParamsS x = ([], x)
-
-getApps (SApp h a b) = id *** (++ [(h, b)]) $ getApps a -- todo: make it efficient
-getApps x = (x, [])
-
-getApps' (App a b) = id *** (++ [b]) $ getApps' a -- todo: make it efficient
-getApps' x = (x, [])
-
-arity :: Exp -> Int
-arity = length . arity_
-arity_ = map fst . fst . getParams
-
-getParams :: Exp -> ([(Visibility, Exp)], Exp)
-getParams (Pi h a b) = ((h, a):) *** id $ getParams b
-getParams x = ([], x)
-
-apps a b = foldl SAppV (SGlobal a) b
-apps' a b = foldl sapp (SGlobal a) b
-
-replaceMetas err bind = \case
-    Meta a t -> bind Hidden a <$> replaceMetas err bind t
-    Assign i x t -> bind Hidden (cstr (Var i) $ upE i 1 x) . up1E 0 . upE i 1 <$> replaceMetas err bind t  -- todo: remove?
-    t -> checkMetas err t
-
-replaceMetas' bind = \case
-    Meta a t -> bind Hidden a $ replaceMetas' bind t
-    Assign i x t -> bind Hidden (cstr (Var i) $ upE i 1 x) . up1E 0 . upE i 1 $ replaceMetas' bind t
-    t ->  t
-
--- todo: remove
-checkMetas err = \case
-    x@Meta{} -> throwError $ "checkMetas " ++ err ++ ": " ++ show x
-    x@Assign{} -> throwError $ "checkMetas " ++ err ++ ": " ++ show x
-    Lam h a b -> Lam h <$> f a <*> f b
-    Bind (BLam _) _ _ -> error "impossible: chm"
-    Bind h a b -> Bind h <$> f a <*> f b
-    Label z v -> Label <$> f z <*> pure v
-    App a b  -> App <$> f a <*> f b
-    Fun s xs -> Fun s <$> mapM f xs
-    CaseFun s xs -> CaseFun s <$> mapM f xs
-    Con s xs -> Con s <$> mapM f xs
-    TyCon s xs -> TyCon s <$> mapM f xs
-    x@TType  -> pure x
-    x@ELit{} -> pure x
-    x@Var{}  -> pure x
-    LabelEnd x -> LabelEnd <$> f x
-  where
-    f = checkMetas err
-
-getGEnv f = gets (flip EGlobal mempty) >>= f
-inferTerm msg tr f t = getGEnv $ \env -> let env' = f env in smartTrace $ \tr -> 
-    fmap (\t -> if tr_light then length (showExp $ fst t) `seq` t else t) $ fmap (addType . recheck msg env') $ replaceMetas "lam" Lam . fst =<< lift (inferN (if tr then trace_level else 0) env' t)
-inferType tr t = getGEnv $ \env -> fmap (recheck "inferType" env) $ replaceMetas "pi" Pi . fst =<< lift (inferN (if tr then trace_level else 0) (CheckType TType env) t)
-
-smartTrace :: MonadError String m => (Bool -> m a) -> m a
-smartTrace f | trace_level >= 2 = f True
-smartTrace f | trace_level == 0 = f False
-smartTrace f = catchError (f False) $ \err ->
-    trace_ (unlines
-        [ "---------------------------------"
-        , err
-        , "try again with trace"
-        , "---------------------------------"
-        ]) $ f True
-
-addToEnv :: Monad m => String -> (Exp, Exp) -> ElabStmtM m ()
---addToEnv s (x, t) | Just msg <- ambiguityCheck s t = throwError msg
-addToEnv s (x, t) = do
-    maybe (pure ()) throwError_ $ ambiguityCheck s t
-    (if tr_light then trace_ (s ++ "  ::  " ++ showExp t) else id) $ modify $ Map.alter (Just . maybe (x, t) (const $ error $ "already defined: " ++ s)) s
-
--- Ambiguous: (Int ~ F a) => Int
--- Not ambiguous: (Show a, a ~ F b) => b
-ambiguityCheck :: String -> Exp -> Maybe String
-ambiguityCheck s ty = case ambigVars ty of
-    [] -> Nothing
-    err -> Just $ s ++ " has ambiguous type:\n" ++ showExp ty ++ "\nproblematic vars:\n" ++ show err
-
-ambigVars :: Exp -> [(Int, Exp)]
-ambigVars ty = [(n, c) | (n, c) <- hid, not $ any (`Set.member` defined) $ Set.insert n $ freeE c]
-  where
-    defined = dependentVars hid $ freeE ty'
-
-    i = length hid_
-    hid = zipWith (\k t -> (k, upE 0 (k+1) t)) (reverse [0..i-1]) hid_
-    (hid_, ty') = hiddenVars ty
-
-floatLetMeta :: Exp -> Bool
-floatLetMeta ty = (i-1) `Set.member` defined
-  where
-    defined = dependentVars hid $ Set.map (+i) $ freeE ty
-
-    i = length hid_
-    hid = zipWith (\k t -> (k, upE 0 (k+1) t)) (reverse [0..i-1]) hid_
-    (hid_, ty') = hiddenVars ty
-
-hiddenVars (Pi Hidden a b) = (a:) *** id $ hiddenVars b
-hiddenVars t = ([], t)
-
--- compute dependent type vars in constraints
--- Example:  dependentVars [(a, b) ~ F b c, d ~ F e] [c] == [a,b,c]
-dependentVars :: [(Int, Exp)] -> Set.Set Int -> Set.Set Int
-dependentVars ie s = cycle mempty s
-  where
-    freeVars = freeE
-
-    cycle acc s
-        | Set.null s = acc
-        | otherwise = cycle (acc <> s) (grow s Set.\\ acc)
-
-    grow = flip foldMap ie $ \case
-      (n, t) -> (Set.singleton n <-> freeVars t) <> case t of
-        Cstr ty f -> freeVars ty <-> freeVars f
-        CSplit a b c -> freeVars a <-> (freeVars b <> freeVars c)
---        CUnify{} -> mempty --error "dependentVars: impossible" 
-        _ -> mempty
---      (n, ISubst False x) -> (Set.singleton n <-> freeVars x)
-      where
-        a --> b = \s -> if Set.null $ a `Set.intersection` s then mempty else b
-        a <-> b = (a --> b) <> (b --> a)
-
-expType = expType_ (EGlobal initEnv [])
-addType x = (x, expType x)
-addType_ te x = (x, expType_ te x)
-
-downTo n m = map SVar [n+m-1, n+m-2..n]
-
-defined' = Map.keys
-
-addF = gets $ addForalls . defined'
-
-fixType = Pi Hidden TType $ Pi Visible (Pi Visible (Var 0) (Var 1)) (Var 1) -- forall a . (a -> a) -> a
-
-handleStmt :: MonadFix m => Stmt -> ElabStmtM m ()
-handleStmt = \case
-  PrecDef{} -> return ()
-    -- non-recursive let
-  Let n mf mt ar (downS 0 -> Just t_) -> {-trace ("begin: " ++ n) $ -} do
-        af <- addF
-        (x, t) <- inferTerm n tr id (maybe id (flip SAnn . af) mt t_)
-        let addLams [] _ e = Fun (FunName n mf t) $ reverse e
-            addLams (h: ar) (Pi h' d t) e | h == h' = Lam h d $ addLams ar t (Var 0: map (up1E 0) e)
-            addLams ar@(Visible: _) (Pi h@Hidden d t) e = Lam h d $ addLams ar t (Var 0: map (up1E 0) e)
-        addToEnv n (label (addLams ar t []) x, t)
-    -- recursive let
-  Let n mf mt ar t_ -> do
-    af <- addF
-    (x@(Lam Hidden _ e), _)
-        <- {-trace ("beg: " ++ n) $ -} inferTerm n tr (EBind2 BMeta fixType) (SAppV (SVar 0) $ SLam Visible (Wildcard SType) $ maybe id (flip SAnn . af) mt t_)
-    let
-        par i (Lam Hidden k z) = Lam Hidden k $ par (i+1) z
-        par i (Var i' `App` _ `App` f) | i == i' = x where
-            x = label (Fun (FunName n mf t) $ map Var $ reverse [0..i-1]) $ f `app_` x
-
-        x' =  x `app_` (Lam Hidden TType $ Lam Visible (Pi Visible (Var 0) (Var 1)) $ TFun "f_i_x" fixType [Var 1, Var 0])
-        t = expType x'
-    
-    {- trace_ (n ++ ": " ++ showExp t) $ -} 
-    addToEnv n (par 0 e, traceD ("addToEnv: " ++ n ++ " = " ++ showExp x') t)
-    -- primitive
-  Primitive con n t_ -> do
-        t <- inferType tr =<< ($ t_) <$> addF
-        addToEnv n $ flip (,) t $ case con of
-            Just True  -> TyCon (TyConName n Nothing (error "todo: inum3") t (error "todo: tcn cons 1") $ error "tycon case type") []
-            Just False -> Con (ConName n Nothing (-1) t) []
-            Nothing    -> {-Label (Fun (FunName n Nothing t) []) $ -} f t
-              where
-                f (Pi h a b) = Lam h a $ f b
-                f _ = TFun n t $ map Var $ reverse [0..arity t - 1]
-  Data s ps t_ cs -> do
-    af <- gets $ addForalls . (s:) . defined'
-    vty <- inferType tr $ addParams ps t_
-    let
-        pnum' = length $ filter ((== Visible) . fst) ps
-        inum = arity vty - length ps
-
-        mkConstr j (cn, af -> ct)
-            | c == SGlobal s && take pnum' xs == downTo (length . fst . getParamsS $ ct) pnum'
-            = do
-                cty <- removeHiddenUnit <$> inferType tr (addParams [(Hidden, x) | (Visible, x) <- ps] ct)
-                let     pars = zipWith (\x -> id *** STyped . flip (,) TType . upE x (1+j)) [0..] $ drop (length ps) $ fst $ getParams cty
-                        act = length . fst . getParams $ cty
-                        acts = map fst . fst . getParams $ cty
-                        conn = ConName cn Nothing j cty
-                addToEnv cn (Con conn [], cty)
-                return ( conn
-                       , addParams pars
-                       $ foldl SAppV (SVar $ j + length pars) $ drop pnum' xs ++ [apps' cn (zip acts $ downTo (j+1+length pars) (length ps) ++ downTo 0 (act- length ps))]
-                       )
-            | otherwise = throwError $ "illegal data definition (parameters are not uniform) " -- ++ show (c, cn, take pnum' xs, act)
-            where
-                                        (c, map snd -> xs) = getApps $ snd $ getParamsS ct
-
-        motive = addParams (replicate inum (Visible, Wildcard SType)) $
-           SPi Visible (apps' s $ zip (map fst ps) (downTo inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downTo 0 inum)) SType
-
-        addToEnv'' s t cs ct = addToEnv s (TyCon (TyConName s Nothing inum t cs ct) [], t)
-        addToEnv''' _ s t i = addToEnv s (f t, t)
-          where
-            f (Pi h a b) = Lam h a $ f b
-            f _ = TCaseFun s t i $ map Var $ reverse [0..arity t - 1]
-    mdo
-        addToEnv'' s vty (map fst cons) ct
-        cons <- zipWithM mkConstr [0..] cs
-        ct <- inferType tr
-            ( (\x -> traceD ("type of case-elim before elaboration: " ++ showSExp x) x) $ addParams
-                ( [(Hidden, x) | (_, x) <- ps]
-                ++ (Visible, motive)
-                : map ((,) Visible . snd) cons
-                ++ replicate inum (Hidden, Wildcard SType)
-                ++ [(Visible, apps' s $ zip (map fst ps) (downTo (inum + length cs + 1) $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downTo 0 inum))]
-                )
-            $ foldl SAppV (SVar $ length cs + inum + 1) $ downTo 1 inum ++ [SVar 0]
-            )
-        addToEnv''' False (caseName s) ct (length ps)
-
-removeHiddenUnit (Pi Hidden Unit (downE 0 -> Just t)) = removeHiddenUnit t
-removeHiddenUnit (Pi h a b) = Pi h a $ removeHiddenUnit b
-removeHiddenUnit t = t
-
--------------------------------------------------------------------------------- parser
-
-addForalls :: [SName] -> SExp -> SExp
-addForalls defined x = foldl f x [v | v <- reverse $ freeS x, v `notElem'` defined]
-  where
-    f e v = SPi Hidden (Wildcard SType) $ substSG v (SVar 0) $ upS e
-
-defined defs = ("Type":) $ flip foldMap defs $ \case
-    TypeAnn x _ -> [x]
-    Let x _ _ _ _ -> [x]
-    Data x _ _ cs -> x: map fst cs
-    Primitive _ x _ -> [x]
-
-type InnerP = Reader GlobalEnv'
-
-type P = ParsecT (IndentStream (CharIndentStream String)) SourcePos InnerP
-
-lexer :: Pa.GenTokenParser (IndentStream (CharIndentStream String)) SourcePos InnerP
-lexer = makeTokenParser $ makeIndentLanguageDef style
-  where
-    style = Pa.LanguageDef
-        { Pa.commentStart   = "{-"
-        , Pa.commentEnd     = "-}"
-        , Pa.commentLine    = "--"
-        , Pa.nestedComments = True
-        , Pa.identStart     = letter <|> oneOf "_"
-        , Pa.identLetter    = alphaNum <|> oneOf "_'"
-        , Pa.opStart        = Pa.opLetter style
-        , Pa.opLetter       = oneOf ":!#$%&*+./<=>?@\\^|-~"
-        , Pa.reservedOpNames= ["->", "=>", "~", "\\", "|", "::", "<-", "=", "@", ".."]
-        , Pa.reservedNames  = ["forall", "data", "builtins", "builtincons", "builtintycons", "_", "case", "of", "where", "import", "module", "let", "in", "infix", "infixr", "infixl", "if", "then", "else", "class", "instance"]
-        , Pa.caseSensitive  = True
-        }
-
-position :: P SourcePos
-position = getPosition
-
-positionBeforeSpace :: P SourcePos
-positionBeforeSpace = getState
-
-optional :: P a -> P (Maybe a)
-optional = optionMaybe
-
-keyword :: String -> P ()
-keyword = Pa.reserved lexer
-
-operator :: String -> P ()
-operator = Pa.reservedOp lexer
-
-tick (Just True, _) ('\'':n) = n
-tick (Just True, _) n | n `elem` ["Type", "Nat", "Float", "Int", "Bool", "IO", "Unit", "Empty", "T2"] = n
-                      | otherwise = '\'': n
-tick _ n = n
-
-lcIdents ns = tick ns <$> ((++) <$> (option [] $ ("'" <$ char '\'')) <*> Pa.identifier lexer)
-
-lcOps = Pa.operator lexer
-
-ident = id
-parens    = Pa.parens lexer
-braces    = Pa.braces lexer
-brackets  = Pa.brackets lexer
-commaSep  = Pa.commaSep lexer
-commaSep1 = Pa.commaSep1 lexer
-dot       = Pa.dot lexer
-comma     = Pa.comma lexer
-colon     = Pa.colon lexer
-natural   = Pa.natural lexer
-integer   = Pa.integer lexer
-float     = Pa.float lexer
-charLiteral   = Pa.charLiteral lexer
-stringLiteral = Pa.stringLiteral lexer
-whiteSpace    = Pa.whiteSpace lexer
-
-data Extension
-    = NoImplicitPrelude
-    | NoTypeNamespace
-    | NoConstructorNamespace
-    deriving (Eq, Ord, Show)
-
-type Name = String
-type DefinitionR = Stmt
-
-data Export = ExportModule Name | ExportId Name
-
-data ModuleR
-  = Module
-  { extensions    :: [Extension]
-  , moduleImports :: [Name]    -- TODO
-  , moduleExports :: Maybe [Export]
-  , definitions   :: GlobalEnv' -> Either String [DefinitionR]
-  }
-
-(<&>) = flip (<$>)
-
--------------------------------------------------------------------------------- parser combinators
-
--- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602
-try' s m = try m <?> s
-{-
-qualified_ id = do
-    q <- try' "qualification" $ upperCase' <* dot
-    (N t qs n i) <- qualified_ id
-    return $ N t (q:qs) n i
-  <|>
-    id
-  where
-    upperCase' = (:) <$> satisfy isUpper <*> many (satisfy isAlphaNum)
--}
--------------------------------------------------------------------------------- identifiers
-
-check msg p m = try' msg $ do
-    x <- m
-    if p x then return x else fail $ msg ++ " expected"
-
---upperCase, lowerCase, symbols, colonSymbols :: P String
-upperCase (Nothing, _) = mzero -- todo
-upperCase ns = (if snd ns then check "uppercase ident" (isUpper . head) else id) $ ident $ lcIdents ns
-lowerCase ns = (if snd ns then check "lowercase ident" (isLower . head) else id) (ident $ lcIdents ns) <|> try (('_':) <$ char '_' <*> ident (lcIdents ns))
-symbols   = check "symbols" ((/=':') . head) $ ident lcOps
-colonSymbols = "Cons" <$ operator ":" <|> check "symbols" ((==':') . head) (ident lcOps)
-
---------------------------------------------------------------------------------
-
-pattern ExpN' :: String -> P.Doc -> String
-pattern ExpN' s p <- ((,) undefined -> (p, s)) where ExpN' s p = s
-pattern ExpN s = s
-
---typeConstructor, upperCaseIdent, typeVar, var, varId, qIdent, operator', conOperator, moduleName :: P Name
---typeConstructor = upperCase <&> \i -> TypeN' i (Pa.text i)
-upperCaseIdent ns = upperCase ns <&> ExpN
---typeVar         = (\p i -> TypeN' i $ P.text $ i ++ show p) <$> position <*> lowerCase
-var ns          = (\p i -> ExpN' i $ P.text $ i ++ show p) <$> position <*> lowerCase ns
-qIdent ns       = {-qualified_ todo-} (var ns <|> upperCaseIdent ns)
-conOperator     = (\p i -> ExpN' i $ P.text $ i ++ show p) <$> position <*> colonSymbols
-varId ns        = var ns <|> parens operator'
-backquotedIdent = try' "backquoted" $ char '`' *> (ExpN <$> ((:) <$> satisfy isAlpha <*> many (satisfy isAlphaNum))) <* char '`' <* whiteSpace
-operator'       = (\p i -> ExpN' i $ P.text $ i ++ show p) <$> position <*> symbols
-              <|> conOperator
-              <|> backquotedIdent
-moduleName      = {-qualified_ todo-} upperCaseIdent (Just False, False)
-
--------------------------------------------------------------------------------- fixity declarations
-
-fixityDef :: P [DefinitionR]
-fixityDef = do
-  dir <-    Nothing      <$ keyword "infix" 
-        <|> Just FDLeft  <$ keyword "infixl"
-        <|> Just FDRight <$ keyword "infixr"
-  localIndentation Gt $ do
-    i <- natural
-    ns <- commaSep1 operator'
-    return [PrecDef n (dir, fromIntegral i) | n <- ns]
-
---------------------------------------------------------------------------------
-
-export :: Namespace -> P Export
-export ns =
-        ExportModule <$ keyword "module" <*> moduleName
-    <|> ExportId <$> varId ns
-
-parseExtensions :: P [Extension]
-parseExtensions = do
-    try (string "{-#")
-    simpleSpace
-    string "LANGUAGE"
-    simpleSpace
-    s <- commaSep ext
-    simpleSpace
-    string "#-}"
-    simpleSpace
-    return s
-  where
-    simpleSpace = skipMany (satisfy isSpace)
-
-    ext = do
-        s <- some $ satisfy isAlphaNum
-        case s of
-            "NoImplicitPrelude" -> return NoImplicitPrelude
-            "NoTypeNamespace"   -> return NoTypeNamespace
-            "NoConstructorNamespace" -> return NoConstructorNamespace
-            _ -> fail $ "language extension expected instead of " ++ s
-
-importlist ns = parens (commaSep (varId ns <|> upperCaseIdent ns))
-
-parse :: SourceName -> String -> Either String ModuleR
-parse f str = x
-  where
-    x = (show +++ id) . flip runReader (error "globalenv used") . runParserT p (newPos "" 0 0) f . mkIndentStream 0 infIndentation True Ge . mkCharIndentStream $ str
-
-    p = do
-        getPosition >>= setState
-        setPosition =<< flip setSourceName f <$> getPosition
-        exts <- concat <$> many parseExtensions
-        let ns = (if NoTypeNamespace `elem` exts then Nothing else Just False, not $ NoConstructorNamespace `elem` exts)
-        whiteSpace
-        header <- optional $ do
-            modn <- keyword "module" *> moduleName
-            exps <- optional (parens $ commaSep $ export ns)
-            keyword "where"
-            return (modn, exps)
-        idefs <- many $ keyword "import" *> moduleName
-                     <* optional (keyword "hiding" *> importlist ns <|> importlist ns)
-                     <* optional (keyword "as" *> moduleName)
-
-        st <- getParserState
-
-        let defs ge = (show +++ id) . flip runReader ge . runParserT p (newPos "" 0 0) f . mkIndentStream 0 infIndentation True Ge . mkCharIndentStream $ ""
-              where
-                p = do
-                    setParserState st
-                    parseStmts SLabelEnd ns [] <* eof
-        return $ Module
-          { extensions = exts
-          , moduleImports = if NoImplicitPrelude `elem` exts
-                then idefs
-                else ExpN "Prelude": idefs
-          , moduleExports = join $ snd <$> header
-          , definitions   = defs
-          }
-
-parseType ns mb vs = maybe id option mb $ operator "::" *> parseTTerm ns PrecLam vs
-patVar ns = lcIdents ns <|> "" <$ keyword "_"
-patVar2 ns = lowerCase ns <|> "" <$ keyword "_"
-typedId ns mb vs = (,) <$> patVar ns <*> localIndentation Gt {-TODO-} (parseType ns mb vs)
-typedId' ns mb vs = (,) <$> commaSep1 (varId ns <|> patVar ns) <*> localIndentation Gt {-TODO-} (parseType ns mb vs)
-
-telescope ns mb vs = option (vs, []) $ do
-    (x, vt) <-
-            operator "@" *> (maybe empty (\x -> flip (,) (Hidden, x) <$> patVar ns) mb <|> parens (f Hidden))
-        <|> try (parens $ f Visible)
-        <|> maybe ((,) "" . (,) Visible <$> parseTerm ns PrecAtom vs) (\x -> flip (,) (Visible, x) <$> patVar ns) mb
-    (id *** (vt:)) <$> telescope ns mb (x: vs)
-  where
-    f v = (id *** (,) v) <$> typedId ns mb vs
-
-parseClause ns e = do
-    (fe, p) <- pattern' ns e
-    localIndentation Gt $ do
-        x <- operator "->" *> parseETerm ns PrecLam fe
-        f <- parseWhereBlock ns fe
-        return (p, f x)
-
-patternAtom ns vs =
-     (,) vs . flip ViewPat eqPP . SAppV (SGlobal "primCompareFloat") . sLit . LFloat <$> try float
- <|> (,) vs . flip ViewPat eqPP . SAppV (SGlobal "primCompareInt") . sLit . LInt . fromIntegral <$> natural
- <|> (,) <$> ((:vs) <$> patVar2 ns) <*> (pure PVar)
- <|> (,) vs . flip PCon [] <$> upperCaseIdent ns
- <|> (id *** mkListPat) <$> brackets (patlist ns vs <|> pure (vs, []))
- <|> (id *** mkTupPat) <$> parens (patlist ns vs)
-
-eqPP = ParPat [PCon "EQ" []]
-truePP = ParPat [PCon "True" []]
-
-patlist ns vs = commaSep1' (\vs -> (\(vs, p) t -> (vs, patType p t)) <$> pattern' ns vs <*> parseType ns (Just $ Wildcard SType) vs) vs
-
-mkListPat (p: ps) = PCon "Cons" $ map (ParPat . (:[])) [p, mkListPat ps]
-mkListPat [] = PCon "Nil" []
-
-pattern' ns vs =
-     {-((,) vs . PLit . LFloat) <$> try float
- <|> -}pCon <$> upperCaseIdent ns <*> patterns ns vs
- <|> (patternAtom ns vs >>= \(vs, p) -> option (vs, p) ((id *** (\p' -> PCon "Cons" (ParPat . (:[]) <$> [p, p']))) <$ operator ":" <*> pattern' ns vs))
-
-patterns ns vs =
-     do patternAtom ns vs >>= \(vs, p) -> patterns ns vs >>= \(vs, ps) -> pure (vs, ParPat [p]: ps)
- <|> pure (vs, [])
-
-pCon i (vs, x) = (vs, PCon i x)
-
-patType p (Wildcard SType) = p
-patType p t = PatType (ParPat [p]) t
-
-mkTupPat :: [Pat] -> Pat
-mkTupPat [x] = x
-mkTupPat ps = PCon ("Tuple" ++ show (length ps)) (ParPat . (:[]) <$> ps)
-
-commaSep1' :: (t -> P (t, a)) -> t -> P (t, [a])
-commaSep1' p vs =
-     p vs >>= \(vs, x) -> (\(vs, xs) -> (vs, x: xs)) <$ comma <*> commaSep1' p vs
-                      <|> pure (vs, [x])
-
-commaSep' :: (t -> P (t, a)) -> t -> P (t, [a])
-commaSep' p vs =
-      commaSep1' p vs
-  <|> pure (vs, [])
-
-telescope' ns vs = option (vs, []) $ do
-    (vs', vt) <-
-            operator "@" *> (f Hidden <$> patternAtom ns vs)
-        <|> f Visible <$> patternAtom ns vs
-    (id *** (vt:)) <$> telescope' ns vs'
-  where
-    f h (vs, PatType (ParPat [p]) t) = (vs, ((h, t), p))
-    f h (vs, p) = (vs, ((h, Wildcard SType), p))
-
-parseStmts lend ns e = (asks $ \ge -> pairTypeAnns ge . concat) <*> some (parseStmt ns e)
-  where
-    pairTypeAnns ge ds = concatMap f $ groupBy h ds where
-        h (FunAlt n _ _ _) (FunAlt m _ _ _) = m == n
-        h _ _ = False
-
-        f [TypeAnn{}] = []
-        f [p@PrecDef{}] = [p]
-
-        f fs@((FunAlt n vs _ _): _) = [Let n (listToMaybe [t | PrecDef n' t <- ds, n' == n])
-                                   (listToMaybe [t | TypeAnn n' t <- ds, n' == n])
-                                   (map (fst . fst) vs)
-                                   (foldr (uncurry SLam) (compileGuardTree lend ge $ Alts
-                                        [ compilePatts (zip (map snd vs) $ reverse [0..length vs - 1]) gs x
-                                        | FunAlt _ vs gs x <- fs
-                                        ]) (map fst vs))
-                            ]
-        f x = x
-
-parseStmt :: Namespace -> [String] -> P [Stmt]
-parseStmt ns e =
-     do con <- Nothing <$ keyword "builtins" <|> Just False <$ keyword "builtincons" <|> Just True <$ keyword "builtintycons"
-        fmap concat $ localIndentation Gt $ localAbsoluteIndentation $ many $ do
-            (\(vs, t) -> Primitive con <$> vs <*> pure t) <$> typedId' ns Nothing []
- <|> do keyword "data"
-        localIndentation Gt $ do
-            x <- lcIdents (typeNS ns)
-            (nps, ts) <- telescope (typeNS ns) (Just SType) e
-            t <- parseType (typeNS ns) (Just SType) nps
-            let mkConTy mk (nps', ts') =
-                    ( if mk then Just $ take (length nps' - length nps) nps' else Nothing
-                    , foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ downTo (length ts') $ length ts) ts')
-            cs <-
-                 do keyword "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ (id *** (,) Nothing) <$> typedId' ns Nothing nps)
-             <|> do operator "=" *>
-                      sepBy1 ((,) <$> (pure <$> lcIdents ns)
-                                  <*> (    braces (mkConTy True <$> (telescopeDataFields (typeNS ns) nps))
-                                       <|> (mkConTy False <$> telescope (typeNS ns) Nothing nps)) )
-                                      (operator "|")
-             <|> pure []
-            ge <- ask
-            return $ mkData ge x ts t $ concatMap (\(vs, t) -> (,) <$> vs <*> pure t) cs
- <|> do (vs, t) <- try $ typedId' ns Nothing []
-        return $ TypeAnn <$> vs <*> pure t
- <|> fixityDef
- <|> do (n, (fe, ts)) <-
-            do try' "operator definition" $ do
-                (e', a1) <- patternAtom ns ("": e)
-                localIndentation Gt $ do
-                    n <- operator'
-                    (e'', a2) <- patternAtom ns $ take (length e' - length e - 1) e' ++ n: e
-                    lookAhead $ operator "=" <|> operator "|"
-                    return (n, (e'', (,) (Visible, Wildcard SType) <$> [a1, a2]))
-          <|> do try $ do
-                    n <- varId ns
-                    localIndentation Gt $ (,) n <$> telescope' (expNS ns) (n: e) <* (lookAhead $ operator "=" <|> operator "|")
-        localIndentation Gt $ do
-            gu <- option Nothing $ do
-                operator "|"
-                Just <$> parseETerm ns PrecOp fe
-            operator "="
-            rhs <- parseETerm ns PrecLam fe
-            f <- parseWhereBlock ns fe
-            return $ pure $ FunAlt n ts gu $ f rhs
- <|> pure . uncurry ValueDef <$> valueDef ns e
- where
-   telescopeDataFields ns vs = option (vs, []) $ do
-       (x, vt) <- do name <- var (expNS ns)
-                     operator "::"
-                     term <- parseTerm ns PrecLam vs
-                     return (name, (Visible, term))
-       (id *** (vt:)) <$> (comma *> telescopeDataFields ns (x: vs) <|> pure (vs, []))
-
-mkData ge x ts t cs = [Data x ts t $ (id *** snd) <$> cs] ++ concatMap mkProj cs
-  where
-    mkProj (cn, (Just fs, _)) = [ Let fn Nothing Nothing [Visible]
-                                $ upS $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar]) $ SVar i
-                                | (i, fn) <- zip [0..] fs]
-    mkProj _ = []
---  data F = X {a :: A, b :: B}
---  a (X w _) = w
---  b (X _ w) = w
-
-parseWhereBlock ns fe = option id $ do
-    keyword "where"
-    dcls <- localIndentation Ge (localAbsoluteIndentation $ parseStmts id ns fe)
-    ge <- ask
-    return $ mkLets ge dcls
-
-type DBNames = [SName]  -- De Bruijn variable names
-
-valueDef :: Namespace -> DBNames -> P ((DBNames, Pat), SExp)
-valueDef ns e = do
-    (e', p) <- try $ pattern' ns e <* operator "="
-    localIndentation Gt $ do
-        ex <- parseETerm ns PrecLam e
-        return ((take (length e' - length e) e', p), ex)
-
-pattern TPVar t = ParPat [PatType (ParPat [PVar]) t]
-
-sapp a (v, b) = SApp v a b
-
-type Namespace = (Maybe Bool {-True: type namespace-}, Bool)
-
-parseTTerm ns = parseTerm $ typeNS ns
-parseETerm ns = parseTerm $ expNS ns
-
-typeNS = (True <$) *** id
-expNS = (False <$) *** id
-
-parseTerm :: Namespace -> Prec -> [String] -> P SExp
-parseTerm ns PrecLam e =
-     mkIf <$ keyword "if" <*> parseTerm ns PrecLam e <* keyword "then" <*> parseTerm ns PrecLam e <* keyword "else" <*> parseTerm ns PrecLam e
- <|> do (tok, ns) <- (SPi . const Hidden <$ operator "." <|> SPi . const Visible <$ operator "->", typeNS ns) <$ keyword "forall"
-        (fe, ts) <- telescope ns (Just $ Wildcard SType) e
-        f <- tok
-        t' <- parseTerm ns PrecLam fe
-        return $ foldr (uncurry f) t' ts
- <|> do (tok, ns) <- (asks (patLam_ id) <* operator "->", expNS ns) <$ operator "\\"
-        (fe, ts) <- telescope' ns e
-        f <- tok
-        t' <- parseTerm ns PrecLam fe
-        return $ foldr (uncurry f) t' ts
- <|> do (asks compileCase) <* keyword "case" <*> parseETerm ns PrecLam e
-                                 <* keyword "of" <*> localIndentation Ge (localAbsoluteIndentation $ some $ parseClause ns e)
- <|> do (asks $ \ge -> compileGuardTree id ge . Alts) <*> parseSomeGuards ns (const True) e
- <|> do t <- parseTerm ns PrecEq e
-        option t $ mkPi <$> (Visible <$ operator "->" <|> Hidden <$ operator "=>") <*> pure t <*> parseTTerm ns PrecLam e
-parseTerm ns PrecEq e = parseTerm ns PrecAnn e >>= \t -> option t $ SCstr t <$ operator "~" <*> parseTTerm ns PrecAnn e
-parseTerm ns PrecAnn e = parseTerm ns PrecOp e >>= \t -> option t $ SAnn t <$> parseType ns Nothing e
-parseTerm ns PrecOp e = (asks $ \dcls -> calculatePrecs dcls e) <*> p' where
-    p' = (\(t, xs) -> (mkNat ns 0, ("-!", t): xs)) <$ operator "-" <*> p_
-     <|> p_
-    p_ = (,) <$> parseTerm ns PrecApp e <*> (option [] $ operator' >>= p)
-    p op = do (exp, op') <- try ((,) <$> parseTerm ns PrecApp e <*> operator')
-              ((op, exp):) <$> p op'
-       <|> pure . (,) op <$> parseTerm ns PrecLam e
-parseTerm ns PrecApp e = 
-    try {- TODO: adjust try for better error messages e.g. don't use braces -}
-      (foldl sapp <$> (sVar e <$> upperCaseIdent ns) <*> braces (commaSep $ lcIdents ns *> operator "=" *> ((,) Visible <$> parseTerm ns PrecLam e))) <|>
-    (foldl sapp <$> parseTerm ns PrecSwiz e <*> many
-            (   (,) Visible <$> parseTerm ns PrecSwiz e
-            <|> (,) Hidden <$ operator "@" <*> parseTTerm ns PrecSwiz e))
-parseTerm ns PrecSwiz e = do
-    t <- parseTerm ns PrecProj e
-    try (mkSwizzling t <$ char '%' <*> manyNM 1 4 (satisfy (`elem` ("xyzwrgba" :: [Char]))) <* whiteSpace) <|> pure t
-parseTerm ns PrecProj e = do
-    t <- parseTerm ns PrecAtom e
-    try (mkProjection t <$ char '.' <*> (sepBy1 (sLit . LString <$> lcIdents ns) (char '.'))) <|> pure t
-parseTerm ns PrecAtom e =
-     sLit . LChar    <$> try charLiteral
- <|> sLit . LString  <$> stringLiteral
- <|> sLit . LFloat   <$> try float
- <|> sLit . LInt . fromIntegral <$ char '#' <*> natural
- <|> mkNat ns <$> natural
- <|> Wildcard (Wildcard SType) <$ keyword "_"
- <|> sVar e <$> (lcIdents ns <|> try (varId ns))
- <|> mkDotDot <$> try (operator "[" *> parseTerm ns PrecLam e <* operator ".." ) <*> parseTerm ns PrecLam e <* operator "]"
- <|> listCompr ns e
- <|> mkList ns <$> brackets (commaSep $ parseTerm ns PrecLam e)
- <|> mkTuple ns <$> parens (commaSep $ parseTerm ns PrecLam e)
- <|> mkRecord <$> braces (commaSep $ ((,) <$> lowerCase ns <* colon <*> parseTerm ns PrecLam e))
- <|> do keyword "let"
-        dcls <- localIndentation Ge (localAbsoluteIndentation $ parseStmts id ns e)
-        ge <- ask
-        mkLets ge dcls <$ keyword "in" <*> parseTerm ns PrecLam e
-
-mkSwizzling term = swizzcall
-  where
-    sc c = SGlobal $ 'S':c:[]
-    swizzcall [x] = SGlobal "swizzscalar" `SAppV` term `SAppV` (sc . synonym) x
-    swizzcall xs  = SGlobal "swizzvector" `SAppV` term `SAppV` swizzparam xs
-    swizzparam xs  = foldl (\exp s -> exp `SAppV` s) (vec xs) $ map (sc . synonym) xs
-    vec xs = SGlobal $ case length xs of
-        0 -> error "impossible: swizzling parsing returned empty pattern"
-        1 -> error "impossible: swizzling went to vector for one scalar"
-        n -> "V" ++ show n
-    synonym 'r' = 'x'
-    synonym 'g' = 'y'
-    synonym 'b' = 'z'
-    synonym 'a' = 'w'
-    synonym c   = c
-
-mkProjection term = foldl (\exp field -> SGlobal "project" `SAppV` field `SAppV` exp) term
-
--- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, (2.0, (3.0, ())))
-mkRecord xs = SGlobal "RecordCons" `SAppH` names `SAppV` values
-  where
-    (names, values) = mkNames *** mkValues $ unzip xs
-
-    mkNameTuple v = SGlobal "Tuple2" `SAppV` (sLit $ LString v) `SAppV` Wildcard SType
-    mkNames = foldr (\n ns -> SGlobal "Cons" `SAppV` (mkNameTuple n) `SAppV` ns)
-                    (SGlobal "Nil")
-
-    mkValues = foldr (\x xs -> SGlobal "Tuple2" `SAppV` x `SAppV` xs)
-                     (SGlobal "Tuple0")
-
-sVar e x = maybe (SGlobal x) SVar $ elemIndex' x e
-
-mkIf b t f = SGlobal "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f
-
-mkDotDot e f = SGlobal "fromTo" `SAppV` e `SAppV` f
-
--- n, m >= 1, n < m
-manyNM n m p = do
-  xs <- many1 p
-  let lxs = length xs
-  unless (n <= lxs && lxs <= m) . fail $ unwords ["manyNM", show n, show m, "found", show lxs, "occurences."]
-  return xs
-
--------------------------------------------------------------------------------- list comprehensions
-{- example
-
-  dbs<<[ x | y <- [1..10], let x = y * y]>>
--->
-  dbs<<[ _ | y <- [1..10], let x = y * y]>>  $  dbs<<x>>
--->
-  (\exp -> SGlobal "concatMap" `SAppV` 
-     SLam
-            | PVar <- Var 0 = y:dbs<<[ _ | let x = y * y]>>  $  exp
-            | _ = <<[]>>
-     <<[1..10]>>
-  ) (SGlobal "x")
--->
-  (\exp -> SGlobal "concatMap" `SAppV` 
-     SLam
-            | PVar <- Var 0 = SLet (y:dbs<<y * y>>) ((x:y:dbs<<[ _ ]>>) $ exp)
-            | _ = <<[]>>
-     <<[1..10]>>
-  ) (SGlobal "x")
--->
-  (\exp -> SGlobal "concatMap" `SAppV` 
-     SLam
-            | PVar <- Var 0 = SLet (y:dbs<<y * y>>) ((x:y:dbs<<[ _ ]>>) $ exp)
-            | _ = <<[]>>
-     <<[1..10]>>
-  ) (SGlobal "x")
--->
-  SGlobal "concatMap" `SAppV` 
-     SLam
-            | PVar <- Var 0 = SLet (Var 0 * Var 0) (Var 0)
-            | _ = <<[]>>
-     <<[1..10]>>
--->
--}
-
-generator, letdecl, boolExpression :: Namespace -> DBNames -> P (DBNames, SExp -> SExp)
-
-generator ns dbs = do
-    (dbs', pat) <- try $ pattern' ns dbs <* operator "<-"
-    exp <- parseTerm ns PrecLam dbs
-    ge <- ask
-    return $ (,) ({-join traceShow-} dbs') $ \e -> application
-        [ SGlobal "concatMap"
-        , SLam Visible (Wildcard SType) $ compileGuardTree id ge $ Alts
-            [ compilePatts [(pat, 0)] Nothing $ {-upS $ -} e
-            , GuardLeaf $ SGlobal "Nil"
-            ]
-        , exp
-        ]
-
-letdecl ns dbs = ask >>= \ge -> keyword "let" *> ((\((dbs', p), e) -> ({-join traceShow dbs' ++ -} dbs, \exp -> {-traceShow exp $ -} mkLets ge [ValueDef (dbs', p) e] exp)) <$> valueDef ns dbs)
-
-boolExpression ns dbs = do
-    pred <- parseTerm ns PrecLam dbs
-    return (dbs, \e -> application [SGlobal "primIfThenElse", pred, e, SGlobal "Nil"])
-
-application = foldl1 SAppV
-
-listCompr :: Namespace -> DBNames -> P SExp
-listCompr ns dbs = (\e (dbs', fs) -> foldr ($) (deBruinify (take (length dbs' - length dbs) dbs') e) fs)
- <$> try' "List comprehension" ((SGlobal "singleton" `SAppV`) <$ operator "[" <*> parseTerm ns PrecLam dbs <* operator "|")
- <*> commaSep' (liftA2 (<|>) (generator ns) $ liftA2 (<|>) (letdecl ns) (boolExpression ns)) dbs <* operator "]"
-
-deBruinify :: DBNames -> SExp -> SExp
-deBruinify [] e = e
-deBruinify (n: ns) e = substSG n (SVar 0) $ upS $ deBruinify ns e
-
--- deBruinify ["a","b"] <<a * b>>  -->     Var 0 * Var 1
-
---------------------------------------------------------------------------------
-
-calculatePrecs :: GlobalEnv' -> [SName] -> (SExp, [(SName, SExp)]) -> SExp
-calculatePrecs _ vs (e, []) = e
-calculatePrecs dcls vs (e, xs) = calcPrec (\op x y -> op `SAppV` x `SAppV` y) (getFixity dcls . gf) e $ (sVar vs *** id) <$> xs
-  where
-    gf (SGlobal n) = n
-    gf (SVar i) = vs !! i
-
-getFixity :: GlobalEnv' -> SName -> Fixity
-getFixity (fm, _) n = fromMaybe (Just FDLeft, 9) $ Map.lookup n fm
-
-mkGlobalEnv' :: [Stmt] -> GlobalEnv'
-mkGlobalEnv' ss =
-    ( Map.fromList [(s, f) | PrecDef s f <- ss]
-    , Map.fromList [(cn, ((t, length (fst $ getParamsS ty){-todo-}), (id *** f) <$> cs)) | Data t ps ty cs <- ss, (cn, ct) <- cs]
-    )
-  where
-    f ct = length $ filter ((==Visible) . fst) $ fst $ getParamsS ct
-
-extractGlobalEnv' :: GlobalEnv -> GlobalEnv'
-extractGlobalEnv' ge =
-    ( Map.fromList
-        [ (n, f) | (n, (d, _)) <- Map.toList ge, f <- maybeToList $ case d of
-            Con (ConName _ f _ _) [] -> f
-            TyCon (TyConName _ f _ _ _ _) [] -> f
-            Label (getFunName -> Just (FunName _ f _)) _ -> f
-            Fun (FunName _ f _) [] -> f
-            _ -> Nothing
-        ]
-    , Map.fromList
-        [ (n, case conTypeName cn of TyConName t _ inum _ cons _ -> ((t, inum), map f cons))
-        | (n, (Con cn [], _)) <- Map.toList ge
-        ]
-    )
-  where
-    f (ConName n _ _ ct) = (n, length $ filter ((==Visible) . fst) $ fst $ getParams ct)
-
-joinGlobalEnv' (fm, cm) (fm', cm') = (Map.union fm fm', Map.union cm cm')
-
-calcPrec
-  :: (Show e)
-     => (e -> e -> e -> e)
-     -> (e -> Fixity)
-     -> e
-     -> [(e, e)]
-     -> e
-calcPrec app getFixity e es = compileOps [((Nothing, -1), undefined, e)] es
-  where
-    compileOps [(_, _, e)] [] = e
-    compileOps acc [] = compileOps (shrink acc) []
-    compileOps acc@((p, g, e1): ee) es_@((op, e'): es) = case compareFixity (pr, op) (p, g) of
-        Right GT -> compileOps ((pr, op, e'): acc) es
-        Right LT -> compileOps (shrink acc) es_
-        Left err -> error err
-      where
-        pr = getFixity op
-
-    shrink ((_, op, e): (pr, op', e'): es) = (pr, op', app op e' e): es
-
-    compareFixity ((dir, i), op) ((dir', i'), op')
-        | i > i' = Right GT
-        | i < i' = Right LT
-        | otherwise = case (dir, dir') of
-            (Just FDLeft, Just FDLeft) -> Right LT
-            (Just FDRight, Just FDRight) -> Right GT
-            _ -> Left $ "fixity error:" ++ show (op, op')
-
-mkPi Hidden (getTTuple -> Just (n, xs)) b | n == length xs = foldr (sNonDepPi Hidden) b xs
-mkPi h a b = sNonDepPi h a b
-
-sNonDepPi h a b = SPi h a $ upS b
-
-getTTuple (SAppV (getTTuple -> Just (n, xs)) z) = Just (n, xs ++ [z]{-todo: eff-})
-getTTuple (SGlobal s@(splitAt 6 -> ("'Tuple", reads -> [(n, "")]))) = Just (n :: Int, [])
-getTTuple _ = Nothing
-
-mkLets :: GlobalEnv' -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-}
-mkLets _ [] e = e
-mkLets ge (Let n _ mt _ (downS 0 -> Just x): ds) e
-    = SLet ({-maybe id (flip SAnn . af) mt-}{-todo-} x) (substSG n (SVar 0) $ upS $ mkLets ge ds e)
-mkLets ge (ValueDef (ns, p) x: ds) e = patLam id ge p (deBruinify ns $ mkLets ge ds e) `SAppV` x    -- (p = e; f) -->  (\p -> f) e
-mkLets _ (x: ds) e = error $ "mkLets: " ++ show x
-
-patLam f ge = patLam_ f ge (Visible, Wildcard SType)
-
-patLam_ :: (SExp -> SExp) -> GlobalEnv' -> (Visibility, SExp) -> Pat -> SExp -> SExp
-patLam_ f ge (v, t) p e = SLam v t $ compileGuardTree f ge $ compilePatts [(p, 0)] Nothing e
-
-mkTuple _ [x] = x
-mkTuple (Just True, _) xs = foldl SAppV (SGlobal $ "'Tuple" ++ show (length xs)) xs
-mkTuple (Just False, _) xs = foldl SAppV (SGlobal $ "Tuple" ++ show (length xs)) xs
-mkTuple _ xs = error "mkTuple"
-
-mkList (Just True, _) [x] = SGlobal "'List" `SAppV` x
-mkList (Just False, _) xs = foldr (\x l -> SGlobal "Cons" `SAppV` x `SAppV` l) (SGlobal "Nil") xs
-mkList _ xs = error "mkList"
-
-parseSomeGuards ns f e = do
-    pos <- sourceColumn <$> getPosition <* operator "|"
-    guard $ f pos
-    (e', f) <-
-         do (e', PCon p vs) <- try $ pattern' ns e <* operator "<-"
-            x <- parseETerm ns PrecEq e
-            return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs)
-     <|> do x <- parseETerm ns PrecEq e
-            return (e, \gs' gs -> [GuardNode x "True" [] $ Alts gs', GuardNode x "False" [] $ Alts gs])
-    f <$> (parseSomeGuards ns (> pos) e' <|> (:[]) . GuardLeaf <$ operator "->" <*> parseETerm ns PrecLam e')
-      <*> (parseSomeGuards ns (== pos) e <|> pure [])
-
-findAdt (_, cm) con = case Map.lookup con cm of
-    Just i -> i
-    _ -> error $ "findAdt:" ++ con
-
-mkNat (Just False, _) n = SGlobal "fromInt" `SAppV` sLit (LInt $ fromIntegral n)
-mkNat _ n = toNat n
-
-toNat 0 = SGlobal "Zero"
-toNat n = SAppV (SGlobal "Succ") $ toNat (n-1)
-
---------------------------------------------------------------------------------
-
--- parallel patterns like  v@(f -> [])@(Just x)
-newtype ParPat = ParPat [Pat]
-  deriving Show
-
-data Pat
-    = PVar -- Int
-    | PCon SName [ParPat]
-    | ViewPat SExp ParPat
-    | PatType ParPat SExp
-  deriving Show
-
-data GuardTree
-    = GuardNode SExp Name [ParPat] GuardTree -- _ <- _
-    | Alts [GuardTree]          --      _ | _
-    | GuardLeaf SExp            --     _ -> e
-  deriving Show
-
-mapGT k i = \case
-    GuardNode e c pps gt -> GuardNode (i k e) c ({-todo: up-} pps) $ mapGT (k + sum (map varPP pps)) i gt
-    Alts gts -> Alts $ map (mapGT k i) gts
-    GuardLeaf e -> GuardLeaf $ i k e
-
-upGT k i = mapGT k $ \k -> upS__ k i
-
-substGT i j = mapGT 0 $ \k -> rearrangeS $ \r -> if r == k + i then k + j else if r > k + i then r - 1 else r
-{-
-substGT :: Int -> Int -> GuardTree -> GuardTree
-substGT i x = \case
-    GuardNode e n ps t -> GuardNode (substS i (Var x) e) n ps{-todo-} $ substGT i x
-    Alts gs -> Alts $ substGT i x <$> gs
-    GuardLeaf e -> substS i (Var x) e
--}
-
-mapPP f = \case
-    ParPat ps -> ParPat (mapP f <$> ps)
-
-mapP :: (SExp -> SExp) -> Pat -> Pat
-mapP f = \case
-    PVar -> PVar
-    PCon n pp -> PCon n (mapPP f <$> pp)
-    ViewPat e pp -> ViewPat (f e) (mapPP f pp)
-    PatType pp e -> PatType (mapPP f pp) (f e)
-
-upP i j = mapP (upS__ i j)
-
-varPP = \case
-    ParPat ps -> sum $ map varP ps
-
-varP = \case
-    PVar -> 1
-    PCon n pp -> sum $ map varPP pp
-    ViewPat e pp -> varPP pp
-    PatType pp e -> varPP pp
-
-
-alts (Alts xs) = concatMap alts xs
-alts x = [x]
-
-compileGuardTree :: (SExp -> SExp) -> GlobalEnv' -> GuardTree -> SExp
-compileGuardTree node adts t = (\x -> traceD ("  !  :" ++ showSExp x) x) $ guardTreeToCases t
-  where
-    guardTreeToCases :: GuardTree -> SExp
-    guardTreeToCases t = case alts t of
-        [] -> node $ SGlobal "undefined"
-        GuardLeaf e: _ -> node e
-        ts@(GuardNode f s _ _: _) ->
-          mkCase t inum f $
-            [ (n, guardTreeToCases $ Alts $ map (filterGuardTree (upS__ 0 n f) cn 0 n . upGT 0 n) ts)
-            | (cn, n) <- cns
-            ]
-          where
-            ((t, inum), cns) = findAdt adts s
-
-    mkCase :: SName -> Int -> SExp -> [(Int, SExp)] -> SExp
-    mkCase t inum f cs = foldl SAppV (SGlobal (caseName t) `SAppV` iterateN (1 + inum) (SLam Visible $ Wildcard SType) (Wildcard SType))
-        [iterateN vs (SLam Visible (Wildcard SType)) e | (vs, e) <- cs]
-        `SAppV` f
-
-    filterGuardTree :: SExp -> SName{-constr.-} -> Int -> Int{-number of constr. params-} -> GuardTree -> GuardTree
-    filterGuardTree f s k ns = \case
-        GuardLeaf e -> GuardLeaf e
-        Alts ts -> Alts $ map (filterGuardTree f s k ns) ts
-        GuardNode f' s' ps gs
-            | f /= f'  -> GuardNode f' s' ps $ filterGuardTree (upS__ 0 su f) s (su + k) ns gs
-            | s == s'  -> filterGuardTree f s k ns $ guardNodes (zips [k+ns-1, k+ns-2..] ps) gs
-            | otherwise -> Alts []
-          where
-            zips is ps = zip (map SVar $ zipWith (+) is $ sums $ map varPP ps) ps
-            su = sum $ map varPP ps
-            sums = scanl (+) 0
-
-    guardNodes :: [(SExp, ParPat)] -> GuardTree -> GuardTree
-    guardNodes [] l = l
-    guardNodes ((v, ParPat ws): vs) e = guardNode v ws $ guardNodes vs e
-
-    guardNode :: SExp -> [Pat] -> GuardTree -> GuardTree
---    guardNode v [] e = e
-    guardNode v (w: []) e = case w of
-        PVar -> {-todo guardNode v (subst x v ws) $ -} varGuardNode 0 v e
-        ViewPat f (ParPat p) -> guardNode (f `SAppV` v) p {- $ guardNode v ws -} e
-        PCon s ps' -> GuardNode v s ps' {- $ guardNode v ws -} e
-
-varGuardNode v (SVar e) gt = substGT v e gt
-
-compileCase ge x cs
-    = SLam Visible (Wildcard SType) (compileGuardTree id ge $ Alts [compilePatts [(p, 0)] Nothing e | (p, e) <- cs]) `SAppV` x
-
--- todo: clenup
-compilePatts :: [(Pat, Int)] -> Maybe SExp -> SExp -> GuardTree
-compilePatts ps gu = cp [] ps
-  where
-    cp ps' [] e = case gu of
-        Nothing -> rhs
-        Just ge -> GuardNode (rearrangeS (f $ reverse ps') ge) "True" [] rhs
-      where rhs = GuardLeaf $ rearrangeS (f $ reverse ps') e
-    cp ps' ((p@PVar, i): xs) e = cp (p: ps') xs e
-    cp ps' ((p@(PCon n ps), i): xs) e = GuardNode (SVar $ i + sum (map (fromMaybe 0 . ff) ps')) n ps $ cp (p: ps') xs e
-    cp ps' ((p@(ViewPat f (ParPat [PCon n ps])), i): xs) e
-        = GuardNode (SAppV f $ SVar $ i + sum (map (fromMaybe 0 . ff) ps')) n ps $ cp (p: ps') xs e
-
-    m = length ps
-
-    ff PVar = Nothing
-    ff p = Just $ varP p
-
-    f ps i
-        | i >= s = i - s + m + sum vs'
-        | i < s = case vs_ !! n of
-        Nothing -> m + sum vs' - 1 - n
-        Just _ -> m + sum vs' - 1 - (m + sum (take n vs') + j)
-      where
-        i' = s - 1 - i
-        (n, j) = concat (zipWith (\k j -> zip (repeat j) [0..k-1]) vs [0..]) !! i'
-
-        vs_ = map ff ps
-        vs = map (fromMaybe 1) vs_
-        vs' = map (fromMaybe 0) vs_
-        s = sum vs
-
-
--------------------------------------------------------------------------------- pretty print
-
-showExp :: Exp -> String
-showExp = showDoc . expDoc
-
-showSExp :: SExp -> String
-showSExp = showDoc . sExpDoc
-
-showEnv :: Env -> String
-showEnv e = showDoc $ envDoc e $ pure $ shAtom $ underlined "<<HERE>>"
-
-showEnvExp :: Env -> Exp -> String
-showEnvExp e c = showDoc $ envDoc e $ epar <$> expDoc c
-
-showEnvSExp :: Env -> SExp -> String
-showEnvSExp e c = showDoc $ envDoc e $ epar <$> sExpDoc c
-
-showEnvSExpType :: Env -> SExp -> Exp -> String
-showEnvSExpType e c t = showDoc $ envDoc e $ epar <$> (shAnn "::" False <$> sExpDoc c <**> expDoc t)
-  where
-    infixl 4 <**>
-    (<**>) :: Doc_ (a -> b) -> Doc_ a -> Doc_ b
-    a <**> b = get >>= \s -> lift $ evalStateT a s <*> evalStateT b s
-
-showDoc :: Doc -> String
-showDoc = str . flip runReader [] . flip evalStateT (flip (:) <$> iterate ('\'':) "" <*> ['a'..'z'])
-
-type Doc_ a = StateT [String] (Reader [String]) a
-type Doc = Doc_ PrecString
-
-envDoc :: Env -> Doc -> Doc
-envDoc x m = case x of
-    EGlobal{}           -> m
-    EBind1 h ts b       -> envDoc ts $ join $ shLam (usedS 0 b) h <$> m <*> pure (sExpDoc b)
-    EBind2 h a ts       -> envDoc ts $ join $ shLam True h <$> expDoc a <*> pure m
-    EApp1 h ts b        -> envDoc ts $ shApp h <$> m <*> sExpDoc b
-    EApp2 h (Lam Visible TType (Var 0)) ts -> envDoc ts $ shApp h (shAtom "tyType") <$> m
-    EApp2 h a ts        -> envDoc ts $ shApp h <$> expDoc a <*> m
-    ELet1 ts b          -> envDoc ts $ shLet_ m (sExpDoc b)
-    ELet2 (x, _) ts     -> envDoc ts $ shLet_ (expDoc x) m
-    EAssign i x ts      -> envDoc ts $ shLet i (expDoc x) m
-    CheckType t ts      -> envDoc ts $ shAnn ":" False <$> m <*> expDoc t
-    CheckSame t ts      -> envDoc ts $ shCstr <$> m <*> expDoc t
-    CheckAppType h t te b      -> envDoc (EApp1 h (CheckType t te) b) m
-    ELabelEnd ts        -> envDoc ts $ shApp Visible (shAtom "labEnd") <$> m
-
-expDoc :: Exp -> Doc
-expDoc e = fmap inGreen <$> f e
-  where
-    f = \case
-        Label x _       -> f x
-        Var k           -> shVar k
-        App a b         -> shApp Visible <$> f a <*> f b
-        Lam h a b       -> join $ shLam (usedE 0 b) (BLam h) <$> f a <*> pure (f b)
-        Bind h a b      -> join $ shLam (usedE 0 b) h <$> f a <*> pure (f b)
-        Cstr a b        -> shCstr <$> f a <*> f b
-        FunN s xs       -> foldl (shApp Visible) (shAtom s) <$> mapM f xs
-        CaseFunN s xs   -> foldl (shApp Visible) (shAtom s) <$> mapM f xs
-        ConN s xs       -> foldl (shApp Visible) (shAtom s) <$> mapM f xs
-        TyConN s xs     -> foldl (shApp Visible) (shAtom s) <$> mapM f xs
-        TType           -> pure $ shAtom "Type"
-        ELit l          -> pure $ shAtom $ show l
-        Assign i x e    -> shLet i (f x) (f e)
-        LabelEnd x      -> shApp Visible (shAtom "labend") <$> f x
-
-sExpDoc :: SExp -> Doc
-sExpDoc = \case
-    SGlobal s       -> pure $ shAtom s
-    SAnn a b        -> shAnn ":" False <$> sExpDoc a <*> sExpDoc b
-    TyType a        -> shApp Visible (shAtom "tyType") <$> sExpDoc a
-    SApp h a b      -> shApp h <$> sExpDoc a <*> sExpDoc b
---    Wildcard t      -> shAnn True (shAtom "_") <$> sExpDoc t
-    SBind h a b     -> join $ shLam (usedS 0 b) h <$> sExpDoc a <*> pure (sExpDoc b)
-    SLet a b        -> shLet_ (sExpDoc a) (sExpDoc b)
-    STyped (e, t)   -> expDoc e
-    SVar i          -> expDoc (Var i)
-
-shVar i = asks $ shAtom . lookupVarName where
-    lookupVarName xs | i < length xs && i >= 0 = xs !! i
-    lookupVarName _ = "V" ++ show i
-
-shLet i a b = shVar i >>= \i' -> local (dropNth i) $ shLam' <$> (cpar . shLet' (fmap inBlue i') <$> a) <*> b
-shLet_ a b = (gets head <* modify tail) >>= \i -> shLam' <$> (cpar . shLet' (shAtom i) <$> a) <*> local (i:) b
-shLam used h a b = (gets head <* modify tail) >>= \i ->
-    let lam = case h of
-            BPi _ -> shArr
-            _ -> shLam'
-        p = case h of
-            BMeta -> cpar . shAnn ":" True (shAtom $ inBlue i)
-            BLam h -> vpar h
-            BPi h -> vpar h
-        vpar Hidden = brace . shAnn ":" True (shAtom $ inGreen i)
-        vpar Visible = ann (shAtom $ inGreen i)
-        ann | used = shAnn ":" False
-            | otherwise = const id
-    in lam (p a) <$> local (i:) b
-
------------------------------------------
-
-data PS a = PS Prec a deriving (Functor)
-type PrecString = PS String
-
-getPrec (PS p _) = p
-prec i s = PS i (s i)
-str (PS _ s) = s
-
-data Prec
-    = PrecAtom      --  ( _ )  ...
-    | PrecAtom'
-    | PrecProj      --  _ ._                {left}
-    | PrecSwiz      --  _%_                 {left}
-    | PrecApp       --  _ _                 {left}
-    | PrecOp
-    | PrecArr       --  _ -> _              {right}
-    | PrecEq        --  _ ~ _
-    | PrecAnn       --  _ :: _              {right}
-    | PrecLet       --  _ := _
-    | PrecLam       --  \ _ -> _            {right} {accum}
-    deriving (Eq, Ord)
-
-lpar, rpar :: PrecString -> Prec -> String
-lpar (PS i s) j = par (i >. j) s  where
-    PrecLam >. i = i > PrecAtom'
-    i >. PrecLam = i >= PrecArr
-    PrecApp >. PrecApp = False
-    i >. j  = i >= j
-rpar (PS i s) j = par (i >. j) s where
-    PrecLam >. PrecLam = False
-    PrecLam >. i = i > PrecAtom'
-    PrecArr >. PrecArr = False
-    PrecAnn >. PrecAnn = False
-    i >. j  = i >= j
-
-par True s = "(" ++ s ++ ")"
-par False s = s
-
-isAtom = (==PrecAtom) . getPrec
-isAtom' = (<=PrecAtom') . getPrec
-
-shAtom = PS PrecAtom
-shAtom' = PS PrecAtom'
-shAnn _ True x y | str y `elem` ["Type", inGreen "Type"] = x
-shAnn s simp x y | isAtom x && isAtom y = shAtom' $ str x <> s <> str y
-shAnn s simp x y = prec PrecAnn $ lpar x <> " " <> const s <> " " <> rpar y
-shApp Hidden x y = prec PrecApp $ lpar x <> " " <> const (str $ brace y)
-shApp h x y = prec PrecApp $ lpar x <> " " <> rpar y
-shArr x y | isAtom x && isAtom y = shAtom' $ str x <> "->" <> str y
-shArr x y = prec PrecArr $ lpar x <> " -> " <> rpar y
-shCstr x y | isAtom x && isAtom y = shAtom' $ str x <> "~" <> str y
-shCstr x y = prec PrecEq $ lpar x <> " ~ " <> rpar y
-shLet' x y | isAtom x && isAtom y = shAtom' $ str x <> ":=" <> str y
-shLet' x y = prec PrecLet $ lpar x <> " := " <> rpar y
-shLam' x y | PrecLam <- getPrec y = prec PrecLam $ "\\" <> lpar x <> " " <> pure (dropC $ str y)
-shLam' x y | isAtom x && isAtom y = shAtom' $ "\\" <> str x <> "->" <> str y
-shLam' x y = prec PrecLam $ "\\" <> lpar x <> " -> " <> rpar y
-brace s = shAtom $ "{" <> str s <> "}"
-cpar s | isAtom' s = s      -- TODO: replace with lpar, rpar
-cpar s = shAtom $ par True $ str s
-epar s = fmap underlined s
-
-dropC (ESC s (dropC -> x)) = ESC s x
-dropC (x: xs) = xs
-
-pattern ESC a b <- (splitESC -> Just (a, b)) where ESC a b | all (/='m') a = "\ESC[" ++ a ++ "m" ++ b
-
-splitESC ('\ESC':'[': (span (/='m') -> (a, ~(c: b)))) | c == 'm' = Just (a, b)
-splitESC _ = Nothing
-
-instance IsString (Prec -> String) where fromString = const
-
-inGreen = withEsc 32
-inBlue = withEsc 34
-inRed = withEsc 31
-underlined = withEsc 47
-withEsc i s = ESC (show i) $ s ++ ESC "" ""
-
-correctEscs = (++ "\ESC[K") . f ["39","49"] where
-    f acc (ESC i@(_:_) cs) = ESC i $ f (i:acc) cs
-    f (a: acc) (ESC "" cs) = ESC (compOld (cType a) acc) $ f acc cs
-    f acc (c: cs) = c: f acc cs
-    f acc [] = []
-
-    compOld x xs = head $ filter ((== x) . cType) xs
-
-    cType n
-        | "30" <= n && n <= "39" = 0
-        | "40" <= n && n <= "49" = 1
-        | otherwise = 2
-
-
-putStrLn_ = putStrLn . correctEscs
-error_ = error . correctEscs
-trace_ = trace . correctEscs
-throwError_ = throwError . correctEscs
-traceD x = if debug then trace_ x else id
-
--------------------------------------------------------------------------------- main
-
-type TraceLevel = Int
-trace_level = 0 :: TraceLevel  -- 0: no trace
-tr = False --trace_level >= 2
-tr_light = trace_level >= 1
-
-debug = False--True--tr
-debug_light = True--False
-
-infer :: GlobalEnv -> [Stmt] -> Either String GlobalEnv
-infer env = fmap (forceGE . snd) . runExcept . flip runStateT (initEnv <> env) . mapM_ handleStmt
-
-forceGE x = length (concatMap (uncurry (++) . (showExp *** showExp)) $ Map.elems x) `seq` x
-
-fromRight ~(Right x) = x
-
--------------------------------------------------------------------------------- utils
-
-dropNth i xs = take i xs ++ drop (i+1) xs
-iterateN n f e = iterate f e !! n
-holes xs = [(as, x, bs) | (as, x: bs) <- zip (inits xs) (tails xs)]
-
diff --git a/prototypes/Linear.hs b/prototypes/Linear.hs
deleted file mode 120000
index 5f80cf33..00000000
--- a/prototypes/Linear.hs
+++ /dev/null
@@ -1 +0,0 @@
-../Linear.hs
\ No newline at end of file
diff --git a/prototypes/Parser.hs b/prototypes/Parser.hs
deleted file mode 100644
index 75a3a722..00000000
--- a/prototypes/Parser.hs
+++ /dev/null
@@ -1 +0,0 @@
-module Parser where
diff --git a/prototypes/Pretty.hs b/prototypes/Pretty.hs
deleted file mode 120000
index eb36e481..00000000
--- a/prototypes/Pretty.hs
+++ /dev/null
@@ -1 +0,0 @@
-../Pretty.hs
\ No newline at end of file
diff --git a/prototypes/TODO b/prototypes/TODO
deleted file mode 100644
index 9329cd9f..00000000
--- a/prototypes/TODO
+++ /dev/null
@@ -1,207 +0,0 @@
-
-Done:
-
--   pattern match compiler prototípus
-    -   beépítve a korábbi fordítóba
--   IORef-es/STRef-es kiértékelő
-    ->  ennek a használata elbonyolítaná az implementációt:
-        -   mindent monadikussá kellene tenni, ez különösen fájdalmas mintaillesztéskor
-        -   plusz típusváltozó minden típuban / vagy IO mindenhol
-        -   explicit sharing mindenhol
--   tiszta hatékony interpreter + típusellenőrző függő típusozáshoz
-    -   tiszta, a Haskell lusta kiértékelését használja sharingre
-    -   külön kiértékelő típusozás közben és típusozás után a hatékonyság növelésére
-    -   type erasure a hatékonyság növelésére (az dep. type ellensúlyozására)
-    -   memory leak ellen védett De Bruijn változók
-    -   a kifejezésektől különválasztott típus a hatékonyság növelésére
-    -   többszöri próbálkozás az beépítésre az előző fordítóba
-        még meglévő különbségek:
-        -   nincs különválasztva a típusozás közbeni és utáni kiértékelés
-        -   globális nevek vs. De Bruijn
-        -   ad-hoc rejtett argumentumok (működnek vele a dep. rekordokkal emulált típusosztályok)
-        -   ad-hoc RankNTypes (magic, valahogy működnek vele a dep. rekordokkal emulált típusosztályok)
-        -   ad-hoc type erasure (megy konstruktorokra, nem megy a felhasználó által definiált kifejezésekre)
-        -   nincs különválasztva a típus
-        -   a kompozícionális típusozó nem tudja felhasználni a típusban megadott segítséget
-            -   ez kizárja pl. RankNType-ot, és a függő típusozást
-            -   a meglévő példákhoz nem kellett, összetettebb dep. rekordos típusosztályoknál kritikus lehet
--   típusozó prototípus
-    -   irányított (figyelembe veszi a megadott típusokat)
-    -   dependens
-    -   rejtett argumentumok
-    -   RankNTypes
-    -   pattern matching compiler beépítése
-    -   több implementáció kipróbálása, a legutolsó zippereket használ
-        -   könyebb debugolás
-        -   eddigi leghatékonyabb
-        -   kicsi implementáció, és bővíthetőnek is látszik
-    -   címkézés a jobb mintaillesztés támogatáshoz
-
-összefoglaló TODO lista
-
-fő tennivaló: a típusozó kiegészítése
--   syntactic sugars
--   type classes as a syntax sugar
-    -   egyszerűbb, átlátható szemantika
-        -   könnyebb a más nyelvi elemekkel való viszonyát tisztázni
-    -   modulárisabb implementáció
-        -   könnyebben karbantartható
-        -   könnyebben tesztelhető implementáció
--   teljesítmény javítás, több check
-
-
--------------------------------------------------------------------------------- short-term TODOs
--   GLSL codegen doesn't support Vector and tuple patterns (not compiler frontend related):
-      fragment02tuple
-      fragment02vectorpattern
-      fragment05uniform
--   recheck should not fail - coe missing?
--   fix loop
-        primes
-        recursivetexture01
--   (a ~ b) + (a ~ c)   --->   b ~ c        (fragment06tailrecursion)
-
--------------------------------------------------------------------------------- TODOs after 100% tests (completion & cleanup)
-
--   @ patterns
--   guards
--   guards + where
--   complete & review builtin reductions & move out into libraries
--   type annotation in where blocks
--   dependent prelude should work again
-
--   constructor operator fixities (also in patterns)
--   local pattern matching functions
--   mutual recursion (as a language extension)
--   record filed name handling
-
--   data Wrong = Wrong a
-
--   basic refactoring
-
--   de-brunify move away from parser? / refactoring
-
--   ambiguity check
-    -   suppress univ. polymorphic ambiguity
-    -   konstans megadott típus szigorúan vétele
-    -   prohibit constraints like    a ~ List a,  a ~ a -> a, etc.
-
--   bug fix (as needed)
-    -   (~) :: forall a b . a -> b -> Type                ?
-    -   bug: head <-> tail  csere nem jelez hibát, viszont recheck fails
-    -   coe korrektebb használata (másmikor kell beszúrni)   ?
-    -   app típusozás jobban
-    -   label + let arity in recursive definitions
-
-
--------------------------------------------------------------------------------- medium-term TODOs
-
--   type classes
-    -   generate type-case functions
-    -   class parse + desugaring
-    -   instance parse (drop it first)
-    -   type class desugaring
-    -   super class "visszaállítás"
-    -   Constraint type: uniqueness of witnesses 0-1 elemű típusokra
-
--   better error messages
-    -   location infó
-    -   jobb normalizáció elkerülés (String => [Char] lehetőleg ne)
-    -   kompozícionálisabb inference?
-
--   systematic micro tests (with quickcheck?)
-
--   performance
-    -   típus-érték különválasztás (vs. church style lambda)
-        -   lam változó típusának kitörlése
-                    expType
-                    recheck
-                    envDoc, expDoc
-                    cstr
-                    foldE ?
-        -   neutrális termek külön
-        -   konstruktorok univ. pol. típusainak kitörlése
-    -   irrelevance + erasure
-    -   max. De Bruijn index számolás
-
-    -   ügyesebb De Bruijn (kitörlős)
-    -   interpretált De Bruijn
-    -   coe / type class irrelevance switch
-
--   injektivitás inferencia
-
--   open functions, type families syntax
-
--   dep. pattern matching
--   evalXXX deriválás
-
--   frekvenciák
-
--   separate LambdaCube 3D specific parts
-
--------------------------------------------------------------------------------- cleanup after medium-term TODOs
-
--   huge refactoring, documentation, test cases, ...
-
-milestone: 1.0 compiler
-
-
--------------------------------------------------------------------------------- notes
---------------------------------------------------------------------------------
-
--------------------------------------------------------------------------------- row polymorphism
-
-builtins
-    Split :: Type -> Type -> Type -> Constraint --Type
-
-
-data RecordC (xs :: List (Pair String Type))
-    = RecordCons (tuptype (map snd xs))
-
-tuptype [] = ()
-tuptype (x: xs) = (x,  tuptype xs)
-
-Record :: List (Pair String Type) -> Type
-Record xs = RecordC (sortBy fst xs)
-
-builtins
-    project :: forall (xs :: List [(String, Type)]) . (s :: String) -> (Split (RecordC xs) (RecordC [(s, a)] b) -> RecordC xs -> a
-
--- project = ...
-
-
-w :: Split a b c
- iff
-a = Record as
-b = Record bs
-c = Record cs
-
-bs `sublist` as
-cs `sublist` as
-map fst bs  `disjunct`  map fst cs
-
-
- :: Record {x: Float}
-
-
-v1 :: Record {x: Float, y: Float, z: Float}
-v1 = {x: 1.0, y: 2.0, z: 3.0}                   ----> RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, (2.0, (3.0, ())))
-v2 = {x: 1.0, y: 2.0, z: 3.0, a: 4.0}
-
-f :: (Split a (Record {x: Float, y: Float}) b) => a -> Float
-f v = v.x +! v.y
-
-r = f v1 +! f v2    -- this is valid
-
-
-        exp.field      ----->           project field exp
-
-f v1           --        a ~ Record {x: Float, y: Float, z: Float}
-
-
-    eval
-        Split (Record xs) (Record ys) c    = eval $   c ~ Record (xs \\ ys)
-        Split (Record xs) c (Record ys)    = eval $   c ~ Record (xs \\ ys)
-        Split a (Record xs) (Record ys)    = eval $   a ~ Record (xs ++ ys)
-
-
diff --git a/prototypes/Text b/prototypes/Text
deleted file mode 120000
index 4ea788ba..00000000
--- a/prototypes/Text
+++ /dev/null
@@ -1 +0,0 @@
-../Text
\ No newline at end of file
diff --git a/prototypes/Type.hs b/prototypes/Type.hs
deleted file mode 100644
index 8e1e6af5..00000000
--- a/prototypes/Type.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-module Type ( module CGExp ) where
-import CGExp
diff --git a/prototypes/Typecheck.hs b/prototypes/Typecheck.hs
deleted file mode 100644
index dc82a9a0..00000000
--- a/prototypes/Typecheck.hs
+++ /dev/null
@@ -1 +0,0 @@
-module Typecheck where
diff --git a/prototypes/create-test-report.sh b/prototypes/create-test-report.sh
deleted file mode 100755
index 4d26467a..00000000
--- a/prototypes/create-test-report.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#! /bin/sh
-
-CABAL_NAME=lambdacube-compiler
-
-HPC_DIR=dist/hpc/${CABAL_NAME}
-HPC_REPO_DIR=$HPC_DIR
-
-TEST_DIR=src/UnitTest
-TIX=lambdacube-compiler-test-suite.tix
-
-hpc report ${TIX} --hpcdir=${HPC_DIR} --xml-output > ${HPC_REPO_DIR}/result.xml
-hpc markup ${TIX} --hpcdir=${HPC_DIR} --destdir=${HPC_REPO_DIR}
diff --git a/prototypes/lambdacube-compiler.cabal b/prototypes/lambdacube-compiler.cabal
deleted file mode 100644
index 76d26c98..00000000
--- a/prototypes/lambdacube-compiler.cabal
+++ /dev/null
@@ -1,96 +0,0 @@
--- Initial lambdacube-dsl.cabal generated by cabal init.  For further 
--- documentation, see http://haskell.org/cabal/users-guide/
-
-name:                lambdacube-compiler
-version:             0.2.0.0
-homepage:            lambdacube3d.com
-license:             BSD3
-license-file:        LICENSE
-author:              Csaba Hruska, Peter Divianszky
-maintainer:          csaba.hruska@gmail.com
-category:            Graphics
-build-type:          Simple
-cabal-version:       >=1.10
-
-Flag profiling
-  Description: Enable profiling
-  Default: False
-
-library
-  -- indentation parser modules
-  exposed-modules:   Text.Parser.Indentation.Implementation,
-                     Text.Parsec.Indentation,
-                     Text.Parsec.Indentation.Char,
-                     Text.Parsec.Indentation.Token
-  exposed-modules:
-    -- Compiler
-    Pretty
-    Type
-    Typecheck
-    Parser
-    IR
-    Linear
-    CoreToIR
-    CoreToGLSL
-    Infer
-    CGExp
-    Driver
-  other-extensions:
-    LambdaCase
-    PatternSynonyms
-    ViewPatterns
-    TypeSynonymInstances
-    FlexibleInstances
-    NoMonomorphismRestriction
-    TypeFamilies
-    RecordWildCards
-    DeriveFunctor
-    DeriveFoldable
-    DeriveTraversable
-    GeneralizedNewtypeDeriving
-    OverloadedStrings
-    TupleSections
-    MonadComprehensions
-    ExistentialQuantification
-    ScopedTypeVariables
-    ParallelListComp
-  build-depends:
-    -- compiler
-    aeson >= 0.9 && <1,
-    base >=4.7 && <4.9,
-    containers >=0.5 && <0.6,
-    deepseq,
-    directory,
-    exceptions >= 0.8 && <0.9,
-    filepath,
-    mtl >=2.2 && <2.3,
-    parsec >= 3.1 && <3.2,
-    pretty-compact >=1.0 && <1.1,
-    text >= 1.2 && <1.3,
-    vector >= 0.11 && <0.12
-  hs-source-dirs:      .
-  default-language:    Haskell2010
-
-executable lambdacube-compiler-test-suite
-  hs-source-dirs:   .
-  main-is:          runTests.hs
-
-  build-depends:
-    aeson >= 0.9 && <1,
-    base < 4.9,
-    containers >=0.5 && <0.6,
-    deepseq,
-    directory,
-    exceptions >= 0.8 && <0.9,
-    filepath,
-    mtl >=2.2 && <2.3,
-    lambdacube-compiler,
-    parsec >= 3.1 && <3.2,
-    pretty-compact >=1.0 && <1.1,
-    text >= 1.2 && <1.3,
-    vector >= 0.11 && <0.12
-  default-language:    Haskell2010
-  if flag(profiling)
-    GHC-Options: -O2 -fhpc -hpcdir dist/hpc/lambdacube-compiler -prof -fprof-auto -rtsopts
-  else
-    GHC-Options: -O2 -fhpc -hpcdir dist/hpc/lambdacube-compiler
diff --git a/prototypes/run-test-suite.sh b/prototypes/run-test-suite.sh
deleted file mode 100755
index 9ced8e55..00000000
--- a/prototypes/run-test-suite.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/bin/bash
-
-if [ "$1" == "--profile" ] ; then
-  shift
-  cabal clean
-  cabal sandbox delete
-  cabal sandbox init
-  cabal install --only-dependencies --enable-library-profiling --enable-executable-profiling
-  cabal configure --flags "profiling" --enable-library-profiling --enable-executable-profiling
-  cabal build
-  cabal run lambdacube-compiler-test-suite -- $@ +RTS -p
-  ./create-test-report.sh
-  rm lambdacube-compiler-test-suite.tix
-  cabal sandbox delete
-  cabal clean
-else
-  cabal run lambdacube-compiler-test-suite -- $@
-  ./create-test-report.sh
-  rm lambdacube-compiler-test-suite.tix
-fi
diff --git a/prototypes/runTests.hs b/prototypes/runTests.hs
deleted file mode 120000
index 74e37a7a..00000000
--- a/prototypes/runTests.hs
+++ /dev/null
@@ -1 +0,0 @@
-../runTests.hs
\ No newline at end of file
diff --git a/prototypes/tests/accept/Builtins.lc b/prototypes/tests/accept/Builtins.lc
deleted file mode 100644
index 187a6e9e..00000000
--- a/prototypes/tests/accept/Builtins.lc
+++ /dev/null
@@ -1,568 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
--- module Builtins where
-
-builtins
-    cstr :: Type -> Type -> Type
---    reflCstr :: forall (a :: Type) -> cstr a a
-    T2 :: Type -> Type -> Type
-    T2C :: Unit -> Unit -> Unit
-
-data Unit = TT
-
--- TODO: generate?
-data Tuple0 = Tuple0
-data Tuple1 a = Tuple1 a
-data Tuple2 a b = Tuple2 a b
-data Tuple3 a b c = Tuple3 a b c
-data Tuple4 a b c d = Tuple4 a b c d
-data Tuple5 a b c d e = Tuple5 a b c d e
-
-id x = x
-
-data Bool = False | True
-
-data Ordering = LT | EQ | GT
-
-primIfThenElse :: Bool -> a -> a -> a
-primIfThenElse True  a b = a
-primIfThenElse False a b = b
-
----------------------------------------
-
-data Nat = Zero | Succ Nat
-
-builtintycons
-    Int     :: Type
-    Word    :: Type
-    Float   :: Type
-    Char    :: Type
-    String  :: Type
-
-{-
-type family TFVec (n :: Nat) a                  -- may be a data family
-type family VecScalar (n :: Nat) a
-type family TFMat i j                           -- may be a data family
-type family MatVecElem a
-type family MatVecScalarElem a
-type family FTRepr' a
-type family ColorRepr a
-type family TFFrameBuffer a
-type family FragOps a
-type family JoinTupleType t1 t2
-class AttributeTuple a
-class ValidOutput a
-class ValidFrameBuffer a
--}
-builtins
-    TFVec           :: Nat -> Type -> Type
-    VecScalar       :: Nat -> Type -> Type
-    TFMat           :: Type -> Type -> Type
-    MatVecElem      :: Type -> Type
-    MatVecScalarElem :: Type -> Type
-    FTRepr'         :: Type -> Type
-    ColorRepr       :: Type -> Type
-    TFFrameBuffer   :: Type -> Type
-    FragOps         :: Type -> Type
-    JoinTupleType   :: Type -> Type -> Type
-
-    AttributeTuple  :: Type -> Type
-    ValidOutput     :: Type -> Type
-    ValidFrameBuffer :: Type -> Type
-
-data VecS (a :: Type) :: Nat -> Type where
-  V2 :: a -> a -> VecS a 2
-  V3 :: a -> a -> a -> VecS a 3
-  V4 :: a -> a -> a -> a -> VecS a 4
-
-builtins
-    Vec :: Nat -> Type -> Type
---Vec n t = VecS t n
-
-
-data Mat :: Nat -> Nat -> Type -> Type where
-  M22F :: Vec 2 Float -> Vec 2 Float -> Mat 2 2 Float
-  M23F :: Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 3 Float
-  M24F :: Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 4 Float
-  M32F :: Vec 3 Float -> Vec 3 Float -> Mat 3 2 Float
-  M33F :: Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 3 3 Float
-  M34F :: Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 3 4 Float
-  M42F :: Vec 4 Float -> Vec 4 Float -> Mat 4 2 Float
-  M43F :: Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 3 Float
-  M44F :: Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
-
-
-builtins
-    CNum, Signed, Num, Component, Integral, NumComponent, Floating :: Type -> Type
-
-    fromInt :: Num a => Int -> a
-    compare :: Num a => a -> a -> Ordering
-    negate :: Num a => a -> a
-
-    vec2 :: Component a => a -> a -> Vec 2 a
-    vec3 :: Component a => a -> a -> a -> Vec 3 a
-    vec4 :: Component a => a -> a -> a -> a -> Vec 4 a
-    zeroComp :: Component a => a
-    oneComp :: Component a => a
-
---------------------------------------- swizzling
-
-data Swizz = Sx | Sy | Sz | Sw
-
-builtins
-  swizzvector :: forall n . forall m . Vec n a -> Vec m Swizz -> Vec m a
-  swizzscalar :: forall n . Vec n a -> Swizz -> a
-
-{-
---------------------------------------- type classes
-
-class CNum a
-
-instance CNum           Int
-instance CNum           Float
-
-class Signed a
-
-instance Signed         Int
-instance Signed         Float
-
-class Num a where
-  fromInt :: Int -> a
-  compare :: a -> a -> Ordering
-  negate :: a -> a
--}
-builtins
-  primIntToWord  :: Int -> Word
-  primIntToFloat :: Int -> Float
-  primCompareInt   :: Int   -> Int   -> Ordering
-  primCompareWord  :: Word  -> Word  -> Ordering
-  primCompareFloat :: Float -> Float -> Ordering
-  primNegateInt   :: Int   -> Int
-  primNegateWord  :: Word  -> Word
-  primNegateFloat :: Float -> Float
-
-{-
-instance Num Int where
-  fromInt = id
-  compare = primCompareInt
-  negate = primNegateInt
-instance Num Word where
-  fromInt = primIntToWord
-  compare = primCompareWord
-  negate = primNegateWord
-instance Num Float where
-  fromInt = primIntToFloat
-  compare = primCompareFloat
-  negate = primNegateFloat
-
-class Component a where
-  vec2 :: a -> a -> Vec 2 a
-  vec3 :: a -> a -> a -> Vec 3 a
-  vec4 :: a -> a -> a -> a -> Vec 4 a
-  zeroComp :: a
-  oneComp :: a
---  PrimZero, PrimOne :: {- (Component a) => -- TODO -} a
-
-
-instance Component Bool where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = False
-  oneComp = True
-
-instance Component Int where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = 0
-  oneComp = 1
-
-instance Component Word where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = 0
-  oneComp = 1
-
-instance Component Float where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = 0
-  oneComp = 1
-
-instance Component (Vec 2 Float) where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = V2 0.0 0.0
-  oneComp = V2 1.0 1.0
-instance Component (Vec 3 Float) where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = V3 0.0 0.0 0.0
-  oneComp = V3 1.0 1.0 1.0
-instance Component (Vec 4 Float) where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = V4 0.0 0.0 0.0 0.0
-  oneComp = V4 1.0 1.0 1.0 1.0
-
---instance Component (Vec 2 Bool) where
---instance Component (Vec 3 Bool) where
-
-instance Component (Vec 4 Bool) where
-  vec2 = V2
-  vec3 = V3
-  vec4 = V4
-  zeroComp = V4 False False False False
-  oneComp = V4 True True True True
-
-class Integral a
-
-instance Integral       Int
-instance Integral       Word
-
-class NumComponent a
-
-instance NumComponent   Int
-instance NumComponent   Word
-instance NumComponent   Float
-instance NumComponent   (Vec 2 Float)
-instance NumComponent   (Vec 3 Float)
-instance NumComponent   (Vec 4 Float)
-
-class Floating a
-
-instance Floating       Float
-instance Floating       (Vec 2 Float)
-instance Floating       (Vec 3 Float)
-instance Floating       (Vec 4 Float)
-instance Floating       (Mat 2 2 Float)
-instance Floating       (Mat 2 3 Float)
-instance Floating       (Mat 2 4 Float)
-instance Floating       (Mat 3 2 Float)
-instance Floating       (Mat 3 3 Float)
-instance Floating       (Mat 3 4 Float)
-instance Floating       (Mat 4 2 Float)
-instance Floating       (Mat 4 3 Float)
-instance Floating       (Mat 4 4 Float)
--}
-
-data BlendingFactor
-    = Zero' --- FIXME: modified
-    | One
-    | SrcColor
-    | OneMinusSrcColor
-    | DstColor
-    | OneMinusDstColor
-    | SrcAlpha
-    | OneMinusSrcAlpha
-    | DstAlpha
-    | OneMinusDstAlpha
-    | ConstantColor
-    | OneMinusConstantColor
-    | ConstantAlpha
-    | OneMinusConstantAlpha
-    | SrcAlphaSaturate
-
-data BlendEquation
-    = FuncAdd
-    | FuncSubtract
-    | FuncReverseSubtract
-    | Min
-    | Max
-
-data LogicOperation
-    = Clear
-    | And
-    | AndReverse
-    | Copy
-    | AndInverted
-    | Noop
-    | Xor
-    | Or
-    | Nor
-    | Equiv
-    | Invert
-    | OrReverse
-    | CopyInverted
-    | OrInverted
-    | Nand
-    | Set
-
-data StencilOperation
-    = OpZero
-    | OpKeep
-    | OpReplace
-    | OpIncr
-    | OpIncrWrap
-    | OpDecr
-    | OpDecrWrap
-    | OpInvert
-
-data ComparisonFunction
-    = Never
-    | Less
-    | Equal
-    | Lequal
-    | Greater
-    | Notequal
-    | Gequal
-    | Always
-
-data ProvokingVertex
-    = LastVertex
-    | FirstVertex
-
-data FrontFace
-    = CW
-    | CCW
-
-data CullMode
-    = CullFront FrontFace
-    | CullBack FrontFace
-    | CullNone
-
-data PointSize
-    = PointSize Float
-    | ProgramPointSize
-
-data PolygonMode
-    = PolygonFill
-    | PolygonPoint PointSize
-    | PolygonLine Float
-
-data PolygonOffset
-    = NoOffset
-    | Offset Float Float
-
-data PointSpriteCoordOrigin
-    = LowerLeft
-    | UpperLeft
-
-
-data Depth a where
-data Stencil a where
-data Color a where
-
-data PrimitiveType
-    = Triangle
-    | Line
-    | Point
-    | TriangleAdjacency
-    | LineAdjacency
-
-builtincons
-  PrimTexture :: () -> Vec 2 Float -> Vec 4 Float
-
-builtincons
-  Uniform   :: String -> t
-  Attribute :: String -> t
-
-data FragmentOut a where
-  FragmentOut          :: (a ~ ColorRepr t) => t                -> FragmentOut a
-  FragmentOutDepth     :: (x ~ ColorRepr t, a ~ JoinTupleType (Depth Float) x) => Float -> t
-                                                                -> FragmentOut a
-  FragmentOutRastDepth :: (x ~ ColorRepr t, a ~ JoinTupleType (Depth Float) x) => t
-                                                                -> FragmentOut a
-
-data VertexOut a where
-  VertexOut           :: (a ~ FTRepr' x) => Vec 4 Float -> Float -> (){-TODO-} -> x -> VertexOut a
-
-data RasterContext :: PrimitiveType -> Type where
-  TriangleCtx         :: CullMode -> PolygonMode -> PolygonOffset -> ProvokingVertex -> RasterContext Triangle
-  PointCtx            :: PointSize -> Float -> PointSpriteCoordOrigin                -> RasterContext Point
-  LineCtx             :: Float -> ProvokingVertex                                    -> RasterContext Line
-
-data FetchPrimitive :: PrimitiveType -> Type where
-   Points              :: FetchPrimitive Point
-   Lines               :: FetchPrimitive Line
-   Triangles           :: FetchPrimitive Triangle
-   LinesAdjacency      :: FetchPrimitive LineAdjacency
-   TrianglesAdjacency  :: FetchPrimitive TriangleAdjacency
-
-data AccumulationContext a where
-  AccumulationContext  :: (a ~ FragOps t) => t -> AccumulationContext a
-
-data Image (a :: Nat) :: Type -> Type where
-  ColorImage          :: (Num t, color ~ VecScalar d t)
-                      => color  -> Image a (Color color)
-  DepthImage          :: Float  -> Image a (Depth Float)
-  StencilImage        :: Int    -> Image a (Stencil Int)
-
-data Interpolated t where
-  Smooth, NoPerspective
-                      :: (Floating t) => t -> Interpolated t
-  Flat                ::                 t -> Interpolated t
-
-data Blending :: Type -> Type where
-  NoBlending          ::                                   Blending t
-  BlendLogicOp        :: (Integral t) => LogicOperation -> Blending t
-  Blend               :: (BlendEquation, BlendEquation)
-                         -> ((BlendingFactor, BlendingFactor), (BlendingFactor, BlendingFactor))
-                         -> Vec 4 Float ->                 Blending Float
-
-{- TODO: more precise kinds
-  FragmentOperation    :: Semantic -> *
-  FragmentOut          :: Semantic -> *
-  VertexOut            :: ???
--}
-
-data FragmentOperation :: Type -> Type where
-  ColorOp             :: (mask ~ VecScalar d Bool, color ~ VecScalar d c, Num c) => Blending c -> mask
-                                                                   -> FragmentOperation (Color color)
-  DepthOp             :: ComparisonFunction -> Bool                -> FragmentOperation (Depth Float)
-  StencilOp           :: StencilTests -> StencilOps -> StencilOps -> FragmentOperation (Stencil Int32)
-
-data FragmentFilter t where
-  PassAll             ::                FragmentFilter t
-  Filter              :: (t -> Bool) -> FragmentFilter t
-
-data VertexStream (a :: PrimitiveType) t where
-  Fetch               :: (AttributeTuple t) => String -> FetchPrimitive a -> t -> VertexStream a t
-  FetchArrays         :: (AttributeTuple t, t ~ FTRepr' t') => FetchPrimitive a -> t' -> VertexStream a t
-
-data PrimitiveStream (p :: PrimitiveType) :: Nat -> Type -> Type where
-  Transform           :: (a -> VertexOut b) -> VertexStream p a -> PrimitiveStream p 1 b
-
-  -- Render Operations
-data FragmentStream (n :: Nat) a where
-  Rasterize           :: RasterContext x -> PrimitiveStream x n a -> FragmentStream n a
-
-data FrameBuffer (n :: Nat) b where
-  Accumulate          :: (ValidOutput b) =>
-                           AccumulationContext b
-                        -> FragmentFilter a
-                        -> (a -> FragmentOut b)
-                        -> FragmentStream n a
-                        -> FrameBuffer n b
-                        -> FrameBuffer n b
-
-  FrameBuffer        :: (ValidFrameBuffer b, FrameBuffer n b ~ TFFrameBuffer a)
-                        => a -> FrameBuffer n b
-
-
-data Output where
-  ScreenOut           :: FrameBuffer a b -> Output
-
-builtins
-  -- * Primitive Functions *
-  -- Arithmetic Functions (componentwise)
-
-  PrimAdd, PrimSub, PrimMul     :: (t ~ MatVecElem a, Num t) => a -> a -> a
-  PrimAddS, PrimSubS, PrimMulS  :: (t ~ MatVecScalarElem a, Num t) => a -> t -> a
-  PrimDiv, PrimMod              :: (Num t, a ~ VecScalar d t) => a -> a -> a
-  PrimDivS, PrimModS            :: (Num t, a ~ VecScalar d t) => a -> t -> a
-  PrimNeg                       :: (t ~ MatVecScalarElem a, Signed t) => a -> a
-  -- Bit-wise Functions
-  PrimBAnd, PrimBOr, PrimBXor   :: (Integral t, a ~ VecScalar d t) => a -> a -> a
-  PrimBAndS, PrimBOrS, PrimBXorS:: (Integral t, a ~ VecScalar d t) => a -> t -> a
-  PrimBNot                      :: (Integral t, a ~ VecScalar d t) => a -> a
-  PrimBShiftL, PrimBShiftR      :: (Integral t, a ~ VecScalar d t, b ~ VecScalar d Word) => a -> b -> a
-  PrimBShiftLS, PrimBShiftRS    :: (Integral t, a ~ VecScalar d t) => a -> Word -> a
-  -- Logic Functions
-  PrimAnd, PrimOr, PrimXor      :: Bool -> Bool -> Bool
-  PrimNot                       :: (a ~ VecScalar d Bool) => a -> a
-  PrimAny, PrimAll              :: (a ~ VecScalar d Bool) => a -> Bool
-
-  -- Angle, Trigonometry and Exponential Functions
-  PrimACos, PrimACosH, PrimASin, PrimASinH, PrimATan, PrimATanH, PrimCos, PrimCosH, PrimDegrees, PrimRadians, PrimSin, PrimSinH, PrimTan, PrimTanH, PrimExp, PrimLog, PrimExp2, PrimLog2, PrimSqrt, PrimInvSqrt
-                                :: (a ~ VecScalar d Float) => a -> a
-  PrimPow, PrimATan2            :: (a ~ VecScalar d Float) => a -> a -> a
-  -- Common Functions
-  PrimFloor, PrimTrunc, PrimRound, PrimRoundEven, PrimCeil, PrimFract
-                                :: (a ~ VecScalar d Float) => a -> a
-  PrimMin, PrimMax              :: (Num t, a ~ VecScalar d t) => a -> a -> a
-  PrimMinS, PrimMaxS            :: (Num t, a ~ VecScalar d t) => a -> t -> a
-  PrimIsNan, PrimIsInf          :: (a ~ VecScalar d Float, b ~ VecScalar d Bool) => a -> b
-  PrimAbs, PrimSign             :: (Signed t, a ~ VecScalar d t) => a -> a
-  PrimModF            :: (a ~ VecScalar d Float) => a -> (a, a)
-  PrimClamp           :: (Num t, a ~ VecScalar d t) => a -> a -> a -> a
-  PrimClampS          :: (Num t, a ~ VecScalar d t) => a -> t -> t -> a
-  PrimMix             :: (a ~ VecScalar d Float) => a -> a -> a -> a
-  PrimMixS            :: (a ~ VecScalar d Float) => a -> a -> Float -> a
-  PrimMixB            :: (a ~ VecScalar d Float, b ~ VecScalar d Bool) => a -> a -> b -> a
-  PrimStep            :: (a ~ TFVec d Float) => a -> a -> a
-  PrimStepS           :: (a ~ VecScalar d Float) => Float -> a -> a
-  PrimSmoothStep      :: (a ~ TFVec d Float) => a -> a -> a -> a
-  PrimSmoothStepS     :: (a ~ VecScalar d Float) => Float -> Float -> a -> a
-
-  -- Integer/Floatonversion Functions
-  PrimFloatBitsToInt  :: (fv ~ VecScalar d Float, iv ~ VecScalar d Int)  => fv -> iv
-  PrimFloatBitsToUInt :: (fv ~ VecScalar d Float, uv ~ VecScalar d Word) => fv -> uv
-  PrimIntBitsToFloat  :: (fv ~ VecScalar d Float, iv ~ VecScalar d Int)  => iv -> fv
-  PrimUIntBitsToFloat :: (fv ~ VecScalar d Float, uv ~ VecScalar d Word) => uv -> fv
-  -- Geometric Functions
-  PrimLength          :: (a ~ VecScalar d Float) => a -> Float
-  PrimDistance, PrimDot
-                      :: (a ~ VecScalar d Float) => a -> a -> Float
-  PrimCross           :: (a ~ VecScalar 3 Float) => a -> a -> a
-  PrimNormalize       :: (a ~ VecScalar d Float) => a -> a
-  PrimFaceForward, PrimRefract
-                      :: (a ~ VecScalar d Float) => a -> a -> a -> a
-  PrimReflect         :: (a ~ VecScalar d Float) => a -> a -> a
-  -- Matrix Functions
-  PrimTranspose       :: (a ~ TFMat h w, b ~ TFMat w h) => a -> b
-  PrimDeterminant     :: (m ~ TFMat s s) => m -> Float
-  PrimInverse         :: (m ~ TFMat s s) => m -> m
-  PrimOuterProduct    :: (m ~ TFMat h w) => w -> h -> m
-  PrimMulMatVec       :: (m ~ TFMat h w) => m -> w -> h
-  PrimMulVecMat       :: (m ~ TFMat h w) => h -> m -> w
-  PrimMulMatMat       :: (a ~ TFMat i j, b ~ TFMat j k, c ~ TFMat i k) => a -> b -> c
-  -- Vector and Scalar Relational Functions
-  PrimLessThan, PrimLessThanEqual, PrimGreaterThan, PrimGreaterThanEqual, PrimEqualV, PrimNotEqualV
-                      :: (Num t, a ~ VecScalar d t, b ~ VecScalar d Bool) => a -> a -> b
-  PrimEqual, PrimNotEqual
-                      :: (t ~ MatVecScalarElem a) => a -> a -> Bool
-  -- Fragment Processing Functions
-  PrimDFdx, PrimDFdy, PrimFWidth
-                      :: (a ~ VecScalar d Float) => a -> a
-  -- Noise Functions
-  PrimNoise1          :: (a ~ VecScalar d Float) => a -> Float
-  PrimNoise2          :: (a ~ VecScalar d Float, b ~ VecScalar 2 Float) => a -> b
-  PrimNoise3          :: (a ~ VecScalar d Float, b ~ VecScalar 3 Float) => a -> b
-  PrimNoise4          :: (a ~ VecScalar d Float, b ~ VecScalar 4 Float) => a -> b
-
-{-
-    -- Vec/Mat (de)construction
-    PrimTupToV2             :: Component a                            => PrimFun stage ((a,a)     -> V2 a)
-    PrimTupToV3             :: Component a                            => PrimFun stage ((a,a,a)   -> V3 a)
-    PrimTupToV4             :: Component a                            => PrimFun stage ((a,a,a,a) -> V4 a)
-    PrimV2ToTup             :: Component a                            => PrimFun stage (V2 a     -> (a,a))
-    PrimV3ToTup             :: Component a                            => PrimFun stage (V3 a   -> (a,a,a))
-    PrimV4ToTup             :: Component a                            => PrimFun stage (V4 a -> (a,a,a,a))
--}
-
---------------------
--- * Texture support
--- FIXME: currently only Float RGBA 2D texture is supported
-
-builtincons
-  PrjImage      :: FrameBuffer 1 a -> Image 1 a
-  PrjImageColor :: FrameBuffer 1 (Depth Float, Color (Vec 4 Float)) -> Image 1 (Color (Vec 4 Float))
-
-data Texture where
-  Texture2DSlot :: String -- texture slot name
-                -> Texture
-
-  Texture2D     :: Vec 2 Int -- FIXME: use Word here
-                -> Image 1 (Color (Vec 4 Float))
-                -> Texture
-
-data Filter
-  = PointFilter
-  | LinearFilter
-
-data EdgeMode
-  = Repeat
-  | MirroredRepeat
-  | ClampToEdge
-
-data Sampler = Sampler Filter EdgeMode Texture
-
-builtincons
-  texture2D :: Sampler -> Vec 2 Float -> Vec 4 Float
-
diff --git a/prototypes/tests/accept/DepPrelude.lc b/prototypes/tests/accept/DepPrelude.lc
deleted file mode 100644
index facb4b7b..00000000
--- a/prototypes/tests/accept/DepPrelude.lc
+++ /dev/null
@@ -1,568 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE NoTypeNamespace #-}
-{-# LANGUAGE NoConstructorNamespace #-}
--- contains the lambda-pi prelude (http://www.andres-loeh.de/LambdaPi/prelude.lp) adatpted to the lc compiler prototype
-builtintycons
-    Int :: Type
-
-data Unit = TT
-
-builtins
-    cstr :: Type -> Type -> Type      -- TODO
---  cstr :: forall (a :: Type) (b :: Type) -> a -> b -> Type
---    reflCstr :: forall (a :: Type) -> cstr a a
-    coe :: forall (a :: Type) (b :: Type) -> cstr a b -> a -> b
-
-tyType (a :: Type) = a
-id a = a
-const x y = x
-const' :: forall a b . a -> b -> a
-const' x y = x
-const'' :: forall b a . a -> b -> a
-const'' x y = x
-id' a = id a
-id'' = id id
-app f x = f x
-comp f g x = f (g x)
-app2 f x y = f x y
-flip f x y = f y x
-scomb a b c = a c (b c)
-
-builtins fix :: forall a . (a -> a) -> a
-builtins f_i_x :: forall a . (a -> a) -> a
-
-data Sigma a (b :: a -> Type) = Pair (x :: a) (b x)
-
--- undefined = undefined
-builtins
-    undefined :: forall (a :: Type) . a
-
-data Empty
---data T2 a b = T2C a b
-builtins
-    T2 :: Type -> Type -> Type
-    T2C :: Unit -> Unit -> Unit
-
--- identity function, used for type annotations internally
-typeAnn = \(A :: Type) (a :: A) -> a
-
-data Bool = False | True
-
-otherwise = True
-
-if' b t f = case b of True -> t
-                      False -> f
-
--- higher-order unification test
-htest b = if' b id
-htest' b = if' b id :: (forall a . a -> a) -> _
-htest'' b = if' b id :: _ -> (forall a . a -> a)
-
-data List a = Nil' | Cons' a (List a)
-
-builtins
-    primAdd, primSub, primMod
-              :: Int -> Int -> Int
-    primSqrt  :: Int -> Int
-    primIntEq, primIntLess
-              :: Int -> Int -> Bool
-
-dcomp
-    (X :: Type)
-    (Y :: X -> Type)
-    (Z :: forall (x :: X) -> Y x -> Type)
-    (f :: forall x (y :: Y x) -> Z x y)
-    (g :: forall (x :: X) -> Y x)
-    (x :: X)
-        = f x (g x)
-dcomp'
-    @X
-    @(Y :: X -> _)
-    @(Z :: forall x -> Y x -> _)
-    (f :: forall x . forall y -> Z x y)
-    (g :: forall x -> Y x)
-    x
-        = f (g x)
-dcomp''
-    :: forall
-        X
-        (Y :: X -> _)
-        (Z :: forall x -> Y x -> _)
-    . forall
-        (f :: forall x . forall y -> Z x y)
-        (g :: forall x -> Y x) x
-    -> Z x (g x)
-dcomp'' f g x = f (g x)
-
-listMap f xs =
-    | Nil'       <- xs -> Nil'
-    | Cons' x xs <- xs -> Cons' (f x) (listMap f xs)
-foldr c n xs = case xs of
-      Nil' -> n
-      Cons' x xs -> c x (foldr c n xs)
-
-concat xs ys = foldr Cons' ys xs
-
-from n = Cons' n (from (primAdd #1 n))
-head x = case x of
-             Nil' -> undefined
-             Cons' x _ -> x
-tail    = listCase (\_ -> _) undefined (\_ xs -> xs)
-nth n xs =
-    | primIntEq #0 n -> head xs
-    | otherwise      -> nth (primSub n #1) (tail xs)
-filter p xs =
-    | Nil'       <- xs -> Nil'
-    | Cons' x xs <- xs ->
-        | p x       -> Cons' x (filter p xs)
-        | otherwise -> filter p xs
-takeWhile p xs =
-    | Nil'       <- xs -> Nil'
-    | Cons' x xs <- xs ->
-        | p x -> Cons' x (takeWhile p xs)
-        | otherwise -> Nil'
-and' a b = boolCase (\_ -> _) False b a
-or'  a b = boolCase (\_ -> _) b True a
-not'    = boolCase (\_ -> _) True False
-all p = listCase (\_ -> _) True (\x xs -> and' (p x) (all p xs))
-intLEq n m = or' (primIntLess n m) (primIntEq n m)
-{- todo
-primes =
-   Cons' #2 (Cons' #3 (filter (\x -> all (\i -> not' (primIntEq #0 (primMod x i))) (
-        takeWhile (\p -> (\m -> or' (primIntLess p m) (primIntEq p m)) (primSqrt x)) primes
-    )) (from #5)))
-
-nthPrimes n = nth n primes
-main = nthPrimes #10
--}
-data Nat = Zero | Succ Nat
-data Fin :: Nat -> Type where
-    FZero :: Fin (Succ n)
-    FSucc :: Fin n -> Fin (Succ n)
-data Vec a :: Nat -> Type where
-    Nil  :: Vec a Zero
-    Cons :: a -> Vec a n -> Vec a (Succ n)
-data Eq @a :: a -> a -> Type where
-    Refl :: Eq x x
-
-wrong
-    x = 1 1
-
-vec = Vec _
-
-builtins
-    natElim :: forall m -> m Zero -> (forall n -> m n -> m (Succ n)) -> forall b -> m b
-
---natElim (m :: Nat -> Type) (z :: m Zero) (s :: forall n -> m n -> m (Succ n)) = fix (\natElim -> natCase m z (\n -> s n (natElim n)))
-
-builtins
-    finElim ::
-      forall (m :: forall n -> Fin n -> _)
-       -> (forall n . m (Succ n) FZero)
-       -> (forall n . forall f -> m n f -> m (Succ n) (FSucc f))
-       -> forall n f -> m n f
-
--- addition of natural numbers
-plus =
-  natElim
-    (\_ -> _)           -- motive
-    (\n -> n)                    -- case for Zero
-    (\p rec n -> Succ (rec n))   -- case for Succ
-
--- predecessor, mapping 0 to 0
-pred =
-  natElim
-    (\_ -> _)
-    Zero
-    (\n' _ -> n')
-
--- a simpler elimination scheme for natural numbers
-natFold =
-    \mz ms -> natElim
-                   (\_ -> _)
-                   mz
-                   (\_ rec -> ms rec)
-
--- an eliminator for natural numbers that has special
--- cases for 0 and 1
-nat1Elim = \m m0 m1 ms -> natElim m m0
-                            (\p rec -> natElim (\n -> m (Succ n)) m1 ms p)
-
--- an eliminator for natural numbers that has special
--- cases for 0, 1 and 2
-nat2Elim = \m m0 m1 m2 ms -> nat1Elim m m0 m1
-                                (\p rec -> natElim (\n -> m (Succ (Succ n))) m2 ms p)
-
--- increment by one
-inc = natFold (Succ Zero) Succ
-
--- embed Fin into Nat
-finNat = finElim (\_ _ -> Nat)
-                     Zero
-                     (\_ rec -> Succ rec)
-
--- unit type
-Unit' = Fin 1
--- constructor
-U = FZero :: Unit'
--- eliminator
-
-unitElim = \m mu -> finElim (nat1Elim (\n -> Fin n -> Type)
-                                 (\_ -> Unit')
-                                 (\x -> m x)
-                                 (\_ _ _ -> Unit'))
-                      (\ @n -> natElim (\n -> natElim (\n -> Fin (Succ n) -> Type)
-                                                (\x -> m x)
-                                                (\_ _ _ -> Unit')
-                                                n FZero)
-                                mu
-                                (\_ _ -> U) n)
-                      (\ @n f _ -> finElim (\n f -> natElim (\n -> Fin (Succ n) -> Type)
-                                                             (\x -> m x)
-                                                             (\_ _ _ -> Unit')
-                                                             n (FSucc f))
-                                           U
-                                           (\_ _ -> U)
-                                           n f)
-                      1
-
--- empty type
-Void = Fin 0
--- eliminator
-voidElim m = finElim (natElim (\n -> Fin n -> Type)
-                            (\x -> m x)
-                            (\_ _ _ -> _))
-                   U
-                   (\_ _ -> U)
-                   0
-
--- type of booleans 
-Bool' = Fin 2 
--- constructors
-False' = FZero :: Bool'
-True'  = FSucc FZero :: Bool'
--- eliminator
-
-boolElim = \m mf mt -> finElim ( nat2Elim (\n -> Fin n -> Type)
-                                    (\_ -> Unit') (\_ -> Unit')
-                                    (\x -> m x)
-                                    (\_ _ _ -> Unit'))
-                         (\ @n -> nat1Elim (\n -> nat1Elim (\n -> Fin (Succ n) -> Type)
-                                                      (\_ -> Unit')
-                                                      (\x -> m x)
-                                                      (\_ _ _ -> Unit')
-                                                      n FZero)
-                                    U mf (\_ _ -> U) n)
-                         (\ @n f _ -> finElim (\n f -> nat1Elim (\n -> Fin (Succ n) -> Type)
-                                                                  (\_ -> Unit')
-                                                                  (\x -> m x)
-                                                                  (\_ _ _ -> Unit')
-                                                                  n (FSucc f))
-                                              (\ @n -> natElim
-                                                  (\n -> natElim
-                                                             (\n -> Fin (Succ (Succ n)) -> Type)
-                                                             (\x -> m x)
-                                                             (\_ _ _ -> Unit')
-                                                             n (FSucc FZero))
-                                                  mt (\_ _ -> U) n)
-                                              (\ @n f _ -> finElim
-                                                             (\n f -> natElim
-                                                                         (\n -> Fin (Succ (Succ n)) -> Type)
-                                                                         (\x -> m x)
-                                                                         (\_ _ _ -> Unit')
-                                                                         n (FSucc (FSucc f)))
-                                                             U
-                                                             (\_ _ -> U)
-                                                             n f)
-                                              n f)
-                         2
-
-
--- boolean not, and, or, equivalence, xor
-not = boolElim (\_ -> _) True' False'
-and = boolElim (\_ -> _) (const False') id
-or  = boolElim (\_ -> _) id (const True')
-iff = boolElim (\_ -> _) not id
-xor = boolElim (\_ -> _) id not
-
--- even, odd, isZero, isSucc
-even    = natFold True' not
-odd     = natFold False' not
-isZero  = natFold True' (const False')
-isSucc  = natFold False' (const True')
-
--- equality on natural numbers
-natEq =
-  natElim
-    (\_ -> _)
-    (natElim
-        (\_ -> _)
-        True'
-        (\n' _ -> False'))
-    (\m' rec_m' -> natElim
-                       (\_ -> _)
-                       False'
-                       (\n' _ -> rec_m' n'))
-
--- "oh so true"
-Prop = boolElim (\_ -> _) Void Unit'
-
--- reflexivity of equality on natural numbers
-pNatEqRefl =
-  natElim
-    (\n -> Prop (natEq n n))
-    U
-    (\_ rec -> rec)
- --  :: forall (n :: Nat) -> Prop (natEq n n)
-
--- alias for type-level negation 
-Not a = a -> Void
-
--- Leibniz prinicple:  forall a b . (a -> b) -> forall (x :: a) (y :: a) -> Eq x y -> Eq (f x) (f y)
-leibniz f x y = eqCase
-                 (\x y _ -> Eq (f x) (f y))
-                 Refl @x @y
-
--- symmetry of (general) equality
-symm x y = eqCase (\x y _ -> Eq y x) Refl @x @y
-
--- transitivity of (general) equality
-tran eq_x_y = eqCase
-    (\x y _ -> forall z -> Eq y z -> Eq x z)
-    (\_ x -> x)
-    eq_x_y _
-
--- apply an equality proof on two types
-apply = eqCase (\a b _ -> a -> b) id
-
-p1IsNot0 p = apply
-                (leibniz
-                         (natElim (\_ -> _) Void (\_ _ -> Unit'))
-                         1 0 p)
-                U
-
--- proof that 0 is not 1
-p0IsNot1 p = p1IsNot0 (symm 0 1 p)
-
--- proof that zero is not a successor
-p0IsNoSucc = 
-  natElim
-    (\n -> Not (Eq 0 (Succ n)))
-    p0IsNot1
-    (\n' rec_n' eq_0_SSn' ->
-      rec_n' (leibniz pred Zero (Succ (Succ n')) eq_0_SSn'))
-
--- generate a vector of given length from a specified element (replicate)
-
-replicate =
-    natElim
-      (\n -> forall a -> a -> Vec a n)
-      (\_ _ -> Nil)
-      (\n' rec_n' a x -> Cons x (rec_n' a x))
-
--- alternative definition of replicate
-replicate' =
-    natElim
-      (\n -> _ -> vec n)
-      (\_ -> Nil)
-      (\n' rec_n' x -> Cons x (rec_n' x))
-
-replicate'' x = natElim vec Nil (\n' rec_n' -> Cons x rec_n')
-
--- generate a vector of given length n, containing the natural numbers smaller than n
-fromto = natElim vec Nil (\n' rec_n' -> Cons n' rec_n')
-
-builtins
-    vecElim ::
-      forall (m :: forall k -> vec k -> _) ->
-         m Zero Nil
-         -> (forall l . forall x xs -> m l xs -> m (Succ l) (Cons x xs))
-         -> forall k xs -> m k xs
-
--- append two vectors
-append = vecElim
-             (\m _ -> forall n -> vec n -> vec (plus m n))
-             (\_ v -> v)
-             (\v vs rec n w -> Cons v (rec n w))
-
--- helper function for tail, see below
-tail' a = vecElim (\m v -> forall n -> Eq m (Succ n) -> Vec a n)
-                    (\n eq_0_SuccN -> voidElim (\_ -> _)
-                                                 (p0IsNoSucc n eq_0_SuccN))
-                    (\ @m' v vs rec_m' n eq_SuccM'_SuccN ->
-                      eqCase
-                             (\m' n e -> Vec a m' -> Vec a n)
-                             id
-                             @m' @n
-                             (leibniz pred (Succ m') (Succ n) eq_SuccM'_SuccN) vs)
-
--- compute the tail of a vector
-tailVec = \n v -> tail' _ (Succ n) v n Refl
-
--- projection out of a vector
-at =
-    vecElim (\n v -> Fin n -> _)
-                    (\f -> voidElim (\_ -> _) f)
-                    (\ @n' v vs rec_n' f_SuccN' ->
-                      finElim (\n _ -> Eq n (Succ n') -> _)
-                              (\e -> v)
-                              (\ @n f_N _ eq_SuccN_SuccN' ->
-                                rec_n' (eqCase
-                                               (\x y e -> Fin x -> Fin y)
-                                               id
-                                               @n @n'
-                                               (leibniz pred
-                                                        (Succ n) (Succ n') eq_SuccN_SuccN')
-                                               f_N))
-                              (Succ n')
-                              f_SuccN'
-                              Refl)
-
--- head of a vector
-headVec n v = at (Succ n) v FZero
-
--- vector map
-map f = vecElim (\n _ -> vec n) Nil (\x _ rec -> Cons (f x) rec)
-
--- proofs that 0 is the neutral element of addition
--- one direction is trivial by definition of plus:
-p0PlusNisN = Refl :: forall n . Eq (plus 0 n) n
-
--- the other direction requires induction on N:
-pNPlus0isN =
-  natElim (\n -> Eq (plus n 0) n)
-          Refl
-          (\n' rec -> leibniz Succ (plus n' 0) n' rec)
-
-testNoNorm = Refl :: Eq (primIntEq #3 #3) True
-
-True''  = FSucc FZero :: Bool'
-
-
-data EqD a = EqDC (a -> a -> Bool)
-
-eqInt = EqDC primIntEq
-
-builtins
-    matchInt  :: Type -> (Type -> Type) -> Type -> Type
-    matchList :: (Type -> Type) -> (Type -> Type) -> Type -> Type
-
-Eq_ :: Type -> Type
-Eq_ a = matchInt Unit (matchList Eq_ (\_ -> Empty)) a
-
-builtins eqD :: Eq_ a => EqD a
-
-eq = eqDCase (\_ -> _) id eqD
-
-eq' = eqDCase (\_ -> _) id
-
-eqList = EqDC (\as bs -> listCase (\_ -> _) (listCase (\_ -> _) True (\_ _ -> False) bs) (\a as -> listCase (\_ -> _) False (\b bs -> and' (eq a b) (eq as bs)) bs) as)
-
-main_ = eq' eqList (Cons' #3 Nil') Nil'
-main'' = eq (Cons' #3 Nil') Nil'
-
-data MonadD (m :: Type -> Type) = MonadDC (forall a . a -> m a) (forall a b . m a -> (a -> m b) -> m b)
-
-data Identity a = IdentityC a
-
-identityMonad = MonadDC IdentityC (\m f -> identityCase (\_ -> _) f m)
-
-Char = Int
-
-data IO a where
-   IORet :: a -> IO a
-   PutChar :: Char -> IO a -> IO a
-   GetChar :: (Char -> IO a) -> IO a
-
-data ReaderT r (m :: Type -> Type) a = ReaderTC (r -> m a)
-
------------------------------
-
-builtins
-    ifIdentity1 :: forall a . a -> ((Type -> Type) -> a) -> (Type -> Type) -> a
-    ifReaderT1 :: forall a . (Type -> (Type -> Type) -> a) -> ((Type -> Type) -> a) -> (Type -> Type) -> a
-
-builtins
-    Monad :: (Type -> Type) -> Type
---let Monad = fix (\Monad -> ifIdentity1 Unit (ifReaderT1 (\r m -> Monad m) (\_ -> Empty)))
-
------------------ recursive definition
-builtins monadD :: forall m . Monad m => MonadD m
--- let monadD = fix (\monadD @t -> ifIdentity_1 identityMonad (ifReaderT_1 (\r m -> monadReaderT) undefined t))
-
-return = monadDCase (\_ -> _) (\r _ -> r) monadD
-bind = monadDCase (\_ -> _) (\_ b -> b) monadD
-
-monadReaderT = MonadDC (\a -> ReaderTC (\r -> return a))
-     (\m f -> ReaderTC (\r -> 
-        readerTCase (\_ -> _)
-            (\g -> bind
-                (g r)
-                (\a -> readerTCase (\_ -> _) (\h -> h r) (f a))) 
-            m))
-  --    :: forall r m . Monad m => MonadD (ReaderT r m)
-
-IOBind ma f = case ma of
-    IORet a -> f a
-    PutChar i r -> PutChar i (bind r f)
-    GetChar g -> GetChar (\i -> bind (g i) f)
-
-monadIO = MonadDC IORet IOBind
--------------------------- end of recursive definition
-
-liftReaderT m = ReaderTC (\r -> m)
-
-bind' m m' = bind m (const m')
-fmap f m = bind m (comp return f)
-
-sequence = listCase (\_ -> _) (return Nil') (\x xs -> bind x (\vx -> fmap (Cons' vx) (sequence xs)))
-sequence_ = listCase (\_ -> _) (return TT) (\x xs -> bind' x (sequence_ xs))
-
-mapM f = comp sequence (listMap f)
-mapM_ f = comp sequence_ (listMap f)
-
-putChar i = PutChar i (return TT)
-getChar = GetChar return
-
-putStr = mapM_ putChar
-putStrLn = comp putStr (flip concat (Cons' #0 Nil'))
-
--- todo -- getLine = bind getChar (\c -> boolCase (\_ -> _) (bind getLine (\cs -> return (Cons' c cs))) (return Nil') (eq c #0))
-
---let mex_ = return' monadReaderT #3
-mex = return #3 :: IO Int
-mex' = return #3 :: ReaderT Bool IO Int
-
--- todo -- main' = bind getLine putStrLn
-
-
-data Exp :: Type -> Type where
-    EInt :: Int -> Exp Int
-    EApp :: Exp (a -> b) -> Exp a -> Exp b
-    ECond :: Exp Bool -> Exp a -> Exp a -> Exp a
-
-expCase' :: forall
-       (c :: forall a -> Exp a -> Type)
-    -> (forall d -> c Int (EInt d))
-    -> (forall f g . forall i j -> c g (EApp @f @g i j))
-    -> (forall l . forall m n o -> c l (ECond @l m n o))
-    -> forall q
-       (r :: Exp q) -> c q r
-expCase' m i a c x e = expCase m i a c @x e
-
-expCase'' :: forall
-       (c :: forall a -> Exp a -> Type)
-    -> (forall d -> c Int (EInt d))
-    -> (forall f g . forall i j -> c g (EApp @f @g i j))
-    -> (forall l . forall m n o -> c l (ECond @l m n o))
-    -> forall q
-    . forall (r :: Exp q) -> c q r
-expCase'' m i a c @x e = expCase' m i a c x e
-
--- todo -- eval  :: forall a . Exp a -> a
-eval = expCase (\b _ -> b)      -- todo: how to guess the motive
-            (\i -> i)
-            (\f a -> eval f (eval a))
-            (\b m n -> boolCase (\_ -> _) (eval n) (eval m) (eval b))
-  :: forall a . Exp a -> a
-
diff --git a/prototypes/tests/accept/Graphics.lc b/prototypes/tests/accept/Graphics.lc
deleted file mode 120000
index 974d8372..00000000
--- a/prototypes/tests/accept/Graphics.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/Graphics.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/Material.lc b/prototypes/tests/accept/Material.lc
deleted file mode 120000
index d8ac6673..00000000
--- a/prototypes/tests/accept/Material.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/Material.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/NewStyle.lc b/prototypes/tests/accept/NewStyle.lc
deleted file mode 120000
index 68032c3f..00000000
--- a/prototypes/tests/accept/NewStyle.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/NewStyle.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/Prelude.lc b/prototypes/tests/accept/Prelude.lc
deleted file mode 100644
index 35d27f0a..00000000
--- a/prototypes/tests/accept/Prelude.lc
+++ /dev/null
@@ -1,311 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-module Prelude 
-    ( module Prelude
-    , module Builtins
-    ) where
-
-import Builtins
-
-infixr 9 .
-infixl 7 `PrimMulMatVec`, `PrimDot`
-infixr 3 ***
-infixr 5 :
-infixr 0 $
---infixl 0 &
-
-const x y = x
-
-otherwise = True
-
---undefined = undefined
-
-builtins
-    undefined :: forall (a :: Type) . a
-
-x & f = f x
-
-($) = \f x -> f x
-(.) = \f g x -> f (g x)
-
-uncurry f (x, y) = f x y
-
-(***) f g (x, y) = (f x, g y)
-
-data List a = Nil | Cons a (List a)
-
-pi = 3.14
-
-zip :: [a] -> [b] -> [(a,b)]
-zip []      xs     = []
-zip xs      []     = []
-zip (a: as) (b: bs) = (a,b): zip as bs
-
-unzip :: [(a,b)] -> ([a],[b])
-unzip [] = ([],[])
-unzip ((a,b):xs) = (a:as,b:bs)
-  where (as,bs) = unzip xs
-
-filter pred []    = []
-filter pred (x:xs) = case pred x of
-                       True -> (x : filter pred xs)
-                       False -> (filter pred xs)
-
-tail :: [a] -> [a]
-tail (_: xs) = xs
-
-pairs :: [a] -> [(a, a)]
-pairs v = zip v (tail v)
-
-foldl' f e [] = e
-foldl' f e (x: xs) = foldl' f (f e x) xs
-
-singleton a = [a]
-
-append []     ys = ys
-append (x:xs) ys = x : append xs ys
-
-concat = foldl' append []
-
-map _ []     = []
-map f (x:xs) = f x : map f xs
-
-concatMap :: (a -> [b]) -> [a] -> [b]
-concatMap f x = concat (map f x)
-
-split [] = ([], [])
-split (x: xs) = (x: bs, as)  where (as, bs) = split xs
-
-mergeBy f (x:xs) (y:ys) = case f x y of
-    LT -> x: mergeBy f xs (y:ys)
-    _ -> y: mergeBy f (x:xs) ys
-mergeBy f [] xs = xs
-mergeBy f xs [] = xs
-
-sortBy f [] = []
-sortBy f [x] = [x]
-sortBy f xs = uncurry (mergeBy f) ((sortBy f *** sortBy f) (split xs))
-
-data Maybe a
-    = Nothing
-    | Just a
---    deriving (Eq, Ord, Show)
-
-
-snd (Tuple2 a b) = b
-
--- Row polymorphism
-builtins
-  Split :: Type -> Type -> Type -> Type {- TODO - LATER: Constraint -}
-
-tuptype :: List Type -> Type
-tuptype [] = 'Tuple0
-tuptype (x:xs) = 'Tuple2 x (tuptype xs)
-
-data RecordC (xs :: List (Tuple2 String Type))
-    = RecordCons (tuptype (map snd xs))
-
-builtins
-  record :: List (Tuple2 String Type) -> Type
---record xs = RecordCons ({- TODO: sortBy fst-} xs)
-
-builtins
-    project :: forall (xs :: List (Tuple2 String Type)) . forall (s :: String) -> Split (RecordC xs) (RecordC ('Cons ('Tuple2 s a) 'Nil)) b => RecordC xs -> a
-
-
---------------------------------------- HTML colors
-
-rgb r g b = V4 r g b 1.0
-
-black   = rgb 0.0 0.0 0.0
-gray    = rgb 0.5 0.5 0.5
-silver  = rgb 0.75 0.75 0.75
-white   = rgb 1.0 1.0 1.0
-maroon  = rgb 0.5 0.0 0.0
-red     = rgb 1.0 0.0 0.0
-olive   = rgb 0.5 0.5 0.0
-yellow  = rgb 1.0 1.0 0.0
-green   = rgb 0.0 0.5 0.0
-lime    = rgb 0.0 1.0 0.0
-teal    = rgb 0.0 0.5 0.5
-aqua    = rgb 0.0 1.0 1.0
-navy    = rgb 0.0 0.0 0.5
-blue    = rgb 0.0 0.0 1.0
-purple  = rgb 0.5 0.0 0.5
-fuchsia = rgb 1.0 0.0 1.0
-
-colorImage1 = ColorImage @1
-colorImage2 = ColorImage @2
-
-depthImage1 = DepthImage @1
-
-v3FToV4F :: Vec 3 Float -> Vec 4 Float
-v3FToV4F v = V4 0.0 0.0 0.0 1.0  --- todo! -- V4 v%x v%y v%z 1
-
-------------
--- * WebGL 1
-------------
-
--- angle and trigonometric
-radians = PrimRadians
-degrees = PrimDegrees
-sin = PrimSin
-cos = PrimCos
-tan = PrimTan
-asin = PrimASin
-acos = PrimACos
-atan = PrimATan
-atan2 = PrimATan2
-
--- exponential functions
-pow = PrimPow
-exp = PrimExp
-log = PrimLog
-exp2 = PrimExp2
-log2 = PrimLog2
-sqrt = PrimSqrt
-inversesqrt = PrimInvSqrt
-
--- common functions
-abs = PrimAbs
-sign = PrimSign
-floor = PrimFloor
-ceil = PrimCeil
-fract = PrimFract
-mod = PrimMod
-min = PrimMin
-max = PrimMax
-clamp = PrimClamp
-clampS = PrimClampS
-mix = PrimMix
-step = PrimStep
-smoothstep = PrimSmoothStep
-
--- geometric functions
-length = PrimLength
-distance = PrimDistance
-dot = PrimDot
-cross = PrimCross
-normalize = PrimNormalize
-faceforward = PrimFaceForward
-reflect = PrimReflect
-refract = PrimRefract
-
--- operators
-infixl 7  *, /, %
-infixl 6  +, -
-infix  4  ==, /=, <, <=, >=, >
-
-infixr 3  &&
-infixr 2  ||
-
-infix 7 `dot`   -- dot
-infix 7 `cross` -- cross
-
-infixr 7 *.     -- mulmv
-infixl 7 .*     -- mulvm
-infixl 7 .*.    -- mulmm
-
--- arithemtic
-a + b = PrimAdd a b
-a - b = PrimSub a b
-a * b = PrimMul a b
-a / b = PrimDiv a b
-a % b = PrimMod a b
-
-neg a = PrimNeg a
-
--- comparison
-a == b = PrimEqual a b
-a /= b = PrimNotEqual a b
-a < b = PrimLessThan a b
-a <= b = PrimLessThanEqual a b
-a >= b = PrimGreaterThanEqual a b
-a > b = PrimGreaterThan a b
-
--- logical
-a && b = PrimAnd a b
-a || b = PrimOr a b
-not a = PrimNot a
-any a = PrimAny a
-all a = PrimAll a
-
--- matrix functions
-a .*. b = PrimMulMatMat a b
-a *. b = PrimMulMatVec a b
-a .* b = PrimMulVecMat a b
-
-dFdx = PrimDFdx
-dFdy = PrimDFdy
-
--- extra
-round = PrimRound
-
-
--- temp hack for vector <---> scalar operators
-infixl 7  *!, /!, %!
-infixl 6  +!, -!
-
--- arithemtic
-a +! b = PrimAddS a b
-a -! b = PrimSubS a b
-a *! b = PrimMulS a b
-a /! b = PrimDivS a b
-a %! b = PrimModS a b
-
-------------------
--- common matrices
-------------------
-{-
--- | Perspective transformation matrix in row major order.
-perspective :: Float  -- ^ Near plane clipping distance (always positive).
-            -> Float  -- ^ Far plane clipping distance (always positive).
-            -> Float  -- ^ Field of view of the y axis, in radians.
-            -> Float  -- ^ Aspect ratio, i.e. screen's width\/height.
-            -> Mat 4 4 Float
-perspective n f fovy aspect = --transpose $
-    M44F (V4F (2*n/(r-l))       0       (-(r+l)/(r-l))        0)
-         (V4F     0        (2*n/(t-b))  ((t+b)/(t-b))         0)
-         (V4F     0             0       (-(f+n)/(f-n))  (-2*f*n/(f-n)))
-         (V4F     0             0            (-1)             0)
-  where
-    t = n*tan(fovy/2)
-    b = -t
-    r = aspect*t
-    l = -r
--}
-rotMatrixZ a = M44F (V4 c s 0 0) (V4 (-s) c 0 0) (V4 0 0 1 0) (V4 0 0 0 1)
-  where
-    c = cos a
-    s = sin a
-
-rotMatrixY a = M44F (V4 c 0 (-s) 0) (V4 0 1 0 0) (V4 s 0 c 0) (V4 0 0 0 1)
-  where
-    c = cos a
-    s = sin a
-
-rotMatrixX a = M44F (V4 1 0 0 0) (V4 0 c s 0) (V4 0 (-s) c 0) (V4 0 0 0 1)
-  where
-    c = cos a
-    s = sin a
-
-rotationEuler a b c = rotMatrixY a .*. rotMatrixX b .*. rotMatrixZ c
-
-{-
--- | Camera transformation matrix.
-lookat :: Vec 3 Float  -- ^ Camera position.
-       -> Vec 3 Float  -- ^ Target position.
-       -> Vec 3 Float  -- ^ Upward direction.
-       -> M44F
-lookat pos target up = translateBefore4 (neg pos) (orthogonal $ toOrthoUnsafe r)
-  where
-    w = normalize $ pos - target
-    u = normalize $ up `cross` w
-    v = w `cross` u
-    r = transpose $ Mat3 u v w
--}
-
-scale t v = v * V4 t t t 1.0
-
-fromTo :: Float -> Float -> [Float]
-fromTo a b = if a > b then [] else a:fromTo (a +! 1.0) b
-
diff --git a/prototypes/tests/accept/PrimReduce.lc b/prototypes/tests/accept/PrimReduce.lc
deleted file mode 120000
index 587d6508..00000000
--- a/prototypes/tests/accept/PrimReduce.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/PrimReduce.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/SampleMaterial.lc b/prototypes/tests/accept/SampleMaterial.lc
deleted file mode 120000
index b8627b81..00000000
--- a/prototypes/tests/accept/SampleMaterial.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/SampleMaterial.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/ambig.lc b/prototypes/tests/accept/ambig.lc
deleted file mode 120000
index 9259c4a8..00000000
--- a/prototypes/tests/accept/ambig.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/ambig.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/concatmap01.lc b/prototypes/tests/accept/concatmap01.lc
deleted file mode 120000
index 43cee1d5..00000000
--- a/prototypes/tests/accept/concatmap01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/concatmap01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/data.lc b/prototypes/tests/accept/data.lc
deleted file mode 100644
index 60731eb8..00000000
--- a/prototypes/tests/accept/data.lc
+++ /dev/null
@@ -1,18 +0,0 @@
-data Data0 = Data0
-
-data Data1 a b c = Data1 a b c
-
-data Data2 = Data21 Int
-           | Data22 { x :: Int, y::Int }
-           | Data23 { x :: Int }
-           | Data24 { }
-
-data Data5 a5 b5 c5 = Data51 { a5::a5}
-                    | Data52 { a5::a5, b5::b5, c5::c5 }
-                    | Data53 Int a5 Float b5 c5
-
-{-
-f (Data41 {}) = 5
-f (Data42 {c4=c}) = c
-f d = a4 d
--}
diff --git a/prototypes/tests/accept/dotdot01.lc b/prototypes/tests/accept/dotdot01.lc
deleted file mode 120000
index 8274c557..00000000
--- a/prototypes/tests/accept/dotdot01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/dotdot01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/dotdot02.lc b/prototypes/tests/accept/dotdot02.lc
deleted file mode 120000
index 78248be7..00000000
--- a/prototypes/tests/accept/dotdot02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/dotdot02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/empty.lc b/prototypes/tests/accept/empty.lc
deleted file mode 100644
index ae71538d..00000000
--- a/prototypes/tests/accept/empty.lc
+++ /dev/null
@@ -1,3 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-data Empty
diff --git a/prototypes/tests/accept/example06.lc b/prototypes/tests/accept/example06.lc
deleted file mode 120000
index 9a1cd6f1..00000000
--- a/prototypes/tests/accept/example06.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/example06.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/example07.lc b/prototypes/tests/accept/example07.lc
deleted file mode 120000
index 70995cd0..00000000
--- a/prototypes/tests/accept/example07.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/example07.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/example08.lc b/prototypes/tests/accept/example08.lc
deleted file mode 120000
index 206a7ce5..00000000
--- a/prototypes/tests/accept/example08.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/example08.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/fetcharrays01.lc b/prototypes/tests/accept/fetcharrays01.lc
deleted file mode 120000
index 190d5855..00000000
--- a/prototypes/tests/accept/fetcharrays01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/fetcharrays01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/fragment01.lc b/prototypes/tests/accept/fragment01.lc
deleted file mode 120000
index 9a7d18cb..00000000
--- a/prototypes/tests/accept/fragment01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/fragment01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/fragment03swizzling.lc b/prototypes/tests/accept/fragment03swizzling.lc
deleted file mode 120000
index f9b6c97e..00000000
--- a/prototypes/tests/accept/fragment03swizzling.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/fragment03swizzling.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/fragment04ifthenelse.lc b/prototypes/tests/accept/fragment04ifthenelse.lc
deleted file mode 120000
index 15510f2c..00000000
--- a/prototypes/tests/accept/fragment04ifthenelse.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/fragment04ifthenelse.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/fragment07let.lc b/prototypes/tests/accept/fragment07let.lc
deleted file mode 120000
index 42f8d268..00000000
--- a/prototypes/tests/accept/fragment07let.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/fragment07let.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/framebuffer01.lc b/prototypes/tests/accept/framebuffer01.lc
deleted file mode 120000
index f6f5b060..00000000
--- a/prototypes/tests/accept/framebuffer01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/framebuffer01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/framebuffer02.lc b/prototypes/tests/accept/framebuffer02.lc
deleted file mode 120000
index 8a5e36e8..00000000
--- a/prototypes/tests/accept/framebuffer02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/framebuffer02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/framebuffer03.lc b/prototypes/tests/accept/framebuffer03.lc
deleted file mode 120000
index ab6ddf42..00000000
--- a/prototypes/tests/accept/framebuffer03.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/framebuffer03.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/framebuffer04.lc b/prototypes/tests/accept/framebuffer04.lc
deleted file mode 120000
index ddd9144d..00000000
--- a/prototypes/tests/accept/framebuffer04.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/framebuffer04.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/framebuffer05.lc b/prototypes/tests/accept/framebuffer05.lc
deleted file mode 120000
index 99d73bbd..00000000
--- a/prototypes/tests/accept/framebuffer05.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/framebuffer05.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/fromto.lc b/prototypes/tests/accept/fromto.lc
deleted file mode 120000
index 3656552c..00000000
--- a/prototypes/tests/accept/fromto.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/fromto.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/gfx00.lc b/prototypes/tests/accept/gfx00.lc
deleted file mode 120000
index ac68f6dc..00000000
--- a/prototypes/tests/accept/gfx00.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/gfx00.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/gfx01.lc b/prototypes/tests/accept/gfx01.lc
deleted file mode 120000
index fdcd64c2..00000000
--- a/prototypes/tests/accept/gfx01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/gfx01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/gfx02.lc b/prototypes/tests/accept/gfx02.lc
deleted file mode 120000
index 7ac40c46..00000000
--- a/prototypes/tests/accept/gfx02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/gfx02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/gfx03.lc b/prototypes/tests/accept/gfx03.lc
deleted file mode 120000
index 01d05167..00000000
--- a/prototypes/tests/accept/gfx03.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/gfx03.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/gfx04.lc b/prototypes/tests/accept/gfx04.lc
deleted file mode 120000
index 8ab3d531..00000000
--- a/prototypes/tests/accept/gfx04.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/gfx04.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/gfx05.lc b/prototypes/tests/accept/gfx05.lc
deleted file mode 120000
index 8ff2c366..00000000
--- a/prototypes/tests/accept/gfx05.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/gfx05.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/heartbeat01.lc b/prototypes/tests/accept/heartbeat01.lc
deleted file mode 120000
index 4915e9e2..00000000
--- a/prototypes/tests/accept/heartbeat01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/heartbeat01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/id.lc b/prototypes/tests/accept/id.lc
deleted file mode 120000
index 033be71e..00000000
--- a/prototypes/tests/accept/id.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/id.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/ifThenElse01.lc b/prototypes/tests/accept/ifThenElse01.lc
deleted file mode 120000
index 910b04fa..00000000
--- a/prototypes/tests/accept/ifThenElse01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/ifThenElse01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/instantiate.lc b/prototypes/tests/accept/instantiate.lc
deleted file mode 120000
index 4bba908b..00000000
--- a/prototypes/tests/accept/instantiate.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/instantiate.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/let.lc b/prototypes/tests/accept/let.lc
deleted file mode 120000
index fce72e3b..00000000
--- a/prototypes/tests/accept/let.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/let.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/letIndent.lc b/prototypes/tests/accept/letIndent.lc
deleted file mode 120000
index ef9d2cc4..00000000
--- a/prototypes/tests/accept/letIndent.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/letIndent.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/line01.lc b/prototypes/tests/accept/line01.lc
deleted file mode 120000
index a7dbf6ec..00000000
--- a/prototypes/tests/accept/line01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/line01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/listcompr01.lc b/prototypes/tests/accept/listcompr01.lc
deleted file mode 120000
index 9245a221..00000000
--- a/prototypes/tests/accept/listcompr01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/listcompr01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/listcompr02.lc b/prototypes/tests/accept/listcompr02.lc
deleted file mode 120000
index 14a8e390..00000000
--- a/prototypes/tests/accept/listcompr02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/listcompr02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/listcompr03.lc b/prototypes/tests/accept/listcompr03.lc
deleted file mode 120000
index b612974c..00000000
--- a/prototypes/tests/accept/listcompr03.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/listcompr03.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/listcompr04.lc b/prototypes/tests/accept/listcompr04.lc
deleted file mode 120000
index 0bb81d2c..00000000
--- a/prototypes/tests/accept/listcompr04.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/listcompr04.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/listcompr05.lc b/prototypes/tests/accept/listcompr05.lc
deleted file mode 120000
index cd8cacd0..00000000
--- a/prototypes/tests/accept/listcompr05.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/listcompr05.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/point01.lc b/prototypes/tests/accept/point01.lc
deleted file mode 120000
index 279582fa..00000000
--- a/prototypes/tests/accept/point01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/point01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/record01.lc b/prototypes/tests/accept/record01.lc
deleted file mode 120000
index 22769059..00000000
--- a/prototypes/tests/accept/record01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/record01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/record02.lc b/prototypes/tests/accept/record02.lc
deleted file mode 120000
index b6adcf48..00000000
--- a/prototypes/tests/accept/record02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/record02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/recursivetexture02.lc b/prototypes/tests/accept/recursivetexture02.lc
deleted file mode 120000
index 97bf2b71..00000000
--- a/prototypes/tests/accept/recursivetexture02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/recursivetexture02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/reduce01.lc b/prototypes/tests/accept/reduce01.lc
deleted file mode 120000
index 4907dfa3..00000000
--- a/prototypes/tests/accept/reduce01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/reduce01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/reduce02.lc b/prototypes/tests/accept/reduce02.lc
deleted file mode 120000
index 3a26d616..00000000
--- a/prototypes/tests/accept/reduce02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/reduce02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/reduce03.lc b/prototypes/tests/accept/reduce03.lc
deleted file mode 120000
index a39bc4b3..00000000
--- a/prototypes/tests/accept/reduce03.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/reduce03.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/reduce04.lc b/prototypes/tests/accept/reduce04.lc
deleted file mode 120000
index 2d6d9cd5..00000000
--- a/prototypes/tests/accept/reduce04.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/reduce04.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/reduce05.lc b/prototypes/tests/accept/reduce05.lc
deleted file mode 120000
index 29b9a695..00000000
--- a/prototypes/tests/accept/reduce05.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/reduce05.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/reduce06.lc b/prototypes/tests/accept/reduce06.lc
deleted file mode 120000
index d8415c9c..00000000
--- a/prototypes/tests/accept/reduce06.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/reduce06.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/simple02.lc b/prototypes/tests/accept/simple02.lc
deleted file mode 120000
index 9daa3328..00000000
--- a/prototypes/tests/accept/simple02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/simple02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/simple03.lc b/prototypes/tests/accept/simple03.lc
deleted file mode 120000
index 12f5db1e..00000000
--- a/prototypes/tests/accept/simple03.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/simple03.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/swizzling.lc b/prototypes/tests/accept/swizzling.lc
deleted file mode 120000
index a36ac043..00000000
--- a/prototypes/tests/accept/swizzling.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/swizzling.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/texture01.lc b/prototypes/tests/accept/texture01.lc
deleted file mode 120000
index 69504d89..00000000
--- a/prototypes/tests/accept/texture01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/texture01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/texture02.lc b/prototypes/tests/accept/texture02.lc
deleted file mode 120000
index ec570de7..00000000
--- a/prototypes/tests/accept/texture02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/texture02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/typeclass0.lc b/prototypes/tests/accept/typeclass0.lc
deleted file mode 120000
index 87bfef05..00000000
--- a/prototypes/tests/accept/typeclass0.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/typeclass0.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/uniformparam01.lc b/prototypes/tests/accept/uniformparam01.lc
deleted file mode 120000
index 52da0bc6..00000000
--- a/prototypes/tests/accept/uniformparam01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/uniformparam01.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/uniformparam02.lc b/prototypes/tests/accept/uniformparam02.lc
deleted file mode 120000
index a4337d3a..00000000
--- a/prototypes/tests/accept/uniformparam02.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/uniformparam02.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/uniformparam03.lc b/prototypes/tests/accept/uniformparam03.lc
deleted file mode 120000
index 13143d6e..00000000
--- a/prototypes/tests/accept/uniformparam03.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/uniformparam03.lc
\ No newline at end of file
diff --git a/prototypes/tests/accept/zip01.lc b/prototypes/tests/accept/zip01.lc
deleted file mode 120000
index 8854d4fa..00000000
--- a/prototypes/tests/accept/zip01.lc
+++ /dev/null
@@ -1 +0,0 @@
-../../../tests/accept/zip01.lc
\ No newline at end of file
diff --git a/prototypes/tests/demo/.placeholder b/prototypes/tests/demo/.placeholder
deleted file mode 100644
index e69de29b..00000000
--- a/prototypes/tests/demo/.placeholder
+++ /dev/null
diff --git a/prototypes/tests/reject/.placeholder b/prototypes/tests/reject/.placeholder
deleted file mode 100644
index e69de29b..00000000
--- a/prototypes/tests/reject/.placeholder
+++ /dev/null
diff --git a/prototypes/tests/reject/data.lc b/prototypes/tests/reject/data.lc
deleted file mode 100644
index 4f609a33..00000000
--- a/prototypes/tests/reject/data.lc
+++ /dev/null
@@ -1 +0,0 @@
-data Data1 = Data1 a b c
diff --git a/prototypes/tests/reject/empty.lc b/prototypes/tests/reject/empty.lc
deleted file mode 100644
index 5349cc9b..00000000
--- a/prototypes/tests/reject/empty.lc
+++ /dev/null
@@ -1,3 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-data Empty2 =