Email Gateway (Aug 18 2022 at 14:28): Email Gateway (Aug 18 2022 at 14:28):From: Rick Murphy <rick@rickmurphy.org>
All:
I am further testing Haskabelle and observing results such as the following:
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"!)
The Haskabelle documentation calls for a list of Haskell source files.
Does this mean that I am required to include System.IO in that list
as well?
Could you provide a pointer to documentation on the config file?
Email Gateway (Aug 18 2022 at 14:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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"!)
- Does this mean that I am required to include System.IO in that list
as well?
Basically, you have the choice between two solutions:
Include source code file of System.IO into your current working
directory structure.
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.
- 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:
types
"Prelude.Bool" "bool"
consts
"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
Florian
signature.asc
Last updated: Apr 19 2024 at 01:05 UTC