为什么在IDRIS中，“时钟时间”似乎不起作用？

Question

可能有库可以执行此操作（尽管我还没有找到任何），我实际上是在衡量函数在IDRIS中运行的时间。我发现的方式是使用 ClockTime 从 System 中使用，并在函数运行之前和之后区分。这是一个示例代码：

module Main

import Data.String
import System

factorial : Integer -> Integer
factorial 0 = 1
factorial 1 = 1
factorial n = n * factorial (n - 1)

main : IO ()
main = do
    args <- getArgs

    case args of
        [self ] => putStrLn "Please enter a value"
        [_, ar] => do
            case parseInteger ar of
                Just a => do

                    t1 <- clockTime
                    let r = factorial a
                    t2 <- clockTime

                    let elapsed = (nanoseconds t2) - (nanoseconds t1)

                    putStrLn $ "fact(" ++ show a ++ ") = "
                                       ++ show r ++ " in "
                                       ++ (show elapsed) ++ " ns"

                Nothing => putStrLn "Not a valid number"

为了避免IDRI通过已经评估阶乘来优化程序，我只是要求与参数调用该程序。

但是，该代码不起作用：无论我输入什么数字，例如 10000 ，idris总是返回0纳秒，这使我非常怀疑，甚至只分配一个bigint会花费时间。我使用 iDris main.idr -o main 编译。

我在代码中做错了什么？ 时钟时间不是基准的好计划吗？

Answer 1

IDRIS 1不再维护。
在IDRIS 2中，可以使用。

clockTime : (typ : ClockType) -> IO (clockTimeReturnType typ)

可以在IDRIS2编译器中找到其用于基准测试的一个示例l120“ rel =“ nofollow noreferrer”>在这里。