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

{-# OPTIONS_HADDOCK not-home #-}

-- | Some internally used typelevel proofs.
module Morley.Michelson.Optimizer.Internal.Proofs
  ( module Morley.Michelson.Optimizer.Internal.Proofs
  ) where

import Prelude hiding (EQ, GT, LT)

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

import Morley.Michelson.Typed (SingT(..), T(..))
import Morley.Michelson.Typed.Instr.Constraints
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.StubbedProof
import Morley.Util.Type

dropNDropNProof
  :: forall inp out out' n m.
     ( out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True
     , out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True)
  => PeanoNatural n -> PeanoNatural m
  -> Dict (Drop (AddPeano n m) inp ~ out', IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof Zero _ = Dict
dropNDropNProof (Succ n) m = Dict
  \\ stubProof @(Drop (AddPeano n m) inp) @out' case assumeKnown @inp of
      KCons _ (_ :: Proxy xs) -> Refl \\ dropNDropNProof @xs @out @out' n m
  \\ stubProof @(IsLongerOrSameLength inp (AddPeano n m)) @'True case assumeKnown @inp of
      KCons _ (_ :: Proxy xs) -> Refl \\ dropNDropNProof @xs @out @out' n m

unpairN2isUnpairProof
  :: forall inp out pair s. (inp ~ pair : s, out ~ UnpairN ('S ('S 'Z)) pair ++ s
    , ConstraintUnpairN (ToPeano 2) pair)
  => inp :~: PairN (ToPeano 2) out
unpairN2isUnpairProof = stubProof case assumeSing @pair of
  STPair{} -> case assumeKnown @out of
    KCons{} -> Refl
  where _ = Dict @(ConstraintUnpairN (ToPeano 2) pair)

unpairNisUnpairDipUnpairNProof
  :: forall inp out pair s n. (inp ~ pair : s, out ~ UnpairN ('S n) pair ++ s, ConstraintUnpairN ('S n) pair)
  => PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof n = stubProof case assumeSing @pair of
  STPair _ (_ :: SingT r) -> case n of
    Succ Zero -> Refl
    Succ m@Succ{} -> Refl \\ unpairNisUnpairDipUnpairNProof @(r : s) @(Tail out) m
  where _ = Dict @(inp ~ pair : s)

dipPairNPairIsPairNProof
  :: forall inp n. ( n >= ToPeano 2 ~ 'True, IsLongerOrSameLength (Tail inp) n ~ 'True
                   , inp ~ Head inp : Tail inp)
  => PeanoNatural n
  -> PairN ('S n) inp :~: 'TPair (Head inp) (RightComb (LazyTake n (Tail inp))) : Drop n (Tail inp)
dipPairNPairIsPairNProof n = stubProof case (n, assumeKnown @inp) of
  (Succ Succ{}, KCons{}) -> Refl
  where _ = Dict @(n >= ToPeano 2 ~ 'True, IsLongerOrSameLength (Tail inp) n ~ 'True)

pairN2isPairProof
  :: forall inp. (IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)
  => inp :~: Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp
pairN2isPairProof = stubProof case assumeKnown @inp of
  KCons _ (_ :: Proxy xs) -> case klist @xs of
    KCons {} -> Refl
  where _ = Dict @(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)

unconsListProof
  :: forall inp n. (IsLongerOrSameLength inp ('S n) ~ 'True)
  => PeanoNatural n -> inp :~: Head inp : Tail inp
unconsListProof _ = stubProof case assumeKnown @inp of
  KCons{} -> Refl
  where _ = Dict @(IsLongerOrSameLength inp ('S n) ~ 'True)