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