jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Allow symbolic static_exp eval.

Browse source
This commit is contained in:
Léonard Gérard 2011-11-14 15:30:40 +01:00
parent bdd85f5f81
commit 4e3c58bb40
2 changed files with 53 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

94
compiler/global/global_compare.ml
View file

@ -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

8
compiler/global/static.ml
View file

@ -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 ->