From 4f03eaebf95f1855040a3cb151189d117567de47 Mon Sep 17 00:00:00 2001 From: Dougal Date: Mon, 26 Aug 2024 09:06:09 -0400 Subject: [PATCH] wip --- dex.cabal | 4 +- src/lib/AbstractSyntax.hs | 28 +- src/lib/ConcreteSyntax.hs | 3 +- src/lib/Inference.hs | 2274 +++++++++++++++++++++++++++++++++ src/lib/SourceRename.hs | 63 +- src/lib/Subst.hs | 510 ++++++++ src/lib/TopLevel2.hs | 124 +- src/lib/Types/Complicated.hs | 21 + src/lib/Types/Primitives.hs | 1 - src/lib/Types/Source.hs | 6 + src/old/Inference.hs | 2299 ---------------------------------- src/old/Subst.hs | 512 -------- 12 files changed, 2909 insertions(+), 2936 deletions(-) create mode 100644 src/lib/Inference.hs create mode 100644 src/lib/Subst.hs delete mode 100644 src/old/Inference.hs delete mode 100644 src/old/Subst.hs diff --git a/dex.cabal b/dex.cabal index a8c2b6882..98dd56d8c 100644 --- a/dex.cabal +++ b/dex.cabal @@ -53,7 +53,7 @@ library -- , Imp -- , ImpToLLVM , IncState - -- , Inference + , Inference -- , Inline -- , JAX.Concrete -- , JAX.Rename @@ -77,7 +77,7 @@ library -- , RuntimePrint -- , Serialize -- , Simplify - -- , Subst + , Subst , SourceRename , SourceIdTraversal , TopLevel2 diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs index 81a242de2..d221b6893 100644 --- a/src/lib/AbstractSyntax.hs +++ b/src/lib/AbstractSyntax.hs @@ -101,9 +101,8 @@ checkSourceBlockParses = \case type SyntaxM = Except 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) +topDecl (WithSrcs sid sids topDecl') = case topDecl' of + CSDecl ann d -> topCSDecl ann (WithSrcs sid sids d) -- CData name tyConParams givens constructors -> do -- tyConParams' <- fromMaybeM tyConParams Empty aExplicitParams -- givens' <- aOptGivens givens @@ -132,6 +131,29 @@ topDecl (WithSrcs sid sids topDecl') = undefined -- return $ UInterface params' methodTys (fromSourceNameW name) (toNest methodNames) -- CInstanceDecl def -> aInstanceDef def +topCSDecl :: LetAnn -> CSDeclW -> SyntaxM UTopDecl +topCSDecl ann (WithSrcs sid _ d) = case d of + CLet binder rhs -> do + (b, ann) <- topBinderOptAnn binder + UTopLet b ann <$> (asExpr <$> block rhs) + CDefDecl def -> do + (name, lam) <- aDef def + return $ UTopLet (fromSourceNameW name) Nothing (WithSrcE sid (ULam lam)) + CExpr g -> UTopExpr <$> expr g + CPass -> error "not implemented" + +-- Binder pattern with an optional type annotation +topBinderOptAnn :: GroupW -> SyntaxM (TopBinder, Maybe (UType VoidS)) +topBinderOptAnn = \case + WithSrcs _ _ (CBin Colon lhs typeAnn) -> (,) <$> topBinder lhs <*> (Just <$> expr typeAnn) + WithSrcs _ _ (CParens [g]) -> topBinderOptAnn g + g -> (,Nothing) <$> topBinder g + +topBinder :: GroupW -> SyntaxM TopBinder +topBinder (WithSrcs sid _ b) = case b of + CLeaf (CIdentifier name) -> return $ fromSourceNameW $ WithSrc sid name + _ -> throw sid UnexpectedBinder + decl :: LetAnn -> CSDeclW -> SyntaxM (UDecl VoidS VoidS) decl ann (WithSrcs sid _ d) = WithSrcB sid <$> case d of CLet binder rhs -> do diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs index d62405e5b..50ae48149 100644 --- a/src/lib/ConcreteSyntax.hs +++ b/src/lib/ConcreteSyntax.hs @@ -56,7 +56,8 @@ parseUModule name s = do {-# SCC parseUModule #-} preludeImportBlock :: SourceBlock -preludeImportBlock = SourceBlock 0 0 "" mempty (Misc $ ImportModule Prelude) +preludeImportBlock = SourceBlock 0 0 "" mempty (Misc EmptyLines) +-- preludeImportBlock = SourceBlock 0 0 "" mempty (Misc $ ImportModule Prelude) sourceBlocks :: Parser [SourceBlock] sourceBlocks = manyTill (sourceBlock <* outputLines) eof diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs new file mode 100644 index 000000000..90d1e6e29 --- /dev/null +++ b/src/lib/Inference.hs @@ -0,0 +1,2274 @@ +-- Copyright 2021 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 #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Inference (inferTopUDecl) where + +import Prelude hiding ((.), id) +import Control.Category +import Control.Applicative +import Control.Monad +import Control.Monad.State.Strict +import Control.Monad.Reader +import Data.Either (partitionEithers) +import Data.Foldable (asum) +import Data.Functor ((<&>)) +import Data.List (sortOn) +import Data.Maybe (fromJust, fromMaybe, catMaybes) +import Data.Word +import qualified Data.HashMap.Strict as HM +import qualified Data.Map.Strict as M +import GHC.Generics (Generic (..)) + +import Err +import MonadUtil +import MTL1 +import Name +import PPrint +import QueryTypePure +import Types.Complicated +import Types.Imp +import Types.Primitives +import qualified Types.Source as S +import Subst +import Types.Source hiding (ConName (..), TCName (..), CTopDecl) +import Types.Top2 +import Util hiding (group) + +-- === Top-level interface === + +inferTopUDecl :: (Fallible m, TopLogger m) => UTopDecl -> m CTopDecl +inferTopUDecl decl = liftInfererM $ case decl of + UTopLet (WithSrc _ b) maybeTy expr -> do + expr' <- checkMaybeAnnExpr maybeTy expr + return $ CTopLet b expr' + + +-- (UStructDecl tc def) result = undefined +-- tc' <- emitBinding (getNameHint tc) $ TyConBinding Nothing (DotMethods mempty) +-- def' <- liftInfererM $ extendRenamer (tc@>tc') $ inferStructDef def +-- updateTopEnv $ UpdateTyConDef tc' def' +-- UStructDef _ paramBs _ methods <- return def +-- forM_ methods \(letAnn, methodName, methodDef) -> do +-- method <- liftInfererM $ extendRenamer (tc@>tc') $ +-- inferDotMethod tc' (Abs paramBs methodDef) +-- method' <- emitTopLet (getNameHint methodName) letAnn (Atom $ toAtom $ Lam method) +-- updateTopEnv $ UpdateFieldDef tc' methodName (atomVarName method') +-- UDeclResultDone <$> applyRename (tc @> tc') result +-- inferTopUDecl (UDataDefDecl def tc dcs) result = do +-- tcDef@(TyConDef _ _ _ (ADTCons dataCons)) <- liftInfererM $ inferTyConDef def +-- tc' <- emitBinding (getNameHint tcDef) $ TyConBinding (Just tcDef) (DotMethods mempty) +-- dcs' <- forM (enumerate dataCons) \(i, dcDef) -> +-- emitBinding (getNameHint dcDef) $ DataConBinding tc' i +-- let subst = tc @> tc' <.> dcs @@> dcs' +-- UDeclResultDone <$> applyRename subst result +-- inferTopUDecl (UInterface paramBs methodTys className methodNames) result = do +-- let sn = getSourceName className +-- let methodSourceNames = nestToList getSourceName methodNames +-- classDef <- liftInfererM $ inferClassDef sn methodSourceNames paramBs methodTys +-- className' <- emitBinding (getNameHint sn) $ ClassBinding classDef +-- methodNames' <- forM (enumerate methodSourceNames) \(i, prettyName) -> do +-- emitBinding (getNameHint prettyName) $ MethodBinding className' i +-- let subst = className @> className' <.> methodNames @@> methodNames' +-- UDeclResultDone <$> applyRename subst result +-- inferTopUDecl (UInstance className bs params methods maybeName expl) result = do +-- let (InternalName _ _ className') = className +-- def <- liftInfererM $ withUBinders bs \(ZipB roleExpls bs') -> do +-- ClassDef _ _ _ _ _ paramBinders _ _ <- lookupClassDef (sink className') +-- params' <- checkInstanceParams paramBinders params +-- body <- checkInstanceBody (sink className') params' methods +-- return $ InstanceDef className' roleExpls bs' params' body +-- UDeclResultDone <$> case maybeName of +-- RightB UnitB -> do +-- instanceName <- emitInstanceDef def +-- ClassDef _ builtinName _ _ _ _ _ _ <- lookupClassDef className' +-- addInstanceSynthCandidate className' builtinName instanceName +-- return result +-- JustB instanceName' -> do +-- instanceName <- emitInstanceDef def +-- lam <- instanceFun instanceName expl +-- instanceAtomName <- emitTopLet (getNameHint instanceName') PlainLet $ Atom lam +-- applyRename (instanceName' @> atomVarName instanceAtomName) result +-- _ -> error "impossible" +-- inferTopUDecl (ULocalDecl (WithSrcB _ decl)) result = case decl of +-- UPass -> return $ UDeclResultDone result +-- UExprDecl _ -> error "Shouldn't have this at the top level (should have become a command instead)" +-- ULet letAnn p tyAnn rhs -> case p of +-- WithSrcB _ (UPatBinder b) -> do +-- block <- liftInfererM $ buildBlock do +-- checkMaybeAnnExpr tyAnn rhs +-- (topBlock, resultTy) <- asTopBlock block +-- let letAnn' = considerInlineAnn letAnn resultTy +-- return $ UDeclResultBindName letAnn' topBlock (Abs b result) +-- _ -> do +-- PairE block recon <- liftInfererM $ buildBlockInfWithRecon do +-- val <- checkMaybeAnnExpr tyAnn rhs +-- v <- emitDecl (getNameHint p) PlainLet $ Atom val +-- bindLetPat p v do +-- renameM result +-- (topBlock, _) <- asTopBlock block +-- return $ UDeclResultBindPattern (getNameHint p) topBlock recon +-- {-# SCC inferTopUDecl #-} + +-- asTopBlock :: EnvReader m => CExpr n -> m n (TopBlock n, CType n) +-- asTopBlock block = do +-- let ty = getType block +-- return (TopLam False (PiType Empty ty) (LamExpr Empty block), ty) + +-- getInstanceType :: EnvReader m => InstanceDef n -> m n (CorePiType n) +-- getInstanceType (InstanceDef className expls bs params _) = liftEnvReaderM do +-- refreshAbs (Abs bs (ListE params)) \bs' (ListE params') -> do +-- className' <- sinkM className +-- dTy <- toType <$> dictType className' params' +-- return $ CorePiType ImplicitApp expls bs' dTy + +-- -- === Inferer monad === + +-- newtype SolverSubst n = SolverSubst { fromSolverSubst :: M.Map (CAtomName n) (CAtom n) } + +-- emptySolverSubst :: SolverSubst n +-- emptySolverSubst = SolverSubst mempty + +data InfState (n::S) = InfState + { givens :: Givens n } + +newtype InfererM (i::S) (o::S) (a:: *) = InfererM + { runInfererM' :: SubstReaderT Name (ReaderT1 InfState (ScopeReaderT (ExceptT (State TypingInfo)))) i o a } + deriving (Functor, Applicative, Monad, MonadFail, Fallible, SubstReader Name) + +-- type InfererCPSB b i o a = (forall o'. DExt o o' => b o o' -> InfererM i o' a) -> InfererM i o a +-- type InfererCPSB2 b i i' o a = (forall o'. DExt o o' => b o o' -> InfererM i' o' a) -> InfererM i o a + +liftInfererM :: (TopLogger m, Fallible m) => InfererM VoidS VoidS a -> m a +liftInfererM cont = do + let (ansExcept, typeInfo) = liftInfererMPure cont + emitLog $ Outputs [SourceInfo $ SITypingInfo typeInfo] + liftExcept ansExcept +{-# INLINE liftInfererM #-} + +liftInfererMPure :: InfererM VoidS VoidS a -> (Except a, TypingInfo) +liftInfererMPure cont = do + let ansM = runScopeReaderT emptyOutMap $ runReaderT1 emptyInfState $ runSubstReaderT idSubst $ runInfererM' cont + runState (runExceptT ansM) mempty + where + emptyInfState :: InfState n + emptyInfState = InfState (Givens HM.empty) +{-# INLINE liftInfererMPure #-} + +-- -- === Solver monad === + +-- type Solution = PairE CAtomName CAtom +-- newtype SolverDiff (n::S) = SolverDiff (RListE Solution n) +-- deriving (MonoidE, SinkableE, HoistableE, RenameE) +-- type SolverM i o a = DiffStateT1 SolverSubst SolverDiff (InfererM i) o a + +-- type Zonkable e = (HasNamesE e, SubstE AtomSubstVal e) + +-- liftSolverM :: SolverM i o a -> InfererM i o a +-- liftSolverM cont = fst <$> runDiffStateT1 emptySolverSubst cont + +-- solverFail :: SolverM i o a +-- solverFail = empty + +-- zonk :: Zonkable e => e n -> SolverM i n (e n) +-- zonk e = do +-- s <- getDiffState +-- applySolverSubst s e +-- {-# INLINE zonk #-} + +-- zonkStuck :: CStuck n -> SolverM i n (CAtom n) +-- zonkStuck stuck = do +-- solverSubst <- getDiffState +-- Distinct <- getDistinct +-- env <- unsafeGetEnv +-- let subst = newSubst (lookupSolverSubst solverSubst) +-- return $ substStuck (env, subst) stuck + +-- applySolverSubst :: (EnvReader m, Zonkable e) => SolverSubst n -> e n -> m n (e n) +-- applySolverSubst subst e = do +-- Distinct <- getDistinct +-- env <- unsafeGetEnv +-- return $ fmapNames env (lookupSolverSubst subst) e +-- {-# INLINE applySolverSubst #-} + +-- withFreshBinderInf :: NameHint -> Explicitness -> CType o -> InfererCPSB CBinder i o a +-- withFreshBinderInf hint expl ty cont = +-- withFreshBinder hint ty \b -> do +-- givens <- case expl of +-- Inferred _ (Synth _) -> return [toAtom $ binderVar b] +-- _ -> return [] +-- extendGivens givens $ cont b +-- {-# INLINE withFreshBinderInf #-} + +-- withFreshBindersInf +-- :: (SinkableE e, RenameE e) +-- => [Explicitness] -> Abs (Nest CBinder) e o +-- -> (forall o'. DExt o o' => Nest CBinder o o' -> e o' -> InfererM i o' a) +-- -> InfererM i o a +-- withFreshBindersInf explsTop (Abs bsTop e) contTop = +-- runSubstReaderT idSubst $ go explsTop bsTop \bs' -> do +-- e' <- renameM e +-- liftSubstReaderT $ contTop bs' e' +-- where +-- go :: [Explicitness] -> Nest CBinder ii ii' +-- -> (forall o'. DExt o o' => Nest CBinder o o' -> SubstReaderT Name (InfererM i) ii' o' a) +-- -> SubstReaderT Name (InfererM i) ii o a +-- go [] Empty cont = withDistinct $ cont Empty +-- go (expl:expls) (Nest b bs) cont = do +-- ty <- renameM $ binderType b +-- SubstReaderT \s -> withFreshBinderInf (getNameHint b) expl ty \b' -> do +-- runSubstReaderT (sink s) $ extendSubst (b@>binderName b') do +-- go expls bs \bs' -> cont (Nest b' bs') +-- go _ _ _ = error "zip error" +-- {-# INLINE withFreshBindersInf #-} + +-- withInferenceVar +-- :: (Zonkable e, Emits o, ToBinding binding) => NameHint -> binding o +-- -> (forall o'. (Emits o', DExt o o') => CAtomName o' -> SolverM i o' (e o', CAtom o')) +-- -> SolverM i o (e o) +-- withInferenceVar hint binding cont = diffStateT1 \s -> do +-- declsAndAns <- withFreshBinder hint binding \(b:>_) -> do +-- hardHoist b <$> buildScoped do +-- v <- sinkM $ binderName b +-- s' <- sinkM s +-- (PairE ans soln, diff) <- runDiffStateT1 s' do +-- toPairE <$> cont v +-- let subst = SolverSubst $ M.singleton v soln +-- ans' <- applySolverSubst subst ans +-- diff' <- applySolutionToDiff subst v diff +-- return $ PairE ans' diff' +-- fromPairE <$> emitDecls declsAndAns +-- where +-- applySolutionToDiff :: SolverSubst n -> CAtomName n -> SolverDiff n -> InfererM i n (SolverDiff n) +-- applySolutionToDiff subst vSoln (SolverDiff (RListE (ReversedList cs))) = do +-- SolverDiff . RListE . ReversedList <$> forMFilter cs \(PairE v x) -> +-- case v == vSoln of +-- True -> return Nothing +-- False -> Just . PairE v <$> applySolverSubst subst x +-- {-# INLINE withInferenceVar #-} + +-- withFreshUnificationVar +-- :: (Zonkable e, Emits o) => SrcId -> InfVarDesc -> CType o +-- -> (forall o'. (Emits o', DExt o o') => CAtomVar o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- withFreshUnificationVar sid desc k cont = do +-- withInferenceVar "_unif_" (InfVarBound k) \v -> do +-- ans <- toAtomVar v >>= cont +-- soln <- (M.lookup v <$> fromSolverSubst <$> getDiffState) >>= \case +-- Just soln -> return soln +-- Nothing -> throw sid $ AmbiguousInferenceVar (pprint v) (pprint k) desc +-- return (ans, soln) +-- {-# INLINE withFreshUnificationVar #-} + +-- withFreshUnificationVarNoEmits +-- :: (Zonkable e) => SrcId -> InfVarDesc -> CType o +-- -> (forall o'. (DExt o o') => CAtomVar o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- withFreshUnificationVarNoEmits sid desc k cont = diffStateT1 \s -> do +-- Abs Empty resultAndDiff <- buildScoped do +-- liftM toPairE $ runDiffStateT1 (sink s) $ +-- withFreshUnificationVar sid desc (sink k) cont +-- return $ fromPairE resultAndDiff + +-- withFreshDictVar +-- :: (Zonkable e, Emits o) => CType o +-- -- This tells us how to synthesize the dict. The supplied CType won't contain inference vars. +-- -> (forall o'. ( DExt o o') => CType o' -> SolverM i o' (CAtom o')) +-- -> (forall o'. (Emits o', DExt o o') => CAtom o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- withFreshDictVar dictTy synthIt cont = hasInferenceVars dictTy >>= \case +-- False -> withDistinct $ synthIt dictTy >>= cont +-- True -> withInferenceVar "_dict_" (DictBound dictTy) \v -> do +-- ans <- cont =<< (toAtom <$> toAtomVar v) +-- dictTy' <- zonk $ sink dictTy +-- dict <- synthIt dictTy' +-- return (ans, dict) +-- {-# INLINE withFreshDictVar #-} + +-- withFreshDictVarNoEmits +-- :: (Zonkable e) => CType o +-- -- This tells us how to synthesize the dict. The supplied CType won't contain inference vars. +-- -> (forall o'. (DExt o o') => CType o' -> SolverM i o' (CAtom o')) +-- -> (forall o'. (DExt o o') => CAtom o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- withFreshDictVarNoEmits dictTy synthIt cont = diffStateT1 \s -> do +-- Abs Empty resultAndDiff <- buildScoped do +-- liftM toPairE $ runDiffStateT1 (sink s) $ +-- withFreshDictVar (sink dictTy) synthIt cont +-- return $ fromPairE resultAndDiff +-- {-# INLINE withFreshDictVarNoEmits #-} + +-- withDict +-- :: (Zonkable e, Emits o) => SrcId -> CType o +-- -> (forall o'. (Emits o', DExt o o') => CAtom o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- withDict sid dictTy cont = withFreshDictVar dictTy +-- (\dictTy' -> lift11 $ trySynthTerm sid dictTy' Full) +-- cont +-- {-# INLINE withDict#-} + +-- addConstraint :: CAtomName o -> CAtom o -> SolverM i o () +-- addConstraint v ty = updateDiffStateM (SolverDiff $ RListE $ toSnocList [PairE v ty]) +-- {-# INLINE addConstraint #-} + +-- getInfState :: InfererM i o (InfState o) +-- getInfState = InfererM $ liftSubstReaderT ask +-- {-# INLINE getInfState #-} + +-- withInfState :: (InfState o -> InfState o) -> InfererM i o a -> InfererM i o a +-- withInfState f cont = InfererM $ local f (runInfererM' cont) +-- {-# INLINE withInfState #-} + +-- getTypeAndEmit :: HasType e => SrcId -> e o -> InfererM i o (e o) +-- getTypeAndEmit sid e = do +-- emitExprType sid (getType e) +-- return e + +emitExprType :: SrcId -> CType any -> InfererM i o () +emitExprType sid ty = emitTypeInfo sid $ ExprType $ pprint ty + +emitTypeInfo :: SrcId -> TypeInfo -> InfererM i o () +emitTypeInfo sid tyInfo = + InfererM $ liftSubstReaderT $ lift11 $ lift1 $ lift $ + modify (<> TypingInfo (M.singleton sid tyInfo)) + +-- === actual inference pass === + +type CAtom = CExpr + +data RequiredTy (n::S) = + Check (CType n) + | Infer + deriving Show + +data PartialPiType (n::S) where + PartialPiType + :: AppExplicitness -> [Explicitness] + -> Nest CBinder n l + -> RequiredTy l + -> PartialPiType n + +data PartialType (n::S) = + PartialType (PartialPiType n) + | FullType (CType n) + +checkOrInfer :: RequiredTy o -> UExpr i -> InfererM i o (CAtom o) +checkOrInfer reqTy expr = case reqTy of + Infer -> bottomUp expr + Check t -> topDown t expr + +topDown :: CType o -> UExpr i -> InfererM i o (CExpr o) +topDown ty uexpr = undefined -- topDownPartial (typeAsPartialType ty) uexpr + +topDownPartial :: PartialType o -> UExpr i -> InfererM i o (CAtom o) +topDownPartial partialTy exprWithSrc@(WithSrcE sid expr) = undefined +-- topDownPartial partialTy exprWithSrc@(WithSrcE sid expr) = +-- case partialTy of +-- PartialType partialPiTy -> case expr of +-- ULam lam -> toAtom <$> Lam <$> checkULamPartial partialPiTy sid lam +-- _ -> toAtom <$> Lam <$> etaExpandPartialPi partialPiTy \resultTy explicitArgs -> do +-- expr' <- bottomUpExplicit exprWithSrc +-- dropSubst $ checkOrInferApp sid sid expr' explicitArgs [] resultTy +-- FullType ty -> topDownExplicit ty exprWithSrc + +-- Creates a lambda for all args and returns (via CPA) the explicit args +etaExpandPartialPi + :: PartialPiType o + -> (forall o'. (DExt o o') => RequiredTy o' -> [CAtom o'] -> InfererM i o' (CAtom o')) + -> InfererM i o (CoreLamExpr o) +etaExpandPartialPi (PartialPiType appExpl expls bs reqTy) cont = undefined +-- etaExpandPartialPi (PartialPiType appExpl expls bs reqTy) cont = do +-- withFreshBindersInf expls (Abs bs reqTy) \bs' reqTy' -> do +-- let args = zip expls (toAtom <$> bindersVars bs') +-- explicits <- return $ catMaybes $ args <&> \case +-- (Explicit, arg) -> Just arg +-- _ -> Nothing +-- body <- buildBlock $ cont (sink reqTy') (sink <$> explicits) +-- let piTy = CorePiType appExpl expls bs' (getType body) +-- return $ CoreLamExpr piTy $ Abs bs' body + +-- Expects the uexpr to be a type-like thing, including ordinary data types, pi +-- types, dict types etc. +topDownType :: UExpr i -> InfererM i o (CType o) +topDownType exprWithSrc@(WithSrcE sid expr) = undefined +-- topDownType exprWithSrc@(WithSrcE sid expr) = case expr of +-- UPrim UTuple xs -> toType . ProdType <$> mapM checkUType xs +-- _ -> do +-- ty <- bottomUpExplicit exprWithSrc +-- ty' <- maybeInterpretPunsAsTyCons (Check (toType $ Kind TypeKind)) ty +-- ty'' <- instantiateSigma sid Infer ty' +-- case toMaybeType ty'' of +-- Nothing -> throw sid $ ExpectedAType (pprint ty'') +-- Just ty''' -> return ty''' + +-- Doesn't introduce implicit pi binders or dependent pairs +topDownExplicit :: forall i o. CType o -> UExpr i -> InfererM i o (CAtom o) +topDownExplicit = undefined +-- topDownExplicit reqTy exprWithSrc@(WithSrcE sid expr) = emitExprType sid reqTy >> case expr of +-- ULam lamExpr -> case reqTy of +-- TyCon (Pi piTy) -> toAtom <$> Lam <$> checkULam sid lamExpr piTy +-- _ -> throw sid $ UnexpectedTerm "lambda" (pprint reqTy) +-- UFor dir uFor@(UForExpr b _) -> case reqTy of +-- TyCon (TabPi tabPiTy) -> do +-- lam@(UnaryLamExpr b' _) <- checkUForExpr sid uFor tabPiTy +-- ixTy <- asIxType (getSrcId b) $ binderType b' +-- emitHof $ For dir ixTy lam +-- _ -> throw sid $ UnexpectedTerm "`for` expression" (pprint reqTy) +-- UApp f posArgs namedArgs -> do +-- f' <- bottomUpExplicit f +-- checkOrInferApp sid (getSrcId f) f' posArgs namedArgs (Check reqTy) +-- UDepPair lhs rhs -> case reqTy of +-- TyCon (DepPairTy ty@(DepPairType _ (_ :> lhsTy) _)) -> do +-- lhs' <- checkSigmaDependent lhs (FullType lhsTy) +-- rhsTy <- instantiate ty [lhs'] +-- rhs' <- topDown rhsTy rhs +-- return $ toAtom $ DepPair lhs' rhs' ty +-- _ -> throw sid $ UnexpectedTerm "dependent pair" (pprint reqTy) +-- UCase scrut alts -> do +-- scrut' <- bottomUp scrut +-- let scrutTy = getType scrut' +-- alts' <- mapM (checkCaseAlt (Check reqTy) scrutTy) alts +-- buildSortedCase scrut' alts' reqTy +-- UDo block -> withBlockDecls block \result -> topDownExplicit (sink reqTy) result +-- UTabCon xs -> do +-- case reqTy of +-- TyCon (TabPi tabPiTy) -> checkTabCon tabPiTy sid xs +-- _ -> throw sid $ UnexpectedTerm "table constructor" (pprint reqTy) +-- UNatLit x -> fromNatLit sid x reqTy +-- UIntLit x -> fromIntLit sid x reqTy +-- UPrim UTuple xs -> case reqTy of +-- TyCon (Kind TypeKind) -> toAtom . ProdType <$> mapM checkUType xs +-- TyCon (ProdType reqTys) -> do +-- when (length reqTys /= length xs) $ throw sid $ TupleLengthMismatch (length reqTys) (length xs) +-- toAtom <$> ProdCon <$> forM (zip reqTys xs) \(reqTy', x) -> topDown reqTy' x +-- _ -> throw sid $ UnexpectedTerm "tuple" (pprint reqTy) +-- UFieldAccess _ _ -> infer +-- UVar _ -> infer +-- UTypeAnn _ _ -> infer +-- UTabApp _ _ -> infer +-- UFloatLit _ -> infer +-- UPrim _ _ -> infer +-- ULit _ -> infer +-- UPi _ -> infer +-- UTabPi _ -> infer +-- UDepPairTy _ -> infer +-- UHole -> throw sid InferHoleErr +-- where +-- infer :: InfererM i o (CAtom o) +-- infer = do +-- sigmaAtom <- maybeInterpretPunsAsTyCons (Check reqTy) =<< bottomUpExplicit exprWithSrc +-- instantiateSigma sid (Check reqTy) sigmaAtom + +bottomUp :: UExpr i -> InfererM i o (CExpr o) +bottomUp expr = bottomUpExplicit expr >>= instantiateSigma (getSrcId expr) Infer + +-- Doesn't instantiate implicit args +bottomUpExplicit :: UExpr i -> InfererM i o (SigmaAtom o) +bottomUpExplicit (WithSrcE sid expr) = undefined -- getTypeAndEmit sid =<< case expr of + -- UVar ~(InternalName _ sn v) -> do + -- v' <- renameM v + -- ty <- getUVarType v' + -- return $ SigmaUVar sn ty v' + -- ULit l -> return $ SigmaAtom Nothing $ Con $ Lit l +-- UFieldAccess x (WithSrc _ field) -> do +-- x' <- bottomUp x +-- ty <- return $ getType x' +-- fields <- getFieldDefs sid ty +-- case M.lookup field fields of +-- Just def -> case def of +-- FieldProj i -> SigmaAtom Nothing <$> projectField i x' +-- FieldDotMethod method (TyConParams _ params) -> do +-- method' <- toAtomVar method +-- resultTy <- partialAppType (getType method') (params ++ [x']) +-- return $ SigmaPartialApp resultTy (toAtom method') (params ++ [x']) +-- Nothing -> throw sid $ CantFindField (pprint field) (pprint ty) (map pprint $ M.keys fields) +-- ULam lamExpr -> SigmaAtom Nothing <$> toAtom <$> inferULam lamExpr +-- UFor dir uFor@(UForExpr b _) -> do +-- lam@(UnaryLamExpr b' _) <- inferUForExpr uFor +-- ixTy <- asIxType (getSrcId b) $ binderType b' +-- liftM (SigmaAtom Nothing) $ emitHof $ For dir ixTy lam +-- UApp f posArgs namedArgs -> do +-- f' <- bottomUpExplicit f +-- SigmaAtom Nothing <$> checkOrInferApp sid (getSrcId f) f' posArgs namedArgs Infer +-- UTabApp tab args -> do +-- tab' <- bottomUp tab +-- SigmaAtom Nothing <$> inferTabApp (getSrcId tab) tab' args +-- UPi (UPiExpr bs appExpl ty) -> do +-- -- TODO: check explicitness constraints +-- withUBinders bs \(ZipB expls bs') -> do +-- ty' <- checkUType ty +-- return $ SigmaAtom Nothing $ toAtom $ +-- Pi $ CorePiType appExpl expls bs' ty' +-- UTabPi (UTabPiExpr b ty) -> do +-- Abs b' ty' <- withUBinder b \(WithAttrB _ b') -> +-- liftM (Abs b') $ checkUType ty +-- d <- getIxDict (getSrcId b) $ binderType b' +-- let piTy = TabPiType d b' ty' +-- return $ SigmaAtom Nothing $ toAtom $ TabPi piTy +-- UDepPairTy (UDepPairType expl b rhs) -> do +-- withUBinder b \(WithAttrB _ b') -> do +-- rhs' <- checkUType rhs +-- return $ SigmaAtom Nothing $ toAtom $ DepPairTy $ DepPairType expl b' rhs' +-- UDepPair _ _ -> throw sid InferDepPairErr +-- UCase scrut (alt:alts) -> do +-- scrut' <- bottomUp scrut +-- let scrutTy = getType scrut' +-- alt'@(IndexedAlt _ altAbs) <- checkCaseAlt Infer scrutTy alt +-- Abs b ty <- liftEnvReaderM $ refreshAbs altAbs \b body -> do +-- return $ Abs b (getType body) +-- resultTy <- liftHoistExcept sid $ hoist b ty +-- alts' <- mapM (checkCaseAlt (Check resultTy) scrutTy) alts +-- SigmaAtom Nothing <$> buildSortedCase scrut' (alt':alts') resultTy +-- UCase _ [] -> throw sid InferEmptyCaseEff +-- UDo block -> withBlockDecls block \result -> bottomUpExplicit result +-- UTabCon xs -> liftM (SigmaAtom Nothing) $ inferTabCon sid xs +-- UTypeAnn val ty -> do +-- ty' <- checkUType ty +-- liftM (SigmaAtom Nothing) $ topDown ty' val +-- UPrim UTuple xs -> do +-- xs' <- forM xs \x -> bottomUp x +-- return $ SigmaAtom Nothing $ Con $ ProdCon xs' +-- UPrim UMonoLiteral [WithSrcE _ l] -> case l of +-- UIntLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Int32Lit $ fromIntegral x +-- UNatLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Word32Lit $ fromIntegral x +-- _ -> throwInternal "argument to %monoLit must be a literal" +-- UPrim UExplicitApply (f:xs) -> do +-- f' <- bottomUpExplicit f +-- xs' <- mapM bottomUp xs +-- SigmaAtom Nothing <$> applySigmaAtom f' xs' +-- UPrim UProjNewtype [x] -> do +-- x' <- bottomUp x >>= unwrapNewtype +-- return $ SigmaAtom Nothing x' +-- UPrim prim xs -> do +-- xs' <- forM xs \x -> do +-- inferPrimArg x >>= \case +-- Stuck _ (Var v) -> lookupAtomName (atomVarName v) >>= \case +-- LetBound (DeclBinding _ (Atom e)) -> return e +-- _ -> return $ toAtom v +-- x' -> return x' +-- liftM (SigmaAtom Nothing) $ matchPrimApp prim xs' +-- UNatLit l -> liftM (SigmaAtom Nothing) $ fromNatLit sid l NatTy +-- UIntLit l -> liftM (SigmaAtom Nothing) $ fromIntLit sid l (BaseTy $ Scalar Int32Type) +-- UFloatLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Float32Lit $ realToFrac x +-- UHole -> throw sid InferHoleErr + +-- expectEq :: (PrettyE e, AlphaEqE e) => SrcId -> e o -> e o -> InfererM i o () +-- expectEq sid reqTy actualTy = alphaEq reqTy actualTy >>= \case +-- True -> return () +-- False -> throw sid $ TypeMismatch (pprint reqTy) (pprint actualTy) +-- {-# INLINE expectEq #-} + +-- fromIntLit :: Emits o => SrcId -> Int -> CType o -> InfererM i o (CAtom o) +-- fromIntLit sid x ty = do +-- let litVal = Con $ Lit $ Int64Lit $ fromIntegral x +-- applyFromLiteralMethod sid ty "from_integer" litVal + +-- fromNatLit :: Emits o => SrcId -> Word64 -> CType o -> InfererM i o (CAtom o) +-- fromNatLit sid x ty = do +-- let litVal = Con $ Lit $ Word64Lit $ fromIntegral x +-- applyFromLiteralMethod sid ty "from_unsigned_integer" litVal + +instantiateSigma :: SrcId -> RequiredTy o -> SigmaAtom o -> InfererM i o (CAtom o) +instantiateSigma sid reqTy sigmaAtom = undefined +-- instantiateSigma sid reqTy sigmaAtom = case sigmaAtom of +-- SigmaUVar _ _ _ -> case getType sigmaAtom of +-- TyCon (Pi (CorePiType ImplicitApp expls bs resultTy)) -> do +-- bsConstrained <- buildConstraints (Abs bs resultTy) \_ resultTy' -> do +-- case reqTy of +-- Infer -> return [] +-- Check reqTy' -> return [TypeConstraint sid (sink reqTy') resultTy'] +-- args <- inferMixedArgs @UExpr sid fDesc expls bsConstrained ([], []) +-- applySigmaAtom sigmaAtom args +-- _ -> fallback +-- _ -> fallback +-- where +-- fallback = forceSigmaAtom sigmaAtom >>= matchReq sid reqTy +-- fDesc = getSourceName sigmaAtom + +-- matchReq :: Ext o o' => SrcId -> RequiredTy o -> CAtom o' -> InfererM i o' (CAtom o') +-- matchReq sid (Check reqTy) x = do +-- reqTy' <- sinkM reqTy +-- return x <* expectEq sid reqTy' (getType x) +-- matchReq _ Infer x = return x +-- {-# INLINE matchReq #-} + +-- forceSigmaAtom :: Emits o => SigmaAtom o -> InfererM i o (CAtom o) +-- forceSigmaAtom sigmaAtom = case sigmaAtom of +-- SigmaAtom _ x -> return x +-- SigmaUVar _ _ v -> undefined +-- -- SigmaUVar _ _ v -> case v of +-- -- UAtomVar v' -> inlineTypeAliases v' +-- -- _ -> applySigmaAtom sigmaAtom [] +-- SigmaPartialApp _ _ _ -> error "not implemented" -- better error message? + +-- withBlockDecls +-- :: (Emits o, Zonkable e) +-- => UBlock i +-- -> (forall i' o'. (Emits o', DExt o o') => UExpr i' -> InfererM i' o' (e o')) +-- -> InfererM i o (e o) +-- withBlockDecls (WithSrcE _ (UBlock declsTop result)) contTop = +-- go declsTop $ contTop result where +-- go :: (Emits o, Zonkable e) +-- => Nest UDecl i i' +-- -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) +-- -> InfererM i o (e o) +-- go decls cont = case decls of +-- Empty -> withDistinct cont +-- Nest d ds -> withUDecl d $ go ds $ cont + +-- withUDecl +-- :: (Emits o, Zonkable e) +-- => UDecl i i' +-- -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) +-- -> InfererM i o (e o) +-- withUDecl (WithSrcB _ d) cont = case d of +-- UPass -> withDistinct cont +-- UExprDecl e -> withDistinct $ bottomUp e >> cont +-- ULet letAnn p ann rhs -> do +-- val <- checkMaybeAnnExpr ann rhs +-- let letAnn' = considerInlineAnn letAnn (getType val) +-- var <- emitDecl (getNameHint p) letAnn' $ Atom val +-- bindLetPat p var cont + +-- considerInlineAnn :: LetAnn -> CType n -> LetAnn +-- considerInlineAnn PlainLet (TyCon (Kind _)) = InlineLet +-- considerInlineAnn PlainLet (TyCon (Pi (CorePiType _ _ _ (TyCon (Kind _))))) = InlineLet +-- considerInlineAnn ann _ = ann + +-- applyFromLiteralMethod +-- :: Emits n => SrcId -> CType n -> SourceName -> CAtom n -> InfererM i n (CAtom n) +-- applyFromLiteralMethod sid resultTy methodName litVal = +-- lookupSourceMap methodName >>= \case +-- Nothing -> error $ "prelude function not found: " ++ pprint methodName +-- Just methodName' -> do +-- MethodBinding className _ <- lookupEnv methodName' +-- dictTy <- toType <$> dictType className [toAtom resultTy] +-- Just d <- toMaybeDict <$> trySynthTerm sid dictTy Full +-- emit =<< mkApplyMethod d 0 [litVal] + +-- atom that requires instantiation to become a rho type +data SigmaAtom n = + SigmaAtom (Maybe SourceName) (CExpr n) + | SigmaUVar SourceName (CType n) (UVar n) + | SigmaPartialApp (CType n) (CExpr n) [CExpr n] + deriving (Show) + +-- -- XXX: this gives the type of the atom in the absence of other type information. +-- -- So it interprets struct names as data constructors rather than type constructors. +-- instance HasType SigmaAtom where +-- getType = \case +-- SigmaAtom _ x -> getType x +-- SigmaUVar _ ty _ -> ty +-- SigmaPartialApp ty _ _ -> ty + +-- instance HasSourceName (SigmaAtom n) where +-- getSourceName = \case +-- SigmaAtom sn _ -> case sn of +-- Just sn' -> sn' +-- Nothing -> "" +-- SigmaUVar sn _ _ -> sn +-- SigmaPartialApp _ _ _ -> "" + +-- data FieldDef (n::S) = +-- FieldProj Int +-- | FieldDotMethod (CAtomName n) (TyConParams n) +-- deriving (Show, Generic) + +-- getFieldDefs :: SrcId -> CType n -> InfererM i n (M.Map FieldName' (FieldDef n)) +-- getFieldDefs sid ty = case ty of +-- StuckTy _ _ -> noFields +-- TyCon con -> case con of +-- NewtypeTyCon (UserADTType _ tyName params) -> do +-- TyConBinding ~(Just tyDef) (DotMethods dotMethods) <- lookupEnv tyName +-- instantiateTyConDef tyDef params >>= \case +-- StructFields fields -> do +-- let projFields = enumerate fields <&> \(i, (field, _)) -> +-- [(FieldName field, FieldProj i), (FieldNum i, FieldProj i)] +-- let methodFields = M.toList dotMethods <&> \(field, f) -> +-- (FieldName field, FieldDotMethod f params) +-- return $ M.fromList $ concat projFields ++ methodFields +-- ADTCons _ -> noFields +-- RefType valTy -> case valTy of +-- RefTy _ -> noFields +-- _ -> do +-- valFields <- getFieldDefs sid valTy +-- return $ M.filter isProj valFields +-- where isProj = \case +-- FieldProj _ -> True +-- _ -> False +-- ProdType ts -> return $ M.fromList $ enumerate ts <&> \(i, _) -> (FieldNum i, FieldProj i) +-- TabPi _ -> noFields +-- _ -> noFields +-- where noFields = throw sid $ NoFields $ pprint ty + +-- projectField :: Emits o => Int -> CAtom o -> InfererM i o (CAtom o) +-- projectField i x = case getType x of +-- StuckTy _ _ -> bad +-- TyCon con -> case con of +-- ProdType _ -> proj i x +-- NewtypeTyCon _ -> projectStruct i x +-- RefType valTy -> case valTy of +-- TyCon (ProdType _) -> getProjRef (ProjectProduct i) x +-- TyCon (NewtypeTyCon _) -> projectStructRef i x +-- _ -> bad +-- _ -> bad +-- where bad = error $ "bad projection: " ++ pprint (i, x) + +class PrettyE e => ExplicitArg (e::E) where + checkExplicitNonDependentArg :: e i -> PartialType o -> InfererM i o (CAtom o) + checkExplicitDependentArg :: e i -> PartialType o -> InfererM i o (CAtom o) + inferExplicitArg :: e i -> InfererM i o (CAtom o) + isHole :: e n -> Bool + explicitArgSrcId :: e n -> SrcId + +-- instance ExplicitArg UExpr where +-- checkExplicitDependentArg arg argTy = checkSigmaDependent arg argTy +-- checkExplicitNonDependentArg arg argTy = topDownPartial argTy arg +-- inferExplicitArg arg = bottomUp arg +-- isHole = \case +-- WithSrcE _ UHole -> True +-- _ -> False +-- explicitArgSrcId = getSrcId + +-- instance ExplicitArg CAtom where +-- checkExplicitDependentArg = checkCAtom +-- checkExplicitNonDependentArg = checkCAtom +-- inferExplicitArg arg = renameM arg +-- isHole _ = False +-- explicitArgSrcId _ = rootSrcId + +-- checkCAtom :: CAtom i -> PartialType o -> InfererM i o (CAtom o) +-- checkCAtom arg argTy = do +-- arg' <- renameM arg +-- case argTy of +-- FullType argTy' -> expectEq rootSrcId argTy' (getType arg') +-- PartialType _ -> return () -- TODO? +-- return arg' + +checkOrInferApp + :: forall i o arg . (ExplicitArg arg) + => SrcId -> SrcId -> SigmaAtom o -> [arg i] -> [(SourceName, arg i)] + -> RequiredTy o -> InfererM i o (CAtom o) +checkOrInferApp appSrcId funSrcId f' posArgs namedArgs reqTy = undefined +-- checkOrInferApp appSrcId funSrcId f' posArgs namedArgs reqTy = do +-- f <- maybeInterpretPunsAsTyCons reqTy f' +-- case getType f of +-- TyCon (Pi piTy@(CorePiType appExpl expls _ _)) -> case appExpl of +-- ExplicitApp -> do +-- checkExplicitArity appSrcId expls posArgs +-- bsConstrained <- buildAppConstraints appSrcId reqTy piTy +-- args <- inferMixedArgs appSrcId fDesc expls bsConstrained (posArgs, namedArgs) +-- applySigmaAtom f args +-- ImplicitApp -> error "should already have handled this case" +-- ty -> throw funSrcId $ EliminationErr "function type" (pprint ty) +-- where +-- fDesc :: SourceName +-- fDesc = getSourceName f' + +-- buildAppConstraints :: SrcId -> RequiredTy n -> CorePiType n -> InfererM i n (ConstrainedBinders n) +-- buildAppConstraints appSrcId reqTy (CorePiType _ _ bs ty) = do +-- buildConstraints (Abs bs ty) \_ resultTy -> do +-- return case reqTy of +-- Infer -> [] +-- Check reqTy' -> [TypeConstraint appSrcId (sink reqTy') resultTy] + +-- maybeInterpretPunsAsTyCons :: RequiredTy n -> SigmaAtom n -> InfererM i n (SigmaAtom n) +-- maybeInterpretPunsAsTyCons = undefined +-- -- maybeInterpretPunsAsTyCons (Check (TyCon (Kind TypeKind))) (SigmaUVar sn _ (UPunVar v)) = do +-- -- let v' = UTyConVar v +-- -- ty <- getUVarType v' +-- -- return $ SigmaUVar sn ty v' +-- -- maybeInterpretPunsAsTyCons _ x = return x + +-- type IsDependent = Bool + +-- inlineTypeAliases :: CAtomName n -> InfererM i n (CAtom n) +-- inlineTypeAliases v = do +-- lookupAtomName v >>= \case +-- LetBound (DeclBinding InlineLet (Atom e)) -> return e +-- _ -> toAtom <$> toAtomVar v + +-- applySigmaAtom :: Emits o => SigmaAtom o -> [CAtom o] -> InfererM i o (CAtom o) +-- applySigmaAtom (SigmaAtom _ f) args = emit =<< mkApp f args +-- -- applySigmaAtom (SigmaUVar _ _ f) args = case f of +-- -- UAtomVar f' -> do +-- -- f'' <- inlineTypeAliases f' +-- -- emit =<< mkApp f'' args +-- -- UTyConVar f' -> do +-- -- TyConDef sn expls _ _ <- lookupTyCon f' +-- -- return $ toAtom $ UserADTType sn f' (TyConParams expls args) +-- -- UDataConVar v -> do +-- -- (tyCon, i) <- lookupDataCon v +-- -- applyDataCon tyCon i args +-- -- UPunVar tc -> do +-- -- TyConDef sn _ _ _ <- lookupTyCon tc +-- -- -- interpret as a data constructor by default +-- -- (params, dataArgs) <- splitParamPrefix tc args +-- -- repVal <- makeStructRepVal tc dataArgs +-- -- return $ toAtom $ NewtypeCon (UserADTData sn tc params) repVal +-- -- UClassVar f' -> do +-- -- ClassDef sourceName builtinName _ _ _ _ _ _ <- lookupClassDef f' +-- -- return $ toAtom case builtinName of +-- -- Just Ix -> IxDictType singleTyParam +-- -- Nothing -> DictType sourceName f' args +-- -- where singleTyParam = case args of +-- -- [p] -> fromJust $ toMaybeType p +-- -- _ -> error "not a single type param" +-- -- UMethodVar f' -> do +-- -- MethodBinding className methodIdx <- lookupEnv f' +-- -- ClassDef _ _ _ _ _ paramBs _ _ <- lookupClassDef className +-- -- let numParams = nestLength paramBs +-- -- -- params aren't needed because they're already implied by the dict argument +-- -- let (dictArg:args') = drop numParams args +-- -- emit =<< mkApplyMethod (fromJust $ toMaybeDict dictArg) methodIdx args' +-- applySigmaAtom (SigmaPartialApp _ f prevArgs) args = +-- emit =<< mkApp f (prevArgs ++ args) + +-- splitParamPrefix :: EnvReader m => TyConName n -> [CAtom n] -> m n (TyConParams n, [CAtom n]) +-- splitParamPrefix tc args = do +-- TyConDef _ _ paramBs _ <- lookupTyCon tc +-- let (paramArgs, dataArgs) = splitAt (nestLength paramBs) args +-- params <- makeTyConParams tc paramArgs +-- return (params, dataArgs) + +-- applyDataCon :: Emits o => TyConName o -> Int -> [CAtom o] -> InfererM i o (CAtom o) +-- applyDataCon tc conIx topArgs = do +-- tyDef@(TyConDef sn _ _ _) <- lookupTyCon tc +-- (params, dataArgs) <- splitParamPrefix tc topArgs +-- ADTCons conDefs <- instantiateTyConDef tyDef params +-- DataConDef _ _ repTy _ <- return $ conDefs !! conIx +-- conProd <- wrap repTy dataArgs +-- repVal <- return case conDefs of +-- [] -> error "unreachable" +-- [_] -> conProd +-- _ -> Con $ SumCon conTys conIx conProd +-- where conTys = conDefs <&> \(DataConDef _ _ rty _) -> rty +-- return $ toAtom $ NewtypeCon (UserADTData sn tc params) repVal +-- where +-- wrap :: EnvReader m => CType n -> [CAtom n] -> m n (CAtom n) +-- wrap _ [arg] = return $ arg +-- wrap rty args = case rty of +-- TyCon (ProdType tys) -> +-- if nargs == ntys +-- then return $ Con $ ProdCon args +-- else Con . ProdCon . (curArgs ++) . (:[]) <$> wrap (last tys) remArgs +-- where +-- nargs = length args; ntys = length tys +-- (curArgs, remArgs) = splitAt (ntys - 1) args +-- TyCon (DepPairTy dpt@(DepPairType _ b rty')) -> do +-- rty'' <- applySubst (b@>SubstVal h) rty' +-- ans <- wrap rty'' t +-- return $ toAtom $ DepPair h ans dpt +-- where h:t = args +-- _ -> error $ "Unexpected data con representation type: " ++ pprint rty + +-- checkExplicitArity :: SrcId -> [Explicitness] -> [a] -> InfererM i o () +-- checkExplicitArity sid expls args = do +-- let arity = length [() | Explicit <- expls] +-- let numArgs = length args +-- when (numArgs /= arity) $ throw sid $ ArityErr arity numArgs + +-- type MixedArgs arg = ([arg], [(SourceName, arg)]) -- positional args, named args +-- data Constraint (n::S) = TypeConstraint SrcId (CType n) (CType n) + +-- type Constraints = ListE Constraint +-- type ConstrainedBinders n = ([IsDependent], Abs (Nest CBinder) Constraints n) + +-- buildConstraints +-- :: HasNamesE e +-- => Abs (Nest CBinder) e o +-- -> (forall o'. DExt o o' => [CAtom o'] -> e o' -> EnvReaderM o' [Constraint o']) +-- -> InfererM i o (ConstrainedBinders o) +-- buildConstraints ab cont = liftEnvReaderM do +-- refreshAbs ab \bs e -> do +-- cs <- cont (toAtom <$> bindersVars bs) e +-- return (getDependence (Abs bs e), Abs bs $ ListE cs) +-- where +-- getDependence :: HasNamesE e => Abs (Nest CBinder) e n -> [IsDependent] +-- getDependence (Abs Empty _) = [] +-- getDependence (Abs (Nest b bs) e) = +-- (binderName b `isFreeIn` Abs bs e) : getDependence (Abs bs e) + +-- -- TODO: check that there are no extra named args provided +-- inferMixedArgs +-- :: forall arg i o . (Emits o, ExplicitArg arg) +-- => SrcId -> SourceName +-- -> [Explicitness] -> ConstrainedBinders o +-- -> MixedArgs (arg i) +-- -> InfererM i o [CAtom o] +-- inferMixedArgs appSrcId fSourceName explsTop (dependenceTop, bsAbs) argsTop@(_, namedArgsTop) = do +-- checkNamedArgValidity appSrcId explsTop (map fst namedArgsTop) +-- liftSolverM $ fromListE <$> go explsTop dependenceTop bsAbs argsTop +-- where +-- go :: Emits oo +-- => [Explicitness] -> [IsDependent] -> Abs (Nest CBinder) Constraints oo -> MixedArgs (arg i) +-- -> SolverM i oo (ListE CAtom oo) +-- go expls dependence (Abs bs cs) args = do +-- cs' <- eagerlyApplyConstraints bs cs +-- case (expls, dependence, bs) of +-- ([], [], Empty) -> return mempty +-- (expl:explsRest, isDependent:dependenceRest, Nest b bsRest) -> do +-- inferMixedArg isDependent (binderType b) expl args \arg restArgs -> do +-- bs' <- applySubst (b @> SubstVal arg) (Abs bsRest cs') +-- (ListE [arg] <>) <$> go explsRest dependenceRest bs' restArgs +-- (_, _, _) -> error "zip error" + +-- eagerlyApplyConstraints +-- :: Nest CBinder oo oo' -> Constraints oo' +-- -> SolverM i oo (Constraints oo') +-- eagerlyApplyConstraints Empty (ListE cs) = mapM_ applyConstraint cs >> return (ListE []) +-- eagerlyApplyConstraints bs (ListE cs) = ListE <$> forMFilter cs \c -> do +-- case hoist bs c of +-- HoistSuccess c' -> case c' of +-- TypeConstraint _ _ _ -> applyConstraint c' >> return Nothing +-- HoistFailure _ -> return $ Just c + +-- inferMixedArg +-- :: (Emits oo, Zonkable e) => IsDependent -> CType oo -> Explicitness -> MixedArgs (arg i) +-- -> (forall o'. (Emits o', DExt oo o') => CAtom o' -> MixedArgs (arg i) -> SolverM i o' (e o')) +-- -> SolverM i oo (e oo) +-- inferMixedArg isDependent argTy' expl args cont = do +-- argTy <- zonk argTy' +-- case expl of +-- Explicit -> do +-- -- this should succeed because we've already done the arity check +-- (arg:argsRest, namedArgs) <- return args +-- if isHole arg +-- then do +-- let desc = (pprint fSourceName, "_") +-- withFreshUnificationVar appSrcId (ImplicitArgInfVar desc) argTy \v -> +-- cont (toAtom v) (argsRest, namedArgs) +-- else do +-- arg' <- checkOrInferExplicitArg isDependent arg argTy +-- withDistinct $ cont arg' (argsRest, namedArgs) +-- Inferred argName infMech -> do +-- let desc = (pprint $ fSourceName, fromMaybe "_" (fmap pprint argName)) +-- case lookupNamedArg args argName of +-- Just arg -> do +-- arg' <- checkOrInferExplicitArg isDependent arg argTy +-- withDistinct $ cont arg' args +-- Nothing -> case infMech of +-- Unify -> withFreshUnificationVar appSrcId (ImplicitArgInfVar desc) argTy \v -> cont (toAtom v) args +-- Synth _ -> withDict appSrcId argTy \d -> cont d args + +-- checkOrInferExplicitArg :: Emits oo => Bool -> arg i -> CType oo -> SolverM i oo (CAtom oo) +-- checkOrInferExplicitArg isDependent arg argTy = do +-- arg' <- lift11 $ withoutInfVarsPartial argTy >>= \case +-- Just partialTy -> case isDependent of +-- True -> checkExplicitDependentArg arg partialTy +-- False -> checkExplicitNonDependentArg arg partialTy +-- Nothing -> inferExplicitArg arg +-- constrainEq (explicitArgSrcId arg) argTy (getType arg') +-- return arg' + +-- lookupNamedArg :: MixedArgs x -> Maybe SourceName -> Maybe x +-- lookupNamedArg _ Nothing = Nothing +-- lookupNamedArg (_, namedArgs) (Just v) = lookup v namedArgs + +-- withoutInfVarsPartial :: CType n -> InfererM i n (Maybe (PartialType n)) +-- withoutInfVarsPartial = \case +-- TyCon (Pi piTy) -> +-- withoutInfVars piTy >>= \case +-- Just piTy' -> return $ Just $ PartialType $ piAsPartialPi piTy' +-- Nothing -> withoutInfVars $ PartialType $ piAsPartialPiDropResultTy piTy +-- ty -> liftM (FullType <$>) $ withoutInfVars ty + +-- withoutInfVars :: HoistableE e => e n -> InfererM i n (Maybe (e n)) +-- withoutInfVars x = hasInferenceVars x >>= \case +-- True -> return Nothing +-- False -> return $ Just x + +-- checkNamedArgValidity :: Fallible m => SrcId -> [Explicitness] -> [SourceName] -> m () +-- checkNamedArgValidity sid expls offeredNames = do +-- let explToMaybeName = \case +-- Explicit -> Nothing +-- Inferred v _ -> v +-- let acceptedNames = catMaybes $ map explToMaybeName expls +-- let duplicates = repeated offeredNames +-- when (not $ null duplicates) $ throw sid $ RepeatedOptionalArgs $ map pprint duplicates +-- let unrecognizedNames = filter (not . (`elem` acceptedNames)) offeredNames +-- when (not $ null unrecognizedNames) do +-- throw sid $ UnrecognizedOptionalArgs (map pprint unrecognizedNames) (map pprint acceptedNames) + +-- inferPrimArg :: Emits o => UExpr i -> InfererM i o (CAtom o) +-- inferPrimArg x = do +-- xBlock <- buildBlock $ bottomUp x +-- case getType xBlock of +-- TyCon (Kind TypeKind) -> reduceExpr xBlock >>= \case +-- Just reduced -> return reduced +-- _ -> throwInternal "Type args to primops must be reducible" +-- _ -> emit xBlock + +-- matchPrimApp :: Emits o => PrimName -> [CAtom o] -> InfererM i o (CAtom o) +-- matchPrimApp = \case +-- UNat -> \case ~[] -> return $ toAtom $ NewtypeTyCon Nat +-- UFin -> \case ~[n] -> return $ toAtom $ NewtypeTyCon (Fin n) +-- UBaseType b -> \case ~[] -> return $ toAtomR $ BaseType b +-- UNatCon -> \case ~[x] -> return $ toAtom $ NewtypeCon NatCon x +-- UPrimTC tc -> case tc of +-- S.ProdType -> \ts -> return $ toAtom $ ProdType $ map (fromJust . toMaybeType) ts +-- S.SumType -> \ts -> return $ toAtom $ SumType $ map (fromJust . toMaybeType) ts +-- S.RefType -> \case ~[h, a] -> undefined -- return $ toAtom $ RefType h (fromJust $ toMaybeType a) +-- S.TypeKind -> \case ~[] -> return $ toAtom $ Kind $ TypeKind +-- UCon con -> case con of +-- S.ProdCon -> \xs -> return $ toAtom $ ProdCon xs +-- S.SumCon _ -> error "not supported" +-- -- UMiscOp op -> \x -> emit =<< MiscOp <$> matchGenericOp op x +-- -- UMemOp op -> \x -> emit =<< MemOp <$> matchGenericOp op x +-- UBinOp op -> \case ~[x, y] -> emitBinOp op x y +-- UUnOp op -> \case ~[x] -> emitUnOp op x +-- UMGet -> \case ~[r] -> emitRefOp r MGet +-- UMPut -> \case ~[r, x] -> emitRefOp r $ MPut x +-- UIndexRef -> \case ~[r, i] -> indexRef r i +-- UApplyMethod i -> \case ~(d:args) -> emit =<< mkApplyMethod (fromJust $ toMaybeDict d) i args +-- ULinearize -> \case ~[f, x] -> do f' <- lam1 f; emitHof $ Linearize f' x +-- UTranspose -> \case ~[f, x] -> do f' <- lam1 f; emitHof $ Transpose f' x +-- p -> \case xs -> throwInternal $ "Bad primitive application: " ++ show (p, xs) +-- where +-- lam2 :: Fallible m => CAtom n -> m (LamExpr n) +-- lam2 x = do +-- ExplicitCoreLam (BinaryNest b1 b2) body <- return x +-- return $ BinaryLamExpr b1 b2 body + +-- lam1 :: Fallible m => CAtom n -> m (LamExpr n) +-- lam1 x = do +-- ExplicitCoreLam (UnaryNest b) body <- return x +-- return $ UnaryLamExpr b body + +-- -- matchGenericOp :: GenericOp op => OpConst op -> [CAtom n] -> InfererM i n (op n) +-- -- matchGenericOp op xs = do +-- -- (tyArgs, dataArgs) <- partitionEithers <$> forM xs \x -> do +-- -- case getType x of +-- -- TyCon (Kind TypeKind) -> do +-- -- Just x' <- return $ toMaybeType x +-- -- return $ Left x' +-- -- _ -> return $ Right x +-- -- let tyArgs' = case tyArgs of +-- -- [] -> Nothing +-- -- [t] -> Just t +-- -- _ -> error "Expected at most one type arg" +-- -- return $ fromJust $ toOp $ GenericOpRep op tyArgs' dataArgs + +-- pattern ExplicitCoreLam :: Nest CBinder n l -> CExpr l -> CAtom n +-- pattern ExplicitCoreLam bs body <- Con (Lam (CoreLamExpr _ (LamExpr bs body))) + +-- -- === n-ary applications === + +-- inferTabApp :: Emits o => SrcId -> CAtom o -> [UExpr i] -> InfererM i o (CAtom o) +-- inferTabApp tabSrcId tab args = do +-- tabTy <- return $ getType tab +-- args' <- inferNaryTabAppArgs tabSrcId tabTy args +-- naryTabApp tab args' + +-- inferNaryTabAppArgs :: Emits o => SrcId -> CType o -> [UExpr i] -> InfererM i o [CAtom o] +-- inferNaryTabAppArgs _ _ [] = return [] +-- inferNaryTabAppArgs tabSrcId tabTy (arg:rest) = case tabTy of +-- TyCon (TabPi (TabPiType _ b resultTy)) -> do +-- let ixTy = binderType b +-- let isDependent = binderName b `isFreeIn` resultTy +-- arg' <- if isDependent +-- then checkSigmaDependent arg (FullType ixTy) +-- else topDown ixTy arg +-- resultTy' <- applySubst (b @> SubstVal arg') resultTy +-- rest' <- inferNaryTabAppArgs tabSrcId resultTy' rest +-- return $ arg':rest' +-- _ -> throw tabSrcId $ EliminationErr "table type" (pprint tabTy) + +-- checkSigmaDependent :: UExpr i -> PartialType o -> InfererM i o (CAtom o) +-- checkSigmaDependent e ty = withReducibleEmissions (getSrcId e) CantReduceDependentArg $ +-- topDownPartial (sink ty) e + +-- -- === sorting case alternatives === + +-- data IndexedAlt n = IndexedAlt CaseAltIndex (Alt n) + +-- instance SinkableE IndexedAlt where +-- sinkingProofE = todoSinkableProof + +-- buildNthOrderedAlt :: (Emits n, Builder m) +-- => [IndexedAlt n] -> CType n -> CType n -> Int -> CAtom n +-- -> m n (CAtom n) +-- buildNthOrderedAlt alts _ resultTy i v = do +-- case lookup i [(idx, alt) | IndexedAlt idx alt <- alts] of +-- Nothing -> do +-- resultTy' <- sinkM resultTy +-- emit $ PrimOp resultTy' $ MiscOp ThrowError +-- Just alt -> applyAbs alt (SubstVal v) >>= emit + +-- buildMonomorphicCase +-- :: (Emits n, ScopableBuilder m) +-- => [IndexedAlt n] -> CAtom n -> CType n -> m n (CAtom n) +-- buildMonomorphicCase alts scrut resultTy = do +-- scrutTy <- return $ getType scrut +-- buildCase scrut resultTy \i v -> do +-- ListE alts' <- sinkM $ ListE alts +-- scrutTy' <- sinkM scrutTy +-- resultTy' <- sinkM resultTy +-- buildNthOrderedAlt alts' scrutTy' resultTy' i v + +-- buildSortedCase :: (Fallible1 m, Builder m, Emits n) +-- => CAtom n -> [IndexedAlt n] -> CType n +-- -> m n (CAtom n) +-- buildSortedCase scrut alts resultTy = do +-- scrutTy <- return $ getType scrut +-- case scrutTy of +-- TyCon (NewtypeTyCon (UserADTType _ defName _)) -> do +-- TyConDef _ _ _ (ADTCons cons) <- lookupTyCon defName +-- case cons of +-- [] -> error "case of void?" +-- -- Single constructor ADTs are not sum types, so elide the case. +-- [_] -> do +-- let [IndexedAlt _ alt] = alts +-- scrut' <- unwrapNewtype scrut +-- emit =<< applyAbs alt (SubstVal scrut') +-- _ -> do +-- scrut' <- unwrapNewtype scrut +-- liftEmitBuilder $ buildMonomorphicCase alts scrut' resultTy +-- _ -> fail $ "Unexpected case expression type: " <> pprint scrutTy + +-- -- TODO: cache this with the instance def (requires a recursive binding) +-- instanceFun :: EnvReader m => InstanceName n -> AppExplicitness -> m n (CAtom n) +-- instanceFun instanceName appExpl = do +-- InstanceDef _ expls bs _ _ <- lookupInstanceDef instanceName +-- liftEnvReaderM $ refreshAbs (Abs bs UnitE) \bs' UnitE -> do +-- args <- mapM toAtomVar $ nestToNames bs' +-- result <- toAtom <$> mkInstanceDict (sink instanceName) (toAtom <$> args) +-- let piTy = CorePiType appExpl expls bs' (getType result) +-- return $ toAtom $ CoreLamExpr piTy (LamExpr bs' $ Atom result) + +checkMaybeAnnExpr :: Maybe (UType i) -> UExpr i -> InfererM i o (CExpr o) +checkMaybeAnnExpr ty expr = case ty of + Nothing -> bottomUp expr + Just ty' -> do + ty'' <- checkUType ty' + topDown ty'' expr + +-- inferTyConDef :: UDataDef i -> InfererM i o (TyConDef o) +-- inferTyConDef (UDataDef tyConName paramBs dataCons) = do +-- withUBinders paramBs \(ZipB expls paramBs') -> do +-- dataCons' <- ADTCons <$> mapM inferDataCon dataCons +-- return (TyConDef tyConName expls paramBs' dataCons') + +-- inferStructDef :: UStructDef i -> InfererM i o (TyConDef o) +-- inferStructDef (UStructDef tyConName paramBs fields _) = do +-- withUBinders paramBs \(ZipB expls paramBs') -> do +-- let (fieldNames, fieldTys) = unzip fields +-- tys <- mapM checkUType fieldTys +-- let dataConDefs = StructFields $ zip (withoutSrc <$> fieldNames) tys +-- return $ TyConDef tyConName expls paramBs' dataConDefs + +-- inferDotMethod +-- :: TyConName o +-- -> Abs (Nest UAnnBinder) (Abs UBinder ULamExpr) i +-- -> InfererM i o (CoreLamExpr o) +-- inferDotMethod tc (Abs uparamBs (Abs selfB lam)) = do +-- TyConDef sn expls paramBs _ <- lookupTyCon tc +-- withFreshBindersInf expls (Abs paramBs UnitE) \paramBs' UnitE -> do +-- let paramVs = bindersVars paramBs' +-- extendRenamer (uparamBs @@> (atomVarName <$> paramVs)) do +-- let selfTy = toType $ UserADTType sn (sink tc) (TyConParams expls (toAtom <$> paramVs)) +-- withFreshBinderInf "self" Explicit selfTy \selfB' -> do +-- lam' <- extendRenamer (selfB @> binderName selfB') $ inferULam lam +-- return $ prependCoreLamExpr (expls ++ [Explicit]) (paramBs' >>> UnaryNest selfB') lam' + +-- where +-- prependCoreLamExpr :: [Explicitness] -> Nest CBinder n l -> CoreLamExpr l -> CoreLamExpr n +-- prependCoreLamExpr expls bs e = case e of +-- CoreLamExpr (CorePiType appExpl piExpls piBs effTy) (LamExpr lamBs body) -> do +-- let piType = CorePiType appExpl (expls <> piExpls) (bs >>> piBs) effTy +-- let lamExpr = LamExpr (bs >>> lamBs) body +-- CoreLamExpr piType lamExpr + +-- inferDataCon :: (SourceName, UDataDefTrail i) -> InfererM i o (DataConDef o) +-- inferDataCon (sourceName, UDataDefTrail argBs) = do +-- withUBinders argBs \(ZipB _ argBs') -> do +-- let (repTy, projIdxs) = dataConRepTy $ EmptyAbs argBs' +-- return $ DataConDef sourceName (EmptyAbs argBs') repTy projIdxs + +-- dataConRepTy :: EmptyAbs (Nest CBinder) n -> (CType n, [[Projection]]) +-- dataConRepTy (Abs topBs UnitE) = case topBs of +-- Empty -> (UnitTy, []) +-- _ -> go [] [UnwrapNewtype] topBs +-- where +-- go :: [CType l] -> [Projection] -> Nest (Binder) l p -> (CType l, [[Projection]]) +-- go revAcc projIdxs = \case +-- Empty -> case revAcc of +-- [] -> error "should never happen" +-- [ty] -> (ty, [projIdxs]) +-- _ -> ( toType $ ProdType $ reverse revAcc +-- , iota (length revAcc) <&> \i -> ProjectProduct i:projIdxs ) +-- Nest b bs -> case hoist b (EmptyAbs bs) of +-- HoistSuccess (Abs bs' UnitE) -> go (binderType b:revAcc) projIdxs bs' +-- HoistFailure _ -> (fullTy, idxs) +-- where +-- accSize = length revAcc +-- (fullTy, depTyIdxs) = case revAcc of +-- [] -> (depTy, []) +-- _ -> (toType $ ProdType $ reverse revAcc ++ [depTy], [ProjectProduct accSize]) +-- (tailTy, tailIdxs) = go [] (ProjectProduct 1 : (depTyIdxs ++ projIdxs)) bs +-- idxs = (iota accSize <&> \i -> ProjectProduct i : projIdxs) ++ +-- ((ProjectProduct 0 : (depTyIdxs ++ projIdxs)) : tailIdxs) +-- depTy = toType $ DepPairTy $ DepPairType ExplicitDepPair b tailTy + +-- inferClassDef +-- :: SourceName -> [SourceName] -> Nest UAnnBinder i i' -> [UType i'] +-- -> InfererM i o (ClassDef o) +-- inferClassDef className methodNames paramBs methodTys = do +-- withUBinders paramBs \(ZipB expls paramBs') -> do +-- let paramNames = catMaybes $ nestToListFlip paramBs \(UAnnBinder expl b _ _) -> +-- case expl of Inferred _ (Synth _) -> Nothing +-- _ -> Just $ Just $ getSourceName b +-- methodTys' <- forM methodTys \m -> do +-- checkUType m >>= \case +-- TyCon (Pi t) -> return t +-- t -> return $ CorePiType ImplicitApp [] Empty t +-- PairB paramBs'' superclassBs <- partitionBinders rootSrcId (zipAttrs expls paramBs') $ +-- \b@(WithAttrB expl b') -> case expl of +-- Explicit -> return $ LeftB b +-- -- TODO: Add a proper SrcId here. We'll need to plumb it through from the original UBinders +-- Inferred _ Unify -> throw rootSrcId InterfacesNoImplicitParams +-- Inferred _ (Synth _) -> return $ RightB b' +-- let (roleExpls', paramBs''') = unzipAttrs paramBs'' +-- builtinName <- case className of +-- -- TODO: this is hacky. Let's just make the Ix class, including its +-- -- methods, fully built-in instead of prelude-defined. +-- "Ix" -> return $ Just Ix +-- _ -> return Nothing +-- return $ ClassDef className builtinName methodNames paramNames roleExpls' paramBs''' superclassBs methodTys' + +-- withUBinder :: UAnnBinder i i' -> InfererCPSB2 (WithExpl CBinder) i i' o a +-- withUBinder (UAnnBinder expl (WithSrcB sid b) ann cs) cont = do +-- ty <- inferAnn sid ann cs +-- emitExprType sid ty +-- withFreshBinderInf (getNameHint b) expl ty \b' -> +-- extendSubst (b@>binderName b') $ cont (WithAttrB expl b') + +-- withUBinders :: Nest UAnnBinder i i' -> InfererCPSB2 (Nest (WithExpl CBinder)) i i' o a +-- withUBinders bs cont = do +-- Abs bs' UnitE <- inferUBinders bs \_ -> return UnitE +-- let (expls, bs'') = unzipAttrs bs' +-- withFreshBindersInf expls (Abs bs'' UnitE) \bs''' UnitE -> do +-- extendSubst (bs@@> (atomVarName <$> bindersVars bs''')) $ +-- cont $ zipAttrs expls bs''' + +-- inferUBinders +-- :: Zonkable e => Nest UAnnBinder i i' +-- -> (forall o'. DExt o o' => [CAtomName o'] -> InfererM i' o' (e o')) +-- -> InfererM i o (Abs (Nest (WithExpl CBinder)) e o) +-- inferUBinders Empty cont = withDistinct $ Abs Empty <$> cont [] +-- inferUBinders (Nest (UAnnBinder expl (WithSrcB sid b) ann cs) bs) cont = do +-- -- TODO: factor out the common part of each case (requires an annotated +-- -- `where` clause because of the rank-2 type) +-- ty <- inferAnn sid ann cs +-- emitExprType sid ty +-- withFreshBinderInf (getNameHint b) expl ty \b' -> do +-- extendSubst (b@>binderName b') do +-- Abs bs' e <- inferUBinders bs \vs -> cont (sink (binderName b') : vs) +-- return $ Abs (Nest (WithAttrB expl b') bs') e + +-- inferAnn :: SrcId -> UAnn i -> [UConstraint i] -> InfererM i o (CType o) +-- inferAnn binderSrcId ann cs = case ann of +-- UAnn ty -> checkUType ty +-- UNoAnn -> case cs of +-- WithSrcE sid (UVar ~(InternalName _ _ v)):_ -> do +-- renameM v >>= getUVarType >>= \case +-- TyCon (Pi (CorePiType ExplicitApp [Explicit] (UnaryNest (_:>ty)) _)) -> return ty +-- ty -> throw sid $ NotAUnaryConstraint $ pprint ty +-- _ -> throw binderSrcId AnnotationRequired + +-- checkULamPartial :: PartialPiType o -> SrcId -> ULamExpr i -> InfererM i o (CoreLamExpr o) +-- checkULamPartial partialPiTy sid lamExpr = do +-- PartialPiType piAppExpl expls piBs piReqTy <- return partialPiTy +-- ULamExpr lamBs lamAppExpl lamResultTy body <- return lamExpr +-- checkExplicitArity sid expls (nestToList (const ()) lamBs) +-- when (piAppExpl /= lamAppExpl) $ throw sid $ WrongArrowErr (pprint piAppExpl) (pprint lamAppExpl) +-- checkLamBinders expls piBs lamBs \lamBs' -> do +-- piReqTy' <- applyRename (piBs @@> (atomVarName <$> bindersVars lamBs')) piReqTy +-- resultTy <- case (lamResultTy, piReqTy') of +-- (Nothing, Infer ) -> return Infer +-- (Just t , Infer ) -> Check <$> checkUType t +-- (Nothing, Check t) -> Check <$> return t +-- (Just t , Check t') -> checkUType t >>= expectEq (getSrcId t) t' >> return (Check t') +-- body' <- buildBlock $ withBlockDecls body \result -> checkOrInfer (sink resultTy) result +-- resultTy' <- case resultTy of +-- Infer -> return $ getType body' +-- Check t -> return t +-- let piTy = CorePiType piAppExpl expls lamBs' resultTy' +-- return $ CoreLamExpr piTy (LamExpr lamBs' body') +-- where +-- checkLamBinders +-- :: [Explicitness] -> Nest CBinder o any -> Nest UAnnBinder i i' +-- -> InfererCPSB2 (Nest CBinder) i i' o a +-- checkLamBinders [] Empty Empty cont = withDistinct $ cont Empty +-- checkLamBinders (piExpl:piExpls) (Nest (piB:>piAnn) piBs) lamBs cont = do +-- case piExpl of +-- Inferred _ _ -> do +-- withFreshBinderInf (getNameHint piB) piExpl piAnn \b -> do +-- Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs) +-- checkLamBinders piExpls piBs' lamBs \bs -> cont (Nest b bs) +-- Explicit -> case lamBs of +-- Nest (UAnnBinder _ (WithSrcB bSid lamB) lamAnn _) lamBsRest -> emitExprType bSid piAnn >> do +-- case lamAnn of +-- UAnn lamAnn' -> checkUType lamAnn' >>= expectEq (getSrcId lamAnn') piAnn +-- UNoAnn -> return () +-- withFreshBinderInf (getNameHint lamB) Explicit piAnn \b -> do +-- Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs) +-- extendRenamer (lamB@>sink (binderName b)) $ +-- checkLamBinders piExpls piBs' lamBsRest \bs -> cont (Nest b bs) +-- Empty -> error "zip error" +-- checkLamBinders _ _ _ _ = error "zip error" + +-- inferUForExpr :: Emits o => UForExpr i -> InfererM i o (LamExpr o) +-- inferUForExpr (UForExpr b body) = do +-- withUBinder b \(WithAttrB _ b') -> do +-- body' <- buildBlock $ withBlockDecls body \result -> bottomUp result +-- return $ LamExpr (UnaryNest b') body' + +-- checkUForExpr :: Emits o => SrcId -> UForExpr i -> TabPiType o -> InfererM i o (LamExpr o) +-- checkUForExpr sid (UForExpr bFor body) (TabPiType _ bPi resultTy) = do +-- let uLamExpr = ULamExpr (UnaryNest bFor) ExplicitApp Nothing body +-- partialPi <- liftEnvReaderM $ refreshAbs (Abs bPi resultTy) \bPi' resultTy' -> do +-- return $ PartialPiType ExplicitApp [Explicit] (UnaryNest bPi') (Check resultTy') +-- CoreLamExpr _ lamExpr <- checkULamPartial partialPi sid uLamExpr +-- return lamExpr + +-- inferULam :: ULamExpr i -> InfererM i o (CoreLamExpr o) +-- inferULam (ULamExpr bs appExpl resultTy body) = do +-- Abs (ZipB expls bs') (PairE ty body') <- inferUBinders bs \_ -> do +-- resultTy' <- mapM checkUType resultTy +-- body' <- buildBlock do +-- withBlockDecls body \result -> +-- case resultTy' of +-- Nothing -> bottomUp result +-- Just resultTy'' -> topDown (sink resultTy'') result +-- return $ PairE (getType body') body' +-- return $ CoreLamExpr (CorePiType appExpl expls bs' ty) (LamExpr bs' body') + +-- checkULam :: SrcId -> ULamExpr i -> CorePiType o -> InfererM i o (CoreLamExpr o) +-- checkULam sid ulam piTy = checkULamPartial (piAsPartialPi piTy) sid ulam + +-- piAsPartialPi :: CorePiType n -> PartialPiType n +-- piAsPartialPi (CorePiType appExpl expls bs ty) = +-- PartialPiType appExpl expls bs (Check ty) + +-- typeAsPartialType :: CType n -> PartialType n +-- typeAsPartialType (TyCon (Pi piTy)) = PartialType $ piAsPartialPi piTy +-- typeAsPartialType ty = FullType ty + +-- piAsPartialPiDropResultTy :: CorePiType n -> PartialPiType n +-- piAsPartialPiDropResultTy (CorePiType appExpl expls bs _) = +-- PartialPiType appExpl expls bs Infer + +-- checkInstanceParams :: Nest CBinder o any -> [UExpr i] -> InfererM i o [CAtom o] +-- checkInstanceParams bsTop paramsTop = go bsTop paramsTop +-- where +-- go :: Nest CBinder o any -> [UExpr i] -> InfererM i o [CAtom o] +-- go Empty [] = return [] +-- go (Nest (b:>ty) bs) (x:xs) = do +-- let msg = CantReduceType $ pprint x +-- x' <- withReducibleEmissions (getSrcId x) msg $ topDown (sink ty) x +-- Abs bs' UnitE <- applySubst (b@>SubstVal x') $ Abs bs UnitE +-- (x':) <$> go bs' xs +-- go _ _ = error "zip error" + +-- checkInstanceBody +-- :: ClassName o -> [CAtom o] +-- -> [UMethodDef i] -> InfererM i o (InstanceBody o) +-- checkInstanceBody className params methods = do +-- -- instances are top-level so it's ok to have imprecise root srcIds here +-- let sid = rootSrcId +-- ClassDef _ _ methodNames _ _ paramBs scBs methodTys <- lookupClassDef className +-- Abs scBs' methodTys' <- applySubst (paramBs @@> (SubstVal <$> params)) $ Abs scBs $ ListE methodTys +-- superclassTys <- superclassDictTys scBs' +-- superclassDicts <- mapM (flip (trySynthTerm sid) Full) superclassTys +-- ListE methodTys'' <- applySubst (scBs'@@>(SubstVal<$>superclassDicts)) methodTys' +-- methodsChecked <- mapM (checkMethodDef className methodTys'') methods +-- let (idxs, methods') = unzip $ sortOn fst $ methodsChecked +-- forM_ (repeated idxs) \i -> +-- throw sid $ DuplicateMethod $ pprint (methodNames!!i) +-- forM_ ([0..(length methodTys''-1)] `listDiff` idxs) \i -> +-- throw sid $ MissingMethod $ pprint (methodNames!!i) +-- return $ InstanceBody superclassDicts methods' + +-- superclassDictTys :: Nest CBinder o o' -> InfererM i o [CType o] +-- superclassDictTys Empty = return [] +-- superclassDictTys (Nest b bs) = do +-- Abs bs' UnitE <- liftHoistExcept rootSrcId $ hoist b $ Abs bs UnitE +-- (binderType b:) <$> superclassDictTys bs' + +-- checkMethodDef :: ClassName o -> [CorePiType o] -> UMethodDef i -> InfererM i o (Int, CAtom o) +-- checkMethodDef className methodTys (WithSrcE sid m) = do +-- UMethodDef ~(InternalName _ sourceName v) rhs <- return m +-- MethodBinding className' i <- renameM v >>= lookupEnv +-- when (className /= className') do +-- ClassBinding classDef <- lookupEnv className +-- throw sid $ NotAMethod (pprint sourceName) (pprint $ getSourceName classDef) +-- (i,) <$> toAtom <$> Lam <$> checkULam sid rhs (methodTys !! i) + +-- type CaseAltIndex = Int + +-- checkCaseAlt :: Emits o => RequiredTy o -> CType o -> UAlt i -> InfererM i o (IndexedAlt o) +-- checkCaseAlt reqTy scrutineeTy (UAlt pat body) = do +-- alt <- checkCasePat pat scrutineeTy do +-- withBlockDecls body \result -> checkOrInfer (sink reqTy) result +-- idx <- getCaseAltIndex pat +-- return $ IndexedAlt idx alt + +-- getCaseAltIndex :: UPat i i' -> InfererM i o CaseAltIndex +-- getCaseAltIndex (WithSrcB sid pat) = case pat of +-- UPatCon ~(InternalName _ _ conName) _ -> do +-- (_, con) <- renameM conName >>= lookupDataCon +-- return con +-- _ -> throw sid IllFormedCasePattern + +-- checkCasePat +-- :: Emits o +-- => UPat i i' -> CType o +-- -> (forall o'. (Emits o', Ext o o') => InfererM i' o' (CAtom o')) +-- -> InfererM i o (Alt o) +-- checkCasePat (WithSrcB sid pat) scrutineeTy cont = case pat of +-- UPatCon ~(InternalName _ _ conName) ps -> do +-- (dataDefName, con) <- renameM conName >>= lookupDataCon +-- tyConDef <- lookupTyCon dataDefName +-- params <- inferParams sid scrutineeTy dataDefName +-- ADTCons cons <- instantiateTyConDef tyConDef params +-- DataConDef _ _ repTy idxs <- return $ cons !! con +-- when (length idxs /= nestLength ps) $ throw sid $ PatternArityErr (length idxs) (nestLength ps) +-- withFreshBinderInf noHint Explicit repTy \b -> Abs b <$> do +-- buildBlock do +-- args <- forM idxs \projs -> do +-- emitToVar =<< applyProjectionsReduced (init projs) (sink $ toAtom $ binderVar b) +-- bindLetPats ps args $ cont +-- _ -> throw sid IllFormedCasePattern + +-- inferParams :: Emits o => SrcId -> CType o -> TyConName o -> InfererM i o (TyConParams o) +-- inferParams sid ty dataDefName = do +-- TyConDef sourceName paramExpls paramBs _ <- lookupTyCon dataDefName +-- let inferenceExpls = paramExpls <&> \case +-- Explicit -> Inferred Nothing Unify +-- expl -> expl +-- paramBsAbs <- buildConstraints (Abs paramBs UnitE) \params _ -> do +-- let ty' = toType $ UserADTType sourceName (sink dataDefName) $ TyConParams paramExpls params +-- return [TypeConstraint sid (sink ty) ty'] +-- args <- inferMixedArgs sid sourceName inferenceExpls paramBsAbs emptyMixedArgs +-- return $ TyConParams paramExpls args + +-- bindLetPats +-- :: (Emits o, HasNamesE e) +-- => Nest UPat i i' -> [CAtomVar o] +-- -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) +-- -> InfererM i o (e o) +-- bindLetPats Empty [] cont = getDistinct >>= \Distinct -> cont +-- bindLetPats (Nest p ps) (x:xs) cont = bindLetPat p x $ bindLetPats ps (sink <$> xs) cont +-- bindLetPats _ _ _ = error "mismatched number of args" + +-- bindLetPat +-- :: (Emits o, HasNamesE e) +-- => UPat i i' -> CAtomVar o +-- -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) +-- -> InfererM i o (e o) +-- bindLetPat (WithSrcB sid pat) v cont = emitExprType sid (getType v) >> case pat of +-- UPatBinder b -> getDistinct >>= \Distinct -> extendSubst (b @> atomVarName v) cont +-- UPatProd ps -> do +-- let n = nestLength ps +-- case getType v of +-- TyCon (ProdType ts) | length ts == n -> return () +-- ty -> throw sid $ PatTypeErr "product type" (pprint ty) +-- xs <- forM (iota n) \i -> proj i (toAtom v) >>= emitInline +-- bindLetPats ps xs cont +-- UPatDepPair (PairB p1 p2) -> do +-- case getType v of +-- TyCon (DepPairTy _) -> return () +-- ty -> throw sid $ PatTypeErr "dependent pair" (pprint ty) +-- -- XXX: we're careful here to reduce the projection because of the dependent +-- -- types. We do the same in the `UPatCon` case. +-- x1 <- reduceProj 0 (toAtom v) >>= emitInline +-- bindLetPat p1 x1 do +-- x2 <- getSnd (sink $ toAtom v) >>= emitInline +-- bindLetPat p2 x2 do +-- cont +-- UPatCon ~(InternalName _ _ conName) ps -> do +-- (dataDefName, _) <- lookupDataCon =<< renameM conName +-- TyConDef _ _ _ cons <- lookupTyCon dataDefName +-- case cons of +-- ADTCons [DataConDef _ _ _ idxss] -> do +-- when (length idxss /= nestLength ps) $ +-- throw sid $ PatternArityErr (length idxss) (nestLength ps) +-- void $ inferParams sid (getType $ toAtom v) dataDefName +-- xs <- forM idxss \idxs -> applyProjectionsReduced idxs (toAtom v) >>= emitInline +-- bindLetPats ps xs cont +-- _ -> throw sid SumTypeCantFail +-- UPatTable ps -> do +-- let n = fromIntegral (nestLength ps) :: Word32 +-- case getType v of +-- TyCon (TabPi (TabPiType _ (_:>FinConst n') _)) | n == n' -> return () +-- ty -> throw sid $ PatTypeErr ("Fin " ++ show n ++ " table") (pprint ty) +-- xs <- forM [0 .. n - 1] \i -> do +-- emitToVar =<< mkTabApp (toAtom v) (toAtom $ NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i)) +-- bindLetPats ps xs cont +-- where +-- emitInline :: Emits n => CAtom n -> InfererM i n (AtomVar n) +-- emitInline atom = emitDecl noHint InlineLet $ Atom atom + +checkUType :: UType i -> InfererM i o (CType o) +checkUType t = do + topDownType t + where msg = CantReduceType $ pprint t + +-- inferTabCon :: forall i o. Emits o => SrcId -> [UExpr i] -> InfererM i o (CAtom o) +-- inferTabCon sid xs = do +-- let n = fromIntegral (length xs) :: Word32 +-- let finTy = FinConst n +-- elemTy <- case xs of +-- [] -> throw sid InferEmptyTable +-- x:_ -> getType <$> bottomUp x +-- ixTy <- asIxType sid finTy +-- let tabTy = ixTy ==> elemTy +-- xs' <- forM xs \x -> topDown elemTy x +-- emit $ TabCon tabTy xs' + +-- checkTabCon :: forall i o. Emits o => TabPiType o -> SrcId -> [UExpr i] -> InfererM i o (CAtom o) +-- checkTabCon tabTy@(TabPiType _ b elemTy) sid xs = do +-- let n = fromIntegral (length xs) :: Word32 +-- let finTy = FinConst n +-- expectEq sid (binderType b) finTy +-- xs' <- forM (enumerate xs) \(i, x) -> do +-- let i' = toAtom (NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i)) :: CAtom o +-- elemTy' <- applySubst (b@>SubstVal i') elemTy +-- topDown elemTy' x +-- emit $ TabCon (TyCon (TabPi tabTy)) xs' + +-- getIxDict :: SrcId -> CType o -> InfererM i o (IxDict o) +-- getIxDict sid t = fromJust <$> toMaybeDict <$> trySynthTerm sid (toType $ IxDictType t) Full + +-- asIxType :: SrcId -> CType o -> InfererM i o (IxType o) +-- asIxType sid ty = IxType ty <$> getIxDict sid ty + +-- -- === Solver === + +-- -- TODO: put this pattern and friends in the Name library? Don't really want to +-- -- have to think about `eqNameColorRep` just to implement a partial map. +-- lookupSolverSubst :: forall n. SolverSubst n -> Name n -> AtomSubstVal n +-- lookupSolverSubst (SolverSubst m) name = undefined +-- -- lookupSolverSubst (SolverSubst m) name = +-- -- case eqColorRep of +-- -- Nothing -> Rename name +-- -- Just (ColorsEqual :: ColorsEqual c (AtomNameC))-> case M.lookup name m of +-- -- Nothing -> Rename name +-- -- Just sol -> SubstVal sol + +-- applyConstraint :: Constraint o -> SolverM i o () +-- applyConstraint = \case +-- TypeConstraint sid t1 t2 -> constrainEq sid t1 t2 + +-- constrainEq :: ToAtom e => SrcId -> e o -> e o -> SolverM i o () +-- constrainEq sid t1 t2 = do +-- t1' <- zonk $ toAtom t1 +-- t2' <- zonk $ toAtom t2 +-- msg <- liftEnvReaderM do +-- ab <- renameForPrinting $ PairE t1' t2' +-- return $ canonicalizeForPrinting ab \(Abs infVars (PairE t1Pretty t2Pretty)) -> +-- UnificationFailure (pprint t1Pretty) (pprint t2Pretty) (nestToList pprint infVars) +-- void $ searchFailureAsTypeErr sid msg $ unify t1' t2' + +-- searchFailureAsTypeErr :: ToErr e => SrcId -> e -> SolverM i n a -> SolverM i n a +-- searchFailureAsTypeErr sid msg cont = cont <|> throw sid msg +-- {-# INLINE searchFailureAsTypeErr #-} + +-- class AlphaEqE e => Unifiable (e::E) where +-- unify :: e n -> e n -> SolverM i n () + +-- instance Unifiable (Stuck) where +-- unify s1 s2 = do +-- x1 <- zonkStuck s1 +-- x2 <- zonkStuck s2 +-- case (x1, x2) of +-- (Con c, Con c') -> unify c c' +-- (Stuck _ s, Stuck _ s') -> unifyStuckZonked s s' +-- (Stuck _ s, Con c) -> unifyStuckConZonked s c +-- (Con c, Stuck _ s) -> unifyStuckConZonked s c + +-- -- assumes both `CStuck` args are zonked +-- unifyStuckZonked :: CStuck n -> CStuck n -> SolverM i n () +-- unifyStuckZonked s1 s2 = do +-- x1 <- mkStuck s1 +-- x2 <- mkStuck s2 +-- case (s1, s2) of +-- (Var v1, Var v2) -> do +-- if atomVarName v1 == atomVarName v2 +-- then return () +-- else extendSolution v2 x1 <|> extendSolution v1 x2 +-- (_, Var v2) -> extendSolution v2 x1 +-- (Var v1, _) -> extendSolution v1 x2 +-- (_, _) -> unifyEq s1 s2 + +-- unifyStuckConZonked :: CStuck n -> Con n -> SolverM i n () +-- unifyStuckConZonked s x = case s of +-- Var v -> extendSolution v (Con x) +-- _ -> empty + +-- unifyStuckCon :: CStuck n -> Con n -> SolverM i n () +-- unifyStuckCon s con = do +-- x <- zonkStuck s +-- case x of +-- Stuck _ s' -> unifyStuckConZonked s' con +-- Con con' -> unify con' con + +-- instance Unifiable (Atom) where +-- unify (Con c) (Con c') = unify c c' +-- unify (Stuck _ s) (Stuck _ s') = unify s s' +-- unify (Stuck _ s) (Con c) = unifyStuckCon s c +-- unify (Con c) (Stuck _ s) = unifyStuckCon s c + +-- -- TODO: do this directly rather than going via `CAtom` using `Type`. We just +-- -- need to deal with `Stuck`. +-- instance Unifiable (Type) where +-- unify (TyCon c) (TyCon c') = unify c c' +-- unify (StuckTy _ s) (StuckTy _ s') = unify s s' +-- unify (StuckTy _ s) (TyCon c) = unifyStuckCon s (TyConAtom c) +-- unify (TyCon c) (StuckTy _ s) = unifyStuckCon s (TyConAtom c) + +-- instance Unifiable (Con) where +-- unify e1 e2 = case e1 of +-- ( Lit x ) -> do +-- { Lit x' <- matchit; guard (x == x')} +-- ( ProdCon xs ) -> do +-- { ProdCon xs' <- matchit; unifyLists xs xs'} +-- ( SumCon ts i x ) -> do +-- { SumCon ts' i' x' <- matchit; unifyLists ts ts'; guard (i==i'); unify x x'} +-- ( DepPair t x y ) -> do +-- { DepPair t' x' y' <- matchit; unify t t'; unify x x'; unify y y'} +-- ( Lam lam ) -> do +-- { Lam lam' <- matchit; unifyEq lam lam'} +-- ( NewtypeCon con x ) -> do +-- { NewtypeCon con' x' <- matchit; unifyEq con con'; unify x x'} +-- ( TyConAtom t ) -> do +-- { TyConAtom t' <- matchit; unify t t'} +-- ( DictConAtom d ) -> do +-- { DictConAtom d' <- matchit; unifyEq d d'} +-- where matchit = return e2 + +-- instance Unifiable (TyCon) where +-- unify t1 t2 = case t1 of +-- ( BaseType b ) -> do +-- { BaseType b' <- matchit; guard $ b == b'} +-- ( Kind k ) -> do +-- { Kind k' <- matchit; guard $ k == k' } +-- ( Pi piTy ) -> do +-- { Pi piTy' <- matchit; unify piTy piTy'} +-- ( TabPi piTy) -> do +-- { TabPi piTy' <- matchit; unify piTy piTy'} +-- ( DictTy d ) -> do +-- { DictTy d' <- matchit; unify d d'} +-- ( NewtypeTyCon con ) -> do +-- { NewtypeTyCon con' <- matchit; unify con con'} +-- ( SumType ts ) -> do +-- { SumType ts' <- matchit; unifyLists ts ts'} +-- ( ProdType ts ) -> do +-- { ProdType ts' <- matchit; unifyLists ts ts'} +-- ( RefType t ) -> do +-- { RefType t' <- matchit; unify t t'} +-- ( DepPairTy t ) -> do +-- { DepPairTy t' <- matchit; unify t t'} +-- where matchit = return t2 + +-- unifyLists :: Unifiable e => [e n] -> [e n] -> SolverM i n () +-- unifyLists [] [] = return () +-- unifyLists (x:xs) (y:ys) = unify x y >> unifyLists xs ys +-- unifyLists _ _ = empty + +-- instance Unifiable DictType where +-- unify d1 d2 = case d1 of +-- ( DictType _ c params )-> do +-- { DictType _ c' params' <- matchit; guard (c == c'); unifyLists params params'} +-- ( IxDictType t ) -> do +-- { IxDictType t' <- matchit; unify t t'} +-- where matchit = return d2 +-- {-# INLINE unify #-} + +-- instance Unifiable NewtypeTyCon where +-- unify e1 e2 = case e1 of +-- ( Nat ) -> do +-- { Nat <- matchit; return ()} +-- ( Fin n ) -> do +-- { Fin n' <- matchit; unify n n'} +-- ( UserADTType _ c params ) -> do +-- { UserADTType _ c' params' <- matchit; guard (c == c') >> unify params params' } +-- where matchit = return e2 + +-- instance Unifiable (IxType) where +-- -- We ignore the dictionaries because we assume coherence +-- unify (IxType t _) (IxType t' _) = unify t t' + +-- instance Unifiable TyConParams where +-- -- We ignore the dictionaries because we assume coherence +-- unify ps ps' = zipWithM_ unify (ignoreSynthParams ps) (ignoreSynthParams ps') + +-- unifyEq :: AlphaEqE e => e n -> e n -> SolverM i n () +-- unifyEq e1 e2 = guard =<< alphaEq e1 e2 +-- {-# INLINE unifyEq #-} + +-- instance Unifiable CorePiType where +-- unify (CorePiType appExpl1 expls1 bsTop1 effTy1) +-- (CorePiType appExpl2 expls2 bsTop2 effTy2) = do +-- unless (appExpl1 == appExpl2) empty +-- unless (expls1 == expls2) empty +-- go (Abs bsTop1 effTy1) (Abs bsTop2 effTy2) +-- where +-- go :: Abs (Nest CBinder) (Type) n +-- -> Abs (Nest CBinder) (Type) n +-- -> SolverM i n () +-- go (Abs Empty t1) (Abs Empty t2) = unify t1 t2 +-- go (Abs (Nest (b1:>t1) bs1) rest1) +-- (Abs (Nest (b2:>t2) bs2) rest2) = do +-- unify t1 t2 +-- void $ withFreshSkolemName t1 \v -> do +-- ab1 <- zonk =<< applyRename (b1@>atomVarName v) (Abs bs1 rest1) +-- ab2 <- zonk =<< applyRename (b2@>atomVarName v) (Abs bs2 rest2) +-- go ab1 ab2 +-- return UnitE +-- go _ _ = empty + +-- instance Unifiable (TabPiType) where +-- unify (TabPiType _ b1 ty1) (TabPiType _ b2 ty2) = +-- unify (Abs b1 ty1) (Abs b2 ty2) + +-- instance Unifiable (DepPairType) where +-- unify (DepPairType expl1 b1 rhs1) (DepPairType expl2 b2 rhs2) = do +-- guard $ expl1 == expl2 +-- unify (Abs b1 rhs1) (Abs b2 rhs2) + +-- instance Unifiable (Abs CBinder CType) where +-- unify (Abs b1 ty1) (Abs b2 ty2) = do +-- let ann1 = binderType b1 +-- let ann2 = binderType b2 +-- unify ann1 ann2 +-- void $ withFreshSkolemName ann1 \v -> do +-- ty1' <- applyRename (b1@>atomVarName v) ty1 +-- ty2' <- applyRename (b2@>atomVarName v) ty2 +-- unify ty1' ty2' +-- return UnitE + +-- withFreshSkolemName +-- :: Zonkable e => CType o +-- -> (forall o'. DExt o o' => CAtomVar o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- withFreshSkolemName ty cont = diffStateT1 \s -> do +-- withFreshBinder "skol" (SkolemBound ty) \b -> do +-- (ans, diff) <- runDiffStateT1 (sink s) do +-- v <- toAtomVar $ binderName b +-- ans <- cont v >>= zonk +-- case hoist b ans of +-- HoistSuccess ans' -> return ans' +-- HoistFailure _ -> empty +-- case hoist b diff of +-- HoistSuccess diff' -> return (ans, diff') +-- HoistFailure _ -> empty +-- {-# INLINE withFreshSkolemName #-} + +-- extendSolution :: CAtomVar n -> CAtom n -> SolverM i n () +-- extendSolution (AtomVar v _) t = +-- isUnificationName v >>= \case +-- True -> do +-- when (v `isFreeIn` t) solverFail -- occurs check +-- -- When we unify under a pi binder we replace its occurrences with a +-- -- skolem variable. We don't want to unify with terms containing these +-- -- variables because that would mean inferring dependence, which is a can +-- -- of worms. +-- forM_ (freeVarsList t) \fv -> +-- whenM (isSkolemName fv) solverFail -- can't unify with skolems +-- addConstraint v t +-- False -> empty + +-- isUnificationName :: EnvReader m => CAtomName n -> m n Bool +-- isUnificationName v = lookupEnv v >>= \case +-- AtomNameBinding (SolverBound (InfVarBound _)) -> return True +-- _ -> return False +-- {-# INLINE isUnificationName #-} + +-- isSolverName :: EnvReader m => CAtomName n -> m n Bool +-- isSolverName v = lookupEnv v >>= \case +-- AtomNameBinding (SolverBound _) -> return True +-- _ -> return False + + +-- isSkolemName :: EnvReader m => CAtomName n -> m n Bool +-- isSkolemName v = lookupEnv v >>= \case +-- AtomNameBinding (SolverBound (SkolemBound _)) -> return True +-- _ -> return False +-- {-# INLINE isSkolemName #-} + +-- renameForPrinting :: EnvReader m +-- => (PairE CAtom CAtom n) -> m n (Abs (Nest (AtomNameBinder)) (PairE CAtom CAtom) n) +-- renameForPrinting e = do +-- infVars <- filterM isSolverName $ freeVarsList e +-- let ab = abstractFreeVarsNoAnn infVars e +-- let hints = take (length infVars) $ map getNameHint $ +-- map (:[]) ['a'..'z'] ++ map show [(0::Int)..] +-- Distinct <- getDistinct +-- scope <- toScope <$> unsafeGetEnv -- TODO: figure out how to do it safely +-- return $ withManyFresh hints scope \bs' -> +-- runScopeReaderM (scope `extendOutMap` toScopeFrag bs') do +-- Abs bsAbs eAbs <- sinkM ab +-- e' <- applyRename (bsAbs@@>nestToNames bs') eAbs +-- return $ Abs bs' e' + +-- -- === builder and type querying helpers === + +-- makeStructRepVal :: (Fallible1 m, EnvReader m) => TyConName n -> [CAtom n] -> m n (CAtom n) +-- makeStructRepVal tyConName args = do +-- TyConDef _ _ _ (StructFields fields) <- lookupTyCon tyConName +-- case fields of +-- [_] -> case args of +-- [arg] -> return arg +-- _ -> error "wrong number of args" +-- _ -> return $ Con $ ProdCon args + +-- -- === dictionary synthesis === + +-- -- Given a simplified dict (an Atom of type `DictTy _` in the +-- -- post-simplification IR), and a requested, more general, dict type, generalize +-- -- the dict to match the more general type. This is only possible because we +-- -- require that instances are polymorphic in data-role parameters. It would be +-- -- valid to implement `generalizeDict` by re-synthesizing the whole dictionary, +-- -- but we know that the derivation tree has to be the same, so we take the +-- -- shortcut of just generalizing the data parameters. +-- generalizeDict :: EnvReader m => CType n -> CDict n -> m n (CDict n) +-- generalizeDict ty dict = do +-- result <- liftEnvReaderM $ liftM fst $ liftInfererMPure $ generalizeDictRec ty dict +-- case result of +-- Failure e -> error $ "Failed to generalize " ++ pprint dict +-- ++ " to " ++ show ty ++ " because " ++ pprint e +-- Success ans -> return ans + +-- generalizeDictRec :: CType n -> CDict n -> InfererM i n (CDict n) +-- generalizeDictRec targetTy (DictCon dict) = case dict of +-- InstanceDict _ instanceName args -> do +-- InstanceDef _ _ bs _ _ <- lookupInstanceDef instanceName +-- liftSolverM $ generalizeInstanceArgs bs args \args' -> do +-- d <- mkInstanceDict (sink instanceName) args' +-- -- We use rootSrcId here because we only call this after type inference so +-- -- precise source info isn't needed. +-- constrainEq rootSrcId (sink $ toAtom targetTy) (toAtom $ getType d) +-- return d +-- IxFin _ -> do +-- TyCon (DictTy (IxDictType (TyCon (NewtypeTyCon (Fin n))))) <- return targetTy +-- return $ DictCon $ IxFin n +-- IxRawFin _ -> error "not a simplified dict" +-- generalizeDictRec _ _ = error "not a simplified dict" + +-- data ParamRole = TypeParam | DictParam | DataParam deriving (Show, Generic, Eq) + +-- inferRoleFromType :: EnvReader m => CType n -> m n ParamRole +-- inferRoleFromType = undefined -- TODO + +-- generalizeInstanceArgs +-- :: Zonkable e => Nest CBinder o any -> [CAtom o] +-- -> (forall o'. DExt o o' => [CAtom o'] -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- generalizeInstanceArgs Empty [] cont = withDistinct $ cont [] +-- generalizeInstanceArgs (Nest (b:>ty) bs) (arg:args) cont = do +-- role <- inferRoleFromType ty +-- generalizeInstanceArg role ty arg \arg' -> do +-- Abs bs' UnitE <- applySubst (b@>SubstVal arg') (Abs bs UnitE) +-- generalizeInstanceArgs bs' (sink <$> args) \args' -> +-- cont $ sink arg' : args' +-- generalizeInstanceArgs _ _ _ = error "zip error" + +-- generalizeInstanceArg +-- :: Zonkable e => ParamRole -> CType o -> CAtom o +-- -> (forall o'. DExt o o' => CAtom o' -> SolverM i o' (e o')) +-- -> SolverM i o (e o) +-- generalizeInstanceArg role ty arg cont = case role of +-- -- XXX: for `TypeParam` we can just emit a fresh inference name rather than +-- -- traversing the whole type like we do in `Generalize.hs`. The reason is +-- -- that it's valid to implement `generalizeDict` by synthesizing an entirely +-- -- fresh dictionary, and if we were to do that, we would infer this type +-- -- parameter exactly as we do here, using inference. +-- TypeParam -> withFreshUnificationVarNoEmits rootSrcId MiscInfVar (toType $ Kind TypeKind) \v -> cont $ toAtom v +-- DictParam -> withFreshDictVarNoEmits ty ( +-- \ty' -> case toMaybeDict (sink arg) of +-- Just d -> liftM toAtom $ lift11 $ generalizeDictRec ty' d +-- _ -> error "not a dict") cont +-- DataParam -> withFreshUnificationVarNoEmits rootSrcId MiscInfVar ty \v -> cont $ toAtom v + +-- emitInstanceDef :: (Mut n, TopBuilder m) => InstanceDef n -> m n (Name n) +-- emitInstanceDef instanceDef@(InstanceDef className _ _ _ _) = do +-- ty <- getInstanceType instanceDef +-- emitBinding (getNameHint className) $ InstanceBinding instanceDef ty + +-- -- main entrypoint to dictionary synthesizer +-- trySynthTerm :: SrcId -> CType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n) +-- trySynthTerm sid ty reqMethodAccess = do +-- hasInferenceVars ty >>= \case +-- True -> throw sid $ CantSynthInfVars $ pprint ty +-- False -> withVoidSubst do +-- synthTy <- liftExcept $ typeAsSynthType sid ty +-- synthTerm sid synthTy reqMethodAccess +-- <|> (throw sid $ CantSynthDict $ pprint ty) +-- {-# SCC trySynthTerm #-} + +-- hasInferenceVars :: (EnvReader m, HoistableE e) => e n -> m n Bool +-- hasInferenceVars e = liftEnvReaderM $ anyInferenceVars $ freeVarsList e +-- {-# INLINE hasInferenceVars #-} + +-- anyInferenceVars :: [CAtomName n] -> EnvReaderM n Bool +-- anyInferenceVars = \case +-- [] -> return False +-- (v:vs) -> isSolverName v >>= \case +-- True -> return True +-- False -> anyInferenceVars vs + +type SynthAtom = CExpr +type SynthPiType n = ([Explicitness], Abs (Nest CBinder) DictType n) +data SynthType n = + SynthDictType (DictType n) + | SynthPiType (SynthPiType n) + deriving (Show, Generic) + +data Givens n = Givens { fromGivens :: HM.HashMap (EKey SynthType n) (SynthAtom n) } + +-- getGivens :: InfererM i o (Givens o) +-- getGivens = givens <$> getInfState + +-- withGivens :: Givens o -> InfererM i o a -> InfererM i o a +-- withGivens givens cont = withInfState (\s -> s { givens = givens }) cont + +-- extendGivens :: [SynthAtom o] -> InfererM i o a -> InfererM i o a +-- extendGivens newGivens cont = do +-- prevGivens <- getGivens +-- finalGivens <- getSuperclassClosure prevGivens newGivens +-- withGivens finalGivens cont +-- {-# INLINE extendGivens #-} + +-- getSynthType :: SynthAtom n -> SynthType n +-- getSynthType x = ignoreExcept $ typeAsSynthType rootSrcId (getType x) +-- {-# INLINE getSynthType #-} + +-- typeAsSynthType :: SrcId -> CType n -> Except (SynthType n) +-- typeAsSynthType sid = \case +-- TyCon (DictTy dictTy) -> return $ SynthDictType dictTy +-- TyCon (Pi (CorePiType ImplicitApp expls bs (TyCon (DictTy d)))) -> +-- return $ SynthPiType (expls, Abs bs d) +-- ty -> Failure $ toErr sid $ NotASynthType $ pprint ty +-- {-# SCC typeAsSynthType #-} + +-- getSuperclassClosure :: EnvReader m => Givens n -> [SynthAtom n] -> m n (Givens n) +-- getSuperclassClosure givens newGivens = do +-- Distinct <- getDistinct +-- env <- unsafeGetEnv +-- return $ getSuperclassClosurePure env givens newGivens +-- {-# INLINE getSuperclassClosure #-} + +-- getSuperclassClosurePure :: Distinct n => Env n -> Givens n -> [SynthAtom n] -> Givens n +-- getSuperclassClosurePure env givens newGivens = +-- snd $ runState (runEnvReaderT env (mapM_ visitGiven newGivens)) givens +-- where +-- visitGiven :: SynthAtom n -> EnvReaderT (State (Givens n)) n () +-- visitGiven x = alreadyVisited x >>= \case +-- True -> return () +-- False -> do +-- markAsVisited x +-- parents <- getDirectSuperclasses x +-- mapM_ visitGiven parents + +-- alreadyVisited :: SynthAtom n -> EnvReaderT (State (Givens n)) n Bool +-- alreadyVisited x = do +-- Givens m <- get +-- ty <- return $ getSynthType x +-- return $ EKey ty `HM.member` m + +-- markAsVisited :: SynthAtom n -> EnvReaderT (State (Givens n)) n () +-- markAsVisited x = do +-- ty <- return $ getSynthType x +-- modify \(Givens m) -> Givens $ HM.insert (EKey ty) x m + +-- getDirectSuperclasses :: SynthAtom n -> EnvReaderT (State (Givens n)) n [SynthAtom n] +-- getDirectSuperclasses synthExpr = do +-- synthTy <- return $ getSynthType synthExpr +-- superclasses <- case synthTy of +-- SynthPiType _ -> return [] +-- SynthDictType dTy -> getSuperclassTys dTy +-- forM (enumerate superclasses) \(i, _) -> do +-- reduceSuperclassProj i $ fromJust (toMaybeDict synthExpr) + +-- synthTerm :: SrcId -> SynthType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n) +-- synthTerm sid targetTy reqMethodAccess = case targetTy of +-- SynthPiType (expls, ab) -> do +-- ab' <- withFreshBindersInf expls ab \bs' targetTy' -> do +-- Abs bs' <$> synthTerm sid (SynthDictType targetTy') reqMethodAccess +-- Abs bs' synthExpr <- return ab' +-- let piTy = CorePiType ImplicitApp expls bs' (getType synthExpr) +-- let lamExpr = LamExpr bs' (Atom synthExpr) +-- return $ toAtom $ Lam $ CoreLamExpr piTy lamExpr +-- SynthDictType dictTy -> case dictTy of +-- IxDictType (TyCon (NewtypeTyCon (Fin n))) -> return $ toAtom $ IxFin n +-- _ -> do +-- dict <- synthDictFromInstance sid dictTy <|> synthDictFromGiven sid dictTy +-- case dict of +-- Con (DictConAtom (InstanceDict _ instanceName _)) -> do +-- isReqMethodAccessAllowed <- reqMethodAccess `isMethodAccessAllowedBy` instanceName +-- if isReqMethodAccessAllowed +-- then return dict +-- else empty +-- _ -> return dict +-- {-# SCC synthTerm #-} + +-- isMethodAccessAllowedBy :: EnvReader m => RequiredMethodAccess -> InstanceName n -> m n Bool +-- isMethodAccessAllowedBy access instanceName = do +-- InstanceDef className _ _ _ (InstanceBody _ methods) <- lookupInstanceDef instanceName +-- let numInstanceMethods = length methods +-- ClassDef _ _ _ _ _ _ _ methodTys <- lookupClassDef className +-- let numClassMethods = length methodTys +-- case access of +-- Full -> return $ numClassMethods == numInstanceMethods +-- Partial numReqMethods -> return $ numReqMethods <= numInstanceMethods + +-- synthDictFromGiven :: SrcId -> DictType n -> InfererM i n (SynthAtom n) +-- synthDictFromGiven sid targetTy = do +-- givens <- ((HM.elems . fromGivens) <$> getGivens) +-- asum $ givens <&> \given -> do +-- case getSynthType given of +-- SynthDictType givenDictTy -> do +-- guard =<< alphaEq targetTy givenDictTy +-- return given +-- SynthPiType givenPiTy -> typeErrAsSearchFailure do +-- args <- instantiateSynthArgs sid targetTy givenPiTy +-- reduceInstantiateGiven given args + +-- synthDictFromInstance :: SrcId -> DictType n -> InfererM i n (SynthAtom n) +-- synthDictFromInstance sid targetTy = do +-- instances <- getInstanceDicts targetTy +-- asum $ instances <&> \candidate -> typeErrAsSearchFailure do +-- CorePiType _ expls bs (TyCon (DictTy candidateTy)) <- lookupInstanceTy candidate +-- args <- instantiateSynthArgs sid targetTy (expls, Abs bs candidateTy) +-- return $ toAtom $ InstanceDict (toType targetTy) candidate args + +-- getInstanceDicts :: EnvReader m => DictType n -> m n [InstanceName n] +-- getInstanceDicts dictTy = do +-- env <- withEnv (envSynthCandidates . moduleEnv) +-- case dictTy of +-- DictType _ name _ -> return $ M.findWithDefault [] name $ instanceDicts env +-- IxDictType _ -> return $ ixInstances env + +-- addInstanceSynthCandidate :: TopBuilder m => ClassName n -> Maybe BuiltinClassName -> InstanceName n -> m n () +-- addInstanceSynthCandidate className maybeBuiltin instanceName = do +-- sc <- return case maybeBuiltin of +-- Nothing -> mempty {instanceDicts = M.singleton className [instanceName] } +-- Just Ix -> mempty {ixInstances = [instanceName]} +-- emitLocalModuleEnv $ mempty {envSynthCandidates = sc} + +-- instantiateSynthArgs :: SrcId -> DictType n -> SynthPiType n -> InfererM i n [CAtom n] +-- instantiateSynthArgs sid target (expls, synthPiTy) = do +-- liftM fromListE $ withReducibleEmissions sid CantReduceDict do +-- bsConstrained <- buildConstraints (sink synthPiTy) \_ resultTy -> do +-- return [TypeConstraint sid (TyCon $ DictTy $ sink target) (TyCon $ DictTy resultTy)] +-- ListE <$> inferMixedArgs sid "dict" expls bsConstrained emptyMixedArgs + +-- emptyMixedArgs :: MixedArgs (CAtom n) +-- emptyMixedArgs = ([], []) + +-- typeErrAsSearchFailure :: InfererM i n a -> InfererM i n a +-- typeErrAsSearchFailure cont = cont `catchErr` \case +-- TypeErr _ _ -> empty +-- e -> throwErr e + +-- instance GenericE Givens where +-- type RepE Givens = HashMapE (EKey SynthType) SynthAtom +-- fromE (Givens m) = HashMapE m +-- {-# INLINE fromE #-} +-- toE (HashMapE m) = Givens m +-- {-# INLINE toE #-} + +-- instance SinkableE Givens where + +-- -- === Inference-specific builder patterns === + +-- type WithExpl = WithAttrB Explicitness + +-- buildBlockInfWithRecon +-- :: HasNamesE e +-- => (forall l. (Emits l, DExt n l) => InfererM i l (e l)) +-- -> InfererM i n (PairE CExpr (ReconAbs e) n) +-- buildBlockInfWithRecon cont = do +-- ab <- buildScoped cont +-- (block, recon) <- liftEnvReaderM $ refreshAbs ab \decls result -> do +-- (newResult, recon) <- telescopicCapture decls result +-- return (Abs decls newResult, recon) +-- block' <- mkBlock block +-- return $ PairE block' recon +-- {-# INLINE buildBlockInfWithRecon #-} + +-- -- === IFunType === + +-- asFFIFunType :: EnvReader m => CType n -> m n (Maybe (IFunType, CorePiType n)) +-- asFFIFunType ty = return do +-- TyCon (Pi piTy) <- return ty +-- impTy <- checkFFIFunTypeM piTy +-- return (impTy, piTy) + +-- checkFFIFunTypeM :: Fallible m => CorePiType n -> m IFunType +-- checkFFIFunTypeM (CorePiType appExpl (_:expls) (Nest b bs) ty) = do +-- argTy <- checkScalar $ binderType b +-- case bs of +-- Empty -> do +-- resultTys <- checkScalarOrPairType ty +-- let cc = case length resultTys of +-- 0 -> error "Not implemented" +-- 1 -> FFICC +-- _ -> FFIMultiResultCC +-- return $ IFunType cc [argTy] resultTys +-- Nest b' rest -> do +-- let naryPiRest = CorePiType appExpl expls (Nest b' rest) ty +-- IFunType cc argTys resultTys <- checkFFIFunTypeM naryPiRest +-- return $ IFunType cc (argTy:argTys) resultTys +-- checkFFIFunTypeM _ = error "expected at least one argument" + +-- checkScalar :: Fallible m => Type n -> m BaseType +-- checkScalar (BaseTy ty) = return ty +-- checkScalar ty = throw rootSrcId $ FFIArgTyNotScalar $ pprint ty + +-- checkScalarOrPairType :: Fallible m => Type n -> m [BaseType] +-- checkScalarOrPairType (PairTy a b) = do +-- tys1 <- checkScalarOrPairType a +-- tys2 <- checkScalarOrPairType b +-- return $ tys1 ++ tys2 +-- checkScalarOrPairType (BaseTy ty) = return [ty] +-- checkScalarOrPairType ty = throw rootSrcId $ FFIResultTyErr $ pprint ty + +-- -- === instances === + +-- instance DiffStateE SolverSubst SolverDiff where +-- updateDiffStateE :: forall n. Distinct n => Env n -> SolverSubst n -> SolverDiff n -> SolverSubst n +-- updateDiffStateE _ initState (SolverDiff (RListE diffs)) = foldl update' initState (unsnoc diffs) +-- where +-- update' :: Distinct n => SolverSubst n -> Solution n -> SolverSubst n +-- update' (SolverSubst subst) (PairE v x) = SolverSubst $ M.insert v x subst + +-- instance SinkableE InfState where sinkingProofE _ = todoSinkableProof + +-- instance GenericE SigmaAtom where +-- type RepE SigmaAtom = EitherE3 (LiftE (Maybe SourceName) `PairE` CAtom) +-- (LiftE SourceName `PairE` CType `PairE` UVar) +-- (CType `PairE` CAtom `PairE` ListE CAtom) +-- fromE = \case +-- SigmaAtom x y -> Case0 $ LiftE x `PairE` y +-- SigmaUVar x y z -> Case1 $ LiftE x `PairE` y `PairE` z +-- SigmaPartialApp x y z -> Case2 $ x `PairE` y `PairE` ListE z +-- {-# INLINE fromE #-} + +-- toE = \case +-- Case0 (LiftE x `PairE` y) -> SigmaAtom x y +-- Case1 (LiftE x `PairE` y `PairE` z) -> SigmaUVar x y z +-- Case2 (x `PairE` y `PairE` ListE z) -> SigmaPartialApp x y z +-- _ -> error "impossible" +-- {-# INLINE toE #-} + +-- instance RenameE SigmaAtom +-- instance HoistableE SigmaAtom +-- instance SinkableE SigmaAtom + +-- instance SubstE AtomSubstVal SigmaAtom where +-- substE env (SigmaAtom sn x) = SigmaAtom sn $ substE env x +-- substE env (SigmaUVar sn ty uvar) = undefined +-- -- UAtomVar v -> substE env $ SigmaAtom (Just sn) $ toAtom (AtomVar v ty) +-- -- UTyConVar v -> SigmaUVar sn ty' $ UTyConVar $ substE env v +-- -- UDataConVar v -> SigmaUVar sn ty' $ UDataConVar $ substE env v +-- -- UPunVar v -> SigmaUVar sn ty' $ UPunVar $ substE env v +-- -- UClassVar v -> SigmaUVar sn ty' $ UClassVar $ substE env v +-- -- UMethodVar v -> SigmaUVar sn ty' $ UMethodVar $ substE env v +-- -- where ty' = substE env ty +-- substE env (SigmaPartialApp ty f xs) = +-- SigmaPartialApp (substE env ty) (substE env f) (map (substE env) xs) + +-- instance PrettyE e => Pretty (UDeclInferenceResult e l) where +-- pretty = \case +-- UDeclResultDone e -> pretty e +-- UDeclResultBindName _ block _ -> pretty block +-- UDeclResultBindPattern _ block _ -> pretty block + +-- instance SinkableE e => SinkableE (UDeclInferenceResult e) where +-- sinkingProofE = todoSinkableProof + +-- instance GenericE SynthType where +-- type RepE SynthType = EitherE2 DictType (PairE (LiftE [Explicitness]) (Abs (Nest CBinder) DictType)) +-- fromE (SynthDictType d) = Case0 d +-- fromE (SynthPiType (expl, t)) = Case1 (PairE (LiftE expl) t) +-- toE (Case0 d) = SynthDictType d +-- toE (Case1 (PairE (LiftE expl) t)) = SynthPiType (expl, t) +-- toE _ = error "impossible" + +-- instance AlphaEqE SynthType +-- instance AlphaHashableE SynthType +-- instance SinkableE SynthType +-- instance HoistableE SynthType +-- instance RenameE SynthType +-- instance SubstE AtomSubstVal SynthType + +-- instance GenericE Constraint where +-- type RepE Constraint = PairE (LiftE SrcId) (PairE CType CType) +-- fromE (TypeConstraint sid t1 t2) = LiftE sid `PairE` PairE t1 t2 +-- {-# INLINE fromE #-} +-- toE (LiftE sid `PairE` PairE t1 t2) = TypeConstraint sid t1 t2 +-- {-# INLINE toE #-} + +-- instance SinkableE Constraint +-- instance HoistableE Constraint +-- instance (SubstE AtomSubstVal) Constraint + +-- instance GenericE RequiredTy where +-- type RepE RequiredTy = EitherE CType UnitE +-- fromE (Check ty) = LeftE ty +-- fromE Infer = RightE UnitE +-- {-# INLINE fromE #-} +-- toE (LeftE ty) = Check ty +-- toE (RightE UnitE) = Infer +-- {-# INLINE toE #-} + +-- instance SinkableE RequiredTy +-- instance HoistableE RequiredTy +-- instance AlphaEqE RequiredTy +-- instance RenameE RequiredTy + +-- instance GenericE PartialType where +-- type RepE PartialType = EitherE PartialPiType CType +-- fromE (PartialType ty) = LeftE ty +-- fromE (FullType ty) = RightE ty +-- {-# INLINE fromE #-} +-- toE (LeftE ty) = PartialType ty +-- toE (RightE ty) = FullType ty +-- {-# INLINE toE #-} + +-- instance SinkableE PartialType +-- instance HoistableE PartialType +-- instance AlphaEqE PartialType +-- instance RenameE PartialType + +-- instance GenericE SolverSubst where +-- -- XXX: this is a bit sketchy because it's not actually bijective... +-- type RepE SolverSubst = ListE (PairE CAtomName CAtom) +-- fromE (SolverSubst m) = ListE $ map (uncurry PairE) $ M.toList m +-- {-# INLINE fromE #-} +-- toE (ListE pairs) = SolverSubst $ M.fromList $ map fromPairE pairs +-- {-# INLINE toE #-} + +-- instance SinkableE SolverSubst where +-- instance RenameE SolverSubst where +-- instance HoistableE SolverSubst + +-- instance GenericE PartialPiType where +-- type RepE PartialPiType = LiftE (AppExplicitness, [Explicitness]) `PairE` Abs (Nest CBinder) RequiredTy +-- fromE (PartialPiType ex exs b ty) = LiftE (ex, exs) `PairE` Abs b ty +-- {-# INLINE fromE #-} +-- toE (LiftE (ex, exs) `PairE` Abs b ty) = PartialPiType ex exs b ty +-- {-# INLINE toE #-} + +-- instance SinkableE PartialPiType +-- instance HoistableE PartialPiType +-- instance AlphaEqE PartialPiType +-- instance RenameE PartialPiType diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs index 4bf8d907f..7d3b5c52b 100644 --- a/src/lib/SourceRename.hs +++ b/src/lib/SourceRename.hs @@ -24,37 +24,9 @@ import Types.Source import Types.Primitives 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, 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 +renameSourceNames :: (Fallible m, TopLogger m) => UTopDecl -> m UTopDecl +renameSourceNames decl = liftRenamer $ sourceRenameTop decl +{-# SCC renameSourceNames #-} data RenamerSubst n = RenamerSubst { renamerSourceMap :: SourceMap n , renamerMayShadow :: Bool } @@ -64,15 +36,12 @@ newtype RenamerM (n::S) (a:: *) = deriving ( Functor, Applicative, Monad, MonadFail, Fallible , ScopeReader, ScopeExtender) -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 +liftRenamer :: (Fallible m, TopLogger m) => RenamerM VoidS a -> m a +liftRenamer cont = do + let m = runScopeReaderT emptyOutMap $ runReaderT1 (RenamerSubst mempty 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 @@ -281,6 +250,20 @@ sourceRenameUBinder (WithSrcB sid ubinder) cont = case ubinder of UBind _ _ -> error "Shouldn't be source-renaming internal names" UIgnore -> cont $ WithSrcB sid $ UIgnore +instance SourceRenamableTop UTopDecl where + sourceRenameTop = \case + UTopLet b ty e -> UTopLet b <$> mapM sourceRenameE ty <*> sourceRenameE e + UTopExpr e -> UTopExpr <$> sourceRenameE e + UStructDecl def b -> UStructDecl <$> sourceRenameTop def <*> pure b + UInterface def b bs -> UInterface <$> sourceRenameTop def <*> pure b <*> pure bs + UInstance def -> UInstance <$> sourceRenameTop def + +instance SourceRenamableTop UInterfaceDef where + sourceRenameTop = undefined + +instance SourceRenamableTop UInstanceDef where + sourceRenameTop = undefined + instance SourceRenamableTop UDataDef where sourceRenameTop (UDataDef tyConName paramBs dataCons) = do sourceRenameB paramBs \paramBs' -> do diff --git a/src/lib/Subst.hs b/src/lib/Subst.hs new file mode 100644 index 000000000..a44d19a6e --- /dev/null +++ b/src/lib/Subst.hs @@ -0,0 +1,510 @@ +-- 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 FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +module Subst where + +import Control.Applicative +import Control.Monad.Identity +import Control.Monad.Reader +import Control.Monad.State.Strict + +import Name +import MTL1 +import Types.Complicated +import qualified RawName as R +import QueryTypePure +import Err + +-- === SubstReader class === + +class (SinkableE v, Monad2 m) => SubstReader (v::E) (m::MonadKind2) | m -> v where + getSubst :: m i o (Subst v i o) + withSubst :: Subst v i' o -> m i' o a -> m i o a + +lookupSubstM :: SubstReader v m => Name i -> m i o (v o) +lookupSubstM name = (!name) <$> getSubst + +dropSubst :: (SubstReader v m, FromName v) => m o o a -> m i o a +dropSubst cont = withSubst idSubst cont +{-# INLINE dropSubst #-} + +withVoidSubst :: (SubstReader v m, FromName v) => m VoidS o a -> m i o a +withVoidSubst cont = withSubst (newSubst absurdNameFunction) cont +{-# INLINE withVoidSubst #-} + +extendSubst :: SubstReader v m => SubstFrag v i i' o -> m i' o a -> m i o a +extendSubst frag cont = do + env <- (<>>frag) <$> getSubst + withSubst env cont +{-# INLINE extendSubst #-} + +-- XXX: this only (monadically) visits each name once, even if a name has +-- multiple occurrences. So don't use it to count occurrences or anything like +-- that! It's not deliberate. It's just an accident of the implementation, where +-- we gather the (de-duplicated) free names and then traverse them. At some +-- point we may add a monadic traversal to `Subst{E,B}`, which would actually +-- visit each occurrence. +-- traverseNames +-- :: forall v e m i o. +-- (SubstE v e, HoistableE e, SinkableE e, FromName v, EnvReader m) +-- => (Name i -> m o (v o)) +-- -> e i -> m o (e o) +-- traverseNames f e = do +-- let vs = freeVarsE e +-- m <- flip R.traverseWithKey (fromNameSet vs) \rawName (SubstItem d _) -> do +-- v' <- f (UnsafeMakeName rawName :: Name i) +-- return $ SubstItem d v' +-- fmapNamesM (applyTraversed m) e +-- {-# INLINE traverseNames #-} + +-- applyTraversed :: FromName v +-- => RawNameMap (SubstItem v n) -> Name i -> v n +-- applyTraversed m = \((UnsafeMakeName v) :: Name i) -> case R.lookup v m of +-- Just item -> fromSubstItem item +-- Nothing -> fromName $ (UnsafeMakeName v :: Name o) + +-- fmapNames :: (SubstE v e, Distinct o) +-- => Env o -> (Name i -> v o) -> e i -> e o +-- fmapNames env f e = substE (env, newSubst f) e +-- {-# INLINE fmapNames #-} + +-- fmapNamesM :: (SubstE v e, SinkableE e, EnvReader m) +-- => (Name i -> v o) +-- -> e i -> m o (e o) +-- fmapNamesM f e = do +-- env <- unsafeGetEnv +-- Distinct <- getDistinct +-- return $ substE (env, newSubst f) e +-- {-# INLINE fmapNamesM #-} + +-- -- === type classes for traversing names === + +-- class FromName v => SubstE (v::E) (e::E) where +-- -- TODO: can't make an alias for these constraints because of impredicativity +-- substE :: Distinct o => (Env o, Subst v i o) -> e i -> e o + +-- default substE :: (GenericE e, SubstE v (RepE e), Distinct o) +-- => (Env o, Subst v i o) -> e i -> e o +-- substE env e = toE $ substE env (fromE e) + +-- class (FromName v, SinkableB b) => SubstB (v::E) (b::B) where +-- substB +-- :: Distinct o +-- => (Env o, Subst v i o) +-- -> b i i' +-- -> (forall o'. Distinct o' => (Env o', Subst v i' o') -> b o o' -> a) +-- -> a + +-- default substB +-- :: (GenericB b, SubstB v (RepB b)) +-- => Distinct o +-- => (Env o, Subst v i o) +-- -> b i i' +-- -> (forall o'. Distinct o' => (Env o', Subst v i' o') -> b o o' -> a) +-- -> a +-- substB env b cont = +-- substB env (fromB b) \env' b' -> +-- cont env' $ toB b' + +-- instance RenameE atom => RenameE (SubstVal atom) where +-- renameE (_, env) (Rename name) = Rename $ env ! name +-- renameE (scope, env) (SubstVal atom) = SubstVal $ renameE (scope, env) atom + +-- substM :: (SubstReader v m, EnvReader2 m, SinkableE e, SubstE v e, FromName v) +-- => e i -> m i o (e o) +-- substM e = do +-- subst <- getSubst +-- substM' subst e +-- {-# INLINE substM #-} + +-- substM' :: (EnvReader m, SinkableE e, SubstE v e, FromName v) +-- => Subst v i o -> e i -> m o (e o) +-- substM' subst e = do +-- case tryApplyIdentitySubst subst e of +-- Just e' -> return $ e' +-- Nothing -> do +-- env <- unsafeGetEnv +-- Distinct <- getDistinct +-- return $ fmapNames env (subst!) e +-- {-# INLINE substM' #-} + +-- fromConstAbs :: (BindsNames b, HoistableE e) => Abs b e n -> HoistExcept (e n) +-- fromConstAbs (Abs b e) = hoist b e + +-- -- === rename-only substitutions === + +-- extendRenamer :: (SubstReader v m, FromName v) => SubstFrag Name i i' o -> m i' o r -> m i o r +-- extendRenamer frag = extendSubst (fmapSubstFrag (const fromName) frag) + +-- extendBinderRename +-- :: (SubstReader v m, FromName v, BindsAtMostOneName b, BindsOneName b') +-- => b i i' -> b' o o' -> m i' o' r -> m i o' r +-- extendBinderRename b b' cont = extendSubst (b@>fromName (binderName b')) cont +-- {-# INLINE extendBinderRename #-} + +-- applyRename +-- :: (ScopeReader m, RenameE e, SinkableE e) +-- => Ext h o => SubstFrag Name h i o -> e i -> m o (e o) +-- applyRename substFrag x = do +-- Distinct <- getDistinct +-- scope <- unsafeGetScope +-- let subst = sink idSubst <>> substFrag +-- case tryApplyIdentitySubst subst x of +-- Just x' -> return x' +-- Nothing -> return $ renameE (scope, newSubst (subst!)) x +-- {-# INLINE applyRename #-} + +-- renameM +-- :: (SubstReader Name m, ScopeReader2 m, SinkableE e, RenameE e) +-- => e i -> m i o (e o) +-- renameM e = do +-- env <- getSubst +-- case tryApplyIdentitySubst env e of +-- Just e' -> return $ e' +-- Nothing -> do +-- WithScope scope env' <- addScope env +-- sinkM $ renameE (scope, newSubst (env'!)) e +-- {-# INLINE renameM #-} + +-- renameBinders +-- :: (EnvExtender2 m, SubstReader Name m, RenameB b, BindsEnv b) +-- => b i i' +-- -> (forall o'. DExt o o' => b o o' -> m i' o' a) +-- -> m i o a +-- renameBinders b cont = do +-- ab <- renameM $ Abs b $ idSubstFrag b +-- refreshAbs ab \b' subst -> extendSubst subst $ cont b' +-- {-# INLINE renameBinders #-} + +-- -- === various convenience utilities === + +-- applySubstFragPure :: (SubstE v e, SinkableE e, SinkableE v, FromName v, Ext h o, Distinct o) +-- => Env o -> SubstFrag v h i o -> e i -> e o +-- applySubstFragPure env substFrag x = do +-- let fullSubst = sink idSubst <>> substFrag +-- applySubstPure env fullSubst x + +-- applySubstPure :: (SubstE v e, SinkableE e, SinkableE v, FromName v, Distinct o) +-- => Env o -> Subst v i o -> e i -> e o +-- applySubstPure env subst x = do +-- case tryApplyIdentitySubst subst x of +-- Just x' -> x' +-- Nothing -> fmapNames env (subst !) x + +-- applySubst :: (EnvReader m, SubstE v e, SinkableE e, SinkableE v, FromName v) +-- => Ext h o +-- => SubstFrag v h i o -> e i -> m o (e o) +-- applySubst substFrag x = do +-- Distinct <- getDistinct +-- env <- unsafeGetEnv +-- return $ applySubstFragPure env substFrag x +-- {-# INLINE applySubst #-} + +-- applyAbs :: ( SinkableE v, SinkableE e +-- , FromName v, EnvReader m, BindsOneName b, SubstE v e) +-- => Abs b e n -> v n -> m n (e n) +-- applyAbs (Abs b body) x = applySubst (b@>x) body +-- {-# INLINE applyAbs #-} + +-- applyNaryAbs :: ( SinkableE v, FromName v, EnvReader m, BindsNameList b, SubstE v e +-- , SubstB v b, SinkableE e) +-- => Abs b e n -> [v n] -> m n (e n) +-- applyNaryAbs (Abs bs body) xs = applySubst (bs @@> xs) body +-- {-# INLINE applyNaryAbs #-} + +-- substBinders +-- :: ( SinkableE v, SubstE v v, EnvExtender2 m, FromName v +-- , SubstReader v m, SubstB v b, RenameE v, RenameB b, BindsEnv b) +-- => b i i' +-- -> (forall o'. DExt o o' => b o o' -> m i' o' a) +-- -> m i o a +-- substBinders b cont = do +-- substBindersFrag b \subst b' -> extendSubst subst $ cont b' +-- {-# INLINE substBinders #-} + +-- substBindersFrag +-- :: ( SinkableE v, SubstE v v, EnvExtender2 m, FromName v +-- , SubstReader v m, SubstB v b, RenameE v, RenameB b, BindsEnv b) +-- => b i i' +-- -> (forall o'. DExt o o' => SubstFrag v i i' o' -> b o o' -> m i o' a) +-- -> m i o a +-- substBindersFrag b cont = do +-- ab <- substM $ Abs b $ idSubstFrag b +-- refreshAbs ab \b' subst -> cont subst b' +-- {-# INLINE substBindersFrag #-} + +-- -- === atom subst vals === + +-- data SubstVal (atom::E) (n::S) = +-- SubstVal (atom n) +-- | Rename (Name n) +-- type AtomSubstVal = SubstVal Atom + +-- instance FromName (SubstVal atom) where +-- fromName = Rename +-- {-# INLINE fromName #-} + +-- class ToSubstVal (v::E) (atom::E) where +-- toSubstVal :: v n -> SubstVal atom n + +-- instance ToSubstVal (Name::E) (atom::E) where +-- toSubstVal = Rename + +-- instance ToSubstVal (SubstVal atom) atom where +-- toSubstVal = id + +-- type AtomSubstReader v m = (SubstReader v m, FromName v, ToSubstVal v Atom) + +-- toAtomVar :: EnvReader m => AtomName n -> m n (AtomVar n) +-- toAtomVar v = do +-- ty <- getType <$> lookupAtomName v +-- return $ AtomVar v ty + +-- lookupAtomSubst :: (SubstReader AtomSubstVal m, EnvReader2 m) => AtomName i -> m i o (Atom o) +-- lookupAtomSubst v = do +-- lookupSubstM v >>= \case +-- Rename v' -> toAtom <$> toAtomVar v' +-- SubstVal x -> return x + +-- atomSubstM :: (AtomSubstReader v m, EnvReader2 m, SinkableE e, SubstE AtomSubstVal e) +-- => e i -> m i o (e o) +-- atomSubstM e = do +-- subst <- getSubst +-- let subst' = asAtomSubstValSubst subst +-- substM' subst' e + +-- asAtomSubstValSubst :: ToSubstVal v Atom => Subst v i o -> Subst AtomSubstVal i o +-- asAtomSubstValSubst subst = newSubst \v -> toSubstVal (subst ! v) + +-- === SubstReaderT transformer === + +newtype SubstReaderT (v::E) (m::MonadKind1) (i::S) (o::S) (a:: *) = + SubstReaderT' { runSubstReaderT' :: ReaderT (Subst v i o) (m o) a } + +pattern SubstReaderT :: (Subst v i o -> m o a) -> SubstReaderT v m i o a +pattern SubstReaderT f = SubstReaderT' (ReaderT f) + +runSubstReaderT :: Subst v i o -> SubstReaderT v m i o a -> m o a +runSubstReaderT env m = runReaderT (runSubstReaderT' m) env +{-# INLINE runSubstReaderT #-} + +instance (forall n. Functor (m n)) => Functor (SubstReaderT v m i o) where + fmap f (SubstReaderT' m) = SubstReaderT' $ fmap f m + {-# INLINE fmap #-} + +instance Monad1 m => Applicative (SubstReaderT v m i o) where + pure = SubstReaderT' . pure + {-# INLINE pure #-} + liftA2 f (SubstReaderT' x) (SubstReaderT' y) = SubstReaderT' $ liftA2 f x y + {-# INLINE liftA2 #-} + (SubstReaderT' f) <*> (SubstReaderT' x) = SubstReaderT' $ f <*> x + {-# INLINE (<*>) #-} + +instance (forall n. Monad (m n)) => Monad (SubstReaderT v m i o) where + return = SubstReaderT' . return + {-# INLINE return #-} + (SubstReaderT' m) >>= f = SubstReaderT' (m >>= (runSubstReaderT' . f)) + {-# INLINE (>>=) #-} + +deriving instance (Monad1 m, MonadFail1 m) => MonadFail (SubstReaderT v m i o) +deriving instance (Monad1 m, Alternative1 m) => Alternative (SubstReaderT v m i o) +deriving instance Fallible1 m => Fallible (SubstReaderT v m i o) +deriving instance Catchable1 m => Catchable (SubstReaderT v m i o) + +type ScopedSubstReader (v::E) = SubstReaderT v (ScopeReaderT Identity) :: MonadKind2 + +liftSubstReaderT :: Monad1 m => m o a -> SubstReaderT v m i o a +liftSubstReaderT m = SubstReaderT' $ lift m +{-# INLINE liftSubstReaderT #-} + +runScopedSubstReader :: Distinct o => Scope o -> Subst v i o + -> ScopedSubstReader v i o a -> a +runScopedSubstReader scope env m = + runIdentity $ runScopeReaderT scope $ runSubstReaderT env m +{-# INLINE runScopedSubstReader #-} + +withSubstReaderT :: FromName v => SubstReaderT v m n n a -> m n a +withSubstReaderT = runSubstReaderT idSubst +{-# INLINE withSubstReaderT #-} + +instance (SinkableE v, Monad1 m) => SubstReader v (SubstReaderT v m) where + getSubst = SubstReaderT' ask + {-# INLINE getSubst #-} + withSubst env (SubstReaderT' cont) = SubstReaderT' $ withReaderT (const env) cont + {-# INLINE withSubst #-} + +instance (SinkableE v, ScopeReader m) => ScopeReader (SubstReaderT v m i) where + unsafeGetScope = liftSubstReaderT unsafeGetScope + {-# INLINE unsafeGetScope #-} + getDistinct = liftSubstReaderT getDistinct + {-# INLINE getDistinct #-} + +-- instance (SinkableE v, EnvReader m) => EnvReader (SubstReaderT v m i) where +-- unsafeGetEnv = liftSubstReaderT unsafeGetEnv +-- {-# INLINE unsafeGetEnv #-} + +-- instance (SinkableE v, ScopeReader m, EnvExtender m) +-- => EnvExtender (SubstReaderT v m i) where +-- refreshAbs ab cont = SubstReaderT \subst -> +-- refreshAbs ab \b e -> do +-- subst' <- sinkM subst +-- let SubstReaderT cont' = cont b e +-- cont' subst' +-- {-# INLINE refreshAbs #-} + +-- instance MonadDiffState1 m s d => MonadDiffState1 (SubstReaderT v m i) s d where +-- withDiffState s m = +-- SubstReaderT \subst -> do +-- withDiffState s $ runSubstReaderT subst m + +-- updateDiffStateM d = liftSubstReaderT $ updateDiffStateM d +-- getDiffState = liftSubstReaderT getDiffState + +-- type SubstEnvReaderM v = SubstReaderT v EnvReaderM :: MonadKind2 + +-- liftSubstEnvReaderM +-- :: forall v m n a. (EnvReader m, FromName v) +-- => SubstEnvReaderM v n n a +-- -> m n a +-- liftSubstEnvReaderM cont = liftEnvReaderM $ runSubstReaderT idSubst $ cont +-- {-# INLINE liftSubstEnvReaderM #-} + +instance (SinkableE v, ScopeReader m, ScopeExtender m) + => ScopeExtender (SubstReaderT v m i) where + refreshAbsScope ab cont = SubstReaderT \env -> + refreshAbsScope ab \b e -> do + let SubstReaderT cont' = cont b e + env' <- sinkM env + cont' env' + +instance (SinkableE v, MonadIO1 m) => MonadIO (SubstReaderT v m i o) where + liftIO m = liftSubstReaderT $ liftIO m + {-# INLINE liftIO #-} + +instance (Monad1 m, MonadState (s o) (m o)) => MonadState (s o) (SubstReaderT v m i o) where + state = liftSubstReaderT . state + {-# INLINE state #-} + +instance (Monad1 m, MonadReader (r o) (m o)) => MonadReader (r o) (SubstReaderT v m i o) where + ask = SubstReaderT $ const ask + {-# INLINE ask #-} + local r (SubstReaderT' (ReaderT f)) = SubstReaderT \env -> local r $ f env + {-# INLINE local #-} + +-- -- === instances === + +-- instance SinkableE atom => SinkableE (SubstVal atom) where +-- sinkingProofE fresh substVal = case substVal of +-- Rename name -> Rename $ sinkingProofE fresh name +-- SubstVal val -> SubstVal $ sinkingProofE fresh val + +-- instance (SubstB v b, SubstE v e) => SubstE v (Abs b e) where +-- substE env (Abs b body) = do +-- substB env b \env' b' -> Abs b' $ substE env' body + +-- instance ( BindsNames b1, SubstB v b1 +-- , BindsNames b2, SubstB v b2 +-- , SinkableE v, FromName v) +-- => SubstB v (PairB b1 b2) where +-- substB env (PairB b1 b2) cont = +-- substB env b1 \env' b1' -> +-- substB env' b2 \env'' b2' -> +-- cont env'' $ PairB b1' b2' + +-- instance (SinkableE e, SubstE v e) => SubstB v (LiftB e) where +-- substB env@(_, subst) (LiftB e) cont = case tryApplyIdentitySubst subst e of +-- Just e' -> cont env $ LiftB e' +-- Nothing -> cont env $ LiftB $ substE env e +-- {-# INLINE substB #-} + +-- instance (SubstB v b1, SubstB v b2) => SubstB v (EitherB b1 b2) where +-- substB env (LeftB b) cont = +-- substB env b \env' b' -> +-- cont env' $ LeftB b' +-- substB env (RightB b) cont = +-- substB env b \env' b' -> +-- cont env' $ RightB b' + +-- instance (SinkableE ann, SubstE v ann, SinkableE v, ToBinding ann) +-- => SubstB v (BinderP ann) where +-- substB (env, subst) (b:>ty) cont = do +-- let ty' = substE (env, subst) ty +-- withFresh (getNameHint b) (toScope env) \bRaw -> do +-- let b' = bRaw:>ty' +-- let env' = env `extendOutMap` toEnvFrag b' +-- let UnsafeMakeName bn = binderName b +-- let UnsafeMakeName bn' = binderName b' +-- let subst' = case subst of +-- UnsafeMakeIdentitySubst | bn == bn' -> UnsafeMakeIdentitySubst +-- _ -> sink subst <>> b @> (fromName $ binderName b') +-- cont (env', subst') b' + +-- instance (BindsNames b, SubstB v b, SinkableE v) => SubstB v (Nest b) where +-- substB env (Nest b bs) cont = +-- substB env b \env' b' -> +-- substB env' bs \env'' bs' -> +-- cont env'' $ Nest b' bs' +-- substB env Empty cont = cont env Empty + +-- instance FromName v => SubstE v UnitE where +-- substE _ UnitE = UnitE + +-- instance SubstB v b => SubstB v (WithAttrB a b) where +-- substB env (WithAttrB x b) cont = +-- substB env b \env' b' -> cont env' $ WithAttrB x b' + +-- instance (Traversable f, SubstE v e) => SubstE v (ComposeE f e) where +-- substE env (ComposeE xs) = ComposeE $ fmap (substE env) xs + +-- instance (SubstE v e1, SubstE v e2) => SubstE v (PairE e1 e2) where +-- substE env (PairE x y) = PairE (substE env x) (substE env y) + +-- instance (SubstE v e1, SubstE v e2) => SubstE v (EitherE e1 e2) where +-- substE env (LeftE x) = LeftE $ substE env x +-- substE env (RightE x) = RightE $ substE env x + +-- instance FromName v => SubstE v VoidE where +-- substE _ _ = error "impossible" + +-- instance FromName v => SubstE v (LiftE a) where +-- substE _ (LiftE x) = LiftE x + +-- instance SubstE v e => SubstE v (ListE e) where +-- substE env (ListE xs) = ListE $ map (substE env) xs + +-- instance SubstE v e => SubstE v (RListE e) where +-- substE env (RListE xs) = RListE $ fmap (substE env) xs + +-- instance SubstE v e => SubstE v (NonEmptyListE e) where +-- substE env (NonEmptyListE xs) = NonEmptyListE $ fmap (substE env) xs + +-- instance SubstE substVal v => SubstE substVal (SubstFrag v i i') where +-- substE env frag = fmapSubstFrag (\_ val -> substE env val) frag + +-- instance SubstE substVal v => SubstE substVal (Subst v i) where +-- substE env = \case +-- Subst f frag -> Subst (\n -> substE env (f n)) $ substE env frag +-- UnsafeMakeIdentitySubst +-- -> Subst (\n -> substE env (fromName $ unsafeCoerceE n)) emptyInFrag + +-- instance (SubstE v e0, SubstE v e1, SubstE v e2, +-- SubstE v e3, SubstE v e4, SubstE v e5, +-- SubstE v e6, SubstE v e7) +-- => SubstE v (EitherE8 e0 e1 e2 e3 e4 e5 e6 e7) where +-- substE env = \case +-- Case0 e -> Case0 $ substE env e +-- Case1 e -> Case1 $ substE env e +-- Case2 e -> Case2 $ substE env e +-- Case3 e -> Case3 $ substE env e +-- Case4 e -> Case4 $ substE env e +-- Case5 e -> Case5 $ substE env e +-- Case6 e -> Case6 $ substE env e +-- Case7 e -> Case7 $ substE env e +-- {-# INLINE substE #-} diff --git a/src/lib/TopLevel2.hs b/src/lib/TopLevel2.hs index d283f9a89..e657b8b8e 100644 --- a/src/lib/TopLevel2.hs +++ b/src/lib/TopLevel2.hs @@ -7,7 +7,7 @@ {-# LANGUAGE UndecidableInstances #-} module TopLevel2 ( - EvalConfig (..), Topper, TopperM, runTopperM, + EvalConfig (..), TopperM, runTopperM, evalSourceBlockRepl, OptLevel (..), LibPath (..), evalSourceBlockIO, initTopState, simpOptimizations, ExitStatus (..), parseSourceBlocks, captureLogs) where @@ -41,6 +41,7 @@ import qualified LLVM.AST import AbstractSyntax import ConcreteSyntax import Err +import Inference import MonadUtil import Paths_dex (getDataFileName) import SourceRename @@ -69,20 +70,10 @@ 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 } + , topperLogAction :: LogAction + , topperTopState :: IORef TopState } newtype TopperM a = TopperM { runTopperM' @@ -94,23 +85,14 @@ 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 +runTopperM cfg logAction initState cont = do + stateRef <- newIORef initState + result <- flip runReaderT (TopperReaderData cfg logAction stateRef) $ runTopperM' cont + finalState <- readIORef stateRef + return (result, finalState) initTopState :: IO TopState -initTopState = undefined - -- dyvarStores <- allocateDynamicVarKeyPtrs - -- return $ TopState emptyOutMap dyvarStores +initTopState = return TopState captureLogs :: (LogAction -> IO a) -> IO (a, Outputs) captureLogs cont = do @@ -133,14 +115,16 @@ 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 :: SourceBlock -> TopperM 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 + maybeErr <- catchErrExcept do + logTop $ SourceInfo $ SIGroupingInfo $ getGroupingInfo $ sbContents block + evalSourceBlock' Main block case maybeErr of Success () -> return ExitSuccess Failure e -> do @@ -151,7 +135,7 @@ evalSourceBlockRepl block = do -- (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 -> TopperM () ensureModuleLoaded moduleSourceName = undefined -- ensureModuleLoaded moduleSourceName = do -- -- TODO: think about where import errors should be handled @@ -161,24 +145,9 @@ ensureModuleLoaded moduleSourceName = undefined -- 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' :: ModuleSourceName -> SourceBlock -> TopperM () evalSourceBlock' mname block = case sbContents block of - TopDecl decl -> parseDecl decl >>= execUDecl (makeTopNameDescription mname block) + TopDecl decl -> parseDecl decl >>= execUDecl UnParseable _ s -> throwErr $ ParseErr $ MiscParseErr s Misc m -> case m of ImportModule moduleName -> undefined -- importModule moduleName @@ -279,7 +248,7 @@ evalSourceBlock' mname block = case sbContents block of -- let evaluatedModule = Module name directDeps transDeps sm scs -- emitEnv $ Abs fragToReEmit evaluatedModule -dropSourceInfoLogging :: Topper m => m a -> m a +dropSourceInfoLogging :: TopperM a -> TopperM a dropSourceInfoLogging cont = do (ans, Outputs logs) <- captureIOLogs cont let logs' = filter isNotSourceInfo logs @@ -341,7 +310,7 @@ dropSourceInfoLogging cont = do -- evalBlock _ = error "not a top block" -- {-# SCC evalBlock #-} -simpOptimizations :: Topper m => STopLam -> m STopLam +simpOptimizations :: STopLam -> TopperM STopLam simpOptimizations simp = undefined -- simpOptimizations simp = do -- analyzed <- whenOpt simp $ checkPass OccAnalysisPass . analyzeOccurrences @@ -350,37 +319,38 @@ simpOptimizations simp = undefined -- 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' +execUDecl :: UTopDecl -> TopperM () +execUDecl decl = do + logPass Parse decl + renamed <- renameSourceNames decl + logPass RenamePass renamed + typedDecl <- checkPass TypePass $ inferTopUDecl renamed + + undefined + -- 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 :: Pretty e => PassName -> TopperM e -> TopperM e checkPass name cont = do result <- cont logPass name result @@ -396,7 +366,7 @@ logDebug m = getLogLevel >>= \case x <- m emitLog $ Outputs [x] -logPass :: Topper m => Pretty a => PassName -> a -> m () +logPass :: Pretty a => PassName -> a -> TopperM () logPass passName result = do getLogLevel >>= \case NormalLogLevel -> logTop $ PassResult passName Nothing @@ -408,8 +378,6 @@ logPass passName result = do instance ConfigReader TopperM where getConfig = TopperM $ asks topperEvalConfig -instance Topper TopperM - instance Logger Outputs TopperM where emitLog x = do logger <- getIOLogAction diff --git a/src/lib/Types/Complicated.hs b/src/lib/Types/Complicated.hs index 3e0f02dfb..a9fc439e2 100644 --- a/src/lib/Types/Complicated.hs +++ b/src/lib/Types/Complicated.hs @@ -55,6 +55,24 @@ type CType = CExpr type CBinder = BinderP CType :: B +type TopBinder = SourceName + +data CTopDecl = + CTopLet TopBinder (CExpr VoidS) + | CTopExpr (CExpr VoidS) + -- | CDataDefDecl + -- DataDef + -- TopBinder -- type constructor name + -- [TopBinder] -- data constructor names + -- | CStructDecl + -- UStructDef + -- TopBinder -- type constructor name + | CInterface + (ClassDef VoidS) + TopBinder -- class name + [TopBinder] -- method names + | CInstance (InstanceDef VoidS) + data CDecl (n::S) (l::S) = CLet (NameBinder n l) (CExpr n) deriving (Show, Generic) type CBlock = Abs (Nest CDecl) CExpr @@ -356,3 +374,6 @@ instance AlphaHashableB CDecl instance ProvesExt CDecl instance BindsNames CDecl instance Store (CDecl n l) + +instance Pretty CTopDecl where + pretty = undefined diff --git a/src/lib/Types/Primitives.hs b/src/lib/Types/Primitives.hs index 07d406d2d..53cc43149 100644 --- a/src/lib/Types/Primitives.hs +++ b/src/lib/Types/Primitives.hs @@ -137,7 +137,6 @@ data TopName = TopGenName TopNameHint Int deriving (Show, Eq, Ord, Generic) instance Hashable TopName instance Store TopName -type TopBinder = TopName newtype SourceName = MkSourceName String deriving (Show, Eq, Ord, Generic) diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs index c9b748c8d..e4058b657 100644 --- a/src/lib/Types/Source.hs +++ b/src/lib/Types/Source.hs @@ -130,6 +130,7 @@ data TypeInfo = -- === Results === +type TopLogger = Logger Outputs type TopLogger1 (m::MonadKind1) = forall n. Logger Outputs (m n) type LitProg = [(SourceBlock, Outputs)] @@ -274,6 +275,8 @@ data CSBlock = type UVar = Name +type TopBinder = WithSrc SourceName + type UBinder = WithSrcB UBinder' data UBinder' (n::S) (l::S) where -- Only appears before renaming pass @@ -499,6 +502,9 @@ instance FromSourceNameW (UAnnBinder VoidS VoidS) where instance FromSourceNameW (UExpr' VoidS) where fromSourceNameW = UVar . fromSourceNameW +instance FromSourceNameW TopBinder where + fromSourceNameW x = x + instance FromSourceNameW (a n) => FromSourceNameW (WithSrcE a n) where fromSourceNameW x = WithSrcE (srcPos x) $ fromSourceNameW x diff --git a/src/old/Inference.hs b/src/old/Inference.hs deleted file mode 100644 index 432010293..000000000 --- a/src/old/Inference.hs +++ /dev/null @@ -1,2299 +0,0 @@ --- Copyright 2021 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 #-} -{-# OPTIONS_GHC -Wno-orphans #-} - -module Inference - ( inferTopUDecl, checkTopUType, inferTopUExpr , generalizeDict, asTopBlock - , UDeclInferenceResult (..), asFFIFunType, ParamRole (..), inferRoleFromType) where - -import Prelude hiding ((.), id) -import Control.Category -import Control.Applicative -import Control.Monad -import Control.Monad.State.Strict -import Control.Monad.Reader -import Data.Either (partitionEithers) -import Data.Foldable (asum) -import Data.Functor ((<&>)) -import Data.List (sortOn) -import Data.Maybe (fromJust, fromMaybe, catMaybes) -import Data.Word -import qualified Data.HashMap.Strict as HM -import qualified Data.Map.Strict as M -import GHC.Generics (Generic (..)) - -import Builder -import CheapReduction --- import CheckType -import Core -import Err -import MonadUtil -import MTL1 -import Name -import Subst -import PPrint -import QueryType -import Types.Core -import Types.Imp -import Types.Primitives -import qualified Types.Source as S -import Types.Source hiding (ConName (..), TCName (..)) -import Types.Top -import Util hiding (group) - --- === Top-level interface === - -checkTopUType :: (Fallible1 m, TopLogger1 m, EnvReader m) => UType n -> m n (CType n) -checkTopUType ty = liftInfererM $ checkUType ty -{-# SCC checkTopUType #-} - -inferTopUExpr :: (Fallible1 m, TopLogger1 m, EnvReader m) => UExpr n -> m n (TopBlock n) -inferTopUExpr e = fst <$> (asTopBlock =<< liftInfererM (buildBlock $ bottomUp e)) -{-# SCC inferTopUExpr #-} - -data UDeclInferenceResult e n = - UDeclResultDone (e n) -- used for UDataDefDecl, UInterface and UInstance - | UDeclResultBindName LetAnn (TopBlock n) (Abs UBinder e n) - | UDeclResultBindPattern NameHint (TopBlock n) (ReconAbs e n) - -inferTopUDecl :: (Mut n, Fallible1 m, TopBuilder m, HasNamesE e, TopLogger1 m) - => UTopDecl n l -> e l -> m n (UDeclInferenceResult e n) -inferTopUDecl (UStructDecl tc def) result = do - tc' <- emitBinding (getNameHint tc) $ TyConBinding Nothing (DotMethods mempty) - def' <- liftInfererM $ extendRenamer (tc@>tc') $ inferStructDef def - updateTopEnv $ UpdateTyConDef tc' def' - UStructDef _ paramBs _ methods <- return def - forM_ methods \(letAnn, methodName, methodDef) -> do - method <- liftInfererM $ extendRenamer (tc@>tc') $ - inferDotMethod tc' (Abs paramBs methodDef) - method' <- emitTopLet (getNameHint methodName) letAnn (Atom $ toAtom $ Lam method) - updateTopEnv $ UpdateFieldDef tc' methodName (atomVarName method') - UDeclResultDone <$> applyRename (tc @> tc') result -inferTopUDecl (UDataDefDecl def tc dcs) result = do - tcDef@(TyConDef _ _ _ (ADTCons dataCons)) <- liftInfererM $ inferTyConDef def - tc' <- emitBinding (getNameHint tcDef) $ TyConBinding (Just tcDef) (DotMethods mempty) - dcs' <- forM (enumerate dataCons) \(i, dcDef) -> - emitBinding (getNameHint dcDef) $ DataConBinding tc' i - let subst = tc @> tc' <.> dcs @@> dcs' - UDeclResultDone <$> applyRename subst result -inferTopUDecl (UInterface paramBs methodTys className methodNames) result = do - let sn = getSourceName className - let methodSourceNames = nestToList getSourceName methodNames - classDef <- liftInfererM $ inferClassDef sn methodSourceNames paramBs methodTys - className' <- emitBinding (getNameHint sn) $ ClassBinding classDef - methodNames' <- forM (enumerate methodSourceNames) \(i, prettyName) -> do - emitBinding (getNameHint prettyName) $ MethodBinding className' i - let subst = className @> className' <.> methodNames @@> methodNames' - UDeclResultDone <$> applyRename subst result -inferTopUDecl (UInstance className bs params methods maybeName expl) result = do - let (InternalName _ _ className') = className - def <- liftInfererM $ withUBinders bs \(ZipB roleExpls bs') -> do - ClassDef _ _ _ _ _ paramBinders _ _ <- lookupClassDef (sink className') - params' <- checkInstanceParams paramBinders params - body <- checkInstanceBody (sink className') params' methods - return $ InstanceDef className' roleExpls bs' params' body - UDeclResultDone <$> case maybeName of - RightB UnitB -> do - instanceName <- emitInstanceDef def - ClassDef _ builtinName _ _ _ _ _ _ <- lookupClassDef className' - addInstanceSynthCandidate className' builtinName instanceName - return result - JustB instanceName' -> do - instanceName <- emitInstanceDef def - lam <- instanceFun instanceName expl - instanceAtomName <- emitTopLet (getNameHint instanceName') PlainLet $ Atom lam - applyRename (instanceName' @> atomVarName instanceAtomName) result - _ -> error "impossible" -inferTopUDecl (ULocalDecl (WithSrcB _ decl)) result = case decl of - UPass -> return $ UDeclResultDone result - UExprDecl _ -> error "Shouldn't have this at the top level (should have become a command instead)" - ULet letAnn p tyAnn rhs -> case p of - WithSrcB _ (UPatBinder b) -> do - block <- liftInfererM $ buildBlock do - checkMaybeAnnExpr tyAnn rhs - (topBlock, resultTy) <- asTopBlock block - let letAnn' = considerInlineAnn letAnn resultTy - return $ UDeclResultBindName letAnn' topBlock (Abs b result) - _ -> do - PairE block recon <- liftInfererM $ buildBlockInfWithRecon do - val <- checkMaybeAnnExpr tyAnn rhs - v <- emitDecl (getNameHint p) PlainLet $ Atom val - bindLetPat p v do - renameM result - (topBlock, _) <- asTopBlock block - return $ UDeclResultBindPattern (getNameHint p) topBlock recon -{-# SCC inferTopUDecl #-} - -asTopBlock :: EnvReader m => CExpr n -> m n (TopBlock n, CType n) -asTopBlock block = do - let ty = getType block - return (TopLam False (PiType Empty ty) (LamExpr Empty block), ty) - -getInstanceType :: EnvReader m => InstanceDef n -> m n (CorePiType n) -getInstanceType (InstanceDef className expls bs params _) = liftEnvReaderM do - refreshAbs (Abs bs (ListE params)) \bs' (ListE params') -> do - className' <- sinkM className - dTy <- toType <$> dictType className' params' - return $ CorePiType ImplicitApp expls bs' dTy - --- === Inferer monad === - -newtype SolverSubst n = SolverSubst { fromSolverSubst :: M.Map (CAtomName n) (CAtom n) } - -emptySolverSubst :: SolverSubst n -emptySolverSubst = SolverSubst mempty - -data InfState (n::S) = InfState - { givens :: Givens n } - -newtype InfererM (i::S) (o::S) (a:: *) = InfererM - { runInfererM' :: SubstReaderT Name (ReaderT1 InfState (BuilderT (ExceptT (State TypingInfo)))) i o a } - deriving (Functor, Applicative, Monad, MonadFail, Alternative, Builder, - EnvExtender, ScopableBuilder, - ScopeReader, EnvReader, Fallible, Catchable, SubstReader Name) - -type InfererCPSB b i o a = (forall o'. DExt o o' => b o o' -> InfererM i o' a) -> InfererM i o a -type InfererCPSB2 b i i' o a = (forall o'. DExt o o' => b o o' -> InfererM i' o' a) -> InfererM i o a - -liftInfererM :: (EnvReader m, TopLogger1 m, Fallible1 m) => InfererM n n a -> m n a -liftInfererM cont = do - (ansExcept, typeInfo) <- liftInfererMPure cont - emitLog $ Outputs [SourceInfo $ SITypingInfo typeInfo] - liftExcept ansExcept -{-# INLINE liftInfererM #-} - -liftInfererMPure :: EnvReader m => InfererM n n a -> m n (Except a, TypingInfo) -liftInfererMPure cont = do - ansM <- liftBuilderT $ runReaderT1 emptyInfState $ runSubstReaderT idSubst $ runInfererM' cont - return $ runState (runExceptT ansM) mempty - where - emptyInfState :: InfState n - emptyInfState = InfState (Givens HM.empty) -{-# INLINE liftInfererMPure #-} - --- === Solver monad === - -type Solution = PairE CAtomName CAtom -newtype SolverDiff (n::S) = SolverDiff (RListE Solution n) - deriving (MonoidE, SinkableE, HoistableE, RenameE) -type SolverM i o a = DiffStateT1 SolverSubst SolverDiff (InfererM i) o a - -type Zonkable e = (HasNamesE e, SubstE AtomSubstVal e) - -liftSolverM :: SolverM i o a -> InfererM i o a -liftSolverM cont = fst <$> runDiffStateT1 emptySolverSubst cont - -solverFail :: SolverM i o a -solverFail = empty - -zonk :: Zonkable e => e n -> SolverM i n (e n) -zonk e = do - s <- getDiffState - applySolverSubst s e -{-# INLINE zonk #-} - -zonkStuck :: CStuck n -> SolverM i n (CAtom n) -zonkStuck stuck = do - solverSubst <- getDiffState - Distinct <- getDistinct - env <- unsafeGetEnv - let subst = newSubst (lookupSolverSubst solverSubst) - return $ substStuck (env, subst) stuck - -applySolverSubst :: (EnvReader m, Zonkable e) => SolverSubst n -> e n -> m n (e n) -applySolverSubst subst e = do - Distinct <- getDistinct - env <- unsafeGetEnv - return $ fmapNames env (lookupSolverSubst subst) e -{-# INLINE applySolverSubst #-} - -withFreshBinderInf :: NameHint -> Explicitness -> CType o -> InfererCPSB CBinder i o a -withFreshBinderInf hint expl ty cont = - withFreshBinder hint ty \b -> do - givens <- case expl of - Inferred _ (Synth _) -> return [toAtom $ binderVar b] - _ -> return [] - extendGivens givens $ cont b -{-# INLINE withFreshBinderInf #-} - -withFreshBindersInf - :: (SinkableE e, RenameE e) - => [Explicitness] -> Abs (Nest CBinder) e o - -> (forall o'. DExt o o' => Nest CBinder o o' -> e o' -> InfererM i o' a) - -> InfererM i o a -withFreshBindersInf explsTop (Abs bsTop e) contTop = - runSubstReaderT idSubst $ go explsTop bsTop \bs' -> do - e' <- renameM e - liftSubstReaderT $ contTop bs' e' - where - go :: [Explicitness] -> Nest CBinder ii ii' - -> (forall o'. DExt o o' => Nest CBinder o o' -> SubstReaderT Name (InfererM i) ii' o' a) - -> SubstReaderT Name (InfererM i) ii o a - go [] Empty cont = withDistinct $ cont Empty - go (expl:expls) (Nest b bs) cont = do - ty <- renameM $ binderType b - SubstReaderT \s -> withFreshBinderInf (getNameHint b) expl ty \b' -> do - runSubstReaderT (sink s) $ extendSubst (b@>binderName b') do - go expls bs \bs' -> cont (Nest b' bs') - go _ _ _ = error "zip error" -{-# INLINE withFreshBindersInf #-} - -withInferenceVar - :: (Zonkable e, Emits o, ToBinding binding) => NameHint -> binding o - -> (forall o'. (Emits o', DExt o o') => CAtomName o' -> SolverM i o' (e o', CAtom o')) - -> SolverM i o (e o) -withInferenceVar hint binding cont = diffStateT1 \s -> do - declsAndAns <- withFreshBinder hint binding \(b:>_) -> do - hardHoist b <$> buildScoped do - v <- sinkM $ binderName b - s' <- sinkM s - (PairE ans soln, diff) <- runDiffStateT1 s' do - toPairE <$> cont v - let subst = SolverSubst $ M.singleton v soln - ans' <- applySolverSubst subst ans - diff' <- applySolutionToDiff subst v diff - return $ PairE ans' diff' - fromPairE <$> emitDecls declsAndAns - where - applySolutionToDiff :: SolverSubst n -> CAtomName n -> SolverDiff n -> InfererM i n (SolverDiff n) - applySolutionToDiff subst vSoln (SolverDiff (RListE (ReversedList cs))) = do - SolverDiff . RListE . ReversedList <$> forMFilter cs \(PairE v x) -> - case v == vSoln of - True -> return Nothing - False -> Just . PairE v <$> applySolverSubst subst x -{-# INLINE withInferenceVar #-} - -withFreshUnificationVar - :: (Zonkable e, Emits o) => SrcId -> InfVarDesc -> CType o - -> (forall o'. (Emits o', DExt o o') => CAtomVar o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -withFreshUnificationVar sid desc k cont = do - withInferenceVar "_unif_" (InfVarBound k) \v -> do - ans <- toAtomVar v >>= cont - soln <- (M.lookup v <$> fromSolverSubst <$> getDiffState) >>= \case - Just soln -> return soln - Nothing -> throw sid $ AmbiguousInferenceVar (pprint v) (pprint k) desc - return (ans, soln) -{-# INLINE withFreshUnificationVar #-} - -withFreshUnificationVarNoEmits - :: (Zonkable e) => SrcId -> InfVarDesc -> CType o - -> (forall o'. (DExt o o') => CAtomVar o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -withFreshUnificationVarNoEmits sid desc k cont = diffStateT1 \s -> do - Abs Empty resultAndDiff <- buildScoped do - liftM toPairE $ runDiffStateT1 (sink s) $ - withFreshUnificationVar sid desc (sink k) cont - return $ fromPairE resultAndDiff - -withFreshDictVar - :: (Zonkable e, Emits o) => CType o - -- This tells us how to synthesize the dict. The supplied CType won't contain inference vars. - -> (forall o'. ( DExt o o') => CType o' -> SolverM i o' (CAtom o')) - -> (forall o'. (Emits o', DExt o o') => CAtom o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -withFreshDictVar dictTy synthIt cont = hasInferenceVars dictTy >>= \case - False -> withDistinct $ synthIt dictTy >>= cont - True -> withInferenceVar "_dict_" (DictBound dictTy) \v -> do - ans <- cont =<< (toAtom <$> toAtomVar v) - dictTy' <- zonk $ sink dictTy - dict <- synthIt dictTy' - return (ans, dict) -{-# INLINE withFreshDictVar #-} - -withFreshDictVarNoEmits - :: (Zonkable e) => CType o - -- This tells us how to synthesize the dict. The supplied CType won't contain inference vars. - -> (forall o'. (DExt o o') => CType o' -> SolverM i o' (CAtom o')) - -> (forall o'. (DExt o o') => CAtom o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -withFreshDictVarNoEmits dictTy synthIt cont = diffStateT1 \s -> do - Abs Empty resultAndDiff <- buildScoped do - liftM toPairE $ runDiffStateT1 (sink s) $ - withFreshDictVar (sink dictTy) synthIt cont - return $ fromPairE resultAndDiff -{-# INLINE withFreshDictVarNoEmits #-} - -withDict - :: (Zonkable e, Emits o) => SrcId -> CType o - -> (forall o'. (Emits o', DExt o o') => CAtom o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -withDict sid dictTy cont = withFreshDictVar dictTy - (\dictTy' -> lift11 $ trySynthTerm sid dictTy' Full) - cont -{-# INLINE withDict#-} - -addConstraint :: CAtomName o -> CAtom o -> SolverM i o () -addConstraint v ty = updateDiffStateM (SolverDiff $ RListE $ toSnocList [PairE v ty]) -{-# INLINE addConstraint #-} - -getInfState :: InfererM i o (InfState o) -getInfState = InfererM $ liftSubstReaderT ask -{-# INLINE getInfState #-} - -withInfState :: (InfState o -> InfState o) -> InfererM i o a -> InfererM i o a -withInfState f cont = InfererM $ local f (runInfererM' cont) -{-# INLINE withInfState #-} - -getTypeAndEmit :: HasType e => SrcId -> e o -> InfererM i o (e o) -getTypeAndEmit sid e = do - emitExprType sid (getType e) - return e - -emitExprType :: SrcId -> CType any -> InfererM i o () -emitExprType sid ty = emitTypeInfo sid $ ExprType $ pprint ty - -emitTypeInfo :: SrcId -> TypeInfo -> InfererM i o () -emitTypeInfo sid tyInfo = - InfererM $ liftSubstReaderT $ lift11 $ lift1 $ lift $ - modify (<> TypingInfo (M.singleton sid tyInfo)) - -withReducibleEmissions - :: (HasNamesE e, SubstE AtomSubstVal e, ToErr err) - => SrcId -> err - -> (forall o' . (Emits o', DExt o o') => InfererM i o' (e o')) - -> InfererM i o (e o) -withReducibleEmissions sid msg cont = do - withDecls <- buildScoped cont - reduceWithDecls withDecls >>= \case - Just t -> return t - _ -> throw sid msg -{-# INLINE withReducibleEmissions #-} - --- === actual inference pass === - -data RequiredTy (n::S) = - Check (CType n) - | Infer - deriving Show - -data PartialPiType (n::S) where - PartialPiType - :: AppExplicitness -> [Explicitness] - -> Nest CBinder n l - -> RequiredTy l - -> PartialPiType n - -data PartialType (n::S) = - PartialType (PartialPiType n) - | FullType (CType n) - -checkOrInfer :: Emits o => RequiredTy o -> UExpr i -> InfererM i o (CAtom o) -checkOrInfer reqTy expr = case reqTy of - Infer -> bottomUp expr - Check t -> topDown t expr - -topDown :: forall i o. Emits o => CType o -> UExpr i -> InfererM i o (CAtom o) -topDown ty uexpr = topDownPartial (typeAsPartialType ty) uexpr - -topDownPartial :: Emits o => PartialType o -> UExpr i -> InfererM i o (CAtom o) -topDownPartial partialTy exprWithSrc@(WithSrcE sid expr) = - case partialTy of - PartialType partialPiTy -> case expr of - ULam lam -> toAtom <$> Lam <$> checkULamPartial partialPiTy sid lam - _ -> toAtom <$> Lam <$> etaExpandPartialPi partialPiTy \resultTy explicitArgs -> do - expr' <- bottomUpExplicit exprWithSrc - dropSubst $ checkOrInferApp sid sid expr' explicitArgs [] resultTy - FullType ty -> topDownExplicit ty exprWithSrc - --- Creates a lambda for all args and returns (via CPA) the explicit args -etaExpandPartialPi - :: PartialPiType o - -> (forall o'. (Emits o', DExt o o') => RequiredTy o' -> [CAtom o'] -> InfererM i o' (CAtom o')) - -> InfererM i o (CoreLamExpr o) -etaExpandPartialPi (PartialPiType appExpl expls bs reqTy) cont = do - withFreshBindersInf expls (Abs bs reqTy) \bs' reqTy' -> do - let args = zip expls (toAtom <$> bindersVars bs') - explicits <- return $ catMaybes $ args <&> \case - (Explicit, arg) -> Just arg - _ -> Nothing - body <- buildBlock $ cont (sink reqTy') (sink <$> explicits) - let piTy = CorePiType appExpl expls bs' (getType body) - return $ CoreLamExpr piTy $ LamExpr bs' body - --- Expects the uexpr to be a type-like thing, including ordinary data types, pi --- types, dict types etc. -topDownType :: forall i o. Emits o => UExpr i -> InfererM i o (CType o) -topDownType exprWithSrc@(WithSrcE sid expr) = case expr of - UPrim UTuple xs -> toType . ProdType <$> mapM checkUType xs - _ -> do - ty <- bottomUpExplicit exprWithSrc - ty' <- maybeInterpretPunsAsTyCons (Check (toType $ Kind TypeKind)) ty - ty'' <- instantiateSigma sid Infer ty' - case toMaybeType ty'' of - Nothing -> throw sid $ ExpectedAType (pprint ty'') - Just ty''' -> return ty''' - --- Doesn't introduce implicit pi binders or dependent pairs -topDownExplicit :: forall i o. Emits o => CType o -> UExpr i -> InfererM i o (CAtom o) -topDownExplicit reqTy exprWithSrc@(WithSrcE sid expr) = emitExprType sid reqTy >> case expr of - ULam lamExpr -> case reqTy of - TyCon (Pi piTy) -> toAtom <$> Lam <$> checkULam sid lamExpr piTy - _ -> throw sid $ UnexpectedTerm "lambda" (pprint reqTy) - UFor dir uFor@(UForExpr b _) -> case reqTy of - TyCon (TabPi tabPiTy) -> do - lam@(UnaryLamExpr b' _) <- checkUForExpr sid uFor tabPiTy - ixTy <- asIxType (getSrcId b) $ binderType b' - emitHof $ For dir ixTy lam - _ -> throw sid $ UnexpectedTerm "`for` expression" (pprint reqTy) - UApp f posArgs namedArgs -> do - f' <- bottomUpExplicit f - checkOrInferApp sid (getSrcId f) f' posArgs namedArgs (Check reqTy) - UDepPair lhs rhs -> case reqTy of - TyCon (DepPairTy ty@(DepPairType _ (_ :> lhsTy) _)) -> do - lhs' <- checkSigmaDependent lhs (FullType lhsTy) - rhsTy <- instantiate ty [lhs'] - rhs' <- topDown rhsTy rhs - return $ toAtom $ DepPair lhs' rhs' ty - _ -> throw sid $ UnexpectedTerm "dependent pair" (pprint reqTy) - UCase scrut alts -> do - scrut' <- bottomUp scrut - let scrutTy = getType scrut' - alts' <- mapM (checkCaseAlt (Check reqTy) scrutTy) alts - buildSortedCase scrut' alts' reqTy - UDo block -> withBlockDecls block \result -> topDownExplicit (sink reqTy) result - UTabCon xs -> do - case reqTy of - TyCon (TabPi tabPiTy) -> checkTabCon tabPiTy sid xs - _ -> throw sid $ UnexpectedTerm "table constructor" (pprint reqTy) - UNatLit x -> fromNatLit sid x reqTy - UIntLit x -> fromIntLit sid x reqTy - UPrim UTuple xs -> case reqTy of - TyCon (Kind TypeKind) -> toAtom . ProdType <$> mapM checkUType xs - TyCon (ProdType reqTys) -> do - when (length reqTys /= length xs) $ throw sid $ TupleLengthMismatch (length reqTys) (length xs) - toAtom <$> ProdCon <$> forM (zip reqTys xs) \(reqTy', x) -> topDown reqTy' x - _ -> throw sid $ UnexpectedTerm "tuple" (pprint reqTy) - UFieldAccess _ _ -> infer - UVar _ -> infer - UTypeAnn _ _ -> infer - UTabApp _ _ -> infer - UFloatLit _ -> infer - UPrim _ _ -> infer - ULit _ -> infer - UPi _ -> infer - UTabPi _ -> infer - UDepPairTy _ -> infer - UHole -> throw sid InferHoleErr - where - infer :: InfererM i o (CAtom o) - infer = do - sigmaAtom <- maybeInterpretPunsAsTyCons (Check reqTy) =<< bottomUpExplicit exprWithSrc - instantiateSigma sid (Check reqTy) sigmaAtom - -bottomUp :: Emits o => UExpr i -> InfererM i o (CAtom o) -bottomUp expr = bottomUpExplicit expr >>= instantiateSigma (getSrcId expr) Infer - --- Doesn't instantiate implicit args -bottomUpExplicit :: Emits o => UExpr i -> InfererM i o (SigmaAtom o) -bottomUpExplicit (WithSrcE sid expr) = getTypeAndEmit sid =<< case expr of - UVar ~(InternalName _ sn v) -> do - v' <- renameM v - ty <- getUVarType v' - return $ SigmaUVar sn ty v' - ULit l -> return $ SigmaAtom Nothing $ Con $ Lit l - UFieldAccess x (WithSrc _ field) -> do - x' <- bottomUp x - ty <- return $ getType x' - fields <- getFieldDefs sid ty - case M.lookup field fields of - Just def -> case def of - FieldProj i -> SigmaAtom Nothing <$> projectField i x' - FieldDotMethod method (TyConParams _ params) -> do - method' <- toAtomVar method - resultTy <- partialAppType (getType method') (params ++ [x']) - return $ SigmaPartialApp resultTy (toAtom method') (params ++ [x']) - Nothing -> throw sid $ CantFindField (pprint field) (pprint ty) (map pprint $ M.keys fields) - ULam lamExpr -> SigmaAtom Nothing <$> toAtom <$> inferULam lamExpr - UFor dir uFor@(UForExpr b _) -> do - lam@(UnaryLamExpr b' _) <- inferUForExpr uFor - ixTy <- asIxType (getSrcId b) $ binderType b' - liftM (SigmaAtom Nothing) $ emitHof $ For dir ixTy lam - UApp f posArgs namedArgs -> do - f' <- bottomUpExplicit f - SigmaAtom Nothing <$> checkOrInferApp sid (getSrcId f) f' posArgs namedArgs Infer - UTabApp tab args -> do - tab' <- bottomUp tab - SigmaAtom Nothing <$> inferTabApp (getSrcId tab) tab' args - UPi (UPiExpr bs appExpl ty) -> do - -- TODO: check explicitness constraints - withUBinders bs \(ZipB expls bs') -> do - ty' <- checkUType ty - return $ SigmaAtom Nothing $ toAtom $ - Pi $ CorePiType appExpl expls bs' ty' - UTabPi (UTabPiExpr b ty) -> do - Abs b' ty' <- withUBinder b \(WithAttrB _ b') -> - liftM (Abs b') $ checkUType ty - d <- getIxDict (getSrcId b) $ binderType b' - let piTy = TabPiType d b' ty' - return $ SigmaAtom Nothing $ toAtom $ TabPi piTy - UDepPairTy (UDepPairType expl b rhs) -> do - withUBinder b \(WithAttrB _ b') -> do - rhs' <- checkUType rhs - return $ SigmaAtom Nothing $ toAtom $ DepPairTy $ DepPairType expl b' rhs' - UDepPair _ _ -> throw sid InferDepPairErr - UCase scrut (alt:alts) -> do - scrut' <- bottomUp scrut - let scrutTy = getType scrut' - alt'@(IndexedAlt _ altAbs) <- checkCaseAlt Infer scrutTy alt - Abs b ty <- liftEnvReaderM $ refreshAbs altAbs \b body -> do - return $ Abs b (getType body) - resultTy <- liftHoistExcept sid $ hoist b ty - alts' <- mapM (checkCaseAlt (Check resultTy) scrutTy) alts - SigmaAtom Nothing <$> buildSortedCase scrut' (alt':alts') resultTy - UCase _ [] -> throw sid InferEmptyCaseEff - UDo block -> withBlockDecls block \result -> bottomUpExplicit result - UTabCon xs -> liftM (SigmaAtom Nothing) $ inferTabCon sid xs - UTypeAnn val ty -> do - ty' <- checkUType ty - liftM (SigmaAtom Nothing) $ topDown ty' val - UPrim UTuple xs -> do - xs' <- forM xs \x -> bottomUp x - return $ SigmaAtom Nothing $ Con $ ProdCon xs' - UPrim UMonoLiteral [WithSrcE _ l] -> case l of - UIntLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Int32Lit $ fromIntegral x - UNatLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Word32Lit $ fromIntegral x - _ -> throwInternal "argument to %monoLit must be a literal" - UPrim UExplicitApply (f:xs) -> do - f' <- bottomUpExplicit f - xs' <- mapM bottomUp xs - SigmaAtom Nothing <$> applySigmaAtom f' xs' - UPrim UProjNewtype [x] -> do - x' <- bottomUp x >>= unwrapNewtype - return $ SigmaAtom Nothing x' - UPrim prim xs -> do - xs' <- forM xs \x -> do - inferPrimArg x >>= \case - Stuck _ (Var v) -> lookupAtomName (atomVarName v) >>= \case - LetBound (DeclBinding _ (Atom e)) -> return e - _ -> return $ toAtom v - x' -> return x' - liftM (SigmaAtom Nothing) $ matchPrimApp prim xs' - UNatLit l -> liftM (SigmaAtom Nothing) $ fromNatLit sid l NatTy - UIntLit l -> liftM (SigmaAtom Nothing) $ fromIntLit sid l (BaseTy $ Scalar Int32Type) - UFloatLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Float32Lit $ realToFrac x - UHole -> throw sid InferHoleErr - -expectEq :: (PrettyE e, AlphaEqE e) => SrcId -> e o -> e o -> InfererM i o () -expectEq sid reqTy actualTy = alphaEq reqTy actualTy >>= \case - True -> return () - False -> throw sid $ TypeMismatch (pprint reqTy) (pprint actualTy) -{-# INLINE expectEq #-} - -fromIntLit :: Emits o => SrcId -> Int -> CType o -> InfererM i o (CAtom o) -fromIntLit sid x ty = do - let litVal = Con $ Lit $ Int64Lit $ fromIntegral x - applyFromLiteralMethod sid ty "from_integer" litVal - -fromNatLit :: Emits o => SrcId -> Word64 -> CType o -> InfererM i o (CAtom o) -fromNatLit sid x ty = do - let litVal = Con $ Lit $ Word64Lit $ fromIntegral x - applyFromLiteralMethod sid ty "from_unsigned_integer" litVal - -instantiateSigma :: Emits o => SrcId -> RequiredTy o -> SigmaAtom o -> InfererM i o (CAtom o) -instantiateSigma sid reqTy sigmaAtom = case sigmaAtom of - SigmaUVar _ _ _ -> case getType sigmaAtom of - TyCon (Pi (CorePiType ImplicitApp expls bs resultTy)) -> do - bsConstrained <- buildConstraints (Abs bs resultTy) \_ resultTy' -> do - case reqTy of - Infer -> return [] - Check reqTy' -> return [TypeConstraint sid (sink reqTy') resultTy'] - args <- inferMixedArgs @UExpr sid fDesc expls bsConstrained ([], []) - applySigmaAtom sigmaAtom args - _ -> fallback - _ -> fallback - where - fallback = forceSigmaAtom sigmaAtom >>= matchReq sid reqTy - fDesc = getSourceName sigmaAtom - -matchReq :: Ext o o' => SrcId -> RequiredTy o -> CAtom o' -> InfererM i o' (CAtom o') -matchReq sid (Check reqTy) x = do - reqTy' <- sinkM reqTy - return x <* expectEq sid reqTy' (getType x) -matchReq _ Infer x = return x -{-# INLINE matchReq #-} - -forceSigmaAtom :: Emits o => SigmaAtom o -> InfererM i o (CAtom o) -forceSigmaAtom sigmaAtom = case sigmaAtom of - SigmaAtom _ x -> return x - SigmaUVar _ _ v -> undefined - -- SigmaUVar _ _ v -> case v of - -- UAtomVar v' -> inlineTypeAliases v' - -- _ -> applySigmaAtom sigmaAtom [] - SigmaPartialApp _ _ _ -> error "not implemented" -- better error message? - -withBlockDecls - :: (Emits o, Zonkable e) - => UBlock i - -> (forall i' o'. (Emits o', DExt o o') => UExpr i' -> InfererM i' o' (e o')) - -> InfererM i o (e o) -withBlockDecls (WithSrcE _ (UBlock declsTop result)) contTop = - go declsTop $ contTop result where - go :: (Emits o, Zonkable e) - => Nest UDecl i i' - -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) - -> InfererM i o (e o) - go decls cont = case decls of - Empty -> withDistinct cont - Nest d ds -> withUDecl d $ go ds $ cont - -withUDecl - :: (Emits o, Zonkable e) - => UDecl i i' - -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) - -> InfererM i o (e o) -withUDecl (WithSrcB _ d) cont = case d of - UPass -> withDistinct cont - UExprDecl e -> withDistinct $ bottomUp e >> cont - ULet letAnn p ann rhs -> do - val <- checkMaybeAnnExpr ann rhs - let letAnn' = considerInlineAnn letAnn (getType val) - var <- emitDecl (getNameHint p) letAnn' $ Atom val - bindLetPat p var cont - -considerInlineAnn :: LetAnn -> CType n -> LetAnn -considerInlineAnn PlainLet (TyCon (Kind _)) = InlineLet -considerInlineAnn PlainLet (TyCon (Pi (CorePiType _ _ _ (TyCon (Kind _))))) = InlineLet -considerInlineAnn ann _ = ann - -applyFromLiteralMethod - :: Emits n => SrcId -> CType n -> SourceName -> CAtom n -> InfererM i n (CAtom n) -applyFromLiteralMethod sid resultTy methodName litVal = - lookupSourceMap methodName >>= \case - Nothing -> error $ "prelude function not found: " ++ pprint methodName - Just methodName' -> do - MethodBinding className _ <- lookupEnv methodName' - dictTy <- toType <$> dictType className [toAtom resultTy] - Just d <- toMaybeDict <$> trySynthTerm sid dictTy Full - emit =<< mkApplyMethod d 0 [litVal] - --- atom that requires instantiation to become a rho type -data SigmaAtom n = - SigmaAtom (Maybe SourceName) (CAtom n) - | SigmaUVar SourceName (CType n) (UVar n) - | SigmaPartialApp (CType n) (CAtom n) [CAtom n] - deriving (Show) - --- XXX: this gives the type of the atom in the absence of other type information. --- So it interprets struct names as data constructors rather than type constructors. -instance HasType SigmaAtom where - getType = \case - SigmaAtom _ x -> getType x - SigmaUVar _ ty _ -> ty - SigmaPartialApp ty _ _ -> ty - -instance HasSourceName (SigmaAtom n) where - getSourceName = \case - SigmaAtom sn _ -> case sn of - Just sn' -> sn' - Nothing -> "" - SigmaUVar sn _ _ -> sn - SigmaPartialApp _ _ _ -> "" - -data FieldDef (n::S) = - FieldProj Int - | FieldDotMethod (CAtomName n) (TyConParams n) - deriving (Show, Generic) - -getFieldDefs :: SrcId -> CType n -> InfererM i n (M.Map FieldName' (FieldDef n)) -getFieldDefs sid ty = case ty of - StuckTy _ _ -> noFields - TyCon con -> case con of - NewtypeTyCon (UserADTType _ tyName params) -> do - TyConBinding ~(Just tyDef) (DotMethods dotMethods) <- lookupEnv tyName - instantiateTyConDef tyDef params >>= \case - StructFields fields -> do - let projFields = enumerate fields <&> \(i, (field, _)) -> - [(FieldName field, FieldProj i), (FieldNum i, FieldProj i)] - let methodFields = M.toList dotMethods <&> \(field, f) -> - (FieldName field, FieldDotMethod f params) - return $ M.fromList $ concat projFields ++ methodFields - ADTCons _ -> noFields - RefType valTy -> case valTy of - RefTy _ -> noFields - _ -> do - valFields <- getFieldDefs sid valTy - return $ M.filter isProj valFields - where isProj = \case - FieldProj _ -> True - _ -> False - ProdType ts -> return $ M.fromList $ enumerate ts <&> \(i, _) -> (FieldNum i, FieldProj i) - TabPi _ -> noFields - _ -> noFields - where noFields = throw sid $ NoFields $ pprint ty - -projectField :: Emits o => Int -> CAtom o -> InfererM i o (CAtom o) -projectField i x = case getType x of - StuckTy _ _ -> bad - TyCon con -> case con of - ProdType _ -> proj i x - NewtypeTyCon _ -> projectStruct i x - RefType valTy -> case valTy of - TyCon (ProdType _) -> getProjRef (ProjectProduct i) x - TyCon (NewtypeTyCon _) -> projectStructRef i x - _ -> bad - _ -> bad - where bad = error $ "bad projection: " ++ pprint (i, x) - -class PrettyE e => ExplicitArg (e::E) where - checkExplicitNonDependentArg :: Emits o => e i -> PartialType o -> InfererM i o (CAtom o) - checkExplicitDependentArg :: e i -> PartialType o -> InfererM i o (CAtom o) - inferExplicitArg :: Emits o => e i -> InfererM i o (CAtom o) - isHole :: e n -> Bool - explicitArgSrcId :: e n -> SrcId - -instance ExplicitArg UExpr where - checkExplicitDependentArg arg argTy = checkSigmaDependent arg argTy - checkExplicitNonDependentArg arg argTy = topDownPartial argTy arg - inferExplicitArg arg = bottomUp arg - isHole = \case - WithSrcE _ UHole -> True - _ -> False - explicitArgSrcId = getSrcId - -instance ExplicitArg CAtom where - checkExplicitDependentArg = checkCAtom - checkExplicitNonDependentArg = checkCAtom - inferExplicitArg arg = renameM arg - isHole _ = False - explicitArgSrcId _ = rootSrcId - -checkCAtom :: CAtom i -> PartialType o -> InfererM i o (CAtom o) -checkCAtom arg argTy = do - arg' <- renameM arg - case argTy of - FullType argTy' -> expectEq rootSrcId argTy' (getType arg') - PartialType _ -> return () -- TODO? - return arg' - -checkOrInferApp - :: forall i o arg . (Emits o, ExplicitArg arg) - => SrcId -> SrcId -> SigmaAtom o -> [arg i] -> [(SourceName, arg i)] - -> RequiredTy o -> InfererM i o (CAtom o) -checkOrInferApp appSrcId funSrcId f' posArgs namedArgs reqTy = do - f <- maybeInterpretPunsAsTyCons reqTy f' - case getType f of - TyCon (Pi piTy@(CorePiType appExpl expls _ _)) -> case appExpl of - ExplicitApp -> do - checkExplicitArity appSrcId expls posArgs - bsConstrained <- buildAppConstraints appSrcId reqTy piTy - args <- inferMixedArgs appSrcId fDesc expls bsConstrained (posArgs, namedArgs) - applySigmaAtom f args - ImplicitApp -> error "should already have handled this case" - ty -> throw funSrcId $ EliminationErr "function type" (pprint ty) - where - fDesc :: SourceName - fDesc = getSourceName f' - -buildAppConstraints :: SrcId -> RequiredTy n -> CorePiType n -> InfererM i n (ConstrainedBinders n) -buildAppConstraints appSrcId reqTy (CorePiType _ _ bs ty) = do - buildConstraints (Abs bs ty) \_ resultTy -> do - return case reqTy of - Infer -> [] - Check reqTy' -> [TypeConstraint appSrcId (sink reqTy') resultTy] - -maybeInterpretPunsAsTyCons :: RequiredTy n -> SigmaAtom n -> InfererM i n (SigmaAtom n) -maybeInterpretPunsAsTyCons = undefined --- maybeInterpretPunsAsTyCons (Check (TyCon (Kind TypeKind))) (SigmaUVar sn _ (UPunVar v)) = do --- let v' = UTyConVar v --- ty <- getUVarType v' --- return $ SigmaUVar sn ty v' --- maybeInterpretPunsAsTyCons _ x = return x - -type IsDependent = Bool - -inlineTypeAliases :: CAtomName n -> InfererM i n (CAtom n) -inlineTypeAliases v = do - lookupAtomName v >>= \case - LetBound (DeclBinding InlineLet (Atom e)) -> return e - _ -> toAtom <$> toAtomVar v - -applySigmaAtom :: Emits o => SigmaAtom o -> [CAtom o] -> InfererM i o (CAtom o) -applySigmaAtom (SigmaAtom _ f) args = emit =<< mkApp f args --- applySigmaAtom (SigmaUVar _ _ f) args = case f of --- UAtomVar f' -> do --- f'' <- inlineTypeAliases f' --- emit =<< mkApp f'' args --- UTyConVar f' -> do --- TyConDef sn expls _ _ <- lookupTyCon f' --- return $ toAtom $ UserADTType sn f' (TyConParams expls args) --- UDataConVar v -> do --- (tyCon, i) <- lookupDataCon v --- applyDataCon tyCon i args --- UPunVar tc -> do --- TyConDef sn _ _ _ <- lookupTyCon tc --- -- interpret as a data constructor by default --- (params, dataArgs) <- splitParamPrefix tc args --- repVal <- makeStructRepVal tc dataArgs --- return $ toAtom $ NewtypeCon (UserADTData sn tc params) repVal --- UClassVar f' -> do --- ClassDef sourceName builtinName _ _ _ _ _ _ <- lookupClassDef f' --- return $ toAtom case builtinName of --- Just Ix -> IxDictType singleTyParam --- Nothing -> DictType sourceName f' args --- where singleTyParam = case args of --- [p] -> fromJust $ toMaybeType p --- _ -> error "not a single type param" --- UMethodVar f' -> do --- MethodBinding className methodIdx <- lookupEnv f' --- ClassDef _ _ _ _ _ paramBs _ _ <- lookupClassDef className --- let numParams = nestLength paramBs --- -- params aren't needed because they're already implied by the dict argument --- let (dictArg:args') = drop numParams args --- emit =<< mkApplyMethod (fromJust $ toMaybeDict dictArg) methodIdx args' -applySigmaAtom (SigmaPartialApp _ f prevArgs) args = - emit =<< mkApp f (prevArgs ++ args) - -splitParamPrefix :: EnvReader m => TyConName n -> [CAtom n] -> m n (TyConParams n, [CAtom n]) -splitParamPrefix tc args = do - TyConDef _ _ paramBs _ <- lookupTyCon tc - let (paramArgs, dataArgs) = splitAt (nestLength paramBs) args - params <- makeTyConParams tc paramArgs - return (params, dataArgs) - -applyDataCon :: Emits o => TyConName o -> Int -> [CAtom o] -> InfererM i o (CAtom o) -applyDataCon tc conIx topArgs = do - tyDef@(TyConDef sn _ _ _) <- lookupTyCon tc - (params, dataArgs) <- splitParamPrefix tc topArgs - ADTCons conDefs <- instantiateTyConDef tyDef params - DataConDef _ _ repTy _ <- return $ conDefs !! conIx - conProd <- wrap repTy dataArgs - repVal <- return case conDefs of - [] -> error "unreachable" - [_] -> conProd - _ -> Con $ SumCon conTys conIx conProd - where conTys = conDefs <&> \(DataConDef _ _ rty _) -> rty - return $ toAtom $ NewtypeCon (UserADTData sn tc params) repVal - where - wrap :: EnvReader m => CType n -> [CAtom n] -> m n (CAtom n) - wrap _ [arg] = return $ arg - wrap rty args = case rty of - TyCon (ProdType tys) -> - if nargs == ntys - then return $ Con $ ProdCon args - else Con . ProdCon . (curArgs ++) . (:[]) <$> wrap (last tys) remArgs - where - nargs = length args; ntys = length tys - (curArgs, remArgs) = splitAt (ntys - 1) args - TyCon (DepPairTy dpt@(DepPairType _ b rty')) -> do - rty'' <- applySubst (b@>SubstVal h) rty' - ans <- wrap rty'' t - return $ toAtom $ DepPair h ans dpt - where h:t = args - _ -> error $ "Unexpected data con representation type: " ++ pprint rty - -checkExplicitArity :: SrcId -> [Explicitness] -> [a] -> InfererM i o () -checkExplicitArity sid expls args = do - let arity = length [() | Explicit <- expls] - let numArgs = length args - when (numArgs /= arity) $ throw sid $ ArityErr arity numArgs - -type MixedArgs arg = ([arg], [(SourceName, arg)]) -- positional args, named args -data Constraint (n::S) = TypeConstraint SrcId (CType n) (CType n) - -type Constraints = ListE Constraint -type ConstrainedBinders n = ([IsDependent], Abs (Nest CBinder) Constraints n) - -buildConstraints - :: HasNamesE e - => Abs (Nest CBinder) e o - -> (forall o'. DExt o o' => [CAtom o'] -> e o' -> EnvReaderM o' [Constraint o']) - -> InfererM i o (ConstrainedBinders o) -buildConstraints ab cont = liftEnvReaderM do - refreshAbs ab \bs e -> do - cs <- cont (toAtom <$> bindersVars bs) e - return (getDependence (Abs bs e), Abs bs $ ListE cs) - where - getDependence :: HasNamesE e => Abs (Nest CBinder) e n -> [IsDependent] - getDependence (Abs Empty _) = [] - getDependence (Abs (Nest b bs) e) = - (binderName b `isFreeIn` Abs bs e) : getDependence (Abs bs e) - --- TODO: check that there are no extra named args provided -inferMixedArgs - :: forall arg i o . (Emits o, ExplicitArg arg) - => SrcId -> SourceName - -> [Explicitness] -> ConstrainedBinders o - -> MixedArgs (arg i) - -> InfererM i o [CAtom o] -inferMixedArgs appSrcId fSourceName explsTop (dependenceTop, bsAbs) argsTop@(_, namedArgsTop) = do - checkNamedArgValidity appSrcId explsTop (map fst namedArgsTop) - liftSolverM $ fromListE <$> go explsTop dependenceTop bsAbs argsTop - where - go :: Emits oo - => [Explicitness] -> [IsDependent] -> Abs (Nest CBinder) Constraints oo -> MixedArgs (arg i) - -> SolverM i oo (ListE CAtom oo) - go expls dependence (Abs bs cs) args = do - cs' <- eagerlyApplyConstraints bs cs - case (expls, dependence, bs) of - ([], [], Empty) -> return mempty - (expl:explsRest, isDependent:dependenceRest, Nest b bsRest) -> do - inferMixedArg isDependent (binderType b) expl args \arg restArgs -> do - bs' <- applySubst (b @> SubstVal arg) (Abs bsRest cs') - (ListE [arg] <>) <$> go explsRest dependenceRest bs' restArgs - (_, _, _) -> error "zip error" - - eagerlyApplyConstraints - :: Nest CBinder oo oo' -> Constraints oo' - -> SolverM i oo (Constraints oo') - eagerlyApplyConstraints Empty (ListE cs) = mapM_ applyConstraint cs >> return (ListE []) - eagerlyApplyConstraints bs (ListE cs) = ListE <$> forMFilter cs \c -> do - case hoist bs c of - HoistSuccess c' -> case c' of - TypeConstraint _ _ _ -> applyConstraint c' >> return Nothing - HoistFailure _ -> return $ Just c - - inferMixedArg - :: (Emits oo, Zonkable e) => IsDependent -> CType oo -> Explicitness -> MixedArgs (arg i) - -> (forall o'. (Emits o', DExt oo o') => CAtom o' -> MixedArgs (arg i) -> SolverM i o' (e o')) - -> SolverM i oo (e oo) - inferMixedArg isDependent argTy' expl args cont = do - argTy <- zonk argTy' - case expl of - Explicit -> do - -- this should succeed because we've already done the arity check - (arg:argsRest, namedArgs) <- return args - if isHole arg - then do - let desc = (pprint fSourceName, "_") - withFreshUnificationVar appSrcId (ImplicitArgInfVar desc) argTy \v -> - cont (toAtom v) (argsRest, namedArgs) - else do - arg' <- checkOrInferExplicitArg isDependent arg argTy - withDistinct $ cont arg' (argsRest, namedArgs) - Inferred argName infMech -> do - let desc = (pprint $ fSourceName, fromMaybe "_" (fmap pprint argName)) - case lookupNamedArg args argName of - Just arg -> do - arg' <- checkOrInferExplicitArg isDependent arg argTy - withDistinct $ cont arg' args - Nothing -> case infMech of - Unify -> withFreshUnificationVar appSrcId (ImplicitArgInfVar desc) argTy \v -> cont (toAtom v) args - Synth _ -> withDict appSrcId argTy \d -> cont d args - - checkOrInferExplicitArg :: Emits oo => Bool -> arg i -> CType oo -> SolverM i oo (CAtom oo) - checkOrInferExplicitArg isDependent arg argTy = do - arg' <- lift11 $ withoutInfVarsPartial argTy >>= \case - Just partialTy -> case isDependent of - True -> checkExplicitDependentArg arg partialTy - False -> checkExplicitNonDependentArg arg partialTy - Nothing -> inferExplicitArg arg - constrainEq (explicitArgSrcId arg) argTy (getType arg') - return arg' - - lookupNamedArg :: MixedArgs x -> Maybe SourceName -> Maybe x - lookupNamedArg _ Nothing = Nothing - lookupNamedArg (_, namedArgs) (Just v) = lookup v namedArgs - - withoutInfVarsPartial :: CType n -> InfererM i n (Maybe (PartialType n)) - withoutInfVarsPartial = \case - TyCon (Pi piTy) -> - withoutInfVars piTy >>= \case - Just piTy' -> return $ Just $ PartialType $ piAsPartialPi piTy' - Nothing -> withoutInfVars $ PartialType $ piAsPartialPiDropResultTy piTy - ty -> liftM (FullType <$>) $ withoutInfVars ty - - withoutInfVars :: HoistableE e => e n -> InfererM i n (Maybe (e n)) - withoutInfVars x = hasInferenceVars x >>= \case - True -> return Nothing - False -> return $ Just x - -checkNamedArgValidity :: Fallible m => SrcId -> [Explicitness] -> [SourceName] -> m () -checkNamedArgValidity sid expls offeredNames = do - let explToMaybeName = \case - Explicit -> Nothing - Inferred v _ -> v - let acceptedNames = catMaybes $ map explToMaybeName expls - let duplicates = repeated offeredNames - when (not $ null duplicates) $ throw sid $ RepeatedOptionalArgs $ map pprint duplicates - let unrecognizedNames = filter (not . (`elem` acceptedNames)) offeredNames - when (not $ null unrecognizedNames) do - throw sid $ UnrecognizedOptionalArgs (map pprint unrecognizedNames) (map pprint acceptedNames) - -inferPrimArg :: Emits o => UExpr i -> InfererM i o (CAtom o) -inferPrimArg x = do - xBlock <- buildBlock $ bottomUp x - case getType xBlock of - TyCon (Kind TypeKind) -> reduceExpr xBlock >>= \case - Just reduced -> return reduced - _ -> throwInternal "Type args to primops must be reducible" - _ -> emit xBlock - -matchPrimApp :: Emits o => PrimName -> [CAtom o] -> InfererM i o (CAtom o) -matchPrimApp = \case - UNat -> \case ~[] -> return $ toAtom $ NewtypeTyCon Nat - UFin -> \case ~[n] -> return $ toAtom $ NewtypeTyCon (Fin n) - UBaseType b -> \case ~[] -> return $ toAtomR $ BaseType b - UNatCon -> \case ~[x] -> return $ toAtom $ NewtypeCon NatCon x - UPrimTC tc -> case tc of - S.ProdType -> \ts -> return $ toAtom $ ProdType $ map (fromJust . toMaybeType) ts - S.SumType -> \ts -> return $ toAtom $ SumType $ map (fromJust . toMaybeType) ts - S.RefType -> \case ~[h, a] -> undefined -- return $ toAtom $ RefType h (fromJust $ toMaybeType a) - S.TypeKind -> \case ~[] -> return $ toAtom $ Kind $ TypeKind - UCon con -> case con of - S.ProdCon -> \xs -> return $ toAtom $ ProdCon xs - S.SumCon _ -> error "not supported" - -- UMiscOp op -> \x -> emit =<< MiscOp <$> matchGenericOp op x - -- UMemOp op -> \x -> emit =<< MemOp <$> matchGenericOp op x - UBinOp op -> \case ~[x, y] -> emitBinOp op x y - UUnOp op -> \case ~[x] -> emitUnOp op x - UMGet -> \case ~[r] -> emitRefOp r MGet - UMPut -> \case ~[r, x] -> emitRefOp r $ MPut x - UIndexRef -> \case ~[r, i] -> indexRef r i - UApplyMethod i -> \case ~(d:args) -> emit =<< mkApplyMethod (fromJust $ toMaybeDict d) i args - ULinearize -> \case ~[f, x] -> do f' <- lam1 f; emitHof $ Linearize f' x - UTranspose -> \case ~[f, x] -> do f' <- lam1 f; emitHof $ Transpose f' x - p -> \case xs -> throwInternal $ "Bad primitive application: " ++ show (p, xs) - where - lam2 :: Fallible m => CAtom n -> m (LamExpr n) - lam2 x = do - ExplicitCoreLam (BinaryNest b1 b2) body <- return x - return $ BinaryLamExpr b1 b2 body - - lam1 :: Fallible m => CAtom n -> m (LamExpr n) - lam1 x = do - ExplicitCoreLam (UnaryNest b) body <- return x - return $ UnaryLamExpr b body - - -- matchGenericOp :: GenericOp op => OpConst op -> [CAtom n] -> InfererM i n (op n) - -- matchGenericOp op xs = do - -- (tyArgs, dataArgs) <- partitionEithers <$> forM xs \x -> do - -- case getType x of - -- TyCon (Kind TypeKind) -> do - -- Just x' <- return $ toMaybeType x - -- return $ Left x' - -- _ -> return $ Right x - -- let tyArgs' = case tyArgs of - -- [] -> Nothing - -- [t] -> Just t - -- _ -> error "Expected at most one type arg" - -- return $ fromJust $ toOp $ GenericOpRep op tyArgs' dataArgs - -pattern ExplicitCoreLam :: Nest CBinder n l -> CExpr l -> CAtom n -pattern ExplicitCoreLam bs body <- Con (Lam (CoreLamExpr _ (LamExpr bs body))) - --- === n-ary applications === - -inferTabApp :: Emits o => SrcId -> CAtom o -> [UExpr i] -> InfererM i o (CAtom o) -inferTabApp tabSrcId tab args = do - tabTy <- return $ getType tab - args' <- inferNaryTabAppArgs tabSrcId tabTy args - naryTabApp tab args' - -inferNaryTabAppArgs :: Emits o => SrcId -> CType o -> [UExpr i] -> InfererM i o [CAtom o] -inferNaryTabAppArgs _ _ [] = return [] -inferNaryTabAppArgs tabSrcId tabTy (arg:rest) = case tabTy of - TyCon (TabPi (TabPiType _ b resultTy)) -> do - let ixTy = binderType b - let isDependent = binderName b `isFreeIn` resultTy - arg' <- if isDependent - then checkSigmaDependent arg (FullType ixTy) - else topDown ixTy arg - resultTy' <- applySubst (b @> SubstVal arg') resultTy - rest' <- inferNaryTabAppArgs tabSrcId resultTy' rest - return $ arg':rest' - _ -> throw tabSrcId $ EliminationErr "table type" (pprint tabTy) - -checkSigmaDependent :: UExpr i -> PartialType o -> InfererM i o (CAtom o) -checkSigmaDependent e ty = withReducibleEmissions (getSrcId e) CantReduceDependentArg $ - topDownPartial (sink ty) e - --- === sorting case alternatives === - -data IndexedAlt n = IndexedAlt CaseAltIndex (Alt n) - -instance SinkableE IndexedAlt where - sinkingProofE = todoSinkableProof - -buildNthOrderedAlt :: (Emits n, Builder m) - => [IndexedAlt n] -> CType n -> CType n -> Int -> CAtom n - -> m n (CAtom n) -buildNthOrderedAlt alts _ resultTy i v = do - case lookup i [(idx, alt) | IndexedAlt idx alt <- alts] of - Nothing -> do - resultTy' <- sinkM resultTy - emit $ PrimOp resultTy' $ MiscOp ThrowError - Just alt -> applyAbs alt (SubstVal v) >>= emit - -buildMonomorphicCase - :: (Emits n, ScopableBuilder m) - => [IndexedAlt n] -> CAtom n -> CType n -> m n (CAtom n) -buildMonomorphicCase alts scrut resultTy = do - scrutTy <- return $ getType scrut - buildCase scrut resultTy \i v -> do - ListE alts' <- sinkM $ ListE alts - scrutTy' <- sinkM scrutTy - resultTy' <- sinkM resultTy - buildNthOrderedAlt alts' scrutTy' resultTy' i v - -buildSortedCase :: (Fallible1 m, Builder m, Emits n) - => CAtom n -> [IndexedAlt n] -> CType n - -> m n (CAtom n) -buildSortedCase scrut alts resultTy = do - scrutTy <- return $ getType scrut - case scrutTy of - TyCon (NewtypeTyCon (UserADTType _ defName _)) -> do - TyConDef _ _ _ (ADTCons cons) <- lookupTyCon defName - case cons of - [] -> error "case of void?" - -- Single constructor ADTs are not sum types, so elide the case. - [_] -> do - let [IndexedAlt _ alt] = alts - scrut' <- unwrapNewtype scrut - emit =<< applyAbs alt (SubstVal scrut') - _ -> do - scrut' <- unwrapNewtype scrut - liftEmitBuilder $ buildMonomorphicCase alts scrut' resultTy - _ -> fail $ "Unexpected case expression type: " <> pprint scrutTy - --- TODO: cache this with the instance def (requires a recursive binding) -instanceFun :: EnvReader m => InstanceName n -> AppExplicitness -> m n (CAtom n) -instanceFun instanceName appExpl = do - InstanceDef _ expls bs _ _ <- lookupInstanceDef instanceName - liftEnvReaderM $ refreshAbs (Abs bs UnitE) \bs' UnitE -> do - args <- mapM toAtomVar $ nestToNames bs' - result <- toAtom <$> mkInstanceDict (sink instanceName) (toAtom <$> args) - let piTy = CorePiType appExpl expls bs' (getType result) - return $ toAtom $ CoreLamExpr piTy (LamExpr bs' $ Atom result) - -checkMaybeAnnExpr :: Emits o => Maybe (UType i) -> UExpr i -> InfererM i o (CAtom o) -checkMaybeAnnExpr ty expr = confuseGHC >>= \_ -> case ty of - Nothing -> bottomUp expr - Just ty' -> do - ty'' <- checkUType ty' - topDown ty'' expr - -inferTyConDef :: UDataDef i -> InfererM i o (TyConDef o) -inferTyConDef (UDataDef tyConName paramBs dataCons) = do - withUBinders paramBs \(ZipB expls paramBs') -> do - dataCons' <- ADTCons <$> mapM inferDataCon dataCons - return (TyConDef tyConName expls paramBs' dataCons') - -inferStructDef :: UStructDef i -> InfererM i o (TyConDef o) -inferStructDef (UStructDef tyConName paramBs fields _) = do - withUBinders paramBs \(ZipB expls paramBs') -> do - let (fieldNames, fieldTys) = unzip fields - tys <- mapM checkUType fieldTys - let dataConDefs = StructFields $ zip (withoutSrc <$> fieldNames) tys - return $ TyConDef tyConName expls paramBs' dataConDefs - -inferDotMethod - :: TyConName o - -> Abs (Nest UAnnBinder) (Abs UBinder ULamExpr) i - -> InfererM i o (CoreLamExpr o) -inferDotMethod tc (Abs uparamBs (Abs selfB lam)) = do - TyConDef sn expls paramBs _ <- lookupTyCon tc - withFreshBindersInf expls (Abs paramBs UnitE) \paramBs' UnitE -> do - let paramVs = bindersVars paramBs' - extendRenamer (uparamBs @@> (atomVarName <$> paramVs)) do - let selfTy = toType $ UserADTType sn (sink tc) (TyConParams expls (toAtom <$> paramVs)) - withFreshBinderInf "self" Explicit selfTy \selfB' -> do - lam' <- extendRenamer (selfB @> binderName selfB') $ inferULam lam - return $ prependCoreLamExpr (expls ++ [Explicit]) (paramBs' >>> UnaryNest selfB') lam' - - where - prependCoreLamExpr :: [Explicitness] -> Nest CBinder n l -> CoreLamExpr l -> CoreLamExpr n - prependCoreLamExpr expls bs e = case e of - CoreLamExpr (CorePiType appExpl piExpls piBs effTy) (LamExpr lamBs body) -> do - let piType = CorePiType appExpl (expls <> piExpls) (bs >>> piBs) effTy - let lamExpr = LamExpr (bs >>> lamBs) body - CoreLamExpr piType lamExpr - -inferDataCon :: (SourceName, UDataDefTrail i) -> InfererM i o (DataConDef o) -inferDataCon (sourceName, UDataDefTrail argBs) = do - withUBinders argBs \(ZipB _ argBs') -> do - let (repTy, projIdxs) = dataConRepTy $ EmptyAbs argBs' - return $ DataConDef sourceName (EmptyAbs argBs') repTy projIdxs - -dataConRepTy :: EmptyAbs (Nest CBinder) n -> (CType n, [[Projection]]) -dataConRepTy (Abs topBs UnitE) = case topBs of - Empty -> (UnitTy, []) - _ -> go [] [UnwrapNewtype] topBs - where - go :: [CType l] -> [Projection] -> Nest (Binder) l p -> (CType l, [[Projection]]) - go revAcc projIdxs = \case - Empty -> case revAcc of - [] -> error "should never happen" - [ty] -> (ty, [projIdxs]) - _ -> ( toType $ ProdType $ reverse revAcc - , iota (length revAcc) <&> \i -> ProjectProduct i:projIdxs ) - Nest b bs -> case hoist b (EmptyAbs bs) of - HoistSuccess (Abs bs' UnitE) -> go (binderType b:revAcc) projIdxs bs' - HoistFailure _ -> (fullTy, idxs) - where - accSize = length revAcc - (fullTy, depTyIdxs) = case revAcc of - [] -> (depTy, []) - _ -> (toType $ ProdType $ reverse revAcc ++ [depTy], [ProjectProduct accSize]) - (tailTy, tailIdxs) = go [] (ProjectProduct 1 : (depTyIdxs ++ projIdxs)) bs - idxs = (iota accSize <&> \i -> ProjectProduct i : projIdxs) ++ - ((ProjectProduct 0 : (depTyIdxs ++ projIdxs)) : tailIdxs) - depTy = toType $ DepPairTy $ DepPairType ExplicitDepPair b tailTy - -inferClassDef - :: SourceName -> [SourceName] -> Nest UAnnBinder i i' -> [UType i'] - -> InfererM i o (ClassDef o) -inferClassDef className methodNames paramBs methodTys = do - withUBinders paramBs \(ZipB expls paramBs') -> do - let paramNames = catMaybes $ nestToListFlip paramBs \(UAnnBinder expl b _ _) -> - case expl of Inferred _ (Synth _) -> Nothing - _ -> Just $ Just $ getSourceName b - methodTys' <- forM methodTys \m -> do - checkUType m >>= \case - TyCon (Pi t) -> return t - t -> return $ CorePiType ImplicitApp [] Empty t - PairB paramBs'' superclassBs <- partitionBinders rootSrcId (zipAttrs expls paramBs') $ - \b@(WithAttrB expl b') -> case expl of - Explicit -> return $ LeftB b - -- TODO: Add a proper SrcId here. We'll need to plumb it through from the original UBinders - Inferred _ Unify -> throw rootSrcId InterfacesNoImplicitParams - Inferred _ (Synth _) -> return $ RightB b' - let (roleExpls', paramBs''') = unzipAttrs paramBs'' - builtinName <- case className of - -- TODO: this is hacky. Let's just make the Ix class, including its - -- methods, fully built-in instead of prelude-defined. - "Ix" -> return $ Just Ix - _ -> return Nothing - return $ ClassDef className builtinName methodNames paramNames roleExpls' paramBs''' superclassBs methodTys' - -withUBinder :: UAnnBinder i i' -> InfererCPSB2 (WithExpl CBinder) i i' o a -withUBinder (UAnnBinder expl (WithSrcB sid b) ann cs) cont = do - ty <- inferAnn sid ann cs - emitExprType sid ty - withFreshBinderInf (getNameHint b) expl ty \b' -> - extendSubst (b@>binderName b') $ cont (WithAttrB expl b') - -withUBinders :: Nest UAnnBinder i i' -> InfererCPSB2 (Nest (WithExpl CBinder)) i i' o a -withUBinders bs cont = do - Abs bs' UnitE <- inferUBinders bs \_ -> return UnitE - let (expls, bs'') = unzipAttrs bs' - withFreshBindersInf expls (Abs bs'' UnitE) \bs''' UnitE -> do - extendSubst (bs@@> (atomVarName <$> bindersVars bs''')) $ - cont $ zipAttrs expls bs''' - -inferUBinders - :: Zonkable e => Nest UAnnBinder i i' - -> (forall o'. DExt o o' => [CAtomName o'] -> InfererM i' o' (e o')) - -> InfererM i o (Abs (Nest (WithExpl CBinder)) e o) -inferUBinders Empty cont = withDistinct $ Abs Empty <$> cont [] -inferUBinders (Nest (UAnnBinder expl (WithSrcB sid b) ann cs) bs) cont = do - -- TODO: factor out the common part of each case (requires an annotated - -- `where` clause because of the rank-2 type) - ty <- inferAnn sid ann cs - emitExprType sid ty - withFreshBinderInf (getNameHint b) expl ty \b' -> do - extendSubst (b@>binderName b') do - Abs bs' e <- inferUBinders bs \vs -> cont (sink (binderName b') : vs) - return $ Abs (Nest (WithAttrB expl b') bs') e - -inferAnn :: SrcId -> UAnn i -> [UConstraint i] -> InfererM i o (CType o) -inferAnn binderSrcId ann cs = case ann of - UAnn ty -> checkUType ty - UNoAnn -> case cs of - WithSrcE sid (UVar ~(InternalName _ _ v)):_ -> do - renameM v >>= getUVarType >>= \case - TyCon (Pi (CorePiType ExplicitApp [Explicit] (UnaryNest (_:>ty)) _)) -> return ty - ty -> throw sid $ NotAUnaryConstraint $ pprint ty - _ -> throw binderSrcId AnnotationRequired - -checkULamPartial :: PartialPiType o -> SrcId -> ULamExpr i -> InfererM i o (CoreLamExpr o) -checkULamPartial partialPiTy sid lamExpr = do - PartialPiType piAppExpl expls piBs piReqTy <- return partialPiTy - ULamExpr lamBs lamAppExpl lamResultTy body <- return lamExpr - checkExplicitArity sid expls (nestToList (const ()) lamBs) - when (piAppExpl /= lamAppExpl) $ throw sid $ WrongArrowErr (pprint piAppExpl) (pprint lamAppExpl) - checkLamBinders expls piBs lamBs \lamBs' -> do - piReqTy' <- applyRename (piBs @@> (atomVarName <$> bindersVars lamBs')) piReqTy - resultTy <- case (lamResultTy, piReqTy') of - (Nothing, Infer ) -> return Infer - (Just t , Infer ) -> Check <$> checkUType t - (Nothing, Check t) -> Check <$> return t - (Just t , Check t') -> checkUType t >>= expectEq (getSrcId t) t' >> return (Check t') - body' <- buildBlock $ withBlockDecls body \result -> checkOrInfer (sink resultTy) result - resultTy' <- case resultTy of - Infer -> return $ getType body' - Check t -> return t - let piTy = CorePiType piAppExpl expls lamBs' resultTy' - return $ CoreLamExpr piTy (LamExpr lamBs' body') - where - checkLamBinders - :: [Explicitness] -> Nest CBinder o any -> Nest UAnnBinder i i' - -> InfererCPSB2 (Nest CBinder) i i' o a - checkLamBinders [] Empty Empty cont = withDistinct $ cont Empty - checkLamBinders (piExpl:piExpls) (Nest (piB:>piAnn) piBs) lamBs cont = do - case piExpl of - Inferred _ _ -> do - withFreshBinderInf (getNameHint piB) piExpl piAnn \b -> do - Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs) - checkLamBinders piExpls piBs' lamBs \bs -> cont (Nest b bs) - Explicit -> case lamBs of - Nest (UAnnBinder _ (WithSrcB bSid lamB) lamAnn _) lamBsRest -> emitExprType bSid piAnn >> do - case lamAnn of - UAnn lamAnn' -> checkUType lamAnn' >>= expectEq (getSrcId lamAnn') piAnn - UNoAnn -> return () - withFreshBinderInf (getNameHint lamB) Explicit piAnn \b -> do - Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs) - extendRenamer (lamB@>sink (binderName b)) $ - checkLamBinders piExpls piBs' lamBsRest \bs -> cont (Nest b bs) - Empty -> error "zip error" - checkLamBinders _ _ _ _ = error "zip error" - -inferUForExpr :: Emits o => UForExpr i -> InfererM i o (LamExpr o) -inferUForExpr (UForExpr b body) = do - withUBinder b \(WithAttrB _ b') -> do - body' <- buildBlock $ withBlockDecls body \result -> bottomUp result - return $ LamExpr (UnaryNest b') body' - -checkUForExpr :: Emits o => SrcId -> UForExpr i -> TabPiType o -> InfererM i o (LamExpr o) -checkUForExpr sid (UForExpr bFor body) (TabPiType _ bPi resultTy) = do - let uLamExpr = ULamExpr (UnaryNest bFor) ExplicitApp Nothing body - partialPi <- liftEnvReaderM $ refreshAbs (Abs bPi resultTy) \bPi' resultTy' -> do - return $ PartialPiType ExplicitApp [Explicit] (UnaryNest bPi') (Check resultTy') - CoreLamExpr _ lamExpr <- checkULamPartial partialPi sid uLamExpr - return lamExpr - -inferULam :: ULamExpr i -> InfererM i o (CoreLamExpr o) -inferULam (ULamExpr bs appExpl resultTy body) = do - Abs (ZipB expls bs') (PairE ty body') <- inferUBinders bs \_ -> do - resultTy' <- mapM checkUType resultTy - body' <- buildBlock do - withBlockDecls body \result -> - case resultTy' of - Nothing -> bottomUp result - Just resultTy'' -> topDown (sink resultTy'') result - return $ PairE (getType body') body' - return $ CoreLamExpr (CorePiType appExpl expls bs' ty) (LamExpr bs' body') - -checkULam :: SrcId -> ULamExpr i -> CorePiType o -> InfererM i o (CoreLamExpr o) -checkULam sid ulam piTy = checkULamPartial (piAsPartialPi piTy) sid ulam - -piAsPartialPi :: CorePiType n -> PartialPiType n -piAsPartialPi (CorePiType appExpl expls bs ty) = - PartialPiType appExpl expls bs (Check ty) - -typeAsPartialType :: CType n -> PartialType n -typeAsPartialType (TyCon (Pi piTy)) = PartialType $ piAsPartialPi piTy -typeAsPartialType ty = FullType ty - -piAsPartialPiDropResultTy :: CorePiType n -> PartialPiType n -piAsPartialPiDropResultTy (CorePiType appExpl expls bs _) = - PartialPiType appExpl expls bs Infer - -checkInstanceParams :: Nest CBinder o any -> [UExpr i] -> InfererM i o [CAtom o] -checkInstanceParams bsTop paramsTop = go bsTop paramsTop - where - go :: Nest CBinder o any -> [UExpr i] -> InfererM i o [CAtom o] - go Empty [] = return [] - go (Nest (b:>ty) bs) (x:xs) = do - let msg = CantReduceType $ pprint x - x' <- withReducibleEmissions (getSrcId x) msg $ topDown (sink ty) x - Abs bs' UnitE <- applySubst (b@>SubstVal x') $ Abs bs UnitE - (x':) <$> go bs' xs - go _ _ = error "zip error" - -checkInstanceBody - :: ClassName o -> [CAtom o] - -> [UMethodDef i] -> InfererM i o (InstanceBody o) -checkInstanceBody className params methods = do - -- instances are top-level so it's ok to have imprecise root srcIds here - let sid = rootSrcId - ClassDef _ _ methodNames _ _ paramBs scBs methodTys <- lookupClassDef className - Abs scBs' methodTys' <- applySubst (paramBs @@> (SubstVal <$> params)) $ Abs scBs $ ListE methodTys - superclassTys <- superclassDictTys scBs' - superclassDicts <- mapM (flip (trySynthTerm sid) Full) superclassTys - ListE methodTys'' <- applySubst (scBs'@@>(SubstVal<$>superclassDicts)) methodTys' - methodsChecked <- mapM (checkMethodDef className methodTys'') methods - let (idxs, methods') = unzip $ sortOn fst $ methodsChecked - forM_ (repeated idxs) \i -> - throw sid $ DuplicateMethod $ pprint (methodNames!!i) - forM_ ([0..(length methodTys''-1)] `listDiff` idxs) \i -> - throw sid $ MissingMethod $ pprint (methodNames!!i) - return $ InstanceBody superclassDicts methods' - -superclassDictTys :: Nest CBinder o o' -> InfererM i o [CType o] -superclassDictTys Empty = return [] -superclassDictTys (Nest b bs) = do - Abs bs' UnitE <- liftHoistExcept rootSrcId $ hoist b $ Abs bs UnitE - (binderType b:) <$> superclassDictTys bs' - -checkMethodDef :: ClassName o -> [CorePiType o] -> UMethodDef i -> InfererM i o (Int, CAtom o) -checkMethodDef className methodTys (WithSrcE sid m) = do - UMethodDef ~(InternalName _ sourceName v) rhs <- return m - MethodBinding className' i <- renameM v >>= lookupEnv - when (className /= className') do - ClassBinding classDef <- lookupEnv className - throw sid $ NotAMethod (pprint sourceName) (pprint $ getSourceName classDef) - (i,) <$> toAtom <$> Lam <$> checkULam sid rhs (methodTys !! i) - -type CaseAltIndex = Int - -checkCaseAlt :: Emits o => RequiredTy o -> CType o -> UAlt i -> InfererM i o (IndexedAlt o) -checkCaseAlt reqTy scrutineeTy (UAlt pat body) = do - alt <- checkCasePat pat scrutineeTy do - withBlockDecls body \result -> checkOrInfer (sink reqTy) result - idx <- getCaseAltIndex pat - return $ IndexedAlt idx alt - -getCaseAltIndex :: UPat i i' -> InfererM i o CaseAltIndex -getCaseAltIndex (WithSrcB sid pat) = case pat of - UPatCon ~(InternalName _ _ conName) _ -> do - (_, con) <- renameM conName >>= lookupDataCon - return con - _ -> throw sid IllFormedCasePattern - -checkCasePat - :: Emits o - => UPat i i' -> CType o - -> (forall o'. (Emits o', Ext o o') => InfererM i' o' (CAtom o')) - -> InfererM i o (Alt o) -checkCasePat (WithSrcB sid pat) scrutineeTy cont = case pat of - UPatCon ~(InternalName _ _ conName) ps -> do - (dataDefName, con) <- renameM conName >>= lookupDataCon - tyConDef <- lookupTyCon dataDefName - params <- inferParams sid scrutineeTy dataDefName - ADTCons cons <- instantiateTyConDef tyConDef params - DataConDef _ _ repTy idxs <- return $ cons !! con - when (length idxs /= nestLength ps) $ throw sid $ PatternArityErr (length idxs) (nestLength ps) - withFreshBinderInf noHint Explicit repTy \b -> Abs b <$> do - buildBlock do - args <- forM idxs \projs -> do - emitToVar =<< applyProjectionsReduced (init projs) (sink $ toAtom $ binderVar b) - bindLetPats ps args $ cont - _ -> throw sid IllFormedCasePattern - -inferParams :: Emits o => SrcId -> CType o -> TyConName o -> InfererM i o (TyConParams o) -inferParams sid ty dataDefName = do - TyConDef sourceName paramExpls paramBs _ <- lookupTyCon dataDefName - let inferenceExpls = paramExpls <&> \case - Explicit -> Inferred Nothing Unify - expl -> expl - paramBsAbs <- buildConstraints (Abs paramBs UnitE) \params _ -> do - let ty' = toType $ UserADTType sourceName (sink dataDefName) $ TyConParams paramExpls params - return [TypeConstraint sid (sink ty) ty'] - args <- inferMixedArgs sid sourceName inferenceExpls paramBsAbs emptyMixedArgs - return $ TyConParams paramExpls args - -bindLetPats - :: (Emits o, HasNamesE e) - => Nest UPat i i' -> [CAtomVar o] - -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) - -> InfererM i o (e o) -bindLetPats Empty [] cont = getDistinct >>= \Distinct -> cont -bindLetPats (Nest p ps) (x:xs) cont = bindLetPat p x $ bindLetPats ps (sink <$> xs) cont -bindLetPats _ _ _ = error "mismatched number of args" - -bindLetPat - :: (Emits o, HasNamesE e) - => UPat i i' -> CAtomVar o - -> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o')) - -> InfererM i o (e o) -bindLetPat (WithSrcB sid pat) v cont = emitExprType sid (getType v) >> case pat of - UPatBinder b -> getDistinct >>= \Distinct -> extendSubst (b @> atomVarName v) cont - UPatProd ps -> do - let n = nestLength ps - case getType v of - TyCon (ProdType ts) | length ts == n -> return () - ty -> throw sid $ PatTypeErr "product type" (pprint ty) - xs <- forM (iota n) \i -> proj i (toAtom v) >>= emitInline - bindLetPats ps xs cont - UPatDepPair (PairB p1 p2) -> do - case getType v of - TyCon (DepPairTy _) -> return () - ty -> throw sid $ PatTypeErr "dependent pair" (pprint ty) - -- XXX: we're careful here to reduce the projection because of the dependent - -- types. We do the same in the `UPatCon` case. - x1 <- reduceProj 0 (toAtom v) >>= emitInline - bindLetPat p1 x1 do - x2 <- getSnd (sink $ toAtom v) >>= emitInline - bindLetPat p2 x2 do - cont - UPatCon ~(InternalName _ _ conName) ps -> do - (dataDefName, _) <- lookupDataCon =<< renameM conName - TyConDef _ _ _ cons <- lookupTyCon dataDefName - case cons of - ADTCons [DataConDef _ _ _ idxss] -> do - when (length idxss /= nestLength ps) $ - throw sid $ PatternArityErr (length idxss) (nestLength ps) - void $ inferParams sid (getType $ toAtom v) dataDefName - xs <- forM idxss \idxs -> applyProjectionsReduced idxs (toAtom v) >>= emitInline - bindLetPats ps xs cont - _ -> throw sid SumTypeCantFail - UPatTable ps -> do - let n = fromIntegral (nestLength ps) :: Word32 - case getType v of - TyCon (TabPi (TabPiType _ (_:>FinConst n') _)) | n == n' -> return () - ty -> throw sid $ PatTypeErr ("Fin " ++ show n ++ " table") (pprint ty) - xs <- forM [0 .. n - 1] \i -> do - emitToVar =<< mkTabApp (toAtom v) (toAtom $ NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i)) - bindLetPats ps xs cont - where - emitInline :: Emits n => CAtom n -> InfererM i n (AtomVar n) - emitInline atom = emitDecl noHint InlineLet $ Atom atom - -checkUType :: UType i -> InfererM i o (CType o) -checkUType t = withReducibleEmissions (getSrcId t) msg do - topDownType t - where msg = CantReduceType $ pprint t - -inferTabCon :: forall i o. Emits o => SrcId -> [UExpr i] -> InfererM i o (CAtom o) -inferTabCon sid xs = do - let n = fromIntegral (length xs) :: Word32 - let finTy = FinConst n - elemTy <- case xs of - [] -> throw sid InferEmptyTable - x:_ -> getType <$> bottomUp x - ixTy <- asIxType sid finTy - let tabTy = ixTy ==> elemTy - xs' <- forM xs \x -> topDown elemTy x - emit $ TabCon tabTy xs' - -checkTabCon :: forall i o. Emits o => TabPiType o -> SrcId -> [UExpr i] -> InfererM i o (CAtom o) -checkTabCon tabTy@(TabPiType _ b elemTy) sid xs = do - let n = fromIntegral (length xs) :: Word32 - let finTy = FinConst n - expectEq sid (binderType b) finTy - xs' <- forM (enumerate xs) \(i, x) -> do - let i' = toAtom (NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i)) :: CAtom o - elemTy' <- applySubst (b@>SubstVal i') elemTy - topDown elemTy' x - emit $ TabCon (TyCon (TabPi tabTy)) xs' - -getIxDict :: SrcId -> CType o -> InfererM i o (IxDict o) -getIxDict sid t = fromJust <$> toMaybeDict <$> trySynthTerm sid (toType $ IxDictType t) Full - -asIxType :: SrcId -> CType o -> InfererM i o (IxType o) -asIxType sid ty = IxType ty <$> getIxDict sid ty - --- === Solver === - --- TODO: put this pattern and friends in the Name library? Don't really want to --- have to think about `eqNameColorRep` just to implement a partial map. -lookupSolverSubst :: forall n. SolverSubst n -> Name n -> AtomSubstVal n -lookupSolverSubst (SolverSubst m) name = undefined --- lookupSolverSubst (SolverSubst m) name = --- case eqColorRep of --- Nothing -> Rename name --- Just (ColorsEqual :: ColorsEqual c (AtomNameC))-> case M.lookup name m of --- Nothing -> Rename name --- Just sol -> SubstVal sol - -applyConstraint :: Constraint o -> SolverM i o () -applyConstraint = \case - TypeConstraint sid t1 t2 -> constrainEq sid t1 t2 - -constrainEq :: ToAtom e => SrcId -> e o -> e o -> SolverM i o () -constrainEq sid t1 t2 = do - t1' <- zonk $ toAtom t1 - t2' <- zonk $ toAtom t2 - msg <- liftEnvReaderM do - ab <- renameForPrinting $ PairE t1' t2' - return $ canonicalizeForPrinting ab \(Abs infVars (PairE t1Pretty t2Pretty)) -> - UnificationFailure (pprint t1Pretty) (pprint t2Pretty) (nestToList pprint infVars) - void $ searchFailureAsTypeErr sid msg $ unify t1' t2' - -searchFailureAsTypeErr :: ToErr e => SrcId -> e -> SolverM i n a -> SolverM i n a -searchFailureAsTypeErr sid msg cont = cont <|> throw sid msg -{-# INLINE searchFailureAsTypeErr #-} - -class AlphaEqE e => Unifiable (e::E) where - unify :: e n -> e n -> SolverM i n () - -instance Unifiable (Stuck) where - unify s1 s2 = do - x1 <- zonkStuck s1 - x2 <- zonkStuck s2 - case (x1, x2) of - (Con c, Con c') -> unify c c' - (Stuck _ s, Stuck _ s') -> unifyStuckZonked s s' - (Stuck _ s, Con c) -> unifyStuckConZonked s c - (Con c, Stuck _ s) -> unifyStuckConZonked s c - --- assumes both `CStuck` args are zonked -unifyStuckZonked :: CStuck n -> CStuck n -> SolverM i n () -unifyStuckZonked s1 s2 = do - x1 <- mkStuck s1 - x2 <- mkStuck s2 - case (s1, s2) of - (Var v1, Var v2) -> do - if atomVarName v1 == atomVarName v2 - then return () - else extendSolution v2 x1 <|> extendSolution v1 x2 - (_, Var v2) -> extendSolution v2 x1 - (Var v1, _) -> extendSolution v1 x2 - (_, _) -> unifyEq s1 s2 - -unifyStuckConZonked :: CStuck n -> Con n -> SolverM i n () -unifyStuckConZonked s x = case s of - Var v -> extendSolution v (Con x) - _ -> empty - -unifyStuckCon :: CStuck n -> Con n -> SolverM i n () -unifyStuckCon s con = do - x <- zonkStuck s - case x of - Stuck _ s' -> unifyStuckConZonked s' con - Con con' -> unify con' con - -instance Unifiable (Atom) where - unify (Con c) (Con c') = unify c c' - unify (Stuck _ s) (Stuck _ s') = unify s s' - unify (Stuck _ s) (Con c) = unifyStuckCon s c - unify (Con c) (Stuck _ s) = unifyStuckCon s c - --- TODO: do this directly rather than going via `CAtom` using `Type`. We just --- need to deal with `Stuck`. -instance Unifiable (Type) where - unify (TyCon c) (TyCon c') = unify c c' - unify (StuckTy _ s) (StuckTy _ s') = unify s s' - unify (StuckTy _ s) (TyCon c) = unifyStuckCon s (TyConAtom c) - unify (TyCon c) (StuckTy _ s) = unifyStuckCon s (TyConAtom c) - -instance Unifiable (Con) where - unify e1 e2 = case e1 of - ( Lit x ) -> do - { Lit x' <- matchit; guard (x == x')} - ( ProdCon xs ) -> do - { ProdCon xs' <- matchit; unifyLists xs xs'} - ( SumCon ts i x ) -> do - { SumCon ts' i' x' <- matchit; unifyLists ts ts'; guard (i==i'); unify x x'} - ( DepPair t x y ) -> do - { DepPair t' x' y' <- matchit; unify t t'; unify x x'; unify y y'} - ( Lam lam ) -> do - { Lam lam' <- matchit; unifyEq lam lam'} - ( NewtypeCon con x ) -> do - { NewtypeCon con' x' <- matchit; unifyEq con con'; unify x x'} - ( TyConAtom t ) -> do - { TyConAtom t' <- matchit; unify t t'} - ( DictConAtom d ) -> do - { DictConAtom d' <- matchit; unifyEq d d'} - where matchit = return e2 - -instance Unifiable (TyCon) where - unify t1 t2 = case t1 of - ( BaseType b ) -> do - { BaseType b' <- matchit; guard $ b == b'} - ( Kind k ) -> do - { Kind k' <- matchit; guard $ k == k' } - ( Pi piTy ) -> do - { Pi piTy' <- matchit; unify piTy piTy'} - ( TabPi piTy) -> do - { TabPi piTy' <- matchit; unify piTy piTy'} - ( DictTy d ) -> do - { DictTy d' <- matchit; unify d d'} - ( NewtypeTyCon con ) -> do - { NewtypeTyCon con' <- matchit; unify con con'} - ( SumType ts ) -> do - { SumType ts' <- matchit; unifyLists ts ts'} - ( ProdType ts ) -> do - { ProdType ts' <- matchit; unifyLists ts ts'} - ( RefType t ) -> do - { RefType t' <- matchit; unify t t'} - ( DepPairTy t ) -> do - { DepPairTy t' <- matchit; unify t t'} - where matchit = return t2 - -unifyLists :: Unifiable e => [e n] -> [e n] -> SolverM i n () -unifyLists [] [] = return () -unifyLists (x:xs) (y:ys) = unify x y >> unifyLists xs ys -unifyLists _ _ = empty - -instance Unifiable DictType where - unify d1 d2 = case d1 of - ( DictType _ c params )-> do - { DictType _ c' params' <- matchit; guard (c == c'); unifyLists params params'} - ( IxDictType t ) -> do - { IxDictType t' <- matchit; unify t t'} - where matchit = return d2 - {-# INLINE unify #-} - -instance Unifiable NewtypeTyCon where - unify e1 e2 = case e1 of - ( Nat ) -> do - { Nat <- matchit; return ()} - ( Fin n ) -> do - { Fin n' <- matchit; unify n n'} - ( UserADTType _ c params ) -> do - { UserADTType _ c' params' <- matchit; guard (c == c') >> unify params params' } - where matchit = return e2 - -instance Unifiable (IxType) where - -- We ignore the dictionaries because we assume coherence - unify (IxType t _) (IxType t' _) = unify t t' - -instance Unifiable TyConParams where - -- We ignore the dictionaries because we assume coherence - unify ps ps' = zipWithM_ unify (ignoreSynthParams ps) (ignoreSynthParams ps') - -unifyEq :: AlphaEqE e => e n -> e n -> SolverM i n () -unifyEq e1 e2 = guard =<< alphaEq e1 e2 -{-# INLINE unifyEq #-} - -instance Unifiable CorePiType where - unify (CorePiType appExpl1 expls1 bsTop1 effTy1) - (CorePiType appExpl2 expls2 bsTop2 effTy2) = do - unless (appExpl1 == appExpl2) empty - unless (expls1 == expls2) empty - go (Abs bsTop1 effTy1) (Abs bsTop2 effTy2) - where - go :: Abs (Nest CBinder) (Type) n - -> Abs (Nest CBinder) (Type) n - -> SolverM i n () - go (Abs Empty t1) (Abs Empty t2) = unify t1 t2 - go (Abs (Nest (b1:>t1) bs1) rest1) - (Abs (Nest (b2:>t2) bs2) rest2) = do - unify t1 t2 - void $ withFreshSkolemName t1 \v -> do - ab1 <- zonk =<< applyRename (b1@>atomVarName v) (Abs bs1 rest1) - ab2 <- zonk =<< applyRename (b2@>atomVarName v) (Abs bs2 rest2) - go ab1 ab2 - return UnitE - go _ _ = empty - -instance Unifiable (TabPiType) where - unify (TabPiType _ b1 ty1) (TabPiType _ b2 ty2) = - unify (Abs b1 ty1) (Abs b2 ty2) - -instance Unifiable (DepPairType) where - unify (DepPairType expl1 b1 rhs1) (DepPairType expl2 b2 rhs2) = do - guard $ expl1 == expl2 - unify (Abs b1 rhs1) (Abs b2 rhs2) - -instance Unifiable (Abs CBinder CType) where - unify (Abs b1 ty1) (Abs b2 ty2) = do - let ann1 = binderType b1 - let ann2 = binderType b2 - unify ann1 ann2 - void $ withFreshSkolemName ann1 \v -> do - ty1' <- applyRename (b1@>atomVarName v) ty1 - ty2' <- applyRename (b2@>atomVarName v) ty2 - unify ty1' ty2' - return UnitE - -withFreshSkolemName - :: Zonkable e => CType o - -> (forall o'. DExt o o' => CAtomVar o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -withFreshSkolemName ty cont = diffStateT1 \s -> do - withFreshBinder "skol" (SkolemBound ty) \b -> do - (ans, diff) <- runDiffStateT1 (sink s) do - v <- toAtomVar $ binderName b - ans <- cont v >>= zonk - case hoist b ans of - HoistSuccess ans' -> return ans' - HoistFailure _ -> empty - case hoist b diff of - HoistSuccess diff' -> return (ans, diff') - HoistFailure _ -> empty -{-# INLINE withFreshSkolemName #-} - -extendSolution :: CAtomVar n -> CAtom n -> SolverM i n () -extendSolution (AtomVar v _) t = - isUnificationName v >>= \case - True -> do - when (v `isFreeIn` t) solverFail -- occurs check - -- When we unify under a pi binder we replace its occurrences with a - -- skolem variable. We don't want to unify with terms containing these - -- variables because that would mean inferring dependence, which is a can - -- of worms. - forM_ (freeVarsList t) \fv -> - whenM (isSkolemName fv) solverFail -- can't unify with skolems - addConstraint v t - False -> empty - -isUnificationName :: EnvReader m => CAtomName n -> m n Bool -isUnificationName v = lookupEnv v >>= \case - AtomNameBinding (SolverBound (InfVarBound _)) -> return True - _ -> return False -{-# INLINE isUnificationName #-} - -isSolverName :: EnvReader m => CAtomName n -> m n Bool -isSolverName v = lookupEnv v >>= \case - AtomNameBinding (SolverBound _) -> return True - _ -> return False - - -isSkolemName :: EnvReader m => CAtomName n -> m n Bool -isSkolemName v = lookupEnv v >>= \case - AtomNameBinding (SolverBound (SkolemBound _)) -> return True - _ -> return False -{-# INLINE isSkolemName #-} - -renameForPrinting :: EnvReader m - => (PairE CAtom CAtom n) -> m n (Abs (Nest (AtomNameBinder)) (PairE CAtom CAtom) n) -renameForPrinting e = do - infVars <- filterM isSolverName $ freeVarsList e - let ab = abstractFreeVarsNoAnn infVars e - let hints = take (length infVars) $ map getNameHint $ - map (:[]) ['a'..'z'] ++ map show [(0::Int)..] - Distinct <- getDistinct - scope <- toScope <$> unsafeGetEnv -- TODO: figure out how to do it safely - return $ withManyFresh hints scope \bs' -> - runScopeReaderM (scope `extendOutMap` toScopeFrag bs') do - Abs bsAbs eAbs <- sinkM ab - e' <- applyRename (bsAbs@@>nestToNames bs') eAbs - return $ Abs bs' e' - --- === builder and type querying helpers === - -makeStructRepVal :: (Fallible1 m, EnvReader m) => TyConName n -> [CAtom n] -> m n (CAtom n) -makeStructRepVal tyConName args = do - TyConDef _ _ _ (StructFields fields) <- lookupTyCon tyConName - case fields of - [_] -> case args of - [arg] -> return arg - _ -> error "wrong number of args" - _ -> return $ Con $ ProdCon args - --- === dictionary synthesis === - --- Given a simplified dict (an Atom of type `DictTy _` in the --- post-simplification IR), and a requested, more general, dict type, generalize --- the dict to match the more general type. This is only possible because we --- require that instances are polymorphic in data-role parameters. It would be --- valid to implement `generalizeDict` by re-synthesizing the whole dictionary, --- but we know that the derivation tree has to be the same, so we take the --- shortcut of just generalizing the data parameters. -generalizeDict :: EnvReader m => CType n -> CDict n -> m n (CDict n) -generalizeDict ty dict = do - result <- liftEnvReaderM $ liftM fst $ liftInfererMPure $ generalizeDictRec ty dict - case result of - Failure e -> error $ "Failed to generalize " ++ pprint dict - ++ " to " ++ show ty ++ " because " ++ pprint e - Success ans -> return ans - -generalizeDictRec :: CType n -> CDict n -> InfererM i n (CDict n) -generalizeDictRec targetTy (DictCon dict) = case dict of - InstanceDict _ instanceName args -> do - InstanceDef _ _ bs _ _ <- lookupInstanceDef instanceName - liftSolverM $ generalizeInstanceArgs bs args \args' -> do - d <- mkInstanceDict (sink instanceName) args' - -- We use rootSrcId here because we only call this after type inference so - -- precise source info isn't needed. - constrainEq rootSrcId (sink $ toAtom targetTy) (toAtom $ getType d) - return d - IxFin _ -> do - TyCon (DictTy (IxDictType (TyCon (NewtypeTyCon (Fin n))))) <- return targetTy - return $ DictCon $ IxFin n - IxRawFin _ -> error "not a simplified dict" -generalizeDictRec _ _ = error "not a simplified dict" - -data ParamRole = TypeParam | DictParam | DataParam deriving (Show, Generic, Eq) - -inferRoleFromType :: EnvReader m => CType n -> m n ParamRole -inferRoleFromType = undefined -- TODO - -generalizeInstanceArgs - :: Zonkable e => Nest CBinder o any -> [CAtom o] - -> (forall o'. DExt o o' => [CAtom o'] -> SolverM i o' (e o')) - -> SolverM i o (e o) -generalizeInstanceArgs Empty [] cont = withDistinct $ cont [] -generalizeInstanceArgs (Nest (b:>ty) bs) (arg:args) cont = do - role <- inferRoleFromType ty - generalizeInstanceArg role ty arg \arg' -> do - Abs bs' UnitE <- applySubst (b@>SubstVal arg') (Abs bs UnitE) - generalizeInstanceArgs bs' (sink <$> args) \args' -> - cont $ sink arg' : args' -generalizeInstanceArgs _ _ _ = error "zip error" - -generalizeInstanceArg - :: Zonkable e => ParamRole -> CType o -> CAtom o - -> (forall o'. DExt o o' => CAtom o' -> SolverM i o' (e o')) - -> SolverM i o (e o) -generalizeInstanceArg role ty arg cont = case role of - -- XXX: for `TypeParam` we can just emit a fresh inference name rather than - -- traversing the whole type like we do in `Generalize.hs`. The reason is - -- that it's valid to implement `generalizeDict` by synthesizing an entirely - -- fresh dictionary, and if we were to do that, we would infer this type - -- parameter exactly as we do here, using inference. - TypeParam -> withFreshUnificationVarNoEmits rootSrcId MiscInfVar (toType $ Kind TypeKind) \v -> cont $ toAtom v - DictParam -> withFreshDictVarNoEmits ty ( - \ty' -> case toMaybeDict (sink arg) of - Just d -> liftM toAtom $ lift11 $ generalizeDictRec ty' d - _ -> error "not a dict") cont - DataParam -> withFreshUnificationVarNoEmits rootSrcId MiscInfVar ty \v -> cont $ toAtom v - -emitInstanceDef :: (Mut n, TopBuilder m) => InstanceDef n -> m n (Name n) -emitInstanceDef instanceDef@(InstanceDef className _ _ _ _) = do - ty <- getInstanceType instanceDef - emitBinding (getNameHint className) $ InstanceBinding instanceDef ty - --- main entrypoint to dictionary synthesizer -trySynthTerm :: SrcId -> CType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n) -trySynthTerm sid ty reqMethodAccess = do - hasInferenceVars ty >>= \case - True -> throw sid $ CantSynthInfVars $ pprint ty - False -> withVoidSubst do - synthTy <- liftExcept $ typeAsSynthType sid ty - synthTerm sid synthTy reqMethodAccess - <|> (throw sid $ CantSynthDict $ pprint ty) -{-# SCC trySynthTerm #-} - -hasInferenceVars :: (EnvReader m, HoistableE e) => e n -> m n Bool -hasInferenceVars e = liftEnvReaderM $ anyInferenceVars $ freeVarsList e -{-# INLINE hasInferenceVars #-} - -anyInferenceVars :: [CAtomName n] -> EnvReaderM n Bool -anyInferenceVars = \case - [] -> return False - (v:vs) -> isSolverName v >>= \case - True -> return True - False -> anyInferenceVars vs - -type SynthAtom = CAtom -type SynthPiType n = ([Explicitness], Abs (Nest CBinder) DictType n) -data SynthType n = - SynthDictType (DictType n) - | SynthPiType (SynthPiType n) - deriving (Show, Generic) - -data Givens n = Givens { fromGivens :: HM.HashMap (EKey SynthType n) (SynthAtom n) } - -getGivens :: InfererM i o (Givens o) -getGivens = givens <$> getInfState - -withGivens :: Givens o -> InfererM i o a -> InfererM i o a -withGivens givens cont = withInfState (\s -> s { givens = givens }) cont - -extendGivens :: [SynthAtom o] -> InfererM i o a -> InfererM i o a -extendGivens newGivens cont = do - prevGivens <- getGivens - finalGivens <- getSuperclassClosure prevGivens newGivens - withGivens finalGivens cont -{-# INLINE extendGivens #-} - -getSynthType :: SynthAtom n -> SynthType n -getSynthType x = ignoreExcept $ typeAsSynthType rootSrcId (getType x) -{-# INLINE getSynthType #-} - -typeAsSynthType :: SrcId -> CType n -> Except (SynthType n) -typeAsSynthType sid = \case - TyCon (DictTy dictTy) -> return $ SynthDictType dictTy - TyCon (Pi (CorePiType ImplicitApp expls bs (TyCon (DictTy d)))) -> - return $ SynthPiType (expls, Abs bs d) - ty -> Failure $ toErr sid $ NotASynthType $ pprint ty -{-# SCC typeAsSynthType #-} - -getSuperclassClosure :: EnvReader m => Givens n -> [SynthAtom n] -> m n (Givens n) -getSuperclassClosure givens newGivens = do - Distinct <- getDistinct - env <- unsafeGetEnv - return $ getSuperclassClosurePure env givens newGivens -{-# INLINE getSuperclassClosure #-} - -getSuperclassClosurePure :: Distinct n => Env n -> Givens n -> [SynthAtom n] -> Givens n -getSuperclassClosurePure env givens newGivens = - snd $ runState (runEnvReaderT env (mapM_ visitGiven newGivens)) givens - where - visitGiven :: SynthAtom n -> EnvReaderT (State (Givens n)) n () - visitGiven x = alreadyVisited x >>= \case - True -> return () - False -> do - markAsVisited x - parents <- getDirectSuperclasses x - mapM_ visitGiven parents - - alreadyVisited :: SynthAtom n -> EnvReaderT (State (Givens n)) n Bool - alreadyVisited x = do - Givens m <- get - ty <- return $ getSynthType x - return $ EKey ty `HM.member` m - - markAsVisited :: SynthAtom n -> EnvReaderT (State (Givens n)) n () - markAsVisited x = do - ty <- return $ getSynthType x - modify \(Givens m) -> Givens $ HM.insert (EKey ty) x m - - getDirectSuperclasses :: SynthAtom n -> EnvReaderT (State (Givens n)) n [SynthAtom n] - getDirectSuperclasses synthExpr = do - synthTy <- return $ getSynthType synthExpr - superclasses <- case synthTy of - SynthPiType _ -> return [] - SynthDictType dTy -> getSuperclassTys dTy - forM (enumerate superclasses) \(i, _) -> do - reduceSuperclassProj i $ fromJust (toMaybeDict synthExpr) - -synthTerm :: SrcId -> SynthType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n) -synthTerm sid targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of - SynthPiType (expls, ab) -> do - ab' <- withFreshBindersInf expls ab \bs' targetTy' -> do - Abs bs' <$> synthTerm sid (SynthDictType targetTy') reqMethodAccess - Abs bs' synthExpr <- return ab' - let piTy = CorePiType ImplicitApp expls bs' (getType synthExpr) - let lamExpr = LamExpr bs' (Atom synthExpr) - return $ toAtom $ Lam $ CoreLamExpr piTy lamExpr - SynthDictType dictTy -> case dictTy of - IxDictType (TyCon (NewtypeTyCon (Fin n))) -> return $ toAtom $ IxFin n - _ -> do - dict <- synthDictFromInstance sid dictTy <|> synthDictFromGiven sid dictTy - case dict of - Con (DictConAtom (InstanceDict _ instanceName _)) -> do - isReqMethodAccessAllowed <- reqMethodAccess `isMethodAccessAllowedBy` instanceName - if isReqMethodAccessAllowed - then return dict - else empty - _ -> return dict -{-# SCC synthTerm #-} - -isMethodAccessAllowedBy :: EnvReader m => RequiredMethodAccess -> InstanceName n -> m n Bool -isMethodAccessAllowedBy access instanceName = do - InstanceDef className _ _ _ (InstanceBody _ methods) <- lookupInstanceDef instanceName - let numInstanceMethods = length methods - ClassDef _ _ _ _ _ _ _ methodTys <- lookupClassDef className - let numClassMethods = length methodTys - case access of - Full -> return $ numClassMethods == numInstanceMethods - Partial numReqMethods -> return $ numReqMethods <= numInstanceMethods - -synthDictFromGiven :: SrcId -> DictType n -> InfererM i n (SynthAtom n) -synthDictFromGiven sid targetTy = do - givens <- ((HM.elems . fromGivens) <$> getGivens) - asum $ givens <&> \given -> do - case getSynthType given of - SynthDictType givenDictTy -> do - guard =<< alphaEq targetTy givenDictTy - return given - SynthPiType givenPiTy -> typeErrAsSearchFailure do - args <- instantiateSynthArgs sid targetTy givenPiTy - reduceInstantiateGiven given args - -synthDictFromInstance :: SrcId -> DictType n -> InfererM i n (SynthAtom n) -synthDictFromInstance sid targetTy = do - instances <- getInstanceDicts targetTy - asum $ instances <&> \candidate -> typeErrAsSearchFailure do - CorePiType _ expls bs (TyCon (DictTy candidateTy)) <- lookupInstanceTy candidate - args <- instantiateSynthArgs sid targetTy (expls, Abs bs candidateTy) - return $ toAtom $ InstanceDict (toType targetTy) candidate args - -getInstanceDicts :: EnvReader m => DictType n -> m n [InstanceName n] -getInstanceDicts dictTy = do - env <- withEnv (envSynthCandidates . moduleEnv) - case dictTy of - DictType _ name _ -> return $ M.findWithDefault [] name $ instanceDicts env - IxDictType _ -> return $ ixInstances env - -addInstanceSynthCandidate :: TopBuilder m => ClassName n -> Maybe BuiltinClassName -> InstanceName n -> m n () -addInstanceSynthCandidate className maybeBuiltin instanceName = do - sc <- return case maybeBuiltin of - Nothing -> mempty {instanceDicts = M.singleton className [instanceName] } - Just Ix -> mempty {ixInstances = [instanceName]} - emitLocalModuleEnv $ mempty {envSynthCandidates = sc} - -instantiateSynthArgs :: SrcId -> DictType n -> SynthPiType n -> InfererM i n [CAtom n] -instantiateSynthArgs sid target (expls, synthPiTy) = do - liftM fromListE $ withReducibleEmissions sid CantReduceDict do - bsConstrained <- buildConstraints (sink synthPiTy) \_ resultTy -> do - return [TypeConstraint sid (TyCon $ DictTy $ sink target) (TyCon $ DictTy resultTy)] - ListE <$> inferMixedArgs sid "dict" expls bsConstrained emptyMixedArgs - -emptyMixedArgs :: MixedArgs (CAtom n) -emptyMixedArgs = ([], []) - -typeErrAsSearchFailure :: InfererM i n a -> InfererM i n a -typeErrAsSearchFailure cont = cont `catchErr` \case - TypeErr _ _ -> empty - e -> throwErr e - -instance GenericE Givens where - type RepE Givens = HashMapE (EKey SynthType) SynthAtom - fromE (Givens m) = HashMapE m - {-# INLINE fromE #-} - toE (HashMapE m) = Givens m - {-# INLINE toE #-} - -instance SinkableE Givens where - --- === Inference-specific builder patterns === - -type WithExpl = WithAttrB Explicitness - -buildBlockInfWithRecon - :: HasNamesE e - => (forall l. (Emits l, DExt n l) => InfererM i l (e l)) - -> InfererM i n (PairE CExpr (ReconAbs e) n) -buildBlockInfWithRecon cont = do - ab <- buildScoped cont - (block, recon) <- liftEnvReaderM $ refreshAbs ab \decls result -> do - (newResult, recon) <- telescopicCapture decls result - return (Abs decls newResult, recon) - block' <- mkBlock block - return $ PairE block' recon -{-# INLINE buildBlockInfWithRecon #-} - --- === IFunType === - -asFFIFunType :: EnvReader m => CType n -> m n (Maybe (IFunType, CorePiType n)) -asFFIFunType ty = return do - TyCon (Pi piTy) <- return ty - impTy <- checkFFIFunTypeM piTy - return (impTy, piTy) - -checkFFIFunTypeM :: Fallible m => CorePiType n -> m IFunType -checkFFIFunTypeM (CorePiType appExpl (_:expls) (Nest b bs) ty) = do - argTy <- checkScalar $ binderType b - case bs of - Empty -> do - resultTys <- checkScalarOrPairType ty - let cc = case length resultTys of - 0 -> error "Not implemented" - 1 -> FFICC - _ -> FFIMultiResultCC - return $ IFunType cc [argTy] resultTys - Nest b' rest -> do - let naryPiRest = CorePiType appExpl expls (Nest b' rest) ty - IFunType cc argTys resultTys <- checkFFIFunTypeM naryPiRest - return $ IFunType cc (argTy:argTys) resultTys -checkFFIFunTypeM _ = error "expected at least one argument" - -checkScalar :: Fallible m => Type n -> m BaseType -checkScalar (BaseTy ty) = return ty -checkScalar ty = throw rootSrcId $ FFIArgTyNotScalar $ pprint ty - -checkScalarOrPairType :: Fallible m => Type n -> m [BaseType] -checkScalarOrPairType (PairTy a b) = do - tys1 <- checkScalarOrPairType a - tys2 <- checkScalarOrPairType b - return $ tys1 ++ tys2 -checkScalarOrPairType (BaseTy ty) = return [ty] -checkScalarOrPairType ty = throw rootSrcId $ FFIResultTyErr $ pprint ty - --- === instances === - -instance DiffStateE SolverSubst SolverDiff where - updateDiffStateE :: forall n. Distinct n => Env n -> SolverSubst n -> SolverDiff n -> SolverSubst n - updateDiffStateE _ initState (SolverDiff (RListE diffs)) = foldl update' initState (unsnoc diffs) - where - update' :: Distinct n => SolverSubst n -> Solution n -> SolverSubst n - update' (SolverSubst subst) (PairE v x) = SolverSubst $ M.insert v x subst - -instance SinkableE InfState where sinkingProofE _ = todoSinkableProof - -instance GenericE SigmaAtom where - type RepE SigmaAtom = EitherE3 (LiftE (Maybe SourceName) `PairE` CAtom) - (LiftE SourceName `PairE` CType `PairE` UVar) - (CType `PairE` CAtom `PairE` ListE CAtom) - fromE = \case - SigmaAtom x y -> Case0 $ LiftE x `PairE` y - SigmaUVar x y z -> Case1 $ LiftE x `PairE` y `PairE` z - SigmaPartialApp x y z -> Case2 $ x `PairE` y `PairE` ListE z - {-# INLINE fromE #-} - - toE = \case - Case0 (LiftE x `PairE` y) -> SigmaAtom x y - Case1 (LiftE x `PairE` y `PairE` z) -> SigmaUVar x y z - Case2 (x `PairE` y `PairE` ListE z) -> SigmaPartialApp x y z - _ -> error "impossible" - {-# INLINE toE #-} - -instance RenameE SigmaAtom -instance HoistableE SigmaAtom -instance SinkableE SigmaAtom - -instance SubstE AtomSubstVal SigmaAtom where - substE env (SigmaAtom sn x) = SigmaAtom sn $ substE env x - substE env (SigmaUVar sn ty uvar) = undefined - -- UAtomVar v -> substE env $ SigmaAtom (Just sn) $ toAtom (AtomVar v ty) - -- UTyConVar v -> SigmaUVar sn ty' $ UTyConVar $ substE env v - -- UDataConVar v -> SigmaUVar sn ty' $ UDataConVar $ substE env v - -- UPunVar v -> SigmaUVar sn ty' $ UPunVar $ substE env v - -- UClassVar v -> SigmaUVar sn ty' $ UClassVar $ substE env v - -- UMethodVar v -> SigmaUVar sn ty' $ UMethodVar $ substE env v - -- where ty' = substE env ty - substE env (SigmaPartialApp ty f xs) = - SigmaPartialApp (substE env ty) (substE env f) (map (substE env) xs) - -instance PrettyE e => Pretty (UDeclInferenceResult e l) where - pretty = \case - UDeclResultDone e -> pretty e - UDeclResultBindName _ block _ -> pretty block - UDeclResultBindPattern _ block _ -> pretty block - -instance SinkableE e => SinkableE (UDeclInferenceResult e) where - sinkingProofE = todoSinkableProof - -instance GenericE SynthType where - type RepE SynthType = EitherE2 DictType (PairE (LiftE [Explicitness]) (Abs (Nest CBinder) DictType)) - fromE (SynthDictType d) = Case0 d - fromE (SynthPiType (expl, t)) = Case1 (PairE (LiftE expl) t) - toE (Case0 d) = SynthDictType d - toE (Case1 (PairE (LiftE expl) t)) = SynthPiType (expl, t) - toE _ = error "impossible" - -instance AlphaEqE SynthType -instance AlphaHashableE SynthType -instance SinkableE SynthType -instance HoistableE SynthType -instance RenameE SynthType -instance SubstE AtomSubstVal SynthType - -instance GenericE Constraint where - type RepE Constraint = PairE (LiftE SrcId) (PairE CType CType) - fromE (TypeConstraint sid t1 t2) = LiftE sid `PairE` PairE t1 t2 - {-# INLINE fromE #-} - toE (LiftE sid `PairE` PairE t1 t2) = TypeConstraint sid t1 t2 - {-# INLINE toE #-} - -instance SinkableE Constraint -instance HoistableE Constraint -instance (SubstE AtomSubstVal) Constraint - -instance GenericE RequiredTy where - type RepE RequiredTy = EitherE CType UnitE - fromE (Check ty) = LeftE ty - fromE Infer = RightE UnitE - {-# INLINE fromE #-} - toE (LeftE ty) = Check ty - toE (RightE UnitE) = Infer - {-# INLINE toE #-} - -instance SinkableE RequiredTy -instance HoistableE RequiredTy -instance AlphaEqE RequiredTy -instance RenameE RequiredTy - -instance GenericE PartialType where - type RepE PartialType = EitherE PartialPiType CType - fromE (PartialType ty) = LeftE ty - fromE (FullType ty) = RightE ty - {-# INLINE fromE #-} - toE (LeftE ty) = PartialType ty - toE (RightE ty) = FullType ty - {-# INLINE toE #-} - -instance SinkableE PartialType -instance HoistableE PartialType -instance AlphaEqE PartialType -instance RenameE PartialType - -instance GenericE SolverSubst where - -- XXX: this is a bit sketchy because it's not actually bijective... - type RepE SolverSubst = ListE (PairE CAtomName CAtom) - fromE (SolverSubst m) = ListE $ map (uncurry PairE) $ M.toList m - {-# INLINE fromE #-} - toE (ListE pairs) = SolverSubst $ M.fromList $ map fromPairE pairs - {-# INLINE toE #-} - -instance SinkableE SolverSubst where -instance RenameE SolverSubst where -instance HoistableE SolverSubst - -instance GenericE PartialPiType where - type RepE PartialPiType = LiftE (AppExplicitness, [Explicitness]) `PairE` Abs (Nest CBinder) RequiredTy - fromE (PartialPiType ex exs b ty) = LiftE (ex, exs) `PairE` Abs b ty - {-# INLINE fromE #-} - toE (LiftE (ex, exs) `PairE` Abs b ty) = PartialPiType ex exs b ty - {-# INLINE toE #-} - -instance SinkableE PartialPiType -instance HoistableE PartialPiType -instance AlphaEqE PartialPiType -instance RenameE PartialPiType - --- See Note [Confuse GHC] from Simplify.hs -confuseGHC :: EnvReader m => m n (DistinctEvidence n) -confuseGHC = getDistinct -{-# INLINE confuseGHC #-} diff --git a/src/old/Subst.hs b/src/old/Subst.hs deleted file mode 100644 index 593f2a418..000000000 --- a/src/old/Subst.hs +++ /dev/null @@ -1,512 +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 - -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE UndecidableInstances #-} - -module Subst where - -import Control.Applicative -import Control.Monad.Identity -import Control.Monad.Reader -import Control.Monad.State.Strict - -import Name -import MTL1 -import Types.Core -import Types.Top -import Core -import qualified RawName as R -import QueryTypePure -import Err - --- === SubstReader class === - -class (SinkableE v, Monad2 m) => SubstReader (v::E) (m::MonadKind2) | m -> v where - getSubst :: m i o (Subst v i o) - withSubst :: Subst v i' o -> m i' o a -> m i o a - -lookupSubstM :: SubstReader v m => Name i -> m i o (v o) -lookupSubstM name = (!name) <$> getSubst - -dropSubst :: (SubstReader v m, FromName v) => m o o a -> m i o a -dropSubst cont = withSubst idSubst cont -{-# INLINE dropSubst #-} - -withVoidSubst :: (SubstReader v m, FromName v) => m VoidS o a -> m i o a -withVoidSubst cont = withSubst (newSubst absurdNameFunction) cont -{-# INLINE withVoidSubst #-} - -extendSubst :: SubstReader v m => SubstFrag v i i' o -> m i' o a -> m i o a -extendSubst frag cont = do - env <- (<>>frag) <$> getSubst - withSubst env cont -{-# INLINE extendSubst #-} - --- XXX: this only (monadically) visits each name once, even if a name has --- multiple occurrences. So don't use it to count occurrences or anything like --- that! It's not deliberate. It's just an accident of the implementation, where --- we gather the (de-duplicated) free names and then traverse them. At some --- point we may add a monadic traversal to `Subst{E,B}`, which would actually --- visit each occurrence. -traverseNames - :: forall v e m i o. - (SubstE v e, HoistableE e, SinkableE e, FromName v, EnvReader m) - => (Name i -> m o (v o)) - -> e i -> m o (e o) -traverseNames f e = do - let vs = freeVarsE e - m <- flip R.traverseWithKey (fromNameSet vs) \rawName (SubstItem d _) -> do - v' <- f (UnsafeMakeName rawName :: Name i) - return $ SubstItem d v' - fmapNamesM (applyTraversed m) e -{-# INLINE traverseNames #-} - -applyTraversed :: FromName v - => RawNameMap (SubstItem v n) -> Name i -> v n -applyTraversed m = \((UnsafeMakeName v) :: Name i) -> case R.lookup v m of - Just item -> fromSubstItem item - Nothing -> fromName $ (UnsafeMakeName v :: Name o) - -fmapNames :: (SubstE v e, Distinct o) - => Env o -> (Name i -> v o) -> e i -> e o -fmapNames env f e = substE (env, newSubst f) e -{-# INLINE fmapNames #-} - -fmapNamesM :: (SubstE v e, SinkableE e, EnvReader m) - => (Name i -> v o) - -> e i -> m o (e o) -fmapNamesM f e = do - env <- unsafeGetEnv - Distinct <- getDistinct - return $ substE (env, newSubst f) e -{-# INLINE fmapNamesM #-} - --- === type classes for traversing names === - -class FromName v => SubstE (v::E) (e::E) where - -- TODO: can't make an alias for these constraints because of impredicativity - substE :: Distinct o => (Env o, Subst v i o) -> e i -> e o - - default substE :: (GenericE e, SubstE v (RepE e), Distinct o) - => (Env o, Subst v i o) -> e i -> e o - substE env e = toE $ substE env (fromE e) - -class (FromName v, SinkableB b) => SubstB (v::E) (b::B) where - substB - :: Distinct o - => (Env o, Subst v i o) - -> b i i' - -> (forall o'. Distinct o' => (Env o', Subst v i' o') -> b o o' -> a) - -> a - - default substB - :: (GenericB b, SubstB v (RepB b)) - => Distinct o - => (Env o, Subst v i o) - -> b i i' - -> (forall o'. Distinct o' => (Env o', Subst v i' o') -> b o o' -> a) - -> a - substB env b cont = - substB env (fromB b) \env' b' -> - cont env' $ toB b' - -instance RenameE atom => RenameE (SubstVal atom) where - renameE (_, env) (Rename name) = Rename $ env ! name - renameE (scope, env) (SubstVal atom) = SubstVal $ renameE (scope, env) atom - -substM :: (SubstReader v m, EnvReader2 m, SinkableE e, SubstE v e, FromName v) - => e i -> m i o (e o) -substM e = do - subst <- getSubst - substM' subst e -{-# INLINE substM #-} - -substM' :: (EnvReader m, SinkableE e, SubstE v e, FromName v) - => Subst v i o -> e i -> m o (e o) -substM' subst e = do - case tryApplyIdentitySubst subst e of - Just e' -> return $ e' - Nothing -> do - env <- unsafeGetEnv - Distinct <- getDistinct - return $ fmapNames env (subst!) e -{-# INLINE substM' #-} - -fromConstAbs :: (BindsNames b, HoistableE e) => Abs b e n -> HoistExcept (e n) -fromConstAbs (Abs b e) = hoist b e - --- === rename-only substitutions === - -extendRenamer :: (SubstReader v m, FromName v) => SubstFrag Name i i' o -> m i' o r -> m i o r -extendRenamer frag = extendSubst (fmapSubstFrag (const fromName) frag) - -extendBinderRename - :: (SubstReader v m, FromName v, BindsAtMostOneName b, BindsOneName b') - => b i i' -> b' o o' -> m i' o' r -> m i o' r -extendBinderRename b b' cont = extendSubst (b@>fromName (binderName b')) cont -{-# INLINE extendBinderRename #-} - -applyRename - :: (ScopeReader m, RenameE e, SinkableE e) - => Ext h o => SubstFrag Name h i o -> e i -> m o (e o) -applyRename substFrag x = do - Distinct <- getDistinct - scope <- unsafeGetScope - let subst = sink idSubst <>> substFrag - case tryApplyIdentitySubst subst x of - Just x' -> return x' - Nothing -> return $ renameE (scope, newSubst (subst!)) x -{-# INLINE applyRename #-} - -renameM - :: (SubstReader Name m, ScopeReader2 m, SinkableE e, RenameE e) - => e i -> m i o (e o) -renameM e = do - env <- getSubst - case tryApplyIdentitySubst env e of - Just e' -> return $ e' - Nothing -> do - WithScope scope env' <- addScope env - sinkM $ renameE (scope, newSubst (env'!)) e -{-# INLINE renameM #-} - -renameBinders - :: (EnvExtender2 m, SubstReader Name m, RenameB b, BindsEnv b) - => b i i' - -> (forall o'. DExt o o' => b o o' -> m i' o' a) - -> m i o a -renameBinders b cont = do - ab <- renameM $ Abs b $ idSubstFrag b - refreshAbs ab \b' subst -> extendSubst subst $ cont b' -{-# INLINE renameBinders #-} - --- === various convenience utilities === - -applySubstFragPure :: (SubstE v e, SinkableE e, SinkableE v, FromName v, Ext h o, Distinct o) - => Env o -> SubstFrag v h i o -> e i -> e o -applySubstFragPure env substFrag x = do - let fullSubst = sink idSubst <>> substFrag - applySubstPure env fullSubst x - -applySubstPure :: (SubstE v e, SinkableE e, SinkableE v, FromName v, Distinct o) - => Env o -> Subst v i o -> e i -> e o -applySubstPure env subst x = do - case tryApplyIdentitySubst subst x of - Just x' -> x' - Nothing -> fmapNames env (subst !) x - -applySubst :: (EnvReader m, SubstE v e, SinkableE e, SinkableE v, FromName v) - => Ext h o - => SubstFrag v h i o -> e i -> m o (e o) -applySubst substFrag x = do - Distinct <- getDistinct - env <- unsafeGetEnv - return $ applySubstFragPure env substFrag x -{-# INLINE applySubst #-} - -applyAbs :: ( SinkableE v, SinkableE e - , FromName v, EnvReader m, BindsOneName b, SubstE v e) - => Abs b e n -> v n -> m n (e n) -applyAbs (Abs b body) x = applySubst (b@>x) body -{-# INLINE applyAbs #-} - -applyNaryAbs :: ( SinkableE v, FromName v, EnvReader m, BindsNameList b, SubstE v e - , SubstB v b, SinkableE e) - => Abs b e n -> [v n] -> m n (e n) -applyNaryAbs (Abs bs body) xs = applySubst (bs @@> xs) body -{-# INLINE applyNaryAbs #-} - -substBinders - :: ( SinkableE v, SubstE v v, EnvExtender2 m, FromName v - , SubstReader v m, SubstB v b, RenameE v, RenameB b, BindsEnv b) - => b i i' - -> (forall o'. DExt o o' => b o o' -> m i' o' a) - -> m i o a -substBinders b cont = do - substBindersFrag b \subst b' -> extendSubst subst $ cont b' -{-# INLINE substBinders #-} - -substBindersFrag - :: ( SinkableE v, SubstE v v, EnvExtender2 m, FromName v - , SubstReader v m, SubstB v b, RenameE v, RenameB b, BindsEnv b) - => b i i' - -> (forall o'. DExt o o' => SubstFrag v i i' o' -> b o o' -> m i o' a) - -> m i o a -substBindersFrag b cont = do - ab <- substM $ Abs b $ idSubstFrag b - refreshAbs ab \b' subst -> cont subst b' -{-# INLINE substBindersFrag #-} - --- === atom subst vals === - -data SubstVal (atom::E) (n::S) = - SubstVal (atom n) - | Rename (Name n) -type AtomSubstVal = SubstVal Atom - -instance FromName (SubstVal atom) where - fromName = Rename - {-# INLINE fromName #-} - -class ToSubstVal (v::E) (atom::E) where - toSubstVal :: v n -> SubstVal atom n - -instance ToSubstVal (Name::E) (atom::E) where - toSubstVal = Rename - -instance ToSubstVal (SubstVal atom) atom where - toSubstVal = id - -type AtomSubstReader v m = (SubstReader v m, FromName v, ToSubstVal v Atom) - -toAtomVar :: EnvReader m => AtomName n -> m n (AtomVar n) -toAtomVar v = do - ty <- getType <$> lookupAtomName v - return $ AtomVar v ty - -lookupAtomSubst :: (SubstReader AtomSubstVal m, EnvReader2 m) => AtomName i -> m i o (Atom o) -lookupAtomSubst v = do - lookupSubstM v >>= \case - Rename v' -> toAtom <$> toAtomVar v' - SubstVal x -> return x - -atomSubstM :: (AtomSubstReader v m, EnvReader2 m, SinkableE e, SubstE AtomSubstVal e) - => e i -> m i o (e o) -atomSubstM e = do - subst <- getSubst - let subst' = asAtomSubstValSubst subst - substM' subst' e - -asAtomSubstValSubst :: ToSubstVal v Atom => Subst v i o -> Subst AtomSubstVal i o -asAtomSubstValSubst subst = newSubst \v -> toSubstVal (subst ! v) - --- === SubstReaderT transformer === - -newtype SubstReaderT (v::E) (m::MonadKind1) (i::S) (o::S) (a:: *) = - SubstReaderT' { runSubstReaderT' :: ReaderT (Subst v i o) (m o) a } - -pattern SubstReaderT :: (Subst v i o -> m o a) -> SubstReaderT v m i o a -pattern SubstReaderT f = SubstReaderT' (ReaderT f) - -runSubstReaderT :: Subst v i o -> SubstReaderT v m i o a -> m o a -runSubstReaderT env m = runReaderT (runSubstReaderT' m) env -{-# INLINE runSubstReaderT #-} - -instance (forall n. Functor (m n)) => Functor (SubstReaderT v m i o) where - fmap f (SubstReaderT' m) = SubstReaderT' $ fmap f m - {-# INLINE fmap #-} - -instance Monad1 m => Applicative (SubstReaderT v m i o) where - pure = SubstReaderT' . pure - {-# INLINE pure #-} - liftA2 f (SubstReaderT' x) (SubstReaderT' y) = SubstReaderT' $ liftA2 f x y - {-# INLINE liftA2 #-} - (SubstReaderT' f) <*> (SubstReaderT' x) = SubstReaderT' $ f <*> x - {-# INLINE (<*>) #-} - -instance (forall n. Monad (m n)) => Monad (SubstReaderT v m i o) where - return = SubstReaderT' . return - {-# INLINE return #-} - (SubstReaderT' m) >>= f = SubstReaderT' (m >>= (runSubstReaderT' . f)) - {-# INLINE (>>=) #-} - -deriving instance (Monad1 m, MonadFail1 m) => MonadFail (SubstReaderT v m i o) -deriving instance (Monad1 m, Alternative1 m) => Alternative (SubstReaderT v m i o) -deriving instance Fallible1 m => Fallible (SubstReaderT v m i o) -deriving instance Catchable1 m => Catchable (SubstReaderT v m i o) - -type ScopedSubstReader (v::E) = SubstReaderT v (ScopeReaderT Identity) :: MonadKind2 - -liftSubstReaderT :: Monad1 m => m o a -> SubstReaderT v m i o a -liftSubstReaderT m = SubstReaderT' $ lift m -{-# INLINE liftSubstReaderT #-} - -runScopedSubstReader :: Distinct o => Scope o -> Subst v i o - -> ScopedSubstReader v i o a -> a -runScopedSubstReader scope env m = - runIdentity $ runScopeReaderT scope $ runSubstReaderT env m -{-# INLINE runScopedSubstReader #-} - -withSubstReaderT :: FromName v => SubstReaderT v m n n a -> m n a -withSubstReaderT = runSubstReaderT idSubst -{-# INLINE withSubstReaderT #-} - -instance (SinkableE v, Monad1 m) => SubstReader v (SubstReaderT v m) where - getSubst = SubstReaderT' ask - {-# INLINE getSubst #-} - withSubst env (SubstReaderT' cont) = SubstReaderT' $ withReaderT (const env) cont - {-# INLINE withSubst #-} - -instance (SinkableE v, ScopeReader m) => ScopeReader (SubstReaderT v m i) where - unsafeGetScope = liftSubstReaderT unsafeGetScope - {-# INLINE unsafeGetScope #-} - getDistinct = liftSubstReaderT getDistinct - {-# INLINE getDistinct #-} - -instance (SinkableE v, EnvReader m) => EnvReader (SubstReaderT v m i) where - unsafeGetEnv = liftSubstReaderT unsafeGetEnv - {-# INLINE unsafeGetEnv #-} - -instance (SinkableE v, ScopeReader m, EnvExtender m) - => EnvExtender (SubstReaderT v m i) where - refreshAbs ab cont = SubstReaderT \subst -> - refreshAbs ab \b e -> do - subst' <- sinkM subst - let SubstReaderT cont' = cont b e - cont' subst' - {-# INLINE refreshAbs #-} - -instance MonadDiffState1 m s d => MonadDiffState1 (SubstReaderT v m i) s d where - withDiffState s m = - SubstReaderT \subst -> do - withDiffState s $ runSubstReaderT subst m - - updateDiffStateM d = liftSubstReaderT $ updateDiffStateM d - getDiffState = liftSubstReaderT getDiffState - -type SubstEnvReaderM v = SubstReaderT v EnvReaderM :: MonadKind2 - -liftSubstEnvReaderM - :: forall v m n a. (EnvReader m, FromName v) - => SubstEnvReaderM v n n a - -> m n a -liftSubstEnvReaderM cont = liftEnvReaderM $ runSubstReaderT idSubst $ cont -{-# INLINE liftSubstEnvReaderM #-} - -instance (SinkableE v, ScopeReader m, ScopeExtender m) - => ScopeExtender (SubstReaderT v m i) where - refreshAbsScope ab cont = SubstReaderT \env -> - refreshAbsScope ab \b e -> do - let SubstReaderT cont' = cont b e - env' <- sinkM env - cont' env' - -instance (SinkableE v, MonadIO1 m) => MonadIO (SubstReaderT v m i o) where - liftIO m = liftSubstReaderT $ liftIO m - {-# INLINE liftIO #-} - -instance (Monad1 m, MonadState (s o) (m o)) => MonadState (s o) (SubstReaderT v m i o) where - state = liftSubstReaderT . state - {-# INLINE state #-} - -instance (Monad1 m, MonadReader (r o) (m o)) => MonadReader (r o) (SubstReaderT v m i o) where - ask = SubstReaderT $ const ask - {-# INLINE ask #-} - local r (SubstReaderT' (ReaderT f)) = SubstReaderT \env -> local r $ f env - {-# INLINE local #-} - --- === instances === - -instance SinkableE atom => SinkableE (SubstVal atom) where - sinkingProofE fresh substVal = case substVal of - Rename name -> Rename $ sinkingProofE fresh name - SubstVal val -> SubstVal $ sinkingProofE fresh val - -instance (SubstB v b, SubstE v e) => SubstE v (Abs b e) where - substE env (Abs b body) = do - substB env b \env' b' -> Abs b' $ substE env' body - -instance ( BindsNames b1, SubstB v b1 - , BindsNames b2, SubstB v b2 - , SinkableE v, FromName v) - => SubstB v (PairB b1 b2) where - substB env (PairB b1 b2) cont = - substB env b1 \env' b1' -> - substB env' b2 \env'' b2' -> - cont env'' $ PairB b1' b2' - -instance (SinkableE e, SubstE v e) => SubstB v (LiftB e) where - substB env@(_, subst) (LiftB e) cont = case tryApplyIdentitySubst subst e of - Just e' -> cont env $ LiftB e' - Nothing -> cont env $ LiftB $ substE env e - {-# INLINE substB #-} - -instance (SubstB v b1, SubstB v b2) => SubstB v (EitherB b1 b2) where - substB env (LeftB b) cont = - substB env b \env' b' -> - cont env' $ LeftB b' - substB env (RightB b) cont = - substB env b \env' b' -> - cont env' $ RightB b' - -instance (SinkableE ann, SubstE v ann, SinkableE v, ToBinding ann) - => SubstB v (BinderP ann) where - substB (env, subst) (b:>ty) cont = do - let ty' = substE (env, subst) ty - withFresh (getNameHint b) (toScope env) \bRaw -> do - let b' = bRaw:>ty' - let env' = env `extendOutMap` toEnvFrag b' - let UnsafeMakeName bn = binderName b - let UnsafeMakeName bn' = binderName b' - let subst' = case subst of - UnsafeMakeIdentitySubst | bn == bn' -> UnsafeMakeIdentitySubst - _ -> sink subst <>> b @> (fromName $ binderName b') - cont (env', subst') b' - -instance (BindsNames b, SubstB v b, SinkableE v) => SubstB v (Nest b) where - substB env (Nest b bs) cont = - substB env b \env' b' -> - substB env' bs \env'' bs' -> - cont env'' $ Nest b' bs' - substB env Empty cont = cont env Empty - -instance FromName v => SubstE v UnitE where - substE _ UnitE = UnitE - -instance SubstB v b => SubstB v (WithAttrB a b) where - substB env (WithAttrB x b) cont = - substB env b \env' b' -> cont env' $ WithAttrB x b' - -instance (Traversable f, SubstE v e) => SubstE v (ComposeE f e) where - substE env (ComposeE xs) = ComposeE $ fmap (substE env) xs - -instance (SubstE v e1, SubstE v e2) => SubstE v (PairE e1 e2) where - substE env (PairE x y) = PairE (substE env x) (substE env y) - -instance (SubstE v e1, SubstE v e2) => SubstE v (EitherE e1 e2) where - substE env (LeftE x) = LeftE $ substE env x - substE env (RightE x) = RightE $ substE env x - -instance FromName v => SubstE v VoidE where - substE _ _ = error "impossible" - -instance FromName v => SubstE v (LiftE a) where - substE _ (LiftE x) = LiftE x - -instance SubstE v e => SubstE v (ListE e) where - substE env (ListE xs) = ListE $ map (substE env) xs - -instance SubstE v e => SubstE v (RListE e) where - substE env (RListE xs) = RListE $ fmap (substE env) xs - -instance SubstE v e => SubstE v (NonEmptyListE e) where - substE env (NonEmptyListE xs) = NonEmptyListE $ fmap (substE env) xs - -instance SubstE substVal v => SubstE substVal (SubstFrag v i i') where - substE env frag = fmapSubstFrag (\_ val -> substE env val) frag - -instance SubstE substVal v => SubstE substVal (Subst v i) where - substE env = \case - Subst f frag -> Subst (\n -> substE env (f n)) $ substE env frag - UnsafeMakeIdentitySubst - -> Subst (\n -> substE env (fromName $ unsafeCoerceE n)) emptyInFrag - -instance (SubstE v e0, SubstE v e1, SubstE v e2, - SubstE v e3, SubstE v e4, SubstE v e5, - SubstE v e6, SubstE v e7) - => SubstE v (EitherE8 e0 e1 e2 e3 e4 e5 e6 e7) where - substE env = \case - Case0 e -> Case0 $ substE env e - Case1 e -> Case1 $ substE env e - Case2 e -> Case2 $ substE env e - Case3 e -> Case3 $ substE env e - Case4 e -> Case4 $ substE env e - Case5 e -> Case5 $ substE env e - Case6 e -> Case6 $ substE env e - Case7 e -> Case7 $ substE env e - {-# INLINE substE #-}