open import Relation.Binary  using (Rel; Decidable)
open import Relation.Nullary using (yes; no; ¬_)
open import Level            using (Level)

module insertionSort {A : Set} {ℓ : Level} {_≈_ _≤_ : Rel A ℓ}
                     (_≤?_ : Decidable _≤_) (_=?_ : Decidable _≈_) where

--                      (ord : TotalOrder ℓ ℓ ℓ) -- _≈_ _≤_) where

-- open TotalOrder ord          using (total; equivalence)
-- open Equivalence equivalence using (refl)

open import Data.Bool       using (Bool; true; false; _∧_; _∨_)
open import Data.List       using (List; []; _∷_; [_])
-- open import Function                                        using (_∘_; flip)
-- open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; sym)
-- open PropEq.≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
-- import Algebra.FunctionProperties as P; open P (_≡_ {A = ℕ})

ins : A → List A → List A
ins a []              = [ a ]
ins a (b ∷ x) with a ≤? b
... | yes _ = a ∷ (b ∷ x)
... | no _  = b ∷ ins a x

sort : List A → List A
sort []      = []
sort (a ∷ x) = ins a (sort x)

sorted : List A → Bool
sorted []          = true
sorted (_ ∷ [])    = true
sorted (a ∷ b ∷ x) with a ≤? b
... | yes _ = sorted (b ∷ x)
... | no  _ = false

elem : A → List A → Bool
elem a []      = false
elem a (b ∷ x) with a =? b
... | yes _ = true
... | no  _ = elem a x

delete : A → List A → List A
delete a [] = []
delete a (b ∷ x) with a =? b 
... | yes _ = x
... | no  _ = b ∷ delete a x

permutation : List A → List A → Bool
-- permutation x y = (x is a permutation of y)
permutation []      [] = true
permutation []      _  = false
permutation (a ∷ x) y  = elem a y ∧ permutation x (delete a y)  

sortCorrect : ∀ {x : List A} → Bool
sortCorrect {x} = sorted (sort x) ∧ permutation (sort x) x