{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
module Cubix.Language.Lua.Parametric.Common.Semantics () where
import Data.Type.Equality ( (:~:)(..), gcastWith )
import Data.Comp.Multi ( (:-<:), project, inject')
import Data.Comp.Multi.Strategy.Classification ( KDynCase(..), kIsSort )
import Cubix.Language.Lua.Parametric.Common.Types
import Cubix.Language.Lua.Parametric.Full
import Cubix.Language.Parametric.Semantics.SemanticProperties
import Cubix.Language.Parametric.Syntax
import Cubix.Sin.Compdata.Annotation ( annM )
instance {-# OVERLAPPING #-} (Binop :-<: gs) => GetStrictness' gs Exp where
getStrictness' :: forall l. Exp (Term gs) l -> [Strictness]
getStrictness' t :: Exp (Term gs) l
t@(Binop Term gs BinopL
op Term gs ExpL
_ Term gs ExpL
_) = case Term gs BinopL
op of
Term gs BinopL
And' -> [Strictness
NoEval, Strictness
Strict, Place -> Strictness
GuardedBy (Int -> Place
Place Int
1)]
Term gs BinopL
Or' -> [Strictness
NoEval, Strictness
Strict, Place -> Strictness
GuardedBy (Int -> Place
NegPlace Int
1)]
Term gs BinopL
_ -> Exp (Term gs) l -> [Strictness]
forall (f :: (* -> *) -> * -> *) (e :: * -> *) l.
HFoldable f =>
f e l -> [Strictness]
defaultGetStrictness Exp (Term gs) l
t
getStrictness' Exp (Term gs) l
x = Exp (Term gs) l -> [Strictness]
forall (f :: (* -> *) -> * -> *) (e :: * -> *) l.
HFoldable f =>
f e l -> [Strictness]
defaultGetStrictness Exp (Term gs) l
x
instance {-# OVERLAPPING #-} InsertAt' MLuaSig BlockItemL ListF where
insertAt' :: forall a (m :: * -> *) i.
MonadAnnotater a m =>
NodeEvaluationPoint
-> AnnTerm a MLuaSig BlockItemL
-> (:&:) ListF a (AnnTerm a MLuaSig) i
-> m (AnnTerm a MLuaSig i)
insertAt' NodeEvaluationPoint
EnterEvalPoint AnnTerm a MLuaSig BlockItemL
e (:&:) ListF a (AnnTerm a MLuaSig) i
t = case (:&:) ListF a (AnnTerm a MLuaSig) i -> Maybe (i :~: [BlockItemL])
forall (e :: * -> *) b.
(:&:) ListF a e b -> Maybe (b :~: [BlockItemL])
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase (:&:) ListF a (AnnTerm a MLuaSig) i
t :: Maybe (_ :~: [BlockItemL]) of
Maybe (i :~: [BlockItemL])
Nothing -> AnnTerm a MLuaSig i -> m (AnnTerm a MLuaSig i)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnTerm a MLuaSig i -> m (AnnTerm a MLuaSig i))
-> AnnTerm a MLuaSig i -> m (AnnTerm a MLuaSig i)
forall a b. (a -> b) -> a -> b
$ (:&:) ListF a (AnnTerm a MLuaSig) i -> AnnTerm a MLuaSig i
(:&:) ListF a (AnnTerm a MLuaSig) :-> AnnTerm a MLuaSig
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
(a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' (:&:) ListF a (AnnTerm a MLuaSig) i
t
Just i :~: [BlockItemL]
p -> (i :~: [BlockItemL])
-> ((i ~ [BlockItemL]) => m (AnnTerm a MLuaSig i))
-> m (AnnTerm a MLuaSig i)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith i :~: [BlockItemL]
p (((i ~ [BlockItemL]) => m (AnnTerm a MLuaSig i))
-> m (AnnTerm a MLuaSig i))
-> ((i ~ [BlockItemL]) => m (AnnTerm a MLuaSig i))
-> m (AnnTerm a MLuaSig i)
forall a b. (a -> b) -> a -> b
$ (:&:) ListF a (AnnTerm a MLuaSig) i -> AnnTerm a MLuaSig i
(:&:) ListF a (AnnTerm a MLuaSig) :-> AnnTerm a MLuaSig
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
(a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' ((:&:) ListF a (AnnTerm a MLuaSig) i -> AnnTerm a MLuaSig i)
-> m ((:&:) ListF a (AnnTerm a MLuaSig) i)
-> m (AnnTerm a MLuaSig i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ListF (AnnTerm a MLuaSig) i
-> m ((:&:) ListF a (AnnTerm a MLuaSig) i)
forall a (m :: * -> *) (f :: (* -> *) -> * -> *) (e :: * -> *) l.
MonadAnnotater a m =>
f e l -> m ((:&:) f a e l)
forall (f :: (* -> *) -> * -> *) (e :: * -> *) l.
f e l -> m ((:&:) f a e l)
annM (AnnTerm a MLuaSig BlockItemL
-> Cxt NoHole (Sum MLuaSig :&: a) (K ()) [BlockItemL]
-> ListF (AnnTerm a MLuaSig) [BlockItemL]
forall l1 (e :: * -> *).
Typeable l1 =>
e l1 -> e [l1] -> ListF e [l1]
ConsF AnnTerm a MLuaSig BlockItemL
e ((:&:) ListF a (AnnTerm a MLuaSig) [BlockItemL]
-> Cxt NoHole (Sum MLuaSig :&: a) (K ()) [BlockItemL]
(:&:) ListF a (AnnTerm a MLuaSig) :-> AnnTerm a MLuaSig
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
(a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' (:&:) ListF a (AnnTerm a MLuaSig) i
(:&:) ListF a (AnnTerm a MLuaSig) [BlockItemL]
t))
insertAt' NodeEvaluationPoint
_ AnnTerm a MLuaSig BlockItemL
_ (:&:) ListF a (AnnTerm a MLuaSig) i
t = AnnTerm a MLuaSig i -> m (AnnTerm a MLuaSig i)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnTerm a MLuaSig i -> m (AnnTerm a MLuaSig i))
-> AnnTerm a MLuaSig i -> m (AnnTerm a MLuaSig i)
forall a b. (a -> b) -> a -> b
$ (:&:) ListF a (AnnTerm a MLuaSig) i -> AnnTerm a MLuaSig i
(:&:) ListF a (AnnTerm a MLuaSig) :-> AnnTerm a MLuaSig
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
(a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' (:&:) ListF a (AnnTerm a MLuaSig) i
t
canInsertAt' :: forall a i.
NodeEvaluationPoint
-> Proxy BlockItemL -> (:&:) ListF a (AnnTerm a MLuaSig) i -> Bool
canInsertAt' NodeEvaluationPoint
EnterEvalPoint Proxy BlockItemL
_ = forall l (f :: (* -> *) -> * -> *) i (e :: * -> *).
KDynCase f l =>
f e i -> Bool
kIsSort @[BlockItemL]
canInsertAt' NodeEvaluationPoint
_ Proxy BlockItemL
_ = Bool -> (:&:) ListF a (AnnTerm a MLuaSig) i -> Bool
forall a b. a -> b -> a
const Bool
False