From 9656c0b86bc1293125a3a3c07cbd44d380ff3572 Mon Sep 17 00:00:00 2001 From: Heinrich Apfelmus Date: Fri, 20 Oct 2023 14:40:44 +0200 Subject: [PATCH] Implement assertion `==` on module identities --- lib/fine-types/fine-types.cabal | 1 + .../FineTypes/Commands/Check/PrettyPrinter.hs | 25 +++++++++++- .../src/Language/FineTypes/Package.hs | 3 ++ .../src/Language/FineTypes/Package/Compile.hs | 11 +++++- .../src/Language/FineTypes/Package/Content.hs | 39 ++++++++++++++++++- .../Language/FineTypes/Package/Description.hs | 6 ++- .../src/Language/FineTypes/Package/Parser.hs | 32 +++++++++++---- .../FineTypes/Package/PrettyPrinter.hs | 19 +++++++++ lib/fine-types/test/data/package/P2.fine | 2 + 9 files changed, 125 insertions(+), 13 deletions(-) create mode 100644 lib/fine-types/src/Language/FineTypes/Package/PrettyPrinter.hs diff --git a/lib/fine-types/fine-types.cabal b/lib/fine-types/fine-types.cabal index 7dd7663..4a04811 100644 --- a/lib/fine-types/fine-types.cabal +++ b/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 diff --git a/lib/fine-types/src/Language/FineTypes/Commands/Check/PrettyPrinter.hs b/lib/fine-types/src/Language/FineTypes/Commands/Check/PrettyPrinter.hs index d746732..2022bd0 100644 --- a/lib/fine-types/src/Language/FineTypes/Commands/Check/PrettyPrinter.hs +++ b/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) @@ -68,6 +69,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 @@ -102,6 +107,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 diff --git a/lib/fine-types/src/Language/FineTypes/Package.hs b/lib/fine-types/src/Language/FineTypes/Package.hs index 2a39eec..f09a656 100644 --- a/lib/fine-types/src/Language/FineTypes/Package.hs +++ b/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 diff --git a/lib/fine-types/src/Language/FineTypes/Package/Compile.hs b/lib/fine-types/src/Language/FineTypes/Package/Compile.hs index 1232654..3d6bc00 100644 --- a/lib/fine-types/src/Language/FineTypes/Package/Compile.hs +++ b/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 diff --git a/lib/fine-types/src/Language/FineTypes/Package/Content.hs b/lib/fine-types/src/Language/FineTypes/Package/Content.hs index 9528a07..1a399ba 100644 --- a/lib/fine-types/src/Language/FineTypes/Package/Content.hs +++ b/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) @@ -39,6 +42,9 @@ import Language.FineTypes.Module.Instance , getDeclarations , mkModuleInstance ) +import Language.FineTypes.Package.Description + ( Assertion (..) + ) import Language.FineTypes.Signature (Signature (..)) import Language.FineTypes.Typ (TypName) @@ -192,3 +198,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 diff --git a/lib/fine-types/src/Language/FineTypes/Package/Description.hs b/lib/fine-types/src/Language/FineTypes/Package/Description.hs index 807570c..eb2dcd9 100644 --- a/lib/fine-types/src/Language/FineTypes/Package/Description.hs +++ b/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 diff --git a/lib/fine-types/src/Language/FineTypes/Package/Parser.hs b/lib/fine-types/src/Language/FineTypes/Package/Parser.hs index 9c5766e..b1fe06d 100644 --- a/lib/fine-types/src/Language/FineTypes/Package/Parser.hs +++ b/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 = diff --git a/lib/fine-types/src/Language/FineTypes/Package/PrettyPrinter.hs b/lib/fine-types/src/Language/FineTypes/Package/PrettyPrinter.hs new file mode 100644 index 0000000..b3adbe9 --- /dev/null +++ b/lib/fine-types/src/Language/FineTypes/Package/PrettyPrinter.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Language.FineTypes.Package.PrettyPrinter + ( prettyAssertion + ) where + +import Language.FineTypes.Package.Description + ( Assertion (..) + ) +import Prettyprinter + ( Doc + , Pretty (pretty) + , (<+>) + ) + +-- | Pretty print an 'Assertion'. +prettyAssertion :: Assertion -> Doc ann +prettyAssertion (Equal a b) = + pretty a <+> "==" <+> pretty b diff --git a/lib/fine-types/test/data/package/P2.fine b/lib/fine-types/test/data/package/P2.fine index 1bb5bcc..0d2f2a7 100644 --- a/lib/fine-types/test/data/package/P2.fine +++ b/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;