From d8fe2d4bf52e840985d0ed3f101cf5e0a95254ab Mon Sep 17 00:00:00 2001 From: Dougal Date: Fri, 17 May 2024 23:46:49 -0400 Subject: [PATCH] Split CExpr and SExpr into different ADTs (WIP) --- dex.cabal | 3 +- src/lib/Core.hs | 3 +- src/lib/Name.hs | 8 +- src/lib/QueryTypePure.hs | 3 +- src/lib/Types/Complicated.hs | 358 ++++++++ src/lib/Types/Core.hs | 1600 ---------------------------------- src/lib/Types/Simple.hs | 125 +++ src/lib/Types/Top.hs | 226 ++--- 8 files changed, 559 insertions(+), 1767 deletions(-) create mode 100644 src/lib/Types/Complicated.hs delete mode 100644 src/lib/Types/Core.hs create mode 100644 src/lib/Types/Simple.hs diff --git a/dex.cabal b/dex.cabal index e599f6938..2d75e9184 100644 --- a/dex.cabal +++ b/dex.cabal @@ -82,7 +82,8 @@ library , SourceIdTraversal , TopLevel -- , Transpose - , Types.Core + , Types.Simple + , Types.Complicated , Types.Imp , Types.Primitives , Types.Source diff --git a/src/lib/Core.hs b/src/lib/Core.hs index d1ed372b2..5f3cbf860 100644 --- a/src/lib/Core.hs +++ b/src/lib/Core.hs @@ -35,7 +35,8 @@ import qualified Data.Map.Strict as M import Name import Err -import Types.Core +import Types.Complicated +import Types.Simple import Types.Top import Types.Imp import Types.Primitives diff --git a/src/lib/Name.hs b/src/lib/Name.hs index 101c3fef0..6a460e9a4 100644 --- a/src/lib/Name.hs +++ b/src/lib/Name.hs @@ -23,10 +23,8 @@ import Control.Monad.Writer.Strict import Control.Monad.State.Strict import qualified Data.HashMap.Strict as HM import qualified Data.Map.Strict as M -import Data.Bits import Data.Functor ((<&>)) import Data.Foldable (toList, foldl') -import Data.Maybe (fromJust, catMaybes) import Data.Hashable import Data.Kind (Type) import Data.Function ((&)) @@ -2192,7 +2190,7 @@ absurdNameFunction :: Name VoidS -> a absurdNameFunction v = error $ "Void names shouldn't exist: " ++ show v scopeFragToSubstFrag :: forall v i i' o - . (forall c. Name (i:=>:i') -> v o) + . (Name (i:=>:i') -> v o) -> ScopeFrag i i' -> SubstFrag v i i' o scopeFragToSubstFrag f (UnsafeScopeFromSubst m) = fmapSubstFrag (\n _ -> f n) m @@ -2220,7 +2218,7 @@ newNames n = do let bs = unsafeListToNest $ map UnsafeMakeBinder ns unsafeCoerceE $ Abs bs $ ListE vs -withFresh :: forall n c a. (Distinct n) +withFresh :: forall n a. (Distinct n) => NameHint -> Scope n -> (forall l. DExt n l => NameBinder n l -> a) -> a withFresh hint (Scope (UnsafeMakeScopeFrag scope)) cont = @@ -2749,7 +2747,7 @@ instance BindsNames (SubstPair v o) where -- === instances === -instance (forall c. Pretty (v n)) => Pretty (SubstItem v n) where +instance Pretty (v n) => Pretty (SubstItem v n) where pretty (SubstItem _ val) = pretty val instance SinkableE v => SinkableE (SubstFrag v i i') where diff --git a/src/lib/QueryTypePure.hs b/src/lib/QueryTypePure.hs index b943acc82..e4d24e071 100644 --- a/src/lib/QueryTypePure.hs +++ b/src/lib/QueryTypePure.hs @@ -7,7 +7,8 @@ module QueryTypePure where import Types.Primitives -import Types.Core +import Types.Simple +import Types.Complicated import Types.Top import Name diff --git a/src/lib/Types/Complicated.hs b/src/lib/Types/Complicated.hs new file mode 100644 index 000000000..05ce6d2cf --- /dev/null +++ b/src/lib/Types/Complicated.hs @@ -0,0 +1,358 @@ +-- Copyright 2022 Google LLC +-- +-- Use of this source code is governed by a BSD-style +-- license that can be found in the LICENSE file or at +-- https://developers.google.com/open-source/licenses/bsd + +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE StrictData #-} + +module Types.Complicated (module Types.Complicated) where + +import Data.Word +import Data.Foldable (toList) +import Data.Hashable +import Data.String (fromString) +import Data.Text.Prettyprint.Doc +import Data.Text (Text, unsnoc, uncons) +import qualified Data.Map.Strict as M + +import GHC.Generics (Generic (..)) +import Data.Store (Store (..)) + +import Name +import Util (Tree (..)) +import PPrint + +import Types.Source (HasSourceName (..)) +import Types.Primitives + +data CExpr (n::S) = + CBlock (CType n) (CBlock n) + | CVar (Name n) (CType n) + | CLit LitVal + | CPrimOp (CType n) (PrimOp (CExpr n)) + | CTyCon (CTyCon n) + | Lam (CoreLamExpr n) + | NewtypeCon (NewtypeCon n) (CExpr n) + | Dict (DictCon n) + deriving (Show, Generic) + +data CTyCon (n::S) = + CBaseType BaseType + | CProdType [CType n] + | CSumType [CType n] + | CRefType (CType n) + | DictTy (DictType n) + | Pi (CorePiType n) + | NewtypeTyCon (NewtypeTyCon n) + | CTabPi (CTabPiType n) + | CDepPairTy (CDepPairType n) + | Kind Kind + deriving (Show, Generic) + +type CType = CExpr + +type CBinder = BinderP CType :: B + +data CDecl (n::S) (l::S) = CLet (NameBinder n l) (CExpr n) deriving (Show, Generic) +type CBlock = Abs (Nest CDecl) CExpr + +data CorePiType (n::S) = CorePiType AppExplicitness [Explicitness] (Abs (Nest CBinder) CType n) + deriving (Show, Generic) + +type IxDict = CExpr +data CTabPiType (n::S) = CTabPiType (IxDict n) (Abs CBinder CType n) + deriving (Show, Generic) + +data CDepPairType (n::S) = CDepPairType DepPairExplicitness (Abs CBinder CType n) + deriving (Show, Generic) + +data CoreLamExpr (n::S) = CoreLamExpr (CorePiType n) (Abs (Nest CBinder) CExpr n) + deriving (Show, Generic) + +data Kind = DataKind | RefKind | TypeKind | FunKind | DictKind | OtherKind + deriving (Show, Generic, Eq, Ord) +instance Store Kind +instance Hashable Kind + +type ClassName = Name +data DictType (n::S) = + DictType SourceName (ClassName n) [CExpr n] + | IxDictType (CType n) + deriving (Show, Generic) + +type InstanceName = Name +data DictCon (n::S) = + InstanceDict (CType n) (InstanceName n) [CExpr n] + | IxFin (CExpr n) + deriving (Show, Generic) + +-- Describes how to lift the "shallow" representation type to the newtype. +data NewtypeCon (n::S) = + UserADTData SourceName (TyConName n) (TyConParams n) -- source name is for the type + | NatCon + | FinCon (CExpr n) + deriving (Show, Generic) + +type TyConName = Name +data NewtypeTyCon (n::S) = + Nat + | Fin (CExpr n) + | UserADTType SourceName (TyConName n) (TyConParams n) + deriving (Show, Generic) + +-- We track the explicitness information because we need it for the equality +-- check since we skip equality checking on dicts. +data TyConParams n = TyConParams [Explicitness] [CExpr n] + deriving (Show, Generic) + +-- === top-level definitions === + +data ClassDef (n::S) where + ClassDef + :: SourceName -- name of class + -> Maybe BuiltinClassName + -> [SourceName] -- method source names + -> [Maybe SourceName] -- parameter source names + -> [Explicitness] -- parameter info + -> Nest CBinder n1 n2 -- parameters + -> Nest CBinder n2 n3 -- superclasses + -> [CorePiType n3] -- method types + -> ClassDef n1 + +data BuiltinClassName = Ix deriving (Show, Generic, Eq) +instance Hashable BuiltinClassName +instance Store BuiltinClassName + +data InstanceDef (n::S) where + InstanceDef + :: ClassName n1 + -> [Explicitness] -- parameter info + -> Nest CBinder n1 n2 -- parameters (types and dictionaries) + -> [CExpr n2] -- class parameters + -> [CExpr n2] -- superclasses dicts + -> [CExpr n2] -- method definitions + -> InstanceDef n1 + +newtype DotMethods n = DotMethods (M.Map SourceName (Name n)) + deriving (Show, Generic, Monoid, Semigroup) + +data TyConDef n = TyConDef + SourceName -- just for pretty-printing + [Explicitness] + (Abs (Nest CBinder) DataConDefs n) + deriving (Show, Generic) + +data DataConDefs n = + ADTCons [DataConDef n] + | StructFields [(SourceName, CType n)] + deriving (Show, Generic) + +data DataConDef n = + -- Name for pretty printing, constructor elements, representation type, + -- list of projection indices that recovers elements from the representation. + DataConDef SourceName (EmptyAbs (Nest CBinder) n) (CType n) [[Projection]] + deriving (Show, Generic) + +-- === type classes === + +instance GenericE CExpr where + type RepE CExpr = UnitE +instance Pretty (CExpr n) +instance SinkableE CExpr +instance HoistableE CExpr +instance RenameE CExpr +instance AlphaEqE CExpr +instance AlphaHashableE CExpr +instance Store (CExpr n) + +instance GenericE DictType where + type RepE DictType = UnitE +instance Pretty (DictType n) +instance SinkableE DictType +instance HoistableE DictType +instance RenameE DictType +instance AlphaEqE DictType +instance AlphaHashableE DictType +instance Store (DictType n) + +instance GenericE CDepPairType where + type RepE CDepPairType = UnitE +instance Pretty (CDepPairType n) +instance SinkableE CDepPairType +instance HoistableE CDepPairType +instance RenameE CDepPairType +instance AlphaEqE CDepPairType +instance AlphaHashableE CDepPairType +instance Store (CDepPairType n) + +instance GenericE CTabPiType where + type RepE CTabPiType = UnitE +instance Pretty (CTabPiType n) +instance SinkableE CTabPiType +instance HoistableE CTabPiType +instance RenameE CTabPiType +instance AlphaEqE CTabPiType +instance AlphaHashableE CTabPiType +instance Store (CTabPiType n) + +instance GenericE NewtypeTyCon where + type RepE NewtypeTyCon = UnitE +instance Pretty (NewtypeTyCon n) +instance SinkableE NewtypeTyCon +instance HoistableE NewtypeTyCon +instance RenameE NewtypeTyCon +instance AlphaEqE NewtypeTyCon +instance AlphaHashableE NewtypeTyCon +instance Store (NewtypeTyCon n) + +instance GenericE CTyCon where + type RepE CTyCon = UnitE +instance Pretty (CTyCon n) +instance SinkableE CTyCon +instance HoistableE CTyCon +instance RenameE CTyCon +instance AlphaEqE CTyCon +instance AlphaHashableE CTyCon +instance Store (CTyCon n) + +instance GenericE DictCon where + type RepE DictCon = UnitE +instance Pretty (DictCon n) +instance SinkableE DictCon +instance HoistableE DictCon +instance RenameE DictCon +instance AlphaEqE DictCon +instance AlphaHashableE DictCon +instance Store (DictCon n) + +instance GenericE TyConDef where + type RepE TyConDef = UnitE +instance Pretty (TyConDef n) +instance SinkableE TyConDef +instance HoistableE TyConDef +instance RenameE TyConDef +instance AlphaEqE TyConDef +instance AlphaHashableE TyConDef +instance Store (TyConDef n) + +instance GenericE DataConDef where + type RepE DataConDef = UnitE +instance Pretty (DataConDef n) +instance SinkableE DataConDef +instance HoistableE DataConDef +instance RenameE DataConDef +instance AlphaEqE DataConDef +instance AlphaHashableE DataConDef +instance Store (DataConDef n) + +instance GenericE DataConDefs where + type RepE DataConDefs = UnitE +instance Pretty (DataConDefs n) +instance SinkableE DataConDefs +instance HoistableE DataConDefs +instance RenameE DataConDefs +instance AlphaEqE DataConDefs +instance AlphaHashableE DataConDefs +instance Store (DataConDefs n) + +instance GenericE NewtypeCon where + type RepE NewtypeCon = UnitE +instance Pretty (NewtypeCon n) +instance SinkableE NewtypeCon +instance HoistableE NewtypeCon +instance RenameE NewtypeCon +instance AlphaEqE NewtypeCon +instance AlphaHashableE NewtypeCon +instance Store (NewtypeCon n) + +instance GenericE CoreLamExpr where + type RepE CoreLamExpr = UnitE +instance Pretty (CoreLamExpr n) +instance SinkableE CoreLamExpr +instance HoistableE CoreLamExpr +instance RenameE CoreLamExpr +instance AlphaEqE CoreLamExpr +instance AlphaHashableE CoreLamExpr +instance Store (CoreLamExpr n) + +instance GenericE TyConParams where + type RepE TyConParams = UnitE +instance Pretty (TyConParams n) +instance SinkableE TyConParams +instance HoistableE TyConParams +instance RenameE TyConParams +instance AlphaEqE TyConParams +instance AlphaHashableE TyConParams +instance Store (TyConParams n) + +instance GenericE CorePiType where + type RepE CorePiType = UnitE +instance Pretty (CorePiType n) +instance SinkableE CorePiType +instance HoistableE CorePiType +instance RenameE CorePiType +instance AlphaEqE CorePiType +instance AlphaHashableE CorePiType +instance Store (CorePiType n) + +instance GenericE DotMethods where + type RepE DotMethods = UnitE +instance Pretty (DotMethods n) +instance SinkableE DotMethods +instance HoistableE DotMethods +instance RenameE DotMethods +instance AlphaEqE DotMethods +instance AlphaHashableE DotMethods +instance Store (DotMethods n) + +instance GenericE ClassDef where + type RepE ClassDef = + LiftE (SourceName, Maybe BuiltinClassName, [SourceName], [Maybe SourceName], [Explicitness]) + `PairE` Abs (Nest CBinder) (Abs (Nest CBinder) (ListE CorePiType)) + fromE (ClassDef name builtin names paramNames roleExpls b scs tys) = + LiftE (name, builtin, names, paramNames, roleExpls) `PairE` Abs b (Abs scs (ListE tys)) + {-# INLINE fromE #-} + toE (LiftE (name, builtin, names, paramNames, roleExpls) `PairE` Abs b (Abs scs (ListE tys))) = + ClassDef name builtin names paramNames roleExpls b scs tys + {-# INLINE toE #-} +instance Pretty (ClassDef n) +instance SinkableE ClassDef +instance HoistableE ClassDef +instance AlphaEqE ClassDef +instance AlphaHashableE ClassDef +instance RenameE ClassDef +deriving instance Show (ClassDef n) +deriving via WrapE ClassDef n instance Generic (ClassDef n) +instance Store (ClassDef n) +instance HasSourceName (ClassDef n) where + getSourceName = \case ClassDef name _ _ _ _ _ _ _ -> name + +instance GenericE InstanceDef where + type RepE InstanceDef = UnitE +instance Pretty (InstanceDef n) +instance SinkableE InstanceDef +instance HoistableE InstanceDef +instance RenameE InstanceDef +instance AlphaEqE InstanceDef +instance AlphaHashableE InstanceDef +instance Store (InstanceDef n) +deriving instance Show (InstanceDef n) +deriving via WrapE InstanceDef n instance Generic (InstanceDef n) + +instance GenericB CDecl where + type RepB CDecl = BinderP CExpr + fromB (CLet b expr) = b :> expr + {-# INLINE fromB #-} + toB (b :> expr) = CLet b expr + {-# INLINE toB #-} +instance Pretty (CDecl n l) +instance SinkableB CDecl +instance HoistableB CDecl +instance RenameB CDecl +instance AlphaEqB CDecl +instance AlphaHashableB CDecl +instance ProvesExt CDecl +instance BindsNames CDecl +instance Store (CDecl n l) diff --git a/src/lib/Types/Core.hs b/src/lib/Types/Core.hs deleted file mode 100644 index e7b5a1f84..000000000 --- a/src/lib/Types/Core.hs +++ /dev/null @@ -1,1600 +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 UndecidableInstances #-} -{-# LANGUAGE StrictData #-} - --- Core data types for CoreIR and its variations. - -module Types.Core (module Types.Core) where - -import Data.Word -import Data.Foldable (toList) -import Data.Hashable -import Data.String (fromString) -import Data.Text.Prettyprint.Doc -import Data.Text (Text, unsnoc, uncons) -import qualified Data.Map.Strict as M - -import GHC.Generics (Generic (..)) -import Data.Store (Store (..)) - -import Name -import Util (Tree (..)) -import PPrint - -import Types.Primitives -import Types.Source (HasSourceName (..)) -import Types.Imp - --- === core IR === - -data Atom (n::S) = - Con (Con n) - | Stuck (Type n) (Stuck n) - deriving (Show, Generic) - -data Type (n::S) where - TyCon :: TyCon n -> Type n - StuckTy :: Kind -> CStuck n -> Type n - -data Kind = DataKind | RefKind | TypeKind | FunKind | DictKind | OtherKind - deriving (Show, Generic, Eq, Ord) - -data Dict (n::S) where - DictCon :: DictCon n -> Dict n - StuckDict :: CType n -> CStuck n -> Dict n - -data Con (n::S) where - Lit :: LitVal -> Con n - ProdCon :: [Atom n] -> Con n - SumCon :: [Type n] -> Int -> Atom n -> Con n -- type, tag, payload - DepPair :: Atom n -> Atom n -> DepPairType n -> Con n - Lam :: CoreLamExpr n -> Con n - NewtypeCon :: NewtypeCon n -> Atom n -> Con n - DictConAtom :: DictCon n -> Con n - TyConAtom :: TyCon n -> Con n - -data Stuck (n::S) where - Var :: AtomVar n -> Stuck n - StuckProject :: Int -> Stuck n -> Stuck n - StuckTabApp :: Stuck n -> Atom n -> Stuck n - PtrVar :: PtrType -> PtrName n -> Stuck n - RepValAtom :: RepVal n -> Stuck n - StuckUnwrap :: CStuck n -> Stuck n - InstantiatedGiven :: CStuck n -> [CAtom n] -> Stuck n - SuperclassProj :: Int -> CStuck n -> Stuck n - -data TyCon (n::S) where - BaseType :: BaseType -> TyCon n - ProdType :: [Type n] -> TyCon n - SumType :: [Type n] -> TyCon n - RefType :: Type n -> TyCon n - TabPi :: TabPiType n -> TyCon n - DepPairTy :: DepPairType n -> TyCon n - DictTy :: DictType n -> TyCon n - Pi :: CorePiType n -> TyCon n - NewtypeTyCon :: NewtypeTyCon n -> TyCon n - Kind :: Kind -> TyCon n - -data AtomVar (n::S) = AtomVar - { atomVarName :: AtomName n - , atomVarType :: Type n } - deriving (Show, Generic) - -deriving instance Show (DictCon n) -deriving instance Show (Dict n) -deriving instance Show (Con n) -deriving instance Show (TyCon n) -deriving instance Show (Type n) -deriving instance Show (Stuck n) - -deriving via WrapE DictCon n instance Generic (DictCon n) -deriving via WrapE Dict n instance Generic (Dict n) -deriving via WrapE Con n instance Generic (Con n) -deriving via WrapE TyCon n instance Generic (TyCon n) -deriving via WrapE Type n instance Generic (Type n) -deriving via WrapE Stuck n instance Generic (Stuck n) - -data Expr n where - Block :: EffTy n -> Block n -> Expr n - TopApp :: EffTy n -> TopFunName n -> [SAtom n] -> Expr n - TabApp :: Type n -> Atom n -> Atom n -> Expr n - Case :: Atom n -> [Alt n] -> EffTy n -> Expr n - Atom :: Atom n -> Expr n - TabCon :: Type n -> [Atom n] -> Expr n - PrimOp :: Type n -> PrimOp (Atom n) -> Expr n - Hof :: TypedHof n -> Expr n - Project :: Type n -> Int -> Atom n -> Expr n - App :: EffTy n -> CAtom n -> [CAtom n] -> Expr n - Unwrap :: CType n -> CAtom n -> Expr n - ApplyMethod :: EffTy n -> CAtom n -> Int -> [CAtom n] -> Expr n - -deriving instance Show (Expr n) -deriving via WrapE Expr n instance Generic (Expr n) - -data RepVal (n::S) = RepVal (Type n) (Tree (IExpr n)) - deriving (Show, Generic) - -data DeclBinding n = DeclBinding LetAnn (Expr n) - deriving (Show, Generic) -data Decl (n::S) (l::S) = Let (AtomNameBinder n l) (DeclBinding n) - deriving (Show, Generic) -type Decls = Nest Decl - -type AtomName = Name -type AtomNameBinder = NameBinder - -type ClassName = Name -type TyConName = Name -type DataConName = Name -type InstanceName = Name -type MethodName = Name -type ModuleName = Name -type SpecDictName = Name -type TopFunName = Name - -type AtomBinderP = BinderP -type Binder = AtomBinderP Type :: B -type Alt = Abs Binder Expr :: E - -newtype DotMethods n = DotMethods (M.Map SourceName (CAtomName n)) - deriving (Show, Generic, Monoid, Semigroup) - -data TyConDef n where - -- The `SourceName` is just for pretty-printing. The actual alpha-renamable - -- binder name is in UExpr and Env - TyConDef - :: SourceName - -> [Explicitness] - -> Nest CBinder n l - -> DataConDefs l - -> TyConDef n - -data DataConDefs n = - ADTCons [DataConDef n] - | StructFields [(SourceName, CType n)] - deriving (Show, Generic) - -data DataConDef n = - -- Name for pretty printing, constructor elements, representation type, - -- list of projection indices that recovers elements from the representation. - DataConDef SourceName (EmptyAbs (Nest CBinder) n) (CType n) [[Projection]] - deriving (Show, Generic) - --- We track the explicitness information because we need it for the equality --- check since we skip equality checking on dicts. -data TyConParams n = TyConParams [Explicitness] [Atom n] - deriving (Show, Generic) - -type WithDecls = Abs Decls :: E -> E -type Block = WithDecls Expr :: E - -data LamExpr (n::S) where - LamExpr :: Nest Binder n l -> Expr l -> LamExpr n - -data CoreLamExpr (n::S) = CoreLamExpr (CorePiType n) (LamExpr n) deriving (Show, Generic) - -type TabLamExpr = PairE TabPiType (Abs SBinder CAtom) -type IxDict = Dict - -data IxMethod = Size | Ordinal | UnsafeFromOrdinal - deriving (Show, Generic, Enum, Bounded, Eq) - -data IxType (n::S) = - IxType { ixTypeType :: Type n - , ixTypeDict :: IxDict n } - deriving (Show, Generic) - -data TabPiType (n::S) where - TabPiType :: IxDict n -> Binder n l -> Type l -> TabPiType n - -data PiType (n::S) where - PiType :: Nest Binder n l -> Type l -> PiType n - -data CorePiType (n::S) where - CorePiType :: AppExplicitness -> [Explicitness] -> Nest CBinder n l -> CType l -> CorePiType n - -data DepPairType (n::S) where - DepPairType :: DepPairExplicitness -> Binder n l -> Type l -> DepPairType n - --- A nest where the annotation of a binder cannot depend on the binders --- introduced before it. You can think of it as introducing a bunch of --- names into the scope in parallel, but since safer names only reasons --- about sequential scope extensions, we encode it differently. -data NonDepNest ann n l = NonDepNest (Nest AtomNameBinder n l) [ann n] - deriving (Generic) - --- === ToAtomAbs class === - -class ToBindersAbs (e::E) (body::E) | e -> body where - toAbs :: e n -> Abs (Nest Binder) body n - -instance ToBindersAbs CorePiType Type where - toAbs (CorePiType _ _ bs ty) = Abs bs ty - -instance ToBindersAbs CoreLamExpr Expr where - toAbs (CoreLamExpr _ lam) = toAbs lam - -instance ToBindersAbs (Abs (Nest Binder) body) body where - toAbs = id - -instance ToBindersAbs PiType Type where - toAbs (PiType bs ty) = Abs bs ty - -instance ToBindersAbs LamExpr Expr where - toAbs (LamExpr bs body) = Abs bs body - -instance ToBindersAbs TabPiType Type where - toAbs (TabPiType _ b eltTy) = Abs (UnaryNest b) eltTy - -instance ToBindersAbs DepPairType Type where - toAbs (DepPairType _ b rhsTy) = Abs (UnaryNest b) rhsTy - -instance ToBindersAbs InstanceDef (ListE CAtom `PairE` InstanceBody) where - toAbs (InstanceDef _ _ bs params body) = Abs bs (ListE params `PairE` body) - -instance ToBindersAbs TyConDef DataConDefs where - toAbs (TyConDef _ _ bs body) = Abs bs body - -instance ToBindersAbs ClassDef (Abs (Nest CBinder) (ListE CorePiType)) where - toAbs (ClassDef _ _ _ _ _ bs scBs tys) = Abs bs (Abs scBs (ListE tys)) - -showStringBufferSize :: Word32 -showStringBufferSize = 32 - --- === Hofs === - -data TypedHof n = TypedHof (EffTy n) (Hof n) - deriving (Show, Generic) - -data Hof n = - For ForAnn (IxType n) (LamExpr n) - | While (Expr n) - | Linearize (LamExpr n) (CAtom n) - | Transpose (LamExpr n) (CAtom n) - deriving (Show, Generic) - --- === IR variants === - -type CAtom = Atom -type CType = Type -type CDict = Dict -type CStuck = Stuck -type CBinder = Binder -type CExpr = Expr -type CBlock = Block -type CDecl = Decl -type CDecls = Decls -type CAtomName = AtomName -type CAtomVar = AtomVar - -type SAtom = Atom -type SType = Type -type SDict = Dict -type SStuck = Stuck -type SExpr = Expr -type SBlock = Block -type SAlt = Alt -type SDecl = Decl -type SDecls = Decls -type SAtomName = AtomName -type SAtomVar = AtomVar -type SBinder = Binder -type SLam = LamExpr - --- === newtypes === - --- Describes how to lift the "shallow" representation type to the newtype. -data NewtypeCon (n::S) = - UserADTData SourceName (TyConName n) (TyConParams n) -- source name is for the type - | NatCon - | FinCon (Atom n) - deriving (Show, Generic) - -data NewtypeTyCon (n::S) = - Nat - | Fin (Atom n) - | UserADTType SourceName (TyConName n) (TyConParams n) - deriving (Show, Generic) - -isSumCon :: NewtypeCon n -> Bool -isSumCon = \case - UserADTData _ _ _ -> True - _ -> False - --- === type classes === - -data ClassDef (n::S) where - ClassDef - :: SourceName -- name of class - -> Maybe BuiltinClassName - -> [SourceName] -- method source names - -> [Maybe SourceName] -- parameter source names - -> [Explicitness] -- parameter info - -> Nest CBinder n1 n2 -- parameters - -> Nest CBinder n2 n3 -- superclasses - -> [CorePiType n3] -- method types - -> ClassDef n1 - -data BuiltinClassName = Ix deriving (Show, Generic, Eq) - -data InstanceDef (n::S) where - InstanceDef - :: ClassName n1 - -> [Explicitness] -- parameter info - -> Nest CBinder n1 n2 -- parameters (types and dictionaries) - -> [CAtom n2] -- class parameters - -> InstanceBody n2 - -> InstanceDef n1 - -data InstanceBody (n::S) = - InstanceBody - [CAtom n] -- superclasses dicts - [CAtom n] -- method definitions - deriving (Show, Generic) - -data DictType (n::S) = - DictType SourceName (ClassName n) [CAtom n] - | IxDictType (CType n) - deriving (Show, Generic) - -data DictCon (n::S) where - InstanceDict :: CType n -> InstanceName n -> [CAtom n] -> DictCon n - IxFin :: CAtom n -> DictCon n - -- IxRawFin is like `Fin`, but it's parameterized by a newtyped-stripped - -- `IxRepVal` instead of `Nat`, and it describes indices of type `IxRepVal`. - -- TODO: make is-only - IxRawFin :: Atom n -> DictCon n - IxSpecialized :: SpecDictName n -> [SAtom n] -> DictCon n - -data Effects (n::S) = Pure | Effectful - deriving (Generic, Show) - -instance Semigroup (Effects n) where - Pure <> Pure = Pure - _ <> _ = Effectful - -instance Monoid (Effects n) where - mempty = Pure - -data EffTy (n::S) = - EffTy { etEff :: Effects n - , etTy :: Type n } - deriving (Generic, Show) - --- === Binder utils === - -binderType :: Binder n l -> Type n -binderType (_:>ty) = ty - -binderVar :: (DExt n l) => Binder n l -> AtomVar l -binderVar (b:>ty) = AtomVar (binderName b) (sink ty) - -bindersVars :: (Distinct l, Ext n l) => Nest Binder n l -> [AtomVar l] -bindersVars = \case - Empty -> [] - Nest b bs -> withExtEvidence b $ withSubscopeDistinct bs $ - sink (binderVar b) : bindersVars bs - --- === ToAtom === - -class ToAtom (e::E) where - toAtom :: e n -> Atom n - -instance ToAtom Atom where toAtom = id -instance ToAtom Con where toAtom = Con -instance ToAtom (TyCon ) where toAtom = Con . TyConAtom -instance ToAtom (DictCon ) where toAtom = Con . DictConAtom -instance ToAtom CoreLamExpr where toAtom = Con . Lam -instance ToAtom DictType where toAtom = Con . TyConAtom . DictTy -instance ToAtom NewtypeTyCon where toAtom = Con . TyConAtom . NewtypeTyCon -instance ToAtom AtomVar where - toAtom (AtomVar v ty) = Stuck ty (Var (AtomVar v ty)) -instance ToAtom RepVal where - toAtom (RepVal ty tree) = Stuck ty $ RepValAtom $ RepVal ty tree -instance ToAtom (Type) where - toAtom = \case - TyCon con -> Con $ TyConAtom con - StuckTy k s -> Stuck (TyCon $ Kind k) s -instance ToAtom (Dict) where - toAtom = \case - DictCon d -> Con $ DictConAtom d - StuckDict t s -> Stuck t s - --- This can help avoid ambiguous `r` parameter with ToAtom -toAtomR :: ToAtom e => e n -> Atom n -toAtomR = toAtom - --- === ToType === - -class ToType (e::E) where - toType :: e n -> Type n - -instance ToType Type where toType = id -instance ToType TyCon where toType = TyCon -instance ToType TabPiType where toType = TyCon . TabPi -instance ToType DepPairType where toType = TyCon . DepPairTy -instance ToType CorePiType where toType = TyCon . Pi -instance ToType DictType where toType = TyCon . DictTy -instance ToType NewtypeTyCon where toType = TyCon . NewtypeTyCon - -toMaybeType :: CAtom n -> Maybe (CType n) -toMaybeType = \case - Stuck (TyCon (Kind k)) s -> Just $ StuckTy k s - Con (TyConAtom t) -> Just $ TyCon t - _ -> Nothing - --- === ToDict === - -class ToDict (e::E) where - toDict :: e n -> Dict n - -instance ToDict Dict where toDict = id -instance ToDict DictCon where toDict = DictCon -instance ToDict CAtomVar where - toDict (AtomVar v ty) = StuckDict ty (Var (AtomVar v ty)) - -toMaybeDict :: CAtom n -> Maybe (CDict n) -toMaybeDict = \case - Stuck t s -> Just $ StuckDict t s - Con (DictConAtom d) -> Just $ DictCon d - _ -> Nothing - --- === Pattern synonyms === - -pattern IdxRepScalarBaseTy :: ScalarBaseType -pattern IdxRepScalarBaseTy = Word32Type - --- Type used to represent indices and sizes at run-time -pattern IdxRepTy :: Type n -pattern IdxRepTy = TyCon (BaseType (Scalar Word32Type)) - -pattern IdxRepVal :: Word32 -> Atom n -pattern IdxRepVal x = Con (Lit (Word32Lit x)) - -pattern IIdxRepVal :: Word32 -> IExpr n -pattern IIdxRepVal x = ILit (Word32Lit x) - -pattern IIdxRepTy :: IType -pattern IIdxRepTy = Scalar Word32Type - --- Type used to represent sum type tags at run-time -pattern TagRepTy :: Type n -pattern TagRepTy = TyCon (BaseType (Scalar Word8Type)) - -pattern TagRepVal :: Word8 -> Atom n -pattern TagRepVal x = Con (Lit (Word8Lit x)) - -pattern CharRepTy :: Type n -pattern CharRepTy = Word8Ty - -charRepVal :: Char -> Atom n -charRepVal c = Con (Lit (Word8Lit (fromIntegral $ fromEnum c))) - -pattern Word8Ty :: Type n -pattern Word8Ty = TyCon (BaseType (Scalar Word8Type)) - -pattern PairVal :: Atom n -> Atom n -> Atom n -pattern PairVal x y = Con (ProdCon [x, y]) - -pattern PairTy :: Type n -> Type n -> Type n -pattern PairTy x y = TyCon (ProdType [x, y]) - -pattern UnitVal :: Atom n -pattern UnitVal = Con (ProdCon []) - -pattern UnitTy :: Type n -pattern UnitTy = TyCon (ProdType []) - -pattern BaseTy :: BaseType -> Type n -pattern BaseTy b = TyCon (BaseType b) - -pattern PtrTy :: PtrType -> Type n -pattern PtrTy ty = TyCon (BaseType (PtrType ty)) - -pattern RefTy :: Type n -> Type n -pattern RefTy a = TyCon (RefType a) - -pattern TabTy :: IxDict n -> Binder n l -> Type l -> Type n -pattern TabTy d b body = TyCon (TabPi (TabPiType d b body)) - -pattern FinTy :: Atom n -> Type n -pattern FinTy n = TyCon (NewtypeTyCon (Fin n)) - -pattern NatTy :: Type n -pattern NatTy = TyCon (NewtypeTyCon Nat) - -pattern NatVal :: Word32 -> Atom n -pattern NatVal n = Con (NewtypeCon NatCon (IdxRepVal n)) - -pattern FinConst :: Word32 -> Type n -pattern FinConst n = TyCon (NewtypeTyCon (Fin (NatVal n))) - -pattern NullaryLamExpr :: Expr n -> LamExpr n -pattern NullaryLamExpr body = LamExpr Empty body - -pattern UnaryLamExpr :: Binder n l -> Expr l -> LamExpr n -pattern UnaryLamExpr b body = LamExpr (UnaryNest b) body - -pattern BinaryLamExpr :: Binder n l1 -> Binder l1 l2 -> Expr l2 -> LamExpr n -pattern BinaryLamExpr b1 b2 body = LamExpr (BinaryNest b1 b2) body - -pattern MaybeTy :: Type n -> Type n -pattern MaybeTy a = TyCon (SumType [UnitTy, a]) - -pattern NothingAtom :: Type n -> Atom n -pattern NothingAtom a = Con (SumCon [UnitTy, a] 0 UnitVal) - -pattern JustAtom :: Type n -> Atom n -> Atom n -pattern JustAtom a x = Con (SumCon [UnitTy, a] 1 x) - -pattern BoolTy :: Type n -pattern BoolTy = Word8Ty - -pattern FalseAtom :: Atom n -pattern FalseAtom = Con (Lit (Word8Lit 0)) - -pattern TrueAtom :: Atom n -pattern TrueAtom = Con (Lit (Word8Lit 1)) - --- === Typeclass instances for Name and other Haskell libraries === - -instance GenericE RepVal where - type RepE RepVal = PairE Type (ComposeE Tree IExpr) - fromE (RepVal ty tree) = ty `PairE` ComposeE tree - toE (ty `PairE` ComposeE tree) = RepVal ty tree - -instance SinkableE RepVal -instance RenameE RepVal -instance HoistableE RepVal -instance AlphaHashableE RepVal -instance AlphaEqE RepVal - -instance GenericE TyConParams where - type RepE TyConParams = PairE (LiftE [Explicitness]) (ListE CAtom) - fromE (TyConParams infs xs) = PairE (LiftE infs) (ListE xs) - {-# INLINE fromE #-} - toE (PairE (LiftE infs) (ListE xs)) = TyConParams infs xs - {-# INLINE toE #-} - --- We ignore the dictionary parameters because we assume coherence -instance AlphaEqE TyConParams where - alphaEqE params params' = - alphaEqE (ListE $ ignoreSynthParams params) (ListE $ ignoreSynthParams params') - -instance AlphaHashableE TyConParams where - hashWithSaltE env salt params = - hashWithSaltE env salt $ ListE $ ignoreSynthParams params - -ignoreSynthParams :: TyConParams n -> [CAtom n] -ignoreSynthParams (TyConParams infs xs) = [x | (inf, x) <- zip infs xs, notSynth inf] - where notSynth = \case - Inferred _ (Synth _) -> False - _ -> True - -instance SinkableE TyConParams -instance HoistableE TyConParams -instance RenameE TyConParams - -instance GenericE DataConDefs where - type RepE DataConDefs = EitherE (ListE DataConDef) (ListE (PairE (LiftE SourceName) CType)) - fromE = \case - ADTCons cons -> LeftE $ ListE cons - StructFields fields -> RightE $ ListE [PairE (LiftE name) ty | (name, ty) <- fields] - {-# INLINE fromE #-} - toE = \case - LeftE (ListE cons) -> ADTCons cons - RightE (ListE fields) -> StructFields [(name, ty) | PairE (LiftE name) ty <- fields] - {-# INLINE toE #-} - -instance SinkableE DataConDefs -instance HoistableE DataConDefs -instance RenameE DataConDefs -instance AlphaEqE DataConDefs -instance AlphaHashableE DataConDefs - -instance GenericE TyConDef where - type RepE TyConDef = PairE (LiftE (SourceName, [Explicitness])) (Abs (Nest CBinder) DataConDefs) - fromE (TyConDef sourceName expls bs cons) = PairE (LiftE (sourceName, expls)) (Abs bs cons) - {-# INLINE fromE #-} - toE (PairE (LiftE (sourceName, expls)) (Abs bs cons)) = TyConDef sourceName expls bs cons - {-# INLINE toE #-} - -deriving instance Show (TyConDef n) -deriving via WrapE TyConDef n instance Generic (TyConDef n) -instance SinkableE TyConDef -instance HoistableE TyConDef -instance RenameE TyConDef -instance AlphaEqE TyConDef -instance AlphaHashableE TyConDef - -instance HasNameHint (TyConDef n) where - getNameHint (TyConDef v _ _ _) = getNameHint v - -instance HasSourceName (TyConDef n) where - getSourceName (TyConDef v _ _ _) = v - -instance GenericE DataConDef where - type RepE DataConDef = (LiftE (SourceName, [[Projection]])) - `PairE` EmptyAbs (Nest CBinder) `PairE` Type - fromE (DataConDef name bs repTy idxs) = (LiftE (name, idxs)) `PairE` bs `PairE` repTy - {-# INLINE fromE #-} - toE ((LiftE (name, idxs)) `PairE` bs `PairE` repTy) = DataConDef name bs repTy idxs - {-# INLINE toE #-} -instance SinkableE DataConDef -instance HoistableE DataConDef -instance RenameE DataConDef -instance AlphaEqE DataConDef -instance AlphaHashableE DataConDef - -instance HasNameHint (DataConDef n) where - getNameHint (DataConDef v _ _ _) = getNameHint v - -instance GenericE NewtypeCon where - type RepE NewtypeCon = EitherE3 - {- UserADTData -} (LiftE SourceName `PairE` TyConName `PairE` TyConParams) - {- NatCon -} UnitE - {- FinCon -} CAtom - fromE = \case - UserADTData sn d p -> Case0 $ LiftE sn `PairE` d `PairE` p - NatCon -> Case1 UnitE - FinCon n -> Case2 n - {-# INLINE fromE #-} - toE = \case - Case0 (LiftE sn `PairE` d `PairE` p) -> UserADTData sn d p - Case1 UnitE -> NatCon - Case2 n -> FinCon n - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE NewtypeCon -instance HoistableE NewtypeCon -instance AlphaEqE NewtypeCon -instance AlphaHashableE NewtypeCon -instance RenameE NewtypeCon - -instance GenericE NewtypeTyCon where - type RepE NewtypeTyCon = EitherE3 - {- Nat -} UnitE - {- Fin -} CAtom - {- UserADTType -} (LiftE SourceName `PairE` TyConName `PairE` TyConParams) - fromE = \case - Nat -> Case0 UnitE - Fin n -> Case1 n - UserADTType s d p -> Case2 (LiftE s `PairE` d `PairE` p) - {-# INLINE fromE #-} - - toE = \case - Case0 UnitE -> Nat - Case1 n -> Fin n - Case2 (LiftE s `PairE` d `PairE` p) -> UserADTType s d p - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE NewtypeTyCon -instance HoistableE NewtypeTyCon -instance AlphaEqE NewtypeTyCon -instance AlphaHashableE NewtypeTyCon -instance RenameE NewtypeTyCon - -instance GenericE TypedHof where - type RepE TypedHof = EffTy `PairE` Hof - fromE (TypedHof effTy hof) = effTy `PairE` hof - {-# INLINE fromE #-} - toE (effTy `PairE` hof) = TypedHof effTy hof - {-# INLINE toE #-} - -instance SinkableE TypedHof -instance HoistableE TypedHof -instance RenameE TypedHof -instance AlphaEqE TypedHof -instance AlphaHashableE TypedHof - -instance GenericE Hof where - type RepE Hof = EitherE4 - {- For -} (LiftE ForAnn `PairE` IxType `PairE` LamExpr) - {- While -} Expr - {- Linearize -} (LamExpr `PairE` Atom) - {- Transpose -} (LamExpr `PairE` Atom) - - fromE = \case - For ann d body -> Case0 (LiftE ann `PairE` d `PairE` body) - While body -> Case1 body - Linearize body x -> Case2 (PairE body x) - Transpose body x -> Case3 (PairE body x) - {-# INLINE fromE #-} - toE = \case - Case0 (LiftE ann `PairE` d `PairE` body) -> For ann d body - Case1 body -> While body - Case2 (PairE body x) -> Linearize body x - Case3 (PairE body x) -> Transpose body x - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE Hof -instance HoistableE Hof -instance RenameE Hof -instance AlphaEqE Hof -instance AlphaHashableE Hof - -instance GenericE Atom where - type RepE Atom = EitherE (PairE Type Stuck) Con - fromE = \case - Stuck t x -> LeftE (PairE t x) - Con x -> RightE x - {-# INLINE fromE #-} - toE = \case - LeftE (PairE t x) -> Stuck t x - RightE x -> Con x - {-# INLINE toE #-} - -instance SinkableE Atom -instance HoistableE Atom -instance AlphaEqE Atom -instance AlphaHashableE Atom -instance RenameE Atom - -instance GenericE Stuck where - type RepE Stuck = EitherE2 - (EitherE6 - {- Var -} AtomVar - {- StuckProject -} (LiftE Int `PairE` Stuck) - {- StuckTabApp -} (Stuck `PairE` Atom) - {- StuckUnwrap -} (CStuck) - {- InstantiatedGiven -} (CStuck `PairE` ListE CAtom) - {- SuperclassProj -} (LiftE Int `PairE` CStuck) - ) (EitherE2 - {- PtrVar -} (LiftE PtrType `PairE` PtrName) - {- RepValAtom -} RepVal - ) - - fromE = \case - Var v -> Case0 $ Case0 v - StuckProject i e -> Case0 $ Case1 $ LiftE i `PairE` e - StuckTabApp f x -> Case0 $ Case2 $ f `PairE` x - StuckUnwrap e -> Case0 $ Case3 $ e - InstantiatedGiven e xs -> Case0 $ Case4 $ e `PairE` ListE xs - SuperclassProj i e -> Case0 $ Case5 $ LiftE i `PairE` e - PtrVar t p -> Case1 $ Case0 $ LiftE t `PairE` p - RepValAtom r -> Case1 $ Case1 $ r - {-# INLINE fromE #-} - - toE = \case - Case0 con -> case con of - Case0 v -> Var v - Case1 (LiftE i `PairE` e) -> StuckProject i e - Case2 (f `PairE` x) -> StuckTabApp f x - Case3 e -> StuckUnwrap e - Case4 (e `PairE` ListE xs) -> InstantiatedGiven e xs - Case5 (LiftE i `PairE` e) -> SuperclassProj i e - _ -> error "impossible" - Case1 con -> case con of - Case0 (LiftE t `PairE` p) -> PtrVar t p - Case1 r -> RepValAtom r - _ -> error "impossible" - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE Stuck -instance HoistableE Stuck -instance AlphaEqE Stuck -instance AlphaHashableE Stuck -instance RenameE Stuck - -instance GenericE AtomVar where - type RepE AtomVar = PairE AtomName Type - fromE (AtomVar v t) = PairE v t - {-# INLINE fromE #-} - toE (PairE v t) = AtomVar v t - {-# INLINE toE #-} - -instance HasNameHint (AtomVar n) where - getNameHint (AtomVar v _) = getNameHint v - -instance Eq (AtomVar n) where - AtomVar v1 _ == AtomVar v2 _ = v1 == v2 - -instance SinkableE AtomVar -instance HoistableE AtomVar - --- We ignore the type annotation because it should be determined by the var -instance AlphaEqE AtomVar where - alphaEqE (AtomVar v _) (AtomVar v' _) = alphaEqE v v' - --- We ignore the type annotation because it should be determined by the var -instance AlphaHashableE AtomVar where - hashWithSaltE env salt (AtomVar v _) = hashWithSaltE env salt v - -instance RenameE AtomVar - -instance GenericE Type where - type RepE Type = EitherE (PairE (LiftE Kind) Stuck ) TyCon - fromE = \case - StuckTy k x -> LeftE (PairE (LiftE k) x) - TyCon x -> RightE x - {-# INLINE fromE #-} - toE = \case - LeftE (PairE (LiftE k) x) -> StuckTy k x - RightE x -> TyCon x - {-# INLINE toE #-} - -instance SinkableE Type -instance HoistableE Type -instance AlphaEqE Type -instance AlphaHashableE Type -instance RenameE Type - -instance GenericE Expr where - type RepE Expr = EitherE2 - ( EitherE6 - {- App -} (EffTy `PairE` Atom `PairE` ListE Atom) - {- TabApp -} (Type `PairE` Atom `PairE` Atom) - {- Case -} (Atom `PairE` ListE Alt `PairE` EffTy) - {- Atom -} Atom - {- TopApp -} (EffTy `PairE` TopFunName `PairE` ListE Atom) - {- Block -} (EffTy `PairE` Block) - ) - ( EitherE6 - {- TabCon -} (Type `PairE` ListE Atom) - {- PrimOp -} (Type `PairE` ComposeE PrimOp Atom) - {- ApplyMethod -} (EffTy `PairE` Atom `PairE` LiftE Int `PairE` ListE Atom) - {- Project -} (Type `PairE` LiftE Int `PairE` Atom) - {- Unwrap -} (CType `PairE` CAtom) - {- Hof -} TypedHof) - fromE = \case - App et f xs -> Case0 $ Case0 (et `PairE` f `PairE` ListE xs) - TabApp t f x -> Case0 $ Case1 (t `PairE` f `PairE` x) - Case e alts effTy -> Case0 $ Case2 (e `PairE` ListE alts `PairE` effTy) - Atom x -> Case0 $ Case3 (x) - TopApp et f xs -> Case0 $ Case4 (et `PairE` f `PairE` ListE xs) - Block et block -> Case0 $ Case5 (et `PairE` block) - TabCon ty xs -> Case1 $ Case0 (ty `PairE` ListE xs) - PrimOp ty op -> Case1 $ Case1 (ty `PairE` ComposeE op) - ApplyMethod et d i xs -> Case1 $ Case2 (et `PairE` d `PairE` LiftE i `PairE` ListE xs) - Project ty i x -> Case1 $ Case3 (ty `PairE` LiftE i `PairE` x) - Unwrap t x -> Case1 $ Case4 (t `PairE` x) - Hof hof -> Case1 $ Case5 hof - {-# INLINE fromE #-} - toE = \case - Case0 case0 -> case case0 of - Case0 (et `PairE` f `PairE` ListE xs) -> App et f xs - Case1 (t `PairE` f `PairE` x) -> TabApp t f x - Case2 (e `PairE` ListE alts `PairE` effTy) -> Case e alts effTy - Case3 (x) -> Atom x - Case4 (et `PairE` f `PairE` ListE xs) -> TopApp et f xs - Case5 (et `PairE` block) -> Block et block - _ -> error "impossible" - Case1 case1 -> case case1 of - Case0 (ty `PairE` ListE xs) -> TabCon ty xs - Case1 (ty `PairE` ComposeE op) -> PrimOp ty op - Case2 (et `PairE` d `PairE` LiftE i `PairE` ListE xs) -> ApplyMethod et d i xs - Case3 (ty `PairE` LiftE i `PairE` x) -> Project ty i x - Case4 (t `PairE` x) -> Unwrap t x - Case5 hof -> Hof hof - _ -> error "impossible" - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE Expr -instance HoistableE Expr -instance AlphaEqE Expr -instance AlphaHashableE Expr -instance RenameE Expr - -instance GenericE Con where - type RepE Con = EitherE2 - (EitherE4 - {- Lit -} (LiftE LitVal) - {- ProdCon -} (ListE Atom) - {- SumCon -} (ListE Type `PairE` LiftE Int `PairE` Atom) - {- DepPair -} (Atom `PairE` Atom `PairE` DepPairType) - ) (EitherE4 - {- Lam -} CoreLamExpr - {- NewtypeCon -} (NewtypeCon `PairE` CAtom) - {- DictConAtom -} (DictCon) - {- TyConAtom -} TyCon) - fromE = \case - Lit l -> Case0 $ Case0 $ LiftE l - ProdCon xs -> Case0 $ Case1 $ ListE xs - SumCon ts i x -> Case0 $ Case2 $ ListE ts `PairE` LiftE i `PairE` x - DepPair x y t -> Case0 $ Case3 $ x `PairE` y `PairE` t - Lam lam -> Case1 $ Case0 lam - NewtypeCon con x -> Case1 $ Case1 $ con `PairE` x - DictConAtom con -> Case1 $ Case2 con - TyConAtom tc -> Case1 $ Case3 tc - {-# INLINE fromE #-} - toE = \case - Case0 con -> case con of - Case0 (LiftE l) -> Lit l - Case1 (ListE xs) -> ProdCon xs - Case2 (ListE ts `PairE` LiftE i `PairE` x) -> SumCon ts i x - Case3 (x `PairE` y `PairE` t) -> DepPair x y t - _ -> error "impossible" - Case1 (con) -> case con of - Case0 lam -> Lam lam - Case1 (con' `PairE` x) -> NewtypeCon con' x - Case2 con' -> DictConAtom con' - Case3 tc -> TyConAtom tc - _ -> error "impossible" - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE Con -instance HoistableE Con -instance AlphaEqE Con -instance AlphaHashableE Con -instance RenameE Con - -instance GenericE TyCon where - type RepE TyCon = EitherE3 - (EitherE4 - {- BaseType -} (LiftE BaseType) - {- ProdType -} (ListE Type) - {- SumType -} (ListE Type) - {- RefType -} Type) - (EitherE3 - {- TabPi -} TabPiType - {- DepPairTy -} DepPairType - {- Kind -} (LiftE Kind)) - (EitherE3 - {- DictTy -} (DictType) - {- Pi -} (CorePiType) - {- NewtypeTyCon -} (NewtypeTyCon)) - fromE = \case - BaseType b -> Case0 (Case0 (LiftE b)) - ProdType ts -> Case0 (Case1 (ListE ts)) - SumType ts -> Case0 (Case2 (ListE ts)) - RefType t -> Case0 (Case3 t) - TabPi t -> Case1 (Case0 t) - DepPairTy t -> Case1 (Case1 t) - Kind k -> Case1 (Case2 (LiftE k)) - DictTy t -> Case2 (Case0 t) - Pi t -> Case2 (Case1 t) - NewtypeTyCon t -> Case2 (Case2 t) - {-# INLINE fromE #-} - toE = \case - Case0 c -> case c of - Case0 (LiftE b ) -> BaseType b - Case1 (ListE ts) -> ProdType ts - Case2 (ListE ts) -> SumType ts - Case3 t -> RefType t - _ -> error "impossible" - Case1 c -> case c of - Case0 t -> TabPi t - Case1 t -> DepPairTy t - Case2 (LiftE k) -> Kind k - _ -> error "impossible" - Case2 c -> case c of - Case0 t -> DictTy t - Case1 t -> Pi t - Case2 t -> NewtypeTyCon t - _ -> error "impossible" - _ -> error "impossible" - {-# INLINE toE #-} - -instance SinkableE TyCon -instance HoistableE TyCon -instance AlphaEqE TyCon -instance AlphaHashableE TyCon -instance RenameE TyCon - -instance GenericB (NonDepNest ann) where - type RepB (NonDepNest ann) = (LiftB (ListE ann)) `PairB` Nest AtomNameBinder - fromB (NonDepNest bs anns) = LiftB (ListE anns) `PairB` bs - {-# INLINE fromB #-} - toB (LiftB (ListE anns) `PairB` bs) = NonDepNest bs anns - {-# INLINE toB #-} -instance ProvesExt (NonDepNest ann) -instance BindsNames (NonDepNest ann) -instance (SinkableE ann) => SinkableB (NonDepNest ann) -instance (HoistableE ann) => HoistableB (NonDepNest ann) -instance (RenameE ann, SinkableE ann) => RenameB (NonDepNest ann) -instance (AlphaEqE ann) => AlphaEqB (NonDepNest ann) -instance (AlphaHashableE ann) => AlphaHashableB (NonDepNest ann) -deriving instance (Show (ann n)) => Show (NonDepNest ann n l) - -instance GenericE ClassDef where - type RepE ClassDef = - LiftE (SourceName, Maybe BuiltinClassName, [SourceName], [Maybe SourceName], [Explicitness]) - `PairE` Abs (Nest CBinder) (Abs (Nest CBinder) (ListE CorePiType)) - fromE (ClassDef name builtin names paramNames roleExpls b scs tys) = - LiftE (name, builtin, names, paramNames, roleExpls) `PairE` Abs b (Abs scs (ListE tys)) - {-# INLINE fromE #-} - toE (LiftE (name, builtin, names, paramNames, roleExpls) `PairE` Abs b (Abs scs (ListE tys))) = - ClassDef name builtin names paramNames roleExpls b scs tys - {-# INLINE toE #-} - -instance SinkableE ClassDef -instance HoistableE ClassDef -instance AlphaEqE ClassDef -instance AlphaHashableE ClassDef -instance RenameE ClassDef -deriving instance Show (ClassDef n) -deriving via WrapE ClassDef n instance Generic (ClassDef n) -instance HasSourceName (ClassDef n) where - getSourceName = \case ClassDef name _ _ _ _ _ _ _ -> name - -instance GenericE InstanceDef where - type RepE InstanceDef = - ClassName `PairE` LiftE [Explicitness] `PairE` Abs (Nest CBinder) (ListE CAtom `PairE` InstanceBody) - fromE (InstanceDef name expls bs params body) = - name `PairE` LiftE expls `PairE` Abs bs (ListE params `PairE` body) - toE (name `PairE` LiftE expls `PairE` Abs bs (ListE params `PairE` body)) = - InstanceDef name expls bs params body - -instance SinkableE InstanceDef -instance HoistableE InstanceDef -instance AlphaEqE InstanceDef -instance AlphaHashableE InstanceDef -instance RenameE InstanceDef -deriving instance Show (InstanceDef n) -deriving via WrapE InstanceDef n instance Generic (InstanceDef n) - -instance GenericE InstanceBody where - type RepE InstanceBody = ListE CAtom `PairE` ListE CAtom - fromE (InstanceBody scs methods) = ListE scs `PairE` ListE methods - toE (ListE scs `PairE` ListE methods) = InstanceBody scs methods - -instance SinkableE InstanceBody -instance HoistableE InstanceBody -instance AlphaEqE InstanceBody -instance AlphaHashableE InstanceBody -instance RenameE InstanceBody - -instance GenericE DictType where - type RepE DictType = EitherE2 - {- DictType -} (LiftE SourceName `PairE` ClassName `PairE` ListE CAtom) - {- IxDictType -} CType - fromE = \case - DictType sourceName className params -> Case0 $ LiftE sourceName `PairE` className `PairE` ListE params - IxDictType ty -> Case1 ty - toE = \case - Case0 (LiftE sourceName `PairE` className `PairE` ListE params) -> DictType sourceName className params - Case1 ty -> IxDictType ty - _ -> error "impossible" - -instance SinkableE DictType -instance HoistableE DictType -instance AlphaEqE DictType -instance AlphaHashableE DictType -instance RenameE DictType - -instance GenericE Dict where - type RepE Dict = EitherE (PairE Type Stuck) DictCon - fromE = \case - StuckDict t d -> LeftE (PairE t d) - DictCon d -> RightE d - {-# INLINE fromE #-} - toE = \case - LeftE (PairE t d) -> StuckDict t d - RightE d -> DictCon d - {-# INLINE toE #-} - -instance SinkableE Dict -instance HoistableE Dict -instance AlphaEqE Dict -instance AlphaHashableE Dict -instance RenameE Dict - -instance GenericE DictCon where - type RepE DictCon = EitherE4 - {- InstanceDict -} (CType `PairE` PairE InstanceName (ListE CAtom)) - {- IxFin -} CAtom - {- IxRawFin -} Atom - {- IxSpecialized -} (SpecDictName `PairE` ListE SAtom) - fromE = \case - InstanceDict t v args -> Case0 $ t `PairE` PairE v (ListE args) - IxFin x -> Case1 $ x - IxRawFin n -> Case2 $ n - IxSpecialized d xs -> Case3 $ d `PairE` ListE xs - toE = \case - Case0 (t `PairE` (PairE v (ListE args))) -> InstanceDict t v args - Case1 x -> IxFin x - Case2 n -> IxRawFin n - Case3 (d `PairE` ListE xs) -> IxSpecialized d xs - _ -> error "impossible" - -instance SinkableE DictCon -instance HoistableE DictCon -instance AlphaEqE DictCon -instance AlphaHashableE DictCon -instance RenameE DictCon - -instance GenericE LamExpr where - type RepE LamExpr = Abs (Nest Binder) Expr - fromE (LamExpr b block) = Abs b block - {-# INLINE fromE #-} - toE (Abs b block) = LamExpr b block - {-# INLINE toE #-} - -instance SinkableE LamExpr -instance HoistableE LamExpr -instance AlphaEqE LamExpr -instance AlphaHashableE LamExpr -instance RenameE LamExpr -deriving instance Show (LamExpr n) -deriving via WrapE LamExpr n instance Generic (LamExpr n) - -instance GenericE CoreLamExpr where - type RepE CoreLamExpr = CorePiType `PairE` LamExpr - fromE (CoreLamExpr ty lam) = ty `PairE` lam - {-# INLINE fromE #-} - toE (ty `PairE` lam) = CoreLamExpr ty lam - {-# INLINE toE #-} - -instance SinkableE CoreLamExpr -instance HoistableE CoreLamExpr -instance AlphaEqE CoreLamExpr -instance AlphaHashableE CoreLamExpr -instance RenameE CoreLamExpr - -instance GenericE CorePiType where - type RepE CorePiType = LiftE (AppExplicitness, [Explicitness]) `PairE` Abs (Nest CBinder) (Type) - fromE (CorePiType ex exs b effTy) = LiftE (ex, exs) `PairE` Abs b effTy - {-# INLINE fromE #-} - toE (LiftE (ex, exs) `PairE` Abs b effTy) = CorePiType ex exs b effTy - {-# INLINE toE #-} - -instance SinkableE CorePiType -instance HoistableE CorePiType -instance AlphaEqE CorePiType -instance AlphaHashableE CorePiType -instance RenameE CorePiType -deriving instance Show (CorePiType n) -deriving via WrapE CorePiType n instance Generic (CorePiType n) - -instance GenericE IxType where - type RepE IxType = PairE Type IxDict - fromE (IxType ty d) = PairE ty d - {-# INLINE fromE #-} - toE (PairE ty d) = IxType ty d - {-# INLINE toE #-} - -instance SinkableE IxType -instance HoistableE IxType -instance RenameE IxType - -instance AlphaEqE IxType where - alphaEqE (IxType t1 _) (IxType t2 _) = alphaEqE t1 t2 - -instance AlphaHashableE IxType where - hashWithSaltE env salt (IxType t _) = hashWithSaltE env salt t - -instance GenericE TabPiType where - type RepE TabPiType = PairE IxDict (Abs Binder Type) - fromE (TabPiType d b resultTy) = PairE d (Abs b resultTy) - {-# INLINE fromE #-} - toE (PairE d (Abs b resultTy)) = TabPiType d b resultTy - {-# INLINE toE #-} - -instance AlphaEqE TabPiType where - alphaEqE (TabPiType _ b1 t1) (TabPiType _ b2 t2) = - alphaEqE (Abs b1 t1) (Abs b2 t2) - -instance AlphaHashableE TabPiType where - hashWithSaltE env salt (TabPiType _ b t) = hashWithSaltE env salt $ Abs b t - -instance HasNameHint (TabPiType n) where - getNameHint (TabPiType _ b _) = getNameHint b - -instance SinkableE TabPiType -instance HoistableE TabPiType -instance RenameE TabPiType -deriving instance Show (TabPiType n) -deriving via WrapE TabPiType n instance Generic (TabPiType n) - -instance GenericE PiType where - type RepE PiType = Abs (Nest Binder) Type - fromE (PiType bs effTy) = Abs bs effTy - {-# INLINE fromE #-} - toE (Abs bs effTy) = PiType bs effTy - {-# INLINE toE #-} - -instance SinkableE PiType -instance HoistableE PiType -instance AlphaEqE PiType -instance AlphaHashableE PiType -instance RenameE PiType -deriving instance Show (PiType n) -deriving via WrapE PiType n instance Generic (PiType n) -instance Store (PiType n) - -instance GenericE DepPairType where - type RepE DepPairType = PairE (LiftE DepPairExplicitness) (Abs Binder Type) - fromE (DepPairType expl b resultTy) = LiftE expl `PairE` Abs b resultTy - {-# INLINE fromE #-} - toE (LiftE expl `PairE` Abs b resultTy) = DepPairType expl b resultTy - {-# INLINE toE #-} - -instance SinkableE DepPairType -instance HoistableE DepPairType -instance AlphaEqE DepPairType -instance AlphaHashableE DepPairType -instance RenameE DepPairType -deriving instance Show (DepPairType n) -deriving via WrapE DepPairType n instance Generic (DepPairType n) - -instance GenericE DotMethods where - type RepE DotMethods = ListE (LiftE SourceName `PairE` CAtomName) - fromE (DotMethods xys) = ListE $ [LiftE x `PairE` y | (x, y) <- M.toList xys] - {-# INLINE fromE #-} - toE (ListE xys) = DotMethods $ M.fromList [(x, y) | LiftE x `PairE` y <- xys] - {-# INLINE toE #-} - -instance SinkableE DotMethods -instance HoistableE DotMethods -instance RenameE DotMethods -instance AlphaEqE DotMethods -instance AlphaHashableE DotMethods - -instance GenericE Effects where - type RepE Effects = EitherE UnitE UnitE - fromE = \case - Pure -> LeftE UnitE - Effectful -> RightE UnitE - {-# INLINE fromE #-} - toE = \case - LeftE UnitE -> Pure - RightE UnitE -> Effectful - {-# INLINE toE #-} - -instance SinkableE Effects -instance HoistableE Effects -instance RenameE Effects -instance AlphaEqE Effects -instance AlphaHashableE Effects - -instance GenericE EffTy where - type RepE EffTy = PairE Effects Type - fromE (EffTy eff ty) = eff `PairE` ty - {-# INLINE fromE #-} - toE (eff `PairE` ty) = EffTy eff ty - {-# INLINE toE #-} - -instance SinkableE EffTy -instance HoistableE EffTy -instance RenameE EffTy -instance AlphaEqE EffTy -instance AlphaHashableE EffTy - -instance GenericE DeclBinding where - type RepE DeclBinding = LiftE LetAnn `PairE` Expr - fromE (DeclBinding ann expr) = LiftE ann `PairE` expr - {-# INLINE fromE #-} - toE (LiftE ann `PairE` expr) = DeclBinding ann expr - {-# INLINE toE #-} - -instance SinkableE DeclBinding -instance HoistableE DeclBinding -instance RenameE DeclBinding -instance AlphaEqE DeclBinding -instance AlphaHashableE DeclBinding - -instance GenericB Decl where - type RepB Decl = AtomBinderP DeclBinding - fromB (Let b binding) = b :> binding - {-# INLINE fromB #-} - toB (b :> binding) = Let b binding - {-# INLINE toB #-} - -instance SinkableB Decl -instance HoistableB Decl -instance RenameB Decl -instance AlphaEqB Decl -instance AlphaHashableB Decl -instance ProvesExt Decl -instance BindsNames Decl - -instance BindsAtMostOneName Decl where - Let b _ @> x = b @> x - {-# INLINE (@>) #-} - -instance BindsOneName Decl where - binderName (Let b _) = binderName b - {-# INLINE binderName #-} - -instance Hashable IxMethod -instance Hashable BuiltinClassName -instance Hashable Kind - -instance Store (TyCon n) -instance Store (Con n) -instance Store (RepVal n) -instance Store (Type n) -instance Store Kind -instance Store (Effects n) -instance Store (EffTy n) -instance Store (Stuck n) -instance Store (Atom n) -instance Store (AtomVar n) -instance Store (Expr n) -instance Store (DeclBinding n) -instance Store (Decl n l) -instance Store (TyConParams n) -instance Store (DataConDefs n) -instance Store (TyConDef n) -instance Store (DataConDef n) -instance Store (LamExpr n) -instance Store (IxType n) -instance Store (CorePiType n) -instance Store (CoreLamExpr n) -instance Store (TabPiType n) -instance Store (DepPairType n) -instance Store BuiltinClassName -instance Store (ClassDef n) -instance Store (InstanceDef n) -instance Store (InstanceBody n) -instance Store (DictType n) -instance Store (DictCon n) -instance Store (ann n) => Store (NonDepNest ann n l) -instance Store IxMethod -instance Store (Dict n) -instance Store (TypedHof n) -instance Store (Hof n) -instance Store (NewtypeCon n) -instance Store (NewtypeTyCon n) -instance Store (DotMethods n) - --- === Pretty instances === - -instance Pretty (Hof n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (Hof n) where - prettyPrec hof = atPrec LowestPrec case hof of - For _ _ lam -> "for" <+> pLowest lam - While body -> "while" <+> pArg body - Linearize body x -> "linearize" <+> pArg body <+> pArg x - Transpose body x -> "transpose" <+> pArg body <+> pArg x - -instance Pretty (TyCon n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (TyCon n) where - prettyPrec con = case con of - BaseType b -> prettyPrec b - ProdType [] -> atPrec ArgPrec $ "()" - ProdType as -> atPrec ArgPrec $ align $ group $ - encloseSep "(" ")" ", " $ fmap pApp as - SumType cs -> atPrec ArgPrec $ align $ group $ - encloseSep "(|" "|)" " | " $ fmap pApp cs - RefType a -> atPrec AppPrec $ "Ref" <+> p a - Kind k -> atPrec ArgPrec $ pretty $ show k - Pi piType -> atPrec LowestPrec $ align $ p piType - TabPi piType -> atPrec LowestPrec $ align $ p piType - DepPairTy ty -> prettyPrec ty - DictTy t -> atPrec LowestPrec $ p t - NewtypeTyCon con' -> prettyPrec con' - where - p :: Pretty a => a -> Doc ann - p = pretty - -prettyPrecNewtype :: NewtypeCon n -> CAtom n -> DocPrec ann -prettyPrecNewtype con x = case (con, x) of - (NatCon, (IdxRepVal n)) -> atPrec ArgPrec $ pretty n - (_, x') -> prettyPrec x' - -instance Pretty (NewtypeTyCon n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (NewtypeTyCon n) where - prettyPrec = \case - Nat -> atPrec ArgPrec $ "Nat" - Fin n -> atPrec AppPrec $ "Fin" <+> pArg n - UserADTType name _ (TyConParams infs params) -> case (infs, params) of - ([], []) -> atPrec ArgPrec $ pretty name - ([Explicit, Explicit], [l, r]) - | Just sym <- fromInfix (fromString $ pprint name) -> - atPrec ArgPrec $ align $ group $ - parens $ flatAlt " " "" <> pApp l <> line <> pretty sym <+> pApp r - _ -> atPrec LowestPrec $ pAppArg (pretty name) $ ignoreSynthParams (TyConParams infs params) - where - fromInfix :: Text -> Maybe Text - fromInfix t = do - ('(', t') <- uncons t - (t'', ')') <- unsnoc t' - return t'' - -instance Pretty (Con n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (Con n) where - prettyPrec = \case - Lit l -> prettyPrec l - ProdCon [x] -> atPrec ArgPrec $ "(" <> pLowest x <> ",)" - ProdCon xs -> atPrec ArgPrec $ align $ group $ - encloseSep "(" ")" ", " $ fmap pLowest xs - SumCon _ tag payload -> atPrec ArgPrec $ - "(" <> p tag <> "|" <+> pApp payload <+> "|)" - Lam lam -> atPrec LowestPrec $ p lam - DepPair x y _ -> atPrec ArgPrec $ align $ group $ - parens $ p x <+> ",>" <+> p y - DictConAtom d -> atPrec LowestPrec $ p d - NewtypeCon con x -> prettyPrecNewtype con x - TyConAtom ty -> prettyPrec ty - where - p :: Pretty a => a -> Doc ann - p = pretty - -instance Pretty IxMethod where - pretty method = pretty $ show method - -instance Pretty (TyConParams n) where - pretty (TyConParams _ _) = undefined - -instance Pretty (TyConDef n) where - pretty (TyConDef name _ bs cons) = "enum" <+> pretty name <+> pretty bs <> pretty cons - -instance Pretty (DataConDefs n) where - pretty = undefined - -instance Pretty (DataConDef n) where - pretty (DataConDef name _ repTy _) = pretty name <+> ":" <+> pretty repTy - -instance Pretty (ClassDef n) where - pretty (ClassDef classSourceName _ methodNames _ _ params superclasses methodTys) = - "Class:" <+> pretty classSourceName <+> pretty methodNames - <> indented ( - line <> "parameter binders:" <+> pretty params <> - line <> "superclasses:" <+> pretty superclasses <> - line <> "methods:" <+> pretty methodTys) - -instance Pretty (InstanceDef n) where - pretty (InstanceDef className _ bs params _) = - "Instance" <+> pretty className <+> pretty bs <+> pretty params - -instance Pretty (Expr n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (Expr n) where - prettyPrec = \case - Atom x -> prettyPrec x - Block _ (Abs decls body) -> atPrec AppPrec $ prettyBlock decls body - App _ f xs -> atPrec AppPrec $ pApp f <+> spaced (toList xs) - TopApp _ f xs -> atPrec AppPrec $ pApp f <+> spaced (toList xs) - TabApp _ f x -> atPrec AppPrec $ pApp f <> brackets (p x) - Case e alts _ -> prettyPrecCase "case" e alts - TabCon _ es -> atPrec ArgPrec $ list $ pApp <$> es - PrimOp _ op -> prettyPrec op - ApplyMethod _ d i xs -> atPrec AppPrec $ "applyMethod" <+> p d <+> p i <+> p xs - Project _ i x -> atPrec AppPrec $ "Project" <+> p i <+> p x - Unwrap _ x -> atPrec AppPrec $ "Unwrap" <+> p x - Hof (TypedHof _ hof) -> prettyPrec hof - where - p :: Pretty a => a -> Doc ann - p = pretty - -prettyPrecCase :: Doc ann -> Atom n -> [Alt n] -> DocPrec ann -prettyPrecCase name e alts = atPrec LowestPrec $ - name <+> pApp e <+> "of" <> - nest 2 (foldMap (\alt -> hardline <> prettyAlt alt) alts) - -prettyAlt :: Alt n -> Doc ann -prettyAlt (Abs b body) = prettyBinderNoAnn b <+> "->" <> nest 2 (pretty body) - -prettyBinderNoAnn :: Binder n l -> Doc ann -prettyBinderNoAnn (b:>_) = pretty b - -instance Pretty (DeclBinding n) where - pretty (DeclBinding ann expr) = "Decl" <> pretty ann <+> pretty expr - -instance Pretty (Decl n l) where - pretty (Let b (DeclBinding ann rhs)) = - align $ annDoc <> pretty b <+> "=" <> (nest 2 $ group $ line <> pLowest rhs) - where annDoc = case ann of NoInlineLet -> pretty ann <> " "; _ -> pretty ann - -instance Pretty (PiType n) where - pretty (PiType bs resultTy) = - (spaced $ unsafeFromNest $ bs) <+> "->" <+> pretty resultTy - -instance Pretty (LamExpr n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (LamExpr n) where - prettyPrec (LamExpr bs body) = atPrec LowestPrec $ prettyLam (pretty bs <> ".") body - -instance Pretty (IxType n) where - pretty (IxType ty dict) = parens $ "IxType" <+> pretty ty <> prettyIxDict dict - -instance Pretty (Dict n) where - pretty = \case - DictCon con -> pretty con - StuckDict _ stuck -> pretty stuck - -instance Pretty (DictCon n) where - pretty = \case - InstanceDict _ name args -> "Instance" <+> pretty name <+> pretty args - IxFin n -> "Ix (Fin" <+> pretty n <> ")" - IxRawFin n -> "Ix (RawFin " <> pretty n <> ")" - IxSpecialized d xs -> pretty d <+> pretty xs - -instance Pretty (DictType n) where - pretty = \case - DictType classSourceName _ params -> pretty classSourceName <+> spaced params - IxDictType ty -> "Ix" <+> pretty ty - -instance Pretty (DepPairType n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (DepPairType n) where - prettyPrec (DepPairType _ b rhs) = - atPrec ArgPrec $ align $ group $ parensSep (spaceIfColinear <> "&> ") [pretty b, pretty rhs] - -instance Pretty (CoreLamExpr n) where - pretty (CoreLamExpr _ lam) = pretty lam - -instance Pretty (Atom n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (Atom n) where - prettyPrec atom = case atom of - Con e -> prettyPrec e - Stuck _ e -> prettyPrec e - -instance Pretty (Type n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (Type n) where - prettyPrec = \case - TyCon e -> prettyPrec e - StuckTy _ e -> prettyPrec e - -instance Pretty (Stuck n) where pretty = prettyFromPrettyPrec -instance PrettyPrec (Stuck n) where - prettyPrec = \case - Var v -> atPrec ArgPrec $ p v - StuckProject i v -> atPrec LowestPrec $ "StuckProject" <+> p i <+> p v - StuckTabApp f xs -> atPrec AppPrec $ pArg f <> "." <> pArg xs - StuckUnwrap v -> atPrec LowestPrec $ "StuckUnwrap" <+> p v - InstantiatedGiven v args -> atPrec LowestPrec $ "Given" <+> p v <+> p (toList args) - SuperclassProj d' i -> atPrec LowestPrec $ "SuperclassProj" <+> p d' <+> p i - PtrVar _ v -> atPrec ArgPrec $ p v - RepValAtom x -> atPrec LowestPrec $ pretty x - where - p :: Pretty a => a -> Doc ann - p = pretty - -instance PrettyPrec (AtomVar n) where - prettyPrec (AtomVar v _) = prettyPrec v -instance Pretty (AtomVar n) where pretty = prettyFromPrettyPrec - -prettyLam :: Pretty a => Doc ann -> a -> Doc ann -prettyLam binders body = group $ group (nest 4 $ binders) <> group (nest 2 $ pretty body) - -instance Pretty (TabPiType n) where - pretty (TabPiType dict (b:>ty) body) = let - prettyBody = case body of - TyCon (Pi subpi) -> pretty subpi - _ -> pLowest body - prettyBinder = prettyBinderHelper (b:>ty) body - in prettyBinder <> prettyIxDict dict <> (group $ line <> "=>" <+> prettyBody) - --- A helper to let us turn dict printing on and off. We mostly want it off to --- reduce clutter in prints and error messages, but when debugging synthesis we --- want it on. -prettyIxDict :: IxDict n -> Doc ann -prettyIxDict dict = if False then " " <> pretty dict else mempty - -prettyBinderHelper :: HoistableE e => Binder n l -> e l -> Doc ann -prettyBinderHelper (b:>ty) body = - if binderName b `isFreeIn` body - then parens $ pretty (b:>ty) - else pretty ty - -instance Pretty (CorePiType n) where - pretty (CorePiType appExpl expls bs resultTy) = - prettyBindersWithExpl expls bs <+> pretty appExpl <> pretty resultTy - -prettyBindersWithExpl :: forall b n l ann. PrettyB b - => [Explicitness] -> Nest b n l -> Doc ann -prettyBindersWithExpl expls bs = do - let groups = groupByExpl $ zip expls (unsafeFromNest bs) - let groups' = case groups of [] -> [(Explicit, [])] - _ -> groups - mconcat [withExplParens expl $ commaSep bsGroup | (expl, bsGroup) <- groups'] - -groupByExpl :: [(Explicitness, b UnsafeS UnsafeS)] -> [(Explicitness, [b UnsafeS UnsafeS])] -groupByExpl [] = [] -groupByExpl ((expl, b):bs) = do - let (matches, rest) = span (\(expl', _) -> expl == expl') bs - let matches' = map snd matches - (expl, b:matches') : groupByExpl rest - -withExplParens :: Explicitness -> Doc ann -> Doc ann -withExplParens Explicit x = parens x -withExplParens (Inferred _ Unify) x = braces $ x -withExplParens (Inferred _ (Synth _)) x = brackets x - -instance Pretty (RepVal n) where - pretty (RepVal ty tree) = " pretty tree <+> ":" <+> pretty ty <> ">" - -prettyBlock :: PrettyPrec (e l) => Nest Decl n l -> e l -> Doc ann -prettyBlock Empty expr = group $ line <> pLowest expr -prettyBlock decls expr = prettyLines decls' <> hardline <> pLowest expr - where decls' = unsafeFromNest decls diff --git a/src/lib/Types/Simple.hs b/src/lib/Types/Simple.hs new file mode 100644 index 000000000..b033b3815 --- /dev/null +++ b/src/lib/Types/Simple.hs @@ -0,0 +1,125 @@ + +-- Copyright 2022 Google LLC +-- +-- Use of this source code is governed by a BSD-style +-- license that can be found in the LICENSE file or at +-- https://developers.google.com/open-source/licenses/bsd + +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE StrictData #-} + +module Types.Simple (module Types.Simple) where + +import Data.Word +import Data.Foldable (toList) +import Data.Hashable +import Data.String (fromString) +import Data.Text.Prettyprint.Doc +import Data.Text (Text, unsnoc, uncons) +import qualified Data.Map.Strict as M + +import GHC.Generics (Generic (..)) +import Data.Store (Store (..)) + +import Name +import Util (Tree (..)) +import PPrint + +import Types.Primitives +import Types.Source (HasSourceName (..)) +import Types.Imp + +-- === SimpIR === + +data Expr (n::S) = + Block (Type n) (Block n) + | TopApp (Type n) (TopFunName n) [Atom n] + | Case (Type n) (Atom n) [LamExpr n] + | For (Atom n) (LamExpr n) + | While (Expr n) + | PrimOp (Type n) (PrimOp (Atom n)) + deriving (Show, Generic) + +data Atom (n::S) = + Var (Name n) (Type n) + | Lit LitVal deriving (Show, Generic) + +data Type (n::S) = + BaseType BaseType + | ProdType [Type n] + | SumType [Type n] + | RefType (Type n) + | DepPairTy (DepPairType n) + | TabPi (TabPiType n) + deriving (Show, Generic) + +type TopFunName = Name +type Binder = BinderP Type :: B +data Decl (n::S) (l::S) = Let (NameBinder n l) (Expr n) + deriving (Show, Generic) +type Block = Abs (Nest Decl) Expr + +data TabPiType (n::S) = TabPiType (Atom n) (Abs Binder Type n) -- length, element type + deriving (Show, Generic) + +type DepPairType = Abs Binder Type +type LamExpr = Abs (Nest Binder) Expr :: E +type PiType = Abs (Nest Binder) Type :: E + +-- === type classes === + +instance GenericE Expr where + type RepE Expr = UnitE +instance Pretty (Expr n) +instance SinkableE Expr +instance HoistableE Expr +instance RenameE Expr +instance AlphaEqE Expr +instance AlphaHashableE Expr +instance Store (Expr n) + +instance GenericE Atom where + type RepE Atom = UnitE +instance Pretty (Atom n) +instance SinkableE Atom +instance HoistableE Atom +instance RenameE Atom +instance AlphaEqE Atom +instance AlphaHashableE Atom +instance Store (Atom n) + +instance GenericE Type where + type RepE Type = UnitE +instance Pretty (Type n) +instance SinkableE Type +instance HoistableE Type +instance RenameE Type +instance AlphaEqE Type +instance AlphaHashableE Type +instance Store (Type n) + +instance GenericE TabPiType where + type RepE TabPiType = UnitE +instance Pretty (TabPiType n) +instance SinkableE TabPiType +instance HoistableE TabPiType +instance RenameE TabPiType +instance AlphaEqE TabPiType +instance AlphaHashableE TabPiType +instance Store (TabPiType n) + +instance GenericB Decl where + type RepB Decl = BinderP Expr + fromB (Let b expr) = b :> expr + {-# INLINE fromB #-} + toB (b :> expr) = Let b expr + {-# INLINE toB #-} +instance Pretty (Decl n l) +instance SinkableB Decl +instance HoistableB Decl +instance RenameB Decl +instance AlphaEqB Decl +instance AlphaHashableB Decl +instance ProvesExt Decl +instance BindsNames Decl +instance Store (Decl n l) diff --git a/src/lib/Types/Top.hs b/src/lib/Types/Top.hs index e3e58bf5e..a47fc8452 100644 --- a/src/lib/Types/Top.hs +++ b/src/lib/Types/Top.hs @@ -26,13 +26,13 @@ import Util (FileHash, SnocList (..)) import PPrint import Types.Primitives -import Types.Core +import Types.Complicated +import Types.Simple import Types.Source import Types.Imp type TopBlock = TopLam -- used for nullary lambda -type IsDestLam = Bool -data TopLam (n::S) = TopLam IsDestLam (PiType n) (LamExpr n) +data TopLam (n::S) = TopLam (PiType n) (LamExpr n) deriving (Show, Generic) type STopLam = TopLam type CTopLam = TopLam @@ -59,12 +59,11 @@ newtype TopFunLowerings (n::S) = TopFunLowerings { topFunObjCode :: FunObjCodeName n } -- TODO: add optimized, imp etc. as needed deriving (Show, Generic, SinkableE, HoistableE, RenameE, AlphaEqE, AlphaHashableE, Pretty) -data AtomBinding (n::S) where - LetBound :: DeclBinding n -> AtomBinding n - MiscBound :: Type n -> AtomBinding n - SolverBound :: SolverBinding n -> AtomBinding n - NoinlineFun :: CType n -> CAtom n -> AtomBinding n - FFIFunBound :: CorePiType n -> TopFunName n -> AtomBinding n +data AtomBinding (n::S) = + LetBound (CExpr n) + | MiscBound (Type n) + | SolverBound (SolverBinding n) + | FFIFunBound (CorePiType n) (TopFunName n) deriving instance Show (AtomBinding n) deriving via WrapE AtomBinding n instance Generic (AtomBinding n) @@ -75,14 +74,7 @@ data SolverBinding (n::S) = | DictBound (CType n) deriving (Show, Generic) --- TODO: Use an IntMap -newtype CustomRules (n::S) = - CustomRules { customRulesMap :: M.Map (AtomName n) (AtomRules n) } - deriving (Semigroup, Monoid, Store) -data AtomRules (n::S) = - -- number of implicit args, number of explicit args, linearization function - CustomLinearize Int Int SymbolicZeros (CAtom n) - deriving (Generic) +-- === top-level definitions === -- === envs and modules === @@ -99,7 +91,6 @@ newtype EnvFrag (n::S) (l::S) = EnvFrag (RecSubstFrag Binding n l) data TopEnv (n::S) = TopEnv { envDefs :: RecSubst Binding n - , envCustomRules :: CustomRules n , envCache :: Cache n , envLoadedModules :: LoadedModules n , envLoadedObjects :: LoadedObjects n } @@ -107,7 +98,6 @@ data TopEnv (n::S) = TopEnv data SerializedEnv n = SerializedEnv { serializedEnvDefs :: RecSubst Binding n - , serializedEnvCustomRules :: CustomRules n , serializedEnvCache :: Cache n } deriving (Generic) @@ -124,6 +114,7 @@ data ModuleEnv (n::S) = ModuleEnv , envSynthCandidates :: SynthCandidates n } deriving (Generic) +type ModuleName = Name data Module (n::S) = Module { moduleSourceName :: ModuleSourceName , moduleDirectDeps :: S.Set (ModuleName n) @@ -163,15 +154,12 @@ data TopEnvFrag n l = TopEnvFrag (EnvFrag n l) (ModuleEnv l) (SnocList (TopEnvUp data TopEnvUpdate n = ExtendCache (Cache n) - | AddCustomRule (CAtomName n) (AtomRules n) | UpdateLoadedModules ModuleSourceName (ModuleName n) | UpdateLoadedObjects (FunObjCodeName n) NativeFunction - | FinishDictSpecialization (SpecDictName n) [STopLam n] - | LowerDictSpecialization (SpecDictName n) [STopLam n] | UpdateTopFunEvalStatus (TopFunName n) (TopFunEvalStatus n) | UpdateInstanceDef (InstanceName n) (InstanceDef n) | UpdateTyConDef (TyConName n) (TyConDef n) - | UpdateFieldDef (TyConName n) SourceName (CAtomName n) + | UpdateFieldDef (TyConName n) SourceName (Name n) -- TODO: we could add a lot more structure for querying by dict type, caching, etc. data SynthCandidates n = SynthCandidates @@ -187,7 +175,6 @@ emptyImportStatus = ImportStatus mempty mempty data Cache (n::S) = Cache { specializationCache :: EMap SpecializationSpec TopFunName n - , ixDictCache :: EMap AbsDict SpecDictName n , linearizationCache :: EMap LinearizationSpec (PairE TopFunName TopFunName) n , transpositionCache :: EMap TopFunName TopFunName n -- This is memoizing `parseAndGetDeps :: Text -> [ModuleSourceName]`. But we @@ -228,7 +215,7 @@ dynamicVarLinkMap dyvars = dyvars <&> \(v, ptr) -> (dynamicVarCName v, ptr) type Generalized (e::E) (n::S) = (Abstracted e n, [Atom n]) type Abstracted (e::E) = Abs (Nest Binder) e -type AbsDict = Abstracted CDict +type AbsDict = Abstracted DictCon data SpecializedDictDef n = SpecializedDict @@ -241,7 +228,7 @@ data SpecializedDictDef n = -- TODO: extend with AD-oriented specializations, backend-specific specializations etc. data SpecializationSpec (n::S) = - AppSpecialization (AtomVar n) (Abstracted (ListE CAtom) n) + AppSpecialization (Name n) (Abstracted (ListE CExpr) n) deriving (Show, Generic) type Active = Bool @@ -268,12 +255,6 @@ data Binding (n::S) where -- === ToBinding === -atomBindingToBinding :: AtomBinding n -> Binding n -atomBindingToBinding b = AtomNameBinding b - -bindingToAtomBinding :: Binding n -> AtomBinding n -bindingToAtomBinding (AtomNameBinding b) = b - class (RenameE e, SinkableE e) => ToBinding (e::E) where toBinding :: e n -> Binding n @@ -281,10 +262,7 @@ instance ToBinding Binding where toBinding = id instance ToBinding AtomBinding where - toBinding = atomBindingToBinding - -instance ToBinding DeclBinding where - toBinding = toBinding . LetBound + toBinding = AtomNameBinding instance ToBinding Type where toBinding = toBinding . MiscBound @@ -292,16 +270,10 @@ instance ToBinding Type where instance ToBinding SolverBinding where toBinding = toBinding . SolverBound -instance ToBinding IxType where - toBinding (IxType t _) = toBinding t - instance (ToBinding e1, ToBinding e2) => ToBinding (EitherE e1 e2) where toBinding (LeftE e) = toBinding e toBinding (RightE e) = toBinding e -instance ToBindersAbs TopLam Expr where - toAbs (TopLam _ _ lam) = toAbs lam - -- === GenericE, GenericB === instance GenericE SpecializedDictDef where @@ -326,18 +298,17 @@ instance HasScope Env where instance OutMap Env where emptyOutMap = - Env (TopEnv (RecSubst emptyInFrag) mempty mempty emptyLoadedModules emptyLoadedObjects) + Env (TopEnv (RecSubst emptyInFrag) mempty emptyLoadedModules emptyLoadedObjects) emptyModuleEnv {-# INLINE emptyOutMap #-} instance ExtOutMap Env (RecSubstFrag Binding) where -- TODO: We might want to reorganize this struct to make this -- do less explicit sinking etc. It's a hot operation! - extendOutMap (Env (TopEnv defs rules cache loadedM loadedO) moduleEnv) frag = + extendOutMap (Env (TopEnv defs cache loadedM loadedO) moduleEnv) frag = withExtEvidence frag $ Env (TopEnv (defs `extendRecSubst` frag) - (sink rules) (sink cache) (sink loadedM) (sink loadedO)) @@ -355,29 +326,9 @@ extendEnv env (EnvFrag newEnv) = do Env envTop (ModuleEnv imports sm scs) {-# NOINLINE [1] extendEnv #-} - -instance GenericE AtomRules where - type RepE AtomRules = (LiftE (Int, Int, SymbolicZeros)) `PairE` CAtom - fromE (CustomLinearize ni ne sz a) = LiftE (ni, ne, sz) `PairE` a - toE (LiftE (ni, ne, sz) `PairE` a) = CustomLinearize ni ne sz a -instance SinkableE AtomRules -instance HoistableE AtomRules -instance AlphaEqE AtomRules -instance RenameE AtomRules - -instance GenericE CustomRules where - type RepE CustomRules = ListE (PairE AtomName AtomRules) - fromE (CustomRules m) = ListE $ toPairE <$> M.toList m - toE (ListE l) = CustomRules $ M.fromList $ fromPairE <$> l -instance SinkableE CustomRules -instance HoistableE CustomRules -instance AlphaEqE CustomRules -instance RenameE CustomRules - instance GenericE Cache where type RepE Cache = EMap SpecializationSpec TopFunName - `PairE` EMap AbsDict SpecDictName `PairE` EMap LinearizationSpec (PairE TopFunName TopFunName) `PairE` EMap TopFunName TopFunName `PairE` LiftE (M.Map ModuleSourceName (FileHash, [ModuleSourceName])) @@ -385,13 +336,13 @@ instance GenericE Cache where `PairE` LiftE FileHash `PairE` ListE ModuleName `PairE` ModuleName) - fromE (Cache x y z w parseCache evalCache) = - x `PairE` y `PairE` z `PairE` w `PairE` LiftE parseCache `PairE` + fromE (Cache x y z parseCache evalCache) = + x `PairE` y `PairE` z `PairE` LiftE parseCache `PairE` ListE [LiftE sourceName `PairE` LiftE hashVal `PairE` ListE deps `PairE` result | (sourceName, ((hashVal, deps), result)) <- M.toList evalCache ] {-# INLINE fromE #-} - toE (x `PairE` y `PairE` z `PairE` w `PairE` LiftE parseCache `PairE` ListE evalCache) = - Cache x y z w parseCache + toE (x `PairE` y `PairE` z `PairE` LiftE parseCache `PairE` ListE evalCache) = + Cache x y z parseCache (M.fromList [(sourceName, ((hashVal, deps), result)) | LiftE sourceName `PairE` LiftE hashVal `PairE` ListE deps `PairE` result @@ -405,13 +356,13 @@ instance RenameE Cache instance Store (Cache n) instance Monoid (Cache n) where - mempty = Cache mempty mempty mempty mempty mempty mempty + mempty = Cache mempty mempty mempty mempty mempty mappend = (<>) instance Semigroup (Cache n) where -- right-biased instead of left-biased - Cache x1 x2 x3 x4 x5 x6 <> Cache y1 y2 y3 y4 y5 y6 = - Cache (y1<>x1) (y2<>x2) (y3<>x3) (y4<>x4) (x5<>y5) (x6<>y6) + Cache x1 x2 x3 x4 x5 <> Cache y1 y2 y3 y4 y5 = + Cache (y1<>x1) (y2<>x2) (y3<>x3) (y4<>x4) (x5<>y5) instance GenericE SynthCandidates where @@ -432,33 +383,24 @@ instance RenameE SynthCandidates instance GenericE AtomBinding where type RepE AtomBinding = - EitherE2 (EitherE3 - DeclBinding -- LetBound - Type -- MiscBound - (SolverBinding) -- SolverBound - ) (EitherE2 - ((PairE CType CAtom)) -- NoinlineFun - ((CorePiType `PairE` TopFunName)) -- FFIFunBound - ) + EitherE4 + CExpr -- LetBound + Type -- MiscBound + (SolverBinding) -- SolverBound + (CorePiType `PairE` TopFunName) -- FFIFunBound fromE = \case - LetBound x -> Case0 $ Case0 x - MiscBound x -> Case0 $ Case1 x - SolverBound x -> Case0 $ Case2 $ x - NoinlineFun t x -> Case1 $ Case0 $ PairE t x - FFIFunBound t v -> Case1 $ Case1 $ t `PairE` v + LetBound x -> Case0 x + MiscBound x -> Case1 x + SolverBound x -> Case2 $ x + FFIFunBound t v -> Case3 $ t `PairE` v {-# INLINE fromE #-} toE = \case - Case0 x' -> case x' of - Case0 x -> LetBound x - Case1 x -> MiscBound x - Case2 x -> SolverBound x - _ -> error "impossible" - Case1 x' -> case x' of - Case0 (PairE t x) -> NoinlineFun t x - Case1 (ty `PairE` v) -> FFIFunBound ty v - _ -> error "impossible" + Case0 x -> LetBound x + Case1 x -> MiscBound x + Case2 x -> SolverBound x + Case3 (ty `PairE` v) -> FFIFunBound ty v _ -> error "impossible" {-# INLINE toE #-} @@ -468,6 +410,7 @@ instance HoistableE AtomBinding instance RenameE AtomBinding instance AlphaEqE AtomBinding instance AlphaHashableE AtomBinding +instance Store (AtomBinding n) instance GenericE TopFunDef where type RepE TopFunDef = EitherE3 SpecializationSpec LinearizationSpec LinearizationSpec @@ -490,17 +433,17 @@ instance AlphaEqE TopFunDef instance AlphaHashableE TopFunDef instance GenericE TopLam where - type RepE TopLam = LiftE Bool `PairE` PiType `PairE` LamExpr - fromE (TopLam d x y) = LiftE d `PairE` x `PairE` y + type RepE TopLam = PiType `PairE` LamExpr + fromE (TopLam x y) = x `PairE` y {-# INLINE fromE #-} - toE (LiftE d `PairE` x `PairE` y) = TopLam d x y + toE (x `PairE` y) = TopLam x y {-# INLINE toE #-} - instance SinkableE TopLam instance HoistableE TopLam instance RenameE TopLam instance AlphaEqE TopLam instance AlphaHashableE TopLam +instance Store (TopLam n) instance GenericE TopFun where type RepE TopFun = EitherE @@ -523,7 +466,7 @@ instance AlphaHashableE TopFun instance GenericE SpecializationSpec where type RepE SpecializationSpec = - PairE AtomVar (Abs (Nest Binder) (ListE CAtom)) + PairE Name (Abs (Nest Binder) (ListE CExpr)) fromE (AppSpecialization fname (Abs bs args)) = PairE fname (Abs bs args) {-# INLINE fromE #-} toE (PairE fname (Abs bs args)) = AppSpecialization fname (Abs bs args) @@ -552,10 +495,7 @@ instance AlphaEqE LinearizationSpec instance AlphaHashableE LinearizationSpec instance GenericE SolverBinding where - type RepE SolverBinding = EitherE3 - CType - CType - CType + type RepE SolverBinding = EitherE3 CType CType CType fromE = \case InfVarBound ty -> Case0 ty SkolemBound ty -> Case1 ty @@ -568,12 +508,12 @@ instance GenericE SolverBinding where Case2 ty -> DictBound ty _ -> error "impossible" {-# INLINE toE #-} - instance SinkableE SolverBinding instance HoistableE SolverBinding instance RenameE SolverBinding instance AlphaEqE SolverBinding instance AlphaHashableE SolverBinding +instance Store (SolverBinding n) instance GenericE Binding where type RepE Binding = @@ -628,6 +568,7 @@ instance GenericE Binding where instance SinkableE Binding instance HoistableE Binding instance RenameE Binding +instance Store (Binding n) instance Semigroup (SynthCandidates n) where SynthCandidates xs ys <> SynthCandidates xs' ys' = @@ -649,45 +590,36 @@ instance RenameB EnvFrag instance GenericE TopEnvUpdate where type RepE TopEnvUpdate = EitherE2 ( - EitherE4 + EitherE3 {- ExtendCache -} Cache - {- AddCustomRule -} (CAtomName `PairE` AtomRules) {- UpdateLoadedModules -} (LiftE ModuleSourceName `PairE` ModuleName) {- UpdateLoadedObjects -} (FunObjCodeName `PairE` LiftE NativeFunction) - ) ( EitherE6 - {- FinishDictSpecialization -} (SpecDictName `PairE` ListE STopLam) - {- LowerDictSpecialization -} (SpecDictName `PairE` ListE STopLam) + ) ( EitherE4 {- UpdateTopFunEvalStatus -} (TopFunName `PairE` ComposeE EvalStatus TopFunLowerings) {- UpdateInstanceDef -} (InstanceName `PairE` InstanceDef) {- UpdateTyConDef -} (TyConName `PairE` TyConDef) - {- UpdateFieldDef -} (TyConName `PairE` LiftE SourceName `PairE` CAtomName) + {- UpdateFieldDef -} (TyConName `PairE` LiftE SourceName `PairE` Name) ) fromE = \case ExtendCache x -> Case0 $ Case0 x - AddCustomRule x y -> Case0 $ Case1 (x `PairE` y) - UpdateLoadedModules x y -> Case0 $ Case2 (LiftE x `PairE` y) - UpdateLoadedObjects x y -> Case0 $ Case3 (x `PairE` LiftE y) - FinishDictSpecialization x y -> Case1 $ Case0 (x `PairE` ListE y) - LowerDictSpecialization x y -> Case1 $ Case1 (x `PairE` ListE y) - UpdateTopFunEvalStatus x y -> Case1 $ Case2 (x `PairE` ComposeE y) - UpdateInstanceDef x y -> Case1 $ Case3 (x `PairE` y) - UpdateTyConDef x y -> Case1 $ Case4 (x `PairE` y) - UpdateFieldDef x y z -> Case1 $ Case5 (x `PairE` LiftE y `PairE` z) + UpdateLoadedModules x y -> Case0 $ Case1 (LiftE x `PairE` y) + UpdateLoadedObjects x y -> Case0 $ Case2 (x `PairE` LiftE y) + UpdateTopFunEvalStatus x y -> Case1 $ Case0 (x `PairE` ComposeE y) + UpdateInstanceDef x y -> Case1 $ Case1 (x `PairE` y) + UpdateTyConDef x y -> Case1 $ Case2 (x `PairE` y) + UpdateFieldDef x y z -> Case1 $ Case3 (x `PairE` LiftE y `PairE` z) toE = \case Case0 e -> case e of Case0 x -> ExtendCache x - Case1 (x `PairE` y) -> AddCustomRule x y - Case2 (LiftE x `PairE` y) -> UpdateLoadedModules x y - Case3 (x `PairE` LiftE y) -> UpdateLoadedObjects x y + Case1 (LiftE x `PairE` y) -> UpdateLoadedModules x y + Case2 (x `PairE` LiftE y) -> UpdateLoadedObjects x y _ -> error "impossible" Case1 e -> case e of - Case0 (x `PairE` ListE y) -> FinishDictSpecialization x y - Case1 (x `PairE` ListE y) -> LowerDictSpecialization x y - Case2 (x `PairE` ComposeE y) -> UpdateTopFunEvalStatus x y - Case3 (x `PairE` y) -> UpdateInstanceDef x y - Case4 (x `PairE` y) -> UpdateTyConDef x y - Case5 (x `PairE` LiftE y `PairE` z) -> UpdateFieldDef x y z + Case0 (x `PairE` ComposeE y) -> UpdateTopFunEvalStatus x y + Case1 (x `PairE` y) -> UpdateInstanceDef x y + Case2 (x `PairE` y) -> UpdateTyConDef x y + Case3 (x `PairE` LiftE y `PairE` z) -> UpdateFieldDef x y z _ -> error "impossible" _ -> error "impossible" @@ -726,11 +658,10 @@ instance ExtOutMap Env TopEnvFrag where let newerTopEnv = foldl applyUpdate newTopEnv otherUpdates Env newerTopEnv newModuleEnv where - Env (TopEnv defs rules cache loadedM loadedO) mEnv = env + Env (TopEnv defs cache loadedM loadedO) mEnv = env newTopEnv = withExtEvidence frag $ TopEnv - (defs `extendRecSubst` frag) - (sink rules) (sink cache) (sink loadedM) (sink loadedO) + (defs `extendRecSubst` frag) (sink cache) (sink loadedM) (sink loadedO) newModuleEnv = ModuleEnv @@ -750,20 +681,8 @@ instance ExtOutMap Env TopEnvFrag where applyUpdate :: TopEnv n -> TopEnvUpdate n -> TopEnv n applyUpdate e = \case ExtendCache cache -> e { envCache = envCache e <> cache} - AddCustomRule x y -> e { envCustomRules = envCustomRules e <> CustomRules (M.singleton x y)} UpdateLoadedModules x y -> e { envLoadedModules = envLoadedModules e <> LoadedModules (M.singleton x y)} UpdateLoadedObjects x y -> e { envLoadedObjects = envLoadedObjects e <> LoadedObjects (M.singleton x y)} - FinishDictSpecialization dName methods -> do - let SpecializedDictBinding (SpecializedDict dAbs oldMethods) = lookupEnvPure e dName - case oldMethods of - Nothing -> do - let newBinding = SpecializedDictBinding $ SpecializedDict dAbs (Just methods) - updateEnv dName newBinding e - Just _ -> error "shouldn't be adding methods if we already have them" - LowerDictSpecialization dName methods -> do - let SpecializedDictBinding (SpecializedDict dAbs _) = lookupEnvPure e dName - let newBinding = SpecializedDictBinding $ SpecializedDict dAbs (Just methods) - updateEnv dName newBinding e UpdateTopFunEvalStatus f s -> do case lookupEnvPure e f of TopFunBinding (DexTopFun def lam _) -> @@ -895,20 +814,15 @@ instance Semigroup (LoadedObjects n) where instance Monoid (LoadedObjects n) where mempty = LoadedObjects mempty - -- === instance === prettyRecord :: [(String, Doc ann)] -> Doc ann prettyRecord xs = foldMap (\(name, val) -> pretty name <> indented val) xs instance Pretty (TopEnv n) where - pretty (TopEnv defs rules cache _ _) = - prettyRecord [ ("Defs" , pretty defs) - , ("Rules" , pretty rules) - , ("Cache" , pretty cache) ] - -instance Pretty (CustomRules n) where - pretty _ = "TODO: Rule printing" + pretty (TopEnv defs cache _ _) = + prettyRecord [ ("Defs" , pretty defs) + , ("Cache", pretty cache) ] instance Pretty (ImportStatus n) where pretty imports = pretty $ S.toList $ directImports imports @@ -963,7 +877,7 @@ instance Pretty (EnvFrag n l) where pretty (EnvFrag bindings) = pretty bindings instance Pretty (Cache n) where - pretty (Cache _ _ _ _ _ _) = "" -- TODO + pretty (Cache _ _ _ _ _) = "" -- TODO instance Pretty (SynthCandidates n) where pretty scs = "instance dicts:" <+> pretty (M.toList $ instanceDicts scs) @@ -987,7 +901,7 @@ instance Pretty (TopFun n) where FFITopFun f _ -> pretty f instance Pretty (TopLam n) where - pretty (TopLam _ _ lam) = pretty lam + pretty (TopLam _ lam) = pretty lam instance Pretty (AtomBinding n) where pretty binding = case binding of @@ -995,7 +909,6 @@ instance Pretty (AtomBinding n) where MiscBound t -> pretty t SolverBound b -> pretty b FFIFunBound s _ -> pretty s - NoinlineFun ty _ -> "Top function with type: " <+> pretty ty instance Pretty (SpecializationSpec n) where pretty (AppSpecialization f (Abs bs (ListE args))) = @@ -1003,9 +916,6 @@ instance Pretty (SpecializationSpec n) where instance Hashable a => Hashable (EvalStatus a) -instance Store (SolverBinding n) -instance Store (AtomBinding n) -instance Store (TopLam n) instance Store (SynthCandidates n) instance Store (Module n) instance Store (ImportStatus n) @@ -1013,10 +923,8 @@ instance Store (TopFunLowerings n) instance Store a => Store (EvalStatus a) instance Store (TopFun n) instance Store (TopFunDef n) -instance Store (Binding n) instance Store (ModuleEnv n) instance Store (SerializedEnv n) -instance Store (AtomRules n) instance Store (LinearizationSpec n) instance Store (SpecializedDictDef n) instance Store (SpecializationSpec n)