module UVMHS.Lib.Pretty.Shape where

import UVMHS.Core

-----------
-- Shape --
-----------

-- A shape looks like:
--
--     □□□□XXX
--     XX
--     XXX
--     XXXX
--     XX
--     XXXXXX
--     XXXX
--
-- this example shape is abstracted as:
--
-- □□□□XXX
-- YYYYYY
-- YYYYYY
-- YYYYYY
-- YYYYYY
-- YYYYYY
-- ZZZZ
-- 
-- where:
-- + XXX:    represented by the length of the first line
-- + YYYYYY: represented by the maximum length of any line that isn't
--           the first or last
-- + ZZZZ:   represented by the maximum length of the last line
-- + also:   the total number of newlines in the shape
--           (i.e., one more than number of lines in YYYYYYY)
--
-- A special case is a single-line shape, which is represented as
-- just the length of the line.
--
-- shapes can be combined and form a monoid

data ShapeM = ShapeM
  { ShapeM -> ℕ64
shapeMFirstLength  ∷ {-# UNPACK #-} ℕ64
  , ShapeM -> ℕ64
shapeMMidMaxLength ∷ {-# UNPACK #-} ℕ64
  , ShapeM -> ℕ64
shapeMLastLength   ∷ {-# UNPACK #-} ℕ64
  , ShapeM -> ℕ64
shapeMNewlines     ∷ {-# UNPACK #-} ℕ64
  } deriving (ShapeM -> ShapeM -> Bool
(ShapeM -> ShapeM -> Bool)
-> (ShapeM -> ShapeM -> Bool) -> Eq ShapeM
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ShapeM -> ShapeM -> Bool
== :: ShapeM -> ShapeM -> Bool
$c/= :: ShapeM -> ShapeM -> Bool
/= :: ShapeM -> ShapeM -> Bool
Eq,Eq ShapeM
Eq ShapeM =>
(ShapeM -> ShapeM -> Ordering)
-> (ShapeM -> ShapeM -> Bool)
-> (ShapeM -> ShapeM -> Bool)
-> (ShapeM -> ShapeM -> Bool)
-> (ShapeM -> ShapeM -> Bool)
-> (ShapeM -> ShapeM -> ShapeM)
-> (ShapeM -> ShapeM -> ShapeM)
-> Ord ShapeM
ShapeM -> ShapeM -> Bool
ShapeM -> ShapeM -> Ordering
ShapeM -> ShapeM -> ShapeM
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ShapeM -> ShapeM -> Ordering
compare :: ShapeM -> ShapeM -> Ordering
$c< :: ShapeM -> ShapeM -> Bool
< :: ShapeM -> ShapeM -> Bool
$c<= :: ShapeM -> ShapeM -> Bool
<= :: ShapeM -> ShapeM -> Bool
$c> :: ShapeM -> ShapeM -> Bool
> :: ShapeM -> ShapeM -> Bool
$c>= :: ShapeM -> ShapeM -> Bool
>= :: ShapeM -> ShapeM -> Bool
$cmax :: ShapeM -> ShapeM -> ShapeM
max :: ShapeM -> ShapeM -> ShapeM
$cmin :: ShapeM -> ShapeM -> ShapeM
min :: ShapeM -> ShapeM -> ShapeM
Ord,Int -> ShapeM -> ShowS
[ShapeM] -> ShowS
ShapeM -> String
(Int -> ShapeM -> ShowS)
-> (ShapeM -> String) -> ([ShapeM] -> ShowS) -> Show ShapeM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ShapeM -> ShowS
showsPrec :: Int -> ShapeM -> ShowS
$cshow :: ShapeM -> String
show :: ShapeM -> String
$cshowList :: [ShapeM] -> ShowS
showList :: [ShapeM] -> ShowS
Show)
makeLenses ''ShapeM

data Shape = 
    SingleLine {-# UNPACK #-} ℕ64 
  | MultiLine {-# UNPACK #-} ShapeM
  deriving (Shape -> Shape -> Bool
(Shape -> Shape -> Bool) -> (Shape -> Shape -> Bool) -> Eq Shape
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Shape -> Shape -> Bool
== :: Shape -> Shape -> Bool
$c/= :: Shape -> Shape -> Bool
/= :: Shape -> Shape -> Bool
Eq,Eq Shape
Eq Shape =>
(Shape -> Shape -> Ordering)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Shape)
-> (Shape -> Shape -> Shape)
-> Ord Shape
Shape -> Shape -> Bool
Shape -> Shape -> Ordering
Shape -> Shape -> Shape
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Shape -> Shape -> Ordering
compare :: Shape -> Shape -> Ordering
$c< :: Shape -> Shape -> Bool
< :: Shape -> Shape -> Bool
$c<= :: Shape -> Shape -> Bool
<= :: Shape -> Shape -> Bool
$c> :: Shape -> Shape -> Bool
> :: Shape -> Shape -> Bool
$c>= :: Shape -> Shape -> Bool
>= :: Shape -> Shape -> Bool
$cmax :: Shape -> Shape -> Shape
max :: Shape -> Shape -> Shape
$cmin :: Shape -> Shape -> Shape
min :: Shape -> Shape -> Shape
Ord,Int -> Shape -> ShowS
[Shape] -> ShowS
Shape -> String
(Int -> Shape -> ShowS)
-> (Shape -> String) -> ([Shape] -> ShowS) -> Show Shape
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Shape -> ShowS
showsPrec :: Int -> Shape -> ShowS
$cshow :: Shape -> String
show :: Shape -> String
$cshowList :: [Shape] -> ShowS
showList :: [Shape] -> ShowS
Show)
makePrisms ''Shape

shapeFirstLength ∷ Shape → ℕ64
shapeFirstLength :: Shape -> ℕ64
shapeFirstLength = \case
  SingleLine ℕ64
n → ℕ64
n
  MultiLine ShapeM
sh → ShapeM -> ℕ64
shapeMFirstLength ShapeM
sh

shapeLastLength ∷ Shape → ℕ64
shapeLastLength :: Shape -> ℕ64
shapeLastLength = \case
  SingleLine ℕ64
n → ℕ64
n
  MultiLine ShapeM
sh → ShapeM -> ℕ64
shapeMLastLength ShapeM
sh

newlineShapeM ∷ ShapeM
newlineShapeM :: ShapeM
newlineShapeM = ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM ℕ64
forall a. Zero a => a
zero ℕ64
forall a. Zero a => a
zero ℕ64
forall a. Zero a => a
zero ℕ64
forall a. One a => a
one

newlineShape ∷ Shape
newlineShape :: Shape
newlineShape = ShapeM -> Shape
MultiLine ShapeM
newlineShapeM

boxShape ∷ ℕ64 → ℕ64 → Shape
boxShape :: ℕ64 -> ℕ64 -> Shape
boxShape ℕ64
n ℕ64
nls 
  | ℕ64
nls ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
forall a. Zero a => a
zero = ℕ64 -> Shape
SingleLine ℕ64
n
  | Bool
otherwise  = ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM ℕ64
n ℕ64
n ℕ64
n ℕ64
nls

shapeWidth ∷ Shape → ℕ64
shapeWidth :: Shape -> ℕ64
shapeWidth = \case
  SingleLine ℕ64
n → ℕ64
n
  MultiLine (ShapeM ℕ64
fl ℕ64
mml ℕ64
ll ℕ64
_) → ℕ64
fl ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
mml ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
ll

shapeNewlines ∷ Shape → ℕ64
shapeNewlines :: Shape -> ℕ64
shapeNewlines = \case
  SingleLine ℕ64
_ → ℕ64
forall a. Zero a => a
zero
  MultiLine ShapeM
sh → ShapeM -> ℕ64
shapeMNewlines ShapeM
sh

instance Null Shape where null :: Shape
null = ℕ64 -> Shape
SingleLine ℕ64
forall a. Zero a => a
zero
instance Append Shape where
  SingleLine ℕ64
l₁ ⧺ :: Shape -> Shape -> Shape
⧺ SingleLine ℕ64
l₂ = 
    -- AAA ⧺ XXX = AAAXXX
    ℕ64 -> Shape
SingleLine (ℕ64 -> Shape) -> ℕ64 -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64
l₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Append a => a -> a -> a
⧺ ℕ64
l₂
  SingleLine ℕ64
l₁ ⧺ MultiLine (ShapeM ℕ64
fl₂ ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂) =
    -- AAA  ⧺  □□□□XXX  =  □□□□AAAXXX
    --         YY          YY
    --         ZZZZ        ZZZZ
    ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM (ℕ64
l₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
fl₂) ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂
  MultiLine (ShapeM ℕ64
fl₁ ℕ64
mml₁ ℕ64
ll₁ ℕ64
nls₁) ⧺ SingleLine ℕ64
l₂ = 
    -- □□□□XXX  ⧺  AAA  =  □□□□XXX
    -- YY                  YY
    -- ZZZZ                ZZZZAAA
    ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM ℕ64
fl₁ ℕ64
mml₁ (ℕ64
ll₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
l₂) ℕ64
nls₁
  MultiLine (ShapeM ℕ64
fl₁ ℕ64
mml₁ ℕ64
ll₁ ℕ64
nls₁) ⧺ MultiLine (ShapeM ℕ64
fl₂ ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂) =
    -- □□□□XXX  ⧺  □□□□AAA  =  □□□□XXX
    -- YY          BB          YY
    -- ZZZZ        CCCC        ZZZZAAA
    --                         BB
    --                         CCCC
    ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM ℕ64
fl₁ (ℕ64
mml₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ (ℕ64
ll₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
fl₂) ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
mml₂) ℕ64
ll₂ (ℕ64 -> ShapeM) -> ℕ64 -> ShapeM
forall a b. (a -> b) -> a -> b
$ ℕ64
nls₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
nls₂
instance Monoid Shape

instance Bot Shape where bot :: Shape
bot = ℕ64 -> Shape
SingleLine ℕ64
forall a. Zero a => a
zero
instance Join Shape where
  SingleLine ℕ64
l₁ ⊔ :: Shape -> Shape -> Shape
⊔ SingleLine ℕ64
l₂ = ℕ64 -> Shape
SingleLine (ℕ64 -> Shape) -> ℕ64 -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64
l₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
l₂
  SingleLine ℕ64
l₁ ⊔ MultiLine (ShapeM ℕ64
fl₂ ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂) = 
    ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM (ℕ64
l₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
fl₂) ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂
  MultiLine (ShapeM ℕ64
fl₁ ℕ64
mml₁ ℕ64
ll₁ ℕ64
nls₁) ⊔ SingleLine ℕ64
l₂ = 
    ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM (ℕ64
l₂ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
fl₁) ℕ64
mml₁ ℕ64
ll₁ ℕ64
nls₁
  MultiLine (ShapeM ℕ64
fl₁ ℕ64
mml₁ ℕ64
ll₁ ℕ64
nls₁) ⊔ MultiLine (ShapeM ℕ64
fl₂ ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂) 
    | ℕ64
nls₁ ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
> ℕ64
nls₂ = ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM (ℕ64
fl₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
fl₂) (ℕ64
mml₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
mml₂ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
ll₂) ℕ64
ll₁ ℕ64
nls₁
    | ℕ64
nls₁ ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℕ64
nls₂ = ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM (ℕ64
fl₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
fl₂) (ℕ64
mml₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
mml₂ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
ll₁) ℕ64
ll₂ ℕ64
nls₂
    | Bool
otherwise   = ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM (ℕ64
fl₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
fl₂) (ℕ64
mml₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
mml₂) (ℕ64
ll₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
ll₂) (ℕ64 -> ShapeM) -> ℕ64 -> ShapeM
forall a b. (a -> b) -> a -> b
$ ℕ64
nls₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Join a => a -> a -> a
⊔ ℕ64
nls₂

------------
-- ShapeA --
------------

-- A non-aligned shape looks like:
--
--     □□□□XXX
--     YY
--     ZZZZ
--
-- An aligned shape looks like:
--
--     □□□□XXX
--     ⋅⋅⋅⋅YY
--     ⋅⋅⋅⋅ZZZZ
--
-- Shapes can be combined, which may affect alignment:
--
--     non-aligned + non-aligned = non-aligned
--     non-aligned + aligned     = non-aligned
--     aligned     + non-aligned = aligned
--     aligned     + aligned     = aligned
--
-- When the shape is a single line, it is always non-aligned 
-- (so, aligned = False)

data ShapeA = ShapeA
  { ShapeA -> Bool
shapeIAligned ∷ 𝔹
  , ShapeA -> Shape
shapeIShape   ∷ Shape
  }
  deriving (ShapeA -> ShapeA -> Bool
(ShapeA -> ShapeA -> Bool)
-> (ShapeA -> ShapeA -> Bool) -> Eq ShapeA
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ShapeA -> ShapeA -> Bool
== :: ShapeA -> ShapeA -> Bool
$c/= :: ShapeA -> ShapeA -> Bool
/= :: ShapeA -> ShapeA -> Bool
Eq,Eq ShapeA
Eq ShapeA =>
(ShapeA -> ShapeA -> Ordering)
-> (ShapeA -> ShapeA -> Bool)
-> (ShapeA -> ShapeA -> Bool)
-> (ShapeA -> ShapeA -> Bool)
-> (ShapeA -> ShapeA -> Bool)
-> (ShapeA -> ShapeA -> ShapeA)
-> (ShapeA -> ShapeA -> ShapeA)
-> Ord ShapeA
ShapeA -> ShapeA -> Bool
ShapeA -> ShapeA -> Ordering
ShapeA -> ShapeA -> ShapeA
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ShapeA -> ShapeA -> Ordering
compare :: ShapeA -> ShapeA -> Ordering
$c< :: ShapeA -> ShapeA -> Bool
< :: ShapeA -> ShapeA -> Bool
$c<= :: ShapeA -> ShapeA -> Bool
<= :: ShapeA -> ShapeA -> Bool
$c> :: ShapeA -> ShapeA -> Bool
> :: ShapeA -> ShapeA -> Bool
$c>= :: ShapeA -> ShapeA -> Bool
>= :: ShapeA -> ShapeA -> Bool
$cmax :: ShapeA -> ShapeA -> ShapeA
max :: ShapeA -> ShapeA -> ShapeA
$cmin :: ShapeA -> ShapeA -> ShapeA
min :: ShapeA -> ShapeA -> ShapeA
Ord,Int -> ShapeA -> ShowS
[ShapeA] -> ShowS
ShapeA -> String
(Int -> ShapeA -> ShowS)
-> (ShapeA -> String) -> ([ShapeA] -> ShowS) -> Show ShapeA
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ShapeA -> ShowS
showsPrec :: Int -> ShapeA -> ShowS
$cshow :: ShapeA -> String
show :: ShapeA -> String
$cshowList :: [ShapeA] -> ShowS
showList :: [ShapeA] -> ShowS
Show)
makeLenses ''ShapeA

instance Null ShapeA where null :: ShapeA
null = Bool -> Shape -> ShapeA
ShapeA Bool
False Shape
forall a. Null a => a
null
instance Append ShapeA where
  ShapeA Bool
a₁ Shape
sh₁ ⧺ :: ShapeA -> ShapeA -> ShapeA
⧺ ShapeA Bool
a₂ Shape
sh₂ =
    let sh₂' :: Shape
sh₂' =
          if Bool -> Bool
not Bool
a₂
          -- ‣ sh₁ is single-line
          -- ‣ sh₂ is single-line 
          --
          --     □□□□XXX  ⧺  □□□□AAA  =  □□□□XXXAAA
          --
          -- ‣ sh₁ is single-line 
          -- ‣ sh₂ is multiline non-aligned
          --
          --     □□□□XXX  ⧺  □□□□AAA  =  □□□□XXXAAA
          --                 BB          BB
          --                 CCCC        CCCC
          --
          -- ‣ sh₁ is multiline non-aligned
          -- ‣ sh₂ is single-line
          -- 
          --     □□□□XXX  ⧺ □□□□AAA  =  □□□□XXX
          --     YY                     YY     
          --     ZZZZ                   ZZZZAAA
          -- 
          -- ‣ sh₁ is multiline non-aligned 
          -- ‣ sh₂ is multiline non-aligned
          --     □□□□XXX  ⧺  □□□□AAA  =  □□□□XXX
          --     YY          BB          YY
          --     ZZZZ        CCCC        ZZZZAAA
          --                             BB
          --                             CCCC
          --
          -- ‣ sh₁ is multiline aligned
          -- ‣ sh₂ is single-line
          --
          --     □□□□XXX   ⧺  □□□□AAA  =  □□□□XXX 
          --     ⋅⋅⋅⋅YY                   ⋅⋅⋅⋅YY  
          --     ⋅⋅⋅⋅ZZZZ                 ⋅⋅⋅⋅ZZZZAAA
          --
          -- ‣ sh₁ is multiline aligned
          -- ‣ sh₂ is multiline non-aligned 
          --
          --     □□□□XXX   ⧺  □□□□AAA  =  □□□□XXX
          --     ⋅⋅⋅⋅YY       BB          ⋅⋅⋅⋅YY
          --     ⋅⋅⋅⋅ZZZZ     CCCC        ⋅⋅⋅⋅ZZZZAAA
          --                              ⋅⋅⋅⋅BB
          --                              ⋅⋅⋅⋅CCCC
          --
          then Shape
sh₂
          -- ‣ sh₁ is single-lined
          -- ‣ sh₂ is multiline aligned
          --
          --     □□□□XXX  ⧺   □□□□AAA   =  □□□□XXXAAA 
          --                  ⋅⋅⋅⋅BB       ⋅⋅⋅⋅␣␣␣BB  
          --                  ⋅⋅⋅⋅CCCC     ⋅⋅⋅⋅␣␣␣CCCC
          --
          -- ‣ sh₁ is multiline non-aligned
          -- ‣ sh₂ is multiline aligned
          --
          --     □□□□XXX  ⧺  □□□□AAA   =  □□□□XXX
          --     YY          ⋅⋅⋅⋅BB       YY
          --     ZZZZ        ⋅⋅⋅⋅CCCC     ZZZZAAA
          --                              ␣␣␣␣BB
          --                              ␣␣␣␣CCCC
          --
          -- ‣ sh₁ is multiline aligned
          -- ‣ sh₂ is multiline aligned 
          --
          --     □□□□XXX   ⧺  □□□□AAA   =  □□□□XXX
          --     ⋅⋅⋅⋅YY       ⋅⋅⋅⋅BB       ⋅⋅⋅⋅YY
          --     ⋅⋅⋅⋅ZZZZ     ⋅⋅⋅⋅CCCC     ⋅⋅⋅⋅ZZZZAAA
          --                               ⋅⋅⋅⋅␣␣␣␣BB
          --                               ⋅⋅⋅⋅␣␣␣␣CCCC
          --
          else 
            case Shape
sh₂ of
              MultiLine (ShapeM ℕ64
fl₂ ℕ64
mml₂ ℕ64
ll₂ ℕ64
nls₂) →
                ShapeM -> Shape
MultiLine (ShapeM -> Shape) -> ShapeM -> Shape
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64 -> ℕ64 -> ℕ64 -> ShapeM
ShapeM ℕ64
fl₂ (Shape -> ℕ64
shapeLastLength Shape
sh₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
mml₂) (Shape -> ℕ64
shapeLastLength Shape
sh₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
ll₂) ℕ64
nls₂
              Shape
_ → 𝕊 -> Shape
forall a. STACK => 𝕊 -> a
error 𝕊
"internal error"
    in Bool -> Shape -> ShapeA
ShapeA (Bool
a₁ Bool -> Bool -> Bool
⩔ (Shape ⌲ ℕ64) -> Shape -> Bool
forall a b. (a ⌲ b) -> a -> Bool
shape Shape ⌲ ℕ64
singleLineL Shape
sh₁ Bool -> Bool -> Bool
⩓ Bool
a₂) (Shape -> ShapeA) -> Shape -> ShapeA
forall a b. (a -> b) -> a -> b
$ Shape
sh₁ Shape -> Shape -> Shape
forall a. Append a => a -> a -> a
⧺ Shape
sh₂'
instance Monoid ShapeA

alignShapeA ∷ ShapeA → ShapeA
alignShapeA :: ShapeA -> ShapeA
alignShapeA (ShapeA Bool
a Shape
sh)
  | (Shape ⌲ ShapeM) -> Shape -> Bool
forall a b. (a ⌲ b) -> a -> Bool
shape Shape ⌲ ShapeM
multiLineL Shape
sh = Bool -> Shape -> ShapeA
ShapeA Bool
True Shape
sh
  | Bool
otherwise = Bool -> Shape -> ShapeA
ShapeA Bool
a Shape
sh