Nicolas Magaud (Sep 27 2022 at 20:12): Nicolas Magaud (Sep 27 2022 at 20:12):I try and use hs-to-coq to translate this simple piece of Haskell
module Main (main) where
import GHC.Base
data ClosedAbove = V | B ClosedAbove ClosedAbove deriving(Eq,Show,Read)
data UniquelyClosable = L ClosedAbove
| A UniquelyClosable UniquelyClosable deriving(Eq,Show,Read)
genA 0 = []
genA n | n>0 = [ L x | x <- genB (n-1)] ++ [A x y | k<-[0..n-2], x<-genA k, y<-genA (n-2-k) ]
genB 0 = [V]
genB n | n>0 = [ B a b | k <- [0..n-2], a <- genB k, b <- genB (n-2-k) ]
main = print (genA 4)
However when running
stack exec hs-to-coq -- -o output-directory/ example.hs
I get the following error message :
<command line>: Package environment "-" (specified in GHC_ENVIRONMENT) not found
Any advice ?
Nicolas Magaud (Dec 01 2022 at 14:56):$ stack exec hs-to-coq -- -o output-directory/ ex.hs
When looking up information about GHC.Classes.Eq in classDefns
Could not find GHC/Classes.h2ci in any of these directories:
Please either process GHC.Classes first, or
skip declarations that mention GHC.Classes.
Could not find information for the class `GHC.Classes.Eq' when defining the instance `Main.Eq__MyNat'
When running hs-to-coq, I get this error message and I do not know how to make hs-to-coq aware of the location of GHC/Classes.h2ci.
I use the simpliest example I could invent :
module Main (main) where
import GHC.Base
data MyNat = MyZero | MySucc MyNat deriving(Eq,Show,Read)
main = print (MySucc (MySucc MyZero))
Hi! Take a look at the Makefiles in each of the examples subdirectories, such as https://github.com/plclub/hs-to-coq/blob/master/examples/simple/Makefile. Often you'll need to tell hs-to-coq where to find information about the base libraries.
Last updated: Feb 06 2023 at 05:03 UTC