From 84ad0040a27366629ee665b2d432bcebdb66bac9 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 20 Nov 2024 15:04:17 +0100 Subject: [PATCH] Squashed commit of the following: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit commit 267b34a3f5a728769fa567421eda1ede5107428c Author: Jan Mas Rovira Date: Wed Nov 20 14:18:11 2024 +0100 give proper name of builtins commit d0dc4155db5fa81945df343faeaf023e7850f094 Author: Jan Mas Rovira Date: Wed Nov 20 14:09:37 2024 +0100 better error message commit ccd90448c514ff1a8e9f00b8dd714b660afc0183 Author: Jan Mas Rovira Date: Wed Nov 20 11:27:05 2024 +0100 allow implicit args commit 768f45d5d04505307534ed0e54d109e27ea34e48 Author: Jan Mas Rovira Date: Tue Nov 19 18:44:50 2024 +0100 stdlib commit e778aaf9a427e8af1cec89f5d164cdec9d0984aa Author: Jan Mas Rovira Date: Tue Nov 19 18:29:00 2024 +0100 clean commit 17939c76ea4f034c2840463f24dfd8c7a5325645 Author: Jan Mas Rovira Date: Tue Nov 19 18:27:22 2024 +0100 update stdlib commit 46d73889ae26f8c0d0b34c666ef1b35ad2af859e Author: Jan Mas Rovira Date: Tue Nov 19 18:18:22 2024 +0100 pragmas commit 58d1063b4e4d683f6b6bd314e444d65f30534fd3 Author: Jan Mas Rovira Date: Tue Nov 19 18:09:23 2024 +0100 do not group deriving statements commit 057fdbbeef54683d4c16116bb00e097c00496203 Author: Jan Mas Rovira Date: Tue Nov 19 15:14:31 2024 +0100 default case commit d280fe741c34eaf60543d6cc4c311470d12ead0b Author: Jan Mas Rovira Date: Tue Nov 19 14:55:36 2024 +0100 fix commit e3a7a764872d2c95ebcfbc1a0c5f3b4848c0b0da Author: Jan Mas Rovira Date: Tue Nov 19 09:57:22 2024 +0100 from concrete commit f8fd9f484737749d26d63e41fa6759a82d50fb23 Author: Jan Mas Rovira Date: Mon Nov 18 18:45:20 2024 +0100 refactor Fail commit a889cb65ffa7c62572aa286ac7b669f28d57d5d8 Author: Jan Mas Rovira Date: Mon Nov 18 18:00:27 2024 +0100 wip commit 734f7c192d84e1e637175826b520d994e2f38ec6 Author: Jan Mas Rovira Date: Mon Nov 18 13:00:14 2024 +0100 wip commit 6a2d7d2c994c315e9af86071c94a0f4be33cbeef Author: Jan Mas Rovira Date: Fri Nov 15 13:29:44 2024 +0100 parsing and printing deriving kw commit 412a6545ba3b00a9226103f2a828d7b96e6fe164 Author: Jan Mas Rovira Date: Fri Nov 15 12:52:11 2024 +0100 add deriving kw commit 110146284952ab8d985ca86875c4594eef9375ca Author: Jan Mas Rovira Date: Fri Nov 15 12:51:18 2024 +0100 style commit 3aeec441865484fef18e9956b3579215cddc7c60 Author: Jan Mas Rovira Date: Thu Nov 14 17:39:09 2024 +0100 remove section titles from parser commit 15ec17dd6d8c1f4f421df51d520a1e26f48cc05c Author: Jan Mas Rovira Date: Thu Nov 14 15:29:57 2024 +0100 update stdlib commit 546b5b2f7a6f2a2d4579406f7f672a5a02a19a42 Author: Jan Mas Rovira Date: Thu Nov 14 11:27:04 2024 +0100 make Eq builtin commit 865842046d8ecfe6605f599dbf47ac1debfaa868 Author: Paul Cadman Date: Wed Nov 20 07:53:21 2024 +0000 Support running nockma code with a running Anoma client (#3180) This PR: 1. Adds a new interpretation for the Anoma effect, which makes gRPC calls to an existing Anoma client instead of spawning a new one. 2. Adds a new `nockma run` mode, `with-client`, which can be used to run an Anoma program against a running Anoma client, using its URL and gRPC port. 3. separates the `nockma run` command into subcommands. CLI docs: ## `nockma run` ``` Usage: juvix dev nockma run COMMAND Subcommands used to run an Anoma program. Use with artefacts obtained from compilation with the anoma target Available options: -h,--help Show this help text Available commands: builtin-evaluator Run with the builtin Nockma evaluator ephemeral-client Run with an ephemeral Anoma client with-client Run with a running Anoma client ``` ### `with-client` ``` Usage: juvix dev nockma run with-client NOCKMA_FILE [--args ARGS_FILE] (-p|--grpc-port PORT) [--url URL] Run with a running Anoma client Available options: NOCKMA_FILE Path to a .nockma file --args ARGS_FILE Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0]). -p,--grpc-port PORT The GRPC port of a running Anoma client --url URL The URL of a running Anoma client. default: localhost -h,--help Show this help text ``` ### `ephemeral-client` ``` Usage: juvix dev nockma run ephemeral-client NOCKMA_FILE [--args ARGS_FILE] --anoma-dir ANOMA_DIR Run with an ephemeral Anoma client Available options: NOCKMA_FILE Path to a .nockma file --args ARGS_FILE Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0]). --anoma-dir ANOMA_DIR Path to anoma repository -h,--help Show this help text ``` ### `builtin-evaluator` ``` Usage: juvix dev nockma run builtin-evaluator NOCKMA_FILE [--args ARGS_FILE] [--profile] Run with the builtin Nockma evaluator Available options: NOCKMA_FILE Path to a .nockma file --args ARGS_FILE Path to file containing args. The args file should contain a list (i.e. to pass 2 and [1 4] as args, the contents should be [2 [1 4] 0]). --profile Report evaluator profiling statistics -h,--help Show this help text ``` commit 455249db4d02838d562892075981557bd32a1451 Author: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com> Date: Tue Nov 19 20:34:52 2024 +0100 HTML generation: make the light theme lighter (#3168) * Closes #3141 * Adds the `latte-light` theme with lighter background and makes it the default. This is a bit subjective, but in my opinion the light theme should not have a background darker than the browser window pane. It should be close to white. commit eab02a77da25b07d7336d0f03f5cb065d1da9f2e Author: Paul Cadman Date: Tue Nov 19 17:34:13 2024 +0000 Remove `GetAnomaProcess` from the Anoma effect (#3179) This PR removes `GetAnomaProcess` from the Anoma effect. Use the `launchAnoma` function to start a persistent Anoma client / server (used by `juvix dev anoma node`). Other changes: * It's no longer necessary to pass the protobuf files to `grpcurl` because the Anoma client now supports gRPC reflection. * We pass the elixir start command to `mix` via `-e` argument instead of using a temporary file. The purpose for this change is that we I want to add an interpreter for Anoma that makes gRPC calls to an exisitng Anoma client. `GetAnomaProcess` has no meaning for this interpreter. --- 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 | 7 +- 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 | 68 ++- src/Juvix/Compiler/Concrete/Print/Base.hs | 6 + .../FromParsed/Analysis/Scoping.hs | 220 +++++--- .../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 | 489 ++++++++++++++---- .../Analysis/ArityChecking/Error/Types.hs | 43 +- src/Juvix/Compiler/Pipeline/Package/Loader.hs | 6 +- .../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 +- 36 files changed, 890 insertions(+), 301 deletions(-) create mode 100644 src/Juvix/Compiler/Builtins/Eq.hs 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..56c1869112 --- /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) + unless (isSmallUniverse' (d ^. inductiveType)) (err "Lists should be in the small universe") + let eqTxt = prettyText BuiltinEq + 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..775edf35ca 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 @@ -153,16 +153,22 @@ anameFromScopedIden s = _anameVerbatim = s ^. scopedIdenSrcName . nameVerbatim } -lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a +getInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a +getInfo f = do + tab1 <- ask + fromMaybe (fromJust (f tab1)) . f <$> getBuilderInfoTable + +lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r (Maybe a) lookupInfo f = do tab1 <- ask - fromMaybe (fromJust (f tab1)) . f <$> getInfoTable + tab2 <- getBuilderInfoTable + 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 = getInfo (^. 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..1960655531 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -63,8 +63,13 @@ 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 a = do + mapM_ addSigArg (a ^. funLhsArgs) + whenJust (a ^. funLhsRetType) addExpressionType + 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..2c049b1e7b 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 _funLhsArgs + +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..ffcc6ab2de 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, @@ -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 <$> _funLhsRetType) + ) + 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..97bbd5fe28 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,44 +1052,109 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do (@$>) :: (Functor m) => (a -> m ()) -> a -> m a (@$>) f a = f a $> a -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 - 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 - names' <- checkSigArgNames _sigArgNames - ty' <- mapM checkParseExpressionAtoms _sigArgType - default' <- case _sigArgDefault of - Nothing -> return Nothing - Just ArgDefault {..} -> - let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg}) - in case _sigArgImplicit of - Explicit -> err - ImplicitInstance -> err - Implicit -> do - val' <- checkParseExpressionAtoms _argDefaultValue - return (Just ArgDefault {_argDefaultValue = val', ..}) - return - SigArg - { _sigArgNames = names', - _sigArgType = ty', - _sigArgDefault = default', +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 + (args', ret') <- withLocalScope $ do + args' <- mapM checkSigArg _funLhsArgs + ret' <- mapM checkParseExpressionAtoms _funLhsRetType + return (args', ret') + name' <- + if + | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName + | otherwise -> reserveFunctionSymbol lhs + let lhs' = + FunctionLhs + { _funLhsArgs = args', + _funLhsRetType = ret', + _funLhsName = name', .. } + return + Deriving + { _derivingFunLhs = lhs', + .. + } + +checkSigArg :: + ( Members + '[ State Scope, + Error ScoperError, + State ScoperState, + Reader ScopeParameters, + Reader InfoTable, + Reader PackageId, + HighlightBuilder, + InfoTableBuilder, + NameIdGen, + State ScoperSyntax, + Reader BindingStrategy + ] + r + ) => + SigArg 'Parsed -> + Sem r (SigArg 'Scoped) +checkSigArg arg@SigArg {..} = do + names' <- checkSigArgNames _sigArgNames + ty' <- mapM checkParseExpressionAtoms _sigArgType + default' <- case _sigArgDefault of + Nothing -> return Nothing + Just ArgDefault {..} -> + let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg}) + in case _sigArgImplicit of + Explicit -> err + ImplicitInstance -> err + Implicit -> do + val' <- checkParseExpressionAtoms _argDefaultValue + return (Just ArgDefault {_argDefaultValue = val', ..}) + return + SigArg + { _sigArgNames = names', + _sigArgType = ty', + _sigArgDefault = default', + .. + } + +checkSigArgNames :: + ( Members + '[ State Scope, + Error ScoperError, + State ScoperState, + Reader ScopeParameters, + Reader InfoTable, + Reader PackageId, + HighlightBuilder, + InfoTableBuilder, + NameIdGen, + State ScoperSyntax, + Reader BindingStrategy + ] + r + ) => + 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. @@ -1115,8 +1169,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 +1219,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 +1538,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 +1674,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 +1730,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 +1871,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 +1906,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,7 +2194,8 @@ checkAxiomDef :: AxiomDef 'Parsed -> Sem r (AxiomDef 'Scoped) checkAxiomDef AxiomDef {..} = do - axiomName' <- bindAxiomSymbol _axiomName + axiomType' <- withLocalScope (checkParseExpressionAtoms _axiomType) + axiomName' <- getReservedDefinitionSymbol _axiomName axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc) axiomSig' <- withLocalScope (checkTypeSig _axiomTypeSig) let a = AxiomDef {_axiomName = axiomName', _axiomTypeSig = axiomSig', _axiomDoc = axiomDoc', ..} @@ -2185,6 +2258,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..95e46588ce 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 @@ -63,10 +71,12 @@ fromConcrete :: 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 +84,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 +161,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 +220,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 +280,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 +302,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 +326,7 @@ scanImports = mconcatMap go StatementAxiom {} -> [] StatementSyntax {} -> [] StatementFunctionDef {} -> [] + StatementDeriving {} -> [] StatementProjectionDef {} -> [] goImport :: @@ -331,7 +343,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 +352,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 +384,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 +403,263 @@ 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 + deriveTrait der _derivingPragmas ret name funArgs (n, traitArgs) + +deriveTrait :: + ( Members + '[ Reader S.InfoTable, + Reader Pragmas, + Reader DefaultArgsStack, + Error ScoperError, + Reader Internal.InfoTable, + State LocalTable, + NameIdGen + ] + r + ) => + Internal.DerivingTrait -> + Maybe ParsedPragmas -> + Internal.Expression -> + Internal.Name -> + [Internal.FunctionParameter] -> + (Internal.InductiveName, [Internal.ApplicationArg]) -> + 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 + ) => + Maybe ParsedPragmas -> + Internal.Expression -> + Internal.FunctionName -> + [Internal.FunctionParameter] -> + (Internal.InductiveName, [Internal.ApplicationArg]) -> + Sem r Internal.FunctionDef +deriveEq pragmas ret instanceName funParams (eqName, args) = do + arg <- getArg + argsInfo <- goArgsInfo instanceName + lam <- eqLambda arg + mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq + let body = mkEq Internal.@@ lam + ty = Internal.foldFunType funParams (Internal.foldApplication (Internal.toExpression eqName) args) + pragmas' <- goPragmas pragmas + return + Internal.FunctionDef + { _funDefTerminating = False, + _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance, + _funDefPragmas = pragmas', + _funDefArgsInfo = argsInfo, + _funDefDocComment = Nothing, + _funDefName = instanceName, + _funDefType = ty, + _funDefBody = body, + _funDefBuiltin = Nothing + } + where + 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 instanceName + 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 +668,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 +701,79 @@ 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) _funLhsArgs + ret <- maybe freshHole goExpression _funLhsRetType + return (Internal.foldFunType args ret) + where + freshHole :: Sem r Internal.Expression + freshHole = do + i <- freshNameId + let loc = maybe (getLoc _funLhsName) getLoc (lastMay _funLhsArgs) + 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 +802,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 +825,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 +923,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 +962,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..cc1a224bdd 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -98,7 +98,11 @@ toConcrete t p = run . runReader l $ do _signDoc = Nothing, _signCoercion = Nothing, _signBuiltin = Nothing, - .. + _signArgs = [], + _signRetType, + _signName, + _signColonKw, + _signBody } ) 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