@@ -43,10 +43,10 @@ and expr =
4343 | Dfalse
4444 | Dlit of float
4545 | Dvar of expr_var
46- | Dand of expr * expr
47- | Dor of expr * expr
46+ | Dand of expr list
47+ | Dor of expr list
4848 | Dunop of string * expr
49- | Dbinop of string * expr * expr
49+ | Dbinop of string * expr list
5050 | Dfun of string * expr list
5151 | Dite of expr * expr * expr
5252 | Dinstr of string
@@ -74,7 +74,7 @@ let cast (kind : dflag) (expr : expr) =
7474 | Dfalse , Val -> Dlit 0.
7575 | Dlit 0. , Def -> Dfalse
7676 | Dlit _ , Def -> Dtrue
77- | _ , Def -> Dbinop (" !=" , expr, Dlit 0. )
77+ | _ , Def -> Dbinop (" !=" , [ expr; Dlit 0. ] )
7878 | _ , Val -> expr
7979
8080(* * local stacks operations *)
@@ -106,7 +106,7 @@ let rec expr_position (expr : expr) (st : local_stacks) =
106106 if is_in_stack_scope slot st then Not_to_stack
107107 else if is_on_top slot st then On_top slot.kind
108108 else Must_be_pushed
109- | Dbinop ("/" , e1 , e2 ) -> begin
109+ | Dbinop ("/" , [ e1 ; e2 ] ) -> begin
110110 (* avoid storage of division by zero. It assumes all division are
111111 guarded *)
112112 match (expr_position e1 st, expr_position e2 st) with
@@ -115,6 +115,9 @@ let rec expr_position (expr : expr) (st : local_stacks) =
115115 (* Needed to bumb the stack to avoid erasing subexpressions *)
116116 | _ , _ -> Not_to_stack (* Either already stored, or duplicatable *)
117117 end
118+ | Dbinop ("/" , l ) ->
119+ Format. ksprintf Errors. raise_error " Invalid arity for division (%i)"
120+ (List. length l)
118121 | Ddirect _ -> Not_to_stack
119122 | _ -> Must_be_pushed
120123
@@ -217,42 +220,111 @@ let local_var (lvar : local_var) (stacks : local_stacks) (ctx : local_vars) : t
217220 the point at which the constructed expression is expected to be allocated (if
218221 needed). *)
219222
223+ let dand' (e1 , lv1 ) (e2 , lv2 ) =
224+ match (e1, e2) with
225+ | Dtrue , _ -> (e2, lv2)
226+ | _ , Dtrue -> (e1, lv1)
227+ | Dfalse , _ | _ , Dfalse -> (Dfalse , [] )
228+ | Dvar v1 , Dvar v2 when v1 = v2 -> (e1, lv1)
229+ | Dand l , Dand l' -> (Dand (l @ l'), lv2 @ lv1)
230+ | Dand l , _ -> (Dand (l @ [ e2 ]), lv2 @ lv1)
231+ | _ , Dand l -> (Dand (e1 :: l), lv2 @ lv1)
232+ | _ -> (Dand [ e1; e2 ], lv2 @ lv1)
233+
234+ let dor' (e1 , lv1 ) (e2 , lv2 ) =
235+ match (e1, e2) with
236+ | Dtrue , _ | _ , Dtrue -> (Dtrue , [] )
237+ | Dfalse , _ -> (e2, lv2)
238+ | _ , Dfalse -> (e1, lv1)
239+ | Dvar v1 , Dvar v2 when v1 = v2 -> (e1, lv1)
240+ | Dor l , Dor l' -> (Dor (l @ l'), lv2 @ lv1)
241+ | Dor l , _ -> (Dor (l @ [ e2 ]), lv2 @ lv1)
242+ | _ , Dor l -> (Dor (e1 :: l), lv2 @ lv1)
243+ | _ -> (Dor [ e1; e2 ], lv2 @ lv1)
244+
245+ let dnot' (e , lv ) =
246+ match e with
247+ | Dtrue -> (Dfalse , [] )
248+ | Dfalse -> (Dtrue , [] )
249+ | Dunop ("!" , e ) -> (e, lv)
250+ | _ -> (Dunop (" !" , e), lv)
251+
252+ let minus' (e , lv ) =
253+ match e with
254+ | Dlit f -> (Dlit (-. f), [] )
255+ | Dunop ("-" , e ) -> (e, lv)
256+ | _ -> (Dunop (" -" , e), lv)
257+
258+ let plus' ?(reduce_zero_add = false ) (e1 , lv1 ) (e2 , lv2 ) =
259+ match (e1, e2) with
260+ | Dlit 0. , _ when reduce_zero_add -> (e2, lv2)
261+ | _ , Dlit 0. when reduce_zero_add -> (e1, lv1)
262+ | Dlit f1 , Dlit f2 -> (Dlit (f1 +. f2), [] )
263+ | Dbinop ("+" , l ), Dbinop ("+" , l' ) -> (Dbinop (" +" , l @ l'), lv2 @ lv1)
264+ | Dbinop ("+" , l ), _ -> (Dbinop (" +" , l @ [ e2 ]), lv2 @ lv1)
265+ | _ , Dbinop ("+" , l ) -> (Dbinop (" +" , e1 :: l), lv2 @ lv1)
266+ | _ -> (Dbinop (" +" , [ e1; e2 ]), lv2 @ lv1)
267+
268+ let sub' (e1 , lv1 ) (e2 , lv2 ) =
269+ match (e1, e2) with
270+ | Dlit 0. , _ -> (Dunop (" -" , e2), lv2)
271+ | _ , Dlit 0. -> (e1, lv1)
272+ | Dlit f1 , Dlit f2 -> (Dlit (f1 -. f2), [] )
273+ | _ , Dunop ("-" , e2 ) -> plus' (e1, lv1) (e2, lv2)
274+ | Dbinop ("-" , l ), Dbinop ("+" , l' ) -> (Dbinop (" -" , l @ l'), lv2 @ lv1)
275+ | Dbinop ("-" , l ), e -> (Dbinop (" -" , l @ [ e ]), lv2 @ lv1)
276+ | _ -> (Dbinop (" -" , [ e1; e2 ]), lv2 @ lv1)
277+
278+ let mult' (e1 , lv1 ) (e2 , lv2 ) =
279+ match (e1, e2) with
280+ | Dlit 1. , _ -> (e2, lv2)
281+ | _ , Dlit 1. -> (e1, lv1)
282+ | Dlit 0. , _ | _ , Dlit 0. -> (Dlit 0. , [] )
283+ | Dlit f1 , Dlit f2 -> (Dlit (f1 *. f2), [] )
284+ | Dbinop ("*" , l ), Dbinop ("*" , l' ) -> (Dbinop (" *" , l @ l'), lv2 @ lv1)
285+ | Dbinop ("*" , l ), _ -> (Dbinop (" *" , l @ [ e2 ]), lv2 @ lv1)
286+ | _ , Dbinop ("*" , l ) -> (Dbinop (" *" , e1 :: l), lv2 @ lv1)
287+ | _ -> (Dbinop (" *" , [ e1; e2 ]), lv2 @ lv1)
288+
289+ let div' (e1 , lv1 ) (e2 , lv2 ) =
290+ match (e1, e2) with
291+ | _ , Dlit 1. -> (e1, lv1)
292+ | Dlit f1 , Dlit f2 ->
293+ let f = f1 /. f2 in
294+ (Dlit f, [] )
295+ | _ -> (Dbinop (" /" , [ e1; e2 ]), lv2 @ lv1)
296+
297+ let modulo' (e1 , lv1 ) (e2 , lv2 ) =
298+ match (e1, e2) with
299+ | _ , Dlit 1. -> (e1, lv1)
300+ | Dlit f1 , Dlit f2 ->
301+ let f = mod_float f1 f2 in
302+ (Dlit f, [] )
303+ | _ -> (Dfun (" fmod" , [ e1; e2 ]), lv2 @ lv1)
304+
220305let dand (e1 : constr ) (e2 : constr ) (stacks : local_stacks ) (ctx : local_vars )
221306 : t =
222307 let stacks', lv1, e1 = push_with_kind stacks ctx Def e1 in
223308 let _, lv2, e2 = push_with_kind stacks' ctx Def e2 in
224- match (e1, e2) with
225- | Dtrue , _ -> (e2, Def , lv2)
226- | _ , Dtrue -> (e1, Def , lv1)
227- | Dfalse , _ | _ , Dfalse -> (Dfalse , Def , [] )
228- | Dvar v1 , Dvar v2 when v1 = v2 -> (e1, Def , lv1)
229- | _ -> (Dand (e1, e2), Def , lv2 @ lv1)
309+ let e, l = dand' (e1, lv1) (e2, lv2) in
310+ (e, Def , l)
230311
231312let dor (e1 : constr ) (e2 : constr ) (stacks : local_stacks ) (ctx : local_vars ) :
232313 t =
233314 let stacks', lv1, e1 = push_with_kind stacks ctx Def e1 in
234315 let _, lv2, e2 = push_with_kind stacks' ctx Def e2 in
235- match (e1, e2) with
236- | Dtrue , _ | _ , Dtrue -> (Dtrue , Def , [] )
237- | Dfalse , _ -> (e2, Def , lv2)
238- | _ , Dfalse -> (e1, Def , lv1)
239- | Dvar v1 , Dvar v2 when v1 = v2 -> (e1, Def , lv1)
240- | _ -> (Dor (e1, e2), Def , lv2 @ lv1)
316+ let e, l = dor' (e1, lv1) (e2, lv2) in
317+ (e, Def , l)
241318
242319let dnot (e : constr ) (stacks : local_stacks ) (ctx : local_vars ) : t =
243320 let _, lv, e = push_with_kind stacks ctx Def e in
244- match e with
245- | Dtrue -> (Dfalse , Def , [] )
246- | Dfalse -> (Dtrue , Def , [] )
247- | Dunop ("!" , e ) -> (e, Def , lv)
248- | _ -> (Dunop (" !" , e), Def , lv)
321+ let e, lv = dnot' (e, lv) in
322+ (e, Def , lv)
249323
250324let minus (e : constr ) (stacks : local_stacks ) (ctx : local_vars ) : t =
251325 let _, lv, e = push_with_kind stacks ctx Val e in
252- match e with
253- | Dlit f -> (Dlit (-. f), Val , [] )
254- | Dunop ("-" , e ) -> (e, Val , lv)
255- | _ -> (Dunop (" -" , e), Val , lv)
326+ let e, lv = minus' (e, lv) in
327+ (e, Val , lv)
256328
257329let plus (e1 : constr ) (e2 : constr ) (stacks : local_stacks ) (ctx : local_vars )
258330 : t =
@@ -261,54 +333,36 @@ let plus (e1 : constr) (e2 : constr) (stacks : local_stacks) (ctx : local_vars)
261333 let reduce_zero_add = false in
262334 let stacks', lv1, e1 = push_with_kind stacks ctx Val e1 in
263335 let _, lv2, e2 = push_with_kind stacks' ctx Val e2 in
264- match (e1, e2) with
265- | Dlit 0. , _ when reduce_zero_add -> (e2, Val , lv2)
266- | _ , Dlit 0. when reduce_zero_add -> (e1, Val , lv1)
267- | Dlit f1 , Dlit f2 -> (Dlit (f1 +. f2), Val , [] )
268- | _ -> (Dbinop (" +" , e1, e2), Val , lv2 @ lv1)
336+ let e, lv = plus' ~reduce_zero_add (e1, lv1) (e2, lv2) in
337+ (e, Val , lv)
269338
270339let sub (e1 : constr ) (e2 : constr ) (stacks : local_stacks ) (ctx : local_vars ) :
271340 t =
272341 let stacks', lv1, e1 = push_with_kind stacks ctx Val e1 in
273342 let _, lv2, e2 = push_with_kind stacks' ctx Val e2 in
274- match (e1, e2) with
275- | Dlit 0. , _ -> (Dunop (" -" , e2), Val , lv2)
276- | _ , Dlit 0. -> (e1, Val , lv1)
277- | Dlit f1 , Dlit f2 -> (Dlit (f1 -. f2), Val , [] )
278- | _ -> (Dbinop (" -" , e1, e2), Val , lv2 @ lv1)
343+ let e, lv = sub' (e1, lv1) (e2, lv2) in
344+ (e, Val , lv)
279345
280346let mult (e1 : constr ) (e2 : constr ) (stacks : local_stacks ) (ctx : local_vars )
281347 : t =
282348 let stacks', lv1, e1 = push_with_kind stacks ctx Val e1 in
283349 let _, lv2, e2 = push_with_kind stacks' ctx Val e2 in
284- match (e1, e2) with
285- | Dlit 1. , _ -> (e2, Val , lv2)
286- | _ , Dlit 1. -> (e1, Val , lv1)
287- | Dlit 0. , _ | _ , Dlit 0. -> (Dlit 0. , Val , [] )
288- | Dlit f1 , Dlit f2 -> (Dlit (f1 *. f2), Val , [] )
289- | _ -> (Dbinop (" *" , e1, e2), Val , lv2 @ lv1)
350+ let e, lv = mult' (e1, lv1) (e2, lv2) in
351+ (e, Val , lv)
290352
291353let div (e1 : constr ) (e2 : constr ) (stacks : local_stacks ) (ctx : local_vars ) :
292354 t =
293355 let stacks', lv1, e1 = push_with_kind stacks ctx Val e1 in
294356 let _, lv2, e2 = push_with_kind stacks' ctx Val e2 in
295- match (e1, e2) with
296- | _ , Dlit 1. -> (e1, Val , lv1)
297- | Dlit f1 , Dlit f2 ->
298- let f = f1 /. f2 in
299- (Dlit f, Val , [] )
300- | _ -> (Dbinop (" /" , e1, e2), Val , lv2 @ lv1)
357+ let e, lv = div' (e1, lv1) (e2, lv2) in
358+ (e, Val , lv)
301359
302360let modulo (e1 : constr ) (e2 : constr ) (stacks : local_stacks )
303361 (ctx : local_vars ) : t =
304362 let stacks', lv1, e1 = push_with_kind stacks ctx Val e1 in
305363 let _, lv2, e2 = push_with_kind stacks' ctx Val e2 in
306- match (e1, e2) with
307- | _ , Dlit 1. -> (e1, Val , lv1)
308- | Dlit f1 , Dlit f2 ->
309- let f = mod_float f1 f2 in
310- (Dlit f, Val , [] )
311- | _ -> (Dfun (" fmod" , [ e1; e2 ]), Val , lv2 @ lv1)
364+ let e, lv = modulo' (e1, lv1) (e2, lv2) in
365+ (e, Val , lv)
312366
313367let comp op (e1 : constr ) (e2 : constr ) (stacks : local_stacks )
314368 (ctx : local_vars ) : t =
@@ -324,8 +378,9 @@ let comp op (e1 : constr) (e2 : constr) (stacks : local_stacks)
324378 then Dtrue
325379 else Dfalse
326380 | Dvar v1 , Dvar v2 ->
327- if String. equal op " ==" && v1 = v2 then Dtrue else Dbinop (op, e1, e2)
328- | _ -> Dbinop (op, e1, e2)
381+ if String. equal op " ==" && v1 = v2 then Dtrue
382+ else Dbinop (op, [ e1; e2 ])
383+ | _ -> Dbinop (op, [ e1; e2 ])
329384 in
330385 let e =
331386 match op with
@@ -368,8 +423,8 @@ let ite (c : constr) (t : constr) (e : constr) (stacks : local_stacks)
368423 else (* this will happen. Staying on the safe side *) Val
369424 in
370425 match (c, t, e) with
371- | Dtrue , _ , _ -> (t, tkind, lvt )
372- | Dfalse , _ , _ -> (e, ekind, lve )
426+ | ( Dfalse | Dlit 0. ) , _ , _ -> (e, ekind, lve )
427+ | ( Dtrue | Dlit _ ) , _ , _ -> (t, tkind, lvt )
373428 | _ , Dtrue , Dtrue | _ , Dfalse , Dfalse -> (t, tkind, lvt)
374429 | _ , Dlit 1. , Dlit 0. -> (c, Def , lvc)
375430 | _ , Dlit f , Dlit f' when f = f' -> (Dlit f, ite_kind, [] )
@@ -449,7 +504,12 @@ let format_expr_var (dgfip_flags : Dgfip_options.flags) fmt (ev : expr_var) =
449504 (generate_variable ~trace_flag: dgfip_flags.flg_trace ~def_flag m_sp_opt
450505 var)
451506
452- let rec format_dexpr (dgfip_flags : Dgfip_options.flags ) fmt (de : expr ) =
507+ let rec format_dexpr_list (dgfip_flags : Dgfip_options.flags ) ~sep =
508+ Format. pp_print_list
509+ ~pp_sep: (fun fmt _ -> Format. fprintf fmt " %s " sep)
510+ (format_dexpr dgfip_flags)
511+
512+ and format_dexpr (dgfip_flags : Dgfip_options.flags ) fmt (de : expr ) =
453513 let format_dexpr = format_dexpr dgfip_flags in
454514 match de with
455515 | Dtrue -> Format. fprintf fmt " 1"
@@ -463,36 +523,39 @@ let rec format_dexpr (dgfip_flags : Dgfip_options.flags) fmt (de : expr) =
463523 (* Print literal floats as precisely as possible *)
464524 Format. fprintf fmt " %#.19g" f)
465525 | Dvar evar -> format_expr_var dgfip_flags fmt evar
466- | Dand (de1 , de2 ) ->
467- Format. fprintf fmt " @[<hov 2>(%a@ && %a@])" format_dexpr de1 format_dexpr
468- de2
469- | Dor (de1 , de2 ) ->
470- Format. fprintf fmt " @[<hov 2>(%a@ || %a@])" format_dexpr de1 format_dexpr
471- de2
526+ | Dand l ->
527+ Format. fprintf fmt " @[<hov 2>(%a@])"
528+ (format_dexpr_list dgfip_flags ~sep: " &&" )
529+ l
530+ | Dor l ->
531+ Format. fprintf fmt " @[<hov 2>(%a@])"
532+ (format_dexpr_list dgfip_flags ~sep: " ||" )
533+ l
472534 | Dunop (op , de ) -> Format. fprintf fmt " @[<hov 2>(%s%a@])" op format_dexpr de
473- | Dbinop (op , de1 , de2 ) -> begin
474- match op with
475- | ">" ->
535+ | Dbinop (op , l ) -> begin
536+ match (op, l) with
537+ | ">" , [ de1; de2 ] ->
476538 Format. fprintf fmt " @[<hov 2>(GT_E((%a),(%a))@])" format_dexpr de1
477539 format_dexpr de2
478- | "<" ->
540+ | "<" , [ de1; de2 ] ->
479541 Format. fprintf fmt " @[<hov 2>(LT_E((%a),(%a))@])" format_dexpr de1
480542 format_dexpr de2
481- | ">=" ->
543+ | ">=" , [ de1; de2 ] ->
482544 Format. fprintf fmt " @[<hov 2>(GE_E((%a),(%a))@])" format_dexpr de1
483545 format_dexpr de2
484- | "<=" ->
546+ | "<=" , [ de1; de2 ] ->
485547 Format. fprintf fmt " @[<hov 2>(LE_E((%a),(%a))@])" format_dexpr de1
486548 format_dexpr de2
487- | "==" ->
549+ | "==" , [ de1; de2 ] ->
488550 Format. fprintf fmt " @[<hov 2>(EQ_E((%a),(%a))@])" format_dexpr de1
489551 format_dexpr de2
490- | "!=" ->
552+ | "!=" , [ de1; de2 ] ->
491553 Format. fprintf fmt " @[<hov 2>(NEQ_E((%a),(%a))@])" format_dexpr de1
492554 format_dexpr de2
493555 | _ ->
494- Format. fprintf fmt " @[<hov 2>((%a)@ %s (%a)@])" format_dexpr de1 op
495- format_dexpr de2
556+ Format. fprintf fmt " @[<hov 2>(%a@])"
557+ (format_dexpr_list dgfip_flags ~sep: op)
558+ l
496559 end
497560 | Dfun (funname , des ) ->
498561 Format. fprintf fmt " @[<hov 2>%s(%a@])" funname
0 commit comments