From 5d1d3b4f251bf938648d7d21c6641a1a0cc0768b Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom.smeding@gmail.com>
Date: Sat, 26 Dec 2020 18:08:15 +0100
Subject: Initial

---
 .gitignore              |   1 +
 AST.hs                  |  65 +++++++++++++++++++++
 ASTfunc.hs              | 148 ++++++++++++++++++++++++++++++++++++++++++++++++
 Eval.hs                 |  28 +++++++++
 Language.hs             |  52 +++++++++++++++++
 Main.hs                 |  22 +++++++
 MonMap.hs               |  22 +++++++
 Show.hs                 |  74 ++++++++++++++++++++++++
 Simplify.hs             | 143 ++++++++++++++++++++++++++++++++++++++++++++++
 first-order-exprs.cabal |  18 ++++++
 10 files changed, 573 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 AST.hs
 create mode 100644 ASTfunc.hs
 create mode 100644 Eval.hs
 create mode 100644 Language.hs
 create mode 100644 Main.hs
 create mode 100644 MonMap.hs
 create mode 100644 Show.hs
 create mode 100644 Simplify.hs
 create mode 100644 first-order-exprs.cabal

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
-- 
cgit v1.2.3-70-g09d2