CristalCaveGem » LustreC

setup tests for dune

rewrite a bit the menhir parser

better location error

- tag_true and tag_false moved to lustre_types
- real constants are hidden in Real.ml{i} module

Produce true/false statements as constants

Cocospec: parsing, normalizing and processing machines for contracts.

Some progress on compiling cocospec contract.
Contract resolution still need to be done as well as dealing with the machine code level and so on.

Moved lusic to .h printer after normalizing in case we want one day to produce ACSL from a normalized spec
Trying also to extend the parser to deal with imported nodes....

Unified compilation of lusi and lus files
Different parsers yet but shared process.
In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code...

Added include directive that directly inject a lustre source file in the prog

- Module.load_header and load_program were merged.
- Contract were extended with list of statements.

- Global type env and clock env now availble as a global reference (Global module)
- Adapted the parsing of specification with a cocospec compatible one
- The data structure of contracts is now almost cocospec compatible
- Lustrec-test has been updated to use the newest syntax

Some refactoring
Adapted the parser/types/constructors for cocospec syntax