querycert / qcert

Compilation and Verification of Data-Centric Languages
https://querycert.github.io/
Apache License 2.0
56 stars 9 forks source link

Type inference for binary operators has inconsistent output #103

Closed kach closed 6 years ago

kach commented 6 years ago

The order of the elements in the output of infer_binary_op_type_sub isn't consistent across the various operators. For example, OpLt returns Some (Bool, Nat, Nat), i.e. (output, input, input) (source), whereas OpFloatCompare returns Some (Float, Float, Bool), i.e. (input, input, output) (source). This makes it hard to extract the output type of a binary operator in Ergo, a language we're building using QCert.

(cc @jeromesimeon)

jeromesimeon commented 6 years ago

That bug's traced back to https://github.com/querycert/qcert/commit/970b735f126e887d35107689653c8923fa5846e8#diff-82edd685eaa31ee967ad91b372aa89d3

jeromesimeon commented 6 years ago

Also tested in Ergo now, closing the issue.