-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{- |
This module contains the logic to lookup 'Var's in a stack and the actions to
manipulate it.

For efficiency, actions are implemented using Lorentz macros.
To do so every necessary constraint is checked at runtime.
-}

module Indigo.Internal.Lookup
  ( -- * Variable Lookup Actions
    varActionGet
  , varActionSet
  , varActionUpdate
  , varActionOperation

  -- * Vinyl manipulation helpers
  , rtake
  , rdrop
  ) where

import Data.Constraint (Dict(..), HasDict)
import Data.Singletons (Sing, SingI(..))
import Data.Type.Equality (TestEquality(..))
import Data.Typeable ((:~:)(..), eqT)
import Data.Vinyl ((<+>))
import Data.Vinyl.TypeLevel (type (++))
import Prelude hiding (tail)

import Indigo.Internal.Object (HasSideEffects, IndigoObjectF(..), Ops, operationsVar)
import Indigo.Internal.State (RefId, StackVars, StkEl(..))
import Indigo.Lorentz
import qualified Lorentz.Instr as L
import qualified Lorentz.Macro as L
import Michelson.Typed (ToTs)
import qualified Michelson.Typed.Instr as MI
import qualified Michelson.Typed.T as MI
import Util.Peano

----------------------------------------------------------------------------
-- Variable Lookup Actions
----------------------------------------------------------------------------

-- | Puts a copy of the value for the given 'Var' on top of the stack
varActionGet :: forall a stk . KnownValue a => RefId -> StackVars stk -> stk :-> a & stk
varActionGet :: RefId -> StackVars stk -> stk :-> (a & stk)
varActionGet ref :: RefId
ref stk :: StackVars stk
stk = case RefId -> StackVars stk -> VarDepth
forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars s -> VarDepth
varDepth @a RefId
ref StackVars stk
stk of
  VarDepth n :: Sing idx
n -> Sing idx -> RefId -> StackVars stk -> stk :-> (a & stk)
forall (inp :: [*]) a (m :: Peano) (s :: [*]) (tail :: [*]).
(HasCallStack, KnownValue a, KnownPeano m, SingI m,
 s ~ (Take m inp ++ (a : a : Drop ('S m) inp)),
 tail ~ Drop ('S m) inp) =>
Sing m -> RefId -> StackVars inp -> inp :-> (a : inp)
duupXVar Sing idx
n RefId
ref StackVars stk
stk

-- | Sets the value for the given 'Var' to the topmost value on the stack
varActionSet :: forall a stk . KnownValue a => RefId -> StackVars stk -> a & stk :-> stk
varActionSet :: RefId -> StackVars stk -> (a & stk) :-> stk
varActionSet ref :: RefId
ref stk :: StackVars stk
stk = case RefId -> StackVars stk -> VarDepth
forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars s -> VarDepth
varDepth @a RefId
ref StackVars stk
stk of
  VarDepth n :: Sing idx
n -> Sing ('S idx) -> RefId -> StackVars (a & stk) -> (a & stk) :-> stk
forall (s :: [*]) a (n :: Peano) (mid :: [*]) (tail :: [*]).
(HasCallStack, KnownValue a, mid ~ (Take n (a : s) ++ Drop n s),
 tail ~ Drop n s) =>
Sing n -> RefId -> StackVars (a : s) -> (a : s) :-> s
replaceNVar (SingNat idx -> SingNat ('S idx)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat idx
Sing idx
n) RefId
ref (StkEl a
forall a. KnownValue a => StkEl a
NoRef StkEl a -> StackVars stk -> StackVars (a & stk)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars stk
stk)

-- | Updates the value for the given 'Var' with the topmost value on the stack
-- using the given binary instruction.
varActionUpdate
  :: forall a b stk . (KnownValue a, KnownValue b)
  => RefId
  -> StackVars stk
  -> '[b, a] :-> '[a]
  -> (b ': stk) :-> stk
varActionUpdate :: RefId -> StackVars stk -> ('[b, a] :-> '[a]) -> (b : stk) :-> stk
varActionUpdate v :: RefId
v stk :: StackVars stk
stk instr :: '[b, a] :-> '[a]
instr = case RefId -> StackVars stk -> VarDepth
forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars s -> VarDepth
varDepth @a RefId
v StackVars stk
stk of
  VarDepth n :: Sing idx
n -> Sing ('S idx)
-> RefId
-> StackVars (b : stk)
-> ('[b, a] :-> '[a])
-> (b : stk) :-> stk
forall (s :: [*]) a b (mid :: [*]) (tail :: [*]) (n :: Peano).
(HasCallStack, KnownValue b, tail ~ Drop n s,
 mid ~ (Drop ('S 'Z) (Take n (a : s)) ++ (a : Drop n (a : s)))) =>
Sing n
-> RefId
-> StackVars (a : s)
-> ('[a, b] :-> '[b])
-> (a : s) :-> s
updateNVar (SingNat idx -> SingNat ('S idx)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat idx
Sing idx
n) RefId
v (StkEl b
forall a. KnownValue a => StkEl a
NoRef StkEl b -> StackVars stk -> StackVars (b : stk)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars stk
stk) '[b, a] :-> '[a]
instr

-- | Given a stack with a list of 'Operation's on its bottom, updates it by
-- appending the 'Operation' on the top.
varActionOperation
  :: HasSideEffects
  => StackVars stk
  -> (Operation ': stk) :-> stk
varActionOperation :: StackVars stk -> (Operation : stk) :-> stk
varActionOperation s :: StackVars stk
s =
  case Var Ops
HasSideEffects => Var Ops
operationsVar of
    Cell refId :: RefId
refId -> RefId
-> StackVars stk
-> ('[Operation, Ops] :-> '[Ops])
-> (Operation : stk) :-> stk
forall a b (stk :: [*]).
(KnownValue a, KnownValue b) =>
RefId -> StackVars stk -> ('[b, a] :-> '[a]) -> (b : stk) :-> stk
varActionUpdate @Ops RefId
refId StackVars stk
s '[Operation, Ops] :-> '[Ops]
forall a (s :: [*]). (a & (List a & s)) :-> (List a & s)
L.cons

----------------------------------------------------------------------------
-- Variable-based Macros
----------------------------------------------------------------------------

-- | Like 'varActionGet', but requires the depth of the 'Var' in the input stack
duupXVar
  :: forall inp a (m :: Peano) s tail.
     ( HasCallStack
     , KnownValue a, KnownPeano m, SingI m
     , s ~ ((Take m inp) ++ (a ':  a ': Drop ('S m) inp))
     , tail ~ (Drop ('S m) inp)
     )
  => Sing m -> RefId -> StackVars inp -> inp :-> (a ': inp)
duupXVar :: Sing m -> RefId -> StackVars inp -> inp :-> (a : inp)
duupXVar m :: Sing m
m v :: RefId
v stk :: StackVars inp
stk =
  Maybe (Dict (DuupX ('S m) inp a s tail))
-> (DuupX ('S m) inp a s tail => inp :-> (a : inp))
-> inp :-> (a : inp)
forall (c :: Constraint) e r.
(HasDict c e, HasCallStack) =>
Maybe e -> (c => r) -> r
withVarMaybeDict (Sing ('S m)
-> StackVars inp
-> StkEl a
-> StackVars s
-> StackVars tail
-> Maybe (Dict (DuupX ('S m) inp a s tail))
forall (n :: Peano) (inp :: [*]) a (s :: [*]) (s' :: [*]).
Sing n
-> StackVars inp
-> StkEl a
-> StackVars s
-> StackVars s'
-> Maybe (Dict (DuupX n inp a s s'))
duupXClassConstraint SingNat ('S m)
Sing ('S m)
n StackVars inp
stk StkEl a
a StackVars s
Rec StkEl (Take m inp ++ (a : a : tail))
s StackVars tail
Rec StkEl (Drop ('S m) inp)
tail) ((DuupX ('S m) inp a s tail => inp :-> (a : inp))
 -> inp :-> (a : inp))
-> (DuupX ('S m) inp a s tail => inp :-> (a : inp))
-> inp :-> (a : inp)
forall a b. (a -> b) -> a -> b
$
    DuupX ('S m) inp a s tail => inp :-> (a : inp)
forall k k1 (n :: Peano) (s :: [*]) a (s1 :: k) (tail :: k1).
DuupX n s a s1 tail =>
s :-> (a : s)
L.duupXImpl @('S m) @inp @a @s @tail
  where
    a :: StkEl a
a = RefId -> StkEl a
forall a. KnownValue a => RefId -> StkEl a
Ref @a RefId
v
    n :: SingNat ('S m)
n = SingNat m -> SingNat ('S m)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat m
Sing m
m
    s :: Rec StkEl (Take m inp ++ (a : a : tail))
s = (Sing m -> StackVars inp -> Rec StkEl (Take m inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing m
m StackVars inp
stk) Rec StkEl (Take m inp)
-> Rec StkEl (a : a : tail)
-> Rec StkEl (Take m inp ++ (a : a : tail))
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> (StkEl a
a StkEl a -> Rec StkEl (a : tail) -> Rec StkEl (a : a : tail)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl a
a StkEl a -> StackVars tail -> Rec StkEl (a : tail)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing ('S m) -> StackVars inp -> Rec StkEl (Drop ('S m) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop SingNat ('S m)
Sing ('S m)
n StackVars inp
stk)
    tail :: Rec StkEl (Drop ('S m) inp)
tail = Sing ('S m) -> StackVars inp -> Rec StkEl (Drop ('S m) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop SingNat ('S m)
Sing ('S m)
n StackVars inp
stk

-- | Like 'varActionSet', but requires the depth of the 'Var' in the input stack
replaceNVar
  :: forall s a (n :: Peano) mid tail.
     ( HasCallStack
     , KnownValue a
     , mid ~ (Take n (a ': s) ++ Drop n s)
     , tail ~ Drop n s
     )
  => Sing n -> RefId -> StackVars (a ': s) -> (a ': s) :-> s
replaceNVar :: Sing n -> RefId -> StackVars (a : s) -> (a : s) :-> s
replaceNVar n :: Sing n
n v :: RefId
v stk :: StackVars (a : s)
stk@(_ :& s :: Rec StkEl rs
s) =
  Maybe (Dict (ReplaceN n rs a mid tail))
-> (ReplaceN n s a mid tail => (a : s) :-> s) -> (a : s) :-> s
forall (c :: Constraint) e r.
(HasDict c e, HasCallStack) =>
Maybe e -> (c => r) -> r
withVarMaybeDict (Sing n
-> Rec StkEl rs
-> StkEl a
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ReplaceN n rs a mid tail))
forall (n :: Peano) (s :: [*]) a (mid :: [*]) (tail :: [*]).
Sing n
-> StackVars s
-> StkEl a
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ReplaceN n s a mid tail))
replaceNClassConstraint Sing n
n Rec StkEl rs
s (RefId -> StkEl a
forall a. KnownValue a => RefId -> StkEl a
Ref @a RefId
v) StackVars mid
Rec StkEl (Take n (a : s) ++ tail)
mid StackVars tail
Rec StkEl (Drop n rs)
tail) ((ReplaceN n s a mid tail => (a : s) :-> s) -> (a : s) :-> s)
-> (ReplaceN n s a mid tail => (a : s) :-> s) -> (a : s) :-> s
forall a b. (a -> b) -> a -> b
$
    ReplaceN n s a mid tail => (a : s) :-> s
forall k k1 (n :: Peano) (s :: [*]) a (mid :: k) (tail :: k1).
ReplaceN n s a mid tail =>
(a : s) :-> s
L.replaceNImpl @n @s @a @mid @tail
  where
    mid :: Rec StkEl (Take n (a : s) ++ tail)
mid = Sing n -> StackVars (a : s) -> Rec StkEl (Take n (a : s))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n StackVars (a : s)
stk Rec StkEl (Take n (a : s))
-> StackVars tail -> Rec StkEl (Take n (a : s) ++ tail)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Sing n -> Rec StkEl rs -> Rec StkEl (Drop n rs)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n Rec StkEl rs
s
    tail :: Rec StkEl (Drop n rs)
tail = Sing n -> Rec StkEl rs -> Rec StkEl (Drop n rs)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n Rec StkEl rs
s

-- | Like 'varActionUpdate', but requires the depth of the 'Var' in the input stack
updateNVar
  :: forall s a b mid tail (n :: Peano).
     ( HasCallStack
     , KnownValue b
     , tail ~ Drop n s
     , mid ~ ((Drop ('S 'Z) (Take n (a ': s))) ++ (a ': Drop n (a ': s)))
     )
  => Sing n -> RefId -> StackVars (a ': s)
  -> '[a, b] :-> '[b]
  -> (a ': s) :-> s
updateNVar :: Sing n
-> RefId
-> StackVars (a : s)
-> ('[a, b] :-> '[b])
-> (a : s) :-> s
updateNVar n :: Sing n
n v :: RefId
v stk :: StackVars (a : s)
stk@(a :: StkEl r
a :& s :: Rec StkEl rs
s) instr :: '[a, b] :-> '[b]
instr =
  Maybe (Dict (UpdateN n rs r b mid tail))
-> (UpdateN n s a b mid tail => (a : s) :-> s) -> (a : s) :-> s
forall (c :: Constraint) e r.
(HasDict c e, HasCallStack) =>
Maybe e -> (c => r) -> r
withVarMaybeDict (Sing n
-> Rec StkEl rs
-> StkEl r
-> StkEl b
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (UpdateN n rs r b mid tail))
forall (n :: Peano) (s :: [*]) a b (mid :: [*]) (tail :: [*]).
Sing n
-> StackVars s
-> StkEl a
-> StkEl b
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (UpdateN n s a b mid tail))
updateNClassConstraint Sing n
n Rec StkEl rs
s StkEl r
a (RefId -> StkEl b
forall a. KnownValue a => RefId -> StkEl a
Ref @b RefId
v) StackVars mid
Rec StkEl (Drop ('S 'Z) (Take n (a : s)) ++ (r : Drop n (a : s)))
mid StackVars tail
Rec StkEl (Drop n rs)
tail) ((UpdateN n s a b mid tail => (a : s) :-> s) -> (a : s) :-> s)
-> (UpdateN n s a b mid tail => (a : s) :-> s) -> (a : s) :-> s
forall a b. (a -> b) -> a -> b
$
    ('[a, b] :-> '[b]) -> (a : s) :-> s
forall k k1 (n :: Peano) (s :: [*]) a b (mid :: k) (tail :: k1).
UpdateN n s a b mid tail =>
('[a, b] :-> '[b]) -> (a : s) :-> s
L.updateNImpl @n @s @a @b @mid @tail '[a, b] :-> '[b]
instr
  where
    mid :: Rec StkEl (Drop ('S 'Z) (Take n (a : s)) ++ (r : Drop n (a : s)))
mid = Sing ('S 'Z)
-> Rec StkEl (Take n (a : s))
-> Rec StkEl (Drop ('S 'Z) (Take n (a : s)))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat 'Z -> SingNat ('S 'Z)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat 'Z
SZ) (Sing n -> StackVars (a : s) -> Rec StkEl (Take n (a : s))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n StackVars (a : s)
stk) Rec StkEl (Drop ('S 'Z) (Take n (a : s)))
-> Rec StkEl (r : Drop n (a : s))
-> Rec
     StkEl (Drop ('S 'Z) (Take n (a : s)) ++ (r : Drop n (a : s)))
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> StkEl r
a StkEl r
-> Rec StkEl (Drop n (a : s)) -> Rec StkEl (r : Drop n (a : s))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n -> StackVars (a : s) -> Rec StkEl (Drop n (a : s))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n StackVars (a : s)
stk
    tail :: Rec StkEl (Drop n rs)
tail = Sing n -> Rec StkEl rs -> Rec StkEl (Drop n rs)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n Rec StkEl rs
s

withVarMaybeDict :: (HasDict c e, HasCallStack) => Maybe e -> (c => r) -> r
withVarMaybeDict :: Maybe e -> (c => r) -> r
withVarMaybeDict mDict :: Maybe e
mDict = e -> (c => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (e -> Maybe e -> e
forall a. a -> Maybe a -> a
fromMaybe (Text -> e
forall a. HasCallStack => Text -> a
error Text
constraintFailure) Maybe e
mDict)
  where
    -- NOTE: provided that the 'VarDepth' is correctly calculated every place
    -- where this is used should never result in a 'Nothing', as this is only
    -- necessary to prove to GHC properties that always hold.
    -- For this reason a failure here is always unexpected
    constraintFailure :: Text
constraintFailure = "Unexpected failure in Var's constraint checking"

----------------------------------------------------------------------------
-- Variable's Depth
----------------------------------------------------------------------------

-- | Keeps the 0-indexed depth of a variable as a 'Peano' 'Sing'leton
data VarDepth where
  VarDepth
    :: forall idx . (KnownPeano idx, SingI idx)
    => Sing (idx :: Peano) -> VarDepth

-- | Calculates the 'VarDepth' of the given 'Var' in the stack
varDepth
  :: forall a s. KnownValue a
  => RefId
  -> StackVars s
  -> VarDepth
varDepth :: RefId -> StackVars s -> VarDepth
varDepth refId :: RefId
refId = \case
  RNil -> Text -> VarDepth
forall a. HasCallStack => Text -> a
error (Text -> VarDepth) -> Text -> VarDepth
forall a b. (a -> b) -> a -> b
$ "Manually created or leaked variable. Ref #" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RefId -> Text
forall b a. (Show a, IsString b) => a -> b
show RefId
refId
  stk :: StackVars s
stk@(_ :& _) -> RefId -> StackVars s -> VarDepth
forall a (s :: [*]) x (xs :: [*]).
(KnownValue a, s ~ (x & xs)) =>
RefId -> StackVars s -> VarDepth
varDepthNonEmpty @a RefId
refId StackVars s
stk

varDepthNonEmpty
  :: forall a s x xs. (KnownValue a, s ~ (x & xs))
  => RefId -> StackVars s -> VarDepth
varDepthNonEmpty :: RefId -> StackVars s -> VarDepth
varDepthNonEmpty ref :: RefId
ref (x :: StkEl r
x :& xs :: Rec StkEl rs
xs) = case StkEl r
x of
  Ref topRef :: RefId
topRef | RefId
ref RefId -> RefId -> Bool
forall a. Eq a => a -> a -> Bool
== RefId
topRef -> case (Typeable a, Typeable x) => Maybe (a :~: x)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @x of
    Just Refl -> Sing 'Z -> VarDepth
forall (idx :: Peano).
(KnownPeano idx, SingI idx) =>
Sing idx -> VarDepth
VarDepth SingNat 'Z
Sing 'Z
SZ
    Nothing   -> Text -> VarDepth
forall a. HasCallStack => Text -> a
error (Text -> VarDepth) -> Text -> VarDepth
forall a b. (a -> b) -> a -> b
$ "Invalid variable type. Ref #" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RefId -> Text
forall b a. (Show a, IsString b) => a -> b
show RefId
ref
  _ -> case RefId -> Rec StkEl rs -> VarDepth
forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars s -> VarDepth
varDepth @a RefId
ref Rec StkEl rs
xs of
    VarDepth idx :: Sing idx
idx -> Sing ('S idx) -> VarDepth
forall (idx :: Peano).
(KnownPeano idx, SingI idx) =>
Sing idx -> VarDepth
VarDepth (SingNat idx -> SingNat ('S idx)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat idx
Sing idx
idx)

----------------------------------------------------------------------------
-- Macro class constraints
----------------------------------------------------------------------------

duupXClassConstraint
  :: Sing n -> StackVars inp -> StkEl a -> StackVars s -> StackVars s'
  -> Maybe (Dict (L.DuupX n inp a s s'))
duupXClassConstraint :: Sing n
-> StackVars inp
-> StkEl a
-> StackVars s
-> StackVars s'
-> Maybe (Dict (DuupX n inp a s s'))
duupXClassConstraint n :: Sing n
n inp :: StackVars inp
inp a :: StkEl a
a s :: StackVars s
s s' :: StackVars s'
s' = case Sing n
n of
  SZ -> Maybe (Dict (DuupX n inp a s s'))
forall a. Maybe a
Nothing
  SS SZ -> case StackVars inp
inp of
    (x :: StkEl r
x :& _xs :: Rec StkEl rs
_xs) -> do
      r :~: a
Refl <- StkEl r -> StkEl a -> Maybe (r :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StkEl r
x StkEl a
a
      Dict (DuupX n inp a s s') -> Maybe (Dict (DuupX n inp a s s'))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (DuupX n inp a s s')
forall (a :: Constraint). a => Dict a
Dict
    _ -> Maybe (Dict (DuupX n inp a s s'))
forall a. Maybe a
Nothing
  SS (SS SZ) -> case StackVars inp
inp of
    (_ :& x :: StkEl r
x :& _xs :: Rec StkEl rs
_xs) -> do
      r :~: a
Refl <- StkEl r -> StkEl a -> Maybe (r :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StkEl r
x StkEl a
a
      Dict (DuupX n inp a s s') -> Maybe (Dict (DuupX n inp a s s'))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (DuupX n inp a s s')
forall (a :: Constraint). a => Dict a
Dict
    _ -> Maybe (Dict (DuupX n inp a s s'))
forall a. Maybe a
Nothing
  SS (SS (SS m)) -> do
    Dict
  ((ToTs s' ~ Drop ('S ('S ('S n1))) (ToTs inp),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerOrSameLength (ToTs inp) ('S ('S n1)),
     (Take ('S ('S n1)) (ToTs inp) ++ (ToT a : ToTs s')) ~ ToTs inp,
     (Take ('S ('S n1)) (ToTs inp) ++ (ToT a : ToT a : ToTs s'))
     ~ ToTs s),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerThan (ToTs s) ('S ('S n1)),
     ToTs s
     ~ (Take ('S ('S n1)) (ToTs s)
        ++ (ToT a : Drop ('S ('S ('S n1))) (ToTs s))),
     (ToT a : ToTs inp)
     ~ (ToT a
          : (Take ('S ('S n1)) (ToTs s)
             ++ Drop ('S ('S ('S n1))) (ToTs s))))),
   (s' ~ Drop ('S ('S ('S n1))) inp,
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerOrSameLength inp ('S ('S n1)),
     (Take ('S ('S n1)) inp ++ (a : s')) ~ inp,
     (Take ('S ('S n1)) inp ++ (a : a : s')) ~ s),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerThan s ('S ('S n1)),
     s ~ (Take ('S ('S n1)) s ++ (a : Drop ('S ('S ('S n1))) s)),
     (a : inp)
     ~ (a : (Take ('S ('S n1)) s ++ Drop ('S ('S ('S n1))) s)))))
Dict <- Sing ('S ('S n1))
-> StackVars inp
-> StkEl a
-> StackVars s
-> StackVars s'
-> Maybe
     (Dict
        ((ToTs s' ~ Drop ('S ('S ('S n1))) (ToTs inp),
          (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
           RequireLongerOrSameLength (ToTs inp) ('S ('S n1)),
           (Take ('S ('S n1)) (ToTs inp) ++ (ToT a : ToTs s')) ~ ToTs inp,
           (Take ('S ('S n1)) (ToTs inp) ++ (ToT a : ToT a : ToTs s'))
           ~ ToTs s),
          (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
           RequireLongerThan (ToTs s) ('S ('S n1)),
           ToTs s
           ~ (Take ('S ('S n1)) (ToTs s)
              ++ (ToT a : Drop ('S ('S ('S n1))) (ToTs s))),
           (ToT a : ToTs inp)
           ~ (ToT a
                : (Take ('S ('S n1)) (ToTs s)
                   ++ Drop ('S ('S ('S n1))) (ToTs s))))),
         (s' ~ Drop ('S ('S ('S n1))) inp,
          (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
           RequireLongerOrSameLength inp ('S ('S n1)),
           (Take ('S ('S n1)) inp ++ (a : s')) ~ inp,
           (Take ('S ('S n1)) inp ++ (a : a : s')) ~ s),
          (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
           RequireLongerThan s ('S ('S n1)),
           s ~ (Take ('S ('S n1)) s ++ (a : Drop ('S ('S ('S n1))) s)),
           (a : inp)
           ~ (a : (Take ('S ('S n1)) s ++ Drop ('S ('S ('S n1))) s))))))
forall (n :: Peano) (inp :: [*]) a (s :: [*]) (s' :: [*]).
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StkEl a
-> StackVars s
-> StackVars s'
-> Maybe (Dict (ConstraintDuupXLorentz n inp a s s'))
duupXLorentzConstraint (SingNat ('S n1) -> SingNat ('S ('S n1))
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS (SingNat n1 -> SingNat ('S n1)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n1
m)) StackVars inp
inp StkEl a
a StackVars s
s StackVars s'
s'
    Dict (DuupX n inp a s s') -> Maybe (Dict (DuupX n inp a s s'))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (DuupX n inp a s s')
forall (a :: Constraint). a => Dict a
Dict

replaceNClassConstraint
  :: Sing n -> StackVars s -> StkEl a -> StackVars mid -> StackVars tail
  -> Maybe (Dict (L.ReplaceN n s a mid tail))
replaceNClassConstraint :: Sing n
-> StackVars s
-> StkEl a
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ReplaceN n s a mid tail))
replaceNClassConstraint n :: Sing n
n s :: StackVars s
s a :: StkEl a
a mid :: StackVars mid
mid tail :: StackVars tail
tail = case Sing n
n of
  SZ -> Maybe (Dict (ReplaceN n s a mid tail))
forall a. Maybe a
Nothing
  SS SZ -> case StackVars s
s of
    (x :: StkEl r
x :& _xs :: Rec StkEl rs
_xs) -> do
      r :~: a
Refl <- StkEl r -> StkEl a -> Maybe (r :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StkEl r
x StkEl a
a
      Dict (ReplaceN n s a mid tail)
-> Maybe (Dict (ReplaceN n s a mid tail))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (ReplaceN n s a mid tail)
forall (a :: Constraint). a => Dict a
Dict
    _ -> Maybe (Dict (ReplaceN n s a mid tail))
forall a. Maybe a
Nothing
  SS (SS m) -> do
    Dict
  ((ToTs tail ~ Drop ('S ('S n1)) (ToTs s),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerOrSameLength (ToT a : ToTs s) ('S ('S n1)),
     (ToT a : (Take ('S n1) (ToTs s) ++ (ToT a : ToTs tail)))
     ~ (ToT a : ToTs s),
     (ToT a : (Take ('S n1) (ToTs s) ++ ToTs tail)) ~ ToTs mid),
    (SingI ('S n1), KnownPeano ('S n1),
     RequireLongerThan (ToTs s) ('S n1),
     ToTs mid ~ (ToT a : Drop ('S 'Z) (ToTs mid)),
     ToTs s
     ~ (Take ('S n1) (Drop ('S 'Z) (ToTs mid))
        ++ (ToT a : Drop ('S ('S n1)) (ToTs mid))))),
   (tail ~ Drop ('S ('S n1)) s,
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerOrSameLength (a : s) ('S ('S n1)),
     (a : (Take ('S n1) s ++ (a : tail))) ~ (a : s),
     (a : (Take ('S n1) s ++ tail)) ~ mid),
    (SingI ('S n1), KnownPeano ('S n1), RequireLongerThan s ('S n1),
     mid ~ (a : Drop ('S 'Z) mid),
     s
     ~ (Take ('S n1) (Drop ('S 'Z) mid)
        ++ (a : Drop ('S ('S n1)) mid)))))
Dict <- Sing ('S n1)
-> StackVars s
-> StkEl a
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ConstraintReplaceNLorentz ('S n1) s a mid tail))
forall (n :: Peano) (s :: [*]) a (mid :: [*]) (tail :: [*]).
(KnownPeano n, SingI n) =>
Sing n
-> StackVars s
-> StkEl a
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ConstraintReplaceNLorentz n s a mid tail))
replaceNLorentzConstraint (SingNat n1 -> SingNat ('S n1)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n1
m) StackVars s
s StkEl a
a StackVars mid
mid StackVars tail
tail
    Dict (ReplaceN n s a mid tail)
-> Maybe (Dict (ReplaceN n s a mid tail))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (ReplaceN n s a mid tail)
forall (a :: Constraint). a => Dict a
Dict

updateNClassConstraint
  :: Sing n -> StackVars s -> StkEl a -> StkEl b -> StackVars mid -> StackVars tail
  -> Maybe (Dict (L.UpdateN n s a b mid tail))
updateNClassConstraint :: Sing n
-> StackVars s
-> StkEl a
-> StkEl b
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (UpdateN n s a b mid tail))
updateNClassConstraint n :: Sing n
n s :: StackVars s
s a :: StkEl a
a b :: StkEl b
b mid :: StackVars mid
mid tail :: StackVars tail
tail = case Sing n
n of
  SZ -> Maybe (Dict (UpdateN n s a b mid tail))
forall a. Maybe a
Nothing
  SS SZ -> case StackVars s
s of
    (x :: StkEl r
x :& xs :: Rec StkEl rs
xs) -> do
      r :~: b
Refl <- StkEl r -> StkEl b -> Maybe (r :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StkEl r
x StkEl b
b
      rs :~: tail
Refl <- Rec StkEl rs -> StackVars tail -> Maybe (rs :~: tail)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Rec StkEl rs
xs StackVars tail
tail
      Dict (UpdateN n s a b mid tail)
-> Maybe (Dict (UpdateN n s a b mid tail))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (UpdateN n s a b mid tail)
forall (a :: Constraint). a => Dict a
Dict
    _ -> Maybe (Dict (UpdateN n s a b mid tail))
forall a. Maybe a
Nothing
  SS (SS SZ) -> case StackVars s
s of
    (_x :: StkEl r
_x :& y :: StkEl r
y :& xs :: Rec StkEl rs
xs) -> do
      r :~: b
Refl <- StkEl r -> StkEl b -> Maybe (r :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StkEl r
y StkEl b
b
      rs :~: tail
Refl <- Rec StkEl rs -> StackVars tail -> Maybe (rs :~: tail)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Rec StkEl rs
xs StackVars tail
tail
      Dict (UpdateN n s a b mid tail)
-> Maybe (Dict (UpdateN n s a b mid tail))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (UpdateN n s a b mid tail)
forall (a :: Constraint). a => Dict a
Dict
    _ -> Maybe (Dict (UpdateN n s a b mid tail))
forall a. Maybe a
Nothing
  SS (SS (SS m)) -> do
    Dict
  ((ToTs tail ~ Drop ('S ('S ('S n1))) (ToTs s),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerThan (ToTs mid) ('S ('S n1)),
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     ToTs mid
     ~ (Take ('S ('S n1)) (ToTs s)
        ++ (ToT a : Drop ('S ('S n1)) (ToTs s)))),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerOrSameLength (ToTs mid) ('S ('S n1)),
     (Take ('S ('S n1)) (ToTs mid) ++ (ToT a : ToT b : ToTs tail))
     ~ ToTs mid,
     (Take ('S ('S n1)) (ToTs mid) ++ (ToT b : ToTs tail)) ~ ToTs s)),
   (tail ~ Drop ('S ('S ('S n1))) s,
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerThan mid ('S ('S n1)), (a : s) ~ (a : s),
     mid ~ (Take ('S ('S n1)) s ++ (a : Drop ('S ('S n1)) s))),
    (SingI ('S ('S n1)), KnownPeano ('S ('S n1)),
     RequireLongerOrSameLength mid ('S ('S n1)),
     (Take ('S ('S n1)) mid ++ (a : b : tail)) ~ mid,
     (Take ('S ('S n1)) mid ++ (b : tail)) ~ s)))
Dict <- Sing ('S ('S n1))
-> StackVars s
-> StkEl a
-> StkEl b
-> StackVars mid
-> StackVars tail
-> Maybe
     (Dict (ConstraintUpdateNLorentz ('S ('S n1)) s a b mid tail))
forall (n :: Peano) (s :: [*]) a b (mid :: [*]) (tail :: [*]).
(KnownPeano n, SingI n) =>
Sing n
-> StackVars s
-> StkEl a
-> StkEl b
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ConstraintUpdateNLorentz n s a b mid tail))
updateNLorentzConstraint (SingNat ('S n1) -> SingNat ('S ('S n1))
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS (SingNat n1 -> SingNat ('S n1)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n1
m)) StackVars s
s StkEl a
a StkEl b
b StackVars mid
mid StackVars tail
tail
    Dict (UpdateN n s a b mid tail)
-> Maybe (Dict (UpdateN n s a b mid tail))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (UpdateN n s a b mid tail)
forall (a :: Constraint). a => Dict a
Dict

----------------------------------------------------------------------------
-- Lorentz constraints
----------------------------------------------------------------------------

duupXLorentzConstraint
  :: (KnownPeano n, SingI n)
  => Sing n -> StackVars inp -> StkEl a -> StackVars s -> StackVars s'
  -> Maybe (Dict (L.ConstraintDuupXLorentz n inp a s s'))
duupXLorentzConstraint :: Sing n
-> StackVars inp
-> StkEl a
-> StackVars s
-> StackVars s'
-> Maybe (Dict (ConstraintDuupXLorentz n inp a s s'))
duupXLorentzConstraint n :: Sing n
n s :: StackVars inp
s a :: StkEl a
a s1 :: StackVars s
s1 tail :: StackVars s'
tail = do
  s' :~: Drop ('S n) inp
Refl <- StackVars s'
-> Rec StkEl (Drop ('S n) inp) -> Maybe (s' :~: Drop ('S n) inp)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StackVars s'
tail (Sing ('S n) -> StackVars inp -> Rec StkEl (Drop ('S n) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) StackVars inp
s)
  ToTs s' :~: Drop ('S n) (ToTs inp)
Refl <- Rec TVal (ToTs s')
-> Rec TVal (Drop ('S n) (ToTs inp))
-> Maybe (ToTs s' :~: Drop ('S n) (ToTs inp))
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (StackVars s' -> Rec TVal (ToTs s')
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars s'
tail) (Sing ('S n)
-> Rec TVal (ToTs inp) -> Rec TVal (Drop ('S n) (ToTs inp))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) (StackVars inp -> Rec TVal (ToTs inp)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars inp
s))
  Dict
  ((SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
    (Take n (ToTs inp) ++ (ToT a : ToTs s')) ~ ToTs inp,
    (Take n (ToTs inp) ++ (ToT a : ToT a : ToTs s')) ~ ToTs s),
   (SingI n, KnownPeano n, RequireLongerOrSameLength inp n,
    (Take n inp ++ (a : s')) ~ inp, (Take n inp ++ (a : a : s')) ~ s))
Dict <- Sing n
-> StackVars inp
-> StackVars s
-> StackVars (a : s')
-> StackVars (a : a : s')
-> Maybe
     (Dict (ConstraintDIPNLorentz n inp s (a : s') (a : a : s')))
forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StackVars out
-> StackVars s
-> StackVars s'
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint Sing n
n StackVars inp
s StackVars s
s1 (StkEl a
a StkEl a -> StackVars s' -> StackVars (a : s')
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars s'
tail) (StkEl a
a StkEl a -> StackVars (a : s') -> StackVars (a : a : s')
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl a
a StkEl a -> StackVars s' -> StackVars (a : s')
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars s'
tail)
  Dict
  ((SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
    ToTs s ~ (Take n (ToTs s) ++ (ToT a : Drop ('S n) (ToTs s))),
    (ToT a : ToTs inp)
    ~ (ToT a : (Take n (ToTs s) ++ Drop ('S n) (ToTs s)))),
   (SingI n, KnownPeano n, RequireLongerThan s n,
    s ~ (Take n s ++ (a : Drop ('S n) s)),
    (a : inp) ~ (a : (Take n s ++ Drop ('S n) s))))
Dict <- Sing n
-> StackVars s
-> StackVars (a : inp)
-> StkEl a
-> Maybe (Dict (ConstraintDIGLorentz n s (a : inp) a))
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe (Dict (ConstraintDIGLorentz n inp out a))
digLorentzConstraint Sing n
n StackVars s
s1 (StkEl a
a StkEl a -> StackVars inp -> StackVars (a : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars inp
s) StkEl a
a
  Dict
  ((ToTs s' ~ ToTs s',
    (SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
     ToTs inp ~ ToTs inp, ToTs s ~ ToTs s),
    (SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
     ToTs s ~ ToTs s, (ToT a : ToTs inp) ~ (ToT a : ToTs inp))),
   (s' ~ s',
    (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
     s ~ s),
    (SingI n, KnownPeano n, RequireLongerThan s n, s ~ s,
     (a : inp) ~ (a : inp))))
-> Maybe
     (Dict
        ((ToTs s' ~ ToTs s',
          (SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
           ToTs inp ~ ToTs inp, ToTs s ~ ToTs s),
          (SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
           ToTs s ~ ToTs s, (ToT a : ToTs inp) ~ (ToT a : ToTs inp))),
         (s' ~ s',
          (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
           s ~ s),
          (SingI n, KnownPeano n, RequireLongerThan s n, s ~ s,
           (a : inp) ~ (a : inp)))))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((ToTs s' ~ ToTs s',
    (SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
     ToTs inp ~ ToTs inp, ToTs s ~ ToTs s),
    (SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
     ToTs s ~ ToTs s, (ToT a : ToTs inp) ~ (ToT a : ToTs inp))),
   (s' ~ s',
    (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
     s ~ s),
    (SingI n, KnownPeano n, RequireLongerThan s n, s ~ s,
     (a : inp) ~ (a : inp))))
forall (a :: Constraint). a => Dict a
Dict

updateNLorentzConstraint
  :: (KnownPeano n, SingI n)
  => Sing n -> StackVars s -> StkEl a -> StkEl b -> StackVars mid -> StackVars tail
  -> Maybe (Dict (L.ConstraintUpdateNLorentz n s a b mid tail))
updateNLorentzConstraint :: Sing n
-> StackVars s
-> StkEl a
-> StkEl b
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ConstraintUpdateNLorentz n s a b mid tail))
updateNLorentzConstraint n :: Sing n
n s :: StackVars s
s a :: StkEl a
a b :: StkEl b
b mid :: StackVars mid
mid tail :: StackVars tail
tail = do
  tail :~: Drop ('S n) s
Refl <- StackVars tail
-> Rec StkEl (Drop ('S n) s) -> Maybe (tail :~: Drop ('S n) s)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StackVars tail
tail (Sing ('S n) -> StackVars s -> Rec StkEl (Drop ('S n) s)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) StackVars s
s)
  ToTs tail :~: Drop ('S n) (ToTs s)
Refl <- Rec TVal (ToTs tail)
-> Rec TVal (Drop ('S n) (ToTs s))
-> Maybe (ToTs tail :~: Drop ('S n) (ToTs s))
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (StackVars tail -> Rec TVal (ToTs tail)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars tail
tail) (Sing ('S n) -> Rec TVal (ToTs s) -> Rec TVal (Drop ('S n) (ToTs s))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) (StackVars s -> Rec TVal (ToTs s)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars s
s))
  Dict
  ((SingI n, KnownPeano n, RequireLongerThan (ToTs mid) n,
    (ToT a : ToTs s) ~ (ToT a : ToTs s),
    ToTs mid ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
   (SingI n, KnownPeano n, RequireLongerThan mid n, (a : s) ~ (a : s),
    mid ~ (Take n s ++ (a : Drop n s))))
Dict <- Sing n
-> StackVars (a : s)
-> StackVars mid
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n (a : s) mid a))
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n inp out a))
dugLorentzConstraint Sing n
n (StkEl a
a StkEl a -> StackVars s -> StackVars (a : s)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars s
s) StackVars mid
mid StkEl a
a
  Dict
  ((SingI n, KnownPeano n,
    RequireLongerOrSameLength
      (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
    (Take n (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ++ (ToT a : ToT b : ToTs tail))
    ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
    (Take n (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ++ (ToT b : ToTs tail))
    ~ ToTs s),
   (SingI n, KnownPeano n, RequireLongerOrSameLength mid n,
    (Take n mid ++ (a : b : tail)) ~ mid,
    (Take n mid ++ (b : tail)) ~ s))
Dict <- Sing n
-> StackVars mid
-> StackVars s
-> StackVars (a : b : tail)
-> StackVars (b : tail)
-> Maybe
     (Dict (ConstraintDIPNLorentz n mid s (a : b : tail) (b : tail)))
forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StackVars out
-> StackVars s
-> StackVars s'
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint Sing n
n StackVars mid
mid StackVars s
s (StkEl a
a StkEl a -> StackVars (b : tail) -> StackVars (a : b : tail)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl b
b StkEl b -> StackVars tail -> StackVars (b : tail)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars tail
tail) (StkEl b
b StkEl b -> StackVars tail -> StackVars (b : tail)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars tail
tail)
  Dict
  ((ToTs tail ~ ToTs tail,
    (SingI n, KnownPeano n,
     RequireLongerThan (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
    (SingI n, KnownPeano n,
     RequireLongerOrSameLength
       (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
     ToTs s ~ ToTs s)),
   (tail ~ tail,
    (SingI n, KnownPeano n, RequireLongerThan mid n, (a : s) ~ (a : s),
     mid ~ mid),
    (SingI n, KnownPeano n, RequireLongerOrSameLength mid n, mid ~ mid,
     s ~ s)))
-> Maybe
     (Dict
        ((ToTs tail ~ ToTs tail,
          (SingI n, KnownPeano n,
           RequireLongerThan (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
           (ToT a : ToTs s) ~ (ToT a : ToTs s),
           (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
           ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
          (SingI n, KnownPeano n,
           RequireLongerOrSameLength
             (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
           (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
           ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
           ToTs s ~ ToTs s)),
         (tail ~ tail,
          (SingI n, KnownPeano n, RequireLongerThan mid n, (a : s) ~ (a : s),
           mid ~ mid),
          (SingI n, KnownPeano n, RequireLongerOrSameLength mid n, mid ~ mid,
           s ~ s))))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((ToTs tail ~ ToTs tail,
    (SingI n, KnownPeano n,
     RequireLongerThan (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
    (SingI n, KnownPeano n,
     RequireLongerOrSameLength
       (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (Take n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
     ToTs s ~ ToTs s)),
   (tail ~ tail,
    (SingI n, KnownPeano n, RequireLongerThan mid n, (a : s) ~ (a : s),
     mid ~ mid),
    (SingI n, KnownPeano n, RequireLongerOrSameLength mid n, mid ~ mid,
     s ~ s)))
forall (a :: Constraint). a => Dict a
Dict

replaceNLorentzConstraint
  :: (KnownPeano n, SingI n)
  => Sing n -> StackVars s -> StkEl a -> StackVars mid -> StackVars tail
  -> Maybe (Dict (L.ConstraintReplaceNLorentz n s a mid tail))
replaceNLorentzConstraint :: Sing n
-> StackVars s
-> StkEl a
-> StackVars mid
-> StackVars tail
-> Maybe (Dict (ConstraintReplaceNLorentz n s a mid tail))
replaceNLorentzConstraint n :: Sing n
n s :: StackVars s
s a :: StkEl a
a mid :: StackVars mid
mid tail :: StackVars tail
tail = do
  tail :~: Drop ('S n) s
Refl <- StackVars tail
-> Rec StkEl (Drop ('S n) s) -> Maybe (tail :~: Drop ('S n) s)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StackVars tail
tail (Sing ('S n) -> StackVars s -> Rec StkEl (Drop ('S n) s)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) StackVars s
s)
  ToTs tail :~: Drop ('S n) (ToTs s)
Refl <- Rec TVal (ToTs tail)
-> Rec TVal (Drop ('S n) (ToTs s))
-> Maybe (ToTs tail :~: Drop ('S n) (ToTs s))
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (StackVars tail -> Rec TVal (ToTs tail)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars tail
tail) (Sing ('S n) -> Rec TVal (ToTs s) -> Rec TVal (Drop ('S n) (ToTs s))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) (StackVars s -> Rec TVal (ToTs s)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars s
s))
  Dict
  ((SingI ('S n), KnownPeano ('S n),
    RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
    (ToT a : (Take n (ToTs s) ++ (ToT a : ToTs tail)))
    ~ (ToT a : ToTs s),
    (ToT a : (Take n (ToTs s) ++ ToTs tail)) ~ ToTs mid),
   (SingI ('S n), KnownPeano ('S n),
    RequireLongerOrSameLength (a : s) ('S n),
    (a : (Take n s ++ (a : tail))) ~ (a : s),
    (a : (Take n s ++ tail)) ~ mid))
Dict <- Sing ('S n)
-> StackVars (a : s)
-> StackVars mid
-> StackVars (a : tail)
-> StackVars tail
-> Maybe
     (Dict (ConstraintDIPNLorentz ('S n) (a : s) mid (a : tail) tail))
forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StackVars out
-> StackVars s
-> StackVars s'
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) (StkEl a
a StkEl a -> StackVars s -> StackVars (a : s)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars s
s) StackVars mid
mid (StkEl a
a StkEl a -> StackVars tail -> StackVars (a : tail)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars tail
tail) StackVars tail
tail
  Dict
  ((SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
    (ToT a : ToTs (Take n s ++ tail))
    ~ (ToT a : ToTs (Take n s ++ tail)),
    ToTs s
    ~ (Take n (ToTs (Take n s ++ tail))
       ++ (ToT a : Drop n (ToTs (Take n s ++ tail))))),
   (SingI n, KnownPeano n, RequireLongerThan s n,
    (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail)),
    s
    ~ (Take n (Take n s ++ tail) ++ (a : Drop n (Take n s ++ tail)))))
Dict <- Sing n
-> StackVars mid
-> StackVars s
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n mid s a))
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
(KnownPeano n, SingI n) =>
Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n inp out a))
dugLorentzConstraint Sing n
n StackVars mid
mid StackVars s
s StkEl a
a
  Dict
  ((ToTs tail ~ ToTs tail,
    (SingI ('S n), KnownPeano ('S n),
     RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (ToT a : ToTs (Take n s ++ tail))
     ~ (ToT a : ToTs (Take n s ++ tail))),
    (SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
     (ToT a : ToTs (Take n s ++ tail))
     ~ (ToT a : ToTs (Take n s ++ tail)),
     ToTs s ~ ToTs s)),
   (tail ~ tail,
    (SingI ('S n), KnownPeano ('S n),
     RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
     (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail))),
    (SingI n, KnownPeano n, RequireLongerThan s n,
     (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail)), s ~ s)))
-> Maybe
     (Dict
        ((ToTs tail ~ ToTs tail,
          (SingI ('S n), KnownPeano ('S n),
           RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
           (ToT a : ToTs s) ~ (ToT a : ToTs s),
           (ToT a : ToTs (Take n s ++ tail))
           ~ (ToT a : ToTs (Take n s ++ tail))),
          (SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
           (ToT a : ToTs (Take n s ++ tail))
           ~ (ToT a : ToTs (Take n s ++ tail)),
           ToTs s ~ ToTs s)),
         (tail ~ tail,
          (SingI ('S n), KnownPeano ('S n),
           RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
           (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail))),
          (SingI n, KnownPeano n, RequireLongerThan s n,
           (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail)), s ~ s))))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((ToTs tail ~ ToTs tail,
    (SingI ('S n), KnownPeano ('S n),
     RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (ToT a : ToTs (Take n s ++ tail))
     ~ (ToT a : ToTs (Take n s ++ tail))),
    (SingI n, KnownPeano n, RequireLongerThan (ToTs s) n,
     (ToT a : ToTs (Take n s ++ tail))
     ~ (ToT a : ToTs (Take n s ++ tail)),
     ToTs s ~ ToTs s)),
   (tail ~ tail,
    (SingI ('S n), KnownPeano ('S n),
     RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
     (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail))),
    (SingI n, KnownPeano n, RequireLongerThan s n,
     (a : (Take n s ++ tail)) ~ (a : (Take n s ++ tail)), s ~ s)))
forall (a :: Constraint). a => Dict a
Dict

dugLorentzConstraint
  :: (KnownPeano n, SingI n)
  => Sing n -> StackVars inp -> StackVars out -> StkEl a
  -> Maybe (Dict (L.ConstraintDUGLorentz n inp out a))
dugLorentzConstraint :: Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n inp out a))
dugLorentzConstraint n :: Sing n
n inp :: StackVars inp
inp out :: StackVars out
out a :: StkEl a
a = do
  Dict
  (SingI n, KnownPeano n, RequireLongerThan out n,
   inp ~ (a : Drop ('S 'Z) inp),
   out ~ (Take n (Drop ('S 'Z) inp) ++ (a : Drop ('S n) inp)))
Dict <- Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerThan out n,
         inp ~ (a : Drop ('S 'Z) inp),
         out ~ (Take n (Drop ('S 'Z) inp) ++ (a : Drop ('S n) inp))))
forall (n :: Peano) kind (any :: kind -> *) (inp :: [kind])
       (out :: [kind]) (a :: kind).
(KnownPeano n, SingI n, TestEquality any) =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUG' kind n inp out a))
dugConstraint Sing n
n StackVars inp
inp StackVars out
out StkEl a
a
  Dict
  (SingI n, KnownPeano n, RequireLongerThan (ToTs out) n,
   (ToT a : ToTs (Drop ('S 'Z) inp))
   ~ (ToT a : ToTs (Drop ('S 'Z) inp)),
   ToTs out
   ~ (Take n (ToTs (Drop ('S 'Z) inp))
      ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp)))))
Dict <- Sing n
-> Rec TVal (ToT a : ToTs (Drop ('S 'Z) inp))
-> Rec TVal (ToTs out)
-> TVal (ToT a)
-> Maybe
     (Dict
        (ConstraintDUG'
           T n (ToT a : ToTs (Drop ('S 'Z) inp)) (ToTs out) (ToT a)))
forall (n :: Peano) kind (any :: kind -> *) (inp :: [kind])
       (out :: [kind]) (a :: kind).
(KnownPeano n, SingI n, TestEquality any) =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUG' kind n inp out a))
dugConstraint Sing n
n (StackVars inp -> TValStack (ToTs inp)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars inp
inp) (StackVars out -> Rec TVal (ToTs out)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars out
out) (StkEl a -> TVal (ToT a)
forall a. StkEl a -> TVal (ToT a)
toTVal StkEl a
a)
  Dict
  ((SingI n, KnownPeano n,
    RequireLongerThan
      (Take n (ToTs (Drop ('S 'Z) inp))
       ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))
      n,
    (ToT a : ToTs (Drop ('S 'Z) inp))
    ~ (ToT a : ToTs (Drop ('S 'Z) inp)),
    (Take n (ToTs (Drop ('S 'Z) inp))
     ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))
    ~ (Take n (ToTs (Drop ('S 'Z) inp))
       ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))),
   (SingI n, KnownPeano n, RequireLongerThan out n,
    (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out))
-> Maybe
     (Dict
        ((SingI n, KnownPeano n,
          RequireLongerThan
            (Take n (ToTs (Drop ('S 'Z) inp))
             ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))
            n,
          (ToT a : ToTs (Drop ('S 'Z) inp))
          ~ (ToT a : ToTs (Drop ('S 'Z) inp)),
          (Take n (ToTs (Drop ('S 'Z) inp))
           ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))
          ~ (Take n (ToTs (Drop ('S 'Z) inp))
             ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))),
         (SingI n, KnownPeano n, RequireLongerThan out n,
          (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out)))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((SingI n, KnownPeano n,
    RequireLongerThan
      (Take n (ToTs (Drop ('S 'Z) inp))
       ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))
      n,
    (ToT a : ToTs (Drop ('S 'Z) inp))
    ~ (ToT a : ToTs (Drop ('S 'Z) inp)),
    (Take n (ToTs (Drop ('S 'Z) inp))
     ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))
    ~ (Take n (ToTs (Drop ('S 'Z) inp))
       ++ (ToT a : Drop n (ToTs (Drop ('S 'Z) inp))))),
   (SingI n, KnownPeano n, RequireLongerThan out n,
    (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out))
forall (a :: Constraint). a => Dict a
Dict

dipNLorentzConstraint
  :: (KnownPeano n, SingI n)
  => Sing n -> StackVars inp -> StackVars out -> StackVars s -> StackVars s'
  -> Maybe (Dict (L.ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint :: Sing n
-> StackVars inp
-> StackVars out
-> StackVars s
-> StackVars s'
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint n :: Sing n
n inp :: StackVars inp
inp out :: StackVars out
out s :: StackVars s
s s' :: StackVars s'
s' = do
  Dict
  (SingI n, KnownPeano n, RequireLongerOrSameLength inp n,
   (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ out)
Dict <- Sing n
-> StackVars inp
-> StackVars out
-> StackVars s
-> StackVars s'
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerOrSameLength inp n,
         (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ out))
forall (n :: Peano) kind (any :: kind -> *) (inp :: [kind])
       (out :: [kind]) (s :: [kind]) (s' :: [kind]).
(KnownPeano n, SingI n, TestEquality any) =>
Sing n
-> Rec any inp
-> Rec any out
-> Rec any s
-> Rec any s'
-> Maybe (Dict (ConstraintDIPN' kind n inp out s s'))
dipNConstraint Sing n
n StackVars inp
inp StackVars out
out StackVars s
s StackVars s'
s'
  Dict
  (SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
   (Take n (ToTs inp) ++ ToTs s) ~ ToTs inp,
   (Take n (ToTs inp) ++ ToTs s') ~ ToTs out)
Dict <- Sing n
-> Rec TVal (ToTs inp)
-> Rec TVal (ToTs out)
-> Rec TVal (ToTs s)
-> Rec TVal (ToTs s')
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
         (Take n (ToTs inp) ++ ToTs s) ~ ToTs inp,
         (Take n (ToTs inp) ++ ToTs s') ~ ToTs out))
forall (n :: Peano) kind (any :: kind -> *) (inp :: [kind])
       (out :: [kind]) (s :: [kind]) (s' :: [kind]).
(KnownPeano n, SingI n, TestEquality any) =>
Sing n
-> Rec any inp
-> Rec any out
-> Rec any s
-> Rec any s'
-> Maybe (Dict (ConstraintDIPN' kind n inp out s s'))
dipNConstraint Sing n
n (StackVars inp -> Rec TVal (ToTs inp)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars inp
inp) (StackVars out -> Rec TVal (ToTs out)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars out
out) (StackVars s -> Rec TVal (ToTs s)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars s
s) (StackVars s' -> Rec TVal (ToTs s')
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars s'
s')
  Dict
  ((SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
    ToTs inp ~ ToTs inp, ToTs out ~ ToTs out),
   (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
    out ~ out))
-> Maybe
     (Dict
        ((SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
          ToTs inp ~ ToTs inp, ToTs out ~ ToTs out),
         (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
          out ~ out)))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((SingI n, KnownPeano n, RequireLongerOrSameLength (ToTs inp) n,
    ToTs inp ~ ToTs inp, ToTs out ~ ToTs out),
   (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
    out ~ out))
forall (a :: Constraint). a => Dict a
Dict

digLorentzConstraint
  :: (KnownPeano n, SingI n)
  => Sing n -> StackVars inp -> StackVars out -> StkEl a
  -> Maybe (Dict (L.ConstraintDIGLorentz n inp out a))
digLorentzConstraint :: Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe (Dict (ConstraintDIGLorentz n inp out a))
digLorentzConstraint n :: Sing n
n inp :: StackVars inp
inp out :: StackVars out
out a :: StkEl a
a = do
  Dict
  (SingI n, KnownPeano n, RequireLongerThan inp n,
   inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
   out ~ (a : (Take n inp ++ Drop ('S n) inp)))
Dict <- Sing n
-> StackVars inp
-> StackVars out
-> StkEl a
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerThan inp n,
         inp ~ (Take n inp ++ (a : Drop ('S n) inp)),
         out ~ (a : (Take n inp ++ Drop ('S n) inp))))
forall (n :: Peano) kind (any :: kind -> *) (inp :: [kind])
       (out :: [kind]) (a :: kind).
(KnownPeano n, SingI n, TestEquality any) =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDIG' kind n inp out a))
digConstraint Sing n
n StackVars inp
inp StackVars out
out StkEl a
a
  Dict
  (SingI n, KnownPeano n, RequireLongerThan (ToTs inp) n,
   ToTs inp ~ (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))),
   (ToT a : ToTs (Take n inp ++ Drop ('S n) inp))
   ~ (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp))))
Dict <- Sing n
-> Rec TVal (ToTs inp)
-> Rec TVal (ToT a : ToTs (Take n inp ++ Drop ('S n) inp))
-> TVal (ToT a)
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerThan (ToTs inp) n,
         ToTs inp ~ (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))),
         (ToT a : ToTs (Take n inp ++ Drop ('S n) inp))
         ~ (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))))
forall (n :: Peano) kind (any :: kind -> *) (inp :: [kind])
       (out :: [kind]) (a :: kind).
(KnownPeano n, SingI n, TestEquality any) =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDIG' kind n inp out a))
digConstraint Sing n
n (StackVars inp -> Rec TVal (ToTs inp)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars inp
inp) (StackVars out -> TValStack (ToTs out)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals StackVars out
out) (StkEl a -> TVal (ToT a)
forall a. StkEl a -> TVal (ToT a)
toTVal StkEl a
a)
  Dict
  ((SingI n, KnownPeano n,
    RequireLongerThan
      (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))) n,
    (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp)))
    ~ (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))),
    (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))
    ~ (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))),
   (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ inp,
    (a : (Take n inp ++ Drop ('S n) inp))
    ~ (a : (Take n inp ++ Drop ('S n) inp))))
-> Maybe
     (Dict
        ((SingI n, KnownPeano n,
          RequireLongerThan
            (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))) n,
          (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp)))
          ~ (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))),
          (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))
          ~ (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))),
         (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ inp,
          (a : (Take n inp ++ Drop ('S n) inp))
          ~ (a : (Take n inp ++ Drop ('S n) inp)))))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((SingI n, KnownPeano n,
    RequireLongerThan
      (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))) n,
    (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp)))
    ~ (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp))),
    (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))
    ~ (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))),
   (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ inp,
    (a : (Take n inp ++ Drop ('S n) inp))
    ~ (a : (Take n inp ++ Drop ('S n) inp))))
forall (a :: Constraint). a => Dict a
Dict

----------------------------------------------------------------------------
-- Morley constraints
----------------------------------------------------------------------------

dugConstraint
  :: (KnownPeano n, SingI n, TestEquality any)
  => Sing n -> Rec any inp -> Rec any out -> any a
  -> Maybe (Dict (MI.ConstraintDUG' kind n inp out a))
dugConstraint :: Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUG' kind n inp out a))
dugConstraint n :: Sing n
n inp :: Rec any inp
inp out :: Rec any out
out a :: any a
a = do
  Dict (RequireLongerThan out n)
Dict <- Rec any out -> Sing n -> Maybe (Dict (RequireLongerThan out n))
forall k (any :: k -> *) (stk :: [k]) (n :: Peano).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any out
out Sing n
n
  (a : Drop ('S 'Z) inp) :~: inp
Refl <- Rec any (a : Drop ('S 'Z) inp)
-> Rec any inp -> Maybe ((a : Drop ('S 'Z) inp) :~: inp)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (any a
a any a
-> Rec any (Drop ('S 'Z) inp) -> Rec any (a : Drop ('S 'Z) inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing ('S 'Z) -> Rec any inp -> Rec any (Drop ('S 'Z) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat 'Z -> SingNat ('S 'Z)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat 'Z
SZ) Rec any inp
inp) Rec any inp
inp
  (Take n (Drop ('S 'Z) inp) ++ (a : Drop n (Drop ('S 'Z) inp)))
:~: out
Refl <- Rec
  any (Take n (Drop ('S 'Z) inp) ++ (a : Drop n (Drop ('S 'Z) inp)))
-> Rec any out
-> Maybe
     ((Take n (Drop ('S 'Z) inp) ++ (a : Drop n (Drop ('S 'Z) inp)))
      :~: out)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Sing n
-> Rec any (Drop ('S 'Z) inp)
-> Rec any (Take n (Drop ('S 'Z) inp))
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n (Sing ('S 'Z) -> Rec any inp -> Rec any (Drop ('S 'Z) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat 'Z -> SingNat ('S 'Z)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat 'Z
SZ) Rec any inp
inp) Rec any (Take n (Drop ('S 'Z) inp))
-> Rec any (a : Drop n (Drop ('S 'Z) inp))
-> Rec
     any (Take n (Drop ('S 'Z) inp) ++ (a : Drop n (Drop ('S 'Z) inp)))
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> any a
a any a
-> Rec any (Drop n (Drop ('S 'Z) inp))
-> Rec any (a : Drop n (Drop ('S 'Z) inp))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing ('S n) -> Rec any inp -> Rec any (Drop ('S n) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) Rec any inp
inp) Rec any out
out
  Dict
  (SingI n, KnownPeano n, RequireLongerThan out n,
   (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out)
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerThan out n,
         (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  (SingI n, KnownPeano n, RequireLongerThan out n,
   (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out)
forall (a :: Constraint). a => Dict a
Dict

dipNConstraint
  :: (KnownPeano n, SingI n, TestEquality any)
  => Sing n -> Rec any inp -> Rec any out -> Rec any s -> Rec any s'
  -> Maybe (Dict (MI.ConstraintDIPN' kind n inp out s s'))
dipNConstraint :: Sing n
-> Rec any inp
-> Rec any out
-> Rec any s
-> Rec any s'
-> Maybe (Dict (ConstraintDIPN' kind n inp out s s'))
dipNConstraint n :: Sing n
n inp :: Rec any inp
inp out :: Rec any out
out s :: Rec any s
s s' :: Rec any s'
s' = do
  Dict (RequireLongerOrSameLength inp n)
Dict <- Rec any inp
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength inp n))
forall k (any :: k -> *) (stk :: [k]) (n :: Peano).
Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any inp
inp Sing n
n
  (Take n inp ++ s) :~: inp
Refl <- Rec any (Take n inp ++ s)
-> Rec any inp -> Maybe ((Take n inp ++ s) :~: inp)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Sing n -> Rec any inp -> Rec any (Take n inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n Rec any inp
inp Rec any (Take n inp) -> Rec any s -> Rec any (Take n inp ++ s)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec any s
s) Rec any inp
inp
  (Take n inp ++ s') :~: out
Refl <- Rec any (Take n inp ++ s')
-> Rec any out -> Maybe ((Take n inp ++ s') :~: out)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Sing n -> Rec any inp -> Rec any (Take n inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n Rec any inp
inp Rec any (Take n inp) -> Rec any s' -> Rec any (Take n inp ++ s')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec any s'
s') Rec any out
out
  Dict
  (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
   out ~ out)
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
         out ~ out))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, inp ~ inp,
   out ~ out)
forall (a :: Constraint). a => Dict a
Dict

digConstraint
  :: (KnownPeano n, SingI n, TestEquality any)
  => Sing n -> Rec any inp -> Rec any out -> any a
  -> Maybe (Dict (MI.ConstraintDIG' kind n inp out a))
digConstraint :: Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDIG' kind n inp out a))
digConstraint n :: Sing n
n inp :: Rec any inp
inp out :: Rec any out
out a :: any a
a = do
  Dict (RequireLongerThan inp n)
Dict <- Rec any inp -> Sing n -> Maybe (Dict (RequireLongerThan inp n))
forall k (any :: k -> *) (stk :: [k]) (n :: Peano).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any inp
inp Sing n
n
  inp :~: (Take n inp ++ (a : Drop ('S n) inp))
Refl <- Rec any inp
-> Rec any (Take n inp ++ (a : Drop ('S n) inp))
-> Maybe (inp :~: (Take n inp ++ (a : Drop ('S n) inp)))
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Rec any inp
inp (Sing n -> Rec any inp -> Rec any (Take n inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n Rec any inp
inp Rec any (Take n inp)
-> Rec any (a : Drop ('S n) inp)
-> Rec any (Take n inp ++ (a : Drop ('S n) inp))
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> any a
a any a -> Rec any (Drop ('S n) inp) -> Rec any (a : Drop ('S n) inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing ('S n) -> Rec any inp -> Rec any (Drop ('S n) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) Rec any inp
inp)
  out :~: (a : (Take n inp ++ Drop ('S n) inp))
Refl <- Rec any out
-> Rec any (a : (Take n inp ++ Drop ('S n) inp))
-> Maybe (out :~: (a : (Take n inp ++ Drop ('S n) inp)))
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Rec any out
out (any a
a any a -> Rec any (Take n inp) -> Rec any (a : Take n inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n -> Rec any inp -> Rec any (Take n inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n Rec any inp
inp Rec any (a : Take n inp)
-> Rec any (Drop ('S n) inp)
-> Rec any ((a : Take n inp) ++ Drop ('S n) inp)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Sing ('S n) -> Rec any inp -> Rec any (Drop ('S n) inp)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (SingNat n -> SingNat ('S n)
forall (n1 :: Peano).
(SingI n1, KnownPeano n1) =>
SingNat n1 -> SingNat ('S n1)
SS SingNat n
Sing n
n) Rec any inp
inp)
  Dict
  (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ inp,
   (a : (Take n inp ++ Drop ('S n) inp))
   ~ (a : (Take n inp ++ Drop ('S n) inp)))
-> Maybe
     (Dict
        (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ inp,
         (a : (Take n inp ++ Drop ('S n) inp))
         ~ (a : (Take n inp ++ Drop ('S n) inp))))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ inp,
   (a : (Take n inp ++ Drop ('S n) inp))
   ~ (a : (Take n inp ++ Drop ('S n) inp)))
forall (a :: Constraint). a => Dict a
Dict

----------------------------------------------------------------------------
-- Conversion for ToT constraints
----------------------------------------------------------------------------

-- | Stack representation of 'MI.T' used for constraint checking
type TValStack (stk :: [MI.T]) = Rec TVal stk

-- | Simple datatype used to keep a 'MI.T' and its 'Typeable' constraint
data TVal (a :: MI.T) where
  TVal :: Typeable a => TVal a

instance TestEquality TVal where
  testEquality :: TVal a -> TVal b -> Maybe (a :~: b)
testEquality (TVal a
TVal :: TVal a) (TVal b
TVal :: TVal b) = (Typeable a, Typeable b) => Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b

toTVal :: forall a. StkEl a -> TVal (ToT a)
toTVal :: StkEl a -> TVal (ToT a)
toTVal = \case
  NoRef -> Typeable (ToT a) => TVal (ToT a)
forall (a :: T). Typeable a => TVal a
TVal @(ToT a)
  Ref _ -> Typeable (ToT a) => TVal (ToT a)
forall (a :: T). Typeable a => TVal a
TVal @(ToT a)

toTVals :: StackVars stk -> TValStack (ToTs stk)
toTVals :: StackVars stk -> TValStack (ToTs stk)
toTVals = \case
  RNil          -> TValStack (ToTs stk)
forall u (a :: u -> *). Rec a '[]
RNil
  (NoRef :& xs :: Rec StkEl rs
xs) -> TVal (ToT r)
forall (a :: T). Typeable a => TVal a
TVal TVal (ToT r) -> Rec TVal (ToTs rs) -> Rec TVal (ToT r : ToTs rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs -> Rec TVal (ToTs rs)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals Rec StkEl rs
xs
  (Ref _ :& xs :: Rec StkEl rs
xs) -> TVal (ToT r)
forall (a :: T). Typeable a => TVal a
TVal TVal (ToT r) -> Rec TVal (ToTs rs) -> Rec TVal (ToT r : ToTs rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs -> Rec TVal (ToTs rs)
forall (stk :: [*]). StackVars stk -> TValStack (ToTs stk)
toTVals Rec StkEl rs
xs

----------------------------------------------------------------------------
-- Vinyl manipulation helpers
----------------------------------------------------------------------------

rtake :: Sing n -> Rec any s -> Rec any (Take n s)
rtake :: Sing n -> Rec any s -> Rec any (Take n s)
rtake sn :: Sing n
sn stk :: Rec any s
stk = case (SingNat n
Sing n
sn, Rec any s
stk) of
  (SZ, _)           -> Rec any (Take n s)
forall u (a :: u -> *). Rec a '[]
RNil
  (SS n :: SingNat n1
n, (x :: any r
x :& xs :: Rec any rs
xs)) -> any r
x any r -> Rec any (Take n1 rs) -> Rec any (r : Take n1 rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n1 -> Rec any rs -> Rec any (Take n1 rs)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake SingNat n1
Sing n1
n Rec any rs
xs
  (SS _, RNil)      -> Text -> Rec any '[]
forall a. HasCallStack => Text -> a
error "given stack is too small"

rdrop :: Sing n -> Rec any s -> Rec any (Drop n s)
rdrop :: Sing n -> Rec any s -> Rec any (Drop n s)
rdrop sn :: Sing n
sn stk :: Rec any s
stk = case (SingNat n
Sing n
sn, Rec any s
stk) of
  (SZ, _)           -> Rec any s
Rec any (Drop n s)
stk
  (SS n :: SingNat n1
n, (_ :& xs :: Rec any rs
xs)) -> Sing n1 -> Rec any rs -> Rec any (Drop n1 rs)
forall k (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop SingNat n1
Sing n1
n Rec any rs
xs
  (SS _, RNil)      -> Text -> Rec any '[]
forall a. HasCallStack => Text -> a
error "given stack is too small"