Programatica Tools

Directory tools/hs2alfa

The README file is displayed below the directory index.

Name	Last modified	Size
Parent Directory		-
tstProp2Alfa.hs	2002-05-25 20:27	1.0K
tstHs2Alfa.hs	2002-05-25 20:27	1.0K
tst1propb.alfa	2001-09-11 07:39	802
tst1prop.alfa	2001-09-11 07:39	276
tst1.hs	2001-09-11 07:39	386
tst0f.hs	2001-11-14 20:50	177
tst0.hs	2001-11-13 09:43	1.3K
tests/	2005-10-11 01:09	-
apfe.hs	2004-01-24 01:15	213
USCC.hs	2003-01-09 01:17	397
Prop2Alfa.hs	2005-05-11 22:52	9.1K
Prop.alfa	2001-09-08 09:58	507
Prelude.alfa	2001-11-13 20:48	636
PfeAlfaCmds.hs	2005-10-11 01:09	3.5K
Makefile	2005-02-02 00:38	1.2K
HuMakefile	2005-03-22 23:08	650
Hs2Alfa.hs	2002-11-19 00:17	788
Flags.ghc	2002-10-20 09:12	272
BaseStruct2Alfa.hs	2005-07-21 00:02	32K
AlfaSource/	2004-01-23 23:23	-

What is in this directory (hs2alfa)

This directory contains the translator from Haskell to Alfa, which is built on top of the PFE framework and parts of Alfa.

By running make you can create apfe, a command line tool that has all the functionality of the PFE framework, plus the ability to translate Haskell files to Alfa files.

There are also two (obsolete) test programs that don't depend on the PFE framework: tstHs2Alfa (for the base language, Haskell 98) and tstProp2Alfa (for Hasell 98 + property declarations). They can be compiled with make progamname.

The code compiles with GHC, provided that the directory AlfaSource, containing certain modules from Alfa, is present (get alfaforpfe.tar.gz and unpack it in this directory).

Limitations

The translator is work in progress (as everything else here). It does handle

the most common forms of declarations and expressions,
polymorphism,
classes and overloading (by the dictionary translation, which is performed mostly by the Haskell type checker in ../base/TI/),
data types and (some forms of) pattern matching,
the list comprehension syntax,
mutually recursive modules (by combining them into one module, name clashes can cause problems).

The translator does not yet (fully) support

pattern matching with guards,
literals in patterns,
data constructors with labelled fields,
names that are reserved in Alfa but not in Haskell (but sig, . and Type are translated).
certain constructions that the Agda type checker rejects, e.g. case let ... in ... of ...

Other problems:

Type signatures containing synonyms for function types (like ReadS) can cause problems. (Workaround: comment out the type signature or manually expand the type synonym.)

Name capture can occur, for example, in the translation of


    class Functor f where fmap :: (a->b)->f a->f b
    instance Ix a => Ix (Array a) where fmap = ...

there will be a problem with capture of the type variable a.

The translator can translate P-logic predicate definitions and property assertions, but

the fixed point operators Lfp and Gfp are translated, but their meaning in Alfa is probably not what it should be.
the use of constructors lifted to predicates is not yet supported,
the P-logic equality operator (===) is translated to intentional equality, which differs for functions.
the comprehension syntax is restricted.

The subdirectory tests contains sample Haskell modules that the translator can translate. (There are also some test files in this directory.)

Author: Thomas Hallgren

Contact: TH