Project

General

Profile

« Previous | Next » 

Revision 3dfb5cd8

Added by Lélio Brun over 2 years ago

rewrite a bit the menhir parser

View differences:

src/parsers/parser_lustre.mly
14 14 
open Lustre_types
15 15 
open Corelang
16 16 
open Dimension
17 
open Parse
18 17 

  		




  19
  18
  
    
   


  		




  20
  19
  
    
let get_loc () = Location.symbol_rloc ()


  		




  21
  20
  
    

  		




  22
  21
  
    
let mkident x = x, get_loc ()


  		




  23
  
  
    
let mktyp x = mktyp (get_loc ()) x


  		




  24
  
  
    
let mkclock x = mkclock (get_loc ()) x


  		




  
  22
  
    
let mktyp = mktyp (get_loc ())


  		




  
  23
  
    
let mkotyp x = match x with Some t -> Some (mktyp t) | None -> None


  		




  
  24
  
    
let mkclock = mkclock (get_loc ())


  		




  25
  25
  
    
let mkvar_decl x loc = mkvar_decl loc ~orig:true x


  		




  26
  
  
    
let mkexpr x = mkexpr (get_loc ()) x


  		




  27
  
  
    
let mkeexpr x = mkeexpr (get_loc ()) x 


  		




  28
  
  
    
let mkeq x = mkeq (get_loc ()) x


  		




  29
  
  
    
let mkassert x = mkassert (get_loc ()) x


  		




  30
  
  
    
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x


  		




  31
  
  
    
let mkpredef_call x = mkpredef_call (get_loc ()) x


  		




  32
  
  
    
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)


  		




  33
  
  
    

  		




  34
  
  
    
let mkdim_int i = mkdim_int (get_loc ()) i


  		




  35
  
  
    
let mkdim_bool b = mkdim_bool (get_loc ()) b


  		




  36
  
  
    
let mkdim_ident id = mkdim_ident (get_loc ()) id


  		




  37
  
  
    
let mkdim_appl f args = mkdim_appl (get_loc ()) f args


  		




  38
  
  
    
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e


  		




  39
  
  
    

  		




  40
  
  
    
let mkannots annots = { annots = annots; annot_loc = get_loc () }


  		




  
  26
  
    
let mkexpr = mkexpr (get_loc ())


  		




  
  27
  
    
let mkeexpr = mkeexpr (get_loc ())


  		




  
  28
  
    
let mkeq = mkeq (get_loc ())


  		




  
  29
  
    
let mkassert = mkassert (get_loc ())


  		




  
  30
  
    
let mktop_decl = mktop_decl (get_loc ()) (Location.get_module ())


  		




  
  31
  
    
let mkpredef_call = mkpredef_call (get_loc ())


  		




  
  32
  
    
let mkpredef_call_b f x1 x2 = mkpredef_call f [x1; x2]


  		




  
  33
  
    
let mkpredef_call_u f x = mkpredef_call f [x]


  		




  
  34
  
    

  		




  
  35
  
    
let mkdim_int = mkdim_int (get_loc ())


  		




  
  36
  
    
(* let mkdim_bool b = mkdim_bool (get_loc ()) b *)


  		




  
  37
  
    
let mkdim_ident = mkdim_ident (get_loc ())


  		




  
  38
  
    
let mkdim_appl = mkdim_appl (get_loc ())


  		




  
  39
  
    
let mkdim_appl_b f x1 x2 = mkdim_appl f [x1; x2]


  		




  
  40
  
    
let mkdim_appl_u f x = mkdim_appl f [x]


  		




  
  41
  
    
let mkdim_ite = mkdim_ite (get_loc ())


  		




  
  42
  
    

  		




  
  43
  
    
let mkarraytype = List.fold_left (fun t d -> Tydec_array (d, t))


  		




  
  44
  
    

  		




  
  45
  
    
let mkvdecls const typ clock expr =


  		




  
  46
  
    
  List.map (fun (id, loc) ->


  		




  
  47
  
    
      mkvar_decl (id,


  		




  
  48
  
    
                  mktyp (match typ with Some t -> t | None -> Tydec_any),


  		




  
  49
  
    
                  (match clock with Some ck -> ck | None -> mkclock Ckdec_any),


  		




  
  50
  
    
                  const, expr, None) loc)


  		




  
  51
  
    

  		




  
  52
  
    
(* let mkannots annots = { annots = annots; annot_loc = get_loc () } *)


  		




  41
  53
  
    

  		




  42
  54
  
    
let node_stack : ident list ref = ref []


  		




  43
  
  
    
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack


  		




  44
  
  
    
let push_node nd =  node_stack:= nd :: !node_stack


  		




  
  55
  
    
(* let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack *)


  		




  
  56
  
    
let push_node nd = node_stack := nd :: !node_stack; nd


  		




  45
  57
  
    
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false


  		




  46
  58
  
    
let get_current_node () = try List.hd !node_stack with _ -> assert false


  		




  47
  59
  
    

  		




  48
  60
  
    
let rec fby expr n init =


  		




  49
  
  
    
  if n<=1 then


  		




  
  61
  
    
  if n <= 1 then


  		




  50
  62
  
    
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))


  		




  51
  63
  
    
  else


  		




  52
  
  
    
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))


  		




  
  64
  
    
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n - 1) init))))


  		




  53
  65
  
    

  		




  54
  66
  
    
 


  		




  55
  67
  
    
%}


  		




  ......




  69
  81
  
    
%token AMPERAMPER BARBAR NOT POWER


  		




  70
  82
  
    
%token IF THEN ELSE


  		




  71
  83
  
    
%token MERGE FBY WHEN WHENNOT EVERY


  		




  72
  
  
    
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST


  		




  
  84
  
    
%token NODE LET TEL RETURNS VAR TYPE CONST


  		




  73
  85
  
    
%token STRUCT ENUM


  		




  74
  86
  
    
%token TINT TREAL TBOOL TCLOCK


  		




  75
  87
  
    
%token EQ LT GT LTE GTE NEQ


  		




  76
  88
  
    
%token AND OR XOR IMPL


  		




  77
  89
  
    
%token MULT DIV MOD


  		




  78
  
  
    
%token MINUS PLUS UMINUS


  		




  
  90
  
    
%token MINUS PLUS 


  		




  79
  91
  
    
%token PRE ARROW


  		




  80
  92
  
    
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT


  		




  81
  93
  
    
%token INVARIANT MODE CCODE MATLAB


  		




  ......




  83
  95
  
    
%token PROTOTYPE LIB


  		




  84
  96
  
    
%token EOF


  		




  85
  97
  
    

  		




  86
  
  
    
%nonassoc prec_exists prec_forall


  		




  87
  
  
    
%nonassoc COMMA


  		




  
  98
  
    
%nonassoc p_string


  		




  
  99
  
    
%nonassoc p_vdecl


  		




  
  100
  
    
%left SCOL


  		




  88
  101
  
    
%nonassoc EVERY


  		




  89
  
  
    
%left MERGE IF


  		




  90
  102
  
    
%nonassoc ELSE


  		




  91
  103
  
    
%right ARROW FBY


  		




  92
  104
  
    
%left WHEN WHENNOT 


  		




  93
  
  
    
%right COLCOL


  		




  94
  105
  
    
%right IMPL


  		




  95
  106
  
    
%left OR XOR BARBAR


  		




  96
  107
  
    
%left AND AMPERAMPER


  		




  97
  108
  
    
%left NOT


  		




  98
  
  
    
%nonassoc INT


  		




  99
  109
  
    
%nonassoc EQ LT GT LTE GTE NEQ


  		




  100
  110
  
    
%left MINUS PLUS


  		




  101
  111
  
    
%left MULT DIV MOD


  		




  102
  
  
    
%left UMINUS


  		




  
  112
  
    
%left p_uminus


  		




  103
  113
  
    
%left POWER


  		




  104
  
  
    
%left PRE LAST


  		




  
  114
  
    
%left PRE


  		




  105
  115
  
    
%nonassoc RBRACKET


  		




  106
  116
  
    
%nonassoc LBRACKET


  		




  107
  117
  
    

  		




  108
  
  
    
%start prog


  		




  109
  
  
    
%type <Lustre_types.top_decl list> prog


  		




  
  118
  
    
%start <Lustre_types.top_decl list> prog


  		




  110
  119
  
    

  		




  111
  
  
    
%start header


  		




  112
  
  
    
%type <Lustre_types.top_decl list> header


  		




  
  120
  
    
%start <Lustre_types.top_decl list> header


  		




  113
  121
  
    

  		




  114
  
  
    
%start lustre_annot


  		




  115
  
  
    
%type <Lustre_types.expr_annot> lustre_annot


  		




  
  122
  
    
%start <Lustre_types.expr_annot> lustre_annot


  		




  116
  123
  
    

  		




  117
  
  
    
%start lustre_spec


  		




  118
  
  
    
%type <Lustre_types.spec_types> lustre_spec


  		




  
  124
  
    
%start <Lustre_types.spec_types> lustre_spec


  		




  119
  125
  
    

  		




  120
  
  
    
%start signed_const


  		




  121
  
  
    
%type <Lustre_types.constant> signed_const


  		




  122
  
  
    

  		




  123
  
  
    
%start expr


  		




  124
  
  
    
%type <Lustre_types.expr> expr


  		




  125
  
  
    

  		




  126
  
  
    
%start stmt_list


  		




  127
  
  
    
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list


  		




  128
  
  
    

  		




  129
  
  
    
%start vdecl_list


  		




  130
  
  
    
%type <Lustre_types.var_decl list> vdecl_list


  		




  131
  126
  
    
%%


  		




  132
  127
  
    

  		




  
  128
  
    
ident:


  		




  
  129
  
    
| x=UIDENT { x }


  		




  
  130
  
    
| x=IDENT  { x }


  		




  133
  131
  
    

  		




  134
  132
  
    
module_ident:


  		




  135
  
  
    
  UIDENT { $1 }


  		




  136
  
  
    
| IDENT  { $1 }


  		




  
  133
  
    
| m=ident { m }


  		




  137
  134
  
    

  		




  138
  135
  
    
file_ident:


  		




  139
  
  
    
module_ident { $1 } 


  		




  140
  
  
    
| module_ident POINT file_ident { $1 ^ "." ^ $3 } 


  		




  
  136
  
    
| m=module_ident                    { m }


  		




  
  137
  
    
| m=module_ident POINT f=file_ident { m ^ "." ^ f }


  		




  141
  138
  
    

  		




  142
  139
  
    
path_ident:


  		




  143
  
  
    
POINT DIV path_ident { "./" ^ $3 }


  		




  144
  
  
    
| file_ident DIV path_ident { $1 ^ "/" ^ $3 }


  		




  145
  
  
    
| DIV path_ident { "/" ^ $2 }


  		




  146
  
  
    
| file_ident { $1 }


  		




  
  140
  
    
| POINT DIV p=path_ident        { "./" ^ p }


  		




  
  141
  
    
| f=file_ident DIV p=path_ident { f ^ "/" ^ p }


  		




  
  142
  
    
| DIV p=path_ident              { "/" ^ p }


  		




  
  143
  
    
| f=file_ident                  { f }


  		




  147
  144
  
    

  		




  148
  145
  
    
tag_bool:


  		




  149
  
  
    
  | TRUE    { tag_true }


  		




  150
  
  
    
  | FALSE   { tag_false }


  		




  
  146
  
    
| TRUE  { tag_true }


  		




  
  147
  
    
| FALSE { tag_false }


  		




  151
  148
  
    

  		




  152
  149
  
    
tag_ident:


  		




  153
  
  
    
  UIDENT  { $1 }


  		




  154
  
  
    
  | tag_bool { $1 }


  		




  
  150
  
    
| t=UIDENT   { t }


  		




  
  151
  
    
| t=tag_bool { t }


  		




  155
  152
  
    

  		




  156
  153
  
    
node_ident:


  		




  157
  
  
    
  UIDENT { $1 }


  		




  158
  
  
    
| IDENT  { $1 }


  		




  
  154
  
    
| n=ident { n }


  		




  159
  155
  
    

  		




  160
  156
  
    
node_ident_decl:


  		




  161
  
  
    
 node_ident { push_node $1; $1 }


  		




  
  157
  
    
| n=node_ident { push_node n }


  		




  162
  158
  
    

  		




  163
  159
  
    
vdecl_ident:


  		




  164
  
  
    
  UIDENT { mkident $1 }


  		




  165
  
  
    
| IDENT  { mkident $1 }


  		




  
  160
  
    
| x=ident { mkident x }


  		




  166
  161
  
    

  		




  167
  162
  
    
const_ident:


  		




  168
  
  
    
  UIDENT { $1 }


  		




  169
  
  
    
| IDENT  { $1 }


  		




  
  163
  
    
| c=ident { c }


  		




  170
  164
  
    

  		




  171
  165
  
    
type_ident:


  		




  172
  
  
    
  IDENT { $1 }


  		




  
  166
  
    
| t=IDENT { t }


  		




  173
  167
  
    

  		




  174
  168
  
    
prog:


  		




  175
  
  
    
 prefix_prog top_decl_list EOF { $1 @ (List.rev $2) }


  		




  176
  
  
    

  		




  177
  
  
    
prefix_prog:


  		




  178
  
  
    
    { [] }


  		




  179
  
  
    
  | open_lusi prefix_prog { $1 :: $2 }


  		




  180
  
  
    
  | typ_def prefix_prog   { ($1 false (* not a header *)) :: $2 }


  		




  181
  
  
    

  		




  182
  
  
    
prefix_header:


  		




  183
  
  
    
    { [] }


  		




  184
  
  
    
  | open_lusi prefix_header { $1 :: $2 }


  		




  185
  
  
    
  | typ_def prefix_header   { ($1 true (* is a header *)) :: $2 }


  		




  
  169
  
    
| p=prefix ds=flatten(top_decl*) EOF { List.map ((|>) false) p @ ds }


  		




  186
  170
  
    

  		




  187
  171
  
    
header:


  		




  188
  
  
    
 prefix_header top_decl_header_list EOF { $1 @ (List.rev $2) }


  		




  
  172
  
    
| p=prefix ds=flatten(top_decl_header*) EOF { List.map ((|>) true) p @ ds }


  		




  189
  173
  
    

  		




  
  174
  
    
prefix:


  		




  
  175
  
    
|                      { [] }


  		




  
  176
  
    
| o=open_lusi p=prefix { (fun _ -> o) :: p }


  		




  
  177
  
    
| td=typ_def p=prefix  { (fun is_header -> td is_header) :: p }


  		




  190
  178
  
    

  		




  191
  179
  
    
open_lusi:


  		




  192
  
  
    
  | OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) }


  		




  193
  
  
    
  | INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) }


  		




  194
  
  
    
  | OPEN LT path_ident GT { mktop_decl false (Open (false, $3))  }


  		




  195
  
  
    

  		




  196
  
  
    
top_decl_list:


  		




  197
  
  
    
   {[]}


  		




  198
  
  
    
| top_decl_list top_decl {$2@$1}


  		




  199
  
  
    

  		




  200
  
  
    

  		




  201
  
  
    
top_decl_header_list:


  		




  202
  
  
    
   { [] }


  		




  203
  
  
    
| top_decl_header_list top_decl_header { $2@$1 }


  		




  
  180
  
    
| OPEN QUOTE p=path_ident QUOTE    { mktop_decl false (Open (true, p)) }


  		




  
  181
  
    
| INCLUDE QUOTE p=path_ident QUOTE { mktop_decl false (Include p) }


  		




  
  182
  
    
| OPEN LT p=path_ident GT          { mktop_decl false (Open (false, p))  }


  		




  204
  183
  
    

  		




  205
  184
  
    
state_annot:


  		




  206
  
  
    
  FUNCTION { true }


  		




  207
  
  
    
| NODE { false }


  		




  
  185
  
    
| FUNCTION { true }


  		




  
  186
  
    
| NODE     { false }


  		




  208
  187
  
    

  		




  209
  188
  
    
top_decl_header:


  		




  210
  
  
    
| CONST cdecl_list { List.rev ($2 true) }


  		




  211
  
  
    
| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL


  		




  212
  
  
    
    {


  		




  213
  
  
    
      let inputs = List.rev $5 in


  		




  214
  
  
    
      let outputs = List.rev $10 in


  		




  215
  
  
    
      let nd = mktop_decl true (ImportedNode


  		




  216
  
  
    
				 {nodei_id = $3;


  		




  217
  
  
    
				  nodei_type = Types.new_var ();


  		




  218
  
  
    
				  nodei_clock = Clocks.new_var true;


  		




  219
  
  
    
				  nodei_inputs = inputs;


  		




  220
  
  
    
				  nodei_outputs = outputs;


  		




  221
  
  
    
				  nodei_stateless = $2;


  		




  222
  
  
    
				  nodei_spec = $1;


  		




  223
  
  
    
				  nodei_prototype = $13;


  		




  224
  
  
    
				  nodei_in_lib = $14;})


  		




  225
  
  
    
     in


  		




  226
  
  
    
     pop_node ();


  		




  227
  
  
    
     [nd] } 


  		




  228
  
  
    
| top_contract { [$1] }


  		




  229
  
  
    

  		




  230
  
  
    

  		




  231
  
  
    
prototype_opt:


  		




  232
  
  
    
 { None }


  		




  233
  
  
    
| PROTOTYPE node_ident { Some $2}


  		




  234
  
  
    

  		




  235
  
  
    
in_lib_list:


  		




  236
  
  
    
{ [] }


  		




  237
  
  
    
| LIB module_ident in_lib_list { $2::$3 } 


  		




  
  189
  
    
| CONST ds=cdecl+ SCOL


  		




  
  190
  
    
  { List.map ((|>) true) ds }


  		




  
  191
  
    
| nodei_spec=nodespecs nodei_stateless=state_annot nodei_id=node_ident_decl


  		




  
  192
  
    
  LPAR nodei_inputs=vdecl_list SCOL? RPAR


  		




  
  193
  
    
  RETURNS LPAR nodei_outputs=vdecl_list SCOL? RPAR


  		




  
  194
  
    
  nodei_prototype=preceded(PROTOTYPE, node_ident)?


  		




  
  195
  
    
  nodei_in_lib=preceded(LIB, module_ident)* SCOL


  		




  
  196
  
    
  { let nd = mktop_decl true (ImportedNode {


  		




  
  197
  
    
                                  nodei_id;


  		




  
  198
  
    
                                  nodei_type = Types.new_var ();


  		




  
  199
  
    
                                  nodei_clock = Clocks.new_var true;


  		




  
  200
  
    
                                  nodei_inputs;


  		




  
  201
  
    
                                  nodei_outputs;


  		




  
  202
  
    
                                  nodei_stateless;


  		




  
  203
  
    
                                  nodei_spec;


  		




  
  204
  
    
                                  nodei_prototype;


  		




  
  205
  
    
                                  nodei_in_lib


  		




  
  206
  
    
               })


  		




  
  207
  
    
    in


  		




  
  208
  
    
    pop_node ();


  		




  
  209
  
    
    [nd]


  		




  
  210
  
    
  }


  		




  
  211
  
    
| c=top_contract


  		




  
  212
  
    
  { [c] }


  		




  238
  213
  
    

  		




  239
  214
  
    
top_decl:


  		




  240
  
  
    
| CONST cdecl_list { List.rev ($2 false) }


  		




  241
  
  
    
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL 


  		




  242
  
  
    
    {


  		




  243
  
  
    
     let stmts, asserts, annots = $16 in


  		




  244
  
  
    
      (* Declaring eqs annots *)


  		




  245
  
  
    
      List.iter (fun ann -> 


  		




  246
  
  
    
	List.iter (fun (key, _) -> 


  		




  247
  
  
    
	  Annotations.add_node_ann $2 key


  		




  248
  
  
    
	) ann.annots


  		




  249
  
  
    
      ) annots;


  		




  250
  
  
    
      (* Building the node *)


  		




  251
  
  
    
      let inputs = List.rev $4 in


  		




  252
  
  
    
      let outputs = List.rev $9 in


  		




  253
  
  
    
     let nd = mktop_decl false (Node


  		




  254
  
  
    
				  {node_id = $2;


  		




  255
  
  
    
				   node_type = Types.new_var ();


  		




  256
  
  
    
				   node_clock = Clocks.new_var true;


  		




  257
  
  
    
				   node_inputs = inputs;


  		




  258
  
  
    
				   node_outputs = outputs;


  		




  259
  
  
    
				   node_locals = List.rev $14;


  		




  260
  
  
    
				   node_gencalls = [];


  		




  261
  
  
    
				   node_checks = [];


  		




  262
  
  
    
				   node_asserts = asserts; 


  		




  263
  
  
    
				   node_stmts = stmts;


  		




  264
  
  
    
				   node_dec_stateless = $1;


  		




  265
  
  
    
				   node_stateless = None;


  		




  266
  
  
    
				   node_spec = $13;


  		




  267
  
  
    
				   node_annot = annots;


  		




  268
  
  
    
				   node_iscontract = false;


  		




  269
  
  
    
			       })


  		




  270
  
  
    
     in


  		




  271
  
  
    
     pop_node ();


  		




  272
  
  
    
     (*add_node $3 nd;*) [nd] }


  		




  273
  
  
    

  		




  274
  
  
    

  		




  275
  
  
    
| NODESPEC


  		




  276
  
  
    
    { match $1 with


  		




  277
  
  
    
      | LocalContract c -> assert false


  		




  278
  
  
    
      | TopContract c   -> c


  		




  279
  
  
    
			 


  		




  280
  
  
    
    }


  		




  
  215
  
    
| CONST ds=cdecl+ SCOL


  		




  
  216
  
    
  { List.map ((|>) false) ds }


  		




  
  217
  
    
| node_dec_stateless=state_annot node_id=node_ident_decl


  		




  
  218
  
    
  LPAR node_inputs=vdecl_list SCOL? RPAR


  		




  
  219
  
    
  RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?


  		




  
  220
  
    
  node_spec=nodespecs


  		




  
  221
  
    
  node_locals=locals LET content=stmt_list TEL


  		




  
  222
  
    
  { let node_stmts, node_asserts, node_annot = content in


  		




  
  223
  
    
    (* Declaring eqs annots *)


  		




  
  224
  
    
    List.iter (fun ann ->


  		




  
  225
  
    
        List.iter (fun (key, _) ->


  		




  
  226
  
    
            Annotations.add_node_ann node_id key)


  		




  
  227
  
    
          ann.annots)


  		




  
  228
  
    
      node_annot;


  		




  
  229
  
    
    (* Building the node *)


  		




  
  230
  
    
    let nd = mktop_decl false (Node


  		




  
  231
  
    
                                 {node_id;


  		




  
  232
  
    
                                  node_type = Types.new_var ();


  		




  
  233
  
    
                                  node_clock = Clocks.new_var true;


  		




  
  234
  
    
                                  node_inputs;


  		




  
  235
  
    
                                  node_outputs;


  		




  
  236
  
    
                                  node_locals;


  		




  
  237
  
    
                                  node_gencalls = [];


  		




  
  238
  
    
                                  node_checks = [];


  		




  
  239
  
    
                                  node_asserts;


  		




  
  240
  
    
                                  node_stmts;


  		




  
  241
  
    
                                  node_dec_stateless;


  		




  
  242
  
    
                                  node_stateless = None;


  		




  
  243
  
    
                                  node_spec;


  		




  
  244
  
    
                                  node_annot;


  		




  
  245
  
    
                                  node_iscontract = false;


  		




  
  246
  
    
               })


  		




  
  247
  
    
    in


  		




  
  248
  
    
    pop_node ();


  		




  
  249
  
    
    (*add_node $3 nd;*)


  		




  
  250
  
    
    [nd]


  		




  
  251
  
    
  }


  		




  
  252
  
    
| s=NODESPEC


  		




  
  253
  
    
  { match s with


  		




  
  254
  
    
    | LocalContract _ -> assert false


  		




  
  255
  
    
    | TopContract c   -> c


  		




  
  256
  
    
  }


  		




  281
  257
  
    

  		




  282
  258
  
    
nodespecs:


  		




  283
  
  
    
nodespec_list {


  		




  284
  
  
    
  match $1 with


  		




  285
  
  
    
  | None -> None 


  		




  286
  
  
    
  | Some c -> Some (Contract c)


  		




  287
  
  
    
}


  		




  
  259
  
    
| ss=nodespec_list


  		




  
  260
  
    
  { match ss with


  		




  
  261
  
    
    | None   -> None


  		




  
  262
  
    
    | Some c -> Some (Contract c)


  		




  
  263
  
    
  }


  		




  288
  264
  
    

  		




  289
  265
  
    
nodespec_list:


  		




  290
  
  
    
 { None }


  		




  291
  
  
    
  | NODESPEC nodespec_list {


  		




  292
  
  
    
	       let extract x = match x with LocalContract c -> c | _ -> assert false in


  		




  293
  
  
    
	       let s1 = extract $1 in


  		




  294
  
  
    
	       match $2 with


  		




  295
  
  
    
	       | None -> Some s1


  		




  296
  
  
    
	       | Some s2 -> Some (merge_contracts s1 s2) }


  		




  297
  
  
    

  		




  298
  
  
    
typ_def_list:


  		




  299
  
  
    
    /* empty */             { (fun itf -> []) }


  		




  300
  
  
    
| typ_def typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($2 itf)) }


  		




  
  266
  
    
| { None }


  		




  
  267
  
    
| s=NODESPEC ss=nodespec_list


  		




  
  268
  
    
  { let extract x = match x with LocalContract c -> c | _ -> assert false in


  		




  
  269
  
    
    let s1 = extract s in


  		




  
  270
  
    
    match ss with


  		




  
  271
  
    
    | None -> Some s1


  		




  
  272
  
    
    | Some s2 -> Some (merge_contracts s1 s2)


  		




  
  273
  
    
  }


  		




  301
  274
  
    

  		




  302
  275
  
    
typ_def:


  		




  303
  
  
    
  TYPE type_ident EQ typ_def_rhs SCOL { (fun itf ->


  		




  304
  
  
    
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;


  		




  305
  
  
    
								   tydef_desc = $4


  		




  306
  
  
    
							})


  		




  307
  
  
    
			       in (*add_type itf $2 typ;*) typ) }


  		




  
  276
  
    
| TYPE tydef_id=type_ident EQ tydef_desc=typ_def_rhs SCOL


  		




  
  277
  
    
  { fun itf ->


  		




  
  278
  
    
    let typ = mktop_decl itf (TypeDef { tydef_id; tydef_desc }) in


  		




  
  279
  
    
    (*add_type itf $2 typ;*)


  		




  
  280
  
    
    typ


  		




  
  281
  
    
  }


  		




  308
  282
  
    

  		




  309
  283
  
    
typ_def_rhs:


  		




  310
  
  
    
  typeconst                   { $1 }


  		




  311
  
  
    
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }


  		




  312
  
  
    
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }


  		




  
  284
  
    
| t=typeconst


  		




  
  285
  
    
  { t }


  		




  
  286
  
    
| ENUM LCUR ts=separated_nonempty_list(COMMA, UIDENT) RCUR


  		




  
  287
  
    
  { Tydec_enum ts }


  		




  
  288
  
    
| STRUCT LCUR fs=separated_list(SCOL, separated_pair(IDENT, COL, typeconst)) RCUR


  		




  
  289
  
    
  { Tydec_struct fs }


  		




  313
  290
  
    

  		




  314
  
  
    
array_typ_decl:


  		




  315
  
  
    
 %prec POWER                { fun typ -> typ }


  		




  316
  
  
    
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }


  		




  
  291
  
    
%inline array_typ_decl:


  		




  
  292
  
    
|                          { [] }


  		




  
  293
  
    
| ds=preceded(POWER, dim)+ { ds }


  		




  317
  294
  
    

  		




  318
  295
  
    
typeconst:


  		




  319
  
  
    
  TINT array_typ_decl   { $2 Tydec_int }


  		




  320
  
  
    
| TBOOL array_typ_decl  { $2 Tydec_bool  }


  		




  321
  
  
    
| TREAL array_typ_decl  { $2 Tydec_real  }


  		




  322
  
  
    
/* | TFLOAT array_typ_decl { $2 Tydec_float } */


  		




  323
  
  
    
| type_ident array_typ_decl  { $2 (Tydec_const $1) }


  		




  324
  
  
    
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }


  		




  325
  
  
    
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }


  		




  326
  
  
    

  		




  327
  
  
    
tag_list:


  		




  328
  
  
    
  UIDENT                { $1 :: [] }


  		




  329
  
  
    
| tag_list COMMA UIDENT { $3 :: $1 }


  		




  330
  
  
    
      


  		




  331
  
  
    
field_list:                           { [] }


  		




  332
  
  
    
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }


  		




  333
  
  
    
      


  		




  
  296
  
    
| TINT ds=array_typ_decl         { mkarraytype Tydec_int ds }


  		




  
  297
  
    
| TBOOL ds=array_typ_decl        { mkarraytype Tydec_bool ds }


  		




  
  298
  
    
| TREAL ds=array_typ_decl        { mkarraytype Tydec_real ds }


  		




  
  299
  
    
/* | TFLOAT ds=array_typ_decl { mkarraytype Tydec_float ds } */


  		




  
  300
  
    
| t=type_ident ds=array_typ_decl { mkarraytype (Tydec_const t) ds }


  		




  
  301
  
    
| TBOOL TCLOCK                   { Tydec_clock Tydec_bool }


  		




  
  302
  
    
| t=IDENT TCLOCK                 { Tydec_clock (Tydec_const t) }


  		




  
  303
  
    

  		




  334
  304
  
    
stmt_list:


  		




  335
  
  
    
  { [], [], [] }


  		




  336
  
  
    
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}


  		




  337
  
  
    
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}


  		




  338
  
  
    
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}


  		




  339
  
  
    
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}


  		




  
  305
  
    
| { [], [], [] }


  		




  
  306
  
    
| e=eq ss=stmt_list


  		




  
  307
  
    
  { let eql, assertl, annotl = ss in


  		




  
  308
  
    
    Eq e :: eql, assertl, annotl


  		




  
  309
  
    
  }


  		




  
  310
  
    
| a=assert_ ss=stmt_list


  		




  
  311
  
    
  { let eql, assertl, annotl = ss in


  		




  
  312
  
    
    eql, a :: assertl, annotl


  		




  
  313
  
    
  }


  		




  
  314
  
    
| a=ANNOT ss=stmt_list


  		




  
  315
  
    
  { let eql, assertl, annotl = ss in


  		




  
  316
  
    
    eql, assertl, a :: annotl


  		




  
  317
  
    
  }


  		




  
  318
  
    
| a=automaton ss=stmt_list


  		




  
  319
  
    
  { let eql, assertl, annotl = ss in


  		




  
  320
  
    
    Aut a :: eql, assertl, annotl


  		




  
  321
  
    
  }


  		




  340
  322
  
    

  		




  341
  323
  
    
automaton:


  		




  342
  
  
    
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }


  		




  343
  
  
    

  		




  344
  
  
    
handler_list:


  		




  345
  
  
    
     { [] }


  		




  346
  
  
    
| handler handler_list { $1::$2 }


  		




  
  324
  
    
| AUTOMATON t=type_ident hs=handler* { Automata.mkautomata (get_loc ()) t hs }


  		




  347
  325
  
    

  		




  348
  326
  
    
handler:


  		




  349
  
  
    
 STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }


  		




  350
  
  
    

  		




  351
  
  
    
unless_list:


  		




  352
  
  
    
    { [] }


  		




  353
  
  
    
| unless unless_list { $1::$2 }


  		




  354
  
  
    

  		




  355
  
  
    
until_list:


  		




  356
  
  
    
    { [] }


  		




  357
  
  
    
| until until_list { $1::$2 }


  		




  
  327
  
    
| STATE x=UIDENT COL ul=unless* l=locals LET ss=stmt_list TEL ut=until*


  		




  
  328
  
    
  { Automata.mkhandler (get_loc ()) x ul ut l ss }


  		




  358
  329
  
    

  		




  359
  330
  
    
unless:


  		




  360
  
  
    
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }


  		




  361
  
  
    
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }


  		




  
  331
  
    
| UNLESS e=expr RESTART s=UIDENT { get_loc (), e, true, s  }


  		




  
  332
  
    
| UNLESS e=expr RESUME s=UIDENT  { get_loc (), e, false, s }


  		




  362
  333
  
    

  		




  363
  334
  
    
until:


  		




  364
  
  
    
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }


  		




  365
  
  
    
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }


  		




  
  335
  
    
| UNTIL e=expr RESTART s=UIDENT { get_loc (), e, true, s }


  		




  
  336
  
    
| UNTIL e=expr RESUME s=UIDENT  { get_loc (), e, false, s }


  		




  366
  337
  
    

  		




  367
  338
  
    
assert_:


  		




  368
  
  
    
| ASSERT expr SCOL {mkassert ($2)}


  		




  
  339
  
    
| ASSERT e=expr SCOL { mkassert e }


  		




  369
  340
  
    

  		




  370
  341
  
    
eq:


  		




  371
  
  
    
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}


  		




  372
  
  
    
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}


  		




  
  342
  
    
| xs=pattern EQ e=expr SCOL {mkeq (List.map fst xs, e)}


  		




  373
  343
  
    

  		




  374
  
  
    
lustre_spec:


  		




  375
  
  
    
| top_contracts EOF     { TopContract $1 }


  		




  376
  
  
    
| contract_content EOF { LocalContract $1}


  		




  
  344
  
    
%inline pattern:


  		




  
  345
  
    
| xs=ident_list           { xs }


  		




  
  346
  
    
| LPAR xs=ident_list RPAR { xs }


  		




  377
  347
  
    

  		




  378
  
  
    
top_contracts:


  		




  379
  
  
    
| top_contract { [$1] }


  		




  380
  
  
    
| top_contract top_contracts { $1::$2 }


  		




  
  348
  
    
lustre_spec:


  		




  
  349
  
    
| cs=top_contract+ EOF   { TopContract cs }


  		




  
  350
  
    
| c=contract_content EOF { LocalContract c }


  		




  381
  351
  
    

  		




  382
  352
  
    
top_contract:


  		




  383
  
  
    
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL 


  		




  384
  
  
    
    {


  		




  385
  
  
    
      let nd = mktop_decl true (Node


  		




  386
  
  
    
				 {node_id = $2;


  		




  387
  
  
    
				  node_type = Types.new_var ();


  		




  388
  
  
    
				  node_clock = Clocks.new_var true;


  		




  389
  
  
    
				  node_inputs = List.rev $4;


  		




  390
  
  
    
				  node_outputs = List.rev $9;


  		




  391
  
  
    
				  node_locals = []; (* will be filled later *)


  		




  392
  
  
    
				  node_gencalls = [];


  		




  393
  
  
    
				  node_checks = [];


  		




  394
  
  
    
				  node_asserts = [];


  		




  395
  
  
    
				  node_stmts = []; (* will be filled later *)


  		




  396
  
  
    
				  node_dec_stateless = false;


  		




  397
  
  
    
				  (* By default we assume contracts as stateful *)


  		




  398
  
  
    
				  node_stateless = None;


  		




  399
  
  
    
				  node_spec = Some (Contract $14);


  		




  400
  
  
    
				  node_annot = [];


  		




  401
  
  
    
				  node_iscontract = true;


  		




  402
  
  
    
				 }


  		




  403
  
  
    
			       )


  		




  404
  
  
    
     in


  		




  405
  
  
    
     pop_node ();


  		




  406
  
  
    
     (*add_imported_node $3 nd;*)


  		




  407
  
  
    
     nd }


  		




  
  353
  
    
| CONTRACT node_id=node_ident_decl


  		




  
  354
  
    
  LPAR node_inputs=vdecl_list SCOL? RPAR


  		




  
  355
  
    
  RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?


  		




  
  356
  
    
  LET cc=contract_content TEL


  		




  
  357
  
    
  { let nd = mktop_decl true (Node {


  		




  
  358
  
    
                                  node_id;


  		




  
  359
  
    
                                  node_type = Types.new_var ();


  		




  
  360
  
    
                                  node_clock = Clocks.new_var true;


  		




  
  361
  
    
                                  node_inputs;


  		




  
  362
  
    
                                  node_outputs;


  		




  
  363
  
    
                                  node_locals = []; (* will be filled later *)


  		




  
  364
  
    
                                  node_gencalls = [];


  		




  
  365
  
    
                                  node_checks = [];


  		




  
  366
  
    
                                  node_asserts = [];


  		




  
  367
  
    
                                  node_stmts = []; (* will be filled later *)


  		




  
  368
  
    
                                  node_dec_stateless = false;


  		




  
  369
  
    
                                  (* By default we assume contracts as stateful *)


  		




  
  370
  
    
                                  node_stateless = None;


  		




  
  371
  
    
                                  node_spec = Some (Contract cc);


  		




  
  372
  
    
                                  node_annot = [];


  		




  
  373
  
    
                                  node_iscontract = true;


  		




  
  374
  
    
                                }


  		




  
  375
  
    
               )


  		




  
  376
  
    
    in


  		




  
  377
  
    
    pop_node ();


  		




  
  378
  
    
    (*add_imported_node $3 nd;*)


  		




  
  379
  
    
    nd


  		




  
  380
  
    
  }


  		




  408
  381
  
    

  		




  409
  382
  
    
contract_content:


  		




  410
  
  
    
{ empty_contract }


  		




  411
  
  
    
| CONTRACT contract_content { $2 }


  		




  412
  
  
    
| CONST IDENT EQ expr SCOL contract_content


  		




  413
  
  
    
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }


  		




  414
  
  
    
| CONST IDENT COL typeconst EQ expr SCOL contract_content


  		




  415
  
  
    
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }


  		




  416
  
  
    
| VAR IDENT COL typeconst EQ expr SCOL contract_content


  		




  417
  
  
    
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }


  		




  418
  
  
    
| ASSUME qexpr SCOL contract_content


  		




  419
  
  
    
    { merge_contracts (mk_contract_assume $2) $4 }


  		




  420
  
  
    
| ASSUME STRING qexpr SCOL contract_content


  		




  421
  
  
    
    { merge_contracts (mk_contract_assume ~name:$2 $3) $5 }


  		




  422
  
  
    
| GUARANTEES qexpr SCOL contract_content	


  		




  423
  
  
    
    { merge_contracts (mk_contract_guarantees $2) $4 }


  		




  424
  
  
    
| GUARANTEES STRING qexpr SCOL contract_content	


  		




  425
  
  
    
    { merge_contracts (mk_contract_guarantees ~name:$2 $3) $5 }


  		




  426
  
  
    
| MODE IDENT LPAR mode_content RPAR SCOL contract_content


  		




  427
  
  
    
	{ merge_contracts (


  		




  428
  
  
    
	  let r, e = $4 in 


  		




  429
  
  
    
	  mk_contract_mode $2 r e (get_loc())) $7 }	


  		




  430
  
  
    
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content


  		




  431
  
  
    
    { merge_contracts (mk_contract_import $2  (mkexpr (Expr_tuple (List.rev $4)))  (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }


  		




  432
  
  
    
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content


  		




  433
  
  
    
    { merge_contracts (mk_contract_import $2  $4  (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }


  		




  434
  
  
    
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR expr RPAR SCOL contract_content


  		




  435
  
  
    
    { merge_contracts (mk_contract_import $2  (mkexpr (Expr_tuple (List.rev $4)))  $8 (get_loc())) $11 }


  		




  436
  
  
    
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content


  		




  437
  
  
    
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }


  		




  
  383
  
    
| { empty_contract }


  		




  
  384
  
    
| CONTRACT cc=contract_content


  		




  
  385
  
    
  { cc }


  		




  
  386
  
    
| CONST x=IDENT COL t=typeconst? EQ e=expr SCOL cc=contract_content


  		




  
  387
  
    
  { merge_contracts (mk_contract_var x true (mkotyp t) e (get_loc())) cc }


  		




  
  388
  
    
| VAR x=IDENT COL t=typeconst EQ e=expr SCOL cc=contract_content


  		




  
  389
  
    
  { merge_contracts (mk_contract_var x false (Some (mktyp t)) e (get_loc())) cc }


  		




  
  390
  
    
| ASSUME x=ioption(STRING) e=qexpr SCOL cc=contract_content


  		




  
  391
  
    
  { merge_contracts (mk_contract_assume x e) cc }


  		




  
  392
  
    
| GUARANTEES x=ioption(STRING) e=qexpr SCOL cc=contract_content


  		




  
  393
  
    
  { merge_contracts (mk_contract_guarantees x e) cc }


  		




  
  394
  
    
| MODE x=IDENT LPAR mc=mode_content RPAR SCOL cc=contract_content


  		




  
  395
  
    
  { merge_contracts (


  		




  
  396
  
    
        let r, e = mc in


  		




  
  397
  
    
        mk_contract_mode x r e (get_loc())) cc


  		




  
  398
  
    
  }


  		




  
  399
  
    
| IMPORT x=IDENT LPAR xs=expr_or_tuple RPAR RETURNS LPAR ys=expr_or_tuple RPAR


  		




  
  400
  
    
  SCOL cc=contract_content


  		




  
  401
  
    
  { merge_contracts (mk_contract_import x xs ys (get_loc())) cc }


  		




  
  402
  
    

  		




  
  403
  
    
%inline expr_or_tuple:


  		




  
  404
  
    
| e=expr                     { e }


  		




  
  405
  
    
| e=expr COMMA es=array_expr { mkexpr (Expr_tuple (e :: es)) }


  		




  438
  406
  
    

  		




  439
  407
  
    
mode_content:


  		




  440
  
  
    
{ [], [] }


  		




  441
  
  
    
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }


  		




  442
  
  
    
| REQUIRE STRING qexpr SCOL mode_content { let (r,e) = $5 in {$3 with eexpr_name = Some $2}::r, e }


  		




  443
  
  
    
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }


  		




  444
  
  
    
| ENSURE STRING qexpr SCOL mode_content { let (r,e) = $5 in r, {$3 with eexpr_name = Some $2}::e }


  		




  445
  
  
    

  		




  446
  
  
    
/* WARNING: UNUSED RULES */


  		




  447
  
  
    
tuple_qexpr:


  		




  448
  
  
    
| qexpr COMMA qexpr {[$3;$1]}


  		




  449
  
  
    
| tuple_qexpr COMMA qexpr {$3::$1}


  		




  
  408
  
    
| { [], [] }


  		




  
  409
  
    
| REQUIRE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content


  		




  
  410
  
    
  { let (r, e) = mc in


  		




  
  411
  
    
    { qe with eexpr_name } :: r, e }


  		




  
  412
  
    
| ENSURE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content


  		




  
  413
  
    
  { let (r, e) = mc in


  		




  
  414
  
    
    r, { qe with eexpr_name } :: e }


  		




  
  415
  
    

  		




  
  416
  
    
(* /* WARNING: UNUSED RULES */


  		




  
  417
  
    
 * tuple_qexpr:


  		




  
  418
  
    
 * | qexpr COMMA qexpr {[$3;$1]}


  		




  
  419
  
    
 * | tuple_qexpr COMMA qexpr {$3::$1} *)


  		




  450
  420
  
    

  		




  451
  421
  
    
qexpr:


  		




  452
  
  
    
| expr { mkeexpr $1 }


  		




  
  422
  
    
| e=expr                      { mkeexpr e }


  		




  453
  423
  
    
  /* Quantifiers */


  		




  454
  
  
    
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 


  		




  455
  
  
    
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }


  		




  
  424
  
    
| EXISTS x=vdecl SCOL e=qexpr { extend_eexpr [Exists, x] e }


  		




  
  425
  
    
| FORALL x=vdecl SCOL e=qexpr { extend_eexpr [Forall, x] e }


  		




  456
  426
  
    

  		




  457
  
  
    

  		




  458
  
  
    
tuple_expr:


  		




  459
  
  
    
    expr COMMA expr {[$3;$1]}


  		




  460
  
  
    
| tuple_expr COMMA expr {$3::$1}


  		




  
  427
  
    
(* %inline tuple_expr:


  		




  
  428
  
    
 * | e=expr COMMA es=array_expr { e :: es } *)


  		




  461
  429
  
    

  		




  462
  430
  
    
// Same as tuple expr but accepting lists with single element


  		




  463
  
  
    
array_expr:


  		




  464
  
  
    
  expr {[$1]}


  		




  465
  
  
    
| expr COMMA array_expr {$1::$3}


  		




  466
  
  
    

  		




  467
  
  
    
dim_list:


  		




  468
  
  
    
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }


  		




  469
  
  
    
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }


  		




  
  431
  
    
%inline array_expr:


  		




  
  432
  
    
| es=separated_nonempty_list(COMMA, expr) { es }


  		




  470
  433
  
    

  		




  471
  434
  
    
expr:


  		




  472
  435
  
    
/* constants */


  		




  473
  
  
    
  INT {mkexpr (Expr_const (Const_int $1))}


  		




  474
  
  
    
| REAL {mkexpr (Expr_const (Const_real $1))}


  		




  475
  
  
    
| STRING {mkexpr (Expr_const (Const_string $1))}


  		




  476
  
  
    
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} 


  		




  477
  
  
    
    


  		




  478
  
  
    
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/


  		




  
  436
  
    
| c=INT                   { mkexpr (Expr_const (Const_int c)) }


  		




  
  437
  
    
| c=REAL                  { mkexpr (Expr_const (Const_real c)) }


  		




  
  438
  
    
| c=STRING %prec p_string { mkexpr (Expr_const (Const_string c)) }


  		




  
  439
  
    
| COLCOL c=IDENT          { mkexpr (Expr_const (Const_modeid c)) }


  		




  
  440
  
    
/* | c=FLOAT { mkexpr (Expr_const (Const_float c)) }*/


  		




  
  441
  
    

  		




  479
  442
  
    
/* Idents or type enum tags */


  		




  480
  
  
    
| IDENT { mkexpr (Expr_ident $1) }


  		




  481
  
  
    
| UIDENT { mkexpr (Expr_ident $1) (* TODO we will differenciate enum constants from variables later *) }


  		




  482
  
  
    
| tag_bool {


  		




  483
  
  
    
	(* on sept 2014, X chenged the Const to 


  		




  484
  
  
    
	mkexpr (Expr_ident $1)


  		




  485
  
  
    
	reverted back to const on july 2019 *)


  		




  486
  
  
    
	mkexpr (Expr_const (Const_tag $1)) }


  		




  487
  
  
    
| LPAR ANNOT expr RPAR


  		




  488
  
  
    
    {update_expr_annot (get_current_node ()) $3 $2}


  		




  489
  
  
    
| LPAR expr RPAR


  		




  490
  
  
    
    {$2}


  		




  491
  
  
    
| LPAR tuple_expr RPAR


  		




  492
  
  
    
    {mkexpr (Expr_tuple (List.rev $2))}


  		




  
  443
  
    
| x=IDENT    { mkexpr (Expr_ident x) }


  		




  
  444
  
    
| x=UIDENT   { mkexpr (Expr_ident x) (* TODO we will differenciate enum constants from variables later *) }


  		




  
  445
  
    
| t=tag_bool { mkexpr (Expr_const (Const_tag t)) } (* on sept 2014, X changed the Const to


  		




  
  446
  
    
                                                      mkexpr (Expr_ident $1)


  		




  
  447
  
    
                                                      reverted back to const on july 2019 *)


  		




  
  448
  
    
| LPAR a=ANNOT e=expr RPAR  { update_expr_annot (get_current_node ()) e a }


  		




  
  449
  
    
| LPAR e=expr_or_tuple RPAR { e }


  		




  493
  450
  
    

  		




  494
  451
  
    
/* Array expressions */


  		




  495
  
  
    
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }


  		




  496
  
  
    
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }


  		




  497
  
  
    
| expr LBRACKET dim_list { $3 $1 }


  		




  
  452
  
    
| LBRACKET es=array_expr RBRACKET


  		




  
  453
  
    
  { mkexpr (Expr_array es) }


  		




  
  454
  
    
| e=expr POWER d=dim


  		




  
  455
  
    
  { mkexpr (Expr_power (e, d)) }


  		




  
  456
  
    
| e=expr ds=delimited(LBRACKET, dim, RBRACKET)+


  		




  
  457
  
    
  { List.fold_left (fun base d -> mkexpr (Expr_access (base, d))) e ds }


  		




  498
  458
  
    

  		




  499
  459
  
    
/* Temporal operators */


  		




  500
  
  
    
| PRE expr 


  		




  501
  
  
    
    {mkexpr (Expr_pre $2)}


  		




  502
  
  
    
| expr ARROW expr 


  		




  503
  
  
    
    {mkexpr (Expr_arrow ($1,$3))}


  		




  504
  
  
    
| expr FBY expr 


  		




  505
  
  
    
    {(*mkexpr (Expr_fby ($1,$3))*)


  		




  506
  
  
    
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}


  		




  507
  
  
    
| expr WHEN vdecl_ident


  		




  508
  
  
    
    {mkexpr (Expr_when ($1,fst $3,tag_true))}


  		




  509
  
  
    
| expr WHENNOT vdecl_ident


  		




  510
  
  
    
    {mkexpr (Expr_when ($1,fst $3,tag_false))}


  		




  511
  
  
    
| expr WHEN tag_ident LPAR vdecl_ident RPAR


  		




  512
  
  
    
    {mkexpr (Expr_when ($1, fst $5, $3))}


  		




  513
  
  
    
| MERGE vdecl_ident handler_expr_list


  		




  514
  
  
    
    {mkexpr (Expr_merge (fst $2,$3))}


  		




  
  460
  
    
| PRE e=expr


  		




  
  461
  
    
  { mkexpr (Expr_pre e) }


  		




  
  462
  
    
| e1=expr ARROW e2=expr


  		




  
  463
  
    
  { mkexpr (Expr_arrow (e1, e2)) }


  		




  
  464
  
    
| e1=expr FBY e2=expr


  		




  
  465
  
    
  { mkexpr (Expr_arrow (e1, mkexpr (Expr_pre e2))) }


  		




  
  466
  
    
| e=expr WHEN x=vdecl_ident


  		




  
  467
  
    
  { mkexpr (Expr_when (e, fst x, tag_true)) }


  		




  
  468
  
    
| e=expr WHENNOT x=vdecl_ident


  		




  
  469
  
    
  { mkexpr (Expr_when (e, fst x, tag_false)) }


  		




  
  470
  
    
| e=expr WHEN t=tag_ident LPAR x=vdecl_ident RPAR


  		




  
  471
  
    
  { mkexpr (Expr_when (e, fst x, t)) }


  		




  
  472
  
    
| MERGE x=vdecl_ident


  		




  
  473
  
    
  hs=delimited(LPAR, separated_pair(tag_ident, ARROW, expr), RPAR)*


  		




  
  474
  
    
  { mkexpr (Expr_merge (fst x, hs)) }


  		




  515
  475
  
    

  		




  516
  476
  
    
/* Applications */


  		




  517
  
  
    
| node_ident LPAR expr RPAR


  		




  518
  
  
    
    {mkexpr (Expr_appl ($1, $3, None))}


  		




  519
  
  
    
| node_ident LPAR expr RPAR EVERY expr


  		




  520
  
  
    
    {mkexpr (Expr_appl ($1, $3, Some $6))}


  		




  521
  
  
    
| node_ident LPAR tuple_expr RPAR


  		




  522
  
  
    
    {


  		




  523
  
  
    
      let id=$1 in


  		




  524
  
  
    
      let args=List.rev $3 in


  		




  525
  
  
    
      match id, args with


  		




  526
  
  
    
      | "fbyn", [expr;n;init] ->


  		




  527
  
  
    
	let n = match n.expr_desc with


  		




  528
  
  
    
	  | Expr_const (Const_int n) -> n


  		




  529
  
  
    
	  | _ -> assert false


  		




  530
  
  
    
	in


  		




  531
  
  
    
	fby expr n init


  		




  532
  
  
    
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))


  		




  533
  
  
    
    }


  		




  534
  
  
    
| node_ident LPAR tuple_expr RPAR EVERY expr


  		




  535
  
  
    
    {


  		




  536
  
  
    
      let id=$1 in


  		




  537
  
  
    
      let args=List.rev $3 in


  		




  538
  
  
    
      let clock=$6 in


  		




  539
  
  
    
      if id="fby" then


  		




  540
  
  
    
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)


  		




  541
  
  
    
      else


  		




  542
  
  
    
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 


  		




  543
  
  
    
    }


  		




  
  477
  
    
| f=node_ident LPAR es=expr_or_tuple RPAR r=preceded(EVERY, expr)?


  		




  
  478
  
    
  { match f, es.expr_desc, r with


  		




  
  479
  
    
    | "fbyn", Expr_tuple [expr; n; init], None ->


  		




  
  480
  
    
       let n = match n.expr_desc with


  		




  
  481
  
    
         | Expr_const (Const_int n) -> n


  		




  
  482
  
    
         | _ -> assert false


  		




  
  483
  
    
       in


  		




  
  484
  
    
       fby expr n init


  		




  
  485
  
    
    | "fbyn", _ , Some _ ->


  		




  
  486
  
    
       assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)


  		




  
  487
  
    
    | _ -> mkexpr (Expr_appl (f, es, r))


  		




  
  488
  
    
  }


  		




  544
  489
  
    

  		




  545
  490
  
    
/* Boolean expr */


  		




  546
  
  
    
| expr AND expr 


  		




  547
  
  
    
    {mkpredef_call "&&" [$1;$3]}


  		




  548
  
  
    
| expr AMPERAMPER expr 


  		




  549
  
  
    
    {mkpredef_call "&&" [$1;$3]}


  		




  550
  
  
    
| expr OR expr 


  		




  551
  
  
    
    {mkpredef_call "||" [$1;$3]}


  		




  552
  
  
    
| expr BARBAR expr 


  		




  553
  
  
    
    {mkpredef_call "||" [$1;$3]}


  		




  554
  
  
    
| expr XOR expr 


  		




  555
  
  
    
    {mkpredef_call "xor" [$1;$3]}


  		




  556
  
  
    
| NOT expr 


  		




  557
  
  
    
    {mkpredef_call "not" [$2]}


  		




  558
  
  
    
| expr IMPL expr 


  		




  559
  
  
    
    {mkpredef_call "impl" [$1;$3]}


  		




  
  491
  
    
| e1=expr AND e2=expr         { mkpredef_call_b "&&" e1 e2 }


  		




  
  492
  
    
| e1=expr AMPERAMPER e2=expr  { mkpredef_call_b "&&" e1 e2 }


  		




  
  493
  
    
| e1=expr OR e2=expr          { mkpredef_call_b "||" e1 e2 }


  		




  
  494
  
    
| e1=expr BARBAR e2=expr      { mkpredef_call_b "||" e1 e2 }


  		




  
  495
  
    
| e1=expr XOR e2=expr         { mkpredef_call_b "xor" e1 e2 }


  		




  
  496
  
    
| NOT e=expr                  { mkpredef_call_u "not" e }


  		




  
  497
  
    
| e1=expr IMPL e2=expr        { mkpredef_call_b "impl" e1 e2 }


  		




  560
  498
  
    

  		




  561
  499
  
    
/* Comparison expr */


  		




  562
  
  
    
| expr EQ expr 


  		




  563
  
  
    
    {mkpredef_call "=" [$1;$3]}


  		




  564
  
  
    
| expr LT expr 


  		




  565
  
  
    
    {mkpredef_call "<" [$1;$3]}


  		




  566
  
  
    
| expr LTE expr 


  		




  567
  
  
    
    {mkpredef_call "<=" [$1;$3]}


  		




  568
  
  
    
| expr GT expr 


  		




  569
  
  
    
    {mkpredef_call ">" [$1;$3]}


  		




  570
  
  
    
| expr GTE  expr 


  		




  571
  
  
    
    {mkpredef_call ">=" [$1;$3]}


  		




  572
  
  
    
| expr NEQ expr 


  		




  573
  
  
    
    {mkpredef_call "!=" [$1;$3]}


  		




  
  500
  
    
| e1=expr EQ e2=expr          { mkpredef_call_b "=" e1 e2 }


  		




  
  501
  
    
| e1=expr LT e2=expr          { mkpredef_call_b "<" e1 e2 }


  		




  
  502
  
    
| e1=expr LTE e2=expr         { mkpredef_call_b "<=" e1 e2 }


  		




  
  503
  
    
| e1=expr GT e2=expr          { mkpredef_call_b ">" e1 e2 }


  		




  
  504
  
    
| e1=expr GTE e2=expr         { mkpredef_call_b ">=" e1 e2 }


  		




  
  505
  
    
| e1=expr NEQ e2=expr         { mkpredef_call_b "!=" e1 e2 }


  		




  574
  506
  
    

  		




  575
  507
  
    
/* Arithmetic expr */


  		




  576
  
  
    
| expr PLUS expr 


  		




  577
  
  
    
    {mkpredef_call "+" [$1;$3]}


  		




  578
  
  
    
| expr MINUS expr 


  		




  579
  
  
    
    {mkpredef_call "-" [$1;$3]}


  		




  580
  
  
    
| expr MULT expr 


  		




  581
  
  
    
    {mkpredef_call "*" [$1;$3]}


  		




  582
  
  
    
| expr DIV expr 


  		




  583
  
  
    
    {mkpredef_call "/" [$1;$3]}


  		




  584
  
  
    
| MINUS expr %prec UMINUS


  		




  585
  
  
    
  {mkpredef_call "uminus" [$2]}


  		




  586
  
  
    
| expr MOD expr 


  		




  587
  
  
    
    {mkpredef_call "mod" [$1;$3]}


  		




  
  508
  
    
| e1=expr PLUS e2=expr        { mkpredef_call_b "+" e1 e2 }


  		




  
  509
  
    
| e1=expr MINUS e2=expr       { mkpredef_call_b "-" e1 e2 }


  		




  
  510
  
    
| e1=expr MULT e2=expr        { mkpredef_call_b "*" e1 e2 }


  		




  
  511
  
    
| e1=expr DIV e2=expr         { mkpredef_call_b "/" e1 e2 }


  		




  
  512
  
    
| MINUS e=expr %prec p_uminus { mkpredef_call_u "uminus" e }


  		




  
  513
  
    
| e1=expr MOD e2=expr         { mkpredef_call_b "mod" e1 e2 }


  		




  588
  514
  
    

  		




  589
  515
  
    
/* If */


  		




  590
  
  
    
| IF expr THEN expr ELSE expr


  		




  591
  
  
    
    {mkexpr (Expr_ite ($2, $4, $6))}


  		




  592
  
  
    

  		




  593
  
  
    
handler_expr_list:


  		




  594
  
  
    
   { [] }


  		




  595
  
  
    
| handler_expr handler_expr_list { $1 :: $2 }


  		




  596
  
  
    

  		




  597
  
  
    
handler_expr:


  		




  598
  
  
    
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }


  		




  599
  
  
    

  		




  600
  
  
    
signed_const_array:


  		




  601
  
  
    
| signed_const { [$1] }


  		




  602
  
  
    
| signed_const COMMA signed_const_array { $1 :: $3 }


  		




  603
  
  
    

  		




  604
  
  
    
signed_const_struct:


  		




  605
  
  
    
| IDENT EQ signed_const { [ ($1, $3) ] }


  		




  606
  
  
    
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }


  		




  
  516
  
    
| IF e=expr THEN t=expr ELSE f=expr { mkexpr (Expr_ite (e, t, f)) }


  		




  607
  517
  
    

  		




  608
  518
  
    
signed_const:


  		




  609
  
  
    
  INT {Const_int $1}


  		




  610
  
  
    
| REAL {Const_real $1}


  		




  611
  
  
    
/* | FLOAT {Const_float $1} */


  		




  612
  
  
    
| tag_ident {Const_tag $1}


  		




  613
  
  
    
| MINUS INT {Const_int (-1 * $2)}


  		




  614
  
  
    
| MINUS REAL {Const_real (Real.uminus $2)}


  		




  615
  
  
    
/* | MINUS FLOAT {Const_float (-1. *. $2)} */


  		




  616
  
  
    
| LCUR signed_const_struct RCUR { Const_struct $2 }


  		




  617
  
  
    
| LBRACKET signed_const_array RBRACKET { Const_array $2 }


  		




  
  519
  
    
| c=INT


  		




  
  520
  
    
  { Const_int c }


  		




  
  521
  
    
| c=REAL


  		




  
  522
  
    
  { Const_real c }


  		




  
  523
  
    
/* | c=FLOAT { Const_float c } */


  		




  
  524
  
    
| t=tag_ident { Const_tag t }


  		




  
  525
  
    
| MINUS c=INT


  		




  
  526
  
    
  { Const_int (-1 * c) }


  		




  
  527
  
    
| MINUS c=REAL


  		




  
  528
  
    
  { Const_real (Real.uminus c) }


  		




  
  529
  
    
/* | MINUS c=FLOAT { Const_float (-1. *. c) } */


  		




  
  530
  
    
| LCUR


  		




  
  531
  
    
  cs=separated_nonempty_list(COMMA, separated_pair(IDENT, EQ, signed_const))


  		




  
  532
  
    
  RCUR


  		




  
  533
  
    
  { Const_struct cs }


  		




  
  534
  
    
| LBRACKET cs=separated_nonempty_list(COMMA, signed_const) RBRACKET


  		




  
  535
  
    
  { Const_array cs }


  		




  618
  536
  
    

  		




  619
  537
  
    
dim:


  		




  620
  
  
    
   INT { mkdim_int $1 }


  		




  621
  
  
    
| LPAR dim RPAR { $2 }


  		




  622
  
  
    
| UIDENT { mkdim_ident $1 }


  		




  623
  
  
    
| IDENT { mkdim_ident $1 }


  		




  624
  
  
    
| dim AND dim 


  		




  625
  
  
    
    {mkdim_appl "&&" [$1;$3]}


  		




  626
  
  
    
| dim AMPERAMPER dim 


  		




  627
  
  
    
    {mkdim_appl "&&" [$1;$3]}


  		




  628
  
  
    
| dim OR dim 


  		




  629
  
  
    
    {mkdim_appl "||" [$1;$3]}


  		




  630
  
  
    
| dim BARBAR dim 


  		




  631
  
  
    
    {mkdim_appl "||" [$1;$3]}


  		




  632
  
  
    
| dim XOR dim 


  		




  633
  
  
    
    {mkdim_appl "xor" [$1;$3]}


  		




  634
  
  
    
| NOT dim 


  		




  635
  
  
    
    {mkdim_appl "not" [$2]}


  		




  636
  
  
    
| dim IMPL dim 


  		




  637
  
  
    
    {mkdim_appl "impl" [$1;$3]}


  		




  
  538
  
    
| i=INT                      { mkdim_int i }


  		




  
  539
  
    
| LPAR d=dim RPAR            { d }


  		




  
  540
  
    
| x=ident                    { mkdim_ident x }


  		




  
  541
  
    
| d1=dim AND d2=dim          { mkdim_appl_b "&&" d1 d2 }


  		




  
  542
  
    
| d1=dim AMPERAMPER d2=dim   { mkdim_appl_b "&&" d1 d2 }


  		




  
  543
  
    
| d1=dim OR d2=dim           { mkdim_appl_b "||" d1 d2 }


  		




  
  544
  
    
| d1=dim BARBAR d2=dim       { mkdim_appl_b "||" d1 d2 }


  		




  
  545
  
    
| d1=dim XOR d2=dim          { mkdim_appl_b "xor" d1 d2 }


  		




  
  546
  
    
| NOT d=dim                  { mkdim_appl_u "not" d }


  		




  
  547
  
    
| d1=dim IMPL d2=dim         { mkdim_appl_b "impl" d1 d2 }


  		




  638
  548
  
    

  		




  639
  549
  
    
/* Comparison dim */


  		




  640
  
  
    
| dim EQ dim 


  		




  641
  
  
    
    {mkdim_appl "=" [$1;$3]}


  		




  642
  
  
    
| dim LT dim 


  		




  643
  
  
    
    {mkdim_appl "<" [$1;$3]}


  		




  644
  
  
    
| dim LTE dim 


  		




  645
  
  
    
    {mkdim_appl "<=" [$1;$3]}


  		




  646
  
  
    
| dim GT dim 


  		




  647
  
  
    
    {mkdim_appl ">" [$1;$3]}


  		




  648
  
  
    
| dim GTE  dim 


  		




  649
  
  
    
    {mkdim_appl ">=" [$1;$3]}


  		




  650
  
  
    
| dim NEQ dim 


  		




  651
  
  
    
    {mkdim_appl "!=" [$1;$3]}


  		




  
  550
  
    
| d1=dim EQ d2=dim           { mkdim_appl_b "=" d1 d2 }


  		




  
  551
  
    
| d1=dim LT d2=dim           { mkdim_appl_b "<" d1 d2 }


  		




  
  552
  
    
| d1=dim LTE d2=dim          { mkdim_appl_b "<=" d1 d2 }


  		




  
  553
  
    
| d1=dim GT d2=dim           { mkdim_appl_b ">" d1 d2 }


  		




  
  554
  
    
| d1=dim GTE  d2=dim         { mkdim_appl_b ">=" d1 d2 }


  		




  
  555
  
    
| d1=dim NEQ d2=dim          { mkdim_appl_b "!=" d1 d2 }


  		




  652
  556
  
    

  		




  653
  557
  
    
/* Arithmetic dim */


  		




  654
  
  
    
| dim PLUS dim 


  		




  655
  
  
    
    {mkdim_appl "+" [$1;$3]}


  		




  656
  
  
    
| dim MINUS dim 


  		




  657
  
  
    
    {mkdim_appl "-" [$1;$3]}


  		




  658
  
  
    
| dim MULT dim 


  		




  659
  
  
    
    {mkdim_appl "*" [$1;$3]}


  		




  660
  
  
    
| dim DIV dim 


  		




  661
  
  
    
    {mkdim_appl "/" [$1;$3]}


  		




  662
  
  
    
| MINUS dim %prec UMINUS


  		




  663
  
  
    
  {mkdim_appl "uminus" [$2]}


  		




  664
  
  
    
| dim MOD dim 


  		




  665
  
  
    
    {mkdim_appl "mod" [$1;$3]}


  		




  
  558
  
    
| d1=dim PLUS d2=dim         { mkdim_appl_b "+" d1 d2 }


  		




  
  559
  
    
| d1=dim MINUS d2=dim        { mkdim_appl_b "-" d1 d2 }


  		




  
  560
  
    
| d1=dim MULT d2=dim         { mkdim_appl_b "*" d1 d2 }


  		




  
  561
  
    
| d1=dim DIV d2=dim          { mkdim_appl_b "/" d1 d2 }


  		




  
  562
  
    
| MINUS d=dim %prec p_uminus { mkdim_appl_u "uminus" d }


  		




  
  563
  
    
| d1=dim MOD d2=dim          { mkdim_appl_b "mod" d1 d2 }


  		




  
  564
  
    

  		




  666
  565
  
    
/* If */


  		




  667
  
  
    
| IF dim THEN dim ELSE dim


  		




  668
  
  
    
    {mkdim_ite $2 $4 $6}


  		




  
  566
  
    
| IF d=dim THEN t=dim ELSE f=dim { mkdim_ite d t f }


  		




  669
  567
  
    

  		




  670
  
  
    
locals:


  		




  671
  
  
    
  {[]}


  		




  672
  
  
    
| VAR local_vdecl_list SCOL {$2}


  		




  
  568
  
    
%inline locals:


  		




  
  569
  
    
| xs=loption(preceded(VAR, flatten(separated_nonempty_list(SCOL, local_vdecl))))


  		




  
  570
  
    
  { xs }


  		




  673
  571
  
    

  		




  674
  572
  
    
vdecl_list:


  		




  675
  
  
    
  vdecl {$1}


  		




  676
  
  
    
| vdecl_list SCOL vdecl {$3 @ $1}


  		




  
  573
  
    
| d=vdecl %prec p_vdecl { d }


  		




  
  574
  
    
| d=vdecl SCOL ds=vdecl_list { d @ ds }


  		




  677
  575
  
    

  		




  678
  576
  
    
vdecl:


  		




  679
  
  
    
  ident_list COL typeconst clock 


  		




  680
  
  
    
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }


  		




  681
  
  
    
| CONST ident_list /* static parameters don't have clocks */


  		




  682
  
  
    
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }


  		




  683
  
  
    
| CONST ident_list COL typeconst /* static parameters don't have clocks */


  		




  684
  
  
    
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }


  		




  685
  
  
    

  		




  686
  
  
    
local_vdecl_list:


  		




  687
  
  
    
  local_vdecl {$1}


  		




  688
  
  
    
| local_vdecl_list SCOL local_vdecl {$3 @ $1}


  		




  
  577
  
    
| xs=ident_list COL t=typeconst c=clock?


  		




  
  578
  
    
  { mkvdecls false (Some t) c None xs }


  		




  
  579
  
    
| CONST xs=ident_list t=preceded(COL, typeconst)?


  		




  
  580
  
    
  /* static parameters don't have clocks */


  		




  
  581
  
    
  { mkvdecls true t None None xs }


  		




  689
  582
  
    

  		




  690
  583
  
    
local_vdecl:


  		




  691
  
  
    
/* Useless no ?*/    ident_list


  		




  692
  
  
    
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }


  		




  693
  
  
    
| ident_list COL typeconst clock 


  		




  694
  
  
    
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }


  		




  695
  
  
    
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */


  		




  696
  
  
    
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }


  		




  697
  
  
    
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */


  		




  698
  
  
    
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }


  		




  699
  
  
    

  		




  700
  
  
    
cdecl_list:


  		




  701
  
  
    
  cdecl SCOL { (fun itf -> [$1 itf]) }


  		




  702
  
  
    
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }


  		




  
  584
  
    
| xs=ident_list /* Useless no ?*/


  		




  
  585
  
    
  { mkvdecls false None None None xs }


  		




  
  586
  
    
| xs=ident_list COL t=typeconst c=clock?


  		




  
  587
  
    
  { mkvdecls false (Some t) c None xs }


  		




  
  588
  
    
| CONST x=vdecl_ident t=preceded(COL, typeconst)? EQ e=expr


  		




  
  589
  
    
  /* static parameters don't have clocks */


  		




  
  590
  
    
  { mkvdecls true t None (Some e) [x] }


  		




  703
  591
  
    

  		




  704
  592
  
    
cdecl:


  		




  705
  
  
    
    const_ident EQ signed_const {


  		




  706
  
  
    
      (fun itf -> 


  		




  707
  
  
    
       let c = mktop_decl itf (Const {


  		




  708
  
  
    
				   const_id = $1;


  		




  709
  
  
    
				   const_loc = get_loc ();


  		




  710
  
  
    
				   const_type = Types.new_var ();


  		




  711
  
  
    
				   const_value = $3})


  		




  712
  
  
    
       in


  		




  713
  
  
    
       (*add_const itf $1 c;*) c)


  		




  714
  
  
    
    }


  		




  715
  
  
    

  		




  716
  
  
    
clock:


  		




  717
  
  
    
    {mkclock Ckdec_any}


  		




  718
  
  
    
| when_list


  		




  719
  
  
    
    {mkclock (Ckdec_bool (List.rev $1))}


  		




  
  593
  
    
| x=const_ident EQ c=signed_const


  		




  
  594
  
    
  { fun itf ->


  		




  
  595
  
    
    let c = mktop_decl itf (Const {


  		




  
  596
  
    
                                const_id = x;


  		




  
  597
  
    
                                const_loc = get_loc ();


  		




  
  598
  
    
                                const_type = Types.new_var ();


  		




  
  599
  
    
                                const_value = c


  		




  
  600
  
    
              })


  		




  
  601
  
    
    in


  		




  
  602
  
    
    (*add_const itf $1 c;*)


  		




  
  603
  
    
    c


  		




  
  604
  
    
  }


  		




  
  605
  
    

  		




  
  606
  
    
%inline clock:


  		




  
  607
  
    
| l=when_cond+ { mkclock (Ckdec_bool l) }


  		




  720
  608
  
    

  		




  721
  609
  
    
when_cond:


  		




  722
  
  
    
  WHEN IDENT {($2, tag_true)}


  		




  723
  
  
    
| WHENNOT IDENT {($2, tag_false)}


  		




  724
  
  
    
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}


  		




  725
  
  
    

  		




  726
  
  
    
when_list:


  		




  727
  
  
    
    when_cond {[$1]}


  		




  728
  
  
    
| when_list when_cond {$2::$1}


  		




  729
  
  
    

  		




  730
  
  
    
ident_list:


  		




  731
  
  
    
  vdecl_ident {[$1]}


  		




  732
  
  
    
| ident_list COMMA vdecl_ident {$3::$1}


  		




  733
  
  
    

  		




  734
  
  
    
SCOL_opt:


  		




  735
  
  
    
    SCOL {} | {}


  		




  
  610
  
    
| WHEN x=IDENT                       { x, tag_true }


  		




  
  611
  
    
| WHENNOT x=IDENT                    { x, tag_false }


  		




  
  612
  
    
| WHEN t=tag_ident LPAR x=IDENT RPAR { x, t }


  		




  736
  613
  
    

  		




  
  614
  
    
%inline ident_list:


  		




  
  615
  
    
| ds=separated_nonempty_list(COMMA, vdecl_ident) { ds }


  		




  737
  616
  
    

  		




  738
  617
  
    
lustre_annot:


  		




  739
  
  
    
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }


  		




  
  618
  
    
| lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }


  		




  740
  619
  
    

  		




  741
  620
  
    
lustre_annot_list:


  		




  742
  621
  
    
  { [] } 


  		












Also available in:  Unified diff