Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / basic_library.ml @ b38ffff3

History | View | Annotate | Download (6.9 KB)

1
(********************************************************************)
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

    
12
(* Parts of this file come from the Prelude compiler *)
13

    
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
  List.fold_left 
27
    (fun env (op, op_type) -> TE.add_value env op op_type)
28
    TE.initial
29
    [
30
       "+", (static_op type_bin_poly_op);
31
      "uminus", (static_op type_unary_poly_op); 
32
      "-", (static_op type_bin_poly_op); 
33
      "*", (static_op type_bin_poly_op);
34
      "/", (static_op type_bin_poly_op);
35
      "mod", (static_op type_bin_int_op);
36
      "&&", (static_op type_bin_bool_op);
37
      "||", (static_op type_bin_bool_op);
38
      "xor", (static_op type_bin_bool_op);
39
      "equi", (static_op type_bin_bool_op);
40
      "impl", (static_op type_bin_bool_op);
41
      "<", (static_op type_bin_comp_op);
42
      "<=", (static_op type_bin_comp_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
      "not", (static_op type_unary_bool_op)
48
]
49
 
50
module CE = Env
51

    
52
let clock_env =
53
  let init_env = CE.initial in
54
  let env' = 
55
    List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
56
      ["uminus"; "not"] init_env in
57
  let env' = 
58
    List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
59
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
60
  env'
61

    
62
module DE = Env
63

    
64
let delay_env =
65
  let init_env = DE.initial in
66
  let env' = 
67
    List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
68
      ["uminus"; "not"] init_env in
69
  let env' = 
70
    List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
71
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
72
  let env' = 
73
    List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
74
      [] env' in
75
  env'
76

    
77
module VE = Env
78

    
79
let eval_env =
80
  let defs = [ 
81
    "uminus", (function [Dint a] -> Dint (-a)           | _ -> assert false);
82
    "not", (function [Dbool b] -> Dbool (not b)         | _ -> assert false);
83
    "+", (function [Dint a; Dint b] -> Dint (a+b)       | _ -> assert false);
84
    "-", (function [Dint a; Dint b] -> Dint (a-b)       | _ -> assert false);
85
    "*", (function [Dint a; Dint b] -> Dint (a*b)       | _ -> assert false);
86
    "/", (function [Dint a; Dint b] -> Dint (a/b)       | _ -> assert false);
87
    "mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false);
88
    "&&", (function [Dbool a; Dbool b] -> Dbool (a&&b)  | _ -> assert false);
89
    "||", (function [Dbool a; Dbool b] -> Dbool (a||b)  | _ -> assert false);
90
    "xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);
91
    "equi", (function [Dbool a; Dbool b] -> Dbool (a=b) | _ -> assert false);
92
    "impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false);
93
    "<", (function [Dint a; Dint b] -> Dbool (a<b)      | _ -> assert false);
94
    ">", (function [Dint a; Dint b] -> Dbool (a>b)      | _ -> assert false);
95
    "<=", (function [Dint a; Dint b] -> Dbool (a<=b)    | _ -> assert false);
96
    ">=", (function [Dint a; Dint b] -> Dbool (a>=b)    | _ -> assert false);
97
    "!=", (function [a; b] -> Dbool (a<>b)              | _ -> assert false);
98
    "=", (function [a; b] -> Dbool (a=b)                | _ -> assert false);
99
  ]
100
  in
101
  List.fold_left 
102
    (fun env (op, op_eval) -> VE.add_value env op op_eval)
103
    VE.initial
104
    defs
105

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

    
108
let is_internal_fun x =
109
  List.mem x internal_funs
110

    
111
let pp_c i pp_val fmt vl =
112
  match i, vl with
113
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
114
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
115
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
116
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
117
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
118
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
119
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
120
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
121
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
122
    | _ -> failwith i
123

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

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

    
156
(* Local Variables: *)
157
(* compile-command:"make -C .." *)
158
(* End: *)