diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | AST.hs | 65 | ||||
| -rw-r--r-- | ASTfunc.hs | 148 | ||||
| -rw-r--r-- | Eval.hs | 28 | ||||
| -rw-r--r-- | Language.hs | 52 | ||||
| -rw-r--r-- | Main.hs | 22 | ||||
| -rw-r--r-- | MonMap.hs | 22 | ||||
| -rw-r--r-- | Show.hs | 74 | ||||
| -rw-r--r-- | Simplify.hs | 143 | ||||
| -rw-r--r-- | first-order-exprs.cabal | 18 |
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/ @@ -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) @@ -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" @@ -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 @@ -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 |