Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 7291cb80

# Date Author Comment
7291cb80 02/28/2014 04:56 PM Xavier Thirioux

- 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

0777a7be 02/28/2014 03:28 PM Pierre-Loïc Garoche

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

c6f61bd7 02/28/2014 02:05 PM Pierre-Loïc Garoche

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

c11dbf10 02/28/2014 02:04 PM Pierre-Loïc Garoche

desome

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@167 041b043f-8d7c-46b2-b46e-ef0dd855326e

867595f2 02/28/2014 01:52 PM Pierre-Loïc Garoche

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

b09a175c 02/28/2014 01:43 PM Pierre-Loïc Garoche

inliner function

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@165 041b043f-8d7c-46b2-b46e-ef0dd855326e

c653e640 02/28/2014 10:39 AM Pierre-Loïc Garoche

Minor bugs

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@164 041b043f-8d7c-46b2-b46e-ef0dd855326e

64dfa450 02/28/2014 10:35 AM Eric Noulard

Do not use stable sort because it requires recent ocamlgraph
library (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

e2380d4d 02/28/2014 10:33 AM Pierre-Loïc Garoche

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test 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

1577dc7e 02/26/2014 03:37 PM Xavier Thirioux

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

11242500 02/26/2014 02:37 PM Xavier Thirioux

again, debugged tuple subtyping

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@160 041b043f-8d7c-46b2-b46e-ef0dd855326e

17249d2e 02/26/2014 02:04 PM Xavier Thirioux

removed debug printing

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@159 041b043f-8d7c-46b2-b46e-ef0dd855326e

9b5969d4 02/26/2014 02:02 PM Xavier Thirioux

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

4a840259 02/26/2014 01:42 PM Xavier Thirioux

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

71513f0e 02/26/2014 07:48 AM Pierre-Loïc Garoche

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

4be0d54a 02/24/2014 04:26 PM Pierre-Loïc Garoche

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

cd6efd9b 02/24/2014 11:47 AM Pierre-Loïc Garoche

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

9cab57c9 02/24/2014 11:25 AM Pierre-Loïc Garoche

...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@151 041b043f-8d7c-46b2-b46e-ef0dd855326e

2f44a4cc 02/24/2014 10:50 AM Pierre-Loïc Garoche

Is it working?

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@150 041b043f-8d7c-46b2-b46e-ef0dd855326e

c76f1d66 02/24/2014 09:46 AM Pierre-Loïc Garoche

Working on bugs

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@149 041b043f-8d7c-46b2-b46e-ef0dd855326e

f19eb2fd 02/21/2014 05:11 PM Pierre-Loïc Garoche

Second (almost) working version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@147 041b043f-8d7c-46b2-b46e-ef0dd855326e

20e9de2d 02/21/2014 04:39 PM Pierre-Loïc Garoche

First (almost) working version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@146 041b043f-8d7c-46b2-b46e-ef0dd855326e

96babff4 02/21/2014 12:42 PM Pierre-Loïc Garoche

Ongoing ...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@145 041b043f-8d7c-46b2-b46e-ef0dd855326e

8605c4a4 02/21/2014 12:38 PM Pierre-Loïc Garoche

Ongoing ...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@144 041b043f-8d7c-46b2-b46e-ef0dd855326e

7a19992d 02/21/2014 08:37 AM Pierre-Loïc Garoche

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

dcbf9d3a 02/20/2014 06:45 AM Pierre-Loïc Garoche

The missing file

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@142 041b043f-8d7c-46b2-b46e-ef0dd855326e

3ee1012f 02/19/2014 05:02 PM Pierre-Loïc Garoche

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

17d2db94 11/14/2013 12:15 PM Pierre-Loïc Garoche

- 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

7a47b44f 11/12/2013 11:20 PM Xavier Thirioux

- work in progress for interface typing

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@129 041b043f-8d7c-46b2-b46e-ef0dd855326e

b3381ae8 11/07/2013 07:03 PM Xavier Thirioux

- 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

5c1184ad 10/22/2013 10:39 AM Pierre-Loïc Garoche

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

22fe1c93 10/02/2013 08:13 AM Pierre-Loïc Garoche

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