Add fail nodes to Geb

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")
   ]