diff --git a/lib/simplify.ml b/lib/simplify.ml index 13dde28..d11dc15 100644 --- a/lib/simplify.ml +++ b/lib/simplify.ml @@ -8,9 +8,7 @@ let rec fold_plus (term : Expression.arith) = | Plus (Num m, Num n) -> Num (m + n) | Plus (Plus (t, Num m), Num n) -> fold_plus (Plus (t, Num (m + n))) | _ as t -> t - -(* TODO: - nested concats: <0>@(<0>@slice) -> <00> @ slice - s[0:1]@s[1:2] -> - s[0:2] *) + let rec fold_concat t = match t with | Concat (Bv Nil, t2) -> fold_concat t2 @@ -29,6 +27,12 @@ let rec fold_concat t = fold_concat (Concat (Slice (s1, ll, rr), t22)) else Concat (t1, fold_concat (Concat (t21, t22))) + | Concat + (Concat ( t11, (Slice (s1, ll, lr) as t12)), (Slice (s2, rl, rr) as t2)) -> + if [%compare.equal: Sliceable.t] s1 s2 && lr = rl then + fold_concat (Concat (t11, Slice (s1, ll, rr))) + else + Concat (fold_concat (Concat (t11, t12)), t2) | Concat (t1, t2) -> Concat (fold_concat t1, fold_concat t2) | _ -> t