Revision 333e3a25
Added by PierreLoïc Garoche over 5 years ago
src/corelang.ml  

130  130 
match top_decl.top_decl_desc with 
131  131 
 TypeDef tdef > 
132  132 
(match tdef.tydef_desc with 
133 
 Tydec_enum tags > List.map (fun tag > let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags 

133 
 Tydec_enum tags > 

134 
List.map 

135 
(fun tag > 

136 
let cdecl = { 

137 
const_id = tag; 

138 
const_loc = top_decl.top_decl_loc; 

139 
const_value = Const_tag tag; 

140 
const_type = Type_predef.type_const tdef.tydef_id 

141 
} in 

142 
{ top_decl with top_decl_desc = Const cdecl }) 

143 
tags 

134  144 
 _ > []) 
135  145 
 _ > assert false 
136  146  
...  ...  
538  548 
(* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *) 
539  549 
raise Not_found 
540  550 
end 
541 


551  
552  
542  553 
let get_node_eqs = 
543  554 
let get_eqs stmts = 
544  555 
List.fold_right 
545 
(fun stmt res >


556 
(fun stmt (res_eq, res_aut) >


546  557 
match stmt with 
547 
 Eq eq > eq :: res 

548 
 Aut _ > assert false)


558 
 Eq eq > eq :: res_eq, res_aut


559 
 Aut aut > res_eq, aut::res_aut)


549  560 
stmts 
550 
[] in


561 
([], []) in


551  562 
let table_eqs = Hashtbl.create 23 in 
552  563 
(fun nd > 
553  564 
try 
...  ...  
561  572 
end) 
562  573  
563  574 
let get_node_eq id node = 
564 
List.find (fun eq > List.mem id eq.eq_lhs) (get_node_eqs node) 

565  
575 
let eqs, auts = get_node_eqs node in 

576 
try 

577 
List.find (fun eq > List.mem id eq.eq_lhs) eqs 

578 
with 

579 
Not_found > (* Shall be defined in automata auts *) raise Not_found 

580 


566  581 
let get_nodes prog = 
567  582 
List.fold_left ( 
568  583 
fun nodes decl > 
...  ...  
630  645 
 Ckdec_bool cl > Ckdec_bool (List.map (fun (c, l) > rename c, l) cl) 
631  646 
 _ > cck 
632  647  
633 
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) 

648 
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)


634  649  
635  650 
(* applies the renaming function [fvar] to all variables of expression [expr] *) 
636 
let rec expr_replace_var fvar expr = 

637 
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } 

638  
639 
and expr_desc_replace_var fvar expr_desc = 

640 
match expr_desc with 

641 
 Expr_const _ > expr_desc 

642 
 Expr_ident i > Expr_ident (fvar i) 

643 
 Expr_array el > Expr_array (List.map (expr_replace_var fvar) el) 

644 
 Expr_access (e1, d) > Expr_access (expr_replace_var fvar e1, d) 

645 
 Expr_power (e1, d) > Expr_power (expr_replace_var fvar e1, d) 

646 
 Expr_tuple el > Expr_tuple (List.map (expr_replace_var fvar) el) 

647 
 Expr_ite (c, t, e) > Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) 

648 
 Expr_arrow (e1, e2)> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 

649 
 Expr_fby (e1, e2) > Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) 

650 
 Expr_pre e' > Expr_pre (expr_replace_var fvar e') 

651 
 Expr_when (e', i, l)> Expr_when (expr_replace_var fvar e', fvar i, l) 

652 
 Expr_merge (i, hl) > Expr_merge (fvar i, List.map (fun (t, h) > (t, expr_replace_var fvar h)) hl) 

653 
 Expr_appl (i, e', i') > Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') 

654  
655 
(* Applies the renaming function [fvar] to every rhs 

656 
only when the corresponding lhs satisfies predicate [pvar] *) 

657 
let eq_replace_rhs_var pvar fvar eq = 

658 
let pvar l = List.exists pvar l in 

659 
let rec replace lhs rhs = 

660 
{ rhs with expr_desc = 

661 
match lhs with 

662 
 [] > assert false 

663 
 [_] > if pvar lhs then expr_desc_replace_var fvar rhs.expr_desc else rhs.expr_desc 

664 
 _ > 

665 
(match rhs.expr_desc with 

666 
 Expr_tuple tl > 

667 
Expr_tuple (List.map2 (fun v e > replace [v] e) lhs tl) 

668 
 Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs > 

669 
let args = expr_list_of_expr arg in 

670 
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) 

671 
 Expr_array _ 

672 
 Expr_access _ 

673 
 Expr_power _ 

674 
 Expr_const _ 

675 
 Expr_ident _ 

676 
 Expr_appl _ > 

677 
if pvar lhs 

678 
then expr_desc_replace_var fvar rhs.expr_desc 

679 
else rhs.expr_desc 

680 
 Expr_ite (c, t, e) > Expr_ite (replace lhs c, replace lhs t, replace lhs e) 

681 
 Expr_arrow (e1, e2) > Expr_arrow (replace lhs e1, replace lhs e2) 

682 
 Expr_fby (e1, e2) > Expr_fby (replace lhs e1, replace lhs e2) 

683 
 Expr_pre e' > Expr_pre (replace lhs e') 

684 
 Expr_when (e', i, l) > let i' = if pvar lhs then fvar i else i 

685 
in Expr_when (replace lhs e', i', l) 

686 
 Expr_merge (i, hl) > let i' = if pvar lhs then fvar i else i 

687 
in Expr_merge (i', List.map (fun (t, h) > (t, replace lhs h)) hl) 

688 
) 

689 
} 

690 
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } 

651 
(* let rec expr_replace_var fvar expr = *) 

652 
(* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *) 

691  653  
692  
693 
let rec rename_expr f_node f_var f_const expr = 

694 
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } 

695 
and rename_expr_desc f_node f_var f_const expr_desc = 

696 
let re = rename_expr f_node f_var f_const in 

654 
(* and expr_desc_replace_var fvar expr_desc = *) 

655 
(* match expr_desc with *) 

656 
(*  Expr_const _ > expr_desc *) 

657 
(*  Expr_ident i > Expr_ident (fvar i) *) 

658 
(*  Expr_array el > Expr_array (List.map (expr_replace_var fvar) el) *) 

659 
(*  Expr_access (e1, d) > Expr_access (expr_replace_var fvar e1, d) *) 

660 
(*  Expr_power (e1, d) > Expr_power (expr_replace_var fvar e1, d) *) 

661 
(*  Expr_tuple el > Expr_tuple (List.map (expr_replace_var fvar) el) *) 

662 
(*  Expr_ite (c, t, e) > Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *) 

663 
(*  Expr_arrow (e1, e2)> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) *) 

664 
(*  Expr_fby (e1, e2) > Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *) 

665 
(*  Expr_pre e' > Expr_pre (expr_replace_var fvar e') *) 

666 
(*  Expr_when (e', i, l)> Expr_when (expr_replace_var fvar e', fvar i, l) *) 

667 
(*  Expr_merge (i, hl) > Expr_merge (fvar i, List.map (fun (t, h) > (t, expr_replace_var fvar h)) hl) *) 

668 
(*  Expr_appl (i, e', i') > Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *) 

669  
670  
671  
672 
let rec rename_expr f_node f_var expr = 

673 
{ expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc } 

674 
and rename_expr_desc f_node f_var expr_desc = 

675 
let re = rename_expr f_node f_var in 

697  676 
match expr_desc with 
698  677 
 Expr_const _ > expr_desc 
699  678 
 Expr_ident i > Expr_ident (f_var i) 
...  ...  
710  689 
Expr_merge (f_var i, List.map (fun (t, h) > (t, re h)) hl) 
711  690 
 Expr_appl (i, e', i') > 
712  691 
Expr_appl (f_node i, re e', Utils.option_map re i') 
713 


714 
let rename_node_annot f_node f_var f_const expr = 

715 
expr 

716 
(* TODO assert false *) 

717  
718 
let rename_expr_annot f_node f_var f_const annot = 

719 
annot 

720 
(* TODO assert false *) 

721  
722 
let rename_node f_node f_var f_const nd = 

723 
let rename_var v = { v with var_id = f_var v.var_id } in 

724 
let rename_eq eq = { eq with 

725 
eq_lhs = List.map f_var eq.eq_lhs; 

726 
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs 

727 
} 

728 
in 

729 
let inputs = List.map rename_var nd.node_inputs in 

730 
let outputs = List.map rename_var nd.node_outputs in 

731 
let locals = List.map rename_var nd.node_locals in 

732 
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in 

733 
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in 

734 
let node_asserts = List.map 

735 
(fun a > 

736 
{a with assert_expr = 

737 
let expr = a.assert_expr in 

738 
rename_expr f_node f_var f_const expr}) 

739 
nd.node_asserts 

740 
in 

741 
let node_stmts = List.map (fun eq > Eq (rename_eq eq)) (get_node_eqs nd) in 

742 
let spec = 

743 
Utils.option_map 

744 
(fun s > rename_node_annot f_node f_var f_const s) 

745 
nd.node_spec 

746 
in 

747 
let annot = 

748 
List.map 

749 
(fun s > rename_expr_annot f_node f_var f_const s) 

750 
nd.node_annot 

751 
in 

752 
{ 

753 
node_id = f_node nd.node_id; 

754 
node_type = nd.node_type; 

755 
node_clock = nd.node_clock; 

756 
node_inputs = inputs; 

757 
node_outputs = outputs; 

758 
node_locals = locals; 

759 
node_gencalls = gen_calls; 

760 
node_checks = node_checks; 

761 
node_asserts = node_asserts; 

762 
node_stmts = node_stmts; 

763 
node_dec_stateless = nd.node_dec_stateless; 

764 
node_stateless = nd.node_stateless; 

765 
node_spec = spec; 

766 
node_annot = annot; 

767 
} 

692  
693 
let rename_dec_type f_node f_var t = assert false (* 

694 
Types.rename_dim_type (Dimension.rename f_node f_var) t*) 

695  
696 
let rename_dec_clock f_node f_var c = assert false (* 

697 
Clocks.rename_clock_expr f_var c*) 

698 


699 
let rename_var f_node f_var v = { 

700 
v with 

701 
var_id = f_var v.var_id; 

702 
var_dec_type = rename_dec_type f_node f_var v.var_type; 

703 
var_dec_clock = rename_dec_clock f_node f_var v.var_clock 

704 
} 

705  
706 
let rename_vars f_node f_var = List.map (rename_var f_node f_var) 

707  
708 
let rec rename_eq f_node f_var eq = { eq with 

709 
eq_lhs = List.map f_var eq.eq_lhs; 

710 
eq_rhs = rename_expr f_node f_var eq.eq_rhs 

711 
} 

712 
and rename_handler f_node f_var h = {h with 

713 
hand_state = f_var h.hand_state; 

714 
hand_unless = List.map ( 

715 
fun (l,e,b,id) > l, rename_expr f_node f_var e, b, f_var id 

716 
) h.hand_unless; 

717 
hand_until = List.map ( 

718 
fun (l,e,b,id) > l, rename_expr f_node f_var e, b, f_var id 

719 
) h.hand_until; 

720 
hand_locals = rename_vars f_node f_var h.hand_locals; 

721 
hand_stmts = rename_stmts f_node f_var h.hand_stmts; 

722 
hand_annots = rename_annots f_node f_var h.hand_annots; 

723 


724 
} 

725 
and rename_aut f_node f_var aut = { aut with 

726 
aut_id = f_var aut.aut_id; 

727 
aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers; 

728 
} 

729 
and rename_stmts f_node f_var stmts = List.map (fun stmt > match stmt with 

730 
 Eq eq > Eq (rename_eq f_node f_var eq) 

731 
 Aut at > Aut (rename_aut f_node f_var at)) 

732 
stmts 

733 
and rename_annotl f_node f_var annots = 

734 
List.map 

735 
(fun (key, value) > key, rename_eexpr f_node f_var value) 

736 
annots 

737 
and rename_annot f_node f_var annot = 

738 
{ annot with annots = rename_annotl f_node f_var annot.annots } 

739 
and rename_annots f_node f_var annots = 

740 
List.map (rename_annot f_node f_var) annots 

741 
and rename_eexpr f_node f_var ee = 

742 
{ ee with 

743 
eexpr_tag = Utils.new_tag (); 

744 
eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr; 

745 
eexpr_quantifiers = List.map (fun (typ,vdecls) > typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers; 

746 
eexpr_normalized = Utils.option_map 

747 
(fun (vdecl, eqs, vdecls) > 

748 
rename_var f_node f_var vdecl, 

749 
List.map (rename_eq f_node f_var) eqs, 

750 
rename_vars f_node f_var vdecls 

751 
) ee.eexpr_normalized; 

752 


753 
} 

754 


755 


756 


757 


758 
let rename_node f_node f_var nd = 

759 
let rename_var = rename_var f_node f_var in 

760 
let rename_expr = rename_expr f_node f_var in 

761 
let rename_stmts = rename_stmts f_node f_var in 

762 
let inputs = List.map rename_var nd.node_inputs in 

763 
let outputs = List.map rename_var nd.node_outputs in 

764 
let locals = List.map rename_var nd.node_locals in 

765 
let gen_calls = List.map rename_expr nd.node_gencalls in 

766 
let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in 

767 
let node_asserts = List.map 

768 
(fun a > 

769 
{a with assert_expr = 

770 
let expr = a.assert_expr in 

771 
rename_expr expr}) 

772 
nd.node_asserts 

773 
in 

774 
let node_stmts = rename_stmts nd.node_stmts 

775  
776 


777 
in 

778 
let spec = 

779 
Utils.option_map 

780 
(fun s > assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *) 

781 
nd.node_spec 

782 
in 

783 
let annot = rename_annots f_node f_var nd.node_annot in 

784 
{ 

785 
node_id = f_node nd.node_id; 

786 
node_type = nd.node_type; 

787 
node_clock = nd.node_clock; 

788 
node_inputs = inputs; 

789 
node_outputs = outputs; 

790 
node_locals = locals; 

791 
node_gencalls = gen_calls; 

792 
node_checks = node_checks; 

793 
node_asserts = node_asserts; 

794 
node_stmts = node_stmts; 

795 
node_dec_stateless = nd.node_dec_stateless; 

796 
node_stateless = nd.node_stateless; 

797 
node_spec = spec; 

798 
node_annot = annot; 

799 
} 

768  800  
769  801  
770  802 
let rename_const f_const c = 
...  ...  
780  812 
List.fold_left (fun accu top > 
781  813 
(match top.top_decl_desc with 
782  814 
 Node nd > 
783 
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }


815 
{ top with top_decl_desc = Node (rename_node f_node f_var nd) } 

784  816 
 Const c > 
785  817 
{ top with top_decl_desc = Const (rename_const f_const c) } 
786  818 
 TypeDef tdef > 
...  ...  
791  823 
) [] prog 
792  824 
) 
793  825  
826 
(* Applies the renaming function [fvar] to every rhs 

827 
only when the corresponding lhs satisfies predicate [pvar] *) 

828 
let eq_replace_rhs_var pvar fvar eq = 

829 
let pvar l = List.exists pvar l in 

830 
let rec replace lhs rhs = 

831 
{ rhs with expr_desc = 

832 
match lhs with 

833 
 [] > assert false 

834 
 [_] > if pvar lhs then rename_expr_desc (fun x > x) fvar rhs.expr_desc else rhs.expr_desc 

835 
 _ > 

836 
(match rhs.expr_desc with 

837 
 Expr_tuple tl > 

838 
Expr_tuple (List.map2 (fun v e > replace [v] e) lhs tl) 

839 
 Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs > 

840 
let args = expr_list_of_expr arg in 

841 
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) 

842 
 Expr_array _ 

843 
 Expr_access _ 

844 
 Expr_power _ 

845 
 Expr_const _ 

846 
 Expr_ident _ 

847 
 Expr_appl _ > 

848 
if pvar lhs 

849 
then rename_expr_desc (fun x > x) fvar rhs.expr_desc 

850 
else rhs.expr_desc 

851 
 Expr_ite (c, t, e) > Expr_ite (replace lhs c, replace lhs t, replace lhs e) 

852 
 Expr_arrow (e1, e2) > Expr_arrow (replace lhs e1, replace lhs e2) 

853 
 Expr_fby (e1, e2) > Expr_fby (replace lhs e1, replace lhs e2) 

854 
 Expr_pre e' > Expr_pre (replace lhs e') 

855 
 Expr_when (e', i, l) > let i' = if pvar lhs then fvar i else i 

856 
in Expr_when (replace lhs e', i', l) 

857 
 Expr_merge (i, hl) > let i' = if pvar lhs then fvar i else i 

858 
in Expr_merge (i', List.map (fun (t, h) > (t, replace lhs h)) hl) 

859 
) 

860 
} 

861 
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } 

862  
863 


794  864 
(**********************************************************************) 
795  865 
(* Pretty printers *) 
796  866  
...  ...  
964  1034  
965  1035 
and get_eq_calls nodes eq = 
966  1036 
get_expr_calls nodes eq.eq_rhs 
1037 
and get_aut_handler_calls nodes h = 

1038 
List.fold_left (fun accu stmt > match stmt with 

1039 
 Eq eq > Utils.ISet.union (get_eq_calls nodes eq) accu 

1040 
 Aut aut' > Utils.ISet.union (get_aut_calls nodes aut') accu 

1041 
) Utils.ISet.empty h.hand_stmts 

1042 
and get_aut_calls nodes aut = 

1043 
List.fold_left (fun accu h > Utils.ISet.union (get_aut_handler_calls nodes h) accu) 

1044 
Utils.ISet.empty aut.aut_handlers 

967  1045 
and get_node_calls nodes node = 
968 
List.fold_left (fun accu eq > Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node) 

1046 
let eqs, auts = get_node_eqs node in 

1047 
let aut_calls = 

1048 
List.fold_left 

1049 
(fun accu aut > Utils.ISet.union (get_aut_calls nodes aut) accu) 

1050 
Utils.ISet.empty auts 

1051 
in 

1052 
List.fold_left 

1053 
(fun accu eq > Utils.ISet.union (get_eq_calls nodes eq) accu) 

1054 
aut_calls eqs 

969  1055  
970  1056 
let get_expr_vars e = 
971  1057 
let rec get_expr_vars vars e = 
...  ...  
1010  1096  
1011  1097 
and eq_has_arrows eq = 
1012  1098 
expr_has_arrows eq.eq_rhs 
1099 
and aut_has_arrows aut = List.exists (fun h > List.exists (fun stmt > match stmt with Eq eq > eq_has_arrows eq  Aut aut' > aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers 

1013  1100 
and node_has_arrows node = 
1014 
List.exists (fun eq > eq_has_arrows eq) (get_node_eqs node) 

1101 
let eqs, auts = get_node_eqs node in 

1102 
List.exists (fun eq > eq_has_arrows eq) eqs  List.exists (fun aut > aut_has_arrows aut) auts 

1103  
1015  1104  
1016  1105  
1017  1106 
let copy_var_decl vdecl = 
Also available in: Unified diff
[general] Refactor get_node_eqs to produce (eqs, auts) with automatons