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

Cannot find class information for Foldable/Traversable/Monoid #26

Closed sweirich closed 6 years ago

sweirich commented 7 years ago

When I translate ghc/compiler/Util/Pair.v (in examples/ghc)

I get these messages:

(* Translating `instance Data.Foldable.Foldable Pair' failed: OOPS! Cannot find
   information for class "Data.Foldable.Foldable" unsupported *)

(* Translating `instance Data.Traversable.Traversable Pair' failed: OOPS! Cannot
  find information for class "Data.Traversable.Traversable" unsupported *)

(* Translating `instance forall {a}, forall `{GHC.Base.Monoid a},
  GHC.Base.Monoid (Pair a)' failed: OOPS! Cannot find information for class
 "GHC.Base.Monoid" unsupported *)

Do we need to do something special to tell hs-to-coq where to find these classes?

antalsz commented 7 years ago

We need to add support for this in hs-to-coq as part of #23.

nomeata commented 7 years ago

Temporarily we can do what we do for Make etc.: Hardcode them in the code.

sweirich commented 7 years ago

Where is this hardcoded? This is not urgent (yet).

nomeata commented 7 years ago

https://github.com/antalsz/hs-to-coq/blob/master/hs-to-coq/src/lib/HsToCoq/ConvertHaskell/Monad.hs#L109

(There are partial bits about Monoid and Foldable there from earlier experiments, but they lack some methods, and the name should be fully qualified.)

sweirich commented 7 years ago

Thanks. We can wait for #23 now, but if it is blocking, I'll know what to do.

nomeata commented 6 years ago

Closing this in favor of #23