Skip to content

Example which fails for js target Contracts fails for Contra too #1

Open
@Udiknedormin

Description

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.

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions