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

{- |
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.Backend.Lookup
  ( -- * Variable Lookup Actions
    varActionGet
  , varActionSet
  , varActionUpdate
  , varActionOperation

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

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

import Indigo.Common.Var
  (HasSideEffects, Ops, RefId, StackVars(..), StackVars', StkEl(..), Var(..), operationsVar)
import Indigo.Lorentz
import Lorentz.Instr qualified as L
import Lorentz.Macro qualified as L
import Morley.Michelson.Typed (ToTs)
import Morley.Michelson.Typed.Instr.Constraints qualified as MI
import Morley.Michelson.Typed.T qualified as MI
import Morley.Util.Peano
import Morley.Util.Sing

----------------------------------------------------------------------------
-- 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 :: forall a (stk :: [*]).
KnownValue a =>
RefId -> StackVars stk -> stk :-> (a : stk)
varActionGet RefId
_ StackVars stk
FailureStack = Text -> stk :-> (a : stk)
forall a. HasCallStack => Text -> a
error Text
"You try to get a cell on failure stack"
varActionGet RefId
ref (StkElements Rec StkEl stk
stk) = case forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars' s -> VarDepth
varDepth @a RefId
ref Rec StkEl stk
stk of
  VarDepth Sing idx
n -> Sing idx -> RefId -> Rec StkEl stk -> stk :-> (a : stk)
forall (inp :: [*]) a (m :: Peano).
(HasCallStack, KnownValue a) =>
Sing m -> RefId -> StackVars' inp -> inp :-> (a : inp)
duupXVar Sing idx
n RefId
ref Rec StkEl 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 :: forall a (stk :: [*]).
KnownValue a =>
RefId -> StackVars stk -> (a : stk) :-> stk
varActionSet RefId
_ StackVars stk
FailureStack = Text -> (a : stk) :-> stk
forall a. HasCallStack => Text -> a
error Text
"You try to set a cell on failure stack"
varActionSet RefId
ref (StkElements Rec StkEl stk
stk) = case forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars' s -> VarDepth
varDepth @a RefId
ref Rec StkEl stk
stk of
  VarDepth 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 (Sing idx -> SingNat ('S idx)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing idx
n) RefId
ref (StkEl a
forall a. (KnownValue a, KnownIsoT a) => StkEl a
NoRef StkEl a -> Rec StkEl stk -> StackVars' (a : stk)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl 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 :: forall a b (stk :: [*]).
(KnownValue a, KnownValue b) =>
RefId -> StackVars stk -> ('[b, a] :-> '[a]) -> (b : stk) :-> stk
varActionUpdate RefId
_ StackVars stk
FailureStack '[b, a] :-> '[a]
_ = Text -> (b : stk) :-> stk
forall a. HasCallStack => Text -> a
error Text
"You try to update a cell on failure stack"
varActionUpdate RefId
v (StkElements Rec StkEl stk
stk) '[b, a] :-> '[a]
instr = case forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars' s -> VarDepth
varDepth @a RefId
v Rec StkEl stk
stk of
  VarDepth 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 (Sing idx -> SingNat ('S idx)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing idx
n) RefId
v (StkEl b
forall a. (KnownValue a, KnownIsoT a) => StkEl a
NoRef StkEl b -> Rec StkEl stk -> StackVars' (b : stk)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl 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 :: forall (stk :: [*]).
HasSideEffects =>
StackVars stk -> (Operation : stk) :-> stk
varActionOperation StackVars stk
s =
  case Var Ops
HasSideEffects => Var Ops
operationsVar of
    Var RefId
refId -> 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).
     ( HasCallStack
     , KnownValue a
     )
  => Sing m -> RefId -> StackVars' inp -> inp :-> (a ': inp)
duupXVar :: forall (inp :: [*]) a (m :: Peano).
(HasCallStack, KnownValue a) =>
Sing m -> RefId -> StackVars' inp -> inp :-> (a : inp)
duupXVar Sing m
m RefId
v StackVars' inp
stk =
  Maybe
  (Dict
     ((RequireLongerOrSameLength (ToTs inp) ('S m), 'True ~ 'True,
       ToTs inp
       ~ (LazyTake m (ToTs inp) ++ (ToT a : Drop ('S m) (ToTs inp))),
       (ToT a : ToTs inp) ~ (ToT a : ToTs inp)),
      (RequireLongerOrSameLength inp ('S m), 'True ~ 'True,
       inp ~ (LazyTake m inp ++ (a : Drop ('S m) inp)),
       (a : inp) ~ (a : inp)),
      SingI ('S m)))
-> (((RequireLongerOrSameLength (ToTs inp) ('S m), 'True ~ 'True,
      ToTs inp
      ~ (LazyTake m (ToTs inp) ++ (ToT a : Drop ('S m) (ToTs inp))),
      (ToT a : ToTs inp) ~ (ToT a : ToTs inp)),
     (RequireLongerOrSameLength inp ('S m), 'True ~ 'True,
      inp ~ (LazyTake m inp ++ (a : Drop ('S m) inp)),
      (a : inp) ~ (a : inp)),
     SingI ('S m)) =>
    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' (a : inp)
-> Maybe (Dict (ConstraintDUPNLorentz ('S m) inp (a : inp) a))
forall (n :: Peano) (inp :: [*]) a (out :: [*]).
Sing n
-> StackVars' inp
-> StkEl a
-> StackVars' out
-> Maybe (Dict (ConstraintDUPNLorentz n inp out a))
dupNLorentzConstraint Sing ('S m)
SingNat ('S m)
n StackVars' inp
stk StkEl a
a StackVars' (a : inp)
out) ((((RequireLongerOrSameLength (ToTs inp) ('S m), 'True ~ 'True,
    ToTs inp
    ~ (LazyTake m (ToTs inp) ++ (ToT a : Drop ('S m) (ToTs inp))),
    (ToT a : ToTs inp) ~ (ToT a : ToTs inp)),
   (RequireLongerOrSameLength inp ('S m), 'True ~ 'True,
    inp ~ (LazyTake m inp ++ (a : Drop ('S m) inp)),
    (a : inp) ~ (a : inp)),
   SingI ('S m)) =>
  inp :-> (a : inp))
 -> inp :-> (a : inp))
-> (((RequireLongerOrSameLength (ToTs inp) ('S m), 'True ~ 'True,
      ToTs inp
      ~ (LazyTake m (ToTs inp) ++ (ToT a : Drop ('S m) (ToTs inp))),
      (ToT a : ToTs inp) ~ (ToT a : ToTs inp)),
     (RequireLongerOrSameLength inp ('S m), 'True ~ 'True,
      inp ~ (LazyTake m inp ++ (a : Drop ('S m) inp)),
      (a : inp) ~ (a : inp)),
     SingI ('S m)) =>
    inp :-> (a : inp))
-> inp :-> (a : inp)
forall a b. (a -> b) -> a -> b
$
  Dict
  ((SingI (ToT a),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket (ToT a) ~ 'False)),
   KnownValue a)
-> (((SingI (ToT a),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
         ('Text "Type `ticket` is not allowed in this scope")
         (() :: Constraint),
       ContainsTicket (ToT a) ~ 'False)),
     KnownValue a) =>
    inp :-> (a : inp))
-> inp :-> (a : inp)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (StkEl a
-> Dict
     ((SingI (ToT a),
       (FailWhenElsePoly
          (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
          ('Text "Type `ticket` is not allowed in this scope")
          (() :: Constraint),
        ContainsTicket (ToT a) ~ 'False)),
      KnownValue a)
forall a.
(KnownValue a, HasCallStack) =>
StkEl a -> Dict (Dupable a)
dupableConstraint StkEl a
a) ((((SingI (ToT a),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket (ToT a) ~ 'False)),
   KnownValue a) =>
  inp :-> (a : inp))
 -> inp :-> (a : inp))
-> (((SingI (ToT a),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
         ('Text "Type `ticket` is not allowed in this scope")
         (() :: Constraint),
       ContainsTicket (ToT a) ~ 'False)),
     KnownValue a) =>
    inp :-> (a : inp))
-> inp :-> (a : inp)
forall a b. (a -> b) -> a -> b
$
    forall (n :: Peano) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz n inp out a, Dupable a) =>
inp :-> out
L.dupNPeano @('S m) @a @inp @(a ': inp)
  where
    a :: StkEl a
a = forall a. (KnownValue a, KnownIsoT a) => RefId -> StkEl a
Ref @a RefId
v
    n :: SingNat ('S m)
n = Sing m -> SingNat ('S m)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing m
m
    out :: StackVars' (a : inp)
out = 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
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 :: 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
n RefId
v stk :: StackVars' (a : s)
stk@(StkEl r
_ :& 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 (forall a. (KnownValue a, KnownIsoT 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
$
    forall {k} {k1} (n :: Peano) (s :: [*]) a (mid :: k) (tail :: k1).
ReplaceN n s a mid tail =>
(a : s) :-> s
forall (n :: Peano) (s :: [*]) a (mid :: [*]) (tail :: [*]).
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 :: 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
n RefId
v stk :: StackVars' (a : s)
stk@(StkEl r
a :& Rec StkEl rs
s) '[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 (forall a. (KnownValue a, KnownIsoT 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
$
    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
forall (n :: Peano) (s :: [*]) a b (mid :: [*]) (tail :: [*]).
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 (Sing 'Z -> SingNat ('S 'Z)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing 'Z
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 :: forall (c :: Constraint) e r.
(HasDict c e, HasCallStack) =>
Maybe e -> (c => r) -> r
withVarMaybeDict 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 = Text
"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 :: 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 :: forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars' s -> VarDepth
varDepth RefId
refId = \case
  StackVars' s
RNil -> Text -> VarDepth
forall a. HasCallStack => Text -> a
error (Text -> VarDepth) -> Text -> VarDepth
forall a b. (a -> b) -> a -> b
$
    Text
"You are looking for manually created or leaked variable. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
    RefId -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty RefId
refId Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" of type " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TypeRep -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))
  stk :: StackVars' s
stk@(StkEl r
_ :& Rec StkEl rs
_) -> 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 :: forall a (s :: [*]) x (xs :: [*]).
(KnownValue a, s ~ (x : xs)) =>
RefId -> StackVars' s -> VarDepth
varDepthNonEmpty RefId
ref (StkEl r
x :& Rec StkEl rs
xs) = case StkEl r
x of
  Ref RefId
topRef | RefId
ref RefId -> RefId -> Bool
forall a. Eq a => a -> a -> Bool
== RefId
topRef -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @x of
    Just a :~: x
Refl -> Sing 'Z -> VarDepth
forall (idx :: Peano). Sing idx -> VarDepth
VarDepth Sing 'Z
SingNat 'Z
SZ
    Maybe (a :~: x)
Nothing   -> Text -> VarDepth
forall a. HasCallStack => Text -> a
error (Text -> VarDepth) -> Text -> VarDepth
forall a b. (a -> b) -> a -> b
$
      Text
"Invalid variable type. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RefId -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty RefId
ref Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
      Text
".\nWas looking for a " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TypeRep -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a -> TypeRep) -> Proxy a -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
      Text
", but found a: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TypeRep -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Proxy x -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy x -> TypeRep) -> Proxy x -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
  StkEl r
_ -> case forall a (s :: [*]).
KnownValue a =>
RefId -> StackVars' s -> VarDepth
varDepth @a RefId
ref Rec StkEl rs
xs of
    VarDepth Sing idx
idx -> Sing ('S idx) -> VarDepth
forall (idx :: Peano). Sing idx -> VarDepth
VarDepth (Sing idx -> SingNat ('S idx)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing idx
idx)

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

replaceNClassConstraint
  :: Sing n -> StackVars' s -> StkEl a -> StackVars' mid -> StackVars' tail
  -> Maybe (Dict (L.ReplaceN n s a mid tail))
replaceNClassConstraint :: 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 StackVars' s
s StkEl a
a StackVars' mid
mid StackVars' tail
tail = case Sing n
n of
  Sing n
SingNat n
SZ -> Maybe (Dict (ReplaceN n s a mid tail))
forall a. Maybe a
Nothing
  SS Sing n
SingNat n
SZ -> case StackVars' s
s of
    (StkEl r
x :& 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
    StackVars' s
_ -> Maybe (Dict (ReplaceN n s a mid tail))
forall a. Maybe a
Nothing
  SS (SS Sing n
m) -> do
    Dict
  ((ToTs tail ~ Drop ('S ('S n)) (ToTs s),
    (RequireLongerOrSameLength (ToT a : ToTs s) ('S ('S n)),
     (ToT a
        : Head (ToTs s)
        : (LazyTake n (Tail (ToTs s)) ++ (ToT a : ToTs tail)))
     ~ (ToT a : ToTs s),
     (ToT a : Head (ToTs s) : (LazyTake n (Tail (ToTs s)) ++ ToTs tail))
     ~ ToTs mid,
     (ToT a : ToTs tail) ~ Drop ('S n) (ToTs s),
     ToTs tail ~ Drop ('S ('S n)) (ToTs mid)),
    (RequireLongerThan (ToTs s) ('S n),
     ToTs mid
     ~ (ToT a
          : Head (ToTs s)
          : (LazyTake n (Tail (ToTs s)) ++ Drop ('S ('S n)) (ToTs s))),
     ToTs s
     ~ (Head (Drop ('S 'Z) (ToTs mid))
          : (LazyTake n (Tail (Drop ('S 'Z) (ToTs mid)))
             ++ (ToT a : Drop ('S ('S n)) (ToTs mid)))))),
   (tail ~ Drop ('S ('S n)) s,
    (RequireLongerOrSameLength (a : s) ('S ('S n)),
     (a : Head s : (LazyTake n (Tail s) ++ (a : tail))) ~ (a : s),
     (a : Head s : (LazyTake n (Tail s) ++ tail)) ~ mid,
     (a : tail) ~ Drop ('S n) s, tail ~ Drop ('S ('S n)) mid),
    (RequireLongerThan s ('S n),
     mid ~ (a : Head s : (LazyTake n (Tail s) ++ Drop ('S ('S n)) s)),
     s
     ~ (Head (Drop ('S 'Z) mid)
          : (LazyTake n (Tail (Drop ('S 'Z) mid))
             ++ (a : Drop ('S ('S n)) mid))))))
Dict <- Sing ('S n)
-> StackVars' s
-> StkEl a
-> StackVars' mid
-> StackVars' tail
-> Maybe (Dict (ConstraintReplaceNLorentz ('S n) s a mid tail))
forall (n :: Peano) (s :: [*]) a (mid :: [*]) (tail :: [*]).
Sing n
-> StackVars' s
-> StkEl a
-> StackVars' mid
-> StackVars' tail
-> Maybe (Dict (ConstraintReplaceNLorentz n s a mid tail))
replaceNLorentzConstraint (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
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)
 -> Maybe (Dict (ReplaceN n s a mid tail)))
-> Dict (ReplaceN n s a mid tail)
-> Maybe (Dict (ReplaceN n s a mid tail))
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => Dict (ReplaceN n s a mid tail))
-> Dict (ReplaceN n s a mid tail)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
m ((SingI n => Dict (ReplaceN n s a mid tail))
 -> Dict (ReplaceN n s a mid tail))
-> (SingI n => Dict (ReplaceN n s a mid tail))
-> Dict (ReplaceN n s a mid tail)
forall a b. (a -> b) -> a -> b
$ SingI n => 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 :: 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 StackVars' s
s StkEl a
a StkEl b
b StackVars' mid
mid StackVars' tail
tail = case Sing n
n of
  Sing n
SingNat n
SZ -> Maybe (Dict (UpdateN n s a b mid tail))
forall a. Maybe a
Nothing
  SS Sing n
SingNat n
SZ -> case StackVars' s
s of
    (StkEl r
x :& 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
    StackVars' s
_ -> Maybe (Dict (UpdateN n s a b mid tail))
forall a. Maybe a
Nothing
  SS (SS Sing n
SingNat n
SZ) -> case StackVars' s
s of
    (StkEl r
_x :& StkEl r
y :& 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
    StackVars' s
_ -> Maybe (Dict (UpdateN n s a b mid tail))
forall a. Maybe a
Nothing
  SS (SS (SS Sing n
m)) -> do
    Dict
  ((ToTs tail ~ Drop ('S ('S ('S n))) (ToTs s),
    (RequireLongerThan (ToTs mid) ('S ('S n)),
     (ToT a : ToTs s)
     ~ (ToT a
          : Head (ToTs mid) : Head (Tail (ToTs mid))
          : (LazyTake n (Tail (Tail (ToTs mid)))
             ++ Drop ('S ('S ('S n))) (ToTs mid))),
     ToTs mid
     ~ (Head (ToTs s)
          : Head (Tail (ToTs s))
          : (LazyTake n (Tail (Tail (ToTs s)))
             ++ (ToT a : Drop ('S ('S n)) (ToTs s))))),
    (RequireLongerOrSameLength (ToTs mid) ('S ('S n)),
     (Head (ToTs mid)
        : Head (Tail (ToTs mid))
        : (LazyTake n (Tail (Tail (ToTs mid)))
           ++ (ToT a : ToT b : ToTs tail)))
     ~ ToTs mid,
     (Head (ToTs mid)
        : Head (Tail (ToTs mid))
        : (LazyTake n (Tail (Tail (ToTs mid))) ++ (ToT b : ToTs tail)))
     ~ ToTs s,
     (ToT a : ToT b : ToTs tail) ~ Drop ('S ('S n)) (ToTs mid),
     (ToT b : ToTs tail) ~ Drop ('S ('S n)) (ToTs s))),
   (tail ~ Drop ('S ('S ('S n))) s,
    (RequireLongerThan mid ('S ('S n)),
     (a : s)
     ~ (a : Head mid : Head (Tail mid)
          : (LazyTake n (Tail (Tail mid)) ++ Drop ('S ('S ('S n))) mid)),
     mid
     ~ (Head s
          : Head (Tail s)
          : (LazyTake n (Tail (Tail s)) ++ (a : Drop ('S ('S n)) s)))),
    (RequireLongerOrSameLength mid ('S ('S n)),
     (Head mid
        : Head (Tail mid)
        : (LazyTake n (Tail (Tail mid)) ++ (a : b : tail)))
     ~ mid,
     (Head mid
        : Head (Tail mid) : (LazyTake n (Tail (Tail mid)) ++ (b : tail)))
     ~ s,
     (a : b : tail) ~ Drop ('S ('S n)) mid,
     (b : tail) ~ Drop ('S ('S n)) s)))
Dict <- Sing ('S ('S n))
-> StackVars' s
-> StkEl a
-> StkEl b
-> StackVars' mid
-> StackVars' tail
-> Maybe
     (Dict (ConstraintUpdateNLorentz ('S ('S n)) s a 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 (ConstraintUpdateNLorentz n s a b mid tail))
updateNLorentzConstraint (Sing ('S n) -> SingNat ('S ('S n))
forall (n :: Peano). Sing n -> SingNat ('S n)
SS (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
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)
 -> Maybe (Dict (UpdateN n s a b mid tail)))
-> Dict (UpdateN n s a b mid tail)
-> Maybe (Dict (UpdateN n s a b mid tail))
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => Dict (UpdateN n s a b mid tail))
-> Dict (UpdateN n s a b mid tail)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
m ((SingI n => Dict (UpdateN n s a b mid tail))
 -> Dict (UpdateN n s a b mid tail))
-> (SingI n => Dict (UpdateN n s a b mid tail))
-> Dict (UpdateN n s a b mid tail)
forall a b. (a -> b) -> a -> b
$ SingI n => Dict (UpdateN n s a b mid tail)
forall (a :: Constraint). a => Dict a
Dict

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

dupableConstraint
  :: (KnownValue a, HasCallStack)
  => StkEl a
  -> Dict (Dupable a)
dupableConstraint :: forall a.
(KnownValue a, HasCallStack) =>
StkEl a -> Dict (Dupable a)
dupableConstraint (StkEl a
_ :: StkEl a) =
  case forall a. KnownValue a => DupableDecision a
decideOnDupable @a of
    DupableDecision a
IsDupable -> Dict (Dupable a)
forall (a :: Constraint). a => Dict a
Dict
    DupableDecision a
IsNotDupable ->
      Text -> Dict (Dupable a)
forall a. HasCallStack => Text -> a
error Text
"Non-dupable values (like tickets) are not supported yet"

dupNLorentzConstraint
  :: Sing n -> StackVars' inp -> StkEl a -> StackVars' out
  -> Maybe (Dict (L.ConstraintDUPNLorentz n inp out a))
dupNLorentzConstraint :: forall (n :: Peano) (inp :: [*]) a (out :: [*]).
Sing n
-> StackVars' inp
-> StkEl a
-> StackVars' out
-> Maybe (Dict (ConstraintDUPNLorentz n inp out a))
dupNLorentzConstraint Sing n
n StackVars' inp
inp StkEl a
a StackVars' out
out = do
  Dict
  (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True,
   inp ~ (LazyTake (Decrement n) inp ++ (a : Drop n inp)),
   out ~ (a : inp))
Dict <- Sing n
-> StackVars' inp
-> StackVars' out
-> StkEl a
-> Maybe
     (Dict
        (RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True,
         inp ~ (LazyTake (Decrement n) inp ++ (a : Drop n inp)),
         out ~ (a : inp)))
forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (a :: kind).
TestEquality any =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUPN' kind n inp out a))
dupNConstraint Sing n
n StackVars' inp
inp StackVars' out
out StkEl a
a
  Dict
  (RequireLongerOrSameLength (ToTs inp) n, (n > 'Z) ~ 'True,
   ToTs inp
   ~ (LazyTake (Decrement n) (ToTs inp)
      ++ (ToT a : Drop n (ToTs inp))),
   (ToT a : ToTs inp) ~ (ToT a : ToTs inp))
Dict <- Sing n
-> Rec TVal (ToTs inp)
-> Rec TVal (ToT a : ToTs inp)
-> TVal (ToT a)
-> Maybe
     (Dict
        (RequireLongerOrSameLength (ToTs inp) n, (n > 'Z) ~ 'True,
         ToTs inp
         ~ (LazyTake (Decrement n) (ToTs inp)
            ++ (ToT a : Drop n (ToTs inp))),
         (ToT a : ToTs inp) ~ (ToT a : ToTs inp)))
forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (a :: kind).
TestEquality any =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUPN' kind n inp out a))
dupNConstraint 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 (ConstraintDUPNLorentz n inp out a)
-> Maybe (Dict (ConstraintDUPNLorentz n inp out a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Dict (ConstraintDUPNLorentz n inp out a)
 -> Maybe (Dict (ConstraintDUPNLorentz n inp out a)))
-> Dict (ConstraintDUPNLorentz n inp out a)
-> Maybe (Dict (ConstraintDUPNLorentz n inp out a))
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => Dict (ConstraintDUPNLorentz n inp out a))
-> Dict (ConstraintDUPNLorentz n inp out a)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
n ((SingI n => Dict (ConstraintDUPNLorentz n inp out a))
 -> Dict (ConstraintDUPNLorentz n inp out a))
-> (SingI n => Dict (ConstraintDUPNLorentz n inp out a))
-> Dict (ConstraintDUPNLorentz n inp out a)
forall a b. (a -> b) -> a -> b
$ SingI n => Dict (ConstraintDUPNLorentz n inp out a)
forall (a :: Constraint). a => Dict a
Dict

updateNLorentzConstraint
  :: Sing n -> StackVars' s -> StkEl a -> StkEl b -> StackVars' mid -> StackVars' tail
  -> Maybe (Dict (L.ConstraintUpdateNLorentz n s a b mid tail))
updateNLorentzConstraint :: forall (n :: Peano) (s :: [*]) a b (mid :: [*]) (tail :: [*]).
Sing n
-> StackVars' s
-> StkEl a
-> StkEl b
-> StackVars' mid
-> StackVars' tail
-> Maybe (Dict (ConstraintUpdateNLorentz n s a b mid tail))
updateNLorentzConstraint Sing n
n StackVars' s
s StkEl a
a StkEl b
b StackVars' mid
mid 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 (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS 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 (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
n) (StackVars' s -> Rec TVal (ToTs s)
forall (stk :: [*]). StackVars' stk -> TValStack (ToTs stk)
toTVals StackVars' s
s))
  Dict
  ((RequireLongerThan (ToTs mid) n,
    (ToT a : ToTs s)
    ~ (ToT a : (LazyTake n (ToTs mid) ++ Drop ('S n) (ToTs mid))),
    ToTs mid ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
   (RequireLongerThan mid n,
    (a : s) ~ (a : (LazyTake n mid ++ Drop ('S n) mid)),
    mid ~ (LazyTake n s ++ (a : Drop n s))),
   SingI n)
Dict <- Sing n
-> StackVars' (a : s)
-> StackVars' mid
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n (a : s) mid a))
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
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
  ((RequireLongerOrSameLength
      (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
    (LazyTake n (ToTs mid) ++ (ToT a : ToT b : ToTs tail))
    ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
    (LazyTake n (ToTs mid) ++ (ToT b : ToTs tail)) ~ ToTs s,
    (ToT a : ToT b : ToTs tail)
    ~ Drop n (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
    (ToT b : ToTs tail) ~ Drop n (ToTs s)),
   (RequireLongerOrSameLength mid n,
    (LazyTake n mid ++ (a : b : tail)) ~ mid,
    (LazyTake n mid ++ (b : tail)) ~ s, (a : b : tail) ~ Drop n mid,
    (b : tail) ~ Drop n s),
   SingI n)
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' :: [*]).
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,
    (RequireLongerThan
       (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
    (RequireLongerOrSameLength
       (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
     ToTs s ~ ToTs s,
     (ToT a : ToT b : ToTs tail) ~ (ToT a : ToT b : ToTs tail),
     (ToT b : ToTs tail) ~ (ToT b : ToTs tail))),
   (tail ~ tail,
    (RequireLongerThan mid n, (a : s) ~ (a : s), mid ~ mid),
    (RequireLongerOrSameLength mid n, mid ~ mid, s ~ s,
     (a : b : tail) ~ (a : b : tail), (b : tail) ~ (b : tail))))
-> Maybe
     (Dict
        ((ToTs tail ~ ToTs tail,
          (RequireLongerThan
             (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
           (ToT a : ToTs s) ~ (ToT a : ToTs s),
           (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
           ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
          (RequireLongerOrSameLength
             (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
           (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
           ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
           ToTs s ~ ToTs s,
           (ToT a : ToT b : ToTs tail) ~ (ToT a : ToT b : ToTs tail),
           (ToT b : ToTs tail) ~ (ToT b : ToTs tail))),
         (tail ~ tail,
          (RequireLongerThan mid n, (a : s) ~ (a : s), mid ~ mid),
          (RequireLongerOrSameLength mid n, mid ~ mid, s ~ s,
           (a : b : tail) ~ (a : b : tail), (b : tail) ~ (b : tail)))))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  ((ToTs tail ~ ToTs tail,
    (RequireLongerThan
       (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))),
    (RequireLongerOrSameLength
       (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))) n,
     (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s)))
     ~ (LazyTake n (ToTs s) ++ (ToT a : Drop n (ToTs s))),
     ToTs s ~ ToTs s,
     (ToT a : ToT b : ToTs tail) ~ (ToT a : ToT b : ToTs tail),
     (ToT b : ToTs tail) ~ (ToT b : ToTs tail))),
   (tail ~ tail,
    (RequireLongerThan mid n, (a : s) ~ (a : s), mid ~ mid),
    (RequireLongerOrSameLength mid n, mid ~ mid, s ~ s,
     (a : b : tail) ~ (a : b : tail), (b : tail) ~ (b : tail))))
forall (a :: Constraint). a => Dict a
Dict

replaceNLorentzConstraint
  :: Sing n -> StackVars' s -> StkEl a -> StackVars' mid -> StackVars' tail
  -> Maybe (Dict (L.ConstraintReplaceNLorentz n s a mid tail))
replaceNLorentzConstraint :: forall (n :: Peano) (s :: [*]) a (mid :: [*]) (tail :: [*]).
Sing n
-> StackVars' s
-> StkEl a
-> StackVars' mid
-> StackVars' tail
-> Maybe (Dict (ConstraintReplaceNLorentz n s a mid tail))
replaceNLorentzConstraint Sing n
n StackVars' s
s StkEl a
a StackVars' mid
mid 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 (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS 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 (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
n) (StackVars' s -> Rec TVal (ToTs s)
forall (stk :: [*]). StackVars' stk -> TValStack (ToTs stk)
toTVals StackVars' s
s))
  Dict
  ((RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
    (ToT a : (LazyTake n (ToTs s) ++ (ToT a : ToTs tail)))
    ~ (ToT a : ToTs s),
    (ToT a : (LazyTake n (ToTs s) ++ ToTs tail)) ~ ToTs mid,
    (ToT a : ToTs tail) ~ Drop n (ToTs s),
    ToTs tail ~ Drop ('S n) (ToTs mid)),
   (RequireLongerOrSameLength (a : s) ('S n),
    (a : (LazyTake n s ++ (a : tail))) ~ (a : s),
    (a : (LazyTake n s ++ tail)) ~ mid, (a : tail) ~ Drop n s,
    tail ~ Drop ('S n) mid),
   SingI ('S n))
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' :: [*]).
Sing n
-> StackVars' inp
-> StackVars' out
-> StackVars' s
-> StackVars' s'
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS 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
  ((RequireLongerThan (ToTs s) n,
    (ToT a : ToTs (LazyTake n s ++ tail))
    ~ (ToT a : (LazyTake n (ToTs s) ++ ToTs tail)),
    ToTs s
    ~ (LazyTake n (ToTs (LazyTake n s ++ tail))
       ++ (ToT a : ToTs tail))),
   (RequireLongerThan s n,
    (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
    s ~ (LazyTake n (LazyTake n s ++ tail) ++ (a : tail))),
   SingI n)
Dict <- Sing n
-> StackVars' mid
-> StackVars' s
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n mid s a))
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
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,
    (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (ToT a : ToTs (LazyTake n s ++ tail))
     ~ (ToT a : ToTs (LazyTake n s ++ tail)),
     (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
    (RequireLongerThan (ToTs s) n,
     (ToT a : ToTs (LazyTake n s ++ tail))
     ~ (ToT a : ToTs (LazyTake n s ++ tail)),
     ToTs s ~ ToTs s)),
   (tail ~ tail,
    (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
     (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
     (a : tail) ~ (a : tail), tail ~ tail),
    (RequireLongerThan s n,
     (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
     s ~ s)))
-> Maybe
     (Dict
        ((ToTs tail ~ ToTs tail,
          (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
           (ToT a : ToTs s) ~ (ToT a : ToTs s),
           (ToT a : ToTs (LazyTake n s ++ tail))
           ~ (ToT a : ToTs (LazyTake n s ++ tail)),
           (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
          (RequireLongerThan (ToTs s) n,
           (ToT a : ToTs (LazyTake n s ++ tail))
           ~ (ToT a : ToTs (LazyTake n s ++ tail)),
           ToTs s ~ ToTs s)),
         (tail ~ tail,
          (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
           (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
           (a : tail) ~ (a : tail), tail ~ tail),
          (RequireLongerThan s n,
           (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
           s ~ s))))
forall (m :: * -> *) a. Monad m => a -> m a
return (Dict
   ((ToTs tail ~ ToTs tail,
     (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
      (ToT a : ToTs s) ~ (ToT a : ToTs s),
      (ToT a : ToTs (LazyTake n s ++ tail))
      ~ (ToT a : ToTs (LazyTake n s ++ tail)),
      (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
     (RequireLongerThan (ToTs s) n,
      (ToT a : ToTs (LazyTake n s ++ tail))
      ~ (ToT a : ToTs (LazyTake n s ++ tail)),
      ToTs s ~ ToTs s)),
    (tail ~ tail,
     (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
      (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
      (a : tail) ~ (a : tail), tail ~ tail),
     (RequireLongerThan s n,
      (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
      s ~ s)))
 -> Maybe
      (Dict
         ((ToTs tail ~ ToTs tail,
           (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
            (ToT a : ToTs s) ~ (ToT a : ToTs s),
            (ToT a : ToTs (LazyTake n s ++ tail))
            ~ (ToT a : ToTs (LazyTake n s ++ tail)),
            (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
           (RequireLongerThan (ToTs s) n,
            (ToT a : ToTs (LazyTake n s ++ tail))
            ~ (ToT a : ToTs (LazyTake n s ++ tail)),
            ToTs s ~ ToTs s)),
          (tail ~ tail,
           (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
            (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
            (a : tail) ~ (a : tail), tail ~ tail),
           (RequireLongerThan s n,
            (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
            s ~ s)))))
-> Dict
     ((ToTs tail ~ ToTs tail,
       (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
        (ToT a : ToTs s) ~ (ToT a : ToTs s),
        (ToT a : ToTs (LazyTake n s ++ tail))
        ~ (ToT a : ToTs (LazyTake n s ++ tail)),
        (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
       (RequireLongerThan (ToTs s) n,
        (ToT a : ToTs (LazyTake n s ++ tail))
        ~ (ToT a : ToTs (LazyTake n s ++ tail)),
        ToTs s ~ ToTs s)),
      (tail ~ tail,
       (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
        (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
        (a : tail) ~ (a : tail), tail ~ tail),
       (RequireLongerThan s n,
        (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
        s ~ s)))
-> Maybe
     (Dict
        ((ToTs tail ~ ToTs tail,
          (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
           (ToT a : ToTs s) ~ (ToT a : ToTs s),
           (ToT a : ToTs (LazyTake n s ++ tail))
           ~ (ToT a : ToTs (LazyTake n s ++ tail)),
           (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
          (RequireLongerThan (ToTs s) n,
           (ToT a : ToTs (LazyTake n s ++ tail))
           ~ (ToT a : ToTs (LazyTake n s ++ tail)),
           ToTs s ~ ToTs s)),
         (tail ~ tail,
          (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
           (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
           (a : tail) ~ (a : tail), tail ~ tail),
          (RequireLongerThan s n,
           (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
           s ~ s))))
forall a b. (a -> b) -> a -> b
$ Dict
  ((ToTs tail ~ ToTs tail,
    (RequireLongerOrSameLength (ToT a : ToTs s) ('S n),
     (ToT a : ToTs s) ~ (ToT a : ToTs s),
     (ToT a : ToTs (LazyTake n s ++ tail))
     ~ (ToT a : ToTs (LazyTake n s ++ tail)),
     (ToT a : ToTs tail) ~ (ToT a : ToTs tail), ToTs tail ~ ToTs tail),
    (RequireLongerThan (ToTs s) n,
     (ToT a : ToTs (LazyTake n s ++ tail))
     ~ (ToT a : ToTs (LazyTake n s ++ tail)),
     ToTs s ~ ToTs s)),
   (tail ~ tail,
    (RequireLongerOrSameLength (a : s) ('S n), (a : s) ~ (a : s),
     (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
     (a : tail) ~ (a : tail), tail ~ tail),
    (RequireLongerThan s n,
     (a : (LazyTake n s ++ tail)) ~ (a : (LazyTake n s ++ tail)),
     s ~ s)))
forall (a :: Constraint). a => Dict a
Dict

dugLorentzConstraint
  :: Sing n -> StackVars' inp -> StackVars' out -> StkEl a
  -> Maybe (Dict (L.ConstraintDUGLorentz n inp out a))
dugLorentzConstraint :: forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
Sing n
-> StackVars' inp
-> StackVars' out
-> StkEl a
-> Maybe (Dict (ConstraintDUGLorentz n inp out a))
dugLorentzConstraint Sing n
n StackVars' inp
inp StackVars' out
out StkEl a
a = do
  Dict
  (RequireLongerThan out n,
   inp ~ (a : (LazyTake n out ++ Drop ('S n) out)),
   out ~ (LazyTake n (Drop ('S 'Z) inp) ++ (a : Drop ('S n) inp)))
Dict <- Sing n
-> StackVars' inp
-> StackVars' out
-> StkEl a
-> Maybe
     (Dict
        (RequireLongerThan out n,
         inp ~ (a : (LazyTake n out ++ Drop ('S n) out)),
         out ~ (LazyTake n (Drop ('S 'Z) inp) ++ (a : Drop ('S n) inp))))
forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (a :: kind).
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
  (RequireLongerThan (ToTs out) n,
   (ToT a : ToTs (LazyTake n out ++ Drop ('S n) out))
   ~ (ToT a : (LazyTake n (ToTs out) ++ Drop ('S n) (ToTs out))),
   ToTs out
   ~ (LazyTake n (ToTs (LazyTake n out ++ Drop ('S n) out))
      ++ (ToT a : Drop n (ToTs (LazyTake n out ++ Drop ('S n) out)))))
Dict <- Sing n
-> Rec TVal (ToT a : ToTs (LazyTake n out ++ Drop ('S n) out))
-> Rec TVal (ToTs out)
-> TVal (ToT a)
-> Maybe
     (Dict
        (ConstraintDUG'
           T
           n
           (ToT a : ToTs (LazyTake n out ++ Drop ('S n) out))
           (ToTs out)
           (ToT a)))
forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (a :: kind).
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 (ConstraintDUGLorentz n inp out a)
-> Maybe (Dict (ConstraintDUGLorentz n inp out a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Dict (ConstraintDUGLorentz n inp out a)
 -> Maybe (Dict (ConstraintDUGLorentz n inp out a)))
-> Dict (ConstraintDUGLorentz n inp out a)
-> Maybe (Dict (ConstraintDUGLorentz n inp out a))
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => Dict (ConstraintDUGLorentz n inp out a))
-> Dict (ConstraintDUGLorentz n inp out a)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
n ((SingI n => Dict (ConstraintDUGLorentz n inp out a))
 -> Dict (ConstraintDUGLorentz n inp out a))
-> (SingI n => Dict (ConstraintDUGLorentz n inp out a))
-> Dict (ConstraintDUGLorentz n inp out a)
forall a b. (a -> b) -> a -> b
$ SingI n => Dict (ConstraintDUGLorentz n inp out a)
forall (a :: Constraint). a => Dict a
Dict

dipNLorentzConstraint
  :: Sing n -> StackVars' inp -> StackVars' out -> StackVars' s -> StackVars' s'
  -> Maybe (Dict (L.ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint :: forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
Sing n
-> StackVars' inp
-> StackVars' out
-> StackVars' s
-> StackVars' s'
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
dipNLorentzConstraint Sing n
n StackVars' inp
inp StackVars' out
out StackVars' s
s StackVars' s'
s' = do
  Dict
  (RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ inp,
   (LazyTake n inp ++ s') ~ out, s ~ Drop n inp, s' ~ Drop n out)
Dict <- Sing n
-> StackVars' inp
-> StackVars' out
-> StackVars' s
-> StackVars' s'
-> Maybe
     (Dict
        (RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ inp,
         (LazyTake n inp ++ s') ~ out, s ~ Drop n inp, s' ~ Drop n out))
forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (s :: [kind]) (s' :: [kind]).
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
  (RequireLongerOrSameLength (ToTs inp) n,
   (LazyTake n (ToTs inp) ++ ToTs s) ~ ToTs inp,
   (LazyTake n (ToTs inp) ++ ToTs s') ~ ToTs out,
   ToTs s ~ Drop n (ToTs inp), ToTs s' ~ Drop n (ToTs out))
Dict <- Sing n
-> Rec TVal (ToTs inp)
-> Rec TVal (ToTs out)
-> Rec TVal (ToTs s)
-> Rec TVal (ToTs s')
-> Maybe
     (Dict
        (RequireLongerOrSameLength (ToTs inp) n,
         (LazyTake n (ToTs inp) ++ ToTs s) ~ ToTs inp,
         (LazyTake n (ToTs inp) ++ ToTs s') ~ ToTs out,
         ToTs s ~ Drop n (ToTs inp), ToTs s' ~ Drop n (ToTs out)))
forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (s :: [kind]) (s' :: [kind]).
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 (ConstraintDIPNLorentz n inp out s s')
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
forall (m :: * -> *) a. Monad m => a -> m a
return (Dict (ConstraintDIPNLorentz n inp out s s')
 -> Maybe (Dict (ConstraintDIPNLorentz n inp out s s')))
-> Dict (ConstraintDIPNLorentz n inp out s s')
-> Maybe (Dict (ConstraintDIPNLorentz n inp out s s'))
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => Dict (ConstraintDIPNLorentz n inp out s s'))
-> Dict (ConstraintDIPNLorentz n inp out s s')
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
n ((SingI n => Dict (ConstraintDIPNLorentz n inp out s s'))
 -> Dict (ConstraintDIPNLorentz n inp out s s'))
-> (SingI n => Dict (ConstraintDIPNLorentz n inp out s s'))
-> Dict (ConstraintDIPNLorentz n inp out s s')
forall a b. (a -> b) -> a -> b
$ SingI n => Dict (ConstraintDIPNLorentz n inp out s s')
forall (a :: Constraint). a => Dict a
Dict

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

dupNConstraint
  :: TestEquality any
  => Sing n -> Rec any inp -> Rec any out -> any a
  -> Maybe (Dict (MI.ConstraintDUPN' kind n inp out a))
dupNConstraint :: forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (a :: kind).
TestEquality any =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUPN' kind n inp out a))
dupNConstraint Sing n
n Rec any inp
inp Rec any out
out any a
a = 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
  Dict ((n > 'Z) ~ 'True)
Dict <- Sing n -> Sing 'Z -> Maybe (Dict ((n > 'Z) ~ 'True))
forall (a :: Peano) (b :: Peano).
Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing n
n Sing 'Z
SingNat 'Z
SZ
  SingNat (Decrement n)
decN <- Sing n -> Maybe (Sing (Decrement n))
forall (n :: Peano). Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement Sing n
n
  inp :~: (LazyTake (Decrement n) inp ++ (a : Drop n inp))
Refl <- Rec any inp
-> Rec any (LazyTake (Decrement n) inp ++ (a : Drop n inp))
-> Maybe (inp :~: (LazyTake (Decrement n) inp ++ (a : Drop 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 (Decrement n)
-> Rec any inp -> Rec any (LazyTake (Decrement n) inp)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (LazyTake n s)
lazyRtake Sing (Decrement n)
SingNat (Decrement n)
decN Rec any inp
inp) Rec any (LazyTake (Decrement n) inp)
-> Rec any (a : Drop n inp)
-> Rec any (LazyTake (Decrement n) inp ++ (a : Drop 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 n inp) -> Rec any (a : Drop 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 (Drop n inp)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n Rec any inp
inp)
  out :~: (a : inp)
Refl <- Rec any out -> Rec any (a : inp) -> Maybe (out :~: (a : 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 inp -> Rec any (a : inp)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec any inp
inp)
  Dict
  (RequireLongerOrSameLength inp n, 'True ~ 'True, inp ~ inp,
   (a : inp) ~ (a : inp))
-> Maybe
     (Dict
        (RequireLongerOrSameLength inp n, 'True ~ 'True, inp ~ inp,
         (a : inp) ~ (a : inp)))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  (RequireLongerOrSameLength inp n, 'True ~ 'True, inp ~ inp,
   (a : inp) ~ (a : inp))
forall (a :: Constraint). a => Dict a
Dict

dugConstraint
  :: TestEquality any
  => Sing n -> Rec any inp -> Rec any out -> any a
  -> Maybe (Dict (MI.ConstraintDUG' kind n inp out a))
dugConstraint :: forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (a :: kind).
TestEquality any =>
Sing n
-> Rec any inp
-> Rec any out
-> any a
-> Maybe (Dict (ConstraintDUG' kind n inp out a))
dugConstraint Sing n
n Rec any inp
inp Rec any out
out 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 (Sing 'Z -> SingNat ('S 'Z)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing 'Z
SingNat 'Z
SZ) Rec any inp
inp) Rec any inp
inp
  (LazyTake n out ++ Drop ('S n) out) :~: Drop ('S 'Z) inp
Refl <- Rec any (LazyTake n out ++ Drop ('S n) out)
-> Rec any (Drop ('S 'Z) inp)
-> Maybe ((LazyTake n out ++ Drop ('S n) out) :~: Drop ('S 'Z) inp)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Sing n -> Rec any out -> Rec any (LazyTake n out)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (LazyTake n s)
lazyRtake Sing n
n Rec any out
out Rec any (LazyTake n out)
-> Rec any (Drop ('S n) out)
-> Rec any (LazyTake n out ++ Drop ('S n) out)
forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Sing ('S n) -> Rec any out -> Rec any (Drop ('S n) out)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
n) Rec any out
out) (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 (Sing 'Z -> SingNat ('S 'Z)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing 'Z
SingNat 'Z
SZ) Rec any inp
inp)
  (LazyTake n (Drop ('S 'Z) inp) ++ (a : Drop n (Drop ('S 'Z) inp)))
:~: out
Refl <- Rec
  any
  (LazyTake n (Drop ('S 'Z) inp) ++ (a : Drop n (Drop ('S 'Z) inp)))
-> Rec any out
-> Maybe
     ((LazyTake 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 (LazyTake n (Drop ('S 'Z) inp))
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (LazyTake n s)
lazyRtake 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 (Sing 'Z -> SingNat ('S 'Z)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing 'Z
SingNat 'Z
SZ) Rec any inp
inp) Rec any (LazyTake n (Drop ('S 'Z) inp))
-> Rec any (a : Drop n (Drop ('S 'Z) inp))
-> Rec
     any
     (LazyTake 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 n
-> Rec any (Drop ('S 'Z) inp)
-> Rec any (Drop n (Drop ('S 'Z) inp))
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop 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 (Sing 'Z -> SingNat ('S 'Z)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing 'Z
SingNat 'Z
SZ) Rec any inp
inp)) Rec any out
out
  Dict
  (RequireLongerThan out n,
   (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out)
-> Maybe
     (Dict
        (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
  (RequireLongerThan out n,
   (a : Drop ('S 'Z) inp) ~ (a : Drop ('S 'Z) inp), out ~ out)
forall (a :: Constraint). a => Dict a
Dict

dipNConstraint
  :: 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 :: forall kind (any :: kind -> *) (n :: Peano) (inp :: [kind])
       (out :: [kind]) (s :: [kind]) (s' :: [kind]).
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 Rec any inp
inp Rec any out
out Rec any 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
  (LazyTake n inp ++ s) :~: inp
Refl <- Rec any (LazyTake n inp ++ s)
-> Rec any inp -> Maybe ((LazyTake 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 (LazyTake n inp)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (LazyTake n s)
lazyRtake Sing n
n Rec any inp
inp Rec any (LazyTake n inp)
-> Rec any s -> Rec any (LazyTake 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
  (LazyTake n inp ++ s') :~: out
Refl <- Rec any (LazyTake n inp ++ s')
-> Rec any out -> Maybe ((LazyTake 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 (LazyTake n inp)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (LazyTake n s)
lazyRtake Sing n
n Rec any inp
inp Rec any (LazyTake n inp)
-> Rec any s' -> Rec any (LazyTake 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
  Drop n inp :~: s
Refl <- Rec any (Drop n inp) -> Rec any s -> Maybe (Drop n inp :~: s)
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 (Drop n inp)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n Rec any inp
inp) Rec any s
s
  Drop n out :~: s'
Refl <- Rec any (Drop n out) -> Rec any s' -> Maybe (Drop n out :~: s')
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Sing n -> Rec any out -> Rec any (Drop n out)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Drop n s)
rdrop Sing n
n Rec any out
out) Rec any s'
s'
  Dict
  (RequireLongerOrSameLength inp n, inp ~ inp, out ~ out, s ~ s,
   s' ~ s')
-> Maybe
     (Dict
        (RequireLongerOrSameLength inp n, inp ~ inp, out ~ out, s ~ s,
         s' ~ s'))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict
  (RequireLongerOrSameLength inp n, inp ~ inp, out ~ out, s ~ s,
   s' ~ s')
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 'SingI' constraint
data TVal (a :: MI.T) where
  TVal :: SingI a => TVal a

instance TestEquality TVal where
  testEquality :: forall (a :: T) (b :: T). TVal a -> TVal b -> Maybe (a :~: b)
testEquality (TVal a
TVal :: TVal a) (TVal b
TVal :: TVal b) = forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall (a :: T) (b :: T).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @a @b

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

toTVals :: StackVars' stk -> TValStack (ToTs stk)
toTVals :: forall (stk :: [*]). StackVars' stk -> TValStack (ToTs stk)
toTVals = \case
  StackVars' stk
RNil          -> TValStack (ToTs stk)
forall {u} (a :: u -> *). Rec a '[]
RNil
  (StkEl r
NoRef :& Rec StkEl rs
xs) -> TVal (ToT r)
forall (a :: T). SingI 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 RefId
_ :& Rec StkEl rs
xs) -> TVal (ToT r)
forall (a :: T). SingI 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 :: forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
sn Rec any s
stk = case (Sing n
SingNat n
sn, Rec any s
stk) of
  (SingNat n
SZ, Rec any s
_)           -> Rec any (Take n s)
forall {u} (a :: u -> *). Rec a '[]
RNil
  (SS Sing n
n, (any r
x :& Rec any rs
xs)) -> any r
x any r -> Rec any (Take n rs) -> Rec any (r : Take n rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n -> Rec any rs -> Rec any (Take n rs)
forall {k} (n :: Peano) (any :: k -> *) (s :: [k]).
Sing n -> Rec any s -> Rec any (Take n s)
rtake Sing n
n Rec any rs
xs
  (SS Sing n
_, Rec any s
RNil)      -> Text -> Rec any '[]
forall a. HasCallStack => Text -> a
error Text
"given stack is too small"

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

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