Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
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
Merged horn_traces branch