Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / basic_library.ml @ df647a81

History | View | Annotate | Download (8.69 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
5
 *
6
 * This file is part of Prelude
7
 *
8
 * Prelude is free software; you can redistribute it and/or
9
 * modify it under the terms of the GNU Lesser General Public License
10
 * as published by the Free Software Foundation ; either version 2 of
11
 * the License, or (at your option) any later version.
12
 *
13
 * Prelude is distributed in the hope that it will be useful, but
14
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
15
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
16
 * Lesser General Public License for more details.
17
 *
18
 * You should have received a copy of the GNU Lesser General Public
19
 * License along with this program ; if not, write to the Free Software
20
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
21
 * USA
22
 *---------------------------------------------------------------------------- *)
23

    
24
(* This module is used for the lustre to C compiler *)
25

    
26
open Type_predef
27
open Clock_predef
28
open Delay_predef
29
open Dimension
30

    
31
module TE = Env
32

    
33
let static_op ty =
34
  type_static (mkdim_var ()) ty
35

    
36
let type_env =
37
  List.fold_left 
38
    (fun env (op, op_type) -> TE.add_value env op op_type)
39
    TE.initial
40
    [
41
       "+", (static_op type_bin_poly_op);
42
      "uminus", (static_op type_unary_poly_op); 
43
      "-", (static_op type_bin_poly_op); 
44
      "*", (static_op type_bin_poly_op);
45
      "/", (static_op type_bin_poly_op);
46
      "mod", (static_op type_bin_int_op);
47
      "&&", (static_op type_bin_bool_op);
48
      "||", (static_op type_bin_bool_op);
49
      "xor", (static_op type_bin_bool_op);
50
      "impl", (static_op type_bin_bool_op);
51
      "<", (static_op type_bin_comp_op);
52
      "<=", (static_op type_bin_comp_op);
53
      ">", (static_op type_bin_comp_op);
54
      ">=", (static_op type_bin_comp_op);
55
      "!=", (static_op type_bin_comp_op);
56
      "=", (static_op type_bin_comp_op);
57
      "not", (static_op type_unary_bool_op)
58
]
59
 
60
module CE = Env
61

    
62
let clock_env =
63
  let init_env = CE.initial in
64
  let env' = 
65
    List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
66
      ["uminus"; "not"] init_env in
67
  let env' = 
68
    List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
69
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
70
  env'
71

    
72
module DE = Env
73

    
74
let delay_env =
75
  let init_env = DE.initial in
76
  let env' = 
77
    List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
78
      ["uminus"; "not"] init_env in
79
  let env' = 
80
    List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
81
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
82
  let env' = 
83
    List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
84
      [] env' in
85
  env'
86

    
87
module VE = Env
88

    
89
let eval_env =
90
  let defs = [ 
91
    "uminus", (function [Dint a] -> Dint (-a)           | _ -> assert false);
92
    "not", (function [Dbool b] -> Dbool (not 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
    "*", (function [Dint a; Dint b] -> Dint (a*b)       | _ -> assert false);
96
    "/", (function [Dint a; Dint b] -> Dint (a/b)       | _ -> assert false);
97
    "mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false);
98
    "&&", (function [Dbool a; Dbool b] -> Dbool (a&&b)  | _ -> assert false);
99
    "||", (function [Dbool a; Dbool b] -> Dbool (a||b)  | _ -> assert false);
100
    "xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);
101
    "impl", (function [Dbool a; Dbool 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 [Dint a; Dint b] -> Dbool (a>=b)    | _ -> assert false);
106
    "!=", (function [a; b] -> Dbool (a<>b)              | _ -> assert false);
107
    "=", (function [a; b] -> Dbool (a=b)                | _ -> assert false);
108
  ]
109
  in
110
  List.fold_left 
111
    (fun env (op, op_eval) -> VE.add_value env op op_eval)
112
    VE.initial
113
    defs
114

    
115
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
116

    
117
let is_internal_fun x =
118
  List.mem x internal_funs
119

    
120
(*
121
let imported_node name inputs outputs sl spec =
122
  mktop_decl Location.dummy_loc
123
    (
124
      ImportedNode
125
	{nodei_id = name;
126
	 nodei_type = Types.new_var ();
127
	 nodei_clock = Clocks.new_var true;
128
	 nodei_inputs = inputs;
129
	 nodei_outputs = outputs;
130
	 nodei_stateless = sl;
131
	nodei_spec = spec})
132
    
133
let mk_new_var id =
134
  let loc = Location.dummy_loc in
135
  mkvar_decl loc (id, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)
136

    
137
let _ = 
138
  let binary_fun id = id, [mk_new_var "x"; mk_new_var "y"], [mk_new_var "z"] in
139
  let unary_fun id = id, [mk_new_var "x"], [mk_new_var "y"] in
140
  (* All following functions are stateless *)
141
  let st = true in
142
  List.iter (fun (n,i,o) -> Hashtbl.add node_table n (imported_node n i o st None))
143
    (
144
(*("ite", [mk_new_var "g"; mk_new_var "x"; mk_new_var "y"], [mk_new_var "z"])::*)
145
    (List.map binary_fun
146
	["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"="])
147
     @(List.map unary_fun ["uminus";"not"]))
148
*)  
149
let pp_c i get_val_type pp_val fmt vl =
150
  match i, vl with
151
    | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3
152
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
153
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
154
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
155
    | "=", [v1; v2] when get_val_type v1 == Types.Tbool-> 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
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
159
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
160
    | _ -> raise (Failure ("No C printer for function " ^ i))
161

    
162
let pp_java i pp_val fmt vl =
163
  match i, vl with
164
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
165
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
166
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
167
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
168
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
169
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
170
    | _ -> raise (Failure ("No Java printer for function " ^ i))
171

    
172
let pp_horn i pp_val fmt vl = 
173
  match i, vl with
174
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 
175
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
176
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v 
177
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
178
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
179
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
180
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
181
  (* | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 *)
182
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
183
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
184
  | _ -> raise (Failure ("No horn printer for function " ^ i))
185
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
186
  
187
*)
188

    
189

    
190
let pp_acsl i get_val_type pp_val fmt vl =
191
  match i, vl with
192
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 
193
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
194
  | "not", [v] -> Format.fprintf fmt "((%a == 0)?1:0)" pp_val v 
195
  | "impl", [v1; v2] -> Format.fprintf fmt "(%a?(%a?1:0):1)" pp_val v1 pp_val v2 
196
  | "=", [v1; v2] when get_val_type v1 == Types.Tbool-> Format.fprintf fmt "(((!!%a) == (!!%a))?1:0)" pp_val v1 pp_val v2
197
  | "=", [v1; v2] -> Format.fprintf fmt "((%a == %a)?1:0)" pp_val v1 pp_val v2
198
  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
199
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
200
  | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
201
  | _ -> raise (Failure ("No ACSL printer for function " ^ i))
202

    
203
(* Local Variables: *)
204
(* compile-command:"make -C .." *)
205
(* End: *)