| 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 |
8446bf03
|
ploc
|
(*open LustreSpec*)
|
| 15 |
22fe1c93
|
ploc
|
open Type_predef
|
| 16 |
|
|
open Clock_predef
|
| 17 |
|
|
open Delay_predef
|
| 18 |
|
|
open Dimension
|
| 19 |
|
|
module TE = Env
|
| 20 |
|
|
|
| 21 |
ca7ff3f7
|
Lélio Brun
|
let static_op ty = type_static (mkdim_var ()) ty
|
| 22 |
22fe1c93
|
ploc
|
|
| 23 |
|
|
let type_env =
|
| 24 |
e9b71779
|
tkahsai
|
List.fold_left
|
| 25 |
5c1184ad
|
ploc
|
(fun env (op, op_type) -> TE.add_value env op op_type)
|
| 26 |
|
|
TE.initial
|
| 27 |
|
|
[
|
| 28 |
ca7ff3f7
|
Lélio Brun
|
"true", static_op type_bool;
|
| 29 |
|
|
"false", static_op type_bool;
|
| 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 |
e9b71779
|
tkahsai
|
|
| 50 |
22fe1c93
|
ploc
|
module CE = Env
|
| 51 |
|
|
|
| 52 |
|
|
let clock_env =
|
| 53 |
|
|
let init_env = CE.initial in
|
| 54 |
ef34b4ae
|
xthirioux
|
let env' =
|
| 55 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 56 |
|
|
(fun op env -> CE.add_value env op ck_nullary_univ)
|
| 57 |
|
|
[ "true"; "false" ] init_env
|
| 58 |
|
|
in
|
| 59 |
e9b71779
|
tkahsai
|
let env' =
|
| 60 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 61 |
|
|
(fun op env -> CE.add_value env op ck_unary_univ)
|
| 62 |
|
|
[ "uminus"; "not" ] env'
|
| 63 |
|
|
in
|
| 64 |
e9b71779
|
tkahsai
|
let env' =
|
| 65 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 66 |
|
|
(fun op env -> CE.add_value env op ck_bin_univ)
|
| 67 |
|
|
[
|
| 68 |
|
|
"+";
|
| 69 |
|
|
"-";
|
| 70 |
|
|
"*";
|
| 71 |
|
|
"/";
|
| 72 |
|
|
"mod";
|
| 73 |
|
|
"&&";
|
| 74 |
|
|
"||";
|
| 75 |
|
|
"xor";
|
| 76 |
|
|
"equi";
|
| 77 |
|
|
"impl";
|
| 78 |
|
|
"<";
|
| 79 |
|
|
"<=";
|
| 80 |
|
|
">";
|
| 81 |
|
|
">=";
|
| 82 |
|
|
"!=";
|
| 83 |
|
|
"=";
|
| 84 |
|
|
]
|
| 85 |
|
|
env'
|
| 86 |
|
|
in
|
| 87 |
22fe1c93
|
ploc
|
env'
|
| 88 |
|
|
|
| 89 |
|
|
module DE = Env
|
| 90 |
|
|
|
| 91 |
|
|
let delay_env =
|
| 92 |
|
|
let init_env = DE.initial in
|
| 93 |
ef34b4ae
|
xthirioux
|
let env' =
|
| 94 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 95 |
|
|
(fun op env -> DE.add_value env op delay_nullary_poly_op)
|
| 96 |
|
|
[ "true"; "false" ] init_env
|
| 97 |
|
|
in
|
| 98 |
ef34b4ae
|
xthirioux
|
let env' =
|
| 99 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 100 |
|
|
(fun op env -> DE.add_value env op delay_unary_poly_op)
|
| 101 |
|
|
[ "uminus"; "not" ] env'
|
| 102 |
|
|
in
|
| 103 |
e9b71779
|
tkahsai
|
let env' =
|
| 104 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 105 |
|
|
(fun op env -> DE.add_value env op delay_binary_poly_op)
|
| 106 |
|
|
[
|
| 107 |
|
|
"+";
|
| 108 |
|
|
"-";
|
| 109 |
|
|
"*";
|
| 110 |
|
|
"/";
|
| 111 |
|
|
"mod";
|
| 112 |
|
|
"&&";
|
| 113 |
|
|
"||";
|
| 114 |
|
|
"xor";
|
| 115 |
|
|
"equi";
|
| 116 |
|
|
"impl";
|
| 117 |
|
|
"<";
|
| 118 |
|
|
"<=";
|
| 119 |
|
|
">";
|
| 120 |
|
|
">=";
|
| 121 |
|
|
"!=";
|
| 122 |
|
|
"=";
|
| 123 |
|
|
]
|
| 124 |
|
|
env'
|
| 125 |
|
|
in
|
| 126 |
e9b71779
|
tkahsai
|
let env' =
|
| 127 |
ca7ff3f7
|
Lélio Brun
|
List.fold_right
|
| 128 |
|
|
(fun op env -> DE.add_value env op delay_ternary_poly_op)
|
| 129 |
|
|
[] env'
|
| 130 |
|
|
in
|
| 131 |
22fe1c93
|
ploc
|
env'
|
| 132 |
|
|
|
| 133 |
|
|
module VE = Env
|
| 134 |
|
|
|
| 135 |
2d2d89d7
|
ploc
|
let eval_dim_env =
|
| 136 |
ca7ff3f7
|
Lélio Brun
|
let defs =
|
| 137 |
|
|
[
|
| 138 |
|
|
("uminus", function [ Dint a ] -> Dint (-a) | _ -> assert false);
|
| 139 |
|
|
("not", function [ Dbool b ] -> Dbool (not b) | _ -> assert false);
|
| 140 |
|
|
("+", function [ Dint a; Dint b ] -> Dint (a + b) | _ -> assert false);
|
| 141 |
|
|
("-", function [ Dint a; Dint b ] -> Dint (a - b) | _ -> assert false);
|
| 142 |
|
|
("*", function [ Dint a; Dint b ] -> Dint (a * b) | _ -> assert false);
|
| 143 |
|
|
("/", function [ Dint a; Dint b ] -> Dint (a / b) | _ -> assert false);
|
| 144 |
|
|
( "mod",
|
| 145 |
|
|
function [ Dint a; Dint b ] -> Dint (a mod b) | _ -> assert false );
|
| 146 |
|
|
( "&&",
|
| 147 |
|
|
function [ Dbool a; Dbool b ] -> Dbool (a && b) | _ -> assert false );
|
| 148 |
|
|
( "||",
|
| 149 |
|
|
function [ Dbool a; Dbool b ] -> Dbool (a || b) | _ -> assert false );
|
| 150 |
|
|
( "xor",
|
| 151 |
|
|
function [ Dbool a; Dbool b ] -> Dbool (a <> b) | _ -> assert false );
|
| 152 |
|
|
( "equi",
|
| 153 |
|
|
function [ Dbool a; Dbool b ] -> Dbool (a = b) | _ -> assert false );
|
| 154 |
|
|
( "impl",
|
| 155 |
|
|
function [ Dbool a; Dbool b ] -> Dbool (a <= b) | _ -> assert false );
|
| 156 |
|
|
("<", function [ Dint a; Dint b ] -> Dbool (a < b) | _ -> assert false);
|
| 157 |
|
|
(">", function [ Dint a; Dint b ] -> Dbool (a > b) | _ -> assert false);
|
| 158 |
|
|
("<=", function [ Dint a; Dint b ] -> Dbool (a <= b) | _ -> assert false);
|
| 159 |
|
|
(">=", function [ Dint a; Dint b ] -> Dbool (a >= b) | _ -> assert false);
|
| 160 |
|
|
("!=", function [ a; b ] -> Dbool (a <> b) | _ -> assert false);
|
| 161 |
|
|
("=", function [ a; b ] -> Dbool (a = b) | _ -> assert false);
|
| 162 |
|
|
]
|
| 163 |
5c1184ad
|
ploc
|
in
|
| 164 |
e9b71779
|
tkahsai
|
List.fold_left
|
| 165 |
5c1184ad
|
ploc
|
(fun env (op, op_eval) -> VE.add_value env op op_eval)
|
| 166 |
ca7ff3f7
|
Lélio Brun
|
VE.initial defs
|
| 167 |
|
|
|
| 168 |
|
|
let arith_funs = [ "+"; "-"; "*"; "/"; "mod"; "uminus" ]
|
| 169 |
22fe1c93
|
ploc
|
|
| 170 |
ca7ff3f7
|
Lélio Brun
|
let bool_funs = [ "&&"; "||"; "xor"; "equi"; "impl"; "not" ]
|
| 171 |
|
|
|
| 172 |
|
|
let rel_funs = [ "<"; ">"; "<="; ">="; "!="; "=" ]
|
| 173 |
|
|
|
| 174 |
|
|
let internal_funs = arith_funs @ bool_funs @ rel_funs
|
| 175 |
719f9992
|
xthirioux
|
|
| 176 |
04a63d25
|
xthirioux
|
let rec is_internal_fun x targs =
|
| 177 |
ca7ff3f7
|
Lélio Brun
|
(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*)
|
| 178 |
04a63d25
|
xthirioux
|
match targs with
|
| 179 |
ca7ff3f7
|
Lélio Brun
|
| [] ->
|
| 180 |
|
|
assert false
|
| 181 |
|
|
| t :: _ when Types.is_real_type t ->
|
| 182 |
|
|
List.mem x internal_funs && not !Options.mpfr
|
| 183 |
|
|
| t :: _ when Types.is_array_type t ->
|
| 184 |
|
|
is_internal_fun x [ Types.array_element_type t ]
|
| 185 |
|
|
| _ ->
|
| 186 |
|
|
List.mem x internal_funs
|
| 187 |
04a63d25
|
xthirioux
|
|
| 188 |
|
|
let is_expr_internal_fun expr =
|
| 189 |
8446bf03
|
ploc
|
let open Lustre_types in
|
| 190 |
04a63d25
|
xthirioux
|
match expr.expr_desc with
|
| 191 |
ca7ff3f7
|
Lélio Brun
|
| Expr_appl (f, e, _) ->
|
| 192 |
|
|
is_internal_fun f (Types.type_list_of_type e.expr_type)
|
| 193 |
|
|
| _ ->
|
| 194 |
|
|
assert false
|
| 195 |
04a63d25
|
xthirioux
|
|
| 196 |
|
|
let is_value_internal_fun v =
|
| 197 |
8446bf03
|
ploc
|
let open Machine_code_types in
|
| 198 |
04a63d25
|
xthirioux
|
match v.value_desc with
|
| 199 |
ca7ff3f7
|
Lélio Brun
|
| Fun (f, vl) ->
|
| 200 |
|
|
is_internal_fun f (List.map (fun v -> v.value_type) vl)
|
| 201 |
|
|
| _ ->
|
| 202 |
|
|
assert false
|
| 203 |
53206908
|
xthirioux
|
|
| 204 |
ca7ff3f7
|
Lélio Brun
|
let is_numeric_operator x = List.mem x arith_funs
|
| 205 |
04a63d25
|
xthirioux
|
|
| 206 |
ca7ff3f7
|
Lélio Brun
|
let is_homomorphic_fun x = List.mem x internal_funs
|
| 207 |
22fe1c93
|
ploc
|
|
| 208 |
ca7ff3f7
|
Lélio Brun
|
let is_stateless_fun x = List.mem x internal_funs
|
| 209 |
ea8f51ae
|
ploc
|
|
| 210 |
|
|
(* let pp_java i pp_val fmt vl = *)
|
| 211 |
|
|
(* match i, vl with *)
|
| 212 |
ca7ff3f7
|
Lélio Brun
|
(* (\* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1
|
| 213 |
|
|
pp_val v2 pp_val v3 *\) *)
|
| 214 |
ea8f51ae
|
ploc
|
(* | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *)
|
| 215 |
|
|
(* | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *)
|
| 216 |
ca7ff3f7
|
Lélio Brun
|
(* | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *)
|
| 217 |
|
|
(* | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
|
| 218 |
|
|
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *)
|
| 219 |
|
|
(* | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
|
| 220 |
|
|
(* | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *)
|
| 221 |
|
|
(* | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *)
|
| 222 |
|
|
(* | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert
|
| 223 |
|
|
false) *)
|
| 224 |
ea8f51ae
|
ploc
|
|
| 225 |
ca7e8027
|
Lélio Brun
|
let partial_eval op e opt =
|
| 226 |
2d2d89d7
|
ploc
|
let open Lustre_types in
|
| 227 |
|
|
let is_zero e =
|
| 228 |
|
|
match e.expr_desc with
|
| 229 |
ca7ff3f7
|
Lélio Brun
|
| Expr_const (Const_int 0) ->
|
| 230 |
|
|
true
|
| 231 |
|
|
| Expr_const (Const_real r) when Real.is_zero r ->
|
| 232 |
|
|
true
|
| 233 |
|
|
| _ ->
|
| 234 |
|
|
false
|
| 235 |
2d2d89d7
|
ploc
|
in
|
| 236 |
|
|
let is_one e =
|
| 237 |
|
|
match e.expr_desc with
|
| 238 |
ca7ff3f7
|
Lélio Brun
|
| Expr_const (Const_int 1) ->
|
| 239 |
|
|
true
|
| 240 |
|
|
| Expr_const (Const_real r) when Real.is_one r ->
|
| 241 |
|
|
true
|
| 242 |
|
|
| _ ->
|
| 243 |
|
|
false
|
| 244 |
2d2d89d7
|
ploc
|
in
|
| 245 |
|
|
let is_true, is_false =
|
| 246 |
|
|
let is_tag t e = e.expr_desc = Expr_const (Const_tag t) in
|
| 247 |
|
|
is_tag tag_true, is_tag tag_false
|
| 248 |
|
|
in
|
| 249 |
ca7ff3f7
|
Lélio Brun
|
let int_arith_op, real_arith_op =
|
| 250 |
|
|
let assoc op =
|
| 251 |
2d2d89d7
|
ploc
|
match op with
|
| 252 |
ca7ff3f7
|
Lélio Brun
|
| "+" ->
|
| 253 |
|
|
( + ), Real.add
|
| 254 |
|
|
| "-" ->
|
| 255 |
|
|
( - ), Real.minus
|
| 256 |
|
|
| "*" ->
|
| 257 |
|
|
( * ), Real.times
|
| 258 |
|
|
| "/" ->
|
| 259 |
|
|
( / ), Real.div
|
| 260 |
|
|
| "mod" ->
|
| 261 |
|
|
( mod ), fun _ _ -> assert false
|
| 262 |
|
|
| _ ->
|
| 263 |
|
|
assert false
|
| 264 |
2d2d89d7
|
ploc
|
in
|
| 265 |
ca7ff3f7
|
Lélio Brun
|
(fun op -> fst (assoc op)), fun op -> snd (assoc op)
|
| 266 |
2d2d89d7
|
ploc
|
in
|
| 267 |
|
|
let int_rel_op, real_rel_op =
|
| 268 |
|
|
let assoc op =
|
| 269 |
|
|
match op with
|
| 270 |
ca7ff3f7
|
Lélio Brun
|
| "<" ->
|
| 271 |
|
|
( < ), Real.lt
|
| 272 |
|
|
| ">" ->
|
| 273 |
|
|
( > ), Real.gt
|
| 274 |
|
|
| "<=" ->
|
| 275 |
|
|
( <= ), Real.le
|
| 276 |
|
|
| ">=" ->
|
| 277 |
|
|
( >= ), Real.ge
|
| 278 |
|
|
| "!=" ->
|
| 279 |
|
|
( != ), Real.diseq
|
| 280 |
|
|
| "=" ->
|
| 281 |
|
|
( = ), Real.eq
|
| 282 |
|
|
| _ ->
|
| 283 |
|
|
assert false
|
| 284 |
2d2d89d7
|
ploc
|
in
|
| 285 |
ca7ff3f7
|
Lélio Brun
|
(fun op -> fst (assoc op)), fun op -> snd (assoc op)
|
| 286 |
2d2d89d7
|
ploc
|
in
|
| 287 |
ca7ff3f7
|
Lélio Brun
|
let eval_bool_fun op e1 e2 =
|
| 288 |
|
|
let s2b s =
|
| 289 |
|
|
if s = tag_true then true
|
| 290 |
|
|
else if s = tag_false then false
|
| 291 |
|
|
else assert false
|
| 292 |
|
|
in
|
| 293 |
2d2d89d7
|
ploc
|
let e1, e2 = s2b e1, s2b e2 in
|
| 294 |
|
|
let r =
|
| 295 |
|
|
match op with
|
| 296 |
ca7ff3f7
|
Lélio Brun
|
| "&&" ->
|
| 297 |
|
|
e1 && e2
|
| 298 |
|
|
| "||" ->
|
| 299 |
|
|
e1 || e2
|
| 300 |
|
|
| "xor" ->
|
| 301 |
|
|
(e1 && e2) || ((not e1) && not e2)
|
| 302 |
|
|
| "impl" ->
|
| 303 |
|
|
(not e1) || e2
|
| 304 |
|
|
| "equi" ->
|
| 305 |
|
|
((not e1) || e2) && ((not e2) || e1)
|
| 306 |
|
|
| _ ->
|
| 307 |
|
|
assert false
|
| 308 |
2d2d89d7
|
ploc
|
in
|
| 309 |
|
|
if r then Const_tag tag_true else Const_tag tag_false
|
| 310 |
|
|
in
|
| 311 |
ca7ff3f7
|
Lélio Brun
|
let is_const e = match e.expr_desc with Expr_const _ -> true | _ -> false in
|
| 312 |
2d2d89d7
|
ploc
|
let deconst e =
|
| 313 |
ca7ff3f7
|
Lélio Brun
|
match e.expr_desc with Expr_const c -> c | _ -> assert false
|
| 314 |
2d2d89d7
|
ploc
|
in
|
| 315 |
ca7ff3f7
|
Lélio Brun
|
match op, match e.expr_desc with Expr_tuple el -> el | _ -> [ e ] with
|
| 316 |
|
|
| _, el when List.for_all is_const el ->
|
| 317 |
|
|
let new_cst =
|
| 318 |
2d2d89d7
|
ploc
|
match op, List.map deconst el with
|
| 319 |
ca7ff3f7
|
Lélio Brun
|
| ("+" | "-" | "*" | "/" | "mod"), [ Const_int c1; Const_int c2 ] ->
|
| 320 |
|
|
Const_int (int_arith_op op c1 c2)
|
| 321 |
|
|
| ("+" | "-" | "*" | "/"), [ Const_real c1; Const_real c2 ] ->
|
| 322 |
|
|
Const_real (real_arith_op op c1 c2)
|
| 323 |
|
|
| "uminus", [ Const_int c ] ->
|
| 324 |
|
|
Const_int (-c)
|
| 325 |
|
|
| "uminus", [ Const_real c ] ->
|
| 326 |
|
|
Const_real (Real.uminus c)
|
| 327 |
|
|
| rel_fun, [ Const_int c1; Const_int c2 ] when List.mem rel_fun rel_funs
|
| 328 |
|
|
->
|
| 329 |
|
|
if int_rel_op op c1 c2 then Const_tag tag_true else Const_tag tag_false
|
| 330 |
|
|
| rel_fun, [ Const_real c1; Const_real c2 ] when List.mem rel_fun rel_funs
|
| 331 |
|
|
->
|
| 332 |
|
|
if real_rel_op op c1 c2 then Const_tag tag_true else Const_tag tag_false
|
| 333 |
|
|
| "=", [ Const_tag t1; Const_tag t2 ] ->
|
| 334 |
|
|
if t1 = t2 then Const_tag tag_true else Const_tag tag_false
|
| 335 |
|
|
| "!=", [ Const_tag t1; Const_tag t2 ] ->
|
| 336 |
|
|
if t1 = t2 then Const_tag tag_false else Const_tag tag_true
|
| 337 |
|
|
| "not", [ Const_tag c ] ->
|
| 338 |
|
|
Const_tag
|
| 339 |
|
|
(if c = tag_true then tag_false
|
| 340 |
|
|
else if c = tag_false then tag_true
|
| 341 |
|
|
else assert false)
|
| 342 |
|
|
| bool_fun, [ Const_tag c1; Const_tag c2 ]
|
| 343 |
|
|
when List.mem bool_fun bool_funs ->
|
| 344 |
|
|
eval_bool_fun bool_fun c1 c2
|
| 345 |
|
|
| _ ->
|
| 346 |
|
|
let loc = e.expr_loc in
|
| 347 |
|
|
let err =
|
| 348 |
|
|
Error.Unbound_symbol
|
| 349 |
|
|
(op ^ string_of_bool (List.mem op rel_funs) ^ " in basic library")
|
| 350 |
|
|
in
|
| 351 |
|
|
raise (Error.Error (loc, err))
|
| 352 |
2d2d89d7
|
ploc
|
in
|
| 353 |
ca7ff3f7
|
Lélio Brun
|
Expr_const new_cst
|
| 354 |
|
|
| op, el -> (
|
| 355 |
|
|
(* at least one of the arguments is non constant *)
|
| 356 |
2d2d89d7
|
ploc
|
match op, el with
|
| 357 |
ca7ff3f7
|
Lélio Brun
|
| "+", [ e0; e ] when is_zero e0 ->
|
| 358 |
|
|
e.expr_desc
|
| 359 |
|
|
| "+", [ e; e0 ] when is_zero e0 ->
|
| 360 |
|
|
e.expr_desc
|
| 361 |
|
|
| "-", [ e; e0 ] when is_zero e0 ->
|
| 362 |
|
|
e.expr_desc
|
| 363 |
|
|
| "-", [ e0; e ] when is_zero e0 ->
|
| 364 |
|
|
Expr_appl ("uminus", e, None)
|
| 365 |
|
|
| ("*" | "/"), [ e0; _ ] when is_zero e0 ->
|
| 366 |
|
|
e0.expr_desc
|
| 367 |
|
|
| "*", [ _; e0 ] when is_zero e0 ->
|
| 368 |
|
|
e0.expr_desc
|
| 369 |
|
|
| "*", [ e1; e ] when is_one e1 ->
|
| 370 |
|
|
e.expr_desc
|
| 371 |
|
|
| "/", [ e; e1 ] when is_one e1 ->
|
| 372 |
|
|
e.expr_desc
|
| 373 |
|
|
| "&&", [ efalse; _ ] when is_false efalse ->
|
| 374 |
|
|
Expr_const (Const_tag tag_false)
|
| 375 |
|
|
| "&&", [ _; efalse ] when is_false efalse ->
|
| 376 |
|
|
Expr_const (Const_tag tag_false)
|
| 377 |
|
|
| "||", [ etrue; _ ] when is_true etrue ->
|
| 378 |
|
|
Expr_const (Const_tag tag_true)
|
| 379 |
|
|
| "||", [ _; etrue ] when is_true etrue ->
|
| 380 |
|
|
Expr_const (Const_tag tag_true)
|
| 381 |
|
|
| "impl", [ efalse; _ ] when is_false efalse ->
|
| 382 |
|
|
Expr_const (Const_tag tag_true)
|
| 383 |
2d2d89d7
|
ploc
|
| _ ->
|
| 384 |
ca7ff3f7
|
Lélio Brun
|
Expr_appl (op, e, opt))
|
| 385 |
04a188ec
|
ploc
|
|
| 386 |
ca7ff3f7
|
Lélio Brun
|
(* Local Variables: *)
|
| 387 |
|
|
(* compile-command:"make -C .." *)
|
| 388 |
|
|
(* End: *)
|
| 389 |
04a188ec
|
ploc
|
|
| 390 |
|
|
let _ =
|
| 391 |
|
|
(* Loading environement *)
|
| 392 |
|
|
Global.type_env := type_env;
|
| 393 |
|
|
Global.clock_env := clock_env
|