avoid le

src/Juvix/Compiler/Core/Evaluator.hs

@@ -21,12 +21,20 @@ import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Pretty
 import Text.Read qualified as T
 
-newtype EvalOptions = EvalOptions
-  { _evalOptionsNormalize :: Bool
+data EvalOptions = EvalOptions
+  { _evalOptionsNormalize :: Bool,
+    _evalOptionsNoFailure :: Bool
   }
 
 makeLenses ''EvalOptions
 
+defaultEvalOptions :: EvalOptions
+defaultEvalOptions =
+  EvalOptions
+    { _evalOptionsNormalize = False,
+      _evalOptionsNoFailure = False
+    }
+
 data EvalError = EvalError
   { _evalErrorMsg :: !Text,
     _evalErrorNode :: !(Maybe Node)
@@ -63,12 +71,7 @@ evalInfoTable herr info = eval herr idenCtxt [] mainNode
 -- `env`. All nodes in `ctx` must be closed. All nodes in `env` must be values.
 -- Invariant for values v: eval ctx env v = v
 eval :: Handle -> IdentContext -> Env -> Node -> Node
-eval herr ctx env = geval opts herr ctx env
-  where
-    opts =
-      EvalOptions
-        { _evalOptionsNormalize = False
-        }
+eval herr ctx env = geval defaultEvalOptions herr ctx env
 
 geval :: EvalOptions -> Handle -> IdentContext -> Env -> Node -> Node
 geval opts herr ctx env0 = eval' env0
@@ -266,7 +269,7 @@ geval opts herr ctx env0 = eval' env0
         failOp :: [Node] -> Node
         failOp = unary $ \msg ->
           if
-              | opts ^. evalOptionsNormalize ->
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                   mkBuiltinApp' OpFail [eval' env msg]
               | otherwise ->
                   Exception.throw (EvalError ("failure: " <> printNode (eval' env msg)) Nothing)
@@ -361,15 +364,15 @@ geval opts herr ctx env0 = eval' env0
           mkCase i sym b (map (substEnvInBranch env) bs) (fmap (substEnv env) def)
 
 -- Evaluate `node` and interpret the builtin IO actions.
-hEvalIO :: Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node
-hEvalIO herr hin hout ctx env node =
-  let node' = eval herr ctx env node
+hEvalIO' :: EvalOptions -> Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node
+hEvalIO' opts herr hin hout ctx env node =
+  let node' = geval opts herr ctx env node
    in case node' of
         NCtr (Constr _ (BuiltinTag TagReturn) [x]) ->
           return x
         NCtr (Constr _ (BuiltinTag TagBind) [x, f]) -> do
-          x' <- hEvalIO herr hin hout ctx env x
-          hEvalIO herr hin hout ctx env (mkApp Info.empty f x')
+          x' <- hEvalIO' opts herr hin hout ctx env x
+          hEvalIO' opts herr hin hout ctx env (mkApp Info.empty f x')
         NCtr (Constr _ (BuiltinTag TagWrite) [NCst (Constant _ (ConstString s))]) -> do
           hPutStr hout s
           return unitNode
@@ -384,6 +387,9 @@ hEvalIO herr hin hout ctx env node =
   where
     unitNode = mkConstr (Info.singleton (NoDisplayInfo ())) (BuiltinTag TagTrue) []
 
+hEvalIO :: Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node
+hEvalIO = hEvalIO' defaultEvalOptions
+
 evalIO :: IdentContext -> Env -> Node -> IO Node
 evalIO = hEvalIO stderr stdin stdout
 

src/Juvix/Compiler/Core/Normalizer.hs

@@ -42,7 +42,7 @@ normalize tab0 = run . evalInfoTableBuilder tab0 . runReader normEnv . normalize
       return $ geval opts stdout (tab ^. identContext) env node
       where
         opts =
-          EvalOptions
+          defaultEvalOptions
             { _evalOptionsNormalize = True
             }
 

src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs

@@ -74,17 +74,18 @@ convertNode tab = rmap go
                   0 ->
                     recur [] $ mkIf _caseInfo sym (mkBuiltinApp' OpEq [_caseValue, mkConstant' (ConstInteger 0)]) _caseBranchBody br
                   1 ->
-                    mkLet mempty binder' (mkBuiltinApp' OpIntSub [go recur _caseValue, mkConstant' (ConstInteger 1)]) $
+                    mkLet mempty binder' (go recur _caseValue) $
                       mkIf
                         _caseInfo
                         sym
-                        (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar (Info.singleton (NameInfo name)) 0])
-                        (go (recur . (BCKeep binder :)) _caseBranchBody)
+                        (mkBuiltinApp' OpEq [mkConstant' (ConstInteger 0), mkVar (Info.singleton (NameInfo name)) 0])
                         (go (recur . (BCAdd 1 :)) br)
+                        (go (recur . ([BCAdd 1, BCRemove (BinderRemove binder subNode)] ++)) _caseBranchBody)
                     where
                       binder = List.head _caseBranchBinders
                       name = binder ^. binderName
                       binder' = over binderType (go recur) binder
+                      subNode = mkBuiltinApp' OpIntSub [mkVar (Info.singleton (NameInfo name)) 0, mkConstant' (ConstInteger 1)]
                   _ -> impossible
           maybeBranch :: Maybe Node -> Node
           maybeBranch = fromMaybe (mkBuiltinApp' OpFail [mkConstant' (ConstString "no matching branch")])

test/Core/Eval/Base.hs

@@ -68,7 +68,7 @@ coreEvalAssertion' mode tab mainFile expectedFile step =
                   let tyargs = typeArgs (lookupIdentifierInfo tab sym ^. identifierType)
                       args = zipWith mkArg (tyargs ++ repeat mkDynamic') (map snd _evalDataInput)
                       node' = mkApps' node args
-                  r' <- doEval mainFile hout tab node'
+                  r' <- doEval' opts mainFile hout tab node'
                   case r' of
                     Left err -> do
                       hClose hout
@@ -87,6 +87,10 @@ coreEvalAssertion' mode tab mainFile expectedFile step =
     sym = fromJust (tab ^. infoMain)
     ii = lookupIdentifierInfo tab sym
 
+    opts = case mode of
+      EvalModePlain -> defaultEvalOptions
+      EvalModeJSON -> defaultEvalOptions {_evalOptionsNoFailure = True}
+
     mkArg :: Type -> Text -> Node
     mkArg ty arg =
       let n = fst $ fromRight' $ decimal arg
@@ -178,13 +182,22 @@ parseFile f = do
   s <- readFile f'
   return $ runParser f emptyInfoTable s
 
-doEval ::
+doEval' ::
+  EvalOptions ->
   Path Abs File ->
   Handle ->
   InfoTable ->
   Node ->
   IO (Either CoreError Node)
-doEval f hout tab node =
-  catchEvalErrorIO defaultLoc (hEvalIO hout stdin hout (tab ^. identContext) [] node)
+doEval' opts f hout tab node =
+  catchEvalErrorIO defaultLoc (hEvalIO' opts hout stdin hout (tab ^. identContext) [] node)
   where
     defaultLoc = singletonInterval (mkInitialLoc f)
+
+doEval ::
+  Path Abs File ->
+  Handle ->
+  InfoTable ->
+  Node ->
+  IO (Either CoreError Node)
+doEval = doEval' defaultEvalOptions

test/VampIR/Compilation/Positive.hs

@@ -106,31 +106,31 @@ tests =
       $(mkRelFile "test010.juvix")
       $(mkRelFile "data/test010.json"),
     posTest
-      12
+      8
       "Test011: recursion"
       $(mkRelDir ".")
       $(mkRelFile "test011.juvix")
       $(mkRelFile "data/test011.json"),
     posTest
-      12
+      8
       "Test012: tail recursion"
       $(mkRelDir ".")
       $(mkRelFile "test012.juvix")
       $(mkRelFile "data/test012.json"),
     posTest
-      12
+      8
       "Test013: tail recursion: Fibonacci numbers in linear time"
       $(mkRelDir ".")
       $(mkRelFile "test013.juvix")
       $(mkRelFile "data/test013.json"),
     posTest
-      12
+      8
       "Test014: recursion through higher-order functions"
       $(mkRelDir ".")
       $(mkRelFile "test014.juvix")
       $(mkRelFile "data/test014.json"),
     posTest
-      12
+      8
       "Test015: tail recursion through higher-order functions"
       $(mkRelDir ".")
       $(mkRelFile "test015.juvix")
@@ -142,7 +142,7 @@ tests =
       $(mkRelFile "test016.juvix")
       $(mkRelFile "data/test016.json"),
     posTest
-      14
+      9
       "Test017: mutual recursion"
       $(mkRelDir ".")
       $(mkRelFile "test017.juvix")
@@ -160,7 +160,7 @@ tests =
       $(mkRelFile "test019.juvix")
       $(mkRelFile "data/test019.json"),
     posTest
-      12
+      8
       "Test020: boolean target"
       $(mkRelDir ".")
       $(mkRelFile "test020.juvix")

tests/VampIR/positive/Compilation/test017.juvix

@@ -12,9 +12,9 @@ g : Nat → Nat;
 terminating
 h : Nat → Nat;
 
-f x := if (x < 1) 1 (2 * x + g (sub x 1));
-g x := if (x < 1) 1 (x + h (sub x 1));
-h x := if (x < 1) 1 (x * f (sub x 1));
+f x := case x | zero := 1 | suc y := 2 * x + g y;
+g x := case x | zero := 1 | suc y := x + h y;
+h x := case x | zero := 1 | suc y := x * f y;
 
 main : Nat → Nat;
 main x := f x + f (2 * x);