Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
Udiknedormin opened this issue Jun 20, 2020 · 1 comment
Open

Comments

@Udiknedormin
Copy link

Udiknedormin commented Jun 20, 2020

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
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant