From 24c62fd39b5f758c0138c94e1614d8f5c7e36572 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 4 Mar 2020 06:21:22 -0800
Subject: [PATCH] [sledge] Strengthen canonizer of Extract terms
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
When extracting from a concatenation, drop a prefix of the concat with
length equal to the offset of the extraction:
```
(α₀^…^αᵢ^…) [0+n₀+…+nᵢ₋₁, l) ==> (αᵢ^…)[0,l) where nₓ ≡ |αₓ|
```

Reviewed By: jvillard

Differential Revision: D20192874

fbshipit-source-id: cd015aa36
---
 sledge/src/llair/term.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index edfdc1a23..b1a7ee038 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -741,6 +741,14 @@ let rec simp_extract agg off len =
                       | 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)