From 37ddf95a49b928ce1f297d1a452154f8d899f377 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 10 Mar 2020 02:20:56 -0700 Subject: [PATCH] [sledge] Strengthen and simplify canonizer for Extract terms Summary: Formulate the canonizer for Extract from Concat terms uniformly as a concatenation of extracts. Reviewed By: jvillard Differential Revision: D20303064 fbshipit-source-id: a45bc45dd --- sledge/src/import/vector.ml | 8 +++ sledge/src/import/vector.mli | 8 +++ sledge/src/llair/term.ml | 94 +++++++++++++++--------------------- 3 files changed, 55 insertions(+), 55 deletions(-) diff --git a/sledge/src/import/vector.ml b/sledge/src/import/vector.ml index 0836584fe..706e4715b 100644 --- a/sledge/src/import/vector.ml +++ b/sledge/src/import/vector.ml @@ -101,6 +101,14 @@ let fold_map x ~init ~f = let s, x = Array.fold_map (a x) ~init ~f in (s, v x) +let fold_map_until xs ~init ~f ~finish = + With_return.with_return (fun {return} -> + finish + (fold_map xs ~init ~f:(fun s x -> + match (f s x : _ Continue_or_stop.t) with + | Continue x -> x + | Stop x -> return x )) ) + let concat xs = v (Array.concat (al xs)) let copy x = v (Array.copy (a x)) let sub ~pos ~len x = v (Array.sub ~pos ~len (a x)) diff --git a/sledge/src/import/vector.mli b/sledge/src/import/vector.mli index bb98ba2db..a97a725af 100644 --- a/sledge/src/import/vector.mli +++ b/sledge/src/import/vector.mli @@ -108,6 +108,14 @@ val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t (* val folding_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'c t *) (* val folding_mapi : 'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b * 'c) -> 'c t *) + +val fold_map_until : + 'a t + -> init:'accum + -> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t) + -> finish:('accum * 'b t -> 'final) + -> 'final + val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t (* val fold_mapi : diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 166403ab6..3e5deea84 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -720,61 +720,45 @@ let rec simp_extract agg off len = simp_memory len e (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *) | Ap2 (Memory, n, _) when equal off zero && equal n len -> agg - (* (α₀^…^αᵢ^…^αⱼ^…) [0+n₀+…+nᵢ₋₁, nᵢ+…+nⱼ) ==> αᵢ^…^αⱼ where nₓ ≡ |αₓ| *) - | ApN (Concat, na1N) -> - let n = Vector.length na1N in - (* invariant: oI = ∑ᵥ₌₀ⁱ⁻¹ nᵥ *) - let rec find_off oI i = - [%Trace.call fun {pf} -> pf "o_0^%i = %a" i pp oI] - ; - ( if i = n then Ap3 (Extract, agg, off, len) - else - match Vector.get na1N i with - | Ap2 (Memory, nI, _) | Ap3 (Extract, _, _, nI) -> ( - match (oI, off) with - | Integer {data= y}, Integer {data= z} when Z.gt y z -> - Ap3 (Extract, agg, off, len) - | _ when not (equal oI off) -> - find_off (simp_add2 oI nI) (i + 1) - | _ -> - (* invariant: lIJ = ∑ᵥ₌ᵢʲ⁻¹ nᵥ *) - let rec find_len lIJ j = - [%Trace.call fun {pf} -> pf "l_%i^%i = %a" i j pp lIJ] - ; - ( if j = n then find_off (simp_add2 oI nI) (i + 1) - else - match Vector.get na1N j with - | Ap2 (Memory, nJ, _) | Ap3 (Extract, _, _, nJ) -> ( - let lIJ = simp_add2 lIJ nJ in - match (lIJ, len) with - (* (α₀^…^αᵢ^…) [0+n₀+…+nᵢ₋₁, l) ==> (αᵢ^…)[0,l) - where nₓ ≡ |αₓ| *) - | Integer {data= y}, Integer {data= z} - when Z.gt y z -> - let naIN = - Vector.sub ~pos:i ~len:(n - i) na1N - in - simp_extract (simp_concat naIN) zero len - | Integer {data= y}, Integer {data= z} - when Z.gt y z -> - Ap3 (Extract, agg, off, len) - | _ when not (equal lIJ len) -> - find_len lIJ (j + 1) - | _ -> - let naIJ = - Vector.sub ~pos:i ~len:(j - i + 1) na1N - in - simp_concat naIJ ) - | _ -> violates invariant agg ) - |> - [%Trace.retn fun {pf} -> pf "%a" pp] - in - find_len zero i ) - | _ -> violates invariant agg ) - |> - [%Trace.retn fun {pf} -> pf "%a" pp] - in - find_off zero 0 + (* For (α₀^α₁)[o,l) there are 3 cases: + * + * ⟨...⟩^⟨...⟩ + * [,) + * o < o+l ≤ |α₀| : (α₀^α₁)[o,l) ==> α₀[o,l) ^ α₁[0,0) + * + * ⟨...⟩^⟨...⟩ + * [ , ) + * o ≤ |α₀| < o+l : (α₀^α₁)[o,l) ==> α₀[o,|α₀|-o) ^ α₁[0,l-(|α₀|-o)) + * + * ⟨...⟩^⟨...⟩ + * [,) + * |α₀| ≤ o : (α₀^α₁)[o,l) ==> α₀[o,0) ^ α₁[o-|α₀|,l) + * + * So in general: + * + * (α₀^α₁)[o,l) ==> α₀[o,l₀) ^ α₁[o₁,l-l₀) + * where l₀ = max 0 (min l |α₀|-o) + * o₁ = max 0 o-|α₀| + *) + | ApN (Concat, na1N) -> ( + match len with + | Integer {data= l} -> + Vector.fold_map_until na1N ~init:(l, off) + ~f:(fun (l, oI) naI -> + let nI = agg_size_exn naI in + if Z.equal Z.zero l then + Continue ((l, oI), simp_extract naI oI zero) + else + let oI_nI = simp_sub oI nI in + match oI_nI with + | Integer {data} -> + let oJ = if Z.sign data <= 0 then zero else oI_nI in + let lI = Z.(max zero (min l (neg data))) in + let l = Z.(l - lI) in + Continue ((l, oJ), simp_extract naI oI (integer lI)) + | _ -> Stop (Ap3 (Extract, agg, off, len)) ) + ~finish:(fun (_, e1N) -> simp_concat e1N) + | _ -> Ap3 (Extract, agg, off, len) ) (* α[o,l) *) | _ -> Ap3 (Extract, agg, off, len) ) |>