include "basics/types.ma".
include "basics/lists/list.ma".
include "arithmetics/nat.ma".
include "common/Integers.ma".

include "ASM/Util.ma".

axiom priority_set: Type[0] → Type[0].
  
axiom pset_empty: ∀elt_type. priority_set elt_type.
axiom pset_size: ∀elt_type. priority_set elt_type → nat.
  
axiom pset_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
  
axiom pset_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
axiom pset_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
axiom pset_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.
  
axiom pset_increment: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
axiom pset_incrementifx: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
axiom pset_modify: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
axiom pset_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat).
  
axiom pset_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
  
axiom pset_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.
axiom pset_fold: ∀elt_type. ∀a: Type[0]. (elt_type → int → a → a) → priority_set elt_type → a → a.

definition pset_is_empty ≝
  λelt_type         : Type[0].
  λpriority_set     : priority_set elt_type.
    pset_size … priority_set = 0.

definition pset_singleton ≝
  λelt_type        : Type[0].
  λelt             : elt_type.
  λpriority        : nat.
    pset_insert … elt priority (pset_empty elt_type).

definition pset_from_list ≝
  λelt_type        : Type[0].
  λthe_list        : list (elt_type × nat).
    foldr … (λelt_priority.
      let 〈elt, priority〉 ≝ elt_priority in
        pset_insert elt_type elt priority)
          (pset_empty …) the_list.