Example which fails for js target Contracts fails for Contra too
Udiknedormin opened this issue · 1 comments
Udiknedormin commented
In the README, it's suggested that Contra can handle the following example code that Contracts fail on:
import contracts
from math import sqrt, floor
proc isqrt[T: SomeInteger](x: T): T {.contractual.} =
require:
x >= 0
ensure:
result * result <= x
(result+1) * (result+1) > x
body:
(T)(x.toBiggestFloat().sqrt().floor().toBiggestInt())
echo isqrt(18) # prints 4
echo isqrt(-8) # runtime error:
# broke 'x >= 0' promised at FILE.nim(LINE,COLUMN)
# [PreConditionError]
(which fails with deepCopy
not being found, which is reported as a JS backend issue)
When rewritten with Contra, as:
import contra
from math import sqrt, floor
proc isqrt[T: SomeInteger](x: T): T =
preconditions(x >= 0)
postconditions(result * result <= x, (result+1) * (result+1) > x)
result = (T)(x.toBiggestFloat().sqrt().floor().toBiggestInt())
echo isqrt(18) # prints 4
echo isqrt(-8) # runtime error
compilation "nim js example.nim" fails:
$ nim js -r example.nim
(...)/.nimble/pkgs/contra-0.2.5/contra.nim(70, 27) Error: type mismatch: got <byte>
but expected one of:
proc `$`(arg: LineInfo): string
first type mismatch at position: 1
required type for arg: LineInfo
but expression 'i' is of type: byte
proc `$`(i: NimIdent): string
first type mismatch at position: 1
required type for i: NimIdent
but expression 'i' is of type: byte
(...)
proc `$`[T](x: set[T]): string
first type mismatch at position: 1
required type for x: set[T]
but expression 'i' is of type: byte
expression: $i
I'm running it on Linux with Nim v1.2.0.
Udiknedormin commented
Update: Contracts no longer fails on that example for JS target at all (missing deepCopy
issue of JS target has been avoided in Contracts).