Add fail nodes to Geb (#1947)

* Adds `fail` morphisms to Geb.Language and Geb.Evaluator.
* Enables recursion in the Core-to-Geb pipeline.
* Adds recursion tests.

src/Juvix/Compiler/Backend/Geb/Analysis/TypeChecking/Checker.hs

@@ -60,6 +60,7 @@ inferObject = \case
   MorphismVar v -> inferObjectVar v
   MorphismLeft a -> inferObjectLeft a
   MorphismRight b -> inferObjectRight b
+  MorphismFail x -> return $ x ^. failureType
 
 inferObjectAbsurd :: InferEffects r => Absurd -> Sem r Object
 inferObjectAbsurd x = do

src/Juvix/Compiler/Backend/Geb/Evaluator.hs

@@ -81,6 +81,7 @@ eval morph =
     MorphismSecond s -> evalSecond s
     MorphismUnit -> return GebValueMorphismUnit
     MorphismVar x -> evalVar x
+    MorphismFail x -> evalFail x
 
 evalVar :: EvalEffects r => Var -> Sem r GebValue
 evalVar var = do
@@ -210,7 +211,7 @@ evalCase c = do
           }
 
 evalBinop ::
-  Members '[Reader Env, Error EvalError] r =>
+  EvalEffects r =>
   Binop ->
   Sem r GebValue
 evalBinop binop = do
@@ -264,6 +265,15 @@ evalBinop binop = do
               _evalErrorGebExpression = Just (MorphismBinop binop)
             }
 
+evalFail :: EvalEffects r => Failure -> Sem r GebValue
+evalFail Failure {..} =
+  throw
+    EvalError
+      { _evalErrorMsg = "failure: " <> _failureMessage,
+        _evalErrorGebValue = Nothing,
+        _evalErrorGebExpression = Nothing
+      }
+
 sameKind :: GebValue -> GebValue -> Bool
 sameKind l r = case (l, r) of
   (GebValueMorphismInteger _, GebValueMorphismInteger _) -> True

src/Juvix/Compiler/Backend/Geb/Extra.hs

@@ -109,6 +109,7 @@ mapVars f m = go 0 m
       MorphismVar x -> f k x
       MorphismInteger i -> MorphismInteger i
       MorphismBinop x -> MorphismBinop (over binopLeft (go k) (over binopRight (go k) x))
+      MorphismFail x -> MorphismFail x
 
 shift :: Int -> Morphism -> Morphism
 shift 0 m = m

src/Juvix/Compiler/Backend/Geb/Language.hs

@@ -111,6 +111,12 @@ data Binop = Binop
   }
   deriving stock (Show, Eq, Generic)
 
+data Failure = Failure
+  { _failureMessage :: Text,
+    _failureType :: Object
+  }
+  deriving stock (Show, Eq, Generic)
+
 -- | Corresponds to the GEB type for terms (morphisms of the category): `stlc`
 -- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp).
 data Morphism
@@ -127,6 +133,7 @@ data Morphism
   | MorphismVar Var
   | MorphismInteger Integer
   | MorphismBinop Binop
+  | MorphismFail Failure
   deriving stock (Show, Eq, Generic)
 
 data Product = Product
@@ -198,6 +205,7 @@ instance HasAtomicity Morphism where
     MorphismVar {} -> Aggregate appFixity
     MorphismInteger {} -> Atom
     MorphismBinop {} -> Aggregate appFixity
+    MorphismFail {} -> Aggregate appFixity
 
 instance HasAtomicity Object where
   atomicity = \case
@@ -225,6 +233,7 @@ makeLenses ''Binop
 makeLenses ''Case
 makeLenses ''Coproduct
 makeLenses ''First
+makeLenses ''Failure
 makeLenses ''Hom
 makeLenses ''Lambda
 makeLenses ''LeftInj'

src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs

@@ -142,6 +142,11 @@ instance PrettyCode Binop where
     right <- ppArg _binopRight
     return $ op <> line <> indent' (vsep [left, right])
 
+instance PrettyCode Failure where
+  ppCode Failure {..} = do
+    ty <- ppArg _failureType
+    return $ kwFail <+> ppStringLit _failureMessage <+> ty
+
 instance PrettyCode Var where
   ppCode Var {..} = do
     return $
@@ -163,6 +168,7 @@ instance PrettyCode Morphism where
     MorphismVar idx -> ppCode idx
     MorphismInteger n -> return $ annotate AnnLiteralInteger (pretty n)
     MorphismBinop x -> ppCode x
+    MorphismFail x -> ppCode x
 
 instance PrettyCode Product where
   ppCode Product {..} = do

src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs

@@ -28,7 +28,8 @@ keywords =
     kwSub,
     kwMul,
     kwDiv,
-    kwMod
+    kwMod,
+    kwFail
   ]
 
 kwAbsurd :: Doc Ann
@@ -111,3 +112,6 @@ kwInteger = keyword Str.gebInteger
 
 kwTyped :: Doc Ann
 kwTyped = keyword Str.gebTyped
+
+kwFail :: Doc Ann
+kwFail = keyword Str.gebFail

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -187,6 +187,7 @@ fromCore tab = case tab ^. Core.infoMain of
       Core.OpIntLt -> convertBinop OpLt _builtinAppArgs
       Core.OpIntLe -> convertOpIntLe _builtinAppArgs
       Core.OpEq -> convertOpEq _builtinAppArgs
+      Core.OpFail -> convertOpFail (Info.getInfoType _builtinAppInfo) _builtinAppArgs
       _ ->
         unsupported
 
@@ -275,6 +276,13 @@ fromCore tab = case tab ^. Core.infoMain of
       _ ->
         error "unsupported equality argument types"
 
+    convertOpFail :: Core.Type -> [Core.Node] -> Trans Morphism
+    convertOpFail ty args = case args of
+      [Core.NCst (Core.Constant _ (Core.ConstString msg))] -> do
+        return $ MorphismFail (Failure msg (convertType ty))
+      _ ->
+        error "unsupported fail arguments"
+
     convertConstr :: Core.Constr -> Trans Morphism
     convertConstr Core.Constr {..} = do
       args <- convertProduct _constrArgs

src/Juvix/Compiler/Backend/Geb/Translation/FromSource.hs

@@ -128,6 +128,7 @@ morphism =
             <|> Geb.MorphismApplication <$> morphismApplication
             <|> Geb.MorphismVar <$> morphismVar
             <|> Geb.MorphismBinop <$> morphismBinop
+            <|> Geb.MorphismFail <$> morphismFail
         )
 
 parseNatural :: ParsecS r Integer
@@ -160,6 +161,13 @@ morphismBinop = do
           _binopRight = m2
         }
 
+morphismFail :: ParsecS r Geb.Failure
+morphismFail = do
+  P.label "<geb MorphismFail>" $ do
+    kw kwFail
+    msg <- fst <$> string
+    Geb.Failure msg <$> object
+
 object :: ParsecS r Geb.Object
 object =
   P.label "<geb Object>" $ do

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

@@ -1,18 +1,17 @@
 module Juvix.Compiler.Core.Transformation.CheckGeb where
 
 import Data.HashMap.Strict qualified as HashMap
-import Juvix.Compiler.Core.Data.IdentDependencyInfo
 import Juvix.Compiler.Core.Data.TypeDependencyInfo
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.LocationInfo (getInfoLocation)
+import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Data.PPOutput
 
 checkGeb :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
 checkGeb tab =
-  checkNoRecursion
-    >> checkNoRecursiveTypes
+  checkNoRecursiveTypes
     >> mapAllNodesM checkNoIO tab
     >> mapAllNodesM checkBuiltins tab
     >> mapAllNodesM checkTypes tab
@@ -58,7 +57,12 @@ checkGeb tab =
               OpStrConcat -> throw $ unsupportedError "strings" node (getInfoLocation _builtinAppInfo)
               OpStrToInt -> throw $ unsupportedError "strings" node (getInfoLocation _builtinAppInfo)
               OpTrace -> throw $ unsupportedError "tracing" node (getInfoLocation _builtinAppInfo)
-              OpFail -> throw $ unsupportedError "failing" node (getInfoLocation _builtinAppInfo)
+              OpFail -> do
+                let ty = Info.getInfoType _builtinAppInfo
+                when (isDynamic ty) $
+                  throw $
+                    unsupportedError "failing without type info" node (getInfoLocation _builtinAppInfo)
+                return node
               _ -> return node
           _ -> return node
 
@@ -76,16 +80,6 @@ checkGeb tab =
               _ -> return node
           _ -> return node
 
-    checkNoRecursion :: Sem r ()
-    checkNoRecursion =
-      when (isCyclic (createIdentDependencyInfo tab)) $
-        throw
-          CoreError
-            { _coreErrorMsg = ppOutput "recursion not supported for the GEB target",
-              _coreErrorNode = Nothing,
-              _coreErrorLoc = defaultLoc
-            }
-
     checkNoRecursiveTypes :: Sem r ()
     checkNoRecursiveTypes =
       when (isCyclic (createTypeDependencyInfo tab)) $

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

@@ -54,7 +54,7 @@ computeNodeTypeInfo tab = umapL go
           OpTrace -> case _builtinAppArgs of
             [_, arg2] -> Info.getNodeType arg2
             _ -> error "incorrect trace builtin application"
-          OpFail -> mkDynamic'
+          OpFail -> Info.getNodeType node
       NCtr Constr {..} ->
         let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
             ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives)

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

@@ -4,6 +4,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.IdentDependencyInfo
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.TypeInfo (setNodeType)
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
 
@@ -69,9 +70,12 @@ unrollRecursion tab = do
                   name' = ii ^. identifierName <> "__" <> show limit
                   ii' = ii {_identifierSymbol = sym', _identifierName = name'}
               registerIdent name' ii'
-              let node
+              let failNode =
+                    setNodeType (ii ^. identifierType) $
+                      mkBuiltinApp' OpFail [mkConstant' (ConstString "recursion limit reached")]
+                  node
                     | limit == 0 =
-                        etaExpand (typeArgs (ii ^. identifierType)) (mkBuiltinApp' OpFail [mkConstant' (ConstString "recursion limit reached")])
+                        etaExpand (typeArgs (ii ^. identifierType)) failNode
                     | otherwise =
                         umap (go limit) (fromJust $ HashMap.lookup sym (tab ^. identContext))
               registerIdentNode sym' node

src/Juvix/Extra/Strings.hs

@@ -509,6 +509,9 @@ gebDiv = "div"
 gebMod :: IsString s => s
 gebMod = "mod"
 
+gebFail :: IsString s => s
+gebFail = "fail"
+
 gebEq :: IsString s => s
 gebEq = "eq"
 

test/BackendGeb/Compilation/Positive.hs

@@ -93,5 +93,70 @@ tests =
       "Test012: mid-square hashing (unrolled)"
       $(mkRelDir ".")
       $(mkRelFile "test012.juvix")
-      $(mkRelFile "out/test012.geb")
+      $(mkRelFile "out/test012.geb"),
+    PosTest
+      "Test013: recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "test013.juvix")
+      $(mkRelFile "out/test013.geb"),
+    PosTest
+      "Test014: tail recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "test014.juvix")
+      $(mkRelFile "out/test014.geb"),
+    PosTest
+      "Test015: tail recursion: Fibonacci numbers in linear time"
+      $(mkRelDir ".")
+      $(mkRelFile "test015.juvix")
+      $(mkRelFile "out/test015.geb"),
+    PosTest
+      "Test016: local functions with free variables"
+      $(mkRelDir ".")
+      $(mkRelFile "test016.juvix")
+      $(mkRelFile "out/test016.geb"),
+    PosTest
+      "Test017: recursion through higher-order functions"
+      $(mkRelDir ".")
+      $(mkRelFile "test017.juvix")
+      $(mkRelFile "out/test017.geb"),
+    PosTest
+      "Test018: tail recursion through higher-order functions"
+      $(mkRelDir ".")
+      $(mkRelFile "test018.juvix")
+      $(mkRelFile "out/test018.geb"),
+    PosTest
+      "Test019: higher-order functions and recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "test019.juvix")
+      $(mkRelFile "out/test019.geb"),
+    PosTest
+      "Test020: McCarthy's 91 function"
+      $(mkRelDir ".")
+      $(mkRelFile "test020.juvix")
+      $(mkRelFile "out/test020.geb"),
+    PosTest
+      "Test021: fast exponentiation"
+      $(mkRelDir ".")
+      $(mkRelFile "test021.juvix")
+      $(mkRelFile "out/test021.geb"),
+    PosTest
+      "Test022: mutual recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "test022.juvix")
+      $(mkRelFile "out/test022.geb"),
+    PosTest
+      "Test023: Euclid's algorithm"
+      $(mkRelDir ".")
+      $(mkRelFile "test023.juvix")
+      $(mkRelFile "out/test023.geb"),
+    PosTest
+      "Test024: Ackermann function"
+      $(mkRelDir ".")
+      $(mkRelFile "test024.juvix")
+      $(mkRelFile "out/test024.geb"),
+    PosTest
+      "Test025: mid-square hashing"
+      $(mkRelDir ".")
+      $(mkRelFile "test025.juvix")
+      $(mkRelFile "out/test025.geb")
   ]

test/BackendGeb/FromCore/Base.hs

@@ -2,9 +2,11 @@ module BackendGeb.FromCore.Base where
 
 import Base
 import Data.Text.IO qualified as TIO
+import GHC.Base (seq)
 import Juvix.Compiler.Backend (Target (TargetGeb))
 import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Pipeline
 import Juvix.Prelude.Pretty
 
@@ -34,55 +36,56 @@ coreToGebTranslationAssertion' coreInfoTable entryPoint expectedFile step = do
     Left err ->
       assertFailure . show . pretty $
         fromJuvixError @GenericError err
-    Right readyCoreInfoTable -> do
-      step "Translate the Juvix Core node to Geb"
-      let (translatedMorphism, translatedObj) = Geb.fromCore readyCoreInfoTable
-      step "Typecheck the translated Geb node"
-      let typeMorph =
-            Geb.TypedMorphism
-              { _typedMorphism = translatedMorphism,
-                _typedMorphismObject = translatedObj
-              }
-      case run . runError @Geb.CheckingError $ Geb.check' typeMorph of
-        Left err ->
-          assertFailure . show . pretty $
-            fromJuvixError @GenericError (JuvixError err)
-        Right _ -> do
-          step "Try evaluating the JuvixCore node"
-          let resultCoreEval :: Core.Node = Core.evalInfoTable stderr readyCoreInfoTable
-          step "Translate the result of the evaluated JuvixCore node to Geb"
-          let (gebCoreEvalResult, _) = Geb.fromCore $ Core.setupMainFunction readyCoreInfoTable resultCoreEval
-          case ( Geb.eval' Geb.defaultEvalEnv translatedMorphism,
-                 Geb.eval' Geb.defaultEvalEnv gebCoreEvalResult
-               ) of
-            (Left err, _) -> do
-              step "The evaluation of the translated Geb node failed"
-              assertFailure . show . pretty $
-                fromJuvixError @GenericError (JuvixError err)
-            (_, Left err) -> do
-              step "The evaluation of gebCoreEvalResult failed"
-              assertFailure . show . pretty $ fromJuvixError @GenericError (JuvixError err)
-            ( Right resEvalTranslatedMorph,
-              Right resEvalGebCoreEvalResult
-              ) -> do
-                step "Compare the geb value of the Core eval output and the Geb eval output"
-                if
-                    | resEvalTranslatedMorph /= resEvalGebCoreEvalResult ->
-                        assertFailure "The evaluation for the Core node and the Geb node are not equal"
-                    | otherwise -> do
-                        let fpath = toFilePath expectedFile
-                        expectedInput <- TIO.readFile fpath
-                        step "Compare expected and actual program output"
-                        let compareEvalOutput morph =
-                              if
-                                  | Geb.quote resEvalTranslatedMorph /= morph ->
-                                      assertFailure $
-                                        "The result of evaluating the translated Geb"
-                                          <> "node is not equal to the expected output"
-                                  | otherwise -> assertBool "" True
-                        case Geb.runParser expectedFile expectedInput of
-                          Left parseErr -> assertFailure . show . pretty $ parseErr
-                          Right (Geb.ExpressionMorphism m) -> compareEvalOutput m
-                          Right (Geb.ExpressionTypedMorphism m) -> compareEvalOutput (m ^. Geb.typedMorphism)
-                          Right (Geb.ExpressionObject _) ->
-                            assertFailure "Expected a morphism, but got an object for the expected output"
+    Right readyCoreInfoTable ->
+      length (fromText (Core.ppTrace readyCoreInfoTable) :: String) `seq` do
+        step "Translate the Juvix Core node to Geb"
+        let (translatedMorphism, translatedObj) = Geb.fromCore readyCoreInfoTable
+        step "Typecheck the translated Geb node"
+        let typeMorph =
+              Geb.TypedMorphism
+                { _typedMorphism = translatedMorphism,
+                  _typedMorphismObject = translatedObj
+                }
+        case run . runError @Geb.CheckingError $ Geb.check' typeMorph of
+          Left err ->
+            assertFailure . show . pretty $
+              fromJuvixError @GenericError (JuvixError err)
+          Right _ -> do
+            step "Try evaluating the JuvixCore node"
+            let resultCoreEval :: Core.Node = Core.evalInfoTable stderr readyCoreInfoTable
+            step "Translate the result of the evaluated JuvixCore node to Geb"
+            let (gebCoreEvalResult, _) = Geb.fromCore $ Core.setupMainFunction readyCoreInfoTable resultCoreEval
+            case ( Geb.eval' Geb.defaultEvalEnv translatedMorphism,
+                   Geb.eval' Geb.defaultEvalEnv gebCoreEvalResult
+                 ) of
+              (Left err, _) -> do
+                step "The evaluation of the translated Geb node failed"
+                assertFailure . show . pretty $
+                  fromJuvixError @GenericError (JuvixError err)
+              (_, Left err) -> do
+                step "The evaluation of gebCoreEvalResult failed"
+                assertFailure . show . pretty $ fromJuvixError @GenericError (JuvixError err)
+              ( Right resEvalTranslatedMorph,
+                Right resEvalGebCoreEvalResult
+                ) -> do
+                  step "Compare the geb value of the Core eval output and the Geb eval output"
+                  if
+                      | resEvalTranslatedMorph /= resEvalGebCoreEvalResult ->
+                          assertFailure "The evaluation for the Core node and the Geb node are not equal"
+                      | otherwise -> do
+                          let fpath = toFilePath expectedFile
+                          expectedInput <- TIO.readFile fpath
+                          step "Compare expected and actual program output"
+                          let compareEvalOutput morph =
+                                if
+                                    | Geb.quote resEvalTranslatedMorph /= morph ->
+                                        assertFailure $
+                                          "The result of evaluating the translated Geb"
+                                            <> "node is not equal to the expected output"
+                                    | otherwise -> assertBool "" True
+                          case Geb.runParser expectedFile expectedInput of
+                            Left parseErr -> assertFailure . show . pretty $ parseErr
+                            Right (Geb.ExpressionMorphism m) -> compareEvalOutput m
+                            Right (Geb.ExpressionTypedMorphism m) -> compareEvalOutput (m ^. Geb.typedMorphism)
+                            Right (Geb.ExpressionObject _) ->
+                              assertFailure "Expected a morphism, but got an object for the expected output"

test/BackendGeb/FromCore/Positive.hs

@@ -101,5 +101,65 @@ tests =
       "Test013: mid-square hashing (unrolled)"
       $(mkRelDir ".")
       $(mkRelFile "Core/test013.jvc")
-      $(mkRelFile "Eval/out/test013.geb")
+      $(mkRelFile "Eval/out/test013.geb"),
+    PosTest
+      "Test014: recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test014.jvc")
+      $(mkRelFile "Eval/out/test014.geb"),
+    PosTest
+      "Test015: tail recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test015.jvc")
+      $(mkRelFile "Eval/out/test015.geb"),
+    PosTest
+      "Test016: tail recursion: Fibonacci numbers in linear time"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test016.jvc")
+      $(mkRelFile "Eval/out/test016.geb"),
+    PosTest
+      "Test017: recursion through higher-order functions"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test017.jvc")
+      $(mkRelFile "Eval/out/test017.geb"),
+    PosTest
+      "Test018: tail recursion through higher-order functions"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test018.jvc")
+      $(mkRelFile "Eval/out/test018.geb"),
+    PosTest
+      "Test019: higher-order functions and recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test019.jvc")
+      $(mkRelFile "Eval/out/test019.geb"),
+    PosTest
+      "Test020: McCarthy's 91 function"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test020.jvc")
+      $(mkRelFile "Eval/out/test020.geb"),
+    PosTest
+      "Test021: fast exponentiation"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test021.jvc")
+      $(mkRelFile "Eval/out/test021.geb"),
+    PosTest
+      "Test022: mutual recursion"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test022.jvc")
+      $(mkRelFile "Eval/out/test022.geb"),
+    PosTest
+      "Test023: Euclid's algorithm"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test023.jvc")
+      $(mkRelFile "Eval/out/test023.geb"),
+    PosTest
+      "Test024: Ackermann function"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test024.jvc")
+      $(mkRelFile "Eval/out/test024.geb"),
+    PosTest
+      "Test025: mid-square hashing"
+      $(mkRelDir ".")
+      $(mkRelFile "Core/test025.jvc")
+      $(mkRelFile "Eval/out/test025.geb")
   ]

tests/Geb/positive/Compilation/out/test013.geb

@@ -0,0 +1 @@
+5050

tests/Geb/positive/Compilation/out/test014.geb

@@ -0,0 +1 @@
+5050

tests/Geb/positive/Compilation/out/test015.geb

@@ -0,0 +1 @@
+55

tests/Geb/positive/Compilation/out/test016.geb

@@ -0,0 +1 @@
+771

tests/Geb/positive/Compilation/out/test017.geb

@@ -0,0 +1 @@
+55

tests/Geb/positive/Compilation/out/test018.geb

@@ -0,0 +1 @@
+5050

tests/Geb/positive/Compilation/out/test019.geb

@@ -0,0 +1 @@
+11

tests/Geb/positive/Compilation/out/test020.geb

@@ -0,0 +1 @@
+364

tests/Geb/positive/Compilation/out/test021.geb

@@ -0,0 +1 @@
+48830320

tests/Geb/positive/Compilation/out/test022.geb

@@ -0,0 +1 @@
+6386010

tests/Geb/positive/Compilation/out/test023.geb

@@ -0,0 +1 @@
+87

tests/Geb/positive/Compilation/out/test024.geb

@@ -0,0 +1 @@
+203

tests/Geb/positive/Compilation/out/test025.geb

@@ -0,0 +1 @@
+3

tests/Geb/positive/Compilation/test002.juvix

@@ -1,3 +1,4 @@
+-- pattern matching
 module test002;
 
 open import Stdlib.Prelude;

tests/Geb/positive/Compilation/test013.juvix

@@ -0,0 +1,11 @@
+-- recursion
+module test013;
+
+open import Stdlib.Prelude;
+
+sum : Nat → Nat;
+sum zero := 0;
+sum (suc x) := suc x + sum x;
+
+main : Nat;
+main := sum 100;

tests/Geb/positive/Compilation/test014.juvix

@@ -0,0 +1,14 @@
+-- tail recursion
+module test014;
+
+open import Stdlib.Prelude;
+
+sum' : Nat → Nat → Nat;
+sum' acc zero := acc;
+sum' acc (suc x) := sum' (suc x + acc) x;
+
+sum : Nat → Nat;
+sum := sum' 0;
+
+main : Nat;
+main := sum 100;

tests/Geb/positive/Compilation/test015.juvix

@@ -0,0 +1,14 @@
+-- tail recursion: Fibonacci numbers in linear time
+module test015;
+
+open import Stdlib.Prelude;
+
+fib' : Nat → Nat → Nat → Nat;
+fib' x y zero := x;
+fib' x y (suc n) := fib' y (x + y) n;
+
+fib : Nat → Nat;
+fib := fib' 0 1;
+
+main : Nat;
+main := fib 10;

tests/Geb/positive/Compilation/test016.juvix

@@ -0,0 +1,26 @@
+-- local functions with free variables
+module test016;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+terminating
+f : Nat → Nat → Nat;
+f x :=
+    let g : Nat → Nat; g y := x + y in
+    if (x == 0)
+       (f 10)
+       (if (x < 10)
+           λ{y := g (f (sub x 1) y)}
+           g);
+
+g : Nat → (Nat → Nat) → Nat;
+g x h := x + h x;
+
+terminating
+h : Nat → Nat;
+h zero := 0;
+h (suc x) := g x h;
+
+main : Nat;
+main := f 100 500 + f 5 0 + f 5 5 + h 10 + g 10 h + g 3 (f 10);

tests/Geb/positive/Compilation/test017.juvix

@@ -0,0 +1,15 @@
+-- recursion through higher-order functions
+module test017;
+
+open import Stdlib.Prelude;
+
+g : (Nat → Nat) → Nat → Nat;
+g f zero := 0;
+g f (suc x) := f x;
+
+terminating
+f : Nat → Nat;
+f x := x + g f x;
+
+main : Nat;
+main := f 10; -- 55

tests/Geb/positive/Compilation/test018.juvix

@@ -0,0 +1,18 @@
+-- tail recursion through higher-order functions
+module test018;
+
+open import Stdlib.Prelude;
+
+sumb : Nat → (Nat → Nat → Nat) → Nat → Nat;
+sumb acc f zero := acc;
+sumb acc f (suc x) := f acc x;
+
+terminating
+sum' : Nat → Nat → Nat;
+sum' acc x := sumb (x + acc) sum' x;
+
+sum : Nat → Nat;
+sum := sum' 0;
+
+main : Nat;
+main := sum 100;

tests/Geb/positive/Compilation/test019.juvix

@@ -0,0 +1,16 @@
+-- higher-order functions and recursion
+module test019;
+
+open import Stdlib.Prelude;
+
+f : (Nat → Nat) → Nat;
+f g := g 5;
+
+h : Nat → Nat → Nat;
+h x z := x + z;
+
+u : Nat → Nat;
+u x := f (h 4) + x;
+
+main : Nat;
+main := u 2;

tests/Geb/positive/Compilation/test020.juvix

@@ -0,0 +1,12 @@
+-- McCarthy's 91 function
+module test020;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+terminating
+f91 : Nat → Nat;
+f91 n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
+
+main : Nat;
+main := f91 101 + f91 95 + f91 16 + f91 5;

tests/Geb/positive/Compilation/test021.juvix

@@ -0,0 +1,20 @@
+-- fast exponentiation
+module test021;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+terminating
+power' : Nat → Nat → Nat → Nat;
+power' acc a b :=
+  if (b == 0)
+    acc
+    (if (mod b 2 == 0)
+      (power' acc (a * a) (div b 2))
+      (power' (acc * a) (a * a) (div b 2)));
+
+power : Nat → Nat → Nat;
+power := power' 1;
+
+main : Nat;
+main := power 2 3 + power 3 7 + power 5 11;

tests/Geb/positive/Compilation/test022.juvix

@@ -0,0 +1,19 @@
+-- mutual recursion
+module test022;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+terminating
+f : Nat → Nat;
+terminating
+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));
+
+main : Nat;
+main := f 5 + f 10 + f 20;

tests/Geb/positive/Compilation/test023.juvix

@@ -0,0 +1,21 @@
+-- Euclid's algorithm
+module test023;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+terminating
+gcd : Nat → Nat → Nat;
+gcd a b := if (a > b)
+              (gcd b a)
+              (if (a == 0)
+                  b
+                  (gcd (mod b a) a));
+
+main : Nat;
+main :=
+  gcd (3 * 7 * 2) (7 * 2 * 11) +
+  gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5) +
+  gcd 3 7 +
+  gcd 7 3 +
+  gcd (11 * 7 * 3) (2 * 5 * 13);

tests/Geb/positive/Compilation/test024.juvix

@@ -0,0 +1,12 @@
+-- Ackermann function
+module test024;
+
+open import Stdlib.Prelude;
+
+ack : Nat → Nat → Nat;
+ack zero n := n + 1;
+ack (suc m) zero := ack m 1;
+ack (suc m) (suc n) := ack m (ack (suc m) n);
+
+main : Nat;
+main := ack 0 7 + ack 1 7 + ack 1 13 + ack 2 7 + ack 2 13 + ack 3 4;

tests/Geb/positive/Compilation/test025.juvix

@@ -0,0 +1,23 @@
+-- mid-square hashing
+module test025;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+pow : Nat -> Nat;
+pow zero := 1;
+pow (suc n) := 2 * pow n;
+
+hash' : Nat -> Nat -> Nat;
+hash' (suc n@(suc (suc m))) x :=
+  if
+    (x < pow n)
+    (hash' n x)
+    (mod (div (x * x) (pow m)) (pow 6));
+hash' _ x := x * x;
+
+hash : Nat -> Nat := hash' 16;
+
+main : Nat;
+main := hash 1367;
+-- result: 3

tests/Geb/positive/Core/test014.jvc

@@ -0,0 +1,5 @@
+-- recursion
+
+def sum : Int -> Int := \(x : Int) if x = 0 then 0 else x + sum (x - 1);
+
+sum 100

tests/Geb/positive/Core/test015.jvc

@@ -0,0 +1,6 @@
+-- tail recursion
+
+def sum' : Int -> Int -> Int := \(x : Int) \(acc : Int) if x = 0 then acc else sum' (x - 1) (x + acc);
+def sum : Int -> Int := \(x : Int) sum' x 0;
+
+sum 100

tests/Geb/positive/Core/test016.jvc

@@ -0,0 +1,6 @@
+-- tail recursion: Fibonacci numbers in linear time
+
+def fib' : Int -> Int -> Int -> Int := \(n : Int) \(x : Int) \(y : Int) if n = 0 then x else fib' (n - 1) y (x + y);
+def fib : Int -> Int := \(n : Int) fib' n 0 1;
+
+fib 10

tests/Geb/positive/Core/test017.jvc

@@ -0,0 +1,7 @@
+-- recursion through higher-order functions
+
+def g : (Int -> Int) -> Int -> Int :=
+    \(f : Int -> Int) \(x : Int) if x = 0 then 0 else f (x - 1);
+def f : Int -> Int := \(x : Int) x + g f x;
+
+f 10 -- 55

tests/Geb/positive/Core/test018.jvc

@@ -0,0 +1,11 @@
+-- tail recursion through higher-order functions
+
+def sumb : (Int -> Int -> Int) -> Int -> Int -> Int :=
+    \(f : Int -> Int -> Int) \(x : Int) \(acc : Int)
+        if x = 0 then acc else f (x - 1) acc;
+def sum' : Int -> Int -> Int :=
+    \(x : Int) \(acc : Int) sumb sum' x (x + acc);
+def sum : Int -> Int :=
+    \(x : Int) sum' x 0;
+
+sum 100

tests/Geb/positive/Core/test019.jvc

@@ -0,0 +1,7 @@
+-- higher-order functions and recursion
+
+def f : (Int -> Int) -> Int := \(g : Int -> Int) g 5;
+def h : Int -> Int -> Int := \(x : Int) \(z : Int) x + z;
+def u  : Int -> Int := \(x : Int) f (h 4) + x;
+
+u 2 -- 11

tests/Geb/positive/Core/test020.jvc

@@ -0,0 +1,5 @@
+-- McCarthy's 91 function
+
+def f91 : Int -> Int := \(n : Int) if n > 100 then n - 10 else f91 (f91 (n + 11));
+
+f91 101 + f91 95 + f91 16 + f91 5

tests/Geb/positive/Core/test021.jvc

@@ -0,0 +1,13 @@
+-- fast exponentiation
+
+def power' : Int -> Int -> Int -> Int := \(a : Int) \(b : Int) \(acc : Int)
+  if b = 0 then
+    acc
+  else if b % 2 = 0 then
+    power' (a * a) (b / 2) acc
+  else
+    power' (a * a) (b / 2) (acc * a);
+
+def power : Int -> Int -> Int := \(a : Int) \(b : Int) power' a b 1;
+
+power 2 3 + power 3 7 + power 5 11

tests/Geb/positive/Core/test022.jvc

@@ -0,0 +1,28 @@
+-- mutual recursion
+
+def g : Int -> Int;
+
+def f : Int -> Int := \(x : Int) {
+  if x < 1 then
+    1
+  else
+    2 * x + g (x - 1)
+};
+
+def h : Int -> Int;
+
+def g : Int -> Int := \(x : Int) {
+  if x < 1 then
+    1
+  else
+    x + h (x - 1)
+};
+
+def h : Int -> Int := \(x : Int) {
+  if x < 1 then
+    1
+  else
+    x * f (x - 1)
+};
+
+f 5 + f 10

tests/Geb/positive/Core/test023.jvc

@@ -0,0 +1,16 @@
+-- Euclid's algorithm
+
+def gcd : Int -> Int -> Int := \(a : Int) \(b : Int) {
+  if a > b then
+    gcd b a
+  else if a = 0 then
+    b
+  else
+    gcd (b % a) a
+};
+
+gcd (3 * 7 * 2) (7 * 2) +
+gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5) +
+gcd 3 7 +
+gcd 7 3 +
+gcd (11 * 7 * 3) (2 * 5 * 13)

tests/Geb/positive/Core/test024.jvc

@@ -0,0 +1,11 @@
+-- Ackermann function
+
+def ack : Int -> Int -> Int := \(m : Int) \(n : Int)
+  if m = 0 then
+    n + 1
+  else if n = 0 then
+    ack (m - 1) 1
+  else
+    ack (m - 1) (ack m (n - 1));
+
+ack 0 7 + ack 1 7 + ack 1 13 + ack 2 7 + ack 2 13 + ack 3 4

tests/Geb/positive/Core/test025.jvc

@@ -0,0 +1,16 @@
+-- mid-square hashing
+
+def pow : Int -> Int := \(x : Int) if x = 0 then 1 else 2 * pow (x - 1);
+
+def hash' : Int -> Int -> Int := \(n : Int) \(x : Int)
+    if n <= 3 then
+        x * x
+    else if x < pow (n - 1) then
+        hash' (n - 1) x
+    else
+        ((x * x) / pow (n - 3)) % pow 6;
+
+def hash : Int -> Int := hash' 16;
+
+hash 1367
+-- result: 3

tests/Geb/positive/Eval/out/test014.geb

@@ -0,0 +1 @@
+5050

tests/Geb/positive/Eval/out/test015.geb

@@ -0,0 +1 @@
+5050

tests/Geb/positive/Eval/out/test016.geb

@@ -0,0 +1 @@
+55

tests/Geb/positive/Eval/out/test017.geb

@@ -0,0 +1 @@
+55

tests/Geb/positive/Eval/out/test018.geb

@@ -0,0 +1 @@
+5050

tests/Geb/positive/Eval/out/test019.geb

@@ -0,0 +1 @@
+11

tests/Geb/positive/Eval/out/test020.geb

@@ -0,0 +1 @@
+364

tests/Geb/positive/Eval/out/test021.geb

@@ -0,0 +1 @@
+48830320

tests/Geb/positive/Eval/out/test022.geb

@@ -0,0 +1 @@
+901

tests/Geb/positive/Eval/out/test023.geb

@@ -0,0 +1 @@
+87

tests/Geb/positive/Eval/out/test024.geb

@@ -0,0 +1 @@
+203

tests/Geb/positive/Eval/out/test025.geb

@@ -0,0 +1 @@
+3