From 4e3c58bb405fada5b5c5a47293e7531854da92a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Mon, 14 Nov 2011 15:30:40 +0100 Subject: [PATCH] Allow symbolic static_exp eval. --- compiler/global/global_compare.ml | 94 ++++++++++++++++--------------- compiler/global/static.ml | 8 ++- 2 files changed, 53 insertions(+), 49 deletions(-) diff --git a/compiler/global/global_compare.ml b/compiler/global/global_compare.ml index 9ce115b..b5ee535 100644 --- a/compiler/global/global_compare.ml +++ b/compiler/global/global_compare.ml @@ -38,66 +38,68 @@ and link_compare li1 li2 = match li1, li2 with let rec static_exp_compare se1 se2 = let cr = type_compare se1.se_ty se2.se_ty in + if cr <> 0 then cr else static_exp_desc_compare se1.se_desc se2.se_desc - if cr <> 0 then cr else - let c = Pervasives.compare in - match se1.se_desc, se2.se_desc with - | Svar cn1, Svar cn2 -> Pervasives.compare cn1 cn2 - | Sint i1, Sint i2 -> c i1 i2 - | Sfloat f1, Sfloat f2 -> c f1 f2 - | Sbool b1, Sbool b2 -> c b1 b2 - | Sstring s1, Sstring s2 -> c s1 s2 - | Sconstructor c1, Sconstructor c2 -> c c1 c2 - | Sfield f1, Sfield f2 -> c f1 f2 - | Stuple sel1, Stuple sel2 -> - list_compare static_exp_compare sel1 sel2 - | Sarray_power (se11, sel1), Sarray_power (se12, sel2) -> - let cr = static_exp_compare se11 se12 in - if cr <> 0 then cr else list_compare static_exp_compare sel1 sel2 - | Sarray sel1, Sarray sel2 -> - list_compare static_exp_compare sel1 sel2 - | Srecord fnsel1, Srecord fnsel2 -> - let compare_field (fn1, se1) (fn2, se2) = - let cr = c fn1 fn2 in - if cr <> 0 then cr else static_exp_compare se1 se2 in - list_compare compare_field fnsel1 fnsel2 - | Sop (fn1, sel1), Sop (fn2, sel2) -> + +and static_exp_desc_compare sed1 sed2 = + let c = Pervasives.compare in + match sed1, sed2 with + | Svar cn1, Svar cn2 -> Pervasives.compare cn1 cn2 + | Sint i1, Sint i2 -> c i1 i2 + | Sfloat f1, Sfloat f2 -> c f1 f2 + | Sbool b1, Sbool b2 -> c b1 b2 + | Sstring s1, Sstring s2 -> c s1 s2 + | Sconstructor c1, Sconstructor c2 -> c c1 c2 + | Sfield f1, Sfield f2 -> c f1 f2 + | Stuple sel1, Stuple sel2 -> + list_compare static_exp_compare sel1 sel2 + | Sarray_power (se11, sel1), Sarray_power (se12, sel2) -> + let cr = static_exp_compare se11 se12 in + if cr <> 0 then cr else list_compare static_exp_compare sel1 sel2 + | Sarray sel1, Sarray sel2 -> + list_compare static_exp_compare sel1 sel2 + | Srecord fnsel1, Srecord fnsel2 -> + let compare_field (fn1, se1) (fn2, se2) = let cr = c fn1 fn2 in - if cr <> 0 then cr else list_compare static_exp_compare sel1 sel2 + if cr <> 0 then cr else static_exp_compare se1 se2 in + list_compare compare_field fnsel1 fnsel2 + | Sop (fn1, sel1), Sop (fn2, sel2) -> + let cr = c fn1 fn2 in + if cr <> 0 then cr else list_compare static_exp_compare sel1 sel2 - | Svar _, _ -> 1 + | Svar _, _ -> 1 - | Sint _, Svar _ -> -1 - | Sint _, _ -> 1 + | Sint _, Svar _ -> -1 + | Sint _, _ -> 1 - | Sfloat _, (Svar _ | Sint _) -> -1 - | Sfloat _, _ -> 1 + | Sfloat _, (Svar _ | Sint _) -> -1 + | Sfloat _, _ -> 1 - | Sbool _, (Svar _ | Sint _ | Sfloat _) -> -1 - | Sbool _, _ -> 1 + | Sbool _, (Svar _ | Sint _ | Sfloat _) -> -1 + | Sbool _, _ -> 1 - | Sstring _, (Svar _ | Sint _ | Sfloat _ | Sbool _) -> -1 - | Sstring _, _ -> 1 + | Sstring _, (Svar _ | Sint _ | Sfloat _ | Sbool _) -> -1 + | Sstring _, _ -> 1 - | Sconstructor _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sstring _) -> -1 - | Sconstructor _, _ -> 1 + | Sconstructor _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sstring _) -> -1 + | Sconstructor _, _ -> 1 - | Sfield _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sstring _ | Sconstructor _) -> -1 - | Sfield _, _ -> 1 + | Sfield _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sstring _ | Sconstructor _) -> -1 + | Sfield _, _ -> 1 - | Stuple _, (Srecord _ | Sop _ | Sarray _ | Sarray_power _ ) -> 1 - | Stuple _, _ -> -1 + | Stuple _, (Srecord _ | Sop _ | Sarray _ | Sarray_power _ ) -> 1 + | Stuple _, _ -> -1 - | Sarray_power _, (Srecord _ | Sop _ | Sarray _) -> -1 - | Sarray_power _, _ -> 1 + | Sarray_power _, (Srecord _ | Sop _ | Sarray _) -> -1 + | Sarray_power _, _ -> 1 - | Sarray _, (Srecord _ | Sop _) -> 1 - | Sarray _, _ -> -1 + | Sarray _, (Srecord _ | Sop _) -> 1 + | Sarray _, _ -> -1 - | Srecord _, Sop _ -> 1 - | Srecord _, _ -> -1 + | Srecord _, Sop _ -> 1 + | Srecord _, _ -> -1 - | Sop _, _ -> -1 + | Sop _, _ -> -1 and type_compare ty1 ty2 = match ty1, ty2 with | Tprod tyl1, Tprod tyl2 -> list_compare type_compare tyl1 tyl2 diff --git a/compiler/global/static.ml b/compiler/global/static.ml index d140697..7116622 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -75,7 +75,7 @@ let apply_op partial loc op se_list = in let sed_l, has_var = Misc.mapfold has_var_desc false se_list in if (op.qual = Pervasives) && not has_var - then ( (* concret evaluation *) + then ( (* concrete evaluation *) match op.name, sed_l with | "+", [Sint n1; Sint n2] -> Sint (n1 + n2) | "-", [Sint n1; Sint n2] -> Sint (n1 - n2) @@ -101,7 +101,8 @@ let apply_op partial loc op se_list = ) else ( (* symbolic evaluation *) match op, sed_l with - | {qual = Pervasives; name = "=" }, [sed1;sed2] when sed1 = sed2 -> Sbool true + | {qual = Pervasives; name = "=" }, [sed1;sed2] + when Global_compare.static_exp_desc_compare sed1 sed2 = 0 -> Sbool true | _ -> if partial then Sop(op, se_list) (* partial evaluation *) @@ -140,7 +141,8 @@ let rec eval_core partial env se = match se.se_desc with | Sarray se_list -> { se with se_desc = Sarray (List.map (eval_core partial env) se_list) } | Sarray_power (se, n_list) -> - { se with se_desc = Sarray_power (eval_core partial env se, List.map (eval_core partial env) n_list) } + { se with se_desc = + Sarray_power (eval_core partial env se, List.map (eval_core partial env) n_list) } | Stuple se_list -> { se with se_desc = Stuple (List.map (eval_core partial env) se_list) } | Srecord f_se_list ->