WIP

dex.cabal

@@ -54,6 +54,7 @@ library
                      , ConcreteSyntax
                      , Core
                      , Err
+                     , EmitterMonad
                      , Export
                      , Generalize
                      , Imp

src/lib/Algebra.hs

@@ -48,8 +48,8 @@ newtype Polynomial (n::S) =
 -- This is the main entrypoint. Doing polynomial math sometimes lets
 -- us compute sums in closed form. This tries to compute
 -- `\sum_{i=0}^(lim-1) body`. `i`, `lim`, and `body` should all have type `Nat`.
-sumUsingPolys :: (Builder SimpIR m, Fallible1 m, Emits n)
-              => Atom SimpIR n -> Abs (Binder SimpIR) (Block SimpIR) n -> m n (Atom SimpIR n)
+sumUsingPolys :: Emits n
+              => Atom SimpIR n -> Abs (Binder SimpIR) (Block SimpIR) n -> BuilderM SimpIR n (Atom SimpIR n)
 sumUsingPolys lim (Abs i body) = do
   sumAbs <- refreshAbs (Abs i body) \(i':>_) body' -> do
     blockAsPoly body' >>= \case
@@ -192,7 +192,7 @@ blockAsPolyRec decls result = case decls of
 -- coefficients. This is why we have to find the least common multiples and do the
 -- accumulation over numbers multiplied by that LCM. We essentially do fixed point
 -- fractional math here.
-emitPolynomial :: (Emits n, Builder SimpIR m) => Polynomial n -> m n (Atom SimpIR n)
+emitPolynomial :: Emits n => Polynomial n -> BuilderM SimpIR n (Atom SimpIR n)
 emitPolynomial (Polynomial p) = do
   let constLCM = asAtom $ foldl lcm 1 $ fmap (denominator . snd) $ toList p
   monoAtoms <- flip traverse (toList p) $ \(m, c) -> do
@@ -206,7 +206,7 @@ emitPolynomial (Polynomial p) = do
     --       because it might be causing overflows due to all arithmetic being shifted.
     asAtom = IdxRepVal . fromInteger
 
-emitMonomial :: (Emits n, Builder SimpIR m) => Monomial n -> m n (Atom SimpIR n)
+emitMonomial :: Emits n => Monomial n -> BuilderM SimpIR n (Atom SimpIR n)
 emitMonomial (Monomial m) = do
   varAtoms <- forM (toList m) \(v, e) -> case v of
     LeftE v' -> do
@@ -217,7 +217,7 @@ emitMonomial (Monomial m) = do
       ipow atom e
   foldM imul (IdxRepVal 1) varAtoms
 
-ipow :: (Emits n, Builder SimpIR m) => Atom SimpIR n -> Int -> m n (Atom SimpIR n)
+ipow :: Emits n => Atom SimpIR n -> Int -> BuilderM SimpIR n (Atom SimpIR n)
 ipow x i = foldM imul (IdxRepVal 1) (replicate i x)
 
 -- === instances ===

src/lib/Builder.hs

@@ -38,11 +38,11 @@ import Util (enumerate, transitiveClosureM, bindM2, toSnocList, (...))
 
 -- === Ordinary (local) builder class ===
 
-class (EnvReader m, EnvExtender m, Fallible1 m, IRRep r)
+class (EnvReader m, Fallible1 m, IRRep r)
       => Builder (r::IR) (m::MonadKind1) | m -> r where
   rawEmitDecl :: Emits n => NameHint -> LetAnn -> Expr r n -> m n (AtomVar r n)
 
-class Builder r m => ScopableBuilder (r::IR) (m::MonadKind1) | m -> r where
+class (EnvExtender m, Builder r m) => ScopableBuilder (r::IR) (m::MonadKind1) | m -> r where
   buildScopedAndThen
     :: SinkableE e
     => (forall l. (Emits l, DExt n l) => m l (e l))
@@ -252,9 +252,9 @@ instance ( IRRep r, RenameB frag, HoistableB frag, OutFrag frag
   {-# INLINE refreshAbs #-}
 
 instance (SinkableV v, HoistingTopBuilder f m) => HoistingTopBuilder f (SubstReaderT v m i) where
-  emitHoistedEnv ab = SubstReaderT $ lift $ emitHoistedEnv ab
+  emitHoistedEnv ab = liftSubstReaderT $ emitHoistedEnv ab
   {-# INLINE emitHoistedEnv #-}
-  canHoistToTop e = SubstReaderT $ lift $ canHoistToTop e
+  canHoistToTop e = liftSubstReaderT $ canHoistToTop e
   {-# INLINE canHoistToTop #-}
 
 -- === Top-level builder class ===
@@ -302,7 +302,7 @@ emitSynthCandidates sc = emitLocalModuleEnv $ mempty {envSynthCandidates = sc}
 
 addInstanceSynthCandidate :: TopBuilder m => ClassName n -> InstanceName n -> m n ()
 addInstanceSynthCandidate className instanceName =
-  emitSynthCandidates $ SynthCandidates [] (M.singleton className [instanceName])
+  emitSynthCandidates $ SynthCandidates (M.singleton className [instanceName])
 
 updateTransposeRelation :: (Mut n, TopBuilder m) => TopFunName n -> TopFunName n -> m n ()
 updateTransposeRelation f1 f2 =
@@ -401,13 +401,13 @@ instance Fallible m => TopBuilder (TopBuilderT m) where
   {-# INLINE localTopBuilder #-}
 
 instance (SinkableV v, TopBuilder m) => TopBuilder (SubstReaderT v m i) where
-  emitBinding hint binding = SubstReaderT $ lift $ emitBinding hint binding
+  emitBinding hint binding = liftSubstReaderT $ emitBinding hint binding
   {-# INLINE emitBinding #-}
-  emitEnv ab = SubstReaderT $ lift $ emitEnv ab
+  emitEnv ab = liftSubstReaderT $ emitEnv ab
   {-# INLINE emitEnv #-}
-  emitNamelessEnv bs = SubstReaderT $ lift $ emitNamelessEnv bs
+  emitNamelessEnv bs = liftSubstReaderT $ emitNamelessEnv bs
   {-# INLINE emitNamelessEnv #-}
-  localTopBuilder cont = SubstReaderT $ ReaderT \env -> do
+  localTopBuilder cont = SubstReaderT \env -> do
     localTopBuilder do
       Distinct <- getDistinct
       runReaderT (runSubstReaderT' cont) (sink env)
@@ -514,14 +514,14 @@ instance (IRRep r, Fallible m) => EnvExtender (BuilderT r m) where
   {-# INLINE refreshAbs #-}
 
 instance (SinkableV v, ScopableBuilder r m) => ScopableBuilder r (SubstReaderT v m i) where
-  buildScopedAndThen cont1 cont2 = SubstReaderT $ ReaderT \env ->
+  buildScopedAndThen cont1 cont2 = SubstReaderT \env ->
     buildScopedAndThen
       (runReaderT (runSubstReaderT' cont1) (sink env))
       (\d e -> runReaderT (runSubstReaderT' $ cont2 d e) (sink env))
   {-# INLINE buildScopedAndThen #-}
 
 instance (SinkableV v, Builder r m) => Builder r (SubstReaderT v m i) where
-  rawEmitDecl hint ann expr = SubstReaderT $ lift $ emitDecl hint ann expr
+  rawEmitDecl hint ann expr = liftSubstReaderT $ emitDecl hint ann expr
   {-# INLINE rawEmitDecl #-}
 
 instance (SinkableE e, ScopableBuilder r m) => ScopableBuilder r (OutReaderT e m) where
@@ -555,6 +555,10 @@ instance (SinkableE e, Builder r m) => Builder r (ReaderT1 e m) where
     ReaderT1 $ lift $ emitDecl hint ann expr
   {-# INLINE rawEmitDecl #-}
 
+instance (DiffStateE s d, Builder r m) => Builder r (DiffStateT1 s d m) where
+  rawEmitDecl hint ann expr = lift11 $ rawEmitDecl hint ann expr
+  {-# INLINE rawEmitDecl #-}
+
 instance (SinkableE e, HoistableState e, Builder r m) => Builder r (StateT1 e m) where
   rawEmitDecl hint ann expr = lift11 $ emitDecl hint ann expr
   {-# INLINE rawEmitDecl #-}

src/lib/CheapReduction.hs

@@ -20,7 +20,6 @@ module CheapReduction
   where
 
 import Control.Applicative
-import Control.Monad.Trans
 import Control.Monad.Writer.Strict  hiding (Alt)
 import Control.Monad.State.Strict
 import Control.Monad.Reader
@@ -42,7 +41,6 @@ import Types.Core
 import Types.Imp
 import Types.Primitives
 import Util
-import {-# SOURCE #-} Inference (trySynthTerm)
 
 -- Carry out the reductions we are willing to carry out during type
 -- inference.  The goal is to support type aliases like `Int = Int32`
@@ -102,9 +100,9 @@ class ( Alternative2 m, SubstReader AtomSubstVal m
   lookupCache :: AtomName r o -> m i o (Maybe (Maybe (Atom r o)))
 
 instance IRRep r => CheapReducer (CheapReducerM r) r where
-  updateCache v u = CheapReducerM $ SubstReaderT $ lift $ lift11 $
+  updateCache v u = CheapReducerM $ liftSubstReaderT $ lift11 $
     modify (MapE . M.insert v (toMaybeE u) . fromMapE)
-  lookupCache v = CheapReducerM $ SubstReaderT $ lift $ lift11 $
+  lookupCache v = CheapReducerM $ liftSubstReaderT $ lift11 $
     fmap fromMaybeE <$> gets (M.lookup v . fromMapE)
 
 liftCheapReducerM
@@ -185,11 +183,6 @@ instance IRRep r => CheaplyReducibleE r (Atom r) (Atom r) where
     -- TODO: we don't collect the dict holes here, so there's a danger of
     -- dropping them if they turn out to be phantom.
     Lam _ -> substM a
-    DictHole ctx ty' access -> do
-      ty <- cheapReduceE ty'
-      runFallibleT1 (trySynthTerm ty access) >>= \case
-        Success d -> return d
-        Failure _ -> return $ DictHole ctx ty access
     -- We traverse the Atom constructors that might contain lambda expressions
     -- explicitly, to make sure that we can skip normalizing free vars inside those.
     Con con -> Con <$> traverseOp con cheapReduceE cheapReduceE (error "unexpected lambda")
@@ -616,7 +609,6 @@ visitAtomPartial = \case
   Eff eff   -> Eff     <$> visitGeneric eff
   DictCon t d -> DictCon <$> visitType t <*> visitGeneric d
   NewtypeCon con x -> NewtypeCon <$> visitGeneric con <*> visitGeneric x
-  DictHole ctx ty access -> DictHole ctx <$> visitGeneric ty <*> pure access
   TypeAsAtom t -> TypeAsAtom <$> visitGeneric t
   RepValAtom repVal -> RepValAtom <$> visitGeneric repVal
 

src/lib/CheckType.hs

@@ -180,9 +180,6 @@ instance IRRep r => CheckableE r (Atom r) where
       con' <- typeCheckNewtypeCon con xTy
       return $ NewtypeCon con' x'
     SimpInCore x -> SimpInCore <$> checkE x
-    DictHole ctx ty access -> do
-      ty' <- ty |: TyKind
-      return $ DictHole ctx ty' access
     ProjectElt resultTy UnwrapNewtype x -> do
       resultTy' <- resultTy |: TyKind
       (x', NewtypeTyCon con) <- checkAndGetType x

src/lib/Core.hs

@@ -389,12 +389,6 @@ withFreshBinders (binding:rest) cont = do
       cont (Nest b bs)
            (sink (binderName b) : vs)
 
-getInstanceDicts :: EnvReader m => ClassName n -> m n [InstanceName n]
-getInstanceDicts name = do
-  env <- withEnv moduleEnv
-  return $ M.findWithDefault [] name $ instanceDicts $ envSynthCandidates env
-{-# INLINE getInstanceDicts #-}
-
 -- These `fromNary` functions traverse a chain of unary structures (LamExpr,
 -- TabLamExpr, CorePiType, respectively) up to the given maxDepth, and return the
 -- discovered binders packed as the nary structure (NaryLamExpr or PiType),

src/lib/Imp.hs

@@ -25,7 +25,6 @@ import Data.Maybe (fromJust, isJust)
 import Data.Text.Prettyprint.Doc
 import Control.Category
 import Control.Monad.Identity
-import Control.Monad.Reader
 import Control.Monad.Writer.Strict
 import Control.Monad.State.Strict hiding (State)
 import qualified Control.Monad.State.Strict as MTL
@@ -246,14 +245,14 @@ instance ImpBuilder ImpM where
   {-# INLINE extendAllocsToFree #-}
 
 instance ImpBuilder m => ImpBuilder (SubstReaderT AtomSubstVal m i) where
-  emitMultiReturnInstr instr = SubstReaderT $ lift $ emitMultiReturnInstr instr
+  emitMultiReturnInstr instr = liftSubstReaderT $ emitMultiReturnInstr instr
   {-# INLINE emitMultiReturnInstr #-}
-  emitDeclsImp ab = SubstReaderT $ lift $ emitDeclsImp ab
+  emitDeclsImp ab = liftSubstReaderT $ emitDeclsImp ab
   {-# INLINE emitDeclsImp #-}
-  buildScopedImp cont = SubstReaderT $ ReaderT \env ->
+  buildScopedImp cont = SubstReaderT \env ->
     buildScopedImp $ runSubstReaderT (sink env) $ cont
   {-# INLINE buildScopedImp #-}
-  extendAllocsToFree ptr = SubstReaderT $ lift $ extendAllocsToFree ptr
+  extendAllocsToFree ptr = liftSubstReaderT $ extendAllocsToFree ptr
   {-# INLINE extendAllocsToFree #-}
 
 instance ImpBuilder m => Imper (SubstReaderT AtomSubstVal m)

src/lib/ImpToLLVM.hs

@@ -95,7 +95,7 @@ newtype CompileM i o a =
            , EnvReader, SubstReader OperandSubstVal )
 
 instance MonadState CompileState (CompileM i o) where
-  state f = CompileM $ SubstReaderT $ lift $ EnvReaderT $ lift $ state f
+  state f = CompileM $ liftSubstReaderT $ EnvReaderT $ lift $ state f
 
 class MonadState CompileState m => LLVMBuilder (m::MonadKind)