From c7520481976ba4cae214cf13e3692b2e11b405c8 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Fri, 24 Feb 2023 12:13:22 +0000 Subject: [PATCH 01/11] dummy: --- dummy | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 dummy diff --git a/dummy b/dummy new file mode 100644 index 00000000..e69de29b From 231d81f89c38d079dcd64fd00bc154ad9103b2c8 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Wed, 1 Mar 2023 18:25:04 +0000 Subject: [PATCH 02/11] new: infoless monad instance --- .../src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs index f5f5cb03..c6445f36 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs @@ -7,9 +7,11 @@ module LambdaBuffers.Compiler.ProtoCompat.InfoLess ( withInfoLess, withInfoLessF, mkInfoLess, - InfoLessC, + InfoLessC (infoLessId), ) where +import Control.Monad (join) +import Control.Monad.Identity (Identity (Identity)) import Data.Bifunctor (Bifunctor (bimap)) import Data.Default (Default (def)) import Data.Map qualified as M @@ -66,6 +68,8 @@ import LambdaBuffers.Compiler.ProtoCompat.Types ( newtype InfoLess a = InfoLess {unsafeInfoLess :: a} deriving stock (Show, Eq, Ord) deriving stock (Functor, Traversable, Foldable) + deriving (Applicative) via Identity + deriving (Monad) via Identity {- | SourceInfo Less ID. A TypeClass that provides id for types with SourceInfo - where SI is defaulted - therefore ignored. Can only be derived. @@ -90,6 +94,9 @@ withInfoLess (InfoLess a) f = f . unsafeInfoLess . mkInfoLess $ a withInfoLessF :: forall f {a} {b}. InfoLessC a => InfoLess a -> (a -> f b) -> f b withInfoLessF (InfoLess a) f = f . unsafeInfoLess . mkInfoLess $ a +instance InfoLessC a => InfoLessC (InfoLess a) where + infoLessId = join . mkInfoLess + instance InfoLessC a => InfoLessC [a] where infoLessId = fmap infoLessId From 46fe3b9e08fd0e830b047de79ab180cdfd475e64 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Thu, 2 Mar 2023 14:08:33 +0000 Subject: [PATCH 03/11] update: some minor refactoring --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 153 +++---- .../Compiler/KindCheck/Derivation.hs | 18 +- .../Compiler/KindCheck/Inference.hs | 378 +++++++++--------- .../LambdaBuffers/Compiler/KindCheck/Kind.hs | 12 +- .../LambdaBuffers/Compiler/KindCheck/Type.hs | 76 +++- .../Compiler/ProtoCompat/FromProto.hs | 2 + .../Compiler/ProtoCompat/Types.hs | 15 +- lambda-buffers-proto/compiler.proto | 6 +- 8 files changed, 378 insertions(+), 282 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 3c824f29..6f6062ab 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -9,7 +9,8 @@ module LambdaBuffers.Compiler.KindCheck ( foldWithArrowToType, ) where -import Control.Lens (Getter, to, view, (&), (.~), (^.)) +import Control.Lens (view, (&), (.~), (^.)) +import Control.Lens.Iso (withIso) import Control.Monad (void) import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run) import Control.Monad.Freer.Error (Error, runError, throwError) @@ -18,11 +19,16 @@ import Control.Monad.Freer.TH (makeEffect) import Data.Default (Default (def)) import Data.Foldable (Foldable (toList), traverse_) import Data.Map qualified as M - -import LambdaBuffers.Compiler.KindCheck.Derivation (Context, context) +import LambdaBuffers.Compiler.KindCheck.Derivation (Context, constraintContext, context) +import LambdaBuffers.Compiler.KindCheck.Inference (protoKind2Kind) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I -import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)), kind2ProtoKind) -import LambdaBuffers.Compiler.KindCheck.Type (Variable (QualifiedTyRef, TyVar)) +import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:))) +import LambdaBuffers.Compiler.KindCheck.Type ( + Variable (QualifiedConstraint, QualifiedTyRef, TyVar), + ftrISOqtr, + ltrISOqtr, + qTyRef'moduleName, + ) import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC @@ -50,9 +56,8 @@ makeEffect ''GlobalCheck -- | Interactions that happen at the level of the data ModuleCheck a where -- Module KCTypeDefinition :: PC.ModuleName -> Context -> PC.TyDef -> ModuleCheck Kind + KCClassInstance :: PC.ModuleName -> Context -> PC.ClassDef -> ModuleCheck () --- NOTE(cstml & gnumonik): Lets reach consensus on these - Note(1). --- KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck () -- KCClass :: Context -> P.ClassDef -> ModuleCheck () makeEffect ''ModuleCheck @@ -60,8 +65,11 @@ makeEffect ''ModuleCheck data KindCheck a where GetSpecifiedKind :: PC.ModuleName -> PC.TyDef -> KindCheck Kind InferTypeKind :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind + CheckClassDefinition :: PC.ModuleName -> PC.ClassDef -> Context -> KindCheck () CheckKindConsistency :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind +-- CheckClassInstance :: PC.ModuleName -> KindCheck Kind + makeEffect ''KindCheck -------------------------------------------------------------------------------- @@ -113,57 +121,48 @@ localStrategy = reinterpret $ \case desiredK <- getSpecifiedKind modName tyDef k <- inferTypeKind modName tyDef ctx desiredK checkKindConsistency modName tyDef ctx k + KCClassInstance modName ctx classDef -> do + _ <- checkClassDefinition modName classDef ctx + pure () runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a runKindCheck = interpret $ \case - InferTypeKind modName tyDef ctx k -> - either (handleErr modName tyDef) pure $ I.infer ctx tyDef k modName + InferTypeKind modName tyDef ctx _k -> + either (handleErr modName tyDef) pure $ I.infer ctx tyDef modName CheckKindConsistency modName tyDef ctx k -> runReader modName $ resolveKindConsistency tyDef ctx k GetSpecifiedKind modName tyDef -> fmap snd $ runReader modName $ tyDef2NameAndKind tyDef + CheckClassDefinition modName classDef ctx -> + either (handleErr2 modName classDef) pure $ I.runClassDefCheck ctx modName classDef where + handleErr2 = undefined + handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b handleErr modName td = \case - I.InferUnboundTermErr uA -> do - case uA of - QualifiedTyRef fr -> - if (fr ^. #moduleName) == modName - then -- We're looking at the local module. - - throwError - . PC.CompKindCheckError - $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. foreignRef2LocalRef) modName - else -- We're looking at a foreign module. - - throwError - . PC.CompKindCheckError - $ PC.UnboundTyRefError td (PC.ForeignI fr) modName + I.InferUnboundTermErr ut -> + case ut of + QualifiedTyRef qtr -> do + if qtr ^. qTyRef'moduleName == modName + then do + -- We're looking at the local module. + let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr + let err = PC.UnboundTyRefError td localRef modName + throwError . PC.CompKindCheckError $ err + else do + -- We're looking at a foreign module. + let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr + throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td foreignRef modName TyVar tv -> - throwError - . PC.CompKindCheckError - $ PC.UnboundTyVarError td (PC.TyVar tv) modName - I.InferUnifyTermErr (I.Constraint (k1, k2)) -> - throwError - . PC.CompKindCheckError - $ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName + throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName + QualifiedConstraint _ -> error "NOTE(cstml): FIXME." + I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do + err <- PC.IncorrectApplicationError td <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName + throwError $ PC.CompKindCheckError err I.InferRecursiveSubstitutionErr _ -> - throwError - . PC.CompKindCheckError - $ PC.RecursiveKindError td modName + throwError . PC.CompKindCheckError $ PC.RecursiveKindError td modName I.InferImpossibleErr t -> - throwError $ - PC.InternalError t - - foreignRef2LocalRef :: Getter PC.ForeignRef PC.LocalRef - foreignRef2LocalRef = - to - ( \fr -> - PC.LocalRef - { tyName = fr ^. #tyName - , sourceInfo = fr ^. #sourceInfo - } - ) + throwError $ PC.InternalError t -------------------------------------------------------------------------------- -- Resolvers @@ -183,24 +182,28 @@ resolveKindConsistency tyDef _ctx inferredKind = do guard t i d | i == d = pure () | otherwise = do - mn <- ask - throwError - . PC.CompKindCheckError - $ PC.InconsistentTypeError t (kind2ProtoKind i) (kind2ProtoKind d) mn + err <- PC.InconsistentTypeError t <$> kind2ProtoKind i <*> kind2ProtoKind d <*> ask + throwError $ PC.CompKindCheckError err -------------------------------------------------------------------------------- -- Context Creation -- | Resolver function for the context creation. There is a guarantee from ProtoCompat that the input is sanitised. resolveCreateContext :: forall effs. PC.CompilerInput -> Eff effs Context -resolveCreateContext ci = - mconcat <$> traverse module2Context (toList $ ci ^. #modules) +resolveCreateContext = fmap mconcat . traverse module2Context . toList . view #modules module2Context :: forall effs. PC.Module -> Eff effs Context module2Context m = do let typeDefinitions = toList $ m ^. #typeDefs - ctxs <- runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions - pure $ mconcat ctxs + let classDefinitions = toList $ m ^. #classDefs + -- Context built from type definitions. + typeDefCtx <- fmap mconcat . runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions + -- Context built from class definitions. + classDefCtx <- fmap mconcat . runReader (m ^. #moduleName) $ traverse classDef2Context classDefinitions + return $ typeDefCtx <> classDefCtx + +-------------------------------------------------------------------------------- +-- Type Definition Based Context Building. -- | Creates a Context entry from one type definition. tyDef2Context :: @@ -219,11 +222,11 @@ tyDef2NameAndKind :: Eff effs (InfoLess Variable, Kind) tyDef2NameAndKind tyDef = do curModName <- ask - - -- InfoLess name - the SourceInfo doesn't matter therefore it is defaulted. + -- InfoLess Qualified name - the SourceInfo doesn't matter therefore it is defaulted. let name = QualifiedTyRef - . view (PC.localRef2ForeignRef curModName) + . withIso ltrISOqtr const + . (,curModName) $ PC.LocalRef (tyDef ^. #tyName) def k = tyAbsLHS2Kind (tyDef ^. #tyAbs) @@ -231,7 +234,33 @@ tyDef2NameAndKind tyDef = do pure (mkInfoLess name, k) tyAbsLHS2Kind :: PC.TyAbs -> Kind -tyAbsLHS2Kind tyAbs = foldWithArrowToType $ pKind2Kind . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs) +tyAbsLHS2Kind tyAbs = foldWithArrowToType $ tyArg2Kind <$> toList (tyAbs ^. #tyArgs) + +tyArg2Kind :: PC.TyArg -> Kind +tyArg2Kind = protoKind2Kind . view #argKind + +-------------------------------------------------------------------------------- +-- Class Definition Based Context Building. + +--- | Convert from internal Kind to Proto Kind. +kind2ProtoKind :: forall effs. Member Err effs => Kind -> Eff effs PC.Kind +kind2ProtoKind = \case + k1 :->: k2 -> fmap PC.Kind $ PC.KindArrow <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 + KType -> pure . PC.Kind . PC.KindRef $ PC.KType + KVar _ -> pure . PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen. + KConstraint -> pure . PC.Kind . PC.KindRef $ PC.KConstraint + +-------------------------------------------------------------------------------- +-- Class Definition Based Context Building. + +classDef2Context :: forall effs. PC.ClassDef -> Eff effs Context +classDef2Context cDef = do + let className = mkInfoLess . view #className $ cDef + let classArg = tyArg2Kind . view #classArgs $ cDef + pure $ mempty & constraintContext .~ M.singleton className classArg + +-------------------------------------------------------------------------------- +-- utilities {- | Folds kinds and appends them to a Kind result type. In essence creates a curried function with a Type final kind. @@ -250,13 +279,3 @@ foldWithArrowToType = foldWithArrowToKind KType foldWithArrowToKind :: Kind -> [Kind] -> Kind foldWithArrowToKind = foldr (:->:) - --------------------------------------------------------------------------------- --- To Kind Conversion functions - -pKind2Kind :: PC.Kind -> Kind -pKind2Kind k = - case k ^. #kind of - PC.KindRef PC.KType -> KType - PC.KindArrow l r -> pKind2Kind l :->: pKind2Kind r - PC.KindRef PC.KUnspecified -> KType -- (for now) defaulting unspecified kinds to Type diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs index 03b94ba2..f496ab43 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs @@ -1,5 +1,6 @@ module LambdaBuffers.Compiler.KindCheck.Derivation ( Derivation (Axiom, Abstraction, Application, Implication), + QClassName (QClassName), d'type, d'kind, Judgement (Judgement), @@ -10,12 +11,15 @@ module LambdaBuffers.Compiler.KindCheck.Derivation ( context, addContext, getAllContext, + constraintContext, ) where import Control.Lens (Lens', lens, makeLenses, (&), (.~), (^.)) +import Control.Lens.Operators ((%~)) import Data.Map qualified as M import LambdaBuffers.Compiler.KindCheck.Kind (Kind) import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable) +import LambdaBuffers.Compiler.ProtoCompat qualified as PC import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess) import Prettyprinter ( Doc, @@ -33,9 +37,13 @@ import Prettyprinter ( (<+>), ) +-- | Qualified Class Name. +data QClassName = QClassName + data Context = Context { _context :: M.Map (InfoLess Variable) Kind , _addContext :: M.Map (InfoLess Variable) Kind + , _constraintContext :: M.Map (InfoLess PC.ClassName) Kind } deriving stock (Show, Eq) @@ -50,12 +58,16 @@ instance Pretty Context where setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t) instance Semigroup Context where - (Context a1 b1) <> (Context a2 b2) = Context (a1 <> a2) (b1 <> b2) + c1 <> c2 = + c1 + & context %~ (<> c2 ^. context) + & addContext %~ (<> c2 ^. addContext) + & constraintContext %~ (<> c2 ^. constraintContext) instance Monoid Context where - mempty = Context mempty mempty + mempty = Context mempty mempty mempty --- | Utility to unify the two. +-- | Utility to unify the two T. getAllContext :: Context -> M.Map (InfoLess Variable) Kind getAllContext c = c ^. context <> c ^. addContext diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 99e99237..db370655 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -3,27 +3,33 @@ -- This pragma^ is needed due to redundant constraint in Getters and Eff. module LambdaBuffers.Compiler.KindCheck.Inference ( + -- * API functions + infer, + runClassDefCheck, + + -- * Types Kind (..), Context (..), Atom, Type (..), - infer, DeriveM, DeriveEff, - context, - addContext, InferErr (..), Constraint (..), + + -- * Utility functions + protoKind2Kind, ) where -import Control.Lens (view, (%~), (&), (.~), (^.)) +import Control.Lens ((%~), (&), (.~), (^.)) +import Control.Lens.Iso (withIso) +import Control.Monad (void) import Control.Monad.Freer (Eff, Member, Members, run) import Control.Monad.Freer.Error (Error, runError, throwError) import Control.Monad.Freer.Reader (Reader, ask, asks, local, runReader) import Control.Monad.Freer.State (State, evalState, get, put) import Control.Monad.Freer.Writer (Writer, runWriter, tell) -import Data.Bifunctor (Bifunctor (second)) -import Data.Foldable (foldrM) +import Data.Foldable (foldrM, traverse_) import Data.Map qualified as M import Data.Text qualified as T import LambdaBuffers.Compiler.KindCheck.Derivation ( @@ -35,13 +41,14 @@ import LambdaBuffers.Compiler.KindCheck.Derivation ( d'kind, d'type, ) -import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KType, KVar, (:->:))) +import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( Type (Abs, App, Constructor, Opaque, Product, Sum, UnitT, Var, VoidT), Variable (QualifiedTyRef, TyVar), + ftrISOqtr, + ltrISOqtr, ) import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess) -import LambdaBuffers.Compiler.ProtoCompat.Types (localRef2ForeignRef) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), (<+>)) @@ -79,7 +86,6 @@ type Derive a = forall effs. Members '[ Reader Context - , Reader Kind , Reader PC.ModuleName , State DerivationContext , Writer [Constraint] @@ -92,180 +98,183 @@ type Derive a = -- Runners -- | Run derivation builder - not unified yet. -runDerive :: - Context -> - PC.TyAbs -> - Kind -> - PC.ModuleName -> - Either InferErr (Derivation, [Constraint]) -runDerive ctx t k localMod = - run $ - runError $ - runWriter $ - evalState (DC startAtom) $ - runReader ctx $ - runReader k $ - runReader localMod $ - derive t - -infer :: - Context -> - PC.TyDef -> - Kind -> - PC.ModuleName -> - Either InferErr Kind -infer ctx t k localMod = do - (d, c) <- runDerive (defContext <> ctx) (t ^. #tyAbs) k localMod +runDerive :: Context -> PC.ModuleName -> Derive a -> Either InferErr (a, [Constraint]) +runDerive ctx localMod = + run . runError . runWriter . evalState (DC startAtom) . runReader ctx . runReader localMod + +infer :: Context -> PC.TyDef -> PC.ModuleName -> Either InferErr Kind +infer ctx t localMod = do + (d, c) <- runDerive ctx localMod (deriveTyAbs (t ^. #tyAbs)) s <- runUnify' c let res = foldl (flip substitute) d s pure $ res ^. d'kind --- | Default KC Context. -defContext :: Context -defContext = mempty - -------------------------------------------------------------------------------- -- Implementation --- | Creates the derivation -derive :: PC.TyAbs -> Derive Derivation -derive x = deriveTyAbs x - where - fresh :: Derive Atom - fresh = do - DC a <- get - put (DC $ a + 1) - pure a - - deriveTyAbs :: PC.TyAbs -> Derive Derivation - deriveTyAbs tyabs = do - case M.toList (tyabs ^. #tyArgs) of - [] -> deriveTyBody (x ^. #tyBody) - a@(n, ar) : as -> do - let argK = protoKind2Kind (ar ^. #argKind) - bodyK <- KVar <$> fresh - ctx <- ask - - let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) argK) - let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a - let restAbs = tyabs & #tyArgs .~ M.fromList as - - restF <- local (const newContext) $ deriveTyAbs restAbs - - let uK = restF ^. d'kind - tell [Constraint (bodyK, uK)] - pure $ Abstraction (Judgement ctx (Abs newAbs) (argK :->: bodyK)) restF - - deriveTyBody :: PC.TyBody -> Derive Derivation - deriveTyBody = \case - PC.OpaqueI si -> do - ctx <- ask - pure $ Axiom $ Judgement ctx (Opaque si) KType - PC.SumI s -> deriveSum s - - deriveSum :: PC.Sum -> Derive Derivation - deriveSum s = do - case M.toList (s ^. #constructors) of - [] -> voidDerivation - c : cs -> do - dc <- deriveConstructor $ snd c - restDc <- deriveSum $ s & #constructors .~ M.fromList cs - sumDerivation dc restDc - - deriveConstructor :: PC.Constructor -> Derive Derivation - deriveConstructor c = do - ctx <- ask - d <- deriveProduct (c ^. #product) - tell $ Constraint <$> [(KType, d ^. d'kind)] - pure $ Implication (Judgement ctx (Constructor c) (d ^. d'kind)) d - - deriveProduct :: PC.Product -> Derive Derivation - deriveProduct = \case - PC.RecordI r -> deriveRecord r - PC.TupleI t -> deriveTuple t - - deriveRecord :: PC.Record -> Derive Derivation - deriveRecord r = do - case M.toList (r ^. #fields) of - [] -> unitDerivation - f : fs -> do - d1 <- deriveField $ snd f - d2 <- deriveRecord $ r & #fields .~ M.fromList fs - productDerivation d1 d2 - - deriveField :: PC.Field -> Derive Derivation - deriveField f = deriveTy $ f ^. #fieldTy - - deriveTy :: PC.Ty -> Derive Derivation - deriveTy = \case - PC.TyVarI tv -> deriveTyVar tv - PC.TyAppI ta -> deriveTyApp ta - PC.TyRefI tr -> deriveTyRef tr - - deriveTyRef :: PC.TyRef -> Derive Derivation - deriveTyRef = \case - PC.LocalI r -> do - localModule <- ask - let ty = QualifiedTyRef . view (localRef2ForeignRef localModule) $ r - v <- getKind ty - c <- ask - pure . Axiom $ Judgement c (Var ty) v - PC.ForeignI r -> do - let ty = QualifiedTyRef r - v <- getKind ty - c <- ask - pure . Axiom $ Judgement c (Var ty) v - - deriveTyVar :: PC.TyVar -> Derive Derivation - deriveTyVar tv = do - let varName = tv ^. #varName - v <- getKind $ TyVar varName - c <- ask - pure . Axiom $ Judgement c (Var $ TyVar varName) v - - deriveTyApp :: PC.TyApp -> Derive Derivation - deriveTyApp ap = do - f <- deriveTy (ap ^. #tyFunc) - args <- deriveTy `traverse` (ap ^. #tyArgs) - applyDerivation f args - - deriveTuple :: PC.Tuple -> Derive Derivation - deriveTuple t = do - voidD <- voidDerivation - ds <- deriveTy `traverse` (t ^. #fields) - foldrM productDerivation voidD ds - - voidDerivation :: Derive Derivation - voidDerivation = (\ctx -> Axiom $ Judgement ctx VoidT KType) <$> ask - - unitDerivation :: Derive Derivation - unitDerivation = (\ctx -> Axiom $ Judgement ctx UnitT KType) <$> ask - - productDerivation :: Derivation -> Derivation -> Derive Derivation - productDerivation d1 d2 = do +fresh :: Derive Atom +fresh = do + DC a <- get + put (DC $ a + 1) + pure a + +deriveTyAbs :: PC.TyAbs -> Derive Derivation +deriveTyAbs tyabs = do + case M.toList (tyabs ^. #tyArgs) of + [] -> deriveTyBody (tyabs ^. #tyBody) + a@(n, ar) : as -> do + let argK = protoKind2Kind (ar ^. #argKind) + bodyK <- KVar <$> fresh ctx <- ask - let t1 = d1 ^. d'type - let t2 = d2 ^. d'type - tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] - pure $ Application (Judgement ctx (Product t1 t2) KType) d1 d2 - sumDerivation :: Derivation -> Derivation -> Derive Derivation - sumDerivation d1 d2 = do - ctx <- ask - let t1 = d1 ^. d'type - let t2 = d2 ^. d'type - tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] - pure $ Application (Judgement ctx (Sum t1 t2) KType) d1 d2 - - applyDerivation :: Derivation -> [Derivation] -> Derive Derivation - applyDerivation d1 = \case - [] -> pure d1 - d : ds -> do - c <- ask - d2 <- applyDerivation d ds - v <- KVar <$> fresh - tell [Constraint ((d2 ^. d'kind) :->: v, d1 ^. d'kind)] - pure $ Application (Judgement c (App (d ^. d'type) (d2 ^. d'type)) v) d1 d2 + let newContext = ctx & addContext %~ (<> M.singleton (mkInfoLess (TyVar n)) argK) + let newAbs = tyabs & #tyArgs .~ uncurry M.singleton a + let restAbs = tyabs & #tyArgs .~ M.fromList as + + restF <- local (const newContext) $ deriveTyAbs restAbs + + let uK = restF ^. d'kind + tell [Constraint (bodyK, uK)] + pure $ Abstraction (Judgement ctx (Abs newAbs) (argK :->: bodyK)) restF + +deriveTyBody :: PC.TyBody -> Derive Derivation +deriveTyBody = \case + PC.OpaqueI si -> do + ctx <- ask + pure $ Axiom $ Judgement ctx (Opaque si) KType + PC.SumI s -> deriveSum s + +deriveSum :: PC.Sum -> Derive Derivation +deriveSum s = do + case M.toList (s ^. #constructors) of + [] -> voidDerivation + c : cs -> do + dc <- deriveConstructor $ snd c + restDc <- deriveSum $ s & #constructors .~ M.fromList cs + sumDerivation dc restDc + +deriveConstructor :: PC.Constructor -> Derive Derivation +deriveConstructor c = do + ctx <- ask + d <- deriveProduct (c ^. #product) + tell $ Constraint <$> [(KType, d ^. d'kind)] + pure $ Implication (Judgement ctx (Constructor c) (d ^. d'kind)) d + +deriveProduct :: PC.Product -> Derive Derivation +deriveProduct = \case + PC.RecordI r -> deriveRecord r + PC.TupleI t -> deriveTuple t + +deriveRecord :: PC.Record -> Derive Derivation +deriveRecord r = do + case M.toList (r ^. #fields) of + [] -> unitDerivation + f : fs -> do + d1 <- deriveField $ snd f + d2 <- deriveRecord $ r & #fields .~ M.fromList fs + productDerivation d1 d2 + +deriveField :: PC.Field -> Derive Derivation +deriveField f = deriveTy $ f ^. #fieldTy + +deriveTy :: PC.Ty -> Derive Derivation +deriveTy = \case + PC.TyVarI tv -> deriveTyVar tv + PC.TyAppI ta -> deriveTyApp ta + PC.TyRefI tr -> deriveTyRef tr + +deriveTyRef :: PC.TyRef -> Derive Derivation +deriveTyRef = \case + PC.LocalI r -> do + localModule <- ask + let ty = QualifiedTyRef . withIso ltrISOqtr const $ (r, localModule) + v <- getKind ty + c <- ask + pure . Axiom $ Judgement c (Var ty) v + PC.ForeignI r -> do + let ty = QualifiedTyRef . withIso ftrISOqtr const $ r + v <- getKind ty + c <- ask + pure . Axiom $ Judgement c (Var ty) v + +deriveTyVar :: PC.TyVar -> Derive Derivation +deriveTyVar tv = do + let varName = tv ^. #varName + v <- getKind $ TyVar varName + c <- ask + pure . Axiom $ Judgement c (Var $ TyVar varName) v + +deriveTyApp :: PC.TyApp -> Derive Derivation +deriveTyApp ap = do + f <- deriveTy (ap ^. #tyFunc) + args <- deriveTy `traverse` (ap ^. #tyArgs) + applyDerivation f args + +deriveTuple :: PC.Tuple -> Derive Derivation +deriveTuple t = do + voidD <- voidDerivation + ds <- deriveTy `traverse` (t ^. #fields) + foldrM productDerivation voidD ds + +voidDerivation :: Derive Derivation +voidDerivation = (\ctx -> Axiom $ Judgement ctx VoidT KType) <$> ask + +unitDerivation :: Derive Derivation +unitDerivation = (\ctx -> Axiom $ Judgement ctx UnitT KType) <$> ask + +productDerivation :: Derivation -> Derivation -> Derive Derivation +productDerivation d1 d2 = do + ctx <- ask + let t1 = d1 ^. d'type + let t2 = d2 ^. d'type + tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] + pure $ Application (Judgement ctx (Product t1 t2) KType) d1 d2 + +sumDerivation :: Derivation -> Derivation -> Derive Derivation +sumDerivation d1 d2 = do + ctx <- ask + let t1 = d1 ^. d'type + let t2 = d2 ^. d'type + tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)] + pure $ Application (Judgement ctx (Sum t1 t2) KType) d1 d2 + +applyDerivation :: Derivation -> [Derivation] -> Derive Derivation +applyDerivation d1 = \case + [] -> pure d1 + d : ds -> do + c <- ask + d2 <- applyDerivation d ds + v <- KVar <$> fresh + tell [Constraint ((d2 ^. d'kind) :->: v, d1 ^. d'kind)] + pure $ Application (Judgement c (App (d ^. d'type) (d2 ^. d'type)) v) d1 d2 + +-------------------------------------------------------------------------------- +-- Class Checking + +runClassDefCheck :: Context -> PC.ModuleName -> PC.ClassDef -> Either InferErr () +runClassDefCheck ctx modName classDef = do + (_, c) <- runDerive ctx modName $ deriveClassDef classDef + void $ runUnify' c + +-- | Checks the class definition for correct typedness. +deriveClassDef :: PC.ClassDef -> Derive () +deriveClassDef classDef = traverse_ deriveConstraint (classDef ^. #supers) + +deriveConstraint :: PC.Constraint -> Derive Derivation +deriveConstraint _constraint = do + -- ctx <- ask + -- FIXME + -- k2 <- getKind (ConstraintT undefined) + -- argD <- deriveTy (constraint ^. #argument) + pure $ error "NOTE(cstml): fixme." + +-- Application +-- (Judgement ctx (App (Var (QualifiedConstraint undefined))) k2) +-- (Judgement ctx (App (Var (QualifiedConstraint undefined) k2))) +-- argD + +-------------------------------------------------------------------------------- +-- {- | Gets the binding from the context - if the variable is not bound throw an error. @@ -284,6 +293,7 @@ type Unifier a = forall effs. Member (Error InferErr) effs => Eff effs a getVariables :: Kind -> [Atom] getVariables = \case KType -> mempty + KConstraint -> mempty x :->: y -> getVariables x <> getVariables y KVar x -> [x] @@ -294,14 +304,25 @@ getVariables = \case unify :: [Constraint] -> Unifier [Substitution] unify [] = pure [] unify (constraint@(Constraint (l, r)) : xs) = case l of + -- Constants KType -> case r of KType -> unify xs + KConstraint -> nope constraint (_ :->: _) -> nope constraint KVar v -> let sub = Substitution (v, KType) in (sub :) <$> unify (sub `substituteIn` xs) + KConstraint -> case r of + KType -> nope constraint + KConstraint -> unify xs + (_ :->: _) -> nope constraint + KVar v -> + let sub = Substitution (v, KConstraint) + in (sub :) <$> unify (sub `substituteIn` xs) + -- Arrows x :->: y -> case r of KType -> nope constraint + KConstraint -> nope constraint KVar v -> if v `appearsIn` l then appearsErr v l @@ -312,6 +333,7 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of let c1 = Constraint (x, m) c2 = Constraint (y, n) in unify (c1 : c2 : xs) + -- Variables KVar a -> case r of KVar b -> if a == b @@ -349,6 +371,7 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of applySubstitution :: Substitution -> Kind -> Kind applySubstitution s@(Substitution (a, t)) k = case k of KType -> KType + KConstraint -> KConstraint l :->: r -> applySubstitution s l :->: applySubstitution s r KVar v -> if v == a then t else k @@ -368,9 +391,7 @@ substitute s d = case d of where applySubsToJudgement sub (Judgement ctx t k) = Judgement (applySubstitutionCtx s ctx) t (applySubstitution sub k) - applySubstitutionCtx subs c@(Context ctx addCtx) = case M.toList addCtx of - [] -> c - xs -> Context ctx $ M.fromList $ second (applySubstitution subs) <$> xs + applySubstitutionCtx subs ctx = ctx & addContext %~ fmap (applySubstitution subs) -- FIXME(cstml) not avoiding any clashes @@ -384,4 +405,5 @@ protoKind2Kind = \case PC.Kind k -> case k of PC.KindArrow k1 k2 -> protoKind2Kind k1 :->: protoKind2Kind k2 PC.KindRef PC.KType -> KType - PC.KindRef PC.KUnspecified -> KType -- unspecified kinds get inferred and unified + PC.KindRef PC.KUnspecified -> KType -- unspecified kinds get defaulted + PC.KindRef PC.KConstraint -> KConstraint diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs index 8e1558a5..babb517f 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs @@ -1,7 +1,6 @@ -module LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:), KVar), kind2ProtoKind, Atom) where +module LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:), KVar, KConstraint), Atom) where import GHC.Generics (Generic) -import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), parens, (<+>)) import Test.QuickCheck.Arbitrary.Generic (Arbitrary, GenericArbitrary (GenericArbitrary)) @@ -13,6 +12,7 @@ data Kind = KType | Kind :->: Kind | KVar Atom + | KConstraint deriving stock (Eq, Show, Generic) deriving (Arbitrary) via GenericArbitrary Kind @@ -22,10 +22,4 @@ instance Pretty Kind where ((x :->: y) :->: z) -> parens (pretty $ x :->: y) <+> "→" <+> pretty z x :->: y -> pretty x <+> "→" <+> pretty y KVar a -> pretty a - --- | Convert from internal Kind to Proto Kind. -kind2ProtoKind :: Kind -> PC.Kind -kind2ProtoKind = \case - k1 :->: k2 -> PC.Kind $ PC.KindArrow (kind2ProtoKind k1) (kind2ProtoKind k2) - KType -> PC.Kind . PC.KindRef $ PC.KType - KVar _ -> PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen. + KConstraint -> "Constraint" diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs index 709ffac6..a41fbbe0 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs @@ -1,36 +1,63 @@ +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + module LambdaBuffers.Compiler.KindCheck.Type ( Type (Abs, VoidT, Product, Sum, Constructor, Opaque, Var, UnitT, App), tyProd, tyUnit, tySum, tyVoid, - Variable (TyVar, QualifiedTyRef), + Variable (TyVar, QualifiedTyRef, QualifiedConstraint), + QualifiedTyRefName (..), + QualifiedClassName (..), + qTyRef'tyName, + qTyRef'moduleName, + qTyRef'sourceInfo, + ltrISOqtr, + ftrISOqtr, + ltrISOftr, ) where +import Control.Lens (iso, makeLenses, withIso, (^.)) +import Control.Lens.Combinators (Iso') import GHC.Generics (Generic) import Generics.SOP qualified as SOP import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, InfoLessC, withInfoLess) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), viaShow) -import Test.QuickCheck (Arbitrary) -import Test.QuickCheck.Arbitrary.Generic (GenericArbitrary (GenericArbitrary)) -- NOTE(cstml): Let's remove the Arbitrary instances and replaces them with -- Gens. +data QualifiedTyRefName = QualifiedTyRefName + { _qTyRef'tyName :: PC.TyName + , _qTyRef'moduleName :: PC.ModuleName + , _qTyRef'sourceInfo :: PC.SourceInfo + } + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (SOP.Generic) +instance InfoLessC QualifiedTyRefName + +makeLenses ''QualifiedTyRefName + +{- | All TyRefs and ClassNames are fully qualified. The context determines if + they are local or not. +-} data Variable - = -- | All TyRefs are fully qualified. The context determines if they're local - -- or not. - QualifiedTyRef PC.ForeignRef + = QualifiedTyRef QualifiedTyRefName | TyVar PC.VarName - deriving stock (Eq, Ord, Show, Generic) - deriving (Arbitrary) via GenericArbitrary Variable + | QualifiedConstraint QualifiedClassName + deriving stock (Eq, Show, Ord, Generic) deriving anyclass (SOP.Generic) +instance InfoLessC Variable + instance Pretty Variable where pretty = viaShow -instance InfoLessC Variable +data QualifiedClassName = QualifiedClassName PC.ClassName PC.ModuleName + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (SOP.Generic) +instance InfoLessC QualifiedClassName instance Pretty (InfoLess Variable) where pretty x = withInfoLess x pretty @@ -61,3 +88,34 @@ tyVoid = VoidT instance Pretty Type where pretty = viaShow + +-- | (PC.LocalRef, PC.ModuleName) isomorphism with QualifiedTyRefName. +ltrISOqtr :: Iso' (PC.LocalRef, PC.ModuleName) QualifiedTyRefName +ltrISOqtr = iso goRight goLeft + where + goRight :: (PC.LocalRef, PC.ModuleName) -> QualifiedTyRefName + goRight (lr, mn) = QualifiedTyRefName (lr ^. #tyName) mn (lr ^. #sourceInfo) + + goLeft qtr = + ( PC.LocalRef (qtr ^. qTyRef'tyName) (qtr ^. qTyRef'sourceInfo) + , qtr ^. qTyRef'moduleName + ) + +-- | LocalTyRef isomorphism with ForeignTyRef +ltrISOftr :: Iso' (PC.LocalRef, PC.ModuleName) PC.ForeignRef +ltrISOftr = iso goRight goLeft + where + goRight :: (PC.LocalRef, PC.ModuleName) -> PC.ForeignRef + goRight (lr, m) = PC.ForeignRef (lr ^. #tyName) m (lr ^. #sourceInfo) + + goLeft :: PC.ForeignRef -> (PC.LocalRef, PC.ModuleName) + goLeft fr = (PC.LocalRef (fr ^. #tyName) (fr ^. #sourceInfo), fr ^. #moduleName) + +ftrISOqtr :: Iso' PC.ForeignRef QualifiedTyRefName +ftrISOqtr = iso goRight goLeft + where + goRight :: PC.ForeignRef -> QualifiedTyRefName + goRight = withIso ltrISOftr $ \_ f2l -> withIso ltrISOqtr $ \l2q _ -> l2q . f2l + + goLeft :: QualifiedTyRefName -> PC.ForeignRef + goLeft = withIso ltrISOftr $ \l2f _ -> withIso ltrISOqtr $ \_ q2l -> l2f . q2l diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index fba02d7a..5b4aaad0 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -330,6 +330,7 @@ instance IsMessage P.Kind'KindRef PC.KindRefType where ( \case P.Kind'KIND_REF_TYPE -> pure PC.KType P.Kind'KIND_REF_UNSPECIFIED -> pure PC.KUnspecified + P.Kind'KIND_REF_CONSTRAINT -> pure PC.KConstraint P.Kind'KindRef'Unrecognized v -> throwError [ FPProtoParseError $ @@ -343,6 +344,7 @@ instance IsMessage P.Kind'KindRef PC.KindRefType where toProto = \case PC.KType -> P.Kind'KIND_REF_TYPE PC.KUnspecified -> P.Kind'KIND_REF_UNSPECIFIED + PC.KConstraint -> P.Kind'KIND_REF_CONSTRAINT instance IsMessage P.Kind PC.Kind where fromProto k = do diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 88a2d757..819ced01 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -6,7 +6,6 @@ {-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-} module LambdaBuffers.Compiler.ProtoCompat.Types ( - localRef2ForeignRef, ClassDef (..), ClassName (..), CompilerError (..), @@ -54,7 +53,6 @@ module LambdaBuffers.Compiler.ProtoCompat.Types ( ) where import Control.Exception (Exception) -import Control.Lens (Getter, to, (^.)) import Data.Generics.Labels () import Data.Map (Map) import Data.Set (Set) @@ -140,7 +138,7 @@ instance Arbitrary KindType where | n <= 0 = KindRef <$> arbitrary | otherwise = KindArrow <$> resize (n `div` 2) arbitrary <*> resize (n `div` 2) arbitrary -data KindRefType = KUnspecified | KType +data KindRefType = KUnspecified | KType | KConstraint deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary KindRefType deriving anyclass (SOP.Generic) @@ -181,17 +179,6 @@ data LocalRef = LocalRef {tyName :: TyName, sourceInfo :: SourceInfo} deriving (Arbitrary) via GenericArbitrary LocalRef deriving anyclass (SOP.Generic) -localRef2ForeignRef :: ModuleName -> Getter LocalRef ForeignRef -localRef2ForeignRef modName = - to - ( \lr -> - ForeignRef - { tyName = lr ^. #tyName - , sourceInfo = lr ^. #sourceInfo - , moduleName = modName - } - ) - data TyRef = LocalI LocalRef | ForeignI ForeignRef deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary TyRef diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index b2776e95..915e7f90 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -251,6 +251,8 @@ message Kind { KIND_REF_UNSPECIFIED = 0; // A `Type` kind (also know as `*` in Haskell) built-in. KIND_REF_TYPE = 1; + // A `Constraint` kind - relating to the kind of a Type Class. + KIND_REF_CONSTRAINT = 2; }; // A kind arrow. message KindArrow { @@ -648,7 +650,7 @@ message KindCheckError { TyRef ty_ref = 3; } - // In ty_def an error has occurred when trying to unify kind ty_kind_lhs + // In ty_def an error has occurred when trying to unify kind ty_kind_lhs // with ty_kind_rhs. // // FIXME(cstml): Add source of constraint to the error such that user can see @@ -663,7 +665,7 @@ message KindCheckError { // A cyclic kind was encountered. Infinite kinds like this are not acceptable, // and we do not support them. We could not construct infinite kind in ty_def. - // + // // As the implementation currently stands such an error is (most likely) not // representable - therefore not reachable. Such an error would usually occur // for a term like: λa. a a - in which case the inference would try to unify From ad073e56ed68f3072cf04b7e385fa61de3652720 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Thu, 2 Mar 2023 18:38:12 +0000 Subject: [PATCH 04/11] wip: scaffolded the error --- .../lambda-buffers-compiler.cabal | 1 + .../src/LambdaBuffers/Compiler/KindCheck.hs | 7 +- .../Compiler/KindCheck/Inference.hs | 93 +++++++++---------- .../LambdaBuffers/Compiler/KindCheck/Type.hs | 74 ++++++++++++--- .../test/Test/KindCheck.hs | 2 + .../test/Test/KindCheck/TyClass.hs | 6 ++ 6 files changed, 114 insertions(+), 69 deletions(-) create mode 100644 lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index b987a2f4..92691dee 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -172,6 +172,7 @@ test-suite tests Test.DeriveCheck Test.KindCheck Test.KindCheck.Errors + Test.KindCheck.TyClass Test.LambdaBuffers.Compiler Test.LambdaBuffers.Compiler.Coverage Test.LambdaBuffers.Compiler.Mutation diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 6f6062ab..01318344 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -24,7 +24,7 @@ import LambdaBuffers.Compiler.KindCheck.Inference (protoKind2Kind) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( - Variable (QualifiedConstraint, QualifiedTyRef, TyVar), + Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), ftrISOqtr, ltrISOqtr, qTyRef'moduleName, @@ -136,7 +136,8 @@ runKindCheck = interpret $ \case CheckClassDefinition modName classDef ctx -> either (handleErr2 modName classDef) pure $ I.runClassDefCheck ctx modName classDef where - handleErr2 = undefined + handleErr2 :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b + handleErr2 _ _ _err = error "Throw an error" handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b handleErr modName td = \case @@ -155,7 +156,7 @@ runKindCheck = interpret $ \case throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td foreignRef modName TyVar tv -> throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName - QualifiedConstraint _ -> error "NOTE(cstml): FIXME." + QualifiedTyClassRef _ -> error "NOTE(cstml): FIXME." I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do err <- PC.IncorrectApplicationError td <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName throwError $ PC.CompKindCheckError err diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index db370655..9f4ab58b 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -12,7 +12,6 @@ module LambdaBuffers.Compiler.KindCheck.Inference ( Context (..), Atom, Type (..), - DeriveM, DeriveEff, InferErr (..), Constraint (..), @@ -31,30 +30,33 @@ import Control.Monad.Freer.State (State, evalState, get, put) import Control.Monad.Freer.Writer (Writer, runWriter, tell) import Data.Foldable (foldrM, traverse_) import Data.Map qualified as M +import Data.Text (Text) import Data.Text qualified as T import LambdaBuffers.Compiler.KindCheck.Derivation ( Context (Context), Derivation (Abstraction, Application, Axiom, Implication), Judgement (Judgement), addContext, - context, d'kind, d'type, + getAllContext, ) import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( Type (Abs, App, Constructor, Opaque, Product, Sum, UnitT, Var, VoidT), - Variable (QualifiedTyRef, TyVar), + Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), + fcrISOqtcr, ftrISOqtr, + lcrISOftcr, + lcrISOqtcr, ltrISOqtr, ) -import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess) +import LambdaBuffers.Compiler.ProtoCompat.InfoLess (mkInfoLess) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), (<+>)) --- | Utility to unify the two. -getAllContext :: Context -> M.Map (InfoLess Variable) Kind -getAllContext c = c ^. context <> c ^. addContext +-------------------------------------------------------------------------------- +-- Types data InferErr = InferUnboundTermErr Variable @@ -74,30 +76,20 @@ newtype Substitution = Substitution {getSubstitution :: (Atom, Kind)} instance Pretty Substitution where pretty (Substitution (a, k)) = pretty a <+> "↦" <+> pretty k -newtype DerivationContext = DC - { _startAtom :: Atom - } +-------------------------------------------------------------------------------- +-- Effects -type DeriveEff = '[State Context, State DerivationContext, State [Constraint], Error InferErr] +newtype DerivationContext = DC {_startAtom :: Atom} -type DeriveM a = Eff DeriveEff a +type DeriveEff = + '[Reader Context, Reader PC.ModuleName, State DerivationContext, Writer [Constraint], Error InferErr] -type Derive a = - forall effs. - Members - '[ Reader Context - , Reader PC.ModuleName - , State DerivationContext - , Writer [Constraint] - , Error InferErr - ] - effs => - Eff effs a +type Derive a = forall effs. Members DeriveEff effs => Eff effs a -------------------------------------------------------------------------------- -- Runners --- | Run derivation builder - not unified yet. +-- | Run Derive Monad - not unified. runDerive :: Context -> PC.ModuleName -> Derive a -> Either InferErr (a, [Constraint]) runDerive ctx localMod = run . runError . runWriter . evalState (DC startAtom) . runReader ctx . runReader localMod @@ -261,17 +253,24 @@ deriveClassDef :: PC.ClassDef -> Derive () deriveClassDef classDef = traverse_ deriveConstraint (classDef ^. #supers) deriveConstraint :: PC.Constraint -> Derive Derivation -deriveConstraint _constraint = do - -- ctx <- ask - -- FIXME - -- k2 <- getKind (ConstraintT undefined) - -- argD <- deriveTy (constraint ^. #argument) - pure $ error "NOTE(cstml): fixme." - --- Application --- (Judgement ctx (App (Var (QualifiedConstraint undefined))) k2) --- (Judgement ctx (App (Var (QualifiedConstraint undefined) k2))) --- argD +deriveConstraint constraint = do + mn <- ask + ctx <- ask + let qcr = case constraint ^. #classRef of + PC.LocalCI lcr -> QualifiedTyClassRef . withIso lcrISOqtcr const $ (lcr, mn) + PC.ForeignCI fcr -> QualifiedTyClassRef . withIso fcrISOqtcr const $ fcr + dConstraint <- deriveVar qcr + argD <- deriveTy (constraint ^. #argument) + let argTy = argD ^. d'type + freshK <- KVar <$> fresh + tell [Constraint (dConstraint ^. d'kind, (argD ^. d'kind) :->: freshK)] + pure $ Application (Judgement ctx (App (dConstraint ^. d'type) argTy) freshK) dConstraint argD + +deriveVar :: Variable -> Derive Derivation +deriveVar v = do + ctx <- ask + k <- getKind v + pure . Axiom $ Judgement ctx (Var v) k -------------------------------------------------------------------------------- -- @@ -348,19 +347,13 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of appearsErr :: forall eff a. Member (Error InferErr) eff => Atom -> Kind -> Eff eff a appearsErr var ty = - throwError $ - InferRecursiveSubstitutionErr $ - mconcat - [ "Cannot unify: " - , T.pack . show . pretty $ var - , " with " - , T.pack . show . pretty $ ty - , ". " - , T.pack . show . pretty $ var - , " appears in: " - , T.pack . show . pretty $ ty - , "." - ] + throwError + $ InferRecursiveSubstitutionErr + . mconcat + $ ["Cannot unify: ", p var, " with ", p ty, ". ", p var, " appears in: ", p ty, "."] + where + p :: forall b. Pretty b => b -> Text + p = T.pack . show . pretty appearsIn a ty = a `elem` getVariables ty @@ -393,8 +386,6 @@ substitute s d = case d of applySubstitutionCtx subs ctx = ctx & addContext %~ fmap (applySubstitution subs) --- FIXME(cstml) not avoiding any clashes - -- | Fresh startAtom startAtom :: Atom startAtom = 0 @@ -405,5 +396,5 @@ protoKind2Kind = \case PC.Kind k -> case k of PC.KindArrow k1 k2 -> protoKind2Kind k1 :->: protoKind2Kind k2 PC.KindRef PC.KType -> KType - PC.KindRef PC.KUnspecified -> KType -- unspecified kinds get defaulted + PC.KindRef PC.KUnspecified -> KType PC.KindRef PC.KConstraint -> KConstraint diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs index a41fbbe0..fcc8abdd 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs @@ -6,15 +6,20 @@ module LambdaBuffers.Compiler.KindCheck.Type ( tyUnit, tySum, tyVoid, - Variable (TyVar, QualifiedTyRef, QualifiedConstraint), + Variable (TyVar, QualifiedTyRef, QualifiedTyClassRef), QualifiedTyRefName (..), - QualifiedClassName (..), + QualifiedTyClassRefName (..), qTyRef'tyName, qTyRef'moduleName, qTyRef'sourceInfo, + + -- * Isomorphisms. ltrISOqtr, ftrISOqtr, ltrISOftr, + fcrISOqtcr, + lcrISOftcr, + lcrISOqtcr, ) where import Control.Lens (iso, makeLenses, withIso, (^.)) @@ -25,8 +30,7 @@ import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, InfoLessC, withInf import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), viaShow) --- NOTE(cstml): Let's remove the Arbitrary instances and replaces them with --- Gens. +-- NOTE(cstml): Remove the Arbitrary instances and replaces them with Gens. data QualifiedTyRefName = QualifiedTyRefName { _qTyRef'tyName :: PC.TyName @@ -39,13 +43,27 @@ instance InfoLessC QualifiedTyRefName makeLenses ''QualifiedTyRefName +data QualifiedTyClassRefName = QualifiedTyClassRefName + { _qTyClass'className :: PC.ClassName + , _qTyClass'moduleName :: PC.ModuleName + , _qTyClass'sourceInfo :: PC.SourceInfo + } + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (SOP.Generic) +instance InfoLessC QualifiedTyClassRefName + +makeLenses ''QualifiedTyClassRefName + +instance Pretty (InfoLess Variable) where + pretty x = withInfoLess x pretty + {- | All TyRefs and ClassNames are fully qualified. The context determines if they are local or not. -} data Variable = QualifiedTyRef QualifiedTyRefName + | QualifiedTyClassRef QualifiedTyClassRefName | TyVar PC.VarName - | QualifiedConstraint QualifiedClassName deriving stock (Eq, Show, Ord, Generic) deriving anyclass (SOP.Generic) @@ -54,14 +72,6 @@ instance InfoLessC Variable instance Pretty Variable where pretty = viaShow -data QualifiedClassName = QualifiedClassName PC.ClassName PC.ModuleName - deriving stock (Eq, Ord, Show, Generic) - deriving anyclass (SOP.Generic) -instance InfoLessC QualifiedClassName - -instance Pretty (InfoLess Variable) where - pretty x = withInfoLess x pretty - data Type = Abs PC.TyAbs | App Type Type @@ -89,7 +99,9 @@ tyVoid = VoidT instance Pretty Type where pretty = viaShow --- | (PC.LocalRef, PC.ModuleName) isomorphism with QualifiedTyRefName. +-------------------------------------------------------------------------------- +-- Qualified TyRef ISOs. + ltrISOqtr :: Iso' (PC.LocalRef, PC.ModuleName) QualifiedTyRefName ltrISOqtr = iso goRight goLeft where @@ -101,7 +113,6 @@ ltrISOqtr = iso goRight goLeft , qtr ^. qTyRef'moduleName ) --- | LocalTyRef isomorphism with ForeignTyRef ltrISOftr :: Iso' (PC.LocalRef, PC.ModuleName) PC.ForeignRef ltrISOftr = iso goRight goLeft where @@ -119,3 +130,36 @@ ftrISOqtr = iso goRight goLeft goLeft :: QualifiedTyRefName -> PC.ForeignRef goLeft = withIso ltrISOftr $ \l2f _ -> withIso ltrISOqtr $ \_ q2l -> l2f . q2l + +-------------------------------------------------------------------------------- +-- Qualified TyClass Name ISOs. + +lcrISOqtcr :: Iso' (PC.LocalClassRef, PC.ModuleName) QualifiedTyClassRefName +lcrISOqtcr = iso goRight goLeft + where + goRight :: (PC.LocalClassRef, PC.ModuleName) -> QualifiedTyClassRefName + goRight (lcr, mn) = QualifiedTyClassRefName (lcr ^. #className) mn (lcr ^. #sourceInfo) + + goLeft :: QualifiedTyClassRefName -> (PC.LocalClassRef, PC.ModuleName) + goLeft qtcn = + ( PC.LocalClassRef (qtcn ^. qTyClass'className) (qtcn ^. qTyClass'sourceInfo) + , qtcn ^. qTyClass'moduleName + ) + +lcrISOftcr :: Iso' (PC.LocalClassRef, PC.ModuleName) PC.ForeignClassRef +lcrISOftcr = iso goRight goLeft + where + goRight :: (PC.LocalClassRef, PC.ModuleName) -> PC.ForeignClassRef + goRight (lr, mn) = PC.ForeignClassRef (lr ^. #className) mn (lr ^. #sourceInfo) + + goLeft :: PC.ForeignClassRef -> (PC.LocalClassRef, PC.ModuleName) + goLeft fr = (PC.LocalClassRef (fr ^. #className) (fr ^. #sourceInfo), fr ^. #moduleName) + +fcrISOqtcr :: Iso' PC.ForeignClassRef QualifiedTyClassRefName +fcrISOqtcr = iso goRight goLeft + where + goRight :: PC.ForeignClassRef -> QualifiedTyClassRefName + goRight = withIso lcrISOftcr $ \_ f2l -> withIso lcrISOqtcr $ \l2q _ -> l2q . f2l + + goLeft :: QualifiedTyClassRefName -> PC.ForeignClassRef + goLeft = withIso lcrISOftcr $ \l2f _ -> withIso lcrISOqtcr $ \_ q2l -> l2f . q2l diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index effd90d5..95e400c7 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -7,6 +7,7 @@ import LambdaBuffers.Compiler.KindCheck ( import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:))) import Test.KindCheck.Errors (testGKindCheckErrors) +import Test.KindCheck.TyClass qualified as KCTC import Test.QuickCheck (Arbitrary (arbitrary), forAll, (===)) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertBool, testCase, (@?=)) @@ -29,6 +30,7 @@ test = [ testCheck , testFolds , testGKindCheckErrors + , KCTC.test ] -------------------------------------------------------------------------------- diff --git a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs new file mode 100644 index 00000000..71051ab4 --- /dev/null +++ b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs @@ -0,0 +1,6 @@ +module Test.KindCheck.TyClass (test) where + +import Test.Tasty (TestTree, testGroup) + +test :: TestTree +test = testGroup "KC Class definitions Error Group." [] From d5f8ff93e61f3e9745cb4c37bbad74d2d7eef0ef Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Mon, 6 Mar 2023 15:01:24 +0000 Subject: [PATCH 05/11] update: integrate new errors --- .../lambda-buffers-compiler.cabal | 1 + .../src/LambdaBuffers/Compiler/KindCheck.hs | 50 +++++--- .../Compiler/KindCheck/Inference.hs | 3 +- .../LambdaBuffers/Compiler/KindCheck/Type.hs | 9 +- .../Compiler/ProtoCompat/FromProto.hs | 99 ++++++++++++++-- .../Compiler/ProtoCompat/InfoLess.hs | 3 +- .../Compiler/ProtoCompat/Types.hs | 24 ++-- lambda-buffers-compiler/test/Test.hs | 6 +- .../test/Test/KindCheck.hs | 4 +- .../test/Test/KindCheck/Errors.hs | 1 + .../test/Test/KindCheck/TyClass.hs | 22 +++- .../test/Test/Utils/ClassDef.hs | 10 ++ .../test/Test/Utils/CompilerInput.hs | 26 +++-- .../test/Test/Utils/Constructors.hs | 51 ++++++++- .../test/Test/Utils/Module.hs | 33 ++++-- lambda-buffers-proto/a.cpp | Bin 0 -> 12954 bytes lambda-buffers-proto/compiler.proto | 107 ++++++++++++++++-- 17 files changed, 369 insertions(+), 80 deletions(-) create mode 100644 lambda-buffers-compiler/test/Test/Utils/ClassDef.hs create mode 100644 lambda-buffers-proto/a.cpp diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index 92691dee..9026c945 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -179,6 +179,7 @@ test-suite tests Test.LambdaBuffers.Compiler.Utils Test.LambdaBuffers.Compiler.WellFormed Test.TypeClassCheck + Test.Utils.ClassDef Test.Utils.CompilerInput Test.Utils.Constructors Test.Utils.Module diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 01318344..1b1f31f2 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -25,8 +25,11 @@ import LambdaBuffers.Compiler.KindCheck.Inference qualified as I import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), + fcrISOqtcr, ftrISOqtr, + lcrISOqtcr, ltrISOqtr, + qTyClass'moduleName, qTyRef'moduleName, ) import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess) @@ -112,8 +115,9 @@ moduleStrategy :: Transform GlobalCheck ModuleCheck moduleStrategy = reinterpret $ \case CreateContext ci -> resolveCreateContext ci - ValidateModule cx md -> + ValidateModule cx md -> do traverse_ (kCTypeDefinition (md ^. #moduleName) cx) (md ^. #typeDefs) + traverse_ (kCClassInstance (md ^. #moduleName) cx) (md ^. #classDefs) localStrategy :: Transform ModuleCheck KindCheck localStrategy = reinterpret $ \case @@ -121,26 +125,25 @@ localStrategy = reinterpret $ \case desiredK <- getSpecifiedKind modName tyDef k <- inferTypeKind modName tyDef ctx desiredK checkKindConsistency modName tyDef ctx k - KCClassInstance modName ctx classDef -> do - _ <- checkClassDefinition modName classDef ctx - pure () + KCClassInstance modName ctx classDef -> + checkClassDefinition modName classDef ctx runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a runKindCheck = interpret $ \case InferTypeKind modName tyDef ctx _k -> - either (handleErr modName tyDef) pure $ I.infer ctx tyDef modName + either (handleErrTyDef modName tyDef) pure $ I.infer ctx tyDef modName CheckKindConsistency modName tyDef ctx k -> runReader modName $ resolveKindConsistency tyDef ctx k GetSpecifiedKind modName tyDef -> fmap snd $ runReader modName $ tyDef2NameAndKind tyDef CheckClassDefinition modName classDef ctx -> - either (handleErr2 modName classDef) pure $ I.runClassDefCheck ctx modName classDef + either (handleErrClassDef modName classDef) pure $ I.runClassDefCheck ctx modName classDef where - handleErr2 :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b - handleErr2 _ _ _err = error "Throw an error" + handleErrClassDef :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b + handleErrClassDef _ _ _err = error "Throw an error" - handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b - handleErr modName td = \case + handleErrTyDef :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b + handleErrTyDef modName td = \case I.InferUnboundTermErr ut -> case ut of QualifiedTyRef qtr -> do @@ -149,21 +152,32 @@ runKindCheck = interpret $ \case -- We're looking at the local module. let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr let err = PC.UnboundTyRefError td localRef modName - throwError . PC.CompKindCheckError $ err + throwError . PC.CKC'TyDefError $ err else do -- We're looking at a foreign module. let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr - throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td foreignRef modName + throwError . PC.CKC'TyDefError $ PC.UnboundTyRefError td foreignRef modName TyVar tv -> - throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName - QualifiedTyClassRef _ -> error "NOTE(cstml): FIXME." + throwError . PC.CKC'TyDefError $ PC.UnboundTyVarError td (PC.TyVar tv) modName + QualifiedTyClassRef qcr -> + if qcr ^. qTyClass'moduleName == modName + then do + -- We're looking at the local module. + let localClassRef = PC.LocalCI . fst . withIso lcrISOqtcr (\_ f -> f) $ qcr + let err = PC.UnboundTyClassRefError td localClassRef modName + throwError . PC.CKC'TyDefError $ err + else do + -- We're looking at a foreign module. + let foreignRef = PC.ForeignCI . withIso fcrISOqtcr (\_ f -> f) $ qcr + let err = PC.UnboundTyClassRefError td foreignRef modName + throwError . PC.CKC'TyDefError $ err I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do err <- PC.IncorrectApplicationError td <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName - throwError $ PC.CompKindCheckError err + throwError $ PC.CKC'TyDefError err I.InferRecursiveSubstitutionErr _ -> - throwError . PC.CompKindCheckError $ PC.RecursiveKindError td modName + throwError . PC.CKC'TyDefError $ PC.RecursiveKindError td modName I.InferImpossibleErr t -> - throwError $ PC.InternalError t + throwError $ PC.C'InternalError t -------------------------------------------------------------------------------- -- Resolvers @@ -184,7 +198,7 @@ resolveKindConsistency tyDef _ctx inferredKind = do | i == d = pure () | otherwise = do err <- PC.InconsistentTypeError t <$> kind2ProtoKind i <*> kind2ProtoKind d <*> ask - throwError $ PC.CompKindCheckError err + throwError $ PC.CKC'TyDefError err -------------------------------------------------------------------------------- -- Context Creation diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 9f4ab58b..d07954f6 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -250,7 +250,8 @@ runClassDefCheck ctx modName classDef = do -- | Checks the class definition for correct typedness. deriveClassDef :: PC.ClassDef -> Derive () -deriveClassDef classDef = traverse_ deriveConstraint (classDef ^. #supers) +deriveClassDef classDef = + traverse_ deriveConstraint (classDef ^. #supers) deriveConstraint :: PC.Constraint -> Derive Derivation deriveConstraint constraint = do diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs index fcc8abdd..b5de91a4 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs @@ -9,14 +9,19 @@ module LambdaBuffers.Compiler.KindCheck.Type ( Variable (TyVar, QualifiedTyRef, QualifiedTyClassRef), QualifiedTyRefName (..), QualifiedTyClassRefName (..), + + -- * Qualified TyRef qTyRef'tyName, qTyRef'moduleName, qTyRef'sourceInfo, - - -- * Isomorphisms. ltrISOqtr, ftrISOqtr, ltrISOftr, + + -- * Qualified TyClass + qTyClass'className, + qTyClass'moduleName, + qTyClass'sourceInfo, fcrISOqtcr, lcrISOftcr, lcrISOqtcr, diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index 5b4aaad0..97c1a018 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -662,37 +662,42 @@ instance IsMessage P.CompilerInput PC.CompilerInput where Outputs -} -instance IsMessage P.KindCheckError PC.KindCheckError where +instance IsMessage P.KindCheckErrorTyDef (PC.KindCheckError PC.TyDef) where fromProto kce = case kce ^. P.maybe'kindCheckError of Just x -> case x of - P.KindCheckError'UnboundTyVarError' err -> + P.KindCheckErrorTyDef'UnboundTyVarError' err -> PC.UnboundTyVarError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.tyVar) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'UnboundTyRefError' err -> + P.KindCheckErrorTyDef'UnboundTyRefError' err -> PC.UnboundTyRefError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.tyRef) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'UnificationError' err -> + P.KindCheckErrorTyDef'UnboundTyClassRefError' err -> + PC.UnboundTyClassRefError + <$> fromProto (err ^. P.tyDef) + <*> fromProto (err ^. P.tyClassRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorTyDef'UnificationError' err -> PC.IncorrectApplicationError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.tyKindLhs) <*> fromProto (err ^. P.tyKindRhs) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'CyclicKindError' err -> + P.KindCheckErrorTyDef'CyclicKindError' err -> PC.RecursiveKindError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.moduleName) - P.KindCheckError'InconsistentTypeError' err -> + P.KindCheckErrorTyDef'InconsistentTypeError' err -> PC.InconsistentTypeError <$> fromProto (err ^. P.tyDef) <*> fromProto (err ^. P.actualKind) <*> fromProto (err ^. P.expectedKind) <*> fromProto (err ^. P.moduleName) - Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckError)) "kind_check_error" + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckErrorTyDef)) "kind_check_error" toProto = \case PC.UnboundTyVarError tydef tyvar modname -> @@ -705,6 +710,11 @@ instance IsMessage P.KindCheckError PC.KindCheckError where & (P.unboundTyRefError . P.tyDef) .~ toProto tydef & (P.unboundTyRefError . P.tyRef) .~ toProto tyref & (P.unboundTyRefError . P.moduleName) .~ toProto modname + PC.UnboundTyClassRefError tydef tyClassRef modname -> + defMessage + & (P.unboundTyClassRefError . P.tyDef) .~ toProto tydef + & (P.unboundTyClassRefError . P.tyClassRef) .~ toProto tyClassRef + & (P.unboundTyClassRefError . P.moduleName) .~ toProto modname PC.IncorrectApplicationError tydef k1 k2 modname -> defMessage & (P.unificationError . P.tyDef) .~ toProto tydef @@ -722,12 +732,83 @@ instance IsMessage P.KindCheckError PC.KindCheckError where & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd & (P.inconsistentTypeError . P.moduleName) .~ toProto modname +instance IsMessage P.KindCheckErrorClassDef (PC.KindCheckError PC.ClassDef) where + fromProto kce = + case kce ^. P.maybe'kindCheckError of + Just x -> case x of + P.KindCheckErrorClassDef'UnboundTyVarError' err -> + PC.UnboundTyVarError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyVar) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'UnboundTyRefError' err -> + PC.UnboundTyRefError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'UnboundTyClassRefError' err -> + PC.UnboundTyClassRefError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyClassRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'UnificationError' err -> + PC.IncorrectApplicationError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.tyKindLhs) + <*> fromProto (err ^. P.tyKindRhs) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'CyclicKindError' err -> + PC.RecursiveKindError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassDef'InconsistentTypeError' err -> + PC.InconsistentTypeError + <$> fromProto (err ^. P.classDef) + <*> fromProto (err ^. P.actualKind) + <*> fromProto (err ^. P.expectedKind) + <*> fromProto (err ^. P.moduleName) + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckErrorClassDef)) "kind_check_error" + + toProto = \case + PC.UnboundTyVarError classDef tyvar modname -> + defMessage + & (P.unboundTyVarError . P.classDef) .~ toProto classDef + & (P.unboundTyVarError . P.tyVar) .~ toProto tyvar + & (P.unboundTyVarError . P.moduleName) .~ toProto modname + PC.UnboundTyRefError classDef tyref modname -> + defMessage + & (P.unboundTyRefError . P.classDef) .~ toProto classDef + & (P.unboundTyRefError . P.tyRef) .~ toProto tyref + & (P.unboundTyRefError . P.moduleName) .~ toProto modname + PC.UnboundTyClassRefError classDef classRef modName -> + defMessage + & (P.unboundTyClassRefError . P.classDef) .~ toProto classDef + & (P.unboundTyClassRefError . P.tyClassRef) .~ toProto classRef + & (P.unboundTyClassRefError . P.moduleName) .~ toProto modName + PC.IncorrectApplicationError classDef k1 k2 modname -> + defMessage + & (P.unificationError . P.classDef) .~ toProto classDef + & (P.unificationError . P.tyKindLhs) .~ toProto k1 + & (P.unificationError . P.tyKindRhs) .~ toProto k2 + & (P.unificationError . P.moduleName) .~ toProto modname + PC.RecursiveKindError classDef modname -> + defMessage + & (P.cyclicKindError . P.classDef) .~ toProto classDef + & (P.cyclicKindError . P.moduleName) .~ toProto modname + PC.InconsistentTypeError classDef ki kd modname -> + defMessage + & (P.inconsistentTypeError . P.classDef) .~ toProto classDef + & (P.inconsistentTypeError . P.actualKind) .~ toProto ki + & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd + & (P.inconsistentTypeError . P.moduleName) .~ toProto modname + instance IsMessage P.CompilerError PC.CompilerError where fromProto _ = throwInternalError "fromProto CompilerError not implemented" toProto = \case - PC.CompKindCheckError err -> defMessage & P.kindCheckErrors .~ [toProto err] - PC.InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] + PC.CKC'TyDefError err -> defMessage & P.kindCheckErrorsTyDef .~ [toProto err] + PC.CKC'ClassDefError err -> defMessage & P.kindCheckErrorsClassDef .~ [toProto err] + PC.C'InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] instance IsMessage P.CompilerResult PC.CompilerResult where fromProto _ = throwInternalError "fromProto CompilerError not implemented" diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs index c6445f36..4a01f83b 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs @@ -156,6 +156,7 @@ instance InfoLessC Module instance InfoLessC InferenceErr instance InfoLessC KindCheckErr instance InfoLessC CompilerInput -instance InfoLessC KindCheckError +instance InfoLessC (KindCheckError TyDef) +instance InfoLessC (KindCheckError ClassDef) instance InfoLessC CompilerError instance InfoLessC CompilerResult diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 819ced01..30ba4b72 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -53,6 +53,7 @@ module LambdaBuffers.Compiler.ProtoCompat.Types ( ) where import Control.Exception (Exception) +import Data.Data (Typeable) import Data.Generics.Labels () import Data.Map (Map) import Data.Set (Set) @@ -347,28 +348,27 @@ instance Arbitrary CompilerInput where where fn n = CompilerInput <$> resize n arbitrary -data KindCheckError - = UnboundTyVarError TyDef TyVar ModuleName - | UnboundTyRefError TyDef TyRef ModuleName - | IncorrectApplicationError TyDef Kind Kind ModuleName - | RecursiveKindError TyDef ModuleName - | InconsistentTypeError TyDef Kind Kind ModuleName +data KindCheckError loc + = UnboundTyVarError loc TyVar ModuleName + | UnboundTyRefError loc TyRef ModuleName + | UnboundTyClassRefError loc TyClassRef ModuleName + | IncorrectApplicationError loc Kind Kind ModuleName + | RecursiveKindError loc ModuleName + | InconsistentTypeError loc Kind Kind ModuleName deriving stock (Show, Eq, Ord, Generic) - deriving (Arbitrary) via GenericArbitrary KindCheckError deriving anyclass (SOP.Generic) -instance Exception KindCheckError +instance (Typeable loc, Show loc) => Exception (KindCheckError loc) -- | All the compiler errors. data CompilerError - = CompKindCheckError KindCheckError - | InternalError Text + = CKC'TyDefError (KindCheckError TyDef) + | CKC'ClassDefError (KindCheckError ClassDef) + | C'InternalError Text deriving stock (Show, Eq, Ord, Generic) - deriving (Arbitrary) via GenericArbitrary CompilerError deriving anyclass (SOP.Generic) data CompilerResult = CompilerResult deriving stock (Show, Eq, Ord, Generic) - deriving (Arbitrary) via GenericArbitrary CompilerResult deriving anyclass (SOP.Generic) type CompilerOutput = Either CompilerError CompilerResult diff --git a/lambda-buffers-compiler/test/Test.hs b/lambda-buffers-compiler/test/Test.hs index 1f3af148..e1be3d43 100644 --- a/lambda-buffers-compiler/test/Test.hs +++ b/lambda-buffers-compiler/test/Test.hs @@ -12,7 +12,7 @@ main = testGroup "Compiler tests" [ KC.test - , TC.test - , DC.test - , LBC.test + -- , TC.test + -- , DC.test + -- , LBC.test ] diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index 95e400c7..2c29f58b 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -7,7 +7,7 @@ import LambdaBuffers.Compiler.KindCheck ( import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:))) import Test.KindCheck.Errors (testGKindCheckErrors) -import Test.KindCheck.TyClass qualified as KCTC +import Test.KindCheck.TyClass qualified as TyClass import Test.QuickCheck (Arbitrary (arbitrary), forAll, (===)) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertBool, testCase, (@?=)) @@ -30,7 +30,7 @@ test = [ testCheck , testFolds , testGKindCheckErrors - , KCTC.test + , TyClass.test ] -------------------------------------------------------------------------------- diff --git a/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs b/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs index 5f6680ce..d226eb4a 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs @@ -3,6 +3,7 @@ module Test.KindCheck.Errors (testGKindCheckErrors) where import LambdaBuffers.Compiler.KindCheck (check_) import LambdaBuffers.Compiler.ProtoCompat qualified as PC import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CompKindCheckError), KindCheckError (UnboundTyRefError, UnboundTyVarError)) + import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (testCase, (@?=)) import Test.Utils.CompilerInput (compilerInput'undefinedForeignTyRef, compilerInput'undefinedLocalTyRef, compilerInput'undefinedVariable) diff --git a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs index 71051ab4..60a7cdb6 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs @@ -1,6 +1,26 @@ module Test.KindCheck.TyClass (test) where +import LambdaBuffers.Compiler.KindCheck (check_) +import LambdaBuffers.Compiler.ProtoCompat qualified as PC +import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerInput) import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (Assertion, testCase, (@?=)) +import Test.Tasty.Providers (TestName) +import Test.Utils.CompilerInput (compilerInput'classEq, compilerInput'classOrd) +import Test.Utils.Constructors () +import Test.Utils.TyDef () test :: TestTree -test = testGroup "KC Class definitions Error Group." [] +test = testGroup "KC Class definitions Error Group." [ok'Eq, ok'Ord] + +ok'Eq :: TestTree +ok'Eq = oKCase "Class Eq definition." compilerInput'classEq + +ok'Ord :: TestTree +ok'Ord = oKCase "Class Ord definition." compilerInput'classOrd + +oKCase :: TestName -> CompilerInput -> TestTree +oKCase n x = testCase n $ oK x + where + oK :: CompilerInput -> Assertion + oK a = check_ a @?= Right () diff --git a/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs new file mode 100644 index 00000000..6284d08e --- /dev/null +++ b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs @@ -0,0 +1,10 @@ +module Test.Utils.ClassDef (classDef'Eq, classDef'Ord) where + +import LambdaBuffers.Compiler.ProtoCompat qualified as PC +import Test.Utils.Constructors (_ClassDef, _Constraint, _LocalClassRef, _TyVarI, _Type) + +classDef'Eq :: PC.ClassDef +classDef'Eq = _ClassDef "Eq" ("a", _Type) mempty + +classDef'Ord :: PC.ClassDef +classDef'Ord = _ClassDef "Ord" ("a", _Type) [_Constraint (_LocalClassRef "Eq") (_TyVarI "a")] diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index 7785fe19..193fabc7 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -6,11 +6,15 @@ module Test.Utils.CompilerInput ( compilerInput'either, compilerInput'undefinedForeignTyRef, compilerInput'recDef, + compilerInput'classEq, + compilerInput'classOrd, ) where -import LambdaBuffers.Compiler.ProtoCompat qualified as P +import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module ( + module'classEq, + module'classOrd, module'either, module'incoherent, module'maybe, @@ -21,29 +25,35 @@ import Test.Utils.Module ( ) -- | Compiler Input containing 1 module with 1 definition - Maybe. -compilerInput'maybe :: P.CompilerInput +compilerInput'maybe :: PC.CompilerInput compilerInput'maybe = _CompilerInput [module'maybe] -- | Compiler Input containing 1 module with 1 definition - Either. -compilerInput'either :: P.CompilerInput +compilerInput'either :: PC.CompilerInput compilerInput'either = _CompilerInput [module'either] -- | Compiler Input containing 1 module with 1 definition - Either. -compilerInput'recDef :: P.CompilerInput +compilerInput'recDef :: PC.CompilerInput compilerInput'recDef = _CompilerInput [module'recDef] -- | Contains 2 definitions - 1 wrong one. -compilerInput'incoherent :: P.CompilerInput +compilerInput'incoherent :: PC.CompilerInput compilerInput'incoherent = _CompilerInput [module'maybe, module'incoherent] -- | Contains 1 undefined variable. -compilerInput'undefinedVariable :: P.CompilerInput +compilerInput'undefinedVariable :: PC.CompilerInput compilerInput'undefinedVariable = _CompilerInput [module'undefinedVar] -- | Contains 1 undefined Local TyRef. -compilerInput'undefinedLocalTyRef :: P.CompilerInput +compilerInput'undefinedLocalTyRef :: PC.CompilerInput compilerInput'undefinedLocalTyRef = _CompilerInput [module'undefinedLocalTyRef] -- | Contains 1 undefined Foreign TyRef. -compilerInput'undefinedForeignTyRef :: P.CompilerInput +compilerInput'undefinedForeignTyRef :: PC.CompilerInput compilerInput'undefinedForeignTyRef = _CompilerInput [module'undefinedForeignTyRef] + +compilerInput'classEq :: PC.CompilerInput +compilerInput'classEq = _CompilerInput [module'classEq] + +compilerInput'classOrd :: PC.CompilerInput +compilerInput'classOrd = _CompilerInput [module'classOrd] diff --git a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs index 41f0c44c..c2b50674 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs @@ -23,22 +23,26 @@ module Test.Utils.Constructors ( _LocalRef', _ForeignRef', _TyApp, + + -- * Class related. + _ClassDef, + _ClassName, + _LocalClassRef, + _ForeignCI, + _Constraint, ) where import Control.Lens ((^.)) +import Data.Default (def) import Data.Map qualified as Map import Data.Text (Text) import LambdaBuffers.Compiler.ProtoCompat qualified as PC import LambdaBuffers.Compiler.ProtoCompat.Types (SourceInfo) import Proto.Compiler_Fields () -import Data.Default (def) - _CompilerInput :: [PC.Module] -> PC.CompilerInput _CompilerInput ms = - PC.CompilerInput - { PC.modules = Map.fromList [(m ^. #moduleName, m) | m <- ms] - } + PC.CompilerInput {PC.modules = Map.fromList [(m ^. #moduleName, m) | m <- ms]} _Module :: PC.ModuleName -> [PC.TyDef] -> [PC.ClassDef] -> [PC.InstanceClause] -> PC.Module _Module mn tds cds ins = @@ -175,3 +179,40 @@ _ForeignRef' x m s = , PC.moduleName = m , PC.sourceInfo = s } + +-------------------------------------------------------------------------------- +-- Class related. + +_ClassDef :: Text -> (Text, PC.KindType) -> [PC.Constraint] -> PC.ClassDef +_ClassDef n tyArg cs = + PC.ClassDef + { className = _ClassName n + , classArgs = _TyArg tyArg + , supers = cs + , documentation = mempty + , sourceInfo = def + } + +_ClassName :: Text -> PC.ClassName +_ClassName n = PC.ClassName {name = n, sourceInfo = def} + +_Constraint :: PC.TyClassRef -> PC.Ty -> PC.Constraint +_Constraint cr t = + PC.Constraint + { classRef = cr + , argument = t + , sourceInfo = def + } + +_LocalClassRef :: Text -> PC.TyClassRef +_LocalClassRef n = + PC.LocalCI $ PC.LocalClassRef {className = _ClassName n, sourceInfo = def} + +_ForeignCI :: Text -> PC.ModuleName -> PC.TyClassRef +_ForeignCI n mn = + PC.ForeignCI $ + PC.ForeignClassRef + { className = _ClassName n + , moduleName = mn + , sourceInfo = def + } diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index 95d704cc..dca4a077 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -6,9 +6,11 @@ module Test.Utils.Module ( module'undefinedForeignTyRef, module'either, module'recDef, + module'classEq, + module'classOrd, ) where -import LambdaBuffers.Compiler.ProtoCompat qualified as P +import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_Module, _ModuleName) import Test.Utils.TyDef ( tyDef'either, @@ -20,15 +22,17 @@ import Test.Utils.TyDef ( tyDef'undefinedVar, ) +import Test.Utils.ClassDef (classDef'Eq, classDef'Ord) + -- _Module mn tds cds ins = -module'maybe :: P.Module +module'maybe :: PC.Module module'maybe = _Module (_ModuleName ["Prelude"]) [tyDef'maybe] mempty mempty -module'either :: P.Module +module'either :: PC.Module module'either = _Module (_ModuleName ["Prelude"]) [tyDef'either] mempty mempty -module'recDef :: P.Module +module'recDef :: PC.Module module'recDef = _Module (_ModuleName ["Prelude"]) [tyDef'recDef] mempty mempty {- | 1 Module containing @@ -40,7 +44,7 @@ module'recDef = _Module (_ModuleName ["Prelude"]) [tyDef'recDef] mempty mempty Should fail as B a defaults to B :: Type -> Type and Maybe is inferred as Type -> Type. This is an inconsistency failure. -} -module'incoherent :: P.Module +module'incoherent :: PC.Module module'incoherent = _Module (_ModuleName ["Module"]) [tyDef'maybe, tyDef'incoherent] mempty mempty {- | 1 Module containing @@ -48,7 +52,7 @@ module'incoherent = _Module (_ModuleName ["Module"]) [tyDef'maybe, tyDef'incoher Should fail as b is undefined. -} -module'undefinedVar :: P.Module +module'undefinedVar :: PC.Module module'undefinedVar = _Module (_ModuleName ["Module"]) [tyDef'undefinedVar] mempty mempty {- | 1 Module containing @@ -56,7 +60,7 @@ module'undefinedVar = _Module (_ModuleName ["Module"]) [tyDef'undefinedVar] memp ^^^ Should fail as Baz is a local undefined Ty Ref. -} -module'undefinedLocalTyRef :: P.Module +module'undefinedLocalTyRef :: PC.Module module'undefinedLocalTyRef = _Module (_ModuleName ["Module"]) [tyDef'undefinedLocalTyRef] mempty mempty {- | 1 Module containing @@ -64,5 +68,18 @@ module'undefinedLocalTyRef = _Module (_ModuleName ["Module"]) [tyDef'undefinedLo ^^^^^^^^^^^^^^^^^^ Should fail as Baz is a foreign undefined Ty Ref. -} -module'undefinedForeignTyRef :: P.Module +module'undefinedForeignTyRef :: PC.Module module'undefinedForeignTyRef = _Module (_ModuleName ["Module"]) [tyDef'undefinedForeignTyRef] mempty mempty + +{- | 1 Module containing: + class Eq a. +-} +module'classEq :: PC.Module +module'classEq = _Module (_ModuleName ["Module"]) mempty [classDef'Eq] mempty + +{- | 1 Module containing: + class Eq a. + class Eq a => Ord a. +-} +module'classOrd :: PC.Module +module'classOrd = _Module (_ModuleName ["Module"]) mempty [classDef'Ord] mempty diff --git a/lambda-buffers-proto/a.cpp b/lambda-buffers-proto/a.cpp new file mode 100644 index 0000000000000000000000000000000000000000..dcce0994829a69acc8fc1d1975dd38a53a68fdce GIT binary patch literal 12954 zcmd5DNsk*@dF<}C+n;-_Y^@3dlVX4oAcJ}sCWM5UUWt{YyQw$`PL|s)cbnK%j;lB#dNLBn(HEW+(0m~jU(gd*@Z<|ab0fKVmR zx&CyUi3eu&X@ma_Oz4F&99R|p6zL+FJ zsrThd=k5#kLO>4+uF`HR(TBiowc7%R4+^g1)Rn|T;B2QZaQLu259y$1?Z5)_Vcdd6 ztk^HJ}* zRdsr15~>pOu#Yo~H3dSZaFJO0$gWCtD!5%5Q#n2=`9C zaGxO1B7i{!(F0hidmX27;%Zdli60q`YF}Uw*^&Zhbmq5FwM<4Gam>Dk95I_09x;6m z9?$dp9A7>Hf%^caZgc_u2izK;Pv(t&Xs7TT3gpjk|e>=DQjZnp(! zHXJozr5`(Gp^Fjz7_ur%UK|YvV8?U)fP?VGk*Ps$zu`1%Y`qtzFr>26toZ)LQu!T6 z`dti|l5xVr&u@+!jy}V#S2^~_$kWF@Wp_%9GYR*9kUZ5np=^!$X0mLJ0Ib~C1@>{n zttk;ckQCeR;T}7Sfb=jM8UB@qdB%pt9(F2#ma zj0Dd}wrDpdsvN=c7xM|^=x6?7d>ZDPPCZa5bhvJKr?CkOoyN&&FqS%Ht91xjB1vLw zz~y_zgWa;dw_kpA@bGAFr?_9-+g*FXScm2Cm(o{{_SRCyHMkTm?HnFFEZJMdgVI`h zI|K71ko6WtcCL+XLdI)Xo^*9VmuTUKybD#L_8XsqIlrrG@asv(^03=N7}~j=3+p%Q z0b~T*GGV5(evyVbBxKx!r78!zZZ+^aI*WX42yX=mj=bOQ10LjTL?S=GYBax_ zf_#hwAr%heZkZ^qK$1h+AYkmApMxy6Q8i>*8B<~vek9wl^^phbH}jBHi^iLf={Qxd zQ&U!)m~9n6!RFm$0s==E+@RaW4o$Q(62n1>b`u7HGk=Ez+HCPl3fo@xd6<%51Tk4tLN0%N{gtJDy8AEloBRvJI6q*l-n8urVYxGV|0N6y+w`S zEy(!YHVzK3l_SUz{!?kVfvq5nmtnc)Rl6<64JtGh*qG?r~cyRcKkb3KX1YlFk63dy6PBdi5*r@DQq&OGGw;&!AeK!vj`dC&R*G1ySKO+DN73~i zSuDlekzMY|w+q%Z4~=f(QK(yFP8eh308LtazU@{lxt3XjL?bk+Fqpn_~4@kRpe%1 ziJmVd1qzM@1TO~42zDXYQ1H!Qt+!h@V7cf9PRFe@_poi~(Ac--pRlv$Y#kjG+x}t!6=p$#aC68>&YO0m>Ko6rOejk!dKMZ~9YO|O*WifgK&$kD11H(zmPC2W@caboi=azM}&L-UO-8()LVp6isodfD}YvhM_n z;v!SLIj(vSUFWcV-~|tzK$BZTynSoNDHvV%vFkl`%Z}S^DN4D?C_NGkdx#*Uq_Bo- z<{?~qaMp$6@kr|9apRHsgA^DVW8|WcRQ^E^ap8O~Dn-Q=bpdhOPd* zCir^kOJ@Ej1skEJ2Lj0d zQ=Y-uj0iQ|Y{tZ9AT;qCw}vorX$R5{tc1nW4g2)r_0Ao-5OYwO?3aFr&gJEuMf4pkvuit@xb88B}AqvUx||me=z@+g7xt9 zL!HmWVejbHKgu1WlbSUCltCnrp^=S#=>z#zubA}9gYyG9)8|JXnwyF74oQf}H_3w^ z<`2^pV*1T?HhJ(FkLNbzG4Qa9G*4;HLKBkVH%Zv|li}Y#^|6Hxp*sjI?ll&)ed?P( zNx|xXZ#@q>G2czYm2>^?dEgG;8_QR!K^I@3p;H^{#6SS()bP!A(^1qB z6-OFTKGloHXw%i!(hdU0sIhnAZ9>$O(kp)$y_N+5b%j`?;-xedL?JfG zIf*kfd9M+%U`eGh?7$M`tPq7%WQp%qU=kuo!~qDVk=%z>c~c|8BWXUd*_KJJLbWWw z8e0)xw5368giLyx(XSvNTT2WYLsbng?OEY68BRpSow8zUi9r>r?G;#Z`7Bih^7pyu zGDX^jM_`<3#`V2Q;>c&AaIU?GKn z2^F026lD!wE n - because m appears in both terms - + // the cyclic unification error would be thrown. + // + // In the case of LambdaBuffers - such an error is not (currently) achievable + // as the kind of the variable is given by the context - (i.e. λa : m . a a, + // where m is a kind) therefore the unification would fail with Unification + // Error. Nevertheless - future features might require it. + message CyclicKindError { + ModuleName module_name = 1; + ClassDef class_def = 2; + } + + // The actual_kind differs from the expected_kind. + message InconsistentTypeError { + ModuleName module_name = 1; + ClassDef class_def = 2; + Kind actual_kind = 3; + Kind expected_kind = 4; + } + + // One of the errors occurred during kind checking. + oneof kind_check_error { + UnboundTyRefError unbound_ty_ref_error = 1; + UnboundTyVarError unbound_ty_var_error = 2; + UnboundTyClassRefError unbound_ty_class_ref_error = 3; + UnificationError unification_error = 4; + CyclicKindError cyclic_kind_error = 5; + InconsistentTypeError inconsistent_type_error = 6; + } +} + +// Kind checking errors - in a Type definition. +message KindCheckErrorTyDef { // Unbound variable ty_var detected in term ty_def. message UnboundTyVarError { @@ -650,6 +725,15 @@ message KindCheckError { TyRef ty_ref = 3; } + + // Unbound type class reference ty_class_ref detected in term ty_def. + message UnboundTyClassRefError { + ModuleName module_name = 1; + TyDef ty_def = 2; + TyClassRef ty_class_ref = 3; + } + + // In ty_def an error has occurred when trying to unify kind ty_kind_lhs // with ty_kind_rhs. // @@ -677,8 +761,8 @@ message KindCheckError { // where m is a kind) therefore the unification would fail with Unification // Error. Nevertheless - future features might require it. message CyclicKindError { - TyDef ty_def = 1; - ModuleName module_name = 2; + ModuleName module_name = 1; + TyDef ty_def = 2; } // The actual_kind differs from the expected_kind. @@ -693,9 +777,10 @@ message KindCheckError { oneof kind_check_error { UnboundTyRefError unbound_ty_ref_error = 1; UnboundTyVarError unbound_ty_var_error = 2; - UnificationError unification_error = 3; - CyclicKindError cyclic_kind_error = 4; - InconsistentTypeError inconsistent_type_error = 5; + UnboundTyClassRefError unbound_ty_class_ref_error = 3; + UnificationError unification_error = 4; + CyclicKindError cyclic_kind_error = 5; + InconsistentTypeError inconsistent_type_error = 6; } } @@ -718,10 +803,12 @@ message CompilerError { repeated ProtoParseError proto_parse_errors = 1; // Errors occurred during naming checking. repeated NamingError naming_errors = 2; - // Errors occurred during kind checking. - repeated KindCheckError kind_check_errors = 4; + // Errors occurred during kind checking Type definitions. + repeated KindCheckErrorTyDef kind_check_errors_ty_defs = 4; + // Errors occurred during kind checking Class definitions. + repeated KindCheckErrorClassDef kind_check_errors_class_defs = 5; // Errors internal to the compiler implementation. - repeated InternalError internal_errors = 5; + repeated InternalError internal_errors = 6; } // Compiler Result ~ a successful Compilation Output. From f392aeb64aa81114fc16e5cda1670f9c766da048 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Mon, 6 Mar 2023 16:37:02 +0000 Subject: [PATCH 06/11] new: add error handling --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 36 ++++++++++++++++++- .../Compiler/ProtoCompat/Types.hs | 6 ++-- .../test/Test/KindCheck/Errors.hs | 8 ++--- 3 files changed, 43 insertions(+), 7 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 1b1f31f2..a2fff947 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -140,7 +140,41 @@ runKindCheck = interpret $ \case either (handleErrClassDef modName classDef) pure $ I.runClassDefCheck ctx modName classDef where handleErrClassDef :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b - handleErrClassDef _ _ _err = error "Throw an error" + handleErrClassDef modName classDef = \case + I.InferUnboundTermErr ut -> + case ut of + QualifiedTyRef qtr -> do + if qtr ^. qTyRef'moduleName == modName + then do + -- We're looking at the local module. + let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr + let err = PC.UnboundTyRefError classDef localRef modName + throwError . PC.CKC'ClassDefError $ err + else do + -- We're looking at a foreign module. + let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr + throwError . PC.CKC'ClassDefError $ PC.UnboundTyRefError classDef foreignRef modName + TyVar tv -> + throwError . PC.CKC'ClassDefError $ PC.UnboundTyVarError classDef (PC.TyVar tv) modName + QualifiedTyClassRef qcr -> + if qcr ^. qTyClass'moduleName == modName + then do + -- We're looking at the local module. + let localClassRef = PC.LocalCI . fst . withIso lcrISOqtcr (\_ f -> f) $ qcr + let err = PC.UnboundTyClassRefError classDef localClassRef modName + throwError . PC.CKC'ClassDefError $ err + else do + -- We're looking at a foreign module. + let foreignRef = PC.ForeignCI . withIso fcrISOqtcr (\_ f -> f) $ qcr + let err = PC.UnboundTyClassRefError classDef foreignRef modName + throwError . PC.CKC'ClassDefError $ err + I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do + err <- PC.IncorrectApplicationError classDef <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName + throwError $ PC.CKC'ClassDefError err + I.InferRecursiveSubstitutionErr _ -> + throwError . PC.CKC'ClassDefError $ PC.RecursiveKindError classDef modName + I.InferImpossibleErr t -> + throwError $ PC.C'InternalError t handleErrTyDef :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b handleErrTyDef modName td = \case diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 30ba4b72..0478b505 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -361,8 +361,10 @@ instance (Typeable loc, Show loc) => Exception (KindCheckError loc) -- | All the compiler errors. data CompilerError - = CKC'TyDefError (KindCheckError TyDef) - | CKC'ClassDefError (KindCheckError ClassDef) + = -- | Compiler KindChecker Error - within a Type Definition. + CKC'TyDefError (KindCheckError TyDef) + | -- | Compiler KindChecker Error - within a Class Definition. + CKC'ClassDefError (KindCheckError ClassDef) | C'InternalError Text deriving stock (Show, Eq, Ord, Generic) deriving anyclass (SOP.Generic) diff --git a/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs b/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs index d226eb4a..360859bf 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/Errors.hs @@ -2,7 +2,7 @@ module Test.KindCheck.Errors (testGKindCheckErrors) where import LambdaBuffers.Compiler.KindCheck (check_) import LambdaBuffers.Compiler.ProtoCompat qualified as PC -import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CompKindCheckError), KindCheckError (UnboundTyRefError, UnboundTyVarError)) +import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CKC'TyDefError), KindCheckError (UnboundTyRefError, UnboundTyVarError)) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (testCase, (@?=)) @@ -17,19 +17,19 @@ undefinedVariable :: TestTree undefinedVariable = testCase "Catch undefined(free) variable in Type Definition." $ check_ compilerInput'undefinedVariable - @?= (Left . CompKindCheckError . withDefModule) (UnboundTyVarError tyDef'undefinedVar tyDef'undefinedVar'var) + @?= (Left . CKC'TyDefError . withDefModule) (UnboundTyVarError tyDef'undefinedVar tyDef'undefinedVar'var) undefinedLocalTyRef :: TestTree undefinedLocalTyRef = testCase "Catch undefined Local TyRef in Type Definition." $ check_ compilerInput'undefinedLocalTyRef - @?= (Left . CompKindCheckError . withDefModule) (UnboundTyRefError tyDef'undefinedLocalTyRef tyDef'undefinedLocalTyRef'TyRef) + @?= (Left . CKC'TyDefError . withDefModule) (UnboundTyRefError tyDef'undefinedLocalTyRef tyDef'undefinedLocalTyRef'TyRef) undefinedForeignTyRef :: TestTree undefinedForeignTyRef = testCase "Catch undefined Foreign TyRef in Type Definition." $ check_ compilerInput'undefinedForeignTyRef - @?= (Left . CompKindCheckError . withDefModule) (UnboundTyRefError tyDef'undefinedForeignTyRef tyDef'undefinedForeignTyRef'TyRef) + @?= (Left . CKC'TyDefError . withDefModule) (UnboundTyRefError tyDef'undefinedForeignTyRef tyDef'undefinedForeignTyRef'TyRef) withDefModule :: forall a. (PC.ModuleName -> a) -> a withDefModule f = f (_ModuleName ["Module"]) From d45446a6fb0c01908b7efafe79213516c4b43e7e Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Mon, 6 Mar 2023 17:45:56 +0000 Subject: [PATCH 07/11] bugfix: Fix Constraint's kinds --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 11 +++++++---- .../Compiler/KindCheck/Derivation.hs | 13 +++++++------ .../Compiler/KindCheck/Inference.hs | 17 +++++++++++++---- .../Compiler/ProtoCompat/FromProto.hs | 4 ++-- lambda-buffers-compiler/test/Test.hs | 6 +++--- .../test/Test/KindCheck/TyClass.hs | 1 - .../test/Test/Utils/Module.hs | 2 +- 7 files changed, 33 insertions(+), 21 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index a2fff947..506277ef 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -19,11 +19,12 @@ import Control.Monad.Freer.TH (makeEffect) import Data.Default (Default (def)) import Data.Foldable (Foldable (toList), traverse_) import Data.Map qualified as M -import LambdaBuffers.Compiler.KindCheck.Derivation (Context, constraintContext, context) +import LambdaBuffers.Compiler.KindCheck.Derivation (Context, classContext, context) import LambdaBuffers.Compiler.KindCheck.Inference (protoKind2Kind) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( + QualifiedTyClassRefName (QualifiedTyClassRefName), Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), fcrISOqtcr, ftrISOqtr, @@ -302,11 +303,13 @@ kind2ProtoKind = \case -------------------------------------------------------------------------------- -- Class Definition Based Context Building. -classDef2Context :: forall effs. PC.ClassDef -> Eff effs Context +classDef2Context :: forall effs. Member (Reader PC.ModuleName) effs => PC.ClassDef -> Eff effs Context classDef2Context cDef = do - let className = mkInfoLess . view #className $ cDef + modName <- ask + let className = cDef ^. #className + let qtcn = mkInfoLess . QualifiedTyClassRef $ QualifiedTyClassRefName className modName def let classArg = tyArg2Kind . view #classArgs $ cDef - pure $ mempty & constraintContext .~ M.singleton className classArg + pure $ mempty & classContext .~ M.singleton qtcn (classArg :->: KConstraint) -------------------------------------------------------------------------------- -- utilities diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs index f496ab43..b86a27e4 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Derivation.hs @@ -1,3 +1,5 @@ +{-# OPTIONS_GHC -Wno-unused-imports #-} + module LambdaBuffers.Compiler.KindCheck.Derivation ( Derivation (Axiom, Abstraction, Application, Implication), QClassName (QClassName), @@ -11,15 +13,14 @@ module LambdaBuffers.Compiler.KindCheck.Derivation ( context, addContext, getAllContext, - constraintContext, + classContext, ) where import Control.Lens (Lens', lens, makeLenses, (&), (.~), (^.)) import Control.Lens.Operators ((%~)) import Data.Map qualified as M import LambdaBuffers.Compiler.KindCheck.Kind (Kind) -import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable) -import LambdaBuffers.Compiler.ProtoCompat qualified as PC +import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable (QualifiedTyClassRef)) import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess) import Prettyprinter ( Doc, @@ -43,7 +44,7 @@ data QClassName = QClassName data Context = Context { _context :: M.Map (InfoLess Variable) Kind , _addContext :: M.Map (InfoLess Variable) Kind - , _constraintContext :: M.Map (InfoLess PC.ClassName) Kind + , _classContext :: M.Map (InfoLess Variable) Kind } deriving stock (Show, Eq) @@ -62,14 +63,14 @@ instance Semigroup Context where c1 & context %~ (<> c2 ^. context) & addContext %~ (<> c2 ^. addContext) - & constraintContext %~ (<> c2 ^. constraintContext) + & classContext %~ (<> c2 ^. classContext) instance Monoid Context where mempty = Context mempty mempty mempty -- | Utility to unify the two T. getAllContext :: Context -> M.Map (InfoLess Variable) Kind -getAllContext c = c ^. context <> c ^. addContext +getAllContext c = c ^. context <> c ^. addContext <> c ^. classContext data Judgement = Judgement { _j'ctx :: Context diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index d07954f6..4c46219c 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -21,6 +21,7 @@ module LambdaBuffers.Compiler.KindCheck.Inference ( ) where import Control.Lens ((%~), (&), (.~), (^.)) +import Control.Lens.Combinators (to) import Control.Lens.Iso (withIso) import Control.Monad (void) import Control.Monad.Freer (Eff, Member, Members, run) @@ -47,7 +48,6 @@ import LambdaBuffers.Compiler.KindCheck.Type ( Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), fcrISOqtcr, ftrISOqtr, - lcrISOftcr, lcrISOqtcr, ltrISOqtr, ) @@ -250,8 +250,17 @@ runClassDefCheck ctx modName classDef = do -- | Checks the class definition for correct typedness. deriveClassDef :: PC.ClassDef -> Derive () -deriveClassDef classDef = - traverse_ deriveConstraint (classDef ^. #supers) +deriveClassDef classDef = do + vars <- createLocalConstraintContext classDef + traverse_ (local (<> vars) . deriveConstraint) (classDef ^. #supers) + +-- | Adds the kind of the variable to the local context. +createLocalConstraintContext :: PC.ClassDef -> Derive Context +createLocalConstraintContext cd = do + let arg = cd ^. #classArgs + let n = mkInfoLess $ TyVar $ arg ^. #argName + let k = arg ^. #argKind . to protoKind2Kind + return $ mempty & addContext .~ M.singleton n k deriveConstraint :: PC.Constraint -> Derive Derivation deriveConstraint constraint = do @@ -397,5 +406,5 @@ protoKind2Kind = \case PC.Kind k -> case k of PC.KindArrow k1 k2 -> protoKind2Kind k1 :->: protoKind2Kind k2 PC.KindRef PC.KType -> KType - PC.KindRef PC.KUnspecified -> KType PC.KindRef PC.KConstraint -> KConstraint + PC.KindRef PC.KUnspecified -> KType diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index 97c1a018..790a72d2 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -806,8 +806,8 @@ instance IsMessage P.CompilerError PC.CompilerError where fromProto _ = throwInternalError "fromProto CompilerError not implemented" toProto = \case - PC.CKC'TyDefError err -> defMessage & P.kindCheckErrorsTyDef .~ [toProto err] - PC.CKC'ClassDefError err -> defMessage & P.kindCheckErrorsClassDef .~ [toProto err] + PC.CKC'TyDefError err -> defMessage & P.kindCheckErrorsTyDefs .~ [toProto err] + PC.CKC'ClassDefError err -> defMessage & P.kindCheckErrorsClassDefs .~ [toProto err] PC.C'InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] instance IsMessage P.CompilerResult PC.CompilerResult where diff --git a/lambda-buffers-compiler/test/Test.hs b/lambda-buffers-compiler/test/Test.hs index e1be3d43..1f3af148 100644 --- a/lambda-buffers-compiler/test/Test.hs +++ b/lambda-buffers-compiler/test/Test.hs @@ -12,7 +12,7 @@ main = testGroup "Compiler tests" [ KC.test - -- , TC.test - -- , DC.test - -- , LBC.test + , TC.test + , DC.test + , LBC.test ] diff --git a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs index 60a7cdb6..7a2b912d 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs @@ -1,7 +1,6 @@ module Test.KindCheck.TyClass (test) where import LambdaBuffers.Compiler.KindCheck (check_) -import LambdaBuffers.Compiler.ProtoCompat qualified as PC import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerInput) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (Assertion, testCase, (@?=)) diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index dca4a077..1021c5f6 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -82,4 +82,4 @@ module'classEq = _Module (_ModuleName ["Module"]) mempty [classDef'Eq] mempty class Eq a => Ord a. -} module'classOrd :: PC.Module -module'classOrd = _Module (_ModuleName ["Module"]) mempty [classDef'Ord] mempty +module'classOrd = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] mempty From 40aaa879b27779c3c58215535de93fc81f52bda1 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Tue, 7 Mar 2023 17:39:02 +0000 Subject: [PATCH 08/11] update: trivial instances --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 84 +++++++------------ .../Compiler/KindCheck/Inference.hs | 36 +++++++- .../Compiler/ProtoCompat/FromProto.hs | 71 ++++++++++++++++ .../Compiler/ProtoCompat/InfoLess.hs | 1 + .../Compiler/ProtoCompat/Types.hs | 1 + .../test/Test/KindCheck/TyClass.hs | 30 ++++++- .../test/Test/Utils/ClassDef.hs | 7 +- .../test/Test/Utils/CompilerInput.hs | 10 +++ .../test/Test/Utils/Constructors.hs | 23 +++++ .../test/Test/Utils/Module.hs | 17 +++- .../test/Test/Utils/TyDef.hs | 7 ++ lambda-buffers-proto/compiler.proto | 80 +++++++++++++++++- 12 files changed, 304 insertions(+), 63 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 506277ef..298ab635 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -33,6 +33,7 @@ import LambdaBuffers.Compiler.KindCheck.Type ( qTyClass'moduleName, qTyRef'moduleName, ) +import LambdaBuffers.Compiler.ProtoCompat (KindCheckError) import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC @@ -60,7 +61,8 @@ makeEffect ''GlobalCheck -- | Interactions that happen at the level of the data ModuleCheck a where -- Module KCTypeDefinition :: PC.ModuleName -> Context -> PC.TyDef -> ModuleCheck Kind - KCClassInstance :: PC.ModuleName -> Context -> PC.ClassDef -> ModuleCheck () + KCClassDef :: PC.ModuleName -> Context -> PC.ClassDef -> ModuleCheck () + KCClassInstance :: PC.ModuleName -> Context -> PC.InstanceClause -> ModuleCheck () -- KCClass :: Context -> P.ClassDef -> ModuleCheck () @@ -70,6 +72,7 @@ data KindCheck a where GetSpecifiedKind :: PC.ModuleName -> PC.TyDef -> KindCheck Kind InferTypeKind :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind CheckClassDefinition :: PC.ModuleName -> PC.ClassDef -> Context -> KindCheck () + CheckClassInstance :: PC.ModuleName -> PC.InstanceClause -> Context -> KindCheck () CheckKindConsistency :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind -- CheckClassInstance :: PC.ModuleName -> KindCheck Kind @@ -118,7 +121,8 @@ moduleStrategy = reinterpret $ \case resolveCreateContext ci ValidateModule cx md -> do traverse_ (kCTypeDefinition (md ^. #moduleName) cx) (md ^. #typeDefs) - traverse_ (kCClassInstance (md ^. #moduleName) cx) (md ^. #classDefs) + traverse_ (kCClassDef (md ^. #moduleName) cx) (md ^. #classDefs) + traverse_ (kCClassInstance (md ^. #moduleName) cx) (md ^. #instances) localStrategy :: Transform ModuleCheck KindCheck localStrategy = reinterpret $ \case @@ -126,8 +130,10 @@ localStrategy = reinterpret $ \case desiredK <- getSpecifiedKind modName tyDef k <- inferTypeKind modName tyDef ctx desiredK checkKindConsistency modName tyDef ctx k - KCClassInstance modName ctx classDef -> + KCClassDef modName ctx classDef -> checkClassDefinition modName classDef ctx + KCClassInstance modName ctx inst -> + checkClassInstance modName inst ctx runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a runKindCheck = interpret $ \case @@ -139,46 +145,20 @@ runKindCheck = interpret $ \case fmap snd $ runReader modName $ tyDef2NameAndKind tyDef CheckClassDefinition modName classDef ctx -> either (handleErrClassDef modName classDef) pure $ I.runClassDefCheck ctx modName classDef + CheckClassInstance modName classInst ctx -> + either (handleErrClassInst modName classInst) pure $ I.runClassInstanceCheck ctx modName classInst where + handleErrClassInst :: forall {b}. PC.ModuleName -> PC.InstanceClause -> I.InferErr -> Eff effs b + handleErrClassInst = handleErr PC.CKC'ClassInstanceError + handleErrClassDef :: forall {b}. PC.ModuleName -> PC.ClassDef -> I.InferErr -> Eff effs b - handleErrClassDef modName classDef = \case - I.InferUnboundTermErr ut -> - case ut of - QualifiedTyRef qtr -> do - if qtr ^. qTyRef'moduleName == modName - then do - -- We're looking at the local module. - let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr - let err = PC.UnboundTyRefError classDef localRef modName - throwError . PC.CKC'ClassDefError $ err - else do - -- We're looking at a foreign module. - let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr - throwError . PC.CKC'ClassDefError $ PC.UnboundTyRefError classDef foreignRef modName - TyVar tv -> - throwError . PC.CKC'ClassDefError $ PC.UnboundTyVarError classDef (PC.TyVar tv) modName - QualifiedTyClassRef qcr -> - if qcr ^. qTyClass'moduleName == modName - then do - -- We're looking at the local module. - let localClassRef = PC.LocalCI . fst . withIso lcrISOqtcr (\_ f -> f) $ qcr - let err = PC.UnboundTyClassRefError classDef localClassRef modName - throwError . PC.CKC'ClassDefError $ err - else do - -- We're looking at a foreign module. - let foreignRef = PC.ForeignCI . withIso fcrISOqtcr (\_ f -> f) $ qcr - let err = PC.UnboundTyClassRefError classDef foreignRef modName - throwError . PC.CKC'ClassDefError $ err - I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do - err <- PC.IncorrectApplicationError classDef <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName - throwError $ PC.CKC'ClassDefError err - I.InferRecursiveSubstitutionErr _ -> - throwError . PC.CKC'ClassDefError $ PC.RecursiveKindError classDef modName - I.InferImpossibleErr t -> - throwError $ PC.C'InternalError t + handleErrClassDef = handleErr PC.CKC'ClassDefError handleErrTyDef :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b - handleErrTyDef modName td = \case + handleErrTyDef = handleErr PC.CKC'TyDefError + + handleErr :: forall {loc} {b}. (KindCheckError loc -> CompilerErr) -> PC.ModuleName -> loc -> I.InferErr -> Eff effs b + handleErr constructor modName loc = \case I.InferUnboundTermErr ut -> case ut of QualifiedTyRef qtr -> do @@ -186,33 +166,31 @@ runKindCheck = interpret $ \case then do -- We're looking at the local module. let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr - let err = PC.UnboundTyRefError td localRef modName - throwError . PC.CKC'TyDefError $ err + let err = PC.UnboundTyRefError loc localRef modName + throwError . constructor $ err else do -- We're looking at a foreign module. let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr - throwError . PC.CKC'TyDefError $ PC.UnboundTyRefError td foreignRef modName + throwError . constructor $ PC.UnboundTyRefError loc foreignRef modName TyVar tv -> - throwError . PC.CKC'TyDefError $ PC.UnboundTyVarError td (PC.TyVar tv) modName + throwError . constructor $ PC.UnboundTyVarError loc (PC.TyVar tv) modName QualifiedTyClassRef qcr -> if qcr ^. qTyClass'moduleName == modName then do -- We're looking at the local module. let localClassRef = PC.LocalCI . fst . withIso lcrISOqtcr (\_ f -> f) $ qcr - let err = PC.UnboundTyClassRefError td localClassRef modName - throwError . PC.CKC'TyDefError $ err + let err = PC.UnboundTyClassRefError loc localClassRef modName + throwError . constructor $ err else do -- We're looking at a foreign module. let foreignRef = PC.ForeignCI . withIso fcrISOqtcr (\_ f -> f) $ qcr - let err = PC.UnboundTyClassRefError td foreignRef modName - throwError . PC.CKC'TyDefError $ err + let err = PC.UnboundTyClassRefError loc foreignRef modName + throwError . constructor $ err I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do - err <- PC.IncorrectApplicationError td <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName - throwError $ PC.CKC'TyDefError err - I.InferRecursiveSubstitutionErr _ -> - throwError . PC.CKC'TyDefError $ PC.RecursiveKindError td modName - I.InferImpossibleErr t -> - throwError $ PC.C'InternalError t + err <- PC.IncorrectApplicationError loc <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName + throwError $ constructor err + I.InferRecursiveSubstitutionErr _ -> throwError . constructor $ PC.RecursiveKindError loc modName + I.InferImpossibleErr t -> throwError $ PC.C'InternalError t -------------------------------------------------------------------------------- -- Resolvers diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 4c46219c..2293d113 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -6,6 +6,7 @@ module LambdaBuffers.Compiler.KindCheck.Inference ( -- * API functions infer, runClassDefCheck, + runClassInstanceCheck, -- * Types Kind (..), @@ -44,6 +45,7 @@ import LambdaBuffers.Compiler.KindCheck.Derivation ( ) import LambdaBuffers.Compiler.KindCheck.Kind (Atom, Kind (KConstraint, KType, KVar, (:->:))) import LambdaBuffers.Compiler.KindCheck.Type ( + QualifiedTyClassRefName, Type (Abs, App, Constructor, Opaque, Product, Sum, UnitT, Var, VoidT), Variable (QualifiedTyClassRef, QualifiedTyRef, TyVar), fcrISOqtcr, @@ -248,6 +250,27 @@ runClassDefCheck ctx modName classDef = do (_, c) <- runDerive ctx modName $ deriveClassDef classDef void $ runUnify' c +runClassInstanceCheck :: Context -> PC.ModuleName -> PC.InstanceClause -> Either InferErr () +runClassInstanceCheck ctx modName classInst = do + (_, c) <- runDerive ctx modName $ deriveClassInst classInst + void $ runUnify' c + +deriveClassInst :: PC.InstanceClause -> Derive () +deriveClassInst instClause = do + void $ deriveClassInstDef instClause + traverse_ deriveConstraint $ instClause ^. #constraints + where + deriveClassInstDef :: PC.InstanceClause -> Derive Derivation + deriveClassInstDef ic = do + ctx <- ask + qcr <- QualifiedTyClassRef <$> classRef2Quantified (ic ^. #classRef) + dConstraint <- deriveVar qcr + argD <- deriveTy (ic ^. #head) + let argTy = argD ^. d'type + freshK <- KVar <$> fresh + tell [Constraint (dConstraint ^. d'kind, (argD ^. d'kind) :->: freshK)] + pure $ Application (Judgement ctx (App (dConstraint ^. d'type) argTy) freshK) dConstraint argD + -- | Checks the class definition for correct typedness. deriveClassDef :: PC.ClassDef -> Derive () deriveClassDef classDef = do @@ -262,13 +285,18 @@ createLocalConstraintContext cd = do let k = arg ^. #argKind . to protoKind2Kind return $ mempty & addContext .~ M.singleton n k +classRef2Quantified :: PC.TyClassRef -> Derive QualifiedTyClassRefName +classRef2Quantified cr = do + mn <- ask + let qcr = case cr of + PC.LocalCI lcr -> withIso lcrISOqtcr const (lcr, mn) + PC.ForeignCI fcr -> withIso fcrISOqtcr const fcr + pure qcr + deriveConstraint :: PC.Constraint -> Derive Derivation deriveConstraint constraint = do - mn <- ask + qcr <- QualifiedTyClassRef <$> classRef2Quantified (constraint ^. #classRef) ctx <- ask - let qcr = case constraint ^. #classRef of - PC.LocalCI lcr -> QualifiedTyClassRef . withIso lcrISOqtcr const $ (lcr, mn) - PC.ForeignCI fcr -> QualifiedTyClassRef . withIso fcrISOqtcr const $ fcr dConstraint <- deriveVar qcr argD <- deriveTy (constraint ^. #argument) let argTy = argD ^. d'type diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index 790a72d2..a2c92147 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -802,12 +802,83 @@ instance IsMessage P.KindCheckErrorClassDef (PC.KindCheckError PC.ClassDef) wher & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd & (P.inconsistentTypeError . P.moduleName) .~ toProto modname +instance IsMessage P.KindCheckErrorClassInstance (PC.KindCheckError PC.InstanceClause) where + fromProto kce = + case kce ^. P.maybe'kindCheckError of + Just x -> case x of + P.KindCheckErrorClassInstance'UnboundTyVarError' err -> + PC.UnboundTyVarError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyVar) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'UnboundTyRefError' err -> + PC.UnboundTyRefError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'UnboundTyClassRefError' err -> + PC.UnboundTyClassRefError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyClassRef) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'UnificationError' err -> + PC.IncorrectApplicationError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.tyKindLhs) + <*> fromProto (err ^. P.tyKindRhs) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'CyclicKindError' err -> + PC.RecursiveKindError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.moduleName) + P.KindCheckErrorClassInstance'InconsistentTypeError' err -> + PC.InconsistentTypeError + <$> fromProto (err ^. P.instanceClause) + <*> fromProto (err ^. P.actualKind) + <*> fromProto (err ^. P.expectedKind) + <*> fromProto (err ^. P.moduleName) + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckErrorClassInstance)) "kind_check_error" + + toProto = \case + PC.UnboundTyVarError instanceClause tyvar modname -> + defMessage + & (P.unboundTyVarError . P.instanceClause) .~ toProto instanceClause + & (P.unboundTyVarError . P.tyVar) .~ toProto tyvar + & (P.unboundTyVarError . P.moduleName) .~ toProto modname + PC.UnboundTyRefError instanceClause tyref modname -> + defMessage + & (P.unboundTyRefError . P.instanceClause) .~ toProto instanceClause + & (P.unboundTyRefError . P.tyRef) .~ toProto tyref + & (P.unboundTyRefError . P.moduleName) .~ toProto modname + PC.UnboundTyClassRefError instanceClause classRef modName -> + defMessage + & (P.unboundTyClassRefError . P.instanceClause) .~ toProto instanceClause + & (P.unboundTyClassRefError . P.tyClassRef) .~ toProto classRef + & (P.unboundTyClassRefError . P.moduleName) .~ toProto modName + PC.IncorrectApplicationError instanceClause k1 k2 modname -> + defMessage + & (P.unificationError . P.instanceClause) .~ toProto instanceClause + & (P.unificationError . P.tyKindLhs) .~ toProto k1 + & (P.unificationError . P.tyKindRhs) .~ toProto k2 + & (P.unificationError . P.moduleName) .~ toProto modname + PC.RecursiveKindError instanceClause modname -> + defMessage + & (P.cyclicKindError . P.instanceClause) .~ toProto instanceClause + & (P.cyclicKindError . P.moduleName) .~ toProto modname + PC.InconsistentTypeError instanceClause ki kd modname -> + defMessage + & (P.inconsistentTypeError . P.instanceClause) .~ toProto instanceClause + & (P.inconsistentTypeError . P.actualKind) .~ toProto ki + & (P.inconsistentTypeError . P.expectedKind) .~ toProto kd + & (P.inconsistentTypeError . P.moduleName) .~ toProto modname + instance IsMessage P.CompilerError PC.CompilerError where fromProto _ = throwInternalError "fromProto CompilerError not implemented" toProto = \case PC.CKC'TyDefError err -> defMessage & P.kindCheckErrorsTyDefs .~ [toProto err] PC.CKC'ClassDefError err -> defMessage & P.kindCheckErrorsClassDefs .~ [toProto err] + PC.CKC'ClassInstanceError err -> defMessage & P.kindCheckErrorsClassInstances .~ [toProto err] PC.C'InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] instance IsMessage P.CompilerResult PC.CompilerResult where diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs index 4a01f83b..788eb92f 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/InfoLess.hs @@ -158,5 +158,6 @@ instance InfoLessC KindCheckErr instance InfoLessC CompilerInput instance InfoLessC (KindCheckError TyDef) instance InfoLessC (KindCheckError ClassDef) +instance InfoLessC (KindCheckError InstanceClause) instance InfoLessC CompilerError instance InfoLessC CompilerResult diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 0478b505..73f06ca4 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -365,6 +365,7 @@ data CompilerError CKC'TyDefError (KindCheckError TyDef) | -- | Compiler KindChecker Error - within a Class Definition. CKC'ClassDefError (KindCheckError ClassDef) + | CKC'ClassInstanceError (KindCheckError InstanceClause) | C'InternalError Text deriving stock (Show, Eq, Ord, Generic) deriving anyclass (SOP.Generic) diff --git a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs index 7a2b912d..b786d20b 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs @@ -5,12 +5,20 @@ import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerInput) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (Assertion, testCase, (@?=)) import Test.Tasty.Providers (TestName) -import Test.Utils.CompilerInput (compilerInput'classEq, compilerInput'classOrd) +import Test.Utils.CompilerInput (compilerInput'IntEqInstance, compilerInput'classEq, compilerInput'classOrd, compilerInput'unboundEq) import Test.Utils.Constructors () import Test.Utils.TyDef () test :: TestTree -test = testGroup "KC Class definitions Error Group." [ok'Eq, ok'Ord] +test = + testGroup + "KC Class Error." + [ testGroup "Class Defs." [ok'Eq, ok'Ord, fail'Ord] + , testGroup "Class Instances." [ok'IntEqInstance] + ] + +-------------------------------------------------------------------------------- +-- Class Defs ok'Eq :: TestTree ok'Eq = oKCase "Class Eq definition." compilerInput'classEq @@ -18,6 +26,24 @@ ok'Eq = oKCase "Class Eq definition." compilerInput'classEq ok'Ord :: TestTree ok'Ord = oKCase "Class Ord definition." compilerInput'classOrd +fail'Ord :: TestTree +fail'Ord = failCase "Unbound reference to eq." compilerInput'unboundEq + +-------------------------------------------------------------------------------- +-- Class Instances + +ok'IntEqInstance :: TestTree +ok'IntEqInstance = oKCase "Int Eq Instance." compilerInput'IntEqInstance + +-------------------------------------------------------------------------------- +-- Utils + +failCase :: TestName -> CompilerInput -> TestTree +failCase n x = testCase n $ justFail x + where + justFail :: CompilerInput -> Assertion + justFail a = either (Left . const ()) Right (check_ a) @?= Left () + oKCase :: TestName -> CompilerInput -> TestTree oKCase n x = testCase n $ oK x where diff --git a/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs index 6284d08e..b88ac1f3 100644 --- a/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs +++ b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs @@ -1,10 +1,13 @@ -module Test.Utils.ClassDef (classDef'Eq, classDef'Ord) where +module Test.Utils.ClassDef (classDef'Eq, classDef'Ord, classInstance'IntEq) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC -import Test.Utils.Constructors (_ClassDef, _Constraint, _LocalClassRef, _TyVarI, _Type) +import Test.Utils.Constructors (_ClassDef, _Constraint, _InstanceClause, _LocalClassRef, _TyRefILocal, _TyVarI, _Type) classDef'Eq :: PC.ClassDef classDef'Eq = _ClassDef "Eq" ("a", _Type) mempty classDef'Ord :: PC.ClassDef classDef'Ord = _ClassDef "Ord" ("a", _Type) [_Constraint (_LocalClassRef "Eq") (_TyVarI "a")] + +classInstance'IntEq :: PC.InstanceClause +classInstance'IntEq = _InstanceClause "Eq" (_TyRefILocal "Int") diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index 193fabc7..d614432c 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -8,17 +8,21 @@ module Test.Utils.CompilerInput ( compilerInput'recDef, compilerInput'classEq, compilerInput'classOrd, + compilerInput'unboundEq, + compilerInput'IntEqInstance, ) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module ( + module'IntEqInstance, module'classEq, module'classOrd, module'either, module'incoherent, module'maybe, module'recDef, + module'unboundEq, module'undefinedForeignTyRef, module'undefinedLocalTyRef, module'undefinedVar, @@ -57,3 +61,9 @@ compilerInput'classEq = _CompilerInput [module'classEq] compilerInput'classOrd :: PC.CompilerInput compilerInput'classOrd = _CompilerInput [module'classOrd] + +compilerInput'unboundEq :: PC.CompilerInput +compilerInput'unboundEq = _CompilerInput [module'unboundEq] + +compilerInput'IntEqInstance :: PC.CompilerInput +compilerInput'IntEqInstance = _CompilerInput [module'classEq, module'IntEqInstance] diff --git a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs index c2b50674..8bed50f1 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs @@ -23,6 +23,8 @@ module Test.Utils.Constructors ( _LocalRef', _ForeignRef', _TyApp, + _Opaque, + _TyAbs', -- * Class related. _ClassDef, @@ -30,6 +32,7 @@ module Test.Utils.Constructors ( _LocalClassRef, _ForeignCI, _Constraint, + _InstanceClause, ) where import Control.Lens ((^.)) @@ -141,6 +144,14 @@ _TyAbs args body = , sourceInfo = PC.defSourceInfo } +_TyAbs' :: [(Text, PC.KindType)] -> PC.TyBody -> PC.TyAbs +_TyAbs' args body = + PC.TyAbs + { PC.tyArgs = Map.fromList [(ta ^. #argName, ta) | ta <- _TyArg <$> args] + , PC.tyBody = body + , sourceInfo = PC.defSourceInfo + } + _TyArg :: (Text, PC.KindType) -> PC.TyArg _TyArg (a, k) = PC.TyArg @@ -216,3 +227,15 @@ _ForeignCI n mn = , moduleName = mn , sourceInfo = def } + +_InstanceClause :: Text -> PC.Ty -> PC.InstanceClause +_InstanceClause n ty = + PC.InstanceClause + { classRef = _LocalClassRef n + , head = ty + , constraints = mempty + , sourceInfo = def + } + +_Opaque :: PC.TyBody +_Opaque = PC.OpaqueI def diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index 1021c5f6..c0f9806f 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -7,12 +7,15 @@ module Test.Utils.Module ( module'either, module'recDef, module'classEq, + module'unboundEq, module'classOrd, + module'IntEqInstance, ) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_Module, _ModuleName) import Test.Utils.TyDef ( + tyDef'Int, tyDef'either, tyDef'incoherent, tyDef'maybe, @@ -22,7 +25,7 @@ import Test.Utils.TyDef ( tyDef'undefinedVar, ) -import Test.Utils.ClassDef (classDef'Eq, classDef'Ord) +import Test.Utils.ClassDef (classDef'Eq, classDef'Ord, classInstance'IntEq) -- _Module mn tds cds ins = @@ -83,3 +86,15 @@ module'classEq = _Module (_ModuleName ["Module"]) mempty [classDef'Eq] mempty -} module'classOrd :: PC.Module module'classOrd = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] mempty + +module'unboundEq :: PC.Module +module'unboundEq = _Module (_ModuleName ["Module"]) mempty [classDef'Ord] mempty + +module'Int :: PC.Module +module'Int = _Module (_ModuleName ["Module"]) [] mempty mempty + +{- | 1 Module containing: + instance Eq Int. +-} +module'IntEqInstance :: PC.Module +module'IntEqInstance = _Module (_ModuleName ["Module"]) [tyDef'Int] [classDef'Eq] [classInstance'IntEq] diff --git a/lambda-buffers-compiler/test/Test/Utils/TyDef.hs b/lambda-buffers-compiler/test/Test/Utils/TyDef.hs index 56f5e569..487983e9 100644 --- a/lambda-buffers-compiler/test/Test/Utils/TyDef.hs +++ b/lambda-buffers-compiler/test/Test/Utils/TyDef.hs @@ -9,6 +9,7 @@ module Test.Utils.TyDef ( tyDef'undefinedForeignTyRef'TyRef, tyDef'recDef, tyDef'either, + tyDef'Int, ) where import LambdaBuffers.Compiler.ProtoCompat.Types (Ty (TyVarI)) @@ -17,9 +18,11 @@ import Test.Utils.Constructors ( _ForeignRef', _LocalRef', _ModuleName, + _Opaque, _SourceInfo, _TupleI, _TyAbs, + _TyAbs', _TyApp, _TyDef, _TyName, @@ -142,3 +145,7 @@ tyDef'undefinedForeignTyRef = -} tyDef'undefinedForeignTyRef'TyRef :: P.TyRef tyDef'undefinedForeignTyRef'TyRef = P.ForeignI $ _ForeignRef' "Baz" (_ModuleName ["Foreign", "Module"]) (_SourceInfo 1 2) + +-- Int +tyDef'Int :: P.TyDef +tyDef'Int = _TyDef (_TyName "Int") (_TyAbs' [] _Opaque) diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index 95f34e99..0493abaf 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -784,6 +784,82 @@ message KindCheckErrorTyDef { } } +// Kind checking errors - in a Class definition. +message KindCheckErrorClassInstance { + + // Unbound variable ty_var detected in term ty_def. + message UnboundTyVarError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + TyVar ty_var = 3; + } + + // Unbound type reference ty_ref detected in term ty_def. + message UnboundTyRefError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + TyRef ty_ref = 3; + } + + + // Unbound type class reference ty_class_ref detected in term ty_def. + message UnboundTyClassRefError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + TyClassRef ty_class_ref = 3; + } + + // In ty_def an error has occurred when trying to unify kind ty_kind_lhs + // with ty_kind_rhs. + // + // FIXME(cstml): Add source of constraint to the error such that user can see + // where the constraint was generated - therefore where the error precisely + // is. + message UnificationError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + Kind ty_kind_lhs = 3; + Kind ty_kind_rhs = 4; + } + + // A cyclic kind was encountered. Infinite kinds like this are not acceptable, + // and we do not support them. We could not construct infinite kind in ty_def. + // + // As the implementation currently stands such an error is (most likely) not + // representable - therefore not reachable. Such an error would usually occur + // for a term like: λa. a a - in which case the inference would try to unify + // two kinds of the form: m and m -> n - because m appears in both terms - + // the cyclic unification error would be thrown. + // + // In the case of LambdaBuffers - such an error is not (currently) achievable + // as the kind of the variable is given by the context - (i.e. λa : m . a a, + // where m is a kind) therefore the unification would fail with Unification + // Error. Nevertheless - future features might require it. + message CyclicKindError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + } + + // The actual_kind differs from the expected_kind. + message InconsistentTypeError { + ModuleName module_name = 1; + InstanceClause instance_clause = 2; + Kind actual_kind = 3; + Kind expected_kind = 4; + } + + // One of the errors occurred during kind checking. + oneof kind_check_error { + UnboundTyRefError unbound_ty_ref_error = 1; + UnboundTyVarError unbound_ty_var_error = 2; + UnboundTyClassRefError unbound_ty_class_ref_error = 3; + UnificationError unification_error = 4; + CyclicKindError cyclic_kind_error = 5; + InconsistentTypeError inconsistent_type_error = 6; + } +} + + /* Naming error message */ message NamingError { // One of naming errors. @@ -807,8 +883,10 @@ message CompilerError { repeated KindCheckErrorTyDef kind_check_errors_ty_defs = 4; // Errors occurred during kind checking Class definitions. repeated KindCheckErrorClassDef kind_check_errors_class_defs = 5; + // Errors occurred during kind checking Class instances. + repeated KindCheckErrorClassInstance kind_check_errors_class_instances = 6; // Errors internal to the compiler implementation. - repeated InternalError internal_errors = 6; + repeated InternalError internal_errors = 7; } // Compiler Result ~ a successful Compilation Output. From 574bbcb78bd5249d270c41cc0b64114c15ae21ec Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Tue, 7 Mar 2023 17:55:52 +0000 Subject: [PATCH 09/11] note: add fixme note. --- .../src/LambdaBuffers/Compiler/KindCheck/Inference.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 2293d113..8995af1c 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -255,6 +255,10 @@ runClassInstanceCheck ctx modName classInst = do (_, c) <- runDerive ctx modName $ deriveClassInst classInst void $ runUnify' c +{- | NOTE(cstml): This is a partial solution because I am not clear where to pluck + the variables from and how to work with the constraints in this case. same + applies to the above definition check. +-} deriveClassInst :: PC.InstanceClause -> Derive () deriveClassInst instClause = do void $ deriveClassInstDef instClause From 5a2d9fed7770f3af0ba43f182f214d86815a0617 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Wed, 8 Mar 2023 10:25:31 +0000 Subject: [PATCH 10/11] update: passing test? --- lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs | 3 ++- lambda-buffers-compiler/test/Test/Utils/Module.hs | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index d614432c..c7b96ab5 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -15,6 +15,7 @@ module Test.Utils.CompilerInput ( import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module ( + module'Int, module'IntEqInstance, module'classEq, module'classOrd, @@ -66,4 +67,4 @@ compilerInput'unboundEq :: PC.CompilerInput compilerInput'unboundEq = _CompilerInput [module'unboundEq] compilerInput'IntEqInstance :: PC.CompilerInput -compilerInput'IntEqInstance = _CompilerInput [module'classEq, module'IntEqInstance] +compilerInput'IntEqInstance = _CompilerInput [module'classEq, module'IntEqInstance, module'Int] diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index c0f9806f..3eb9c05a 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -10,6 +10,7 @@ module Test.Utils.Module ( module'unboundEq, module'classOrd, module'IntEqInstance, + module'Int, ) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC From 708fee5b814f9e1d08389ce5152b2f51d3c40d33 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Wed, 8 Mar 2023 17:21:12 +0000 Subject: [PATCH 11/11] update: Variable logic in instances --- .../Compiler/KindCheck/Inference.hs | 26 ++++++++++++++----- .../Compiler/ProtoCompat/Types.hs | 3 ++- .../test/Test/KindCheck/TyClass.hs | 19 +++++++++++--- .../test/Test/Utils/ClassDef.hs | 10 +++++-- .../test/Test/Utils/CompilerInput.hs | 10 +++++++ .../test/Test/Utils/Constructors.hs | 10 +++++++ .../test/Test/Utils/Module.hs | 16 +++++++++++- 7 files changed, 81 insertions(+), 13 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 8995af1c..4ce69c1e 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -32,6 +32,7 @@ import Control.Monad.Freer.State (State, evalState, get, put) import Control.Monad.Freer.Writer (Writer, runWriter, tell) import Data.Foldable (foldrM, traverse_) import Data.Map qualified as M +import Data.Set qualified as S import Data.Text (Text) import Data.Text qualified as T import LambdaBuffers.Compiler.KindCheck.Derivation ( @@ -255,15 +256,28 @@ runClassInstanceCheck ctx modName classInst = do (_, c) <- runDerive ctx modName $ deriveClassInst classInst void $ runUnify' c -{- | NOTE(cstml): This is a partial solution because I am not clear where to pluck - the variables from and how to work with the constraints in this case. same - applies to the above definition check. --} deriveClassInst :: PC.InstanceClause -> Derive () deriveClassInst instClause = do - void $ deriveClassInstDef instClause - traverse_ deriveConstraint $ instClause ^. #constraints + let vs = getTyVariables (instClause ^. #head) + extraContext <- generateKinds vs + void $ local (<> extraContext) $ do + void $ deriveClassInstDef instClause + traverse_ deriveConstraint $ instClause ^. #constraints where + getTyVariables :: PC.Ty -> S.Set PC.TyVar + getTyVariables = \case + PC.TyVarI v -> S.singleton v + PC.TyAppI l -> getTyVariables (l ^. #tyFunc) <> mconcat (getTyVariables <$> l ^. #tyArgs) + PC.TyRefI _ -> mempty + + generateKinds :: S.Set PC.TyVar -> Derive Context + generateKinds s = fmap mconcat $ traverse generateKind $ S.toList s + where + generateKind :: PC.TyVar -> Derive Context + generateKind tv = do + freshK <- KVar <$> fresh + pure $ mempty & addContext .~ M.singleton (mkInfoLess $ TyVar $ tv ^. #varName) freshK + deriveClassInstDef :: PC.InstanceClause -> Derive Derivation deriveClassInstDef ic = do ctx <- ask diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 73f06ca4..ee7c60c9 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -365,7 +365,8 @@ data CompilerError CKC'TyDefError (KindCheckError TyDef) | -- | Compiler KindChecker Error - within a Class Definition. CKC'ClassDefError (KindCheckError ClassDef) - | CKC'ClassInstanceError (KindCheckError InstanceClause) + | -- | Compiler KindChecker Error - within a Class Instance. + CKC'ClassInstanceError (KindCheckError InstanceClause) | C'InternalError Text deriving stock (Show, Eq, Ord, Generic) deriving anyclass (SOP.Generic) diff --git a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs index b786d20b..510ea5f8 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck/TyClass.hs @@ -5,7 +5,14 @@ import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerInput) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (Assertion, testCase, (@?=)) import Test.Tasty.Providers (TestName) -import Test.Utils.CompilerInput (compilerInput'IntEqInstance, compilerInput'classEq, compilerInput'classOrd, compilerInput'unboundEq) +import Test.Utils.CompilerInput ( + compilerInput'IntEqInstance, + compilerInput'classEq, + compilerInput'classOrd, + compilerInput'classOrdInstanceEq, + compilerInput'failingAdditionalVarConstraint, + compilerInput'unboundEq, + ) import Test.Utils.Constructors () import Test.Utils.TyDef () @@ -14,7 +21,7 @@ test = testGroup "KC Class Error." [ testGroup "Class Defs." [ok'Eq, ok'Ord, fail'Ord] - , testGroup "Class Instances." [ok'IntEqInstance] + , testGroup "Class Instances." [ok'IntEqInstance, ok'OrdInstanceEq, fail'RedundantVar] ] -------------------------------------------------------------------------------- @@ -33,7 +40,13 @@ fail'Ord = failCase "Unbound reference to eq." compilerInput'unboundEq -- Class Instances ok'IntEqInstance :: TestTree -ok'IntEqInstance = oKCase "Int Eq Instance." compilerInput'IntEqInstance +ok'IntEqInstance = oKCase "instance Int Eq." compilerInput'IntEqInstance + +ok'OrdInstanceEq :: TestTree +ok'OrdInstanceEq = oKCase "instance Ord a => Eq a." compilerInput'classOrdInstanceEq + +fail'RedundantVar :: TestTree +fail'RedundantVar = failCase "instance Ord b => Eq a." compilerInput'failingAdditionalVarConstraint -------------------------------------------------------------------------------- -- Utils diff --git a/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs index b88ac1f3..f1afc03f 100644 --- a/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs +++ b/lambda-buffers-compiler/test/Test/Utils/ClassDef.hs @@ -1,7 +1,7 @@ -module Test.Utils.ClassDef (classDef'Eq, classDef'Ord, classInstance'IntEq) where +module Test.Utils.ClassDef (classDef'Eq, classDef'Ord, classInstance'IntEq, classInstance'OrdEq, classInstance'OrdEqFailing) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC -import Test.Utils.Constructors (_ClassDef, _Constraint, _InstanceClause, _LocalClassRef, _TyRefILocal, _TyVarI, _Type) +import Test.Utils.Constructors (_ClassDef, _Constraint, _InstanceClause, _InstanceClause', _LocalClassRef, _TyRefILocal, _TyVarI, _Type) classDef'Eq :: PC.ClassDef classDef'Eq = _ClassDef "Eq" ("a", _Type) mempty @@ -11,3 +11,9 @@ classDef'Ord = _ClassDef "Ord" ("a", _Type) [_Constraint (_LocalClassRef "Eq") ( classInstance'IntEq :: PC.InstanceClause classInstance'IntEq = _InstanceClause "Eq" (_TyRefILocal "Int") + +classInstance'OrdEq :: PC.InstanceClause +classInstance'OrdEq = _InstanceClause' "Eq" (_TyVarI "a") [_Constraint (_LocalClassRef "Ord") (_TyVarI "a")] + +classInstance'OrdEqFailing :: PC.InstanceClause +classInstance'OrdEqFailing = _InstanceClause' "Eq" (_TyVarI "a") [_Constraint (_LocalClassRef "Ord") (_TyVarI "b")] diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index c7b96ab5..9b1927a8 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -10,13 +10,17 @@ module Test.Utils.CompilerInput ( compilerInput'classOrd, compilerInput'unboundEq, compilerInput'IntEqInstance, + compilerInput'classOrdInstanceEq, + compilerInput'failingAdditionalVarConstraint, ) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module ( + module'AdditionalVarEqInstance, module'Int, module'IntEqInstance, + module'OrdEqInstance, module'classEq, module'classOrd, module'either, @@ -63,8 +67,14 @@ compilerInput'classEq = _CompilerInput [module'classEq] compilerInput'classOrd :: PC.CompilerInput compilerInput'classOrd = _CompilerInput [module'classOrd] +compilerInput'classOrdInstanceEq :: PC.CompilerInput +compilerInput'classOrdInstanceEq = _CompilerInput [module'OrdEqInstance] + compilerInput'unboundEq :: PC.CompilerInput compilerInput'unboundEq = _CompilerInput [module'unboundEq] compilerInput'IntEqInstance :: PC.CompilerInput compilerInput'IntEqInstance = _CompilerInput [module'classEq, module'IntEqInstance, module'Int] + +compilerInput'failingAdditionalVarConstraint :: PC.CompilerInput +compilerInput'failingAdditionalVarConstraint = _CompilerInput [module'AdditionalVarEqInstance] diff --git a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs index 8bed50f1..2d7c82de 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs @@ -33,6 +33,7 @@ module Test.Utils.Constructors ( _ForeignCI, _Constraint, _InstanceClause, + _InstanceClause', ) where import Control.Lens ((^.)) @@ -228,6 +229,15 @@ _ForeignCI n mn = , sourceInfo = def } +_InstanceClause' :: Text -> PC.Ty -> [PC.Constraint] -> PC.InstanceClause +_InstanceClause' n ty cs = + PC.InstanceClause + { classRef = _LocalClassRef n + , head = ty + , constraints = cs + , sourceInfo = def + } + _InstanceClause :: Text -> PC.Ty -> PC.InstanceClause _InstanceClause n ty = PC.InstanceClause diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index 3eb9c05a..38dd16a5 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -11,6 +11,8 @@ module Test.Utils.Module ( module'classOrd, module'IntEqInstance, module'Int, + module'OrdEqInstance, + module'AdditionalVarEqInstance, ) where import LambdaBuffers.Compiler.ProtoCompat qualified as PC @@ -26,7 +28,13 @@ import Test.Utils.TyDef ( tyDef'undefinedVar, ) -import Test.Utils.ClassDef (classDef'Eq, classDef'Ord, classInstance'IntEq) +import Test.Utils.ClassDef ( + classDef'Eq, + classDef'Ord, + classInstance'IntEq, + classInstance'OrdEq, + classInstance'OrdEqFailing, + ) -- _Module mn tds cds ins = @@ -99,3 +107,9 @@ module'Int = _Module (_ModuleName ["Module"]) [] mempty mempty -} module'IntEqInstance :: PC.Module module'IntEqInstance = _Module (_ModuleName ["Module"]) [tyDef'Int] [classDef'Eq] [classInstance'IntEq] + +module'OrdEqInstance :: PC.Module +module'OrdEqInstance = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] [classInstance'OrdEq] + +module'AdditionalVarEqInstance :: PC.Module +module'AdditionalVarEqInstance = _Module (_ModuleName ["Module"]) mempty [classDef'Eq, classDef'Ord] [classInstance'OrdEqFailing]