compatibility with ghc(i)

[jwaldmann]

(design question)

I think it would be nice if theory files were valid Haskell modules, so they can be used with ghc(i),
so that the student can interactively develop the program, type-check it, and evaluate expressions.

This applies to data declarations and value (function) declarations. Of course I don't want full Haskell - just that GHC understands CYP syntax and agrees on the semantics.
(This would also make testing any CYP extensions (type system) much easier.)

Then we have CYP axioms and goals, which currently are not-Haskell. We could

• hide them from GHC (inside comments)
• have them type-checked by GHC
• have them executed by some test framework

E.g., goal filter p . filter p .=. filter p could be written as
goal_1 p xs = (filter p . filter p) xs == (filter p) xs
so we can evaluate Test.LeanCheck.check goal_1.

This has two technical problems:

• for actual tests, we need to instantiate polymorphic types (but for proofs, we don't want this)
• we need to add the extra argument since we don't have == on functions (in Leancheck)