diff --git a/compiler/global/linearity.ml b/compiler/global/linearity.ml index 9208545..cd30d15 100644 --- a/compiler/global/linearity.ml +++ b/compiler/global/linearity.ml @@ -95,3 +95,18 @@ let rec lin_to_string = function let print_linearity ff l = fprintf ff " %s" (lin_to_string l) +let rec linearity_compare l1 l2 = match l1, l2 with + | Ltop, Ltop -> 0 + | Lvar v1, Lvar v2 -> compare v1 v2 + | Lat v1, Lat v2 -> compare v1 v2 + | Ltuple l1, Ltuple l2 -> list_compare linearity_compare l1 l2 + + | Ltop, _ -> 1 + + | Lvar _, Ltop -> -1 + | Lvar _, _ -> 1 + + | Lat _ , (Ltop | Lvar _) -> -1 + | Lat _ , _ -> 1 + + | Ltuple _, _ -> -1 diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index 66207c4..f290cf0 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -24,6 +24,9 @@ struct let cr = Global_compare.type_compare w1.w_ty w2.w_ty in if cr <> 0 then cr else + let cr = Linearity.linearity_compare w1.w_linearity w2.w_linearity in + if cr <> 0 then cr + else match w1.w_desc, w2.w_desc with | Wconst se1, Wconst se2 -> Global_compare.static_exp_compare se1 se2 | Wvar vi1, Wvar vi2 -> ident_compare vi1 vi2 @@ -50,6 +53,9 @@ struct let cr = Global_compare.type_compare e1.e_ty e2.e_ty in if cr <> 0 then cr else + let cr = Linearity.linearity_compare e1.e_linearity e2.e_linearity in + if cr <> 0 then cr + else let cr = C.clock_compare e1.e_base_ck e2.e_base_ck in if cr <> 0 then cr else