module Indigo.Backend.Lookup
(
varActionGet
, varActionSet
, varActionUpdate
, varActionOperation
, 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
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
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)
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
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
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
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
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
constraintFailure :: Text
constraintFailure = Text
"Unexpected failure in Var's constraint checking"
data VarDepth where
VarDepth :: Sing (idx :: Peano) -> VarDepth
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)
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
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
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
type TValStack (stk :: [MI.T]) = Rec TVal stk
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
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"