-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_HADDOCK not-home #-}

-- | Module, containing some internally used typelevel proofs.
module Morley.Michelson.Typed.Instr.Internal.Proofs
  ( module Morley.Michelson.Typed.Instr.Internal.Proofs
  ) where

import Prelude hiding (EQ, GT, LT)

import Data.Constraint (Dict(..), (\\))
import Data.Type.Equality ((:~:)(..))

import Morley.Michelson.Typed.Instr.Constraints
import Morley.Michelson.Typed.TypeLevel
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.StubbedProof
import Morley.Util.Type (KList(..), type (++))

assocThm :: forall a b c. (a ++ b) ++ c :~: a ++ (b ++ c)
assocThm = stubProof $ case assumeKnown @a of
  KNil -> Refl
  KCons _ (_ :: Proxy xs) -> Refl \\ assocThm @xs @b @c

takeExtensionThm
  :: forall a s n. IsLongerOrSameLength a n ~ 'True
  => PeanoNatural n
  -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm n = stubProof $ case n of
  Zero -> Refl
  Succ m -> case assumeKnown @a of
    KCons _ (_ :: Proxy xs) -> Refl \\ takeExtensionThm @xs @s m

dropExtensionThm
  :: forall a s n. IsLongerOrSameLength a n ~ 'True
  => PeanoNatural n
  -> Drop n (a ++ s) :~: Drop n a ++ s
dropExtensionThm n = stubProof $ case n of
  Zero -> Refl
  Succ m -> case assumeKnown @a of
    KCons _ (_ :: Proxy xs) -> Refl \\ dropExtensionThm @xs @s m

isLongerOrSameLengthExtThm
  :: forall a s n. IsLongerOrSameLength a n ~ 'True
  => PeanoNatural n
  -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm n = stubProof $ case n of
  Zero -> Refl
  Succ m -> case assumeKnown @a of
    KCons _ (_ :: Proxy xs) -> Refl \\ isLongerOrSameLengthExtThm @xs @s m

isLongerOrSameLengthDecThm
  :: forall a m. IsLongerOrSameLength a ('S m) ~ 'True
  => PeanoNatural ('S m)
  -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm n = stubProof $ case n of
  Succ Zero -> Refl
  Succ (Succ m) -> case assumeKnown @a of
    KCons _ (_ :: Proxy xs) -> Refl \\ isLongerOrSameLengthDecThm @xs (Succ m)

isLongerThanExtThm
  :: forall a s n. IsLongerThan a n ~ 'True
  => PeanoNatural n
  -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm n = stubProof $ case n of
  Zero -> case assumeKnown @a of
    KCons{} -> Refl
  Succ m -> case assumeKnown @a of
    KCons _ (_ :: Proxy xs) -> Refl \\ isLongerThanExtThm @xs @s m

dropHeadThm
  :: forall x a n. IsLongerThan (x : a) n ~ 'True
  => PeanoNatural n
  -> IsLongerOrSameLength a n :~: 'True
dropHeadThm n = stubProof $ case n of
  Zero -> Refl
  Succ m -> case assumeKnown @a of
    KCons (_ :: Proxy y) (_ :: Proxy xs) -> Refl \\ dropHeadThm @y @xs m

isLongerThanIncThm
  :: forall a n. IsLongerThan a n ~ 'True
  => PeanoNatural n
  -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm n = stubProof $ case n of
  Zero -> case assumeKnown @a of
    KCons{} -> Refl
  Succ m -> case assumeKnown @a of
    KCons _ (_ :: Proxy xs) -> Refl \\ isLongerThanIncThm @xs m

dugLengthThm
  :: forall b x n. IsLongerThan b n ~ 'True
  => PeanoNatural n
  -> IsLongerThan (x ': LazyTake n b ++ Drop ('S n) b) n :~: 'True
dugLengthThm n = stubProof $ case n of
  Zero -> Refl
  Succ m -> case assumeKnown @b of
    KCons (_ :: Proxy y) (_ :: Proxy xs) -> Refl \\ dugLengthThm @xs @y m

dropNExtensionThm
  :: forall s a b n. (Drop n a ~ b, IsLongerOrSameLength a n ~ 'True)
  => PeanoNatural n
  -> Dict (Drop n (a ++ s) ~ b ++ s, IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm n = Dict
  \\ dropExtensionThm @a @s n
  \\ isLongerOrSameLengthExtThm @a @s n

dupNExtensionThm
  :: forall s a b n x. (ConstraintDUPN n a b x)
  => PeanoNatural n
  -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm n@(Succ m) = Dict
  \\ isLongerOrSameLengthExtThm @a @s n
  \\ assocThm @(LazyTake (Decrement n) a) @(x : Drop n a) @s
  \\ takeExtensionThm @a @s m \\ isLongerOrSameLengthDecThm @a n
  \\ dropExtensionThm @a @s n

dugNExtensionThm
  :: forall s a b x r n. (a ~ x : r, ConstraintDUG n a b x)
  => PeanoNatural n
  -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm n = Dict
  \\ isLongerThanExtThm @b @s n
  \\ assocThm @(LazyTake n b) @(Drop ('S n) b) @s
  \\ takeExtensionThm @b @s n \\ isLongerOrSameLengthDecThm @b (Succ n)
  \\ dropExtensionThm @b @s (Succ n)
  \\ isLongerThanIncThm @b n
  \\ assocThm @(LazyTake n r) @(x : Drop n r) @s
  \\ takeExtensionThm @r @s n \\ dropExtensionThm @r @s n \\ dropHeadThm @x @r n
  \\ dugLengthThm @b @x n

digNExtensionThm
  :: forall s a b x r n. (b ~ x : r, ConstraintDIG n a b x)
  => PeanoNatural n
  -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm n = Dict
  \\ isLongerThanExtThm @a @s n
  \\ assocThm @(LazyTake n a) @(Drop ('S n) a) @s
  \\ takeExtensionThm @a @s n \\ isLongerOrSameLengthDecThm @a (Succ n)
  \\ dropExtensionThm @a @s (Succ n)
  \\ isLongerThanIncThm @a n
  \\ assocThm @(LazyTake n r) @(x : Drop n r) @s
  \\ takeExtensionThm @r @s n \\ dropExtensionThm @r @s n \\ dropHeadThm @x @r n
  \\ dugLengthThm @a @x n

dipNExtensionThm
  :: forall s a b s1 s1' n. ConstraintDIPN n a b s1 s1'
  => PeanoNatural n
  -> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm n = Dict
  \\ isLongerOrSameLengthExtThm @a @s n
  \\ dropExtensionThm @a @s n
  \\ assocThm @(LazyTake n a) @s1' @s
  \\ takeExtensionThm @a @s n
  \\ assocThm @(LazyTake n a) @s1 @s
  \\ dropExtensionThm @b @s n
  \\ isLongerOrSameLengthExtThm @b @s n
  \\ dipNExtensionLemma @a @b @s1' n

dipNExtensionLemma ::
  forall inp out s n.
    ( RequireLongerOrSameLength inp n
    , LazyTake n inp ++ s ~ out)
  => PeanoNatural n
  -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma n = stubProof $ case n of
  Zero -> Refl
  Succ m -> case (assumeKnown @inp, assumeKnown @out) of
    (KCons _ (_ :: Proxy inp'), KCons _ (_ :: Proxy out')) ->
      Refl \\ dipNExtensionLemma @inp' @out' @s m

pairNExtensionThm
  :: forall s a n. (n >= ToPeano 2 ~ 'True, IsLongerOrSameLength a n ~ 'True)
  => PeanoNatural n
  -> Dict (ConstraintPairN n (a ++ s)
      , RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a)
      , Drop n (a ++ s) ~ (Drop n a ++ s)
      )
pairNExtensionThm n = Dict
  \\ isLongerOrSameLengthExtThm @a @s n
  \\ dropExtensionThm @a @s n
  \\ takeExtensionThm @a @s n

unpairNExtensionThm
  :: forall s a b n x r
    . ( a ~ x : r, CombedPairLeafCountIsAtLeast n x ~ 'True
      , n >= ToPeano 2 ~ 'True, UnpairN n x ++ r ~ b
      )
  => PeanoNatural n
  -> Dict (ConstraintUnpairN n x, UnpairN n x ++ r ++ s ~ b ++ s)
unpairNExtensionThm _ = Dict \\ assocThm @(UnpairN n x) @r @s
  where _ = Dict @(a ~ x : r)