new: add multiple declaration check + test

Author: cstml

lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs

@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 module LambdaBuffers.Compiler.KindCheck (
   -- * Kindchecking functions.
   check,
@@ -11,9 +13,10 @@ module LambdaBuffers.Compiler.KindCheck (
 
 import Control.Lens (view, (&), (.~), (^.))
 import Control.Monad (void)
-import Control.Monad.Freer (Eff, Members, reinterpret, run)
+import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
 import Control.Monad.Freer.Reader (Reader, ask, runReader)
+import Control.Monad.Freer.State (State, evalState, get, modify)
 import Control.Monad.Freer.TH (makeEffect)
 import Data.Foldable (traverse_)
 import Data.List.NonEmpty (NonEmpty ((:|)), uncons, (<|))
@@ -36,51 +39,12 @@ import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
 import LambdaBuffers.Compiler.KindCheck.Type (Type (App))
 import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef))
 import LambdaBuffers.Compiler.ProtoCompat (kind2ProtoKind)
-import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P (
-  ClassDef,
-  CompilerError (..),
-  CompilerInput,
-  Constructor,
-  Field,
-  ForeignRef,
-  InstanceClause,
-  Kind,
-  KindCheckError (
-    InconsistentTypeError,
-    IncorrectApplicationError,
-    RecursiveKindError,
-    UnboundTermError
-  ),
-  KindRefType (KType),
-  KindType (KindArrow, KindRef),
-  LocalRef,
-  Module,
-  ModuleName,
-  Product (..),
-  Record,
-  SourceInfo (SourceInfo),
-  SourcePosition (SourcePosition),
-  Sum,
-  Tuple,
-  Ty (..),
-  TyAbs,
-  TyApp,
-  TyArg,
-  TyBody (..),
-  TyDef (TyDef),
-  TyName,
-  TyRef (..),
-  TyVar,
-  VarName (VarName),
- )
+import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PT
 
 --------------------------------------------------------------------------------
 -- Types
 
--- FIXME(cstml) - We should add the following tests:
--- - double declaration of a type
-
 -- | Kind Check failure types.
 type CompilerErr = P.CompilerError
 
@@ -121,20 +85,27 @@ makeEffect ''KindCheck
 
 --------------------------------------------------------------------------------
 
-runCheck :: Eff (Check ': '[]) a -> Either CompilerErr a
+-- | The Check effect runner.
+runCheck :: Eff '[Check, Err] a -> Either CompilerErr a
 runCheck = run . runError . runKindCheck . localStrategy . moduleStrategy . globalStrategy
 
--- | Run the check - return the validated context or the failure.
+{- | Run the check - return the validated context or the failure. The main API
+ function of the library.
+-}
 check :: P.CompilerInput -> PT.CompilerOutput
 check = fmap (const PT.CompilerResult) . runCheck . kCheck
 
--- | Run the check - drop the result if it succeeds.
+-- | Run the check - drop the result if it succeeds - useful for testing.
 check_ :: P.CompilerInput -> Either CompilerErr ()
 check_ = void . runCheck . kCheck
 
 --------------------------------------------------------------------------------
 
-type Transform x y = forall effs {a}. Eff (x ': effs) a -> Eff (y ': effs) a
+{- | A transformation (in the context of the Kind Checker) is a mapping from one
+ Effect to another. All effects can fial via the `Err` effect - which is
+ essentially the Kind Check failure.
+-}
+type Transform x y = forall effs {a}. Member Err effs => Eff (x ': effs) a -> Eff (y ': effs) a
 
 -- Transformation strategies
 globalStrategy :: Transform Check GlobalCheck
@@ -146,7 +117,7 @@ globalStrategy = reinterpret $ \case
 
 moduleStrategy :: Transform GlobalCheck ModuleCheck
 moduleStrategy = reinterpret $ \case
-  CreateContext ci -> resolveCreateContext ci
+  CreateContext ci -> evalState (mempty @(M.Map Variable P.TyName)) . resolveCreateContext $ ci
   ValidateModule cx md -> do
     traverse_ (kCTypeDefinition (module2ModuleName md) cx) (md ^. #typeDefs)
     traverse_ (kCClassInstance cx) (md ^. #instances)
@@ -159,14 +130,14 @@ localStrategy = reinterpret $ \case
   KCClassInstance _ctx _instClause -> pure () -- "FIXME(cstml)"
   KCClass _ctx _classDef -> pure () --  "FIXME(cstml)"
 
-runKindCheck :: Eff '[KindCheck] a -> Eff '[Err] a
-runKindCheck = reinterpret $ \case
+runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
+runKindCheck = interpret $ \case
   KindFromTyDef moduleName tydef -> runReader moduleName (tyDef2Type tydef)
   -- TyDefToTypes moduleName tydef -> runReader moduleName (tyDef2Types tydef)
   InferTypeKind _modName tyDef ctx ty -> either (handleErr tyDef) pure $ infer ctx ty
   CheckKindConsistency mname def ctx k -> runReader mname $ resolveKindConsistency def ctx k
   where
-    handleErr :: forall a. P.TyDef -> InferErr -> Eff '[Err] a
+    handleErr :: forall {b}. P.TyDef -> InferErr -> Eff effs b
     handleErr td = \case
       InferUnboundTermErr uA ->
         throwError . P.CompKindCheckError $ P.UnboundTermError (tyDef2TyName td) (var2VarName uA)
@@ -208,15 +179,50 @@ resolveKindConsistency tydef _ctx inferredKind = do
           throwError . P.CompKindCheckError $
             P.InconsistentTypeError n (kind2ProtoKind i) (kind2ProtoKind d)
 
-resolveCreateContext :: forall effs. P.CompilerInput -> Eff effs Context
-resolveCreateContext ci = mconcat <$> traverse module2Context (ci ^. #modules)
-
 tyDef2TyName :: P.TyDef -> P.TyName
 tyDef2TyName (P.TyDef n _ _) = n
 
-module2Context :: forall effs. P.Module -> Eff effs Context
-module2Context m = mconcat <$> traverse (tyDef2Context (moduleName2ModName (m ^. #moduleName))) (m ^. #typeDefs)
+--------------------------------------------------------------------------------
+-- Context Creation
 
+{- | Resolver function for the context creation - it fails if two identical
+ declarations are found.
+-}
+resolveCreateContext ::
+  forall effs.
+  Member (State (M.Map Variable P.TyName)) effs =>
+  Member Err effs =>
+  P.CompilerInput ->
+  Eff effs Context
+resolveCreateContext ci = do
+  ctxs <- traverse module2Context (ci ^. #modules)
+  pure $ mconcat ctxs
+
+module2Context :: forall effs. Member (State (M.Map Variable P.TyName)) effs => Member Err effs => P.Module -> Eff effs Context
+module2Context m = do
+  let typeDefinitions = m ^. #typeDefs
+  ctxs <- traverse (tyDef2Context (moduleName2ModName (m ^. #moduleName))) typeDefinitions
+  pure $ mconcat ctxs
+
+-- | Creates a Context entry from one type definition.
+tyDef2Context :: forall effs. Member (State (M.Map Variable P.TyName)) effs => Member Err effs => ModName -> P.TyDef -> Eff effs Context
+tyDef2Context curModName tyDef@(P.TyDef tyName _ _) = do
+  r@(v, _) <- tyDef2NameAndKind curModName tyDef
+  associateName v tyName
+  pure $ mempty & context .~ uncurry M.singleton r
+  where
+    -- Ads the name to our map - we can use its SourceLocation in the case of a
+    -- double use. If it's already in our map - that means we've double declared it.
+    associateName :: Variable -> P.TyName -> Eff effs ()
+    associateName v t = do
+      maps <- get @(M.Map Variable P.TyName)
+      case maps M.!? v of
+        Just otherTyName -> throwError . PT.CompReaderError $ PT.MultipleDeclaration otherTyName t
+        Nothing -> modify (M.insert v t)
+
+{- | Converts the Proto Module name to a local modname - dropping the
+ information.
+-}
 moduleName2ModName :: P.ModuleName -> ModName
 moduleName2ModName mName = (\p -> p ^. #name) <$> mName ^. #parts
 
@@ -227,11 +233,6 @@ tyDef2NameAndKind curModName tyDef = do
   let k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
   pure (name, k)
 
-tyDef2Context :: forall effs. ModName -> P.TyDef -> Eff effs Context
-tyDef2Context curModName tyDef = do
-  r <- tyDef2NameAndKind curModName tyDef
-  pure $ mempty & context .~ uncurry M.singleton r
-
 tyAbsLHS2Kind :: P.TyAbs -> Kind
 tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs)
 

lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs

@@ -41,6 +41,7 @@ module LambdaBuffers.Compiler.ProtoCompat.Types (
   TyRef (..),
   TyVar (..),
   VarName (..),
+  ReaderError (..),
   module VARS,
 ) where
 
@@ -289,8 +290,19 @@ data KindCheckError
   deriving (Arbitrary) via GenericArbitrary KindCheckError
 instance Exception KindCheckError
 
+{- | Reader errors are validation errors which are not directly tied to the kind
+ checking.
+-}
+data ReaderError
+  = -- | The following type@(TyName) was declared here@(SourceInfo) and here@(SourceInfo).
+    MultipleDeclaration TyName TyName
+  deriving stock (Show, Eq, Ord, Generic)
+  deriving (Arbitrary) via GenericArbitrary ReaderError
+
+-- | All the compiler errors.
 data CompilerError
   = CompKindCheckError KindCheckError
+  | CompReaderError ReaderError
   | InternalError Text
   deriving stock (Show, Eq, Ord, Generic)
   deriving (Arbitrary) via GenericArbitrary CompilerError

lambda-buffers-compiler/test/Test/KindCheck.hs

@@ -12,9 +12,8 @@ import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var))
 import LambdaBuffers.Compiler.KindCheck.Variable (
   Variable (LocalRef),
  )
-import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P (
-  CompilerInput (CompilerInput),
- )
+import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P
+
 import Test.QuickCheck (
   Arbitrary (arbitrary, shrink),
   Property,
@@ -25,9 +24,11 @@ import Test.QuickCheck (
   (===),
  )
 import Test.Samples.Proto.CompilerInput (
+  compilerInput'doubleDeclaration,
   compilerInput'incoherent,
   compilerInput'maybe,
  )
+import Test.Samples.Proto.Utils (_tyName)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (assertBool, testCase, (@?=))
 import Test.Tasty.QuickCheck (testProperty)
@@ -36,7 +37,18 @@ import Test.Tasty.QuickCheck (testProperty)
 -- Top Level tests
 
 test :: TestTree
-test = testGroup "Compiler tests" [testCheck, testFolds, testRefl]
+test = testGroup "Compiler tests" [testCheck, testFolds, testRefl, testMultipleDec]
+
+--------------------------------------------------------------------------------
+-- Multiple declaration test
+
+testMultipleDec :: TestTree
+testMultipleDec = testGroup "Multiple declaration tests." [doubleDeclaration]
+
+doubleDeclaration :: TestTree
+doubleDeclaration =
+  testCase "Two declarations of the same type was not detected." $
+    check_ compilerInput'doubleDeclaration @?= Left (P.CompReaderError $ P.MultipleDeclaration (_tyName "Maybe") (_tyName "Maybe"))
 
 --------------------------------------------------------------------------------
 -- Module tests
@@ -78,8 +90,8 @@ kcTestOrdering =
       shuffledMods <- shuffle mods
       pure (P.CompilerInput mods, P.CompilerInput shuffledMods)
 
-    eitherFailOrPass :: forall {a} {c}. Either a c -> Either () ()
-    eitherFailOrPass = bimap (const ()) (const ())
+eitherFailOrPass :: forall {a} {c}. Either a c -> Either () ()
+eitherFailOrPass = bimap (const ()) (const ())
 
 --------------------------------------------------------------------------------
 -- Fold tests

lambda-buffers-compiler/test/Test/Samples/Proto/CompilerInput.hs

@@ -1,4 +1,4 @@
-module Test.Samples.Proto.CompilerInput (compilerInput'incoherent, compilerInput'maybe) where
+module Test.Samples.Proto.CompilerInput (compilerInput'incoherent, compilerInput'maybe, compilerInput'doubleDeclaration) where
 
 import Control.Lens ((&), (.~))
 import LambdaBuffers.Compiler.ProtoCompat qualified as P
@@ -11,3 +11,7 @@ compilerInput'maybe = P.CompilerInput {P.modules = [module'maybe]}
 -- | Contains 2 definitions - 1 wrong one.
 compilerInput'incoherent :: P.CompilerInput
 compilerInput'incoherent = compilerInput'maybe & #modules .~ [module'incoherent]
+
+-- | Declares maybe twice.
+compilerInput'doubleDeclaration :: P.CompilerInput
+compilerInput'doubleDeclaration = compilerInput'maybe <> compilerInput'maybe