Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/corelang.ml
495 495

  
496 496
let rename_node f_node f_var f_const nd =
497 497
  let rename_var v = { v with var_id = f_var v.var_id } in
498
  let rename_eq eq = { eq with
499
      eq_lhs = List.map f_var eq.eq_lhs; 
500
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
501
    } 
502
  in
498 503
  let inputs = List.map rename_var nd.node_inputs in
499 504
  let outputs = List.map rename_var nd.node_outputs in
500 505
  let locals = List.map rename_var nd.node_locals in
......
502 507
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
503 508
  let node_asserts = List.map 
504 509
    (fun a -> 
505
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
506
    ) nd.node_asserts
507
  in
508
  let eqs = List.map 
509
    (fun eq -> { eq with
510
      eq_lhs = List.map f_var eq.eq_lhs; 
511
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
512
    } ) nd.node_eqs
510
      {a with assert_expr = 
511
	  let expr = a.assert_expr in
512
	  rename_expr f_node f_var f_const expr})
513
    nd.node_asserts
513 514
  in
515
  let eqs = List.map rename_eq nd.node_eqs in
514 516
  let spec = 
515 517
    Utils.option_map 
516 518
      (fun s -> rename_node_annot f_node f_var f_const s) 
......
643 645
    Basic_library.internal_funs
644 646

  
645 647

  
648

  
649
(* Replace any occurence of a var in vars_to_replace by its associated
650
   expression in defs until e does not contain any such variables *)
651
let rec substitute_expr vars_to_replace defs e =
652
  let se = substitute_expr vars_to_replace defs in
653
  { e with expr_desc = 
654
      let ed = e.expr_desc in
655
      match ed with
656
      | Expr_const _ -> ed
657
      | Expr_array el -> Expr_array (List.map se el)
658
      | Expr_access (e1, d) -> Expr_access (se e1, d)
659
      | Expr_power (e1, d) -> Expr_power (se e1, d)
660
      | Expr_tuple el -> Expr_tuple (List.map se el)
661
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
662
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
663
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
664
      | Expr_pre e' -> Expr_pre (se e')
665
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
666
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
667
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
668
      | Expr_ident i -> 
669
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
670
	  let eq_i eq = eq.eq_lhs = [i] in
671
	  if List.exists eq_i defs then
672
	    let sub = List.find eq_i defs in
673
	    let sub' = se sub.eq_rhs in
674
	    sub'.expr_desc
675
	  else 
676
	    assert false
677
	)
678
	else
679
	  ed
680

  
681
  }
682
(* FAUT IL RETIRER ?
683
  
684
 let rec expr_to_eexpr  expr =
685
   { eexpr_tag = expr.expr_tag;
686
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
687
     eexpr_type = expr.expr_type;
688
     eexpr_clock = expr.expr_clock;
689
     eexpr_loc = expr.expr_loc
690
   }
691
 and expr_desc_to_eexpr_desc expr_desc =
692
   let conv = expr_to_eexpr in
693
   match expr_desc with
694
   | Expr_const c -> EExpr_const (match c with
695
     | Const_int x -> EConst_int x 
696
     | Const_real x -> EConst_real x 
697
     | Const_float x -> EConst_float x 
698
     | Const_tag x -> EConst_tag x 
699
     | _ -> assert false
700

  
701
   )
702
   | Expr_ident i -> EExpr_ident i
703
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
704

  
705
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
706
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
707
   | Expr_pre e' -> EExpr_pre (conv e')
708
   | Expr_appl (i, e', i') -> 
709
     EExpr_appl 
710
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
711

  
712
   | Expr_when _
713
   | Expr_merge _ -> assert false
714
   | Expr_array _ 
715
   | Expr_access _ 
716
   | Expr_power _  -> assert false
717
   | Expr_ite (c, t, e) -> assert false 
718
   | _ -> assert false
719

  
720
     *)
646 721
let rec get_expr_calls nodes e =
647 722
  get_calls_expr_desc nodes e.expr_desc
648 723
and get_calls_expr_desc nodes expr_desc =

Also available in: Unified diff