juancarlospaco/nim-contra

Example which fails for js target Contracts fails for Contra too

Udiknedormin opened this issue · 1 comments

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.

Update: Contracts no longer fails on that example for JS target at all (missing deepCopy issue of JS target has been avoided in Contracts).