fabian/veribase-idr2 - Change 3UNR6V4M3O7ABUVW7NXBQFPKQXOXIDIGPRNJKMEMQXIOQRN2W6RAC

Continue AVLTree

Created by fabian on June 20, 2021

3UNR6V4M3O7ABUVW7NXBQFPKQXOXIDIGPRNJKMEMQXIOQRN2W6RAC

Dependencies

In channels

main

Change contents

Replacement in src/Data/AVLTree.idr at line 17 [3.160]

B:BD[3.413] → [3.413:522]

data AVLTree : (o : Order t) => (t : Type) -> (height : Natural) -> (bounds : Optional (t, t)) -> Type where

[3.413]

[3.522]

data AVLTree : (t : Type) -> (o : Order t) => (height : Natural) -> (bounds : Optional (t, t)) -> Type where

Replacement in src/Data/AVLTree.idr at line 19 [3.160]

B:BD[3.559] → [3.559:605]

  Node  : AVLTree t leftHeight leftBounds {o}

[3.559]

[3.605]

  Node  : {leftHeight, rightHeight : Natural} -> {leftBounds, rightBounds : Optional (t, t)}
        -> AVLTree t leftHeight leftBounds {o}

Replacement in src/Data/AVLTree.idr at line 23 [3.160]

B:BD[3.677] → [3.677:819]

B:BD[3.819] → [2.0:196]

        -> {auto heightCheck : diff leftHeight rightHeight `LTE` 1}
        -- TODO: Figure out how to make Idris2 happy about this signature
        -- -> {auto leftBoundOk  : (optional leftBounds  ((`LT` @{o} pivot) . Builtin.snd) Unit)}
        -- -> {auto rightBoundOk : (optional rightBounds ((`GT` @{o} pivot) . Builtin.fst) Unit)}

[3.677]

[3.1005]

        -> {auto heightOk : diff leftHeight rightHeight `LTE` 1}
        -> {auto leftBoundOk  : (optional leftBounds  ((\b => LT @{o} b pivot) . Builtin.snd) Unit)}
        -> {auto rightBoundOk : (optional rightBounds ((\b => GT @{o} b pivot) . Builtin.fst) Unit)}

Replacement in src/Data/AVLTree.idr at line 33 [3.160]

B:BD[3.1263] → [3.1263:1301]

  IsNode : NonEmpty (Node _ _ _ @{o})

[3.1263]

[2.197]

  IsNode : {leftTree : AVLTree t leftHeight leftBounds {o}}
         -> {pivot : t}
         -> {rightTree : AVLTree t rightHeight rightBounds {o}}
         -> {auto leftBound : (optional leftBounds  ((\b => LT @{o} b pivot) . Builtin.snd) Unit)}
         -> {auto rightBound : (optional rightBounds ((\b => GT @{o} b pivot) . Builtin.fst) Unit)}
         -> {auto height : diff leftHeight rightHeight `LTE` 1}
         -> NonEmpty (Node leftTree pivot rightTree {leftHeight} {rightHeight})

Replacement in src/Data/AVLTree.idr at line 46 [3.160]

B:BD[2.337] → [2.337:427]

  IsRotatableLeft : {leftTree : AVLTree t h1 b1 {o}} -> {rightTree : AVLTree t h2 b2 {o}}

[2.337]

[2.427]

  IsRotatableLeft : {leftTree : AVLTree t leftHeight leftBounds {o}}
                  -> {pivot : t}
                  -> {rightTree : AVLTree t rightHeight rightBounds {o}}

Replacement in src/Data/AVLTree.idr at line 50 [3.160]

B:BD[2.490] → [2.490:631]

                  -> {auto heightCheck : diff h1 h2 `LTE` 1}
                  -> RotatableLeft (Node leftTree _ rightTree {heightCheck=ok})

[2.490]

[2.631]

                  -> {auto leftBound : (optional leftBounds  ((\b => LT @{o} b pivot) . Builtin.snd) Unit)}
                  -> {auto rightBound : (optional rightBounds ((\b => GT @{o} b pivot) . Builtin.fst) Unit)}
                  -> {auto height : diff leftHeight rightHeight `LTE` 1}
                  -> RotatableLeft (Node leftTree pivot rightTree {leftHeight} {rightHeight})

Replacement in src/Data/AVLTree.idr at line 56 [3.160]

B:BD[2.686] → [2.686:1047]

  IsRotatableRight : {h1, h2 : Natural} -> {leftTree : AVLTree t h1 b1 {o}} -> {rightTree : AVLTree t h2 b2 {o}}
                   -> {auto leftNonEmpty : NonEmpty leftTree}
                   -> {auto heightCheck : diff h1 h2 `LTE` 1}
                   -> RotatableRight (Node leftTree _ rightTree {leftHeight=h1} {rightHeight=h2} {heightCheck=heightCheck})

[2.686]

[2.1047]

  IsRotatableRight : {leftTree : AVLTree t leftHeight leftBounds {o}}
                  -> {pivot : t}
                  -> {rightTree : AVLTree t rightHeight rightBounds {o}}
                  -> {auto leftNonEmpty : NonEmpty leftTree}
                  -> {auto leftBound : (optional leftBounds  ((\b => LT @{o} b pivot) . Builtin.snd) Unit)}
                  -> {auto rightBound : (optional rightBounds ((\b => GT @{o} b pivot) . Builtin.fst) Unit)}
                  -> {auto height : diff leftHeight rightHeight `LTE` 1}
                  -> RotatableRight (Node leftTree pivot rightTree {leftHeight} {rightHeight})

Replacement in src/Data/AVLTree.idr at line 69 [3.160]

B:BD[2.1332] → [2.1332:1383]

  IsRotatableLeft {heightCheck} => ?holeRotateLeft

[2.1332]

[2.1383]

  IsRotatableLeft {height} => ?holeRotateLeft

Replacement in src/Data/AVLTree.idr at line 75 [3.160]

B:BD[2.1671] → [2.1671:1724]

∅:D[2.1724] → [3.1301:1858]

B:BD[3.1301] → [3.1301:1858]

  IsRotatableRight {heightCheck} => ?holeRotateRight
partial
insert : Order t => AVLTree t h b {o} -> (x : t)
       -> Either
            (AVLTree t           h  (Some (optional b (min x . Builtin.fst) x, optional b (max x . Builtin.snd) x)) {o})
            (AVLTree t (Succesor h) (Some (optional b (min x . Builtin.fst) x, optional b (max x . Builtin.snd) x)) {o})
insert Empty x = Right $ Node Empty x Empty
insert (Node leftTree pivot rightTree {leftHeight} {rightHeight}) x =
  case compare x pivot of
    (Left equiv) => Left $ ?hole1
    (Right (Left  lt)) => ?hole2
    (Right (Right gt)) => ?hole3

[2.1671]

  IsRotatableRight {height} => ?holeRotateRight