-- 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 :: forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
       (m :: Peano).
(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 PeanoNatural n
Zero PeanoNatural m
_ = Dict (out' ~ out', 'True ~ 'True)
Dict
  (Drop (AddPeano n m) inp ~ out',
   IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
dropNDropNProof (Succ PeanoNatural m
n) PeanoNatural m
m = Dict (out' ~ out', 'True ~ 'True)
Dict
  (Drop ('S (AddPeano m m)) inp ~ out',
   IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
(Drop ('S (AddPeano m m)) inp ~ out') =>
Dict
  (Drop ('S (AddPeano m m)) inp ~ out',
   IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
  ((Drop ('S (AddPeano m m)) inp ~ out') =>
 Dict
   (Drop ('S (AddPeano m m)) inp ~ out',
    IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True))
-> (Drop ('S (AddPeano m m)) inp :~: out')
-> Dict
     (Drop ('S (AddPeano m m)) inp ~ out',
      IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (b :: [k]). (Stubbed => a :~: b) -> a :~: b
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof @(Drop (AddPeano n m) inp) @out' case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
      KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> out' :~: out'
Drop (AddPeano m m) xs :~: out'
(Drop (AddPeano m m) xs ~ out', 'True ~ 'True) =>
Drop (AddPeano m m) xs :~: out'
forall {k} (a :: k). a :~: a
Refl ((Drop (AddPeano m m) xs ~ out', 'True ~ 'True) =>
 Drop (AddPeano m m) xs :~: out')
-> Dict (Drop (AddPeano m m) xs ~ out', 'True ~ 'True)
-> Drop (AddPeano m m) xs :~: out'
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
       (m :: Peano).
(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)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
       (m :: Peano).
(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 @xs @out @out' PeanoNatural m
n PeanoNatural m
m
  ((IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True) =>
 Dict
   (Drop ('S (AddPeano m m)) inp ~ out',
    IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True))
-> (IsLongerOrSameLength inp ('S (AddPeano m m)) :~: 'True)
-> Dict
     (Drop ('S (AddPeano m m)) inp ~ out',
      IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: Bool) (b :: Bool). (Stubbed => a :~: b) -> a :~: b
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof @(IsLongerOrSameLength inp (AddPeano n m)) @'True case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
      KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerOrSameLength xs (AddPeano m m) :~: 'True
(Drop (AddPeano m m) xs ~ out',
 IsLongerOrSameLength xs (AddPeano m m) ~ 'True) =>
IsLongerOrSameLength xs (AddPeano m m) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((Drop (AddPeano m m) xs ~ out',
  IsLongerOrSameLength xs (AddPeano m m) ~ 'True) =>
 IsLongerOrSameLength xs (AddPeano m m) :~: 'True)
-> Dict
     (Drop (AddPeano m m) xs ~ out',
      IsLongerOrSameLength xs (AddPeano m m) ~ 'True)
-> IsLongerOrSameLength xs (AddPeano m m) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
       (m :: Peano).
(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)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
       (m :: Peano).
(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 @xs @out @out' PeanoNatural m
n PeanoNatural m
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 :: forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T]).
(inp ~ (pair : s), out ~ (UnpairN ('S ('S 'Z)) pair ++ s),
 ConstraintUnpairN (ToPeano 2) pair) =>
inp :~: PairN (ToPeano 2) out
unpairN2isUnpairProof = (Stubbed =>
 inp
 :~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out))
-> inp
   :~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (x :: k). Stubbed => Sing x
forall {k} (x :: k). Sing x
forall (x :: T). Sing x
assumeSing @pair of
  STPair{} -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [T]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @out of
    KCons{} -> inp :~: inp
inp
:~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out)
forall {k} (a :: k). a :~: a
Refl
  where Dict (ConstraintUnpairN (ToPeano 2) pair)
_ = forall (a :: Constraint). a => Dict a
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 :: forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T])
       (n :: Peano).
(inp ~ (pair : s), out ~ (UnpairN ('S n) pair ++ s),
 ConstraintUnpairN ('S n) pair) =>
PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof PeanoNatural n
n = (Stubbed => pair :~: RightComb (Head out : LazyTake n (Tail out)))
-> pair :~: RightComb (Head out : LazyTake n (Tail out))
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (x :: k). Stubbed => Sing x
forall {k} (x :: k). Sing x
forall (x :: T). Sing x
assumeSing @pair of
  STPair Sing n1
_ (SingT n2
_ :: SingT r) -> case PeanoNatural n
n of
    Succ PeanoNatural m
Zero -> pair :~: pair
pair :~: RightComb (Head out : LazyTake n (Tail out))
forall {k} (a :: k). a :~: a
Refl
    Succ m :: PeanoNatural m
m@Succ{} -> pair :~: pair
pair :~: RightComb (Head out : LazyTake n (Tail out))
(n2
 ~ RightComb
     (Head (UnpairN ('S ('S m)) n2 ++ s)
        : Head (Tail (UnpairN ('S ('S m)) n2 ++ s))
        : LazyTake m (Tail (Tail (UnpairN ('S ('S m)) n2 ++ s))))) =>
pair :~: RightComb (Head out : LazyTake n (Tail out))
forall {k} (a :: k). a :~: a
Refl ((n2
  ~ RightComb
      (Head (UnpairN ('S ('S m)) n2 ++ s)
         : Head (Tail (UnpairN ('S ('S m)) n2 ++ s))
         : LazyTake m (Tail (Tail (UnpairN ('S ('S m)) n2 ++ s))))) =>
 pair :~: RightComb (Head out : LazyTake n (Tail out)))
-> (n2
    :~: RightComb
          (Head (UnpairN ('S ('S m)) n2 ++ s)
             : Head (Tail (UnpairN ('S ('S m)) n2 ++ s))
             : LazyTake m (Tail (Tail (UnpairN ('S ('S m)) n2 ++ s)))))
-> pair :~: RightComb (Head out : LazyTake n (Tail out))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T])
       (n :: Peano).
(inp ~ (pair : s), out ~ (UnpairN ('S n) pair ++ s),
 ConstraintUnpairN ('S n) pair) =>
PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof @(r : s) @(Tail out) PeanoNatural m
m
  where Dict (inp ~ (pair : s))
_ = forall (a :: Constraint). a => Dict a
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 :: forall (inp :: [T]) (n :: Peano).
((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 PeanoNatural n
n = (Stubbed =>
 (RightComb (Head inp : LazyTake n (Tail inp)) : Drop n (Tail inp))
 :~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
        : Drop n (Tail inp)))
-> (RightComb (Head inp : LazyTake n (Tail inp))
      : Drop n (Tail inp))
   :~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
          : Drop n (Tail inp))
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case (PeanoNatural n
n, forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [T]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp) of
  (Succ Succ{}, KCons{}) -> (RightComb (Head inp : LazyTake n (Tail inp)) : Drop n (Tail inp))
:~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
       : Drop n (Tail inp))
(RightComb (Head inp : LazyTake n (Tail inp)) : Drop n (Tail inp))
:~: (RightComb (Head inp : LazyTake n (Tail inp))
       : Drop n (Tail inp))
forall {k} (a :: k). a :~: a
Refl
  where Dict
  ((n >= ToPeano 2) ~ 'True,
   IsLongerOrSameLength (Tail inp) n ~ 'True)
_ = forall (a :: Constraint). a => Dict a
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 :: forall {k} (inp :: [k]).
(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True) =>
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
pairN2isPairProof = (Stubbed =>
 inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp))
-> inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
  KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> case forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @xs of
    KCons {} -> inp :~: inp
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
forall {k} (a :: k). a :~: a
Refl
  where Dict (IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)
_ = forall (a :: Constraint). a => Dict a
Dict @(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)

unconsListProof
  :: forall inp n. (IsLongerOrSameLength inp ('S n) ~ 'True)
  => PeanoNatural n -> inp :~: Head inp : Tail inp
unconsListProof :: forall {a} (inp :: [a]) (n :: Peano).
(IsLongerOrSameLength inp ('S n) ~ 'True) =>
PeanoNatural n -> inp :~: (Head inp : Tail inp)
unconsListProof PeanoNatural n
_ = (Stubbed => inp :~: (Head inp : Tail inp))
-> inp :~: (Head inp : Tail inp)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [a]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
  KCons{} -> inp :~: inp
inp :~: (Head inp : Tail inp)
forall {k} (a :: k). a :~: a
Refl
  where Dict (IsLongerOrSameLength inp ('S n) ~ 'True)
_ = forall (a :: Constraint). a => Dict a
Dict @(IsLongerOrSameLength inp ('S n) ~ 'True)