Project

General

Profile

Revision bc504848

View differences:

src/cocospec/kindLustreLexer.mll
485 485

  
486 486
  (* Keyword *)
487 487
  | id as p {
488
    (*Format.printf "seeking symbol '%s' @." p;*)
488 489
    try Hashtbl.find keyword_table p with Not_found -> (SYM p)
489 490
  }
490 491

  
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

  
src/lexer_lustre.mll
85 85

  
86 86

  
87 87
let make_kind_spec lexbuf s =
88
  try 
88 89
    let s_lexbuf = Lexing.from_string s in
89
    let _ = KindLustreParser.contract_in_block KindLustreLexer.token s_lexbuf in
90
    (*Format.printf "KIND SPEC \"%s\"@." s;*)
91
    let _ = KindLustreParser.contract_in_block_main KindLustreLexer.token s_lexbuf in
90 92
    let dummy_ns = { Lustre_types.requires = []; ensures = []; behaviors = []; spec_loc = Location.dummy_loc} in
91 93
    NODESPEC dummy_ns
94
  with exn -> ((*Printexc.print_backtrace stderr; *) raise exn)
92 95

  
93 96
let make_spec = make_kind_spec
94 97
}

Also available in: Unified diff