Re: [isabelle] haskabelle import and config

Hi Rick,

thanks for trying Haskabelle.

> me> /usr/local/Haskabelle/bin/haskabelle tree.hs out
> haskabelle_bin: user error (The module "System.IO" imported from module
> "Tree" cannot be found at "System/IO.hs"!)

> 1. Does this mean that I am required to include System.IO in that list
> as well?

Basically, you have the choice between two solutions:

1. Include source code file of System.IO into your current working
directory structure.

2. Extend the default adaptation in order that all necessary ingredients
of System.IO have appropriate counterparts in existing Isabelle/HOL/Main
theories, including Haskabelle's theory Prelude.thy which can also be
extended as needed.

Solution (1) is often not feasible since standard library source text
contains a lot of technical stuff which cannot be processed by
Haskabelle, requiring a heavy editing of the file.  Solution (2)
requires more dilligence but work quite well in practice.

Anyway the most fundamental question is which functionality your module
using System.IO actually needs.  IO operations cannot be imported
directly because they require some non-functional primitives for which
Isabelle/HOL has no direct counterparts.  In order to really reason
about such programs, you would have to provide an appropriate IO model
within Isabelle/HOL, which is not trivial.  In your case, I would guess
that the dependence on System.IO is just due to some pretty printing
function or something like that;  in such a case you should consider
commenting this out since I assume you hardly want to reason about
pretty printing functions etc.

> 2. Could you provide a pointer to documentation on the config file?

There is no separate documentation; the purpose is to give a mapping of
existing Haskell identifiers (classes, types, function symbols --
constants in Isabelle parlance) to existing Isabelle identifiers such
that these get replaced on translation.  To illustrate this, a quote
from default/adapt.txt:

	  "Prelude.Bool"        "bool"

	  "Prelude.True"        "True"
	  "Prelude.False"       "False"

This instructs Haskabelle to replace the Haskabelle built-in type Bool
("Prelude.Bool") and its constructors "Prelude.True" and "Prelude.False"
with Isabelle's "bool" and constants "True" and "False".

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.