Added declaration/definition of stateless/stateful nodes. The 'function' keyword is for stateless nodes only, the 'node' keyword is any kind of node. Improves compilation and paves the way for more optimizations.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@202 041b043f-8d7c-46b2-b46e-ef0dd855326e
- work in progress for stateless/stateful status computation (to turn conditionals into merges, which yield more efficient C code)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@198 041b043f-8d7c-46b2-b46e-ef0dd855326e
corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@194 041b043f-8d7c-46b2-b46e-ef0dd855326e
- added struct types declaration - added constant definition with a struct type - added checking for multiple definitions of nodes (behavior was buggy) - better and more uniform error messages for undefined/already defined symbols
We still need struct expressions......
work in progress for struct types...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@184 041b043f-8d7c-46b2-b46e-ef0dd855326e
more steps towards struct types...Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/src/corelang.mliM trunk/src/type_predef.mlM trunk/src/main_lustre_compiler.mlM trunk/src/types.mlM trunk/src/printers.mlM trunk/src/typing.ml...
first steps towards struct types...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@182 041b043f-8d7c-46b2-b46e-ef0dd855326e
corrected bug in arrow macros names, added storage attribute for static alloc macros, option -d now creates the destination directory if needed, with current dir as file permissions
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@181 041b043f-8d7c-46b2-b46e-ef0dd855326e
answer to #feature 50: - arrows are now factorized out and become part of include as files arrow.h and arrow.c - no more arrows in generated code - compiling and linking arrow.c is only necessary in case of dynamic allocation - version now includes installation prefix (for the standard lib)...
In order to export any type of constants, moved type definitions from .c to .h
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@179 041b043f-8d7c-46b2-b46e-ef0dd855326e
Generate extern declarations for constant as well.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@178 041b043f-8d7c-46b2-b46e-ef0dd855326e
- added generation of clock information in interface (.lusi) files- added clock checking between interface and implementation files
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@176 041b043f-8d7c-46b2-b46e-ef0dd855326e
Reenabled the generation of witnesses for inline process.Systematic use of the build path
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@175 041b043f-8d7c-46b2-b46e-ef0dd855326e
- merged test script - added -d support - corrected #open parser problem - corrected interface/implementation (.lusi/.lus) checking for types (not yet for clocks)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge back horn backend branch in trunk
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@169 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge trunk modif in branch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@168 041b043f-8d7c-46b2-b46e-ef0dd855326e
desome
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@167 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge inlining branch within trunk.The test target requires branch lustrec/horn as binary lustreh.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@166 041b043f-8d7c-46b2-b46e-ef0dd855326e
inliner function
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@165 041b043f-8d7c-46b2-b46e-ef0dd855326e
Minor bugs
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@164 041b043f-8d7c-46b2-b46e-ef0dd855326e
Do not use stable sort because it requires recent ocamlgraphlibrary (1.8.3) which is not widely available in distro repository.Moreover "stable" sort is not necessary, sort will do.Fixes Issue #49: https://cavale.enseeiht.fr/redmine/issues/49
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@163 041b043f-8d7c-46b2-b46e-ef0dd855326e
Solved some bugs in the lustre printerGeneration of a witness with both the main node and hte inlined main nodeTest script modified to check consistency of the inlining process
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@162 041b043f-8d7c-46b2-b46e-ef0dd855326e
better error message for tuple type mismatch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@161 041b043f-8d7c-46b2-b46e-ef0dd855326e
again, debugged tuple subtyping
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@160 041b043f-8d7c-46b2-b46e-ef0dd855326e
removed debug printing
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@159 041b043f-8d7c-46b2-b46e-ef0dd855326e
corrected wrong subtyping rule for tuple assignment
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@158 041b043f-8d7c-46b2-b46e-ef0dd855326e
added subtyping in equations (rhs may be a subtype of lhs)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@157 041b043f-8d7c-46b2-b46e-ef0dd855326e
Improvements as suggested by e. Noulard: better install of include; modified generated makefile
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@156 041b043f-8d7c-46b2-b46e-ef0dd855326e
Fixed bug on the main part
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@154 041b043f-8d7c-46b2-b46e-ef0dd855326e
First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@152 041b043f-8d7c-46b2-b46e-ef0dd855326e
...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@151 041b043f-8d7c-46b2-b46e-ef0dd855326e
Is it working?
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@150 041b043f-8d7c-46b2-b46e-ef0dd855326e
Working on bugs
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@149 041b043f-8d7c-46b2-b46e-ef0dd855326e
Second (almost) working version
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@147 041b043f-8d7c-46b2-b46e-ef0dd855326e
First (almost) working version
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@146 041b043f-8d7c-46b2-b46e-ef0dd855326e
Ongoing ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@145 041b043f-8d7c-46b2-b46e-ef0dd855326e
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@144 041b043f-8d7c-46b2-b46e-ef0dd855326e
In the middle of the coding process. Just pushing thinks
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@143 041b043f-8d7c-46b2-b46e-ef0dd855326e
The missing file
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@142 041b043f-8d7c-46b2-b46e-ef0dd855326e
Initial copy of the horn output version. Not really working yet
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@141 041b043f-8d7c-46b2-b46e-ef0dd855326e
- Renamed the only target of the generated makefile- Solved bug: xor are now printed as bitwise xor in c : a ^ b and not a xor b.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@131 041b043f-8d7c-46b2-b46e-ef0dd855326e
- work in progress for interface typing
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@129 041b043f-8d7c-46b2-b46e-ef0dd855326e
- small bug correction in dimension typing - #open keyword instead of open - dummy generic matrix/vector library interface added - modified examples according to the new syntax
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@126 041b043f-8d7c-46b2-b46e-ef0dd855326e
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@123 041b043f-8d7c-46b2-b46e-ef0dd855326e
Moved files to trunk in lustre_compiler
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@116 041b043f-8d7c-46b2-b46e-ef0dd855326e