eva2h1

Translator to compile protocol spcifications in EVA concrete syntax
into set of horn clauses in various formats.

+ Unpack:

 untar the package file EVA2H1+EVAlib.tar.gz in a directory 
 of your choice that we shall call SRC below
 (you certainly already have done this if you read this file).
 It produces 2 subdirectories of SRC:
  - EVAlib which contains the source and doc of the EVAtrans library,
    necessary to compile eva2h1
  - EVA2H1 which contains the sources of eva2h1


+ Compilation: 
 It requires Ocaml 3.06 (ocamlc, ocamllex, ocamlyacc), gnu make

 compile the EVAtrans library, it produces cmi files and evatrans.cma
 in the directory SRC type:
 % make -C EVAlib lib

 compile the interpreted executable eva2h1
 it is left in SRC/EVA2H1 and requires ocamlrun to run,
 in the directory SRC/EVA2H1 type:
 % make  

 [optional] compile the native executable eva2h1.opt
            it is left in SRC/EVA2H1
 in SRC/EVA2H1 type:
 % make execopt

 To produces doc files (EVA language syntax and semantics etc), 
 see SRC/EVAlib/README

+ Other optional Makefile targets 
 (type commands in SRC/EVA2H1 )

 build html documentation of sources
 requires ocamldoc
 % make html

 prepares the tar archive eva_pack.tar
 % make tar

 rebuilt dependencies
 requires ocamldep
 % make dep  

 build a tag file TAGS from sources for emacs
 requires etags
 % make tags 

 % make clean 


+ Command:

 eva2h1 [options] file.eva

 with options:
 -eva :    LAEVA output format
 -horn :   Horn clauses output format
 -tptp :   Horn clauses in TPTP output format (default)
 -prolog : Horn clauses in Prolog output format
 -debug :  debugging output format
 -trace :  output debug info
 -help :   resume command and options

+ Files:

 see SRC/EVAlib/README for a description of the files of the EVAtrans library

 SRC/EVA2H1/eva2h1.ml   
  sources main, interpretation of command line

 SRC/EVA2H1/clause.mli 
 SRC/EVA2H1/clause.ml
  type of clauses and functions of translation of
  a spec in EVA abstract syntax into a set of clauses.

 SRC/EVA2H1/hornpp.mli
 SRC/EVA2H1/hornpp.ml 
  pretty printing of list of Horn clauses in folkloric syntac

 SRC/EVA2H1/TPTP.mli
 SRC/EVA2H1/TPTP.ml 
  pretty printing of list of Horn clauses in the syntac
  of the TPTP library (syntax for H1), see http://www.tptp.org

 SRC/EVA2H1/prologpp.mli
 SRC/EVA2H1/prologpp.ml 
  pretty printing of list of Horn clauses in Prolog syntac

 SRC/EVA2H1/README
  this file

 SRC/EVA2H1/Makefile    

 SRC/EVA2H1/.depend 
  dependencies for Makefile  
        
 SRC/EVA2H1/test/
  test files in EVA concrete syntax, for debug purpose