[ Fix #1577 ] Actually use natMinus hack (#1578)

And also make sure that the output is truncated to 0.

Co-authored-by: Guillaume ALLAIS <[email protected]>

Author: redfish64

libs/prelude/Prelude/Types.idr

@@ -33,7 +33,7 @@ prim__integerToNat i
 
 public export
 integerToNat : Integer -> Nat
-integerToNat 0 = Z -- Force evaluation and hencing caching of x at compile time
+integerToNat 0 = Z -- Force evaluation and hence caching of x at compile time
 integerToNat x
   = if intToBool (prim__lte_Integer x 0)
        then Z

src/Compiler/CompileExpr.idr

@@ -176,21 +176,32 @@ magic ms e = go ms e where
     Nothing => go ms e
     Just e' => e'
 
-natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
-natMinus fc fc' [m,n] = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]
+%inline
+magic__integerToNat : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
+magic__integerToNat fc fc' [k]
+  = CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k]
+
+magic__natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
+magic__natMinus fc fc' [m,n]
+  = magic__integerToNat fc fc'
+    [CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]]
+
+-- We don't reuse natMinus here because we assume that unsuc will only be called
+-- on S-headed numbers so we do not need the truncating integerToNat call!
+magic__natUnsuc : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
+magic__natUnsuc fc fc' [m]
+  = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, CPrimVal fc (BI 1)]
 
 -- TODO: next release remove this and use %builtin pragma
 natHack : List Magic
 natHack =
-    [ MagicCRef (NS typesNS (UN "natToInteger")) 1
-         (\ _, _, [k] => k)
-    , MagicCRef (NS typesNS (UN "integerToNat")) 1
-         (\ fc, fc', [k] => CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k])
+    [ MagicCRef (NS typesNS (UN "natToInteger")) 1 (\ _, _, [k] => k)
+    , MagicCRef (NS typesNS (UN "integerToNat")) 1 magic__integerToNat
     , MagicCRef (NS typesNS (UN "plus")) 2
          (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
     , MagicCRef (NS typesNS (UN "mult")) 2
          (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
-    , MagicCRef (NS natNS (UN "minus")) 2 natMinus
+    , MagicCRef (NS typesNS (UN "minus")) 2 magic__natMinus
     ]
 
 -- get all transformation from %builtin pragmas
@@ -237,7 +248,7 @@ trySBranch :
 trySBranch ss n (MkConAlt nm _ _ [arg] sc)
   = do guard $ isJust $ lookup nm ss
        let fc = getFC n
-       pure (CLet fc arg True (natMinus fc fc [n, CPrimVal fc (BI 1)]) sc)
+       pure (CLet fc arg True (magic__natUnsuc fc fc [n]) sc)
 trySBranch _ _ _ = Nothing
 
 tryZBranch :

src/Idris/Package.idr

@@ -711,6 +711,7 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
     optType (OutputDir f)          = POpt
     optType WarningsAsErrors       = POpt
     optType HashesInsteadOfModTime = POpt
+    optType Profile                = POpt
     optType (ConsoleWidth n)       = PIgnore
     optType (Color b)              = PIgnore
     optType NoBanner               = PIgnore

tests/Main.idr

@@ -123,7 +123,7 @@ idrisTestsRegression = MkTestPool "Various regressions" []
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
        "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
-       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041"]
+       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042"]
 
 idrisTestsData : TestPool
 idrisTestsData = MkTestPool "Data and record types" []

tests/idris2/reg042/NatSpeedBug.idr

@@ -0,0 +1,68 @@
+module NatSpeedBug
+
+import System
+import System.Clock
+import Data.List
+import Data.Nat
+import Data.String
+
+timeit : Lazy x -> IO (x,Clock Duration)
+timeit x =
+  do
+    start <- clockTime Monotonic
+    let x' = force x
+    end <- clockTime Monotonic
+    pure (x', timeDifference end start)
+
+v1 : Nat
+v1 = 100000000
+
+v2 : Nat
+v2 = 100000000
+
+v3 : Nat
+v3 = 100000001
+
+test : List (Lazy Bool)
+test =
+ [
+   --fast ops
+   delay $ (natToInteger $ v1 + v2) == 200000000
+  ,delay $ (natToInteger $ 2 * v1) ==  200000000
+  ,delay $ (v1 `minus` v2) == 0    --should be fast, but is slow
+  ,delay $ (natToInteger v1) ==      100000000
+  ,delay $ const True (integerToNat  100000000)
+ ]
+
+toNano : Clock type -> Integer
+toNano (MkClock seconds nanoseconds) =
+  let scale = 1000000000
+   in scale * seconds + nanoseconds
+
+main : IO ()
+main =
+  do
+    cutOff <- getCutoffArg
+    ignore $ traverse (prnIt cutOff) (zip [0..length test] test)
+    pure ()
+  where
+    getCutoffArg : IO (Maybe Integer)
+    getCutoffArg =
+      do
+        args <- getArgs
+        let (_ :: cutoffStr :: _) = args
+               | x => pure Nothing
+        let cutOff = cast $ stringToNatOrZ cutoffStr
+        pure $ if cutOff == 0 then Nothing else Just cutOff
+
+    showit : Bool -> String -> String -> String
+    showit v a b = if v then a else b
+    prnIt : (Maybe Integer) -> (Nat, Lazy Bool) -> IO ()
+    prnIt mCutOff (ind, lb) =
+        do
+          (b, diff) <- timeit lb
+          putStrLn $ (show ind) ++ ": " ++ showit b "Pass" "Fail" ++ " " ++
+             maybe
+               (show diff)
+               (\co => showit (toNano diff < co) "Fast" "Slow")
+               mCutOff

tests/idris2/reg042/expected

@@ -0,0 +1,6 @@
+1/1: Building NatSpeedBug (NatSpeedBug.idr)
+0: Pass Fast
+1: Pass Fast
+2: Pass Fast
+3: Pass Fast
+4: Pass Fast

tests/idris2/reg042/nsb.ipkg

@@ -0,0 +1,6 @@
+package nsb
+
+modules = NatSpeedBug
+
+executable = nsb
+main = NatSpeedBug

tests/idris2/reg042/run

@@ -0,0 +1,4 @@
+$1 --build nsb.ipkg
+build/exec/nsb 100000
+
+rm -rf build