Comparison functions for types, clocks and minils expressions.

This commit is contained in:
Adrien Guatto 2010-09-30 19:41:45 +02:00
parent 1fd2f374ff
commit 6bdca86253
2 changed files with 155 additions and 0 deletions

View file

@ -0,0 +1,72 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
open Clocks
open Types
open Idents
open Misc
let rec clock_compare ck1 ck2 = match ck1, ck2 with
| Cvar { contents = Clink ck1; }, _ -> clock_compare ck1 ck2
| _, Cvar { contents = Clink ck2; } -> clock_compare ck1 ck2
| Cbase, Cbase -> 0
| Cvar lr1, Cvar lr2 -> link_compare !lr1 !lr2
| Con (ck1, cn1, vi1), Con (ck2, cn2, vi2) ->
let cr1 = compare cn1 cn2 in
if cr1 <> 0 then cr1 else
let cr2 = ident_compare vi1 vi2 in
if cr2 <> 0 then cr2 else clock_compare ck1 ck2
| (Cbase | Cvar _), _ -> 1
| (Con _), _ -> -1
and link_compare li1 li2 = match li1, li2 with
| Cindex i1, Cindex i2 -> 0 (* Pervasives.compare i1 i2 *)
| Clink ck1, Clink ck2 -> clock_compare ck1 ck2
| (Cindex _), _ -> 1
| (Clink _), _ -> -1
let rec static_exp_compare se1 se2 =
let cr = type_compare se1.se_ty se2.se_ty in
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
| 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, se21), Sarray_power (se12, se22) ->
let cr = static_exp_compare se11 se12 in
if cr <> 0 then cr else static_exp_compare se21 se22
| 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) ->
let cr = c fn1 fn2 in
if cr <> 0 then cr else list_compare static_exp_compare sel1 sel2
| (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ | Sfield _), _
-> 1
| (Stuple _ | Sarray_power _ | Sarray _ | Srecord _ | Sop _), _ -> -1
and type_compare ty1 ty2 = match ty1, ty2 with
| Tprod tyl1, Tprod tyl2 -> list_compare type_compare tyl1 tyl2
| Tid tyn1, Tid tyn2 -> Pervasives.compare tyn1 tyn2
| Tarray (ty1, se1), Tarray (ty2, se2) ->
let cr = type_compare ty1 ty2 in
if cr <> 0 then cr else static_exp_compare se1 se2
| (Tprod _ | Tid _), _ -> 1
| (Tarray _), _ -> -1

View file

@ -0,0 +1,83 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* Comparison functions for MiniLustre *)
open Idents
open Minils
open Misc
open Global_compare
let rec exp_compare e1 e2 =
let cr = type_compare e1.e_ty e2.e_ty in
if cr <> 0 then cr
else
let cr = clock_compare e1.e_ck e2.e_ck in
if cr <> 0 then cr
else
match e1.e_desc, e2.e_desc with
| Econst se1, Econst se2 -> static_exp_compare se1 se2
| Evar vi1, Evar vi2 -> ident_compare vi1 vi2
| Efby (seo1, e1), Efby (seo2, e2) ->
let cr = option_compare static_exp_compare seo1 seo2 in
if cr <> 0 then cr else exp_compare e1 e2
| Eapp (app1, el1, vio1), Eapp (app2, el2, vio2) ->
let cr = app_compare app1 app2 in
if cr <> 0 then cr
else let cr = list_compare exp_compare el1 el2 in
if cr <> 0 then cr else option_compare ident_compare vio1 vio2
| Ewhen (e1, cn1, vi1), Ewhen (e2, cn2, vi2) ->
let cr = Pervasives.compare cn1 cn2 in
if cr <> 0 then cr else
let cr = ident_compare vi1 vi2 in
if cr <> 0 then cr else exp_compare e1 e2
| Emerge (vi1, cnel1), Emerge (vi2, cnel2) ->
let compare_cne (cn1, e1) (cn2, e2) =
let cr = compare cn1 cn2 in
if cr <> 0 then cr else exp_compare e1 e2 in
let cr = ident_compare vi1 vi2 in
if cr <> 0 then cr else list_compare compare_cne cnel1 cnel2
| Estruct fnel1, Estruct fnel2 ->
let compare_fne (fn1, e1) (fn2, e2) =
let cr = compare fn1 fn2 in
if cr <> 0 then cr else exp_compare e1 e2 in
list_compare compare_fne fnel1 fnel2
| Eiterator (it1, app1, se1, el1, vio1),
Eiterator (it2, app2, se2, el2, vio2) ->
let cr = compare it1 it2 in
if cr <> 0 then cr else
let cr = static_exp_compare se1 se2 in
if cr <> 0 then cr else
let cr = app_compare app1 app2 in
if cr <> 0 then cr else
let cr = option_compare ident_compare vio1 vio2 in
if cr <> 0 then cr else list_compare exp_compare el1 el2
| (Econst _ | Evar _ | Efby _ | Eapp _), _ -> 1
| (Ewhen _ | Emerge _ | Estruct _ | Eiterator _), _ -> -1
and app_compare app1 app2 =
let cr = Pervasives.compare app1.a_unsafe app2.a_unsafe in
if cr <> 0 then cr else let cr = match app1.a_op, app2.a_op with
| Efun ln1, Efun ln2 -> compare ln1 ln2
| x, y when x = y -> 0 (* all constructors can be compared with P.compare *)
| (Eequal | Etuple | Efun _ | Enode _ | Eifthenelse | Efield
| Efield_update), _ -> -1
| (Earray | Earray_fill | Eselect | Eselect_slice | Eselect_dyn | Eupdate
| Econcat), _ -> 1 in
if cr <> 0 then cr
else list_compare static_exp_compare app1.a_params app2.a_params
let rec pat_compare pat1 pat2 = match pat1, pat2 with
| Evarpat id1, Evarpat id2 -> ident_compare id1 id2
| Etuplepat pat_list1, Etuplepat pat_list2 ->
list_compare pat_compare pat_list1 pat_list2
| Evarpat _, _ -> 1
| Etuplepat _, _ -> -1