Make '>>' lazy (#1812)

* Closes #1773 * Closes #1817
anoma · Feb 9, 2023 · 0ee8bdf · 0ee8bdf
1 parent 10c3478
commit 0ee8bdf
Show file tree

Hide file tree

Showing 5 changed files with 70 additions and 48 deletions.
diff --git a/juvix-stdlib b/juvix-stdlib
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -447,16 +447,7 @@ goAxiomDef a = do
       Internal.BuiltinNatPrint -> Just writeLambda
       Internal.BuiltinStringPrint -> Just writeLambda
       Internal.BuiltinBoolPrint -> Just writeLambda
-      Internal.BuiltinIOSequence ->
-        Just
-          ( mkLambda'
-              ( mkLambda'
-                  ( mkConstr'
-                      (BuiltinTag TagBind)
-                      [mkVar' 1, mkLambda' (mkVar' 1)]
-                  )
-              )
-          )
+      Internal.BuiltinIOSequence -> Nothing
       Internal.BuiltinIOReadline ->
         Just
           ( mkLambda'
@@ -633,6 +624,12 @@ goExpression' = \case
       varsNum <- asks (^. indexTableVarsNum)
       return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1))
     Internal.IdenFunction n -> do
+      funInfoBuiltin <- getFunctionBuiltinInfo n
+      case funInfoBuiltin of
+        Just Internal.BuiltinBoolIf -> error "if must be called with 3 arguments"
+        Just Internal.BuiltinBoolOr -> error "|| must be called with 2 arguments"
+        Just Internal.BuiltinBoolAnd -> error "&& must be called with 2 arguments"
+        _ -> return ()
       -- if the function was defined by a let, then in Core it is stored in a variable
       vars <- asks (^. indexTableVars)
       case HashMap.lookup id_ vars of
@@ -658,6 +655,11 @@ goExpression' = \case
         Just _ -> error ("internal to core: not a constructor " <> txt)
         Nothing -> error ("internal to core: undeclared identifier: " <> txt)
     Internal.IdenAxiom n -> do
+      axiomInfoBuiltin <- getAxiomBuiltinInfo n
+      case axiomInfoBuiltin of
+        Just Internal.BuiltinIOSequence -> error ">> must be called with 2 arguments"
+        Just Internal.BuiltinTrace -> error "trace must be called with 2 arguments"
+        _ -> return ()
       m <- getIdent identIndex
       return $ case m of
         Just (IdentFun sym) -> mkIdent (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) sym
@@ -719,14 +721,19 @@ goApplication a = do
 
   case f of
     Internal.ExpressionIden (Internal.IdenAxiom n) -> do
-      axiomInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoAxioms)
-      case axiomInfo ^. Internal.axiomInfoBuiltin of
+      axiomInfoBuiltin <- getAxiomBuiltinInfo n
+      case 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.BuiltinIOSequence -> do
+          as <- exprArgs
+          case as of
+            (arg1 : arg2 : xs) ->
+              return (mkApps' (mkConstr' (BuiltinTag TagBind) [arg1, mkLambda' (shift 1 arg2)]) xs)
+            _ -> error ">> must be called with 2 arguments"
         Just Internal.BuiltinIOReadline -> app
         Just Internal.BuiltinStringConcat -> app
         Just Internal.BuiltinStringEq -> app
@@ -741,8 +748,8 @@ goApplication a = do
         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
+      funInfoBuiltin <- getFunctionBuiltinInfo n
+      case funInfoBuiltin of
         Just Internal.BuiltinBoolIf -> do
           sym <- getBoolSymbol
           as <- exprArgs
@@ -771,3 +778,17 @@ goLiteral intToNat l = case l ^. withLocParam of
   where
     mkLitConst :: ConstantValue -> Node
     mkLitConst = mkConstant (Info.singleton (LocationInfo (l ^. withLocInt)))
+
+getAxiomBuiltinInfo :: Member (Reader Internal.InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom)
+getAxiomBuiltinInfo n = do
+  maybeAxiomInfo <- HashMap.lookup n <$> asks (^. Internal.infoAxioms)
+  return $ case maybeAxiomInfo of
+    Just axiomInfo -> axiomInfo ^. Internal.axiomInfoBuiltin
+    Nothing -> Nothing
+
+getFunctionBuiltinInfo :: Member (Reader Internal.InfoTable) r => Name -> Sem r (Maybe BuiltinFunction)
+getFunctionBuiltinInfo n = do
+  maybeFunInfo <- HashMap.lookup n <$> asks (^. Internal.infoFunctions)
+  return $ case maybeFunInfo of
+    Just funInfo -> funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin
+    Nothing -> Nothing
diff --git a/tests/positive/issue1731/builtinFail.juvix b/tests/positive/issue1731/builtinFail.juvix
@@ -7,4 +7,4 @@ module builtinFail;
   main := printStringLn "Get"
     >> fail "Enough"
     >> printStringLn "Sleep";
-end;
+end;
diff --git a/tests/positive/issue1731/builtinTrace.juvix b/tests/positive/issue1731/builtinTrace.juvix
@@ -17,9 +17,9 @@ trace 4 (f 3 0)
 => trace 4 (trace 3 (trace 2 (trace 1 0)))
 = 0
 
-𝔸 β \X \Y . Apply (Apply trace X) Y 
+𝔸 β \X \Y . Apply (Apply trace X) Y
 
 -}
   main : IO;
   main := printNatLn $ f 4 0;
-end;
+end;
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
@@ -8,12 +8,12 @@ tests:
     stdout:
       contains: "Juvix REPL"
     exit-status: 0
-    
+
   - name: quit
     command:
       - juvix
       - repl
-    stdout: 
+    stdout:
       contains: "Juvix REPL"
     stdin: ":quit"
     exit-status: 0
@@ -41,7 +41,7 @@ tests:
           OK loaded: .*
           Stdlib.Prelude> \1
     exit-status: 0
-    
+
   - name: check-type-null
     command:
       - juvix
@@ -55,7 +55,7 @@ tests:
     command:
       - juvix
       - repl
-    stdout: 
+    stdout:
       contains: "Nat → Nat"
     stdin: ":type suc"
     exit-status: 0
@@ -64,50 +64,50 @@ tests:
     command:
       - juvix
       - repl
-    stdout: 
+    stdout:
       contains: "Nat → Nat"
     stdin: ":t suc"
-    exit-status: 0    
+    exit-status: 0
 
   - name: check-type-suc-short-stdlib
     command:
       shell:
         - bash
       script: |
         cd ./../juvix-stdlib && juvix repl
-    stdout: 
+    stdout:
       contains: "Nat → Nat"
     stdin: ":t suc"
-    exit-status: 0    
+    exit-status: 0
 
   - name: eval-and-operations
     command:
       - juvix
       - repl
     stdin: "true && false"
-    stdout: 
+    stdout:
       matches: |
         Juvix REPL .*
         OK loaded: .*
         Stdlib.Prelude> false
-    exit-status: 0    
+    exit-status: 0
 
   - name: eval-and-operations-with-spaces
     command:
       - juvix
       - repl
     stdin: "   true    &&    false"
-    stdout: 
+    stdout:
       contains:
         "false"
-    exit-status: 0    
+    exit-status: 0
 
   - name: eval-suc-true
     command:
       - juvix
       - repl
     stdin: "suc true"
-    stdout: 
+    stdout:
       contains:
         "Stdlib.Prelude> "
     stderr:
@@ -116,7 +116,7 @@ tests:
           Bool
         but is expected to have type:
           Nat
-    exit-status: 0 
+    exit-status: 0
 
   - name: eval-let-expression
     command:
@@ -137,7 +137,7 @@ tests:
     stdin: ":load BuiltinBool.juvix"
     stdout:
       contains:
-        BuiltinBool>  
+        BuiltinBool>
     exit-status: 0
 
   - name: load-builtin-bool-with-spaces
@@ -147,9 +147,9 @@ tests:
       script: |
         cd ./Internal/positive/ && juvix repl
     stdin: ":load    BuiltinBool.juvix"
-    stdout: 
+    stdout:
       contains:
-        BuiltinBool> 
+        BuiltinBool>
     exit-status: 0
 
   - name: load-builtin-bool-short-form
@@ -161,29 +161,29 @@ tests:
     stdin: |
       :l BuiltinBool.juvix
       main
-    stdout: 
+    stdout:
       contains: |
         true
     exit-status: 0
 
   - name: repl-file
     command:
-      - juvix 
+      - juvix
       - repl
     args:
       - Internal/positive/BuiltinBool.juvix
     stdin: main
-    stdout: 
+    stdout:
       contains: |
         true
     exit-status: 0
-    
+
   - name: root
     command:
       - juvix
       - repl
     stdin: ":root"
-    stdout: 
+    stdout:
       matches: |
         Juvix REPL .*
         OK loaded: .*
@@ -195,19 +195,19 @@ tests:
       - juvix
       - repl
     stdin: "1 + 2"
-    stdout: 
+    stdout:
       contains: |
         suc (suc (suc zero))
     exit-status: 0
 
   - name: repl-trace
     command:
-      - juvix 
+      - juvix
       - repl
     args:
       - positive/issue1731/builtinTrace.juvix
     stdin: trace 2 (printNatLn 3)
-    stdout: 
+    stdout:
       contains: |
         suc (suc (suc zero))
     stderr: |
@@ -216,12 +216,12 @@ tests:
 
   - name: repl-trace-file
     command:
-      - juvix 
+      - juvix
       - repl
     args:
       - positive/issue1731/builtinTrace.juvix
     stdin: f 4 0
-    stdout: 
+    stdout:
       contains: |
        zero
     stderr: |
@@ -233,13 +233,14 @@ tests:
 
   - name: repl-fail
     command:
-      - juvix 
+      - juvix
       - repl
     args:
       - positive/issue1731/builtinFail.juvix
     stdin: main
     stdout:
-      contains: builtinFail> builtinFail>
+      contains: |
+        Get
     stderr:
       contains: |
         evaluation error: failure: Enough