Programatica Tools

Directory tools/hs2alfa

What is in this directory (hs2alfa)

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 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).

• 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 ...

• 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 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.)