在过去的几个月里,我一直在Agda工作,我刚刚遇到了abstractAgda的这个区块,这阻止了该区域范围之外的进一步规范化.
使用它来隐藏我的引理的工作方式大大减少了对我的程序进行类型检查所需的时间.然而,浏览Agda标准库abstract几乎没有使用.在我看来,几乎所有Properties文件中的所有内容(例如Data.Nat.Properties)都可以在一个abstract块内,因为我无法想到用于推理的用法,例如,如何证明加法是可交换的.
这是一个抽象的案例,是一个尚未进入标准库的新功能吗？或者是否有一些abstract我遗漏的标记证明的微妙或缺点？
我正在尝试分析用 Haskell 编写的中型编译器。在示例文件上运行它时，我得到以下分析数据：
vehicle +RTS -po.profiling/vehicle-1706073721 -p -RTS compile --target MarabouQueries --specification vehicle/tests/golden/compile/acasXu/spec.vcl --network acasXu:vehicle/tests/golden/compile/acasXu/fake.onnx
total time = 0.72 secs (716 ticks @ 1000 us, 1 processor)
total alloc = 1,558,506,104 bytes (excludes profiling overheads)
COST CENTRE MODULE SRC %time %alloc
fmap Vehicle.Prelude.Logging.Backend src/Vehicle/Prelude/Logging/Backend.hs:49:13-19 19.7 21.2
runVehicle.\ Vehicle src/Vehicle.hs:(56,46)-(67,52) 12.2 19.3
fmap Vehicle.Prelude.Supply src/Vehicle/Prelude/Supply.hs:28:13-19 9.1 8.2
compileDecls Vehicle.Backend.Queries src/Vehicle/Backend/Queries.hs:(87,1)-(101,47) 5.7 7.2
$mRelevantExplicitArg.\ Vehicle.Syntax.AST.Arg src/Vehicle/Syntax/AST/Arg.hs:51:36-60 5.6 5.4
>>= Vehicle.Prelude.Logging.Backend src/Vehicle/Prelude/Logging/Backend.hs:49:35-39 4.3 2.9
fmap Vehicle.Compile.Context.Free.Instance src/Vehicle/Compile/Context/Free/Instance.hs:24:13-19 4.3 4.2
>>= Vehicle.Prelude.Supply src/Vehicle/Prelude/Supply.hs:28:35-39 3.2 …