{-# OPTIONS --cubical-compatible #-}
module Terra.Data.Nat.Functions where
open import Terra.Data.Decision
open import Terra.Data.Nat
open import Terra.Classes.Contravariant
open import Terra.Data.Negation.Instances
open import Terra.Data.Bool
open import Terra.Data.String
open import Terra.Data.Counit
open import Terra.Data.Bool.Functions
open import Terra.Data.Negation
open import Terra.Data.Equality
open import Terra.Data.Equality.Functions
open import Terra.Tactics
-- open import Terra.Data.Nat.Instances
open import Terra.Classes.Eq

open import Agda.Builtin.Nat using (_+_ ; _-_ ; _*_ ; div-helper ; mod-helper) renaming (_<_ to _<?_;_==_ to nat-eq) public


-- _+_ : Nat -> Nat -> Nat
-- zero + b = b
-- (suc a) + b = suc (a + b)

-- {-# BUILTIN NATPLUS _+_ #-}
-- infixr 5 _+_

-- _-_ : Nat -> Nat -> Nat
-- zero - zero = zero
-- zero - suc b = zero
-- suc a - zero = suc a
-- suc a - suc b = a - b

-- {-# BUILTIN NATMINUS _-_ #-}

-- _*_ : Nat -> Nat -> Nat
-- zero * b = zero
-- suc a * b = b + (a * b)

-- infixr 6 _*_

-- {-# BUILTIN NATTIMES _*_ #-}

-- _==_ : Nat -> Nat -> Bool
-- zero == zero = true
-- zero == suc b = false
-- suc a == zero = false
-- suc a == suc b = a == b

-- {-# BUILTIN NATEQUALS _==_ #-}

-- _<?_ : Nat → Nat → Bool
-- _     <? zero  = false
-- zero  <? suc _ = true
-- suc n <? suc m = n <? m

-- {-# BUILTIN NATLESS _<?_ #-}

-- div-helper : Nat → Nat → Nat → Nat → Nat
-- div-helper k m  zero    j      = k
-- div-helper k m (suc n)  zero   = div-helper (suc k) m n m
-- div-helper k m (suc n) (suc j) = div-helper k m n j

-- {-# BUILTIN NATDIVSUCAUX div-helper #-}

_/_[_] : Nat -> (d : Nat) -> ¬(d ≡ ) -> Nat
a / zero [ p ] = absurd (p refl)
a / suc b [ p ] = div-helper  b a b


-- mod-helper : Nat → Nat → Nat → Nat → Nat
-- mod-helper k m  zero    j      = k
-- mod-helper k m (suc n)  zero   = mod-helper 0 m n m
-- mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j

-- {-# BUILTIN NATMODSUCAUX mod-helper #-}

_mod_[_] : Nat -> (d : Nat) -> ¬(d ≡ ) -> Nat
a mod zero [ p ] = ⊥-elim (p refl)
a mod suc b [ p ] = mod-helper  b a b

z≤n : {n : Nat} ->  ≤ n
z≤n {zero} = orefl
z≤n {suc n} = osuc z≤n

oshift : {a b : Nat} -> a ≤ b -> suc a ≤ suc b
oshift orefl = orefl
oshift (osuc p) = osuc (oshift p)

opred : {a b : Nat} -> suc a ≤ b -> a ≤ b
opred {a} {.(suc a)} orefl = osuc orefl
opred {a} {.(suc _)} (osuc p) = osuc (opred p)

sn≰z : {n : Nat} -> suc n ≤ zero -> ⊥
sn≰z {zero} ()
sn≰z {suc n} ()

ounshift : {a b : Nat} -> suc a ≤ suc b -> a ≤ b
ounshift orefl = orefl
ounshift (osuc p) = opred p

1≤sn : {n : Nat} ->  ≤ suc n
1≤sn = oshift z≤n

pred : Nat -> Nat
pred zero = zero
pred (suc n) = n

_≤?_ : (a b : Nat) -> Decision (a ≤ b)
zero ≤? zero = yes orefl
zero ≤? suc r = yes z≤n
suc l ≤? zero = no (λ ())
suc l ≤? suc r = dec-elim (λ y → yes (oshift y))
                          (λ n → no (contramap ounshift n))
                          (l ≤? r)

≤-sandwitch : {a b : Nat} -> a ≤ b -> b ≤ a -> a ≡ b
≤-sandwitch orefl p2 = refl
≤-sandwitch (osuc p1) orefl = refl
≤-sandwitch (osuc p1) (osuc p2) = cong suc (≤-sandwitch (opred p1) (opred p2))

-- nat-show : Nat -> String
-- nat-show n = {!!}

_^_ : Nat -> Nat -> Nat
b ^ zero = 
b ^ suc n = b * (b ^ n)

max : Nat -> Nat -> Nat
max zero r = r
max (suc l) zero = suc l
max (suc l) (suc r) = suc (max l r)

≤-trans : {a b c : Nat} -> a ≤ b -> b ≤ c -> a ≤ c
≤-trans orefl r = r
≤-trans (osuc l) orefl = osuc l
≤-trans (osuc l) (osuc r) = osuc (≤-trans (osuc l) r)

<-trans : {a b c : Nat} -> a < b -> b < c -> a < c
<-trans orefl q = opred q
<-trans (osuc p) orefl = opred (osuc (oshift p))
<-trans {a} {b} {c} (osuc p) (osuc q) = osuc (<-trans (osuc p) q)

-- arith : (n d : Nat) -> n ≡ n / (suc d) [ (λ ()) ] * (suc d) + n mod (suc d) [ (λ ()) ]
-- arith zero d = refl
-- arith (suc n) zero = {!!}
-- arith (suc n) (suc d) = {!!}