Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / basic_library.ml @ 14d694c7

History | View | Annotate | Download (6.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 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
      "impl", (static_op type_bin_bool_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
      "=", (static_op type_bin_comp_op);
58
      "not", (static_op type_unary_bool_op)
59
]
60
 
61
module CE = Env
62

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

    
73
module DE = Env
74

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

    
88
module VE = Env
89

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

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

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

    
121

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

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

    
144
let pp_horn i pp_val fmt vl = 
145
  match i, vl with
146
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 
147
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
148
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v 
149
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
150
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
151
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
152
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
153
  (* | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 *)
154
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
155
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
156
  | _ -> assert false
157
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
158
  
159
*)
160

    
161
(* Local Variables: *)
162
(* compile-command:"make -C .." *)
163
(* End: *)