From 2c8a36414338cad6275207fe143db50a2b8e99cb Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 10 Jul 2023 19:57:55 +0200 Subject: [PATCH] New syntax for function definitions (#2243) - Closes #2060 - Closes #2189 - This pr adds support for the syntax described in #2189. It does not drop support for the old syntax. It is possible to automatically translate juvix files to the new syntax by using the formatter with the `--new-function-syntax` flag. E.g. ``` juvix format --in-place --new-function-syntax ``` # Syntax changes Type signatures follow this pattern: ``` f (a1 : Expr) .. (an : Expr) : Expr ``` where each `ai` is a non-empty list of symbols. Braces are used instead of parentheses when the argument is implicit. Then, we have these variants: 1. Simple body. After the signature we have `:= Expr;`. 2. Clauses. The function signature is followed by a non-empty sequence of clauses. Each clause has the form: ``` | atomPat .. atomPat := Expr ``` # Mutual recursion Now identifiers **do not need to be defined before they are used**, making it possible to define mutually recursive functions/types without any special syntax. There are some exceptions to this. We cannot forward reference a symbol `f` in some statement `s` if between `s` and the definition of `f` there is one of the following statements: 1. Local module 2. Import statement 3. Open statement I think it should be possible to drop the restriction for local modules and import statements --- Makefile | 16 +- app/Commands/Format.hs | 11 +- app/Commands/Format/Options.hs | 6 + app/Commands/Repl.hs | 24 +- juvix-stdlib | 2 +- src/Juvix/Compiler/Concrete/Data/InfoTable.hs | 35 +- .../Concrete/Data/InfoTableBuilder.hs | 19 +- src/Juvix/Compiler/Concrete/Data/NameRef.hs | 99 ---- src/Juvix/Compiler/Concrete/Extra.hs | 54 ++ src/Juvix/Compiler/Concrete/Language.hs | 241 +++++++-- src/Juvix/Compiler/Concrete/Pretty.hs | 6 +- src/Juvix/Compiler/Concrete/Print.hs | 4 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 88 ++- .../FromParsed/Analysis/Scoping.hs | 508 ++++++++++++++---- .../FromParsed/Analysis/Scoping/Error.hs | 2 - .../Analysis/Scoping/Error/Types.hs | 29 - .../Concrete/Translation/FromSource.hs | 85 ++- .../Internal/Translation/FromConcrete.hs | 92 +++- src/Juvix/Formatter.hs | 26 +- test/Formatter/Positive.hs | 9 +- test/Scope/Negative.hs | 7 - test/Scope/Positive.hs | 14 +- tests/Compilation/positive/test052.juvix | 5 +- tests/negative/DuplicateClause.juvix | 7 - tests/positive/Format.juvix | 36 +- tests/positive/SignatureWithBody.juvix | 30 +- tests/positive/Syntax.juvix | 60 +++ tests/smoke/Commands/repl.smoke.yaml | 12 +- 28 files changed, 1106 insertions(+), 421 deletions(-) delete mode 100644 tests/negative/DuplicateClause.juvix create mode 100644 tests/positive/Syntax.juvix diff --git a/Makefile b/Makefile index b91ad4521a..72b464e1b0 100644 --- a/Makefile +++ b/Makefile @@ -114,7 +114,7 @@ JUVIXFILESTOFORMAT=$(shell find \ -type d \( -name ".juvix-build" -o -name "FancyPaths" \) -prune -o \ -type f -name "*.juvix" -print) -JUVIXFORMATFLAGS?=--in-place +JUVIXFORMATFLAGS?=--in-place --new-function-syntax JUVIXTYPECHECKFLAGS?=--only-errors .PHONY: format-juvix-files @@ -124,12 +124,12 @@ format-juvix-files: exit_code=$$?; \ if [ $$exit_code -eq 0 ]; then \ echo "[OK] $$file"; \ - elif [[ $$exit_code -ne 0 && "$$file" == *"tests/"* ]]; then \ + elif [[ $$exit_code -ne 0 && "$$file" == *"tests/"* ]]; then \ echo "[CONTINUE] $$file is in tests directory."; \ - else \ - echo "[FAIL] $$file formatting failed" && exit 1; \ - fi; \ - done; + else \ + echo "[FAIL] $$file formatting failed" && exit 1; \ + fi; \ + done; .PHONY: check-format-juvix-files check-format-juvix-files: @@ -147,8 +147,8 @@ typecheck-juvix-examples: if [ $$exit_code -eq 0 ]; then \ echo "[OK] $$file typechecks"; \ else \ - echo "[FAIL] Typecking failed for $$file" && exit 1; \ - fi; \ + echo "[FAIL] Typecking failed for $$file" && exit 1; \ + fi; \ done .PHONY: check-ormolu diff --git a/app/Commands/Format.hs b/app/Commands/Format.hs index eff05ab6a9..5575bf9dee 100644 --- a/app/Commands/Format.hs +++ b/app/Commands/Format.hs @@ -33,7 +33,7 @@ targetFromOptions opts = do pkgDir <- askPkgDir case f of Just (Left p) -> return (TargetFile p) - Just (Right {}) -> return (TargetProject pkgDir) + Just Right {} -> return (TargetProject pkgDir) Nothing -> do isPackageGlobal <- askPackageGlobal if @@ -49,8 +49,9 @@ targetFromOptions opts = do runCommand :: forall r. Members '[Embed IO, App, Resource, Files] r => FormatOptions -> Sem r () runCommand opts = do target <- targetFromOptions opts + let newSyntax = NewSyntax (opts ^. formatNewSyntax) runOutputSem (renderFormattedOutput target opts) $ runScopeFileApp $ do - res <- case target of + res <- runReader newSyntax $ case target of TargetFile p -> format p TargetProject p -> formatProject p TargetStdin -> formatStdin @@ -89,9 +90,9 @@ renderFormattedOutput target opts fInfo = do outputResult :: FormatRenderMode -> Sem r () outputResult = \case EditInPlace i@FormattedFileInfo {..} -> - runTempFileIO $ - restoreFileOnError _formattedFileInfoPath $ - writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText) + runTempFileIO + . restoreFileOnError _formattedFileInfoPath + $ writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText) NoEdit m -> case m of ReformattedFile ts -> forM_ ts renderStdOut InputPath p -> say (pack (toFilePath p)) diff --git a/app/Commands/Format/Options.hs b/app/Commands/Format/Options.hs index dc179ed186..60b3f48ec9 100644 --- a/app/Commands/Format/Options.hs +++ b/app/Commands/Format/Options.hs @@ -5,6 +5,7 @@ import CommonOptions data FormatOptions = FormatOptions { _formatInput :: Maybe (Prepath FileOrDir), _formatCheck :: Bool, + _formatNewSyntax :: Bool, _formatInPlace :: Bool } deriving stock (Data) @@ -28,6 +29,11 @@ parseFormat = do ( long "check" <> help "Do not print reformatted sources or unformatted file paths to standard output." ) + _formatNewSyntax <- + switch + ( long "new-function-syntax" + <> help "Format the file using the new function syntax." + ) _formatInPlace <- switch ( long "in-place" diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs index 16a1456066..01bcfcaafa 100644 --- a/app/Commands/Repl.hs +++ b/app/Commands/Repl.hs @@ -207,16 +207,16 @@ core input = do compileRes <- liftIO (compileReplInputIO' ctx (strip (pack input))) >>= replFromEither . snd whenJust compileRes (renderOutLn . Core.ppOut opts) -ppConcrete :: (HasLoc a, Concrete.PrettyPrint a) => a -> Repl AnsiText +ppConcrete :: Concrete.PrettyPrint a => a -> Repl AnsiText ppConcrete a = do gopts <- State.gets (^. replStateGlobalOptions) let popts :: GenericOptions = project' gopts return (Concrete.ppOut popts a) -printConcrete :: (HasLoc a, Concrete.PrettyPrint a) => a -> Repl () +printConcrete :: Concrete.PrettyPrint a => a -> Repl () printConcrete = ppConcrete >=> renderOut -printConcreteLn :: (HasLoc a, Concrete.PrettyPrint a) => a -> Repl () +printConcreteLn :: Concrete.PrettyPrint a => a -> Repl () printConcreteLn = ppConcrete >=> renderOutLn replParseIdentifiers :: String -> Repl (NonEmpty Concrete.ScopedIden) @@ -252,11 +252,11 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers printIdentifier :: Concrete.ScopedIden -> Repl () printIdentifier s = do mdoc <- case s of - Concrete.ScopedAxiom a -> getDocAxiom (a ^. Concrete.axiomRefName . Scoped.nameId) - Concrete.ScopedInductive a -> getDocInductive (a ^. Concrete.inductiveRefName . Scoped.nameId) + Concrete.ScopedAxiom a -> getDocAxiom (a ^. Scoped.nameId) + Concrete.ScopedInductive a -> getDocInductive (a ^. Scoped.nameId) Concrete.ScopedVar {} -> return Nothing - Concrete.ScopedFunction f -> getDocFunction (f ^. Concrete.functionRefName . Scoped.nameId) - Concrete.ScopedConstructor c -> getDocConstructor (c ^. Concrete.constructorRefName . Scoped.nameId) + Concrete.ScopedFunction f -> getDocFunction (f ^. Scoped.nameId) + Concrete.ScopedConstructor c -> getDocConstructor (c ^. Scoped.nameId) printDoc mdoc where printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl () @@ -271,7 +271,7 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers getDocFunction fun = do tbl :: Scoped.InfoTable <- getInfoTable let def :: Scoped.FunctionInfo = tbl ^?! Scoped.infoFunctions . at fun . _Just - return (def ^. Scoped.functionInfoType . Concrete.sigDoc) + return (def ^. Scoped.functionInfoDoc) getDocInductive :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped)) getDocInductive ind = do @@ -305,11 +305,11 @@ printDefinition = replParseIdentifiers >=> printIdentifiers printIdentifier :: Concrete.ScopedIden -> Repl () printIdentifier s = do case s of - Concrete.ScopedAxiom a -> printAxiom (a ^. Concrete.axiomRefName . Scoped.nameId) - Concrete.ScopedInductive a -> printInductive (a ^. Concrete.inductiveRefName . Scoped.nameId) + Concrete.ScopedAxiom a -> printAxiom (a ^. Scoped.nameId) + Concrete.ScopedInductive a -> printInductive (a ^. Scoped.nameId) Concrete.ScopedVar {} -> return () - Concrete.ScopedFunction f -> printFunction (f ^. Concrete.functionRefName . Scoped.nameId) - Concrete.ScopedConstructor c -> printConstructor (c ^. Concrete.constructorRefName . Scoped.nameId) + Concrete.ScopedFunction f -> printFunction (f ^. Scoped.nameId) + Concrete.ScopedConstructor c -> printConstructor (c ^. Scoped.nameId) where printLocation :: HasLoc s => s -> Repl () printLocation def = do diff --git a/juvix-stdlib b/juvix-stdlib index 034c5236af..85751d3a7e 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 034c5236afb1c7b9dc0aa6754515001f5694cc7e +Subproject commit 85751d3a7e5edd97a3d12dae197273731a2088cf diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs index 6b88a9ba64..d6b9bd6a80 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs @@ -4,12 +4,17 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Language import Juvix.Prelude -data FunctionInfo = FunctionInfo - { _functionInfoType :: TypeSignature 'Scoped, - _functionInfoClauses :: [FunctionClause 'Scoped] +data OldFunctionInfo = OldFunctionInfo + { _oldFunctionInfoType :: TypeSignature 'Scoped, + _oldFunctionInfoClauses :: [FunctionClause 'Scoped] } deriving stock (Eq, Show) +data FunctionInfo + = FunctionInfoOld OldFunctionInfo + | FunctionInfoNew (FunctionDef 'Scoped) + deriving stock (Eq, Show) + data ConstructorInfo = ConstructorInfo { _constructorInfoDef :: InductiveConstructorDef 'Scoped, _constructorInfoTypeName :: S.Symbol @@ -50,9 +55,25 @@ makeLenses ''InfoTable makeLenses ''InductiveInfo makeLenses ''ConstructorInfo makeLenses ''AxiomInfo -makeLenses ''FunctionInfo +makeLenses ''OldFunctionInfo + +_FunctionInfoOld :: Traversal' FunctionInfo OldFunctionInfo +_FunctionInfoOld f = \case + FunctionInfoOld x -> FunctionInfoOld <$> f x + r@FunctionInfoNew {} -> pure r + +functionInfoDoc :: Lens' FunctionInfo (Maybe (Judoc 'Scoped)) +functionInfoDoc f = \case + FunctionInfoOld i -> do + i' <- traverseOf (oldFunctionInfoType . sigDoc) f i + pure (FunctionInfoOld i') + FunctionInfoNew i -> do + i' <- traverseOf signDoc f i + pure (FunctionInfoNew i') instance HasLoc FunctionInfo where - getLoc f = - getLoc (f ^. functionInfoType) - <>? (getLocSpan <$> nonEmpty (f ^. functionInfoClauses)) + getLoc = \case + FunctionInfoOld f -> + getLoc (f ^. oldFunctionInfoType) + <>? (getLocSpan <$> nonEmpty (f ^. oldFunctionInfoClauses)) + FunctionInfoNew f -> getLoc f diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index 09ff4f1c2b..f3b625e79d 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -13,6 +13,7 @@ data InfoTableBuilder m a where RegisterConstructor :: S.Symbol -> InductiveConstructorDef 'Scoped -> InfoTableBuilder m () RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m () RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m () + RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m () RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m () RegisterName :: (HasLoc c) => S.Name' c -> InfoTableBuilder m () RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m () @@ -45,13 +46,21 @@ toState = reinterpret $ \case in do modify (over infoInductives (HashMap.insert ref info)) registerDoc (ity ^. inductiveName . nameId) j + RegisterFunctionDef f -> + let ref = f ^. signName . S.nameId + info = FunctionInfoNew f + j = f ^. signDoc + in do + modify (set (infoFunctions . at ref) (Just info)) + registerDoc (f ^. signName . nameId) j RegisterTypeSignature f -> let ref = f ^. sigName . S.nameId info = - FunctionInfo - { _functionInfoType = f, - _functionInfoClauses = [] - } + FunctionInfoOld + OldFunctionInfo + { _oldFunctionInfoType = f, + _oldFunctionInfoClauses = [] + } j = f ^. sigDoc in do modify (set (infoFunctions . at ref) (Just info)) @@ -59,7 +68,7 @@ toState = reinterpret $ \case RegisterFunctionClause c -> -- assumes the signature has already been registered let key = c ^. clauseOwnerFunction . S.nameId - in modify (over (infoFunctions . at key . _Just . functionInfoClauses) (`snoc` c)) + in modify (over (infoFunctions . at key . _Just . _FunctionInfoOld . oldFunctionInfoClauses) (`snoc` c)) RegisterName n -> modify (over highlightNames (cons (S.AName n))) RegisterModule m -> do let j = m ^. moduleDoc diff --git a/src/Juvix/Compiler/Concrete/Data/NameRef.hs b/src/Juvix/Compiler/Concrete/Data/NameRef.hs index 44ff913335..b571eb42b8 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameRef.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameRef.hs @@ -1,108 +1,9 @@ -{-# LANGUAGE UndecidableInstances #-} - module Juvix.Compiler.Concrete.Data.NameRef where import Data.Kind qualified as GHC -import Juvix.Compiler.Concrete.Data.Name qualified as C import Juvix.Compiler.Concrete.Data.ScopedName qualified as S -import Juvix.Prelude hiding (show) -import Prelude (show) type RefNameType :: S.IsConcrete -> GHC.Type type family RefNameType c = res | res -> c where RefNameType 'S.Concrete = S.Name RefNameType 'S.NotConcrete = S.Name' () - -type AxiomRef = AxiomRef' 'S.Concrete - -newtype AxiomRef' (n :: S.IsConcrete) = AxiomRef' - {_axiomRefName :: RefNameType n} - -makeLenses ''AxiomRef' - -instance HasLoc AxiomRef where - getLoc = getLoc . (^. axiomRefName) - -instance Hashable (RefNameType s) => Hashable (AxiomRef' s) where - hashWithSalt i = hashWithSalt i . (^. axiomRefName) - -instance (Eq (RefNameType s)) => Eq (AxiomRef' s) where - (==) = (==) `on` (^. axiomRefName) - -instance (Ord (RefNameType s)) => Ord (AxiomRef' s) where - compare = compare `on` (^. axiomRefName) - -instance (Show (RefNameType s)) => Show (AxiomRef' s) where - show = show . (^. axiomRefName) - -type InductiveRef = InductiveRef' 'S.Concrete - -newtype InductiveRef' (n :: S.IsConcrete) = InductiveRef' - { _inductiveRefName :: RefNameType n - } - -makeLenses ''InductiveRef' - -instance HasLoc InductiveRef where - getLoc = getLoc . (^. inductiveRefName) - -instance Hashable (RefNameType s) => Hashable (InductiveRef' s) where - hashWithSalt i = hashWithSalt i . (^. inductiveRefName) - -instance (Eq (RefNameType s)) => Eq (InductiveRef' s) where - (==) = (==) `on` (^. inductiveRefName) - -instance (Ord (RefNameType s)) => Ord (InductiveRef' s) where - compare = compare `on` (^. inductiveRefName) - -instance (Show (RefNameType s)) => Show (InductiveRef' s) where - show = show . (^. inductiveRefName) - -type FunctionRef = FunctionRef' 'S.Concrete - -newtype FunctionRef' (n :: S.IsConcrete) = FunctionRef' - { _functionRefName :: RefNameType n - } - -makeLenses ''FunctionRef' - -instance HasLoc FunctionRef where - getLoc = getLoc . (^. functionRefName) - -instance Hashable (RefNameType s) => Hashable (FunctionRef' s) where - hashWithSalt i = hashWithSalt i . (^. functionRefName) - -instance (Eq (RefNameType s)) => Eq (FunctionRef' s) where - (==) = (==) `on` (^. functionRefName) - -instance (Ord (RefNameType s)) => Ord (FunctionRef' s) where - compare = compare `on` (^. functionRefName) - -instance (Show (RefNameType s)) => Show (FunctionRef' s) where - show = show . (^. functionRefName) - -type ConstructorRef = ConstructorRef' 'S.Concrete - -newtype ConstructorRef' (n :: S.IsConcrete) = ConstructorRef' - { _constructorRefName :: RefNameType n - } - -makeLenses ''ConstructorRef' - -instance HasLoc ConstructorRef where - getLoc = getLoc . (^. constructorRefName) - -instance Hashable (RefNameType s) => Hashable (ConstructorRef' s) where - hashWithSalt i = hashWithSalt i . (^. constructorRefName) - -instance (Eq (RefNameType s)) => Eq (ConstructorRef' s) where - (==) = (==) `on` (^. constructorRefName) - -instance (Ord (RefNameType s)) => Ord (ConstructorRef' s) where - compare = compare `on` (^. constructorRefName) - -instance (Show (RefNameType s)) => Show (ConstructorRef' s) where - show = show . (^. constructorRefName) - -concreteFunctionRef :: C.Name -> FunctionRef' 'S.NotConcrete -> FunctionRef -concreteFunctionRef s = over functionRefName (set S.nameConcrete s) diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index d9f38cd81b..4af84b47d9 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -6,12 +6,14 @@ module Juvix.Compiler.Concrete.Extra unfoldApplication, groupStatements, flattenStatement, + migrateFunctionSyntax, ) where import Data.HashMap.Strict qualified as HashMap import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Concrete.Data.ScopedName qualified as S +import Juvix.Compiler.Concrete.Keywords import Juvix.Compiler.Concrete.Language import Juvix.Prelude hiding (some) import Juvix.Prelude.Parsing @@ -98,6 +100,8 @@ groupStatements = \case (StatementModule {}, _) -> False (StatementAxiom {}, StatementAxiom {}) -> False (StatementAxiom {}, _) -> False + (StatementFunctionDef {}, _) -> False + (_, StatementFunctionDef {}) -> False (StatementTypeSignature sig, StatementFunctionClause fun) -> case sing :: SStage s of SParsed -> sig ^. sigName == fun ^. clauseOwnerFunction @@ -134,3 +138,53 @@ flattenStatement :: Statement s -> [Statement s] flattenStatement = \case StatementModule m -> concatMap flattenStatement (m ^. moduleBody) s -> [s] + +migrateFunctionSyntax :: Module 'Scoped t -> Module 'Scoped t +migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m + where + goStatement :: Statement 'Scoped -> Maybe (Statement 'Scoped) + goStatement s = case s of + StatementSyntax {} -> Just s + StatementImport {} -> Just s + StatementAxiom {} -> Just s + StatementModule l -> Just (StatementModule (migrateFunctionSyntax l)) + StatementInductive {} -> Just s + StatementOpenModule {} -> Just s + StatementFunctionDef {} -> Just s + StatementFunctionClause {} -> Nothing + StatementTypeSignature sig -> Just (StatementFunctionDef (mkFunctionDef sig (getClauses (sig ^. sigName)))) + + ss' :: [Statement 'Scoped] + ss' = m ^. moduleBody + + mkFunctionDef :: TypeSignature 'Scoped -> [FunctionClause 'Scoped] -> FunctionDef 'Scoped + mkFunctionDef sig cls = + FunctionDef + { _signName = sig ^. sigName, + _signColonKw = sig ^. sigColonKw, + _signRetType = sig ^. sigType, + _signDoc = sig ^. sigDoc, + _signPragmas = sig ^. sigPragmas, + _signTerminating = sig ^. sigTerminating, + _signBuiltin = sig ^. sigBuiltin, + _signArgs = [], + _signBody = case sig ^. sigBody of + Just e -> SigBodyExpression e + Nothing -> case cls of + [] -> impossible + [c] + | null (c ^. clausePatterns) -> SigBodyExpression (c ^. clauseBody) + | otherwise -> SigBodyClauses (pure (mkClause c)) + c : cs -> SigBodyClauses (mkClause <$> c :| cs) + } + where + mkClause :: FunctionClause 'Scoped -> NewFunctionClause 'Scoped + mkClause c = + NewFunctionClause + { _clausenPipeKw = Irrelevant (KeywordRef kwPipe (getLoc (c ^. clauseOwnerFunction)) Ascii), + _clausenAssignKw = c ^. clauseAssignKw, + _clausenBody = c ^. clauseBody, + _clausenPatterns = nonEmpty' (c ^. clausePatterns) + } + getClauses :: S.Symbol -> [FunctionClause 'Scoped] + getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction] diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 92fb43ed3a..8e64a762d1 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -132,9 +132,41 @@ type ParsedIteratorAttribs = WithLoc (WithSource IteratorAttribs) -- Top level statement -------------------------------------------------------------------------------- +-- | We group consecutive definitions and reserve symbols in advance, so that we +-- don't need extra syntax for mutually recursive definitions. Also, it allows +-- us to be more flexible with the ordering of the definitions. +data StatementSections (s :: Stage) + = SectionsDefinitions (DefinitionsSection s) + | SectionsNonDefinitions (NonDefinitionsSection s) + | SectionsEmpty + +data DefinitionsSection (s :: Stage) = DefinitionsSection + { _definitionsSection :: NonEmpty (Definition s), + _definitionsNext :: Maybe (NonDefinitionsSection s) + } + +data NonDefinitionsSection (s :: Stage) = NonDefinitionsSection + { _nonDefinitionsSection :: NonEmpty (NonDefinition s), + _nonDefinitionsNext :: Maybe (DefinitionsSection s) + } + +data Definition (s :: Stage) + = DefinitionSyntax SyntaxDef + | DefinitionFunctionDef (FunctionDef s) + | DefinitionInductive (InductiveDef s) + | DefinitionAxiom (AxiomDef s) + | DefinitionTypeSignature (TypeSignature s) + +data NonDefinition (s :: Stage) + = NonDefinitionImport (Import s) + | NonDefinitionModule (Module s 'ModuleLocal) + | NonDefinitionFunctionClause (FunctionClause s) + | NonDefinitionOpenModule (OpenModule s) + data Statement (s :: Stage) = StatementSyntax SyntaxDef | StatementTypeSignature (TypeSignature s) + | StatementFunctionDef (FunctionDef s) | StatementImport (Import s) | StatementInductive (InductiveDef s) | StatementModule (Module s 'ModuleLocal) @@ -242,6 +274,124 @@ instance HasLoc IteratorSyntaxDef where -- Type signature declaration ------------------------------------------------------------------------------- +data SigArg (s :: Stage) = SigArg + { _sigArgDelims :: Irrelevant (KeywordRef, KeywordRef), + _sigArgImplicit :: IsImplicit, + _sigArgColon :: Irrelevant KeywordRef, + _sigArgNames :: NonEmpty (SymbolType s), + _sigArgType :: ExpressionType s + } + +deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (SigArg s) + +deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (SigArg s) + +deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (SigArg s) + +data NewFunctionClause (s :: Stage) = NewFunctionClause + { _clausenPipeKw :: Irrelevant KeywordRef, + _clausenPatterns :: NonEmpty (PatternAtomType s), + _clausenAssignKw :: Irrelevant KeywordRef, + _clausenBody :: ExpressionType s + } + +deriving stock instance + ( Show (PatternAtomType s), + Show (IdentifierType s), + Show (ModuleRefType s), + Show (SymbolType s), + Show (ExpressionType s) + ) => + Show (NewFunctionClause s) + +deriving stock instance + ( Eq (PatternAtomType s), + Eq (IdentifierType s), + Eq (ModuleRefType s), + Eq (SymbolType s), + Eq (ExpressionType s) + ) => + Eq (NewFunctionClause s) + +deriving stock instance + ( Ord (PatternAtomType s), + Ord (IdentifierType s), + Ord (ModuleRefType s), + Ord (SymbolType s), + Ord (ExpressionType s) + ) => + Ord (NewFunctionClause s) + +data FunctionDefBody (s :: Stage) + = SigBodyExpression (ExpressionType s) + | SigBodyClauses (NonEmpty (NewFunctionClause s)) + +deriving stock instance + ( Show (PatternAtomType s), + Show (IdentifierType s), + Show (ModuleRefType s), + Show (SymbolType s), + Show (ExpressionType s) + ) => + Show (FunctionDefBody s) + +deriving stock instance + ( Eq (PatternAtomType s), + Eq (IdentifierType s), + Eq (ModuleRefType s), + Eq (SymbolType s), + Eq (ExpressionType s) + ) => + Eq (FunctionDefBody s) + +deriving stock instance + ( Ord (PatternAtomType s), + Ord (IdentifierType s), + Ord (ModuleRefType s), + Ord (SymbolType s), + Ord (ExpressionType s) + ) => + Ord (FunctionDefBody s) + +data FunctionDef (s :: Stage) = FunctionDef + { _signName :: FunctionName s, + _signArgs :: [SigArg s], + _signColonKw :: Irrelevant KeywordRef, + _signRetType :: ExpressionType s, + _signDoc :: Maybe (Judoc s), + _signPragmas :: Maybe ParsedPragmas, + _signBuiltin :: Maybe (WithLoc BuiltinFunction), + _signBody :: FunctionDefBody s, + _signTerminating :: Maybe KeywordRef + } + +deriving stock instance + ( Show (PatternAtomType s), + Show (IdentifierType s), + Show (ModuleRefType s), + Show (SymbolType s), + Show (ExpressionType s) + ) => + Show (FunctionDef s) + +deriving stock instance + ( Eq (PatternAtomType s), + Eq (IdentifierType s), + Eq (ModuleRefType s), + Eq (SymbolType s), + Eq (ExpressionType s) + ) => + Eq (FunctionDef s) + +deriving stock instance + ( Ord (PatternAtomType s), + Ord (IdentifierType s), + Ord (ModuleRefType s), + Ord (SymbolType s), + Ord (ExpressionType s) + ) => + Ord (FunctionDef s) + data TypeSignature (s :: Stage) = TypeSignature { _sigName :: FunctionName s, _sigColonKw :: Irrelevant KeywordRef, @@ -345,22 +495,22 @@ data PatternApp = PatternApp data PatternInfixApp = PatternInfixApp { _patInfixLeft :: PatternArg, - _patInfixConstructor :: ConstructorRef, + _patInfixConstructor :: S.Name, _patInfixRight :: PatternArg } deriving stock (Show, Eq, Ord) instance HasFixity PatternInfixApp where - getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity) + getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. S.nameFixity) data PatternPostfixApp = PatternPostfixApp { _patPostfixParameter :: PatternArg, - _patPostfixConstructor :: ConstructorRef + _patPostfixConstructor :: S.Name } deriving stock (Show, Eq, Ord) instance HasFixity PatternPostfixApp where - getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity) + getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. S.nameFixity) data PatternArg = PatternArg { _patternArgIsImplicit :: IsImplicit, @@ -371,7 +521,7 @@ data PatternArg = PatternArg data Pattern = PatternVariable (SymbolType 'Scoped) - | PatternConstructor ConstructorRef + | PatternConstructor S.Name | PatternApplication PatternApp | PatternList (ListPattern 'Scoped) | PatternInfixApplication PatternInfixApp @@ -400,7 +550,7 @@ instance HasAtomicity Pattern where data PatternScopedIden = PatternScopedVar S.Symbol - | PatternScopedConstructor ConstructorRef + | PatternScopedConstructor S.Name deriving stock (Show, Ord, Eq) data PatternBinding = PatternBinding @@ -682,10 +832,10 @@ instance (Show (RefNameType s)) => Show (ModuleRef'' s t) where show ModuleRef'' {..} = show _moduleRefName data SymbolEntry - = EntryAxiom (AxiomRef' 'S.NotConcrete) - | EntryInductive (InductiveRef' 'S.NotConcrete) - | EntryFunction (FunctionRef' 'S.NotConcrete) - | EntryConstructor (ConstructorRef' 'S.NotConcrete) + = EntryAxiom (RefNameType 'S.NotConcrete) + | EntryInductive (RefNameType 'S.NotConcrete) + | EntryFunction (RefNameType 'S.NotConcrete) + | EntryConstructor (RefNameType 'S.NotConcrete) | EntryModule (ModuleRef' 'S.NotConcrete) | EntryVariable (S.Name' ()) deriving stock (Show) @@ -745,11 +895,11 @@ deriving stock instance type ScopedIden = ScopedIden' 'S.Concrete data ScopedIden' (n :: S.IsConcrete) - = ScopedAxiom (AxiomRef' n) - | ScopedInductive (InductiveRef' n) + = ScopedAxiom (RefNameType n) + | ScopedInductive (RefNameType n) | ScopedVar S.Symbol - | ScopedFunction (FunctionRef' n) - | ScopedConstructor (ConstructorRef' n) + | ScopedFunction (RefNameType n) + | ScopedConstructor (RefNameType n) deriving stock instance (Eq (RefNameType s)) => Eq (ScopedIden' s) @@ -762,16 +912,16 @@ deriving stock instance identifierName :: forall n. (SingI n) => ScopedIden' n -> RefNameType n identifierName = \case - ScopedAxiom a -> a ^. axiomRefName - ScopedInductive i -> i ^. inductiveRefName + ScopedAxiom a -> a + ScopedInductive i -> i ScopedVar v -> ( case sing :: S.SIsConcrete n of S.SConcrete -> id S.SNotConcrete -> set S.nameConcrete () ) (unqualifiedSymbol v) - ScopedFunction f -> f ^. functionRefName - ScopedConstructor c -> c ^. constructorRefName + ScopedFunction f -> f + ScopedConstructor c -> c data Expression = ExpressionIdentifier ScopedIden @@ -1273,6 +1423,7 @@ makeLenses ''IteratorSyntaxDef makeLenses ''InductiveConstructorDef makeLenses ''Module makeLenses ''TypeSignature +makeLenses ''FunctionDef makeLenses ''AxiomDef makeLenses ''FunctionClause makeLenses ''InductiveParameters @@ -1428,6 +1579,7 @@ instance HasLoc (Statement 'Scoped) where getLoc = \case StatementSyntax t -> getLoc t StatementTypeSignature t -> getLoc t + StatementFunctionDef t -> getLoc t StatementImport t -> getLoc t StatementInductive t -> getLoc t StatementModule t -> getLoc t @@ -1531,13 +1683,38 @@ getLocExpressionType = case sing :: SStage s of SParsed -> getLoc SScoped -> getLoc +instance HasLoc (SigArg s) where + getLoc SigArg {..} = getLoc l <> getLoc r + where + Irrelevant (l, r) = _sigArgDelims + +instance SingI s => HasLoc (NewFunctionClause s) where + getLoc NewFunctionClause {..} = + getLoc _clausenPipeKw + <> getLocExpressionType _clausenBody + +instance SingI s => HasLoc (FunctionDefBody s) where + getLoc = \case + SigBodyExpression e -> getLocExpressionType e + SigBodyClauses cl -> getLocSpan cl + +instance SingI s => HasLoc (FunctionDef s) where + getLoc FunctionDef {..} = + (getLoc <$> _signDoc) + ?<> (getLoc <$> _signPragmas) + ?<> (getLoc <$> _signBuiltin) + ?<> (getLoc <$> _signTerminating) + ?<> getLocSymbolType _signName + <> getLoc _signBody + instance SingI s => HasLoc (TypeSignature s) where getLoc TypeSignature {..} = (getLoc <$> _sigDoc) ?<> (getLoc <$> _sigPragmas) ?<> (getLoc <$> _sigBuiltin) ?<> (getLoc <$> _sigTerminating) - ?<> (getLocExpressionType <$> _sigBody) + ?<> getLocSymbolType _sigName + <> (getLocExpressionType <$> _sigBody) ?<> getLocExpressionType _sigType instance HasLoc (Example s) where @@ -1771,7 +1948,7 @@ instance IsApe PatternInfixApp ApeLeaf where { _infixFixity = getFixity i, _infixLeft = toApe l, _infixRight = toApe r, - _infixIsDelimiter = isDelimiterStr (prettyText (op ^. constructorRefName . S.nameConcrete)), + _infixIsDelimiter = isDelimiterStr (prettyText (op ^. S.nameConcrete)), _infixOp = ApeLeafPattern (PatternConstructor op) } @@ -1847,18 +2024,18 @@ instance HasAtomicity PatternArg where idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden idenOverName f = \case - ScopedAxiom a -> ScopedAxiom (over axiomRefName f a) - ScopedInductive i -> ScopedInductive (over inductiveRefName f i) + ScopedAxiom a -> ScopedAxiom (f a) + ScopedInductive i -> ScopedInductive (f i) ScopedVar v -> ScopedVar (f v) - ScopedFunction fun -> ScopedFunction (over functionRefName f fun) - ScopedConstructor c -> ScopedConstructor (over constructorRefName f c) + ScopedFunction fun -> ScopedFunction (f fun) + ScopedConstructor c -> ScopedConstructor (f c) entryPrism :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> (S.Name' (), SymbolEntry) entryPrism f = \case - EntryAxiom a -> (a ^. axiomRefName, EntryAxiom (over axiomRefName f a)) - EntryInductive i -> (i ^. inductiveRefName, EntryInductive (over inductiveRefName f i)) - EntryFunction fun -> (fun ^. functionRefName, EntryFunction (over functionRefName f fun)) - EntryConstructor c -> (c ^. constructorRefName, EntryConstructor (over constructorRefName f c)) + EntryAxiom a -> (a, EntryAxiom (f a)) + EntryInductive i -> (i, EntryInductive (f i)) + EntryFunction fun -> (fun, EntryFunction (f fun)) + EntryConstructor c -> (c, EntryConstructor (f c)) EntryModule m -> (getModuleRefNameType m, EntryModule (overModuleRef'' (over moduleRefName f) m)) EntryVariable m -> (m, EntryVariable (f m)) @@ -1904,10 +2081,10 @@ symbolEntryNameId = (^. S.nameId) . symbolEntryToSName symbolEntryToSName :: SymbolEntry -> S.Name' () symbolEntryToSName = \case - EntryAxiom a -> a ^. axiomRefName - EntryInductive i -> i ^. inductiveRefName - EntryFunction f -> f ^. functionRefName - EntryConstructor c -> c ^. constructorRefName + EntryAxiom a -> a + EntryInductive i -> i + EntryFunction f -> f + EntryConstructor c -> c EntryModule m -> getModuleRefNameType m EntryVariable m -> m diff --git a/src/Juvix/Compiler/Concrete/Pretty.hs b/src/Juvix/Compiler/Concrete/Pretty.hs index be3240a3fc..b67338bd34 100644 --- a/src/Juvix/Compiler/Concrete/Pretty.hs +++ b/src/Juvix/Compiler/Concrete/Pretty.hs @@ -11,11 +11,11 @@ import Juvix.Compiler.Concrete.Print qualified as Print import Juvix.Data.PPOutput import Juvix.Prelude -ppOutDefault :: (PrettyPrint c, HasLoc c) => c -> AnsiText +ppOutDefault :: PrettyPrint c => c -> AnsiText ppOutDefault = Print.ppOutNoComments defaultOptions -ppOut :: (HasLoc c, CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText +ppOut :: (CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText ppOut = Print.ppOutNoComments -ppTrace :: (HasLoc c, PrettyPrint c) => c -> Text +ppTrace :: PrettyPrint c => c -> Text ppTrace = toAnsiText True . ppOut traceOptions diff --git a/src/Juvix/Compiler/Concrete/Print.hs b/src/Juvix/Compiler/Concrete/Print.hs index 0e43ace8b4..b4edb49618 100644 --- a/src/Juvix/Compiler/Concrete/Print.hs +++ b/src/Juvix/Compiler/Concrete/Print.hs @@ -17,5 +17,5 @@ ppOutDefault cs = mkAnsiText . PPOutput . doc defaultOptions cs ppOut :: (CanonicalProjection a Options, PrettyPrint c, HasLoc c) => a -> Comments -> c -> AnsiText ppOut o cs = mkAnsiText . PPOutput . doc (project o) cs -ppOutNoComments :: (CanonicalProjection a Options, PrettyPrint c, HasLoc c) => a -> c -> AnsiText -ppOutNoComments o = mkAnsiText . PPOutput . doc (project o) emptyComments +ppOutNoComments :: (CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText +ppOutNoComments o = mkAnsiText . PPOutput . docNoLoc (project o) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 37866890a7..8d5f065d9c 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -57,6 +57,9 @@ docHelper cs opts x = . ppCode $ x +docNoLoc :: PrettyPrint c => Options -> c -> Doc Ann +docNoLoc opts x = docHelper Nothing opts x + doc :: (PrettyPrint c, HasLoc c) => Options -> Comments -> c -> Doc Ann doc opts cs x = docHelper (Just (fileComments file cs)) opts x where @@ -113,8 +116,8 @@ ppExpressionType = case sing :: SStage s of ppPatternAtomType :: forall s. SingI s => PrettyPrinting (PatternAtomType s) ppPatternAtomType = case sing :: SStage s of - SParsed -> ppCode - SScoped -> ppCode + SParsed -> ppCodeAtom + SScoped -> ppCodeAtom ppPatternParensType :: forall s. SingI s => PrettyPrinting (PatternParensType s) ppPatternParensType = case sing :: SStage s of @@ -190,12 +193,13 @@ instance SingI s => PrettyPrint (Iterator s) where instance PrettyPrint S.AName where ppCode (S.AName n) = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.nameVerbatim))) --- TODO print without spaces when the type signature is not next to the clauses instance PrettyPrint FunctionInfo where - ppCode f = do - let ty = StatementTypeSignature (f ^. functionInfoType) - cs = map StatementFunctionClause (f ^. functionInfoClauses) - ppCode (ty : cs) + ppCode = \case + FunctionInfoOld f -> do + let ty = StatementTypeSignature (f ^. oldFunctionInfoType) + cs = map StatementFunctionClause (f ^. oldFunctionInfoClauses) + ppStatements (ty : cs) + FunctionInfoNew f -> ppCode f instance SingI s => PrettyPrint (List s) where ppCode List {..} = do @@ -242,7 +246,7 @@ instance PrettyPrint S.NameId where instance (SingI t, SingI s) => PrettyPrint (Module s t) where ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Module s t -> Sem r () ppCode Module {..} = do - let moduleBody' = localIndent (ppCode _moduleBody) + let moduleBody' = localIndent (ppStatements _moduleBody) modulePath' = ppModulePathType _modulePath moduleDoc' = whenJust _moduleDoc ppCode modulePragmas' = whenJust _modulePragmas ppCode @@ -276,12 +280,16 @@ instance (SingI t, SingI s) => PrettyPrint (Module s t) where SModuleLocal -> ppCode _moduleKwEnd SModuleTop -> end -instance SingI s => PrettyPrint [Statement s] where - ppCode :: forall r. Members '[ExactPrint, Reader Options] r => [Statement s] -> Sem r () - ppCode ss = paragraphs (ppGroup <$> Concrete.groupStatements ss) - where - ppGroup :: NonEmpty (Statement s) -> Sem r () - ppGroup = vsep . sepEndSemicolon . fmap ppCode +instance PrettyPrint a => PrettyPrint [a] where + ppCode x = do + let cs = map ppCode (toList x) + encloseSep (ppCode @Text "[") (ppCode @Text "]") (ppCode @Text ", ") cs + +ppStatements :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => [Statement s] -> Sem r () +ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements ss) + where + ppGroup :: NonEmpty (Statement s) -> Sem r () + ppGroup = vsep . sepEndSemicolon . fmap ppCode instance PrettyPrint TopModulePath where ppCode TopModulePath {..} = @@ -310,18 +318,6 @@ instance PrettyPrint QualifiedName where instance PrettyPrint (ModuleRef'' 'S.Concrete 'ModuleTop) where ppCode m = ppCode (m ^. moduleRefName) -instance PrettyPrint AxiomRef where - ppCode a = ppCode (a ^. axiomRefName) - -instance PrettyPrint InductiveRef where - ppCode a = ppCode (a ^. inductiveRefName) - -instance PrettyPrint FunctionRef where - ppCode a = ppCode (a ^. functionRefName) - -instance PrettyPrint ConstructorRef where - ppCode a = ppCode (a ^. constructorRefName) - instance PrettyPrint ScopedIden where ppCode = \case ScopedAxiom a -> ppCode a @@ -645,6 +641,45 @@ instance PrettyPrint BuiltinFunction where instance PrettyPrint BuiltinAxiom where ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i) +instance SingI s => PrettyPrint (NewFunctionClause s) where + ppCode :: forall r. Members '[ExactPrint, Reader Options] r => NewFunctionClause s -> Sem r () + ppCode NewFunctionClause {..} = do + let pats' = hsep (ppPatternAtomType <$> _clausenPatterns) + e' = ppExpressionType _clausenBody + ppCode _clausenPipeKw <+> pats' <+> ppCode _clausenAssignKw <> oneLineOrNext e' + +instance SingI s => PrettyPrint (SigArg s) where + ppCode :: Members '[ExactPrint, Reader Options] r => SigArg s -> Sem r () + ppCode SigArg {..} = do + let Irrelevant (l, r) = _sigArgDelims + names' = hsep (ppSymbolType <$> _sigArgNames) + colon' = ppCode _sigArgColon + ty' = ppExpressionType _sigArgType + ppCode l <> names' <+> colon' <+> ty' <> ppCode r + +instance SingI s => PrettyPrint (FunctionDef s) where + ppCode :: forall r. Members '[ExactPrint, Reader Options] r => FunctionDef s -> Sem r () + ppCode FunctionDef {..} = do + let termin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _signTerminating + doc' :: Maybe (Sem r ()) = ppCode <$> _signDoc + pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas + args' = hsep . fmap ppCode <$> nonEmpty _signArgs + builtin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _signBuiltin + type' = oneLineOrNext (ppCode _signColonKw <+> ppExpressionType _signRetType) + name' = annDef _signName (ppSymbolType _signName) + body' = case _signBody of + SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppExpressionType e) + SigBodyClauses k -> line <> indent (vsep (ppCode <$> k)) + doc' + ?<> pragmas' + ?<> builtin' + ?<> termin' + ?<> ( name' + <+?> args' + <> type' + <> body' + ) + instance SingI s => PrettyPrint (TypeSignature s) where ppCode :: forall r. Members '[ExactPrint, Reader Options] r => TypeSignature s -> Sem r () ppCode TypeSignature {..} = do @@ -851,6 +886,7 @@ instance SingI s => PrettyPrint (Statement s) where ppCode = \case StatementSyntax s -> ppCode s StatementTypeSignature s -> ppCode s + StatementFunctionDef 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 b142e31b64..2c73e5ad6b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -18,6 +18,7 @@ import Juvix.Compiler.Concrete.Data.Scope import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra qualified as P import Juvix.Compiler.Concrete.Language +import Juvix.Compiler.Concrete.Pretty (ppTrace) import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context (ParserResult) @@ -127,7 +128,7 @@ freshVariable = freshSymbol S.KNameLocal freshSymbol :: forall r. - (Members '[State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r) => + Members '[State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r => S.NameKind -> Symbol -> Sem r S.Symbol @@ -165,13 +166,36 @@ freshSymbol _nameKind _nameConcrete = do reserveSymbolOf :: forall r. - (Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState] r) => + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r => S.NameKind -> Symbol -> Sem r S.Symbol reserveSymbolOf k s = do checkNotBound - freshSymbol k s + s' <- freshSymbol k s + path <- gets (^. scopePath) + strat <- ask + modify (set (scopeLocalSymbols . at s) (Just s')) + let c = S.unConcrete s' + mentry :: Maybe SymbolEntry + mentry = case k of + S.KNameConstructor -> Just (EntryConstructor c) + S.KNameInductive -> Just (EntryInductive c) + S.KNameFunction -> Just (EntryFunction c) + S.KNameAxiom -> Just (EntryAxiom c) + S.KNameLocal -> Just (EntryVariable c) + S.KNameLocalModule -> Nothing + S.KNameTopModule -> Nothing + addS :: SymbolEntry -> Maybe SymbolInfo -> SymbolInfo + addS entry m = case m of + Nothing -> symbolInfoSingle entry + Just SymbolInfo {..} -> case strat of + BindingLocal -> symbolInfoSingle entry + BindingTop -> SymbolInfo (HashMap.insert path entry _symbolInfo) + whenJust mentry $ \entry -> + modify (over scopeSymbols (HashMap.alter (Just . addS entry) s)) + + return s' where checkNotBound :: Sem r () checkNotBound = do @@ -185,12 +209,16 @@ reserveSymbolOf k s = do } ) -bindReservedSymbol :: Members '[State Scope, InfoTableBuilder, Reader BindingStrategy] r => S.Symbol -> SymbolEntry -> Sem r () +bindReservedSymbol :: + Members '[State Scope, InfoTableBuilder, Reader BindingStrategy] r => + S.Symbol -> + SymbolEntry -> + Sem r () bindReservedSymbol s' entry = do path <- gets (^. scopePath) strat <- ask + -- TODO only modules are meant to be stored here? modify (over scopeSymbols (HashMap.alter (Just . addS strat path) s)) - modify (set (scopeLocalSymbols . at s) (Just s')) registerName (S.unqualifiedSymbol s') where s :: Symbol @@ -203,7 +231,7 @@ bindReservedSymbol s' entry = do BindingTop -> SymbolInfo (HashMap.insert path entry _symbolInfo) bindSymbolOf :: - (Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r) => + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => S.NameKind -> (S.Name' () -> SymbolEntry) -> Symbol -> @@ -213,42 +241,79 @@ bindSymbolOf k mkEntry s = do bindReservedSymbol s' (mkEntry (S.unConcrete s')) return s' +bindReservedDefinitionSymbol :: + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => + (S.Name' () -> SymbolEntry) -> + Symbol -> + Sem r S.Symbol +bindReservedDefinitionSymbol mkEntry s = do + m <- gets (^. scopeLocalSymbols) + let s' = fromMaybe err (m ^. at s) + err = error ("impossible. Contents of scope:\n" <> ppTrace (toList m)) + bindReservedSymbol s' (mkEntry (S.unConcrete s')) + return s' + ignoreFixities :: Sem (State ScoperFixities ': r) a -> Sem r a ignoreFixities = evalState mempty ignoreIterators :: Sem (State ScoperIterators ': r) a -> Sem r a ignoreIterators = evalState mempty --- variables are assumed to never be infix operators +-- | variables are assumed to never be infix operators bindVariableSymbol :: Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, State ScoperState] r => Symbol -> Sem r S.Symbol bindVariableSymbol = localBindings . ignoreFixities . ignoreIterators . bindSymbolOf S.KNameLocal EntryVariable +reserveInductiveSymbol :: + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r => + Symbol -> + Sem r S.Symbol +reserveInductiveSymbol = reserveSymbolOf S.KNameInductive + +reserveConstructorSymbol :: + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r => + Symbol -> + Sem r S.Symbol +reserveConstructorSymbol = reserveSymbolOf S.KNameConstructor + +reserveFunctionSymbol :: + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r => + Symbol -> + Sem r S.Symbol +reserveFunctionSymbol = reserveSymbolOf S.KNameFunction + +reserveAxiomSymbol :: + Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r => + Symbol -> + Sem r S.Symbol +reserveAxiomSymbol = reserveSymbolOf S.KNameAxiom + +-- | symbols must be reserved in advance bindFunctionSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => Symbol -> Sem r S.Symbol -bindFunctionSymbol = bindSymbolOf S.KNameFunction (EntryFunction . FunctionRef') +bindFunctionSymbol = bindReservedDefinitionSymbol EntryFunction bindInductiveSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => Symbol -> Sem r S.Symbol -bindInductiveSymbol = bindSymbolOf S.KNameInductive (EntryInductive . InductiveRef') +bindInductiveSymbol = bindReservedDefinitionSymbol EntryInductive bindAxiomSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => Symbol -> Sem r S.Symbol -bindAxiomSymbol = bindSymbolOf S.KNameAxiom (EntryAxiom . AxiomRef') +bindAxiomSymbol = bindReservedDefinitionSymbol EntryAxiom bindConstructorSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => Symbol -> Sem r S.Symbol -bindConstructorSymbol = bindSymbolOf S.KNameConstructor (EntryConstructor . ConstructorRef') +bindConstructorSymbol = bindReservedDefinitionSymbol EntryConstructor bindLocalModuleSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r => @@ -419,13 +484,13 @@ entryToScopedIden name e = do scopedName = set S.nameConcrete name (entryName e) registerName scopedName return $ case e of - EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref) + EntryAxiom ref -> ScopedAxiom (set S.nameConcrete name ref) EntryInductive ref -> - ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref) + ScopedInductive (set S.nameConcrete name ref) EntryConstructor ref -> - ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref) + ScopedConstructor (set S.nameConcrete name ref) EntryFunction ref -> - ScopedFunction (set (functionRefName . S.nameConcrete) name ref) + ScopedFunction (set S.nameConcrete name ref) EntryVariable v -> case name of NameQualified {} -> impossible NameUnqualified uname -> ScopedVar (set S.nameConcrete uname v) @@ -514,8 +579,59 @@ checkIteratorSyntaxDef s@IteratorSyntaxDef {..} = do (@$>) :: Functor m => (a -> m ()) -> a -> m a (@$>) f a = f a $> a +checkFunctionDef :: + forall r. + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r => + FunctionDef 'Parsed -> + Sem r (FunctionDef 'Scoped) +checkFunctionDef FunctionDef {..} = do + sigName' <- bindFunctionSymbol _signName + sigDoc' <- mapM checkJudoc _signDoc + (args', sigType', sigBody') <- withLocalScope $ do + a' <- mapM checkArg _signArgs + t' <- checkParseExpressionAtoms _signRetType + b' <- checkBody + return (a', t', b') + registerFunctionDef + @$> FunctionDef + { _signName = sigName', + _signRetType = sigType', + _signDoc = sigDoc', + _signBody = sigBody', + _signArgs = args', + .. + } + where + checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped) + checkArg SigArg {..} = do + names' <- mapM bindVariableSymbol _sigArgNames + ty' <- checkParseExpressionAtoms _sigArgType + return + SigArg + { _sigArgNames = names', + _sigArgType = ty', + .. + } + checkBody :: Sem r (FunctionDefBody 'Scoped) + checkBody = case _signBody of + SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e + SigBodyClauses cls -> SigBodyClauses <$> mapM checkClause cls + checkClause :: NewFunctionClause 'Parsed -> Sem r (NewFunctionClause 'Scoped) + checkClause NewFunctionClause {..} = do + (patterns', body') <- withLocalScope $ do + p <- mapM checkParsePatternAtom _clausenPatterns + b <- checkParseExpressionAtoms _clausenBody + return (p, b) + return + NewFunctionClause + { _clausenBody = body', + _clausenPatterns = patterns', + _clausenPipeKw, + _clausenAssignKw + } + checkTypeSignature :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r => TypeSignature 'Parsed -> Sem r (TypeSignature 'Scoped) checkTypeSignature TypeSignature {..} = do @@ -534,7 +650,7 @@ checkTypeSignature TypeSignature {..} = do checkInductiveParameters :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => InductiveParameters 'Parsed -> Sem r (InductiveParameters 'Scoped) checkInductiveParameters params = do @@ -544,16 +660,24 @@ checkInductiveParameters params = do checkInductiveDef :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, Reader BindingStrategy] r => InductiveDef 'Parsed -> Sem r (InductiveDef 'Scoped) checkInductiveDef InductiveDef {..} = do - inductiveName' <- topBindings (bindInductiveSymbol _inductiveName) + (inductiveName', constructorNames' :: NonEmpty S.Symbol) <- topBindings $ do + i <- bindInductiveSymbol _inductiveName + cs <- mapM (bindConstructorSymbol . (^. constructorName)) _inductiveConstructors + return (i, cs) (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') <- withLocalScope $ do inductiveParameters' <- mapM checkInductiveParameters _inductiveParameters inductiveType' <- mapM checkParseExpressionAtoms _inductiveType inductiveDoc' <- mapM checkJudoc _inductiveDoc - inductiveConstructors' <- mapM (checkConstructorDef inductiveName') _inductiveConstructors + inductiveConstructors' <- + nonEmpty' + <$> sequence + [ checkConstructorDef inductiveName' cname cdef + | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors) + ] return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') forM_ inductiveConstructors' bindConstructor registerInductive @@ -576,15 +700,13 @@ checkInductiveDef InductiveDef {..} = do bindReservedSymbol (d ^. constructorName) ( EntryConstructor - ( ConstructorRef' - (S.unConcrete (d ^. constructorName)) + ( S.unConcrete (d ^. constructorName) ) ) -- note that the constructor name is not bound here - checkConstructorDef :: S.Symbol -> InductiveConstructorDef 'Parsed -> Sem r (InductiveConstructorDef 'Scoped) - checkConstructorDef tyName InductiveConstructorDef {..} = do + checkConstructorDef :: S.Symbol -> S.Symbol -> InductiveConstructorDef 'Parsed -> Sem r (InductiveConstructorDef 'Scoped) + checkConstructorDef tyName constructorName' InductiveConstructorDef {..} = do constructorType' <- checkParseExpressionAtoms _constructorType - constructorName' <- reserveSymbolOf S.KNameConstructor _constructorName doc' <- mapM checkJudoc _constructorDoc registerConstructor tyName @$> InductiveConstructorDef @@ -601,10 +723,10 @@ createExportsTable ei = foldr (HashSet.insert . getNameId) HashSet.empty (HashMa where getNameId :: SymbolEntry -> NameId getNameId = \case - EntryAxiom r -> getNameRefId (r ^. axiomRefName) - EntryInductive r -> getNameRefId (r ^. inductiveRefName) - EntryFunction r -> getNameRefId (r ^. functionRefName) - EntryConstructor r -> getNameRefId (r ^. constructorRefName) + EntryAxiom r -> getNameRefId r + EntryInductive r -> getNameRefId r + EntryFunction r -> getNameRefId r + EntryConstructor r -> getNameRefId r EntryModule r -> getModuleRefNameId r EntryVariable v -> v ^. S.nameId @@ -723,13 +845,180 @@ checkModuleBody :: [Statement 'Parsed] -> Sem r (ExportInfo, [Statement 'Scoped]) checkModuleBody body = do - body' <- fixitiesBlock (iteratorsBlock (mapM checkStatement body)) + body' <- + fmap flattenSections + . fixitiesBlock + . iteratorsBlock + $ checkSections (mkSections body) exported <- get >>= exportScope return (exported, body') + where + flattenSections :: forall s. StatementSections s -> [Statement s] + flattenSections s = run . execOutputList $ case s of + SectionsEmpty -> return () + SectionsNonDefinitions n -> goNonDefinitions n + SectionsDefinitions n -> goDefinitions n + where + goNonDefinitions :: forall t. Members '[Output (Statement s)] t => NonDefinitionsSection s -> Sem t () + goNonDefinitions NonDefinitionsSection {..} = do + mapM_ go _nonDefinitionsSection + whenJust _nonDefinitionsNext goDefinitions + where + go :: NonDefinition s -> Sem t () + go = \case + NonDefinitionImport d -> output (StatementImport d) + NonDefinitionModule d -> output (StatementModule d) + NonDefinitionFunctionClause d -> output (StatementFunctionClause d) + NonDefinitionOpenModule d -> output (StatementOpenModule d) + + goDefinitions :: forall t. Members '[Output (Statement s)] t => DefinitionsSection s -> Sem t () + goDefinitions DefinitionsSection {..} = do + mapM_ go _definitionsSection + whenJust _definitionsNext goNonDefinitions + where + go :: Definition s -> Sem t () + go = \case + DefinitionSyntax d -> output @(Statement s) (StatementSyntax d) + DefinitionAxiom d -> output (StatementAxiom d) + DefinitionFunctionDef d -> output @(Statement s) (StatementFunctionDef d) + DefinitionInductive d -> output @(Statement s) (StatementInductive d) + DefinitionTypeSignature d -> output @(Statement s) (StatementTypeSignature d) + +checkSections :: + forall r. + Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r => + StatementSections 'Parsed -> + Sem r (StatementSections 'Scoped) +checkSections sec = topBindings $ case sec of + SectionsEmpty -> return SectionsEmpty + SectionsDefinitions d -> SectionsDefinitions <$> goDefinitions d + SectionsNonDefinitions d -> SectionsNonDefinitions <$> goNonDefinitions d + where + goNonDefinitions :: NonDefinitionsSection 'Parsed -> Sem (Reader BindingStrategy ': r) (NonDefinitionsSection 'Scoped) + goNonDefinitions NonDefinitionsSection {..} = do + sec' <- mapM goNonDefinition _nonDefinitionsSection + next' <- mapM goDefinitions _nonDefinitionsNext + return + NonDefinitionsSection + { _nonDefinitionsNext = next', + _nonDefinitionsSection = sec' + } + where + goNonDefinition :: NonDefinition 'Parsed -> Sem (Reader BindingStrategy ': r) (NonDefinition 'Scoped) + goNonDefinition = \case + NonDefinitionModule m -> NonDefinitionModule <$> checkLocalModule m + NonDefinitionImport i -> NonDefinitionImport <$> checkImport i + NonDefinitionFunctionClause i -> NonDefinitionFunctionClause <$> checkFunctionClause i + NonDefinitionOpenModule i -> NonDefinitionOpenModule <$> checkOpenModule i + + goDefinitions :: DefinitionsSection 'Parsed -> Sem (Reader BindingStrategy ': r) (DefinitionsSection 'Scoped) + goDefinitions DefinitionsSection {..} = do + mapM_ reserveDefinition _definitionsSection + sec' <- mapM goDefinition _definitionsSection + next' <- mapM goNonDefinitions _definitionsNext + return + DefinitionsSection + { _definitionsNext = next', + _definitionsSection = sec' + } + where + reserveDefinition :: Definition 'Parsed -> Sem (Reader BindingStrategy ': r) () + reserveDefinition = \case + DefinitionSyntax s -> void (checkSyntaxDef s) + DefinitionFunctionDef d -> void (reserveFunctionSymbol (d ^. signName)) + DefinitionTypeSignature d -> void (reserveFunctionSymbol (d ^. sigName)) + DefinitionAxiom d -> void (reserveAxiomSymbol (d ^. axiomName)) + DefinitionInductive d -> do + void (reserveInductiveSymbol (d ^. inductiveName)) + mapM_ reserveConstructorSymbol (d ^.. inductiveConstructors . each . constructorName) + goDefinition :: Definition 'Parsed -> Sem (Reader BindingStrategy ': r) (Definition 'Scoped) + goDefinition = \case + DefinitionSyntax s -> return (DefinitionSyntax s) + DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d + DefinitionTypeSignature d -> DefinitionTypeSignature <$> checkTypeSignature d + DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d + DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d + +checkStatement :: + Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r => + Statement 'Parsed -> + Sem r (Statement 'Scoped) +checkStatement s = topBindings $ case s of + StatementSyntax synDef -> StatementSyntax <$> checkSyntaxDef synDef + StatementTypeSignature tySig -> StatementTypeSignature <$> checkTypeSignature tySig + StatementFunctionDef tySig -> StatementFunctionDef <$> checkFunctionDef tySig + StatementImport imp -> StatementImport <$> checkImport imp + StatementInductive dt -> StatementInductive <$> checkInductiveDef dt + StatementModule dt -> StatementModule <$> checkLocalModule dt + StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open + StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause + StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax + +mkLetSections :: [LetClause 'Parsed] -> StatementSections 'Parsed +mkLetSections = mkSections . map fromLetClause + where + fromLetClause :: LetClause 'Parsed -> Statement 'Parsed + fromLetClause = \case + LetTypeSig t -> StatementTypeSignature t + LetFunClause c -> StatementFunctionClause c + +mkSections :: [Statement 'Parsed] -> StatementSections 'Parsed +mkSections = \case + [] -> SectionsEmpty + h : hs -> case fromStatement h of + Left d -> SectionsDefinitions (goDefinitions (pure d) hs) + Right d -> SectionsNonDefinitions (goNonDefinitions (pure d) hs) + where + goDefinitions :: NonEmpty (Definition 'Parsed) -> [Statement 'Parsed] -> DefinitionsSection 'Parsed + goDefinitions acc = \case + s : ss -> case fromStatement s of + Left d -> goDefinitions (NonEmpty.cons d acc) ss + Right d -> + DefinitionsSection + { _definitionsSection = NonEmpty.reverse acc, + _definitionsNext = Just (goNonDefinitions (pure d) ss) + } + [] -> + DefinitionsSection + { _definitionsSection = NonEmpty.reverse acc, + _definitionsNext = Nothing + } + goNonDefinitions :: NonEmpty (NonDefinition 'Parsed) -> [Statement 'Parsed] -> NonDefinitionsSection 'Parsed + goNonDefinitions acc = \case + s : ss -> case fromStatement s of + Right d -> goNonDefinitions (NonEmpty.cons d acc) ss + Left d -> + NonDefinitionsSection + { _nonDefinitionsSection = NonEmpty.reverse acc, + _nonDefinitionsNext = Just (goDefinitions (pure d) ss) + } + [] -> + NonDefinitionsSection + { _nonDefinitionsSection = NonEmpty.reverse acc, + _nonDefinitionsNext = Nothing + } + fromStatement :: Statement 'Parsed -> Either (Definition 'Parsed) (NonDefinition 'Parsed) + fromStatement = \case + StatementAxiom a -> Left (DefinitionAxiom a) + StatementTypeSignature t -> Left (DefinitionTypeSignature t) + StatementFunctionDef n -> Left (DefinitionFunctionDef n) + StatementInductive i -> Left (DefinitionInductive i) + StatementSyntax s -> Left (DefinitionSyntax s) + StatementImport i -> Right (NonDefinitionImport i) + StatementModule m -> Right (NonDefinitionModule m) + StatementOpenModule o -> Right (NonDefinitionOpenModule o) + StatementFunctionClause c -> Right (NonDefinitionFunctionClause c) + +reserveLocalModuleSymbol :: + Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r => + Symbol -> + Sem r S.Symbol +reserveLocalModuleSymbol = + ignoreFixities . ignoreIterators . reserveSymbolOf S.KNameLocalModule checkLocalModule :: forall r. - (Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r) => + Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r => Module 'Parsed 'ModuleLocal -> Sem r (Module 'Scoped 'ModuleLocal) checkLocalModule Module {..} = do @@ -739,7 +1028,7 @@ checkLocalModule Module {..} = do (e, b) <- checkModuleBody _moduleBody doc' <- mapM checkJudoc _moduleDoc return (e, b, doc') - _modulePath' <- ignoreFixities (ignoreIterators (reserveSymbolOf S.KNameLocalModule _modulePath)) + _modulePath' <- reserveLocalModuleSymbol _modulePath let moduleId = _modulePath' ^. S.nameId _moduleRefName = S.unConcrete _modulePath' _moduleRefModule = @@ -997,7 +1286,7 @@ checkOpenModule op checkFunctionClause :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r => FunctionClause 'Parsed -> Sem r (FunctionClause 'Scoped) checkFunctionClause clause@FunctionClause {..} = do @@ -1027,7 +1316,7 @@ checkFunctionClause clause@FunctionClause {..} = do err = throw (ErrLacksTypeSig (LacksTypeSig clause)) checkAxiomDef :: - (Members '[InfoTableBuilder, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r) => + Members '[Reader ScopeParameters, InfoTableBuilder, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r => AxiomDef 'Parsed -> Sem r (AxiomDef 'Scoped) checkAxiomDef AxiomDef {..} = do @@ -1041,7 +1330,7 @@ entryToSymbol sentry csym = set S.nameConcrete csym (symbolEntryToSName sentry) checkFunction :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Function 'Parsed -> Sem r (Function 'Scoped) checkFunction f = do @@ -1058,14 +1347,47 @@ checkFunction f = do _funKw = f ^. funKw return Function {..} --- for now functions defined in let clauses cannot be infix operators -checkLetClause :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => - LetClause 'Parsed -> - Sem r (LetClause 'Scoped) -checkLetClause lc = localBindings . ignoreFixities . ignoreIterators $ case lc of - LetTypeSig t -> LetTypeSig <$> checkTypeSignature t - LetFunClause c -> LetFunClause <$> checkFunctionClause c +-- | for now functions defined in let clauses cannot be infix operators +checkLetClauses :: + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + NonEmpty (LetClause 'Parsed) -> + Sem r (NonEmpty (LetClause 'Scoped)) +checkLetClauses = + localBindings + . ignoreFixities + . ignoreIterators + . fmap fromSections + . checkSections + . mkLetSections + . toList + where + fromSections :: StatementSections s -> NonEmpty (LetClause s) + fromSections = \case + SectionsEmpty -> impossible + SectionsDefinitions d -> fromDefs d + SectionsNonDefinitions d -> fromNonDefs d + where + fromDefs :: DefinitionsSection s -> NonEmpty (LetClause s) + fromDefs DefinitionsSection {..} = + (fromDef <$> _definitionsSection) <>? (fromNonDefs <$> _definitionsNext) + where + fromDef :: Definition s -> LetClause s + fromDef = \case + DefinitionTypeSignature d -> LetTypeSig d + DefinitionFunctionDef {} -> impossible + DefinitionInductive {} -> impossible + DefinitionAxiom {} -> impossible + DefinitionSyntax {} -> impossible + fromNonDefs :: NonDefinitionsSection s -> NonEmpty (LetClause s) + fromNonDefs NonDefinitionsSection {..} = + (fromNonDef <$> _nonDefinitionsSection) <>? (fromDefs <$> _nonDefinitionsNext) + where + fromNonDef :: NonDefinition s -> LetClause s + fromNonDef = \case + NonDefinitionFunctionClause f -> LetFunClause f + NonDefinitionImport {} -> impossible + NonDefinitionModule {} -> impossible + NonDefinitionOpenModule {} -> impossible checkListPattern :: forall r. @@ -1080,7 +1402,7 @@ checkListPattern l = do checkList :: forall r. - Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => List 'Parsed -> Sem r (List 'Scoped) checkList l = do @@ -1091,12 +1413,11 @@ checkList l = do checkLet :: forall r. - Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Let 'Parsed -> Sem r (Let 'Scoped) checkLet Let {..} = withLocalScope $ do - -- local definitions should not stay in scope letClauses' <- checkLetClauses _letClauses letExpression' <- checkParseExpressionAtoms _letExpression return @@ -1106,13 +1427,10 @@ checkLet Let {..} = _letKw, _letInKw } - where - checkLetClauses :: NonEmpty (LetClause 'Parsed) -> Sem r (NonEmpty (LetClause 'Scoped)) - checkLetClauses = mapM checkLetClause checkCaseBranch :: forall r. - Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => CaseBranch 'Parsed -> Sem r (CaseBranch 'Scoped) checkCaseBranch CaseBranch {..} = withLocalScope $ do @@ -1133,7 +1451,7 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do (throw (ErrCaseBranchImplicitPattern (CaseBranchImplicitPattern p))) checkCase :: - Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Case 'Parsed -> Sem r (Case 'Scoped) checkCase Case {..} = do @@ -1148,7 +1466,7 @@ checkCase Case {..} = do } checkLambda :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Lambda 'Parsed -> Sem r (Lambda 'Scoped) checkLambda Lambda {..} = do @@ -1161,7 +1479,7 @@ checkLambda Lambda {..} = do } checkLambdaClause :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => LambdaClause 'Parsed -> Sem r (LambdaClause 'Scoped) checkLambdaClause LambdaClause {..} = withLocalScope $ do @@ -1187,13 +1505,13 @@ scopedVar s n = do scopedFunction :: (Members '[InfoTableBuilder] r) => - FunctionRef' 'S.NotConcrete -> + RefNameType 'S.NotConcrete -> Symbol -> - Sem r FunctionRef -scopedFunction (FunctionRef' fref) n = do + Sem r S.Name +scopedFunction fref n = do let scoped :: S.Name = set S.nameConcrete (NameUnqualified n) fref registerName scoped - return (FunctionRef' scoped) + return scoped checkUnqualified :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => @@ -1239,14 +1557,14 @@ resolveShadowing es = go [(e, entryName e ^. S.nameWhyInScope) | e <- es] checkPatternName :: forall r. - (Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder] r) => + Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder] r => Name -> Sem r PatternScopedIden checkPatternName n = do c <- getConstructorRef case c of Just constr -> do - registerName (constr ^. constructorRefName) + registerName constr return (PatternScopedConstructor constr) -- the symbol is a constructor Nothing -> PatternScopedVar <$> bindVariableSymbol sym -- the symbol is a variable where @@ -1254,16 +1572,16 @@ checkPatternName n = do NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s) NameUnqualified s -> ([], s) -- check whether the symbol is a constructor in scope - getConstructorRef :: Sem r (Maybe ConstructorRef) + getConstructorRef :: Sem r (Maybe S.Name) getConstructorRef = do entries <- mapMaybe getConstructor <$> lookupQualifiedSymbol (path, sym) case entries of [] -> case SymbolPath <$> nonEmpty path of Nothing -> return Nothing -- There is no constructor with such a name Just pth -> throw (ErrQualSymNotInScope (QualSymNotInScope (QualifiedName pth sym))) - [e] -> return (Just (set (constructorRefName . S.nameConcrete) n e)) -- There is one constructor with such a name + [e] -> return (Just (set S.nameConcrete n e)) -- There is one constructor with such a name es -> throw (ErrAmbiguousSym (AmbiguousSym n (map EntryConstructor es))) - getConstructor :: SymbolEntry -> Maybe (ConstructorRef' 'S.NotConcrete) + getConstructor :: SymbolEntry -> Maybe (RefNameType 'S.NotConcrete) getConstructor = \case EntryConstructor r -> Just r _ -> Nothing @@ -1313,7 +1631,7 @@ checkName n = case n of NameUnqualified s -> checkUnqualified s checkExpressionAtom :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => ExpressionAtom 'Parsed -> Sem r (ExpressionAtom 'Scoped) checkExpressionAtom e = case e of @@ -1332,7 +1650,7 @@ checkExpressionAtom e = case e of AtomIterator i -> AtomIterator <$> checkIterator i checkIterator :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Iterator 'Parsed -> Sem r (Iterator 'Scoped) checkIterator iter = do @@ -1375,7 +1693,7 @@ checkIterator iter = do return Iterator {..} checkInitializer :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Initializer 'Parsed -> Sem r (Initializer 'Scoped) checkInitializer ini = do @@ -1388,7 +1706,7 @@ checkInitializer ini = do } checkRange :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Range 'Parsed -> Sem r (Range 'Scoped) checkRange rng = do @@ -1413,7 +1731,7 @@ checkHole h = do } checkParens :: - Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => ExpressionAtoms 'Parsed -> Sem r Expression checkParens e@(ExpressionAtoms as _) = case as of @@ -1427,19 +1745,19 @@ checkParens e@(ExpressionAtoms as _) = case as of checkExpressionAtoms :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => ExpressionAtoms 'Parsed -> Sem r (ExpressionAtoms 'Scoped) checkExpressionAtoms (ExpressionAtoms l i) = (`ExpressionAtoms` i) <$> mapM checkExpressionAtom l checkJudoc :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => Judoc 'Parsed -> Sem r (Judoc 'Scoped) checkJudoc (Judoc groups) = Judoc <$> mapM checkJudocGroup groups checkJudocGroup :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => JudocGroup 'Parsed -> Sem r (JudocGroup 'Scoped) checkJudocGroup = \case @@ -1447,7 +1765,7 @@ checkJudocGroup = \case JudocGroupLines l -> JudocGroupLines <$> mapM checkJudocBlock l checkJudocBlock :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => JudocBlock 'Parsed -> Sem r (JudocBlock 'Scoped) checkJudocBlock = \case @@ -1455,19 +1773,19 @@ checkJudocBlock = \case JudocExample e -> JudocExample <$> traverseOf exampleExpression checkParseExpressionAtoms e checkJudocBlockParagraph :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => JudocBlockParagraph 'Parsed -> Sem r (JudocBlockParagraph 'Scoped) checkJudocBlockParagraph = traverseOf judocBlockParagraphBlocks (mapM checkJudocBlock) checkJudocLine :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => JudocLine 'Parsed -> Sem r (JudocLine 'Scoped) checkJudocLine (JudocLine delim atoms) = JudocLine delim <$> mapM (mapM checkJudocAtom) atoms checkJudocAtom :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => JudocAtom 'Parsed -> Sem r (JudocAtom 'Scoped) checkJudocAtom = \case @@ -1476,7 +1794,7 @@ checkJudocAtom = \case checkParseExpressionAtoms :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) => + Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => ExpressionAtoms 'Parsed -> Sem r Expression checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms @@ -1487,20 +1805,6 @@ checkParsePatternAtom :: Sem r PatternArg checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom -checkStatement :: - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r) => - Statement 'Parsed -> - Sem r (Statement 'Scoped) -checkStatement s = topBindings $ case s of - StatementSyntax synDef -> StatementSyntax <$> checkSyntaxDef synDef - StatementTypeSignature tySig -> StatementTypeSignature <$> checkTypeSignature tySig - StatementImport imp -> StatementImport <$> checkImport imp - StatementInductive dt -> StatementInductive <$> checkInductiveDef dt - StatementModule dt -> StatementModule <$> checkLocalModule dt - StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open - StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause - StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax - checkSyntaxDef :: (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r) => SyntaxDef -> @@ -1755,29 +2059,29 @@ makePatternTable :: PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]] makePatternTable (PatternAtoms latoms _) = [appOp] : operators where - getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef + getConstructorRef :: PatternAtom 'Scoped -> Maybe S.Name getConstructorRef = \case PatternAtomIden i -> case i of PatternScopedConstructor c -> Just c _ -> Nothing _ -> Nothing operators = mkSymbolTable (mapMaybe getConstructorRef (toList latoms)) - mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat PatternArg]] + mkSymbolTable :: [S.Name] -> [[P.Operator ParsePat PatternArg]] mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp where - unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat PatternArg) - unqualifiedSymbolOp (ConstructorRef' S.Name' {..}) + unqualifiedSymbolOp :: S.Name -> Maybe (Precedence, P.Operator ParsePat PatternArg) + unqualifiedSymbolOp S.Name' {..} | Just Fixity {..} <- _nameFixity, _nameKind == S.KNameConstructor = Just $ case _fixityArity of Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId)) where - unaryApp :: ConstructorRef -> PatternArg -> PatternArg - unaryApp funName = case u of - AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` funName) + unaryApp :: S.Name -> PatternArg -> PatternArg + unaryApp constrName = case u of + AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` constrName) Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId)) where - binaryInfixApp :: ConstructorRef -> PatternArg -> PatternArg -> PatternArg + binaryInfixApp :: S.Name -> PatternArg -> PatternArg -> PatternArg binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg infixLRN = case b of @@ -1785,13 +2089,13 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators AssocRight -> P.InfixR AssocNone -> P.InfixN | otherwise = Nothing - parseSymbolId :: S.NameId -> ParsePat ConstructorRef + parseSymbolId :: S.NameId -> ParsePat S.Name parseSymbolId uid = P.token getConstructorRefWithId mempty where - getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe ConstructorRef + getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe S.Name getConstructorRefWithId s = do ref <- getConstructorRef s - guard (ref ^. constructorRefName . S.nameId == uid) + guard (ref ^. S.nameId == uid) return ref -- Application by juxtaposition. @@ -1837,12 +2141,12 @@ parsePatternTerm = do explicitP . PatternConstructor <$> P.token constructorNoFixity mempty where - constructorNoFixity :: PatternAtom 'Scoped -> Maybe ConstructorRef + constructorNoFixity :: PatternAtom 'Scoped -> Maybe S.Name constructorNoFixity s = case s of PatternAtomIden (PatternScopedConstructor ref) | not (S.hasFixity n) -> Just ref where - n = ref ^. constructorRefName + n = ref _ -> Nothing parseWildcard :: ParsePat PatternArg 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 0068c648a0..4fd17a377b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -17,7 +17,6 @@ data ScoperError | ErrMultipleDeclarations MultipleDeclarations | ErrLacksTypeSig LacksTypeSig | ErrLacksFunctionClause LacksFunctionClause - | ErrDuplicateFunctionClause DuplicateFunctionClause | ErrImportCycle ImportCycle | ErrSymNotInScope NotInScope | ErrQualSymNotInScope QualSymNotInScope @@ -44,7 +43,6 @@ data ScoperError instance ToGenericError ScoperError where genericError = \case ErrCaseBranchImplicitPattern e -> genericError e - ErrDuplicateFunctionClause e -> genericError e ErrInfixParser e -> genericError e ErrAppLeftImplicit e -> genericError e ErrInfixPattern e -> genericError e 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 9e81277c06..a0a1944585 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 @@ -643,35 +643,6 @@ instance ToGenericError ConstructorExpectedLeftApplication where "Constructor expected on the left of a pattern application:" <+> ppCode opts' pat -data DuplicateFunctionClause = DuplicateFunctionClause - { _duplicateFunctionClauseSignature :: TypeSignature 'Scoped, - _duplicateFunctionClauseClause :: FunctionClause 'Scoped - } - deriving stock (Show) - -makeLenses ''DuplicateFunctionClause - -instance ToGenericError DuplicateFunctionClause where - genericError e = ask >>= generr - where - generr opts = - return - GenericError - { _genericErrorLoc = clLoc, - _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [clLoc, sigLoc] - } - where - opts' = fromGenericOptions opts - cl :: FunctionClause 'Scoped - cl = e ^. duplicateFunctionClauseClause - name :: S.Symbol - name = e ^. duplicateFunctionClauseSignature . sigName - clLoc = getLoc (cl ^. clauseOwnerFunction) - sigLoc = getLoc name - msg = - "The function" <+> ppCode opts' name <+> "has already been assigned a definition and so it cannot have additional clauses" - newtype CaseBranchImplicitPattern = CaseBranchImplicitPattern { _caseBranchImplicitPattern :: PatternArg } diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 0b13cec5c5..41c580cf4a 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -273,15 +273,34 @@ topModulePath = mkTopModulePath <$> dottedSymbol -- Top level statement -------------------------------------------------------------------------------- -statement :: (Members '[Files, Error ParserError, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed) +infixl 3 + +-- | Tries the left alternative. If it fails, backtracks and restores the contents of the pragmas and judoc stashes. Then parses the right atlernative +() :: Members '[PragmasStash, JudocStash] r => ParsecS r a -> ParsecS r a -> ParsecS r a +l r = do + p <- P.lift (get @(Maybe ParsedPragmas)) + j <- P.lift (get @(Maybe (Judoc 'Parsed))) + let recover = do + P.lift (put p) + P.lift (put j) + r + P.withRecovery (const recover) (P.try l) + +statement :: Members '[Files, Error ParserError, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (Statement 'Parsed) statement = P.label "" $ do optional_ stashJudoc optional_ stashPragmas ms <- optional ( StatementSyntax <$> syntaxDef - <|> P.try (StatementOpenModule <$> newOpenSyntax) - <|> StatementOpenModule <$> openModule + <|> StatementOpenModule + <$> newOpenSyntax + -- TODO remove after removing old syntax + StatementFunctionDef + <$> newTypeSignature Nothing + -- TODO remove after removing old syntax + StatementOpenModule + <$> openModule <|> StatementImport <$> import_ <|> StatementInductive <$> inductiveDef Nothing <|> StatementModule <$> moduleDef @@ -476,11 +495,18 @@ builtinTypeSig b = do fun <- symbol typeSignature terminating fun (Just b) +builtinNewTypeSig :: + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => + WithLoc BuiltinFunction -> + ParsecS r (FunctionDef 'Parsed) +builtinNewTypeSig = newTypeSignature . Just + builtinStatement :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed) builtinStatement = do void (kw kwBuiltin) (builtinInductive >>= fmap StatementInductive . builtinInductiveDef) - <|> (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig) + <|> (builtinFunction >>= fmap StatementFunctionDef . builtinNewTypeSig) + (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig) <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef) -------------------------------------------------------------------------------- @@ -793,8 +819,8 @@ auxTypeSigFunClause = do Left <$> typeSignature terminating sym Nothing | otherwise -> checkEq - <|> (Left <$> typeSignature terminating sym Nothing) - <|> (Right <$> functionClause sym) + <|> Left <$> typeSignature terminating sym Nothing + <|> Right <$> functionClause sym where checkEq :: ParsecS r a checkEq = do @@ -802,6 +828,53 @@ auxTypeSigFunClause = do kw kwEq parseFailure off "expected \":=\" instead of \"=\"" +newTypeSignature :: + forall r. + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => + Maybe (WithLoc BuiltinFunction) -> + ParsecS r (FunctionDef 'Parsed) +newTypeSignature _signBuiltin = P.label "" $ do + _signTerminating <- optional (kw kwTerminating) + _signName <- symbol + _signArgs <- many parseArg + _signColonKw <- Irrelevant <$> kw kwColon + _signRetType <- parseExpressionAtoms + _signDoc <- getJudoc + _signPragmas <- getPragmas + _signBody <- parseBody + return FunctionDef {..} + where + parseArg :: ParsecS r (SigArg 'Parsed) + parseArg = do + (openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do + (opn, impl) <- implicitOpen + n <- some1 symbol + c <- Irrelevant <$> kw kwColon + return (opn, n, impl, c) + _sigArgType <- parseExpressionAtoms + closeDelim <- implicitClose _sigArgImplicit + let _sigArgDelims = Irrelevant (openDelim, closeDelim) + return SigArg {..} + + parseBody :: ParsecS r (FunctionDefBody 'Parsed) + parseBody = + SigBodyExpression <$> bodyExpr + <|> (SigBodyClauses <$> bodyClauses) + where + bodyClause :: ParsecS r (NewFunctionClause 'Parsed) + bodyClause = do + _clausenPipeKw <- Irrelevant <$> kw kwPipe + _clausenPatterns <- some1 patternAtom + _clausenAssignKw <- Irrelevant <$> kw kwAssign + _clausenBody <- parseExpressionAtoms + return NewFunctionClause {..} + bodyClauses :: ParsecS r (NonEmpty (NewFunctionClause 'Parsed)) + bodyClauses = some1 bodyClause + bodyExpr :: ParsecS r (ExpressionAtoms 'Parsed) + bodyExpr = do + void (kw kwAssign) + parseExpressionAtoms + axiomDef :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Maybe (WithLoc BuiltinAxiom) -> diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a26ed134f2..0debfdbe7f 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -278,20 +278,30 @@ goModuleBody stmts = do _moduleImports <- mapM goImport (scanImports stmts) otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goStatement) ss functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions + newFunctions <- map (fmap Internal.PreFunctionDef) <$> newCompiledFunctions let _moduleStatements = map (^. indexedThing) ( sortOn (^. indexedIx) - (otherThanFunctions <> functions) + (otherThanFunctions <> functions <> newFunctions) ) return Internal.ModuleBody {..} where + ss' :: [Statement 'Scoped] ss' = concatMap Concrete.flattenStatement stmts ss :: [Indexed (Statement 'Scoped)] ss = zipWith Indexed [0 ..] ss' + newCompiledFunctions :: Sem r [Indexed Internal.FunctionDef] + newCompiledFunctions = + sequence + [ Indexed i <$> funDef + | Indexed i (StatementFunctionDef f) <- ss, + let funDef = goTopNewFunctionDef f + ] + compiledFunctions :: Sem r [Indexed Internal.FunctionDef] compiledFunctions = sequence @@ -304,7 +314,7 @@ goModuleBody stmts = do getClauses :: S.Symbol -> [FunctionClause 'Scoped] getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction] sigs :: [Indexed (TypeSignature 'Scoped)] - sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss] + sigs = [Indexed i t | Indexed i (StatementTypeSignature t) <- ss] scanImports :: [Statement 'Scoped] -> [Import 'Scoped] scanImports stmts = mconcatMap go stmts @@ -319,6 +329,7 @@ scanImports stmts = mconcatMap go stmts StatementTypeSignature {} -> [] StatementAxiom {} -> [] StatementSyntax {} -> [] + StatementFunctionDef {} -> [] where openImport :: OpenModule 'Scoped -> Maybe (Import 'Scoped) openImport o = case o ^. openModuleImportKw of @@ -352,6 +363,7 @@ guardNotCached (hit, m) = do guard (not hit) return m +-- | Ignores functions goStatement :: forall r. Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r => @@ -362,6 +374,7 @@ goStatement = \case StatementAxiom d -> pure . Internal.PreAxiomDef <$> goAxiom d StatementModule f -> goLocalModule f StatementImport {} -> return [] + StatementFunctionDef {} -> return [] StatementSyntax {} -> return [] StatementOpenModule {} -> return [] StatementTypeSignature {} -> return [] @@ -416,7 +429,7 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do _funDefPragmas <- goPragmas _sigPragmas _funDefClauses <- case (_sigBody, nonEmpty clauses) of (Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig)) - (Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses'))) + (Just {}, Just {}) -> error "duplicate function clause. TODO remove this when old function syntax is removed" (Just body, Nothing) -> do body' <- goExpression body return @@ -430,6 +443,65 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do (Nothing, Just clauses') -> mapM goFunctionClause clauses' return Internal.FunctionDef {..} +goTopNewFunctionDef :: + forall r. + (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => + FunctionDef 'Scoped -> + Sem r Internal.FunctionDef +goTopNewFunctionDef FunctionDef {..} = do + let _funDefName = goSymbol _signName + _funDefTerminating = isJust _signTerminating + _funDefBuiltin = (^. withLocParam) <$> _signBuiltin + _funDefType <- goDefType + _funDefExamples <- goExamples _signDoc + _funDefPragmas <- goPragmas _signPragmas + _funDefClauses <- goBody + return Internal.FunctionDef {..} + where + goBody :: Sem r (NonEmpty Internal.FunctionClause) + goBody = do + commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs + let _clauseName = goSymbol _signName + goClause :: NewFunctionClause 'Scoped -> Sem r Internal.FunctionClause + goClause NewFunctionClause {..} = do + let _clauseName = goSymbol _signName + _clauseBody <- goExpression _clausenBody + extraPatterns <- toList <$> (mapM goPatternArg _clausenPatterns) + let _clausePatterns = commonPatterns <> extraPatterns + return Internal.FunctionClause {..} + case _signBody of + SigBodyExpression body -> do + _clauseBody <- goExpression body + let _clausePatterns = commonPatterns + return (pure Internal.FunctionClause {..}) + SigBodyClauses cls -> mapM goClause cls + + goDefType :: Sem r Internal.Expression + goDefType = do + args <- concatMapM (fmap toList . argToParam) _signArgs + ret <- goExpression _signRetType + return (Internal.foldFunType args ret) + where + argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter) + argToParam SigArg {..} = do + _paramType <- goExpression _sigArgType + let _paramImplicit = _sigArgImplicit + mk :: S.Symbol -> Sem r Internal.FunctionParameter + mk s = + let _paramName = Just (goSymbol s) + in return Internal.FunctionParameter {..} + mapM mk _sigArgNames + + argToPattern :: SigArg 'Scoped -> Sem r (NonEmpty Internal.PatternArg) + argToPattern SigArg {..} = do + let _patternArgIsImplicit = _sigArgImplicit + _patternArgName :: Maybe Internal.Name = Nothing + mk :: S.Symbol -> Sem r Internal.PatternArg + mk s = do + let _patternArgPattern = Internal.PatternVariable (goSymbol s) + return Internal.PatternArg {..} + mapM mk _sigArgNames + goTopFunctionDef :: forall r. (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => @@ -671,11 +743,11 @@ goExpression = \case goIden :: Concrete.ScopedIden -> Internal.Expression goIden x = Internal.ExpressionIden $ case x of - ScopedAxiom a -> Internal.IdenAxiom (goName (a ^. Concrete.axiomRefName)) - ScopedInductive i -> Internal.IdenInductive (goName (i ^. Concrete.inductiveRefName)) + ScopedAxiom a -> Internal.IdenAxiom (goName a) + ScopedInductive i -> Internal.IdenInductive (goName i) ScopedVar v -> Internal.IdenVar (goSymbol v) - ScopedFunction fun -> Internal.IdenFunction (goName (fun ^. Concrete.functionRefName)) - ScopedConstructor c -> Internal.IdenConstructor (goName (c ^. Concrete.constructorRefName)) + ScopedFunction fun -> Internal.IdenFunction (goName fun) + ScopedConstructor c -> Internal.IdenConstructor (goName c) goLet :: Let 'Scoped -> Sem r Internal.Let goLet l = do @@ -834,7 +906,7 @@ goPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternApplicatio goPatternConstructor :: Members '[Builtins, NameIdGen, Error ScoperError] r => - ConstructorRef -> + S.Name -> Sem r Internal.ConstructorApp goPatternConstructor a = uncurry mkConstructorApp <$> viewApp (PatternConstructor a) @@ -874,8 +946,8 @@ viewApp p = case p of | otherwise = viewApp (l ^. patternArgPattern) err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p)) -goConstructorRef :: ConstructorRef -> Internal.Name -goConstructorRef (ConstructorRef' n) = goName n +goConstructorRef :: S.Name -> Internal.Name +goConstructorRef n = goName n goPatternArg :: Members '[Builtins, NameIdGen, Error ScoperError] r => PatternArg -> Sem r Internal.PatternArg goPatternArg p = do diff --git a/src/Juvix/Formatter.hs b/src/Juvix/Formatter.hs index 19e22089f8..1808e3c0c7 100644 --- a/src/Juvix/Formatter.hs +++ b/src/Juvix/Formatter.hs @@ -2,6 +2,7 @@ module Juvix.Formatter where import Data.List.NonEmpty qualified as NonEmpty import Data.Text qualified as T +import Juvix.Compiler.Concrete.Extra (migrateFunctionSyntax) import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Print (ppOutDefault) import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper @@ -17,6 +18,8 @@ data FormattedFileInfo = FormattedFileInfo _formattedFileInfoContentsModified :: Bool } +newtype NewSyntax = NewSyntax Bool + data ScopeEff m a where ScopeFile :: Path Abs File -> ScopeEff m Scoper.ScoperResult ScopeStdin :: ScopeEff m Scoper.ScoperResult @@ -62,7 +65,7 @@ formattedFileInfoContentsText = to infoToPlainText -- contents of the file. format :: forall r. - Members '[ScopeEff, Files, Output FormattedFileInfo] r => + Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r => Path Abs File -> Sem r FormatResult format p = do @@ -88,7 +91,7 @@ format p = do -- subdirectories that contain a juvix.yaml file. formatProject :: forall r. - Members '[ScopeEff, Files, Output FormattedFileInfo] r => + Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r => Path Abs Dir -> Sem r FormatResult formatProject p = do @@ -105,14 +108,14 @@ formatProject p = do subRes <- combineResults <$> mapM format juvixFiles return (res <> subRes, RecurseFilter (\hasJuvixYaml d -> not hasJuvixYaml && not (isHiddenDirectory d))) -formatPath :: Members [Reader Text, ScopeEff] r => Path Abs File -> Sem r (NonEmpty AnsiText) +formatPath :: Members [Reader NewSyntax, Reader Text, ScopeEff] r => Path Abs File -> Sem r (NonEmpty AnsiText) formatPath p = do res <- scopeFile p formatScoperResult res formatStdin :: forall r. - Members '[ScopeEff, Files, Output FormattedFileInfo] r => + Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r => Sem r FormatResult formatStdin = do res <- scopeStdin @@ -144,10 +147,13 @@ formatResultFromContents formattedContents filepath = do ) return res -formatScoperResult :: Member (Reader Text) r => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText) +formatScoperResult :: Members [Reader NewSyntax, Reader Text] r => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText) formatScoperResult res = do let cs = res ^. Scoper.comments - formattedModules = run (runReader cs (mapM formatTopModule (res ^. Scoper.resultModules))) + formattedModules <- + runReader cs + . mapM formatTopModule + $ res ^. Scoper.resultModules case res ^. Scoper.mainModule . modulePragmas of Just pragmas -> case pragmas ^. withLocParam . withSourceValue . pragmasFormat of @@ -159,7 +165,11 @@ formatScoperResult res = do Nothing -> return formattedModules where - formatTopModule :: Member (Reader Comments) r => Module 'Scoped 'ModuleTop -> Sem r AnsiText + formatTopModule :: Members [Reader NewSyntax, Reader Comments] r => Module 'Scoped 'ModuleTop -> Sem r AnsiText formatTopModule m = do + NewSyntax newSyntax <- ask cs <- ask - return (ppOutDefault cs m) + let m' + | newSyntax = migrateFunctionSyntax m + | otherwise = m + return (ppOutDefault cs m') diff --git a/test/Formatter/Positive.hs b/test/Formatter/Positive.hs index abd5227829..d36a5898a5 100644 --- a/test/Formatter/Positive.hs +++ b/test/Formatter/Positive.hs @@ -22,7 +22,14 @@ makeFormatTest' Scope.PosTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - d <- runM $ runError $ runOutputList @FormattedFileInfo $ runScopeEffIO $ runFilesIO $ format file' + d <- + runM + . runError + . runOutputList @FormattedFileInfo + . runScopeEffIO + . runFilesIO + . runReader (NewSyntax False) + $ format file' case d of Right (_, FormatResultOK) -> return () Right (_, FormatResultNotFormatted) -> assertFailure ("File: " <> show file' <> " is not formatted") diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index aa37a2396d..e1d21dd2f1 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -225,13 +225,6 @@ scoperErrorTests = $ \case ErrMultipleDeclarations {} -> Nothing _ -> wrongError, - NegTest - "A function has a duplicate clause" - $(mkRelDir ".") - $(mkRelFile "DuplicateClause.juvix") - $ \case - ErrDuplicateFunctionClause {} -> Nothing - _ -> wrongError, NegTest "A function lacks a type signature" $(mkRelDir ".") diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 024f006b6c..b2408d679d 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -6,7 +6,6 @@ import Juvix.Compiler.Builtins (evalTopBuiltins) import Juvix.Compiler.Concrete qualified as Concrete import Juvix.Compiler.Concrete.Data.Highlight (ignoreHighlightBuilder) import Juvix.Compiler.Concrete.Extra -import Juvix.Compiler.Concrete.Pretty qualified as M import Juvix.Compiler.Concrete.Print qualified as P import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper @@ -26,11 +25,8 @@ makeLenses ''PosTest root :: Path Abs Dir root = relToProject $(mkRelDir "tests/positive") -renderCodeOld :: (HasLoc c, M.PrettyPrint c) => c -> Text -renderCodeOld = toPlainText . M.ppOutDefault - -renderCodeNew :: (HasLoc c, P.PrettyPrint c) => c -> Text -renderCodeNew = toPlainText . P.ppOutDefault emptyComments +renderCodeNew :: P.PrettyPrint c => c -> Text +renderCodeNew = toPlainText . P.ppOutNoComments P.defaultOptions testDescr :: PosTest -> TestDescr testDescr PosTest {..} = helper renderCodeNew @@ -84,7 +80,7 @@ testDescr PosTest {..} = helper renderCodeNew fsParsed :: HashMap (Path Abs File) Text fsParsed = HashMap.fromList $ - [ (getModuleFilePath m, renderCodeOld m) + [ (getModuleFilePath m, renderCodeNew m) | m <- toList (p ^. Parser.resultTable . Parser.infoParsedModules) ] <> yamlFiles @@ -239,6 +235,10 @@ tests = "Iterators" $(mkRelDir ".") $(mkRelFile "Iterators.juvix"), + PosTest + "New function syntax" + $(mkRelDir ".") + $(mkRelFile "Syntax.juvix"), PosTest "Format pragma" $(mkRelDir ".") diff --git a/tests/Compilation/positive/test052.juvix b/tests/Compilation/positive/test052.juvix index 09df937d77..9fcd4c1747 100644 --- a/tests/Compilation/positive/test052.juvix +++ b/tests/Compilation/positive/test052.juvix @@ -2,6 +2,7 @@ module test052; open import Stdlib.Prelude; +import Stdlib.Trait.Show as Show; fromShow : {a : Type} -> Show a -> a -> String; fromShow (mkShow s) a := s a; @@ -84,7 +85,7 @@ module ExprTraits; toString (num n) := natToString n; --- ;Show; instance for ;Expr;. - Show : Show Expr; + Show : Show.Show Expr; Show := mkShow toString; end; @@ -94,7 +95,7 @@ module ValTraits; --- ;Show; instance for ;Val;. terminating - Show : Show Val; + Show : Show.Show Val; Show := mkShow valToString; valToString (vnum n) := natToString n; diff --git a/tests/negative/DuplicateClause.juvix b/tests/negative/DuplicateClause.juvix deleted file mode 100644 index 04dd487714..0000000000 --- a/tests/negative/DuplicateClause.juvix +++ /dev/null @@ -1,7 +0,0 @@ -module DuplicateClause; - -axiom T : Type; - -id : T → T := λ {t := t}; -id t := t; - diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix index c8ef8d1854..5320d71958 100644 --- a/tests/positive/Format.juvix +++ b/tests/positive/Format.juvix @@ -5,9 +5,9 @@ Format; import -- Import a module of name: Stdlib.Prelude open -- Bring all names into scope but.. hiding -- Hide some names -{-- like this +{-- like this ,; -- don't want , here --- Bool either +-- Bool either Bool; true; false}; import Stdlib.Data.Nat.Ord open; @@ -117,8 +117,8 @@ axiom undefined : {A : Type} -> A; -- 200 in the body is idented with respect to the start of the chain -- (at {A : Type}) -exampleFunction2 : - {A : Type} +exampleFunction2 + : {A : Type} -> List A -> List A -> List A @@ -127,20 +127,20 @@ exampleFunction2 : -> List A -> List A -> Nat := - λ {_ _ _ _ _ _ _ := - undefined - -- comment after first - + undefined - -- comment after second - + undefined - + undefined - + undefined - + undefined - + undefined - + undefined - + undefined - + undefined - + undefined}; + λ {_ _ _ _ _ _ _ := + undefined + -- comment after first + + undefined + -- comment after second + + undefined + + undefined + + undefined + + undefined + + undefined + + undefined + + undefined + + undefined + + undefined}; positive type T0 (A : Type) := diff --git a/tests/positive/SignatureWithBody.juvix b/tests/positive/SignatureWithBody.juvix index 30964257f8..6c59876bf1 100644 --- a/tests/positive/SignatureWithBody.juvix +++ b/tests/positive/SignatureWithBody.juvix @@ -2,20 +2,18 @@ module SignatureWithBody; import Stdlib.Prelude open; -isNull : - {A : Type} → List A → Bool := - λ { - | nil := true - | _ := false - }; +isNull : {A : Type} → List A → Bool := + λ { + | nil := true + | _ := false + }; -isNull' : - {A : Type} → List A → Bool := - let - aux : - {A : Type} → List A → Bool := - λ { - | nil := true - | _ := false - }; - in aux; +isNull' : {A : Type} → List A → Bool := + let + aux : + {A : Type} → List A → Bool := + λ { + | nil := true + | _ := false + }; + in aux; diff --git a/tests/positive/Syntax.juvix b/tests/positive/Syntax.juvix new file mode 100644 index 0000000000..34ace1b456 --- /dev/null +++ b/tests/positive/Syntax.juvix @@ -0,0 +1,60 @@ +module Syntax; + +compose {A B C : Type} (f : B -> C) (g : A -> B) (x : A) + : C := f (g x); + +compose' {A B C : Type} (f : B -> C) (g : A -> B) : A -> C + | x := f (g x); + +type Bool := + | false : Bool + | true : Bool; + +type Nat := + | zero : Nat + | suc : Nat -> Nat; + +not : Bool -> Bool + | false := true + | true := false; + +even : Nat -> Bool + | zero := true + | (suc n) := odd n; + +odd : Nat -> Bool + | zero := false + | (suc n) := even n; + +syntax infixl 4 ==1; + +==1 : Nat -> Nat -> Bool + | zero zero := true + | (suc a) (suc b) := a ==2 b + | _ _ := false; + +-- note that ==2 is used before its infix definition +syntax infixl 4 ==2; + +==2 : Nat -> Nat -> Bool + | zero zero := true + | (suc a) (suc b) := a ==1 b + | _ _ := false; + +module MutualTypes; + -- we use Tree and isEmpty before their definition + isNotEmpty {a : Type} (t : Tree a) : Bool := + not (isEmpty t); + + isEmpty {a : Type} : (t : Tree a) -> Bool + | empty := true + | (node _ _) := false; + + type Tree (a : Type) := + | empty : Tree a + | node : a -> Forest a -> Tree a; + + type Forest (a : Type) := + | nil : Forest a + | cons : Tree a -> Forest a; +end; diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml index 1ccf7d951c..0d227fd566 100644 --- a/tests/smoke/Commands/repl.smoke.yaml +++ b/tests/smoke/Commands/repl.smoke.yaml @@ -62,9 +62,9 @@ tests: contains: | --- Addition for ;Nat;s. builtin nat-plus - + : Nat → Nat → Nat; - + zero b := b; - + (suc a) b := suc (a + b); + + : Nat → Nat → Nat + | zero b := b + | (suc a) b := suc (a + b) exit-status: 0 - name: repl-def-infix @@ -77,9 +77,9 @@ tests: contains: | --- Addition for ;Nat;s. builtin nat-plus - + : Nat → Nat → Nat; - + zero b := b; - + (suc a) b := suc (a + b); + + : Nat → Nat → Nat + | zero b := b + | (suc a) b := suc (a + b) exit-status: 0 - name: open