module UVMHS.Core.Data.Lattice where

import UVMHS.Core.Init
import UVMHS.Core.Classes
import UVMHS.Core.Data.Arithmetic ()

-- The supplied function should be monotonic
lfp ∷ (POrd a) ⇒ a → (a → a) → a
lfp :: forall a. POrd a => a -> (a -> a) -> a
lfp a
i a -> a
f = a -> a
loop a
i 
  where
   loop :: a -> a
loop a
x =
     let x' :: a
x' = a -> a
f a
x
     in case a
x' a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
x of
       𝔹
True → a
x 
       𝔹
False → a -> a
loop a
x'

lfpN ∷ (POrd a) ⇒ ℕ → a → (a → a) → a
lfpN :: forall a. POrd a => ℕ -> a -> (a -> a) -> a
lfpN ℕ
n₀ a
i a -> a
f = ℕ -> a -> a
loop ℕ
n₀ a
i 
  where
    loop :: ℕ -> a -> a
loop ℕ
n a
x
      | ℕ
n ℕ -> ℕ -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ
0 = a
x
      | 𝔹
otherwise = 
          let x' :: a
x' = a -> a
f a
x
          in case a
x' a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
x of
            𝔹
True → a
x 
            𝔹
False → ℕ -> a -> a
loop (ℕ
n ℕ -> ℕ -> ℕ
forall a. Minus a => a -> a -> a
- ℕ
1) a
x'

-- The supplied function should be antitonic
gfp ∷ (POrd a) ⇒ a → (a → a) → a
gfp :: forall a. POrd a => a -> (a -> a) -> a
gfp a
i a -> a
f = a -> a
loop a
i 
  where
    loop :: a -> a
loop a
x = 
      let x' :: a
x' = a -> a
f a
x
      in case a
x a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
x' of
        𝔹
True → a
x
        𝔹
False → a -> a
loop a
x'

gfpN ∷ (POrd a) ⇒ ℕ → a → (a → a) → a
gfpN :: forall a. POrd a => ℕ -> a -> (a -> a) -> a
gfpN ℕ
n₀ a
i a -> a
f = ℕ -> a -> a
loop ℕ
n₀ a
i 
  where
    loop :: ℕ -> a -> a
loop ℕ
n a
x 
      | ℕ
n ℕ -> ℕ -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ
0 = a
x
      | 𝔹
otherwise = 
          let x' :: a
x' = a -> a
f a
x
          in case a
x a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
x' of
            𝔹
True → a
x
            𝔹
False → ℕ -> a -> a
loop (ℕ
n ℕ -> ℕ -> ℕ
forall a. Minus a => a -> a -> a
- ℕ
1) a
x'