Re: [isabelle] Code generator "eq" instances

Hi John,

> I'm trying to understand how to safely generate Haskell code from HOL,
> where I want the Haskell code to be an instance of the Eq class, but
> with my own definition of the (==) method. I want Isabelle to enforce
> that my definition of (==) is sound, i.e. it implements logical equality.

the system is setup in a way that instantiation of the eq class happens
in exectly that manner automatically on each datatype statements (c.f.
§2.6 of the code generation tutorial):

> So I'm trying to make my datatype an instance of the eq class, but I'm
> running into an error when using the function package to make the
> corresponding definition. Here's an example theory file:
> theory Silly
> imports Main
> begin
> datatype silly = Silly int

Try here,  e.g.

export_code "HOL.eq :: silly => _" in Haskell file -

> instantiation silly :: eq
> begin
> fun "eq_class.eq" where
>   "eq (Silly n) (Silly m) = (m - n = 0)"
> instance ..
> end

The conventions how to write down specifications in an instantiation
block are a little bit unconventional (c.f. class tutorial):

* In a binding (the name with optional type after fun, definition,
primrec, ...), you must write "f_typeconstructor" instead of "f" (in
your case, eq_silly -- the names can be inspected using the "show me
context" button in PG).

* In the specification terms, you may simply use "f" and have to make
sure that typing will it make refer to the particular type instance.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.