From a8b728994eda2a99b90896348afd31b52355db10 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 20 Jun 2023 15:41:57 +0200 Subject: [PATCH] avoid le --- src/Juvix/Compiler/Core/Evaluator.hs | 34 +++++++++++-------- src/Juvix/Compiler/Core/Normalizer.hs | 2 +- .../Core/Transformation/NatToPrimInt.hs | 7 ++-- test/Core/Eval/Base.hs | 21 +++++++++--- test/VampIR/Compilation/Positive.hs | 14 ++++---- .../VampIR/positive/Compilation/test017.juvix | 6 ++-- 6 files changed, 52 insertions(+), 32 deletions(-) diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 672c972016..1f578b04ed 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/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 diff --git a/src/Juvix/Compiler/Core/Normalizer.hs b/src/Juvix/Compiler/Core/Normalizer.hs index 90da01feb5..bc15d6f9a2 100644 --- a/src/Juvix/Compiler/Core/Normalizer.hs +++ b/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 } diff --git a/src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs b/src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs index 7cbfc92bf6..9d46ef429b 100644 --- a/src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs +++ b/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")]) diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs index 5a3dac3230..f0d66f0c16 100644 --- a/test/Core/Eval/Base.hs +++ b/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 diff --git a/test/VampIR/Compilation/Positive.hs b/test/VampIR/Compilation/Positive.hs index 9a233267ef..a0048c04e8 100644 --- a/test/VampIR/Compilation/Positive.hs +++ b/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") diff --git a/tests/VampIR/positive/Compilation/test017.juvix b/tests/VampIR/positive/Compilation/test017.juvix index 8d04cc341c..1405795973 100644 --- a/tests/VampIR/positive/Compilation/test017.juvix +++ b/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);