Add debugging builtin functions trace and fail (#1771)

- Closes #1731

Makefile

@@ -140,7 +140,7 @@ ORMOLUMODE?=inplace
 
 .PHONY: format
 format: clang-format
-	${ORMOLU} ${ORMOLUFLAGS} \
+	@${ORMOLU} ${ORMOLUFLAGS} \
 		--ghc-opt -XStandaloneDeriving \
 		--ghc-opt -XUnicodeSyntax \
 		--ghc-opt -XDerivingStrategies \

src/Juvix/Compiler/Abstract/Extra/Functions.hs

@@ -287,6 +287,7 @@ a === b = (toExpression a ==% toExpression b) mempty
 
 infix 4 ==%
 
+-- TODO: make it symmetric
 (==%) :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
 (==%) a b free =
   isRight

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -261,7 +261,7 @@ registerBuiltinFunction d = \case
   BuiltinBoolAnd -> registerAnd d
 
 registerBuiltinAxiom ::
-  (Members '[InfoTableBuilder, Error ScoperError, Builtins] r) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) =>
   Abstract.AxiomDef ->
   BuiltinAxiom ->
   Sem r ()
@@ -272,6 +272,8 @@ registerBuiltinAxiom d = \case
   BuiltinString -> registerString d
   BuiltinStringPrint -> registerStringPrint d
   BuiltinBoolPrint -> registerBoolPrint d
+  BuiltinTrace -> registerTrace d
+  BuiltinFail -> registerFail d
 
 goInductive ::
   (Members '[InfoTableBuilder, Builtins, Error ScoperError] r) =>
@@ -396,7 +398,7 @@ goExpression = \case
       r' <- goExpression r
       return (Abstract.Application l'' r' Explicit)
 
-goLambda :: forall r. Members '[Error ScoperError, InfoTableBuilder] r => Lambda 'Scoped -> Sem r Abstract.Lambda
+goLambda :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Lambda 'Scoped -> Sem r Abstract.Lambda
 goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses)
   where
     goClause :: LambdaClause 'Scoped -> Sem r Abstract.LambdaClause
@@ -504,7 +506,7 @@ goPattern p = case p of
   PatternWildcard i -> return (Abstract.PatternWildcard i)
   PatternEmpty {} -> return Abstract.PatternEmpty
 
-goAxiom :: (Members '[InfoTableBuilder, Error ScoperError, Builtins] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
+goAxiom :: (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
 goAxiom a = do
   _axiomType' <- goExpression (a ^. axiomType)
   let axiom =

src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs

@@ -24,6 +24,8 @@ builtinAxiomName = \case
   BuiltinString -> Just string_
   BuiltinStringPrint -> Just printString
   BuiltinBoolPrint -> Just printBool
+  BuiltinTrace -> Just trace_
+  BuiltinFail -> Just fail_
 
 builtinFunctionName :: BuiltinFunction -> Maybe Text
 builtinFunctionName = \case

src/Juvix/Compiler/Backend/C/Data/CNames.hs

@@ -80,6 +80,12 @@ boolor = primPrefix "or"
 booland :: Text
 booland = primPrefix "and"
 
+trace_ :: Text
+trace_ = "trace"
+
+fail_ :: Text
+fail_ = "fail"
+
 funField :: Text
 funField = "fun"
 

src/Juvix/Compiler/Builtins.hs

@@ -4,10 +4,12 @@ module Juvix.Compiler.Builtins
     module Juvix.Compiler.Builtins.IO,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.String,
+    module Juvix.Compiler.Builtins.Debug,
   )
 where
 
 import Juvix.Compiler.Builtins.Bool
+import Juvix.Compiler.Builtins.Debug
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Nat

src/Juvix/Compiler/Builtins/Debug.hs

@@ -0,0 +1,30 @@
+module Juvix.Compiler.Builtins.Debug where
+
+import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Abstract.Extra
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Prelude
+
+registerTrace :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerTrace f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse (Universe {_universeLevel = Nothing, _universeLoc = error "Universe with no location"})
+  a <- freshVar "a"
+  b <- freshVar "b"
+  let freeVars = HashSet.fromList [a, b]
+  unless
+    (((u <>--> u <>--> a --> b --> b) ==% ftype) freeVars)
+    (error "trace must be of type {A : Type} -> {B : Type} -> A -> B -> B")
+  registerBuiltin BuiltinTrace (f ^. axiomName)
+
+registerFail :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
+registerFail f = do
+  let ftype = f ^. axiomType
+      u = ExpressionUniverse (Universe {_universeLevel = Nothing, _universeLoc = error "Universe with no location"})
+  a <- freshVar "a"
+  let freeVars = HashSet.fromList [a]
+  string_ <- getBuiltinName (getLoc f) BuiltinString
+  unless
+    (((u <>--> string_ --> a) ==% ftype) freeVars)
+    (error "fail must be of type {A : Type} -> String -> A")
+  registerBuiltin BuiltinFail (f ^. axiomName)

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -100,6 +100,8 @@ data BuiltinAxiom
   | BuiltinString
   | BuiltinIO
   | BuiltinIOSequence
+  | BuiltinTrace
+  | BuiltinFail
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinAxiom
@@ -112,3 +114,5 @@ instance Pretty BuiltinAxiom where
     BuiltinIO -> Str.io
     BuiltinString -> Str.string
     BuiltinIOSequence -> Str.ioSequence
+    BuiltinTrace -> Str.trace_
+    BuiltinFail -> Str.fail_

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -365,6 +365,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinIOSequence -> return ()
       Internal.BuiltinString -> registerInductiveAxiom
       Internal.BuiltinIO -> registerInductiveAxiom
+      Internal.BuiltinTrace -> return ()
+      Internal.BuiltinFail -> return ()
 
     registerInductiveAxiom :: Sem r ()
     registerInductiveAxiom = do
@@ -423,6 +425,9 @@ goAxiomDef a = case a ^. Internal.axiomBuiltin >>= builtinBody of
           )
       Internal.BuiltinString -> Nothing
       Internal.BuiltinIO -> Nothing
+      Internal.BuiltinTrace -> Nothing
+      Internal.BuiltinFail ->
+        Just (mkLambda' (mkLambda' (mkBuiltinApp' OpFail [mkVar' 0])))
 
     axiomType' :: Sem r Type
     axiomType' = runReader initIndexTable (goExpression (a ^. Internal.axiomType))
@@ -652,6 +657,23 @@ goApplication a = do
         mkApps' fExpr <$> exprArgs
 
   case f of
+    Internal.ExpressionIden (Internal.IdenAxiom n) -> do
+      axiomInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoAxioms)
+      case axiomInfo ^. Internal.axiomInfoBuiltin of
+        Just Internal.BuiltinNatPrint -> app
+        Just Internal.BuiltinStringPrint -> app
+        Just Internal.BuiltinBoolPrint -> app
+        Just Internal.BuiltinString -> app
+        Just Internal.BuiltinIO -> app
+        Just Internal.BuiltinIOSequence -> app
+        Just Internal.BuiltinTrace -> do
+          as <- exprArgs
+          case as of
+            (_ : _ : arg1 : arg2 : xs) ->
+              return (mkApps' (mkBuiltinApp' OpTrace [arg1, arg2]) xs)
+            _ -> error "trace must be called with 2 arguments"
+        Just Internal.BuiltinFail -> app
+        Nothing -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
       funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions)
       case funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin of

test/Typecheck/Positive.hs

@@ -189,7 +189,15 @@ tests =
     posTest
       "Issue 1704 (Type synonyms)"
       $(mkRelDir "Internal")
-      $(mkRelFile "Synonyms.juvix")
+      $(mkRelFile "Synonyms.juvix"),
+    posTest
+      "Issue 1731 Trace builtin for debugging"
+      $(mkRelDir "issue1731")
+      $(mkRelFile "builtinTrace.juvix"),
+    posTest
+      "Issue 1731 Fail builtin for debugging"
+      $(mkRelDir "issue1731")
+      $(mkRelFile "builtinFail.juvix")
   ]
     <> [ compilationTest t | t <- Compilation.tests, t ^. Compilation.name /= "Self-application"
        ]

tests/Core/benchmark/test004.jvc

@@ -1,7 +1,9 @@
 -- streams without memoization
 
-constr nil 0;
-constr cons 2;
+type list {
+  nil : list;
+  cons : any -> list -> list;
+};
 
 def force := \f f nil;
 

tests/Core/negative/test005.jvc

@@ -1,7 +1,10 @@
 -- no matching case branch
 
-constr cons 2;
+type list {
+  nil : list;
+  cons : any -> list -> list;
+};
 
-case cons 1 2 of {
+case cons 1 nil of {
   nil -> true
 }

tests/Core/negative/test009.jvc

@@ -1,6 +1,8 @@
 -- erroneous Church numerals
 
-constr pair 2;
+type product {
+  pair : any -> any -> product;
+};
 
 def fst := \p case p of { pair x _ -> x };
 def snd := \p case p of { pair _ x -> x };

tests/Core/positive/test034.jvc

@@ -2,18 +2,16 @@
 
 def g := \x trace x g;
 
-def f := \x \y
-  if x = 0 then
-    9
-  else
-    trace 1 (f (x - 1) (y 0));
+def f := \x \y if x = 0 then 9 else trace 1 (f (x - 1) (y 0));
 
 def h := \x trace 8 (trace x (x + x));
 
 def const := \x \y x;
 
-constr nil 0;
-constr cons 2;
+type list {
+  nil : list;
+  cons : any -> list -> list;
+};
 
 trace (const 0 (trace "!" 1)) (
 trace (const 0 (cons (trace "a" 1) (trace "b" (cons (trace "c" 1) (trace "d" nil))))) (

tests/positive/issue1731/builtinFail.juvix

@@ -0,0 +1,10 @@
+module builtinFail;
+  open import Stdlib.Prelude;
+
+  builtin fail axiom fail : {A : Type} → String → A;
+
+  main : IO;
+  main := printStringLn "Get"
+    >> fail "Enough"
+    >> printStringLn "Sleep";
+end;

tests/positive/issue1731/builtinTrace.juvix

@@ -0,0 +1,25 @@
+module builtinTrace;
+  open import Stdlib.Prelude;
+  open import Stdlib.Data.Nat.Ord;
+
+  builtin trace axiom trace : {A : Type} → {B : Type} → A → B → B;
+
+  terminating
+  f : Nat → Nat → Nat;
+  f x y := if (x == 0) y (trace x (f (sub x 1) y));
+
+{-
+f 4 0 =
+trace 4 (f 3 0)
+=> trace 4 (trace 3 (f 2 0))
+=> trace 4 (trace 3 (trace 2 (f 1 0)))
+=> trace 4 (trace 3 (trace 2 (trace 1 (f 0 0))))
+=> trace 4 (trace 3 (trace 2 (trace 1 0)))
+= 0
+
+𝔸 β \X \Y . Apply (Apply trace X) Y 
+
+-}
+  main : IO;
+  main := printNatLn $ f 4 0;
+end;

tests/smoke/Commands/repl.smoke.yaml

@@ -199,3 +199,48 @@ tests:
       contains: |
         suc (suc (suc zero))
     exit-status: 0
+
+  - name: repl-trace
+    command:
+      - juvix 
+      - repl
+    args:
+      - positive/issue1731/builtinTrace.juvix
+    stdin: trace 2 (printNatLn 3)
+    stdout: 
+      contains: |
+        suc (suc (suc zero))
+    stderr: |
+        suc (suc zero)
+    exit-status: 0
+
+  - name: repl-trace-file
+    command:
+      - juvix 
+      - repl
+    args:
+      - positive/issue1731/builtinTrace.juvix
+    stdin: f 4 0
+    stdout: 
+      contains: |
+       zero
+    stderr: |
+       suc (suc (suc (suc zero)))
+       suc (suc (suc zero))
+       suc (suc zero)
+       suc zero
+    exit-status: 0
+
+  - name: repl-fail
+    command:
+      - juvix 
+      - repl
+    args:
+      - positive/issue1731/builtinFail.juvix
+    stdin: main
+    stdout:
+      contains: builtinFail> builtinFail>
+    stderr:
+      contains: |
+        evaluation error: failure: Enough
+    exit-status: 0