-------------------------------------------------------------------------------

vdm-front -- ISO VDM-SL Parser


This package contains a parser for VDM-SL based on the grammar defined in the
ISO document 13817-1.


Here it can be found information for the following topics:
   GENERAL          - Overview of the folder structure and what can be found
                      in each one.
   NOTES            - Notes about the VDM-SL Grammar.
   VERSION NUMBERS  - Explanaition about the version numbers of this package.
   PREREQUISITES    - Software prerequisites to check the grammar and to build
                      the front-ends
   INSTALLATION     - Notes about what you should do to check the project.
   HASKELL FRONTEND - Explanation of the Haskell front-end and its use.

   
--- GENERAL -------------------------------------------------------------------

Contents of this package:

   - syn      Directory with the grammar
   - test     Directory with the parse-unit testsuite
   - doc      Directory with the documentation (haddock html docs and notes)
   - scripts  Directory with reusable make rules

   - haskell  Directory with the Haskell front end for VDM-SL
   - contrib  Directory containing all necessary import files   
   
--- NOTES ---------------------------------------------------------------------

This grammar was produced by hand coding the grammar specified in the ISO/IEC
13817-1 document in paper.

Errors can be found and should be reported to the authors for correction.
Some of the features of the ISO were not implemented, for more information see
doc/notes.txt file. The same file contains the syntactical differences between 
the ISO VDM-SL and IFAD VDM-SL (a must read when getting parse errors)


--- VERSION NUMBERS -----------------------------------------------------------

Although the grammar specified in the ISO/IEC can be used to parse (because
sglr does not restrict the class of grammars it can use), this grammar is
extremely ambiguous and disambiguation rules can only be add if changing the
grammar. Thus, the grammar will be improved incrementing in each release the
version number.

Version 0.0.1 contains the original grammar, typed by hand from the original ISO
document. This grammar can be used for parsing although when many ambiguities
are found, sglr will fail to parse.

Version 0.0.2 contains an improved grammar, that succeeds parsing the testsuite.
All the detected ambiguities were removed both by adding disambiguation filters
and corrections to the grammar. These corrections tried to change the minimum
possible to allow parsing.

Version 0.0.3 contains a grammar with constructs for creating AST. Some
injenctions were removed.

Version 1.0 adds an Haskell front-end for the parser, called VDMhparser. This
front-end can be used as starting point for any project in Haskell that needs
a parser for VDM-SL (metric generators, program analyzers, program generators,
program transformation tools, etc.).

Version 1.1 introduces a few grammar changes to workaround known implodePT
bugs, and adds a new haskell analysis library that allows calculation of
function and type dependencies. Also, the whole library was updated to work
with GHC 6.4.1.

For more information about changes see ChangeLog and doc/notes.txt files.


--- PREREQUISITES -------------------------------------------------------------

Mandatory requisites:
   - ghc (version 6.4.1)
        http://www.haskell.org/ghc

   - sdf2bundle (version 2.0.1) - sdf2table, sglr, implodePT
        http://www.program-transformation.org/Sdf/SdfBundle (source)
        https://sourceforge.net/projects/voodoom (binary)
   notes: versions of sdf2table after 1.13 may not work because the SDF grammar
          was changed. For using most recent versions of sdf2table one must add
          "context-free start-symbols Document" in the "Document" module of the
          SDF specification (this was not tested).


Optional requisites:
   Software for necessary for checking the grammar against the available tests
   - strategoxt  (version 0.12)  - parse-unit
        http://www.program-transformation.org/Stratego/StrategoRelease012


Others:
   The package uses the following Haskell libraries:
   - Sdf2Haskell (version 2.2)
   - ATermLib    (version 1.4)
   - DrIFT       (version 2.0.4)
   - PURe Libs   (PURe Universty of Minho Haskell Libraries)

   notes: It is NOT necessary to install these libraries since they are already
          available in the contrib folder of the release version.


--- INSTALLATION --------------------------------------------------------------

This project don't have an installation process using the configure scripts.

All the configurations must be done by editing a single configuration file
(./scripts/makerules.configuration).
If all the programs from the prerequisites are in the system path, then no
change is required.

If you have to provide the complete path for all necessary then you must to
edit the configuration file.

Ain't it easy? :-)


--- HASKELL FRONTEND ----------------------------------------------------------

The purpose of the Haskell front-end is to define a starting point for
developing all sort of programs that require a VDM-SL parser, for instance
program analyzers, program transformation, program generators, etc. 

The Haskell front-end, called VDMhparser,  contains a parser for VDM-SL and 
allows to print both the AST and the Pretty printed version of the source file.

The program options are:

VDMhparser
  -h       --help                      Show usage info
  -i FILE  --input=FILE                Input file (mandatory)
  -o FILE  --output=FILE               Output file (default: stdout)
  -a       --ast                       Print Abstract Syntax Tree
  -p       --pretty-printer            Print using the pretty printer (default)
  -t       --type-dependency-analysis  Create the data-type dependency graph in dot format

After compiling VDMhparser its possible to test using the source files
from the test/generics folder.


For printing the AST of the BAMS example you must do (from the haskell folder):
   ./VDMhparser -i ../test/generics/BAMS.vdm -a


IMPORTANT NOTES:

 a) The folder from which you run the VDMhparser is important. The parser
    requires the parsing table for the VDM-SL grammar (isovdm.def.tbl). The
    location of this file is defined staticaly using relative directories and
    for this reason if you run the executable from other directory you will
    get an error saying: "could not open language!".
    This is not a very good solution and must be improved in some point.
 b) Cygwin users may experience errors when running tests. The problem arises
    when parser temporary files are created in the /tmp folder. For some odd
    reason ghc sets /tmp to the c:\tmp folder and completely ignores all the
    environment variables TMP, TMPDIR and TEMP. To solve this, a possible hack
    is to create the c:\tmp folder and then in the cygwin replace the /tmp
    folder by a link to c:\tmp. This can be done in a cygwin bash shell with 
    the following commands:
       mkdir /cygdrive/c/tmp
       rmdir /tmp (make sure that does not exist any file)
       ln /cygdrive/c/tmp /tmp -s
    
    In a few forums it is said that if ghc is installed in a different drive
    you must use the temporary folder of the same drive (this was not tested).
    

-------------------------------------------------------------------------------