Project

General

Profile

Revision 7231d0e4 src/normalization.ml

View differences:

src/normalization.ml
266 266
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
267 267
  defvars', {eq with eq_lhs = lhs' }
268 268

  
269
let rec normalize_eq node defvars eq = 
269
let rec normalize_eq spec node defvars eq = 
270 270
  match eq.eq_rhs.expr_desc with
271
  | Expr_pre _
271
  | Expr_pre _ ->
272
    let (defvars', eq') = decouple_outputs node defvars eq in
273
    let eq_rhs = if spec then
274
      let expr = Corelang.mkexpr eq'.eq_rhs.expr_loc (Expr_pre eq'.eq_rhs) in
275
      expr.expr_type <- eq'.eq_rhs.expr_type; expr
276
    else eq'.eq_rhs in
277
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq_rhs in
278
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
279
    (norm_eq::defs', vars')
272 280
  | Expr_fby _  ->
273 281
    let (defvars', eq') = decouple_outputs node defvars eq in
274
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
282
    let eq_rhs = eq'.eq_rhs in (*TODO: Must be like in pre ??? *)
283
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq_rhs in
275 284
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
276 285
    (norm_eq::defs', vars')
277 286
  | Expr_array _ ->
......
291 300
    let norm_eq = { eq with eq_rhs = norm_rhs } in
292 301
    norm_eq::defs', vars'
293 302

  
294
let normalize_eq_split node defvars eq =
295
  let defs, vars = normalize_eq node defvars eq in
303
let normalize_eq_split spec node defvars eq =
304
  let defs, vars = normalize_eq spec node defvars eq in
296 305
  List.fold_right (fun eq (def, vars) -> 
297 306
    let eq_defs = Splitting.tuple_split_eq eq in
298 307
    if eq_defs = [eq] then
299 308
      eq::def, vars 
300 309
    else
301
      List.fold_left (normalize_eq node) (def, vars) eq_defs
310
      List.fold_left (normalize_eq spec node) (def, vars) eq_defs
302 311
  ) defs ([], vars)  
303 312

  
304 313
let normalize_eexpr decls node vars ee =
......
324 333
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
325 334
  let defs, vars = 
326 335
    if calls = [] && not (eq_has_arrows eq) then
327
      normalize_eq_split node ([], vars) eq     
336
      normalize_eq_split true node ([], vars) eq     
328 337
    else (
329 338
      let locals = 
330 339
	node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
331 340
      let new_locals, eqs = Inliner.inline_eq ~arrows:true eq locals calls in
332 341
      
333 342
    (* Normalizing expr and eqs *)
334
      List.fold_left (normalize_eq_split node) ([], vars@new_locals) eqs 
343
      List.fold_left (normalize_eq_split true node) ([], vars@new_locals) eqs 
335 344
    )
336 345
  in
337 346
  
......
363 372
  let is_local v =
364 373
    List.for_all ((<>) v) inputs_outputs in
365 374
  let defs, vars = 
366
    List.fold_left (normalize_eq_split node) ([], inputs_outputs@node.node_locals) node.node_eqs in
375
    List.fold_left (normalize_eq_split false node) ([], inputs_outputs@node.node_locals) node.node_eqs in
367 376

  
368 377
  (* Update mutable fields of eexpr to perform normalization of specification/annotations *)
369 378
  List.iter (fun a -> List.iter (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann) a.annots)

Also available in: Unified diff