{-# LANGUAGE FunctionalDependencies #-}
module Lorentz.ReferencedByName
(
HasNamedVar
, HasNamedVars
, (:=)
, dupL
, dupLNamed
, VarIsUnnamed
) where
import Data.Constraint (Bottom(..))
import Data.Singletons (Sing)
import Fcf qualified
import Type.Errors (DelayError, IfStuck)
import Lorentz.ADT
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Instr
import Morley.Michelson.Text
import Morley.Util.Label
import Morley.Util.Named
import Morley.Util.Peano
import Morley.Util.Type
import Morley.Util.TypeLits
type StackElemNotFound :: Symbol -> k
type StackElemNotFound name = DelayError
('Text "Element with name " ':<>: 'ShowType name ':<>: 'Text " is not present on stack")
data NamedVariableNotFound name
data VarNamed = VarNamed Symbol | VarUnnamed
type VarName :: Type -> VarNamed
type family VarName (a :: Type) :: VarNamed where
VarName (NamedF _ _ name) = 'VarNamed name
VarName _ = 'VarUnnamed
type VarNamePretty :: Type -> VarNamed
type VarNamePretty x =
IfStuck (VarName x)
(DelayError
('Text "Not clear which name `" ':<>: 'ShowType x ':<>: 'Text "` variable has" ':$$:
'Text "Consider adding `VarIsUnnamed " ':<>: 'ShowType x ':<>: 'Text "` constraint" ':$$:
'Text "or carrying a named variable instead"
)
)
(Fcf.Pure (VarName x))
type VarIsUnnamed x = VarName x ~ 'VarUnnamed
type HasNamedVar :: [Type] -> Symbol -> Type -> Constraint
class HasNamedVar s name var | s name -> var where
varPosition :: VarPosition s name var
type VarPosition :: [Type] -> Symbol -> Type -> Type
data VarPosition s name var where
VarPosition
:: (x ~ name :! var, ConstraintDUPNLorentz ('S n) s (x : s) x)
=> Sing (n :: Peano) -> VarPosition s name var
instance (Bottom, StackElemNotFound name, var ~ NamedVariableNotFound name)
=> HasNamedVar '[] name var where
varPosition :: VarPosition '[] name var
varPosition = VarPosition '[] name var
forall a. Bottom => a
no
instance ElemHasNamedVar (ty : s) name var (VarNamePretty ty == 'VarNamed name)
=> HasNamedVar (ty : s) name var where
varPosition :: VarPosition (ty : s) name var
varPosition = forall (s :: [*]) (name :: Symbol) var (nameMatch :: Bool).
ElemHasNamedVar s name var nameMatch =>
VarPosition s name var
elemVarPosition @(ty : s) @name @var @(VarNamePretty ty == 'VarNamed name)
type ElemHasNamedVar :: [Type] -> Symbol -> Type -> Bool -> Constraint
class ElemHasNamedVar s name var nameMatch | s name nameMatch -> var where
elemVarPosition :: VarPosition s name var
instance ty ~ (name :! var) => ElemHasNamedVar (ty : s) name var 'True where
elemVarPosition :: VarPosition (ty : s) name var
elemVarPosition = Sing 'Z -> VarPosition (ty : s) name var
forall x (name :: Symbol) var (n :: Peano) (s :: [*]).
(x ~ (name :! var), ConstraintDUPNLorentz ('S n) s (x : s) x) =>
Sing n -> VarPosition s name var
VarPosition Sing 'Z
SingNat 'Z
SZ
instance HasNamedVar s name var => ElemHasNamedVar (ty : s) name var 'False where
elemVarPosition :: VarPosition (ty : s) name var
elemVarPosition = case forall (s :: [*]) (name :: Symbol) var.
HasNamedVar s name var =>
VarPosition s name var
varPosition @s @name @var of
VarPosition Sing n
n -> Sing ('S n) -> VarPosition (ty : s) name var
forall x (name :: Symbol) var (n :: Peano) (s :: [*]).
(x ~ (name :! var), ConstraintDUPNLorentz ('S n) s (x : s) x) =>
Sing n -> VarPosition s name var
VarPosition (Sing ('S n) -> VarPosition (ty : s) name var)
-> Sing ('S n) -> VarPosition (ty : s) name var
forall a b. (a -> b) -> a -> b
$ Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
n
type HasNamedVars :: [Type] -> [NamedField] -> Constraint
type family HasNamedVars s vs where
HasNamedVars _ '[] = ()
HasNamedVars s ((n := ty) ': vs) = (HasNamedVar s n ty, HasNamedVars s vs)
dupLNamed
:: forall var name s.
(HasNamedVar s name var, Dupable var)
=> Label name -> s :-> (name :! var) : s
dupLNamed :: forall var (name :: Symbol) (s :: [*]).
(HasNamedVar s name var, Dupable var) =>
Label name -> s :-> ((name :! var) : s)
dupLNamed Label{} =
case forall (s :: [*]) (name :: Symbol) var.
HasNamedVar s name var =>
VarPosition s name var
varPosition @s @name @var of
VarPosition (Sing n
_ :: Sing n) -> forall (n :: Peano) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz n inp out a, Dupable a) =>
inp :-> out
dupNPeano @('S n)
dupL :: forall var name s.
(HasNamedVar s name var, Dupable var)
=> Label name -> s :-> var : s
dupL :: forall var (name :: Symbol) (s :: [*]).
(HasNamedVar s name var, Dupable var) =>
Label name -> s :-> (var : s)
dupL Label name
l = Label name -> s :-> ((name :! var) : s)
forall var (name :: Symbol) (s :: [*]).
(HasNamedVar s name var, Dupable var) =>
Label name -> s :-> ((name :! var) : s)
dupLNamed Label name
l (s :-> ((name :! var) : s))
-> (((name :! var) : s) :-> (var : s)) -> s :-> (var : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name -> ((name :! var) : s) :-> (var : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label name
l
_dupSample1
:: [Integer, Natural, "a" :! (), "b" :! MText, "c" :! ByteString]
:-> [MText, Integer, Natural, "a" :! (), "b" :! MText, "c" :! ByteString]
_dupSample1 :: '[Integer, Natural, "a" :! (), "b" :! MText, "c" :! ByteString]
:-> '[MText, Integer, Natural, "a" :! (), "b" :! MText,
"c" :! ByteString]
_dupSample1 =
Label "b"
-> '[Integer, Natural, "a" :! (), "b" :! MText, "c" :! ByteString]
:-> '[MText, Integer, Natural, "a" :! (), "b" :! MText,
"c" :! ByteString]
forall var (name :: Symbol) (s :: [*]).
(HasNamedVar s name var, Dupable var) =>
Label name -> s :-> (var : s)
dupL IsLabel "b" (Label "b")
Label "b"
#b
_dupSample2
:: (HasNamedVar s "x" Natural)
=> (Integer : s)
:-> (Natural : Integer : s)
_dupSample2 :: forall (s :: [*]).
HasNamedVar s "x" Natural =>
(Integer : s) :-> (Natural : Integer : s)
_dupSample2 =
Label "x" -> (Integer : s) :-> (Natural : Integer : s)
forall var (name :: Symbol) (s :: [*]).
(HasNamedVar s name var, Dupable var) =>
Label name -> s :-> (var : s)
dupL IsLabel "x" (Label "x")
Label "x"
#x
_dupSample3
:: (HasNamedVar s "x" Natural, VarIsUnnamed store)
=> (store : s)
:-> (Natural : store : s)
_dupSample3 :: forall (s :: [*]) store.
(HasNamedVar s "x" Natural, VarIsUnnamed store) =>
(store : s) :-> (Natural : store : s)
_dupSample3 =
Label "x" -> (store : s) :-> (Natural : store : s)
forall var (name :: Symbol) (s :: [*]).
(HasNamedVar s name var, Dupable var) =>
Label name -> s :-> (var : s)
dupL IsLabel "x" (Label "x")
Label "x"
#x