# LANGUAGE ScopedTypeVariables #
# LANGUAGE TypeOperators #
# LANGUAGE KindSignatures #
# LANGUAGE DataKinds #
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
# LANGUAGE FlexibleContexts #
{-# LANGUAGE RankNTypes #-}

module Elevator.Safe.Floor where

import Data.Type.Nat
import Data.Type.Nat.LE
import Data.Type.Equality
import Data.Type.Dec


type GoodFloor mx cur = (SNatI mx, SNatI cur, LE cur mx)
type BelowTop mx cur = LE (S cur) mx

data Floor (mx :: Nat) (cur :: Nat) where
  MkFloor :: GoodFloor mx cur => Floor mx cur

instance Show (Floor mx cur) where
  show MkFloor = "Floor " <> show (snatToNat (snat :: SNat cur))
                 <> " of " <> show (snatToNat (snat :: SNat mx))

next :: BelowTop mx cur => Floor mx cur -> Floor mx (S cur)
next MkFloor = MkFloor

prev :: forall mx cur. Floor mx (S cur) -> Floor mx cur
prev MkFloor =
  withSNat snatCur $
    withLEProof leCur
      MkFloor
 where
   snatCur :: SNat cur
   snatCur = case snat :: SNat (S cur) of
               SS -> snat
   leCur :: LEProof cur mx
   leCur = leStepL leProof

sameFloor :: forall mx to from.
             Floor mx to -> Floor mx from -> Maybe (to :~: from)
sameFloor MkFloor MkFloor = eqNat

mkFloor :: forall mx cur. (SNatI mx, SNatI cur) => Maybe (Floor mx cur)
mkFloor =
  case decideLE :: Dec (LEProof cur mx) of
    Yes prf -> withLEProof prf $ Just MkFloor
    No _ -> Nothing

# LANGUAGE GADTs #
# LANGUAGE ConstraintKinds #
# LANGUAGE RankNTypes #
# LANGUAGE ScopedTypeVariables #
# LANGUAGE TypeOperators #
# LANGUAGE KindSignatures #
# LANGUAGE DataKinds #
# LANGUAGE FlexibleContexts #

module Elevator.Safe.Floor where

import Data.Type.Nat
import Data.Type.Nat.LE
import Data.Type.Equality
import Data.Type.Dec


type GoodFloor mx cur = (SNatI mx, SNatI cur, LE cur mx)
type BelowTop mx cur = LE (S cur) mx

data Floor (mx :: Nat) (cur :: Nat) where
  MkFloor :: GoodFloor mx cur => Floor mx cur

instance Show (Floor mx cur) where
  show MkFloor = "Floor " <> show (snatToNat (snat :: SNat cur))
                 <> " of " <> show (snatToNat (snat :: SNat mx))

next :: BelowTop mx cur => Floor mx cur -> Floor mx (S cur)
next MkFloor = MkFloor

prev :: forall mx cur. Floor mx (S cur) -> Floor mx cur
prev MkFloor =
  withSNat snatCur $
    withLEProof leCur
      MkFloor
 where
   snatCur :: SNat cur
   snatCur = case snat :: SNat (S cur) of
               SS -> snat
   leCur :: LEProof cur mx
   leCur = leStepL leProof

sameFloor :: forall mx to from.
             Floor mx to -> Floor mx from -> Maybe (to :~: from)
sameFloor MkFloor MkFloor = eqNat

mkFloor :: forall mx cur. (SNatI mx, SNatI cur) => Maybe (Floor mx cur)
mkFloor =
  case decideLE :: Dec (LEProof cur mx) of
    Yes prf -> withLEProof prf $ Just MkFloor
    No _ -> Nothing
