Implement assertion == on module identities

lib/fine-types/fine-types.cabal

@@ -118,6 +118,7 @@ library
     Language.FineTypes.Package.Content
     Language.FineTypes.Package.Description
     Language.FineTypes.Package.Parser
+    Language.FineTypes.Package.PrettyPrinter
     Language.FineTypes.ToExpr
 
 

lib/fine-types/src/Language/FineTypes/Commands/Check/PrettyPrinter.hs

@@ -9,11 +9,12 @@ import Data.Foldable (toList)
 import Language.FineTypes.Module.Parser (ErrParseModule (..))
 import Language.FineTypes.Package
     ( ErrAddModule (..)
+    , ErrAssertion (..)
     , ErrCompilePackage (..)
     , ErrIncludePackage (..)
-    , ErrParsePackage
+    , ErrParsePackage (..)
     )
-import Language.FineTypes.Package.Parser (ErrParsePackage (..))
+import Language.FineTypes.Package.PrettyPrinter (prettyAssertion)
 import Prettyprinter
     ( Doc
     , Pretty (pretty)
@@ -67,6 +68,10 @@ prettyPrintCompilePackage = \case
             <+> pretty mn
             <+> prettyString "vs"
             <+> pretty mn'
+    ErrAssertFailed assertion e ->
+        prettyString "Assertion failed:"
+            <+> prettyAssertion assertion
+                </> indent 4 (prettyPrintCheckAssertion e)
 
 prettyPrintAddModule :: ErrAddModule -> Doc ann
 prettyPrintAddModule = \case
@@ -86,6 +91,22 @@ prettyPrintIncludePackage = \case
     ErrModulesAlreadyInScope ms ->
         prettyString "Modules already in scope:" <+> pretty (toList ms)
 
+prettyPrintCheckAssertion :: ErrAssertion -> Doc ann
+prettyPrintCheckAssertion = \case
+    ErrNameNotInScope n ->
+        prettyString "Module name not in scope:" <+> pretty n
+    ErrUnequal ida idb ->
+        prettyString "Module identities are not equal:"
+            </> indent
+                4
+                ( pretty (show ida)
+                    </> prettyString "=/="
+                    </> pretty (show idb)
+                )
+
+{-----------------------------------------------------------------------------
+    Utilities
+------------------------------------------------------------------------------}
 (</>) :: Doc ann -> Doc ann -> Doc ann
 x </> y = x <> line <> y
 

lib/fine-types/src/Language/FineTypes/Package.hs

@@ -6,6 +6,8 @@ module Language.FineTypes.Package
     , emptyPackage
     , includePackage
     , addModule
+    , addSignature
+    , checkAssertion
 
       -- * Package descriptions
     , PackageDescription (..)
@@ -20,6 +22,7 @@ module Language.FineTypes.Package
     , ErrCompilePackage (..)
     , ErrIncludePackage (..)
     , ErrAddModule (..)
+    , ErrAssertion (..)
     ) where
 
 import Language.FineTypes.Package.Compile

lib/fine-types/src/Language/FineTypes/Package/Compile.hs

@@ -23,15 +23,18 @@ import Language.FineTypes.Module (ModuleName, moduleName)
 import Language.FineTypes.Module.Parser (ErrParseModule (..), parseModule')
 import Language.FineTypes.Package.Content
     ( ErrAddModule
+    , ErrAssertion
     , ErrIncludePackage
     , Package (..)
     , addModule
     , addSignature
+    , checkAssertion
     , emptyPackage
     , includePackage
     )
 import Language.FineTypes.Package.Description
-    ( PackageDescription (..)
+    ( Assertion (..)
+    , PackageDescription (..)
     , PackageName
     , Source (..)
     , Statement (..)
@@ -70,6 +73,8 @@ data ErrCompilePackage
     | -- | The module name in the module statement does
       -- not match the included module name
       ErrAddModuleNameMismatch ModuleName ModuleName
+    | -- | Checking the given assertion failed.
+      ErrAssertFailed Assertion ErrAssertion
     deriving (Eq, Show, Generic)
 
 instance ToExpr ErrCompilePackage
@@ -130,7 +135,9 @@ execStatement dir pkg (Signature modName source) = do
         $ modName == signatureName m
     exceptT (ErrAddModule modName)
         $ addSignature m pkg
-execStatement _ pkg (Assert _) =
+execStatement _ pkg (Assert assertion) = do
+    exceptT (ErrAssertFailed assertion)
+        $ checkAssertion pkg assertion
     pure pkg
 
 loadSource

lib/fine-types/src/Language/FineTypes/Package/Content.hs

@@ -9,17 +9,20 @@ module Language.FineTypes.Package.Content
     , emptyPackage
     , includePackage
     , addModule
+    , addSignature
+    , checkAssertion
 
       -- * Error types
     , ErrIncludePackage (..)
     , ErrAddModule (..)
-    , addSignature
+    , ErrAssertion (..)
     ) where
 
 import Prelude
 
 import Data.Foldable (fold)
 import Data.Map (Map)
+import Data.Maybe (isNothing)
 import Data.Set (Set)
 import Data.TreeDiff (ToExpr)
 import GHC.Generics (Generic)
@@ -38,6 +41,9 @@ import Language.FineTypes.Module.Instance
     , getDeclarations
     , mkModuleInstance
     )
+import Language.FineTypes.Package.Description
+    ( Assertion (..)
+    )
 import Language.FineTypes.Signature (Signature (..))
 import Language.FineTypes.Typ (TypName)
 
@@ -185,3 +191,34 @@ addSignature sig@Signature{..} Package{..}
                         (Left sig)
                         packageModules
                 }
+
+{-----------------------------------------------------------------------------
+    Operations
+    Check an assertion
+------------------------------------------------------------------------------}
+
+data ErrAssertion
+    = -- | Name not in scope
+      ErrNameNotInScope ModuleName
+    | -- | The two modules are not equal.
+      ErrUnequal ModuleIdentity ModuleIdentity
+    deriving (Eq, Show, Generic)
+
+instance ToExpr ErrAssertion
+
+-- | Check whether an 'Assertion' on the current 'Package' holds.
+checkAssertion :: Package -> Assertion -> Either ErrAssertion ()
+checkAssertion Package{packageModules} (Equal a b)
+    | mida == midb = Right ()
+    | isNothing mida =
+        Left $ ErrNameNotInScope a
+    | isNothing midb =
+        Left $ ErrNameNotInScope b
+    | Just ida <- mida
+    , Just idb <- midb =
+        Left $ ErrUnequal ida idb
+    | otherwise =
+        error "impossible"
+  where
+    mida = getIdentity <$> Map.lookup a packageModules
+    midb = getIdentity <$> Map.lookup b packageModules

lib/fine-types/src/Language/FineTypes/Package/Description.hs

@@ -42,4 +42,8 @@ instance ToExpr Source
 {-----------------------------------------------------------------------------
     Assertions
 ------------------------------------------------------------------------------}
-type Assertion = ()
+data Assertion
+    = Equal ModuleName ModuleName
+    deriving (Eq, Show, Generic)
+
+instance ToExpr Assertion

lib/fine-types/src/Language/FineTypes/Package/Parser.hs

@@ -13,7 +13,8 @@ import Data.Void (Void)
 import GHC.Generics (Generic)
 import Language.FineTypes.Module.Parser (moduleName)
 import Language.FineTypes.Package.Description
-    ( PackageDescription (PackageDescription)
+    ( Assertion (..)
+    , PackageDescription (PackageDescription)
     , PackageName
     , Source (..)
     , Statement (..)
@@ -68,12 +69,29 @@ statements = statement `endBy` symbol ";"
 
 statement :: Parser Statement
 statement =
-    (Include <$ symbol "include" <*> packageName <*> source)
-        <|> (Module <$ symbol "module" <*> moduleName <*> renaming <*> source)
-        <|> (Signature <$ symbol "signature" <*> moduleName <*> source)
-        <|> (Assert () <$ symbol "assert")
-  where
-    renaming = optional (symbol "renaming" *> moduleName)
+    include
+        <|> module'
+        <|> signature'
+        <|> assert
+
+include :: Parser Statement
+include = Include <$ symbol "include" <*> packageName <*> source
+
+module' :: Parser Statement
+module' =
+    Module
+        <$ symbol "module"
+        <*> moduleName
+        <*> optional (symbol "renaming" *> moduleName)
+        <*> source
+
+signature' :: Parser Statement
+signature' = Signature <$ symbol "signature" <*> moduleName <*> source
+
+assert :: Parser Statement
+assert =
+    (Assert <$ symbol "assert")
+        <*> (Equal <$> moduleName <* symbol "==" <*> moduleName)
 
 source :: Parser Source
 source =

lib/fine-types/test/data/package/P2.fine

@@ -5,3 +5,5 @@ module Y from "Y.fine";
 
 module Xoops renaming X from "X.fine";
 module Z from "Z.fine";
+
+assert X == Xoops;