module FL where

open import Level hiding ( suc ; zero )
open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
open import Data.Fin.Permutation
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
open import Relation.Binary.PropositionalEquality 
open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
open import Data.Product
open import Relation.Nullary
open import Data.Empty
open import  Relation.Binary.Core
open import  Relation.Binary.Definitions
open import logic
open import nat

infixr  100 _::_

data  FL : (n : ℕ )→ Set where
   f0 :  FL 0 
   _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
   f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
   f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )

FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n}  → xn :: x ≡ yn :: y → ( xn ≡ yn )  × (x ≡ y )
FLeq refl = refl , refl 

f-<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
f-<> (f<n x) (f<n x₁) = nat-<> x x₁
f-<> (f<n x) (f<t lt2) = nat-≡< refl x
f-<> (f<t lt) (f<n x) = nat-≡< refl x
f-<> (f<t lt) (f<t lt2) = f-<> lt lt2

f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
f-≡< refl (f<n x) = nat-≡< refl x
f-≡< refl (f<t lt) = f-≡< refl lt 

FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt  → f-<> lt (f<n a) )
... | tri> ¬a ¬b c = tri> (λ lt  → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c)
... | tri≈ ¬a refl ¬c with FLcmp xt yt
... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt  → f-<> lt (f<t a) )
... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt )  refl (λ lt → f-≡< refl lt )
... | tri> ¬a₁ ¬b c = tri> (λ lt  → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)

f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ )
f<-trans {suc n} (f<n x) (f<t y<z) = f<n x
f<-trans {suc n} (f<t x<y) (f<n x) = f<n x
f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z)

infixr 250 _f<?_

_f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
x f<? y with FLcmp x y
... | tri< a ¬b ¬c = yes a
... | tri≈ ¬a refl ¬c = no ( ¬a )
... | tri> ¬a ¬b c = no ( ¬a )

_f≤_ : {n : ℕ } (x : FL n ) (y : FL n)  → Set
_f≤_ x y = (x ≡ y ) ∨  (x f< y )

FL0 : {n : ℕ } → FL n
FL0 {zero} = f0
FL0 {suc n} = zero :: FL0


fmax : { n : ℕ } →  FL n
fmax {zero} = f0
fmax {suc n} = fromℕ< a<sa :: fmax {n}

fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
    fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
    fmax1 {zero} zero = z≤n
    fmax1 {suc n} zero = z≤n
    fmax1 {suc n} (suc x) = s≤s (fmax1 x) 
fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt

fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl ) 
fmax¬ {suc n} {x} ne with FLcmp x fmax
... | tri< a ¬b ¬c = a
... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
... | tri> ¬a ¬b c = ⊥-elim (fmax< c)

FL0≤ : {n : ℕ } → FL0 {n} f≤ fmax
FL0≤ {zero} = case1 refl
FL0≤ {suc zero} = case1 refl
FL0≤ {suc n} with <-fcmp zero (fromℕ< {n} a<sa)
... | tri< a ¬b ¬c = case2 (f<n a)
... | tri≈ ¬a b ¬c with FL0≤ {n}
... | case1 x = case1 (subst₂ (λ j k → (zero :: FL0) ≡ (j :: k ) ) b x refl )
... | case2 x = case2 (subst (λ k →  (zero :: FL0) f< (k :: fmax)) b (f<t x)  )

open import Relation.Binary as B hiding (Decidable; _⇔_)

-- f≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_f≤_ {n})
-- f≤-isDecTotalOrder = record { isTotalOrder = record { isPartialOrder = record { isPreorder = {!!}
--         ; antisym = {!!}
--         }
--      ; total = {!!}
--      }
--   ; _≟_          = {!!}
--   ; _≤?_         = {!!}
--   }

open import Data.Sum.Base as Sum --  inj₁

total : {n : ℕ } → Total (_f≤_ {n})
total f0 f0 = inj₁  (case1 refl) 
total (x :: xt) (y :: yt) with <-fcmp x y
... | tri< a ¬b ¬c = inj₁ (case2 (f<n a))
... | tri> ¬a ¬b c = inj₂ (case2 (f<n c))
... | tri≈ ¬a b ¬c with FLcmp xt yt
... | tri< a ¬b ¬c₁ = inj₁ (case2 (subst (λ k → (x :: xt ) f< (k :: yt) ) b (f<t a)))
... | tri≈ ¬a₁ b₁ ¬c₁ = inj₁ (case1 (subst₂ (λ j k → j :: k ≡ y :: yt ) (sym b)  (sym b₁ ) refl  ))
... | tri> ¬a₁ ¬b c = inj₂ (case2 (subst (λ k → (y :: yt ) f< (k :: xt) ) (sym b) (f<t c)))

open import Relation.Nary using (⌊_⌋)
open import Data.List.Fresh
open import Data.List.Fresh.Relation.Unary.All
open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)

FList : {n : ℕ } → Set
FList {n} = List# (FL n) ⌊ _f<?_ ⌋

fr1 : FList
fr1 =
   ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
   ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
   ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
   ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
   []

open import Data.Product
-- open import Data.Maybe
-- open TotalOrder

open import Relation.Nullary.Decidable hiding (⌊_⌋)
open import Data.Bool -- hiding (T)
open import Data.Unit.Base using (⊤ ; tt)

-- T : Data.Bool.Bool → Set
-- T true  = ⊤
-- T false = ⊥

--  fresh a []        = ⊤
--  fresh a (x ∷# xs) = R a x × fresh a xs

-- toWitness
-- ttf< :  {n : ℕ } → {x a : FL n } → x f< a  → T (isYes (x f<? a))
-- ttf< {n} {x} {a} x<a with x f<? a
-- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
-- ... | no nn = ⊥-elim ( nn x<a )

ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
ttf _ [] fr = Level.lift tt
ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where 
       ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
       ttf1 t x<a = f<-trans x<a (toWitness t)

FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
FLinsert {zero} f0 y = f0 ∷# []
FLinsert {suc n} x [] = x ∷# []
FLinsert {suc n} x (cons a y x₁) with total x a
... | inj₁ (case1 eq) = cons a y x₁
FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
... | inj₂ (case1 eq) = cons a y x₁
FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) []
... | [] | ()
... | cons a₁ t x₂ | e = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 a<x) with total x a₁
... | inj₁ (case1 refl) =  cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
... | inj₂ (case1 refl) =  cons a (cons a₁ y x₂) (Level.lift a<a₁ , fr-ay)
... | inj₁ (case2 x<a₁) =  cons a (cons x  (cons a₁ y x₂) ( Level.lift (fromWitness x<a₁) , ttf x<a₁ y x₂))
                   (  Level.lift (fromWitness a<x) , ttf a<x (cons  a₁ y x₂) ( Level.lift (fromWitness x<a₁) , ttf x<a₁ y x₂))
... | inj₂ (case2 a₁<x) with FLinsert x y
... | [] = []
... | cons a₂ t x₁ = cons a ( cons a₁ ( cons a₂ t x₁ ) ( Level.lift (fromWitness ttf0) , ttf ttf0 t x₁))
               ( Level.lift a<a₁ ,  Level.lift (fromWitness ttf1) , ttf ttf1 t x₁ ) where
    ttf0 : a₁ f< a₂
    ttf0 = ?
    ttf1 : a  f< a₂
    ttf1 = f<-trans (toWitness a<a₁) ttf0 


-- a₁<x  : a₁ f< x
-- a<x   : a f< x
-- a<a₁  : T (isYes (a f<? a₁ | FLcmp a a₁))


fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1