Initial

10 files changed, 573 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..c33954f
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+dist-newstyle/
diff --git a/AST.hs b/AST.hs
new file mode 100644
index 0000000..a456b8e
--- /dev/null
+++ b/AST.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeOperators #-}
+module AST where
+
+
+data Idx env t where
+    Z :: Idx (t ': env) t
+    S :: Idx env t -> Idx (t' ': env) t
+
+data STy t where
+    TInt :: STy Int
+    TFloat :: STy Float
+
+data V s env t =
+    V (s t) (Idx env t)
+
+data Tup s t where
+    T0 :: Tup s ()
+    T1 :: s t -> Tup s t
+    T2 :: Tup s t1 -> Tup s t2 -> Tup s (t1, t2)
+
+data LHS s t env env' where
+    L0 :: Tup s t -> LHS s t env env
+    L1 :: s t -> LHS s t env (t ': env)
+    L2 :: LHS s t1 env env1 -> LHS s t2 env1 env2 -> LHS s (t1, t2) env env2
+
+data PExpr expr env t where
+    Const :: STy t -> t -> PExpr expr env t
+    Pair :: expr env t1 -> expr env t2 -> PExpr expr env (t1, t2)
+    Nil :: PExpr expr env ()
+    Prim :: Oper (t -> t') -> expr env t -> PExpr expr env t'
+    Var :: V STy env t -> PExpr expr env t
+    Let :: LHS STy t env env' -> expr env t -> expr env' t' -> PExpr expr env t'
+
+newtype Expr env t = Expr (PExpr Expr env t)
+
+data Oper t where
+    Add :: STy t -> Oper ((t, t) -> t)
+    Mul :: STy t -> Oper ((t, t) -> t)
+    Round :: Oper (Float -> Int)
+
+data PVal tenv env where  -- partial valuation
+    VZ :: PVal tenv tenv
+    VS :: PVal tenv env -> t -> PVal tenv (t ': env)
+
+type Val = PVal '[]
+
+data PTVal f tenv env where  -- partial tagged valuation
+    TVZ :: PTVal f tenv tenv
+    TVS :: PTVal f tenv env -> f t -> PTVal f tenv (t ': env)
+
+type TVal f = PTVal f '[]
+
+data NumDict t where
+    NumDict :: Num t => NumDict t
+
+data Exists f where
+    Exists :: f t -> Exists f
+
+data env :> env' =
+    Weaken { (>:>) :: forall t. Idx env t -> Idx env' t }
diff --git a/ASTfunc.hs b/ASTfunc.hs
new file mode 100644
index 0000000..59fddbb
--- /dev/null
+++ b/ASTfunc.hs
@@ -0,0 +1,148 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+module ASTfunc where
+
+import AST
+
+
+idxToInt :: Idx env t -> Int
+idxToInt Z = 0
+idxToInt (S i) = succ (idxToInt i)
+
+data LetBound s env t t' =
+    forall env'. LetBound (LHS s t env env') (Tup (V s env') t)
+
+lhsCopy :: Tup s t -> LetBound s env t t
+lhsCopy T0 = LetBound (L0 T0) T0
+lhsCopy (T1 t) = LetBound (L1 t) (T1 (V t Z))
+lhsCopy (T2 t1 t2)
+  | LetBound l1 vs1 <- lhsCopy t1
+  , LetBound l2 vs2 <- lhsCopy t2
+  = LetBound (L2 l1 l2) (T2 (fmapTup (weakenVar (weakenWithLHS l2)) vs1) vs2)
+
+lhstypeOf :: LHS s t env env' -> Tup s t
+lhstypeOf (L0 t) = t
+lhstypeOf (L1 t) = T1 t
+lhstypeOf (L2 l1 l2) = T2 (lhstypeOf l1) (lhstypeOf l2)
+
+rebuildLHS :: LHS s t env env' -> Exists (LHS s t env1)
+rebuildLHS (L0 t) = Exists (L0 t)
+rebuildLHS (L1 t) = Exists (L1 t)
+rebuildLHS (L2 l1 l2)
+  | Exists l1' <- rebuildLHS l1
+  , Exists l2' <- rebuildLHS l2
+  = Exists (L2 l1' l2')
+
+fmapTup :: (forall t'. s t' -> s' t') -> Tup s t -> Tup s' t
+fmapTup _ T0 = T0
+fmapTup f (T1 x) = T1 (f x)
+fmapTup f (T2 t1 t2) = T2 (fmapTup f t1) (fmapTup f t2)
+
+prj :: PVal tenv env -> Idx env t -> Maybe t
+prj VZ _ = Nothing
+prj (VS _ x) Z = Just x
+prj (VS v _) (S i) = prj v i
+
+prjV :: Val env -> Idx env t -> t
+prjV v Z = case v of VS _ x -> x
+prjV v (S i) = case v of VS v' _ -> prjV v' i
+
+vpush :: LHS s t env env' -> t -> Val env -> Val env'
+vpush (L0 _) _ v = v
+vpush (L1 _) x v = VS v x
+vpush (L2 l1 l2) (x, y) v = vpush l2 y (vpush l1 x v)
+
+reifyNum :: STy t -> NumDict t
+reifyNum TInt = NumDict
+reifyNum TFloat = NumDict
+
+(>.) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
+Weaken f >. Weaken g = Weaken (f . g)
+
+weakenId :: env :> env
+weakenId = Weaken id
+
+weakenSucc :: env :> (t ': env)
+weakenSucc = Weaken S
+
+weakenSucc' :: (t ': env) :> env
+weakenSucc' = Weaken (\case S i -> i
+                            Z -> error "weakenSucc': reference to skipped item")
+
+weakenWithLHS :: LHS s t env env' -> env :> env'
+weakenWithLHS (L0 _) = Weaken id
+weakenWithLHS (L1 _) = Weaken S
+weakenWithLHS (L2 l1 l2) = weakenWithLHS l2 >. weakenWithLHS l1
+
+weakenSkip :: LHS s t env env' -> env :> env2 -> env' :> env2
+weakenSkip (L0 _) = id
+weakenSkip (L1 _) = (>. weakenSucc')
+weakenSkip (L2 l1 l2) = weakenSkip l2 . weakenSkip l1
+
+weakenVar :: env :> env' -> V s env t -> V s env' t
+weakenVar w (V t i) = V t (w >:> i)
+
+weakenExpr :: env :> env' -> Expr env t -> Expr env' t
+weakenExpr w (Expr e) = Expr (weakenPExpr weakenExpr w e)
+
+weakenPExpr :: (forall env1 env1' t'. env1 :> env1' -> expr env1 t' -> expr env1' t')
+            -> env :> env' -> PExpr expr env t -> PExpr expr env' t
+weakenPExpr _ _ (Const t x) = Const t x
+weakenPExpr f w (Pair e1 e2) = Pair (f w e1) (f w e2)
+weakenPExpr _ _ Nil = Nil
+weakenPExpr f w (Prim op e) = Prim op (f w e)
+weakenPExpr _ w (Var var) = Var (weakenVar w var)
+weakenPExpr f w (Let lhs rhs e)
+  | Exists lhs' <- rebuildLHS lhs
+  = Let lhs' (f w rhs) (f (sinkWithLHS lhs lhs' w) e)
+
+sinkWithLHS :: LHS s t env1 env1' -> LHS s t env2 env2' -> env1 :> env2 -> env1' :> env2'
+sinkWithLHS (L0 _) (L0 _) w = w
+sinkWithLHS (L1 _) (L1 _) w = Weaken (\case Z -> Z ; S i -> S (w >:> i))
+sinkWithLHS (L2 l1 l2) (L2 l1' l2') w = sinkWithLHS l2 l2' (sinkWithLHS l1 l1' w)
+sinkWithLHS _ _ _ = error "sinkWithLHS: unequal LHSs"
+
+untupleE :: Tup (Expr env) t -> Expr env t
+untupleE = untupleE' Expr
+
+untupleE' :: (forall t'. PExpr expr env t' -> expr env t')
+          -> Tup (expr env) t -> expr env t
+untupleE' f T0 = f Nil
+untupleE' _ (T1 e) = e
+untupleE' f (T2 t1 t2) = f (Pair (untupleE' f t1) (untupleE' f t2))
+
+evars :: Tup (V STy env) t -> Expr env t
+evars = evars' Expr
+
+evars' :: (forall env' t'. PExpr expr env' t' -> expr env' t')
+       -> Tup (V STy env) t -> expr env t
+evars' f = untupleE' f . fmapTup (f . Var)
+
+etypeOf :: Expr env t -> Tup STy t
+etypeOf (Expr e) = eptypeOf etypeOf e
+
+eptypeOf :: (forall env' t'. expr env' t' -> Tup STy t')
+         -> PExpr expr env t -> Tup STy t
+eptypeOf _ (Const t _) = T1 t
+eptypeOf f (Pair e1 e2) = T2 (f e1) (f e2)
+eptypeOf _ Nil = T0
+eptypeOf _ (Prim op _) = T1 (opertypeOf op)
+eptypeOf _ (Var (V t _)) = T1 t
+eptypeOf f (Let _ _ e) = f e
+
+opertypeOf :: Oper (t -> t') -> STy t'
+opertypeOf (Add t) = t
+opertypeOf (Mul t) = t
+opertypeOf Round = TInt
+
+eInto :: (forall env' t'. expr env' t' -> expr' env' t')
+      -> PExpr expr env t -> PExpr expr' env t
+eInto _ (Const t x) = Const t x
+eInto f (Pair e1 e2) = Pair (f e1) (f e2)
+eInto _ Nil = Nil
+eInto f (Prim op e) = Prim op (f e)
+eInto _ (Var v) = Var v
+eInto f (Let lhs rhs e) = Let lhs (f rhs) (f e)
diff --git a/Eval.hs b/Eval.hs
new file mode 100644
index 0000000..af2cd3c
--- /dev/null
+++ b/Eval.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module Eval where
+
+import AST
+import ASTfunc
+
+
+eval :: Expr '[] t -> t
+eval = eval'Expr VZ
+
+eval'Expr :: Val env -> Expr env t -> t
+eval'Expr v (Expr e) = eval' eval'Expr v e
+
+eval' :: (forall env' t'. Val env' -> expr env' t' -> t')
+      -> Val env -> PExpr expr env t -> t
+eval' _ _ (Const _ x) = x
+eval' f v (Pair x y) = (f v x, f v y)
+eval' _ _ Nil = ()
+eval' f v (Prim op x) = applyOper op (f v x)
+eval' _ v (Var (V _ i)) = prjV v i
+eval' f v (Let lhs rhs e) = f (vpush lhs (f v rhs) v) e
+
+applyOper :: Oper (t -> t') -> t -> t'
+applyOper (Add t) (x, y) | NumDict <- reifyNum t = x + y
+applyOper (Mul t) (x, y) | NumDict <- reifyNum t = x * y
+applyOper Round x = round x
diff --git a/Language.hs b/Language.hs
new file mode 100644
index 0000000..7251161
--- /dev/null
+++ b/Language.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+module Language where
+
+import AST
+import ASTfunc
+
+
+class    IsSTy t     where magicSTy :: STy t
+instance IsSTy Int   where magicSTy = TInt
+instance IsSTy Float where magicSTy = TFloat
+
+class    IsTupTy t     where magicTupTy :: Tup STy t
+-- Need to list all the scalar types to avoid overlapping instances
+instance IsTupTy Int   where magicTupTy = T1 TInt
+instance IsTupTy Float where magicTupTy = T1 TFloat
+instance IsTupTy ()    where magicTupTy = T0
+instance (IsTupTy t1, IsTupTy t2) => IsTupTy (t1, t2) where
+    magicTupTy = T2 magicTupTy magicTupTy
+
+con :: IsSTy t => t -> Expr env t
+con = Expr . Const magicSTy
+
+pair :: Expr env t1 -> Expr env t2 -> Expr env (t1, t2)
+pair = (Expr .) . Pair
+
+nil :: Expr env ()
+nil = Expr Nil
+
+add :: IsSTy t => Expr env t -> Expr env t -> Expr env t
+add = ((Expr . Prim (Add magicSTy) . Expr) .) . Pair
+
+mul :: IsSTy t => Expr env t -> Expr env t -> Expr env t
+mul = ((Expr . Prim (Mul magicSTy) . Expr) .) . Pair
+
+let_ :: IsTupTy t
+     => Expr env t
+     -> (forall env'. (forall t2. Expr env t2 -> Expr env' t2)
+                   -> Expr env' t -> Expr env' t')
+     -> Expr env t'
+let_ rhs f
+  | LetBound lhs vs <- lhsCopy magicTupTy
+  = Expr (Let lhs rhs (f (weakenExpr (weakenWithLHS lhs)) (evars vs)))
+
+fst_ :: Expr env (t, t') -> Expr env t
+fst_ (Expr (Pair e1 _)) = e1
+fst_ _ = error "fst_: explicit let-binding necessary"
+
+snd_ :: Expr env (t, t') -> Expr env t'
+snd_ (Expr (Pair _ e2)) = e2
+snd_ _ = error "snd_: explicit let-binding necessary"
diff --git a/Main.hs b/Main.hs
new file mode 100644
index 0000000..e5aa512
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,22 @@
+module Main where
+
+import Eval (eval)
+import Language
+import Show (showExpr)
+import Simplify (simplify)
+
+
+main :: IO ()
+main = do
+    print . eval $
+        let_ (add (con (2 :: Int)) (con 3)) $ \_ x ->
+            mul x x
+
+    let prog =
+            let_ (add (con (2 :: Int)) (con 3)) $ \_ x ->
+            let_ (mul (con (4 :: Int)) (con 5)) $ \wy y ->
+            let_ (pair (wy x) y) $ \wt t ->
+                add (mul (wt (wy x)) (snd_ t)) (mul (wt y) (fst_ t))
+    putStrLn (showExpr prog)
+    putStrLn (showExpr (simplify prog))
+    print (eval prog)
diff --git a/MonMap.hs b/MonMap.hs
new file mode 100644
index 0000000..dd70ec3
--- /dev/null
+++ b/MonMap.hs
@@ -0,0 +1,22 @@
+module MonMap where
+
+import qualified Data.Map.Strict as Map
+
+
+newtype MonMap k v = MonMap (Map.Map k v)
+  deriving (Show)
+
+instance Functor (MonMap k) where
+    fmap f (MonMap m) = MonMap (fmap f m)
+
+instance (Ord k, Semigroup v) => Semigroup (MonMap k v) where
+    MonMap m1 <> MonMap m2 = MonMap (Map.unionWith (<>) m1 m2)
+
+instance (Ord k, Monoid v) => Monoid (MonMap k v) where
+    mempty = MonMap mempty
+
+singleton :: k -> v -> MonMap k v
+singleton = (MonMap .) . Map.singleton
+
+lookup :: Ord k => k -> MonMap k v -> Maybe v
+lookup k (MonMap m) = Map.lookup k m
diff --git a/Show.hs b/Show.hs
new file mode 100644
index 0000000..42d3b2b
--- /dev/null
+++ b/Show.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module Show where
+
+import Control.Monad.State.Strict
+
+import AST
+import ASTfunc
+
+
+showExpr :: Expr env t -> String
+showExpr e = showsExpr e ""
+
+showsExpr :: Expr env t -> ShowS
+showsExpr e = evalState (showsExpr' 0 [] e) 1
+
+showsExpr' :: Int -> [String] -> Expr env t -> State Int ShowS
+showsExpr' d env (Expr e) =
+    showsPExpr' showsExpr' (\case Expr (Pair a b) -> Just (a, b) ; _ -> Nothing) etypeOf d env e
+
+showsPExpr' :: (forall env' t'. Int -> [String] -> expr env' t' -> State Int ShowS)
+            -> (forall env' t1 t2. expr env' (t1, t2) -> Maybe (expr env' t1, expr env' t2))
+            -> (forall env' t'. expr env' t' -> Tup STy t')
+            -> Int -> [String] -> PExpr expr env t -> State Int ShowS
+showsPExpr' _ _ _ _ _ (Const t x) = return (showsScalar t x)
+showsPExpr' f _ _ _ env (Pair e1 e2) = do
+    s1 <- f 0 env e1
+    s2 <- f 0 env e2
+    return (showParen True (s1 . showString ", " . s2))
+showsPExpr' _ _ _ _ _ Nil = return (showString "()")
+showsPExpr' f pf tf d env (Prim op e) = case (showOper op, tf e) of
+    (Infix opd s, T2 _ _) | Just (e1, e2) <- pf e -> do
+        s1 <- f (opd + 1) env e1
+        s2 <- f (opd + 1) env e2
+        return (showParen (d > opd) (s1 . showString (" " ++ s ++ " ") . s2))
+    (Infix _ s, _) -> do
+        s1 <- f 11 env e
+        return (showParen (d > 10) (showString (s ++ " ") . s1))
+    (PrefixFun s, _) -> do
+        s1 <- f 11 env e
+        return (showParen (d > 10) (showString (s ++ " ") . s1))
+showsPExpr' _ _ _ _ env (Var (V _ i)) =
+    case drop (idxToInt i) env of
+      s:_ -> return (showString s)
+      [] -> return (showString ("tUP" ++ show (idxToInt i - length env + 1)))
+showsPExpr' f _ _ d env (Let lhs rhs e) = do
+    (lhss, envf) <- nameifyLHS lhs
+    s1 <- f 0 env rhs
+    s2 <- f 0 (envf env) e
+    return (showParen (d > 0) (showString ("let " ++ lhss ++ " = ") . s1 . showString " in " . s2))
+
+nameifyLHS :: LHS s t env env' -> State Int (String, [String] -> [String])
+nameifyLHS (L0 _) = return ("_", id)
+nameifyLHS (L1 _) = do
+    seed <- get
+    put (seed + 1)
+    let name = 't' : show seed
+    return (name, (name :))
+nameifyLHS (L2 l1 l2) = do
+    (s1, f1) <- nameifyLHS l1
+    (s2, f2) <- nameifyLHS l2
+    return ("(" ++ s1 ++ "," ++ s2 ++ ")", f2 . f1)
+
+data ShownOper t = Infix Int String | PrefixFun String
+
+showOper :: Oper (t -> t') -> ShownOper t
+showOper (Add _) = Infix 4 "+"
+showOper (Mul _) = Infix 5 "*"
+showOper Round = PrefixFun "round"
+
+showsScalar :: STy t -> t -> ShowS
+showsScalar TInt = shows
+showsScalar TFloat = shows
diff --git a/Simplify.hs b/Simplify.hs
new file mode 100644
index 0000000..7435464
--- /dev/null
+++ b/Simplify.hs
@@ -0,0 +1,143 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+module Simplify where
+
+import Data.Monoid (Sum(..))
+
+import AST
+import ASTfunc
+import MonMap (MonMap)
+import qualified MonMap
+
+
+simplify :: Expr env t -> Expr env t
+simplify e = unSExpr (slr' . sli' . slr' $ toSExpr e)
+
+slr' :: SExpr env t -> SExpr env t
+slr' e = slr weakenId e
+
+-- simplify using let-rotate, and work away Unused bindings
+slr :: env :> env' -> SExpr env t -> SExpr env' t
+slr w (Auto expr) = case expr of
+    -- unused binding
+    Let lhs Unused e -> slr (weakenSkip lhs w) e
+
+    -- let-rotate
+    Let lhs (Auto (Let lhs2 rhs2 e2)) e
+      | Exists lhs' <- rebuildLHS lhs
+      -> let sh = sinkWithLHS lhs lhs' (weakenWithLHS lhs2)
+         in slr w (In (Let lhs2 rhs2 (In (Let lhs' e2 (applyShift sh e)))))
+
+    -- let-split
+    Let (L2 l1 l2) (Auto (Pair e1 e2)) e ->
+        slr w (In (Let l1 e1 (In (Let l2 (applyShift (weakenWithLHS l1) e2) e))))
+
+    -- redundant wildcard binding
+    Let (L0 _) _ e -> slr w e
+
+    Const t x -> In (Const t x)
+    Pair e1 e2 -> In (Pair (slr w e1) (slr w e2))
+    Nil -> In Nil
+    Prim op e -> In (Prim op (slr w e))
+    Var (V t i) -> In (Var (V t (w >:> i)))
+    Let lhs rhs e
+      | Exists lhs' <- rebuildLHS lhs
+      -> In (Let lhs' (slr w rhs) (slr (sinkWithLHS lhs lhs' w) e))
+slr _ Unused = error "slr: unused found outside Let RHS"
+
+-- simplify using linear inlining
+sli' :: SExpr env t -> SExpr env t
+sli' expr =
+    let (countmp, expr') = count 0 expr
+        countmp' = ((<= 1) . getSum) <$> countmp
+    in inline countmp' 0 (Inliner (In . Var)) expr'
+
+count :: Int -> SExpr env t -> (MonMap Int (Sum Int), SExpr env t)
+count d (Auto expr) = In <$> case expr of
+    Const t x -> return (Const t x)
+    Pair e1 e2 -> Pair <$> count d e1 <*> count d e2
+    Nil -> return Nil
+    Prim op e -> Prim op <$> count d e
+    Var (V t i) -> (MonMap.singleton (d - 1 - idxToInt i) 1, Var (V t i))
+    Let lhs rhs e -> Let lhs <$> count d rhs <*> count (d + lhsSize lhs) e
+count _ Unused = return Unused
+
+lhsSize :: LHS s t env env' -> Int
+lhsSize (L0 _) = 0
+lhsSize (L1 _) = 0
+lhsSize (L2 l1 l2) = lhsSize l1 + lhsSize l2
+
+data Inliner env = Inliner { unInliner :: forall t. V STy env t -> SExpr env t }
+
+inline :: MonMap Int Bool -> Int -> Inliner env -> SExpr env t -> SExpr env t
+inline countmp = go
+  where
+    go :: Int -> Inliner env -> SExpr env t -> SExpr env t
+    go d il (Auto expr) = case expr of
+        Const t x -> In (Const t x)
+        Pair e1 e2 -> In (Pair (go d il e1) (go d il e2))
+        Nil -> In Nil
+        Prim op e -> In (Prim op (go d il e))
+        Var v -> unInliner il v
+        Let (L1 t) rhs e
+          | Just True <- MonMap.lookup d countmp ->
+              let il' = Inliner
+                      (\case V _ Z -> applyShift weakenSucc rhs
+                             V t' (S i) -> applyShift weakenSucc (unInliner il (V t' i)))
+              in In (Let (L1 t) Unused (go (d + 1) il' e))
+        Let lhs rhs e ->
+            In (Let lhs (go d il rhs)
+                    (go (d + lhsSize lhs) (weakenILwithLHS lhs il) e))
+    go _ _ Unused = Unused
+
+weakenILwithLHS :: LHS STy t env env' -> Inliner env -> Inliner env'
+weakenILwithLHS (L0 _) il = il
+weakenILwithLHS (L1 _) il =
+    Inliner (\case v@(V _ Z) -> In (Var v)
+                   V t (S i) -> applyShift weakenSucc (unInliner il (V t i)))
+weakenILwithLHS (L2 l1 l2) il = weakenILwithLHS l2 (weakenILwithLHS l1 il)
+
+
+data SExpr env t where
+    Shift :: env :> env' -> PExpr SExpr env t -> SExpr env' t
+    In :: PExpr SExpr env t -> SExpr env t
+    Unused :: SExpr env t
+
+toSExpr :: Expr env t -> SExpr env t
+toSExpr (Expr e) = In (eInto toSExpr e)
+
+unSExpr :: SExpr env t -> Expr env t
+unSExpr (In e) = Expr (eInto unSExpr e)
+unSExpr (Shift w e) = Expr (shiftTraverse (eInto unSExpr) w e)
+unSExpr Unused = error "unSExpr: unused found"
+
+applyShift :: env :> env' -> SExpr env t -> SExpr env' t
+applyShift w (In e) = Shift w e
+applyShift w (Shift w' e) = Shift (w >. w') e
+applyShift _ Unused = Unused
+
+pattern Auto :: PExpr SExpr env t -> SExpr env t
+pattern Auto se <- (matchAuto -> Just se)
+{-# COMPLETE Auto, Unused #-}
+
+matchAuto :: SExpr env t -> Maybe (PExpr SExpr env t)
+matchAuto (In e) = Just e
+matchAuto (Shift w e) = Just (shiftTraverse id w e)
+matchAuto Unused = Nothing
+
+shiftTraverse :: (forall env' t'. PExpr SExpr env' t' -> PExpr expr env' t')
+              -> env :> env1 -> PExpr SExpr env t -> PExpr expr env1 t
+shiftTraverse f w e = case e of
+    Const t x -> Const t x
+    Pair e1 e2 -> f (Pair (applyShift w e1) (applyShift w e2))
+    Nil -> Nil
+    Prim op e1 -> f (Prim op (applyShift w e1))
+    Var v -> Var (weakenVar w v)
+    Let lhs rhs e1
+      | Exists lhs' <- rebuildLHS lhs
+      -> f (Let lhs' (applyShift w rhs)
+                     (applyShift (sinkWithLHS lhs lhs' w) e1))
diff --git a/first-order-exprs.cabal b/first-order-exprs.cabal
new file mode 100644
index 0000000..6144d2f
--- /dev/null
+++ b/first-order-exprs.cabal
@@ -0,0 +1,18 @@
+cabal-version:       >=1.10
+name:                first-order-exprs
+synopsis:            First order expressions with simplifier
+version:             0.1.0.0
+license:             MIT
+author:              Tom Smeding
+maintainer:          tom@tomsmeding.com
+build-type:          Simple
+
+executable exprs
+  main-is:             Main.hs
+  other-modules:       AST, ASTfunc, Eval, Language, MonMap, Show, Simplify
+  build-depends:       base >= 4.13 && < 4.15,
+                       containers >= 0.6.3.1 && < 0.7,
+                       mtl
+  hs-source-dirs:      .
+  default-language:    Haskell2010
+  ghc-options:         -Wall -O2 -threaded