From 70cbdd0a302b874cccfac0244ecae158cbd7f858 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Wed, 4 Dec 2024 13:39:20 +0100 Subject: [PATCH 1/2] Global option `--no-check` (#3224) The `--no-check` option disables the backend-specific sanity check in Core (the transformations in `Check/*`, which check the type of main, use of builtins, etc). This is useful for debugging. --- app/GlobalOptions.hs | 9 +++++++++ src/Juvix/Compiler/Core/Pipeline.hs | 8 ++++++-- src/Juvix/Compiler/Pipeline/EntryPoint.hs | 3 +++ 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs index 471717c691..23fa62c0f9 100644 --- a/app/GlobalOptions.hs +++ b/app/GlobalOptions.hs @@ -24,6 +24,7 @@ data GlobalOptions = GlobalOptions _globalNoPositivity :: Bool, _globalNoCoverage :: Bool, _globalNoStdlib :: Bool, + _globalNoCheck :: Bool, _globalUnrollLimit :: Int, _globalNumThreads :: NumThreads, _globalFieldSize :: Maybe Natural, @@ -72,6 +73,7 @@ defaultGlobalOptions = _globalLogLevel = LogLevelProgress, _globalNoCoverage = False, _globalNoStdlib = False, + _globalNoCheck = False, _globalUnrollLimit = defaultUnrollLimit, _globalFieldSize = Nothing, _globalDevShowThreadIds = False, @@ -162,6 +164,11 @@ parseGlobalFlags = do <> intercalate " < " [show l | l <- allElements @LogLevel] ) ) + _globalNoCheck <- + switch + ( long "dev-no-check" + <> help "[DEV] Disable input sanity check in Core" + ) _globalShowNameIds <- switch ( long "show-name-ids" @@ -211,6 +218,7 @@ entryPointFromGlobalOptions root mainFile opts = do _entryPointNoPositivity = opts ^. globalNoPositivity, _entryPointNoCoverage = opts ^. globalNoCoverage, _entryPointNoStdlib = opts ^. globalNoStdlib, + _entryPointNoCheck = opts ^. globalNoCheck, _entryPointUnrollLimit = opts ^. globalUnrollLimit, _entryPointGenericOptions = project opts, _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir, @@ -232,6 +240,7 @@ entryPointFromGlobalOptionsNoFile root opts = do _entryPointNoPositivity = opts ^. globalNoPositivity, _entryPointNoCoverage = opts ^. globalNoCoverage, _entryPointNoStdlib = opts ^. globalNoStdlib, + _entryPointNoCheck = opts ^. globalNoCheck, _entryPointUnrollLimit = opts ^. globalUnrollLimit, _entryPointGenericOptions = project opts, _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir, diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs index 51d4d50658..f762bc7278 100644 --- a/src/Juvix/Compiler/Core/Pipeline.hs +++ b/src/Juvix/Compiler/Core/Pipeline.hs @@ -7,7 +7,7 @@ where import Juvix.Compiler.Core.Data.InfoTable import Juvix.Compiler.Core.Options import Juvix.Compiler.Core.Transformation -import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint) +import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint, entryPointNoCheck) toTypechecked :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module toTypechecked = mapReader fromEntryPoint . applyTransformations toTypecheckTransformations @@ -19,7 +19,11 @@ toStored = mapReader fromEntryPoint . applyTransformations toStoredTransformatio -- | Perform transformations on stored Core necessary before the translation to -- Core.Stripped toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => TransformationId -> Module -> Sem r Module -toStripped checkId = mapReader fromEntryPoint . applyTransformations (toStrippedTransformations checkId) +toStripped checkId md = do + noCheck <- asks (^. entryPointNoCheck) + let checkId' = if noCheck then IdentityTrans else checkId + mapReader fromEntryPoint $ + applyTransformations (toStrippedTransformations checkId') md -- | Perform transformations on stored Core necessary before the translation to VampIR toVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module diff --git a/src/Juvix/Compiler/Pipeline/EntryPoint.hs b/src/Juvix/Compiler/Pipeline/EntryPoint.hs index cf23d9892b..df487703b4 100644 --- a/src/Juvix/Compiler/Pipeline/EntryPoint.hs +++ b/src/Juvix/Compiler/Pipeline/EntryPoint.hs @@ -33,6 +33,8 @@ data EntryPoint = EntryPoint _entryPointTarget :: Maybe Target, _entryPointDebug :: Bool, _entryPointUnsafe :: Bool, + -- | Skip the correctness check in the Core pipeline part. + _entryPointNoCheck :: Bool, _entryPointUnrollLimit :: Int, _entryPointOptimizationLevel :: Int, _entryPointInliningDepth :: Int, @@ -76,6 +78,7 @@ defaultEntryPointNoFile pkg root = _entryPointTarget = Nothing, _entryPointDebug = False, _entryPointUnsafe = False, + _entryPointNoCheck = False, _entryPointUnrollLimit = defaultUnrollLimit, _entryPointOptimizationLevel = defaultOptimizationLevel, _entryPointInliningDepth = defaultInliningDepth, From 021fc0ccb8c6d22a689db2863869d6e1d2c35fd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Wed, 4 Dec 2024 15:59:02 +0100 Subject: [PATCH 2/2] Remove `@?` (#3216) * Closes #3210 --- examples/demo/Package.juvix | 2 +- examples/midsquare/Package.juvix | 2 +- examples/milestone/Bank/Package.juvix | 2 +- examples/milestone/Collatz/Package.juvix | 2 +- examples/milestone/Fibonacci/Package.juvix | 2 +- examples/milestone/Hanoi/Package.juvix | 2 +- examples/milestone/HelloWorld/Package.juvix | 2 +- .../milestone/PascalsTriangle/Package.juvix | 2 +- examples/milestone/TicTacToe/Package.juvix | 2 +- examples/milestone/Tutorial/Package.juvix | 2 +- include/package/PackageDescription/V1.juvix | 2 +- include/package/PackageDescription/V2.juvix | 2 +- juvix-stdlib | 2 +- src/Juvix/Compiler/Concrete/Gen.hs | 36 ++---- src/Juvix/Compiler/Concrete/Keywords.hs | 2 - src/Juvix/Compiler/Concrete/Language/Base.hs | 103 ++++++++---------- .../Concrete/Language/IsApeInstances.hs | 6 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 23 ++-- .../FromParsed/Analysis/Scoping.hs | 52 ++++----- .../Concrete/Translation/FromSource.hs | 46 +++----- .../Internal/Translation/FromConcrete.hs | 24 ++-- .../Pipeline/Package/Loader/Versions.hs | 6 +- src/Juvix/Data/Keyword/All.hs | 3 - src/Juvix/Extra/Strings.hs | 3 - test/Scope/Negative.hs | 2 +- .../Anoma/Compilation/positive/Package.juvix | 2 +- .../Anoma/Compilation/positive/test067.juvix | 2 +- .../Anoma/Compilation/positive/test069.juvix | 2 +- .../Anoma/Compilation/positive/test070.juvix | 6 +- .../Anoma/Compilation/positive/test071.juvix | 4 +- .../positive/test072/Package.juvix | 2 +- .../positive/test073/Package.juvix | 2 +- .../positive/test085/Package.juvix | 2 +- .../positive/test085/client/Package.juvix | 2 +- tests/Casm/Compilation/positive/test067.juvix | 2 +- tests/Casm/Compilation/positive/test069.juvix | 2 +- tests/Casm/Compilation/positive/test070.juvix | 6 +- tests/Casm/Compilation/positive/test071.juvix | 4 +- .../positive/test072/Package.juvix | 2 +- .../positive/test073/Package.juvix | 2 +- tests/Compilation/positive/test061.juvix | 6 +- tests/Compilation/positive/test067.juvix | 2 +- tests/Compilation/positive/test069.juvix | 2 +- tests/Compilation/positive/test070.juvix | 6 +- tests/Compilation/positive/test071.juvix | 16 ++- .../positive/test072/Package.juvix | 2 +- .../positive/test073/Package.juvix | 2 +- .../positive/Dependencies/Dep1/Package.juvix | 2 +- .../positive/Dependencies/Dep2/Package.juvix | 2 +- tests/Rust/Compilation/positive/test067.juvix | 2 +- tests/Rust/Compilation/positive/test069.juvix | 2 +- tests/Rust/Compilation/positive/test070.juvix | 6 +- tests/Rust/Compilation/positive/test071.juvix | 4 +- .../positive/test072/Package.juvix | 2 +- .../positive/test073/Package.juvix | 2 +- tests/negative/DuplicateArgument.juvix | 2 +- tests/negative/MissingArgument.juvix | 2 +- tests/negative/NoDependencies/Package.juvix | 2 +- tests/negative/NoNamedArguments.juvix | 2 +- .../Package.juvix | 2 +- tests/negative/UnexpectedArgument.juvix | 2 +- .../negative/UnexpectedArgumentWildcard.juvix | 2 +- tests/negative/issue2771/Package.juvix | 2 +- tests/negative/issue3161/Package.juvix | 2 +- tests/positive/ConfluentScoping/Package.juvix | 2 +- .../Dependencies/.libs/Extra/Package.juvix | 2 +- tests/positive/Dependencies/Package.juvix | 2 +- tests/positive/FancyPaths/Package.juvix | 2 +- tests/positive/FancyPaths/home/Package.juvix | 2 +- .../FancyPaths/other dep/Package.juvix | 2 +- .../FancyPaths/path with spaces/Package.juvix | 2 +- .../ImportNestedLocalModule/Package.juvix | 2 +- .../Internal/Positivity2/Package.juvix | 2 +- tests/positive/Isabelle/Package.juvix | 2 +- tests/positive/Markdown/markdown/Test.md | 2 +- tests/positive/MarkdownImport/Package.juvix | 2 +- tests/positive/NamedArguments.juvix | 26 ++--- tests/positive/NoDependencies/Package.juvix | 2 +- .../PackageLoader/PackageJuvix/Package.juvix | 2 +- .../PackageJuvixAndYaml/Package.juvix | 2 +- .../Package.juvix | 2 +- .../PackageJuvixUsesLockfile/Package.juvix | 2 +- .../YamlEmptyDependencies/Package.juvix | 2 +- .../PackageJuvix/Package.juvix | 2 +- .../PackageJuvixAndYaml/Package.juvix | 2 +- .../Package.juvix | 2 +- .../PackageJuvixUsesLockfile/Package.juvix | 2 +- tests/positive/Records.juvix | 2 +- tests/positive/StdlibList/Package.juvix | 2 +- .../VisibilityPrecendence/Package.juvix | 2 +- tests/positive/issue2737/Package.juvix | 2 +- tests/positive/issue2929/Package.juvix | 2 +- tests/positive/issue3048/Package.juvix | 2 +- tests/positive/issue3068/Package.juvix | 2 +- tests/positive/package/Package.juvix | 2 +- ...pile-dependencies-package-juvix.smoke.yaml | 38 +++---- .../Commands/compile-dependencies.smoke.yaml | 2 +- 97 files changed, 261 insertions(+), 315 deletions(-) diff --git a/examples/demo/Package.juvix b/examples/demo/Package.juvix index 95fc82192b..39e428effd 100644 --- a/examples/demo/Package.juvix +++ b/examples/demo/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "Demo"; version := mkVersion 0 1 0 }; diff --git a/examples/midsquare/Package.juvix b/examples/midsquare/Package.juvix index 564be67861..191f097606 100644 --- a/examples/midsquare/Package.juvix +++ b/examples/midsquare/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "midsquare"; version := mkVersion 0 1 0 }; diff --git a/examples/milestone/Bank/Package.juvix b/examples/milestone/Bank/Package.juvix index f0b0d1db0f..83819477c1 100644 --- a/examples/milestone/Bank/Package.juvix +++ b/examples/milestone/Bank/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "bank" }; diff --git a/examples/milestone/Collatz/Package.juvix b/examples/milestone/Collatz/Package.juvix index 87fe97ccb4..10d24fc716 100644 --- a/examples/milestone/Collatz/Package.juvix +++ b/examples/milestone/Collatz/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "Collatz"; version := mkVersion 0 1 0; main := just "Collatz.juvix" diff --git a/examples/milestone/Fibonacci/Package.juvix b/examples/milestone/Fibonacci/Package.juvix index eb009b9675..7624e50fb5 100644 --- a/examples/milestone/Fibonacci/Package.juvix +++ b/examples/milestone/Fibonacci/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "Fibonacci"; version := mkVersion 0 1 0; main := just "Fibonacci.juvix" diff --git a/examples/milestone/Hanoi/Package.juvix b/examples/milestone/Hanoi/Package.juvix index 4588aeb0f1..9bb7f6f53e 100644 --- a/examples/milestone/Hanoi/Package.juvix +++ b/examples/milestone/Hanoi/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "Hanoi"; version := mkVersion 0 1 0; main := just "Hanoi.juvix" diff --git a/examples/milestone/HelloWorld/Package.juvix b/examples/milestone/HelloWorld/Package.juvix index 7960036eaf..ec3f84f5c8 100644 --- a/examples/milestone/HelloWorld/Package.juvix +++ b/examples/milestone/HelloWorld/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "HelloWorld"; version := mkVersion 0 1 0; main := just "HelloWorld.juvix" diff --git a/examples/milestone/PascalsTriangle/Package.juvix b/examples/milestone/PascalsTriangle/Package.juvix index a740b3e86b..c6370e1474 100644 --- a/examples/milestone/PascalsTriangle/Package.juvix +++ b/examples/milestone/PascalsTriangle/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "PascalsTriangle"; version := mkVersion 0 1 0; main := just "PascalsTriangle.juvix" diff --git a/examples/milestone/TicTacToe/Package.juvix b/examples/milestone/TicTacToe/Package.juvix index ff3cda7035..edbcb64f7f 100644 --- a/examples/milestone/TicTacToe/Package.juvix +++ b/examples/milestone/TicTacToe/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "TicTacToe"; version := mkVersion 0 1 0; main := just "CLI/TicTacToe.juvix" diff --git a/examples/milestone/Tutorial/Package.juvix b/examples/milestone/Tutorial/Package.juvix index 3c4a4a3ec4..e670c512c8 100644 --- a/examples/milestone/Tutorial/Package.juvix +++ b/examples/milestone/Tutorial/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "Tutorial"; version := mkVersion 0 1 0 }; diff --git a/include/package/PackageDescription/V1.juvix b/include/package/PackageDescription/V1.juvix index 179e2f6dcf..440e7c81c5 100644 --- a/include/package/PackageDescription/V1.juvix +++ b/include/package/PackageDescription/V1.juvix @@ -62,7 +62,7 @@ mkVersion {release : Maybe String := nothing} {meta : Maybe String := nothing} : SemVer := - mkSemVer@?{ + mkSemVer@{ major; minor; patch; diff --git a/include/package/PackageDescription/V2.juvix b/include/package/PackageDescription/V2.juvix index dc043f1bc8..bfaf771899 100644 --- a/include/package/PackageDescription/V2.juvix +++ b/include/package/PackageDescription/V2.juvix @@ -49,7 +49,7 @@ mkVersion {release : Maybe String := nothing} {meta : Maybe String := nothing} : SemVer := - mkSemVer@?{ + mkSemVer@{ major; minor; patch; diff --git a/juvix-stdlib b/juvix-stdlib index 0c456725a2..ff6d964320 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 0c456725a23648606f97aebf8f74a9e2a73e90b6 +Subproject commit ff6d964320d24e3e8010733afcd886a62a56dd70 diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs index 828f67bfeb..0c145247cb 100644 --- a/src/Juvix/Compiler/Concrete/Gen.hs +++ b/src/Juvix/Compiler/Concrete/Gen.hs @@ -67,16 +67,6 @@ smallUniverseExpression = do _expressionAtoms = pure (AtomUniverse (smallUniverse loc)) } -isExhaustive :: (Member (Reader Interval) r) => Bool -> Sem r IsExhaustive -isExhaustive _isExhaustive = do - _isExhaustiveKw <- - Irrelevant - <$> if - | _isExhaustive -> kw kwAt - | otherwise -> kw kwAtQuestion - - return IsExhaustive {..} - symbol :: (Member (Reader Interval) r) => Text -> Sem r Symbol symbol t = do l <- ask @@ -107,25 +97,13 @@ braced a = do l <- ask AtomBraces . WithLoc l <$> expressionAtoms' a -mkIsExhaustive :: (Member (Reader Interval) r) => Bool -> Sem r IsExhaustive -mkIsExhaustive _isExhaustive = do - keyw <- - if - | _isExhaustive -> kw kwAt - | otherwise -> kw kwAtQuestion - return - IsExhaustive - { _isExhaustiveKw = Irrelevant keyw, - _isExhaustive - } - -namedApplication :: Name -> IsExhaustive -> [NamedArgumentNew 'Parsed] -> ExpressionAtom 'Parsed -namedApplication n exh as = - AtomNamedApplicationNew - NamedApplicationNew - { _namedApplicationNewName = n, - _namedApplicationNewExhaustive = exh, - _namedApplicationNewArguments = as +namedApplication :: Name -> Irrelevant KeywordRef -> [NamedArgument 'Parsed] -> ExpressionAtom 'Parsed +namedApplication n kwd as = + AtomNamedApplication + NamedApplication + { _namedApplicationName = n, + _namedApplicationAtKw = kwd, + _namedApplicationArguments = as } literalInteger :: (Member (Reader Interval) r, Integral a) => a -> Sem r (ExpressionAtom 'Parsed) diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index 13bbc43089..d5ac822396 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -28,7 +28,6 @@ import Juvix.Data.Keyword.All kwAssign, kwAssoc, kwAt, - kwAtQuestion, kwAxiom, kwBelow, kwBinary, @@ -88,7 +87,6 @@ reservedKeywords = kwAssign, kwDeriving, kwAt, - kwAtQuestion, kwAxiom, kwCase, kwColon, diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 357d393bc9..c61e9c583a 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -1635,7 +1635,7 @@ data Expression | ExpressionBraces (WithLoc Expression) | ExpressionDoubleBraces (DoubleBracesExpression 'Scoped) | ExpressionIterator (Iterator 'Scoped) - | ExpressionNamedApplicationNew (NamedApplicationNew 'Scoped) + | ExpressionNamedApplication (NamedApplication 'Scoped) deriving stock (Show, Eq, Ord, Generic) instance Serialize Expression @@ -2537,67 +2537,57 @@ deriving stock instance Ord (NamedArgumentPun 'Parsed) deriving stock instance Ord (NamedArgumentPun 'Scoped) -data NamedArgumentNew (s :: Stage) - = NamedArgumentNewFunction (NamedArgumentFunctionDef s) +data NamedArgument (s :: Stage) + = NamedArgumentFunction (NamedArgumentFunctionDef s) | NamedArgumentItemPun (NamedArgumentPun s) deriving stock (Generic) -instance Serialize (NamedArgumentNew 'Scoped) +instance Serialize (NamedArgument 'Scoped) -instance NFData (NamedArgumentNew 'Scoped) +instance NFData (NamedArgument 'Scoped) -instance Serialize (NamedArgumentNew 'Parsed) +instance Serialize (NamedArgument 'Parsed) -instance NFData (NamedArgumentNew 'Parsed) +instance NFData (NamedArgument 'Parsed) -deriving stock instance Show (NamedArgumentNew 'Parsed) +deriving stock instance Show (NamedArgument 'Parsed) -deriving stock instance Show (NamedArgumentNew 'Scoped) +deriving stock instance Show (NamedArgument 'Scoped) -deriving stock instance Eq (NamedArgumentNew 'Parsed) +deriving stock instance Eq (NamedArgument 'Parsed) -deriving stock instance Eq (NamedArgumentNew 'Scoped) +deriving stock instance Eq (NamedArgument 'Scoped) -deriving stock instance Ord (NamedArgumentNew 'Parsed) +deriving stock instance Ord (NamedArgument 'Parsed) -deriving stock instance Ord (NamedArgumentNew 'Scoped) +deriving stock instance Ord (NamedArgument 'Scoped) -data IsExhaustive = IsExhaustive - { _isExhaustive :: Bool, - _isExhaustiveKw :: Irrelevant KeywordRef - } - deriving stock (Eq, Show, Ord, Generic) - -instance Serialize IsExhaustive - -instance NFData IsExhaustive - -data NamedApplicationNew (s :: Stage) = NamedApplicationNew - { _namedApplicationNewName :: IdentifierType s, - _namedApplicationNewExhaustive :: IsExhaustive, - _namedApplicationNewArguments :: [NamedArgumentNew s] +data NamedApplication (s :: Stage) = NamedApplication + { _namedApplicationName :: IdentifierType s, + _namedApplicationAtKw :: Irrelevant KeywordRef, + _namedApplicationArguments :: [NamedArgument s] } deriving stock (Generic) -instance Serialize (NamedApplicationNew 'Scoped) +instance Serialize (NamedApplication 'Scoped) -instance NFData (NamedApplicationNew 'Scoped) +instance NFData (NamedApplication 'Scoped) -instance Serialize (NamedApplicationNew 'Parsed) +instance Serialize (NamedApplication 'Parsed) -instance NFData (NamedApplicationNew 'Parsed) +instance NFData (NamedApplication 'Parsed) -deriving stock instance Show (NamedApplicationNew 'Parsed) +deriving stock instance Show (NamedApplication 'Parsed) -deriving stock instance Show (NamedApplicationNew 'Scoped) +deriving stock instance Show (NamedApplication 'Scoped) -deriving stock instance Eq (NamedApplicationNew 'Parsed) +deriving stock instance Eq (NamedApplication 'Parsed) -deriving stock instance Eq (NamedApplicationNew 'Scoped) +deriving stock instance Eq (NamedApplication 'Scoped) -deriving stock instance Ord (NamedApplicationNew 'Parsed) +deriving stock instance Ord (NamedApplication 'Parsed) -deriving stock instance Ord (NamedApplicationNew 'Scoped) +deriving stock instance Ord (NamedApplication 'Scoped) data RecordSyntaxDef (s :: Stage) = RecordSyntaxOperator (OperatorSyntaxDef s) @@ -2741,7 +2731,7 @@ data ExpressionAtom (s :: Stage) | AtomLiteral LiteralLoc | AtomParens (ExpressionType s) | AtomIterator (Iterator s) - | AtomNamedApplicationNew (NamedApplicationNew s) + | AtomNamedApplication (NamedApplication s) deriving stock (Generic) instance Serialize (ExpressionAtom 'Parsed) @@ -3000,7 +2990,6 @@ makeLenses ''FunctionLhs makeLenses ''Statements makeLenses ''NamedArgumentFunctionDef makeLenses ''NamedArgumentPun -makeLenses ''IsExhaustive makeLenses ''SideIfBranch makeLenses ''RhsExpression makeLenses ''PatternArg @@ -3069,8 +3058,8 @@ makeLenses ''Initializer makeLenses ''Range makeLenses ''ArgumentBlock makeLenses ''NamedArgumentAssign -makeLenses ''NamedArgumentNew -makeLenses ''NamedApplicationNew +makeLenses ''NamedArgument +makeLenses ''NamedApplication makeLenses ''AliasDef makeLenses ''FixitySyntaxDef makeLenses ''ParsedFixityInfo @@ -3083,7 +3072,7 @@ makeLenses ''RecordInfo makeLenses ''MarkdownInfo makeLenses ''Deriving -makePrisms ''NamedArgumentNew +makePrisms ''NamedArgument makePrisms ''ConstructorRhs makePrisms ''FunctionDefNameParsed @@ -3176,7 +3165,7 @@ instance (SingI s) => HasLoc (ArgumentBlock s) where instance HasAtomicity (ArgumentBlock s) where atomicity = const Atom -instance HasAtomicity (NamedApplicationNew s) where +instance HasAtomicity (NamedApplication s) where atomicity = const (Aggregate updateFixity) instance HasAtomicity (Do s) where @@ -3203,7 +3192,7 @@ instance HasAtomicity Expression where ExpressionCase c -> atomicity c ExpressionIf x -> atomicity x ExpressionIterator i -> atomicity i - ExpressionNamedApplicationNew i -> atomicity i + ExpressionNamedApplication i -> atomicity i ExpressionRecordUpdate {} -> Aggregate updateFixity ExpressionParensRecordUpdate {} -> Atom @@ -3414,9 +3403,9 @@ instance HasLoc (List s) where instance (SingI s) => HasLoc (NamedArgumentFunctionDef s) where getLoc (NamedArgumentFunctionDef f) = getLoc f -instance (SingI s) => HasLoc (NamedArgumentNew s) where +instance (SingI s) => HasLoc (NamedArgument s) where getLoc = \case - NamedArgumentNewFunction f -> getLoc f + NamedArgumentFunction f -> getLoc f NamedArgumentItemPun f -> getLoc f instance HasLoc (RecordUpdatePun s) where @@ -3425,8 +3414,8 @@ instance HasLoc (RecordUpdatePun s) where instance HasLoc (NamedArgumentPun s) where getLoc NamedArgumentPun {..} = getLocSymbolType _namedArgumentPunSymbol -instance (SingI s) => HasLoc (NamedApplicationNew s) where - getLoc NamedApplicationNew {..} = getLocIdentifierType _namedApplicationNewName +instance (SingI s) => HasLoc (NamedApplication s) where + getLoc NamedApplication {..} = getLocIdentifierType _namedApplicationName instance (SingI s) => HasLoc (RecordUpdateField s) where getLoc = \case @@ -3478,7 +3467,7 @@ instance HasLoc Expression where ExpressionBraces i -> getLoc i ExpressionDoubleBraces i -> getLoc i ExpressionIterator i -> getLoc i - ExpressionNamedApplicationNew i -> getLoc i + ExpressionNamedApplication i -> getLoc i ExpressionRecordUpdate i -> getLoc i ExpressionParensRecordUpdate i -> getLoc i @@ -3707,7 +3696,7 @@ instance (SingI s) => HasLoc (ExpressionAtom s) where AtomLiteral x -> getLoc x AtomParens x -> getLocExpressionType x AtomIterator x -> getLoc x - AtomNamedApplicationNew x -> getLoc x + AtomNamedApplication x -> getLoc x instance HasLoc (ExpressionAtoms s) where getLoc = getLoc . (^. expressionAtomsLoc) @@ -3769,17 +3758,17 @@ withFunctionSymbol a f sym = case sing :: SStage s of SParsed -> maybe a f (sym ^? _FunctionDefName) SScoped -> f (sym ^. functionDefNameScoped) -namedArgumentNewSymbolParsed :: (SingI s) => SimpleGetter (NamedArgumentNew s) Symbol -namedArgumentNewSymbolParsed = to $ \case +namedArgumentSymbolParsed :: (SingI s) => SimpleGetter (NamedArgument s) Symbol +namedArgumentSymbolParsed = to $ \case NamedArgumentItemPun a -> a ^. namedArgumentPunSymbol - NamedArgumentNewFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . functionDefName)) + NamedArgumentFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . functionDefName)) -namedArgumentNewSymbol :: Lens' (NamedArgumentNew 'Parsed) Symbol -namedArgumentNewSymbol f = \case +namedArgumentSymbol :: Lens' (NamedArgument 'Parsed) Symbol +namedArgumentSymbol f = \case NamedArgumentItemPun a -> NamedArgumentItemPun <$> (namedArgumentPunSymbol f a) - NamedArgumentNewFunction a -> do + NamedArgumentFunction a -> do a' <- f (a ^?! namedArgumentFunctionDef . functionDefName . _FunctionDefName) - return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set functionDefName (FunctionDefName a')) a) + return $ NamedArgumentFunction (over namedArgumentFunctionDef (set functionDefName (FunctionDefName a')) a) scopedIdenSrcName :: Lens' ScopedIden S.Name scopedIdenSrcName f n = case n ^. scopedIdenAlias of diff --git a/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs b/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs index 064754798f..2f253b6b23 100644 --- a/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs +++ b/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs @@ -81,12 +81,12 @@ instance IsApe Name ApeLeaf where _leafExpr = ApeLeafAtom (sing :&: AtomIdentifier n) } -instance (SingI s) => IsApe (NamedApplicationNew s) ApeLeaf where +instance (SingI s) => IsApe (NamedApplication s) ApeLeaf where toApe a = ApeLeaf $ Leaf { _leafAtomicity = atomicity a, - _leafExpr = ApeLeafAtom (sing :&: AtomNamedApplicationNew a) + _leafExpr = ApeLeafAtom (sing :&: AtomNamedApplication a) } instance IsApe Application ApeLeaf where @@ -144,7 +144,7 @@ instance IsApe Expression ApeLeaf where ExpressionInfixApplication a -> toApe a ExpressionPostfixApplication a -> toApe a ExpressionFunction a -> toApe a - ExpressionNamedApplicationNew a -> toApe a + ExpressionNamedApplication a -> toApe a ExpressionRecordUpdate a -> toApe a ExpressionParensRecordUpdate {} -> leaf ExpressionParensIdentifier {} -> leaf diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index ebe2624012..7ea873494c 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -347,18 +347,15 @@ instance (SingI s) => PrettyPrint (ArgumentBlock s) where where Irrelevant d = _argBlockDelims -instance PrettyPrint IsExhaustive where - ppCode IsExhaustive {..} = ppCode _isExhaustiveKw - -instance (SingI s) => PrettyPrint (NamedApplicationNew s) where - ppCode NamedApplicationNew {..} = do +instance (SingI s) => PrettyPrint (NamedApplication s) where + ppCode NamedApplication {..} = do let args' - | null _namedApplicationNewArguments = mempty - | otherwise = ppBlock _namedApplicationNewArguments + | null _namedApplicationArguments = mempty + | otherwise = ppBlock _namedApplicationArguments grouped ( align - ( ppIdentifierType _namedApplicationNewName - <> ppCode _namedApplicationNewExhaustive + ( ppIdentifierType _namedApplicationName + <> ppCode _namedApplicationAtKw <> braces args' ) ) @@ -372,9 +369,9 @@ instance PrettyPrint (RecordUpdatePun s) where instance PrettyPrint (NamedArgumentPun s) where ppCode = ppCode . (^. namedArgumentPunSymbol) -instance (SingI s) => PrettyPrint (NamedArgumentNew s) where +instance (SingI s) => PrettyPrint (NamedArgument s) where ppCode = \case - NamedArgumentNewFunction f -> ppCode f + NamedArgumentFunction f -> ppCode f NamedArgumentItemPun f -> ppCode f instance (SingI s) => PrettyPrint (RecordSyntaxDef s) where @@ -472,7 +469,7 @@ instance (SingI s) => PrettyPrint (ExpressionAtom s) where AtomHole w -> ppHoleType w AtomInstanceHole w -> ppHoleType w AtomIterator i -> ppIterator NotTop i - AtomNamedApplicationNew i -> ppCode i + AtomNamedApplication i -> ppCode i instance PrettyPrint PatternScopedIden where ppCode = \case @@ -1006,7 +1003,7 @@ instance PrettyPrint Expression where ExpressionCase c -> ppCase NotTop c ExpressionIf c -> ppIf NotTop c ExpressionIterator i -> ppIterator NotTop i - ExpressionNamedApplicationNew i -> ppCode i + ExpressionNamedApplication i -> ppCode i ExpressionRecordUpdate i -> ppCode i ExpressionParensRecordUpdate i -> ppCode i diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index b847e6ff8a..006144e12a 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -2911,22 +2911,22 @@ checkExpressionAtom e = case e of AtomLiteral l -> return (pure (AtomLiteral l)) AtomList l -> pure . AtomList <$> checkList l AtomIterator i -> pure . AtomIterator <$> checkIterator i - AtomNamedApplicationNew i -> pure . AtomNamedApplicationNew <$> checkNamedApplicationNew i + AtomNamedApplication i -> pure . AtomNamedApplication <$> checkNamedApplication i AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i -reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgumentNew 'Parsed -> Sem r () +reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgument 'Parsed -> Sem r () reserveNamedArgumentName a = case a of - NamedArgumentNewFunction f -> reserveFunctionLikeSymbol (f ^. namedArgumentFunctionDef) + NamedArgumentFunction f -> reserveFunctionLikeSymbol (f ^. namedArgumentFunctionDef) NamedArgumentItemPun {} -> return () -checkNamedApplicationNew :: +checkNamedApplication :: forall r. (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId] r) => - NamedApplicationNew 'Parsed -> - Sem r (NamedApplicationNew 'Scoped) -checkNamedApplicationNew napp = do - let nargs = napp ^. namedApplicationNewArguments - aname <- checkScopedIden (napp ^. namedApplicationNewName) + NamedApplication 'Parsed -> + Sem r (NamedApplication 'Scoped) +checkNamedApplication napp = do + let nargs = napp ^. namedApplicationArguments + aname <- checkScopedIden (napp ^. namedApplicationName) sig :: NameSignature 'Parsed <- if | null nargs -> return (NameSignature []) @@ -2937,25 +2937,25 @@ checkNamedApplicationNew napp = do ^.. nameSignatureArgs . each . nameBlockSymbols - forM_ nargs (checkNameInSignature namesInSignature . (^. namedArgumentNewSymbol)) - puns <- scopePuns (napp ^.. namedApplicationNewArguments . each . _NamedArgumentItemPun) + forM_ nargs (checkNameInSignature namesInSignature . (^. namedArgumentSymbol)) + puns <- scopePuns (napp ^.. namedApplicationArguments . each . _NamedArgumentItemPun) args' <- withLocalScope . localBindings . ignoreSyntax $ do mapM_ reserveNamedArgumentName nargs - mapM (checkNamedArgumentNew puns) nargs + mapM (checkNamedArgument puns) nargs let signatureExplicitNames = hashSet . concatMap (^.. nameBlockSymbols) . filter (not . isImplicitOrInstance . (^. nameBlockImplicit)) $ sig ^. nameSignatureArgs - givenNames :: HashSet Symbol = hashSet (map (^. namedArgumentNewSymbol) nargs) + givenNames :: HashSet Symbol = hashSet (map (^. namedArgumentSymbol) nargs) missingArgs = HashSet.difference signatureExplicitNames givenNames - unless (null missingArgs || not (napp ^. namedApplicationNewExhaustive . isExhaustive)) $ + unless (null missingArgs) $ throw (ErrMissingArgs (MissingArgs (aname ^. scopedIdenFinal . nameConcrete) missingArgs)) return - NamedApplicationNew - { _namedApplicationNewName = aname, - _namedApplicationNewArguments = args', - _namedApplicationNewExhaustive = napp ^. namedApplicationNewExhaustive + NamedApplication + { _namedApplicationName = aname, + _namedApplicationArguments = args', + _namedApplicationAtKw = napp ^. namedApplicationAtKw } where checkNameInSignature :: HashSet Symbol -> Symbol -> Sem r () @@ -2969,13 +2969,13 @@ checkNamedApplicationNew napp = do scopePun :: Symbol -> Sem r ScopedIden scopePun = checkScopedIden . NameUnqualified -checkNamedArgumentNew :: +checkNamedArgument :: (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId] r) => HashMap Symbol ScopedIden -> - NamedArgumentNew 'Parsed -> - Sem r (NamedArgumentNew 'Scoped) -checkNamedArgumentNew puns = \case - NamedArgumentNewFunction f -> NamedArgumentNewFunction <$> checkNamedArgumentFunctionDef f + NamedArgument 'Parsed -> + Sem r (NamedArgument 'Scoped) +checkNamedArgument puns = \case + NamedArgumentFunction f -> NamedArgumentFunction <$> checkNamedArgumentFunctionDef f NamedArgumentItemPun f -> return (NamedArgumentItemPun (checkNamedArgumentItemPun puns f)) checkNamedArgumentItemPun :: @@ -3599,11 +3599,11 @@ parseTerm = _ -> Nothing parseNamedApplicationNew :: Parse Expression - parseNamedApplicationNew = ExpressionNamedApplicationNew <$> P.token namedApp mempty + parseNamedApplicationNew = ExpressionNamedApplication <$> P.token namedApp mempty where - namedApp :: ExpressionAtom 'Scoped -> Maybe (NamedApplicationNew 'Scoped) + namedApp :: ExpressionAtom 'Scoped -> Maybe (NamedApplication 'Scoped) namedApp s = case s of - AtomNamedApplicationNew u -> Just u + AtomNamedApplication u -> Just u _ -> Nothing parseLet :: Parse Expression diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 19a5003b26..47d485b522 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -882,7 +882,7 @@ expressionAtom = P.label "" $ AtomLiteral <$> P.try literal <|> AtomIterator <$> iterator - <|> AtomNamedApplicationNew <$> namedApplicationNew + <|> AtomNamedApplication <$> namedApplication <|> AtomList <$> parseList <|> AtomIf <$> multiwayIf <|> AtomIdentifier <$> name @@ -1041,19 +1041,19 @@ pnamedArgumentItemPun = do -- | Parses zero or more named arguments. This function is necessary to avoid -- using excessive backtracking. -manyNamedArgumentNewRBrace :: +manyNamedArgumentRBrace :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => - ParsecS r [NamedArgumentNew 'Parsed] -manyNamedArgumentNewRBrace = reverse <$> go [] + ParsecS r [NamedArgument 'Parsed] +manyNamedArgumentRBrace = reverse <$> go [] where - go :: [NamedArgumentNew 'Parsed] -> ParsecS r [NamedArgumentNew 'Parsed] + go :: [NamedArgument 'Parsed] -> ParsecS r [NamedArgument 'Parsed] go acc = rbrace $> acc <|> itemHelper (P.try (withIsLast (NamedArgumentItemPun <$> pnamedArgumentItemPun))) - <|> itemHelper (withIsLast (NamedArgumentNewFunction <$> pnamedArgumentFunctionDef)) + <|> itemHelper (withIsLast (NamedArgumentFunction <$> pnamedArgumentFunctionDef)) where - itemHelper :: ParsecS r (Bool, NamedArgumentNew 'Parsed) -> ParsecS r [NamedArgumentNew 'Parsed] + itemHelper :: ParsecS r (Bool, NamedArgument 'Parsed) -> ParsecS r [NamedArgument 'Parsed] itemHelper p = do (isLast, item) <- p let acc' = item : acc @@ -1072,34 +1072,20 @@ manyNamedArgumentNewRBrace = reverse <$> go [] isLast <- pIsLast return (isLast, res) -pisExhaustive :: - forall r. - (Members '[ParserResultBuilder] r) => - ParsecS r IsExhaustive -pisExhaustive = do - (keyword, exh) <- - (,False) <$> kw kwAtQuestion - <|> (,True) <$> kw kwAt - return - IsExhaustive - { _isExhaustiveKw = Irrelevant keyword, - _isExhaustive = exh - } - -namedApplicationNew :: +namedApplication :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => - ParsecS r (NamedApplicationNew 'Parsed) -namedApplicationNew = P.label "" $ do + ParsecS r (NamedApplication 'Parsed) +namedApplication = P.label "" $ do checkNoNamedApplicationMissingAt - (_namedApplicationNewName, _namedApplicationNewExhaustive) <- P.try $ do + (_namedApplicationName, _namedApplicationAtKw) <- P.try $ do n <- name - exhaustive <- pisExhaustive + kwd <- Irrelevant <$> kw kwAt lbrace - return (n, exhaustive) - _namedApplicationNewArguments <- manyNamedArgumentNewRBrace - let _namedApplicationNewExtra = Irrelevant () - return NamedApplicationNew {..} + return (n, kwd) + _namedApplicationArguments <- manyNamedArgumentRBrace + let _namedApplicationExtra = Irrelevant () + return NamedApplication {..} hole :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (HoleType 'Parsed) hole = kw kwHole diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 505f9678b1..a88d4116af 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -1309,7 +1309,7 @@ goListPattern l = localBuiltins $ do where loc = getLoc l -createArgumentBlocks :: NonEmpty (NamedArgumentNew 'Scoped) -> [NameBlock 'Scoped] -> NonEmpty (ArgumentBlock 'Scoped) +createArgumentBlocks :: NonEmpty (NamedArgument 'Scoped) -> [NameBlock 'Scoped] -> NonEmpty (ArgumentBlock 'Scoped) createArgumentBlocks appargs = nonEmpty' . run @@ -1317,9 +1317,9 @@ createArgumentBlocks appargs = . evalState args0 . mapM_ goBlock where - namedArgumentRefSymbol :: NamedArgumentNew 'Scoped -> S.Symbol + namedArgumentRefSymbol :: NamedArgument 'Scoped -> S.Symbol namedArgumentRefSymbol = \case - NamedArgumentNewFunction p -> p ^. namedArgumentFunctionDef . functionDefName . functionDefNameScoped + NamedArgumentFunction p -> p ^. namedArgumentFunctionDef . functionDefName . functionDefNameScoped NamedArgumentItemPun p -> over S.nameConcrete fromUnqualified' (p ^. namedArgumentReferencedSymbol . scopedIdenFinal) args0 :: HashSet S.Symbol = hashSet (namedArgumentRefSymbol <$> appargs) goBlock :: @@ -1387,7 +1387,7 @@ goExpression = \case ExpressionHole h -> return (Internal.ExpressionHole h) ExpressionInstanceHole h -> return (Internal.ExpressionInstanceHole (fromHole h)) ExpressionIterator i -> goIterator i - ExpressionNamedApplicationNew i -> goNamedApplicationNew i [] + ExpressionNamedApplication i -> goNamedApplication i [] ExpressionRecordUpdate i -> goRecordUpdateApp i ExpressionParensRecordUpdate i -> Internal.ExpressionLambda <$> goRecordUpdate (i ^. parensRecordUpdate) where @@ -1396,19 +1396,19 @@ goExpression = \case s <- asks (^. S.infoNameSigs) runReader s (runNamedArguments fun blocks extraArgs) >>= goDesugaredNamedApplication - goNamedApplicationNew :: - Concrete.NamedApplicationNew 'Scoped -> + goNamedApplication :: + Concrete.NamedApplication 'Scoped -> [Internal.ApplicationArg] -> Sem r Internal.Expression - goNamedApplicationNew napp extraArgs = case nonEmpty (napp ^. namedApplicationNewArguments) of - Nothing -> return (goIden (napp ^. namedApplicationNewName)) + goNamedApplication napp extraArgs = case nonEmpty (napp ^. namedApplicationArguments) of + Nothing -> return (goIden (napp ^. namedApplicationName)) Just appargs -> do - let name = napp ^. namedApplicationNewName . scopedIdenFinal + let name = napp ^. namedApplicationName . scopedIdenFinal sig <- fromJust <$> asks (^. S.infoNameSigs . at (name ^. S.nameId)) - let fun = napp ^. namedApplicationNewName + let fun = napp ^. namedApplicationName blocks = createArgumentBlocks appargs (sig ^. nameSignatureArgs) compiledNameApp <- goNamedApplication' fun blocks extraArgs - case nonEmpty (appargs ^.. each . _NamedArgumentNewFunction) of + case nonEmpty (appargs ^.. each . _NamedArgumentFunction) of Nothing -> return compiledNameApp Just funs -> do cls <- funDefsToClauses funs @@ -1650,7 +1650,7 @@ goExpression = \case let (f, args) = unfoldApp a args' <- toList <$> mapM goApplicationArg args case f of - ExpressionNamedApplicationNew n -> goNamedApplicationNew n args' + ExpressionNamedApplication n -> goNamedApplication n args' _ -> do f' <- goExpression f return (Internal.foldApplication f' args') diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs b/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs index 6f70e8e374..9f63205073 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs @@ -116,9 +116,9 @@ v1v2FromPackage p = run . runReader l $ do Sem r (NonEmpty (ExpressionAtom 'Parsed)) defaultPackageWithArgs as = do defaultPackageName' <- NameUnqualified <$> symbol defaultPackageStr - exhaustive <- mkIsExhaustive False - let args = fmap (NamedArgumentNewFunction . NamedArgumentFunctionDef) as - defaultPackageArg = namedApplication defaultPackageName' exhaustive (toList args) + kwd <- kw kwAt + let args = fmap (NamedArgumentFunction . NamedArgumentFunctionDef) as + defaultPackageArg = namedApplication defaultPackageName' (Irrelevant kwd) (toList args) return (defaultPackageArg :| []) l :: Interval diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index cb5541eab3..cfac78a381 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -61,9 +61,6 @@ kwExclamation = asciiKw Str.exclamation kwAt :: Keyword kwAt = asciiKw Str.at_ -kwAtQuestion :: Keyword -kwAtQuestion = asciiKw Str.atQuestion - kwAxiom :: Keyword kwAxiom = asciiKw Str.axiom diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index a3ca02cbb2..36df2a8be6 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -653,9 +653,6 @@ underscore = "_" at_ :: (IsString s) => s at_ = "@" -atQuestion :: (IsString s) => s -atQuestion = "@?" - dot :: (IsString s) => s dot = "." diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index b87950a646..4703377126 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -223,7 +223,7 @@ scoperErrorTests = "Missing argument" $(mkRelDir ".") $(mkRelFile "MissingArgument.juvix") - $ wantsError ErrNamedArgumentsError, + $ wantsError ErrMissingArgs, negTest "Repeated name in name signature" $(mkRelDir ".") diff --git a/tests/Anoma/Compilation/positive/Package.juvix b/tests/Anoma/Compilation/positive/Package.juvix index 39b0d6b001..b1b787384a 100644 --- a/tests/Anoma/Compilation/positive/Package.juvix +++ b/tests/Anoma/Compilation/positive/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "positive"; }; diff --git a/tests/Anoma/Compilation/positive/test067.juvix b/tests/Anoma/Compilation/positive/test067.juvix index 5c1b90d87d..2c72c42842 100644 --- a/tests/Anoma/Compilation/positive/test067.juvix +++ b/tests/Anoma/Compilation/positive/test067.juvix @@ -6,6 +6,6 @@ import Stdlib.Data.Nat open; f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c; main : Nat := - f@?{ + f@{ c := 5 }; diff --git a/tests/Anoma/Compilation/positive/test069.juvix b/tests/Anoma/Compilation/positive/test069.juvix index 3500b88af9..0fce3fcef3 100644 --- a/tests/Anoma/Compilation/positive/test069.juvix +++ b/tests/Anoma/Compilation/positive/test069.juvix @@ -23,7 +23,7 @@ mkOrdHelper : Ord A := mkOrd cmp lt gt; ordNatNamed : Ord Nat := - mkOrdHelper@?{ + mkOrdHelper@{ cmp := Ord.compare }; diff --git a/tests/Anoma/Compilation/positive/test070.juvix b/tests/Anoma/Compilation/positive/test070.juvix index 9a9b0f653e..a969a12453 100644 --- a/tests/Anoma/Compilation/positive/test070.juvix +++ b/tests/Anoma/Compilation/positive/test070.juvix @@ -6,13 +6,13 @@ import Stdlib.Data.Nat open; fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c; main : Nat := - fun@?{ + fun@{ a := fun; b := - fun@?{ + fun@{ b := 3 } - * fun@?{ + * fun@{ b := fun {2} } }; diff --git a/tests/Anoma/Compilation/positive/test071.juvix b/tests/Anoma/Compilation/positive/test071.juvix index e24bf1ec60..a3f6207795 100644 --- a/tests/Anoma/Compilation/positive/test071.juvix +++ b/tests/Anoma/Compilation/positive/test071.juvix @@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d; main : Nat := fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} + - f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 + - h@?{b := 4} 1; + f@{c := 5} + \{c := g@{b := 4; c}} 3 + ite (Ord.lt 1 0) 1 0 + + \{c := h@{b := 4; c}} 1; diff --git a/tests/Anoma/Compilation/positive/test072/Package.juvix b/tests/Anoma/Compilation/positive/test072/Package.juvix index 16589dc288..398af60eb6 100644 --- a/tests/Anoma/Compilation/positive/test072/Package.juvix +++ b/tests/Anoma/Compilation/positive/test072/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "monads" }; diff --git a/tests/Anoma/Compilation/positive/test073/Package.juvix b/tests/Anoma/Compilation/positive/test073/Package.juvix index eec3c8b6d8..2957205c2f 100644 --- a/tests/Anoma/Compilation/positive/test073/Package.juvix +++ b/tests/Anoma/Compilation/positive/test073/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test073" }; diff --git a/tests/Anoma/Compilation/positive/test085/Package.juvix b/tests/Anoma/Compilation/positive/test085/Package.juvix index 613da5f3b1..5cb6655c31 100644 --- a/tests/Anoma/Compilation/positive/test085/Package.juvix +++ b/tests/Anoma/Compilation/positive/test085/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test085"; dependencies := [defaultStdlib; path "client/"]; }; diff --git a/tests/Anoma/Compilation/positive/test085/client/Package.juvix b/tests/Anoma/Compilation/positive/test085/client/Package.juvix index 7a1c28caf9..8a384a4fdd 100644 --- a/tests/Anoma/Compilation/positive/test085/client/Package.juvix +++ b/tests/Anoma/Compilation/positive/test085/client/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "addtransaction"; }; diff --git a/tests/Casm/Compilation/positive/test067.juvix b/tests/Casm/Compilation/positive/test067.juvix index 5c1b90d87d..2c72c42842 100644 --- a/tests/Casm/Compilation/positive/test067.juvix +++ b/tests/Casm/Compilation/positive/test067.juvix @@ -6,6 +6,6 @@ import Stdlib.Data.Nat open; f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c; main : Nat := - f@?{ + f@{ c := 5 }; diff --git a/tests/Casm/Compilation/positive/test069.juvix b/tests/Casm/Compilation/positive/test069.juvix index 3ed821fd77..965abebcfa 100644 --- a/tests/Casm/Compilation/positive/test069.juvix +++ b/tests/Casm/Compilation/positive/test069.juvix @@ -23,7 +23,7 @@ mkOrdHelper : Ord A := mkOrd cmp lt gt; ordNatNamed : Ord Nat := - mkOrdHelper@?{ + mkOrdHelper@{ cmp := Ord.compare }; diff --git a/tests/Casm/Compilation/positive/test070.juvix b/tests/Casm/Compilation/positive/test070.juvix index 9a9b0f653e..a969a12453 100644 --- a/tests/Casm/Compilation/positive/test070.juvix +++ b/tests/Casm/Compilation/positive/test070.juvix @@ -6,13 +6,13 @@ import Stdlib.Data.Nat open; fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c; main : Nat := - fun@?{ + fun@{ a := fun; b := - fun@?{ + fun@{ b := 3 } - * fun@?{ + * fun@{ b := fun {2} } }; diff --git a/tests/Casm/Compilation/positive/test071.juvix b/tests/Casm/Compilation/positive/test071.juvix index e24bf1ec60..a3f6207795 100644 --- a/tests/Casm/Compilation/positive/test071.juvix +++ b/tests/Casm/Compilation/positive/test071.juvix @@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d; main : Nat := fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} + - f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 + - h@?{b := 4} 1; + f@{c := 5} + \{c := g@{b := 4; c}} 3 + ite (Ord.lt 1 0) 1 0 + + \{c := h@{b := 4; c}} 1; diff --git a/tests/Casm/Compilation/positive/test072/Package.juvix b/tests/Casm/Compilation/positive/test072/Package.juvix index 16589dc288..398af60eb6 100644 --- a/tests/Casm/Compilation/positive/test072/Package.juvix +++ b/tests/Casm/Compilation/positive/test072/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "monads" }; diff --git a/tests/Casm/Compilation/positive/test073/Package.juvix b/tests/Casm/Compilation/positive/test073/Package.juvix index eec3c8b6d8..2957205c2f 100644 --- a/tests/Casm/Compilation/positive/test073/Package.juvix +++ b/tests/Casm/Compilation/positive/test073/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test073" }; diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix index 4aa0406cd0..0fc77ee840 100644 --- a/tests/Compilation/positive/test061.juvix +++ b/tests/Compilation/positive/test061.juvix @@ -12,7 +12,7 @@ Bool' : Type := Bool; instance showStringI : Show String := - mkShow@?{ + mkShow@{ show := id }; @@ -24,7 +24,7 @@ showBoolI : Show' Bool' := instance showNatI : Show Nat := - mkShow@?{ + mkShow@{ show := natToString }; @@ -97,7 +97,7 @@ main : IO := >>> printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >>> printStringLn (f'3 "abba") >>> printStringLn - (f'3@?{ + (f'3@{ M := mkShow λ {x := x ++str "!"} } "abba") diff --git a/tests/Compilation/positive/test067.juvix b/tests/Compilation/positive/test067.juvix index de3721c21d..f761d569cf 100644 --- a/tests/Compilation/positive/test067.juvix +++ b/tests/Compilation/positive/test067.juvix @@ -7,6 +7,6 @@ f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c; main : Nat := - f@?{ + f@{ c := 5 }; diff --git a/tests/Compilation/positive/test069.juvix b/tests/Compilation/positive/test069.juvix index 3500b88af9..0fce3fcef3 100644 --- a/tests/Compilation/positive/test069.juvix +++ b/tests/Compilation/positive/test069.juvix @@ -23,7 +23,7 @@ mkOrdHelper : Ord A := mkOrd cmp lt gt; ordNatNamed : Ord Nat := - mkOrdHelper@?{ + mkOrdHelper@{ cmp := Ord.compare }; diff --git a/tests/Compilation/positive/test070.juvix b/tests/Compilation/positive/test070.juvix index a7fe2c428d..76fcf68ba3 100644 --- a/tests/Compilation/positive/test070.juvix +++ b/tests/Compilation/positive/test070.juvix @@ -6,13 +6,13 @@ import Stdlib.Data.Nat open; fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c; main : Nat := - fun@?{ + fun@{ a := fun; b := - fun@?{ + fun@{ b := 3; } - * fun@?{ + * fun@{ b := fun {2}; }; }; diff --git a/tests/Compilation/positive/test071.juvix b/tests/Compilation/positive/test071.juvix index 0cbb9e7dbf..caddcbbdc5 100644 --- a/tests/Compilation/positive/test071.juvix +++ b/tests/Compilation/positive/test071.juvix @@ -57,12 +57,16 @@ main : Nat := + f@{ c := 5; } - + g@?{ - b := 4; - } + + \{c := + g@{ + b := 4; + c; + }} 3 + ite (Ord.lt 1 0) 1 0 - + h@?{ - b := 4; - } + + \{c := + h@{ + b := 4; + c; + }} 1; diff --git a/tests/Compilation/positive/test072/Package.juvix b/tests/Compilation/positive/test072/Package.juvix index 16589dc288..398af60eb6 100644 --- a/tests/Compilation/positive/test072/Package.juvix +++ b/tests/Compilation/positive/test072/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "monads" }; diff --git a/tests/Compilation/positive/test073/Package.juvix b/tests/Compilation/positive/test073/Package.juvix index eec3c8b6d8..2957205c2f 100644 --- a/tests/Compilation/positive/test073/Package.juvix +++ b/tests/Compilation/positive/test073/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test073" }; diff --git a/tests/Internal/positive/Dependencies/Dep1/Package.juvix b/tests/Internal/positive/Dependencies/Dep1/Package.juvix index bd6138a7a3..a8be479651 100644 --- a/tests/Internal/positive/Dependencies/Dep1/Package.juvix +++ b/tests/Internal/positive/Dependencies/Dep1/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "dep1"; dependencies := [] }; diff --git a/tests/Internal/positive/Dependencies/Dep2/Package.juvix b/tests/Internal/positive/Dependencies/Dep2/Package.juvix index a32d05f4db..99c5086184 100644 --- a/tests/Internal/positive/Dependencies/Dep2/Package.juvix +++ b/tests/Internal/positive/Dependencies/Dep2/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "dep2"; dependencies := [] }; diff --git a/tests/Rust/Compilation/positive/test067.juvix b/tests/Rust/Compilation/positive/test067.juvix index 5c1b90d87d..2c72c42842 100644 --- a/tests/Rust/Compilation/positive/test067.juvix +++ b/tests/Rust/Compilation/positive/test067.juvix @@ -6,6 +6,6 @@ import Stdlib.Data.Nat open; f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c; main : Nat := - f@?{ + f@{ c := 5 }; diff --git a/tests/Rust/Compilation/positive/test069.juvix b/tests/Rust/Compilation/positive/test069.juvix index 3ed821fd77..965abebcfa 100644 --- a/tests/Rust/Compilation/positive/test069.juvix +++ b/tests/Rust/Compilation/positive/test069.juvix @@ -23,7 +23,7 @@ mkOrdHelper : Ord A := mkOrd cmp lt gt; ordNatNamed : Ord Nat := - mkOrdHelper@?{ + mkOrdHelper@{ cmp := Ord.compare }; diff --git a/tests/Rust/Compilation/positive/test070.juvix b/tests/Rust/Compilation/positive/test070.juvix index 9a9b0f653e..a969a12453 100644 --- a/tests/Rust/Compilation/positive/test070.juvix +++ b/tests/Rust/Compilation/positive/test070.juvix @@ -6,13 +6,13 @@ import Stdlib.Data.Nat open; fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c; main : Nat := - fun@?{ + fun@{ a := fun; b := - fun@?{ + fun@{ b := 3 } - * fun@?{ + * fun@{ b := fun {2} } }; diff --git a/tests/Rust/Compilation/positive/test071.juvix b/tests/Rust/Compilation/positive/test071.juvix index e24bf1ec60..a3f6207795 100644 --- a/tests/Rust/Compilation/positive/test071.juvix +++ b/tests/Rust/Compilation/positive/test071.juvix @@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d; main : Nat := fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} + - f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 + - h@?{b := 4} 1; + f@{c := 5} + \{c := g@{b := 4; c}} 3 + ite (Ord.lt 1 0) 1 0 + + \{c := h@{b := 4; c}} 1; diff --git a/tests/Rust/Compilation/positive/test072/Package.juvix b/tests/Rust/Compilation/positive/test072/Package.juvix index 16589dc288..398af60eb6 100644 --- a/tests/Rust/Compilation/positive/test072/Package.juvix +++ b/tests/Rust/Compilation/positive/test072/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "monads" }; diff --git a/tests/Rust/Compilation/positive/test073/Package.juvix b/tests/Rust/Compilation/positive/test073/Package.juvix index eec3c8b6d8..2957205c2f 100644 --- a/tests/Rust/Compilation/positive/test073/Package.juvix +++ b/tests/Rust/Compilation/positive/test073/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test073" }; diff --git a/tests/negative/DuplicateArgument.juvix b/tests/negative/DuplicateArgument.juvix index 362ce08e77..2a0fa6ed83 100644 --- a/tests/negative/DuplicateArgument.juvix +++ b/tests/negative/DuplicateArgument.juvix @@ -5,7 +5,7 @@ type T := t : T; f (a : T) : T := t; x : T := - f@?{ + f@{ a := t; a := t }; diff --git a/tests/negative/MissingArgument.juvix b/tests/negative/MissingArgument.juvix index b31fe67e18..5228425089 100644 --- a/tests/negative/MissingArgument.juvix +++ b/tests/negative/MissingArgument.juvix @@ -5,6 +5,6 @@ type T := t : T; f (a : T) (b : T) : T := t; x : T := - f@?{ + f@{ b := t }; diff --git a/tests/negative/NoDependencies/Package.juvix b/tests/negative/NoDependencies/Package.juvix index a6223b86a4..cfab3cce78 100644 --- a/tests/negative/NoDependencies/Package.juvix +++ b/tests/negative/NoDependencies/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [] }; diff --git a/tests/negative/NoNamedArguments.juvix b/tests/negative/NoNamedArguments.juvix index 367e11e4a3..b895aeb437 100644 --- a/tests/negative/NoNamedArguments.juvix +++ b/tests/negative/NoNamedArguments.juvix @@ -2,6 +2,6 @@ module NoNamedArguments; axiom T : Type; -axiom B : T@?{ +axiom B : T@{ x := Type }; diff --git a/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix b/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix index 8005e06fd7..2cefd28b35 100644 --- a/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix +++ b/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix @@ -2,6 +2,6 @@ module Package; import PackageDescription.V2 open; -package : Package := defaultPackage@?{name := "abc"; version := mkVersion 0 0 1 ; dependencies := [ github "org" "repo" "ref1" ; github "org" "repo" "ref2" ]}; +package : Package := defaultPackage@{name := "abc"; version := mkVersion 0 0 1 ; dependencies := [ github "org" "repo" "ref1" ; github "org" "repo" "ref2" ]}; main : Package := package; diff --git a/tests/negative/UnexpectedArgument.juvix b/tests/negative/UnexpectedArgument.juvix index 4bc72c7ef4..10fb1b7096 100644 --- a/tests/negative/UnexpectedArgument.juvix +++ b/tests/negative/UnexpectedArgument.juvix @@ -5,6 +5,6 @@ type T := t : T; f (a : T) : T := t; x : T := - f@?{ + f@{ x := t }; diff --git a/tests/negative/UnexpectedArgumentWildcard.juvix b/tests/negative/UnexpectedArgumentWildcard.juvix index 52921d51d1..9487c9a9d8 100644 --- a/tests/negative/UnexpectedArgumentWildcard.juvix +++ b/tests/negative/UnexpectedArgumentWildcard.juvix @@ -6,7 +6,7 @@ f (a : T) : {_ : Type} -> (b : T) -> T | b := t; x : T := - f@?{ + f@{ a := t; b := t }; diff --git a/tests/negative/issue2771/Package.juvix b/tests/negative/issue2771/Package.juvix index a92a023e82..03b434d675 100644 --- a/tests/negative/issue2771/Package.juvix +++ b/tests/negative/issue2771/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "issue2771" }; diff --git a/tests/negative/issue3161/Package.juvix b/tests/negative/issue3161/Package.juvix index 91d7741540..5df850b097 100644 --- a/tests/negative/issue3161/Package.juvix +++ b/tests/negative/issue3161/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "stdlib"; version := mkVersion 0 0 1; dependencies := [] diff --git a/tests/positive/ConfluentScoping/Package.juvix b/tests/positive/ConfluentScoping/Package.juvix index 2bf8b10d1e..84bdf2b93b 100644 --- a/tests/positive/ConfluentScoping/Package.juvix +++ b/tests/positive/ConfluentScoping/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "confluentscoping" }; diff --git a/tests/positive/Dependencies/.libs/Extra/Package.juvix b/tests/positive/Dependencies/.libs/Extra/Package.juvix index 2bfda863c1..f0d985b351 100644 --- a/tests/positive/Dependencies/.libs/Extra/Package.juvix +++ b/tests/positive/Dependencies/.libs/Extra/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "extra"; version := mkVersion 1 0 0; dependencies := [defaultStdlib; path "../Base"] diff --git a/tests/positive/Dependencies/Package.juvix b/tests/positive/Dependencies/Package.juvix index 338e18b9d8..438c552fc3 100644 --- a/tests/positive/Dependencies/Package.juvix +++ b/tests/positive/Dependencies/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "main-project"; version := mkVersion 0 0 1; dependencies := diff --git a/tests/positive/FancyPaths/Package.juvix b/tests/positive/FancyPaths/Package.juvix index 8cac8ffad8..6317db5113 100644 --- a/tests/positive/FancyPaths/Package.juvix +++ b/tests/positive/FancyPaths/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [ path "../FancyPaths/././path with spaces" ; path "$(JUVIX_TEST_PATH)/../$(JUVIX_TEST_PATH)/" diff --git a/tests/positive/FancyPaths/home/Package.juvix b/tests/positive/FancyPaths/home/Package.juvix index a6223b86a4..cfab3cce78 100644 --- a/tests/positive/FancyPaths/home/Package.juvix +++ b/tests/positive/FancyPaths/home/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [] }; diff --git a/tests/positive/FancyPaths/other dep/Package.juvix b/tests/positive/FancyPaths/other dep/Package.juvix index a6223b86a4..cfab3cce78 100644 --- a/tests/positive/FancyPaths/other dep/Package.juvix +++ b/tests/positive/FancyPaths/other dep/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [] }; diff --git a/tests/positive/FancyPaths/path with spaces/Package.juvix b/tests/positive/FancyPaths/path with spaces/Package.juvix index a6223b86a4..cfab3cce78 100644 --- a/tests/positive/FancyPaths/path with spaces/Package.juvix +++ b/tests/positive/FancyPaths/path with spaces/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [] }; diff --git a/tests/positive/ImportNestedLocalModule/Package.juvix b/tests/positive/ImportNestedLocalModule/Package.juvix index 59641083b1..a74778ee7f 100644 --- a/tests/positive/ImportNestedLocalModule/Package.juvix +++ b/tests/positive/ImportNestedLocalModule/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test074" }; diff --git a/tests/positive/Internal/Positivity2/Package.juvix b/tests/positive/Internal/Positivity2/Package.juvix index dc768cdde3..52600bdb7c 100644 --- a/tests/positive/Internal/Positivity2/Package.juvix +++ b/tests/positive/Internal/Positivity2/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "positivity2"; dependencies := [] }; diff --git a/tests/positive/Isabelle/Package.juvix b/tests/positive/Isabelle/Package.juvix index b692045cc2..1ac1d4bb85 100644 --- a/tests/positive/Isabelle/Package.juvix +++ b/tests/positive/Isabelle/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "isabelle" }; diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md index f0c03c84c4..17d4080331 100644 --- a/tests/positive/Markdown/markdown/Test.md +++ b/tests/positive/Markdown/markdown/Test.md @@ -23,7 +23,7 @@ You can pass a number to the `extract-module-statements` attribute to drop that Commands like `typecheck` and `compile` can be used with Juvix Markdown files. -
main : IO := readLn (printNatLn << fibonacci << stringToNat);
+
main : IO := readLn (printNatLn << fibonacci << stringToNat);
Other code blocks are not touched, e.g: diff --git a/tests/positive/MarkdownImport/Package.juvix b/tests/positive/MarkdownImport/Package.juvix index b1daecbbdc..39e9528bf2 100644 --- a/tests/positive/MarkdownImport/Package.juvix +++ b/tests/positive/MarkdownImport/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "MarkdownImport" }; diff --git a/tests/positive/NamedArguments.juvix b/tests/positive/NamedArguments.juvix index 2365591bca..f158ae319e 100644 --- a/tests/positive/NamedArguments.juvix +++ b/tests/positive/NamedArguments.juvix @@ -22,7 +22,7 @@ axiom fun1 : (a : Type) -> (b : Type) -> {c : Type} -> Type; -- all provided by name t1 : Type := - fun1@?{ + fun1@{ a := A; b := B; c := C @@ -30,7 +30,7 @@ t1 : Type := -- skip implicit at the end t1' : {_ : Type} -> Type := - fun1@?{ + fun1@{ b := B; a := A }; @@ -43,7 +43,7 @@ axiom fun2 : (a : Type) -- skip implicit in implicit group t2 : {_ : Type} -> Type := - fun2@?{ + fun2@{ a := A; b := B; c := D @@ -57,7 +57,7 @@ axiom fun3 : (a : Type) -- skip implicit in the middle t3 : Type := - fun3@?{ + fun3@{ a := A; b := B; d := unit @@ -71,7 +71,7 @@ axiom fun4 : (a : Type) -- skip implicit in the middle t4 : Type := - fun4@?{ + fun4@{ a := A; b := B; d := unit @@ -85,7 +85,7 @@ axiom fun5 : (a : Type) -> Type; t5 : Type := - fun5@?{ + fun5@{ a := A; b := B; d' := unit; @@ -93,7 +93,7 @@ t5 : Type := }; t5' : Type := - fun5@?{ + fun5@{ a := A; b := B; d' := unit; @@ -109,7 +109,7 @@ axiom fun6 : {a : Type} -> Type; t6 : Type := - fun6@?{ + fun6@{ b := B; d' := unit; d := unit; @@ -117,7 +117,7 @@ t6 : Type := }; t6' : Type := - fun6@?{ + fun6@{ d' := unit; d := unit; a' := unit; @@ -129,18 +129,18 @@ module FakeRecord; mkPair : (fst : A) -> (snd : B) -> Pair A B; pp - : Pair@?{ + : Pair@{ B := Unit; A := Type } := - mkPair@?{ + mkPair@{ snd := unit; fst := Type }; pp2 - : Pair@?{ + : Pair@{ B := Unit; A := Type - } := mkPair@?{fst := Type} (unit); + } := \{snd := mkPair@{fst := Type; snd}} (unit); end; diff --git a/tests/positive/NoDependencies/Package.juvix b/tests/positive/NoDependencies/Package.juvix index a6223b86a4..cfab3cce78 100644 --- a/tests/positive/NoDependencies/Package.juvix +++ b/tests/positive/NoDependencies/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [] }; diff --git a/tests/positive/PackageLoader/PackageJuvix/Package.juvix b/tests/positive/PackageLoader/PackageJuvix/Package.juvix index 4560e71afe..99c18816d8 100644 --- a/tests/positive/PackageLoader/PackageJuvix/Package.juvix +++ b/tests/positive/PackageLoader/PackageJuvix/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V1 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "package-juvix" }; diff --git a/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix b/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix index 4560e71afe..99c18816d8 100644 --- a/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix +++ b/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V1 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "package-juvix" }; diff --git a/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix b/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix index cfc67ae272..8e5ddde7ca 100644 --- a/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix +++ b/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix @@ -4,7 +4,7 @@ import Stdlib.Prelude open; import PackageDescription.V1 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "package-juvix"; dependencies := [] }; diff --git a/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix b/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix index 52fd1ea559..05d7e7f89d 100644 --- a/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix +++ b/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix @@ -4,7 +4,7 @@ import Stdlib.Prelude open; import PackageDescription.V1 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "abc"; version := mkVersion 0 0 0; dependencies := [git "name" "url" "ref1"] diff --git a/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix b/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix index 8991581597..20d310a375 100644 --- a/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix +++ b/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V1 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "abc"; dependencies := [] }; diff --git a/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix index efff5ba9b1..c4bc6755a0 100644 --- a/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix +++ b/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "package-juvix" }; diff --git a/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix index efff5ba9b1..c4bc6755a0 100644 --- a/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix +++ b/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "package-juvix" }; diff --git a/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix index 61853bf96b..4da6bc3104 100644 --- a/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix +++ b/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "package-juvix"; dependencies := [] }; diff --git a/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix index 9e53af38cb..461a2c768a 100644 --- a/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix +++ b/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "abc"; version := mkVersion 0 0 0; dependencies := [git "name" "url" "ref1"] diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix index 85be188405..b7be735399 100644 --- a/tests/positive/Records.juvix +++ b/tests/positive/Records.juvix @@ -31,7 +31,7 @@ type EnumRecord := p2 : Pair EnumRecord EnumRecord := mkPair@{ fst := - C1@?{ + C1@{ c1a := constructT; c1b := constructT }; diff --git a/tests/positive/StdlibList/Package.juvix b/tests/positive/StdlibList/Package.juvix index a6223b86a4..cfab3cce78 100644 --- a/tests/positive/StdlibList/Package.juvix +++ b/tests/positive/StdlibList/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ dependencies := [] }; diff --git a/tests/positive/VisibilityPrecendence/Package.juvix b/tests/positive/VisibilityPrecendence/Package.juvix index 0027a3bac2..105e486066 100644 --- a/tests/positive/VisibilityPrecendence/Package.juvix +++ b/tests/positive/VisibilityPrecendence/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "test075" }; diff --git a/tests/positive/issue2737/Package.juvix b/tests/positive/issue2737/Package.juvix index 6a54fa0cd3..630999cb35 100644 --- a/tests/positive/issue2737/Package.juvix +++ b/tests/positive/issue2737/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "issue2737" }; diff --git a/tests/positive/issue2929/Package.juvix b/tests/positive/issue2929/Package.juvix index ec550a11f2..817eda193c 100644 --- a/tests/positive/issue2929/Package.juvix +++ b/tests/positive/issue2929/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "issue2929" }; diff --git a/tests/positive/issue3048/Package.juvix b/tests/positive/issue3048/Package.juvix index f04d2d888f..d5e0e45e71 100644 --- a/tests/positive/issue3048/Package.juvix +++ b/tests/positive/issue3048/Package.juvix @@ -3,6 +3,6 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "issue3048" }; diff --git a/tests/positive/issue3068/Package.juvix b/tests/positive/issue3068/Package.juvix index bbc6001160..d5fc44153a 100644 --- a/tests/positive/issue3068/Package.juvix +++ b/tests/positive/issue3068/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "issue3068"; dependencies := [] }; diff --git a/tests/positive/package/Package.juvix b/tests/positive/package/Package.juvix index 308c185ec7..b44f7fbb45 100644 --- a/tests/positive/package/Package.juvix +++ b/tests/positive/package/Package.juvix @@ -3,7 +3,7 @@ module Package; import PackageDescription.V2 open; package : Package := - defaultPackage@?{ + defaultPackage@{ name := "foo"; version := mkVersion 0 1 0; dependencies := diff --git a/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml b/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml index c6d26e6852..fc79d447fe 100644 --- a/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml +++ b/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml @@ -37,7 +37,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -103,7 +103,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -173,7 +173,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -218,7 +218,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -280,7 +280,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "Dep1"; + defaultPackage@{name := "Dep1"; version := mkVersion 0 1 0; dependencies := [defaultStdlib; @@ -303,7 +303,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -420,7 +420,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -515,7 +515,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -546,7 +546,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -623,7 +623,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "Dep1"; + defaultPackage@{name := "Dep1"; version := mkVersion 0 1 0; dependencies := [defaultStdlib; @@ -659,7 +659,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -735,7 +735,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -771,7 +771,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -822,7 +822,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -867,7 +867,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -912,7 +912,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -982,7 +982,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -1033,7 +1033,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; @@ -1096,7 +1096,7 @@ tests: import PackageDescription.V2 open; package : Package := - defaultPackage@?{name := "HelloWorld"; + defaultPackage@{name := "HelloWorld"; version := mkVersion 0 0 1; dependencies := [defaultStdlib; diff --git a/tests/smoke/Commands/compile-dependencies.smoke.yaml b/tests/smoke/Commands/compile-dependencies.smoke.yaml index 15e6b4f398..968fb1cd51 100644 --- a/tests/smoke/Commands/compile-dependencies.smoke.yaml +++ b/tests/smoke/Commands/compile-dependencies.smoke.yaml @@ -1056,7 +1056,7 @@ tests: cat <<-EOF > Package.juvix module Package; import PackageDescription.V2 open; - package : Package := defaultPackage@?{dependencies := [defaultStdlib ; git "dep1" "$temp/dep" "main"]} + package : Package := defaultPackage@{dependencies := [defaultStdlib ; git "dep1" "$temp/dep" "main"]} EOF cat <<-EOF > HelloWorld.juvix