Merge remote-tracking branch 'origin/main' into hash-globalpkg

anoma · Dec 4, 2024 · 5dacf3e · 5dacf3e
2 parents a7ec169 + 021fc0c
commit 5dacf3e
Show file tree

Hide file tree

Showing 100 changed files with 279 additions and 317 deletions.
diff --git 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/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git 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
@@ -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,
+1 −1		Package.juvix
+1 −1		Stdlib/Cairo/Ec.juvix
+1 −1		Stdlib/Data/Field.juvix
+8 −6		Stdlib/Data/Int.juvix
+10 −7		Stdlib/Data/Nat.juvix
+1 −1		test/Package.juvix