wip

what4/src/What4/Expr/Builder.hs

@@ -3379,23 +3379,23 @@ instance IsExprBuilder (ExprBuilder t st fs) where
       sbMakeExpr sym $ ArrayMap idx_tps baseRepr new_map def_map
 
   arrayIte sym p x y
-       -- Extract all concrete updates out.
-     | ArrayMapView mx x' <- viewArrayMap x
-     , ArrayMapView my y' <- viewArrayMap y
-     , not (AUM.null mx) || not (AUM.null my) = do
-       case exprType x of
-         BaseArrayRepr idxRepr bRepr -> do
-           let both_fn _ u v = baseTypeIte sym p u v
-               left_fn idx u = do
-                 v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx
-                 both_fn idx u v
-               right_fn idx v = do
-                 u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx
-                 both_fn idx u v
-           mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my
-           z' <- arrayIte sym p x' y'
+    --    -- Extract all concrete updates out.
+    --  | ArrayMapView mx x' <- viewArrayMap x
+    --  , ArrayMapView my y' <- viewArrayMap y
+    --  , not (AUM.null mx) || not (AUM.null my) = do
+    --    case exprType x of
+    --      BaseArrayRepr idxRepr bRepr -> do
+    --        let both_fn _ u v = baseTypeIte sym p u v
+    --            left_fn idx u = do
+    --              v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx
+    --              both_fn idx u v
+    --            right_fn idx v = do
+    --              u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx
+    --              both_fn idx u v
+    --        mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my
+    --        z' <- arrayIte sym p x' y'
 
-           sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'
+    --        sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'
 
      | otherwise = mkIte sym p x y