(.using
 [library
  [lux (.except)
   [abstract
    [equivalence (.only Equivalence)]
    [monad (.only do)]]
   [control
    ["[0]" maybe]]
   [data
    [collection
     ["[0]" tree
      ["[1]" finger (.only Tree)]]]]
   [math
    [number
     ["n" nat (.open: "[1]#[0]" interval)]]]
   [type (.only by_example)
    [primitive (.only primitive abstraction representation)]]]])

(type: .public Priority
  Nat)

(def .public max
  Priority
  n#top)

(def .public min
  Priority
  n#bottom)

(def builder
  (tree.builder n.maximum))

(def :@:
  (by_example [@]
    (is (tree.Builder @ Priority)
        ..builder)
    @))

(primitive .public (Queue a)
  (Maybe (Tree :@: Priority a))

  (def .public empty
    Queue
    (abstraction {.#None}))

  (def .public (front queue)
    (All (_ a) (-> (Queue a) (Maybe a)))
    (do maybe.monad
      [tree (representation queue)]
      (tree.one (n.= (tree.tag tree))
                tree)))

  (def .public (size queue)
    (All (_ a) (-> (Queue a) Nat))
    (case (representation queue)
      {.#None}
      0

      {.#Some tree}
      (loop (again [node tree])
        (case (tree.root node)
          {0 #0 _}
          1

          {0 #1 [left right]}
          (n.+ (again left) (again right))))))

  (def .public (member? equivalence queue member)
    (All (_ a) (-> (Equivalence a) (Queue a) a Bit))
    (case (representation queue)
      {.#None}
      false

      {.#Some tree}
      (loop (again [node tree])
        (case (tree.root node)
          {0 #0 reference}
          (at equivalence = reference member)

          {0 #1 [left right]}
          (or (again left)
              (again right))))))

  (def .public (next queue)
    (All (_ a) (-> (Queue a) (Queue a)))
    (abstraction
     (do maybe.monad
       [tree (representation queue)
        .let [highest_priority (tree.tag tree)]]
       (loop (again [node tree])
         (case (tree.root node)
           {0 #0 reference}
           (if (n.= highest_priority (tree.tag node))
             {.#None}
             {.#Some node})

           {0 #1 left right}
           (if (n.= highest_priority (tree.tag left))
             (case (again left)
               {.#None}
               {.#Some right}

               {.#Some =left}
               {.#Some (at ..builder branch =left right)})
             (case (again right)
               {.#None}
               {.#Some left}

               {.#Some =right}
               {.#Some (at ..builder branch left =right)})))))))

  (def .public (end priority value queue)
    (All (_ a) (-> Priority a (Queue a) (Queue a)))
    (let [addition (at ..builder leaf priority value)]
      (abstraction
       (case (representation queue)
         {.#None}
         {.#Some addition}

         {.#Some tree}
         {.#Some (at ..builder branch tree addition)}))))
  )

(def .public empty?
  (All (_ a) (-> (Queue a) Bit))
  (|>> ..size (n.= 0)))