Literal type inference oddity with hex and octal

[LeventErkok]

Cryptol2 seems to treat hex-literals weirdly when it comes to type checking. To wit:

Cryptol> 411:[32]
411
Cryptol> 0x19b:[32]

[error] at <interactive>:1:1--1:11:
  Type mismatch:
    Expected type: 32
    Inferred type: 12

This is truly bizarre. For instance, there appears to be absolutely no way of writing a 11 bit literal in hex:

Cryptol> 0x3:[11]

[error] at <interactive>:1:1--1:9:
  Type mismatch:
    Expected type: 11
    Inferred type: 4
Cryptol> 0x03:[11]

[error] at <interactive>:1:1--1:10:
  Type mismatch:
    Expected type: 11
    Inferred type: 8
Cryptol> 0x003:[11]

[error] at <interactive>:1:1--1:11:
  Type mismatch:
    Expected type: 11
    Inferred type: 12
Cryptol> 0x0003:[11]

[error] at <interactive>:1:1--1:12:
  Type mismatch:
    Expected type: 11
    Inferred type: 16

A similar experiment with octal (0o) shows it has the same problem.

[weaversa]

One can write an 11 bit literal in hex using backtick:

(`0x3):[11]

Sorry! Talk to John :-)

On May 31, 2014, at 1:49 PM, Levent Erkok notifications@github.com wrote:

Cryptol2 seems to treat hex-literals weirdly when it comes to type checking. To wit:

Cryptol> 411:[32]
411
Cryptol> 0x19b:[32]

[error] at :1:1--1:11:
Type mismatch:
Expected type: 32
Inferred type: 12
This is truly bizarre. For instance, there appears to be absolutely no way of writing a 11 bit literal in hex:

Cryptol> 0x3:[11]

[error] at :1:1--1:9:
Type mismatch:
Expected type: 11
Inferred type: 4
Cryptol> 0x03:[11]

[error] at :1:1--1:10:
Type mismatch:
Expected type: 11
Inferred type: 8
Cryptol> 0x003:[11]

[error] at :1:1--1:11:
Type mismatch:
Expected type: 11
Inferred type: 12
Cryptol> 0x0003:[11]

[error] at :1:1--1:12:
Type mismatch:
Expected type: 11
Inferred type: 16
A similar experiment with octal (0o) shows it has the same problem.

—
Reply to this email directly or view it on GitHub.

[LeventErkok]

ah, the magic backtick..

seriously though; a literal is a literal is a literal; the base you write it in shouldn't really matter, methinks..

[weaversa]

Though I agree with you, some folks see it some other way. I stopped the
fight when I figured out the backtick workaround.

On Sat, May 31, 2014 at 2:38 PM, Levent Erkok notifications@github.com
wrote:

ah, the magic backtick..

seriously though; a literal is a literal is a literal; the base you write
it in shouldn't really matter, methinks..

—
Reply to this email directly or view it on GitHub
#30 (comment).

[weaversa]

Also, because you’re going to undoubtedly run:

:sat (a, b) -> if ((a:[32]) != b) then (fnv1a a) == (fnv1a b) else False

Know that the AIGs generated cause an error in an old bit of ABC, namely the ‘cec’ command. I spoke w/ Alan and he says it is a known bug, and the reason he added ‘dcec’, but he has not removed the broken ‘cec’ command. Of course, one can also use ‘&cec’.

On May 31, 2014, at 1:49 PM, Levent Erkok notifications@github.com wrote:

Cryptol2 seems to treat hex-literals weirdly when it comes to type checking. To wit:

Cryptol> 411:[32]
411
Cryptol> 0x19b:[32]

[error] at :1:1--1:11:
Type mismatch:
Expected type: 32
Inferred type: 12
This is truly bizarre. For instance, there appears to be absolutely no way of writing a 11 bit literal in hex:

Cryptol> 0x3:[11]

[error] at :1:1--1:9:
Type mismatch:
Expected type: 11
Inferred type: 4
Cryptol> 0x03:[11]

[error] at :1:1--1:10:
Type mismatch:
Expected type: 11
Inferred type: 8
Cryptol> 0x003:[11]

[error] at :1:1--1:11:
Type mismatch:
Expected type: 11
Inferred type: 12
Cryptol> 0x0003:[11]

[error] at :1:1--1:12:
Type mismatch:
Expected type: 11
Inferred type: 16
A similar experiment with octal (0o) shows it has the same problem.

—
Reply to this email directly or view it on GitHub.

[kiniry]

We'll park this for the moment, since it involves some fundamental design aspects that have work-arounds (that are not viewed as work-arounds by some). Let's make sure this is documented well in the book.

[kiniry]

See #52.