Using deriving_ppx to derive show_ functions for the main types defined in lib/Applying the same procedure of operator specialization taken from the C backend to TinyLustrev has now a functional Tiny plugin :
* -unrolling option has been renamed -duration because from an outside observer it is the length in steps of the abstract simulation...
Transition to dune build systemImprovement of opam integrationDockerfile based on AlpineDockerfile based on UbuntuUpdate the README.md
- Primitive Tiny backend- Renamed Mpfr to lustrec_mpfr- Introduced dependency in Zarith. Trying to move away from Num
[bug cavale 93] solved: issue when resetting a stateless node. Now generating a warning and forcing the stateful status. Could be improved to remove the reset statement. (TODO)
printing nodes + more progress on seal export
- Refactored Error exception and messages- Bugs in partial evaluation for equalities among bool constants and a nice recursive call generating a stack overflow! Now solved- Setup a timeout for z3 in seal- Better log for seal
Reactivated Unfold constant
Output folder for seal-extract
comestic changes, removing useless logs
Cocospec: parsing, normalizing and processing machines for contracts.
Merge branch 'lustrec-seal' into ada
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.
Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into ada
Ada: Add support for arrows as an independent generic package, instantiated in each package using it. It required a lot of refactoring.
Ada: Changed type name for states and normalized variable name to match ada requirements.
Ada: skeletons for Ada compiler
Some progress on EMF bqckend. Refactoring machines code
Cleaning up stuff in normalization. Mainly replace arguments with only required elementsnode_Table hashtbl is now only available through functions of the corelang.mli
Moved lusic to .h printer after normalizing in case we want one day to produce ACSL from a normalized specTrying also to extend the parser to deal with imported nodes....
Unified compilation of lusi and lus filesDifferent 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...
- Dep type with a tuple has been replaced by a record type- Modules now is more integrated and performed the building of the type/clock env. previously some computation were performed twice by different functions. Some of these functions have been moved from compiler_common to modules
- Module.load_header and load_program were merged.- Contract were extended with list of statements.
Merge branch 'unstable' into lustrec-seal
- 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
Tuning the pretty printing of Salsa plugin
Further restructuring:- arrow.ml* to define basic builder for arrow (node, name, ...)- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)- machine_code restricted to the translatation from normalized nodes to machines
- Makefile: solved dependency problem when compiling include lusi- Renamed type declarations as lustre_types and machine_code_types
- Normalization parameters (alias and unfold_array) are now provided as parameter- program type renamed as program_t- Initiating the lustrev tool with dependencies to z3 and seal.
Conditional activation of machine type plugin. currently a little buggy. Shall be desactivated.
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8) typing was transformed as a functor and parametrized by basic types (int/real/bool) it can also be applied multiple times on the same program
[main] node locals are now sorted according to their dependencies wrt clocks. The produced lustre node with types shall now be compilable
Moved stage1 in separate file: it is shared among binaries