diff --git a/dex.cabal b/dex.cabal index 2d75e9184..a8c2b6882 100644 --- a/dex.cabal +++ b/dex.cabal @@ -41,19 +41,19 @@ flag debug library exposed-modules: AbstractSyntax - , Builder - , CUDA - , CheapReduction + -- , Builder + -- , CUDA + -- , CheapReduction -- , CheckType , ConcreteSyntax - , Core - , DPS + -- , Core + -- , DPS , Err - , Generalize - , Imp - , ImpToLLVM + -- , Generalize + -- , Imp + -- , ImpToLLVM , IncState - , Inference + -- , Inference -- , Inline -- , JAX.Concrete -- , JAX.Rename @@ -73,29 +73,29 @@ library -- , PeepholeOptimize , PPrint , RawName - , Runtime + -- , Runtime -- , RuntimePrint - , Serialize - , Simplify - , Subst + -- , Serialize + -- , Simplify + -- , Subst , SourceRename , SourceIdTraversal - , TopLevel + , TopLevel2 -- , Transpose , Types.Simple , Types.Complicated , Types.Imp , Types.Primitives , Types.Source - , Types.Top - , QueryType - , QueryTypePure + , Types.Top2 + -- , QueryType + -- , QueryTypePure , Util -- , Vectorize , Actor - , Live.Eval - , Live.Web - , RenderHtml + -- , Live.Eval + -- , Live.Web + -- , RenderHtml other-modules: Paths_dex build-depends: base , bytestring diff --git a/src/dex.hs b/src/dex.hs index 53fbe0ac0..1f1c1617a 100644 --- a/src/dex.hs +++ b/src/dex.hs @@ -19,15 +19,12 @@ import qualified Data.Map.Strict as M import qualified System.Console.ANSI as ANSI import System.Console.ANSI hiding (Color) -import TopLevel +import Types.Source +import TopLevel2 import AbstractSyntax (parseTopDeclRepl) import ConcreteSyntax (keyWordStrs, preludeImportBlock) -import Live.Web +-- import Live.Web import PPrint hiding (hardline) -import Core -import Types.Imp -import Types.Source -import Types.Top import MonadUtil import Util (readFileText) @@ -45,7 +42,7 @@ data CmdOpts = CmdOpts EvalMode EvalConfig runMode :: CmdOpts -> IO () runMode (CmdOpts evalMode cfg) = case evalMode of ScriptMode fname fmt -> do - env <- loadCache + env <- initTopState -- loadCache ((), finalEnv) <- runTopperM cfg stdOutLogger env do blocks <- parseSourceBlocks <$> readFileText fname forM_ blocks \block -> do @@ -53,35 +50,36 @@ runMode (CmdOpts evalMode cfg) = case evalMode of ResultOnly -> return () TextDoc -> liftIO $ putStr $ pprint block evalSourceBlockRepl block - storeCache finalEnv - ReplMode -> do - env <- loadCache - void $ runTopperM cfg stdOutLogger env do - void $ evalSourceBlockRepl preludeImportBlock - forever do - block <- readSourceBlock - void $ evalSourceBlockRepl block - WebMode fname -> do - env <- loadCache - runWeb fname cfg env - GenerateHTML fname dest -> do - env <- loadCache - generateHTML fname dest cfg env - ClearCache -> clearCache + return () + -- storeCache finalEnv + -- ReplMode -> do + -- env <- loadCache + -- void $ runTopperM cfg stdOutLogger env do + -- void $ evalSourceBlockRepl preludeImportBlock + -- forever do + -- block <- readSourceBlock + -- void $ evalSourceBlockRepl block + -- WebMode fname -> do + -- env <- loadCache + -- runWeb fname cfg env + -- GenerateHTML fname dest -> do + -- env <- loadCache + -- generateHTML fname dest cfg env + -- ClearCache -> clearCache stdOutLogger :: Outputs -> IO () stdOutLogger (Outputs outs) = do isatty <- queryTerminal stdOutput forM_ outs \out -> putStr $ printOutput isatty out -readSourceBlock :: (MonadIO (m n), EnvReader m) => m n SourceBlock -readSourceBlock = do - sourceMap <- withEnv $ envSourceMap . moduleEnv - let filenameAndDexCompletions = - completeQuotedWord (Just '\\') "\"'" listFiles (dexCompletions sourceMap) - let hasklineSettings = setComplete filenameAndDexCompletions defaultSettings - liftIO $ runInputT hasklineSettings $ readMultiline prompt (parseTopDeclRepl . T.pack) - where prompt = ">=> " +-- readSourceBlock :: MonadIO (m n) => m n SourceBlock +-- readSourceBlock = do +-- sourceMap <- withEnv $ envSourceMap . moduleEnv +-- let filenameAndDexCompletions = +-- completeQuotedWord (Just '\\') "\"'" listFiles (dexCompletions sourceMap) +-- let hasklineSettings = setComplete filenameAndDexCompletions defaultSettings +-- liftIO $ runInputT hasklineSettings $ readMultiline prompt (parseTopDeclRepl . T.pack) +-- where prompt = ">=> " dexCompletions :: Monad m => SourceMap n -> CompletionFunc m dexCompletions sourceMap (line, _) = do @@ -145,8 +143,7 @@ enumOption optName prettyOptName defaultVal options = option parseEvalOpts :: Parser EvalConfig parseEvalOpts = EvalConfig - <$> enumOption "backend" "Backend" LLVM backends - <*> (option pathOption $ long "lib-path" <> value [LibBuiltinPath] + <$> (option pathOption $ long "lib-path" <> value [LibBuiltinPath] <> metavar "PATH" <> help "Library path") <*> optional (strOption $ long "prelude" <> metavar "FILE" <> help "Prelude file") <*> flag NoOptimize Optimize (short 'O' <> help "Optimize generated code") @@ -155,8 +152,6 @@ parseEvalOpts = EvalConfig where printBackends = [ ("haskell", PrintHaskell) , ("dex" , PrintCodegen) ] - backends = [ ("llvm" , LLVM ) - , ("llvm-mc", LLVMMC) ] logLevels = [ ("normal", NormalLogLevel) , ("debug" , DebugLogLevel ) ] diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs index 5e40095ba..81a242de2 100644 --- a/src/lib/AbstractSyntax.hs +++ b/src/lib/AbstractSyntax.hs @@ -69,7 +69,7 @@ import Util parseExpr :: Fallible m => GroupW -> m (UExpr VoidS) parseExpr e = liftSyntaxM $ expr e -parseDecl :: Fallible m => CTopDeclW -> m (UTopDecl VoidS VoidS) +parseDecl :: Fallible m => CTopDeclW -> m UTopDecl parseDecl d = liftSyntaxM $ topDecl d parseBlock :: Fallible m => CSBlock -> m (UBlock VoidS) @@ -93,9 +93,6 @@ checkSourceBlockParses = \case when (ann /= PlainLet) $ fail "Cannot annotate expressions" void $ expr e TopDecl d -> void $ topDecl d - Command _ b -> void $ expr b - DeclareForeign _ _ ty -> void $ expr ty - DeclareCustomLinearization _ _ body -> void $ expr body Misc _ -> return () UnParseable _ _ -> return () @@ -103,36 +100,37 @@ checkSourceBlockParses = \case type SyntaxM = Except -topDecl :: CTopDeclW -> SyntaxM (UTopDecl VoidS VoidS) -topDecl (WithSrcs sid sids topDecl') = case topDecl' of - CSDecl ann d -> ULocalDecl <$> decl ann (WithSrcs sid sids d) - CData name tyConParams givens constructors -> do - tyConParams' <- fromMaybeM tyConParams Empty aExplicitParams - givens' <- aOptGivens givens - constructors' <- forM constructors \(v, ps) -> do - ps' <- fromMaybeM ps Empty \(WithSrcs _ _ ps') -> - toNest <$> mapM (tyOptBinder Explicit) ps' - return (v, ps') - return $ UDataDefDecl - (UDataDef (withoutSrc name) (givens' >>> tyConParams') $ - map (\(name', cons) -> (withoutSrc name', UDataDefTrail cons)) constructors') - (fromSourceNameW name) - (toNest $ map (fromSourceNameW . fst) constructors') - CStruct name params givens fields defs -> do - params' <- fromMaybeM params Empty aExplicitParams - givens' <- aOptGivens givens - fields' <- forM fields \(v, ty) -> (v,) <$> expr ty - methods <- forM defs \(ann, d) -> do - (WithSrc _ methodName, lam) <- aDef d - return (ann, methodName, Abs (WithSrcB sid (UBindSource "self")) lam) - return $ UStructDecl (fromSourceNameW name) (UStructDef (withoutSrc name) (givens' >>> params') fields' methods) - CInterface name params methods -> do - params' <- aExplicitParams params - (methodNames, methodTys) <- unzip <$> forM methods \(methodName, ty) -> do - ty' <- expr ty - return (fromSourceNameW methodName, ty') - return $ UInterface params' methodTys (fromSourceNameW name) (toNest methodNames) - CInstanceDecl def -> aInstanceDef def +topDecl :: CTopDeclW -> SyntaxM UTopDecl +topDecl (WithSrcs sid sids topDecl') = undefined +-- topDecl (WithSrcs sid sids topDecl') = case topDecl' of +-- CSDecl ann d -> UTopLet <$> decl ann (WithSrcs sid sids d) +-- CData name tyConParams givens constructors -> do +-- tyConParams' <- fromMaybeM tyConParams Empty aExplicitParams +-- givens' <- aOptGivens givens +-- constructors' <- forM constructors \(v, ps) -> do +-- ps' <- fromMaybeM ps Empty \(WithSrcs _ _ ps') -> +-- toNest <$> mapM (tyOptBinder Explicit) ps' +-- return (v, ps') +-- return $ UDataDefDecl +-- (UDataDef (withoutSrc name) (givens' >>> tyConParams') $ +-- map (\(name', cons) -> (withoutSrc name', UDataDefTrail cons)) constructors') +-- (fromSourceNameW name) +-- (toNest $ map (fromSourceNameW . fst) constructors') +-- CStruct name params givens fields defs -> do +-- params' <- fromMaybeM params Empty aExplicitParams +-- givens' <- aOptGivens givens +-- fields' <- forM fields \(v, ty) -> (v,) <$> expr ty +-- methods <- forM defs \(ann, d) -> do +-- (WithSrc _ methodName, lam) <- aDef d +-- return (ann, methodName, Abs (WithSrcB sid (UBindSource "self")) lam) +-- return $ UStructDecl (fromSourceNameW name) (UStructDef (withoutSrc name) (givens' >>> params') fields' methods) +-- CInterface name params methods -> do +-- params' <- aExplicitParams params +-- (methodNames, methodTys) <- unzip <$> forM methods \(methodName, ty) -> do +-- ty' <- expr ty +-- return (fromSourceNameW methodName, ty') +-- return $ UInterface params' methodTys (fromSourceNameW name) (toNest methodNames) +-- CInstanceDecl def -> aInstanceDef def decl :: LetAnn -> CSDeclW -> SyntaxM (UDecl VoidS VoidS) decl ann (WithSrcs sid _ d) = WithSrcB sid <$> case d of @@ -145,21 +143,22 @@ decl ann (WithSrcs sid _ d) = WithSrcB sid <$> case d of CExpr g -> UExprDecl <$> expr g CPass -> return UPass -aInstanceDef :: CInstanceDef -> SyntaxM (UTopDecl VoidS VoidS) -aInstanceDef (CInstanceDef (WithSrc clNameId clName) args givens methods instNameAndParams) = do - let clName' = SourceName clNameId clName - args' <- mapM expr args - givens' <- aOptGivens givens - methods' <- catMaybes <$> mapM aMethod methods - case instNameAndParams of - Nothing -> return $ UInstance clName' givens' args' methods' NothingB ImplicitApp - Just (WithSrc sid instName, optParams) -> do - let instName' = JustB $ WithSrcB sid $ UBindSource instName - case optParams of - Just params -> do - params' <- aExplicitParams params - return $ UInstance clName' (givens' >>> params') args' methods' instName' ExplicitApp - Nothing -> return $ UInstance clName' givens' args' methods' instName' ImplicitApp +aInstanceDef :: CInstanceDef -> SyntaxM UTopDecl +aInstanceDef = undefined +-- aInstanceDef (CInstanceDef (WithSrc clNameId clName) args givens methods instNameAndParams) = do +-- let clName' = SourceName clNameId clName +-- args' <- mapM expr args +-- givens' <- aOptGivens givens +-- methods' <- catMaybes <$> mapM aMethod methods +-- case instNameAndParams of +-- Nothing -> return $ UInstance clName' givens' args' methods' NothingB ImplicitApp +-- Just (WithSrc sid instName, optParams) -> do +-- let instName' = JustB $ WithSrcB sid $ UBindSource instName +-- case optParams of +-- Just params -> do +-- params' <- aExplicitParams params +-- return $ UInstance clName' (givens' >>> params') args' methods' instName' ExplicitApp +-- Nothing -> return $ UInstance clName' givens' args' methods' instName' ImplicitApp aDef :: CDef -> SyntaxM (SourceNameW, ULamExpr VoidS) aDef (CDef name params optRhs optGivens body) = do diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs index dc6b38677..d62405e5b 100644 --- a/src/lib/ConcreteSyntax.hs +++ b/src/lib/ConcreteSyntax.hs @@ -111,35 +111,15 @@ importModule = Misc . ImportModule . OrdinaryModule <$> do WithSrc _ s <- anyCaseName eol return s - -declareForeign :: Parser SourceBlock' -declareForeign = do - keyWord ForeignKW - foreignName <- strLit - b <- anyName - void $ label "type annotation" $ sym ":" - ty <- cGroup - eol - return $ DeclareForeign (fmap fromString foreignName) b ty - -declareCustomLinearization :: Parser SourceBlock' -declareCustomLinearization = do - zeros <- (keyWord CustomLinearizationSymbolicKW $> SymbolicZeros) - <|> (keyWord CustomLinearizationKW $> InstantiateZeros) - fun <- anyCaseName - linearization <- cGroup - eol - return $ DeclareCustomLinearization fun zeros linearization - consumeTillBreak :: Parser () consumeTillBreak = void $ manyTill anySingle $ eof <|> void (try (eol >> eol)) sourceBlock' :: Parser SourceBlock' sourceBlock' = proseBlock - <|> topLevelCommand + <|> importModule <|> liftM TopDecl topDecl - <|> topLetOrExpr <* eolf + <|> liftM TopDecl topLet <* eolf <|> hidden (some eol >> return (Misc EmptyLines)) <|> hidden (sc >> eol >> return (Misc CommentLine)) @@ -158,15 +138,6 @@ proseBlock :: Parser SourceBlock' proseBlock = label "prose block" $ char '\'' >> fmap (Misc . ProseBlock . fst) (withSource consumeTillBreak) -topLevelCommand :: Parser SourceBlock' -topLevelCommand = - importModule - <|> declareForeign - <|> declareCustomLinearization - -- <|> (Misc . QueryEnv <$> envQuery) - <|> explicitCommand - "top-level command" - _envQuery :: Parser EnvQuery _envQuery = error "not implemented" -- string ":debug" >> sc >> ( @@ -178,25 +149,6 @@ _envQuery = error "not implemented" -- rawName :: Parser RawName -- rawName = RawName <$> (fromString <$> anyName) <*> intLit -explicitCommand :: Parser SourceBlock' -explicitCommand = do - cmdName <- char ':' >> nameString - cmd <- case cmdName of - "p" -> return $ EvalExpr (Printed Nothing) - "pp" -> return $ EvalExpr (Printed (Just PrintHaskell)) - "pcodegen"-> return $ EvalExpr (Printed (Just PrintCodegen)) - "t" -> return $ GetType - "html" -> return $ EvalExpr RenderHtml - "export" -> ExportFun <$> nameString - _ -> fail $ "unrecognized command: " ++ show cmdName - b <- cBlock <* eolf - e <- case b of - ExprBlock e -> return e - IndentedBlock sid decls -> withSrcs $ return $ CDo $ IndentedBlock sid decls - return $ case (e, cmd) of - (WithSrcs sid _ (CLeaf (CIdentifier v)), GetType) -> Misc $ GetNameType (WithSrc sid v) - _ -> Command cmd e - type CDefBody = ([(SourceNameW, GroupW)], [(LetAnn, CDef)]) structDef :: Parser CTopDecl structDef = do @@ -253,13 +205,6 @@ nameAndType = do arg <- cGroup return (n, arg) -topLetOrExpr :: Parser SourceBlock' -topLetOrExpr = topLet >>= \case - WithSrcs _ _ (CSDecl ann (CExpr e)) -> do - when (ann /= PlainLet) $ fail "Cannot annotate expressions" - return $ Command (EvalExpr (Printed Nothing)) e - d -> return $ TopDecl d - topLet :: Parser CTopDeclW topLet = withSrcs do lAnn <- topLetAnn <|> return PlainLet diff --git a/src/lib/MTL1.hs b/src/lib/MTL1.hs index 44fb99206..d0eeefb6d 100644 --- a/src/lib/MTL1.hs +++ b/src/lib/MTL1.hs @@ -17,8 +17,7 @@ import Data.Foldable (toList) import Name import Err -import Types.Top (Env) -import Core (EnvReader (..), EnvExtender (..)) +-- import Types.Top (Env) import Util (SnocList (..), snoc, emptySnocList) class MonadTrans11 (t :: MonadKind1 -> MonadKind1) where @@ -69,27 +68,12 @@ instance Monoid1 w => MonadTrans11 (WriterT1 w) where lift11 = WrapWriterT1 . lift {-# INLINE lift11 #-} -instance (SinkableE w, Monoid1 w, EnvReader m) => EnvReader (WriterT1 w m) where - unsafeGetEnv = lift11 unsafeGetEnv - {-# INLINE unsafeGetEnv #-} - instance (SinkableE w, Monoid1 w, ScopeReader m) => ScopeReader (WriterT1 w m) where unsafeGetScope = lift11 unsafeGetScope {-# INLINE unsafeGetScope #-} getDistinct = lift11 getDistinct {-# INLINE getDistinct #-} -instance ( SinkableE w, Monoid1 w - , HoistableState w, EnvExtender m) - => EnvExtender (WriterT1 w m) where - refreshAbs ab cont = WriterT1 \s -> do - (ans, Abs b new) <- refreshAbs ab \b e -> do - (ans, new) <- runWriterT1From (sink s) $ cont b e - return (ans, Abs b new) - let new' = hoistState s b new - return (ans, s <> new') - {-# INLINE refreshAbs #-} - -------------------- ReaderT1 -------------------- newtype ReaderT1 (r :: E) (m :: MonadKind1) (n :: S) (a :: *) = @@ -115,11 +99,6 @@ instance (Monad1 m, Alternative1 m) => Alternative ((ReaderT1 r m) n) where ReaderT1 $ ReaderT \r -> m1 r <|> m2 r {-# INLINE (<|>) #-} - -instance (SinkableE r, EnvReader m) => EnvReader (ReaderT1 r m) where - unsafeGetEnv = lift11 unsafeGetEnv - {-# INLINE unsafeGetEnv #-} - instance (SinkableE r, ScopeReader m) => ScopeReader (ReaderT1 r m) where unsafeGetScope = lift11 unsafeGetScope {-# INLINE unsafeGetScope #-} @@ -130,10 +109,6 @@ instance (SinkableE r, ScopeExtender m) => ScopeExtender (ReaderT1 r m) where refreshAbsScope ab cont = ReaderT1 $ ReaderT \r -> do refreshAbsScope ab \b e -> runReaderT1 (sink r) $ cont b e -instance (SinkableE r, EnvExtender m) => EnvExtender (ReaderT1 r m) where - refreshAbs ab cont = ReaderT1 $ ReaderT \r -> do - refreshAbs ab \b e -> runReaderT1 (sink r) $ cont b e - instance (Monad1 m, Fallible (m n)) => Fallible (ReaderT1 r m n) where throwErr = lift11 . throwErr @@ -174,10 +149,6 @@ instance MonadTrans11 (StateT1 s) where lift11 = WrapStateT1 . lift {-# INLINE lift11 #-} -instance (SinkableE s, EnvReader m) => EnvReader (StateT1 s m) where - unsafeGetEnv = lift11 unsafeGetEnv - {-# INLINE unsafeGetEnv #-} - instance (SinkableE s, ScopeReader m) => ScopeReader (StateT1 s m) where unsafeGetScope = lift11 unsafeGetScope {-# INLINE unsafeGetScope #-} @@ -199,14 +170,6 @@ instance (Monad1 m, Alternative1 m) => Alternative ((StateT1 s m) n) where class HoistableState (s::E) where hoistState :: BindsNames b => s n -> b n l -> s l -> s n -instance (SinkableE s, EnvExtender m, HoistableState s) => EnvExtender (StateT1 s m) where - refreshAbs ab cont = StateT1 \s -> do - (ans, Abs b s') <- refreshAbs ab \b e -> do - (ans, s') <- flip runStateT1 (sink s) $ cont b e - return (ans, Abs b s') - let s'' = hoistState s b s' - return (ans, s'') - instance HoistableState (LiftE a) where hoistState _ _ (LiftE x) = LiftE x {-# INLINE hoistState #-} @@ -224,7 +187,7 @@ instance Show a => HoistableState (NameMap a) where newtype ScopedT1 (s :: E) (m :: MonadKind1) (n :: S) (a :: *) = WrapScopedT1 { runScopedT1' :: StateT1 s m n a } deriving ( Functor, Monad, MonadState (s n), MonadFail - , MonadTrans11, EnvReader, ScopeReader ) + , MonadTrans11, ScopeReader ) -- This is entirely standard, but we implement it explicitly to encourage GHC to inline. instance (Monad (m n), Applicative (m n)) => Applicative (ScopedT1 s m n) where @@ -246,11 +209,6 @@ runScopedT1 m s = fst <$> runStateT1 (runScopedT1' m) s deriving instance (Monad1 m, Fallible1 m) => Fallible (ScopedT1 s m n) deriving instance (Monad1 m, Catchable1 m) => Catchable (ScopedT1 s m n) -instance (SinkableE s, EnvExtender m) => EnvExtender (ScopedT1 s m) where - refreshAbs ab cont = ScopedT1 \s -> do - ans <- refreshAbs ab \b e -> flip runScopedT1 (sink s) $ cont b e - return (ans, s) - -------------------- MaybeT1 -------------------- newtype MaybeT1 (m :: MonadKind1) (n :: S) (a :: *) = @@ -272,20 +230,12 @@ instance Monad (m n) => MonadFail (MaybeT1 m n) where instance Monad (m n) => Fallible (MaybeT1 m n) where throwErr _ = empty -instance EnvReader m => EnvReader (MaybeT1 m) where - unsafeGetEnv = lift11 unsafeGetEnv - {-# INLINE unsafeGetEnv #-} - instance ScopeReader m => ScopeReader (MaybeT1 m) where unsafeGetScope = lift11 unsafeGetScope {-# INLINE unsafeGetScope #-} getDistinct = lift11 getDistinct {-# INLINE getDistinct #-} -instance EnvExtender m => EnvExtender (MaybeT1 m) where - refreshAbs ab cont = MaybeT1 $ MaybeT $ - refreshAbs ab \b e -> runMaybeT $ runMaybeT1' $ cont b e - -------------------- StreamWriter -------------------- class Monad m => StreamWriter w m | m -> w where @@ -293,7 +243,7 @@ class Monad m => StreamWriter w m | m -> w where newtype StreamWriterT1 (w:: *) (m::MonadKind1) (n::S) (a:: *) = StreamWriterT1 { runStreamWriterT1' :: StateT1 (LiftE (SnocList w)) m n a } - deriving (Functor, Applicative, Monad, MonadFail, MonadIO, ScopeReader, EnvReader) + deriving (Functor, Applicative, Monad, MonadFail, MonadIO, ScopeReader) instance Monad1 m => StreamWriter w (StreamWriterT1 w m n) where writeStream w = StreamWriterT1 $ modify (\(LiftE ws) -> LiftE (ws `snoc` w)) @@ -312,7 +262,7 @@ class Monad m => StreamReader r m | m -> r where newtype StreamReaderT1 (r:: *) (m::MonadKind1) (n::S) (a:: *) = StreamReaderT1 { runStreamReaderT1' :: StateT1 (LiftE [r]) m n a } - deriving (Functor, Applicative, Monad, MonadFail, MonadIO, ScopeReader, EnvReader, MonadTrans11) + deriving (Functor, Applicative, Monad, MonadFail, MonadIO, ScopeReader, MonadTrans11) instance Monad1 m => StreamReader r (StreamReaderT1 r m n) where readStream = StreamReaderT1 $ state \(LiftE rs) -> @@ -327,89 +277,3 @@ runStreamReaderT1 rs m = do return (ans, rsRemaining) {-# INLINE runStreamReaderT1 #-} --------------------- DiffState -------------------- - -class MonoidE (d::E) where - emptyE :: d n - catE :: d n -> d n -> d n - -class MonoidE d => DiffStateE (s::E) (d::E) where - updateDiffStateE :: Distinct n => Env n -> s n -> d n -> s n - -newtype DiffStateT1 (s::E) (d::E) (m::MonadKind1) (n::S) (a:: *) = - DiffStateT1' { runDiffStateT1'' :: StateT (s n, d n) (m n) a } - deriving ( Functor, Applicative, Monad, MonadFail, MonadIO - , Fallible, Catchable) - -pattern DiffStateT1 :: ((s n, d n) -> m n (a, (s n, d n))) -> DiffStateT1 s d m n a -pattern DiffStateT1 cont = DiffStateT1' (StateT cont) - -diffStateT1 - :: (EnvReader m, DiffStateE s d, MonoidE d) - => (s n -> m n (a, d n)) -> DiffStateT1 s d m n a -diffStateT1 cont = DiffStateT1 \(s, d) -> do - (ans, d') <- cont s - env <- unsafeGetEnv - Distinct <- getDistinct - return (ans, (updateDiffStateE env s d', catE d d')) -{-# INLINE diffStateT1 #-} - -runDiffStateT1 - :: (EnvReader m, DiffStateE s d, MonoidE d) - => s n -> DiffStateT1 s d m n a -> m n (a, d n) -runDiffStateT1 s (DiffStateT1' (StateT cont)) = do - (ans, (_, d)) <- cont (s, emptyE) - return (ans, d) -{-# INLINE runDiffStateT1 #-} - -class (Monad1 m, MonoidE d) - => MonadDiffState1 (m::MonadKind1) (s::E) (d::E) | m -> s, m -> d where - withDiffState :: s n -> m n a -> m n (a, d n) - updateDiffStateM :: d n -> m n () - getDiffState :: m n (s n) - -instance (EnvReader m, DiffStateE s d, MonoidE d) => MonadDiffState1 (DiffStateT1 s d m) s d where - getDiffState = DiffStateT1' $ fst <$> get - {-# INLINE getDiffState #-} - - withDiffState s cont = DiffStateT1' do - (sOld, dOld) <- get - put (s, emptyE) - ans <- runDiffStateT1'' cont - (_, dLocal) <- get - put (sOld, dOld) - return (ans, dLocal) - {-# INLINE withDiffState #-} - - updateDiffStateM d = DiffStateT1' do - (s, d') <- get - env <- lift unsafeGetEnv - Distinct <- lift getDistinct - put (updateDiffStateE env s d, catE d d') - {-# INLINE updateDiffStateM #-} - -instance MonoidE (ListE e) where - emptyE = mempty - catE = (<>) - -instance MonoidE (RListE e) where - emptyE = mempty - catE = (<>) - -instance (Monad1 m, Alternative1 m, MonoidE d) => Alternative ((DiffStateT1 s d m) n) where - empty = DiffStateT1' $ StateT \_ -> empty - {-# INLINE empty #-} - DiffStateT1' (StateT m1) <|> DiffStateT1' (StateT m2) = DiffStateT1' $ StateT \s -> - m1 s <|> m2 s - {-# INLINE (<|>) #-} - -instance (ScopeReader m, MonoidE d) => ScopeReader (DiffStateT1 s d m) where - unsafeGetScope = lift11 unsafeGetScope - getDistinct = lift11 getDistinct - -instance (EnvReader m, MonoidE d) => EnvReader (DiffStateT1 s d m) where - unsafeGetEnv = lift11 unsafeGetEnv - -instance MonadTrans11 (DiffStateT1 s d) where - lift11 m = DiffStateT1' $ lift m - {-# INLINE lift11 #-} diff --git a/src/lib/QueryType.hs b/src/lib/QueryType.hs deleted file mode 100644 index 6d1e1397c..000000000 --- a/src/lib/QueryType.hs +++ /dev/null @@ -1,276 +0,0 @@ --- Copyright 2022 Google LLC --- --- Use of this source code is governed by a BSD-style --- license that can be found in the LICENSE file or at --- https://developers.google.com/open-source/licenses/bsd - -module QueryType (module QueryType, module QueryTypePure, toAtomVar) where - -import Control.Category ((>>>)) -import Control.Monad -import Control.Applicative -import Data.List (elemIndex) -import Data.Maybe (fromJust) -import Data.Functor ((<&>)) - -import Types.Primitives -import Types.Core -import Types.Source hiding (TCName (..)) -import Types.Top -import Types.Imp -import Core -import Name hiding (withFreshM) -import Subst -import Util -import PPrint -import QueryTypePure -import CheapReduction - --- === Exposed helpers for querying types and effects === - -caseAltsBinderTys :: EnvReader m => Type n -> m n [Type n] -caseAltsBinderTys ty = case ty of - TyCon (SumType types) -> return types -- need this case? - TyCon (NewtypeTyCon t) -> case t of - UserADTType _ defName params -> do - def <- lookupTyCon defName - ~(ADTCons cons) <- instantiateTyConDef def params - return [repTy | DataConDef _ _ repTy _ <- cons] - _ -> error msg - _ -> error msg - where msg = "Case analysis only supported on ADTs, not on " ++ pprint ty - -piTypeWithoutDest :: PiType n -> PiType n -piTypeWithoutDest (PiType bsRefB _) = - case popNest bsRefB of - Just (PairB bs (_:>RefTy ansTy)) -> PiType bs ansTy - _ -> error "expected trailing dest binder" - -typeOfTabApp :: EnvReader m => Type n -> Atom n -> m n (Type n) -typeOfTabApp (TyCon (TabPi tabTy)) i = instantiate tabTy [i] -typeOfTabApp ty _ = error $ "expected a table type. Got: " ++ pprint ty - -typeOfApplyMethod :: EnvReader m => CDict n -> Int -> [CAtom n] -> m n (EffTy n) -typeOfApplyMethod d i args = do - ty <- toType <$> getMethodType d i - appEffTy ty args - -typeOfTopApp :: EnvReader m => TopFunName n -> [SAtom n] -> m n (EffTy n) -typeOfTopApp f xs = do - piTy <- getTypeTopFun f - ty <- instantiate piTy xs - return $ EffTy undefined ty -- TODO - -typeOfIndexRef :: (EnvReader m, Fallible1 m) => Type n -> Atom n -> m n (Type n) -typeOfIndexRef (TyCon (RefType s)) i = do - TyCon (TabPi tabPi) <- return s - eltTy <- instantiate tabPi [i] - return $ toType $ RefType eltTy -typeOfIndexRef _ _ = error "expected a ref type" - -typeOfProjRef :: EnvReader m => Type n -> Projection -> m n (Type n) -typeOfProjRef (TyCon (RefType s)) p = do - toType . RefType <$> case p of - ProjectProduct i -> do - ~(TyCon (ProdType tys)) <- return s - return $ tys !! i - UnwrapNewtype -> do - case s of - TyCon (NewtypeTyCon tc) -> snd <$> unwrapNewtypeType tc - _ -> error "expected a newtype" -typeOfProjRef _ _ = error "expected a reference" - -appEffTy :: EnvReader m => Type n -> [Atom n] -> m n (EffTy n) -appEffTy (TyCon (Pi piTy)) xs = do - ty <- instantiate piTy xs - return $ EffTy Effectful ty -- TODO: don't assume Effectful -appEffTy t _ = error $ "expected a pi type, got: " ++ pprint t - -partialAppType :: EnvReader m => Type n -> [Atom n] -> m n (Type n) -partialAppType (TyCon (Pi (CorePiType appExpl expls bs effTy))) xs = do - (_, expls2) <- return $ splitAt (length xs) expls - PairB bs1 bs2 <- return $ splitNestAt (length xs) bs - instantiate (Abs bs1 (toType $ CorePiType appExpl expls2 bs2 effTy)) xs -partialAppType _ _ = error "expected a pi type" - -effTyOfHof :: EnvReader m => Hof n -> m n (EffTy n) -effTyOfHof hof = EffTy <$> hofEffects hof <*> typeOfHof hof - -typeOfHof :: EnvReader m => Hof n -> m n (Type n) -typeOfHof = \case - For _ ixTy f -> getLamExprType f >>= \case - PiType (UnaryNest b) eltTy -> return $ TabTy (ixTypeDict ixTy) b eltTy - _ -> error "expected a unary pi type" - While _ -> return UnitTy - Linearize f _ -> getLamExprType f >>= \case - PiType (UnaryNest (binder:>a)) b -> do - let b' = ignoreHoistFailure $ hoist binder b - let fLinTy = toType $ nonDepPiType [a] b' - return $ PairTy b' fLinTy - _ -> error "expected a unary pi type" - Transpose f _ -> getLamExprType f >>= \case - PiType (UnaryNest (_:>a)) _ -> return a - _ -> error "expected a unary pi type" - -hofEffects :: EnvReader m => Hof n -> m n (Effects n) -hofEffects = \case - For _ _ _ -> undefined -- TODO - While body -> return $ getEffects body - Linearize _ _ -> return Pure -- Body has to be a pure function - Transpose _ _ -> return Pure -- Body has to be a pure function - -getMethodIndex :: EnvReader m => ClassName n -> SourceName -> m n Int -getMethodIndex className methodSourceName = do - ClassDef _ _ methodNames _ _ _ _ _ <- lookupClassDef className - case elemIndex methodSourceName methodNames of - Nothing -> error $ pprint methodSourceName ++ " is not a method of " ++ pprint className - Just i -> return i -{-# INLINE getMethodIndex #-} - -getUVarType :: EnvReader m => UVar n -> m n (CType n) -getUVarType = undefined - -getMethodNameType :: EnvReader m => MethodName n -> m n (CType n) -getMethodNameType v = liftEnvReaderM $ lookupEnv v >>= \case - MethodBinding className i -> do - ClassDef _ _ _ paramNames _ paramBs scBinders methodTys <- lookupClassDef className - refreshAbs (Abs paramBs $ Abs scBinders (methodTys !! i)) \paramBs' absPiTy -> do - let params = toAtom <$> bindersVars paramBs' - dictTy <- toType <$> dictType (sink className) params - withFreshBinder noHint dictTy \dictB -> do - scDicts <- getSuperclassDicts (toDict $ binderVar dictB) - CorePiType appExpl methodExpls methodBs effTy <- instantiate (sink absPiTy) scDicts - let paramExpls = paramNames <&> \name -> Inferred name Unify - let expls = paramExpls <> [Inferred Nothing (Synth $ Partial $ succ i)] <> methodExpls - return $ toType $ CorePiType appExpl expls (paramBs' >>> UnaryNest dictB >>> methodBs) effTy - -getMethodType :: EnvReader m => CDict n -> Int -> m n (CorePiType n) -getMethodType dict i = do - ~(TyCon (DictTy dictTy)) <- return $ getType dict - case dictTy of - DictType _ className params -> liftEnvReaderM $ withSubstReaderT do - superclassDicts <- getSuperclassDicts dict - classDef <- lookupClassDef className - withInstantiated classDef params \ab -> do - withInstantiated ab superclassDicts \(ListE methodTys) -> - substM $ methodTys !! i - IxDictType ixTy -> liftEnvReaderM case i of - 0 -> mkCorePiType [] NatTy -- size' : () -> Nat - 1 -> mkCorePiType [ixTy] NatTy -- ordinal : (n) -> Nat - 2 -> mkCorePiType [NatTy] ixTy -- unsafe_from_ordinal : (Nat) -> n - _ -> error "Ix only has three methods" - -mkCorePiType :: EnvReader m => [CType n] -> CType n -> m n (CorePiType n) -mkCorePiType argTys resultTy = liftEnvReaderM $ withFreshBinders argTys \bs _ -> do - expls <- return $ nestToList (const Explicit) bs - return $ CorePiType ExplicitApp expls bs (sink resultTy) - -getTyConNameType :: EnvReader m => TyConName n -> m n (Type n) -getTyConNameType v = do - TyConDef _ expls bs _ <- lookupTyCon v - case bs of - Empty -> return $ toType $ Kind TypeKind - _ -> return $ toType $ CorePiType ExplicitApp expls bs $ toType $ Kind TypeKind - -getDataConNameType :: EnvReader m => DataConName n -> m n (Type n) -getDataConNameType dataCon = liftEnvReaderM $ withSubstReaderT do - (tyCon, i) <- lookupDataCon dataCon - tyConDef <- lookupTyCon tyCon - buildDataConType tyConDef \expls paramBs' paramVs params -> do - withInstantiatedNames tyConDef paramVs \(ADTCons dataCons) -> do - DataConDef _ ab _ _ <- renameM (dataCons !! i) - refreshAbs ab \dataBs UnitE -> do - let appExpl = case dataBs of Empty -> ImplicitApp - _ -> ExplicitApp - let resultTy = toType $ UserADTType (getSourceName tyConDef) (sink tyCon) (sink params) - let dataExpls = nestToList (const $ Explicit) dataBs - return $ toType $ CorePiType appExpl (expls <> dataExpls) (paramBs' >>> dataBs) resultTy - -getStructDataConType :: EnvReader m => TyConName n -> m n (CType n) -getStructDataConType tyCon = liftEnvReaderM $ withSubstReaderT do - tyConDef <- lookupTyCon tyCon - buildDataConType tyConDef \expls paramBs' paramVs params -> do - withInstantiatedNames tyConDef paramVs \(StructFields fields) -> do - fieldTys <- forM fields \(_, t) -> renameM t - let resultTy = toType $ UserADTType (getSourceName tyConDef) (sink tyCon) params - Abs dataBs resultTy' <- return $ typesAsBinderNest fieldTys resultTy - let dataExpls = nestToList (const Explicit) dataBs - return $ toType $ CorePiType ExplicitApp (expls <> dataExpls) (paramBs' >>> dataBs) resultTy' - -buildDataConType - :: (EnvReader m, EnvExtender m) - => TyConDef n - -> (forall l. DExt n l => [Explicitness] -> Nest CBinder n l -> [CAtomName l] -> TyConParams l -> m l a) - -> m n a -buildDataConType (TyConDef _ expls bs _) cont = do - expls' <- forM expls \case - Explicit -> return $ Inferred Nothing Unify - expl -> return $ expl - refreshAbs (Abs bs UnitE) \bs' UnitE -> do - let vs = nestToNames bs' - vs' <- mapM toAtomVar vs - cont expls' bs' vs $ TyConParams expls (toAtom <$> vs') - -makeTyConParams :: EnvReader m => TyConName n -> [CAtom n] -> m n (TyConParams n) -makeTyConParams tc params = do - TyConDef _ expls _ _ <- lookupTyCon tc - return $ TyConParams expls params - -dictType :: EnvReader m => ClassName n -> [CAtom n] -> m n (DictType n) -dictType className params = do - ClassDef sourceName builtinName _ _ _ _ _ _ <- lookupClassDef className - return case builtinName of - Just Ix -> IxDictType singleTyParam - Nothing -> DictType sourceName className params - where singleTyParam = case params of - [p] -> fromJust $ toMaybeType p - _ -> error "not a single type param" - -makePreludeMaybeTy :: EnvReader m => CType n -> m n (CType n) -makePreludeMaybeTy ty = do - ~(Just tyConName) <- lookupSourceMap "Maybe" - let params = TyConParams [Explicit] [toAtom ty] - return $ toType $ UserADTType "Maybe" tyConName params - -getLamExprType :: EnvReader m => LamExpr n -> m n (PiType n) -getLamExprType (LamExpr bs body) = return $ PiType bs (getType body) - -getSuperclassDicts :: EnvReader m => CDict n -> m n ([CAtom n]) -getSuperclassDicts dict = do - case getType dict of - TyCon (DictTy dTy) -> do - ts <- getSuperclassTys dTy - forM (enumerate ts) \(i, _) -> reduceSuperclassProj i dict - _ -> error "expected a dict type" - -getSuperclassTys :: EnvReader m => DictType n -> m n [CType n] -getSuperclassTys = \case - DictType _ className params -> do - ClassDef _ _ _ _ _ bs superclasses _ <- lookupClassDef className - forM [0 .. nestLength superclasses - 1] \i -> do - instantiate (Abs bs $ getSuperclassType REmpty superclasses i) params - IxDictType _ -> return [] - -getTypeTopFun :: EnvReader m => TopFunName n -> m n (PiType n) -getTypeTopFun f = lookupTopFun f >>= \case - DexTopFun _ (TopLam _ piTy _) _ -> return piTy - FFITopFun _ iTy -> liftIFunType iTy - -asTopLam :: EnvReader m => LamExpr n -> m n (TopLam n) -asTopLam lam = do - piTy <- getLamExprType lam - return $ TopLam False piTy lam - -liftIFunType :: EnvReader m => IFunType -> m n (PiType n) -liftIFunType (IFunType _ argTys resultTys) = liftEnvReaderM $ go argTys where - go :: [BaseType] -> EnvReaderM n (PiType n) - go = \case - [] -> return $ PiType Empty resultTy - where resultTy = case resultTys of - [] -> UnitTy - [t] -> toType $ BaseType t - [t1, t2] -> TyCon (ProdType [toType $ BaseType t1, toType $ BaseType t2]) - _ -> error $ "Not a valid FFI return type: " ++ pprint resultTys - t:ts -> withFreshBinder noHint (toType $ BaseType t) \b -> do - PiType bs effTy <- go ts - return $ PiType (Nest b bs) effTy diff --git a/src/lib/QueryTypePure.hs b/src/lib/QueryTypePure.hs index e4d24e071..57e9c7e5d 100644 --- a/src/lib/QueryTypePure.hs +++ b/src/lib/QueryTypePure.hs @@ -9,35 +9,14 @@ module QueryTypePure where import Types.Primitives import Types.Simple import Types.Complicated -import Types.Top +import Types.Top2 import Name class HasType (e::E) where getType :: e n -> Type n -class HasEffects (e::E) where - getEffects :: e n -> Effects n - -getTyCon :: HasType e => e n -> TyCon n -getTyCon e = con where TyCon con = getType e - -isPure :: HasEffects e => e n -> Bool -isPure e = case getEffects e of - Pure -> True - Effectful -> False - -- === querying types implementation === -instance HasType AtomBinding where - getType = \case - LetBound (DeclBinding _ e) -> getType e - MiscBound ty -> ty - SolverBound (InfVarBound ty) -> ty - SolverBound (SkolemBound ty) -> ty - SolverBound (DictBound ty) -> ty - NoinlineFun ty _ -> ty - FFIFunBound piTy _ -> TyCon $ Pi piTy - litType :: LitVal -> BaseType litType v = case v of Int64Lit _ -> Scalar Int64Type @@ -67,59 +46,54 @@ typeUnOp :: UnOp -> BaseType -> BaseType typeUnOp = const id -- All unary ops preserve the type of the input getKind :: Type n -> Kind -getKind = \case - StuckTy k _ -> k - TyCon con -> case con of - BaseType _ -> TypeKind - ProdType _ -> TypeKind - SumType _ -> TypeKind - TabPi _ -> TypeKind - DepPairTy _ -> TypeKind - NewtypeTyCon _ -> TypeKind - RefType _ -> RefKind - Pi _ -> FunKind - DictTy _ -> DictKind - Kind _ -> OtherKind - -instance HasType AtomVar where - getType (AtomVar _ ty) = ty - {-# INLINE getType #-} +getKind = undefined +-- getKind = \case +-- StuckTy k _ -> k +-- TyCon con -> case con of +-- BaseType _ -> TypeKind +-- ProdType _ -> TypeKind +-- SumType _ -> TypeKind +-- TabPi _ -> TypeKind +-- DepPairTy _ -> TypeKind +-- NewtypeTyCon _ -> TypeKind +-- RefType _ -> RefKind +-- Pi _ -> FunKind +-- DictTy _ -> DictKind +-- Kind _ -> OtherKind instance HasType Atom where - getType = \case - Stuck t _ -> t - Con e -> getType e - -instance HasType Dict where - getType = \case - StuckDict t _ -> t - DictCon e -> getType e + getType = undefined + -- getType = \case + -- Stuck t _ -> t + -- Con e -> getType e instance HasType DictCon where - getType = \case - InstanceDict t _ _ -> t - IxFin n -> toType $ IxDictType (FinTy n) - IxRawFin _ -> toType $ IxDictType IdxRepTy + getType = undefined + -- getType = \case + -- InstanceDict t _ _ -> t + -- IxFin n -> toType $ IxDictType (FinTy n) instance HasType NewtypeTyCon where - getType _ = TyCon $ Kind TypeKind + getType _ = undefined -- TyCon $ Kind TypeKind getNewtypeType :: NewtypeCon n -> CType n -getNewtypeType con = case con of - NatCon -> TyCon $ NewtypeTyCon Nat - FinCon n -> TyCon $ NewtypeTyCon $ Fin n - UserADTData sn d xs -> TyCon $ NewtypeTyCon $ UserADTType sn d xs - -instance HasType Con where - getType = \case - Lit l -> toType $ BaseType $ litType l - ProdCon xs -> toType $ ProdType $ map getType xs - SumCon tys _ _ -> toType $ SumType tys - Lam (CoreLamExpr piTy _) -> toType $ Pi piTy - DepPair _ _ ty -> toType $ DepPairTy ty - DictConAtom d -> getType d - NewtypeCon con _ -> getNewtypeType con - TyConAtom k -> TyCon $ Kind $ getKind $ TyCon k +getNewtypeType con = undefined +-- getNewtypeType con = case con of +-- NatCon -> TyCon $ NewtypeTyCon Nat +-- FinCon n -> TyCon $ NewtypeTyCon $ Fin n +-- UserADTData sn d xs -> TyCon $ NewtypeTyCon $ UserADTType sn d xs + +-- instance HasType Con where +-- getType = undefined + -- getType = \case + -- Lit l -> toType $ BaseType $ litType l + -- ProdCon xs -> toType $ ProdType $ map getType xs + -- SumCon tys _ _ -> toType $ SumType tys + -- Lam (CoreLamExpr piTy _) -> toType $ Pi piTy + -- DepPair _ _ ty -> toType $ DepPairTy ty + -- DictConAtom d -> getType d + -- NewtypeCon con _ -> getNewtypeType con + -- TyConAtom k -> TyCon $ Kind $ getKind $ TyCon k getSuperclassType :: RNest CBinder n l -> Nest CBinder l l' -> Int -> CType n getSuperclassType _ Empty = error "bad index" @@ -128,27 +102,20 @@ getSuperclassType bsAbove (Nest b@(_:>t) bs) = \case i -> getSuperclassType (RNest bsAbove b) bs (i-1) instance HasType Expr where - 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 - -instance HasType RepVal where - getType (RepVal ty _) = ty - -getTypeBaseType :: HasType e => e n -> BaseType -getTypeBaseType e = case getType e of - TyCon (BaseType b) -> b - ty -> error $ "Expected a base type. Got: " ++ show ty + 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 -- instance HasType MemOp where -- getType = \case @@ -159,98 +126,3 @@ getTypeBaseType e = case getType e of -- let PtrTy (_, t) = getType ptr -- toType $ BaseType t -- PtrStore _ _ -> UnitTy - -rawStrType :: Type n -rawStrType = case newName "n" of - Abs b v -> do - let tabTy = rawFinTabType (toAtom $ AtomVar v IdxRepTy) CharRepTy - TyCon $ DepPairTy $ DepPairType ExplicitDepPair (b:>IdxRepTy) tabTy - --- `n` argument is IdxRepVal, not Nat -rawFinTabType :: Atom n -> Type n -> Type n -rawFinTabType n eltTy = IxType IdxRepTy (DictCon (IxRawFin n)) ==> eltTy - -tabIxType :: TabPiType n -> IxType n -tabIxType (TabPiType d (_:>t) _) = IxType t d - -typesAsBinderNest - :: (SinkableE e, HoistableE e) - => [Type n] -> e n -> Abs (Nest Binder) e n -typesAsBinderNest types body = toConstBinderNest types body - -nonDepPiType :: [CType n] -> CType n -> CorePiType n -nonDepPiType argTys resultTy = case typesAsBinderNest argTys resultTy of - Abs bs resultTy' -> do - let expls = nestToList (const Explicit) bs - CorePiType ExplicitApp expls bs resultTy' - -nonDepTabPiType :: IxType n -> Type n -> TabPiType n -nonDepTabPiType (IxType t d) resultTy = - case toConstAbsPure resultTy of - Abs b resultTy' -> TabPiType d (b:>t) resultTy' - -corePiTypeToPiType :: CorePiType n -> PiType n -corePiTypeToPiType (CorePiType _ _ bs effTy) = PiType bs effTy - -coreLamToTopLam :: CoreLamExpr n -> TopLam n -coreLamToTopLam (CoreLamExpr ty f) = TopLam False (corePiTypeToPiType ty) f - -(==>) :: IxType n -> Type n -> Type n -a ==> b = TyCon $ TabPi $ nonDepTabPiType a b - -litFinIxTy :: Int -> IxType n -litFinIxTy n = finIxTy $ IdxRepVal $ fromIntegral n - -finIxTy :: Atom n -> IxType n -finIxTy n = IxType IdxRepTy (DictCon (IxRawFin n)) - --- === querying effects implementation === - -instance HasEffects Expr where - getEffects = \case - Atom _ -> Pure - Block (EffTy eff _) _ -> eff - App (EffTy eff _) _ _ -> eff - TopApp (EffTy eff _) _ _ -> eff - TabApp _ _ _ -> Pure - Case _ _ (EffTy effs _) -> effs - TabCon _ _ -> Pure - ApplyMethod (EffTy eff _) _ _ _ -> eff - -- PrimOp _ primOp -> getEffects primOp - Project _ _ _ -> Pure - Unwrap _ _ -> Pure - Hof (TypedHof (EffTy eff _) _) -> eff - -instance HasEffects DeclBinding where - getEffects (DeclBinding _ expr) = getEffects expr - {-# INLINE getEffects #-} - --- instance HasEffects PrimOp r where --- getEffects = \case --- UnOp _ _ -> Pure --- BinOp _ _ _ -> Pure --- VectorOp _ -> Pure --- MemOp op -> case op of --- IOAlloc _ -> Effectful --- IOFree _ -> Effectful --- PtrLoad _ -> Effectful --- PtrStore _ _ -> Effectful --- PtrOffset _ _ -> Pure --- MiscOp op -> case op of --- Select _ _ _ -> Pure --- ThrowError -> Pure --- CastOp _ -> Pure --- UnsafeCoerce _ -> Pure --- GarbageVal -> Pure --- BitcastOp _ -> Pure --- SumTag _ -> Pure --- ToEnum _ -> Pure --- OutputStream -> Pure --- ShowAny _ -> Pure --- ShowScalar _ -> Pure --- RefOp _ m -> case m of --- MGet -> Effectful --- MPut _ -> Effectful --- IndexRef _ -> Pure --- ProjRef _ -> Pure --- {-# INLINE getEffects #-} diff --git a/src/lib/SourceIdTraversal.hs b/src/lib/SourceIdTraversal.hs index d030ab664..85dfe0bfb 100644 --- a/src/lib/SourceIdTraversal.hs +++ b/src/lib/SourceIdTraversal.hs @@ -52,9 +52,6 @@ class IsTree a where instance IsTree SourceBlock' where visit = \case TopDecl decl -> visit decl - Command _ g -> visit g - DeclareForeign v1 v2 g -> visit v1 >> visit v2 >> visit g - DeclareCustomLinearization v _ g -> visit v >> visit g Misc _ -> return () UnParseable _ _ -> return () diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs index 3c0b7d24b..4bf8d907f 100644 --- a/src/lib/SourceRename.hs +++ b/src/lib/SourceRename.hs @@ -6,8 +6,7 @@ {-# LANGUAGE UndecidableInstances #-} -module SourceRename ( renameSourceNamesTopUDecl, uDeclErrSourceMap - , renameSourceNamesUExpr ) where +module SourceRename ( renameSourceNames ) where import Prelude hiding (id, (.)) import Control.Category @@ -18,44 +17,44 @@ import qualified Data.Map.Strict as M import Err import Name -import Core (EnvReader (..), withEnv, lookupSourceMapPure) import MonadUtil import MTL1 import PPrint import Types.Source import Types.Primitives -import Types.Top - -renameSourceNamesTopUDecl - :: (Fallible1 m, EnvReader m, TopLogger1 m) - => TopNameDescription -> UTopDecl VoidS VoidS -> m n (Abs UTopDecl SourceMap n) -renameSourceNamesTopUDecl desc decl = do - Distinct <- getDistinct - Abs renamedDecl sourceMapLocalNames <- liftRenamer $ sourceRenameTopUDecl decl - let sourceMap = SourceMap $ fmap (fmap (\(LocalVar _ v) -> ModuleVar desc (Just v))) $ - fromSourceMap sourceMapLocalNames - return $ Abs renamedDecl sourceMap -{-# SCC renameSourceNamesTopUDecl #-} - -uDeclErrSourceMap:: TopNameDescription -> UTopDecl VoidS VoidS -> SourceMap n -uDeclErrSourceMap desc decl = - SourceMap $ M.fromSet (const [ModuleVar desc Nothing]) (sourceNames decl) +import Types.Top2 + +renameSourceNames + :: (Fallible1 m, ScopeReader m, TopLogger1 m) + => TopNameDescription -> UTopDecl -> m n () -- (Abs UTopDecl SourceMap n) +renameSourceNames desc decl = undefined +-- renameSourceNamesTopUDecl desc decl = do +-- Distinct <- getDistinct +-- Abs renamedDecl sourceMapLocalNames <- liftRenamer $ sourceRenameTopUDecl decl +-- let sourceMap = SourceMap $ fmap (fmap (\(LocalVar _ v) -> ModuleVar desc (Just v))) $ +-- fromSourceMap sourceMapLocalNames +-- return $ Abs renamedDecl sourceMap +-- {-# SCC renameSourceNamesTopUDecl #-} + +uDeclErrSourceMap:: TopNameDescription -> UTopDecl -> SourceMap n +uDeclErrSourceMap desc decl = undefined + -- SourceMap $ M.fromSet (const [ModuleVar desc Nothing]) (sourceNames decl) {-# SCC uDeclErrSourceMap #-} -renameSourceNamesUExpr :: (Fallible1 m, EnvReader m, TopLogger1 m) => UExpr VoidS -> m n (UExpr n) +renameSourceNamesUExpr :: (Fallible1 m, ScopeReader m, TopLogger1 m) => UExpr VoidS -> m n (UExpr n) renameSourceNamesUExpr expr = do Distinct <- getDistinct liftRenamer $ sourceRenameE expr {-# SCC renameSourceNamesUExpr #-} -sourceRenameTopUDecl - :: (Renamer m, Distinct o) - => UTopDecl i i' -> m o (Abs UTopDecl SourceMap o) -sourceRenameTopUDecl udecl = - sourceRenameB udecl \udecl' -> do - SourceMap fullSourceMap <- askSourceMap - let partialSourceMap = fullSourceMap `M.restrictKeys` sourceNames udecl - return $ Abs udecl' $ SourceMap partialSourceMap +-- sourceRenameTopUDecl +-- :: (Renamer m, Distinct o) +-- => UTopDecl i i' -> m o (Abs UTopDecl SourceMap o) +-- sourceRenameTopUDecl udecl = +-- sourceRenameB udecl \udecl' -> do +-- SourceMap fullSourceMap <- askSourceMap +-- let partialSourceMap = fullSourceMap `M.restrictKeys` sourceNames udecl +-- return $ Abs udecl' $ SourceMap partialSourceMap data RenamerSubst n = RenamerSubst { renamerSourceMap :: SourceMap n , renamerMayShadow :: Bool } @@ -65,14 +64,15 @@ newtype RenamerM (n::S) (a:: *) = deriving ( Functor, Applicative, Monad, MonadFail, Fallible , ScopeReader, ScopeExtender) -liftRenamer :: (EnvReader m, Fallible1 m, SinkableE e, TopLogger1 m) => RenamerM n (e n) -> m n (e n) -liftRenamer cont = do - sm <- withEnv $ envSourceMap . moduleEnv - Distinct <- getDistinct - m <- liftScopeReaderT $ runReaderT1 (RenamerSubst sm False) $ runRenamerM $ cont - let (ans, namingInfo) = runState (runExceptT m) mempty - emitLog $ Outputs [SourceInfo $ SINamingInfo namingInfo] - liftExcept ans +liftRenamer :: (ScopeReader m, Fallible1 m, SinkableE e, TopLogger1 m) => RenamerM n (e n) -> m n (e n) +liftRenamer cont = undefined +-- liftRenamer cont = do +-- sm <- withEnv $ envSourceMap . moduleEnv +-- Distinct <- getDistinct +-- m <- liftScopeReaderT $ runReaderT1 (RenamerSubst sm False) $ runRenamerM $ cont +-- let (ans, namingInfo) = runState (runExceptT m) mempty +-- emitLog $ Outputs [SourceInfo $ SINamingInfo namingInfo] +-- liftExcept ans class ( Monad1 m, ScopeReader m , ScopeExtender m, Fallible1 m) => Renamer m where @@ -95,6 +95,9 @@ instance Renamer RenamerM where let newNameInfo = M.insert sid info curNameInfo RenamerM $ lift11 $ lift1 $ lift $ put $ NamingInfo newNameInfo +class SourceRenamableTop a where + sourceRenameTop :: Renamer m => a -> m VoidS a + class SourceRenamableE e where sourceRenameE :: (Distinct o, Renamer m) => e i -> m o (e o) @@ -105,19 +108,20 @@ class SourceRenamableB (b :: B) where -> m o a lookupSourceName :: Renamer m => SrcId -> SourceName -> m n (Name n) -lookupSourceName sid v = do - sm <- askSourceMap - case lookupSourceMapPure sm v of - [] -> throw sid $ UnboundVarErr $ pprint v - LocalVar binderSid v' : _ -> do - emitNameInfo sid $ LocalOcc binderSid - return v' - [ModuleVar desc maybeV] -> case maybeV of - Just v' -> do - emitNameInfo sid $ TopOcc (pprint desc) - return v' - Nothing -> throw sid $ VarDefErr $ pprint v - vs -> throw sid $ AmbiguousVarErr (pprint v) (map pprint vs) +lookupSourceName sid v = undefined +-- lookupSourceName sid v = do +-- sm <- askSourceMap +-- case lookupSourceMapPure sm v of +-- [] -> throw sid $ UnboundVarErr $ pprint v +-- LocalVar binderSid v' : _ -> do +-- emitNameInfo sid $ LocalOcc binderSid +-- return v' +-- [ModuleVar desc maybeV] -> case maybeV of +-- Just v' -> do +-- emitNameInfo sid $ TopOcc (pprint desc) +-- return v' +-- Nothing -> throw sid $ VarDefErr $ pprint v +-- vs -> throw sid $ AmbiguousVarErr (pprint v) (map pprint vs) instance SourceRenamableE (SourceNameOr Name) where sourceRenameE (SourceName sid sourceName) = do @@ -181,32 +185,32 @@ instance SourceRenamableE UAlt where sourceRenameB pat \pat' -> UAlt pat' <$> sourceRenameE body -instance SourceRenamableB UTopDecl where - sourceRenameB decl cont = case decl of - ULocalDecl d -> sourceRenameB d \d' -> cont $ ULocalDecl d' - UDataDefDecl dataDef tyConName dataConNames -> do - dataDef' <- sourceRenameE dataDef - sourceRenameUBinder tyConName \tyConName' -> - sourceRenameUBinderNest dataConNames \dataConNames' -> - cont $ UDataDefDecl dataDef' tyConName' dataConNames' - UStructDecl tyConName structDef -> do - sourceRenameUBinder tyConName \tyConName' -> do - structDef' <- sourceRenameE structDef - cont $ UStructDecl tyConName' structDef' - UInterface paramBs methodTys className methodNames -> do - Abs paramBs' (ListE methodTys') <- - sourceRenameB paramBs \paramBs' -> do - methodTys' <- mapM sourceRenameE methodTys - return $ Abs paramBs' $ ListE methodTys' - sourceRenameUBinder className \className' -> - sourceRenameUBinderNest methodNames \methodNames' -> - cont $ UInterface paramBs' methodTys' className' methodNames' - UInstance className conditions params methodDefs instanceName expl -> do - className' <- sourceRenameE className - Abs conditions' (PairE (ListE params') (ListE methodDefs')) <- - sourceRenameE $ Abs conditions (PairE (ListE params) $ ListE methodDefs) - sourceRenameB instanceName \instanceName' -> - cont $ UInstance className' conditions' params' methodDefs' instanceName' expl +-- instance SourceRenamableB UTopDecl where +-- sourceRenameB decl cont = case decl of +-- ULocalDecl d -> sourceRenameB d \d' -> cont $ ULocalDecl d' +-- UDataDefDecl dataDef tyConName dataConNames -> do +-- dataDef' <- sourceRenameE dataDef +-- sourceRenameUBinder tyConName \tyConName' -> +-- sourceRenameUBinderNest dataConNames \dataConNames' -> +-- cont $ UDataDefDecl dataDef' tyConName' dataConNames' +-- UStructDecl tyConName structDef -> do +-- sourceRenameUBinder tyConName \tyConName' -> do +-- structDef' <- sourceRenameE structDef +-- cont $ UStructDecl tyConName' structDef' +-- UInterface paramBs methodTys className methodNames -> do +-- Abs paramBs' (ListE methodTys') <- +-- sourceRenameB paramBs \paramBs' -> do +-- methodTys' <- mapM sourceRenameE methodTys +-- return $ Abs paramBs' $ ListE methodTys' +-- sourceRenameUBinder className \className' -> +-- sourceRenameUBinderNest methodNames \methodNames' -> +-- cont $ UInterface paramBs' methodTys' className' methodNames' +-- UInstance className conditions params methodDefs instanceName expl -> do +-- className' <- sourceRenameE className +-- Abs conditions' (PairE (ListE params') (ListE methodDefs')) <- +-- sourceRenameE $ Abs conditions (PairE (ListE params) $ ListE methodDefs) +-- sourceRenameB instanceName \instanceName' -> +-- cont $ UInstance className' conditions' params' methodDefs' instanceName' expl instance SourceRenamableB UDecl where sourceRenameB (WithSrcB sid decl) cont = case decl of @@ -277,16 +281,16 @@ sourceRenameUBinder (WithSrcB sid ubinder) cont = case ubinder of UBind _ _ -> error "Shouldn't be source-renaming internal names" UIgnore -> cont $ WithSrcB sid $ UIgnore -instance SourceRenamableE UDataDef where - sourceRenameE (UDataDef tyConName paramBs dataCons) = do +instance SourceRenamableTop UDataDef where + sourceRenameTop (UDataDef tyConName paramBs dataCons) = do sourceRenameB paramBs \paramBs' -> do dataCons' <- forM dataCons \(dataConName, argBs) -> do argBs' <- sourceRenameE argBs return (dataConName, argBs') return $ UDataDef tyConName paramBs' dataCons' -instance SourceRenamableE UStructDef where - sourceRenameE (UStructDef tyConName paramBs fields methods) = do +instance SourceRenamableTop UStructDef where + sourceRenameTop (UStructDef tyConName paramBs fields methods) = do sourceRenameB paramBs \paramBs' -> do fields' <- forM fields \(fieldName, ty) -> do ty' <- sourceRenameE ty @@ -408,17 +412,6 @@ instance SourceRenamableB UPat where class HasSourceNames (b::B) where sourceNames :: b n l -> S.Set SourceName -instance HasSourceNames UTopDecl where - sourceNames decl = case decl of - ULocalDecl d -> sourceNames d - UDataDefDecl _ ~(WithSrcB _ (UBindSource tyConName)) dataConNames -> do - S.singleton tyConName <> sourceNames dataConNames - UStructDecl ~(WithSrcB _ (UBindSource tyConName)) _ -> do - S.singleton tyConName - UInterface _ _ ~(WithSrcB _ (UBindSource className)) methodNames -> do - S.singleton className <> sourceNames methodNames - UInstance _ _ _ _ instanceName _ -> sourceNames instanceName - instance HasSourceNames UDecl' where sourceNames = \case ULet _ pat _ _ -> sourceNames pat diff --git a/src/lib/TopLevel2.hs b/src/lib/TopLevel2.hs new file mode 100644 index 000000000..d283f9a89 --- /dev/null +++ b/src/lib/TopLevel2.hs @@ -0,0 +1,424 @@ +-- Copyright 2020 Google LLC +-- +-- Use of this source code is governed by a BSD-style +-- license that can be found in the LICENSE file or at +-- https://developers.google.com/open-source/licenses/bsd + +{-# LANGUAGE UndecidableInstances #-} + +module TopLevel2 ( + EvalConfig (..), Topper, TopperM, runTopperM, + evalSourceBlockRepl, OptLevel (..), LibPath (..), + evalSourceBlockIO, initTopState, simpOptimizations, + ExitStatus (..), parseSourceBlocks, captureLogs) where + +import Data.Functor +import Data.Maybe (catMaybes) +import Control.Exception (throwIO, catch) +import Control.Monad.Writer.Strict hiding (pass) +import Control.Monad.State.Strict +import Control.Monad.Reader +import qualified Data.ByteString as BS +import qualified Data.Text as T +import Data.IORef +import Data.Text.Prettyprint.Doc +import Data.Store (encode, decode) +import Data.String (fromString) +import qualified Data.Map.Strict as M +import qualified Data.Set as S +import Foreign.Ptr +import Foreign.C.String +import GHC.Generics (Generic (..)) +import System.FilePath +import System.Directory +import System.IO (stderr, hPutStrLn) +import System.IO.Error (isDoesNotExistError) + +import LLVM.Link +import LLVM.Compile +import qualified LLVM.AST + +import AbstractSyntax +import ConcreteSyntax +import Err +import MonadUtil +import Paths_dex (getDataFileName) +import SourceRename +import SourceIdTraversal +import PPrint +import Types.Complicated +import Types.Simple +import Types.Imp +import Types.Primitives +import Types.Source +import Types.Top2 +import Util ( Tree (..), File (..), readFileWithHash) + +-- === top-level monad === + +data LibPath = LibDirectory FilePath | LibBuiltinPath + +data EvalConfig = EvalConfig + { libPaths :: [LibPath] + , preludeFile :: Maybe FilePath + , optLevel :: OptLevel + , printBackend :: PrintBackend + , cfgLogLevel :: LogLevel } + +type LogAction = Outputs -> IO () +class Monad m => ConfigReader m where + getConfig :: m EvalConfig + +type TopLogger m = (MonadIO m, Logger Outputs m) + +class ( Fallible m + , Logger Outputs m + , HasIOLogger Outputs m + , CanSetIOLogger Outputs m + , Catchable m + , ConfigReader m + , MonadIO m ) -- TODO: something more restricted here + => Topper m + +data TopperReaderData = TopperReaderData + { topperEvalConfig :: EvalConfig + , topperLogAction :: LogAction } + +newtype TopperM a = TopperM + { runTopperM' + :: ReaderT TopperReaderData IO a } + deriving ( Functor, Applicative, Monad, MonadIO, MonadFail + , Fallible, Catchable) + +runTopperM + :: EvalConfig -> LogAction -> TopState + -> TopperM a + -> IO (a, TopState) +runTopperM = undefined -- opts logger (TopState env rtEnv) cont = undefined +-- runTopperM opts logger (TopState env rtEnv) cont = do +-- Abs frag (LiftE result) <- +-- flip runReaderT (TopperReaderData opts logger rtEnv) $ +-- runTopBuilderT env $ runTopperM' do +-- localTopBuilder $ LiftE <$> cont +-- return (result, extendTopEnv env rtEnv frag) + +-- extendTopEnv :: Distinct n => Env n -> RuntimeEnv -> TopEnvFrag n l -> TopState +-- extendTopEnv env rtEnv frag = do +-- refreshAbsPure (toScope env) (Abs frag UnitE) \_ frag' UnitE -> +-- TopState (extendOutMap env frag') rtEnv + +initTopState :: IO TopState +initTopState = undefined + -- dyvarStores <- allocateDynamicVarKeyPtrs + -- return $ TopState emptyOutMap dyvarStores + +captureLogs :: (LogAction -> IO a) -> IO (a, Outputs) +captureLogs cont = do + ref <- newIORef mempty + ans <- cont \outs -> modifyIORef ref (<>outs) + finalOuts <- readIORef ref + return (ans, finalOuts) + +-- ====== + +parseSourceBlocks :: T.Text -> [SourceBlock] +parseSourceBlocks source = uModuleSourceBlocks $ parseUModule Main source + +evalSourceBlockIO + :: EvalConfig -> LogAction -> TopState -> SourceBlock -> IO (ExitStatus, TopState) +evalSourceBlockIO opts logger env block = + runTopperM opts logger env $ evalSourceBlockRepl block + +data ExitStatus = ExitSuccess | ExitFailure deriving (Show) + +-- Module imports have to be handled differently in the repl because we don't +-- know ahead of time which modules will be needed. +evalSourceBlockRepl :: Topper m => SourceBlock -> m ExitStatus +evalSourceBlockRepl block = do + case sbContents block of + Misc (ImportModule name) -> do + -- TODO: clear source map and synth candidates before calling this + ensureModuleLoaded name + _ -> return () + maybeErr <- evalSourceBlock Main block + case maybeErr of + Success () -> return ExitSuccess + Failure e -> do + logTop $ Error e + return $ ExitFailure + +-- XXX: This ensures that a module and its transitive dependencies are loaded, +-- (which will require evaluating them if they're not in the cache) but it +-- doesn't bring the names and instances into scope. The modules are "loaded" +-- but not yet "imported". +ensureModuleLoaded :: Topper m => ModuleSourceName -> m () +ensureModuleLoaded moduleSourceName = undefined +-- ensureModuleLoaded moduleSourceName = do +-- -- TODO: think about where import errors should be handled +-- depsRequired <- findDepsTransitively moduleSourceName +-- forM_ depsRequired \md -> do +-- evaluated <- evalPartiallyParsedUModuleCached md +-- updateTopEnv $ UpdateLoadedModules (umppName md) evaluated +-- {-# SCC ensureModuleLoaded #-} + +evalSourceBlock + :: Topper m => ModuleSourceName -> SourceBlock -> m (Except ()) +evalSourceBlock mname block = do + maybeErr <- catchErrExcept do + logTop $ SourceInfo $ SIGroupingInfo $ getGroupingInfo $ sbContents block + evalSourceBlock' mname block + case (maybeErr, sbContents block) of + (Failure _, TopDecl decl) -> do + case parseDecl decl of + Success decl' -> undefined -- emitSourceMap $ uDeclErrSourceMap (makeTopNameDescription mname block) decl' + Failure _ -> return () + _ -> return () + return maybeErr + +evalSourceBlock' + :: Topper m => ModuleSourceName -> SourceBlock -> m () +evalSourceBlock' mname block = case sbContents block of + TopDecl decl -> parseDecl decl >>= execUDecl (makeTopNameDescription mname block) + UnParseable _ s -> throwErr $ ParseErr $ MiscParseErr s + Misc m -> case m of + ImportModule moduleName -> undefined -- importModule moduleName + ProseBlock _ -> return () + CommentLine -> return () + EmptyLines -> return () + where + addTypeAnn :: UExpr n -> UExpr n -> UExpr n + addTypeAnn e = WithSrcE (srcPos e) . UTypeAnn e + addShowAny :: UExpr n -> UExpr n + addShowAny e = WithSrcE (srcPos e) $ UApp (referTo $ WithSrc (srcPos e) "show_any") [e] [] + referTo :: SourceNameW -> UExpr n + referTo (WithSrc sid name) = WithSrcE sid $ UVar $ SourceName sid name + +-- -- returns a toposorted list of the module's transitive dependencies (including +-- -- the module itself) excluding those provided in the set of already known +-- -- modules. +-- findDepsTransitively +-- :: forall m n. (Topper m, Mut n) +-- => ModuleSourceName -> m n [UModulePartialParse] +-- findDepsTransitively initialModuleName = do +-- alreadyLoaded <- M.keysSet . fromLoadedModules +-- <$> withEnv (envLoadedModules . topEnv) +-- flip evalStateT alreadyLoaded $ execWriterT $ go initialModuleName +-- where +-- go :: ModuleSourceName -> WriterT [UModulePartialParse] +-- (StateT (S.Set ModuleSourceName) m) () +-- go name = do +-- alreadyVisited <- S.member name <$> get +-- unless alreadyVisited do +-- modify $ S.insert name +-- config <- lift $ lift $ getConfig +-- source <- loadModuleSource config name +-- deps <- lift $ lift $ parseUModuleDepsCached name source +-- mapM_ go deps +-- tell [UModulePartialParse name deps source] + +-- -- What would it look like to abstract away pattern used here and in +-- -- `evalPartiallyParsedUModuleCached`? We still want case-by-case control over +-- -- keys, eviction policy, etc. Maybe some a type class for caches that implement +-- -- query/extend, with `extend` being where the eviction happens? +-- parseUModuleDepsCached +-- :: (Mut n, TopBuilder m) => ModuleSourceName -> File -> m n [ModuleSourceName] +-- parseUModuleDepsCached Main file = return $ parseUModuleDeps Main file +-- parseUModuleDepsCached name file = do +-- cache <- parsedDeps <$> getCache +-- let req = fHash file +-- case M.lookup name cache of +-- Just (cachedReq, result) | cachedReq == req -> return result +-- _ -> do +-- let result = parseUModuleDeps name file +-- updateTopEnv $ ExtendCache $ mempty { parsedDeps = M.singleton name (req, result) } +-- return result + +-- evalPartiallyParsedUModuleCached +-- :: (Topper m, Mut n) +-- => UModulePartialParse -> m n (ModuleName n) +-- evalPartiallyParsedUModuleCached md@(UModulePartialParse name deps source) = do +-- case name of +-- Main -> evalPartiallyParsedUModule md -- Don't cache main +-- _ -> do +-- LiftE cache <- withEnv $ LiftE . moduleEvaluations . envCache . topEnv +-- -- TODO: we know that these are sufficient to determine the result of +-- -- module evaluation, but maybe we should actually restrict the +-- -- environment we pass to `evalUModule` so that it can't possibly depend +-- -- on anything else. +-- directDeps <- forM deps \dep -> do +-- lookupLoadedModule dep >>= \case +-- Just depVal -> return depVal +-- Nothing -> throwInternal $ pprint dep ++ " isn't loaded" +-- let req = (fHash source, directDeps) +-- case M.lookup name cache of +-- Just (cachedReq, result) | cachedReq == req -> return result +-- _ -> do +-- liftIO $ hPutStrLn stderr $ "Compiling " ++ pprint name +-- result <- evalPartiallyParsedUModule md +-- updateTopEnv $ ExtendCache $ mempty { +-- moduleEvaluations = M.singleton name (req, result) } +-- return result + +-- -- Assumes all module dependencies have been loaded already +-- evalPartiallyParsedUModule +-- :: (Topper m, Mut n) +-- => UModulePartialParse -> m n (ModuleName n) +-- evalPartiallyParsedUModule partiallyParsed = do +-- let name = umppName partiallyParsed +-- let uModule = finishUModuleParse partiallyParsed +-- evaluated <- evalUModule uModule +-- emitBinding (getNameHint name) $ ModuleBinding evaluated + +-- -- Assumes all module dependencies have been loaded already +-- evalUModule :: (Topper m, Mut n) => UModule -> m n (Module n) +-- evalUModule (UModule name _ blocks) = dropSourceInfoLogging do +-- Abs topFrag UnitE <- localTopBuilder $ mapM_ (evalSourceBlock' name) blocks >> return UnitE +-- TopEnvFrag envFrag moduleEnvFrag otherUpdates <- return topFrag +-- ModuleEnv (ImportStatus directDeps transDeps) sm scs <- return moduleEnvFrag +-- let fragToReEmit = TopEnvFrag envFrag mempty otherUpdates +-- let evaluatedModule = Module name directDeps transDeps sm scs +-- emitEnv $ Abs fragToReEmit evaluatedModule + +dropSourceInfoLogging :: Topper m => m a -> m a +dropSourceInfoLogging cont = do + (ans, Outputs logs) <- captureIOLogs cont + let logs' = filter isNotSourceInfo logs + emitLog $ Outputs logs' + return ans + where + isNotSourceInfo = \case + SourceInfo _ -> False + _ -> True + +-- importModule :: (Mut n, TopBuilder m, Fallible1 m) => ModuleSourceName -> m n () +-- importModule name = do +-- lookupLoadedModule name >>= \case +-- Nothing -> throwErr $ MiscErr $ ModuleImportErr $ pprint name +-- Just name' -> do +-- Module _ _ transImports' _ _ <- lookupModule name' +-- let importStatus = ImportStatus (S.singleton name') +-- (S.singleton name' <> transImports') +-- emitLocalModuleEnv $ mempty { envImportStatus = importStatus } +-- {-# SCC importModule #-} + + +-- evalUType :: (Topper m, Mut n) => UType VoidS -> m n (CType n) +-- evalUType ty = do +-- logPass Parse ty +-- renamed <- renameSourceNamesUExpr ty +-- logPass RenamePass renamed +-- checkPass TypePass $ checkTopUType renamed + +-- evalUExpr :: (Topper m, Mut n) => UExpr VoidS -> m n (CAtom n) +-- evalUExpr expr = do +-- logPass Parse expr +-- renamed <- renameSourceNamesUExpr expr +-- logPass RenamePass renamed +-- typed <- checkPass TypePass $ inferTopUExpr renamed +-- evalBlock typed + +-- whenOpt :: Topper m => a -> (a -> m n a) -> m n a +-- whenOpt x act = getConfig <&> optLevel >>= \case +-- NoOptimize -> return x +-- Optimize -> act x + +-- evalBlock :: (Topper m, Mut n) => TopBlock n -> m n (CAtom n) +-- evalBlock typed@(TopLam _ _ (LamExpr Empty body)) = case body of +-- Atom result -> return result +-- _ -> do +-- simp <- checkPass SimpPass $ simplifyTopBlock typed +-- opt <- simpOptimizations simp +-- dps <- checkPass LowerPass $ dpsPass opt +-- lOpt <- checkPass OptPass $ loweredOptimizations dps +-- cc <- getEntryFunCC +-- impOpt <- checkPass ImpPass $ toImpFunction cc lOpt +-- llvmOpt <- packageLLVMCallable impOpt +-- resultVals <- liftIO $ callEntryFun llvmOpt [] +-- TopLam _ destTy _ <- return lOpt +-- resultTy <- return $ assumeConst $ piTypeWithoutDest destTy +-- RepVal _ repVal <- repValFromFlatList resultTy resultVals +-- return $ toAtom $ RepVal (getType body) repVal +-- evalBlock _ = error "not a top block" +-- {-# SCC evalBlock #-} + +simpOptimizations :: Topper m => STopLam -> m STopLam +simpOptimizations simp = undefined +-- simpOptimizations simp = do +-- analyzed <- whenOpt simp $ checkPass OccAnalysisPass . analyzeOccurrences +-- inlined <- whenOpt analyzed $ checkPass InlinePass . inlineBindings +-- analyzed2 <- whenOpt inlined $ checkPass OccAnalysisPass . analyzeOccurrences +-- inlined2 <- whenOpt analyzed2 $ checkPass InlinePass . inlineBindings +-- whenOpt inlined2 $ checkPass OptPass . optimize + +execUDecl :: Topper m => TopNameDescription -> UTopDecl -> m () +execUDecl desc decl = undefined +-- execUDecl desc decl = do +-- logPass Parse decl +-- renamed@(Abs renamedDecl sourceMap) <- renameSourceNamesTopUDecl desc decl +-- logPass RenamePass renamed +-- inferenceResult <- checkPass TypePass $ inferTopUDecl renamedDecl sourceMap +-- case inferenceResult of +-- UDeclResultBindName ann block (Abs b sm) -> do +-- result <- evalBlock block +-- case ann of +-- NoInlineLet -> do +-- let fTy = getType result +-- f <- emitBinding (getNameHint b) $ AtomNameBinding $ NoinlineFun fTy result +-- applyRename (b@>f) sm >>= emitSourceMap +-- _ -> do +-- v <- emitTopLet (getNameHint b) ann (Atom result) +-- applyRename (b@>atomVarName v) sm >>= emitSourceMap +-- UDeclResultBindPattern hint block (Abs bs sm) -> do +-- result <- evalBlock block +-- xs <- unpackTelescope bs result +-- vs <- forM xs \x -> emitTopLet hint PlainLet (Atom x) +-- applyRename (bs@@>(atomVarName <$> vs)) sm >>= emitSourceMap +-- UDeclResultDone sourceMap' -> emitSourceMap sourceMap' + +getLLVMOptLevel :: EvalConfig -> LLVMOptLevel +getLLVMOptLevel cfg = case optLevel cfg of + NoOptimize -> OptALittle + Optimize -> OptAggressively + +checkPass :: (Topper m, Pretty e) => PassName -> m e -> m e +checkPass name cont = do + result <- cont + logPass name result + return result + +logTop :: TopLogger m => Output -> m () +logTop x = emitLog $ Outputs [x] + +logDebug :: TopLogger m => m Output -> m () +logDebug m = getLogLevel >>= \case + NormalLogLevel -> return () + DebugLogLevel -> do + x <- m + emitLog $ Outputs [x] + +logPass :: Topper m => Pretty a => PassName -> a -> m () +logPass passName result = do + getLogLevel >>= \case + NormalLogLevel -> logTop $ PassResult passName Nothing + DebugLogLevel -> logTop $ PassResult passName $ Just s + where s = "=== " <> pprint passName <> " ===\n" <> pprint result + +-- === instances === + +instance ConfigReader TopperM where + getConfig = TopperM $ asks topperEvalConfig + +instance Topper TopperM + +instance Logger Outputs TopperM where + emitLog x = do + logger <- getIOLogAction + liftIO $ logger x + getLogLevel = cfgLogLevel <$> getConfig + +instance HasIOLogger Outputs TopperM where + getIOLogAction = TopperM $ asks topperLogAction + +instance CanSetIOLogger Outputs TopperM where + withIOLogAction logger (TopperM m) = TopperM do + local (\r -> r { topperLogAction = logger }) m diff --git a/src/lib/Types/Complicated.hs b/src/lib/Types/Complicated.hs index 05ce6d2cf..3e0f02dfb 100644 --- a/src/lib/Types/Complicated.hs +++ b/src/lib/Types/Complicated.hs @@ -76,30 +76,30 @@ data Kind = DataKind | RefKind | TypeKind | FunKind | DictKind | OtherKind instance Store Kind instance Hashable Kind -type ClassName = Name +type ClassName = TopName data DictType (n::S) = - DictType SourceName (ClassName n) [CExpr n] + DictType SourceName ClassName [CExpr n] | IxDictType (CType n) deriving (Show, Generic) -type InstanceName = Name +type InstanceName = TopName data DictCon (n::S) = - InstanceDict (CType n) (InstanceName n) [CExpr n] + InstanceDict (CType n) InstanceName [CExpr n] | IxFin (CExpr n) deriving (Show, Generic) -- Describes how to lift the "shallow" representation type to the newtype. data NewtypeCon (n::S) = - UserADTData SourceName (TyConName n) (TyConParams n) -- source name is for the type + UserADTData SourceName TyConName (TyConParams n) -- source name is for the type | NatCon | FinCon (CExpr n) deriving (Show, Generic) -type TyConName = Name +type TyConName = TopName data NewtypeTyCon (n::S) = Nat | Fin (CExpr n) - | UserADTType SourceName (TyConName n) (TyConParams n) + | UserADTType SourceName TyConName (TyConParams n) deriving (Show, Generic) -- We track the explicitness information because we need it for the equality @@ -127,7 +127,7 @@ instance Store BuiltinClassName data InstanceDef (n::S) where InstanceDef - :: ClassName n1 + :: ClassName -> [Explicitness] -- parameter info -> Nest CBinder n1 n2 -- parameters (types and dictionaries) -> [CExpr n2] -- class parameters diff --git a/src/lib/Types/Imp.hs b/src/lib/Types/Imp.hs index cea84d5e3..74401ff3a 100644 --- a/src/lib/Types/Imp.hs +++ b/src/lib/Types/Imp.hs @@ -39,11 +39,10 @@ import Types.Source -- === data types === type ImpName = Name -type PtrName = Name -type ImpFunName = Name +type PtrName = TopName +type ImpFunName = TopName data IExpr n = ILit LitVal | IVar (ImpName n) BaseType - | IPtrVar (PtrName n) PtrType deriving (Show, Generic) data IBinder n l = IBinder (NameBinder n l) IType deriving (Show, Generic) @@ -100,7 +99,7 @@ data CallingConvention = | MCThreadLaunch deriving (Show, Eq, Generic) -data ImpFunction n = ImpFunction IFunType (Abs (Nest IBinder) ImpBlock n) +data ImpFunction = ImpFunction IFunType (Abs (Nest IBinder) ImpBlock VoidS) deriving (Show, Generic) data ImpBlock n where @@ -117,7 +116,7 @@ data ImpInstr n = | IQueryParallelism IFunVar (IExpr n) -- returns the number of available concurrent threads | ISyncWorkgroup | ILaunch IFunVar (Size n) [IExpr n] - | ICall (ImpFunName n) [IExpr n] + | ICall ImpFunName [IExpr n] | Store (IExpr n) (IExpr n) -- dest, val | Alloc AddressSpace IType (Size n) | StackAlloc IType (Size n) @@ -174,22 +173,22 @@ data IFunBinder n l = IFunBinder (NameBinder n l) IFunType -- Imp function with link-time objects abstracted out, suitable for standalone -- compilation. TODO: enforce actual `VoidS` as the scope parameter. -data ClosedImpFunction n where - ClosedImpFunction - :: Nest IFunBinder n1 n2 -- binders for required functions - -> Nest PtrBinder n2 n3 -- binders for required data pointers - -> ImpFunction n3 - -> ClosedImpFunction n1 +data ClosedImpFunction n = ClosedImpFunction -- where + -- ClosedImpFunction + -- :: Nest IFunBinder n1 n2 -- binders for required functions + -- -> Nest PtrBinder n2 n3 -- binders for required data pointers + -- -> ImpFunction n3 + -- -> ClosedImpFunction n1 data PtrBinder n l = PtrBinder (NameBinder n l) PtrType -type FunObjCodeName = Name -data LinktimeNames n = LinktimeNames [FunObjCodeName n] [PtrName n] deriving (Show, Generic) -data LinktimeVals = LinktimeVals [FunPtr ()] [Ptr ()] deriving (Show, Generic) +type FunObjCodeName = TopName +data LinktimeNames = LinktimeNames [FunObjCodeName] [PtrName] deriving (Show, Generic) +data LinktimeVals = LinktimeVals [FunPtr ()] [Ptr ()] deriving (Show, Generic) -data CFunction (n::S) = CFunction +data CFunction = CFunction { nameHint :: NameHint , objectCode :: FunObjCode - , linkerNames :: LinktimeNames n + , linkerNames :: LinktimeNames } deriving (Show, Generic) @@ -249,7 +248,7 @@ instance GenericE ImpInstr where ) (EitherE4 {- ISyncW -} (UnitE) {- ILaunch -} (LiftE IFunVar `PairE` Size `PairE` ListE IExpr) - {- ICall -} (ImpFunName `PairE` ListE IExpr) + {- ICall -} (LiftE ImpFunName `PairE` ListE IExpr) {- Store -} (IExpr `PairE` IExpr) ) (EitherE7 {- Alloc -} (LiftE (AddressSpace, IType) `PairE` Size) @@ -283,7 +282,7 @@ instance GenericE ImpInstr where ISyncWorkgroup -> Case1 $ Case0 UnitE ILaunch f n args -> Case1 $ Case1 $ LiftE f `PairE` n `PairE` ListE args - ICall f args -> Case1 $ Case2 $ f `PairE` ListE args + ICall f args -> Case1 $ Case2 $ LiftE f `PairE` ListE args Store dest val -> Case1 $ Case3 $ dest `PairE` val Alloc a t s -> Case2 $ Case0 $ LiftE (a, t) `PairE` s @@ -320,7 +319,7 @@ instance GenericE ImpInstr where Case1 instr' -> case instr' of Case0 UnitE -> ISyncWorkgroup Case1 (LiftE f `PairE` n `PairE` ListE args) -> ILaunch f n args - Case2 (f `PairE` ListE args) -> ICall f args + Case2 (LiftE f `PairE` ListE args) -> ICall f args Case3 (dest `PairE` val ) -> Store dest val _ -> error "impossible" @@ -367,19 +366,16 @@ instance RenameE ImpBlock deriving via WrapE ImpBlock n instance Generic (ImpBlock n) instance GenericE IExpr where - type RepE IExpr = EitherE3 (LiftE LitVal) + type RepE IExpr = EitherE2 (LiftE LitVal) (PairE ImpName (LiftE BaseType)) - (PairE PtrName (LiftE PtrType)) fromE iexpr = case iexpr of ILit x -> Case0 (LiftE x) IVar v ty -> Case1 (v `PairE` LiftE ty) - IPtrVar v ty -> Case2 (v `PairE` LiftE ty) {-# INLINE fromE #-} toE rep = case rep of Case0 (LiftE x) -> ILit x Case1 (v `PairE` LiftE ty) -> IVar v ty - Case2 (v `PairE` LiftE ty) -> IPtrVar v ty _ -> error "impossible" {-# INLINE toE #-} @@ -426,47 +422,6 @@ instance AlphaHashableB ImpDecl instance ProvesExt ImpDecl instance BindsNames ImpDecl -instance GenericE ImpFunction where - type RepE ImpFunction = LiftE IFunType `PairE` Abs (Nest IBinder) ImpBlock - fromE (ImpFunction ty ab) =LiftE ty `PairE` ab - {-# INLINE fromE #-} - - toE (LiftE ty `PairE` ab) = ImpFunction ty ab - {-# INLINE toE #-} - -instance SinkableE ImpFunction -instance HoistableE ImpFunction -instance AlphaEqE ImpFunction -instance AlphaHashableE ImpFunction -instance RenameE ImpFunction - -instance GenericE LinktimeNames where - type RepE LinktimeNames = ListE FunObjCodeName `PairE` ListE PtrName - fromE (LinktimeNames funs ptrs) = ListE funs `PairE` ListE ptrs - {-# INLINE fromE #-} - toE (ListE funs `PairE` ListE ptrs) = LinktimeNames funs ptrs - {-# INLINE toE #-} - -instance SinkableE LinktimeNames -instance HoistableE LinktimeNames -instance AlphaEqE LinktimeNames -instance AlphaHashableE LinktimeNames -instance RenameE LinktimeNames - -instance GenericE CFunction where - type RepE CFunction = (LiftE NameHint) `PairE` - (LiftE FunObjCode) `PairE` LinktimeNames - fromE (CFunction{..}) = LiftE nameHint `PairE` - LiftE objectCode `PairE` linkerNames - {-# INLINE fromE #-} - toE (LiftE nameHint `PairE` LiftE objectCode `PairE` linkerNames) = - CFunction{..} - {-# INLINE toE #-} - -instance SinkableE CFunction -instance HoistableE CFunction -instance RenameE CFunction - instance Store IsCUDARequired instance Store CallingConvention instance Store a => Store (WithCNameInterface a) @@ -476,9 +431,9 @@ instance Store (IFunType) instance Store (ImpInstr n) instance Store (IExpr n) instance Store (ImpBlock n) -instance Store (ImpFunction n) -instance Store (LinktimeNames n) -instance Store (CFunction n) +instance Store ImpFunction +instance Store LinktimeNames +instance Store CFunction instance Store LinktimeVals instance Hashable IsCUDARequired @@ -487,7 +442,7 @@ instance Hashable IFunType instance Pretty CallingConvention where pretty = fromString . show -instance Pretty (ImpFunction n) where +instance Pretty ImpFunction where pretty (ImpFunction (IFunType cc _ _) (Abs bs body)) = "impfun" <+> pretty cc <+> prettyBinderNest bs <> nest 2 (hardline <> pretty body) <> hardline @@ -552,7 +507,6 @@ instance Pretty (IExpr n) where pretty = \case ILit v -> pretty v IVar v _ -> pretty v - IPtrVar v _ -> pretty v instance PrettyPrec (IExpr n) where prettyPrec = atPrec ArgPrec . pretty diff --git a/src/lib/Types/Primitives.hs b/src/lib/Types/Primitives.hs index e2a76e615..07d406d2d 100644 --- a/src/lib/Types/Primitives.hs +++ b/src/lib/Types/Primitives.hs @@ -130,6 +130,15 @@ instance Store a => Store (RefOp a) -- === various things === +type TopNameHint = String +type ModuleName = SourceName +data TopName = TopGenName TopNameHint Int + | TopSourceName ModuleName SourceName + deriving (Show, Eq, Ord, Generic) +instance Hashable TopName +instance Store TopName +type TopBinder = TopName + newtype SourceName = MkSourceName String deriving (Show, Eq, Ord, Generic) newtype AlwaysEqual a = AlwaysEqual a @@ -280,6 +289,9 @@ instance HasNameHint SourceName where instance Pretty SourceName where pretty (MkSourceName v) = pretty v +instance Pretty TopName where + pretty _ = undefined + instance IsString SourceName where fromString v = MkSourceName v diff --git a/src/lib/Types/Simple.hs b/src/lib/Types/Simple.hs index b033b3815..35b162b12 100644 --- a/src/lib/Types/Simple.hs +++ b/src/lib/Types/Simple.hs @@ -33,7 +33,7 @@ import Types.Imp data Expr (n::S) = Block (Type n) (Block n) - | TopApp (Type n) (TopFunName n) [Atom n] + | TopApp (Type n) TopName [Atom n] | Case (Type n) (Atom n) [LamExpr n] | For (Atom n) (LamExpr n) | While (Expr n) @@ -53,7 +53,7 @@ data Type (n::S) = | TabPi (TabPiType n) deriving (Show, Generic) -type TopFunName = Name +type TopFunName = TopName type Binder = BinderP Type :: B data Decl (n::S) (l::S) = Let (NameBinder n l) (Expr n) deriving (Show, Generic) diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs index 29526d4c2..c9b748c8d 100644 --- a/src/lib/Types/Source.hs +++ b/src/lib/Types/Source.hs @@ -345,49 +345,52 @@ data UDepPairType (n::S) where type UConDef (n::S) (l::S) = (SourceName, Nest UAnnBinder n l) -data UDataDef (n::S) where +data UDataDef where UDataDef :: SourceName -- source name for pretty printing - -> Nest UAnnBinder n l + -> Nest UAnnBinder VoidS l -> [(SourceName, UDataDefTrail l)] -- data constructor types - -> UDataDef n + -> UDataDef -data UStructDef (n::S) where +data UStructDef where UStructDef :: SourceName -- source name for pretty printing - -> Nest UAnnBinder n l + -> Nest UAnnBinder VoidS l -> [(SourceNameW, UType l)] -- named payloads -> [(LetAnn, SourceName, Abs UBinder ULamExpr l)] -- named methods (initial binder is for `self`) - -> UStructDef n + -> UStructDef data UDataDefTrail (l::S) where UDataDefTrail :: Nest UAnnBinder l l' -> UDataDefTrail l -data UTopDecl (n::S) (l::S) where - ULocalDecl :: UDecl n l -> UTopDecl n l - UDataDefDecl - :: UDataDef n -- actual definition - -> UBinder n l' -- type constructor name - -> Nest UBinder l' l -- data constructor names - -> UTopDecl n l - UStructDecl - :: UBinder n l -- type constructor name - -> UStructDef l -- actual definition - -> UTopDecl n l - UInterface - :: Nest UAnnBinder n p -- parameter binders - -> [UType p] -- method types - -> UBinder n l' -- class name - -> Nest UBinder l' l -- method names - -> UTopDecl n l - UInstance - :: SourceNameOr Name n -- class name - -> Nest UAnnBinder n l' +data UInterfaceDef where + UInterfaceDef + :: Nest UAnnBinder VoidS p -- parameter binders + -> [UType p] -- method types + -> UInterfaceDef + +data UInstanceDef where + UInstanceDef + :: Nest UAnnBinder VoidS l' -> [UExpr l'] -- class parameters -> [UMethodDef l'] -- method definitions - -> MaybeB UBinder n l -- optional instance name - -> AppExplicitness -- explicitness (only relevant for named instances) - -> UTopDecl n l + -> UInstanceDef + +data UTopDecl = + UTopLet TopBinder (Maybe (UType VoidS)) (UExpr VoidS) + | UTopExpr (UExpr VoidS) + | UDataDefDecl + UDataDef + TopBinder -- type constructor name + [TopBinder] -- data constructor names + | UStructDecl + UStructDef + TopBinder -- type constructor name + | UInterface + UInterfaceDef + TopBinder -- class name + [TopBinder] -- method names + | UInstance UInstanceDef type UType = UExpr type UConstraint = UExpr @@ -558,17 +561,12 @@ data SymbolicZeros = SymbolicZeros | InstantiateZeros data SourceBlock' = TopDecl CTopDeclW - | Command CmdName GroupW - | DeclareForeign SourceNameW SourceNameW GroupW - | DeclareCustomLinearization SourceNameW SymbolicZeros GroupW | Misc SourceBlockMisc | UnParseable ReachedEOF String deriving (Show, Generic) data SourceBlockMisc - = GetNameType SourceNameW - | ImportModule ModuleSourceName - | QueryEnv EnvQuery + = ImportModule ModuleSourceName | ProseBlock Text | CommentLine | EmptyLines @@ -863,9 +861,6 @@ instance SinkableE UBlock' where instance SinkableB UDecl where sinkingProofB _ _ _ = todoSinkableProof -instance SinkableB UTopDecl where - sinkingProofB _ _ _ = todoSinkableProof - instance Eq SourceBlock where x == y = sbText x == sbText y @@ -888,8 +883,8 @@ deriving instance Show (ULamExpr n) deriving instance Show (UPiExpr n) deriving instance Show (UTabPiExpr n) deriving instance Show (UDepPairType n) -deriving instance Show (UDataDef n) -deriving instance Show (UStructDef n) +deriving instance Show UDataDef +deriving instance Show UStructDef deriving instance Show (UDecl' n l) deriving instance Show (UBlock' n) deriving instance Show (UForExpr n) @@ -991,30 +986,31 @@ instance PrettyPrec (UPat' n l) where instance Pretty (UAlt n) where pretty (UAlt pat body) = pretty pat <+> "->" <+> pretty body -instance Pretty (UTopDecl n l) where - pretty = \case - UDataDefDecl (UDataDef nm bs dataCons) bTyCon bDataCons -> - "enum" <+> p bTyCon <+> p nm <+> spaced (unsafeFromNest bs) <+> "where" <> nest 2 - (prettyLines (zip (toList $ unsafeFromNest bDataCons) dataCons)) - UStructDecl bTyCon (UStructDef nm bs fields defs) -> - "struct" <+> p bTyCon <+> p nm <+> spaced (unsafeFromNest bs) <+> "where" <> nest 2 - (prettyLines fields <> prettyLines defs) - UInterface params methodTys interfaceName methodNames -> - "interface" <+> p params <+> p interfaceName - <> hardline <> foldMap (<>hardline) methods - where - methods = [ p b <> ":" <> p (unsafeCoerceE ty) - | (b, ty) <- zip (toList $ unsafeFromNest methodNames) methodTys] - UInstance className bs params methods (RightB UnitB) _ -> - "instance" <+> p bs <+> p className <+> spaced params <+> - prettyLines methods - UInstance className bs params methods (LeftB v) _ -> - "named-instance" <+> p v <+> ":" <+> p bs <+> p className <+> p params - <> prettyLines methods - ULocalDecl decl -> p decl - where - p :: Pretty a => a -> Doc ann - p = pretty +instance Pretty UTopDecl where + pretty = undefined + -- pretty = \case + -- UDataDefDecl (UDataDef nm bs dataCons) bTyCon bDataCons -> + -- "enum" <+> p bTyCon <+> p nm <+> spaced (unsafeFromNest bs) <+> "where" <> nest 2 + -- (prettyLines (zip (toList $ unsafeFromNest bDataCons) dataCons)) + -- UStructDecl bTyCon (UStructDef nm bs fields defs) -> + -- "struct" <+> p bTyCon <+> p nm <+> spaced (unsafeFromNest bs) <+> "where" <> nest 2 + -- (prettyLines fields <> prettyLines defs) + -- UInterface params methodTys interfaceName methodNames -> + -- "interface" <+> p params <+> p interfaceName + -- <> hardline <> foldMap (<>hardline) methods + -- where + -- methods = [ p b <> ":" <> p (unsafeCoerceE ty) + -- | (b, ty) <- zip (toList $ unsafeFromNest methodNames) methodTys] + -- UInstance className bs params methods (RightB UnitB) _ -> + -- "instance" <+> p bs <+> p className <+> spaced params <+> + -- prettyLines methods + -- UInstance className bs params methods (LeftB v) _ -> + -- "named-instance" <+> p v <+> ":" <+> p bs <+> p className <+> p params + -- <> prettyLines methods + -- ULocalDecl decl -> p decl + -- where + -- p :: Pretty a => a -> Doc ann + -- p = pretty instance Pretty (UDecl' n l) where pretty = \case diff --git a/src/lib/Types/Top2.hs b/src/lib/Types/Top2.hs new file mode 100644 index 000000000..c3c893675 --- /dev/null +++ b/src/lib/Types/Top2.hs @@ -0,0 +1,933 @@ +-- Copyright 2022 Google LLC +-- +-- Use of this source code is governed by a BSD-style +-- license that can be found in the LICENSE file or at +-- https://developers.google.com/open-source/licenses/bsd + +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE StrictData #-} + +-- Top-level data types + +module Types.Top2 where + +import Data.Functor ((<&>)) +import Data.Hashable +import Data.Text.Prettyprint.Doc +import qualified Data.Map.Strict as M +import qualified Data.Set as S + +import GHC.Generics (Generic (..)) +import Data.Store (Store (..)) +import Foreign.Ptr + +import Name +import Util (FileHash, SnocList (..)) +import PPrint + +import Types.Primitives +import Types.Complicated +import Types.Simple +import Types.Source +import Types.Imp + +data TopState = TopState + deriving (Show, Generic) + +-- type TopBlock = TopLam -- used for nullary lambda +data TopLam = TopLam (PiType VoidS) (LamExpr VoidS) + deriving (Show, Generic) +type STopLam = TopLam +type CTopLam = TopLam + +-- data EvalStatus a = Waiting | Running | Finished a +-- deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) +-- type TopFunEvalStatus n = EvalStatus (TopFunLowerings n) + +-- data TopFun (n::S) = +-- DexTopFun (TopFunDef n) (TopLam n) (TopFunEvalStatus n) +-- | FFITopFun String IFunType +-- deriving (Show, Generic) + +-- data TopFunDef (n::S) = +-- Specialization (SpecializationSpec n) +-- | LinearizationPrimal (LinearizationSpec n) +-- -- Tangent functions all take some number of nonlinear args, then a *single* +-- -- linear arg. This is so that transposition can be an involution - you apply +-- -- it twice and you get back to the original function. +-- | LinearizationTangent (LinearizationSpec n) +-- deriving (Show, Generic) + +-- newtype TopFunLowerings (n::S) = TopFunLowerings +-- { topFunObjCode :: FunObjCodeName n } -- TODO: add optimized, imp etc. as needed +-- deriving (Show, Generic, SinkableE, HoistableE, RenameE, AlphaEqE, AlphaHashableE, Pretty) + +-- data AtomBinding (n::S) = +-- LetBound (CExpr n) +-- | MiscBound (Type n) +-- | SolverBound (SolverBinding n) +-- | FFIFunBound (CorePiType n) (TopFunName n) + +-- deriving instance Show (AtomBinding n) +-- deriving via WrapE AtomBinding n instance Generic (AtomBinding n) + +-- data SolverBinding (n::S) = +-- InfVarBound (CType n) +-- | SkolemBound (CType n) +-- | DictBound (CType n) +-- deriving (Show, Generic) + +-- -- === top-level definitions === + +-- -- === envs and modules === + +-- -- `ModuleEnv` contains data that only makes sense in the context of evaluating +-- -- a particular module. `TopEnv` contains everything that makes sense "between" +-- -- evaluating modules. +-- data Env n = Env +-- { topEnv :: {-# UNPACK #-} TopEnv n +-- , moduleEnv :: {-# UNPACK #-} ModuleEnv n } +-- deriving (Generic) + +-- newtype EnvFrag (n::S) (l::S) = EnvFrag (RecSubstFrag Binding n l) +-- deriving (OutFrag) + +-- data TopEnv (n::S) = TopEnv +-- { envDefs :: RecSubst Binding n +-- , envCache :: Cache n +-- , envLoadedModules :: LoadedModules n +-- , envLoadedObjects :: LoadedObjects n } +-- deriving (Generic) + +-- data SerializedEnv n = SerializedEnv +-- { serializedEnvDefs :: RecSubst Binding n +-- , serializedEnvCache :: Cache n } +-- deriving (Generic) + +-- -- TODO: consider splitting this further into `ModuleEnv` (the env that's +-- -- relevant between top-level decls) and `LocalEnv` (the additional parts of the +-- -- env that's relevant under a lambda binder). Unlike the Top/Module +-- -- distinction, there's some overlap. For example, instances can be defined at +-- -- both the module-level and local level. Similarly, if we start allowing +-- -- top-level effects in `Main` then we'll have module-level effects and local +-- -- effects. +-- data ModuleEnv (n::S) = ModuleEnv +-- { envImportStatus :: ImportStatus n +-- , envSourceMap :: SourceMap n +-- , envSynthCandidates :: SynthCandidates n } +-- deriving (Generic) + +-- type ModuleName = Name +-- data Module (n::S) = Module +-- { moduleSourceName :: ModuleSourceName +-- , moduleDirectDeps :: S.Set (ModuleName n) +-- , moduleTransDeps :: S.Set (ModuleName n) -- XXX: doesn't include the module itself +-- , moduleExports :: SourceMap n +-- -- these are just the synth candidates required by this +-- -- module by itself. We'll usually also need those required by the module's +-- -- (transitive) dependencies, which must be looked up separately. +-- , moduleSynthCandidates :: SynthCandidates n } +-- deriving (Show, Generic) + +-- data LoadedModules (n::S) = LoadedModules +-- { fromLoadedModules :: M.Map ModuleSourceName (ModuleName n)} +-- deriving (Show, Generic) + +-- emptyModuleEnv :: ModuleEnv n +-- emptyModuleEnv = ModuleEnv emptyImportStatus (SourceMap mempty) mempty + +-- emptyLoadedModules :: LoadedModules n +-- emptyLoadedModules = LoadedModules mempty + +-- data LoadedObjects (n::S) = LoadedObjects +-- -- the pointer points to the actual runtime function +-- { fromLoadedObjects :: M.Map (FunObjCodeName n) NativeFunction} +-- deriving (Show, Generic) + +-- emptyLoadedObjects :: LoadedObjects n +-- emptyLoadedObjects = LoadedObjects mempty + +-- data ImportStatus (n::S) = ImportStatus +-- { directImports :: S.Set (ModuleName n) +-- -- XXX: This are cached for efficiency. It's derivable from `directImports`. +-- , transImports :: S.Set (ModuleName n) } +-- deriving (Show, Generic) + +-- data TopEnvFrag n l = TopEnvFrag (EnvFrag n l) (ModuleEnv l) (SnocList (TopEnvUpdate l)) + +-- data TopEnvUpdate n = +-- ExtendCache (Cache n) +-- | UpdateLoadedModules ModuleSourceName (ModuleName n) +-- | UpdateLoadedObjects (FunObjCodeName n) NativeFunction +-- | UpdateTopFunEvalStatus (TopFunName n) (TopFunEvalStatus n) +-- | UpdateInstanceDef (InstanceName n) (InstanceDef n) +-- | UpdateTyConDef (TyConName n) (TyConDef n) +-- | UpdateFieldDef (TyConName n) SourceName (Name n) + +-- -- TODO: we could add a lot more structure for querying by dict type, caching, etc. +-- data SynthCandidates n = SynthCandidates +-- { instanceDicts :: M.Map (ClassName n) [InstanceName n] +-- , ixInstances :: [InstanceName n] } +-- deriving (Show, Generic) + +-- emptyImportStatus :: ImportStatus n +-- emptyImportStatus = ImportStatus mempty mempty + +-- -- TODO: figure out the additional top-level context we need -- backend, other +-- -- compiler flags etc. We can have a map from those to this. + +-- data Cache (n::S) = Cache +-- { specializationCache :: EMap SpecializationSpec TopFunName n +-- , linearizationCache :: EMap LinearizationSpec (PairE TopFunName TopFunName) n +-- , transpositionCache :: EMap TopFunName TopFunName n +-- -- This is memoizing `parseAndGetDeps :: Text -> [ModuleSourceName]`. But we +-- -- only want to store one entry per module name as a simple cache eviction +-- -- policy, so we store it keyed on the module name, with the text hash for +-- -- the validity check. +-- , parsedDeps :: M.Map ModuleSourceName (FileHash, [ModuleSourceName]) +-- , moduleEvaluations :: M.Map ModuleSourceName ((FileHash, [ModuleName n]), ModuleName n) +-- } deriving (Show, Generic) + +-- -- === runtime function and variable representations === + +-- type RuntimeEnv = DynamicVarKeyPtrs + +-- type DexDestructor = FunPtr (IO ()) + +-- data NativeFunction = NativeFunction +-- { nativeFunPtr :: FunPtr () +-- , nativeFunTeardown :: IO () } + +-- instance Show NativeFunction where +-- show _ = "" + +-- -- Holds pointers to thread-local storage used to simulate dynamically scoped +-- -- variables, such as the output stream file descriptor. +-- type DynamicVarKeyPtrs = [(DynamicVar, Ptr ())] + +-- data DynamicVar = OutStreamDyvar -- TODO: add others as needed +-- deriving (Enum, Bounded) + +-- dynamicVarCName :: DynamicVar -> String +-- dynamicVarCName OutStreamDyvar = "dex_out_stream_dyvar" + +-- dynamicVarLinkMap :: DynamicVarKeyPtrs -> [(String, Ptr ())] +-- dynamicVarLinkMap dyvars = dyvars <&> \(v, ptr) -> (dynamicVarCName v, ptr) + +-- -- === Specialization and generalization === + +-- type Generalized (e::E) (n::S) = (Abstracted e n, [Atom n]) +-- type Abstracted (e::E) = Abs (Nest Binder) e +-- type AbsDict = Abstracted DictCon + +-- data SpecializedDictDef n = +-- SpecializedDict +-- (AbsDict n) +-- -- Methods (thunked if nullary), if they're available. +-- -- We create specialized dict names during simplification, but we don't +-- -- actually simplify/lower them until we return to TopLevel +-- (Maybe [TopLam n]) +-- deriving (Show, Generic) + +-- -- TODO: extend with AD-oriented specializations, backend-specific specializations etc. +-- data SpecializationSpec (n::S) = +-- AppSpecialization (Name n) (Abstracted (ListE CExpr) n) +-- deriving (Show, Generic) + +-- type Active = Bool +-- data LinearizationSpec (n::S) = LinearizationSpec (TopFunName n) [Active] +-- deriving (Show, Generic) + +-- -- === bindings - static information we carry about a lexical scope === + +-- data Binding (n::S) where +-- AtomNameBinding :: AtomBinding n -> Binding n +-- TyConBinding :: Maybe (TyConDef n) -> DotMethods n -> Binding n +-- DataConBinding :: TyConName n -> Int -> Binding n +-- ClassBinding :: ClassDef n -> Binding n +-- InstanceBinding :: InstanceDef n -> CorePiType n -> Binding n +-- MethodBinding :: ClassName n -> Int -> Binding n +-- TopFunBinding :: TopFun n -> Binding n +-- FunObjCodeBinding :: CFunction n -> Binding n +-- ModuleBinding :: Module n -> Binding n +-- -- TODO: add a case for abstracted pointers, as used in `ClosedImpFunction` +-- PtrBinding :: PtrType -> PtrLitVal -> Binding n +-- SpecializedDictBinding :: SpecializedDictDef n -> Binding n +-- ImpNameBinding :: BaseType -> Binding n +-- deriving (Show, Generic) + +-- -- === ToBinding === + +-- class (RenameE e, SinkableE e) => ToBinding (e::E) where +-- toBinding :: e n -> Binding n + +-- instance ToBinding Binding where +-- toBinding = id + +-- instance ToBinding AtomBinding where +-- toBinding = AtomNameBinding + +-- instance ToBinding Type where +-- toBinding = toBinding . MiscBound + +-- instance ToBinding SolverBinding where +-- toBinding = toBinding . SolverBound + +-- instance (ToBinding e1, ToBinding e2) => ToBinding (EitherE e1 e2) where +-- toBinding (LeftE e) = toBinding e +-- toBinding (RightE e) = toBinding e + +-- -- === GenericE, GenericB === + +-- instance GenericE SpecializedDictDef where +-- type RepE SpecializedDictDef = AbsDict `PairE` MaybeE (ListE STopLam) +-- fromE (SpecializedDict ab methods) = ab `PairE` methods' +-- where methods' = case methods of Just xs -> LeftE (ListE xs) +-- Nothing -> RightE UnitE +-- {-# INLINE fromE #-} +-- toE (ab `PairE` methods) = SpecializedDict ab methods' +-- where methods' = case methods of LeftE (ListE xs) -> Just xs +-- RightE UnitE -> Nothing +-- {-# INLINE toE #-} + +-- instance SinkableE SpecializedDictDef +-- instance HoistableE SpecializedDictDef +-- instance AlphaEqE SpecializedDictDef +-- instance AlphaHashableE SpecializedDictDef +-- instance RenameE SpecializedDictDef + +-- instance HasScope Env where +-- toScope = toScope . envDefs . topEnv + +-- instance OutMap Env where +-- emptyOutMap = +-- Env (TopEnv (RecSubst emptyInFrag) mempty emptyLoadedModules emptyLoadedObjects) +-- emptyModuleEnv +-- {-# INLINE emptyOutMap #-} + +-- instance ExtOutMap Env (RecSubstFrag Binding) where +-- -- TODO: We might want to reorganize this struct to make this +-- -- do less explicit sinking etc. It's a hot operation! +-- extendOutMap (Env (TopEnv defs cache loadedM loadedO) moduleEnv) frag = +-- withExtEvidence frag $ Env +-- (TopEnv +-- (defs `extendRecSubst` frag) +-- (sink cache) +-- (sink loadedM) +-- (sink loadedO)) +-- (sink moduleEnv) +-- {-# INLINE extendOutMap #-} + +-- instance ExtOutMap Env EnvFrag where +-- extendOutMap = extendEnv +-- {-# INLINE extendOutMap #-} + +-- extendEnv :: Distinct l => Env n -> EnvFrag n l -> Env l +-- extendEnv env (EnvFrag newEnv) = do +-- case extendOutMap env newEnv of +-- Env envTop (ModuleEnv imports sm scs) -> do +-- Env envTop (ModuleEnv imports sm scs) +-- {-# NOINLINE [1] extendEnv #-} + +-- instance GenericE Cache where +-- type RepE Cache = +-- EMap SpecializationSpec TopFunName +-- `PairE` EMap LinearizationSpec (PairE TopFunName TopFunName) +-- `PairE` EMap TopFunName TopFunName +-- `PairE` LiftE (M.Map ModuleSourceName (FileHash, [ModuleSourceName])) +-- `PairE` ListE ( LiftE ModuleSourceName +-- `PairE` LiftE FileHash +-- `PairE` ListE ModuleName +-- `PairE` ModuleName) +-- fromE (Cache x y z parseCache evalCache) = +-- x `PairE` y `PairE` z `PairE` LiftE parseCache `PairE` +-- ListE [LiftE sourceName `PairE` LiftE hashVal `PairE` ListE deps `PairE` result +-- | (sourceName, ((hashVal, deps), result)) <- M.toList evalCache ] +-- {-# INLINE fromE #-} +-- toE (x `PairE` y `PairE` z `PairE` LiftE parseCache `PairE` ListE evalCache) = +-- Cache x y z parseCache +-- (M.fromList +-- [(sourceName, ((hashVal, deps), result)) +-- | LiftE sourceName `PairE` LiftE hashVal `PairE` ListE deps `PairE` result +-- <- evalCache]) +-- {-# INLINE toE #-} + +-- instance SinkableE Cache +-- instance HoistableE Cache +-- instance AlphaEqE Cache +-- instance RenameE Cache +-- instance Store (Cache n) + +-- instance Monoid (Cache n) where +-- mempty = Cache mempty mempty mempty mempty mempty +-- mappend = (<>) + +-- instance Semigroup (Cache n) where +-- -- right-biased instead of left-biased +-- Cache x1 x2 x3 x4 x5 <> Cache y1 y2 y3 y4 y5 = +-- Cache (y1<>x1) (y2<>x2) (y3<>x3) (y4<>x4) (x5<>y5) + + +-- instance GenericE SynthCandidates where +-- type RepE SynthCandidates = ListE (PairE ClassName (ListE InstanceName)) +-- `PairE` ListE InstanceName +-- fromE (SynthCandidates xs ys) = ListE xs' `PairE` ListE ys +-- where xs' = map (\(k,vs) -> PairE k (ListE vs)) (M.toList xs) +-- {-# INLINE fromE #-} +-- toE (ListE xs `PairE` ListE ys) = SynthCandidates xs' ys +-- where xs' = M.fromList $ map (\(PairE k (ListE vs)) -> (k,vs)) xs +-- {-# INLINE toE #-} + +-- instance SinkableE SynthCandidates +-- instance HoistableE SynthCandidates +-- instance AlphaEqE SynthCandidates +-- instance AlphaHashableE SynthCandidates +-- instance RenameE SynthCandidates + +-- instance GenericE AtomBinding where +-- type RepE AtomBinding = +-- EitherE4 +-- CExpr -- LetBound +-- Type -- MiscBound +-- (SolverBinding) -- SolverBound +-- (CorePiType `PairE` TopFunName) -- FFIFunBound + +-- fromE = \case +-- LetBound x -> Case0 x +-- MiscBound x -> Case1 x +-- SolverBound x -> Case2 $ x +-- FFIFunBound t v -> Case3 $ t `PairE` v +-- {-# INLINE fromE #-} + +-- toE = \case +-- Case0 x -> LetBound x +-- Case1 x -> MiscBound x +-- Case2 x -> SolverBound x +-- Case3 (ty `PairE` v) -> FFIFunBound ty v +-- _ -> error "impossible" +-- {-# INLINE toE #-} + + +-- instance SinkableE AtomBinding +-- instance HoistableE AtomBinding +-- instance RenameE AtomBinding +-- instance AlphaEqE AtomBinding +-- instance AlphaHashableE AtomBinding +-- instance Store (AtomBinding n) + +-- instance GenericE TopFunDef where +-- type RepE TopFunDef = EitherE3 SpecializationSpec LinearizationSpec LinearizationSpec +-- fromE = \case +-- Specialization s -> Case0 s +-- LinearizationPrimal s -> Case1 s +-- LinearizationTangent s -> Case2 s +-- {-# INLINE fromE #-} +-- toE = \case +-- Case0 s -> Specialization s +-- Case1 s -> LinearizationPrimal s +-- Case2 s -> LinearizationTangent s +-- _ -> error "impossible" +-- {-# INLINE toE #-} + +-- instance SinkableE TopFunDef +-- instance HoistableE TopFunDef +-- instance RenameE TopFunDef +-- instance AlphaEqE TopFunDef +-- instance AlphaHashableE TopFunDef + +-- instance GenericE TopLam where +-- type RepE TopLam = PiType `PairE` LamExpr +-- fromE (TopLam x y) = x `PairE` y +-- {-# INLINE fromE #-} +-- toE (x `PairE` y) = TopLam x y +-- {-# INLINE toE #-} +-- instance SinkableE TopLam +-- instance HoistableE TopLam +-- instance RenameE TopLam +-- instance AlphaEqE TopLam +-- instance AlphaHashableE TopLam +-- instance Store (TopLam n) + +-- instance GenericE TopFun where +-- type RepE TopFun = EitherE +-- (TopFunDef `PairE` STopLam `PairE` ComposeE EvalStatus TopFunLowerings) +-- (LiftE (String, IFunType)) +-- fromE = \case +-- DexTopFun def lam status -> LeftE (def `PairE` lam `PairE` ComposeE status) +-- FFITopFun name ty -> RightE (LiftE (name, ty)) +-- {-# INLINE fromE #-} +-- toE = \case +-- LeftE (def `PairE` lam `PairE` ComposeE status) -> DexTopFun def lam status +-- RightE (LiftE (name, ty)) -> FFITopFun name ty +-- {-# INLINE toE #-} + +-- instance SinkableE TopFun +-- instance HoistableE TopFun +-- instance RenameE TopFun +-- instance AlphaEqE TopFun +-- instance AlphaHashableE TopFun + +-- instance GenericE SpecializationSpec where +-- type RepE SpecializationSpec = +-- PairE Name (Abs (Nest Binder) (ListE CExpr)) +-- fromE (AppSpecialization fname (Abs bs args)) = PairE fname (Abs bs args) +-- {-# INLINE fromE #-} +-- toE (PairE fname (Abs bs args)) = AppSpecialization fname (Abs bs args) +-- {-# INLINE toE #-} + +-- instance HasNameHint (SpecializationSpec n) where +-- getNameHint (AppSpecialization f _) = getNameHint f + +-- instance SinkableE SpecializationSpec +-- instance HoistableE SpecializationSpec +-- instance RenameE SpecializationSpec +-- instance AlphaEqE SpecializationSpec +-- instance AlphaHashableE SpecializationSpec + +-- instance GenericE LinearizationSpec where +-- type RepE LinearizationSpec = PairE TopFunName (LiftE [Active]) +-- fromE (LinearizationSpec fname actives) = PairE fname (LiftE actives) +-- {-# INLINE fromE #-} +-- toE (PairE fname (LiftE actives)) = LinearizationSpec fname actives +-- {-# INLINE toE #-} + +-- instance SinkableE LinearizationSpec +-- instance HoistableE LinearizationSpec +-- instance RenameE LinearizationSpec +-- instance AlphaEqE LinearizationSpec +-- instance AlphaHashableE LinearizationSpec + +-- instance GenericE SolverBinding where +-- type RepE SolverBinding = EitherE3 CType CType CType +-- fromE = \case +-- InfVarBound ty -> Case0 ty +-- SkolemBound ty -> Case1 ty +-- DictBound ty -> Case2 ty +-- {-# INLINE fromE #-} + +-- toE = \case +-- Case0 ty -> InfVarBound ty +-- Case1 ty -> SkolemBound ty +-- Case2 ty -> DictBound ty +-- _ -> error "impossible" +-- {-# INLINE toE #-} +-- instance SinkableE SolverBinding +-- instance HoistableE SolverBinding +-- instance RenameE SolverBinding +-- instance AlphaEqE SolverBinding +-- instance AlphaHashableE SolverBinding +-- instance Store (SolverBinding n) + +-- instance GenericE Binding where +-- type RepE Binding = +-- EitherE3 +-- (EitherE6 +-- (AtomBinding) +-- (MaybeE TyConDef `PairE` DotMethods) +-- (TyConName `PairE` LiftE Int) +-- (ClassDef) +-- (InstanceDef `PairE` CorePiType) +-- (ClassName `PairE` LiftE Int)) +-- (EitherE4 +-- (TopFun) +-- (CFunction) +-- (Module) +-- (LiftE (PtrType, PtrLitVal))) +-- (EitherE2 +-- (SpecializedDictDef) +-- (LiftE BaseType)) + +-- fromE = \case +-- AtomNameBinding binding -> Case0 $ Case0 $ binding +-- TyConBinding dataDef methods -> Case0 $ Case1 $ toMaybeE dataDef `PairE` methods +-- DataConBinding dataDefName idx -> Case0 $ Case2 $ dataDefName `PairE` LiftE idx +-- ClassBinding classDef -> Case0 $ Case3 $ classDef +-- InstanceBinding instanceDef ty -> Case0 $ Case4 $ instanceDef `PairE` ty +-- MethodBinding className idx -> Case0 $ Case5 $ className `PairE` LiftE idx +-- TopFunBinding fun -> Case1 $ Case0 $ fun +-- FunObjCodeBinding cFun -> Case1 $ Case1 $ cFun +-- ModuleBinding m -> Case1 $ Case2 $ m +-- PtrBinding ty p -> Case1 $ Case3 $ LiftE (ty,p) +-- SpecializedDictBinding def -> Case2 $ Case0 $ def +-- ImpNameBinding ty -> Case2 $ Case1 $ LiftE ty +-- {-# INLINE fromE #-} + +-- toE = \case +-- Case0 (Case0 binding) -> AtomNameBinding binding +-- Case0 (Case1 (def `PairE` methods)) -> TyConBinding (fromMaybeE def) methods +-- Case0 (Case2 (n `PairE` LiftE idx)) -> DataConBinding n idx +-- Case0 (Case3 classDef) -> ClassBinding classDef +-- Case0 (Case4 (instanceDef `PairE` ty)) -> InstanceBinding instanceDef ty +-- Case0 (Case5 (n `PairE` LiftE i)) -> MethodBinding n i +-- Case1 (Case0 fun) -> TopFunBinding fun +-- Case1 (Case1 f) -> FunObjCodeBinding f +-- Case1 (Case2 m) -> ModuleBinding m +-- Case1 (Case3 (LiftE (ty,p))) -> PtrBinding ty p +-- Case2 (Case0 def) -> SpecializedDictBinding def +-- Case2 (Case1 (LiftE ty)) -> ImpNameBinding ty +-- _ -> error "impossible" +-- {-# INLINE toE #-} + +-- instance SinkableE Binding +-- instance HoistableE Binding +-- instance RenameE Binding +-- instance Store (Binding n) + +-- instance Semigroup (SynthCandidates n) where +-- SynthCandidates xs ys <> SynthCandidates xs' ys' = +-- SynthCandidates (M.unionWith (<>) xs xs') (ys <> ys') + +-- instance Monoid (SynthCandidates n) where +-- mempty = SynthCandidates mempty mempty + +-- instance GenericB EnvFrag where +-- type RepB EnvFrag = RecSubstFrag Binding +-- fromB (EnvFrag frag) = frag +-- toB frag = EnvFrag frag + +-- instance SinkableB EnvFrag +-- instance HoistableB EnvFrag +-- instance ProvesExt EnvFrag +-- instance BindsNames EnvFrag +-- instance RenameB EnvFrag + +-- instance GenericE TopEnvUpdate where +-- type RepE TopEnvUpdate = EitherE2 ( +-- EitherE3 +-- {- ExtendCache -} Cache +-- {- UpdateLoadedModules -} (LiftE ModuleSourceName `PairE` ModuleName) +-- {- UpdateLoadedObjects -} (FunObjCodeName `PairE` LiftE NativeFunction) +-- ) ( EitherE4 +-- {- UpdateTopFunEvalStatus -} (TopFunName `PairE` ComposeE EvalStatus TopFunLowerings) +-- {- UpdateInstanceDef -} (InstanceName `PairE` InstanceDef) +-- {- UpdateTyConDef -} (TyConName `PairE` TyConDef) +-- {- UpdateFieldDef -} (TyConName `PairE` LiftE SourceName `PairE` Name) +-- ) +-- fromE = \case +-- ExtendCache x -> Case0 $ Case0 x +-- UpdateLoadedModules x y -> Case0 $ Case1 (LiftE x `PairE` y) +-- UpdateLoadedObjects x y -> Case0 $ Case2 (x `PairE` LiftE y) +-- UpdateTopFunEvalStatus x y -> Case1 $ Case0 (x `PairE` ComposeE y) +-- UpdateInstanceDef x y -> Case1 $ Case1 (x `PairE` y) +-- UpdateTyConDef x y -> Case1 $ Case2 (x `PairE` y) +-- UpdateFieldDef x y z -> Case1 $ Case3 (x `PairE` LiftE y `PairE` z) + +-- toE = \case +-- Case0 e -> case e of +-- Case0 x -> ExtendCache x +-- Case1 (LiftE x `PairE` y) -> UpdateLoadedModules x y +-- Case2 (x `PairE` LiftE y) -> UpdateLoadedObjects x y +-- _ -> error "impossible" +-- Case1 e -> case e of +-- Case0 (x `PairE` ComposeE y) -> UpdateTopFunEvalStatus x y +-- Case1 (x `PairE` y) -> UpdateInstanceDef x y +-- Case2 (x `PairE` y) -> UpdateTyConDef x y +-- Case3 (x `PairE` LiftE y `PairE` z) -> UpdateFieldDef x y z +-- _ -> error "impossible" +-- _ -> error "impossible" + +-- instance SinkableE TopEnvUpdate +-- instance HoistableE TopEnvUpdate +-- instance RenameE TopEnvUpdate + +-- instance GenericB TopEnvFrag where +-- type RepB TopEnvFrag = PairB EnvFrag (LiftB (ModuleEnv `PairE` ListE TopEnvUpdate)) +-- fromB (TopEnvFrag x y (ReversedList z)) = PairB x (LiftB (y `PairE` ListE z)) +-- toB (PairB x (LiftB (y `PairE` ListE z))) = TopEnvFrag x y (ReversedList z) + +-- instance RenameB TopEnvFrag +-- instance HoistableB TopEnvFrag +-- instance SinkableB TopEnvFrag +-- instance ProvesExt TopEnvFrag +-- instance BindsNames TopEnvFrag + +-- instance OutFrag TopEnvFrag where +-- emptyOutFrag = TopEnvFrag emptyOutFrag mempty mempty +-- {-# INLINE emptyOutFrag #-} +-- catOutFrags (TopEnvFrag frag1 env1 partial1) +-- (TopEnvFrag frag2 env2 partial2) = +-- withExtEvidence frag2 $ +-- TopEnvFrag +-- (catOutFrags frag1 frag2) +-- (sink env1 <> env2) +-- (sinkSnocList partial1 <> partial2) +-- {-# INLINE catOutFrags #-} + +-- -- XXX: unlike `ExtOutMap Env EnvFrag` instance, this once doesn't +-- -- extend the synthesis candidates based on the annotated let-bound names. It +-- -- only extends synth candidates when they're supplied explicitly. +-- instance ExtOutMap Env TopEnvFrag where +-- extendOutMap env (TopEnvFrag (EnvFrag frag) mEnv' otherUpdates) = do +-- let newerTopEnv = foldl applyUpdate newTopEnv otherUpdates +-- Env newerTopEnv newModuleEnv +-- where +-- Env (TopEnv defs cache loadedM loadedO) mEnv = env + +-- newTopEnv = withExtEvidence frag $ TopEnv +-- (defs `extendRecSubst` frag) (sink cache) (sink loadedM) (sink loadedO) + +-- newModuleEnv = +-- ModuleEnv +-- (imports <> imports') +-- (sm <> sm' <> newImportedSM) +-- (scs <> scs' <> newImportedSC) +-- where +-- ModuleEnv imports sm scs = withExtEvidence frag $ sink mEnv +-- ModuleEnv imports' sm' scs' = mEnv' +-- newDirectImports = S.difference (directImports imports') (directImports imports) +-- newTransImports = S.difference (transImports imports') (transImports imports) +-- newImportedSM = flip foldMap newDirectImports $ moduleExports . lookupModulePure +-- newImportedSC = flip foldMap newTransImports $ moduleSynthCandidates . lookupModulePure + +-- lookupModulePure v = case lookupEnvPure newTopEnv v of ModuleBinding m -> m + +-- applyUpdate :: TopEnv n -> TopEnvUpdate n -> TopEnv n +-- applyUpdate e = \case +-- ExtendCache cache -> e { envCache = envCache e <> cache} +-- UpdateLoadedModules x y -> e { envLoadedModules = envLoadedModules e <> LoadedModules (M.singleton x y)} +-- UpdateLoadedObjects x y -> e { envLoadedObjects = envLoadedObjects e <> LoadedObjects (M.singleton x y)} +-- UpdateTopFunEvalStatus f s -> do +-- case lookupEnvPure e f of +-- TopFunBinding (DexTopFun def lam _) -> +-- updateEnv f (TopFunBinding $ DexTopFun def lam s) e +-- _ -> error "can't update ffi function impl" +-- UpdateInstanceDef name def -> do +-- case lookupEnvPure e name of +-- InstanceBinding _ ty -> updateEnv name (InstanceBinding def ty) e +-- UpdateTyConDef name def -> do +-- let TyConBinding _ methods = lookupEnvPure e name +-- updateEnv name (TyConBinding (Just def) methods) e +-- UpdateFieldDef name sn x -> do +-- let TyConBinding def methods = lookupEnvPure e name +-- updateEnv name (TyConBinding def (methods <> DotMethods (M.singleton sn x))) e + +-- updateEnv :: Name n -> Binding n -> TopEnv n -> TopEnv n +-- updateEnv v rhs env = +-- env { envDefs = RecSubst $ updateSubstFrag v rhs bs } +-- where (RecSubst bs) = envDefs env + +-- lookupEnvPure :: TopEnv n -> Name n -> Binding n +-- lookupEnvPure env v = lookupTerminalSubstFrag (fromRecSubst $ envDefs $ env) v + +-- instance GenericE Module where +-- type RepE Module = LiftE ModuleSourceName +-- `PairE` ListE ModuleName +-- `PairE` ListE ModuleName +-- `PairE` SourceMap +-- `PairE` SynthCandidates + +-- fromE (Module name deps transDeps sm sc) = +-- LiftE name `PairE` ListE (S.toList deps) `PairE` ListE (S.toList transDeps) +-- `PairE` sm `PairE` sc +-- {-# INLINE fromE #-} + +-- toE (LiftE name `PairE` ListE deps `PairE` ListE transDeps +-- `PairE` sm `PairE` sc) = +-- Module name (S.fromList deps) (S.fromList transDeps) sm sc +-- {-# INLINE toE #-} + +-- instance SinkableE Module +-- instance HoistableE Module +-- instance AlphaEqE Module +-- instance AlphaHashableE Module +-- instance RenameE Module + +-- instance GenericE ImportStatus where +-- type RepE ImportStatus = ListE ModuleName `PairE` ListE ModuleName +-- fromE (ImportStatus direct trans) = ListE (S.toList direct) +-- `PairE` ListE (S.toList trans) +-- {-# INLINE fromE #-} +-- toE (ListE direct `PairE` ListE trans) = +-- ImportStatus (S.fromList direct) (S.fromList trans) +-- {-# INLINE toE #-} + +-- instance SinkableE ImportStatus +-- instance HoistableE ImportStatus +-- instance AlphaEqE ImportStatus +-- instance AlphaHashableE ImportStatus +-- instance RenameE ImportStatus + +-- instance Semigroup (ImportStatus n) where +-- ImportStatus direct trans <> ImportStatus direct' trans' = +-- ImportStatus (direct <> direct') (trans <> trans') + +-- instance Monoid (ImportStatus n) where +-- mappend = (<>) +-- mempty = ImportStatus mempty mempty + +-- instance GenericE LoadedModules where +-- type RepE LoadedModules = ListE (PairE (LiftE ModuleSourceName) ModuleName) +-- fromE (LoadedModules m) = +-- ListE $ M.toList m <&> \(v,md) -> PairE (LiftE v) md +-- {-# INLINE fromE #-} +-- toE (ListE pairs) = +-- LoadedModules $ M.fromList $ pairs <&> \(PairE (LiftE v) md) -> (v, md) +-- {-# INLINE toE #-} + +-- instance SinkableE LoadedModules +-- instance HoistableE LoadedModules +-- instance AlphaEqE LoadedModules +-- instance AlphaHashableE LoadedModules +-- instance RenameE LoadedModules + +-- instance GenericE LoadedObjects where +-- type RepE LoadedObjects = ListE (PairE FunObjCodeName (LiftE NativeFunction)) +-- fromE (LoadedObjects m) = +-- ListE $ M.toList m <&> \(v,p) -> PairE v (LiftE p) +-- {-# INLINE fromE #-} +-- toE (ListE pairs) = +-- LoadedObjects $ M.fromList $ pairs <&> \(PairE v (LiftE p)) -> (v, p) +-- {-# INLINE toE #-} + +-- instance SinkableE LoadedObjects +-- instance HoistableE LoadedObjects +-- instance RenameE LoadedObjects + +-- instance GenericE ModuleEnv where +-- type RepE ModuleEnv = ImportStatus +-- `PairE` SourceMap +-- `PairE` SynthCandidates +-- fromE (ModuleEnv imports sm sc) = imports `PairE` sm `PairE` sc +-- {-# INLINE fromE #-} +-- toE (imports `PairE` sm `PairE` sc) = ModuleEnv imports sm sc +-- {-# INLINE toE #-} + +-- instance SinkableE ModuleEnv +-- instance HoistableE ModuleEnv +-- instance AlphaEqE ModuleEnv +-- instance AlphaHashableE ModuleEnv +-- instance RenameE ModuleEnv + +-- instance Semigroup (ModuleEnv n) where +-- ModuleEnv x1 x2 x3 <> ModuleEnv y1 y2 y3 = +-- ModuleEnv (x1<>y1) (x2<>y2) (x3<>y3) + +-- instance Monoid (ModuleEnv n) where +-- mempty = ModuleEnv mempty mempty mempty + +-- instance Semigroup (LoadedModules n) where +-- LoadedModules m1 <> LoadedModules m2 = LoadedModules (m2 <> m1) + +-- instance Monoid (LoadedModules n) where +-- mempty = LoadedModules mempty + +-- instance Semigroup (LoadedObjects n) where +-- LoadedObjects m1 <> LoadedObjects m2 = LoadedObjects (m2 <> m1) + +-- instance Monoid (LoadedObjects n) where +-- mempty = LoadedObjects mempty + +-- -- === instance === + +-- prettyRecord :: [(String, Doc ann)] -> Doc ann +-- prettyRecord xs = foldMap (\(name, val) -> pretty name <> indented val) xs + +-- instance Pretty (TopEnv n) where +-- pretty (TopEnv defs cache _ _) = +-- prettyRecord [ ("Defs" , pretty defs) +-- , ("Cache", pretty cache) ] + +-- instance Pretty (ImportStatus n) where +-- pretty imports = pretty $ S.toList $ directImports imports + +-- instance Pretty (ModuleEnv n) where +-- pretty (ModuleEnv imports sm sc) = +-- prettyRecord [ ("Imports" , pretty imports) +-- , ("Source map" , pretty sm) +-- , ("Synth candidates", pretty sc) ] + +-- instance Pretty (Env n) where +-- pretty (Env env1 env2) = +-- prettyRecord [ ("Top env" , pretty env1) +-- , ("Module env", pretty env2)] + +-- instance Pretty (SolverBinding n) where +-- pretty (InfVarBound ty) = "Inference variable of type:" <+> pretty ty +-- pretty (SkolemBound ty) = "Skolem variable of type:" <+> pretty ty +-- pretty (DictBound ty) = "Dictionary variable of type:" <+> pretty ty + +-- instance Pretty (Binding n) where +-- pretty b = case b of +-- AtomNameBinding info -> "Atom name:" <+> pretty info +-- TyConBinding dataDef _ -> "Type constructor: " <+> pretty dataDef +-- DataConBinding tyConName idx -> "Data constructor:" <+> +-- pretty tyConName <+> "Constructor index:" <+> pretty idx +-- ClassBinding classDef -> pretty classDef +-- InstanceBinding instanceDef _ -> pretty instanceDef +-- MethodBinding className idx -> "Method" <+> pretty idx <+> "of" <+> pretty className +-- TopFunBinding f -> pretty f +-- FunObjCodeBinding _ -> "" +-- ModuleBinding _ -> "" +-- PtrBinding _ _ -> "" +-- SpecializedDictBinding _ -> "" +-- ImpNameBinding ty -> "Imp name of type: " <+> pretty ty + +-- instance Pretty (Module n) where +-- pretty m = prettyRecord +-- [ ("moduleSourceName" , pretty $ moduleSourceName m) +-- , ("moduleDirectDeps" , pretty $ S.toList $ moduleDirectDeps m) +-- , ("moduleTransDeps" , pretty $ S.toList $ moduleTransDeps m) +-- , ("moduleExports" , pretty $ moduleExports m) +-- , ("moduleSynthCandidates", pretty $ moduleSynthCandidates m) ] + +-- instance Pretty a => Pretty (EvalStatus a) where +-- pretty = \case +-- Waiting -> "" +-- Running -> "" +-- Finished a -> pretty a + +-- instance Pretty (EnvFrag n l) where +-- pretty (EnvFrag bindings) = pretty bindings + +-- instance Pretty (Cache n) where +-- pretty (Cache _ _ _ _ _) = "" -- TODO + +-- instance Pretty (SynthCandidates n) where +-- pretty scs = "instance dicts:" <+> pretty (M.toList $ instanceDicts scs) + +-- instance Pretty (LoadedModules n) where +-- pretty _ = "" + +-- instance Pretty (TopFunDef n) where +-- pretty = \case +-- Specialization s -> pretty s +-- LinearizationPrimal _ -> "" +-- LinearizationTangent _ -> "" + +-- instance Pretty (TopFun n) where +-- pretty = \case +-- DexTopFun def lam lowering -> +-- "Top-level Function" +-- <> hardline <+> "definition:" <+> pretty def +-- <> hardline <+> "lambda:" <+> pretty lam +-- <> hardline <+> "lowering:" <+> pretty lowering +-- FFITopFun f _ -> pretty f + +-- instance Pretty (TopLam n) where +-- pretty (TopLam _ lam) = pretty lam + +-- instance Pretty (AtomBinding n) where +-- pretty binding = case binding of +-- LetBound b -> pretty b +-- MiscBound t -> pretty t +-- SolverBound b -> pretty b +-- FFIFunBound s _ -> pretty s + +-- instance Pretty (SpecializationSpec n) where +-- pretty (AppSpecialization f (Abs bs (ListE args))) = +-- "Specialization" <+> pretty f <+> pretty bs <+> pretty args + +-- instance Hashable a => Hashable (EvalStatus a) + +-- instance Store (SynthCandidates n) +-- instance Store (Module n) +-- instance Store (ImportStatus n) +-- instance Store (TopFunLowerings n) +-- instance Store a => Store (EvalStatus a) +-- instance Store (TopFun n) +-- instance Store (TopFunDef n) +-- instance Store (ModuleEnv n) +-- instance Store (SerializedEnv n) +-- instance Store (LinearizationSpec n) +-- instance Store (SpecializedDictDef n) +-- instance Store (SpecializationSpec n) diff --git a/src/lib/Builder.hs b/src/old/Builder.hs similarity index 100% rename from src/lib/Builder.hs rename to src/old/Builder.hs diff --git a/src/lib/CheapReduction.hs b/src/old/CheapReduction.hs similarity index 100% rename from src/lib/CheapReduction.hs rename to src/old/CheapReduction.hs diff --git a/src/lib/Core.hs b/src/old/Core.hs similarity index 100% rename from src/lib/Core.hs rename to src/old/Core.hs diff --git a/src/lib/DPS.hs b/src/old/DPS.hs similarity index 100% rename from src/lib/DPS.hs rename to src/old/DPS.hs diff --git a/src/lib/Generalize.hs b/src/old/Generalize.hs similarity index 100% rename from src/lib/Generalize.hs rename to src/old/Generalize.hs diff --git a/src/lib/Imp.hs b/src/old/Imp.hs similarity index 100% rename from src/lib/Imp.hs rename to src/old/Imp.hs diff --git a/src/lib/ImpToLLVM.hs b/src/old/ImpToLLVM.hs similarity index 100% rename from src/lib/ImpToLLVM.hs rename to src/old/ImpToLLVM.hs diff --git a/src/lib/Inference.hs b/src/old/Inference.hs similarity index 100% rename from src/lib/Inference.hs rename to src/old/Inference.hs diff --git a/src/old/QueryType.hs b/src/old/QueryType.hs new file mode 100644 index 000000000..24aeb1c28 --- /dev/null +++ b/src/old/QueryType.hs @@ -0,0 +1,220 @@ +-- Copyright 2022 Google LLC +-- +-- Use of this source code is governed by a BSD-style +-- license that can be found in the LICENSE file or at +-- https://developers.google.com/open-source/licenses/bsd + +module QueryType (module QueryType, module QueryTypePure, toAtomVar) where + +import Control.Category ((>>>)) +import Control.Monad +import Control.Applicative +import Data.List (elemIndex) +import Data.Maybe (fromJust) +import Data.Functor ((<&>)) + +import Types.Primitives +import Types.Complicated +import Types.Simple +import Types.Source hiding (TCName (..)) +import Types.Top2 +import Types.Imp +import Name hiding (withFreshM) +-- import Subst +import Util +import PPrint +import QueryTypePure + +-- === Exposed helpers for querying types and effects === + +caseAltsBinderTys :: ScopeReader m => Type n -> m n [Type n] +caseAltsBinderTys ty = case ty of + TyCon (SumType types) -> return types -- need this case? + TyCon (NewtypeTyCon t) -> case t of + UserADTType _ defName params -> do + def <- lookupTyCon defName + ~(ADTCons cons) <- instantiateTyConDef def params + return [repTy | DataConDef _ _ repTy _ <- cons] + _ -> error msg + _ -> error msg + where msg = "Case analysis only supported on ADTs, not on " ++ pprint ty + +piTypeWithoutDest :: PiType n -> PiType n +piTypeWithoutDest (PiType bsRefB _) = + case popNest bsRefB of + Just (PairB bs (_:>RefTy ansTy)) -> PiType bs ansTy + _ -> error "expected trailing dest binder" + +typeOfTabApp :: ScopeReader m => Type n -> Atom n -> m n (Type n) +typeOfTabApp (TyCon (TabPi tabTy)) i = instantiate tabTy [i] +typeOfTabApp ty _ = error $ "expected a table type. Got: " ++ pprint ty + +typeOfApplyMethod :: ScopeReader m => CDict n -> Int -> [CAtom n] -> m n (EffTy n) +typeOfApplyMethod d i args = do + ty <- toType <$> getMethodType d i + appEffTy ty args + +typeOfTopApp :: ScopeReader m => TopFunName n -> [SAtom n] -> m n (EffTy n) +typeOfTopApp f xs = do + piTy <- getTypeTopFun f + ty <- instantiate piTy xs + return $ EffTy undefined ty -- TODO + +typeOfIndexRef :: (ScopeReader m, Fallible1 m) => Type n -> Atom n -> m n (Type n) +typeOfIndexRef (TyCon (RefType s)) i = do + TyCon (TabPi tabPi) <- return s + eltTy <- instantiate tabPi [i] + return $ toType $ RefType eltTy +typeOfIndexRef _ _ = error "expected a ref type" + +typeOfProjRef :: ScopeReader m => Type n -> Projection -> m n (Type n) +typeOfProjRef (TyCon (RefType s)) p = do + toType . RefType <$> case p of + ProjectProduct i -> do + ~(TyCon (ProdType tys)) <- return s + return $ tys !! i + UnwrapNewtype -> do + case s of + TyCon (NewtypeTyCon tc) -> snd <$> unwrapNewtypeType tc + _ -> error "expected a newtype" +typeOfProjRef _ _ = error "expected a reference" + +appEffTy :: ScopeReader m => Type n -> [Atom n] -> m n (EffTy n) +appEffTy (TyCon (Pi piTy)) xs = do + ty <- instantiate piTy xs + return $ EffTy Effectful ty -- TODO: don't assume Effectful +appEffTy t _ = error $ "expected a pi type, got: " ++ pprint t + +partialAppType :: ScopeReader m => Type n -> [Atom n] -> m n (Type n) +partialAppType (TyCon (Pi (CorePiType appExpl expls bs effTy))) xs = do + (_, expls2) <- return $ splitAt (length xs) expls + PairB bs1 bs2 <- return $ splitNestAt (length xs) bs + instantiate (Abs bs1 (toType $ CorePiType appExpl expls2 bs2 effTy)) xs +partialAppType _ _ = error "expected a pi type" + +typeOfHof :: ScopeReader m => Hof n -> m n (Type n) +typeOfHof = \case + For _ ixTy f -> getLamExprType f >>= \case + Abs (UnaryNest b) eltTy -> return $ TabTy (ixTypeDict ixTy) b eltTy + _ -> error "expected a unary pi type" + While _ -> return UnitTy + +getMethodIndex :: ScopeReader m => ClassName n -> SourceName -> m n Int +getMethodIndex className methodSourceName = do + ClassDef _ _ methodNames _ _ _ _ _ <- lookupClassDef className + case elemIndex methodSourceName methodNames of + Nothing -> error $ pprint methodSourceName ++ " is not a method of " ++ pprint className + Just i -> return i +{-# INLINE getMethodIndex #-} + +getMethodNameType :: ScopeReader m => TopName -> m n (CType n) +getMethodNameType v = undefined -- liftScopeReaderM $ lookupEnv v >>= \case +-- getMethodNameType v = liftScopeReaderM $ lookupEnv v >>= \case +-- MethodBinding className i -> do +-- ClassDef _ _ _ paramNames _ paramBs scBinders methodTys <- lookupClassDef className +-- refreshAbs (Abs paramBs $ Abs scBinders (methodTys !! i)) \paramBs' absPiTy -> do +-- let params = toAtom <$> bindersVars paramBs' +-- dictTy <- toType <$> dictType (sink className) params +-- withFreshBinder noHint dictTy \dictB -> do +-- scDicts <- getSuperclassDicts (toDict $ binderVar dictB) +-- CorePiType appExpl methodExpls methodBs effTy <- instantiate (sink absPiTy) scDicts +-- let paramExpls = paramNames <&> \name -> Inferred name Unify +-- let expls = paramExpls <> [Inferred Nothing (Synth $ Partial $ succ i)] <> methodExpls +-- return $ toType $ CorePiType appExpl expls (paramBs' >>> UnaryNest dictB >>> methodBs) effTy + +getMethodType :: ScopeReader m => Dict n -> Int -> m n (CorePiType n) +getMethodType dict i = undefined +-- getMethodType dict i = do +-- ~(TyCon (DictTy dictTy)) <- return $ getType dict +-- case dictTy of +-- DictType _ className params -> liftScopeReaderM $ withSubstReaderT do +-- superclassDicts <- getSuperclassDicts dict +-- classDef <- lookupClassDef className +-- withInstantiated classDef params \ab -> do +-- withInstantiated ab superclassDicts \(ListE methodTys) -> +-- substM $ methodTys !! i +-- IxDictType ixTy -> liftScopeReaderM case i of +-- 0 -> mkCorePiType [] NatTy -- size' : () -> Nat +-- 1 -> mkCorePiType [ixTy] NatTy -- ordinal : (n) -> Nat +-- 2 -> mkCorePiType [NatTy] ixTy -- unsafe_from_ordinal : (Nat) -> n +-- _ -> error "Ix only has three methods" + +mkCorePiType :: ScopeReader m => [CType n] -> CType n -> m n (CorePiType n) +mkCorePiType argTys resultTy = liftScopeReaderM $ withFreshBinders argTys \bs _ -> do + expls <- return $ nestToList (const Explicit) bs + return $ CorePiType ExplicitApp expls bs (sink resultTy) + +getTyConNameType :: ScopeReader m => TyConName n -> m n (Type n) +getTyConNameType v = do + TyConDef _ expls bs _ <- lookupTyCon v + case bs of + Empty -> return $ toType $ Kind TypeKind + _ -> return $ toType $ CorePiType ExplicitApp expls bs $ toType $ Kind TypeKind + +type DataConName = TopName +getDataConNameType :: ScopeReader m => DataConName -> m n (Type VoidS) +getDataConNameType dataCon = liftScopeReaderM $ withSubstReaderT do + (tyCon, i) <- lookupDataCon dataCon + tyConDef <- lookupTyCon tyCon + buildDataConType tyConDef \expls paramBs' paramVs params -> do + withInstantiatedNames tyConDef paramVs \(ADTCons dataCons) -> do + DataConDef _ ab _ _ <- renameM (dataCons !! i) + refreshAbs ab \dataBs UnitE -> do + let appExpl = case dataBs of Empty -> ImplicitApp + _ -> ExplicitApp + let resultTy = toType $ UserADTType (getSourceName tyConDef) (sink tyCon) (sink params) + let dataExpls = nestToList (const $ Explicit) dataBs + return $ toType $ CorePiType appExpl (expls <> dataExpls) (paramBs' >>> dataBs) resultTy + +getStructDataConType :: ScopeReader m => TyConName n -> m n (CType n) +getStructDataConType tyCon = liftScopeReaderM $ withSubstReaderT do + tyConDef <- lookupTyCon tyCon + buildDataConType tyConDef \expls paramBs' paramVs params -> do + withInstantiatedNames tyConDef paramVs \(StructFields fields) -> do + fieldTys <- forM fields \(_, t) -> renameM t + let resultTy = toType $ UserADTType (getSourceName tyConDef) (sink tyCon) params + Abs dataBs resultTy' <- return $ typesAsBinderNest fieldTys resultTy + let dataExpls = nestToList (const Explicit) dataBs + return $ toType $ CorePiType ExplicitApp (expls <> dataExpls) (paramBs' >>> dataBs) resultTy' + +buildDataConType + :: (ScopeReader m) + => TyConDef n + -> (forall l. DExt n l => [Explicitness] -> Nest CBinder n l -> [Name l] -> TyConParams l -> m l a) + -> m n a +buildDataConType (TyConDef _ expls bs _) cont = undefined +-- buildDataConType (TyConDef _ expls bs _) cont = do +-- expls' <- forM expls \case +-- Explicit -> return $ Inferred Nothing Unify +-- expl -> return $ expl +-- refreshAbs (Abs bs UnitE) \bs' UnitE -> do +-- let vs = nestToNames bs' +-- vs' <- mapM toAtomVar vs +-- cont expls' bs' vs $ TyConParams expls (toAtom <$> vs') + +makeTyConParams :: ScopeReader m => TyConName n -> [CExpr n] -> m n (TyConParams n) +makeTyConParams tc params = do + TyConDef _ expls _ _ <- lookupTyCon tc + return $ TyConParams expls params + +getSuperclassDicts :: ScopeReader m => CExpr n -> m n ([CExpr n]) +getSuperclassDicts dict = undefined +-- getSuperclassDicts dict = do +-- case getType dict of +-- TyCon (DictTy dTy) -> do +-- ts <- getSuperclassTys dTy +-- forM (enumerate ts) \(i, _) -> reduceSuperclassProj i dict +-- _ -> error "expected a dict type" + +getSuperclassTys :: ScopeReader m => DictType n -> m n [CType n] +getSuperclassTys = \case + DictType _ className params -> do + ClassDef _ _ _ _ _ bs superclasses _ <- lookupClassDef className + forM [0 .. nestLength superclasses - 1] \i -> do + instantiate (Abs bs $ getSuperclassType REmpty superclasses i) params + IxDictType _ -> return [] + +asTopLam :: ScopeReader m => LamExpr n -> m n (TopLam n) +asTopLam lam = do + piTy <- getLamExprType lam + return $ TopLam False piTy lam diff --git a/src/lib/Runtime.hs b/src/old/Runtime.hs similarity index 99% rename from src/lib/Runtime.hs rename to src/old/Runtime.hs index c9a336386..ed8a52f38 100644 --- a/src/lib/Runtime.hs +++ b/src/old/Runtime.hs @@ -29,7 +29,7 @@ import Err import MonadUtil import PPrint () -import Types.Top hiding (DexDestructor) +import Types.Top2 import Types.Source hiding (CInt) import Types.Primitives diff --git a/src/lib/Simplify.hs b/src/old/Simplify.hs similarity index 100% rename from src/lib/Simplify.hs rename to src/old/Simplify.hs diff --git a/src/lib/Subst.hs b/src/old/Subst.hs similarity index 100% rename from src/lib/Subst.hs rename to src/old/Subst.hs diff --git a/src/lib/Types/Top.hs b/src/old/Top.hs similarity index 100% rename from src/lib/Types/Top.hs rename to src/old/Top.hs diff --git a/src/lib/TopLevel.hs b/src/old/TopLevel.hs similarity index 100% rename from src/lib/TopLevel.hs rename to src/old/TopLevel.hs