Project

General

Profile

« Previous | Next » 

Revision c02d255e

Added by Pierre-Loïc Garoche almost 9 years ago

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

View differences:

src/parserLustreSpec.mly
102 102 
    {mkeexpr (EExpr_arrow ($1,$3))}
103 103 
| expr FBY expr
104 104 
    {mkeexpr (EExpr_fby ($1,$3))}
105 
| expr COLCOL expr
106 
    {mkeexpr (EExpr_concat ($1,$3))}
107 
| TAIL LPAR expr RPAR
108 
    {mkeexpr (EExpr_tail $3)}
109 105 
| expr WHEN IDENT
110 106 
    {mkeexpr (EExpr_when ($1,$3))}
111 
| expr WHENNOT IDENT
112 
    {mkeexpr (EExpr_whennot ($1,$3))}
113 107 
| MERGE LPAR IDENT COMMA expr COMMA expr RPAR
114 108 
    {mkeexpr (EExpr_merge ($3,$5,$7))}
115 109 
| IDENT LPAR expr RPAR

Also available in: Unified diff