search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Bugs while translating guards and pattern matchings #46

Closed lastland closed 6 years ago

lastland commented 6 years ago

I have created a minimal example that can reproduce this bug under examples/guard.

The Haskell file contains the following three functions:

f :: Int -> Int
f x | x == 1    = 1
    | otherwise = 2

g :: Int -> Int
g 1 = 1
g _ = 2

h :: Int -> Int
h x = if x == 1 then 1 else 2

hs-to-coq fails to translate f.

It can translate g but the translated Coq file cannot be compiled (because the translated code uses ==, which is a notation must be imported from GHC.Base).

It can successfully translate h.

lastland commented 6 years ago

Change f to:

f :: Int -> Int
f x | True    = 1
    | otherwise = 2

and hs-to-coq still fails to translate f.

lastland commented 6 years ago

But hs-to-coq can successfully translate the following f:

f :: Int -> Int
f x | x == 1 = 1
f _ = 2
sweirich commented 6 years ago

Code for translating pattern matches with guards is here https://github.com/antalsz/hs-to-coq/blob/master/src/lib/HsToCoq/ConvertHaskell/Expr.hs