Project

General

Profile

Revision bc504848 src/cocospec/kindLustreParser.mly

View differences:

src/cocospec/kindLustreParser.mly
214 214
(* Start token *)
215 215
%start <KindLustreAst.t> main
216 216
%start <KindLustreAst.expr> one_expr
217
%start <KindLustreAst.contract> contract_in_block
217
%start <KindLustreAst.contract> contract_in_block_main
218 218
%%
219 219
(** Parser for lustre systems. *)
220 220

  
......
450 450

  
451 451

  
452 452
contract_item:
453
  | v = contract_ghost_var { v } 
454
  | c = contract_ghost_const { c }
455
  | a = contract_assume { a }
456
  | g = contract_guarantee { g }
453
  | v = contract_ghost_var { (*Format.printf "CONTRACT_ITEM (v)@.";*) v } 
454
  | c = contract_ghost_const { (*Format.printf "CONTRACT_ITEM (c)@.";*) c }
455
  | a = contract_assume { (*Format.printf "CONTRACT_ITEM (a)@.";*) a }
456
  | g = contract_guarantee { (*Format.printf "CONTRACT_ITEM (g)@.";*) g }
457 457
  | m = mode_equation { m }
458 458
  | i = contract_import { i }
459 459

  
460
contract_in_block_main:
461
  | c = contract_in_block ; EOF { c }
462

  
460 463
contract_in_block:
461 464
  | c = nonempty_list(contract_item) { c }
462 465

  

Also available in: Unified diff