Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / basic_library.ml @ ef8a361a

History | View | Annotate | Download (8.39 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
open LustreSpec
15
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
  match expr.expr_desc with
130
  | Expr_appl (f, e, _) -> is_internal_fun f (Types.type_list_of_type e.expr_type)
131
  | _                   -> assert false
132
133
let is_value_internal_fun v =
134
  match v.value_desc with
135
  | Fun (f, vl) -> is_internal_fun f (List.map (fun v -> v.value_type) vl)
136
  | _           -> assert false
137
138 53206908 xthirioux
let is_numeric_operator x =
139 85da3a4b ploc
  List.mem x arith_funs
140 53206908 xthirioux
141 04a63d25 xthirioux
let is_homomorphic_fun x =
142
  List.mem x internal_funs
143
144
let is_stateless_fun x =
145 22fe1c93 ploc
  List.mem x internal_funs
146
147
let pp_c i pp_val fmt vl =
148
  match i, vl with
149
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
150
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
151 e9b71779 tkahsai
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
152
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
153
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
154 6afa892a xthirioux
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
155
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
156
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
157 e9b71779 tkahsai
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
158 2d179f5b xthirioux
    | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
159 22fe1c93 ploc
160
let pp_java i pp_val fmt vl =
161
  match i, vl with
162
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
163
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
164 e9b71779 tkahsai
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
165
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
166
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
167 6afa892a xthirioux
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
168
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
169
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
170 e9b71779 tkahsai
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
171 2d179f5b xthirioux
    | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false)
172 22fe1c93 ploc
173 e9b71779 tkahsai
let pp_horn i pp_val fmt vl =
174 7a19992d ploc
  match i, vl with
175 e9b71779 tkahsai
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
176
177 7a19992d ploc
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
178 e9b71779 tkahsai
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
179
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
180
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
181
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
182
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
183 6afa892a xthirioux
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
184
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
185
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
186 e9b71779 tkahsai
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
187
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
188
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
189 2d179f5b xthirioux
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
190 e9b71779 tkahsai
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
191
192 7a19992d ploc
*)
193 22fe1c93 ploc
194
(* Local Variables: *)
195
(* compile-command:"make -C .." *)
196
(* End: *)