From c100812cd00364f11a21b6bc08ab211848b29bf0 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 22 Nov 2024 13:13:26 +0100 Subject: [PATCH] Add deriving for Eq (#3176) This pr adds automatic implementation of `Eq` instances for inductive types. To create such an instance the user will use the same syntax as a regular instance with two differences. 1. It is prefixed with the `deriving` keyword. 2. It has no body. E.g. ``` deriving instance eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B); ``` This desugars into an instance that returns true when the constructors match and all arguments are equal according to their respective instances. There is no special handling of type errors occurring in the generated code. I.e. if the user forgets a necessary instance argument in the type signature, a type error will occur in the generated code. ## Stdlib PR - https://github.com/anoma/juvix-stdlib/pull/148 # Future work * In the future we should look at https://www.dreixel.net/research/pdf/gdmh_nocolor.pdf * See also: https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/generic-deriving --------- Co-authored-by: Lukasz Czajka --- juvix-stdlib | 2 +- .../Backend/Html/Translation/FromTyped.hs | 13 +- .../Markdown/Translation/FromTyped/Source.hs | 15 +- src/Juvix/Compiler/Builtins.hs | 2 + src/Juvix/Compiler/Builtins/Eq.hs | 25 + src/Juvix/Compiler/Concrete/Data/Builtins.hs | 13 + .../Concrete/Data/InfoTableBuilder.hs | 18 +- .../Concrete/Data/NameSignature/Builder.hs | 6 +- src/Juvix/Compiler/Concrete/Extra.hs | 11 +- src/Juvix/Compiler/Concrete/Keywords.hs | 2 + src/Juvix/Compiler/Concrete/Language.hs | 1 + src/Juvix/Compiler/Concrete/Language/Base.hs | 70 ++- src/Juvix/Compiler/Concrete/Print/Base.hs | 6 + .../FromParsed/Analysis/Scoping.hs | 150 ++++-- .../FromParsed/Analysis/Scoping/Error.hs | 2 + .../Analysis/Scoping/Error/Types.hs | 35 ++ .../Concrete/Translation/FromSource.hs | 58 +- src/Juvix/Compiler/Core/Pretty/Base.hs | 9 +- .../Compiler/Core/Translation/FromInternal.hs | 1 + .../Core/Translation/Stripped/FromCore.hs | 7 +- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 3 +- src/Juvix/Compiler/Internal/Extra/Base.hs | 13 +- .../Internal/Extra/DependencyBuilder.hs | 3 +- src/Juvix/Compiler/Internal/Language.hs | 25 +- src/Juvix/Compiler/Internal/Pretty/Base.hs | 3 + .../Internal/Translation/FromConcrete.hs | 494 ++++++++++++++---- .../Analysis/ArityChecking/Error/Types.hs | 43 +- src/Juvix/Compiler/Pipeline/Package/Loader.hs | 7 +- .../Compiler/Store/Internal/Data/InfoTable.hs | 4 + src/Juvix/Data/Effect/Fail.hs | 17 +- src/Juvix/Data/Keyword/All.hs | 3 + src/Juvix/Extra/Strings.hs | 9 + src/Juvix/Prelude.hs | 2 - src/Juvix/Prelude/Base/Foundation.hs | 24 + src/Juvix/Prelude/Effects/StreamOf.hs | 1 - src/Juvix/Prelude/Stream.hs | 31 +- test/Compilation/Positive.hs | 7 +- test/Scope/Negative.hs | 7 +- tests/Compilation/positive/out/test085.out | 7 + tests/Compilation/positive/test085.juvix | 32 ++ tests/negative/WrongDeriving.juvix | 5 + 41 files changed, 905 insertions(+), 281 deletions(-) create mode 100644 src/Juvix/Compiler/Builtins/Eq.hs create mode 100644 tests/Compilation/positive/out/test085.out create mode 100644 tests/Compilation/positive/test085.juvix create mode 100644 tests/negative/WrongDeriving.juvix diff --git a/juvix-stdlib b/juvix-stdlib index 0080b1183a..f0a1e1ed77 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 0080b1183ab55e5180e69bfc3987e4cd6edbc230 +Subproject commit f0a1e1ed77e9e94467434b85736839e110d021d5 diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs index c34c6c676d..4305f162e8 100644 --- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs @@ -423,6 +423,7 @@ goStatement = \case StatementInductive t -> goInductive t StatementOpenModule t -> goOpen t StatementFunctionDef t -> goFunctionDef t + StatementDeriving t -> goDeriving t StatementSyntax syn -> goSyntax syn StatementImport t -> goImport t StatementModule m -> goLocalModule m @@ -537,13 +538,15 @@ goAxiom axiom = do axiomHeader :: Sem r Html axiomHeader = ppCodeHtml defaultOptions (set axiomDoc Nothing axiom) +goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html +goDeriving def = do + sig <- ppHelper (ppCode def) + defHeader (def ^. derivingFunLhs . funLhsName) sig Nothing + goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html goFunctionDef def = do - sig' <- funSig - defHeader (def ^. signName) sig' (def ^. signDoc) - where - funSig :: Sem r Html - funSig = ppHelper (ppCode (functionDefLhs def)) + sig <- ppHelper (ppCode (functionDefLhs def)) + defHeader (def ^. signName) sig (def ^. signDoc) goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html goInductive def = do diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs index f4c849fc3b..ac53b3c3b5 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs @@ -213,12 +213,13 @@ indModuleFilter :: forall s. [Concrete.Statement s] -> [Concrete.Statement s] indModuleFilter = filter ( \case - Concrete.StatementSyntax _ -> True - Concrete.StatementFunctionDef _ -> True - Concrete.StatementImport _ -> True - Concrete.StatementInductive _ -> True Concrete.StatementModule o -> o ^. Concrete.moduleOrigin == LocalModuleSource - Concrete.StatementOpenModule _ -> True - Concrete.StatementAxiom _ -> True - Concrete.StatementProjectionDef _ -> True + Concrete.StatementSyntax {} -> True + Concrete.StatementFunctionDef {} -> True + Concrete.StatementDeriving {} -> True + Concrete.StatementImport {} -> True + Concrete.StatementInductive {} -> True + Concrete.StatementOpenModule {} -> True + Concrete.StatementAxiom {} -> True + Concrete.StatementProjectionDef {} -> True ) diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index d47c5a6e0f..dda105ea62 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/src/Juvix/Compiler/Builtins.hs @@ -1,6 +1,7 @@ module Juvix.Compiler.Builtins ( module Juvix.Compiler.Builtins.Nat, module Juvix.Compiler.Builtins.IO, + module Juvix.Compiler.Builtins.Eq, module Juvix.Compiler.Builtins.Int, module Juvix.Compiler.Builtins.Bool, module Juvix.Compiler.Builtins.List, @@ -24,6 +25,7 @@ import Juvix.Compiler.Builtins.ByteArray import Juvix.Compiler.Builtins.Cairo import Juvix.Compiler.Builtins.Control import Juvix.Compiler.Builtins.Debug +import Juvix.Compiler.Builtins.Eq import Juvix.Compiler.Builtins.Field import Juvix.Compiler.Builtins.IO import Juvix.Compiler.Builtins.Int diff --git a/src/Juvix/Compiler/Builtins/Eq.hs b/src/Juvix/Compiler/Builtins/Eq.hs new file mode 100644 index 0000000000..599cb8bdbe --- /dev/null +++ b/src/Juvix/Compiler/Builtins/Eq.hs @@ -0,0 +1,25 @@ +module Juvix.Compiler.Builtins.Eq where + +import Juvix.Compiler.Internal.Builtins +import Juvix.Compiler.Internal.Extra +import Juvix.Prelude +import Juvix.Prelude.Pretty + +checkEqDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () +checkEqDef d = do + let err :: forall a. Text -> Sem r a + err = builtinsErrorText (getLoc d) + let eqTxt = prettyText BuiltinEq + unless (isSmallUniverse' (d ^. inductiveType)) (err (eqTxt <> " should be in the small universe")) + case d ^. inductiveParameters of + [_] -> return () + _ -> err (eqTxt <> " should have exactly one type parameter") + case d ^. inductiveConstructors of + [c1] -> checkMkEq c1 + _ -> err (eqTxt <> " should have exactly two constructors") + +checkMkEq :: ConstructorDef -> Sem r () +checkMkEq _ = return () + +checkIsEq :: FunctionDef -> Sem r () +checkIsEq _ = return () diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 30deb1eb41..64ab634fd3 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -59,6 +59,7 @@ builtinConstructors = \case BuiltinEcPoint -> [BuiltinMkEcPoint] BuiltinAnomaResource -> [BuiltinMkAnomaResource] BuiltinAnomaAction -> [BuiltinMkAnomaAction] + BuiltinEq -> [BuiltinMkEq] data BuiltinInductive = BuiltinNat @@ -67,6 +68,7 @@ data BuiltinInductive | BuiltinList | BuiltinMaybe | BuiltinPair + | BuiltinEq | BuiltinPoseidonState | BuiltinEcPoint | BuiltinAnomaResource @@ -87,6 +89,7 @@ instance Pretty BuiltinInductive where BuiltinList -> Str.list BuiltinMaybe -> Str.maybe_ BuiltinPair -> Str.pair + BuiltinEq -> Str.eq BuiltinPoseidonState -> Str.cairoPoseidonState BuiltinEcPoint -> Str.cairoEcPoint BuiltinAnomaResource -> Str.anomaResource @@ -109,6 +112,7 @@ instance Pretty BuiltinConstructor where BuiltinMkEcPoint -> Str.cairoMkEcPoint BuiltinMkAnomaResource -> Str.anomaMkResource BuiltinMkAnomaAction -> Str.anomaMkAction + BuiltinMkEq -> Str.mkEq data BuiltinConstructor = BuiltinNatZero @@ -119,6 +123,7 @@ data BuiltinConstructor | BuiltinIntNegSuc | BuiltinListNil | BuiltinListCons + | BuiltinMkEq | BuiltinMaybeNothing | BuiltinMaybeJust | BuiltinPairConstr @@ -161,6 +166,7 @@ data BuiltinFunction | BuiltinIntLe | BuiltinIntLt | BuiltinFromNat + | BuiltinIsEqual | BuiltinFromInt | BuiltinSeq | BuiltinMonadBind @@ -202,6 +208,7 @@ instance Pretty BuiltinFunction where BuiltinFromNat -> Str.fromNat BuiltinFromInt -> Str.fromInt BuiltinSeq -> Str.builtinSeq + BuiltinIsEqual -> Str.isEqual BuiltinMonadBind -> Str.builtinMonadBind data BuiltinAxiom @@ -434,6 +441,7 @@ isNatBuiltin = \case BuiltinNatLt -> True BuiltinNatEq -> True -- + BuiltinIsEqual -> False BuiltinAssert -> False BuiltinBoolIf -> False BuiltinBoolOr -> False @@ -486,6 +494,7 @@ isIntBuiltin = \case BuiltinFromNat -> False BuiltinFromInt -> False BuiltinSeq -> False + BuiltinIsEqual -> False BuiltinMonadBind -> False isCastBuiltin :: BuiltinFunction -> Bool @@ -493,6 +502,7 @@ isCastBuiltin = \case BuiltinFromNat -> True BuiltinFromInt -> True -- + BuiltinIsEqual -> False BuiltinAssert -> False BuiltinIntEq -> False BuiltinIntPlus -> False @@ -532,6 +542,7 @@ isIgnoredBuiltin f .&&. (not . isIntBuiltin) .&&. (not . isCastBuiltin) .&&. (/= BuiltinMonadBind) + .&&. (/= BuiltinIsEqual) $ f explicit :: Bool @@ -562,6 +573,8 @@ isIgnoredBuiltin f BuiltinNatLe -> False BuiltinNatLt -> False BuiltinNatEq -> False + -- Eq + BuiltinIsEqual -> False -- Monad BuiltinMonadBind -> False -- Ignored diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index 288cf107b7..5dc91201aa 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -28,7 +28,7 @@ data InfoTableBuilder :: Effect where RegisterRecordInfo :: S.NameId -> RecordInfo -> InfoTableBuilder m () RegisterAlias :: S.NameId -> PreSymbolEntry -> InfoTableBuilder m () RegisterLocalModule :: ScopedModule -> InfoTableBuilder m () - GetInfoTable :: InfoTableBuilder m InfoTable + GetBuilderInfoTable :: InfoTableBuilder m InfoTable GetBuiltinSymbol' :: Interval -> BuiltinPrim -> InfoTableBuilder m S.Symbol RegisterBuiltin' :: BuiltinPrim -> S.Symbol -> InfoTableBuilder m () @@ -92,7 +92,7 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case modify (over infoScoperAlias (HashMap.insert uid a)) RegisterLocalModule m -> mapM_ (uncurry registerBuiltinHelper) (m ^. scopedModuleInfoTable . infoBuiltins . to HashMap.toList) - GetInfoTable -> + GetBuilderInfoTable -> get GetBuiltinSymbol' i b -> do tbl <- get @InfoTable @@ -154,15 +154,19 @@ anameFromScopedIden s = } lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a -lookupInfo f = do - tab1 <- ask - fromMaybe (fromJust (f tab1)) . f <$> getInfoTable +lookupInfo f = fromJust <$> lookupInfo' f + +lookupInfo' :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r (Maybe a) +lookupInfo' f = do + tab1 <- getBuilderInfoTable + tab2 <- ask + return (f tab1 <|> f tab2) lookupFixity :: (Members '[InfoTableBuilder, Reader InfoTable] r) => S.NameId -> Sem r FixityDef -lookupFixity uid = lookupInfo (HashMap.lookup uid . (^. infoFixities)) +lookupFixity uid = lookupInfo (^. infoFixities . at uid) getPrecedenceGraph :: (Members '[InfoTableBuilder, Reader InfoTable] r) => Sem r PrecedenceGraph getPrecedenceGraph = do tab <- ask - tab' <- getInfoTable + tab' <- getBuilderInfoTable return $ combinePrecedenceGraphs (tab ^. infoPrecedenceGraph) (tab' ^. infoPrecedenceGraph) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 82b60b9737..ace4a4ec24 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -15,6 +15,7 @@ where import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Gen qualified as Gen +import Juvix.Compiler.Concrete.Language.Base import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Prelude @@ -63,8 +64,11 @@ instance (SingI s) => HasNameSignature s (AxiomDef s) where addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r () addArgs a = addArgs (a ^. axiomTypeSig) +instance (SingI s) => HasNameSignature s (FunctionLhs s) where + addArgs FunctionLhs {..} = addArgs _funLhsTypeSig + instance (SingI s) => HasNameSignature s (FunctionDef s) where - addArgs a = addArgs (a ^. signTypeSig) + addArgs = addArgs . functionDefLhs instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where addArgs :: diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 6745e8d43b..cf8dcdcbb4 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -9,6 +9,7 @@ module Juvix.Compiler.Concrete.Extra getPatternAtomIden, isBodyExpression, isFunctionLike, + isLhsFunctionLike, symbolParsed, ) where @@ -46,6 +47,7 @@ groupStatements = \case -- blank line g :: Statement s -> Statement s -> Bool g a b = case (a, b) of + (StatementDeriving _, _) -> False (StatementSyntax _, StatementSyntax _) -> True (StatementSyntax (SyntaxFixity _), _) -> False (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s @@ -108,6 +110,9 @@ isBodyExpression = \case SigBodyExpression {} -> True SigBodyClauses {} -> False -isFunctionLike :: FunctionDef a -> Bool -isFunctionLike = \case - FunctionDef {..} -> not (null (_signTypeSig ^. typeSigArgs)) || not (isBodyExpression _signBody) +isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool +isLhsFunctionLike FunctionLhs {..} = notNull (_funLhsTypeSig ^. typeSigArgs) + +isFunctionLike :: FunctionDef 'Parsed -> Bool +isFunctionLike d@FunctionDef {..} = + isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index 5eab9722a8..13bbc43089 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -36,6 +36,7 @@ import Juvix.Data.Keyword.All kwCase, kwCoercion, kwColon, + kwDeriving, kwDo, kwElse, kwEnd, @@ -85,6 +86,7 @@ reservedKeywords :: [Keyword] reservedKeywords = [ delimSemicolon, kwAssign, + kwDeriving, kwAt, kwAtQuestion, kwAxiom, diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 01af93aac0..6b332ab8b8 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -31,6 +31,7 @@ statementLabel = \case StatementOpenModule {} -> Nothing StatementProjectionDef {} -> Nothing StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel) + StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel) StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel) StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel) StatementModule i -> Just (i ^. modulePath . to modulePathTypeLabel) diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 5bf5224963..6fbe2cc3b5 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -271,6 +271,7 @@ data NonDefinitionsSection (s :: Stage) = NonDefinitionsSection data Definition (s :: Stage) = DefinitionSyntax (SyntaxDef s) | DefinitionFunctionDef (FunctionDef s) + | DefinitionDeriving (Deriving s) | DefinitionInductive (InductiveDef s) | DefinitionAxiom (AxiomDef s) | DefinitionProjectionDef (ProjectionDef s) @@ -287,6 +288,7 @@ newtype Statements (s :: Stage) = Statements data Statement (s :: Stage) = StatementSyntax (SyntaxDef s) | StatementFunctionDef (FunctionDef s) + | StatementDeriving (Deriving s) | StatementImport (Import s) | StatementInductive (InductiveDef s) | StatementModule (Module s 'ModuleLocal) @@ -672,6 +674,33 @@ deriving stock instance Ord (FunctionDefBody 'Parsed) deriving stock instance Ord (FunctionDefBody 'Scoped) +data Deriving (s :: Stage) = Deriving + { _derivingPragmas :: Maybe ParsedPragmas, + _derivingKw :: KeywordRef, + _derivingFunLhs :: FunctionLhs s + } + deriving stock (Generic) + +instance Serialize (Deriving 'Scoped) + +instance NFData (Deriving 'Scoped) + +instance Serialize (Deriving 'Parsed) + +instance NFData (Deriving 'Parsed) + +deriving stock instance Show (Deriving 'Parsed) + +deriving stock instance Show (Deriving 'Scoped) + +deriving stock instance Eq (Deriving 'Parsed) + +deriving stock instance Eq (Deriving 'Scoped) + +deriving stock instance Ord (Deriving 'Parsed) + +deriving stock instance Ord (Deriving 'Scoped) + data FunctionDef (s :: Stage) = FunctionDef { _signName :: FunctionName s, _signTypeSig :: TypeSig s, @@ -859,7 +888,7 @@ deriving stock instance Ord (RhsRecord 'Parsed) deriving stock instance Ord (RhsRecord 'Scoped) -data RhsGadt (s :: Stage) = RhsGadt +newtype RhsGadt (s :: Stage) = RhsGadt { _rhsGadtTypeSig :: TypeSig s } deriving stock (Generic) @@ -2834,6 +2863,27 @@ data FunctionLhs (s :: Stage) = FunctionLhs _funLhsName :: FunctionName s, _funLhsTypeSig :: TypeSig s } + deriving stock (Generic) + +instance Serialize (FunctionLhs 'Scoped) + +instance NFData (FunctionLhs 'Scoped) + +instance Serialize (FunctionLhs 'Parsed) + +instance NFData (FunctionLhs 'Parsed) + +deriving stock instance Show (FunctionLhs 'Parsed) + +deriving stock instance Show (FunctionLhs 'Scoped) + +deriving stock instance Eq (FunctionLhs 'Parsed) + +deriving stock instance Eq (FunctionLhs 'Scoped) + +deriving stock instance Ord (FunctionLhs 'Parsed) + +deriving stock instance Ord (FunctionLhs 'Scoped) makeLenses ''SideIfs makeLenses ''TypeSig @@ -2922,6 +2972,8 @@ makeLenses ''NameBlock makeLenses ''NameItem makeLenses ''RecordInfo makeLenses ''MarkdownInfo +makeLenses ''Deriving + makePrisms ''NamedArgumentNew functionDefLhs :: FunctionDef s -> FunctionLhs s @@ -3094,10 +3146,16 @@ instance HasLoc (OpenModule s short) where instance HasLoc (ProjectionDef s) where getLoc = getLoc . (^. projectionConstructor) +instance (SingI s) => HasLoc (Deriving s) where + getLoc Deriving {..} = + getLoc _derivingKw + <> getLoc _derivingFunLhs + instance HasLoc (Statement 'Scoped) where getLoc :: Statement 'Scoped -> Interval getLoc = \case StatementSyntax t -> getLoc t + StatementDeriving t -> getLoc t StatementFunctionDef t -> getLoc t StatementImport t -> getLoc t StatementInductive t -> getLoc t @@ -3324,6 +3382,14 @@ instance (SingI s) => HasLoc (FunctionDefBody s) where SigBodyExpression e -> getLocExpressionType e SigBodyClauses cl -> getLocSpan cl +instance (SingI s) => HasLoc (FunctionLhs s) where + getLoc FunctionLhs {..} = + (getLoc <$> _funLhsBuiltin) + ?<> (getLoc <$> _funLhsTerminating) + ?<> ( getLocSymbolType _funLhsName + <>? (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType) + ) + instance (SingI s) => HasLoc (FunctionDef s) where getLoc FunctionDef {..} = (getLoc <$> _signDoc) @@ -3331,7 +3397,7 @@ instance (SingI s) => HasLoc (FunctionDef s) where ?<> (getLoc <$> _signBuiltin) ?<> (getLoc <$> _signTerminating) ?<> getLocSymbolType _signName - <> getLoc _signBody + <> (getLoc _signBody) instance HasLoc (Example s) where getLoc e = e ^. exampleLoc diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index fa30dbc2a8..37a5880eee 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -1142,6 +1142,11 @@ instance (SingI s) => PrettyPrint (SigArg s) where defaultVal = ppCode <$> _sigArgDefault ppCode l <> arg <+?> defaultVal <> ppCode r +instance (SingI s) => PrettyPrint (Deriving s) where + ppCode Deriving {..} = + ppCode _derivingKw + <+> ppCode _derivingFunLhs + instance (SingI s) => PrettyPrint (TypeSig s) where ppCode TypeSig {..} = do let margs' = fmap ppCode <$> nonEmpty _typeSigArgs @@ -1536,6 +1541,7 @@ instance (SingI s) => PrettyPrint (Statement s) where ppCode = \case StatementSyntax s -> ppCode s StatementFunctionDef f -> ppCode f + StatementDeriving f -> ppCode f StatementImport i -> ppCode i StatementInductive i -> ppCode i StatementModule m -> ppCode m diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 993a5ec04a..d58f772b71 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -353,7 +353,7 @@ getReservedDefinitionSymbol :: getReservedDefinitionSymbol s = do m <- gets (^. scopeLocalSymbols) let s' = fromMaybe err (m ^. at s) - err = error ("impossible. Contents of scope:\n" <> ppTrace (toList m)) + err = impossibleError ("Symbol " <> ppTrace s <> " not found in the scope. Contents of scope:\n" <> ppTrace (toList m)) return s' ignoreSyntax :: Sem (State ScoperSyntax ': r) a -> Sem r a @@ -404,10 +404,10 @@ reserveConstructorSymbol d c b = do reserveFunctionSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => - FunctionDef 'Parsed -> + FunctionLhs 'Parsed -> Sem r S.Symbol reserveFunctionSymbol f = - reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. signBuiltin) (f ^. signName) + reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (f ^. funLhsName) reserveAxiomSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => @@ -419,37 +419,22 @@ reserveAxiomSymbol a = kindPretty :: NameKind kindPretty = maybe KNameAxiom getNameKind (a ^? axiomBuiltin . _Just . withLocParam) +reserveDerivingSymbol :: + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => + Deriving 'Parsed -> + Sem r () +reserveDerivingSymbol f = do + let lhs = f ^. derivingFunLhs + when (P.isLhsFunctionLike lhs) $ + void (reserveFunctionSymbol lhs) + reserveFunctionLikeSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => FunctionDef 'Parsed -> Sem r () reserveFunctionLikeSymbol f = when (P.isFunctionLike f) $ - void (reserveFunctionSymbol f) - -bindFunctionSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) => - Symbol -> - Sem r S.Symbol -bindFunctionSymbol = getReservedDefinitionSymbol - -bindInductiveSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) => - Symbol -> - Sem r S.Symbol -bindInductiveSymbol = getReservedDefinitionSymbol - -bindAxiomSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) => - Symbol -> - Sem r S.Symbol -bindAxiomSymbol = getReservedDefinitionSymbol - -bindConstructorSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) => - Symbol -> - Sem r S.Symbol -bindConstructorSymbol = getReservedDefinitionSymbol + void (reserveFunctionSymbol (functionDefLhs f)) bindFixitySymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) => @@ -726,7 +711,11 @@ lookupQualifiedSymbol :: ([Symbol], Symbol) -> Sem r (HashSet PreSymbolEntry, HashSet ModuleSymbolEntry, HashSet FixitySymbolEntry) lookupQualifiedSymbol sms = do - (es, (ms, fs)) <- runOutputHashSet . runOutputHashSet . execOutputHashSet $ go sms + (es, (ms, fs)) <- + runOutputHashSet + . runOutputHashSet + . execOutputHashSet + $ go sms return (es, ms, fs) where go :: @@ -1063,25 +1052,58 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do (@$>) :: (Functor m) => (a -> m ()) -> a -> m a (@$>) f a = f a $> a +checkDeriving :: + ( Members + '[ State Scope, + Error ScoperError, + State ScoperState, + Reader ScopeParameters, + Reader InfoTable, + Reader PackageId, + HighlightBuilder, + InfoTableBuilder, + NameIdGen, + State ScoperSyntax, + Reader BindingStrategy + ] + r + ) => + Deriving 'Parsed -> + Sem r (Deriving 'Scoped) +checkDeriving Deriving {..} = do + let lhs@FunctionLhs {..} = _derivingFunLhs + typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig) + name' <- + if + | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName + | otherwise -> reserveFunctionSymbol lhs + let lhs' = + FunctionLhs + { _funLhsName = name', + _funLhsTypeSig = typeSig', + .. + } + return + Deriving + { _derivingFunLhs = lhs', + _derivingKw, + _derivingPragmas + } + checkTypeSig :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => TypeSig 'Parsed -> Sem r (TypeSig 'Scoped) checkTypeSig TypeSig {..} = do - a' <- mapM checkArg _typeSigArgs + a' <- mapM checkSigArg _typeSigArgs t' <- mapM checkParseExpressionAtoms _typeSigRetType return TypeSig {_typeSigArgs = a', _typeSigRetType = t', ..} where - checkSigArgNames :: SigArgNames 'Parsed -> Sem r (SigArgNames 'Scoped) - checkSigArgNames = \case - SigArgNamesInstance -> return SigArgNamesInstance - SigArgNames ns -> fmap SigArgNames . forM ns $ \case - ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s - ArgumentWildcard w -> return (ArgumentWildcard w) - - checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped) - checkArg arg@SigArg {..} = do + checkSigArg :: + SigArg 'Parsed -> + Sem r (SigArg 'Scoped) + checkSigArg arg@SigArg {..} = do names' <- checkSigArgNames _sigArgNames ty' <- mapM checkParseExpressionAtoms _sigArgType default' <- case _sigArgDefault of @@ -1102,6 +1124,13 @@ checkTypeSig TypeSig {..} = do .. } + checkSigArgNames :: SigArgNames 'Parsed -> Sem r (SigArgNames 'Scoped) + checkSigArgNames = \case + SigArgNamesInstance -> return SigArgNamesInstance + SigArgNames ns -> fmap SigArgNames . forM ns $ \case + ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s + ArgumentWildcard w -> return (ArgumentWildcard w) + checkFunctionDef :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => @@ -1115,8 +1144,8 @@ checkFunctionDef fdef@FunctionDef {..} = do return (a', b') sigName' <- if - | P.isFunctionLike fdef -> bindFunctionSymbol _signName - | otherwise -> reserveFunctionSymbol fdef + | P.isFunctionLike fdef -> getReservedDefinitionSymbol _signName + | otherwise -> reserveFunctionSymbol (functionDefLhs fdef) let def = FunctionDef { _signName = sigName', @@ -1165,13 +1194,27 @@ checkInductiveParameters params = do checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => + ( Members + '[ HighlightBuilder, + Reader ScopeParameters, + Error ScoperError, + State Scope, + State ScoperState, + InfoTableBuilder, + Reader InfoTable, + NameIdGen, + Reader PackageId, + State ScoperSyntax, + Reader BindingStrategy + ] + r + ) => InductiveDef 'Parsed -> Sem r (InductiveDef 'Scoped) checkInductiveDef InductiveDef {..} = do (inductiveName', constructorNames' :: NonEmpty S.Symbol) <- topBindings $ do - i <- bindInductiveSymbol _inductiveName - cs <- mapM (bindConstructorSymbol . (^. constructorName)) _inductiveConstructors + i <- getReservedDefinitionSymbol _inductiveName + cs <- mapM (getReservedDefinitionSymbol . (^. constructorName)) _inductiveConstructors return (i, cs) (inductiveParameters', inductiveType', inductiveTypeApplied', inductiveDoc', inductiveConstructors') <- withLocalScope $ do inductiveParameters' <- mapM checkInductiveParameters _inductiveParameters @@ -1470,6 +1513,7 @@ checkModuleBody body = do toStatement :: Definition s -> Statement s toStatement = \case DefinitionSyntax d -> StatementSyntax d + DefinitionDeriving d -> StatementDeriving d DefinitionAxiom d -> StatementAxiom d DefinitionFunctionDef d -> StatementFunctionDef d DefinitionInductive d -> StatementInductive d @@ -1605,6 +1649,7 @@ checkSections sec = topBindings helper reserveDefinition = \case DefinitionSyntax s -> resolveSyntaxDef s $> Nothing DefinitionFunctionDef d -> reserveFunctionLikeSymbol d >> return Nothing + DefinitionDeriving d -> reserveDerivingSymbol d >> return Nothing DefinitionAxiom d -> reserveAxiomSymbol d >> return Nothing DefinitionProjectionDef d -> reserveProjectionSymbol d >> return Nothing DefinitionInductive d -> Just <$> reserveInductive d @@ -1660,6 +1705,7 @@ checkSections sec = topBindings helper goDefinition = \case DefinitionSyntax s -> DefinitionSyntax <$> checkSyntaxDef s DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d + DefinitionDeriving d -> DefinitionDeriving <$> checkDeriving d DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d DefinitionProjectionDef d -> DefinitionProjectionDef <$> checkProjectionDef d @@ -1800,6 +1846,7 @@ mkSections = \case fromStatement = \case StatementAxiom a -> Left (DefinitionAxiom a) StatementFunctionDef n -> Left (DefinitionFunctionDef n) + StatementDeriving n -> Left (DefinitionDeriving n) StatementInductive i -> Left (DefinitionInductive i) StatementSyntax s -> Left (DefinitionSyntax s) StatementProjectionDef s -> Left (DefinitionProjectionDef s) @@ -1834,9 +1881,9 @@ checkLocalModule :: Sem r (Module 'Scoped 'ModuleLocal) checkLocalModule md@Module {..} = do tab1 <- ask @InfoTable - tab2 <- getInfoTable + tab2 <- getBuilderInfoTable (tab, (moduleExportInfo, moduleBody', moduleDoc')) <- - withLocalScope $ runReader (tab1 <> tab2) $ runInfoTableBuilder mempty $ do + withLocalScope . runReader (tab1 <> tab2) . runInfoTableBuilder mempty $ do inheritScope (e, b) <- checkModuleBody _moduleBody doc' <- mapM checkJudoc _moduleDoc @@ -2122,10 +2169,16 @@ checkAxiomDef :: AxiomDef 'Parsed -> Sem r (AxiomDef 'Scoped) checkAxiomDef AxiomDef {..} = do - axiomName' <- bindAxiomSymbol _axiomName + axiomName' <- getReservedDefinitionSymbol _axiomName axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc) axiomSig' <- withLocalScope (checkTypeSig _axiomTypeSig) - let a = AxiomDef {_axiomName = axiomName', _axiomTypeSig = axiomSig', _axiomDoc = axiomDoc', ..} + let a = + AxiomDef + { _axiomName = axiomName', + _axiomTypeSig = axiomSig', + _axiomDoc = axiomDoc', + .. + } registerNameSignature (a ^. axiomName . S.nameId) a registerAxiom @$> a @@ -2185,6 +2238,7 @@ checkLetStatements = DefinitionFunctionDef d -> LetFunctionDef d DefinitionSyntax syn -> fromSyn syn DefinitionInductive {} -> impossible + DefinitionDeriving {} -> impossible DefinitionProjectionDef {} -> impossible DefinitionAxiom {} -> impossible diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 850e219461..c6ad481c77 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -61,6 +61,7 @@ data ScoperError | ErrBuiltinErrorMessage BuiltinErrorMessage | ErrDoLastStatement DoLastStatement | ErrDoBindImplicitPattern DoBindImplicitPattern + | ErrDerivingTypeWrongForm DerivingTypeWrongForm deriving stock (Generic) instance ToGenericError ScoperError where @@ -113,6 +114,7 @@ instance ToGenericError ScoperError where ErrBuiltinErrorMessage e -> genericError e ErrDoLastStatement e -> genericError e ErrDoBindImplicitPattern e -> genericError e + ErrDerivingTypeWrongForm e -> genericError e builtinsErrorMsg :: (Members '[Error ScoperError] r) => Interval -> AnsiText -> Sem r a builtinsErrorMsg loc msg = diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index 67751b95b7..fcf0b17bf4 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -14,6 +14,8 @@ import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Options (Options, fromGenericOptions) import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty import Juvix.Compiler.Concrete.Translation.ImportScanner.Base +import Juvix.Compiler.Internal.Language qualified as I +import Juvix.Compiler.Internal.Pretty qualified as I import Juvix.Compiler.Store.Scoped.Language (FixitySymbolEntry, ModuleSymbolEntry, PreSymbolEntry) import Juvix.Data.CodeAnn import Juvix.Data.PPOutput @@ -1158,3 +1160,36 @@ instance ToGenericError BuiltinErrorMessage where where i :: Interval i = _builtinErrorMessageLoc + +data DerivingTypeWrongForm = DerivingTypeWrongForm + { _derivingTypeWrongForm :: I.Expression, + _derivingTypeBuiltin :: I.DerivingTrait, + _derivingTypeSupportedBuiltins :: [I.Name] + } + +instance ToGenericError DerivingTypeWrongForm where + genericError :: (Member (Reader GenericOptions) r) => DerivingTypeWrongForm -> Sem r GenericError + genericError DerivingTypeWrongForm {..} = do + opts <- I.fromGenericOptions <$> ask + let ss = I.doc opts _derivingTypeWrongForm + msg = + "The return type of the deriving statement has the wrong form:" + <> line + <> ss + <> line + <> "It is expected to be of the form:" + <> line + <> ("" <+> parens " ") + <> line + <> "where is an inductive type and is one of:" + <> line + <> itemize (I.doc opts <$> _derivingTypeSupportedBuiltins) + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = getLoc _derivingTypeWrongForm diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index d65f1a352b..f823c79f47 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -399,10 +399,6 @@ replInput = <|> ReplOpen <$> openModule <|> ReplImport <$> import_ --------------------------------------------------------------------------------- --- Symbols and names --------------------------------------------------------------------------------- - symbol :: (Members '[ParserResultBuilder] r) => ParsecS r Symbol symbol = uncurry (flip WithLoc) <$> identifierL @@ -460,10 +456,6 @@ pusingList = do topModulePath :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r TopModulePath topModulePath = mkTopModulePath <$> dottedSymbol --------------------------------------------------------------------------------- --- Top level statement --------------------------------------------------------------------------------- - recoverStashes :: (Members '[PragmasStash, JudocStash] r) => ParsecS r a -> ParsecS r a recoverStashes r = do p <- P.lift (get @(Maybe ParsedPragmas)) @@ -474,6 +466,23 @@ recoverStashes r = do put j return res +derivingInstance :: + (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => + ParsecS r (Deriving 'Parsed) +derivingInstance = do + _derivingKw <- kw kwDeriving + _derivingPragmas <- getPragmas + let opts = + FunctionSyntaxOptions + { _funAllowOmitType = False, + _funAllowInstance = True + } + off <- P.getOffset + _derivingFunLhs <- functionDefinitionLhs opts Nothing + unless (isJust (_derivingFunLhs ^. funLhsInstance)) $ + parseFailure off "Expected `deriving instance`" + return Deriving {..} + statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed) statement = P.label "" $ do optional_ stashJudoc @@ -486,6 +495,7 @@ statement = P.label "" $ do ms <- optional ( StatementImport <$> import_ + <|> StatementDeriving <$> derivingInstance <|> StatementOpenModule <$> openModule <|> StatementSyntax <$> syntaxDef <|> StatementInductive <$> inductiveDef Nothing @@ -681,10 +691,6 @@ builtinRecordField = do void (kw kwBuiltin) builtinFunction --------------------------------------------------------------------------------- --- Syntax declaration --------------------------------------------------------------------------------- - syntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (SyntaxDef 'Parsed) syntaxDef = do syn <- kw kwSyntax @@ -809,10 +815,6 @@ iteratorSyntaxDef _iterSyntaxKw = do _iterInfo <- optional parsedIteratorInfo return IteratorSyntaxDef {..} --------------------------------------------------------------------------------- --- Import statement --------------------------------------------------------------------------------- - import_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash, Error ParserError] r) => ParsecS r (Import 'Parsed) import_ = do _importKw <- kw kwImport @@ -1088,10 +1090,6 @@ parseList = do _listBracketR <- Irrelevant <$> kw delimBracketR return List {..} --------------------------------------------------------------------------------- --- Literals --------------------------------------------------------------------------------- - literalInteger :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r LiteralLoc literalInteger = fmap LitIntegerWithBase <$> integerWithBase @@ -1274,10 +1272,6 @@ multiwayIf = do _ifBranchElse <- ifBranch return If {..} --------------------------------------------------------------------------------- --- Universe expression --------------------------------------------------------------------------------- - universe :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r Universe universe = do i <- kw kwType @@ -1461,10 +1455,6 @@ axiomDef _axiomBuiltin = do _axiomTypeSig <- typeSig defaultSigOptions return AxiomDef {..} --------------------------------------------------------------------------------- --- Function expression --------------------------------------------------------------------------------- - implicitOpenField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (KeywordRef, IsImplicitField) @@ -1522,10 +1512,6 @@ function = do _funReturn <- parseExpressionAtoms return Function {..} --------------------------------------------------------------------------------- --- Lambda expression --------------------------------------------------------------------------------- - lambdaClause :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed) lambdaClause _lambdaPipe = do _lambdaParameters <- P.some patternAtom @@ -1542,10 +1528,6 @@ lambda = do let _lambdaBraces = Irrelevant (brl, brr) return Lambda {..} -------------------------------------------------------------------------------- --- Data type construction declaration -------------------------------------------------------------------------------- - inductiveDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Maybe (WithLoc BuiltinInductive) -> ParsecS r (InductiveDef 'Parsed) inductiveDef _inductiveBuiltin = do _inductivePositive <- optional (kw kwPositive) @@ -1785,10 +1767,6 @@ parsePatternAtomsNested = do (_patternAtoms, _patternAtomsLoc) <- second Irrelevant <$> interval (P.some patternAtomNested) return PatternAtoms {..} --------------------------------------------------------------------------------- --- Module declaration --------------------------------------------------------------------------------- - pmodulePath :: forall t r. (SingI t, Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ModulePathType 'Parsed t) pmodulePath = case sing :: SModuleIsTop t of SModuleTop -> topModulePath diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index d51c86f441..0bc1b6f237 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -647,16 +647,17 @@ instance PrettyCode InfoTable where shouldPrintInductive :: Maybe BuiltinType -> Bool shouldPrintInductive = \case Just (BuiltinTypeInductive i) -> case i of - BuiltinList -> False - BuiltinMaybe -> False BuiltinPair -> True BuiltinPoseidonState -> True BuiltinEcPoint -> True + BuiltinAnomaResource -> True + BuiltinAnomaAction -> True + BuiltinList -> False + BuiltinEq -> False + BuiltinMaybe -> False BuiltinNat -> False BuiltinInt -> False BuiltinBool -> False - BuiltinAnomaResource -> True - BuiltinAnomaAction -> True Just _ -> False Nothing -> True diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 5fccabbd1e..b85a36eb5b 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -217,6 +217,7 @@ goConstructor sym ctor = do ctorTag = \case Just Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue) Just Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse) + Just Internal.BuiltinMkEq -> freshTag Just Internal.BuiltinNatZero -> freshTag Just Internal.BuiltinNatSuc -> freshTag Just Internal.BuiltinIntOfNat -> freshTag diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 0d8936eb78..c90354ad68 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -54,6 +54,7 @@ fromCore fsize tab = BuiltinIntLe -> False BuiltinIntLt -> False BuiltinSeq -> False + BuiltinIsEqual -> False BuiltinMonadBind -> True -- TODO revise BuiltinFromNat -> True BuiltinFromInt -> True @@ -62,19 +63,20 @@ fromCore fsize tab = shouldKeepConstructor = \case BuiltinListNil -> True BuiltinListCons -> True + BuiltinMkEq -> True BuiltinMkPoseidonState -> True BuiltinMkEcPoint -> True BuiltinMaybeNothing -> True BuiltinMaybeJust -> True BuiltinPairConstr -> True + BuiltinMkAnomaResource -> True + BuiltinMkAnomaAction -> True BuiltinNatZero -> False BuiltinNatSuc -> False BuiltinBoolTrue -> False BuiltinBoolFalse -> False BuiltinIntOfNat -> False BuiltinIntNegSuc -> False - BuiltinMkAnomaResource -> True - BuiltinMkAnomaAction -> True shouldKeepType :: BuiltinType -> Bool shouldKeepType = \case @@ -141,6 +143,7 @@ fromCore fsize tab = BuiltinByteArrayLength -> False BuiltinTypeInductive i -> case i of BuiltinList -> True + BuiltinEq -> True BuiltinMaybe -> True BuiltinPair -> True BuiltinPoseidonState -> True diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index fe591a0227..e2c936e915 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -44,10 +44,11 @@ functionInfoFromFunctionDef isLocal FunctionDef {..} = } inductiveInfoFromInductiveDef :: InductiveDef -> InductiveInfo -inductiveInfoFromInductiveDef InductiveDef {..} = +inductiveInfoFromInductiveDef d@InductiveDef {..} = InductiveInfo { _inductiveInfoName = _inductiveName, _inductiveInfoType = _inductiveType, + _inductiveInfoLoc = getLoc d, _inductiveInfoBuiltin = _inductiveBuiltin, _inductiveInfoParameters = _inductiveParameters, _inductiveInfoConstructors = map (^. inductiveConstructorName) _inductiveConstructors, diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index cde2d3a091..8573a0916c 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -424,12 +424,15 @@ foldApplication f args = case nonEmpty args of unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg) unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l') --- TODO make it tail recursive unfoldExpressionApp :: Expression -> (Expression, [ApplicationArg]) -unfoldExpressionApp = \case - ExpressionApplication (Application l r i) -> - second (`snoc` ApplicationArg i r) (unfoldExpressionApp l) - e -> (e, []) +unfoldExpressionApp = swap . run . runAccumListReverse . go + where + go :: Expression -> Sem '[Accum ApplicationArg] Expression + go = \case + ExpressionApplication (Application l r i) -> do + accum (ApplicationArg i r) + go l + e -> return e unfoldApplication :: Application -> (Expression, NonEmpty Expression) unfoldApplication = fmap (fmap (^. appArg)) . unfoldApplication' diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs index 23c2e2bb99..cdd895b7c1 100644 --- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs +++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs @@ -178,7 +178,7 @@ goInductive p i = do mapM_ goInductiveParameter (i ^. inductiveParameters) goExpression (i ^. inductiveType) --- BuiltinBool and BuiltinNat are required by the Internal to Core translation +-- | BuiltinBool and BuiltinNat are required by the Internal to Core translation -- when translating literal integers to Nats. checkBuiltinInductiveStartNode :: forall r. (Members '[State StartNodes, State BuilderState] r) => InductiveDef -> Sem r () checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go @@ -199,6 +199,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go BuiltinEcPoint -> return () BuiltinAnomaResource -> return () BuiltinAnomaAction -> return () + BuiltinEq -> return () addInductiveStartNode :: Sem r () addInductiveStartNode = addStartNode (i ^. inductiveName) diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 4f080319b8..15be717869 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -12,6 +12,7 @@ where import Juvix.Compiler.Concrete.Data.Builtins import Juvix.Compiler.Internal.Data.Name +import Juvix.Data.CodeAnn import Juvix.Data.Hole import Juvix.Data.InstanceHole import Juvix.Data.IsImplicit @@ -31,6 +32,27 @@ type PreModuleBody = ModuleBody' PreStatement newtype PreLetStatement = PreLetFunctionDef FunctionDef +-- | Traits that support builtin deriving +data DerivingTrait = DerivingEq + deriving stock (Generic, Data, Bounded, Enum, Show) + +derivingTraitFromBuiltinMap :: HashMap BuiltinPrim DerivingTrait +derivingTraitFromBuiltinMap = hashMap [(toBuiltinPrim d, d) | d <- allElements] + +derivingTraitFromBuiltin :: (IsBuiltin builtin) => builtin -> Maybe DerivingTrait +derivingTraitFromBuiltin b = derivingTraitFromBuiltinMap ^. at (toBuiltinPrim b) + +instance IsBuiltin DerivingTrait where + toBuiltinPrim :: DerivingTrait -> BuiltinPrim + toBuiltinPrim = \case + DerivingEq -> toBuiltinPrim BuiltinEq + +instance Pretty DerivingTrait where + pretty = pretty . toBuiltinPrim + +instance PrettyCodeAnn DerivingTrait where + ppCodeAnn = annotateKind KNameInductive . pretty + data PreStatement = PreFunctionDef FunctionDef | PreInductiveDef InductiveDef @@ -484,6 +506,7 @@ data NormalizedExpression = NormalizedExpression } makePrisms ''Expression +makePrisms ''Iden makePrisms ''MutualStatement makeLenses ''SideIfBranch @@ -584,7 +607,7 @@ instance HasAtomicity Pattern where PatternWildcardConstructor {} -> Atom instance HasLoc Module where - getLoc m = getLoc (m ^. moduleName) <>? maybe Nothing (Just . getLocSpan) (nonEmpty (m ^. moduleBody . moduleStatements)) + getLoc m = getLoc (m ^. moduleName) <>? fmap getLocSpan (nonEmpty (m ^. moduleBody . moduleStatements)) instance HasLoc MutualBlock where getLoc = getLocSpan . (^. mutualStatements) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 490ae9305b..3628d8b89e 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -39,6 +39,9 @@ instance PrettyCode Name where showNameId <- asks (^. optShowNameIds) return (prettyName showNameId n) +instance PrettyCode DerivingTrait where + ppCode = return . ppCodeAnn + instance PrettyCode ArgInfo where ppCode ArgInfo {..} = do name <- maybe (return kwWildcard) ppCode _argInfoName diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 43e03192b1..a9bd8fc1aa 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -1,7 +1,6 @@ module Juvix.Compiler.Internal.Translation.FromConcrete ( module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context, fromConcrete, - ConstructorInfos, DefaultArgsStack, goTopModule, fromConcreteExpression, @@ -25,6 +24,7 @@ import Juvix.Compiler.Concrete.Print import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Internal.Builtins +import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal import Juvix.Compiler.Internal.Extra (mkLetClauses) import Juvix.Compiler.Internal.Extra qualified as Internal @@ -34,6 +34,7 @@ import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Pipeline.EntryPoint +import Juvix.Compiler.Store.Extra qualified as Store import Juvix.Compiler.Store.Language qualified as Store import Juvix.Compiler.Store.Scoped.Data.InfoTable qualified as S import Juvix.Compiler.Store.Scoped.Language (createExportsTable) @@ -41,13 +42,20 @@ import Juvix.Compiler.Store.Scoped.Language qualified as S import Juvix.Prelude import Safe (lastMay) --- | Needed only to generate field projections. -newtype ConstructorInfos = ConstructorInfos - { _constructorInfos :: HashMap Internal.ConstructorName ConstructorInfo +-- | Needed to generate field projections and deriving instances +data LocalTable = LocalTable + { _localInfoConstructors :: HashMap Internal.ConstructorName ConstructorInfo, + _localInfoInductives :: HashMap Internal.InductiveName InductiveInfo } - deriving newtype (Semigroup, Monoid) -makeLenses ''ConstructorInfos +emptyLocalTable :: LocalTable +emptyLocalTable = + LocalTable + { _localInfoConstructors = mempty, + _localInfoInductives = mempty + } + +makeLenses ''LocalTable -- | Needed to detect looping while inserting default arguments newtype DefaultArgsStack = DefaultArgsStack @@ -57,16 +65,25 @@ newtype DefaultArgsStack = DefaultArgsStack makeLenses ''DefaultArgsStack +data DerivingArgs = DerivingArgs + { _derivingPragmas :: Maybe ParsedPragmas, + _derivingInstanceName :: Internal.FunctionName, + _derivingParameters :: [Internal.FunctionParameter], + _derivingReturnType :: (Internal.InductiveName, [Internal.ApplicationArg]) + } + fromConcrete :: (Members '[Reader EntryPoint, Error JuvixError, Reader Store.ModuleTable, NameIdGen, Termination] r) => Scoper.ScoperResult -> Sem r InternalResult fromConcrete _resultScoper = do mtab <- ask - let ms = HashMap.elems (mtab ^. Store.moduleTable) + let it :: InternalModuleTable = Store.getInternalModuleTable mtab + ms :: [Store.ModuleInfo] = HashMap.elems (mtab ^. Store.moduleTable) exportTbl = _resultScoper ^. Scoper.resultExports <> mconcatMap (createExportsTable . (^. Store.moduleInfoScopedModule . S.scopedModuleExportInfo)) ms + internalTable :: Internal.InfoTable = computeCombinedInfoTable it tab :: S.InfoTable = S.getCombinedInfoTable (_resultScoper ^. Scoper.resultScopedModule) <> mconcatMap (S.getCombinedInfoTable . (^. Store.moduleInfoScopedModule)) ms @@ -74,8 +91,9 @@ fromConcrete _resultScoper = do runReader @Pragmas mempty . runReader @ExportsTable exportTbl . runReader tab + . runReader internalTable . mapError (JuvixError @ScoperError) - . evalState @ConstructorInfos mempty + . evalState emptyLocalTable . runReader @DefaultArgsStack mempty $ goTopModule m return InternalResult {..} @@ -150,13 +168,13 @@ buildMutualBlocks ss = do CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p) goLocalModule :: - (Members '[Reader EntryPoint, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, State LocalTable, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, Reader S.InfoTable] r) => Module 'Scoped 'ModuleLocal -> Sem r [Internal.PreStatement] goLocalModule = concatMapM goAxiomInductive . (^. moduleBody) goTopModule :: - (Members '[Reader DefaultArgsStack, Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Termination, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, NameIdGen, Reader Pragmas, Termination, Reader S.InfoTable, Reader Internal.InfoTable] r) => Module 'Scoped 'ModuleTop -> Sem r Internal.Module goTopModule m = do @@ -209,7 +227,7 @@ traverseM' f x = sequence <$> traverse f x toPreModule :: forall r. - (Members '[Reader EntryPoint, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, Reader S.InfoTable, Reader Internal.InfoTable] r) => Module 'Scoped 'ModuleTop -> Sem r Internal.PreModule toPreModule Module {..} = do @@ -269,15 +287,19 @@ fromPreModuleBody b = do goModuleBody :: forall r. - (Members '[Reader EntryPoint, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, Reader S.InfoTable, Reader Internal.InfoTable] r) => [Statement 'Scoped] -> Sem r Internal.PreModuleBody -goModuleBody stmts = do +goModuleBody stmts = evalState emptyLocalTable $ do _moduleImports <- mapM goImport (scanImports stmts) otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goAxiomInductive) ss - functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions - projections <- map (fmap Internal.PreFunctionDef) <$> mkProjections - let unsorted = otherThanFunctions <> functions <> projections + funs :: [Indexed Internal.PreStatement] <- + sequence + [ Indexed i . Internal.PreFunctionDef <$> d + | Indexed i s <- ss, + Just d <- [mkFunctionLike s] + ] + let unsorted = otherThanFunctions <> funs _moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx) unsorted) return Internal.ModuleBody {..} where @@ -287,21 +309,17 @@ goModuleBody stmts = do ss :: [Indexed (Statement 'Scoped)] ss = zipWith Indexed [0 ..] ss' - mkProjections :: Sem r [Indexed Internal.FunctionDef] - mkProjections = - sequence - [ Indexed i <$> funDef - | Indexed i (StatementProjectionDef f) <- ss, - let funDef = goProjectionDef f - ] - - compiledFunctions :: Sem r [Indexed Internal.FunctionDef] - compiledFunctions = - sequence - [ Indexed i <$> funDef - | Indexed i (StatementFunctionDef f) <- ss, - let funDef = goFunctionDef f - ] + mkFunctionLike :: Statement 'Scoped -> Maybe (Sem (State LocalTable ': r) (Internal.FunctionDef)) + mkFunctionLike s = case s of + StatementFunctionDef d -> Just (goFunctionDef d) + StatementProjectionDef d -> Just (goProjectionDef d) + StatementDeriving d -> Just (goDeriving d) + StatementSyntax {} -> Nothing + StatementImport {} -> Nothing + StatementInductive {} -> Nothing + StatementModule {} -> Nothing + StatementOpenModule {} -> Nothing + StatementAxiom {} -> Nothing scanImports :: [Statement 'Scoped] -> [Import 'Scoped] scanImports = mconcatMap go @@ -315,6 +333,7 @@ scanImports = mconcatMap go StatementAxiom {} -> [] StatementSyntax {} -> [] StatementFunctionDef {} -> [] + StatementDeriving {} -> [] StatementProjectionDef {} -> [] goImport :: @@ -331,7 +350,7 @@ goImport Import {..} = -- | Ignores functions goAxiomInductive :: forall r. - (Members '[Reader EntryPoint, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, State LocalTable, Error ScoperError, NameIdGen, Reader Pragmas, Reader S.InfoTable] r) => Statement 'Scoped -> Sem r [Internal.PreStatement] goAxiomInductive = \case @@ -340,18 +359,19 @@ goAxiomInductive = \case StatementModule f -> goLocalModule f StatementImport {} -> return [] StatementFunctionDef {} -> return [] + StatementDeriving {} -> return [] StatementSyntax {} -> return [] StatementOpenModule {} -> return [] StatementProjectionDef {} -> return [] goProjectionDef :: forall r. - (Members '[Reader DefaultArgsStack, Reader Pragmas, NameIdGen, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, State LocalTable, Reader Pragmas, NameIdGen, Error ScoperError, Reader S.InfoTable] r) => ProjectionDef 'Scoped -> Sem r Internal.FunctionDef goProjectionDef ProjectionDef {..} = do let c = goSymbol _projectionConstructor - info <- gets (^?! constructorInfos . at c . _Just) + info <- gets (^?! localInfoConstructors . at c . _Just) let field = goSymbol _projectionField msig <- asks (^. S.infoNameSigs . at (field ^. Internal.nameId)) argInfos <- maybe (return mempty) (fmap toList . goNameSignature) msig @@ -371,7 +391,11 @@ goProjectionDef ProjectionDef {..} = do whenJust (fun ^. Internal.funDefBuiltin) (checkBuiltinFunction fun) return fun -goNameSignature :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => NameSignature 'Scoped -> Sem r [Internal.ArgInfo] +goNameSignature :: + forall r. + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + NameSignature 'Scoped -> + Sem r [Internal.ArgInfo] goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs) where goBlock :: NameBlock 'Scoped -> Sem r (NonEmpty Internal.ArgInfo) @@ -386,12 +410,269 @@ goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs) _argInfoName = goSymbol <$> (i ^. nameItemSymbol) } +goDeriving :: + forall r. + (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, State LocalTable, Reader Internal.InfoTable, Reader S.InfoTable] r) => + Deriving 'Scoped -> + Sem r Internal.FunctionDef +goDeriving Deriving {..} = do + let FunctionLhs {..} = _derivingFunLhs + name = goSymbol _funLhsName + (funArgs, ret) <- Internal.unfoldFunType <$> goDefType _derivingFunLhs + let (mtrait, traitArgs) = Internal.unfoldExpressionApp ret + (n, der) <- findDerivingTrait mtrait + let deriveArgs = + DerivingArgs + { _derivingInstanceName = name, + _derivingReturnType = (n, traitArgs), + _derivingParameters = funArgs, + _derivingPragmas + } + deriveTrait der deriveArgs + +deriveTrait :: + ( Members + '[ Reader S.InfoTable, + Reader Pragmas, + Reader DefaultArgsStack, + Error ScoperError, + Reader Internal.InfoTable, + State LocalTable, + NameIdGen + ] + r + ) => + Internal.DerivingTrait -> + DerivingArgs -> + Sem r Internal.FunctionDef +deriveTrait = \case + Internal.DerivingEq -> deriveEq + +findDerivingTrait :: + forall r. + ( Members + '[ Error ScoperError, + Reader S.InfoTable + ] + r + ) => + Internal.Expression -> + Sem r (Internal.Name, Internal.DerivingTrait) +findDerivingTrait ret = do + i :: Internal.Name <- maybe err return (ret ^? Internal._ExpressionIden . Internal._IdenInductive) + tbl :: BuiltinsTable <- asks (^. S.infoBuiltins) + let matches :: Internal.DerivingTrait -> Bool + matches t = Just i == (goSymbol <$> tbl ^. at (toBuiltinPrim t)) + (i,) <$> maybe err return (find matches allElements) + where + err :: Sem r a + err = throwDerivingWrongForm ret + +goArgsInfo :: + ( Members + '[ Reader S.InfoTable, + NameIdGen, + Error ScoperError, + Reader DefaultArgsStack, + Reader Pragmas + ] + r + ) => + Internal.Name -> + Sem r [Internal.ArgInfo] +goArgsInfo name = do + msig <- asks (^. S.infoNameSigs . at (name ^. Internal.nameId)) + maybe (return mempty) (fmap toList . goNameSignature) msig + +getBuiltin :: + (IsBuiltin builtin, Members '[Reader S.InfoTable, Error ScoperError] r) => + Interval -> + builtin -> + Sem r Internal.Name +getBuiltin loc b = do + r <- fmap goSymbol <$> asks (^. S.infoBuiltins . at (toBuiltinPrim b)) + maybe (throw err) return r + where + err :: ScoperError + err = + ErrBuiltinNotDefined + BuiltinNotDefined + { _notDefinedLoc = loc, + _notDefinedBuiltin = toBuiltinPrim b + } + +getDefinedConstructor :: + (Members '[Reader Internal.InfoTable, State LocalTable] r) => + Internal.ConstructorName -> + Sem r ConstructorInfo +getDefinedConstructor ind = do + tbl1 <- gets (^. localInfoConstructors . at ind) + tbl2 <- asks (^. infoConstructors . at ind) + return (fromJust (tbl1 <|> tbl2)) + +getDefinedInductive :: + (Members '[Reader Internal.InfoTable, State LocalTable] r) => + Internal.InductiveName -> + Sem r InductiveInfo +getDefinedInductive ind = do + tbl1 <- gets (^. localInfoInductives . at ind) + tbl2 <- asks (^. infoInductives . at ind) + return (fromJust (tbl1 <|> tbl2)) + +throwDerivingWrongForm :: (Members '[Error ScoperError, Reader S.InfoTable] r) => Internal.Expression -> Sem r a +throwDerivingWrongForm ret = do + let getSym :: (BuiltinPrim, S.Symbol) -> Maybe Internal.Name + getSym (p, s) = do + guard (isJust (Internal.derivingTraitFromBuiltin p)) + return (goSymbol s) + _derivingTypeSupportedBuiltins <- + mapMaybe getSym . HashMap.toList + <$> asks (^. S.infoBuiltins) + throw $ + ErrDerivingTypeWrongForm + DerivingTypeWrongForm + { _derivingTypeWrongForm = ret, + _derivingTypeBuiltin = Internal.DerivingEq, + _derivingTypeSupportedBuiltins + } + +deriveEq :: + forall r. + ( Members + '[ Reader S.InfoTable, + Reader Internal.InfoTable, + State LocalTable, + NameIdGen, + Error ScoperError, + Reader DefaultArgsStack, + Reader Pragmas + ] + r + ) => + DerivingArgs -> + Sem r Internal.FunctionDef +deriveEq DerivingArgs {..} = do + arg <- getArg + argsInfo <- goArgsInfo _derivingInstanceName + lam <- eqLambda arg + mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq + let body = mkEq Internal.@@ lam + ty = Internal.foldFunType _derivingParameters ret + pragmas' <- goPragmas _derivingPragmas + return + Internal.FunctionDef + { _funDefTerminating = False, + _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, + _funDefPragmas = pragmas', + _funDefArgsInfo = argsInfo, + _funDefDocComment = Nothing, + _funDefName = _derivingInstanceName, + _funDefType = ty, + _funDefBody = body, + _funDefBuiltin = Nothing + } + where + ret :: Internal.Expression + ret = Internal.foldApplication (Internal.toExpression eqName) args + + eqName :: Internal.InductiveName + args :: [Internal.ApplicationArg] + (eqName, args) = _derivingReturnType + + getArg :: Sem r Internal.InductiveInfo + getArg = runFailDefaultM (throwDerivingWrongForm ret) $ do + [Internal.ApplicationArg Explicit a] <- return args + Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a)) + getDefinedInductive ind + + eqLambda :: Internal.InductiveInfo -> Sem r Internal.Expression + eqLambda d = do + let loc = getLoc eqName + band <- getBuiltin loc BuiltinBoolAnd + btrue <- getBuiltin loc BuiltinBoolTrue + bfalse <- getBuiltin loc BuiltinBoolFalse + bisEqual <- getBuiltin loc BuiltinIsEqual + case nonEmpty (d ^. Internal.inductiveInfoConstructors) of + Nothing -> return (Internal.toExpression btrue) + Just cs -> do + cl' <- mapM (lambdaClause band btrue bisEqual) cs + defaultCl' <- + if + | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bfalse + | otherwise -> return Nothing + return + ( Internal.ExpressionLambda + Internal.Lambda + { _lambdaType = Nothing, + _lambdaClauses = snocNonEmptyMaybe cl' defaultCl' + } + ) + where + defaultLambdaClause :: Internal.Name -> Sem r Internal.LambdaClause + defaultLambdaClause btrue = do + let loc = getLoc eqName + p1 <- Internal.genWildcard loc Internal.Explicit + p2 <- Internal.genWildcard loc Internal.Explicit + return + Internal.LambdaClause + { _lambdaPatterns = p1 :| [p2], + _lambdaBody = Internal.toExpression btrue + } + + lambdaClause :: + Internal.FunctionName -> + Internal.FunctionName -> + Internal.FunctionName -> + Internal.ConstructorName -> + Sem r Internal.LambdaClause + lambdaClause band btrue bisEqual c = do + numArgs :: [IsImplicit] <- getNumArgs + let loc = getLoc _derivingInstanceName + mkpat :: Sem r ([Internal.VarName], Internal.PatternArg) + mkpat = runOutputList . runStreamOf allWords $ do + xs :: [(IsImplicit, Internal.VarName)] <- forM numArgs $ \impl -> do + v <- yield >>= Internal.freshVar loc + output v + return (impl, v) + return (Internal.mkConstructorVarPattern Explicit c xs) + (v1, p1) <- mkpat + (v2, p2) <- mkpat + return + Internal.LambdaClause + { _lambdaPatterns = p1 :| [p2], + _lambdaBody = allEq (zipExact v1 v2) + } + where + allEq :: (Internal.IsExpression expr) => [(expr, expr)] -> Internal.Expression + allEq k = case nonEmpty k of + Nothing -> Internal.toExpression btrue + Just l -> mkAnds (fmap (uncurry mkEq) l) + + mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression + mkAnds = foldl1 mkAnd . fmap Internal.toExpression + + mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression + mkAnd a b = band Internal.@@ a Internal.@@ b + + mkEq :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression + mkEq a b = bisEqual Internal.@@ a Internal.@@ b + + getNumArgs :: Sem r [IsImplicit] + getNumArgs = do + def <- getDefinedConstructor c + return $ + def + ^.. Internal.constructorInfoType + . to Internal.constructorArgs + . each + . Internal.paramImplicit + goFunctionDef :: forall r. (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => FunctionDef 'Scoped -> Sem r Internal.FunctionDef -goFunctionDef FunctionDef {..} = do +goFunctionDef def@FunctionDef {..} = do let _funDefName = goSymbol _signName _funDefTerminating = isJust _signTerminating _funDefIsInstanceCoercion @@ -400,11 +681,10 @@ goFunctionDef FunctionDef {..} = do | otherwise = Nothing _funDefCoercion = isJust _signCoercion _funDefBuiltin = (^. withLocParam) <$> _signBuiltin - _funDefType <- goDefType + _funDefType <- goDefType (functionDefLhs def) _funDefPragmas <- goPragmas _signPragmas _funDefBody <- goBody - msig <- asks (^. S.infoNameSigs . at (_funDefName ^. Internal.nameId)) - _funDefArgsInfo <- maybe (return mempty) (fmap toList . goNameSignature) msig + _funDefArgsInfo <- goArgsInfo _funDefName let _funDefDocComment = fmap ppPrintJudoc _signDoc fun = Internal.FunctionDef {..} whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam)) @@ -434,63 +714,71 @@ goFunctionDef FunctionDef {..} = do let _lambdaType :: Maybe Internal.Expression = Nothing return (Internal.ExpressionLambda Internal.Lambda {..}) - goDefType :: Sem r Internal.Expression - goDefType = do - args <- concatMapM (fmap toList . argToParam) (_signTypeSig ^. typeSigArgs) - ret <- maybe freshHole goExpression (_signTypeSig ^. typeSigRetType) - return (Internal.foldFunType args ret) - where - freshHole :: Sem r Internal.Expression - freshHole = do - i <- freshNameId - let loc = maybe (getLoc _signName) getLoc (lastMay (_signTypeSig ^. typeSigArgs)) - h = mkHole loc i - return $ Internal.ExpressionHole h - - argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter) - argToParam a@SigArg {..} = do - let _paramImplicit = _sigArgImplicit - _paramType <- case _sigArgType of - Nothing -> return (Internal.smallUniverseE (getLoc a)) - Just ty -> goExpression ty - - let _paramImpligoExpressioncit = _sigArgImplicit - noName = Internal.FunctionParameter {_paramName = Nothing, ..} - mk :: Concrete.Argument 'Scoped -> Internal.FunctionParameter - mk ma = - let _paramName = - case ma of - Concrete.ArgumentSymbol s -> Just (goSymbol s) - Concrete.ArgumentWildcard {} -> Nothing - in Internal.FunctionParameter {..} - - arguments :: Maybe (NonEmpty (Argument 'Scoped)) - arguments = case _sigArgNames of - SigArgNamesInstance -> Nothing - SigArgNames ns -> Just ns - - return (maybe (pure noName) (fmap mk) arguments) - - argToPattern :: SigArg 'Scoped -> Sem r (NonEmpty Internal.PatternArg) - argToPattern arg@SigArg {..} = do - let _patternArgIsImplicit = _sigArgImplicit - _patternArgName :: Maybe Internal.Name = Nothing - noName = goWildcard (Wildcard (getLoc arg)) - goWildcard w = do - _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w - return Internal.PatternArg {..} - mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg - mk = \case - Concrete.ArgumentSymbol s -> - let _patternArgPattern = Internal.PatternVariable (goSymbol s) - in return Internal.PatternArg {..} - Concrete.ArgumentWildcard w -> goWildcard w +argToPattern :: + forall r. + (Members '[NameIdGen] r) => + SigArg 'Scoped -> + Sem r (NonEmpty Internal.PatternArg) +argToPattern arg@SigArg {..} = do + let _patternArgIsImplicit = _sigArgImplicit + _patternArgName :: Maybe Internal.Name = Nothing + noName = goWildcard (Wildcard (getLoc arg)) + goWildcard w = do + _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w + return Internal.PatternArg {..} + mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg + mk = \case + Concrete.ArgumentSymbol s -> + let _patternArgPattern = Internal.PatternVariable (goSymbol s) + in return Internal.PatternArg {..} + Concrete.ArgumentWildcard w -> goWildcard w + + arguments :: Maybe (NonEmpty (Argument 'Scoped)) + arguments = case _sigArgNames of + SigArgNamesInstance -> Nothing + SigArgNames ns -> Just ns + maybe (pure <$> noName) (mapM mk) arguments + +goDefType :: + forall r. + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + FunctionLhs 'Scoped -> + Sem r Internal.Expression +goDefType FunctionLhs {..} = do + args <- concatMapM (fmap toList . argToParam) (_funLhsTypeSig ^. typeSigArgs) + ret <- maybe freshHole goExpression (_funLhsTypeSig ^. typeSigRetType) + return (Internal.foldFunType args ret) + where + freshHole :: Sem r Internal.Expression + freshHole = do + i <- freshNameId + let loc = maybe (getLoc _funLhsName) getLoc (lastMay (_funLhsTypeSig ^. typeSigArgs)) + h = mkHole loc i + return $ Internal.ExpressionHole h + + argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter) + argToParam a@SigArg {..} = do + let _paramImplicit = _sigArgImplicit + _paramType <- case _sigArgType of + Nothing -> return (Internal.smallUniverseE (getLoc a)) + Just ty -> goExpression ty + + let _paramImpligoExpressioncit = _sigArgImplicit + noName = Internal.FunctionParameter {_paramName = Nothing, ..} + mk :: Concrete.Argument 'Scoped -> Internal.FunctionParameter + mk ma = + let _paramName = + case ma of + Concrete.ArgumentSymbol s -> Just (goSymbol s) + Concrete.ArgumentWildcard {} -> Nothing + in Internal.FunctionParameter {..} arguments :: Maybe (NonEmpty (Argument 'Scoped)) arguments = case _sigArgNames of SigArgNamesInstance -> Nothing SigArgNames ns -> Just ns - maybe (pure <$> noName) (mapM mk) arguments + + return (maybe (pure noName) (fmap mk) arguments) goInductiveParameters :: forall r. @@ -519,6 +807,7 @@ checkBuiltinInductive :: Sem r () checkBuiltinInductive d b = localBuiltins $ case b of BuiltinNat -> checkNatDef d + BuiltinEq -> checkEqDef d BuiltinBool -> checkBoolDef d BuiltinInt -> checkIntDef d BuiltinList -> checkListDef d @@ -541,6 +830,7 @@ checkBuiltinFunction :: Sem r () checkBuiltinFunction d f = localBuiltins $ case f of BuiltinAssert -> checkAssert d + BuiltinIsEqual -> checkIsEq d BuiltinNatPlus -> checkNatPlus d BuiltinNatSub -> checkNatSub d BuiltinNatMul -> checkNatMul d @@ -638,7 +928,17 @@ checkBuiltinAxiom d b = localBuiltins $ case b of BuiltinByteArrayLength -> checkByteArrayLength d goInductive :: - (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => + ( Members + '[ Reader EntryPoint, + Reader DefaultArgsStack, + State LocalTable, + NameIdGen, + Reader Pragmas, + Error ScoperError, + Reader S.InfoTable + ] + r + ) => InductiveDef 'Scoped -> Sem r Internal.InductiveDef goInductive ty@InductiveDef {..} = do @@ -667,11 +967,13 @@ goInductive ty@InductiveDef {..} = do checkInductiveConstructors indDef return indDef --- | Checks constructors so we can access them for generating field projections -checkInductiveConstructors :: (Members '[State ConstructorInfos] r) => Internal.InductiveDef -> Sem r () +-- | Stores constructors so we can access them for generating field projections and deriving instances +checkInductiveConstructors :: (Members '[State LocalTable] r) => Internal.InductiveDef -> Sem r () checkInductiveConstructors indDef = do - m <- gets (^. constructorInfos) - put (ConstructorInfos $ foldr (uncurry HashMap.insert) m (mkConstructorEntries indDef)) + let tinfo = inductiveInfoFromInductiveDef indDef + modify (set (localInfoInductives . at (indDef ^. Internal.inductiveName)) (Just tinfo)) + forM_ (mkConstructorEntries indDef) $ \(cname, cinfo) -> + modify (over localInfoConstructors (HashMap.insert cname cinfo)) goConstructorDef :: forall r. diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs index f1b0b50371..71ece1b391 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs @@ -52,25 +52,32 @@ newtype LhsTooManyPatterns = LhsTooManyPatterns makeLenses ''LhsTooManyPatterns instance ToGenericError LhsTooManyPatterns where - genericError e = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = ppOutput msg, - _genericErrorIntervals = [i] - } + genericError e = genErr <$> ask where - i = getLocSpan (e ^. lhsTooManyPatternsRemaining) - n = length (e ^. lhsTooManyPatternsRemaining) - howMany = - "The last" <+> case n of - 1 -> "pattern" - _ -> pretty n <+> "patterns" - msg = - howMany <+> "on the left hand side of the function clause" <+> wasWere <+> "not expected" - wasWere - | n == 1 = "was" - | otherwise = "were" + genErr opts = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = [i] + } + where + opts' = fromGenericOptions opts + i = getLocSpan (e ^. lhsTooManyPatternsRemaining) + n = length (e ^. lhsTooManyPatternsRemaining) + howMany = + "The last" <+> case n of + 1 -> "pattern" + _ -> pretty n <+> "patterns" + msg = + howMany + <+> "on the left hand side of the function clause" + <+> wasWere + <+> "not expected" + <> line + <> itemize (ppCode opts' <$> (e ^. lhsTooManyPatternsRemaining)) + wasWere + | n == 1 = "was" + | otherwise = "were" data WrongPatternIsImplicit = WrongPatternIsImplicit { _wrongPatternIsImplicitExpected :: IsImplicit, diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs index 542e28f9c4..38bff632ca 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -87,7 +87,8 @@ toConcrete t p = run . runReader l $ do _signTypeSig = TypeSig { _typeSigArgs = [], - .. + _typeSigRetType, + _typeSigColonKw } return ( StatementFunctionDef @@ -98,7 +99,9 @@ toConcrete t p = run . runReader l $ do _signDoc = Nothing, _signCoercion = Nothing, _signBuiltin = Nothing, - .. + _signName, + _signBody, + _signTypeSig } ) diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index c80761f933..71c71145a9 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs @@ -52,6 +52,7 @@ data InductiveInfo = InductiveInfo _inductiveInfoConstructors :: [ConstrName], _inductiveInfoPositive :: Bool, _inductiveInfoTrait :: Bool, + _inductiveInfoLoc :: Interval, _inductiveInfoPragmas :: Pragmas } deriving stock (Generic) @@ -60,6 +61,9 @@ instance Serialize InductiveInfo instance NFData InductiveInfo +instance HasLoc InductiveInfo where + getLoc InductiveInfo {..} = _inductiveInfoLoc + data InfoTable = InfoTable { _infoConstructors :: HashMap Name ConstructorInfo, _infoAxioms :: HashMap Name AxiomInfo, diff --git a/src/Juvix/Data/Effect/Fail.hs b/src/Juvix/Data/Effect/Fail.hs index ecd07a7e49..732bdc2054 100644 --- a/src/Juvix/Data/Effect/Fail.hs +++ b/src/Juvix/Data/Effect/Fail.hs @@ -1,19 +1,24 @@ -- | An effect similar to Polysemy Fail but without an error message -module Juvix.Data.Effect.Fail where +module Juvix.Data.Effect.Fail + ( module Juvix.Data.Effect.Fail, + module Effectful.Fail, + ) +where import Control.Exception qualified as X +import Control.Monad.Fail qualified as Fail +import Effectful.Fail (Fail) +import Effectful.Fail qualified as Fail import Juvix.Prelude.Base -data Fail :: Effect where - Fail :: Fail m a - -makeSem ''Fail +fail :: (Member Fail r) => Sem r a +fail = Fail.fail "fail" -- | Run a 'Fail' effect purely. runFail :: Sem (Fail ': r) a -> Sem r (Maybe a) -runFail = fmap (^? _Right) . reinterpret (runError @()) (\Fail -> throw ()) +runFail = fmap (^? _Right) . reinterpret (runError @()) (\Fail.Fail {} -> throw ()) {-# INLINE runFail #-} -- | Run a 'Fail' effect purely with a default value. diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index fca34d037f..cb5541eab3 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -7,6 +7,9 @@ where import Juvix.Data.Keyword import Juvix.Extra.Strings qualified as Str +kwDeriving :: Keyword +kwDeriving = asciiKw Str.deriving_ + kwAs :: Keyword kwAs = asciiKw Str.as diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 95883bd3ce..bc5ee62bfd 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -452,6 +452,9 @@ builtinSeq = "seq" as :: (IsString s) => s as = "as" +deriving_ :: (IsString s) => s +deriving_ = "deriving" + builtin :: (IsString s) => s builtin = "builtin" @@ -539,6 +542,9 @@ seqq_ = ">>>" sseq_ :: (IsString s) => s sseq_ = "seq" +isEqual :: (IsString s) => s +isEqual = "isEqual" + eq :: (IsString s) => s eq = "eq" @@ -1145,6 +1151,9 @@ anomaMkResource = "mkResource" anomaMkAction :: (IsString s) => s anomaMkAction = "mkAction" +mkEq :: (IsString s) => s +mkEq = "mkEq" + rustFn :: (IsString s) => s rustFn = "fn" diff --git a/src/Juvix/Prelude.hs b/src/Juvix/Prelude.hs index 58535957ee..e73f3c1ff2 100644 --- a/src/Juvix/Prelude.hs +++ b/src/Juvix/Prelude.hs @@ -1,7 +1,6 @@ module Juvix.Prelude ( module Juvix.Prelude.Base, module Juvix.Prelude.Lens, - module Juvix.Prelude.Stream, module Juvix.Prelude.Generic, module Juvix.Prelude.Trace, module Juvix.Prelude.Path, @@ -16,5 +15,4 @@ import Juvix.Prelude.Generic import Juvix.Prelude.Lens import Juvix.Prelude.Path import Juvix.Prelude.Prepath -import Juvix.Prelude.Stream import Juvix.Prelude.Trace diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index 8cb924a00c..87908e1e2d 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -180,6 +180,7 @@ import Data.Singletons hiding ((@@)) import Data.Singletons.Sigma import Data.Singletons.TH (genSingletons, promoteOrdInstances, singOrdInstances) import Data.Stream (Stream) +import Data.Stream qualified as Stream import Data.String import Data.String.Interpolate (__i) import Data.Text (Text, pack, strip, unpack) @@ -888,3 +889,26 @@ graphCycle gi = goChildren :: NonEmpty Vertex -> [Tree Vertex] -> Either (NonEmpty Vertex) () goChildren path = mapM_ (go path) + +allNaturals :: Stream Natural +allNaturals = Stream.iterate succ 0 + +allWords :: Stream Text +allWords = pack . toList <$> allFiniteSequences ('a' :| ['b' .. 'z']) + +-- | Returns all non-empty finite sequences +allFiniteSequences :: forall a. NonEmpty a -> Stream (NonEmpty a) +allFiniteSequences elems = build 0 [] + where + build :: Integer -> [NonEmpty a] -> Stream (NonEmpty a) + build n = \case + [] -> build (succ n) (toList (ofLength (succ n))) + s : ss -> Stream.Cons s (build n ss) + ofLength :: Integer -> NonEmpty (NonEmpty a) + ofLength n + | n < 1 = impossible + | n == 1 = pure <$> elems + | otherwise = do + seq <- ofLength (n - 1) + e <- elems + return (pure e <> seq) diff --git a/src/Juvix/Prelude/Effects/StreamOf.hs b/src/Juvix/Prelude/Effects/StreamOf.hs index bcd0e241da..dbb5ecc39b 100644 --- a/src/Juvix/Prelude/Effects/StreamOf.hs +++ b/src/Juvix/Prelude/Effects/StreamOf.hs @@ -9,7 +9,6 @@ where import Data.Stream import Juvix.Prelude.Base.Foundation import Juvix.Prelude.Effects.Base -import Juvix.Prelude.Stream data StreamOf (i :: GHCType) :: Effect diff --git a/src/Juvix/Prelude/Stream.hs b/src/Juvix/Prelude/Stream.hs index 34ea7b8162..7d73d44c23 100644 --- a/src/Juvix/Prelude/Stream.hs +++ b/src/Juvix/Prelude/Stream.hs @@ -1,27 +1,6 @@ -module Juvix.Prelude.Stream where +module Juvix.Prelude.Stream + ( module Data.Stream, + ) +where -import Data.Stream qualified as Stream -import Juvix.Prelude.Base.Foundation - -allNaturals :: Stream Natural -allNaturals = Stream.iterate succ 0 - -allWords :: Stream Text -allWords = pack . toList <$> allFiniteSequences ('a' :| ['b' .. 'z']) - --- | Returns all non-empty finite sequences -allFiniteSequences :: forall a. NonEmpty a -> Stream (NonEmpty a) -allFiniteSequences elems = build 0 [] - where - build :: Integer -> [NonEmpty a] -> Stream (NonEmpty a) - build n = \case - [] -> build (succ n) (toList (ofLength (succ n))) - s : ss -> Stream.Cons s (build n ss) - ofLength :: Integer -> NonEmpty (NonEmpty a) - ofLength n - | n < 1 = impossible - | n == 1 = pure <$> elems - | otherwise = do - seq <- ofLength (n - 1) - e <- elems - return (pure e <> seq) +import Data.Stream diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 178b43554a..b7afcd21c1 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -495,5 +495,10 @@ tests = "Test084: issue3030" $(mkRelDir ".") $(mkRelFile "test084.juvix") - $(mkRelFile "out/test084.out") + $(mkRelFile "out/test084.out"), + posTest + "Test085: Deriving Eq" + $(mkRelDir ".") + $(mkRelFile "test085.juvix") + $(mkRelFile "out/test085.out") ] diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index f3f8b5d9a0..f97949aecc 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -298,5 +298,10 @@ scoperErrorTests = "Import cycles (issue3161)" $(mkRelDir "issue3161") $(mkRelFile "Stdlib/Trait/Partial.juvix") - $ wantsError ErrImportCycleNew + $ wantsError ErrImportCycleNew, + negTest + "Deriving statement wrong form" + $(mkRelDir ".") + $(mkRelFile "WrongDeriving.juvix") + $ wantsError ErrDerivingTypeWrongForm ] diff --git a/tests/Compilation/positive/out/test085.out b/tests/Compilation/positive/out/test085.out new file mode 100644 index 0000000000..aa80bbcca5 --- /dev/null +++ b/tests/Compilation/positive/out/test085.out @@ -0,0 +1,7 @@ +true +true +true +true +true +false +false diff --git a/tests/Compilation/positive/test085.juvix b/tests/Compilation/positive/test085.juvix new file mode 100644 index 0000000000..e49b35c0aa --- /dev/null +++ b/tests/Compilation/positive/test085.juvix @@ -0,0 +1,32 @@ +-- Deriving Eq +module test085; + +import Stdlib.Data.Nat open hiding {isEqual}; +import Stdlib.Data.Fixity open; +import Stdlib.Data.Bool open; +import Stdlib.Data.Pair open; +import Stdlib.Trait.Eq open; +import Stdlib.System.IO open; + +syntax alias isEqual := Eq.eq; + +type Tree A := + | Leaf + | Node (Tree A) A (Tree A); + +{-# inline: case #-} +deriving instance +treeEqI {A} {{Eq A}} : Eq (Tree A); + +t1 : Tree Nat := Node (Node Leaf 0 Leaf) 1 Leaf; +t2 : Tree Nat := Node (Node Leaf 1 Leaf) 1 Leaf; +t3 : Tree Nat := Node Leaf 1 (Node Leaf 0 Leaf); + +main : IO := + printLn (isEqual true true) + >>> printLn (not (isEqual false true)) + >>> printLn (isEqual (false, true) (false, true)) + >>> printLn (not (isEqual (false, true) (false, false))) + >>> printLn (isEqual t1 t1) + >>> printLn (isEqual t1 t2) + >>> printLn (isEqual t1 t3); diff --git a/tests/negative/WrongDeriving.juvix b/tests/negative/WrongDeriving.juvix new file mode 100644 index 0000000000..2b98cc80e3 --- /dev/null +++ b/tests/negative/WrongDeriving.juvix @@ -0,0 +1,5 @@ +module WrongDeriving; + +axiom A : Type; + +deriving instance i : A;