Project

General

Profile

Revision 57392da1

View differences:

src/lexer_lustre.mll
68 68
(* Buffer for parsing specification/annotation *)
69 69
let buf = Buffer.create 1024
70 70

  
71
let make_annot lexbuf s =
71
let make_annot lexbuf s = 
72 72
  try
73 73
    let ann = LexerLustreSpec.annot s in
74 74
    ANNOT ann
75 75
  with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift (Location.curr lexbuf) loc, Parse.Annot_error s))
76 76

  
77
let make_spec lexbuf s =
77
let make_spec lexbuf s = 
78 78
  try
79 79
    let ns = LexerLustreSpec.spec s in
80 80
    NODESPEC ns
81 81
  with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift (Location.curr lexbuf) loc, Parse.Node_spec_error s))
82 82

  
83

  
84
let make_kind_spec lexbuf s =
85
  try
86
    let s_lexbuf = Lexing.from_string s in
87
    (*Format.printf "KIND SPEC \"%s\"@." s;*)
88
    let contract = KindLustreParser.contract_in_block_main KindLustreLexer.token s_lexbuf in
89
    let dummy_ns = { Lustre_types.requires = []; ensures = []; behaviors = []; spec_loc = Location.dummy_loc} in
90
    begin
91
      List.iter (fun item ->
92
      		Format.eprintf "CONTRACT: %a@." KindLustreAst.pp_print_contract_item item) contract;
93
      NODESPEC dummy_ns
94
    end
95
  with exn -> ((*Printexc.print_backtrace stderr; *) raise exn)
96

  
97
(*let make_spec = make_kind_spec*)
83
}
98 84

  
99 85
let newline = ('\010' | '\013' | "\013\010")
100 86
let notnewline = [^ '\010' '\013']
......
103 89
rule token = parse
104 90
| "--@" { Buffer.clear buf;
105 91
	  spec_singleline lexbuf }
106
| "(*@" { Buffer.clear buf;
92
| "(*@" { Buffer.clear buf; 
107 93
	  spec_multiline 0 lexbuf }
108
| "--!" { Buffer.clear buf;
94
| "--!" { Buffer.clear buf; 
109 95
	  annot_singleline lexbuf }
110
| "(*!" { Buffer.clear buf;
96
| "(*!" { Buffer.clear buf; 
111 97
	  annot_multiline 0 lexbuf }
112 98
| "(*"
113 99
    { comment 0 lexbuf }
......
123 109
    {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp , s)}
124 110
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s
125 111
    {REAL (Num.num_of_string (l^r), String.length r, s)}
126
| ['0'-'9']+
112
| ['0'-'9']+ 
127 113
    {INT (int_of_string (Lexing.lexeme lexbuf)) }
128 114
| "tel." {TEL}
129 115
| "tel;" {TEL}
......
191 177

  
192 178
and annot_multiline n = parse
193 179
  | eof { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_annot)) }
194
  | "*)" as s {
195
    if n > 0 then
196
      (Buffer.add_string buf s; annot_multiline (n-1) lexbuf)
197
    else
180
  | "*)" as s { 
181
    if n > 0 then 
182
      (Buffer.add_string buf s; annot_multiline (n-1) lexbuf) 
183
    else 
198 184
      make_annot lexbuf (Buffer.contents buf) }
199 185
  | "(*" as s { Buffer.add_string buf s; annot_multiline (n+1) lexbuf }
200 186
  | newline as s { incr_line lexbuf; Buffer.add_string buf s; annot_multiline n lexbuf }
......
207 193

  
208 194
and spec_multiline n = parse
209 195
  | eof { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_node_spec)) }
210
  | "*)" as s { if n > 0 then
211
      (Buffer.add_string buf s; spec_multiline (n-1) lexbuf)
212
    else
196
  | "*)" as s { if n > 0 then 
197
      (Buffer.add_string buf s; spec_multiline (n-1) lexbuf) 
198
    else 
213 199
      make_spec lexbuf (Buffer.contents buf) }
214 200
  | "(*" as s { Buffer.add_string buf s; spec_multiline (n+1) lexbuf }
215 201
  | newline as s { incr_line lexbuf; Buffer.add_string buf s; spec_multiline n lexbuf }
216 202
  | _ as c { Buffer.add_char buf c; spec_multiline n lexbuf }
203

  

Also available in: Unified diff