From 68841c9a570f739e7dafca03b46548fd89096690 Mon Sep 17 00:00:00 2001 From: Dougal Date: Thu, 16 May 2024 10:59:27 -0400 Subject: [PATCH] Removing colors and IRRep (WIP) --- dex.cabal | 1 - src/lib/AbstractSyntax.hs | 2 +- src/lib/ConcreteSyntax.hs | 1 - src/lib/Core.hs | 48 +- src/lib/IRVariants.hs | 95 --- src/lib/MTL1.hs | 2 +- src/lib/Name.hs | 717 ++++++---------------- src/lib/QueryType.hs | 1 - src/lib/QueryTypePure.hs | 1 - src/lib/SourceRename.hs | 3 +- src/lib/Types/Core.hs | 1122 +++++++++++++++++------------------ src/lib/Types/Imp.hs | 47 +- src/lib/Types/Primitives.hs | 70 ++- src/lib/Types/Source.hs | 141 ++--- src/lib/Types/Top.hs | 266 ++++----- 15 files changed, 995 insertions(+), 1522 deletions(-) delete mode 100644 src/lib/IRVariants.hs diff --git a/dex.cabal b/dex.cabal index 0f688fce5..e599f6938 100644 --- a/dex.cabal +++ b/dex.cabal @@ -55,7 +55,6 @@ library , IncState , Inference -- , Inline - , IRVariants -- , JAX.Concrete -- , JAX.Rename -- , JAX.ToSimp diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs index f726357e2..5e40095ba 100644 --- a/src/lib/AbstractSyntax.hs +++ b/src/lib/AbstractSyntax.hs @@ -255,7 +255,7 @@ patOptAnn (WithSrcs _ _ (CBin Colon lhs typeAnn)) = (,) <$> pat lhs <*> (Just <$ patOptAnn (WithSrcs _ _ (CParens [g])) = patOptAnn g patOptAnn g = (,Nothing) <$> pat g -uBinder :: GroupW -> SyntaxM (UBinder c VoidS VoidS) +uBinder :: GroupW -> SyntaxM (UBinder VoidS VoidS) uBinder (WithSrcs sid _ b) = case b of CLeaf (CIdentifier name) -> return $ fromSourceNameW $ WithSrc sid name CLeaf CHole -> return $ WithSrcB sid UIgnore diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs index 4f4ad3b25..dc6b38677 100644 --- a/src/lib/ConcreteSyntax.hs +++ b/src/lib/ConcreteSyntax.hs @@ -27,7 +27,6 @@ import Text.Megaparsec.Char hiding (space, eol) import Err import Lexing -import Types.Core import Types.Source import Types.Primitives import Util diff --git a/src/lib/Core.hs b/src/lib/Core.hs index cc690cefe..d1ed372b2 100644 --- a/src/lib/Core.hs +++ b/src/lib/Core.hs @@ -34,7 +34,6 @@ import qualified Data.Map.Strict as M import Name import Err -import IRVariants import Types.Core import Types.Top @@ -189,20 +188,20 @@ class BindsNames b => BindsEnv (b::B) where => Distinct l => b n l -> EnvFrag n l toEnvFrag b = toEnvFrag $ fromB b -instance (Color c, SinkableE ann, ToBinding ann c) => BindsEnv (BinderP c ann) where +instance (SinkableE ann, ToBinding ann) => BindsEnv (BinderP ann) where toEnvFrag (b:>ann) = EnvFrag (RecSubstFrag (b @> toBinding ann')) where ann' = withExtEvidence b $ sink ann -instance (IRRep r, SinkableE ann, ToBinding ann (AtomNameC r)) => BindsEnv (NonDepNest r ann) where +instance (SinkableE ann, ToBinding ann) => BindsEnv (NonDepNest ann) where toEnvFrag (NonDepNest topBs topAnns) = toEnvFrag $ zipNest topBs topAnns where - zipNest :: Distinct l => Nest (AtomNameBinder r) n l -> [ann n] -> Nest (BinderP (AtomNameC r) ann) n l + zipNest :: Distinct l => Nest AtomNameBinder n l -> [ann n] -> Nest (BinderP ann) n l zipNest Empty [] = Empty zipNest (Nest b bs) (a:anns) = withExtEvidence b $ withSubscopeDistinct bs $ Nest (b:>a) $ zipNest bs $ sinkList anns zipNest _ _ = error "Mismatched lengths in NonDepNest" -instance IRRep r => BindsEnv (Decl r) where +instance BindsEnv Decl where toEnvFrag (Let b binding) = toEnvFrag $ b :> binding {-# INLINE toEnvFrag #-} @@ -265,12 +264,12 @@ instance (BindsEnv b1, BindsEnv b2) instance BindsEnv UnitB where toEnvFrag UnitB = emptyOutFrag -instance IRRep r => ExtOutMap Env (Nest (Decl r)) where +instance ExtOutMap Env (Nest Decl) where extendOutMap bindings emissions = bindings `extendOutMap` toEnvFrag emissions {-# INLINE extendOutMap #-} -instance IRRep r => ExtOutMap Env (RNest (Decl r)) where +instance ExtOutMap Env (RNest Decl) where extendOutMap bindings emissions = bindings `extendOutMap` toEnvFrag emissions {-# INLINE extendOutMap #-} @@ -281,15 +280,15 @@ instance ExtOutMap Env UnitB where -- === Monadic helpers === -lookupEnv :: (Color c, EnvReader m) => Name c o -> m o (Binding c o) +lookupEnv :: EnvReader m => Name o -> m o (Binding o) lookupEnv v = withEnv $ flip lookupEnvPure v . topEnv {-# INLINE lookupEnv #-} -lookupAtomName :: (IRRep r, EnvReader m) => AtomName r n -> m n (AtomBinding r n) +lookupAtomName :: EnvReader m => AtomName n -> m n (AtomBinding n) lookupAtomName name = bindingToAtomBinding <$> lookupEnv name {-# INLINE lookupAtomName #-} -lookupCustomRules :: EnvReader m => AtomName CoreIR n -> m n (Maybe (AtomRules n)) +lookupCustomRules :: EnvReader m => AtomName n -> m n (Maybe (AtomRules n)) lookupCustomRules name = liftM fromMaybeE $ withEnv $ toMaybeE . M.lookup name . customRulesMap . envCustomRules . topEnv {-# INLINE lookupCustomRules #-} @@ -317,7 +316,7 @@ lookupTyCon name = lookupEnv name >>= \case TyConBinding Nothing _ -> error "TyCon not yet defined" {-# INLINE lookupTyCon #-} -lookupDataCon :: EnvReader m => Name DataConNameC n -> m n (TyConName n, Int) +lookupDataCon :: EnvReader m => DataConName n -> m n (TyConName n, Int) lookupDataCon v = do ~(DataConBinding defName idx) <- lookupEnv v return (defName, idx) @@ -356,9 +355,9 @@ refreshBinders b cont = refreshAbs (Abs b $ idSubstFrag b) cont {-# INLINE refreshBinders #-} withFreshBinder - :: (Color c, EnvExtender m, ToBinding binding c) + :: (EnvExtender m, ToBinding binding) => NameHint -> binding n - -> (forall l. DExt n l => BinderP c binding n l -> m l a) + -> (forall l. DExt n l => BinderP binding n l -> m l a) -> m n a withFreshBinder hint binding cont = do Abs b v <- freshNameM hint @@ -366,9 +365,9 @@ withFreshBinder hint binding cont = do {-# INLINE withFreshBinder #-} withFreshBinders - :: (Color c, EnvExtender m, ToBinding binding c) + :: (EnvExtender m, ToBinding binding) => [binding n] - -> (forall l. DExt n l => Nest (BinderP c binding) n l -> [Name c l] -> m l a) + -> (forall l. DExt n l => Nest (BinderP binding) n l -> [Name l] -> m l a) -> m n a withFreshBinders [] cont = do Distinct <- getDistinct @@ -391,14 +390,14 @@ withFreshBinders (binding:rest) cont = do -- present, in which case exactly maxDepth binders are packed into the nary -- structure. Excess binders, if any, are still left in the unary structures. -liftLamExpr :: (IRRep r, EnvReader m) - => TopLam r n - -> (forall l m2. EnvReader m2 => Expr r l -> m2 l (Expr r l)) - -> m n (TopLam r n) +liftLamExpr :: EnvReader m + => TopLam n + -> (forall l m2. EnvReader m2 => Expr l -> m2 l (Expr l)) + -> m n (TopLam n) liftLamExpr (TopLam d ty (LamExpr bs body)) f = liftM (TopLam d ty) $ liftEnvReaderM $ refreshAbs (Abs bs body) \bs' body' -> LamExpr bs' <$> f body' -fromNaryForExpr :: IRRep r => Int -> Expr r n -> Maybe (Int, LamExpr r n) +fromNaryForExpr :: Int -> Expr n -> Maybe (Int, LamExpr n) fromNaryForExpr maxDepth | maxDepth <= 0 = error "expected non-negative number of args" fromNaryForExpr maxDepth = \case Hof (TypedHof _ (For _ _ (UnaryLamExpr b body))) -> @@ -419,16 +418,13 @@ bundleFold emptyVal pair els = case els of h:t -> (pair h tb, td + 1) where (tb, td) = bundleFold emptyVal pair t -mkBundleTy :: [Type r n] -> (Type r n, BundleDesc) +mkBundleTy :: [Type n] -> (Type n, BundleDesc) mkBundleTy = bundleFold UnitTy (\x y -> TyCon (ProdType [x, y])) -mkBundle :: [Atom r n] -> (Atom r n, BundleDesc) +mkBundle :: [Atom n] -> (Atom n, BundleDesc) mkBundle = bundleFold UnitVal (\x y -> Con (ProdCon [x, y])) -freeAtomVarsList :: forall r e n. (IRRep r, HoistableE e) => e n -> [Name (AtomNameC r) n] -freeAtomVarsList = freeVarsList - -freshNameM :: (Color c, EnvReader m) => NameHint -> m n (Abs (NameBinder c) (Name c) n) +freshNameM :: (EnvReader m) => NameHint -> m n (Abs NameBinder Name n) freshNameM hint = do scope <- toScope <$> unsafeGetEnv Distinct <- getDistinct diff --git a/src/lib/IRVariants.hs b/src/lib/IRVariants.hs deleted file mode 100644 index 2ca28c1b5..000000000 --- a/src/lib/IRVariants.hs +++ /dev/null @@ -1,95 +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 AllowAmbiguousTypes #-} - -module IRVariants - ( IR (..), IRPredicate (..), Sat, Sat' - , CoreToSimpIR, InferenceIR, IRRep (..), IRProxy (..), interpretIR - , IRsEqual (..), eqIRRep, WhenIR (..)) where - -import GHC.Generics (Generic (..)) -import Data.Store -import Data.Hashable -import Data.Store.Internal -import Data.Kind - -import qualified Unsafe.Coerce as TrulyUnsafe - -data IR = - CoreIR -- used after inference and before simplification - | SimpIR -- used after simplification - deriving (Eq, Ord, Generic, Show, Enum) -instance Store IR - -type CoreToSimpIR = CoreIR -- used during the Core-to-Simp translation -data IRFeature = - DAMOps - | CoreOps - | SimpOps - --- TODO: make this a hard distinctions -type InferenceIR = CoreIR -- used during type inference only - -data IRPredicate = - Is IR - -- TODO: find a way to make this safe and derive it automatically. For now, we - -- assert it manually for the valid cases we know about. - | IsSubsetOf IR - | HasFeature IRFeature - -type Sat (r::IR) (p::IRPredicate) = (Sat' r p ~ True) :: Constraint -type family Sat' (r::IR) (p::IRPredicate) where - Sat' r (Is r) = True - -- subsets - Sat' SimpIR (IsSubsetOf CoreIR) = True - -- DAMOps - Sat' SimpIR (HasFeature DAMOps) = True - -- DAMOps - Sat' SimpIR (HasFeature SimpOps) = True - -- CoreOps - Sat' CoreIR (HasFeature CoreOps) = True - -- otherwise - Sat' _ _ = False - -class IRRep (r::IR) where - getIRRep :: IR - -data IRProxy (r::IR) = IRProxy - -interpretIR :: IR -> (forall r. IRRep r => IRProxy r -> a) -> a -interpretIR ir cont = case ir of - CoreIR -> cont $ IRProxy @CoreIR - SimpIR -> cont $ IRProxy @SimpIR - -instance IRRep CoreIR where getIRRep = CoreIR -instance IRRep SimpIR where getIRRep = SimpIR - -data IRsEqual (r1::IR) (r2::IR) where - IRsEqual :: IRsEqual r r - -eqIRRep :: forall r1 r2. (IRRep r1, IRRep r2) => Maybe (IRsEqual r1 r2) -eqIRRep = if r1Rep == r2Rep - then Just (TrulyUnsafe.unsafeCoerce (IRsEqual :: IRsEqual r1 r1) :: IRsEqual r1 r2) - else Nothing - where r1Rep = getIRRep @r1; r2Rep = getIRRep @r2 -{-# INLINE eqIRRep #-} - -data WhenIR (r::IR) (r'::IR) (a::Type) where - WhenIR :: a -> WhenIR r r a - -instance (IRRep r, IRRep r', Store e) => Store (WhenIR r r' e) where - size = VarSize \(WhenIR e) -> getSize e - peek = case eqIRRep @r @r' of - Just IRsEqual -> WhenIR <$> peek - Nothing -> error "impossible" - poke (WhenIR e) = poke e - -instance Hashable a => Hashable (WhenIR r r' a) where - hashWithSalt salt (WhenIR a) = hashWithSalt salt a - -deriving instance Show a => Show (WhenIR r r' a) -deriving instance Eq a => Eq (WhenIR r r' a) diff --git a/src/lib/MTL1.hs b/src/lib/MTL1.hs index 47fe8b8c1..44fb99206 100644 --- a/src/lib/MTL1.hs +++ b/src/lib/MTL1.hs @@ -215,7 +215,7 @@ instance HoistableState UnitE where hoistState _ _ UnitE = UnitE {-# INLINE hoistState #-} -instance Show a => HoistableState (NameMap c a) where +instance Show a => HoistableState (NameMap a) where hoistState _ b m = hoistNameMap b m {-# INLINE hoistState #-} diff --git a/src/lib/Name.hs b/src/lib/Name.hs index 9c144eb37..101c3fef0 100644 --- a/src/lib/Name.hs +++ b/src/lib/Name.hs @@ -46,12 +46,11 @@ import qualified RawName as R import Util ( zipErr, onFst, onSnd, transitiveClosure, SnocList (..), unsnoc ) import PPrint import Err -import IRVariants -- === category-like classes for envs, scopes etc === data Subst v i o where - Subst :: (forall c. Color c => Name c hidden -> v c o) + Subst :: (Name hidden -> v o) -> SubstFrag v hidden i o -> Subst v i o -- This is a compact, but unsafe representation of a substitution @@ -64,7 +63,7 @@ tryApplyIdentitySubst s e = case s of Subst _ _ -> Nothing UnsafeMakeIdentitySubst -> Just $ unsafeCoerceE e -newSubst :: (forall c. Color c => Name c i -> v c o) -> Subst v i o +newSubst :: (Name i -> v o) -> Subst v i o newSubst f = Subst f emptyInFrag envFromFrag :: SubstFrag v VoidS i o -> Subst v i o @@ -78,7 +77,7 @@ idSubstFrag b = scopeFragToSubstFrag (\v -> fromName $ sinkR v) (toScopeFrag b) infixl 9 ! -(!) :: Color c => Subst v i o -> Name c i -> v c o +(!) :: Subst v i o -> Name i -> v o (!) (Subst f env) name = case lookupSubstFragProjected env name of Left name' -> f name' @@ -154,30 +153,29 @@ instance ExtOutMap Scope ScopeFrag where -- outvar version of SubstFrag/Subst, where the query name space and the result name -- space are the same (thus recursive) -newtype RecSubst (v::V) o = RecSubst { fromRecSubst :: SubstFrag v VoidS o o } deriving Generic -newtype RecSubstFrag (v::V) o o' = RecSubstFrag { fromRecSubstFrag :: SubstFrag v o o' o' } deriving Generic +newtype RecSubst (v::E) o = RecSubst { fromRecSubst :: SubstFrag v VoidS o o } deriving Generic +newtype RecSubstFrag (v::E) o o' = RecSubstFrag { fromRecSubstFrag :: SubstFrag v o o' o' } deriving Generic -instance SinkableV v => OutFrag (RecSubstFrag v) where +instance SinkableE v => OutFrag (RecSubstFrag v) where emptyOutFrag = RecSubstFrag $ emptyInFrag {-# INLINE emptyOutFrag #-} catOutFrags = catRecSubstFrags {-# INLINE catOutFrags #-} -catRecSubstFrags :: (Distinct n3, SinkableV v) - => RecSubstFrag v n1 n2 -> RecSubstFrag v n2 n3 -> RecSubstFrag v n1 n3 +catRecSubstFrags :: (Distinct n3, SinkableE v) + => RecSubstFrag v n1 n2 -> RecSubstFrag v n2 n3 -> RecSubstFrag v n1 n3 catRecSubstFrags (RecSubstFrag frag1) (RecSubstFrag frag2) = RecSubstFrag $ withExtEvidence (toExtEvidence (RecSubstFrag frag2)) $ sink frag1 `catInFrags` frag2 -extendRecSubst :: SinkableV v => Distinct l => RecSubst v n -> RecSubstFrag v n l - -> RecSubst v l +extendRecSubst :: SinkableE v => Distinct l => RecSubst v n -> RecSubstFrag v n l -> RecSubst v l extendRecSubst (RecSubst env) (RecSubstFrag frag) = RecSubst $ withExtEvidence (toExtEvidence (RecSubstFrag frag)) $ sink env <.> frag -deriving instance (forall c. Show (v c o')) => Show (RecSubstFrag v o o') +deriving instance Show (v o') => Show (RecSubstFrag v o o') -lookupTerminalSubstFrag :: Color c => SubstFrag v VoidS i o -> Name c i -> v c o +lookupTerminalSubstFrag :: SubstFrag v VoidS i o -> Name i -> v o lookupTerminalSubstFrag frag name = case lookupSubstFragProjected frag name of Left name' -> absurdNameFunction name' @@ -195,10 +193,9 @@ instance (SinkableB b, BindsNames b) => OutFrag (RNest b) where catOutFrags = (>>>) {-# INLINE catOutFrags #-} -updateSubstFrag :: Color c => Name c i -> v c o -> SubstFrag v VoidS i o - -> SubstFrag v VoidS i o +updateSubstFrag :: Name i -> v o -> SubstFrag v VoidS i o -> SubstFrag v VoidS i o updateSubstFrag (UnsafeMakeName v) rhs (UnsafeMakeSubst m) = - UnsafeMakeSubst $ R.adjust (\(SubstItem d c _) -> SubstItem d c (unsafeCoerceVC rhs)) v m + UnsafeMakeSubst $ R.adjust (\(SubstItem d _) -> SubstItem d (unsafeCoerceE rhs)) v m -- === renaming === @@ -226,18 +223,13 @@ class SinkableB b => RenameB (b::B) where -> a renameB env b cont = renameB env (fromB b) \env' b' -> cont env' $ toB b' -class (SinkableV v , forall c. Color c => RenameE (v c)) => RenameV (v::V) - - type HasNamesE e = (RenameE e, SinkableE e, HoistableE e) type HasNamesB = RenameB -instance RenameV Name - -instance Color c => RenameE (Name c) where +instance RenameE Name where renameE (_, env) name = env ! name -instance Color c => RenameB (NameBinder c) where +instance RenameB NameBinder where renameB (scope, env) b cont = do withFresh (getNameHint b) scope \b' -> do let scope' = scope `extendOutMap` toScopeFrag b' @@ -289,8 +281,8 @@ class ScopeReader m => ScopeExtender (m::MonadKind1) where -- === extending envs with name-only substitutions === -class FromName (v::V) where - fromName :: Name c n -> v c n +class FromName (v::E) where + fromName :: Name n -> v n instance FromName Name where fromName = id @@ -342,15 +334,15 @@ popNest bs = case toRNest bs of RNest bs' b -> Just $ PairB (unRNest bs') b REmpty -> Nothing -data BinderP (c::C) (ann::E) (n::S) (l::S) = - (:>) (NameBinder c n l) (ann n) +data BinderP (ann::E) (n::S) (l::S) = + (:>) (NameBinder n l) (ann n) deriving (Show, Generic) type EmptyAbs b = Abs b UnitE :: E pattern EmptyAbs :: b n l -> EmptyAbs b n pattern EmptyAbs bs = Abs bs UnitE -type NaryAbs (c::C) = Abs (Nest (NameBinder c)) :: E -> E +type NaryAbs = Abs (Nest NameBinder) :: E -> E -- Proof object that a given scope is void data IsVoidS n where @@ -404,24 +396,24 @@ sinkM e = do {-# INLINE sinkM #-} toConstAbs :: (SinkableE e, ScopeReader m) - => e n -> m n (Abs (NameBinder c) e n) + => e n -> m n (Abs NameBinder e n) toConstAbs body = do WithScope scope body' <- addScope body withFresh noHint scope \b -> do sinkM $ Abs b $ sink body' toConstAbsPure :: (HoistableE e, SinkableE e) - => e n -> (Abs (NameBinder c) e n) + => e n -> (Abs NameBinder e n) toConstAbsPure e = Abs (UnsafeMakeBinder n) (unsafeCoerceE e) where n = freshRawName noHint $ fromNameSet $ freeVarsE e toConstBinderNest - :: forall n ann e c - . (HoistableE ann, HoistableE e, SinkableE e, SinkableE ann, Color c) - => [ann n] -> e n -> Abs (Nest (BinderP c ann)) e n + :: forall n ann e + . (HoistableE ann, HoistableE e, SinkableE e, SinkableE ann) + => [ann n] -> e n -> Abs (Nest (BinderP ann)) e n toConstBinderNest anns body = withFabricatedDistinct @n $ runScopeReaderM scope $ go anns where - go :: forall l. DExt n l => [ann l] -> ScopeReaderM l (Abs (Nest (BinderP c ann)) e l) + go :: forall l. DExt n l => [ann l] -> ScopeReaderM l (Abs (Nest (BinderP ann)) e l) go = \case [] -> Abs Empty <$> sinkM body ann:rest -> withFreshM noHint \b -> do @@ -435,15 +427,12 @@ type PrettyE e = (forall (n::S) . Pretty (e n )) :: Constraint type PrettyB b = (forall (n::S) (l::S). Pretty (b n l)) :: Constraint type ShowE e = (forall (n::S) . Show (e n )) :: Constraint -type ShowV v = (forall (c::C) (n::S). Show (v c n)) :: Constraint type ShowB b = (forall (n::S) (l::S). Show (b n l)) :: Constraint type EqE e = (forall (n::S) . Eq (e n )) :: Constraint -type EqV v = (forall (c::C) (n::S). Eq (v c n)) :: Constraint type EqB b = (forall (n::S) (l::S). Eq (b n l)) :: Constraint -type OrdE e = (forall (n::S) . Ord (e n )) :: Constraint -type OrdV v = (forall (c::C) (n::S). Ord (v c n)) :: Constraint +type OrdE e = (forall (n::S). Ord (e n)) :: Constraint type OrdB b = (forall (n::S) (l::S). Ord (b n l)) :: Constraint type PrettyPrecE e = (forall (n::S) . PrettyPrec (e n )) :: Constraint @@ -509,30 +498,6 @@ newtype ComposeE (f :: * -> *) (e::E) (n::S) = ComposeE { fromComposeE :: (f (e n)) } deriving (Show, Eq, Generic) -data WhenE (p::Bool) (e::E) (n::S) where - WhenE :: e n -> WhenE True e n - -data WhenIRE (r::IR) (r'::IR) (e::E) (n::S) where - WhenIRE :: e n -> WhenIRE r r e n - -deriving instance ShowE e => Show (WhenIRE r r' e n) - -data WhenC (c::C) (c'::C) (e::E) (n::S) where - WhenC :: e n -> WhenC c c e n - -data WhenAtomName (c::C) (e::IR->E) (n::S) where - WhenAtomName :: e r n -> WhenAtomName (AtomNameC r) e n - -type WhenCore = WhenIRE CoreIR -type WhenSimp = WhenIRE SimpIR - -newtype WrapWithTrue (p::Bool) r = WrapWithTrue { fromWrapWithTrue :: (p ~ True) => r } - -withFabricatedTruth :: forall p a. (p ~ True => a) -> a -withFabricatedTruth cont = fromWrapWithTrue - (TrulyUnsafe.unsafeCoerce (WrapWithTrue cont :: WrapWithTrue p a - ) :: WrapWithTrue True a) - data UnitB (n::S) (l::S) where UnitB :: UnitB n n deriving instance Show (UnitB n l) @@ -570,13 +535,6 @@ forgetEitherB (LeftB b) = b forgetEitherB (RightB b) = b {-# INLINE forgetEitherB #-} --- The constant function of kind `V` -newtype ConstE (const::E) (ignored::C) (n::S) = ConstE (const n) - deriving (Show, Eq, Generic) -type UnitV = ConstE UnitE -pattern UnitV :: UnitV c n -pattern UnitV = ConstE UnitE - type MaybeE e = EitherE e UnitE fromMaybeE :: MaybeE e n -> Maybe (e n) @@ -632,53 +590,52 @@ instance (GenericB b, Generic (RepB b n l)) => Generic (WrapB b n l) where -- -- === various convenience utilities === infixr 7 @> -class BindsNames b => BindsAtMostOneName (b::B) (c::C) | b -> c where - (@>) :: b i i' -> v c o -> SubstFrag v i i' o - -class BindsAtMostOneName (b::B) (c::C) - => BindsOneName (b::B) (c::C) | b -> c where - binderName :: b i i' -> Name c i' - asNameBinder :: b i i' -> NameBinder c i i' - default asNameBinder :: b i i' -> NameBinder c i i' +class BindsNames b => BindsAtMostOneName (b::B) where + (@>) :: b i i' -> v o -> SubstFrag v i i' o + +class BindsAtMostOneName (b::B) => BindsOneName (b::B) where + binderName :: b i i' -> Name i' + asNameBinder :: b i i' -> NameBinder i i' + default asNameBinder :: b i i' -> NameBinder i i' asNameBinder b = UnsafeMakeBinder n where UnsafeMakeName n = binderName b -instance Color c => ProvesExt (NameBinder c) where +instance ProvesExt NameBinder where -instance Color c => BindsAtMostOneName (NameBinder c) c where +instance BindsAtMostOneName NameBinder where b @> x = singletonSubst b x {-# INLINE (@>) #-} -instance Color c => BindsOneName (NameBinder c) c where +instance BindsOneName NameBinder where binderName (UnsafeMakeBinder v) = UnsafeMakeName v {-# INLINE binderName #-} -instance Color c => BindsAtMostOneName (BinderP c ann) c where +instance BindsAtMostOneName (BinderP ann) where (b:>_) @> x = b @> x {-# INLINE (@>) #-} -instance Color c => BindsOneName (BinderP c ann) c where +instance BindsOneName (BinderP ann) where binderName (b:>_) = binderName b {-# INLINE binderName #-} -instance (Color c, BindsAtMostOneName b1 c, BindsAtMostOneName b2 c) => - BindsAtMostOneName (EitherB b1 b2) c where +instance (BindsAtMostOneName b1, BindsAtMostOneName b2) => + BindsAtMostOneName (EitherB b1 b2) where ( LeftB b) @> x = b @> x (RightB b) @> x = b @> x {-# INLINE (@>) #-} -instance (Color c, BindsOneName b1 c, BindsOneName b2 c) => - BindsOneName (EitherB b1 b2) c where +instance (BindsOneName b1, BindsOneName b2) => + BindsOneName (EitherB b1 b2) where binderName ( LeftB b) = binderName b binderName (RightB b) = binderName b infixr 7 @@> -(@@>) :: (Foldable f, BindsNameList b c) => b i i' -> f (v c o) -> SubstFrag v i i' o +(@@>) :: (Foldable f, BindsNameList b) => b i i' -> f (v o) -> SubstFrag v i i' o (@@>) bs xs = bindNameList bs (toList xs) -class BindsNameList (b::B) (c::C) | b -> c where - bindNameList :: b i i' -> [v c o] -> SubstFrag v i i' o +class BindsNameList (b::B) where + bindNameList :: b i i' -> [v o] -> SubstFrag v i i' o -instance BindsAtMostOneName b c => BindsNameList (Nest b) c where +instance BindsAtMostOneName b => BindsNameList (Nest b) where bindNameList Empty [] = emptyInFrag bindNameList (Nest b rest) (x:xs) = b@>x <.> bindNameList rest xs bindNameList _ _ = error "length mismatch" @@ -716,17 +673,17 @@ forEachNestItem n f = runIdentity $ forEachNestItemM n (return . f) -- TODO: make a more general E-kinded Traversable? traverseSubstFrag :: forall v v' i i' o o' m . Monad m - => (forall c. Color c => v c o -> m (v' c o')) + => (v o -> m (v' o')) -> SubstFrag v i i' o -> m (SubstFrag v' i i' o') traverseSubstFrag f frag = liftM fromSubstPairs $ forEachNestItemM (toSubstPairs frag) \(SubstPair b val) -> SubstPair b <$> f val -lookupSubstFragProjected :: SubstFrag v i i' o -> Name c i' - -> Either (Name c i) (v c o) +lookupSubstFragProjected :: SubstFrag v i i' o -> Name i' + -> Either (Name i) (v o) lookupSubstFragProjected (UnsafeMakeSubst s) (UnsafeMakeName rawName) = case R.lookup rawName s of - Just d -> Right $ unsafeFromSubstItem d + Just d -> Right $ fromSubstItem d _ -> Left $ UnsafeMakeName rawName fromSubstPairs :: Nest (SubstPair v o) i i' -> SubstFrag v i i' o @@ -736,7 +693,7 @@ fromSubstPairs (Nest (SubstPair (UnsafeRepeatedNameBinder d (UnsafeMakeBinder b) foldMapSubstFrag :: forall v i i' o accum . Monoid accum - => (forall c. Color c => v c o -> accum) + => (v o -> accum) -> SubstFrag v i i' o -> accum foldMapSubstFrag f frag = execWriter $ traverseSubstFrag (\x -> tell (f x) >> return x) frag @@ -759,8 +716,8 @@ nestToListFlip :: BindsNames b -> [a] nestToListFlip bs f = nestToList f bs -nestToNames :: (Distinct l, Ext n l, BindsOneName b c, BindsNames b) - => Nest b n l -> [Name c l] +nestToNames :: (Distinct l, Ext n l, BindsOneName b, BindsNames b) + => Nest b n l -> [Name l] nestToNames bs = nestToList (sink . binderName) bs nestToList' :: (forall n' l'. b n' l' -> a) -> Nest b n l -> [a] @@ -798,18 +755,18 @@ joinRNest l r = case r of "joinRNest * REmpty" forall n. joinRNest n REmpty = n; #-} -binderAnn :: BinderP c ann n l -> ann n +binderAnn :: BinderP ann n l -> ann n binderAnn (_:>ann) = ann -withFreshM :: (Color c, ScopeExtender m) +withFreshM :: ScopeExtender m => NameHint - -> (forall o'. (DExt o o') => NameBinder c o o' -> m o' a) + -> (forall o'. DExt o o' => NameBinder o o' -> m o' a) -> m o a withFreshM hint cont = refreshAbsScope (newName hint) \b _ -> cont b -withManyFresh :: (Color c, Distinct n) +withManyFresh :: Distinct n => [NameHint] -> Scope n - -> (forall l. DExt n l => Nest (NameBinder c) n l -> a) -> a + -> (forall l. DExt n l => Nest NameBinder n l -> a) -> a withManyFresh [] _ cont = cont Empty withManyFresh (h:hs) scope cont = withFresh h scope \b -> @@ -818,7 +775,7 @@ withManyFresh (h:hs) scope cont = fmapRenamingM :: (RenameE e, SinkableE e, ScopeReader m) - => (forall c. Color c => Name c i -> Name c o) + => (Name i -> Name o) -> e i -> m o (e o) fmapRenamingM f e = do scope <- unsafeGetScope @@ -910,8 +867,8 @@ class ( forall i1 i2 o. Monad (m i1 i2 o) , forall i1 i2 o. MonadFail (m i1 i2 o) , forall i1 i2. ScopeExtender (m i1 i2)) => ZipSubstReader (m :: S -> S -> S -> * -> *) where - lookupZipSubstFst :: Color c => Name c i1 -> m i1 i2 o (Name c o) - lookupZipSubstSnd :: Color c => Name c i2 -> m i1 i2 o (Name c o) + lookupZipSubstFst :: Name i1 -> m i1 i2 o (Name o) + lookupZipSubstSnd :: Name i2 -> m i1 i2 o (Name o) extendZipSubstFst :: SubstFrag Name i1 i1' o -> m i1' i2 o r -> m i1 i2 o r extendZipSubstSnd :: SubstFrag Name i2 i2' o -> m i1 i2' o r -> m i1 i2 o r @@ -936,8 +893,6 @@ class SinkableB b => AlphaEqB (b::B) where -> m i1 i2 o a withAlphaEqB b1 b2 cont = withAlphaEqB (fromB b1) (fromB b2) $ cont -class (SinkableV v, forall c. Color c => AlphaEqE (v c)) => AlphaEqV (v::V) - addScope :: (ScopeReader m, SinkableE e) => e n -> m n (WithScope e n) addScope e = do scope <- unsafeGetScope @@ -945,8 +900,7 @@ addScope e = do return $ WithScope scope (sink e) {-# INLINE addScope #-} -alphaEq :: (AlphaEqE e, ScopeReader m) - => e n -> e n -> m n Bool +alphaEq :: (AlphaEqE e, ScopeReader m) => e n -> e n -> m n Bool alphaEq e1 e2 = do WithScope scope (PairE e1' e2') <- addScope $ PairE e1 e2 return $ case checkAlphaEqPure scope e1' e2' of @@ -959,27 +913,24 @@ checkAlphaEq e1 e2 = do WithScope scope (PairE e1' e2') <- addScope $ PairE e1 e2 liftExcept $ checkAlphaEqPure scope e1' e2' -alphaEqPure :: (AlphaEqE e, Distinct n) - => Scope n -> e n -> e n -> Bool +alphaEqPure :: (AlphaEqE e, Distinct n) => Scope n -> e n -> e n -> Bool alphaEqPure scope e1 e2 = checkAlphaEqPure scope e1 e2 & \case Success _ -> True Failure _ -> False -checkAlphaEqPure :: (AlphaEqE e, Distinct n) - => Scope n -> e n -> e n -> Except () +checkAlphaEqPure :: (AlphaEqE e, Distinct n) => Scope n -> e n -> e n -> Except () checkAlphaEqPure scope e1 e2 = runScopeReaderT scope $ flip runReaderT (emptyInMap, emptyInMap) $ runZipSubstReaderT $ withEmptyZipSubst $ alphaEqE e1 e2 -instance AlphaEqV Name -instance Color c => AlphaEqE (Name c) where +instance AlphaEqE Name where alphaEqE v1 v2 = do v1' <- lookupZipSubstFst v1 v2' <- lookupZipSubstSnd v2 unless (v1' == v2') zipErr -instance Color c => AlphaEqB (NameBinder c) where +instance AlphaEqB NameBinder where withAlphaEqB b1 b2 cont = do withFreshM (getNameHint b1) \b -> do let v = binderName b @@ -1021,7 +972,7 @@ instance Generic (e UnsafeS) => Generic (LiftB e n l) where instance AlphaEqE e => AlphaEqB (LiftB e) where withAlphaEqB (LiftB e1) (LiftB e2) cont = alphaEqE e1 e2 >> cont -instance (Color c, AlphaEqE ann) => AlphaEqB (BinderP c ann) where +instance AlphaEqE ann => AlphaEqB (BinderP ann) where withAlphaEqB (b1:>ann1) (b2:>ann2) cont = do alphaEqE ann1 ann2 withAlphaEqB b1 b2 $ cont @@ -1046,14 +997,14 @@ instance (AlphaEqE e1, AlphaEqE e2) => AlphaEqE (EitherE e1 e2) where -- === alpha-renaming-invariant hashing === type HashVal = Int -data NamePreHash (c::C) (n::S) = +data NamePreHash (n::S) = HashFreeName RawName -- XXX: convention is the opposite of de Bruijn order, `0` means -- the *outermost* binder | HashBoundName Int deriving (Eq, Generic) -instance Hashable (NamePreHash c n) +instance Hashable (NamePreHash n) data HashEnv n = -- the Int is the number of local binders in scope @@ -1062,13 +1013,13 @@ data HashEnv n = emptyHashEnv :: HashEnv n emptyHashEnv = HashEnv 0 (newSubst $ HashFreeName . getRawName) -lookupHashEnv :: Color c => HashEnv n -> Name c n -> NamePreHash c VoidS +lookupHashEnv :: HashEnv n -> Name n -> NamePreHash VoidS lookupHashEnv (HashEnv _ env) name = env ! name alphaHashWithSalt :: AlphaHashableE e => HashVal -> e n -> HashVal alphaHashWithSalt salt e = hashWithSaltE emptyHashEnv salt e -extendHashEnv :: Color c => HashEnv n -> NameBinder c n l -> HashEnv l +extendHashEnv :: HashEnv n -> NameBinder n l -> HashEnv l extendHashEnv (HashEnv depth env) b = HashEnv (depth + 1) (env <>> b @> HashBoundName depth) @@ -1085,10 +1036,10 @@ class AlphaHashableB (b::B) where => HashEnv n -> HashVal -> b n l -> (HashVal, HashEnv l) hashWithSaltB env salt b = hashWithSaltB env salt (fromB b) -instance Color c => AlphaHashableE (Name c) where +instance AlphaHashableE Name where hashWithSaltE env salt v = hashWithSalt salt $ lookupHashEnv env v -instance Color c => AlphaHashableB (NameBinder c) where +instance AlphaHashableB NameBinder where hashWithSaltB env salt b = (salt, extendHashEnv env b) instance AlphaHashableE UnitE where @@ -1117,7 +1068,7 @@ instance (AlphaHashableB b1, AlphaHashableB b2) let (h, env') = hashWithSaltB env salt b1 hashWithSaltB env' h b2 -instance (Color c, AlphaHashableE ann) => AlphaHashableB (BinderP c ann) where +instance (AlphaHashableE ann) => AlphaHashableB (BinderP ann) where hashWithSaltB env salt (b:>ann) = do let h = hashWithSaltE env salt ann hashWithSaltB env h b @@ -1153,18 +1104,6 @@ instance (AlphaHashableB b1, AlphaHashableB b2) instance AlphaHashableE VoidE where hashWithSaltE _ _ _ = error "impossible" -instance (p ~ True => AlphaHashableE e) => AlphaHashableE (WhenE p e) where - hashWithSaltE env val (WhenE e) = hashWithSaltE env val e - -instance (r~r' => AlphaHashableE e) => AlphaHashableE (WhenIRE r r' e) where - hashWithSaltE env val (WhenIRE e) = hashWithSaltE env val e - -instance (c~c' => AlphaHashableE e) => AlphaHashableE (WhenC c c' e) where - hashWithSaltE env val (WhenC e) = hashWithSaltE env val e - -instance (forall r. c ~ AtomNameC r => AlphaHashableE (e r)) => AlphaHashableE (WhenAtomName c e) where - hashWithSaltE env val (WhenAtomName e) = hashWithSaltE env val e - -- === wrapper for E-kinded things suitable for use as keys === newtype EKey (e::E) (n::S) = EKey { fromEKey :: e n } @@ -1422,7 +1361,7 @@ extendSubInplaceT ab = do freshExtendSubInplaceT :: (ExtOutMap b d, ExtOutFrag ds d, Monad m) - => Mut n => NameHint -> (forall l. NameBinder c n l -> (d n l, e l)) -> InplaceT b ds m n (e n) + => Mut n => NameHint -> (forall l. NameBinder n l -> (d n l, e l)) -> InplaceT b ds m n (e n) freshExtendSubInplaceT hint build = UnsafeMakeInplaceT \env decls -> withFresh hint (toScope env) \b -> do @@ -1673,69 +1612,12 @@ extendDoubleInplaceTLocal f cont = -- === name hints === -instance HasNameHint (BinderP c ann n l) where +instance HasNameHint (BinderP ann n l) where getNameHint (b:>_) = getNameHint b --- === handling the dynamic/heterogeneous stuff for Subst === - -data ColorProxy (c::C) = ColorProxy - -data ColorsEqual (c1::C) (c2::C) where - ColorsEqual :: ColorsEqual c c - -eqColorRep :: forall c1 c2. (Color c1, Color c2) => Maybe (ColorsEqual c1 c2) -eqColorRep = if c1Rep == c2Rep - then Just (TrulyUnsafe.unsafeCoerce (ColorsEqual :: ColorsEqual c1 c1) :: ColorsEqual c1 c2) - else Nothing - where c1Rep = getColorRep @c1; c2Rep = getColorRep @c2 -{-# INLINE eqColorRep #-} - -tryAsColor :: forall (v::V) (c1::C) (c2::C) (n::S). - (Color c1, Color c2) => v c1 n -> Maybe (v c2 n) -tryAsColor x = case eqColorRep of - Just (ColorsEqual :: ColorsEqual c1 c2) -> Just x - Nothing -> Nothing - --- like Typeable, this gives a term-level representation of a name color -class Color (c::C) where - getColorRep :: C - -instance IRRep r => Color (AtomNameC r) where getColorRep = AtomNameC $ getIRRep @r -instance Color TyConNameC where getColorRep = TyConNameC -instance Color DataConNameC where getColorRep = DataConNameC -instance Color ClassNameC where getColorRep = ClassNameC -instance Color InstanceNameC where getColorRep = InstanceNameC -instance Color MethodNameC where getColorRep = MethodNameC -instance Color TopFunNameC where getColorRep = TopFunNameC -instance Color FunObjCodeNameC where getColorRep = FunObjCodeNameC -instance Color ModuleNameC where getColorRep = ModuleNameC -instance Color PtrNameC where getColorRep = PtrNameC -instance Color SpecializedDictNameC where getColorRep = SpecializedDictNameC -instance Color ImpNameC where getColorRep = ImpNameC --- The instance for Color UnsafeC is purposefully missing! UnsafeC is --- only used for storing heterogeneously-colored values and we should --- restore their type before we every try to reflect upon their color! - -interpretColor :: C -> (forall c. Color c => ColorProxy c -> a) -> a -interpretColor c cont = case c of - AtomNameC CoreIR -> cont $ ColorProxy @(AtomNameC CoreIR) - AtomNameC SimpIR -> cont $ ColorProxy @(AtomNameC SimpIR) - TyConNameC -> cont $ ColorProxy @TyConNameC - DataConNameC -> cont $ ColorProxy @DataConNameC - ClassNameC -> cont $ ColorProxy @ClassNameC - InstanceNameC -> cont $ ColorProxy @InstanceNameC - MethodNameC -> cont $ ColorProxy @MethodNameC - TopFunNameC -> cont $ ColorProxy @TopFunNameC - FunObjCodeNameC -> cont $ ColorProxy @FunObjCodeNameC - ModuleNameC -> cont $ ColorProxy @ModuleNameC - PtrNameC -> cont $ ColorProxy @PtrNameC - SpecializedDictNameC -> cont $ ColorProxy @SpecializedDictNameC - ImpNameC -> cont $ ColorProxy @ImpNameC - UnsafeC -> error "shouldn't reflect over Unsafe colors!" - -- === instances === -instance SinkableV v => SinkableE (Subst v i) where +instance SinkableE v => SinkableE (Subst v i) where sinkingProofE fresh (Subst f m) = Subst (\name -> sinkingProofE fresh $ f name) (sinkingProofE fresh m) @@ -1813,15 +1695,15 @@ instance (RenameB b1, RenameB b2) => RenameB (EitherB b1 b2) where renameB env b \env' b' -> cont env' $ RightB b' -instance GenericB (BinderP c ann) where - type RepB (BinderP c ann) = PairB (LiftB ann) (NameBinder c) +instance GenericB (BinderP ann) where + type RepB (BinderP ann) = PairB (LiftB ann) NameBinder fromB (b:>ann) = PairB (LiftB ann) b toB (PairB (LiftB ann) b) = b:>ann -instance (Color c, SinkableE ann) => SinkableB (BinderP c ann) -instance (Color c, SinkableE ann, RenameE ann) => RenameB (BinderP c ann) -instance Color c => ProvesExt (BinderP c ann) -instance Color c => BindsNames (BinderP c ann) where +instance SinkableE ann => SinkableB (BinderP ann) +instance (SinkableE ann, RenameE ann) => RenameB (BinderP ann) +instance ProvesExt (BinderP ann) +instance BindsNames (BinderP ann) where toScopeFrag (b :> _) = toScopeFrag b instance BindsNames b => ProvesExt (RNest b) where @@ -1908,10 +1790,6 @@ instance AlphaEqB VoidB where instance RenameB VoidB where renameB _ _ _ = error "impossible" -instance SinkableE const => SinkableV (ConstE const) -instance SinkableE const => SinkableE (ConstE const ignored) where - sinkingProofE fresh (ConstE e) = ConstE $ sinkingProofE fresh e - instance SinkableE VoidE where sinkingProofE _ _ = error "impossible" @@ -2014,86 +1892,6 @@ instance RenameE e => RenameE (ListE e) where instance RenameE e => RenameE (NonEmptyListE e) where renameE env (NonEmptyListE xs) = NonEmptyListE $ fmap (renameE env) xs -instance (p ~ True => SinkableE e) => SinkableE (WhenE p e) where - sinkingProofE rename (WhenE e) = WhenE $ sinkingProofE rename e - -instance (p ~ True => HoistableE e) => HoistableE (WhenE p e) where - freeVarsE (WhenE e) = freeVarsE e - -instance (p ~ True => RenameE e) => RenameE (WhenE p e) where - renameE (scope, subst) (WhenE e) = WhenE $ renameE (scope, subst) e - -instance (p ~ True => AlphaEqE e) => AlphaEqE (WhenE p e) where - alphaEqE (WhenE e1) (WhenE e2) = alphaEqE e1 e2 - -instance (r~r' => SinkableE e) => SinkableE (WhenIRE r r' e) where - sinkingProofE rename (WhenIRE e) = WhenIRE $ sinkingProofE rename e - -instance (r~r' => HoistableE e) => HoistableE (WhenIRE r r' e) where - freeVarsE (WhenIRE e) = freeVarsE e - -instance (r~r' => RenameE e) => RenameE (WhenIRE r r' e) where - renameE (scope, subst) (WhenIRE e) = WhenIRE $ renameE (scope, subst) e - -instance (r~r' => AlphaEqE e) => AlphaEqE (WhenIRE r r' e) where - alphaEqE (WhenIRE e1) (WhenIRE e2) = alphaEqE e1 e2 - -instance (c~c' => SinkableE e) => SinkableE (WhenC c c' e) where - sinkingProofE rename (WhenC e) = WhenC $ sinkingProofE rename e - -instance (c~c' => HoistableE e) => HoistableE (WhenC c c' e) where - freeVarsE (WhenC e) = freeVarsE e - -instance (c~c' => RenameE e) => RenameE (WhenC c c' e) where - renameE (scope, subst) (WhenC e) = WhenC $ renameE (scope, subst) e - -instance (c~c' => AlphaEqE e) => AlphaEqE (WhenC c c' e) where - alphaEqE (WhenC e1) (WhenC e2) = alphaEqE e1 e2 - -instance (Color c, forall r. (c ~ AtomNameC r, IRRep r) => SinkableE (e r)) - => SinkableE (WhenAtomName c e) where - sinkingProofE rename (WhenAtomName e) = - withIRRepFromColor @c \_ -> WhenAtomName $ sinkingProofE rename e - -instance (Color c, forall r. (c ~ AtomNameC r, IRRep r) => HoistableE (e r)) - => HoistableE (WhenAtomName c e) where - freeVarsE (WhenAtomName e) = withIRRepFromColor @c \_ -> freeVarsE e - -instance (Color c, forall r. (c ~ AtomNameC r, IRRep r) => RenameE (e r)) - => RenameE (WhenAtomName c e) where - renameE (scope, subst) (WhenAtomName e) = - withIRRepFromColor @c \_ -> WhenAtomName $ renameE (scope, subst) e - -instance (Color c, forall r. (c ~ AtomNameC r, IRRep r) => AlphaEqE (e r)) - => AlphaEqE (WhenAtomName c e) where - alphaEqE (WhenAtomName e1) (WhenAtomName e2) = - withIRRepFromColor @c \_ -> alphaEqE e1 e2 - -tryAsAtomName - :: forall c a. Color c - => (forall r. (c ~ AtomNameC r, IRRep r) => IRProxy r -> a) - -> Maybe a -tryAsAtomName cont = - case getColorRep @c of - AtomNameC r -> Just $ interpretIR r \(p :: IRProxy r) -> - case eqColorRep @c @(AtomNameC r) of - Just ColorsEqual -> cont p - Nothing -> error "impossible" - _ -> Nothing - -withIRRepFromColor - :: forall c r a. (c ~ AtomNameC r, Color (AtomNameC r)) - => (IRRep r => IRProxy r -> a) -> a -withIRRepFromColor cont = - case getColorRep @c of - AtomNameC r -> do - interpretIR r \(IRProxy :: IRProxy r') -> - case eqColorRep @(AtomNameC r') @(AtomNameC r) of - Just ColorsEqual -> cont IRProxy - Nothing -> error "impossible" - _ -> error "impossible" -{-# INLINE withIRRepFromColor #-} - instance (PrettyB b, PrettyE e) => Pretty (Abs b e n) where pretty (Abs b body) = group $ "(Abs " <> nest 2 (pretty b <> line <> pretty body) <> line <> ")" @@ -2117,7 +1915,7 @@ instance PrettyE e => Pretty (ListE e n) where instance PrettyE e => Pretty (RListE e n) where pretty (RListE e) = pretty $ unsnoc e -deriving instance (forall c n. Pretty (v c n)) => Pretty (RecSubst v o) +deriving instance (forall n. Pretty (v n)) => Pretty (RecSubst v o) instance ( Generic (b UnsafeS UnsafeS) , Generic (body UnsafeS) ) @@ -2150,12 +1948,12 @@ instance ProvesExt (RecSubstFrag v) where instance BindsNames (RecSubstFrag v) where toScopeFrag env = substFragAsScope $ fromRecSubstFrag env {-# INLINE toScopeFrag #-} -instance HoistableV v => HoistableB (RecSubstFrag v) where +instance HoistableE v => HoistableB (RecSubstFrag v) where freeVarsB (RecSubstFrag env) = freeVarsE (Abs (substFragAsScope env) env) -- Traversing a recursive set of bindings is a bit tricky because we have to do -- two passes: first we rename the binders, then we go and subst the payloads. -instance RenameV v => RenameB (RecSubstFrag v) where +instance (SinkableE v, RenameE v) => RenameB (RecSubstFrag v) where renameB env (RecSubstFrag recSubst) cont = do let pairs = toSubstPairs recSubst renameSubstPairBinders env pairs \env' pairs' -> do @@ -2164,7 +1962,7 @@ instance RenameV v => RenameB (RecSubstFrag v) where cont env' $ RecSubstFrag $ fromSubstPairs pairs'' renameSubstPairBinders - :: (Distinct o, SinkableV v) + :: (Distinct o, SinkableE v) => (Scope o, Subst Name i o) -> Nest (SubstPair v ignored) i i' -> (forall o'. @@ -2179,16 +1977,9 @@ renameSubstPairBinders env (Nest (SubstPair b v) rest) cont = renameSubstPairBinders env' rest \env'' rest' -> cont env'' (Nest (SubstPair b' v) rest') -instance HoistableE (UniformNameSet c) where - freeVarsE (UniformNameSet s) = UnsafeMakeNameSet s - -instance RenameE (UniformNameSet c) where - renameE _ (UniformNameSet _) = undefined - -instance SinkableV v => SinkableB (RecSubstFrag v) where +instance SinkableE v => SinkableB (RecSubstFrag v) where sinkingProofB _ _ _ = todoSinkableProof -instance Store C instance Store (UnitE n) instance Store (VoidE n) instance (Store (e1 n), Store (e2 n)) => Store (PairE e1 e2 n) @@ -2197,43 +1988,14 @@ instance (Store (b1 n l), Store (b2 n l)) => Store (EitherB b1 b2 n l) instance Store (e n) => Store (ListE e n) instance Store a => Store (LiftE a n) instance (Store (e UnsafeS), Generic (e UnsafeS)) => Store (LiftB e n l) -instance Store (const n) => Store (ConstE const ignored n) -instance (Store (ann n)) => Store (BinderP c ann n l) +instance (Store (ann n)) => Store (BinderP ann n l) instance (forall a. Store a => Store (f a), Store (e n)) => Store (ComposeE f e n) -instance ( forall c. Color c => Store (v c o') - , forall c. Color c => Generic (v c o')) - => Store (RecSubstFrag v o o') +instance (Store (v o'), Generic (v o')) => Store (RecSubstFrag v o o') -instance ( forall c. Color c => Store (v c o) - , forall c. Color c => Generic (v c o)) - => Store (RecSubst v o) +instance (Store (v o), Generic (v o)) => Store (RecSubst v o) instance Store (Scope n) -deriving instance (forall c n. Pretty (v c n)) => Pretty (RecSubstFrag v o o') - -instance (p ~ True => Store (e n)) => Store (WhenE p e n) where - size = VarSize \(WhenE e) -> getSize e - peek = withFabricatedTruth @p (WhenE <$> peek) - poke (WhenE e) = poke e - -instance (IRRep r, IRRep r', Store (e n)) => Store (WhenIRE r r' e n) where - size = VarSize \(WhenIRE e) -> getSize e - peek = case eqIRRep @r @r' of - Just IRsEqual -> WhenIRE <$> peek - Nothing -> error "impossible" - poke (WhenIRE e) = poke e - -instance (Color c, Color c', Store (e n)) => Store (WhenC c c' e n) where - size = VarSize \(WhenC e) -> getSize e - peek = case eqColorRep @c @c' of - Just ColorsEqual -> WhenC <$> peek - Nothing -> error "impossible" - poke (WhenC e) = poke e - -instance (Color c, forall r. (c ~ AtomNameC r, IRRep r) => Store (e r n)) => Store (WhenAtomName c e n) where - size = VarSize \(WhenAtomName e) -> withIRRepFromColor @c \_ -> getSize e - peek = fromJust $ tryAsAtomName @c \_ -> WhenAtomName <$> peek - poke (WhenAtomName e) = withIRRepFromColor @c \_ -> poke e +deriving instance (forall n. Pretty (v n)) => Pretty (RecSubstFrag v o o') -- We often have high-degree sum types that need GenericE instances, and -- EitherE seems like a natural choice for those. However, if you have 20 @@ -2383,23 +2145,6 @@ data S = (:=>:) S S | VoidS | UnsafeS --- Name "color" ("type", "kind", etc. already taken) -data C = - AtomNameC !IR - | TyConNameC - | DataConNameC - | ClassNameC - | InstanceNameC - | MethodNameC - | TopFunNameC - | FunObjCodeNameC - | ModuleNameC - | PtrNameC - | SpecializedDictNameC - | UnsafeC - | ImpNameC - deriving (Eq, Ord, Generic, Show) - type E = S -> * -- expression-y things, covariant in the S param type B = S -> S -> * -- binder-y things, covariant in the first param and -- contravariant in the second. These are things like @@ -2407,15 +2152,11 @@ type B = S -> S -> * -- binder-y things, covariant in the first param and -- `ScopeFrag n l`, extending `n` to `l`. Their free -- name are in `Scope n`. We sometimes call `n` the -- "outside scope" and "l" the "inside scope". -type V = C -> E -- value-y things that we might look up in an environment - -- with a `Name c n`, parameterized by the name's color. -- We use SubstItem for ColorRep to be able to unsafeCoerce scopes into name sets in O(1). type ColorRep = SubstItem GHC.Exts.Any UnsafeS newtype NameSet (n::S) = UnsafeMakeNameSet { fromNameSet :: RawNameMap ColorRep } deriving (Monoid, Semigroup) -newtype UniformNameSet (c::C) (n::S) = UniformNameSet (RawNameMap ColorRep) - deriving (Monoid, Semigroup) -- ScopeFrag is a SubstFrag that can contain _any_ V-kinded thing. -- Semantically it is equivalent to M.Map RawName [C]. @@ -2442,43 +2183,37 @@ instance Category ScopeFrag where UnsafeMakeScopeFrag $ R.unionWith takeLeftNonDistinct s2 s1 {-# INLINE (.) #-} -instance Color c => BindsNames (NameBinder c) where +instance BindsNames NameBinder where toScopeFrag (UnsafeMakeBinder v) = substFragAsScope $ UnsafeMakeSubst $ R.singleton v $ toSubstItem DistinctName - (TrulyUnsafe.unsafeCoerce UnitV :: GHC.Exts.Any c VoidS) + (TrulyUnsafe.unsafeCoerce UnitE :: GHC.Exts.Any c VoidS) -absurdNameFunction :: Name v VoidS -> a +absurdNameFunction :: Name VoidS -> a absurdNameFunction v = error $ "Void names shouldn't exist: " ++ show v scopeFragToSubstFrag :: forall v i i' o - . (forall c. Name c (i:=>:i') -> v c o) + . (forall c. Name (i:=>:i') -> v o) -> ScopeFrag i i' -> SubstFrag v i i' o scopeFragToSubstFrag f (UnsafeScopeFromSubst m) = fmapSubstFrag (\n _ -> f n) m -newtype Name (c::C) -- Name color - (n::S) -- Scope parameter +newtype Name (n::S) -- Scope parameter = UnsafeMakeName RawName deriving (Show, Eq, Ord, Pretty, HasNameHint, Generic, Store) -newtype NameBinder (c::C) -- name color - (n::S) -- scope above the binder +newtype NameBinder (n::S) -- scope above the binder (l::S) -- scope under the binder (`l` for "local") = UnsafeMakeBinder RawName deriving (Show, Pretty, HasNameHint, Generic, Store) -newBinder :: NameHint -> (forall l. NameBinder c VoidS l -> a) -> a +newBinder :: NameHint -> (forall l. NameBinder VoidS l -> a) -> a newBinder hint cont = cont $ UnsafeMakeBinder $ rawNameFromHint hint -- Closed binder-name pair. The name isn't fresh and it doesn't pretend to be. -- It's intended for subsequent refreshing. -newName :: Color c => NameHint -> Abs (NameBinder c) (Name c) n +newName :: NameHint -> Abs NameBinder Name n newName hint = sinkFromTop $ newBinder hint \b -> Abs b $ binderName b --- uses the monad just to diambiguate the scope parameter -newNameM :: Color c => Monad1 m => NameHint -> m n (Abs (NameBinder c) (Name c) n) -newNameM hint = return $ newName hint - -newNames :: Int -> Abs (Nest (NameBinder c)) (ListE (Name c)) n +newNames :: Int -> Abs (Nest NameBinder) (ListE Name) n newNames n = do let ns = rawNames n let vs = map UnsafeMakeName ns @@ -2487,11 +2222,11 @@ newNames n = do withFresh :: forall n c a. (Distinct n) => NameHint -> Scope n - -> (forall l. DExt n l => NameBinder c n l -> a) -> a + -> (forall l. DExt n l => NameBinder n l -> a) -> a withFresh hint (Scope (UnsafeMakeScopeFrag scope)) cont = withFabricatedDistinct @UnsafeS $ withFabricatedExt @n @UnsafeS $ - cont $ (UnsafeMakeBinder (freshRawName hint scope) :: NameBinder c n UnsafeS) + cont $ (UnsafeMakeBinder (freshRawName hint scope) :: NameBinder n UnsafeS) {-# INLINE withFresh #-} -- proves that the names in n are distinct @@ -2528,7 +2263,7 @@ withSubscopeDistinct b cont = {-# INLINE withSubscopeDistinct #-} -- useful for printing etc. -getRawName :: Name c n -> RawName +getRawName :: Name n -> RawName getRawName (UnsafeMakeName rawName) = rawName -- === sinkings === @@ -2616,23 +2351,10 @@ class SinkableB (b::B) where sinkingProofB fresh b cont = sinkingProofB fresh (fromB b) \fresh' b' -> cont fresh' $ toB b' --- previously we just had the alias --- `type SinkableV v = forall c. SinkableE (v c)` --- but GHC seemed to have trouble figuring out superclasses etc. so --- we're making it an explicit class instead -class (forall c. Color c => SinkableE (v c)) - => SinkableV (v::V) - -class (forall c. Color c => HoistableE (v c)) - => HoistableV (v::V) - data SinkingCoercion (n::S) (l::S) where - SinkingCoercion :: (forall s. Name s n -> Name s l) -> SinkingCoercion n l - -instance SinkableV Name -instance HoistableV Name + SinkingCoercion :: (Name n -> Name l) -> SinkingCoercion n l -instance SinkableE (Name c) where +instance SinkableE Name where sinkingProofE (SinkingCoercion f) name = f name -- This is the unsafely-implemented base case. Here's why it's valid. Let's say @@ -2644,7 +2366,7 @@ instance SinkableE (Name c) where -- (1) x itself, in which case it's also in l' -- (2) in n, in which case it can be sinked to n'. The only issue would be -- if it were shadowed by x, but it can't be because then we'd be in case (1). -instance SinkableB (NameBinder s) where +instance SinkableB NameBinder where sinkingProofB _ (UnsafeMakeBinder b) cont = cont (SinkingCoercion unsafeCoerceE) (UnsafeMakeBinder b) @@ -2745,20 +2467,18 @@ sinkFromTop :: SinkableE e => e VoidS -> e n sinkFromTop = unsafeCoerceE {-# INLINE sinkFromTop #-} -freeVarsList :: (HoistableE e, Color c) => e n -> [Name c n] +freeVarsList :: HoistableE e => e n -> [Name n] freeVarsList e = nameSetToList $ freeVarsE e -nameSetToList :: forall c n. Color c => NameSet n -> [Name c n] +nameSetToList :: NameSet n -> [Name n] nameSetToList nameSet = - catMaybes $ flip map (R.toList $ fromNameSet nameSet) \(rawName, item) -> - case fromSubstItem item of - Nothing -> Nothing - Just (_ :: GHC.Exts.Any c UnsafeS) -> Just $ UnsafeMakeName rawName + flip map (R.toList $ fromNameSet nameSet) \(rawName, item) -> + UnsafeMakeName rawName nameSetIntersection :: NameSet n -> NameSet n -> NameSet n nameSetIntersection s1 s2 = UnsafeMakeNameSet $ R.intersection (fromNameSet s1) (fromNameSet s2) -boundNamesList :: (BindsNames b, Color c) => b n l -> [Name c l] +boundNamesList :: BindsNames b => b n l -> [Name l] boundNamesList b = nameSetToList $ toNameSet $ toScopeFrag b toNameSet :: ScopeFrag n l -> NameSet l @@ -2767,13 +2487,13 @@ toNameSet (UnsafeMakeScopeFrag s) = UnsafeMakeNameSet s nameSetRawNames :: NameSet n -> [RawName] nameSetRawNames m = R.keys $ fromNameSet m -isInNameSet :: Name c n -> NameSet n -> Bool +isInNameSet :: Name n -> NameSet n -> Bool isInNameSet v ns = getRawName v `R.member` fromNameSet ns -isFreeIn :: HoistableE e => Name c n -> e n -> Bool +isFreeIn :: HoistableE e => Name n -> e n -> Bool isFreeIn v e = getRawName v `R.member` fromNameSet (freeVarsE e) -anyFreeIn :: HoistableE e => [Name c n] -> e n -> Bool +anyFreeIn :: HoistableE e => [Name n] -> e n -> Bool anyFreeIn vs e = not $ R.disjoint (R.fromList $ map (\v -> (getRawName v, ())) vs) (fromNameSet $ freeVarsE e) @@ -2811,7 +2531,7 @@ partitionBinders sid bs assignBinder = go bs where -- NameBinder has no free vars, so there's no risk associated with hoisting. -- The scope is completely distinct, so their exchange doesn't create any accidental -- capture either. -exchangeNameBinder :: (Distinct l, SinkableB b) => b n p -> NameBinder c p l -> PairB (NameBinder c) b n l +exchangeNameBinder :: (Distinct l, SinkableB b) => b n p -> NameBinder p l -> PairB NameBinder b n l exchangeNameBinder b nb = PairB (unsafeCoerceB nb) (unsafeCoerceB b) {-# INLINE exchangeNameBinder #-} @@ -2820,19 +2540,19 @@ hoistFilterNameSet b nameSet = UnsafeMakeNameSet $ fromNameSet nameSet `R.difference` frag where UnsafeMakeScopeFrag frag = toScopeFrag b -abstractFreeVar :: Name c n -> e n -> Abs (NameBinder c) e n +abstractFreeVar :: Name n -> e n -> Abs NameBinder e n abstractFreeVar v e = case abstractFreeVarsNoAnn [v] e of Abs (Nest b Empty) e' -> Abs b e' _ -> error "impossible" -abstractFreeVars :: [(Name c n, ann n)] -> e n -> Abs (Nest (BinderP c ann)) e n +abstractFreeVars :: [(Name n, ann n)] -> e n -> Abs (Nest (BinderP ann)) e n abstractFreeVars vs e = Abs bs e where bs = unsafeCoerceB $ unsafeListToNest bsFlat bsFlat = vs <&> \(UnsafeMakeName v, ann) -> UnsafeMakeBinder v :> unsafeCoerceE ann -abstractFreeVarsNoAnn :: [Name c n] -> e n -> Abs (Nest (NameBinder c)) e n +abstractFreeVarsNoAnn :: [Name n] -> e n -> Abs (Nest NameBinder) e n abstractFreeVarsNoAnn vs e = case abstractFreeVars (zip vs (repeat UnitE)) e of Abs bs e' -> Abs bs' e' @@ -2842,18 +2562,18 @@ unsafeFromNest :: Nest b n l -> [b UnsafeS UnsafeS] unsafeFromNest Empty = [] unsafeFromNest (Nest b rest) = unsafeCoerceB b : unsafeFromNest rest -instance Color c => HoistableB (NameBinder c) where +instance HoistableB NameBinder where freeVarsB _ = mempty -instance Color c => HoistableE (Name c) where +instance HoistableE Name where freeVarsE name = UnsafeMakeNameSet $ R.singleton (getRawName name) $ - toSubstItem DistinctName (TrulyUnsafe.unsafeCoerce UnitV :: GHC.Exts.Any c UnsafeS) + toSubstItem DistinctName (TrulyUnsafe.unsafeCoerce UnitE :: GHC.Exts.Any UnsafeS) instance (HoistableB b1, HoistableB b2) => HoistableB (PairB b1 b2) where freeVarsB (PairB b1 b2) = freeVarsB b1 <> hoistFilterNameSet b1 (freeVarsB b2) -instance (Color c, HoistableE ann) => HoistableB (BinderP c ann) where +instance HoistableE ann => HoistableB (BinderP ann) where freeVarsB (b:>ann) = freeVarsB b <> freeVarsE ann instance HoistableB UnitB where @@ -2874,70 +2594,46 @@ instance HoistableE e => HoistableE (RListE e) where -- long chains of case analyses as we extend environments one name at a time. newtype SubstFrag - (v ::V) -- env payload, as a function of the name's color + (v ::E) -- env payload, as a function of the name's color (i ::S) -- starting scope parameter for names we can look up in this env (i'::S) -- ending scope parameter for names we can look up in this env (o ::S) -- scope parameter for the values stored in the env = UnsafeMakeSubst (RawNameMap (SubstItem v o)) - deriving (Generic) -deriving instance (forall c. Show (v c o)) => Show (SubstFrag v i i' o) - -data SubstItem (v::V) (n::S) = SubstItem !FragNameDistinctness !C (v UnsafeC n) -deriving instance (forall c. Show (v c n)) => Show (SubstItem v n) + deriving (Generic, Show) -unsafeFromSubstItem :: forall c v o. SubstItem v o -> (v c o) -unsafeFromSubstItem (SubstItem _ _ val) = TrulyUnsafe.unsafeCoerce val -{-# INLINE unsafeFromSubstItem #-} +data SubstItem (e::E) (n::S) = SubstItem !FragNameDistinctness (e n) + deriving (Show, Generic) -fromSubstItem :: forall c v o. Color c => SubstItem v o -> Maybe (v c o) -fromSubstItem (SubstItem _ c (val :: v c' o)) = - case c == getColorRep @c of - True -> Just (TrulyUnsafe.unsafeCoerce val :: v c o) - False -> Nothing +fromSubstItem :: SubstItem v o -> (v o) +fromSubstItem (SubstItem _ val) = val {-# INLINE fromSubstItem #-} -toSubstItem :: forall v c o. Color c => FragNameDistinctness -> v c o -> SubstItem v o -toSubstItem d v = SubstItem d (getColorRep @c) (unsafeCoerceVC v) +toSubstItem :: forall v o. FragNameDistinctness -> v o -> SubstItem v o +toSubstItem d e = SubstItem d e {-# INLINE toSubstItem #-} -fromSubstItemPoly :: forall v o a. SubstItem v o -> (forall c. Color c => v c o -> a) -> a -fromSubstItemPoly (SubstItem _ c v) cont = - interpretColor c \(ColorProxy :: ColorProxy c) -> cont (unsafeCoerceVC @c v) -{-# INLINE fromSubstItemPoly #-} - --- === Packed representation of SubstItem properties === --- We use the MSB to encode shadowing: a name has been shadowed in the current --- fragment if the bit is set. The rest of the bits are used to encode the tag --- of the C constructor (representing name's color). - -newtype SubstItemFlags = SubstItemFlags Int deriving (Show, Store) - -shadowBit :: Int -shadowBit = finiteBitSize @Int undefined - 1 -{-# INLINE shadowBit #-} - data FragNameDistinctness = DistinctName | ShadowingName deriving (Eq, Show, Generic) instance Store FragNameDistinctness itemDistinctness :: SubstItem v n -> FragNameDistinctness -itemDistinctness (SubstItem d _ _) = d +itemDistinctness (SubstItem d _) = d {-# INLINE itemDistinctness #-} takeLeftNonDistinct :: SubstItem v n -> SubstItem v n -> SubstItem v n -takeLeftNonDistinct (SubstItem _ c v) _ = SubstItem ShadowingName c v +takeLeftNonDistinct (SubstItem _ v) _ = SubstItem ShadowingName v -- === environments and scopes === -lookupSubstFrag :: SubstFrag v i i' o -> Name c (i:=>:i') -> v c o +lookupSubstFrag :: SubstFrag v i i' o -> Name (i:=>:i') -> v o lookupSubstFrag (UnsafeMakeSubst m) (UnsafeMakeName rawName) = undefined case R.lookup rawName m of - Just d -> unsafeFromSubstItem d + Just d -> fromSubstItem d _ -> error "Subst lookup failed (this should never happen)" -- Just for debugging -lookupSubstFragRaw :: SubstFrag v i i' o -> RawName -> Maybe (v UnsafeC o) +lookupSubstFragRaw :: SubstFrag v i i' o -> RawName -> Maybe (v o) lookupSubstFragRaw (UnsafeMakeSubst m) rawName = - R.lookup rawName m <&> \(SubstItem _ _ v) -> v + R.lookup rawName m <&> \(SubstItem _ v) -> v instance InFrag (SubstFrag v) where emptyInFrag = UnsafeMakeSubst mempty @@ -2946,24 +2642,23 @@ instance InFrag (SubstFrag v) where UnsafeMakeSubst (R.unionWith takeLeftNonDistinct m2 m1) {-# INLINE catInFrags #-} -singletonSubst :: Color c => NameBinder c i i' -> v c o -> SubstFrag v i i' o +singletonSubst :: NameBinder i i' -> v o -> SubstFrag v i i' o singletonSubst (UnsafeMakeBinder name) x = UnsafeMakeSubst $ R.singleton name $ toSubstItem DistinctName x {-# INLINE singletonSubst #-} -fmapSubstFrag :: (forall c. Color c => Name c (i:=>:i') -> v c o -> v' c o') +fmapSubstFrag :: (Name (i:=>:i') -> v o -> v' o') -> SubstFrag v i i' o -> SubstFrag v' i i' o' fmapSubstFrag f (UnsafeMakeSubst m) = - UnsafeMakeSubst $ flip R.mapWithKey m $ \k item@(SubstItem d c _) -> - SubstItem d c $ fromSubstItemPoly item \v -> - unsafeCoerceVC @UnsafeC $ f (UnsafeMakeName k) v + UnsafeMakeSubst $ flip R.mapWithKey m $ \k item@(SubstItem d x) -> + SubstItem d $ f (UnsafeMakeName k) x substFragAsScope :: forall v i i' o. SubstFrag v i i' o -> ScopeFrag i i' substFragAsScope m = UnsafeMakeScopeFrag $ TrulyUnsafe.unsafeCoerce m -- === garbage collection === -collectGarbage :: (HoistableV v, HoistableE e) +collectGarbage :: (HoistableE v, HoistableE e) => Distinct l => RecSubstFrag v n l -> e l -> (forall l'. Distinct l' => RecSubstFrag v n l' -> e l' -> a) -> a @@ -2980,46 +2675,46 @@ collectGarbage (RecSubstFrag (UnsafeMakeSubst env)) e cont = do Just item | itemDistinctness item == ShadowingName -> error "shouldn't be possible, due to Distinct constraint" #endif - Just item -> R.keys $ fromSubstItemPoly item (fromNameSet . freeVarsE) + Just item -> R.keys $ fromNameSet $ freeVarsE $ fromSubstItem item -- === iterating through env pairs === -- Taking this binder apart is unsafe, because converting a nest of RepeatedNameBinders -- into a nest of their consecutive NameBinders is expressible in the safe fragment, but -- it doesn't preserve the multiplicity of names in a scope fragment! -data RepeatedNameBinder (c::C) (n::S) (l::S) where - UnsafeRepeatedNameBinder :: !FragNameDistinctness -> NameBinder c n l -> RepeatedNameBinder c n l -instance Color c => SinkableB (RepeatedNameBinder c) where +data RepeatedNameBinder (n::S) (l::S) where + UnsafeRepeatedNameBinder :: !FragNameDistinctness -> NameBinder n l -> RepeatedNameBinder n l +instance SinkableB RepeatedNameBinder where sinkingProofB _ _ _ = todoSinkableProof -instance Color c => ProvesExt (RepeatedNameBinder c) where +instance ProvesExt RepeatedNameBinder where toExtEvidence (UnsafeRepeatedNameBinder _ b) = toExtEvidence b {-# INLINE toExtEvidence #-} -instance Color c => BindsNames (RepeatedNameBinder c) where +instance BindsNames RepeatedNameBinder where toScopeFrag (UnsafeRepeatedNameBinder _ b) = toScopeFrag b {-# INLINE toScopeFrag #-} -instance Color c => RenameB (RepeatedNameBinder c) where +instance RenameB RepeatedNameBinder where renameB env (UnsafeRepeatedNameBinder d b) cont = renameB env b \env' b' -> cont env' $ UnsafeRepeatedNameBinder d b' {-# INLINE renameB #-} -instance Color c => BindsAtMostOneName (RepeatedNameBinder c) c where +instance BindsAtMostOneName RepeatedNameBinder where (UnsafeRepeatedNameBinder _ b) @> v = b @> v {-# INLINE (@>) #-} -instance Color c => BindsOneName (RepeatedNameBinder c) c where +instance BindsOneName (RepeatedNameBinder) where binderName (UnsafeRepeatedNameBinder _ b) = binderName b {-# INLINE binderName #-} -instance HasNameHint (RepeatedNameBinder c n l) where +instance HasNameHint (RepeatedNameBinder n l) where getNameHint (UnsafeRepeatedNameBinder _ b) = getNameHint b {-# INLINE getNameHint #-} -data SubstPair (v::V) (o::S) (i::S) (i'::S) where - SubstPair :: Color c => {-# UNPACK #-} !(RepeatedNameBinder c i i') -> v c o -> SubstPair v o i i' +data SubstPair (v::E) (o::S) (i::S) (i'::S) where + SubstPair :: {-# UNPACK #-} !(RepeatedNameBinder i i') -> v o -> SubstPair v o i i' toSubstPairs :: forall v i i' o . SubstFrag v i i' o -> Nest (SubstPair v o) i i' toSubstPairs (UnsafeMakeSubst m) = - go $ R.toList m <&> \(rawName, item) -> - fromSubstItemPoly item \v -> - SubstPair (UnsafeRepeatedNameBinder (itemDistinctness item) (UnsafeMakeBinder rawName)) v + go $ R.toList m <&> \(rawName, item) -> do + let v = fromSubstItem item + SubstPair (UnsafeRepeatedNameBinder (itemDistinctness item) (UnsafeMakeBinder rawName)) v where go :: [SubstPair v o UnsafeS UnsafeS] -> Nest (SubstPair v o) i i' go [] = unsafeCoerceB Empty @@ -3054,19 +2749,19 @@ instance BindsNames (SubstPair v o) where -- === instances === -instance (forall c. Pretty (v c n)) => Pretty (SubstItem v n) where - pretty (SubstItem _ _ val) = pretty val +instance (forall c. Pretty (v n)) => Pretty (SubstItem v n) where + pretty (SubstItem _ val) = pretty val -instance SinkableV v => SinkableE (SubstFrag v i i') where +instance SinkableE v => SinkableE (SubstFrag v i i') where sinkingProofE fresh m = fmapSubstFrag (\(UnsafeMakeName _) v -> sinkingProofE fresh v) m -instance HoistableV v => HoistableE (SubstFrag v i i') where +instance HoistableE v => HoistableE (SubstFrag v i i') where freeVarsE frag = foldMapSubstFrag freeVarsE frag -instance RenameV v => RenameE (SubstFrag v i i') where +instance RenameE v => RenameE (SubstFrag v i i') where renameE env frag = fmapSubstFrag (\_ val -> renameE env val) frag -instance RenameV v => RenameE (Subst v i) where +instance RenameE v => RenameE (Subst v i) where renameE env = \case Subst f frag -> Subst (\n -> renameE env (f n)) $ renameE env frag UnsafeMakeIdentitySubst @@ -3085,10 +2780,6 @@ unsafeCoerceB :: forall (b::B) n l n' l' . b n l -> b n' l' unsafeCoerceB = TrulyUnsafe.unsafeCoerce {-# NOINLINE [1] unsafeCoerceB #-} -unsafeCoerceVC :: forall c' (v::V) c o. v c o -> v c' o -unsafeCoerceVC = TrulyUnsafe.unsafeCoerce -{-# NOINLINE [1] unsafeCoerceVC #-} - unsafeCoerceM1 :: forall (m::S -> * -> *) (n1::S) (n2::S) (a:: *). m n1 a -> m n2 a unsafeCoerceM1 = TrulyUnsafe.unsafeCoerce {-# NOINLINE [1] unsafeCoerceM1 #-} @@ -3130,9 +2821,9 @@ instance HoistableB b => HoistableB (RNest b) where freeVarsB REmpty = mempty freeVarsB (RNest rest b) = freeVarsB (PairB rest b) -instance (forall c n. Pretty (v c n)) => Pretty (SubstFrag v i i' o) where +instance (forall n. Pretty (v n)) => Pretty (SubstFrag v i i' o) where pretty (UnsafeMakeSubst m) = - vcat [ pretty v <+> "@>" <+> pretty x | (v, SubstItem _ _ x) <- R.toList m ] + vcat [ pretty v <+> "@>" <+> pretty x | (v, SubstItem _ x) <- R.toList m ] instance (Generic (b UnsafeS UnsafeS)) => Generic (Nest b n l) where type Rep (Nest b n l) = Rep [b UnsafeS UnsafeS] @@ -3150,31 +2841,19 @@ unsafeListToNest l = case l of [] -> unsafeCoerceB Empty b:rest -> Nest (unsafeCoerceB b) $ unsafeListToNest rest -instance (forall c. Color c => Store (v c n)) => Store (SubstItem v n) where - size = VarSize \item@(SubstItem d c _) -> - getSize (d, c) + fromSubstItemPoly item getSize - - peek = do - (d, c) <- peek - interpretColor c \(ColorProxy :: ColorProxy c) -> do - v :: v c n <- peek - return $ SubstItem d c (unsafeCoerceVC v) +instance Store (e n) => Store (SubstItem e n) - poke item@(SubstItem d c _) = do - poke (d, c) - fromSubstItemPoly item poke +data StoreNothingE (n::S) = StoreNothingE -data StoreNothingV (c::C) (n::S) = StoreNothingV - -instance Store (StoreNothingV c n) where +instance Store (StoreNothingE n) where size = ConstSize 0 - peek = return StoreNothingV + peek = return StoreNothingE poke = const $ return () -pokeableScopeFrag :: SubstFrag GHC.Exts.Any n l o -> SubstFrag StoreNothingV n l o +pokeableScopeFrag :: SubstFrag GHC.Exts.Any n l o -> SubstFrag StoreNothingE n l o pokeableScopeFrag = TrulyUnsafe.unsafeCoerce -fromPeekedScopeFrag :: SubstFrag StoreNothingV n l o -> SubstFrag GHC.Exts.Any n l o +fromPeekedScopeFrag :: SubstFrag StoreNothingE n l o -> SubstFrag GHC.Exts.Any n l o fromPeekedScopeFrag = TrulyUnsafe.unsafeCoerce instance Store (ScopeFrag n l) where @@ -3182,11 +2861,10 @@ instance Store (ScopeFrag n l) where peek = UnsafeScopeFromSubst . fromPeekedScopeFrag <$> peek poke (UnsafeScopeFromSubst s) = poke $ pokeableScopeFrag s -instance SinkableV v => SinkableE (SubstItem v) where +instance SinkableE v => SinkableE (SubstItem v) where sinkingProofE = todoSinkableProof -instance (forall c. Color c => Store (v c o)) - => Store (SubstFrag v i i' o) where +instance Store (v o) => Store (SubstFrag v i i' o) where instance ( Store (b UnsafeS UnsafeS) , Generic (b UnsafeS UnsafeS) ) => Store (Nest b n l) @@ -3260,13 +2938,13 @@ instance HoistableB b => HoistableB (WithAttrB a b) where -- the only names that are given meaning by the context of the term -- being traversed. -newtype NameMapE (c::C) (e:: E) (n::S) = UnsafeNameMapE (RawNameMap (e n)) +newtype NameMapE (e:: E) (n::S) = UnsafeNameMapE (RawNameMap (e n)) deriving (Eq, Semigroup, Monoid, Store) -- Filters out the entry(ies) for the binder being hoisted above, -- and hoists the values of the remaining entries. hoistNameMapE :: (BindsNames b, HoistableE e, ShowE e) - => b n l -> NameMapE c e l -> HoistExcept (NameMapE c e n) + => b n l -> NameMapE e l -> HoistExcept (NameMapE e n) hoistNameMapE b (UnsafeNameMapE raw) = UnsafeNameMapE <$> traverse (hoist b) diff where @@ -3274,81 +2952,72 @@ hoistNameMapE b (UnsafeNameMapE raw) = UnsafeMakeScopeFrag frag = toScopeFrag b {-# INLINE hoistNameMapE #-} -insertNameMapE :: Name c n -> e n -> NameMapE c e n -> NameMapE c e n +insertNameMapE :: Name n -> e n -> NameMapE e n -> NameMapE e n insertNameMapE (UnsafeMakeName n) x (UnsafeNameMapE raw) = UnsafeNameMapE $ R.insert n x raw {-# INLINE insertNameMapE #-} -lookupNameMapE :: Name c n -> NameMapE c e n -> Maybe (e n) +lookupNameMapE :: Name n -> NameMapE e n -> Maybe (e n) lookupNameMapE (UnsafeMakeName n) (UnsafeNameMapE raw) = R.lookup n raw {-# INLINE lookupNameMapE #-} -singletonNameMapE :: Name c n -> e n -> NameMapE c e n +singletonNameMapE :: Name n -> e n -> NameMapE e n singletonNameMapE (UnsafeMakeName n) x = UnsafeNameMapE $ R.singleton n x {-# INLINE singletonNameMapE #-} -toListNameMapE :: NameMapE c e n -> [(Name c n, (e n))] +toListNameMapE :: NameMapE e n -> [(Name n, (e n))] toListNameMapE (UnsafeNameMapE raw) = R.toList raw <&> \(r, x) -> (UnsafeMakeName r, x) {-# INLINE toListNameMapE #-} -unionWithNameMapE :: (e n -> e n -> e n) -> NameMapE c e n -> NameMapE c e n -> NameMapE c e n +unionWithNameMapE :: (e n -> e n -> e n) -> NameMapE e n -> NameMapE e n -> NameMapE e n unionWithNameMapE f (UnsafeNameMapE raw1) (UnsafeNameMapE raw2) = UnsafeNameMapE $ R.unionWith f raw1 raw2 {-# INLINE unionWithNameMapE #-} -unionsWithNameMapE :: (Foldable f) => (e n -> e n -> e n) -> f (NameMapE c e n) -> NameMapE c e n +unionsWithNameMapE :: (Foldable f) => (e n -> e n -> e n) -> f (NameMapE e n) -> NameMapE e n unionsWithNameMapE func maps = foldl' (unionWithNameMapE func) mempty maps {-# INLINE unionsWithNameMapE #-} -traverseNameMapE :: (Applicative f) => (e1 n -> f (e2 n)) - -> NameMapE c e1 n -> f (NameMapE c e2 n) +traverseNameMapE :: (Applicative f) => (e1 n -> f (e2 n)) -> NameMapE e1 n -> f (NameMapE e2 n) traverseNameMapE f (UnsafeNameMapE raw) = UnsafeNameMapE <$> traverse f raw {-# INLINE traverseNameMapE #-} -mapNameMapE :: (e1 n -> e2 n) - -> NameMapE c e1 n -> NameMapE c e2 n +mapNameMapE :: (e1 n -> e2 n) -> NameMapE e1 n -> NameMapE e2 n mapNameMapE f (UnsafeNameMapE raw) = UnsafeNameMapE $ fmap f raw {-# INLINE mapNameMapE #-} -keysNameMapE :: NameMapE c e n -> [Name c n] +keysNameMapE :: NameMapE e n -> [Name n] keysNameMapE = map fst . toListNameMapE {-# INLINE keysNameMapE #-} -keySetNameMapE :: (Color c) => NameMapE c e n -> NameSet n +keySetNameMapE :: NameMapE e n -> NameSet n keySetNameMapE nmap = freeVarsE $ ListE $ keysNameMapE nmap -instance SinkableE e => SinkableE (NameMapE c e) where +instance SinkableE e => SinkableE (NameMapE e) where sinkingProofE = undefined -instance RenameE e => RenameE (NameMapE c e) where +instance RenameE e => RenameE (NameMapE e) where renameE = undefined -instance HoistableE e => HoistableE (NameMapE c e) where +instance HoistableE e => HoistableE (NameMapE e) where freeVarsE = undefined -- A small short-cut: When the information in a NameMapE does not, in -- fact, reference any names, hoisting the entries cannot fail. -type NameMap (c::C) (a:: *) = NameMapE c (LiftE a) +type NameMap (a:: *) = NameMapE (LiftE a) -hoistNameMap :: (BindsNames b, Show a) - => b n l -> NameMap c a l -> (NameMap c a n) +hoistNameMap :: (BindsNames b, Show a) => b n l -> NameMap a l -> (NameMap a n) hoistNameMap b = ignoreHoistFailure . hoistNameMapE b {-# INLINE hoistNameMap #-} --- === E-kinded IR coercions === - --- XXX: the intention is that we won't have to use this much -unsafeCoerceIRE :: forall (r'::IR) (r::IR) (e::IR->E) (n::S). e r n -> e r' n -unsafeCoerceIRE = TrulyUnsafe.unsafeCoerce - -- === Pretty instances === -instance PrettyPrec (Name s n) where prettyPrec = atPrec ArgPrec . pretty +instance PrettyPrec (Name n) where prettyPrec = atPrec ArgPrec . pretty -instance PrettyE ann => Pretty (BinderP c ann n l) +instance PrettyE ann => Pretty (BinderP ann n l) where pretty (b:>ty) = pretty b <> ":" <> pretty ty -- === notes === diff --git a/src/lib/QueryType.hs b/src/lib/QueryType.hs index bbed09e24..2acf3e66f 100644 --- a/src/lib/QueryType.hs +++ b/src/lib/QueryType.hs @@ -27,7 +27,6 @@ import PPrint import QueryTypePure import CheapReduction - -- === Exposed helpers for querying types and effects === caseAltsBinderTys :: (EnvReader m, IRRep r) => Type r n -> m n [Type r n] diff --git a/src/lib/QueryTypePure.hs b/src/lib/QueryTypePure.hs index d133a094c..88901a613 100644 --- a/src/lib/QueryTypePure.hs +++ b/src/lib/QueryTypePure.hs @@ -9,7 +9,6 @@ module QueryTypePure where import Types.Primitives import Types.Core import Types.Top -import IRVariants import Name class HasType (r::IR) (e::E) | e -> r where diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs index 16e484de5..7598f9d99 100644 --- a/src/lib/SourceRename.hs +++ b/src/lib/SourceRename.hs @@ -22,7 +22,6 @@ import Core (EnvReader (..), withEnv, lookupSourceMapPure) import MonadUtil import MTL1 import PPrint -import IRVariants import Types.Source import Types.Primitives import Types.Top (Env (..), ModuleEnv (..)) @@ -366,7 +365,7 @@ class SourceRenamablePat (pat::B) where -> (forall o'. DExt o o' => SiblingSet -> pat o o' -> m o' a) -> m o a -instance SourceRenamablePat (UBinder (AtomNameC CoreIR)) where +instance SourceRenamablePat UBinder where sourceRenamePat sibs (WithSrcB sid ubinder) cont = do newSibs <- case ubinder of UBindSource b -> do diff --git a/src/lib/Types/Core.hs b/src/lib/Types/Core.hs index cbb539ee4..e7b5a1f84 100644 --- a/src/lib/Types/Core.hs +++ b/src/lib/Types/Core.hs @@ -24,7 +24,6 @@ import Data.Store (Store (..)) import Name import Util (Tree (..)) -import IRVariants import PPrint import Types.Primitives @@ -33,120 +32,114 @@ import Types.Imp -- === core IR === -data Atom (r::IR) (n::S) where - Con :: Con r n -> Atom r n - Stuck :: Type r n -> Stuck r n -> Atom r n - deriving (Show, Generic) +data Atom (n::S) = + Con (Con n) + | Stuck (Type n) (Stuck n) + deriving (Show, Generic) -data Type (r::IR) (n::S) where - TyCon :: TyCon r n -> Type r n - StuckTy :: Kind -> CStuck n -> Type CoreIR n +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 (r::IR) (n::S) where - DictCon :: DictCon r n -> Dict r n - StuckDict :: CType n -> CStuck n -> Dict CoreIR n - -data Con (r::IR) (n::S) where - Lit :: LitVal -> Con r n - ProdCon :: [Atom r n] -> Con r n - SumCon :: [Type r n] -> Int -> Atom r n -> Con r n -- type, tag, payload - DepPair :: Atom r n -> Atom r n -> DepPairType r n -> Con r n - Lam :: CoreLamExpr n -> Con CoreIR n - NewtypeCon :: NewtypeCon n -> Atom CoreIR n -> Con CoreIR n - DictConAtom :: DictCon CoreIR n -> Con CoreIR n - TyConAtom :: TyCon CoreIR n -> Con CoreIR n - -data Stuck (r::IR) (n::S) where - Var :: AtomVar r n -> Stuck r n - StuckProject :: Int -> Stuck r n -> Stuck r n - StuckTabApp :: Stuck r n -> Atom r n -> Stuck r n - PtrVar :: PtrType -> PtrName n -> Stuck r n - RepValAtom :: RepVal r n -> Stuck r n - StuckUnwrap :: CStuck n -> Stuck CoreIR n - InstantiatedGiven :: CStuck n -> [CAtom n] -> Stuck CoreIR n - SuperclassProj :: Int -> CStuck n -> Stuck CoreIR n - -data TyCon (r::IR) (n::S) where - BaseType :: BaseType -> TyCon r n - ProdType :: [Type r n] -> TyCon r n - SumType :: [Type r n] -> TyCon r n - RefType :: Type r n -> TyCon r n - TabPi :: TabPiType r n -> TyCon r n - DepPairTy :: DepPairType r n -> TyCon r n - DictTy :: DictType n -> TyCon CoreIR n - Pi :: CorePiType n -> TyCon CoreIR n - NewtypeTyCon :: NewtypeTyCon n -> TyCon CoreIR n - Kind :: Kind -> TyCon CoreIR n - -data AtomVar (r::IR) (n::S) = AtomVar - { atomVarName :: AtomName r n - , atomVarType :: Type r n } +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 IRRep r => Show (DictCon r n) -deriving instance IRRep r => Show (Dict r n) -deriving instance IRRep r => Show (Con r n) -deriving instance IRRep r => Show (TyCon r n) -deriving instance IRRep r => Show (Type r n) -deriving instance IRRep r => Show (Stuck r n) - -deriving via WrapE (DictCon r) n instance IRRep r => Generic (DictCon r n) -deriving via WrapE (Dict r) n instance IRRep r => Generic (Dict r n) -deriving via WrapE (Con r) n instance IRRep r => Generic (Con r n) -deriving via WrapE (TyCon r) n instance IRRep r => Generic (TyCon r n) -deriving via WrapE (Type r) n instance IRRep r => Generic (Type r n) -deriving via WrapE (Stuck r) n instance IRRep r => Generic (Stuck r n) - -data Expr r n where - Block :: EffTy r n -> Block r n -> Expr r n - TopApp :: EffTy SimpIR n -> TopFunName n -> [SAtom n] -> Expr SimpIR n - TabApp :: Type r n -> Atom r n -> Atom r n -> Expr r n - Case :: Atom r n -> [Alt r n] -> EffTy r n -> Expr r n - Atom :: Atom r n -> Expr r n - TabCon :: Type r n -> [Atom r n] -> Expr r n - PrimOp :: Type r n -> PrimOp r (Atom r n) -> Expr r n - Hof :: TypedHof r n -> Expr r n - Project :: Type r n -> Int -> Atom r n -> Expr r n - App :: EffTy CoreIR n -> CAtom n -> [CAtom n] -> Expr CoreIR n - Unwrap :: CType n -> CAtom n -> Expr CoreIR n - ApplyMethod :: EffTy CoreIR n -> CAtom n -> Int -> [CAtom n] -> Expr CoreIR n - -deriving instance IRRep r => Show (Expr r n) -deriving via WrapE (Expr r) n instance IRRep r => Generic (Expr r n) - -data RepVal (r::IR) (n::S) = RepVal (Type r n) (Tree (IExpr n)) +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 r n = DeclBinding LetAnn (Expr r n) +data DeclBinding n = DeclBinding LetAnn (Expr n) deriving (Show, Generic) -data Decl (r::IR) (n::S) (l::S) = Let (AtomNameBinder r n l) (DeclBinding r n) +data Decl (n::S) (l::S) = Let (AtomNameBinder n l) (DeclBinding n) deriving (Show, Generic) -type Decls r = Nest (Decl r) - --- TODO: make this a newtype with an unsafe constructor The idea is that the `r` --- parameter will play a role a bit like the `c` parameter in names: if you have --- an `AtomName r n` and you look up its definition in the `Env`, you're sure to --- get an `AtomBinding r n`. -type AtomName (r::IR) = Name (AtomNameC r) -type AtomNameBinder (r::IR) = NameBinder (AtomNameC r) - -type ClassName = Name ClassNameC -type TyConName = Name TyConNameC -type DataConName = Name DataConNameC -type InstanceName = Name InstanceNameC -type MethodName = Name MethodNameC -type ModuleName = Name ModuleNameC -type PtrName = Name PtrNameC -type SpecDictName = Name SpecializedDictNameC -type TopFunName = Name TopFunNameC -type FunObjCodeName = Name FunObjCodeNameC - -type AtomBinderP (r::IR) = BinderP (AtomNameC r) -type Binder r = AtomBinderP r (Type r) :: B -type Alt r = Abs (Binder r) (Expr r) :: E +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) @@ -174,80 +167,80 @@ data DataConDef n = -- 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 CoreIR n] +data TyConParams n = TyConParams [Explicitness] [Atom n] deriving (Show, Generic) -type WithDecls (r::IR) = Abs (Decls r) :: E -> E -type Block (r::IR) = WithDecls r (Expr r) :: E +type WithDecls = Abs Decls :: E -> E +type Block = WithDecls Expr :: E -data LamExpr (r::IR) (n::S) where - LamExpr :: Nest (Binder r) n l -> Expr r l -> LamExpr r n +data LamExpr (n::S) where + LamExpr :: Nest Binder n l -> Expr l -> LamExpr n -data CoreLamExpr (n::S) = CoreLamExpr (CorePiType n) (LamExpr CoreIR n) deriving (Show, Generic) +data CoreLamExpr (n::S) = CoreLamExpr (CorePiType n) (LamExpr n) deriving (Show, Generic) -type TabLamExpr = PairE (TabPiType CoreIR) (Abs SBinder CAtom) +type TabLamExpr = PairE TabPiType (Abs SBinder CAtom) type IxDict = Dict data IxMethod = Size | Ordinal | UnsafeFromOrdinal deriving (Show, Generic, Enum, Bounded, Eq) -data IxType (r::IR) (n::S) = - IxType { ixTypeType :: Type r n - , ixTypeDict :: IxDict r n } +data IxType (n::S) = + IxType { ixTypeType :: Type n + , ixTypeDict :: IxDict n } deriving (Show, Generic) -data TabPiType (r::IR) (n::S) where - TabPiType :: IxDict r n -> Binder r n l -> Type r l -> TabPiType r n +data TabPiType (n::S) where + TabPiType :: IxDict n -> Binder n l -> Type l -> TabPiType n -data PiType (r::IR) (n::S) where - PiType :: Nest (Binder r) n l -> Type r l -> PiType r 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 (r::IR) (n::S) where - DepPairType :: DepPairExplicitness -> Binder r n l -> Type r l -> DepPairType r 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 r ann n l = NonDepNest (Nest (AtomNameBinder r) n l) [ann n] +data NonDepNest ann n l = NonDepNest (Nest AtomNameBinder n l) [ann n] deriving (Generic) -- === ToAtomAbs class === -class ToBindersAbs (e::E) (body::E) (r::IR) | e -> body, e -> r where - toAbs :: e n -> Abs (Nest (Binder r)) body n +class ToBindersAbs (e::E) (body::E) | e -> body where + toAbs :: e n -> Abs (Nest Binder) body n -instance ToBindersAbs CorePiType (Type CoreIR) CoreIR where +instance ToBindersAbs CorePiType Type where toAbs (CorePiType _ _ bs ty) = Abs bs ty -instance ToBindersAbs CoreLamExpr (Expr CoreIR) CoreIR where +instance ToBindersAbs CoreLamExpr Expr where toAbs (CoreLamExpr _ lam) = toAbs lam -instance ToBindersAbs (Abs (Nest (Binder r)) body) body r where +instance ToBindersAbs (Abs (Nest Binder) body) body where toAbs = id -instance ToBindersAbs (PiType r) (Type r) r where +instance ToBindersAbs PiType Type where toAbs (PiType bs ty) = Abs bs ty -instance ToBindersAbs (LamExpr r) (Expr r) r where +instance ToBindersAbs LamExpr Expr where toAbs (LamExpr bs body) = Abs bs body -instance ToBindersAbs (TabPiType r) (Type r) r where +instance ToBindersAbs TabPiType Type where toAbs (TabPiType _ b eltTy) = Abs (UnaryNest b) eltTy -instance ToBindersAbs (DepPairType r) (Type r) r where +instance ToBindersAbs DepPairType Type where toAbs (DepPairType _ b rhsTy) = Abs (UnaryNest b) rhsTy -instance ToBindersAbs InstanceDef (ListE CAtom `PairE` InstanceBody) CoreIR where +instance ToBindersAbs InstanceDef (ListE CAtom `PairE` InstanceBody) where toAbs (InstanceDef _ _ bs params body) = Abs bs (ListE params `PairE` body) -instance ToBindersAbs TyConDef DataConDefs CoreIR where +instance ToBindersAbs TyConDef DataConDefs where toAbs (TyConDef _ _ bs body) = Abs bs body -instance ToBindersAbs ClassDef (Abs (Nest CBinder) (ListE CorePiType)) CoreIR where +instance ToBindersAbs ClassDef (Abs (Nest CBinder) (ListE CorePiType)) where toAbs (ClassDef _ _ _ _ _ bs scBs tys) = Abs bs (Abs scBs (ListE tys)) showStringBufferSize :: Word32 @@ -255,45 +248,43 @@ showStringBufferSize = 32 -- === Hofs === -data TypedHof r n = TypedHof (EffTy r n) (Hof r n) +data TypedHof n = TypedHof (EffTy n) (Hof n) deriving (Show, Generic) -data Hof r n where - For :: ForAnn -> IxType r n -> LamExpr r n -> Hof r n - While :: Expr r n -> Hof r n - Linearize :: LamExpr CoreIR n -> Atom CoreIR n -> Hof CoreIR n - Transpose :: LamExpr CoreIR n -> Atom CoreIR n -> Hof CoreIR n - -deriving instance IRRep r => Show (Hof r n) -deriving via WrapE (Hof r) n instance IRRep r => Generic (Hof r n) +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 CoreIR -type CType = Type CoreIR -type CDict = Dict CoreIR -type CStuck = Stuck CoreIR -type CBinder = Binder CoreIR -type CExpr = Expr CoreIR -type CBlock = Block CoreIR -type CDecl = Decl CoreIR -type CDecls = Decls CoreIR -type CAtomName = AtomName CoreIR -type CAtomVar = AtomVar CoreIR - -type SAtom = Atom SimpIR -type SType = Type SimpIR -type SDict = Dict SimpIR -type SStuck = Stuck SimpIR -type SExpr = Expr SimpIR -type SBlock = Block SimpIR -type SAlt = Alt SimpIR -type SDecl = Decl SimpIR -type SDecls = Decls SimpIR -type SAtomName = AtomName SimpIR -type SAtomVar = AtomVar SimpIR -type SBinder = Binder SimpIR -type SLam = LamExpr SimpIR +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 === @@ -301,12 +292,12 @@ type SLam = LamExpr SimpIR data NewtypeCon (n::S) = UserADTData SourceName (TyConName n) (TyConParams n) -- source name is for the type | NatCon - | FinCon (Atom CoreIR n) + | FinCon (Atom n) deriving (Show, Generic) data NewtypeTyCon (n::S) = Nat - | Fin (Atom CoreIR n) + | Fin (Atom n) | UserADTType SourceName (TyConName n) (TyConParams n) deriving (Show, Generic) @@ -351,40 +342,39 @@ data DictType (n::S) = | IxDictType (CType n) deriving (Show, Generic) -data DictCon (r::IR) (n::S) where - InstanceDict :: CType n -> InstanceName n -> [CAtom n] -> DictCon CoreIR n - IxFin :: CAtom n -> DictCon CoreIR n +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 SimpIR-only - IxRawFin :: Atom r n -> DictCon r n - IxSpecialized :: SpecDictName n -> [SAtom n] -> DictCon SimpIR n + -- TODO: make is-only + IxRawFin :: Atom n -> DictCon n + IxSpecialized :: SpecDictName n -> [SAtom n] -> DictCon n -data Effects (r::IR) (n::S) = Pure | Effectful +data Effects (n::S) = Pure | Effectful deriving (Generic, Show) -instance Semigroup (Effects r n) where +instance Semigroup (Effects n) where Pure <> Pure = Pure _ <> _ = Effectful -instance Monoid (Effects r n) where +instance Monoid (Effects n) where mempty = Pure -data EffTy (r::IR) (n::S) = - EffTy { etEff :: Effects r n - , etTy :: Type r n } +data EffTy (n::S) = + EffTy { etEff :: Effects n + , etTy :: Type n } deriving (Generic, Show) -- === Binder utils === -binderType :: Binder r n l -> Type r n +binderType :: Binder n l -> Type n binderType (_:>ty) = ty -binderVar :: (IRRep r, DExt n l) => Binder r n l -> AtomVar r l +binderVar :: (DExt n l) => Binder n l -> AtomVar l binderVar (b:>ty) = AtomVar (binderName b) (sink ty) -bindersVars :: (Distinct l, Ext n l, IRRep r) - => Nest (Binder r) n l -> [AtomVar r l] +bindersVars :: (Distinct l, Ext n l) => Nest Binder n l -> [AtomVar l] bindersVars = \case Empty -> [] Nest b bs -> withExtEvidence b $ withSubscopeDistinct bs $ @@ -392,45 +382,45 @@ bindersVars = \case -- === ToAtom === -class ToAtom (e::E) (r::IR) | e -> r where - toAtom :: e n -> Atom r n - -instance ToAtom (Atom r) r where toAtom = id -instance ToAtom (Con r) r where toAtom = Con -instance ToAtom (TyCon CoreIR) CoreIR where toAtom = Con . TyConAtom -instance ToAtom (DictCon CoreIR) CoreIR where toAtom = Con . DictConAtom -instance ToAtom CoreLamExpr CoreIR where toAtom = Con . Lam -instance ToAtom DictType CoreIR where toAtom = Con . TyConAtom . DictTy -instance ToAtom NewtypeTyCon CoreIR where toAtom = Con . TyConAtom . NewtypeTyCon -instance ToAtom (AtomVar r) r where +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 IRRep r => ToAtom (RepVal r) r where +instance ToAtom RepVal where toAtom (RepVal ty tree) = Stuck ty $ RepValAtom $ RepVal ty tree -instance ToAtom (Type CoreIR) CoreIR where +instance ToAtom (Type) where toAtom = \case TyCon con -> Con $ TyConAtom con StuckTy k s -> Stuck (TyCon $ Kind k) s -instance ToAtom (Dict CoreIR) CoreIR where +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 r) r => e r n -> Atom r n +toAtomR :: ToAtom e => e n -> Atom n toAtomR = toAtom -- === ToType === -class ToType (e::E) (r::IR) | e -> r where - toType :: e n -> Type r n +class ToType (e::E) where + toType :: e n -> Type n -instance ToType (Type r) r where toType = id -instance ToType (TyCon r) r where toType = TyCon -instance ToType (TabPiType r) r where toType = TyCon . TabPi -instance ToType (DepPairType r) r where toType = TyCon . DepPairTy -instance ToType CorePiType CoreIR where toType = TyCon . Pi -instance ToType DictType CoreIR where toType = TyCon . DictTy -instance ToType NewtypeTyCon CoreIR where toType = TyCon . NewtypeTyCon +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 @@ -440,12 +430,12 @@ toMaybeType = \case -- === ToDict === -class ToDict (e::E) (r::IR) | e -> r where - toDict :: e n -> Dict r n +class ToDict (e::E) where + toDict :: e n -> Dict n -instance ToDict (Dict r) r where toDict = id -instance ToDict (DictCon r) r where toDict = DictCon -instance ToDict CAtomVar CoreIR where +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) @@ -460,10 +450,10 @@ pattern IdxRepScalarBaseTy :: ScalarBaseType pattern IdxRepScalarBaseTy = Word32Type -- Type used to represent indices and sizes at run-time -pattern IdxRepTy :: Type r n +pattern IdxRepTy :: Type n pattern IdxRepTy = TyCon (BaseType (Scalar Word32Type)) -pattern IdxRepVal :: Word32 -> Atom r n +pattern IdxRepVal :: Word32 -> Atom n pattern IdxRepVal x = Con (Lit (Word32Lit x)) pattern IIdxRepVal :: Word32 -> IExpr n @@ -473,96 +463,96 @@ pattern IIdxRepTy :: IType pattern IIdxRepTy = Scalar Word32Type -- Type used to represent sum type tags at run-time -pattern TagRepTy :: Type r n +pattern TagRepTy :: Type n pattern TagRepTy = TyCon (BaseType (Scalar Word8Type)) -pattern TagRepVal :: Word8 -> Atom r n +pattern TagRepVal :: Word8 -> Atom n pattern TagRepVal x = Con (Lit (Word8Lit x)) -pattern CharRepTy :: Type r n +pattern CharRepTy :: Type n pattern CharRepTy = Word8Ty -charRepVal :: Char -> Atom r n +charRepVal :: Char -> Atom n charRepVal c = Con (Lit (Word8Lit (fromIntegral $ fromEnum c))) -pattern Word8Ty :: Type r n +pattern Word8Ty :: Type n pattern Word8Ty = TyCon (BaseType (Scalar Word8Type)) -pattern PairVal :: Atom r n -> Atom r n -> Atom r n +pattern PairVal :: Atom n -> Atom n -> Atom n pattern PairVal x y = Con (ProdCon [x, y]) -pattern PairTy :: Type r n -> Type r n -> Type r n +pattern PairTy :: Type n -> Type n -> Type n pattern PairTy x y = TyCon (ProdType [x, y]) -pattern UnitVal :: Atom r n +pattern UnitVal :: Atom n pattern UnitVal = Con (ProdCon []) -pattern UnitTy :: Type r n +pattern UnitTy :: Type n pattern UnitTy = TyCon (ProdType []) -pattern BaseTy :: BaseType -> Type r n +pattern BaseTy :: BaseType -> Type n pattern BaseTy b = TyCon (BaseType b) -pattern PtrTy :: PtrType -> Type r n +pattern PtrTy :: PtrType -> Type n pattern PtrTy ty = TyCon (BaseType (PtrType ty)) -pattern RefTy :: Type r n -> Type r n +pattern RefTy :: Type n -> Type n pattern RefTy a = TyCon (RefType a) -pattern TabTy :: IxDict r n -> Binder r n l -> Type r l -> Type r n +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 CoreIR n -> Type CoreIR n +pattern FinTy :: Atom n -> Type n pattern FinTy n = TyCon (NewtypeTyCon (Fin n)) -pattern NatTy :: Type CoreIR n +pattern NatTy :: Type n pattern NatTy = TyCon (NewtypeTyCon Nat) -pattern NatVal :: Word32 -> Atom CoreIR n +pattern NatVal :: Word32 -> Atom n pattern NatVal n = Con (NewtypeCon NatCon (IdxRepVal n)) -pattern FinConst :: Word32 -> Type CoreIR n +pattern FinConst :: Word32 -> Type n pattern FinConst n = TyCon (NewtypeTyCon (Fin (NatVal n))) -pattern NullaryLamExpr :: Expr r n -> LamExpr r n +pattern NullaryLamExpr :: Expr n -> LamExpr n pattern NullaryLamExpr body = LamExpr Empty body -pattern UnaryLamExpr :: Binder r n l -> Expr r l -> LamExpr r n +pattern UnaryLamExpr :: Binder n l -> Expr l -> LamExpr n pattern UnaryLamExpr b body = LamExpr (UnaryNest b) body -pattern BinaryLamExpr :: Binder r n l1 -> Binder r l1 l2 -> Expr r l2 -> LamExpr r n +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 r n -> Type r n +pattern MaybeTy :: Type n -> Type n pattern MaybeTy a = TyCon (SumType [UnitTy, a]) -pattern NothingAtom :: Type r n -> Atom r n +pattern NothingAtom :: Type n -> Atom n pattern NothingAtom a = Con (SumCon [UnitTy, a] 0 UnitVal) -pattern JustAtom :: Type r n -> Atom r n -> Atom r n +pattern JustAtom :: Type n -> Atom n -> Atom n pattern JustAtom a x = Con (SumCon [UnitTy, a] 1 x) -pattern BoolTy :: Type r n +pattern BoolTy :: Type n pattern BoolTy = Word8Ty -pattern FalseAtom :: Atom r n +pattern FalseAtom :: Atom n pattern FalseAtom = Con (Lit (Word8Lit 0)) -pattern TrueAtom :: Atom r n +pattern TrueAtom :: Atom n pattern TrueAtom = Con (Lit (Word8Lit 1)) -- === Typeclass instances for Name and other Haskell libraries === -instance IRRep r => GenericE (RepVal r) where - type RepE (RepVal r) = PairE (Type r) (ComposeE Tree IExpr) +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 IRRep r => SinkableE (RepVal r) -instance IRRep r => RenameE (RepVal r) -instance IRRep r => HoistableE (RepVal r) -instance IRRep r => AlphaHashableE (RepVal r) -instance IRRep r => AlphaEqE (RepVal r) +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) @@ -630,7 +620,7 @@ instance HasSourceName (TyConDef n) where instance GenericE DataConDef where type RepE DataConDef = (LiftE (SourceName, [[Projection]])) - `PairE` EmptyAbs (Nest CBinder) `PairE` Type CoreIR + `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 @@ -691,48 +681,48 @@ instance AlphaEqE NewtypeTyCon instance AlphaHashableE NewtypeTyCon instance RenameE NewtypeTyCon -instance IRRep r => GenericE (TypedHof r) where - type RepE (TypedHof r) = EffTy r `PairE` Hof r +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 IRRep r => SinkableE (TypedHof r) -instance IRRep r => HoistableE (TypedHof r) -instance IRRep r => RenameE (TypedHof r) -instance IRRep r => AlphaEqE (TypedHof r) -instance IRRep r => AlphaHashableE (TypedHof r) +instance SinkableE TypedHof +instance HoistableE TypedHof +instance RenameE TypedHof +instance AlphaEqE TypedHof +instance AlphaHashableE TypedHof -instance IRRep r => GenericE (Hof r) where - type RepE (Hof r) = EitherE4 - {- For -} (LiftE ForAnn `PairE` IxType r `PairE` LamExpr r) - {- While -} (Expr r) - {- Linearize -} (WhenCore r (LamExpr r `PairE` Atom r)) - {- Transpose -} (WhenCore r (LamExpr r `PairE` Atom r)) +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 (WhenIRE (PairE body x)) - Transpose body x -> Case3 (WhenIRE (PairE body x)) + 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 (WhenIRE (PairE body x)) -> Linearize body x - Case3 (WhenIRE (PairE body x)) -> Transpose body x + Case2 (PairE body x) -> Linearize body x + Case3 (PairE body x) -> Transpose body x _ -> error "impossible" {-# INLINE toE #-} -instance IRRep r => SinkableE (Hof r) -instance IRRep r => HoistableE (Hof r) -instance IRRep r => RenameE (Hof r) -instance IRRep r => AlphaEqE (Hof r) -instance IRRep r => AlphaHashableE (Hof r) +instance SinkableE Hof +instance HoistableE Hof +instance RenameE Hof +instance AlphaEqE Hof +instance AlphaHashableE Hof -instance IRRep r => GenericE (Atom r) where - type RepE (Atom r) = EitherE (PairE (Type r) (Stuck r)) (Con r) +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 @@ -742,180 +732,180 @@ instance IRRep r => GenericE (Atom r) where RightE x -> Con x {-# INLINE toE #-} -instance IRRep r => SinkableE (Atom r) -instance IRRep r => HoistableE (Atom r) -instance IRRep r => AlphaEqE (Atom r) -instance IRRep r => AlphaHashableE (Atom r) -instance IRRep r => RenameE (Atom r) +instance SinkableE Atom +instance HoistableE Atom +instance AlphaEqE Atom +instance AlphaHashableE Atom +instance RenameE Atom -instance IRRep r => GenericE (Stuck r) where - type RepE (Stuck r) = EitherE2 +instance GenericE Stuck where + type RepE Stuck = EitherE2 (EitherE6 - {- Var -} (AtomVar r) - {- StuckProject -} (LiftE Int `PairE` Stuck r) - {- StuckTabApp -} (Stuck r `PairE` Atom r) - {- StuckUnwrap -} (WhenCore r (CStuck)) - {- InstantiatedGiven -} (WhenCore r (CStuck `PairE` ListE CAtom)) - {- SuperclassProj -} (WhenCore r (LiftE Int `PairE` CStuck)) - ) (EitherE2 + {- 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 r) + {- 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 $ WhenIRE $ e - InstantiatedGiven e xs -> Case0 $ Case4 $ WhenIRE $ e `PairE` ListE xs - SuperclassProj i e -> Case0 $ Case5 $ WhenIRE $ LiftE i `PairE` e - PtrVar t p -> Case1 $ Case0 $ LiftE t `PairE` p - RepValAtom r -> Case1 $ Case1 $ r + 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 (WhenIRE e) -> StuckUnwrap e - Case4 (WhenIRE (e `PairE` ListE xs)) -> InstantiatedGiven e xs - Case5 (WhenIRE (LiftE i `PairE` e)) -> SuperclassProj i e + 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 + Case0 (LiftE t `PairE` p) -> PtrVar t p + Case1 r -> RepValAtom r _ -> error "impossible" _ -> error "impossible" {-# INLINE toE #-} -instance IRRep r => SinkableE (Stuck r) -instance IRRep r => HoistableE (Stuck r) -instance IRRep r => AlphaEqE (Stuck r) -instance IRRep r => AlphaHashableE (Stuck r) -instance IRRep r => RenameE (Stuck r) +instance SinkableE Stuck +instance HoistableE Stuck +instance AlphaEqE Stuck +instance AlphaHashableE Stuck +instance RenameE Stuck -instance IRRep r => GenericE (AtomVar r) where - type RepE (AtomVar r) = PairE (AtomName r) (Type r) +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 r n) where +instance HasNameHint (AtomVar n) where getNameHint (AtomVar v _) = getNameHint v -instance Eq (AtomVar r n) where +instance Eq (AtomVar n) where AtomVar v1 _ == AtomVar v2 _ = v1 == v2 -instance IRRep r => SinkableE (AtomVar r) -instance IRRep r => HoistableE (AtomVar r) +instance SinkableE AtomVar +instance HoistableE AtomVar -- We ignore the type annotation because it should be determined by the var -instance IRRep r => AlphaEqE (AtomVar r) where +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 IRRep r => AlphaHashableE (AtomVar r) where +instance AlphaHashableE AtomVar where hashWithSaltE env salt (AtomVar v _) = hashWithSaltE env salt v -instance IRRep r => RenameE (AtomVar r) +instance RenameE AtomVar -instance IRRep r => GenericE (Type r) where - type RepE (Type r) = EitherE (WhenCore r (PairE (LiftE Kind) (Stuck r))) (TyCon r) +instance GenericE Type where + type RepE Type = EitherE (PairE (LiftE Kind) Stuck ) TyCon fromE = \case - StuckTy k x -> LeftE (WhenIRE (PairE (LiftE k) x)) + StuckTy k x -> LeftE (PairE (LiftE k) x) TyCon x -> RightE x {-# INLINE fromE #-} toE = \case - LeftE (WhenIRE (PairE (LiftE k) x)) -> StuckTy k x + LeftE (PairE (LiftE k) x) -> StuckTy k x RightE x -> TyCon x {-# INLINE toE #-} -instance IRRep r => SinkableE (Type r) -instance IRRep r => HoistableE (Type r) -instance IRRep r => AlphaEqE (Type r) -instance IRRep r => AlphaHashableE (Type r) -instance IRRep r => RenameE (Type r) +instance SinkableE Type +instance HoistableE Type +instance AlphaEqE Type +instance AlphaHashableE Type +instance RenameE Type -instance IRRep r => GenericE (Expr r) where - type RepE (Expr r) = EitherE2 +instance GenericE Expr where + type RepE Expr = EitherE2 ( EitherE6 - {- App -} (WhenCore r (EffTy r `PairE` Atom r `PairE` ListE (Atom r))) - {- TabApp -} (Type r `PairE` Atom r `PairE` Atom r) - {- Case -} (Atom r `PairE` ListE (Alt r) `PairE` EffTy r) - {- Atom -} (Atom r) - {- TopApp -} (WhenSimp r (EffTy r `PairE` TopFunName `PairE` ListE (Atom r))) - {- Block -} (EffTy r `PairE` Block r) + {- 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 r `PairE` ListE (Atom r)) - {- PrimOp -} (Type r `PairE` ComposeE (PrimOp r) (Atom r)) - {- ApplyMethod -} (WhenCore r (EffTy r `PairE` Atom r `PairE` LiftE Int `PairE` ListE (Atom r))) - {- Project -} (Type r `PairE` LiftE Int `PairE` Atom r) - {- Unwrap -} (WhenCore r (CType `PairE` CAtom)) - {- Hof -} (TypedHof r)) + {- 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 (WhenIRE (et `PairE` f `PairE` ListE xs)) + 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 (WhenIRE (et `PairE` f `PairE` ListE xs)) + 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 (WhenIRE (et `PairE` d `PairE` LiftE i `PairE` ListE xs)) + 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 (WhenIRE (t `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 (WhenIRE (et `PairE` f `PairE` ListE xs)) -> App et f xs + 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 (WhenIRE (et `PairE` f `PairE` ListE xs)) -> TopApp et f xs + 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 (WhenIRE (et `PairE` d `PairE` LiftE i `PairE` ListE xs)) -> ApplyMethod et d i xs + 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 (WhenIRE (t `PairE` x)) -> Unwrap t x + Case4 (t `PairE` x) -> Unwrap t x Case5 hof -> Hof hof _ -> error "impossible" _ -> error "impossible" {-# INLINE toE #-} -instance IRRep r => SinkableE (Expr r) -instance IRRep r => HoistableE (Expr r) -instance IRRep r => AlphaEqE (Expr r) -instance IRRep r => AlphaHashableE (Expr r) -instance IRRep r => RenameE (Expr r) +instance SinkableE Expr +instance HoistableE Expr +instance AlphaEqE Expr +instance AlphaHashableE Expr +instance RenameE Expr -instance IRRep r => GenericE (Con r) where - type RepE (Con r) = EitherE2 +instance GenericE Con where + type RepE Con = EitherE2 (EitherE4 {- Lit -} (LiftE LitVal) - {- ProdCon -} (ListE (Atom r)) - {- SumCon -} (ListE (Type r) `PairE` LiftE Int `PairE` Atom r) - {- DepPair -} (Atom r `PairE` Atom r `PairE` DepPairType r)) - (WhenCore r (EitherE4 + {- 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 CoreIR) - {- TyConAtom -} (TyCon CoreIR))) + {- 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 $ WhenIRE $ Case0 lam - NewtypeCon con x -> Case1 $ WhenIRE $ Case1 $ con `PairE` x - DictConAtom con -> Case1 $ WhenIRE $ Case2 con - TyConAtom tc -> Case1 $ WhenIRE $ Case3 tc + 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 @@ -924,7 +914,7 @@ instance IRRep r => GenericE (Con r) where 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 (WhenIRE con) -> case con of + Case1 (con) -> case con of Case0 lam -> Lam lam Case1 (con' `PairE` x) -> NewtypeCon con' x Case2 con' -> DictConAtom con' @@ -933,27 +923,27 @@ instance IRRep r => GenericE (Con r) where _ -> error "impossible" {-# INLINE toE #-} -instance IRRep r => SinkableE (Con r) -instance IRRep r => HoistableE (Con r) -instance IRRep r => AlphaEqE (Con r) -instance IRRep r => AlphaHashableE (Con r) -instance IRRep r => RenameE (Con r) +instance SinkableE Con +instance HoistableE Con +instance AlphaEqE Con +instance AlphaHashableE Con +instance RenameE Con -instance IRRep r => GenericE (TyCon r) where - type RepE (TyCon r) = EitherE3 +instance GenericE TyCon where + type RepE TyCon = EitherE3 (EitherE4 {- BaseType -} (LiftE BaseType) - {- ProdType -} (ListE (Type r)) - {- SumType -} (ListE (Type r)) - {- RefType -} (Type r)) + {- ProdType -} (ListE Type) + {- SumType -} (ListE Type) + {- RefType -} Type) (EitherE3 - {- TabPi -} (TabPiType r) - {- DepPairTy -} (DepPairType r) - {- Kind -} (WhenCore r (LiftE Kind))) + {- TabPi -} TabPiType + {- DepPairTy -} DepPairType + {- Kind -} (LiftE Kind)) (EitherE3 - {- DictTy -} (WhenCore r DictType) - {- Pi -} (WhenCore r CorePiType) - {- NewtypeTyCon -} (WhenCore r NewtypeTyCon)) + {- DictTy -} (DictType) + {- Pi -} (CorePiType) + {- NewtypeTyCon -} (NewtypeTyCon)) fromE = \case BaseType b -> Case0 (Case0 (LiftE b)) ProdType ts -> Case0 (Case1 (ListE ts)) @@ -961,10 +951,10 @@ instance IRRep r => GenericE (TyCon r) where RefType t -> Case0 (Case3 t) TabPi t -> Case1 (Case0 t) DepPairTy t -> Case1 (Case1 t) - Kind k -> Case1 (Case2 (WhenIRE (LiftE k))) - DictTy t -> Case2 (Case0 (WhenIRE t)) - Pi t -> Case2 (Case1 (WhenIRE t)) - NewtypeTyCon t -> Case2 (Case2 (WhenIRE 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 @@ -976,36 +966,36 @@ instance IRRep r => GenericE (TyCon r) where Case1 c -> case c of Case0 t -> TabPi t Case1 t -> DepPairTy t - Case2 (WhenIRE (LiftE k)) -> Kind k + Case2 (LiftE k) -> Kind k _ -> error "impossible" Case2 c -> case c of - Case0 (WhenIRE t) -> DictTy t - Case1 (WhenIRE t) -> Pi t - Case2 (WhenIRE t) -> NewtypeTyCon t + Case0 t -> DictTy t + Case1 t -> Pi t + Case2 t -> NewtypeTyCon t _ -> error "impossible" _ -> error "impossible" {-# INLINE toE #-} -instance IRRep r => SinkableE (TyCon r) -instance IRRep r => HoistableE (TyCon r) -instance IRRep r => AlphaEqE (TyCon r) -instance IRRep r => AlphaHashableE (TyCon r) -instance IRRep r => RenameE (TyCon r) +instance SinkableE TyCon +instance HoistableE TyCon +instance AlphaEqE TyCon +instance AlphaHashableE TyCon +instance RenameE TyCon -instance IRRep r => GenericB (NonDepNest r ann) where - type RepB (NonDepNest r ann) = (LiftB (ListE ann)) `PairB` Nest (AtomNameBinder r) +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 IRRep r => ProvesExt (NonDepNest r ann) -instance IRRep r => BindsNames (NonDepNest r ann) -instance (IRRep r, SinkableE ann) => SinkableB (NonDepNest r ann) -instance (IRRep r, HoistableE ann) => HoistableB (NonDepNest r ann) -instance (IRRep r, RenameE ann, SinkableE ann) => RenameB (NonDepNest r ann) -instance (IRRep r, AlphaEqE ann) => AlphaEqB (NonDepNest r ann) -instance (IRRep r, AlphaHashableE ann) => AlphaHashableB (NonDepNest r ann) -deriving instance (Show (ann n)) => IRRep r => Show (NonDepNest r ann n l) +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 = @@ -1073,64 +1063,64 @@ instance AlphaEqE DictType instance AlphaHashableE DictType instance RenameE DictType -instance IRRep r => GenericE (Dict r) where - type RepE (Dict r) = EitherE (WhenCore r (PairE (Type r) (Stuck r))) (DictCon r) +instance GenericE Dict where + type RepE Dict = EitherE (PairE Type Stuck) DictCon fromE = \case - StuckDict t d -> LeftE (WhenIRE (PairE t d)) + StuckDict t d -> LeftE (PairE t d) DictCon d -> RightE d {-# INLINE fromE #-} toE = \case - LeftE (WhenIRE (PairE t d)) -> StuckDict t d + LeftE (PairE t d) -> StuckDict t d RightE d -> DictCon d {-# INLINE toE #-} -instance IRRep r => SinkableE (Dict r) -instance IRRep r => HoistableE (Dict r) -instance IRRep r => AlphaEqE (Dict r) -instance IRRep r => AlphaHashableE (Dict r) -instance IRRep r => RenameE (Dict r) - -instance IRRep r => GenericE (DictCon r) where - type RepE (DictCon r) = EitherE4 - {- InstanceDict -} (WhenCore r (CType `PairE` PairE InstanceName (ListE CAtom))) - {- IxFin -} (WhenCore r CAtom) - {- IxRawFin -} (Atom r) - {- IxSpecialized -} (WhenSimp r (SpecDictName `PairE` ListE SAtom)) +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 $ WhenIRE $ t `PairE` PairE v (ListE args) - IxFin x -> Case1 $ WhenIRE $ x + InstanceDict t v args -> Case0 $ t `PairE` PairE v (ListE args) + IxFin x -> Case1 $ x IxRawFin n -> Case2 $ n - IxSpecialized d xs -> Case3 $ WhenIRE $ d `PairE` ListE xs + IxSpecialized d xs -> Case3 $ d `PairE` ListE xs toE = \case - Case0 (WhenIRE (t `PairE` (PairE v (ListE args)))) -> InstanceDict t v args - Case1 (WhenIRE x) -> IxFin x - Case2 n -> IxRawFin n - Case3 (WhenIRE (d `PairE` ListE xs)) -> IxSpecialized d xs + 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 IRRep r => SinkableE (DictCon r) -instance IRRep r => HoistableE (DictCon r) -instance IRRep r => AlphaEqE (DictCon r) -instance IRRep r => AlphaHashableE (DictCon r) -instance IRRep r => RenameE (DictCon r) +instance SinkableE DictCon +instance HoistableE DictCon +instance AlphaEqE DictCon +instance AlphaHashableE DictCon +instance RenameE DictCon -instance GenericE (LamExpr r) where - type RepE (LamExpr r) = Abs (Nest (Binder r)) (Expr r) +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 IRRep r => SinkableE (LamExpr r) -instance IRRep r => HoistableE (LamExpr r) -instance IRRep r => AlphaEqE (LamExpr r) -instance IRRep r => AlphaHashableE (LamExpr r) -instance IRRep r => RenameE (LamExpr r) -deriving instance IRRep r => Show (LamExpr r n) -deriving via WrapE (LamExpr r) n instance IRRep r => Generic (LamExpr r n) +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 CoreIR + type RepE CoreLamExpr = CorePiType `PairE` LamExpr fromE (CoreLamExpr ty lam) = ty `PairE` lam {-# INLINE fromE #-} toE (ty `PairE` lam) = CoreLamExpr ty lam @@ -1143,7 +1133,7 @@ instance AlphaHashableE CoreLamExpr instance RenameE CoreLamExpr instance GenericE CorePiType where - type RepE CorePiType = LiftE (AppExplicitness, [Explicitness]) `PairE` Abs (Nest CBinder) (Type CoreIR) + 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 @@ -1157,76 +1147,76 @@ instance RenameE CorePiType deriving instance Show (CorePiType n) deriving via WrapE CorePiType n instance Generic (CorePiType n) -instance IRRep r => GenericE (IxType r) where - type RepE (IxType r) = PairE (Type r) (IxDict r) +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 IRRep r => SinkableE (IxType r) -instance IRRep r => HoistableE (IxType r) -instance IRRep r => RenameE (IxType r) +instance SinkableE IxType +instance HoistableE IxType +instance RenameE IxType -instance IRRep r => AlphaEqE (IxType r) where +instance AlphaEqE IxType where alphaEqE (IxType t1 _) (IxType t2 _) = alphaEqE t1 t2 -instance IRRep r => AlphaHashableE (IxType r) where +instance AlphaHashableE IxType where hashWithSaltE env salt (IxType t _) = hashWithSaltE env salt t -instance IRRep r => GenericE (TabPiType r) where - type RepE (TabPiType r) = PairE (IxDict r) (Abs (Binder r) (Type r)) +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 IRRep r => AlphaEqE (TabPiType r) where +instance AlphaEqE TabPiType where alphaEqE (TabPiType _ b1 t1) (TabPiType _ b2 t2) = alphaEqE (Abs b1 t1) (Abs b2 t2) -instance IRRep r => AlphaHashableE (TabPiType r) where +instance AlphaHashableE TabPiType where hashWithSaltE env salt (TabPiType _ b t) = hashWithSaltE env salt $ Abs b t -instance HasNameHint (TabPiType r n) where +instance HasNameHint (TabPiType n) where getNameHint (TabPiType _ b _) = getNameHint b -instance IRRep r => SinkableE (TabPiType r) -instance IRRep r => HoistableE (TabPiType r) -instance IRRep r => RenameE (TabPiType r) -deriving instance IRRep r => Show (TabPiType r n) -deriving via WrapE (TabPiType r) n instance IRRep r => Generic (TabPiType r n) +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 r) where - type RepE (PiType r) = Abs (Nest (Binder r)) (Type r) +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 IRRep r => SinkableE (PiType r) -instance IRRep r => HoistableE (PiType r) -instance IRRep r => AlphaEqE (PiType r) -instance IRRep r => AlphaHashableE (PiType r) -instance IRRep r => RenameE (PiType r) -deriving instance IRRep r => Show (PiType r n) -deriving via WrapE (PiType r) n instance IRRep r => Generic (PiType r n) -instance IRRep r => Store (PiType r n) - -instance GenericE (DepPairType r) where - type RepE (DepPairType r) = PairE (LiftE DepPairExplicitness) (Abs (Binder r) (Type r)) +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 IRRep r => SinkableE (DepPairType r) -instance IRRep r => HoistableE (DepPairType r) -instance IRRep r => AlphaEqE (DepPairType r) -instance IRRep r => AlphaHashableE (DepPairType r) -instance IRRep r => RenameE (DepPairType r) -deriving instance IRRep r => Show (DepPairType r n) -deriving via WrapE (DepPairType r) n instance IRRep r => Generic (DepPairType r n) +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) @@ -1241,8 +1231,8 @@ instance RenameE DotMethods instance AlphaEqE DotMethods instance AlphaHashableE DotMethods -instance IRRep r => GenericE (Effects r) where - type RepE (Effects r) = EitherE UnitE UnitE +instance GenericE Effects where + type RepE Effects = EitherE UnitE UnitE fromE = \case Pure -> LeftE UnitE Effectful -> RightE UnitE @@ -1252,58 +1242,58 @@ instance IRRep r => GenericE (Effects r) where RightE UnitE -> Effectful {-# INLINE toE #-} -instance IRRep r => SinkableE (Effects r) -instance IRRep r => HoistableE (Effects r) -instance IRRep r => RenameE (Effects r) -instance IRRep r => AlphaEqE (Effects r) -instance IRRep r => AlphaHashableE (Effects r) +instance SinkableE Effects +instance HoistableE Effects +instance RenameE Effects +instance AlphaEqE Effects +instance AlphaHashableE Effects -instance IRRep r => GenericE (EffTy r) where - type RepE (EffTy r) = PairE (Effects r) (Type r) +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 IRRep r => SinkableE (EffTy r) -instance IRRep r => HoistableE (EffTy r) -instance IRRep r => RenameE (EffTy r) -instance IRRep r => AlphaEqE (EffTy r) -instance IRRep r => AlphaHashableE (EffTy r) +instance SinkableE EffTy +instance HoistableE EffTy +instance RenameE EffTy +instance AlphaEqE EffTy +instance AlphaHashableE EffTy -instance IRRep r => GenericE (DeclBinding r) where - type RepE (DeclBinding r) = LiftE LetAnn `PairE` Expr r +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 IRRep r => SinkableE (DeclBinding r) -instance IRRep r => HoistableE (DeclBinding r) -instance IRRep r => RenameE (DeclBinding r) -instance IRRep r => AlphaEqE (DeclBinding r) -instance IRRep r => AlphaHashableE (DeclBinding r) +instance SinkableE DeclBinding +instance HoistableE DeclBinding +instance RenameE DeclBinding +instance AlphaEqE DeclBinding +instance AlphaHashableE DeclBinding -instance GenericB (Decl r) where - type RepB (Decl r) = AtomBinderP r (DeclBinding r) +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 IRRep r => SinkableB (Decl r) -instance IRRep r => HoistableB (Decl r) -instance IRRep r => RenameB (Decl r) -instance IRRep r => AlphaEqB (Decl r) -instance IRRep r => AlphaHashableB (Decl r) -instance IRRep r => ProvesExt (Decl r) -instance IRRep r => BindsNames (Decl r) +instance SinkableB Decl +instance HoistableB Decl +instance RenameB Decl +instance AlphaEqB Decl +instance AlphaHashableB Decl +instance ProvesExt Decl +instance BindsNames Decl -instance IRRep r => BindsAtMostOneName (Decl r) (AtomNameC r) where +instance BindsAtMostOneName Decl where Let b _ @> x = b @> x {-# INLINE (@>) #-} -instance IRRep r => BindsOneName (Decl r) (AtomNameC r) where +instance BindsOneName Decl where binderName (Let b _) = binderName b {-# INLINE binderName #-} @@ -1311,56 +1301,56 @@ instance Hashable IxMethod instance Hashable BuiltinClassName instance Hashable Kind -instance IRRep r => Store (TyCon r n) -instance IRRep r => Store (Con r n) -instance IRRep r => Store (RepVal r n) -instance IRRep r => Store (Type r n) +instance Store (TyCon n) +instance Store (Con n) +instance Store (RepVal n) +instance Store (Type n) instance Store Kind -instance IRRep r => Store (Effects r n) -instance IRRep r => Store (EffTy r n) -instance IRRep r => Store (Stuck r n) -instance IRRep r => Store (Atom r n) -instance IRRep r => Store (AtomVar r n) -instance IRRep r => Store (Expr r n) -instance IRRep r => Store (DeclBinding r n) -instance IRRep r => Store (Decl r n l) +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 IRRep r => Store (LamExpr r n) -instance IRRep r => Store (IxType r n) +instance Store (LamExpr n) +instance Store (IxType n) instance Store (CorePiType n) instance Store (CoreLamExpr n) -instance IRRep r => Store (TabPiType r n) -instance IRRep r => Store (DepPairType r 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 IRRep r => Store (DictCon r n) -instance Store (ann n) => Store (NonDepNest r ann n l) +instance Store (DictCon n) +instance Store (ann n) => Store (NonDepNest ann n l) instance Store IxMethod -instance IRRep r => Store (Dict r n) -instance IRRep r => Store (TypedHof r n) -instance IRRep r => Store (Hof r n) +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 IRRep r => Pretty (Hof r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (Hof r n) where +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 IRRep r => Pretty (TyCon r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (TyCon r n) where +instance Pretty (TyCon n) where pretty = prettyFromPrettyPrec +instance PrettyPrec (TyCon n) where prettyPrec con = case con of BaseType b -> prettyPrec b ProdType [] -> atPrec ArgPrec $ "()" @@ -1403,8 +1393,8 @@ instance PrettyPrec (NewtypeTyCon n) where (t'', ')') <- unsnoc t' return t'' -instance IRRep r => Pretty (Con r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (Con r n) where +instance Pretty (Con n) where pretty = prettyFromPrettyPrec +instance PrettyPrec (Con n) where prettyPrec = \case Lit l -> prettyPrec l ProdCon [x] -> atPrec ArgPrec $ "(" <> pLowest x <> ",)" @@ -1449,8 +1439,8 @@ instance Pretty (InstanceDef n) where pretty (InstanceDef className _ bs params _) = "Instance" <+> pretty className <+> pretty bs <+> pretty params -instance IRRep r => Pretty (Expr r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (Expr r n) where +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 @@ -1468,42 +1458,42 @@ instance IRRep r => PrettyPrec (Expr r n) where p :: Pretty a => a -> Doc ann p = pretty -prettyPrecCase :: IRRep r => Doc ann -> Atom r n -> [Alt r n] -> DocPrec ann +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 :: IRRep r => Alt r n -> Doc ann +prettyAlt :: Alt n -> Doc ann prettyAlt (Abs b body) = prettyBinderNoAnn b <+> "->" <> nest 2 (pretty body) -prettyBinderNoAnn :: Binder r n l -> Doc ann +prettyBinderNoAnn :: Binder n l -> Doc ann prettyBinderNoAnn (b:>_) = pretty b -instance IRRep r => Pretty (DeclBinding r n) where +instance Pretty (DeclBinding n) where pretty (DeclBinding ann expr) = "Decl" <> pretty ann <+> pretty expr -instance IRRep r => Pretty (Decl r n l) where +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 IRRep r => Pretty (PiType r n) where +instance Pretty (PiType n) where pretty (PiType bs resultTy) = (spaced $ unsafeFromNest $ bs) <+> "->" <+> pretty resultTy -instance IRRep r => Pretty (LamExpr r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (LamExpr r n) where +instance Pretty (LamExpr n) where pretty = prettyFromPrettyPrec +instance PrettyPrec (LamExpr n) where prettyPrec (LamExpr bs body) = atPrec LowestPrec $ prettyLam (pretty bs <> ".") body -instance IRRep r => Pretty (IxType r n) where +instance Pretty (IxType n) where pretty (IxType ty dict) = parens $ "IxType" <+> pretty ty <> prettyIxDict dict -instance IRRep r => Pretty (Dict r n) where +instance Pretty (Dict n) where pretty = \case DictCon con -> pretty con StuckDict _ stuck -> pretty stuck -instance IRRep r => Pretty (DictCon r n) where +instance Pretty (DictCon n) where pretty = \case InstanceDict _ name args -> "Instance" <+> pretty name <+> pretty args IxFin n -> "Ix (Fin" <+> pretty n <> ")" @@ -1515,28 +1505,28 @@ instance Pretty (DictType n) where DictType classSourceName _ params -> pretty classSourceName <+> spaced params IxDictType ty -> "Ix" <+> pretty ty -instance IRRep r => Pretty (DepPairType r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (DepPairType r n) where +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 IRRep r => Pretty (Atom r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (Atom r n) where +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 IRRep r => Pretty (Type r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (Type r n) where +instance Pretty (Type n) where pretty = prettyFromPrettyPrec +instance PrettyPrec (Type n) where prettyPrec = \case TyCon e -> prettyPrec e StuckTy _ e -> prettyPrec e -instance IRRep r => Pretty (Stuck r n) where pretty = prettyFromPrettyPrec -instance IRRep r => PrettyPrec (Stuck r n) where +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 @@ -1550,14 +1540,14 @@ instance IRRep r => PrettyPrec (Stuck r n) where p :: Pretty a => a -> Doc ann p = pretty -instance PrettyPrec (AtomVar r n) where +instance PrettyPrec (AtomVar n) where prettyPrec (AtomVar v _) = prettyPrec v -instance Pretty (AtomVar r n) where pretty = prettyFromPrettyPrec +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 IRRep r => Pretty (TabPiType r n) where +instance Pretty (TabPiType n) where pretty (TabPiType dict (b:>ty) body) = let prettyBody = case body of TyCon (Pi subpi) -> pretty subpi @@ -1568,10 +1558,10 @@ instance IRRep r => Pretty (TabPiType r n) where -- 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 :: IRRep r => IxDict r n -> Doc ann +prettyIxDict :: IxDict n -> Doc ann prettyIxDict dict = if False then " " <> pretty dict else mempty -prettyBinderHelper :: IRRep r => HoistableE e => Binder r n l -> e l -> Doc ann +prettyBinderHelper :: HoistableE e => Binder n l -> e l -> Doc ann prettyBinderHelper (b:>ty) body = if binderName b `isFreeIn` body then parens $ pretty (b:>ty) @@ -1601,10 +1591,10 @@ withExplParens Explicit x = parens x withExplParens (Inferred _ Unify) x = braces $ x withExplParens (Inferred _ (Synth _)) x = brackets x -instance IRRep r => Pretty (RepVal r n) where +instance Pretty (RepVal n) where pretty (RepVal ty tree) = " pretty tree <+> ":" <+> pretty ty <> ">" -prettyBlock :: (IRRep r, PrettyPrec (e l)) => Nest (Decl r) n l -> e l -> Doc ann +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/Imp.hs b/src/lib/Types/Imp.hs index 9006745ce..71d28495e 100644 --- a/src/lib/Types/Imp.hs +++ b/src/lib/Types/Imp.hs @@ -38,16 +38,15 @@ import Types.Source -- === data types === -type ImpName = Name ImpNameC - -type ImpFunName = Name TopFunNameC +type ImpName = Name +type PtrName = Name +type ImpFunName = Name data IExpr n = ILit LitVal | IVar (ImpName n) BaseType - | IPtrVar (Name PtrNameC n) PtrType + | IPtrVar (PtrName n) PtrType deriving (Show, Generic) -data IBinder n l = IBinder (NameBinder ImpNameC n l) IType - deriving (Show, Generic) +data IBinder n l = IBinder (NameBinder n l) IType deriving (Show, Generic) type IVal = IExpr -- only ILit and IRef constructors type IType = BaseType @@ -171,7 +170,7 @@ data WithCNameInterface a = WithCNameInterface type RawObjCode = BS.ByteString type FunObjCode = WithCNameInterface RawObjCode -data IFunBinder n l = IFunBinder (NameBinder TopFunNameC n l) IFunType +data IFunBinder n l = IFunBinder (NameBinder n l) IFunType -- Imp function with link-time objects abstracted out, suitable for standalone -- compilation. TODO: enforce actual `VoidS` as the scope parameter. @@ -182,9 +181,10 @@ data ClosedImpFunction n where -> ImpFunction n3 -> ClosedImpFunction n1 -data PtrBinder n l = PtrBinder (NameBinder PtrNameC n l) PtrType -data LinktimeNames n = LinktimeNames [Name FunObjCodeNameC n] [Name PtrNameC n] deriving (Show, Generic) -data LinktimeVals = LinktimeVals [FunPtr ()] [Ptr ()] deriving (Show, Generic) +data PtrBinder n l = PtrBinder (NameBinder n l) PtrType +type FunObjCodeName = Name +data LinktimeNames n = LinktimeNames [FunObjCodeName n] [PtrName n] deriving (Show, Generic) +data LinktimeVals = LinktimeVals [FunPtr ()] [Ptr ()] deriving (Show, Generic) data CFunction (n::S) = CFunction { nameHint :: NameHint @@ -193,11 +193,11 @@ data CFunction (n::S) = CFunction } deriving (Show, Generic) -instance BindsAtMostOneName IFunBinder TopFunNameC where +instance BindsAtMostOneName IFunBinder where IFunBinder b _ @> x = b @> x {-# INLINE (@>) #-} -instance BindsOneName IFunBinder TopFunNameC where +instance BindsOneName IFunBinder where binderName (IFunBinder b _) = binderName b {-# INLINE binderName #-} @@ -205,7 +205,7 @@ instance HasNameHint (IFunBinder n l) where getNameHint (IFunBinder b _) = getNameHint b instance GenericB IFunBinder where - type RepB IFunBinder = BinderP TopFunNameC (LiftE IFunType) + type RepB IFunBinder = BinderP (LiftE IFunType) fromB (IFunBinder b ty) = b :> LiftE ty toB (b :> LiftE ty) = IFunBinder b ty @@ -218,14 +218,10 @@ instance AlphaEqB IFunBinder instance AlphaHashableB IFunBinder instance GenericB PtrBinder where - type RepB PtrBinder = BinderP PtrNameC (LiftE PtrType) + type RepB PtrBinder = BinderP (LiftE PtrType) fromB (PtrBinder b ty) = b :> LiftE ty toB (b :> LiftE ty) = PtrBinder b ty -instance BindsAtMostOneName PtrBinder PtrNameC where - PtrBinder b _ @> x = b @> x - {-# INLINE (@>) #-} - instance HasNameHint (PtrBinder n l) where getNameHint (PtrBinder b _) = getNameHint b @@ -368,8 +364,8 @@ deriving via WrapE ImpBlock n instance Generic (ImpBlock n) instance GenericE IExpr where type RepE IExpr = EitherE3 (LiftE LitVal) - (PairE ImpName (LiftE BaseType)) - (PairE (Name PtrNameC) (LiftE PtrType)) + (PairE ImpName (LiftE BaseType)) + (PairE PtrName (LiftE PtrType)) fromE iexpr = case iexpr of ILit x -> Case0 (LiftE x) IVar v ty -> Case1 (v `PairE` LiftE ty) @@ -390,19 +386,13 @@ instance AlphaHashableE IExpr instance RenameE IExpr instance GenericB IBinder where - type RepB IBinder = PairB (LiftB (LiftE IType)) (NameBinder ImpNameC) + type RepB IBinder = PairB (LiftB (LiftE IType)) NameBinder fromB (IBinder b ty) = PairB (LiftB (LiftE ty)) b toB (PairB (LiftB (LiftE ty)) b) = IBinder b ty instance HasNameHint (IBinder n l) where getNameHint (IBinder b _) = getNameHint b -instance BindsAtMostOneName IBinder ImpNameC where - IBinder b _ @> x = b @> x - -instance BindsOneName IBinder ImpNameC where - binderName (IBinder b _) = binderName b - instance BindsNames IBinder where toScopeFrag (IBinder b _) = toScopeFrag b @@ -441,8 +431,7 @@ instance AlphaHashableE ImpFunction instance RenameE ImpFunction instance GenericE LinktimeNames where - type RepE LinktimeNames = ListE (Name FunObjCodeNameC) - `PairE` ListE (Name PtrNameC) + type RepE LinktimeNames = ListE FunObjCodeName `PairE` ListE PtrName fromE (LinktimeNames funs ptrs) = ListE funs `PairE` ListE ptrs {-# INLINE fromE #-} toE (ListE funs `PairE` ListE ptrs) = LinktimeNames funs ptrs diff --git a/src/lib/Types/Primitives.hs b/src/lib/Types/Primitives.hs index f0f8bbf17..e2a76e615 100644 --- a/src/lib/Types/Primitives.hs +++ b/src/lib/Types/Primitives.hs @@ -38,7 +38,6 @@ import GHC.Generics (Generic (..)) import PPrint -- import Occurrence import Name -import IRVariants -- === Primitive ops === @@ -46,38 +45,50 @@ data BinOp = IAdd | ISub | IMul | IDiv | ICmp CmpOp | FAdd | FSub | FMul | FDiv | FCmp CmpOp | FPow | BAnd | BOr | BShL | BShR | IRem | BXor deriving (Show, Eq, Ord, Generic) +instance Hashable BinOp +instance Store BinOp data UnOp = Exp | Exp2 | Log | Log2 | Log10 | Log1p | Sin | Cos | Tan | Sqrt | Floor | Ceil | Round | LGamma | Erf | Erfc | FNeg | BNot deriving (Show, Eq, Ord, Generic) +instance Hashable UnOp +instance Store UnOp data CmpOp = Less | Greater | Equal | LessEqual | GreaterEqual deriving (Show, Eq, Ord, Generic) +instance Hashable CmpOp +instance Store CmpOp data Projection = UnwrapNewtype -- TODO: add `HasCore r` constraint | ProjectProduct Int deriving (Show, Eq, Ord, Generic) +instance Hashable Projection +instance Store Projection -data PrimOp (r::IR) (a:: *) = +data PrimOp a = UnOp UnOp a | BinOp BinOp a a - | MemOp (MemOp r a) - | VectorOp (VectorOp r a) - | MiscOp (MiscOp r a) - | RefOp a (RefOp r a) + | MemOp (MemOp a) + | VectorOp (VectorOp a) + | MiscOp (MiscOp a) + | RefOp a (RefOp a) deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) +instance Hashable a => Hashable (PrimOp a) +instance Store a => Store (PrimOp a) -data MemOp (r::IR) (a:: *) = +data MemOp a = IOAlloc a | IOFree a | PtrOffset a a | PtrLoad a | PtrStore a a deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) +instance Hashable a => Hashable (MemOp a) +instance Store a => Store (MemOp a) -data MiscOp (r::IR) (a:: *) = +data MiscOp a = Select a a a -- (3) predicate, val-if-true, val-if-false | CastOp a -- (2) See CheckType.hs for valid coercions. | BitcastOp a -- (2) See CheckType.hs for valid coercions. @@ -96,20 +107,26 @@ data MiscOp (r::IR) (a:: *) = -- giving the logical size of the result and a fixed-size table, -- `Fin showStringBufferSize => Char`, assumed to have sufficient space. deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) +instance Hashable a => Hashable (MiscOp a) +instance Store a => Store (MiscOp a) -data VectorOp r a = +data VectorOp a = VectorBroadcast a | VectorIota | VectorIdx a a -- table, base ix | VectorSubref a a -- ref, base ix deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) +instance Hashable a => Hashable (VectorOp a) +instance Store a => Store (VectorOp a) -data RefOp r a = +data RefOp a = MGet | MPut a | IndexRef a | ProjRef Projection deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) +instance Hashable a => Hashable (RefOp a) +instance Store a => Store (RefOp a) -- === various things === @@ -357,8 +374,8 @@ instance PrettyPrec ScalarBaseType where Word32Type -> "Word32" Word64Type -> "Word64" -instance (IRRep r, PrettyPrec a) => Pretty (PrimOp r a) where pretty = prettyFromPrettyPrec -instance (IRRep r, PrettyPrec a) => PrettyPrec (PrimOp r a) where +instance PrettyPrec a => Pretty (PrimOp a) where pretty = prettyFromPrettyPrec +instance PrettyPrec a => PrettyPrec (PrimOp a) where prettyPrec = \case MemOp op -> prettyPrec op VectorOp op -> prettyPrec op @@ -379,41 +396,20 @@ instance Pretty Projection where UnwrapNewtype -> "u" ProjectProduct i -> pretty i -instance (IRRep r, PrettyPrec a) => Pretty (MemOp r a) where pretty = prettyFromPrettyPrec -instance (IRRep r, PrettyPrec a) => PrettyPrec (MemOp r a) where +instance PrettyPrec a => Pretty (MemOp a) where pretty = prettyFromPrettyPrec +instance PrettyPrec a => PrettyPrec (MemOp a) where prettyPrec = \case PtrOffset ptr idx -> atPrec LowestPrec $ pApp ptr <+> "+>" <+> pApp idx PtrLoad ptr -> atPrec AppPrec $ pAppArg "load" [ptr] op -> undefined -instance (IRRep r, PrettyPrec a) => Pretty (VectorOp r a) where pretty = prettyFromPrettyPrec -instance (IRRep r, PrettyPrec a) => PrettyPrec (VectorOp r a) where +instance PrettyPrec a => Pretty (VectorOp a) where pretty = prettyFromPrettyPrec +instance PrettyPrec a => PrettyPrec (VectorOp a) where prettyPrec = \case VectorBroadcast v -> atPrec LowestPrec $ "vbroadcast" <+> pApp v VectorIota -> atPrec LowestPrec $ "viota" VectorIdx tbl i -> atPrec LowestPrec $ "vslice" <+> pApp tbl <+> pApp i VectorSubref ref i -> atPrec LowestPrec $ "vrefslice" <+> pApp ref <+> pApp i - instance Pretty Explicitness where pretty expl = pretty (show expl) - -instance Hashable BinOp -instance Hashable UnOp -instance Hashable CmpOp -instance Hashable Projection -instance (IRRep r, Hashable a) => Hashable (PrimOp r a) -instance (IRRep r, Hashable a) => Hashable (MemOp r a) -instance (IRRep r, Hashable a) => Hashable (MiscOp r a) -instance (IRRep r, Hashable a) => Hashable (VectorOp r a) -instance (IRRep r, Hashable a) => Hashable (RefOp r a) - -instance Store BinOp -instance Store UnOp -instance Store CmpOp -instance Store Projection -instance (IRRep r, Store a) => Store (PrimOp r a) -instance (IRRep r, Store a) => Store (MemOp r a) -instance (IRRep r, Store a) => Store (MiscOp r a) -instance (IRRep r, Store a) => Store (VectorOp r a) -instance (IRRep r, Store a) => Store (RefOp r a) diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs index 3d435a12f..29526d4c2 100644 --- a/src/lib/Types/Source.hs +++ b/src/lib/Types/Source.hs @@ -38,7 +38,6 @@ import Data.String (fromString) import Err import PPrint import Name -import IRVariants import MonadUtil import Util (File (..), SnocList) @@ -54,9 +53,6 @@ deriving instance Eq (a n) => Eq (SourceNameOr a n) deriving instance Ord (a n) => Ord (SourceNameOr a n) deriving instance Show (a n) => Show (SourceNameOr a n) -newtype SourceOrInternalName (c::C) (n::S) = SourceOrInternalName (SourceNameOr (Name c) n) - deriving (Eq, Ord, Show, Generic) - -- === Source Info === -- This is just for syntax highlighting. It won't be needed if we have @@ -276,26 +272,18 @@ data CSBlock = -- === Untyped IR === -- The AST of Dex surface language. -data UVar (n::S) = - UAtomVar (Name (AtomNameC CoreIR) n) - | UTyConVar (Name TyConNameC n) - | UDataConVar (Name DataConNameC n) - | UClassVar (Name ClassNameC n) - | UMethodVar (Name MethodNameC n) - | UPunVar (Name TyConNameC n) -- for names also used as data constructors - deriving (Eq, Ord, Show, Generic) - -type UAtomBinder = UBinder (AtomNameC CoreIR) -type UBinder c = WithSrcB (UBinder' c) -data UBinder' (c::C) (n::S) (l::S) where +type UVar = Name + +type UBinder = WithSrcB UBinder' +data UBinder' (n::S) (l::S) where -- Only appears before renaming pass - UBindSource :: SourceName -> UBinder' c n n + UBindSource :: SourceName -> UBinder' n n -- May appear before or after renaming pass - UIgnore :: UBinder' c n n + UIgnore :: UBinder' n n -- The following binders only appear after the renaming pass. -- We maintain the source name for user-facing error messages -- and named arguments. - UBind :: SourceName -> NameBinder c n l -> UBinder' c n l + UBind :: SourceName -> NameBinder n l -> UBinder' n l type UBlock = WithSrcE UBlock' data UBlock' (n::S) where @@ -369,7 +357,7 @@ data UStructDef (n::S) where :: SourceName -- source name for pretty printing -> Nest UAnnBinder n l -> [(SourceNameW, UType l)] -- named payloads - -> [(LetAnn, SourceName, Abs UAtomBinder ULamExpr l)] -- named methods (initial binder is for `self`) + -> [(LetAnn, SourceName, Abs UBinder ULamExpr l)] -- named methods (initial binder is for `self`) -> UStructDef n data UDataDefTrail (l::S) where @@ -378,28 +366,27 @@ data UDataDefTrail (l::S) where data UTopDecl (n::S) (l::S) where ULocalDecl :: UDecl n l -> UTopDecl n l UDataDefDecl - :: UDataDef n -- actual definition - -> UBinder TyConNameC n l' -- type constructor name - -> Nest (UBinder DataConNameC) l' l -- data constructor names + :: UDataDef n -- actual definition + -> UBinder n l' -- type constructor name + -> Nest UBinder l' l -- data constructor names -> UTopDecl n l UStructDecl - :: UBinder TyConNameC n l -- type constructor name - -> UStructDef l -- actual definition + :: UBinder n l -- type constructor name + -> UStructDef l -- actual definition -> UTopDecl n l UInterface :: Nest UAnnBinder n p -- parameter binders - -> [UType p] -- method types - -> UBinder ClassNameC n l' -- class name - -> Nest (UBinder MethodNameC) l' l -- method names + -> [UType p] -- method types + -> UBinder n l' -- class name + -> Nest UBinder l' l -- method names -> UTopDecl n l UInstance - :: SourceNameOr (Name ClassNameC) n -- class name + :: SourceNameOr Name n -- class name -> Nest UAnnBinder n l' - -> [UExpr l'] -- class parameters - -> [UMethodDef l'] -- method definitions - -- Maybe we should make a separate color (namespace) for instance names? - -> MaybeB UAtomBinder n l -- optional instance name - -> AppExplicitness -- explicitness (only relevant for named instances) + -> [UExpr l'] -- class parameters + -> [UMethodDef l'] -- method definitions + -> MaybeB UBinder n l -- optional instance name + -> AppExplicitness -- explicitness (only relevant for named instances) -> UTopDecl n l type UType = UExpr @@ -409,14 +396,14 @@ data UForExpr (n::S) where UForExpr :: UAnnBinder n l -> UBlock l -> UForExpr n type UMethodDef = WithSrcE UMethodDef' -data UMethodDef' (n::S) = UMethodDef (SourceNameOr (Name MethodNameC) n) (ULamExpr n) +data UMethodDef' (n::S) = UMethodDef (SourceNameOr Name n) (ULamExpr n) deriving (Show, Generic) data UAnn (n::S) = UAnn (UType n) | UNoAnn deriving Show -- TODO: SrcId data UAnnBinder (n::S) (l::S) = - UAnnBinder Explicitness (UAtomBinder n l) (UAnn n) [UConstraint n] + UAnnBinder Explicitness (UBinder n l) (UAnn n) [UConstraint n] deriving (Show, Generic) data UAlt (n::S) where @@ -424,8 +411,8 @@ data UAlt (n::S) where type UPat = WithSrcB UPat' data UPat' (n::S) (l::S) = - UPatBinder (UAtomBinder n l) - | UPatCon (SourceNameOr (Name DataConNameC) n) (Nest UPat n l) + UPatBinder (UBinder n l) + | UPatCon (SourceNameOr Name n) (Nest UPat n l) | UPatProd (Nest UPat n l) | UPatDepPair (PairB UPat UPat n l) | UPatTable (Nest UPat n l) @@ -442,7 +429,7 @@ instance HasSourceName (b n l) => HasSourceName (WithSrcB b n l) where instance HasSourceName (UAnnBinder n l) where getSourceName (UAnnBinder _ b _ _) = getSourceName b -instance HasSourceName (UBinder' c n l) where +instance HasSourceName (UBinder' n l) where getSourceName = \case UBindSource sn -> sn UIgnore -> "_" @@ -497,10 +484,7 @@ class FromSourceNameW a where instance FromSourceNameW (SourceNameOr a VoidS) where fromSourceNameW (WithSrc sid x) = SourceName sid x -instance FromSourceNameW (SourceOrInternalName c VoidS) where - fromSourceNameW x = SourceOrInternalName $ fromSourceNameW x - -instance FromSourceNameW (UBinder' s VoidS VoidS) where +instance FromSourceNameW (UBinder' VoidS VoidS) where fromSourceNameW x = UBindSource $ withoutSrc x instance FromSourceNameW (UPat' VoidS VoidS) where @@ -649,9 +633,9 @@ data PrimName = data TCName = ProdType | SumType | RefType | TypeKind deriving (Show, Eq, Generic) data ConName = ProdCon | SumCon Int deriving (Show, Eq, Generic) -type MemOpName = MemOp CoreIR () -type VectorOpName = VectorOp CoreIR () -type MiscOpName = MiscOp CoreIR () +type MemOpName = MemOp () +type VectorOpName = VectorOp () +type MiscOpName = MiscOp () -- === primitive constructors and operators === @@ -801,45 +785,6 @@ instance Pretty (SourceMap n) where pretty (SourceMap m) = fold [pretty v <+> "@>" <+> pretty x <> hardline | (v, x) <- M.toList m ] -instance GenericE UVar where - type RepE UVar = EitherE6 (Name (AtomNameC CoreIR)) (Name TyConNameC) - (Name DataConNameC) (Name ClassNameC) - (Name MethodNameC) (Name TyConNameC) - fromE name = case name of - UAtomVar v -> Case0 v - UTyConVar v -> Case1 v - UDataConVar v -> Case2 v - UClassVar v -> Case3 v - UMethodVar v -> Case4 v - UPunVar v -> Case5 v - {-# INLINE fromE #-} - - toE name = case name of - Case0 v -> UAtomVar v - Case1 v -> UTyConVar v - Case2 v -> UDataConVar v - Case3 v -> UClassVar v - Case4 v -> UMethodVar v - Case5 v -> UPunVar v - _ -> error "impossible" - {-# INLINE toE #-} - -instance Pretty (UVar n) where - pretty name = case name of - UAtomVar v -> "Atom name: " <> pretty v - UTyConVar v -> "Type constructor name: " <> pretty v - UDataConVar v -> "Data constructor name: " <> pretty v - UClassVar v -> "Class name: " <> pretty v - UMethodVar v -> "Method name: " <> pretty v - UPunVar v -> "Shared type constructor / data constructor name: " <> pretty v - --- TODO: name subst instances for the rest of UExpr -instance SinkableE UVar -instance HoistableE UVar -instance AlphaEqE UVar -instance AlphaHashableE UVar -instance RenameE UVar - instance HasNameHint (b n l) => HasNameHint (WithSrcB b n l) where getNameHint (WithSrcB _ b) = getNameHint b @@ -852,28 +797,28 @@ instance HasNameHint ModuleSourceName where getNameHint Prelude = getNameHint @String "prelude" getNameHint Main = getNameHint @String "main" -instance HasNameHint (UBinder' c n l) where +instance HasNameHint (UBinder' n l) where getNameHint b = case b of UBindSource v -> getNameHint v UIgnore -> noHint UBind v _ -> getNameHint v -instance Color c => BindsNames (UBinder' c) where +instance BindsNames UBinder' where toScopeFrag (UBindSource _) = emptyOutFrag toScopeFrag (UIgnore) = emptyOutFrag toScopeFrag (UBind _ b) = toScopeFrag b -instance Color c => ProvesExt (UBinder' c) where -instance Color c => BindsAtMostOneName (UBinder' c) c where +instance ProvesExt UBinder' where +instance BindsAtMostOneName UBinder' where b @> x = case b of UBindSource _ -> emptyInFrag UIgnore -> emptyInFrag UBind _ b' -> b' @> x -instance Color c => SinkableB (UBinder' c) where +instance SinkableB UBinder' where sinkingProofB _ _ _ = todoSinkableProof -instance Color c => RenameB (UBinder' c) where +instance RenameB UBinder' where renameB env ub cont = case ub of UBindSource sn -> cont env $ UBindSource sn UIgnore -> cont env UIgnore @@ -892,14 +837,14 @@ instance ProvesExt b => ProvesExt (WithSrcB b) where instance BindsNames b => BindsNames (WithSrcB b) where toScopeFrag (WithSrcB _ b) = toScopeFrag b -instance BindsAtMostOneName b r => BindsAtMostOneName (WithSrcB b) r where +instance BindsAtMostOneName b => BindsAtMostOneName (WithSrcB b) where WithSrcB _ b @> x = b @> x instance ProvesExt UAnnBinder where instance BindsNames UAnnBinder where toScopeFrag (UAnnBinder _ b _ _) = toScopeFrag b -instance BindsAtMostOneName UAnnBinder (AtomNameC CoreIR) where +instance BindsAtMostOneName UAnnBinder where UAnnBinder _ b _ _ @> x = b @> x instance GenericE (WithSrcE e) where @@ -930,7 +875,6 @@ instance Ord SourceBlock where instance Store SymbolicZeros instance Store PassName instance Store ModuleSourceName -instance Store (UVar n) instance Store (SourceNameDef n) instance Store (SourceMap n) instance Store TopNameDescription @@ -938,7 +882,7 @@ instance Store TopNameDescription instance Hashable ModuleSourceName instance Hashable TopNameDescription -deriving instance Show (UBinder' s n l) +deriving instance Show (UBinder' n l) deriving instance Show (UDataDefTrail n) deriving instance Show (ULamExpr n) deriving instance Show (UPiExpr n) @@ -1094,9 +1038,6 @@ instance PrettyE e => Pretty (SourceNameOr e n) where pretty (SourceName _ v) = pretty v pretty (InternalName _ v _) = pretty v -instance Pretty (SourceOrInternalName c n) where - pretty (SourceOrInternalName sn) = pretty sn - instance Pretty (ULamExpr n) where pretty = prettyFromPrettyPrec instance PrettyPrec (ULamExpr n) where prettyPrec (ULamExpr bs _ _ body) = atPrec LowestPrec $ @@ -1177,8 +1118,8 @@ instance Pretty Output where instance Pretty PassName where pretty x = pretty $ show x -instance Pretty (UBinder' c n l) where pretty = prettyFromPrettyPrec -instance PrettyPrec (UBinder' c n l) where +instance Pretty (UBinder' n l) where pretty = prettyFromPrettyPrec +instance PrettyPrec (UBinder' n l) where prettyPrec b = atPrec ArgPrec case b of UBindSource v -> pretty v UIgnore -> "_" diff --git a/src/lib/Types/Top.hs b/src/lib/Types/Top.hs index 048a19c7f..e3e58bf5e 100644 --- a/src/lib/Types/Top.hs +++ b/src/lib/Types/Top.hs @@ -23,7 +23,6 @@ import Foreign.Ptr import Name import Util (FileHash, SnocList (..)) -import IRVariants import PPrint import Types.Primitives @@ -33,17 +32,17 @@ import Types.Imp type TopBlock = TopLam -- used for nullary lambda type IsDestLam = Bool -data TopLam (r::IR) (n::S) = TopLam IsDestLam (PiType r n) (LamExpr r n) +data TopLam (n::S) = TopLam IsDestLam (PiType n) (LamExpr n) deriving (Show, Generic) -type STopLam = TopLam SimpIR -type CTopLam = TopLam CoreIR +type STopLam = TopLam +type CTopLam = TopLam data EvalStatus a = Waiting | Running | Finished a deriving (Show, Eq, Ord, Generic, Functor, Foldable, Traversable) type TopFunEvalStatus n = EvalStatus (TopFunLowerings n) data TopFun (n::S) = - DexTopFun (TopFunDef n) (TopLam SimpIR n) (TopFunEvalStatus n) + DexTopFun (TopFunDef n) (TopLam n) (TopFunEvalStatus n) | FFITopFun String IFunType deriving (Show, Generic) @@ -60,15 +59,15 @@ 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 (r::IR) (n::S) where - LetBound :: DeclBinding r n -> AtomBinding r n - MiscBound :: Type r n -> AtomBinding r n - SolverBound :: SolverBinding n -> AtomBinding CoreIR n - NoinlineFun :: CType n -> CAtom n -> AtomBinding CoreIR n - FFIFunBound :: CorePiType n -> TopFunName n -> AtomBinding CoreIR n +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 -deriving instance IRRep r => Show (AtomBinding r n) -deriving via WrapE (AtomBinding r) n instance IRRep r => Generic (AtomBinding r n) +deriving instance Show (AtomBinding n) +deriving via WrapE AtomBinding n instance Generic (AtomBinding n) data SolverBinding (n::S) = InfVarBound (CType n) @@ -78,7 +77,7 @@ data SolverBinding (n::S) = -- TODO: Use an IntMap newtype CustomRules (n::S) = - CustomRules { customRulesMap :: M.Map (AtomName CoreIR n) (AtomRules n) } + 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 @@ -167,8 +166,8 @@ data TopEnvUpdate n = | AddCustomRule (CAtomName n) (AtomRules n) | UpdateLoadedModules ModuleSourceName (ModuleName n) | UpdateLoadedObjects (FunObjCodeName n) NativeFunction - | FinishDictSpecialization (SpecDictName n) [TopLam SimpIR n] - | LowerDictSpecialization (SpecDictName n) [TopLam SimpIR n] + | 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) @@ -227,9 +226,9 @@ dynamicVarLinkMap dyvars = dyvars <&> \(v, ptr) -> (dynamicVarCName v, ptr) -- === Specialization and generalization === -type Generalized (r::IR) (e::E) (n::S) = (Abstracted r e n, [Atom r n]) -type Abstracted (r::IR) (e::E) = Abs (Nest (Binder r)) e -type AbsDict = Abstracted CoreIR (Dict CoreIR) +type Generalized (e::E) (n::S) = (Abstracted e n, [Atom n]) +type Abstracted (e::E) = Abs (Nest Binder) e +type AbsDict = Abstracted CDict data SpecializedDictDef n = SpecializedDict @@ -237,12 +236,12 @@ data SpecializedDictDef n = -- Methods (thunked if nullary), if they're available. -- We create specialized dict names during simplification, but we don't -- actually simplify/lower them until we return to TopLevel - (Maybe [TopLam SimpIR n]) + (Maybe [TopLam n]) deriving (Show, Generic) -- TODO: extend with AD-oriented specializations, backend-specific specializations etc. data SpecializationSpec (n::S) = - AppSpecialization (AtomVar CoreIR n) (Abstracted CoreIR (ListE CAtom) n) + AppSpecialization (AtomVar n) (Abstracted (ListE CAtom) n) deriving (Show, Generic) type Active = Bool @@ -251,62 +250,62 @@ data LinearizationSpec (n::S) = LinearizationSpec (TopFunName n) [Active] -- === bindings - static information we carry about a lexical scope === --- TODO: consider making this an open union via a typeable-like class -data Binding (c::C) (n::S) where - AtomNameBinding :: AtomBinding r n -> Binding (AtomNameC r) n - TyConBinding :: Maybe (TyConDef n) -> DotMethods n -> Binding TyConNameC n - DataConBinding :: TyConName n -> Int -> Binding DataConNameC n - ClassBinding :: ClassDef n -> Binding ClassNameC n - InstanceBinding :: InstanceDef n -> CorePiType n -> Binding InstanceNameC n - MethodBinding :: ClassName n -> Int -> Binding MethodNameC n - TopFunBinding :: TopFun n -> Binding TopFunNameC n - FunObjCodeBinding :: CFunction n -> Binding FunObjCodeNameC n - ModuleBinding :: Module n -> Binding ModuleNameC n +data Binding (n::S) where + AtomNameBinding :: AtomBinding n -> Binding n + TyConBinding :: Maybe (TyConDef n) -> DotMethods n -> Binding n + DataConBinding :: TyConName n -> Int -> Binding n + ClassBinding :: ClassDef n -> Binding n + InstanceBinding :: InstanceDef n -> CorePiType n -> Binding n + MethodBinding :: ClassName n -> Int -> Binding n + TopFunBinding :: TopFun n -> Binding n + FunObjCodeBinding :: CFunction n -> Binding n + ModuleBinding :: Module n -> Binding n -- TODO: add a case for abstracted pointers, as used in `ClosedImpFunction` - PtrBinding :: PtrType -> PtrLitVal -> Binding PtrNameC n - SpecializedDictBinding :: SpecializedDictDef n -> Binding SpecializedDictNameC n - ImpNameBinding :: BaseType -> Binding ImpNameC n + PtrBinding :: PtrType -> PtrLitVal -> Binding n + SpecializedDictBinding :: SpecializedDictDef n -> Binding n + ImpNameBinding :: BaseType -> Binding n + deriving (Show, Generic) -- === ToBinding === -atomBindingToBinding :: AtomBinding r n -> Binding (AtomNameC r) n +atomBindingToBinding :: AtomBinding n -> Binding n atomBindingToBinding b = AtomNameBinding b -bindingToAtomBinding :: Binding (AtomNameC r) n -> AtomBinding r n +bindingToAtomBinding :: Binding n -> AtomBinding n bindingToAtomBinding (AtomNameBinding b) = b -class (RenameE e, SinkableE e) => ToBinding (e::E) (c::C) | e -> c where - toBinding :: e n -> Binding c n +class (RenameE e, SinkableE e) => ToBinding (e::E) where + toBinding :: e n -> Binding n -instance Color c => ToBinding (Binding c) c where +instance ToBinding Binding where toBinding = id -instance IRRep r => ToBinding (AtomBinding r) (AtomNameC r) where +instance ToBinding AtomBinding where toBinding = atomBindingToBinding -instance IRRep r => ToBinding (DeclBinding r) (AtomNameC r) where +instance ToBinding DeclBinding where toBinding = toBinding . LetBound -instance IRRep r => ToBinding (Type r) (AtomNameC r) where +instance ToBinding Type where toBinding = toBinding . MiscBound -instance ToBinding SolverBinding (AtomNameC CoreIR) where +instance ToBinding SolverBinding where toBinding = toBinding . SolverBound -instance IRRep r => ToBinding (IxType r) (AtomNameC r) where +instance ToBinding IxType where toBinding (IxType t _) = toBinding t -instance (ToBinding e1 c, ToBinding e2 c) => ToBinding (EitherE e1 e2) c where +instance (ToBinding e1, ToBinding e2) => ToBinding (EitherE e1 e2) where toBinding (LeftE e) = toBinding e toBinding (RightE e) = toBinding e -instance ToBindersAbs (TopLam r) (Expr r) r where +instance ToBindersAbs TopLam Expr where toAbs (TopLam _ _ lam) = toAbs lam -- === GenericE, GenericB === instance GenericE SpecializedDictDef where - type RepE SpecializedDictDef = AbsDict `PairE` MaybeE (ListE (TopLam SimpIR)) + type RepE SpecializedDictDef = AbsDict `PairE` MaybeE (ListE STopLam) fromE (SpecializedDict ab methods) = ab `PairE` methods' where methods' = case methods of Just xs -> LeftE (ListE xs) Nothing -> RightE UnitE @@ -367,7 +366,7 @@ instance AlphaEqE AtomRules instance RenameE AtomRules instance GenericE CustomRules where - type RepE CustomRules = ListE (PairE (AtomName CoreIR) AtomRules) + 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 @@ -431,44 +430,44 @@ instance AlphaEqE SynthCandidates instance AlphaHashableE SynthCandidates instance RenameE SynthCandidates -instance IRRep r => GenericE (AtomBinding r) where - type RepE (AtomBinding r) = +instance GenericE AtomBinding where + type RepE AtomBinding = EitherE2 (EitherE3 - (DeclBinding r) -- LetBound - (Type r) -- MiscBound - (WhenCore r SolverBinding) -- SolverBound + DeclBinding -- LetBound + Type -- MiscBound + (SolverBinding) -- SolverBound ) (EitherE2 - (WhenCore r (PairE CType CAtom)) -- NoinlineFun - (WhenCore r (CorePiType `PairE` TopFunName)) -- FFIFunBound + ((PairE CType CAtom)) -- NoinlineFun + ((CorePiType `PairE` TopFunName)) -- FFIFunBound ) fromE = \case LetBound x -> Case0 $ Case0 x MiscBound x -> Case0 $ Case1 x - SolverBound x -> Case0 $ Case2 $ WhenIRE x - NoinlineFun t x -> Case1 $ Case0 $ WhenIRE $ PairE t x - FFIFunBound t v -> Case1 $ Case1 $ WhenIRE $ t `PairE` v + SolverBound x -> Case0 $ Case2 $ x + NoinlineFun t x -> Case1 $ Case0 $ PairE t x + FFIFunBound t v -> Case1 $ Case1 $ t `PairE` v {-# INLINE fromE #-} toE = \case Case0 x' -> case x' of - Case0 x -> LetBound x - Case1 x -> MiscBound x - Case2 (WhenIRE x) -> SolverBound x + Case0 x -> LetBound x + Case1 x -> MiscBound x + Case2 x -> SolverBound x _ -> error "impossible" Case1 x' -> case x' of - Case0 (WhenIRE (PairE t x)) -> NoinlineFun t x - Case1 (WhenIRE (ty `PairE` v)) -> FFIFunBound ty v + Case0 (PairE t x) -> NoinlineFun t x + Case1 (ty `PairE` v) -> FFIFunBound ty v _ -> error "impossible" _ -> error "impossible" {-# INLINE toE #-} -instance IRRep r => SinkableE (AtomBinding r) -instance IRRep r => HoistableE (AtomBinding r) -instance IRRep r => RenameE (AtomBinding r) -instance IRRep r => AlphaEqE (AtomBinding r) -instance IRRep r => AlphaHashableE (AtomBinding r) +instance SinkableE AtomBinding +instance HoistableE AtomBinding +instance RenameE AtomBinding +instance AlphaEqE AtomBinding +instance AlphaHashableE AtomBinding instance GenericE TopFunDef where type RepE TopFunDef = EitherE3 SpecializationSpec LinearizationSpec LinearizationSpec @@ -490,22 +489,22 @@ instance RenameE TopFunDef instance AlphaEqE TopFunDef instance AlphaHashableE TopFunDef -instance IRRep r => GenericE (TopLam r) where - type RepE (TopLam r) = LiftE Bool `PairE` PiType r `PairE` LamExpr r +instance GenericE TopLam where + type RepE TopLam = LiftE Bool `PairE` PiType `PairE` LamExpr fromE (TopLam d x y) = LiftE d `PairE` x `PairE` y {-# INLINE fromE #-} toE (LiftE d `PairE` x `PairE` y) = TopLam d x y {-# INLINE toE #-} -instance IRRep r => SinkableE (TopLam r) -instance IRRep r => HoistableE (TopLam r) -instance IRRep r => RenameE (TopLam r) -instance IRRep r => AlphaEqE (TopLam r) -instance IRRep r => AlphaHashableE (TopLam r) +instance SinkableE TopLam +instance HoistableE TopLam +instance RenameE TopLam +instance AlphaEqE TopLam +instance AlphaHashableE TopLam instance GenericE TopFun where type RepE TopFun = EitherE - (TopFunDef `PairE` TopLam SimpIR `PairE` ComposeE EvalStatus TopFunLowerings) + (TopFunDef `PairE` STopLam `PairE` ComposeE EvalStatus TopFunLowerings) (LiftE (String, IFunType)) fromE = \case DexTopFun def lam status -> LeftE (def `PairE` lam `PairE` ComposeE status) @@ -524,7 +523,7 @@ instance AlphaHashableE TopFun instance GenericE SpecializationSpec where type RepE SpecializationSpec = - PairE (AtomVar CoreIR) (Abs (Nest (Binder CoreIR)) (ListE CAtom)) + PairE AtomVar (Abs (Nest Binder) (ListE CAtom)) fromE (AppSpecialization fname (Abs bs args)) = PairE fname (Abs bs args) {-# INLINE fromE #-} toE (PairE fname (Abs bs args)) = AppSpecialization fname (Abs bs args) @@ -576,63 +575,59 @@ instance RenameE SolverBinding instance AlphaEqE SolverBinding instance AlphaHashableE SolverBinding -instance GenericE (Binding c) where - type RepE (Binding c) = +instance GenericE Binding where + type RepE Binding = EitherE3 (EitherE6 - (WhenAtomName c AtomBinding) - (WhenC TyConNameC c (MaybeE TyConDef `PairE` DotMethods)) - (WhenC DataConNameC c (TyConName `PairE` LiftE Int)) - (WhenC ClassNameC c (ClassDef)) - (WhenC InstanceNameC c (InstanceDef `PairE` CorePiType)) - (WhenC MethodNameC c (ClassName `PairE` LiftE Int))) + (AtomBinding) + (MaybeE TyConDef `PairE` DotMethods) + (TyConName `PairE` LiftE Int) + (ClassDef) + (InstanceDef `PairE` CorePiType) + (ClassName `PairE` LiftE Int)) (EitherE4 - (WhenC TopFunNameC c (TopFun)) - (WhenC FunObjCodeNameC c (CFunction)) - (WhenC ModuleNameC c (Module)) - (WhenC PtrNameC c (LiftE (PtrType, PtrLitVal)))) + (TopFun) + (CFunction) + (Module) + (LiftE (PtrType, PtrLitVal))) (EitherE2 - (WhenC SpecializedDictNameC c (SpecializedDictDef)) - (WhenC ImpNameC c (LiftE BaseType))) + (SpecializedDictDef) + (LiftE BaseType)) fromE = \case - AtomNameBinding binding -> Case0 $ Case0 $ WhenAtomName binding - TyConBinding dataDef methods -> Case0 $ Case1 $ WhenC $ toMaybeE dataDef `PairE` methods - DataConBinding dataDefName idx -> Case0 $ Case2 $ WhenC $ dataDefName `PairE` LiftE idx - ClassBinding classDef -> Case0 $ Case3 $ WhenC $ classDef - InstanceBinding instanceDef ty -> Case0 $ Case4 $ WhenC $ instanceDef `PairE` ty - MethodBinding className idx -> Case0 $ Case5 $ WhenC $ className `PairE` LiftE idx - TopFunBinding fun -> Case1 $ Case0 $ WhenC $ fun - FunObjCodeBinding cFun -> Case1 $ Case1 $ WhenC $ cFun - ModuleBinding m -> Case1 $ Case2 $ WhenC $ m - PtrBinding ty p -> Case1 $ Case3 $ WhenC $ LiftE (ty,p) - SpecializedDictBinding def -> Case2 $ Case0 $ WhenC $ def - ImpNameBinding ty -> Case2 $ Case1 $ WhenC $ LiftE ty + AtomNameBinding binding -> Case0 $ Case0 $ binding + TyConBinding dataDef methods -> Case0 $ Case1 $ toMaybeE dataDef `PairE` methods + DataConBinding dataDefName idx -> Case0 $ Case2 $ dataDefName `PairE` LiftE idx + ClassBinding classDef -> Case0 $ Case3 $ classDef + InstanceBinding instanceDef ty -> Case0 $ Case4 $ instanceDef `PairE` ty + MethodBinding className idx -> Case0 $ Case5 $ className `PairE` LiftE idx + TopFunBinding fun -> Case1 $ Case0 $ fun + FunObjCodeBinding cFun -> Case1 $ Case1 $ cFun + ModuleBinding m -> Case1 $ Case2 $ m + PtrBinding ty p -> Case1 $ Case3 $ LiftE (ty,p) + SpecializedDictBinding def -> Case2 $ Case0 $ def + ImpNameBinding ty -> Case2 $ Case1 $ LiftE ty {-# INLINE fromE #-} toE = \case - Case0 (Case0 (WhenAtomName binding)) -> AtomNameBinding binding - Case0 (Case1 (WhenC (def `PairE` methods))) -> TyConBinding (fromMaybeE def) methods - Case0 (Case2 (WhenC (n `PairE` LiftE idx))) -> DataConBinding n idx - Case0 (Case3 (WhenC (classDef))) -> ClassBinding classDef - Case0 (Case4 (WhenC (instanceDef `PairE` ty))) -> InstanceBinding instanceDef ty - Case0 (Case5 (WhenC ((n `PairE` LiftE i)))) -> MethodBinding n i - Case1 (Case0 (WhenC (fun))) -> TopFunBinding fun - Case1 (Case1 (WhenC (f))) -> FunObjCodeBinding f - Case1 (Case2 (WhenC (m))) -> ModuleBinding m - Case1 (Case3 (WhenC ((LiftE (ty,p))))) -> PtrBinding ty p - Case2 (Case0 (WhenC (def))) -> SpecializedDictBinding def - Case2 (Case1 (WhenC ((LiftE ty)))) -> ImpNameBinding ty + Case0 (Case0 binding) -> AtomNameBinding binding + Case0 (Case1 (def `PairE` methods)) -> TyConBinding (fromMaybeE def) methods + Case0 (Case2 (n `PairE` LiftE idx)) -> DataConBinding n idx + Case0 (Case3 classDef) -> ClassBinding classDef + Case0 (Case4 (instanceDef `PairE` ty)) -> InstanceBinding instanceDef ty + Case0 (Case5 (n `PairE` LiftE i)) -> MethodBinding n i + Case1 (Case0 fun) -> TopFunBinding fun + Case1 (Case1 f) -> FunObjCodeBinding f + Case1 (Case2 m) -> ModuleBinding m + Case1 (Case3 (LiftE (ty,p))) -> PtrBinding ty p + Case2 (Case0 def) -> SpecializedDictBinding def + Case2 (Case1 (LiftE ty)) -> ImpNameBinding ty _ -> error "impossible" {-# INLINE toE #-} -deriving via WrapE (Binding c) n instance Generic (Binding c n) -instance SinkableV Binding -instance HoistableV Binding -instance RenameV Binding -instance Color c => SinkableE (Binding c) -instance Color c => HoistableE (Binding c) -instance Color c => RenameE (Binding c) +instance SinkableE Binding +instance HoistableE Binding +instance RenameE Binding instance Semigroup (SynthCandidates n) where SynthCandidates xs ys <> SynthCandidates xs' ys' = @@ -660,8 +655,8 @@ instance GenericE TopEnvUpdate where {- UpdateLoadedModules -} (LiftE ModuleSourceName `PairE` ModuleName) {- UpdateLoadedObjects -} (FunObjCodeName `PairE` LiftE NativeFunction) ) ( EitherE6 - {- FinishDictSpecialization -} (SpecDictName `PairE` ListE (TopLam SimpIR)) - {- LowerDictSpecialization -} (SpecDictName `PairE` ListE (TopLam SimpIR)) + {- FinishDictSpecialization -} (SpecDictName `PairE` ListE STopLam) + {- LowerDictSpecialization -} (SpecDictName `PairE` ListE STopLam) {- UpdateTopFunEvalStatus -} (TopFunName `PairE` ComposeE EvalStatus TopFunLowerings) {- UpdateInstanceDef -} (InstanceName `PairE` InstanceDef) {- UpdateTyConDef -} (TyConName `PairE` TyConDef) @@ -784,12 +779,12 @@ applyUpdate e = \case let TyConBinding def methods = lookupEnvPure e name updateEnv name (TyConBinding def (methods <> DotMethods (M.singleton sn x))) e -updateEnv :: Color c => Name c n -> Binding c n -> TopEnv n -> TopEnv n +updateEnv :: Name n -> Binding n -> TopEnv n -> TopEnv n updateEnv v rhs env = env { envDefs = RecSubst $ updateSubstFrag v rhs bs } where (RecSubst bs) = envDefs env -lookupEnvPure :: Color c => TopEnv n -> Name c n -> Binding c n +lookupEnvPure :: TopEnv n -> Name n -> Binding n lookupEnvPure env v = lookupTerminalSubstFrag (fromRecSubst $ envDefs $ env) v instance GenericE Module where @@ -934,12 +929,9 @@ instance Pretty (SolverBinding n) where pretty (SkolemBound ty) = "Skolem variable of type:" <+> pretty ty pretty (DictBound ty) = "Dictionary variable of type:" <+> pretty ty -instance Pretty (Binding c n) where +instance Pretty (Binding n) where pretty b = case b of - -- using `unsafeCoerceIRE` here because otherwise we don't have `IRRep` - -- TODO: can we avoid printing needing IRRep? Presumably it's related to - -- manipulating sets or something, which relies on Eq/Ord, which relies on renaming. - AtomNameBinding info -> "Atom name:" <+> pretty (unsafeCoerceIRE @CoreIR info) + AtomNameBinding info -> "Atom name:" <+> pretty info TyConBinding dataDef _ -> "Type constructor: " <+> pretty dataDef DataConBinding tyConName idx -> "Data constructor:" <+> pretty tyConName <+> "Constructor index:" <+> pretty idx @@ -994,10 +986,10 @@ instance Pretty (TopFun n) where <> hardline <+> "lowering:" <+> pretty lowering FFITopFun f _ -> pretty f -instance IRRep r => Pretty (TopLam r n) where +instance Pretty (TopLam n) where pretty (TopLam _ _ lam) = pretty lam -instance IRRep r => Pretty (AtomBinding r n) where +instance Pretty (AtomBinding n) where pretty binding = case binding of LetBound b -> pretty b MiscBound t -> pretty t @@ -1012,8 +1004,8 @@ instance Pretty (SpecializationSpec n) where instance Hashable a => Hashable (EvalStatus a) instance Store (SolverBinding n) -instance IRRep r => Store (AtomBinding r n) -instance IRRep r => Store (TopLam r n) +instance Store (AtomBinding n) +instance Store (TopLam n) instance Store (SynthCandidates n) instance Store (Module n) instance Store (ImportStatus n) @@ -1021,7 +1013,7 @@ instance Store (TopFunLowerings n) instance Store a => Store (EvalStatus a) instance Store (TopFun n) instance Store (TopFunDef n) -instance Color c => Store (Binding c n) +instance Store (Binding n) instance Store (ModuleEnv n) instance Store (SerializedEnv n) instance Store (AtomRules n)