lustrec / src / basic_library.ml @ 3bc26d43
History | View | Annotate | Download (6.57 KB)
1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|
2 | (* *) |
||
3 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||
4 | (* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *) |
||
5 | (* *) |
||
6 | (* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
||
7 | (* under the terms of the GNU Lesser General Public License *) |
||
8 | (* version 2.1. *) |
||
9 | (* *) |
||
10 | (********************************************************************) |
||
11 | 22fe1c93 | ploc | |
12 | a2d97a3e | ploc | (* Parts of this file come from the Prelude compiler *) |
13 | 22fe1c93 | ploc | |
14 | 8446bf03 | ploc | (*open LustreSpec*) |
15 | 22fe1c93 | ploc | open Type_predef |
16 | open Clock_predef |
||
17 | open Delay_predef |
||
18 | open Dimension |
||
19 | |||
20 | module TE = Env |
||
21 | |||
22 | let static_op ty = |
||
23 | type_static (mkdim_var ()) ty |
||
24 | |||
25 | let type_env = |
||
26 | e9b71779 | tkahsai | List.fold_left |
27 | 5c1184ad | ploc | (fun env (op, op_type) -> TE.add_value env op op_type) |
28 | TE.initial |
||
29 | [ |
||
30 | ef34b4ae | xthirioux | "true", (static_op type_bool); |
31 | "false", (static_op type_bool); |
||
32 | "+", (static_op type_bin_poly_op); |
||
33 | e9b71779 | tkahsai | "uminus", (static_op type_unary_poly_op); |
34 | "-", (static_op type_bin_poly_op); |
||
35 | 5c1184ad | ploc | "*", (static_op type_bin_poly_op); |
36 | "/", (static_op type_bin_poly_op); |
||
37 | "mod", (static_op type_bin_int_op); |
||
38 | "&&", (static_op type_bin_bool_op); |
||
39 | "||", (static_op type_bin_bool_op); |
||
40 | "xor", (static_op type_bin_bool_op); |
||
41 | 6afa892a | xthirioux | "equi", (static_op type_bin_bool_op); |
42 | 5c1184ad | ploc | "impl", (static_op type_bin_bool_op); |
43 | "<", (static_op type_bin_comp_op); |
||
44 | "<=", (static_op type_bin_comp_op); |
||
45 | ">", (static_op type_bin_comp_op); |
||
46 | ">=", (static_op type_bin_comp_op); |
||
47 | "!=", (static_op type_bin_comp_op); |
||
48 | "=", (static_op type_bin_comp_op); |
||
49 | "not", (static_op type_unary_bool_op) |
||
50 | ] |
||
51 | e9b71779 | tkahsai | |
52 | 22fe1c93 | ploc | module CE = Env |
53 | |||
54 | let clock_env = |
||
55 | let init_env = CE.initial in |
||
56 | ef34b4ae | xthirioux | let env' = |
57 | List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ) |
||
58 | ["true"; "false"] init_env in |
||
59 | e9b71779 | tkahsai | let env' = |
60 | 22fe1c93 | ploc | List.fold_right (fun op env -> CE.add_value env op ck_unary_univ) |
61 | ef34b4ae | xthirioux | ["uminus"; "not"] env' in |
62 | e9b71779 | tkahsai | let env' = |
63 | 22fe1c93 | ploc | List.fold_right (fun op env -> CE.add_value env op ck_bin_univ) |
64 | 6afa892a | xthirioux | ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
65 | 22fe1c93 | ploc | env' |
66 | |||
67 | module DE = Env |
||
68 | |||
69 | let delay_env = |
||
70 | let init_env = DE.initial in |
||
71 | ef34b4ae | xthirioux | let env' = |
72 | List.fold_right (fun op env -> DE.add_value env op delay_nullary_poly_op) |
||
73 | ["true"; "false"] init_env in |
||
74 | let env' = |
||
75 | 22fe1c93 | ploc | List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op) |
76 | ef34b4ae | xthirioux | ["uminus"; "not"] env' in |
77 | e9b71779 | tkahsai | let env' = |
78 | 22fe1c93 | ploc | List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op) |
79 | 6afa892a | xthirioux | ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
80 | e9b71779 | tkahsai | let env' = |
81 | 22fe1c93 | ploc | List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op) |
82 | [] env' in |
||
83 | env' |
||
84 | |||
85 | module VE = Env |
||
86 | |||
87 | let eval_env = |
||
88 | e9b71779 | tkahsai | let defs = [ |
89 | 5c1184ad | ploc | "uminus", (function [Dint a] -> Dint (-a) | _ -> assert false); |
90 | "not", (function [Dbool b] -> Dbool (not b) | _ -> assert false); |
||
91 | "+", (function [Dint a; Dint b] -> Dint (a+b) | _ -> assert false); |
||
92 | "-", (function [Dint a; Dint b] -> Dint (a-b) | _ -> assert false); |
||
93 | "*", (function [Dint a; Dint b] -> Dint (a*b) | _ -> assert false); |
||
94 | "/", (function [Dint a; Dint b] -> Dint (a/b) | _ -> assert false); |
||
95 | "mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false); |
||
96 | "&&", (function [Dbool a; Dbool b] -> Dbool (a&&b) | _ -> assert false); |
||
97 | "||", (function [Dbool a; Dbool b] -> Dbool (a||b) | _ -> assert false); |
||
98 | "xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false); |
||
99 | 6afa892a | xthirioux | "equi", (function [Dbool a; Dbool b] -> Dbool (a=b) | _ -> assert false); |
100 | 5c1184ad | ploc | "impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false); |
101 | "<", (function [Dint a; Dint b] -> Dbool (a<b) | _ -> assert false); |
||
102 | ">", (function [Dint a; Dint b] -> Dbool (a>b) | _ -> assert false); |
||
103 | "<=", (function [Dint a; Dint b] -> Dbool (a<=b) | _ -> assert false); |
||
104 | ">=", (function [Dint a; Dint b] -> Dbool (a>=b) | _ -> assert false); |
||
105 | "!=", (function [a; b] -> Dbool (a<>b) | _ -> assert false); |
||
106 | "=", (function [a; b] -> Dbool (a=b) | _ -> assert false); |
||
107 | ] |
||
108 | in |
||
109 | e9b71779 | tkahsai | List.fold_left |
110 | 5c1184ad | ploc | (fun env (op, op_eval) -> VE.add_value env op op_eval) |
111 | VE.initial |
||
112 | defs |
||
113 | 22fe1c93 | ploc | |
114 | 04a63d25 | xthirioux | let arith_funs = ["+";"-";"*";"/";"mod"; "uminus"] |
115 | let bool_funs = ["&&";"||";"xor";"equi";"impl"; "not"] |
||
116 | let rel_funs = ["<";">";"<=";">=";"!=";"="] |
||
117 | 719f9992 | xthirioux | |
118 | 04a63d25 | xthirioux | let internal_funs = arith_funs@bool_funs@rel_funs |
119 | |||
120 | let rec is_internal_fun x targs = |
||
121 | (*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*) |
||
122 | match targs with |
||
123 | | [] -> assert false |
||
124 | | t::_ when Types.is_real_type t -> List.mem x internal_funs && not !Options.mpfr |
||
125 | | t::_ when Types.is_array_type t -> is_internal_fun x [Types.array_element_type t] |
||
126 | | _ -> List.mem x internal_funs |
||
127 | |||
128 | let is_expr_internal_fun expr = |
||
129 | 8446bf03 | ploc | let open Lustre_types in |
130 | 04a63d25 | xthirioux | match expr.expr_desc with |
131 | | Expr_appl (f, e, _) -> is_internal_fun f (Types.type_list_of_type e.expr_type) |
||
132 | | _ -> assert false |
||
133 | |||
134 | let is_value_internal_fun v = |
||
135 | 8446bf03 | ploc | let open Machine_code_types in |
136 | 04a63d25 | xthirioux | match v.value_desc with |
137 | | Fun (f, vl) -> is_internal_fun f (List.map (fun v -> v.value_type) vl) |
||
138 | | _ -> assert false |
||
139 | |||
140 | 53206908 | xthirioux | let is_numeric_operator x = |
141 | 85da3a4b | ploc | List.mem x arith_funs |
142 | 53206908 | xthirioux | |
143 | 04a63d25 | xthirioux | let is_homomorphic_fun x = |
144 | List.mem x internal_funs |
||
145 | |||
146 | let is_stateless_fun x = |
||
147 | 22fe1c93 | ploc | List.mem x internal_funs |
148 | |||
149 | ea8f51ae | ploc | |
150 | (* let pp_java i pp_val fmt vl = *) |
||
151 | (* match i, vl with *) |
||
152 | (* (\* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *\) *) |
||
153 | (* | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *) |
||
154 | (* | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *) |
||
155 | (* | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *) |
||
156 | (* | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *) |
||
157 | (* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *) |
||
158 | (* | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *) |
||
159 | (* | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *) |
||
160 | (* | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *) |
||
161 | (* | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) *) |
||
162 | |||
163 | 22fe1c93 | ploc | |
164 | (* Local Variables: *) |
||
165 | (* compile-command:"make -C .." *) |
||
166 | (* End: *) |