Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / basic_library.ml @ c1adf235

History | View | Annotate | Download (7.28 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 LustreSpec
27
open Type_predef
28
open Clock_predef
29
open Delay_predef
30
open Dimension
31

    
32
module TE = Env
33

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

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

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

    
74
module DE = Env
75

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

    
89
module VE = Env
90

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

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

    
120
let is_internal_fun x =
121
  List.mem x internal_funs
122

    
123
let pp_c i pp_val fmt vl =
124
  match i, vl with
125
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
126
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
127
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
128
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
129
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
130
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
131
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
132
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
133
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
134
    | _ -> failwith i
135

    
136
let pp_java i pp_val fmt vl =
137
  match i, vl with
138
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
139
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
140
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
141
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
142
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
143
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
144
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
145
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
146
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
147
    | _ -> assert false
148

    
149
let pp_horn i pp_val fmt vl = 
150
  match i, vl with
151
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %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 "(not %a)" pp_val v 
154
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
155
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
156
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
157
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
158
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
159
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
160
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
161
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
162
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
163
  | _ -> assert false
164
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
165
  
166
*)
167

    
168
(* Local Variables: *)
169
(* compile-command:"make -C .." *)
170
(* End: *)