Revision 01d48bb0 src/corelang.ml
src/corelang.ml | ||
---|---|---|
41 | 41 |
let mkclock loc d = |
42 | 42 |
{ ck_dec_desc = d; ck_dec_loc = loc } |
43 | 43 |
|
44 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const) = |
|
44 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) = |
|
45 |
assert (value = None || is_const); |
|
45 | 46 |
{ var_id = id; |
46 | 47 |
var_orig = orig; |
47 | 48 |
var_dec_type = ty_dec; |
48 | 49 |
var_dec_clock = ck_dec; |
49 | 50 |
var_dec_const = is_const; |
51 |
var_dec_value = value; |
|
50 | 52 |
var_type = Types.new_var (); |
51 | 53 |
var_clock = Clocks.new_var true; |
52 | 54 |
var_loc = loc } |
... | ... | |
66 | 68 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
67 | 69 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
68 | 70 |
var_dec_const = true; |
71 |
var_dec_value = None; |
|
69 | 72 |
var_type = c.const_type; |
70 | 73 |
var_clock = Clocks.new_var false; |
71 | 74 |
var_loc = c.const_loc } |
... | ... | |
93 | 96 |
let mkpredef_call loc funname args = |
94 | 97 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
95 | 98 |
|
99 |
let is_clock_dec_type cty = |
|
100 |
match cty with |
|
101 |
| Tydec_clock _ -> true |
|
102 |
| _ -> false |
|
96 | 103 |
|
97 | 104 |
let const_of_top top_decl = |
98 | 105 |
match top_decl.top_decl_desc with |
... | ... | |
578 | 585 |
(************************************************************************) |
579 | 586 |
(* Renaming *) |
580 | 587 |
|
588 |
let rec rename_static rename cty = |
|
589 |
match cty with |
|
590 |
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
|
591 |
| Tydec_clock cty -> Tydec_clock (rename_static rename cty) |
|
592 |
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
|
593 |
| _ -> cty |
|
594 |
|
|
595 |
let rec rename_carrier rename cck = |
|
596 |
match cck with |
|
597 |
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
|
598 |
| _ -> cck |
|
599 |
|
|
600 |
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) |
|
601 |
|
|
602 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |
|
603 |
let rec expr_replace_var fvar expr = |
|
604 |
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } |
|
605 |
|
|
606 |
and expr_desc_replace_var fvar expr_desc = |
|
607 |
match expr_desc with |
|
608 |
| Expr_const _ -> expr_desc |
|
609 |
| Expr_ident i -> Expr_ident (fvar i) |
|
610 |
| Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) |
|
611 |
| Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) |
|
612 |
| Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) |
|
613 |
| Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) |
|
614 |
| Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) |
|
615 |
| Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) |
|
616 |
| Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) |
|
617 |
| Expr_pre e' -> Expr_pre (expr_replace_var fvar e') |
|
618 |
| Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) |
|
619 |
| Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) |
|
620 |
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') |
|
621 |
|
|
622 |
(* Applies the renaming function [fvar] to every rhs |
|
623 |
only when the corresponding lhs satisfies predicate [pvar] *) |
|
624 |
let eq_replace_rhs_var pvar fvar eq = |
|
625 |
let pvar l = List.exists pvar l in |
|
626 |
let rec replace lhs rhs = |
|
627 |
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc } |
|
628 |
and replace_desc lhs rhs_desc = |
|
629 |
match lhs with |
|
630 |
| [] -> assert false |
|
631 |
| [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc |
|
632 |
| _ -> |
|
633 |
(match rhs_desc with |
|
634 |
| Expr_tuple tl -> |
|
635 |
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl) |
|
636 |
| Expr_appl (f, arg, None) when Basic_library.is_internal_fun f -> |
|
637 |
let args = expr_list_of_expr arg in |
|
638 |
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) |
|
639 |
| Expr_array _ |
|
640 |
| Expr_access _ |
|
641 |
| Expr_power _ |
|
642 |
| Expr_const _ |
|
643 |
| Expr_ident _ |
|
644 |
| Expr_appl _ -> |
|
645 |
if pvar lhs |
|
646 |
then expr_desc_replace_var fvar rhs_desc |
|
647 |
else rhs_desc |
|
648 |
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e) |
|
649 |
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2) |
|
650 |
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2) |
|
651 |
| Expr_pre e' -> Expr_pre (replace lhs e') |
|
652 |
| Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i |
|
653 |
in Expr_when (replace lhs e', i', l) |
|
654 |
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
|
655 |
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
|
656 |
) |
|
657 |
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
|
658 |
|
|
659 |
|
|
660 |
let rec rename_expr f_node f_var f_const expr = |
|
661 |
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } |
|
662 |
and rename_expr_desc f_node f_var f_const expr_desc = |
|
663 |
let re = rename_expr f_node f_var f_const in |
|
664 |
match expr_desc with |
|
665 |
| Expr_const _ -> expr_desc |
|
666 |
| Expr_ident i -> Expr_ident (f_var i) |
|
667 |
| Expr_array el -> Expr_array (List.map re el) |
|
668 |
| Expr_access (e1, d) -> Expr_access (re e1, d) |
|
669 |
| Expr_power (e1, d) -> Expr_power (re e1, d) |
|
670 |
| Expr_tuple el -> Expr_tuple (List.map re el) |
|
671 |
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
|
672 |
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
|
673 |
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
|
674 |
| Expr_pre e' -> Expr_pre (re e') |
|
675 |
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
|
676 |
| Expr_merge (i, hl) -> |
|
677 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
|
678 |
| Expr_appl (i, e', i') -> |
|
679 |
Expr_appl (f_node i, re e', Utils.option_map re i') |
|
680 |
|
|
681 |
let rename_node_annot f_node f_var f_const expr = |
|
682 |
expr |
|
683 |
(* TODO assert false *) |
|
684 |
|
|
685 |
let rename_expr_annot f_node f_var f_const annot = |
|
686 |
annot |
|
687 |
(* TODO assert false *) |
|
688 |
|
|
689 |
let rename_node f_node f_var f_const nd = |
|
690 |
let rename_var v = { v with var_id = f_var v.var_id } in |
|
691 |
let rename_eq eq = { eq with |
|
692 |
eq_lhs = List.map f_var eq.eq_lhs; |
|
693 |
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs |
|
694 |
} |
|
695 |
in |
|
696 |
let inputs = List.map rename_var nd.node_inputs in |
|
697 |
let outputs = List.map rename_var nd.node_outputs in |
|
698 |
let locals = List.map rename_var nd.node_locals in |
|
699 |
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in |
|
700 |
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in |
|
701 |
let node_asserts = List.map |
|
702 |
(fun a -> |
|
703 |
{a with assert_expr = |
|
704 |
let expr = a.assert_expr in |
|
705 |
rename_expr f_node f_var f_const expr}) |
|
706 |
nd.node_asserts |
|
707 |
in |
|
708 |
let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in |
|
709 |
let spec = |
|
710 |
Utils.option_map |
|
711 |
(fun s -> rename_node_annot f_node f_var f_const s) |
|
712 |
nd.node_spec |
|
713 |
in |
|
714 |
let annot = |
|
715 |
List.map |
|
716 |
(fun s -> rename_expr_annot f_node f_var f_const s) |
|
717 |
nd.node_annot |
|
718 |
in |
|
719 |
{ |
|
720 |
node_id = f_node nd.node_id; |
|
721 |
node_type = nd.node_type; |
|
722 |
node_clock = nd.node_clock; |
|
723 |
node_inputs = inputs; |
|
724 |
node_outputs = outputs; |
|
725 |
node_locals = locals; |
|
726 |
node_gencalls = gen_calls; |
|
727 |
node_checks = node_checks; |
|
728 |
node_asserts = node_asserts; |
|
729 |
node_stmts = node_stmts; |
|
730 |
node_dec_stateless = nd.node_dec_stateless; |
|
731 |
node_stateless = nd.node_stateless; |
|
732 |
node_spec = spec; |
|
733 |
node_annot = annot; |
|
734 |
} |
|
735 |
|
|
736 |
|
|
737 |
let rename_const f_const c = |
|
738 |
{ c with const_id = f_const c.const_id } |
|
739 |
|
|
740 |
let rename_typedef f_var t = |
|
741 |
match t.tydef_desc with |
|
742 |
| Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) } |
|
743 |
| _ -> t |
|
744 |
|
|
745 |
let rename_prog f_node f_var f_const prog = |
|
746 |
List.rev ( |
|
747 |
List.fold_left (fun accu top -> |
|
748 |
(match top.top_decl_desc with |
|
749 |
| Node nd -> |
|
750 |
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } |
|
751 |
| Const c -> |
|
752 |
{ top with top_decl_desc = Const (rename_const f_const c) } |
|
753 |
| TypeDef tdef -> |
|
754 |
{ top with top_decl_desc = TypeDef (rename_typedef f_var tdef) } |
|
755 |
| ImportedNode _ |
|
756 |
| Open _ -> top) |
|
757 |
::accu |
|
758 |
) [] prog |
|
759 |
) |
|
760 |
|
|
761 |
(**********************************************************************) |
|
762 |
(* Pretty printers *) |
|
763 |
|
|
764 |
let pp_decl_type fmt tdecl = |
|
765 |
match tdecl.top_decl_desc with |
|
766 |
| Node nd -> |
|
767 |
fprintf fmt "%s: " nd.node_id; |
|
768 |
Utils.reset_names (); |
|
769 |
fprintf fmt "%a@ " Types.print_ty nd.node_type |
|
770 |
| ImportedNode ind -> |
|
771 |
fprintf fmt "%s: " ind.nodei_id; |
|
772 |
Utils.reset_names (); |
|
773 |
fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
|
774 |
| Const _ | Open _ | TypeDef _ -> () |
|
775 |
|
|
776 |
let pp_prog_type fmt tdecl_list = |
|
777 |
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
|
778 |
|
|
779 |
let pp_decl_clock fmt cdecl = |
|
780 |
match cdecl.top_decl_desc with |
|
781 |
| Node nd -> |
|
782 |
fprintf fmt "%s: " nd.node_id; |
|
783 |
Utils.reset_names (); |
|
784 |
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
|
785 |
| ImportedNode ind -> |
|
786 |
fprintf fmt "%s: " ind.nodei_id; |
|
787 |
Utils.reset_names (); |
|
788 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
|
789 |
| Const _ | Open _ | TypeDef _ -> () |
|
790 |
|
|
791 |
let pp_prog_clock fmt prog = |
|
792 |
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
|
793 |
|
|
794 |
let pp_error fmt = function |
|
795 |
Main_not_found -> |
|
796 |
fprintf fmt "Cannot compile node %s: could not find the node definition.@." |
|
797 |
!Options.main_node |
|
798 |
| Main_wrong_kind -> |
|
799 |
fprintf fmt |
|
800 |
"Name %s does not correspond to a (non-imported) node definition.@." |
|
801 |
!Options.main_node |
|
802 |
| No_main_specified -> |
|
803 |
fprintf fmt "No main node specified@." |
|
804 |
| Unbound_symbol sym -> |
|
805 |
fprintf fmt |
|
806 |
"%s is undefined.@." |
|
807 |
sym |
|
808 |
| Already_bound_symbol sym -> |
|
809 |
fprintf fmt |
|
810 |
"%s is already defined.@." |
|
811 |
sym |
|
812 |
| Unknown_library sym -> |
|
813 |
fprintf fmt |
|
814 |
"impossible to load library %s.lusic@.Please compile the corresponding interface or source file.@." |
|
815 |
sym |
|
816 |
| Wrong_number sym -> |
|
817 |
fprintf fmt |
|
818 |
"library %s.lusic has a different version number and may crash compiler@.Please recompile the corresponding interface or source file.@." |
|
819 |
sym |
|
820 |
|
|
821 |
(* filling node table with internal functions *) |
|
822 |
let vdecls_of_typ_ck cpt ty = |
|
823 |
let loc = Location.dummy_loc in |
|
824 |
List.map |
|
825 |
(fun _ -> incr cpt; |
|
826 |
let name = sprintf "_var_%d" !cpt in |
|
827 |
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None)) |
|
828 |
(Types.type_list_of_type ty) |
|
829 |
|
|
830 |
let mk_internal_node id = |
|
831 |
let spec = None in |
|
832 |
let ty = Env.lookup_value Basic_library.type_env id in |
|
833 |
let ck = Env.lookup_value Basic_library.clock_env id in |
|
834 |
let (tin, tout) = Types.split_arrow ty in |
|
835 |
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) |
|
836 |
let cpt = ref (-1) in |
|
837 |
mktop |
|
838 |
(ImportedNode |
|
839 |
{nodei_id = id; |
|
840 |
nodei_type = ty; |
|
841 |
nodei_clock = ck; |
|
842 |
nodei_inputs = vdecls_of_typ_ck cpt tin; |
|
843 |
nodei_outputs = vdecls_of_typ_ck cpt tout; |
|
844 |
nodei_stateless = Types.get_static_value ty <> None; |
|
845 |
nodei_spec = spec; |
|
846 |
nodei_prototype = None; |
|
847 |
nodei_in_lib = None; |
|
848 |
}) |
|
849 |
|
|
850 |
let add_internal_funs () = |
|
851 |
List.iter |
|
852 |
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
|
853 |
Basic_library.internal_funs |
|
854 |
|
|
855 |
|
|
856 |
|
|
857 |
(* Replace any occurence of a var in vars_to_replace by its associated |
|
858 |
expression in defs until e does not contain any such variables *) |
|
859 |
let rec substitute_expr vars_to_replace defs e = |
|
860 |
let se = substitute_expr vars_to_replace defs in |
|
861 |
{ e with expr_desc = |
|
862 |
let ed = e.expr_desc in |
|
863 |
match ed with |
|
864 |
| Expr_const _ -> ed |
|
865 |
| Expr_array el -> Expr_array (List.map se el) |
|
866 |
| Expr_access (e1, d) -> Expr_access (se e1, d) |
|
867 |
| Expr_power (e1, d) -> Expr_power (se e1, d) |
|
868 |
| Expr_tuple el -> Expr_tuple (List.map se el) |
|
869 |
| Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e) |
|
870 |
| Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) |
|
871 |
| Expr_fby (e1, e2) -> Expr_fby (se e1, se e2) |
|
872 |
| Expr_pre e' -> Expr_pre (se e') |
|
873 |
| Expr_when (e', i, l)-> Expr_when (se e', i, l) |
|
874 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl) |
|
875 |
| Expr_appl (i, e', i') -> Expr_appl (i, se e', i') |
|
876 |
| Expr_ident i -> |
|
877 |
if List.exists (fun v -> v.var_id = i) vars_to_replace then ( |
|
878 |
let eq_i eq = eq.eq_lhs = [i] in |
|
879 |
if List.exists eq_i defs then |
|
880 |
let sub = List.find eq_i defs in |
|
881 |
let sub' = se sub.eq_rhs in |
|
882 |
sub'.expr_desc |
|
883 |
else |
|
884 |
assert false |
|
885 |
) |
|
886 |
else |
|
887 |
ed |
|
888 |
|
|
889 |
} |
|
890 |
(* FAUT IL RETIRER ? |
|
891 |
|
|
892 |
let rec expr_to_eexpr expr = |
|
893 |
{ eexpr_tag = expr.expr_tag; |
|
894 |
eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc; |
|
895 |
eexpr_type = expr.expr_type; |
|
896 |
eexpr_clock = expr.expr_clock; |
|
897 |
eexpr_loc = expr.expr_loc |
|
898 |
} |
|
899 |
and expr_desc_to_eexpr_desc expr_desc = |
|
900 |
let conv = expr_to_eexpr in |
|
901 |
match expr_desc with |
|
902 |
| Expr_const c -> EExpr_const (match c with |
|
903 |
| Const_int x -> EConst_int x |
|
904 |
| Const_real x -> EConst_real x |
|
905 |
| Const_float x -> EConst_float x |
|
906 |
| Const_tag x -> EConst_tag x |
|
907 |
| _ -> assert false |
|
908 |
|
|
909 |
) |
|
910 |
| Expr_ident i -> EExpr_ident i |
|
911 |
| Expr_tuple el -> EExpr_tuple (List.map conv el) |
|
912 |
|
|
913 |
| Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) |
|
914 |
| Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) |
|
915 |
| Expr_pre e' -> EExpr_pre (conv e') |
|
916 |
| Expr_appl (i, e', i') -> |
|
917 |
EExpr_appl |
|
918 |
(i, conv e', match i' with None -> None | Some(id, _) -> Some id) |
|
919 |
|
|
920 |
| Expr_when _ |
|
921 |
| Expr_merge _ -> assert false |
|
922 |
| Expr_array _ |
|
923 |
| Expr_access _ |
|
924 |
| Expr_power _ -> assert false |
|
925 |
| Expr_ite (c, t, e) -> assert false |
|
926 |
| _ -> assert false |
|
927 |
|
|
928 |
*) |
|
929 |
let rec get_expr_calls nodes e = |
|
930 |
get_calls_expr_desc nodes e.expr_desc |
|
931 |
and get_calls_expr_desc nodes expr_desc = |
|
932 |
let get_calls = get_expr_calls nodes in |
|
933 |
match expr_desc with |
|
934 |
| Expr_const _ |
|
935 |
| Expr_ident _ -> Utils.ISet.empty |
|
936 |
| Expr_tuple el |
|
937 |
| Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el |
|
938 |
| Expr_pre e1 |
|
939 |
| Expr_when (e1, _, _) |
|
940 |
| Expr_access (e1, _) |
|
941 |
| Expr_power (e1, _) -> get_calls e1 |
|
942 |
| Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) |
|
943 |
| Expr_arrow (e1, e2) |
|
944 |
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2) |
|
945 |
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl |
|
946 |
| Expr_appl (i, e', i') -> |
|
947 |
if Basic_library.is_internal_fun i then |
|
948 |
(get_calls e') |
|
949 |
else |
|
950 |
let calls = Utils.ISet.add i (get_calls e') in |
|
951 |
let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in |
|
952 |
if List.exists test nodes then |
|
953 |
match (List.find test nodes).top_decl_desc with |
|
954 |
| Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls |
|
955 |
| _ -> assert false |
|
956 |
else |
|
957 |
calls |
|
958 |
|
|
959 |
and get_eq_calls nodes eq = |
|
960 |
get_expr_calls nodes eq.eq_rhs |
|
961 |
and get_node_calls nodes node = |
|
962 |
List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node) |
|
963 |
|
|
964 |
let rec get_expr_vars vars e = |
|
965 |
get_expr_desc_vars vars e.expr_desc |
|
966 |
and get_expr_desc_vars vars expr_desc = |
|
967 |
match expr_desc with |
|
968 |
| Expr_const _ -> vars |
|
969 |
| Expr_ident x -> Utils.ISet.add x vars |
|
970 |
| Expr_tuple el |
|
971 |
| Expr_array el -> List.fold_left get_expr_vars vars el |
|
972 |
| Expr_pre e1 -> get_expr_vars vars e1 |
|
973 |
| Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 |
|
974 |
| Expr_access (e1, d) |
|
975 |
| Expr_power (e1, d) -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d] |
|
976 |
| Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e] |
|
977 |
| Expr_arrow (e1, e2) |
|
978 |
| Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2] |
|
979 |
| Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl |
|
980 |
| Expr_appl (_, arg, None) -> get_expr_vars vars arg |
|
981 |
| Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r] |
|
982 |
|
|
983 |
|
|
984 |
let rec expr_has_arrows e = |
|
985 |
expr_desc_has_arrows e.expr_desc |
|
986 |
and expr_desc_has_arrows expr_desc = |
|
987 |
match expr_desc with |
|
988 |
| Expr_const _ |
|
989 |
| Expr_ident _ -> false |
|
990 |
| Expr_tuple el |
|
991 |
| Expr_array el -> List.exists expr_has_arrows el |
|
992 |
| Expr_pre e1 |
|
993 |
| Expr_when (e1, _, _) |
|
994 |
| Expr_access (e1, _) |
|
995 |
| Expr_power (e1, _) -> expr_has_arrows e1 |
|
996 |
| Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e] |
|
997 |
| Expr_arrow (e1, e2) |
|
998 |
| Expr_fby (e1, e2) -> true |
|
999 |
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl |
|
1000 |
| Expr_appl (i, e', i') -> expr_has_arrows e' |
|
1001 |
|
|
1002 |
and eq_has_arrows eq = |
|
1003 |
expr_has_arrows eq.eq_rhs |
|
1004 |
and node_has_arrows node = |
|
1005 |
List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node) |
|
1006 |
|
|
1007 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) = |
|
1008 |
assert (value = None || is_const); |
|
1009 |
{ var_id = id; |
|
1010 |
var_orig = orig; |
|
1011 |
var_dec_type = ty_dec; |
|
1012 |
var_dec_clock = ck_dec; |
|
1013 |
var_dec_const = is_const; |
|
1014 |
var_dec_value = value; |
|
1015 |
var_type = Types.new_var (); |
|
1016 |
var_clock = Clocks.new_var true; |
|
1017 |
var_loc = loc } |
|
1018 |
|
|
1019 |
let mkexpr loc d = |
|
1020 |
{ expr_tag = Utils.new_tag (); |
|
1021 |
expr_desc = d; |
|
1022 |
expr_type = Types.new_var (); |
|
1023 |
expr_clock = Clocks.new_var true; |
|
1024 |
expr_delay = Delay.new_var (); |
|
1025 |
expr_annot = None; |
|
1026 |
expr_loc = loc } |
|
1027 |
|
|
1028 |
let var_decl_of_const c = |
|
1029 |
{ var_id = c.const_id; |
|
1030 |
var_orig = true; |
|
1031 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
|
1032 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
|
1033 |
var_dec_const = true; |
|
1034 |
var_dec_value = None; |
|
1035 |
var_type = c.const_type; |
|
1036 |
var_clock = Clocks.new_var false; |
|
1037 |
var_loc = c.const_loc } |
|
1038 |
|
|
1039 |
let mk_new_name used id = |
|
1040 |
let rec new_name name cpt = |
|
1041 |
if used name |
|
1042 |
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
|
1043 |
else name |
|
1044 |
in new_name id 1 |
|
1045 |
|
|
1046 |
let mkeq loc (lhs, rhs) = |
|
1047 |
{ eq_lhs = lhs; |
|
1048 |
eq_rhs = rhs; |
|
1049 |
eq_loc = loc } |
|
1050 |
|
|
1051 |
let mkassert loc expr = |
|
1052 |
{ assert_loc = loc; |
|
1053 |
assert_expr = expr |
|
1054 |
} |
|
1055 |
|
|
1056 |
let mktop_decl loc own itf d = |
|
1057 |
{ top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf } |
|
1058 |
|
|
1059 |
let mkpredef_call loc funname args = |
|
1060 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
|
1061 |
|
|
1062 |
let is_clock_dec_type cty = |
|
1063 |
match cty with |
|
1064 |
| Tydec_clock _ -> true |
|
1065 |
| _ -> false |
|
1066 |
|
|
1067 |
let const_of_top top_decl = |
|
1068 |
match top_decl.top_decl_desc with |
|
1069 |
| Const c -> c |
|
1070 |
| _ -> assert false |
|
1071 |
|
|
1072 |
let node_of_top top_decl = |
|
1073 |
match top_decl.top_decl_desc with |
|
1074 |
| Node nd -> nd |
|
1075 |
| _ -> assert false |
|
1076 |
|
|
1077 |
let imported_node_of_top top_decl = |
|
1078 |
match top_decl.top_decl_desc with |
|
1079 |
| ImportedNode ind -> ind |
|
1080 |
| _ -> assert false |
|
1081 |
|
|
1082 |
let typedef_of_top top_decl = |
|
1083 |
match top_decl.top_decl_desc with |
|
1084 |
| TypeDef tdef -> tdef |
|
1085 |
| _ -> assert false |
|
1086 |
|
|
1087 |
let dependency_of_top top_decl = |
|
1088 |
match top_decl.top_decl_desc with |
|
1089 |
| Open (local, dep) -> (local, dep) |
|
1090 |
| _ -> assert false |
|
1091 |
|
|
1092 |
let consts_of_enum_type top_decl = |
|
1093 |
match top_decl.top_decl_desc with |
|
1094 |
| TypeDef tdef -> |
|
1095 |
(match tdef.tydef_desc with |
|
1096 |
| 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 |
|
1097 |
| _ -> []) |
|
1098 |
| _ -> assert false |
|
1099 |
|
|
1100 |
(************************************************************) |
|
1101 |
(* Eexpr functions *) |
|
1102 |
(************************************************************) |
|
1103 |
|
|
1104 |
let merge_node_annot ann1 ann2 = |
|
1105 |
{ requires = ann1.requires @ ann2.requires; |
|
1106 |
ensures = ann1.ensures @ ann2.ensures; |
|
1107 |
behaviors = ann1.behaviors @ ann2.behaviors; |
|
1108 |
spec_loc = ann1.spec_loc |
|
1109 |
} |
|
1110 |
|
|
1111 |
let mkeexpr loc expr = |
|
1112 |
{ eexpr_tag = Utils.new_tag (); |
|
1113 |
eexpr_qfexpr = expr; |
|
1114 |
eexpr_quantifiers = []; |
|
1115 |
eexpr_type = Types.new_var (); |
|
1116 |
eexpr_clock = Clocks.new_var true; |
|
1117 |
eexpr_normalized = None; |
|
1118 |
eexpr_loc = loc } |
|
1119 |
|
|
1120 |
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers } |
|
1121 |
|
|
1122 |
(* |
|
1123 |
let mkepredef_call loc funname args = |
|
1124 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
|
1125 |
|
|
1126 |
let mkepredef_unary_call loc funname arg = |
|
1127 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
|
1128 |
*) |
|
1129 |
|
|
1130 |
let merge_expr_annot ann1 ann2 = |
|
1131 |
match ann1, ann2 with |
|
1132 |
| None, None -> assert false |
|
1133 |
| Some _, None -> ann1 |
|
1134 |
| None, Some _ -> ann2 |
|
1135 |
| Some ann1, Some ann2 -> Some { |
|
1136 |
annots = ann1.annots @ ann2.annots; |
|
1137 |
annot_loc = ann1.annot_loc |
|
1138 |
} |
|
1139 |
|
|
1140 |
let update_expr_annot node_id e annot = |
|
1141 |
List.iter (fun (key, _) -> |
|
1142 |
Annotations.add_expr_ann node_id e.expr_tag key |
|
1143 |
) annot.annots; |
|
1144 |
{ e with expr_annot = merge_expr_annot e.expr_annot (Some annot) } |
|
1145 |
|
|
1146 |
|
|
1147 |
(***********************************************************) |
|
1148 |
(* Fast access to nodes, by name *) |
|
1149 |
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
|
1150 |
let consts_table = Hashtbl.create 30 |
|
1151 |
|
|
1152 |
let print_node_table fmt () = |
|
1153 |
begin |
|
1154 |
Format.fprintf fmt "{ /* node table */@."; |
|
1155 |
Hashtbl.iter (fun id nd -> |
|
1156 |
Format.fprintf fmt "%s |-> %a" |
|
1157 |
id |
|
1158 |
Printers.pp_short_decl nd |
|
1159 |
) node_table; |
|
1160 |
Format.fprintf fmt "}@." |
|
1161 |
end |
|
1162 |
|
|
1163 |
let print_consts_table fmt () = |
|
1164 |
begin |
|
1165 |
Format.fprintf fmt "{ /* consts table */@."; |
|
1166 |
Hashtbl.iter (fun id const -> |
|
1167 |
Format.fprintf fmt "%s |-> %a" |
|
1168 |
id |
|
1169 |
Printers.pp_const_decl (const_of_top const) |
|
1170 |
) consts_table; |
|
1171 |
Format.fprintf fmt "}@." |
|
1172 |
end |
|
1173 |
|
|
1174 |
let node_name td = |
|
1175 |
match td.top_decl_desc with |
|
1176 |
| Node nd -> nd.node_id |
|
1177 |
| ImportedNode nd -> nd.nodei_id |
|
1178 |
| _ -> assert false |
|
1179 |
|
|
1180 |
let is_generic_node td = |
|
1181 |
match td.top_decl_desc with |
|
1182 |
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
|
1183 |
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
|
1184 |
| _ -> assert false |
|
1185 |
|
|
1186 |
let node_inputs td = |
|
1187 |
match td.top_decl_desc with |
|
1188 |
| Node nd -> nd.node_inputs |
|
1189 |
| ImportedNode nd -> nd.nodei_inputs |
|
1190 |
| _ -> assert false |
|
1191 |
|
|
1192 |
let node_from_name id = |
|
1193 |
try |
|
1194 |
Hashtbl.find node_table id |
|
1195 |
with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id; |
|
1196 |
assert false) |
|
1197 |
|
|
1198 |
let is_imported_node td = |
|
1199 |
match td.top_decl_desc with |
|
1200 |
| Node nd -> false |
|
1201 |
| ImportedNode nd -> true |
|
1202 |
| _ -> assert false |
|
1203 |
|
|
1204 |
|
|
1205 |
(* alias and type definition table *) |
|
1206 |
|
|
1207 |
let mktop = mktop_decl Location.dummy_loc Version.include_path false |
|
1208 |
|
|
1209 |
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) |
|
1210 |
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) |
|
1211 |
let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) |
|
1212 |
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real}) |
|
1213 |
|
|
1214 |
let type_table = |
|
1215 |
Utils.create_hashtable 20 [ |
|
1216 |
Tydec_int , top_int_type; |
|
1217 |
Tydec_bool , top_bool_type; |
|
1218 |
Tydec_float, top_float_type; |
|
1219 |
Tydec_real , top_real_type |
|
1220 |
] |
|
1221 |
|
|
1222 |
let print_type_table fmt () = |
|
1223 |
begin |
|
1224 |
Format.fprintf fmt "{ /* type table */@."; |
|
1225 |
Hashtbl.iter (fun tydec tdef -> |
|
1226 |
Format.fprintf fmt "%a |-> %a" |
|
1227 |
Printers.pp_var_type_dec_desc tydec |
|
1228 |
Printers.pp_typedef (typedef_of_top tdef) |
|
1229 |
) type_table; |
|
1230 |
Format.fprintf fmt "}@." |
|
1231 |
end |
|
1232 |
|
|
1233 |
let rec is_user_type typ = |
|
1234 |
match typ with |
|
1235 |
| Tydec_int | Tydec_bool | Tydec_real |
|
1236 |
| Tydec_float | Tydec_any | Tydec_const _ -> false |
|
1237 |
| Tydec_clock typ' -> is_user_type typ' |
|
1238 |
| _ -> true |
|
1239 |
|
|
1240 |
let get_repr_type typ = |
|
1241 |
let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in |
|
1242 |
if is_user_type typ_def then typ else typ_def |
|
1243 |
|
|
1244 |
let rec coretype_equal ty1 ty2 = |
|
1245 |
let res = |
|
1246 |
match ty1, ty2 with |
|
1247 |
| Tydec_any , _ |
|
1248 |
| _ , Tydec_any -> assert false |
|
1249 |
| Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2 |
|
1250 |
| Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc |
|
1251 |
in (not (is_user_type ty1')) && coretype_equal ty1' ty2 |
|
1252 |
| _ , Tydec_const _ -> coretype_equal ty2 ty1 |
|
1253 |
| Tydec_int , Tydec_int |
|
1254 |
| Tydec_real , Tydec_real |
|
1255 |
| Tydec_float , Tydec_float |
|
1256 |
| Tydec_bool , Tydec_bool -> true |
|
1257 |
| Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2 |
|
1258 |
| Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2 |
|
1259 |
| Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2 |
|
1260 |
| Tydec_struct fl1 , Tydec_struct fl2 -> |
|
1261 |
List.length fl1 = List.length fl2 |
|
1262 |
&& List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2) |
|
1263 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1) |
|
1264 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2) |
|
1265 |
| _ -> false |
|
1266 |
in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res) |
|
1267 |
|
|
1268 |
let tag_true = "true" |
|
1269 |
let tag_false = "false" |
|
1270 |
let tag_default = "default" |
|
1271 |
|
|
1272 |
let const_is_bool c = |
|
1273 |
match c with |
|
1274 |
| Const_tag t -> t = tag_true || t = tag_false |
|
1275 |
| _ -> false |
|
1276 |
|
|
1277 |
(* Computes the negation of a boolean constant *) |
|
1278 |
let const_negation c = |
|
1279 |
assert (const_is_bool c); |
|
1280 |
match c with |
|
1281 |
| Const_tag t when t = tag_true -> Const_tag tag_false |
|
1282 |
| _ -> Const_tag tag_true |
|
1283 |
|
|
1284 |
let const_or c1 c2 = |
|
1285 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1286 |
match c1, c2 with |
|
1287 |
| Const_tag t1, _ when t1 = tag_true -> c1 |
|
1288 |
| _ , Const_tag t2 when t2 = tag_true -> c2 |
|
1289 |
| _ -> Const_tag tag_false |
|
1290 |
|
|
1291 |
let const_and c1 c2 = |
|
1292 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1293 |
match c1, c2 with |
|
1294 |
| Const_tag t1, _ when t1 = tag_false -> c1 |
|
1295 |
| _ , Const_tag t2 when t2 = tag_false -> c2 |
|
1296 |
| _ -> Const_tag tag_true |
|
1297 |
|
|
1298 |
let const_xor c1 c2 = |
|
1299 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1300 |
match c1, c2 with |
|
1301 |
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
|
1302 |
| _ -> Const_tag tag_false |
|
1303 |
|
|
1304 |
let const_impl c1 c2 = |
|
1305 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1306 |
match c1, c2 with |
|
1307 |
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
|
1308 |
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
|
1309 |
| _ -> Const_tag tag_false |
|
1310 |
|
|
1311 |
(* To guarantee uniqueness of tags in enum types *) |
|
1312 |
let tag_table = |
|
1313 |
Utils.create_hashtable 20 [ |
|
1314 |
tag_true, top_bool_type; |
|
1315 |
tag_false, top_bool_type |
|
1316 |
] |
|
1317 |
|
|
1318 |
(* To guarantee uniqueness of fields in struct types *) |
|
1319 |
let field_table = |
|
1320 |
Utils.create_hashtable 20 [ |
|
1321 |
] |
|
1322 |
|
|
1323 |
let get_enum_type_tags cty = |
|
1324 |
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*) |
|
1325 |
match cty with |
|
1326 |
| Tydec_bool -> [tag_true; tag_false] |
|
1327 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
1328 |
| Tydec_enum tl -> tl |
|
1329 |
| _ -> assert false) |
|
1330 |
| _ -> assert false |
|
1331 |
|
|
1332 |
let get_struct_type_fields cty = |
|
1333 |
match cty with |
|
1334 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
1335 |
| Tydec_struct fl -> fl |
|
1336 |
| _ -> assert false) |
|
1337 |
| _ -> assert false |
|
1338 |
|
|
1339 |
let const_of_bool b = |
|
1340 |
Const_tag (if b then tag_true else tag_false) |
|
1341 |
|
|
1342 |
(* let get_const c = snd (Hashtbl.find consts_table c) *) |
|
1343 |
|
|
1344 |
let ident_of_expr expr = |
|
1345 |
match expr.expr_desc with |
|
1346 |
| Expr_ident id -> id |
|
1347 |
| _ -> assert false |
|
1348 |
|
|
1349 |
(* Generate a new ident expression from a declared variable *) |
|
1350 |
let expr_of_vdecl v = |
|
1351 |
{ expr_tag = Utils.new_tag (); |
|
1352 |
expr_desc = Expr_ident v.var_id; |
|
1353 |
expr_type = v.var_type; |
|
1354 |
expr_clock = v.var_clock; |
|
1355 |
expr_delay = Delay.new_var (); |
|
1356 |
expr_annot = None; |
|
1357 |
expr_loc = v.var_loc } |
|
1358 |
|
|
1359 |
(* Caution, returns an untyped and unclocked expression *) |
|
1360 |
let expr_of_ident id loc = |
|
1361 |
{expr_tag = Utils.new_tag (); |
|
1362 |
expr_desc = Expr_ident id; |
|
1363 |
expr_type = Types.new_var (); |
|
1364 |
expr_clock = Clocks.new_var true; |
|
1365 |
expr_delay = Delay.new_var (); |
|
1366 |
expr_loc = loc; |
|
1367 |
expr_annot = None} |
|
1368 |
|
|
1369 |
let is_tuple_expr expr = |
|
1370 |
match expr.expr_desc with |
|
1371 |
| Expr_tuple _ -> true |
|
1372 |
| _ -> false |
|
1373 |
|
|
1374 |
let expr_list_of_expr expr = |
|
1375 |
match expr.expr_desc with |
|
1376 |
| Expr_tuple elist -> elist |
|
1377 |
| _ -> [expr] |
|
1378 |
|
|
1379 |
let expr_of_expr_list loc elist = |
|
1380 |
match elist with |
|
1381 |
| [t] -> { t with expr_loc = loc } |
|
1382 |
| t::_ -> |
|
1383 |
let tlist = List.map (fun e -> e.expr_type) elist in |
|
1384 |
let clist = List.map (fun e -> e.expr_clock) elist in |
|
1385 |
{ t with expr_desc = Expr_tuple elist; |
|
1386 |
expr_type = Type_predef.type_tuple tlist; |
|
1387 |
expr_clock = Clock_predef.ck_tuple clist; |
|
1388 |
expr_tag = Utils.new_tag (); |
|
1389 |
expr_loc = loc } |
|
1390 |
| _ -> assert false |
|
1391 |
|
|
1392 |
let call_of_expr expr = |
|
1393 |
match expr.expr_desc with |
|
1394 |
| Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r) |
|
1395 |
| _ -> assert false |
|
1396 |
|
|
1397 |
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) |
|
1398 |
let rec expr_of_dimension dim = |
|
1399 |
match dim.dim_desc with |
|
1400 |
| Dbool b -> |
|
1401 |
mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
|
1402 |
| Dint i -> |
|
1403 |
mkexpr dim.dim_loc (Expr_const (Const_int i)) |
|
1404 |
| Dident id -> |
|
1405 |
mkexpr dim.dim_loc (Expr_ident id) |
|
1406 |
| Dite (c, t, e) -> |
|
1407 |
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
|
1408 |
| Dappl (id, args) -> |
|
1409 |
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) |
|
1410 |
| Dlink dim' -> expr_of_dimension dim' |
|
1411 |
| Dvar |
|
1412 |
| Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim; |
|
1413 |
assert false) |
|
1414 |
|
|
1415 |
let dimension_of_const loc const = |
|
1416 |
match const with |
|
1417 |
| Const_int i -> mkdim_int loc i |
|
1418 |
| Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true) |
|
1419 |
| _ -> raise InvalidDimension |
|
1420 |
|
|
1421 |
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments |
|
1422 |
into dimension expressions *) |
|
1423 |
let rec dimension_of_expr expr = |
|
1424 |
match expr.expr_desc with |
|
1425 |
| Expr_const c -> dimension_of_const expr.expr_loc c |
|
1426 |
| Expr_ident id -> mkdim_ident expr.expr_loc id |
|
1427 |
| Expr_appl (f, args, None) when Basic_library.is_internal_fun f -> |
|
1428 |
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in |
|
1429 |
if k = None then raise InvalidDimension; |
|
1430 |
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) |
|
1431 |
| Expr_ite (i, t, e) -> |
|
1432 |
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) |
|
1433 |
| _ -> raise InvalidDimension (* not a simple dimension expression *) |
|
1434 |
|
|
1435 |
|
|
1436 |
let sort_handlers hl = |
|
1437 |
List.sort (fun (t, _) (t', _) -> compare t t') hl |
|
1438 |
|
|
1439 |
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with |
|
1440 |
| Expr_const c1, Expr_const c2 -> c1 = c2 |
|
1441 |
| Expr_ident i1, Expr_ident i2 -> i1 = i2 |
|
1442 |
| Expr_array el1, Expr_array el2 |
|
1443 |
| Expr_tuple el1, Expr_tuple el2 -> |
|
1444 |
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
|
1445 |
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
|
1446 |
| Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
|
1447 |
| Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2 |
|
1448 |
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *) |
|
1449 |
(* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *) |
|
1450 |
| Expr_pre e, Expr_pre e' -> is_eq_expr e e' |
|
1451 |
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
|
1452 |
| Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl') |
|
1453 |
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
|
1454 |
| Expr_power (e1, i1), Expr_power (e2, i2) |
|
1455 |
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
|
1456 |
| _ -> false |
|
1457 |
|
|
1458 |
let get_node_vars nd = |
|
1459 |
nd.node_inputs @ nd.node_locals @ nd.node_outputs |
|
1460 |
|
|
1461 |
let mk_new_node_name nd id = |
|
1462 |
let used_vars = get_node_vars nd in |
|
1463 |
let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in |
|
1464 |
mk_new_name used id |
|
1465 |
|
|
1466 |
let get_var id var_list = |
|
1467 |
List.find (fun v -> v.var_id = id) var_list |
|
1468 |
|
|
1469 |
let get_node_var id node = |
|
1470 |
get_var id (get_node_vars node) |
|
1471 |
|
|
1472 |
let get_node_eqs = |
|
1473 |
let get_eqs stmts = |
|
1474 |
List.fold_right |
|
1475 |
(fun stmt res -> |
|
1476 |
match stmt with |
|
1477 |
| Eq eq -> eq :: res |
|
1478 |
| Aut _ -> assert false) |
|
1479 |
stmts |
|
1480 |
[] in |
|
1481 |
let table_eqs = Hashtbl.create 23 in |
|
1482 |
(fun nd -> |
|
1483 |
try |
|
1484 |
let (old, res) = Hashtbl.find table_eqs nd.node_id |
|
1485 |
in if old == nd.node_stmts then res else raise Not_found |
|
1486 |
with Not_found -> |
|
1487 |
let res = get_eqs nd.node_stmts in |
|
1488 |
begin |
|
1489 |
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); |
|
1490 |
res |
|
1491 |
end) |
|
1492 |
|
|
1493 |
let get_node_eq id node = |
|
1494 |
List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node) |
|
1495 |
|
|
1496 |
let get_nodes prog = |
|
1497 |
List.fold_left ( |
|
1498 |
fun nodes decl -> |
|
1499 |
match decl.top_decl_desc with |
|
1500 |
| Node _ -> decl::nodes |
|
1501 |
| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes |
|
1502 |
) [] prog |
|
1503 |
|
|
1504 |
let get_imported_nodes prog = |
|
1505 |
List.fold_left ( |
|
1506 |
fun nodes decl -> |
|
1507 |
match decl.top_decl_desc with |
|
1508 |
| ImportedNode _ -> decl::nodes |
|
1509 |
| Const _ | Node _ | Open _ | TypeDef _-> nodes |
|
1510 |
) [] prog |
|
1511 |
|
|
1512 |
let get_consts prog = |
|
1513 |
List.fold_right ( |
|
1514 |
fun decl consts -> |
|
1515 |
match decl.top_decl_desc with |
|
1516 |
| Const _ -> decl::consts |
|
1517 |
| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts |
|
1518 |
) prog [] |
|
1519 |
|
|
1520 |
let get_typedefs prog = |
|
1521 |
List.fold_right ( |
|
1522 |
fun decl types -> |
|
1523 |
match decl.top_decl_desc with |
|
1524 |
| TypeDef _ -> decl::types |
|
1525 |
| Node _ | ImportedNode _ | Open _ | Const _ -> types |
|
1526 |
) prog [] |
|
1527 |
|
|
1528 |
let get_dependencies prog = |
|
1529 |
List.fold_right ( |
|
1530 |
fun decl deps -> |
|
1531 |
match decl.top_decl_desc with |
|
1532 |
| Open _ -> decl::deps |
|
1533 |
| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps |
|
1534 |
) prog [] |
|
1535 |
|
|
1536 |
let get_node_interface nd = |
|
1537 |
{nodei_id = nd.node_id; |
|
1538 |
nodei_type = nd.node_type; |
|
1539 |
nodei_clock = nd.node_clock; |
|
1540 |
nodei_inputs = nd.node_inputs; |
|
1541 |
nodei_outputs = nd.node_outputs; |
|
1542 |
nodei_stateless = nd.node_dec_stateless; |
|
1543 |
nodei_spec = nd.node_spec; |
|
1544 |
nodei_prototype = None; |
|
1545 |
nodei_in_lib = None; |
|
1546 |
} |
|
1547 |
|
|
1548 |
(************************************************************************) |
|
1549 |
(* Renaming *) |
|
1550 |
|
|
1551 |
let rec rename_static rename cty = |
|
1552 |
match cty with |
|
1553 |
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
|
1554 |
| Tydec_clock cty -> Tydec_clock (rename_static rename cty) |
|
1555 |
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
|
1556 |
| _ -> cty |
|
1557 |
|
|
1558 |
let rec rename_carrier rename cck = |
|
1559 |
match cck with |
|
1560 |
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
|
1561 |
| _ -> cck |
|
1562 |
|
|
1563 |
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) |
|
1564 |
|
|
581 | 1565 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |
582 | 1566 |
let rec expr_replace_var fvar expr = |
583 | 1567 |
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } |
... | ... | |
799 | 1783 |
List.map |
800 | 1784 |
(fun _ -> incr cpt; |
801 | 1785 |
let name = sprintf "_var_%d" !cpt in |
802 |
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)) |
|
1786 |
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
|
|
803 | 1787 |
(Types.type_list_of_type ty) |
804 | 1788 |
|
805 | 1789 |
let mk_internal_node id = |
... | ... | |
979 | 1963 |
and node_has_arrows node = |
980 | 1964 |
List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node) |
981 | 1965 |
|
1966 |
let copy_var_decl vdecl = |
|
1967 |
mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value) |
|
1968 |
|
|
1969 |
let copy_const cdecl = |
|
1970 |
{ cdecl with const_type = Types.new_var () } |
|
1971 |
|
|
1972 |
let copy_node nd = |
|
1973 |
{ nd with |
|
1974 |
node_type = Types.new_var (); |
|
1975 |
node_clock = Clocks.new_var true; |
|
1976 |
node_inputs = List.map copy_var_decl nd.node_inputs; |
|
1977 |
node_outputs = List.map copy_var_decl nd.node_outputs; |
|
1978 |
node_locals = List.map copy_var_decl nd.node_locals; |
|
1979 |
node_gencalls = []; |
|
1980 |
node_checks = []; |
|
1981 |
node_stateless = None; |
|
1982 |
} |
|
1983 |
|
|
1984 |
let copy_top top = |
|
1985 |
match top.top_decl_desc with |
|
1986 |
| Node nd -> { top with top_decl_desc = Node (copy_node nd) } |
|
1987 |
| Const c -> { top with top_decl_desc = Const (copy_const c) } |
|
1988 |
| _ -> top |
|
1989 |
|
|
1990 |
let copy_prog top_list = |
|
1991 |
List.map copy_top top_list |
|
1992 |
|
|
982 | 1993 |
(* Local Variables: *) |
983 | 1994 |
(* compile-command:"make -C .." *) |
984 | 1995 |
(* End: *) |
Also available in: Unified diff