From a231326eca52b676b448bd97c0aacb1128eaf9d3 Mon Sep 17 00:00:00 2001 From: Dougal Date: Mon, 2 Dec 2024 16:41:52 -0800 Subject: [PATCH] More SimpIR --- src/lib/Builder.hs | 180 ++++++++++++++++++------------------ src/lib/Name.hs | 151 +++++++++++------------------- src/lib/QueryTypePure.hs | 21 ++--- src/lib/Simplify.hs | 24 +++-- src/lib/Types/Primitives.hs | 2 +- src/lib/Types/Simple.hs | 9 +- 6 files changed, 174 insertions(+), 213 deletions(-) diff --git a/src/lib/Builder.hs b/src/lib/Builder.hs index b59ef39ab..70db80281 100644 --- a/src/lib/Builder.hs +++ b/src/lib/Builder.hs @@ -29,23 +29,9 @@ import PPrint import QueryTypePure import Util (enumerate, transitiveClosureM, bindM2, toSnocList, popList) import Types.Simple +import Types.Primitives --- -- temporary stub --- peepholeExpr :: a -> a --- peepholeExpr = id - --- -- === ToExpr === - --- class ToExpr (e::E) where --- toExpr :: e n -> Expr n - --- instance ToExpr (Expr ) where toExpr = id --- instance ToExpr (Atom ) where toExpr = Atom --- instance ToExpr (Con ) where toExpr = Atom . Con --- instance ToExpr (AtomVar ) where toExpr = toExpr . toAtom --- instance ToExpr (TypedHof) where toExpr = Hof - --- === Ordinary (local) builder class === +-- === builder class === class Fallible1 m => Builder (m::MonadKind1) where rawEmitDecl :: Emits n => NameHint -> Expr n -> m n (Name n) @@ -54,32 +40,43 @@ class Builder m => ScopableBuilder (m::MonadKind1) where buildScopedAndThen :: SinkableE e => (forall l. (Emits l, DExt n l) => m l (e l)) - -> (forall l. DExt n l => Nest Decl n l -> e l -> m l a) + -> (forall l. DExt n l => RNest Decl n l -> e l -> m l a) -> m n a -buildScoped - :: (ScopableBuilder m, SinkableE e) - => (forall l. (Emits l, DExt n l) => m l (e l)) - -> m n (Abs (Nest Decl) e n) -buildScoped cont = buildScopedAndThen cont \decls body -> return $ Abs decls body - - type Builder2 (m :: MonadKind2) = forall i. Builder (m i) type ScopableBuilder2 (m :: MonadKind2) = forall i. ScopableBuilder (m i) --- emitDecl :: (Builder m, Emits n) => NameHint -> LetAnn -> Expr n -> m n (AtomVar n) --- emitDecl _ _ (Atom (Stuck _ (Var n))) = return n --- emitDecl hint ann expr = rawEmitDecl hint ann expr --- {-# INLINE emitDecl #-} +emitDecl :: (Builder m, Emits n) => NameHint -> Expr n -> m n (Name n) +emitDecl hint expr = rawEmitDecl hint expr +{-# INLINE emitDecl #-} --- emit :: (Builder m, ToExpr e, Emits n) => e n -> m n (Atom n) --- emit e = case toExpr e of --- Atom x -> return x --- Block _ block -> emitDecls block >>= emit --- expr -> do --- v <- emitDecl noHint PlainLet $ peepholeExpr expr --- return $ toAtom v --- {-# INLINE emit #-} +emit :: (Builder m, Emits n) => Expr n -> m n (Atom n) +emit e = case e of + Block _ block -> emitDecls block >>= emit + expr -> do + v <- emitDecl noHint expr + return $ Var v (getType expr) +{-# INLINE emit #-} + +idExpr :: Atom n -> Expr n +idExpr x = PrimOp (getType x) (UnOp Identity x) + +declsToExpr :: RNest Decl n l -> Atom l -> Expr n +declsToExpr (RNest ds (Let b e)) (Var v _) | v == binderName b = maybeBlock ds e +declsToExpr ds x = maybeBlock ds (idExpr x) + +maybeBlock :: RNest Decl n l -> Expr l -> Expr n +maybeBlock REmpty expr = expr +maybeBlock rdecls expr = Block ty $ Abs decls expr + where ty = hoistType decls (getType expr) + decls = unRNest rdecls + +-- TODO: if hoisting fails, push the decls into the data parts of the type +hoistType :: Nest Decl n l -> Type l -> Type n +hoistType decls ty = ignoreHoistFailure $ hoist decls ty + +-- if final decl matches var then +-- if there's only one de -- emitUnOp :: (Builder m, Emits n) => UnOp -> Atom n -> m n (Atom n) -- emitUnOp op x = emit $ PrimOp resultTy $ UnOp op x @@ -99,8 +96,10 @@ type ScopableBuilder2 (m :: MonadKind2) = forall i. ScopableBuilder (m i) -- atom -> emitDecl noHint PlainLet (toExpr atom) -- {-# INLINE emitToVar #-} --- emitDecls :: (Builder m, Emits n, RenameE e, SinkableE e) --- => WithDecls e n -> m n (e n) +emitDecls :: (Builder m, Emits n, RenameE e, SinkableE e) + => Abs Decls e n -> m n (e n) +emitDecls (Abs decls result) = undefined +-- runSubstReaderT idSubst $ go decls result where -- emitDecls (Abs decls result) = runSubstReaderT idSubst $ go decls result where -- go :: (Builder m, Emits o, RenameE e, SinkableE e) -- => Nest Decl i i' -> e i' -> SubstReaderT Name m i o (e o) @@ -125,7 +124,7 @@ type ScopableBuilder2 (m :: MonadKind2) = forall i. ScopableBuilder (m i) type BuilderEmissions = RNest Decl newtype BuilderT (m::MonadKind) (n::S) (a:: *) = - BuilderT { runBuilderT' :: InplaceT Scope BuilderEmissions m n a } + BuilderT { runBuilderT' :: InplaceT BuilderEmissions m n a } deriving ( Functor, Applicative, Monad, MonadTrans1, MonadFail, Fallible , Catchable, ScopeReader, Alternative , MonadWriter w, MonadReader r') @@ -145,7 +144,7 @@ instance (MonadState s m) => MonadState s (BuilderT m n) where liftBuilderT :: (Fallible m, ScopeReader m') => BuilderT m n a -> m' n (m a) liftBuilderT cont = do - env <- unsafeGetEnv + env <- unsafeGetScope Distinct <- getDistinct return do (REmpty, result) <- runInplaceT env $ runBuilderT' cont @@ -156,43 +155,44 @@ liftBuilder :: (ScopeReader m) => BuilderM n a -> m n a liftBuilder cont = liftM runHardFail $ liftBuilderT cont {-# INLINE liftBuilder #-} --- TODO: This should not fabricate Emits evidence!! --- XXX: this uses unsafe functions in its implementations. It should be safe to --- use, but be careful changing it. -liftEmitBuilder :: (Builder m, SinkableE e, RenameE e) - => BuilderM n (e n) -> m n (e n) -liftEmitBuilder cont = do - env <- unsafeGetEnv - Distinct <- getDistinct - let (result, decls, _) = runHardFail $ unsafeRunInplaceT (runBuilderT' cont) env emptyOutFrag - Emits <- fabricateEmitsEvidenceM - emitDecls $ Abs (unsafeCoerceB $ unRNest decls) result - --- instance (Fallible m) => ScopableBuilder (BuilderT m) where --- buildScopedAndThen cont1 cont2 = BuilderT $ locallyMutableInplaceT --- (runBuilderT' do --- Emits <- fabricateEmitsEvidenceM --- cont1 ) --- (\rdecls e -> runBuilderT' $ cont2 (unRNest rdecls) e) --- {-# INLINE buildScopedAndThen #-} - --- newtype BuilderDeclEmission (n::S) (l::S) = BuilderDeclEmission (Decl n l) --- instance ExtOutMap Env BuilderDeclEmission where --- extendOutMap env (BuilderDeclEmission d) = env `extendOutMap` toEnvFrag d --- {-# INLINE extendOutMap #-} --- instance ExtOutFrag BuilderEmissions BuilderDeclEmission where --- extendOutFrag rn (BuilderDeclEmission d) = RNest rn d --- {-# INLINE extendOutFrag #-} - --- instance Fallible m => Builder (BuilderT m) where --- rawEmitDecl hint ann expr = do --- ty <- return $ getType expr --- v <- BuilderT $ freshExtendSubInplaceT hint \b -> --- (BuilderDeclEmission $ Let b $ DeclBinding ann expr, binderName b) --- -- -- Debugging snippet --- -- traceM $ pprint v ++ " = " ++ pprint expr --- return $ AtomVar v ty --- {-# INLINE rawEmitDecl #-} +-- -- TODO: This should not fabricate Emits evidence!! +-- -- XXX: this uses unsafe functions in its implementations. It should be safe to +-- -- use, but be careful changing it. +-- liftEmitBuilder :: (Builder m, SinkableE e, RenameE e) +-- => BuilderM n (e n) -> m n (e n) +-- liftEmitBuilder cont = do +-- env <- unsafeGetScope +-- Distinct <- getDistinct +-- let (result, decls, _) = runHardFail $ unsafeRunInplaceT (runBuilderT' cont) env emptyOutFrag +-- Emits <- fabricateEmitsEvidenceM +-- emitDecls $ Abs (unsafeCoerceB $ unRNest decls) result + +instance (Fallible m) => ScopableBuilder (BuilderT m) where + buildScopedAndThen cont1 cont2 = BuilderT $ locallyMutableInplaceT + (runBuilderT' do + Emits <- fabricateEmitsEvidenceM + cont1 ) + (\rdecls e -> runBuilderT' $ cont2 rdecls e) + {-# INLINE buildScopedAndThen #-} + +newtype BuilderDeclEmission (n::S) (l::S) = BuilderDeclEmission (Decl n l) + +instance ProvesExt BuilderDeclEmission where + toExtEvidence (BuilderDeclEmission d) = toExtEvidence d + +instance BindsNames BuilderDeclEmission where + toScopeFrag (BuilderDeclEmission d) = toScopeFrag d + {-# INLINE toScopeFrag #-} + +instance ExtOutFrag BuilderEmissions BuilderDeclEmission where + extendOutFrag rn (BuilderDeclEmission d) = RNest rn d + {-# INLINE extendOutFrag #-} + +instance Fallible m => Builder (BuilderT m) where + rawEmitDecl hint expr = do + BuilderT $ freshExtendSubInplaceT hint \b -> + (BuilderDeclEmission $ Let b expr, binderName b) + -- {-# INLINE rawEmitDecl #-} -- instance Fallible m => EnvReader (BuilderT m) where -- unsafeGetEnv = BuilderT $ getOutMapInplaceT @@ -202,16 +202,16 @@ liftEmitBuilder cont = do -- refreshAbs ab cont = BuilderT $ refreshAbs ab \b e -> runBuilderT' $ cont b e -- {-# INLINE refreshAbs #-} --- instance (SinkableE v, ScopableBuilder m) => ScopableBuilder (SubstReaderT v m i) where --- buildScopedAndThen cont1 cont2 = SubstReaderT \env -> --- buildScopedAndThen --- (runReaderT (runSubstReaderT' cont1) (sink env)) --- (\d e -> runReaderT (runSubstReaderT' $ cont2 d e) (sink env)) --- {-# INLINE buildScopedAndThen #-} +instance (SinkableE v, ScopableBuilder m) => ScopableBuilder (SubstReaderT v m i) where + buildScopedAndThen cont1 cont2 = SubstReaderT \env -> + buildScopedAndThen + (runReaderT (runSubstReaderT' cont1) (sink env)) + (\d e -> runReaderT (runSubstReaderT' $ cont2 d e) (sink env)) + {-# INLINE buildScopedAndThen #-} --- instance (SinkableE v, Builder m) => Builder (SubstReaderT v m i) where --- rawEmitDecl hint ann expr = liftSubstReaderT $ emitDecl hint ann expr --- {-# INLINE rawEmitDecl #-} +instance (SinkableE v, Builder m) => Builder (SubstReaderT v m i) where + rawEmitDecl hint expr = liftSubstReaderT $ emitDecl hint expr + {-# INLINE rawEmitDecl #-} -- instance (SinkableE e, ScopableBuilder m) => ScopableBuilder (ReaderT1 e m) where -- buildScopedAndThen cont1 cont2 = ReaderT1 $ ReaderT \env -> @@ -296,10 +296,11 @@ newtype WrapWithEmits n r = -- -- === lambda-like things === buildBlock - :: (ScopableBuilder m, HasNamesE e) + :: (ScopableBuilder m) => (forall l. (Emits l, DExt n l) => m l (Atom l)) -> m n (Expr n) -buildBlock cont = mkBlock =<< buildScoped cont +buildBlock cont = buildScopedAndThen cont \decls result -> + return $ declsToExpr decls result {-# INLINE buildBlock #-} -- buildCoreLam @@ -685,8 +686,7 @@ buildBlock cont = mkBlock =<< buildScoped cont -- ProjectProduct i -> reduceProj i x' -- UnwrapNewtype -> reduceUnwrap x' -mkBlock :: Abs Decls Atom n -> m n (Expr n) -mkBlock (Abs Empty expr) = undefined -- return $ toExpr expr +-- mkBlock :: Abs Decls Atom n -> m n (Expr n) -- mkBlock (Abs decls body) = do -- let block = Abs decls (toExpr body) -- effTy <- blockEffTy block diff --git a/src/lib/Name.hs b/src/lib/Name.hs index 044c0cd08..47fa624e9 100644 --- a/src/lib/Name.hs +++ b/src/lib/Name.hs @@ -114,7 +114,7 @@ class HasScope scope => OutMap scope where class OutMap env => ExtOutMap (env :: S -> *) (frag :: S -> S -> *) where extendOutMap :: Distinct l => env n -> frag n l -> env l -class ExtOutFrag (frag :: B) (subfrag :: B) where +class BindsNames subfrag => ExtOutFrag (frag :: B) (subfrag :: B) where extendOutFrag :: Distinct m => frag n l -> subfrag l m -> frag n m todoSinkableProof :: a @@ -1272,109 +1272,84 @@ instance (Monad1 m, ScopeReader m, ScopeExtender m, Fallible1 m) -- === in-place scope updating monad -- immutable fragment === -- The bindings returned by the action should be an extension of the input bindings by the emitted decls. -newtype InplaceT (bindings::E) (decls::B) (m::MonadKind) (n::S) (a :: *) = UnsafeMakeInplaceT - { unsafeRunInplaceT :: Distinct n => bindings n -> decls UnsafeS UnsafeS -> m (a, decls UnsafeS UnsafeS, bindings UnsafeS) } +newtype InplaceT (decls::B) (m::MonadKind) (n::S) (a :: *) = UnsafeMakeInplaceT + { unsafeRunInplaceT :: Distinct n => Scope n -> decls UnsafeS UnsafeS -> m (a, decls UnsafeS UnsafeS, Scope UnsafeS) } runInplaceT - :: (ExtOutMap b d, OutFrag d, Monad m) + :: (OutFrag d, Monad m) => Distinct n - => b n - -> InplaceT b d m n a + => Scope n + -> InplaceT d m n a -> m (d n n, a) -runInplaceT bindings (UnsafeMakeInplaceT f) = do - (result, d, _) <- f bindings emptyOutFrag +runInplaceT scope (UnsafeMakeInplaceT f) = do + (result, d, _) <- f scope emptyOutFrag return (unsafeCoerceB d, result) {-# INLINE runInplaceT #-} -- Special case of extending without introducing new names -- (doesn't require `Mut n`) extendTrivialInplaceT - :: (ExtOutMap b d, OutFrag d, Monad m) + :: (OutFrag d, Monad m) => d n n - -> InplaceT b d m n () + -> InplaceT d m n () extendTrivialInplaceT d = UnsafeMakeInplaceT \env decls -> do - let env' = unsafeCoerceE $ extendOutMap env d + let env' = unsafeCoerceE $ extendOutMap env $ toScopeFrag d withFabricatedDistinct @UnsafeS $ return ((), catOutFrags decls $ unsafeCoerceB d, env') {-# INLINE extendTrivialInplaceT #-} extendTrivialSubInplaceT - :: (ExtOutMap b d, ExtOutFrag ds d, Monad m) + :: (ExtOutFrag ds d, Monad m) => d n n - -> InplaceT b ds m n () + -> InplaceT ds m n () extendTrivialSubInplaceT d = UnsafeMakeInplaceT \env decls -> do - let env' = extendOutMap env d + let env' = extendOutMap env $ toScopeFrag d withFabricatedDistinct @UnsafeS $ return ((), extendOutFrag decls $ unsafeCoerceB d, unsafeCoerceE env') {-# INLINE extendTrivialSubInplaceT #-} -- TODO: This should be declared unsafe! getOutMapInplaceT - :: (ExtOutMap b d, Monad m) - => InplaceT b d m n (b n) + :: (Monad m) + => InplaceT d m n (Scope n) getOutMapInplaceT = UnsafeMakeInplaceT \env decls -> return (env, decls, unsafeCoerceE env) {-# INLINE getOutMapInplaceT #-} -- === in-place scope updating monad -- mutable stuff === -extendInplaceTLocal - :: (ExtOutMap b d, OutFrag d, Monad m) - => (b n -> b n) - -> InplaceT b d m n a - -> InplaceT b d m n a -extendInplaceTLocal f cont = - UnsafeMakeInplaceT \env decls -> do - (ans, newDecls, _) <- unsafeRunInplaceT cont (f env) emptyOutFrag - withFabricatedDistinct @UnsafeS $ - return ( ans - , catOutFrags decls $ unsafeCoerceB newDecls - , extendOutMap env $ unsafeCoerceB newDecls) -{-# INLINE extendInplaceTLocal #-} - extendInplaceT - :: forall m b d e n. - (ExtOutMap b d, OutFrag d, Monad m, RenameB d, RenameE e) - => Mut n => Abs d e n -> InplaceT b d m n (e n) + :: forall m d e n. + (OutFrag d, Monad m, RenameB d, RenameE e) + => Mut n => Abs d e n -> InplaceT d m n (e n) extendInplaceT ab = do UnsafeMakeInplaceT \env decls -> refreshAbsPure (toScope env) ab \_ d result -> do - let env' = unsafeCoerceE $ extendOutMap env d + let env' = unsafeCoerceE $ extendOutMap env $ toScopeFrag d withFabricatedDistinct @UnsafeS $ return (unsafeCoerceE result, catOutFrags decls $ unsafeCoerceB d, env') {-# INLINE extendInplaceT #-} -extendSubInplaceT - :: (ExtOutMap b d, ExtOutFrag ds d, BindsNames d, Monad m, RenameB d, RenameE e) - => Mut n => Abs d e n -> InplaceT b ds m n (e n) -extendSubInplaceT ab = do - UnsafeMakeInplaceT \env decls -> - refreshAbsPure (toScope env) ab \_ d result -> do - let env' = unsafeCoerceE $ extendOutMap env d - withFabricatedDistinct @UnsafeS $ - return (unsafeCoerceE result, extendOutFrag decls $ unsafeCoerceB d, env') -{-# INLINE extendSubInplaceT #-} - freshExtendSubInplaceT - :: (ExtOutMap b d, ExtOutFrag ds d, Monad m) - => Mut n => NameHint -> (forall l. NameBinder n l -> (d n l, e l)) -> InplaceT b ds m n (e n) + :: (ExtOutFrag ds d, Monad m) + => Mut n => NameHint -> (forall l. NameBinder n l -> (d n l, e l)) -> InplaceT ds m n (e n) freshExtendSubInplaceT hint build = UnsafeMakeInplaceT \env decls -> withFresh hint (toScope env) \b -> do let (d, result) = build b - let env' = unsafeCoerceE $ extendOutMap env d + let env' = unsafeCoerceE $ extendOutMap env $ toScopeFrag d withFabricatedDistinct @UnsafeS $ return (unsafeCoerceE result, extendOutFrag decls $ unsafeCoerceB d, env') {-# INLINE freshExtendSubInplaceT #-} locallyMutableInplaceT :: forall m b d n e a. - (ExtOutMap b d, OutFrag d, Monad m, SinkableE e) - => (forall l. (Mut l, DExt n l) => InplaceT b d m l (e l)) - -> (forall l. DExt n l => d n l -> e l -> InplaceT b d m l a) - -> InplaceT b d m n a + (OutFrag d, Monad m, SinkableE e) + => (forall l. (Mut l, DExt n l) => InplaceT d m l (e l)) + -> (forall l. DExt n l => d n l -> e l -> InplaceT d m l a) + -> InplaceT d m n a locallyMutableInplaceT cont1 cont2 = do UnsafeMakeInplaceT \env decls -> do (e, d, env') <- withFabricatedMut @n $ @@ -1384,22 +1359,6 @@ locallyMutableInplaceT cont1 cont2 = do return (ans, decls, unsafeCoerceE env) {-# INLINE locallyMutableInplaceT #-} -liftBetweenInplaceTs - :: (Monad m, ExtOutMap bs ds, OutFrag ds, OutFrag ds') - => (forall a'. m' a' -> m a') - -> (bs n -> bs' n) - -> (forall l l' . Distinct l' => ds' l l' -> ds l l') - -> InplaceT bs' ds' m' n a - -> InplaceT bs ds m n a -liftBetweenInplaceTs liftInner lowerBindings liftDecls (UnsafeMakeInplaceT f) = - UnsafeMakeInplaceT \envOuter declsOuter -> do - (result, dInner, _) <- liftInner $ f (lowerBindings envOuter) emptyOutFrag - withFabricatedDistinct @UnsafeS do - let dOuter = liftDecls dInner - let envOuter' = extendOutMap (unsafeCoerceE envOuter) dOuter - return (result, catOutFrags declsOuter dOuter, envOuter') -{-# INLINE liftBetweenInplaceTs #-} - -- === predicates for mutable and immutable scope parameters === class Mut (n::S) @@ -1416,13 +1375,13 @@ newtype WrapWithMut n r = -- === InplaceT instances === -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m) - => Functor (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls, Monad m) + => Functor (InplaceT decls m n) where fmap = liftM {-# INLINE fmap #-} -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m) - => Applicative (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls, Monad m) + => Applicative (InplaceT decls m n) where pure = return {-# INLINE pure #-} liftA2 = liftM2 @@ -1430,8 +1389,8 @@ instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m) f <*> x = do { f' <- f; x' <- x; return (f' x') } {-# INLINE (<*>) #-} -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m) - => Monad (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls, Monad m) + => Monad (InplaceT decls m n) where return x = UnsafeMakeInplaceT \env decls -> do return (x, decls, unsafeCoerceE env) {-# INLINE return #-} @@ -1440,69 +1399,63 @@ instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m) unsafeRunInplaceT (f x) (unsafeCoerceE outMap1) decls1 {-# INLINE (>>=) #-} -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m) - => ScopeReader (InplaceT bindings decls m) where +instance (BindsNames decls, SinkableB decls, Monad m) + => ScopeReader (InplaceT decls m) where getDistinct = UnsafeMakeInplaceT \env decls -> return (Distinct, decls, unsafeCoerceE env) {-# INLINE getDistinct #-} unsafeGetScope = toScope <$> getOutMapInplaceT {-# INLINE unsafeGetScope #-} -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m, MonadFail m) - => MonadFail (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls, Monad m, MonadFail m) + => MonadFail (InplaceT decls m n) where fail s = lift1 $ fail s {-# INLINE fail #-} -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m, Fallible m) - => Fallible (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls, Monad m, Fallible m) + => Fallible (InplaceT decls m n) where throwErr errs = UnsafeMakeInplaceT \_ _ -> throwErr errs -instance ( ExtOutMap bindings decls, BindsNames decls, SinkableB decls, Monad m +instance (BindsNames decls, SinkableB decls, Monad m , Alternative m) - => Alternative (InplaceT bindings decls m n) where + => Alternative (InplaceT decls m n) where empty = lift1 empty {-# INLINE empty #-} UnsafeMakeInplaceT f1 <|> UnsafeMakeInplaceT f2 = UnsafeMakeInplaceT \env decls -> f1 env decls <|> f2 env decls {-# INLINE (<|>) #-} -instance ( ExtOutMap bindings decls, BindsNames decls, SinkableB decls, - Catchable m) - => Catchable (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls, Catchable m) + => Catchable (InplaceT decls m n) where catchErr (UnsafeMakeInplaceT f1) handler = UnsafeMakeInplaceT \env decls -> f1 env decls `catchErr` \err -> case handler err of UnsafeMakeInplaceT f2 -> f2 env decls -instance ( ExtOutMap bindings decls, BindsNames decls, SinkableB decls - , MonadWriter w m) - => MonadWriter w (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls , MonadWriter w m) + => MonadWriter w (InplaceT decls m n) where tell w = lift1 $ tell w {-# INLINE tell #-} listen = undefined pass = undefined -instance ( ExtOutMap bindings decls, BindsNames decls, SinkableB decls - , MonadState s m) - => MonadState s (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls , MonadState s m) + => MonadState s (InplaceT decls m n) where state f = lift1 $ state f {-# INLINE state #-} -instance (ExtOutMap bindings decls, BindsNames decls, SinkableB decls) - => MonadTrans1 (InplaceT bindings decls) where +instance (BindsNames decls, SinkableB decls) => MonadTrans1 (InplaceT decls) where lift1 m = UnsafeMakeInplaceT \env decls -> (, decls, unsafeCoerceE env) <$> m {-# INLINE lift1 #-} -instance ( ExtOutMap bindings decls, BindsNames decls, SinkableB decls - , MonadReader r m) - => MonadReader r (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls , MonadReader r m) + => MonadReader r (InplaceT decls m n) where ask = lift1 $ ask {-# INLINE ask #-} local f (UnsafeMakeInplaceT cont) = UnsafeMakeInplaceT \env decls -> local f (cont env decls) {-# INLINE local #-} -instance ( ExtOutMap bindings decls, BindsNames decls, SinkableB decls - , MonadIO m) - => MonadIO (InplaceT bindings decls m n) where +instance (BindsNames decls, SinkableB decls , MonadIO m) + => MonadIO (InplaceT decls m n) where liftIO = lift1 . liftIO {-# INLINE liftIO #-} diff --git a/src/lib/QueryTypePure.hs b/src/lib/QueryTypePure.hs index a07444442..a1fb8a03b 100644 --- a/src/lib/QueryTypePure.hs +++ b/src/lib/QueryTypePure.hs @@ -102,20 +102,13 @@ getSuperclassType bsAbove (Nest b@(_:>t) bs) = \case i -> getSuperclassType (RNest bsAbove b) bs (i-1) instance HasType Expr where - getType expr = undefined - -- getType expr = case expr of - -- App (EffTy _ ty) _ _ -> ty - -- TopApp (EffTy _ ty) _ _ -> ty - -- TabApp t _ _ -> t - -- Atom x -> getType x - -- Block (EffTy _ ty) _ -> ty - -- TabCon ty _ -> ty - -- PrimOp ty _ -> ty - -- Case _ _ (EffTy _ resultTy) -> resultTy - -- ApplyMethod (EffTy _ t) _ _ _ -> t - -- Project t _ _ -> t - -- Unwrap t _ -> t - -- Hof (TypedHof (EffTy _ ty) _) -> ty + getType = \case + Block ty _ -> ty + TopApp ty _ _ -> ty + PrimOp ty _ -> ty + Case ty _ _ -> ty + For _ _ -> undefined + While _ -> undefined -- instance HasType MemOp where -- getType = \case diff --git a/src/lib/Simplify.hs b/src/lib/Simplify.hs index 0e465e31d..6a6057cff 100644 --- a/src/lib/Simplify.hs +++ b/src/lib/Simplify.hs @@ -37,10 +37,9 @@ simplifyTopFun f = liftSimplifyM $ simplifyLam f -- === Simplification monad === newtype SimplifyM (i::S) (o::S) (a:: *) = SimplifyM - { runSimplifyM' - :: SubstReaderT SimpSubstVal (ScopeReaderT HardFailM) i o a } - deriving ( Functor, Applicative, Monad, ScopeReader - , SubstReader SimpSubstVal, MonadFail) + { runSimplifyM' :: SubstReaderT SimpSubstVal BuilderM i o a } + deriving ( Functor, Applicative, Monad, ScopeReader, ScopableBuilder + , Builder, SubstReader SimpSubstVal, Fallible, MonadFail) data SimpVal (n::S) = SimpAtom (Atom n) -- local data vars @@ -57,8 +56,8 @@ instance SinkableE SimpVal where sinkingProofE _ = undefined liftSimplifyM :: Monad m => SimplifyM VoidS VoidS a -> m a -liftSimplifyM cont = return $ runHardFail $ - runScopeReaderT emptyOutMap $ runSubstReaderT voidSubst $ runSimplifyM' cont +liftSimplifyM cont = runScopeReaderT emptyOutMap $ liftBuilder $ + runSubstReaderT voidSubst $ runSimplifyM' cont {-# INLINE liftSimplifyM #-} -- liftDoubleBuilderToSimplifyM :: DoubleBuilder o a -> SimplifyM i o a @@ -372,7 +371,18 @@ simplifyLam (CoreLamExpr _ ab) = go ab go (Abs Empty body) = liftM (Abs Empty) $ buildBlock $ simplifyExpr body simplifyExpr :: Emits o => CExpr i -> SimplifyM i o (Atom o) -simplifyExpr = undefined +simplifyExpr = \case + CLit val -> return $ Lit val + CPrimOp ty op -> do + op' <- mapM simplifyExpr op + ty <- simplifyType ty + emit $ PrimOp ty op' + e -> error $ show e + +simplifyType :: CType i -> SimplifyM i o (Type o) +simplifyType = \case + CTyCon con -> case con of + CBaseType t -> return $ BaseType t -- simplifyLam (LamExpr bsTop body) = case bsTop of -- Nest b bs -> withSimplifiedBinder b \b' -> do diff --git a/src/lib/Types/Primitives.hs b/src/lib/Types/Primitives.hs index af8c44f28..802e8dd38 100644 --- a/src/lib/Types/Primitives.hs +++ b/src/lib/Types/Primitives.hs @@ -48,7 +48,7 @@ instance Hashable BinOp instance Store BinOp data UnOp = - Exp | Exp2 | Log | Log2 | Log10 | Log1p | Sin | Cos | Tan | Sqrt | Floor + Identity | Exp | Exp2 | Log | Log2 | Log10 | Log1p | Sin | Cos | Tan | Sqrt | Floor | Ceil | Round | LGamma | Erf | Erfc | FNeg | BNot deriving (Show, Eq, Ord, Generic) instance Hashable UnOp diff --git a/src/lib/Types/Simple.hs b/src/lib/Types/Simple.hs index f935e15f1..301b6a6fc 100644 --- a/src/lib/Types/Simple.hs +++ b/src/lib/Types/Simple.hs @@ -76,7 +76,7 @@ instance Pretty (Expr n) where Case _ _ _ -> undefined For _ _ -> undefined While _ -> undefined - PrimOp _ _ -> undefined + PrimOp _ op -> pr op instance SinkableE Expr instance HoistableE Expr @@ -87,7 +87,12 @@ instance Store (Expr n) instance GenericE Atom where type RepE Atom = UnitE -instance Pretty (Atom n) + +instance Pretty (Atom n) where + pr = \case + Var v _ -> pr v + Lit l -> pr l + instance SinkableE Atom instance HoistableE Atom instance RenameE Atom