{-# LANGUAGE DeriveAnyClass         #-}
{-# LANGUAGE DeriveGeneric          #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PartialTypeSignatures  #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

module Cubix.Language.Parametric.Semantics.SemanticProperties (
    Place(..)
  , Strictness(..)
  , GetStrictness'(..)
  , GetStrictness(..)
  , defaultGetStrictness

  , NodeEvaluationPoint(..)
  , InsertAt'(..)
  , InsertAt(..)
  , insertBefore
  , canInsertBefore
  ) where

import Control.DeepSeq ( NFData )
import Control.Monad ( liftM )

import Data.Proxy ( Proxy(..) )
import Data.Type.Equality ( (:~:)(..), gcastWith )
import Data.Typeable ( Typeable )

import GHC.Generics ( Generic )

import Data.Comp.Multi ( unTerm, (:&:)(..), caseCxt, HFunctor, HFoldable, htoList, inject', All, Sum, caseCxt', AnnTerm, Term, (:-<:) )
import Data.Comp.Multi.Strategy.Classification ( DynCase(..), KDynCase(..), kIsSort )

import Cubix.Language.Parametric.Syntax.Functor

import Cubix.Sin.Compdata.Annotation ( MonadAnnotater(..) )

--------------------------------------------O------------------------------------------

-- Need something for locations

data Place = Place Int | NegPlace Int
data Strictness = Strict | GuardedBy Place | NoEval

-- Need better place for this
data Kleene = KTrue | KUnknown | KFalse
  deriving (Kleene -> Kleene -> Bool
(Kleene -> Kleene -> Bool)
-> (Kleene -> Kleene -> Bool) -> Eq Kleene
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kleene -> Kleene -> Bool
$c/= :: Kleene -> Kleene -> Bool
== :: Kleene -> Kleene -> Bool
$c== :: Kleene -> Kleene -> Bool
Eq, Eq Kleene
Eq Kleene =>
(Kleene -> Kleene -> Ordering)
-> (Kleene -> Kleene -> Bool)
-> (Kleene -> Kleene -> Bool)
-> (Kleene -> Kleene -> Bool)
-> (Kleene -> Kleene -> Bool)
-> (Kleene -> Kleene -> Kleene)
-> (Kleene -> Kleene -> Kleene)
-> Ord Kleene
Kleene -> Kleene -> Bool
Kleene -> Kleene -> Ordering
Kleene -> Kleene -> Kleene
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Kleene -> Kleene -> Kleene
$cmin :: Kleene -> Kleene -> Kleene
max :: Kleene -> Kleene -> Kleene
$cmax :: Kleene -> Kleene -> Kleene
>= :: Kleene -> Kleene -> Bool
$c>= :: Kleene -> Kleene -> Bool
> :: Kleene -> Kleene -> Bool
$c> :: Kleene -> Kleene -> Bool
<= :: Kleene -> Kleene -> Bool
$c<= :: Kleene -> Kleene -> Bool
< :: Kleene -> Kleene -> Bool
$c< :: Kleene -> Kleene -> Bool
compare :: Kleene -> Kleene -> Ordering
$ccompare :: Kleene -> Kleene -> Ordering
$cp1Ord :: Eq Kleene
Ord, Int -> Kleene -> ShowS
[Kleene] -> ShowS
Kleene -> String
(Int -> Kleene -> ShowS)
-> (Kleene -> String) -> ([Kleene] -> ShowS) -> Show Kleene
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Kleene] -> ShowS
$cshowList :: [Kleene] -> ShowS
show :: Kleene -> String
$cshow :: Kleene -> String
showsPrec :: Int -> Kleene -> ShowS
$cshowsPrec :: Int -> Kleene -> ShowS
Show)


class GetStrictness' gs f where
  getStrictness' :: f (Term gs) l -> [Strictness]

defaultGetStrictness :: (HFoldable f) => f e l -> [Strictness]
defaultGetStrictness :: f e l -> [Strictness]
defaultGetStrictness t :: f e l
t = Int -> [Strictness] -> [Strictness]
forall a. Int -> [a] -> [a]
take ([E e] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (f e l -> [E e]
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFoldable f =>
f a :=> [E a]
htoList f e l
t)) (Strictness -> [Strictness]
forall a. a -> [a]
repeat Strictness
Strict)

instance {-# OVERLAPPABLE #-} (HFoldable f) => GetStrictness' gs f where
  getStrictness' :: f (Term gs) l -> [Strictness]
getStrictness' = f (Term gs) l -> [Strictness]
forall (f :: (* -> *) -> * -> *) (e :: * -> *) l.
HFoldable f =>
f e l -> [Strictness]
defaultGetStrictness

instance {-# OVERLAPPING #-} (All (GetStrictness' gs) fs) => GetStrictness' gs (Sum fs) where
  getStrictness' :: Sum fs (Term gs) l -> [Strictness]
getStrictness' = Proxy (GetStrictness' gs)
-> (forall (f :: (* -> *) -> * -> *).
    GetStrictness' gs f =>
    f (Term gs) l -> [Strictness])
-> Sum fs (Term gs) l
-> [Strictness]
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (GetStrictness' gs)
forall k (t :: k). Proxy t
Proxy @(GetStrictness' gs)) forall (gs :: [(* -> *) -> * -> *]) (f :: (* -> *) -> * -> *) l.
GetStrictness' gs f =>
f (Term gs) l -> [Strictness]
forall (f :: (* -> *) -> * -> *).
GetStrictness' gs f =>
f (Term gs) l -> [Strictness]
getStrictness'

class GetStrictness fs where
  getStrictness :: Term fs l -> [Strictness]

instance (GetStrictness' fs (Sum fs)) => GetStrictness fs where
  getStrictness :: Term fs l -> [Strictness]
getStrictness = Sum fs (Term fs) l -> [Strictness]
forall (gs :: [(* -> *) -> * -> *]) (f :: (* -> *) -> * -> *) l.
GetStrictness' gs f =>
f (Term gs) l -> [Strictness]
getStrictness' (Sum fs (Term fs) l -> [Strictness])
-> (Term fs l -> Sum fs (Term fs) l) -> Term fs l -> [Strictness]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term fs l -> Sum fs (Term fs) l
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm

--------------------------------------------------------------------------------------

class HasSideEffects' gs f where
  hasSideEffects' :: f (Term gs) l -> Kleene

instance {-# OVERLAPPABLE #-} HasSideEffects' gs f where
  hasSideEffects' :: f (Term gs) l -> Kleene
hasSideEffects' = Kleene -> f (Term gs) l -> Kleene
forall a b. a -> b -> a
const Kleene
KUnknown

instance {-# OVERLAPPING #-} (All (HasSideEffects' gs) fs) => HasSideEffects' gs (Sum fs) where
  hasSideEffects' :: Sum fs (Term gs) l -> Kleene
hasSideEffects' = Proxy (HasSideEffects' gs)
-> (forall (f :: (* -> *) -> * -> *).
    HasSideEffects' gs f =>
    f (Term gs) l -> Kleene)
-> Sum fs (Term gs) l
-> Kleene
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (HasSideEffects' gs)
forall k (t :: k). Proxy t
Proxy @(HasSideEffects' gs)) forall (gs :: [(* -> *) -> * -> *]) (f :: (* -> *) -> * -> *) l.
HasSideEffects' gs f =>
f (Term gs) l -> Kleene
forall (f :: (* -> *) -> * -> *).
HasSideEffects' gs f =>
f (Term gs) l -> Kleene
hasSideEffects'

class HasSideEffects fs where
  hasSideEffects :: Term fs l -> Kleene

instance (HasSideEffects' fs (Sum fs)) => HasSideEffects fs where
  hasSideEffects :: Term fs l -> Kleene
hasSideEffects = Sum fs (Term fs) l -> Kleene
forall (gs :: [(* -> *) -> * -> *]) (f :: (* -> *) -> * -> *) l.
HasSideEffects' gs f =>
f (Term gs) l -> Kleene
hasSideEffects' (Sum fs (Term fs) l -> Kleene)
-> (Term fs l -> Sum fs (Term fs) l) -> Term fs l -> Kleene
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term fs l -> Sum fs (Term fs) l
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm


--------------------------------------------------------------------------------------


-- Ordered from first evaluation to last
data NodeEvaluationPoint = EnterEvalPoint
                         | LoopEntryPoint -- Meant as a target for continue statements
                         | BeforeIntermediateEvalPoint Int -- Meant for nodes that have a list of computations in them, like if/elif
                                                           -- If you want to use this for not a list index, don't
                         | ExitEvalPoint
  deriving ( NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
(NodeEvaluationPoint -> NodeEvaluationPoint -> Bool)
-> (NodeEvaluationPoint -> NodeEvaluationPoint -> Bool)
-> Eq NodeEvaluationPoint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
$c/= :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
== :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
$c== :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
Eq, Eq NodeEvaluationPoint
Eq NodeEvaluationPoint =>
(NodeEvaluationPoint -> NodeEvaluationPoint -> Ordering)
-> (NodeEvaluationPoint -> NodeEvaluationPoint -> Bool)
-> (NodeEvaluationPoint -> NodeEvaluationPoint -> Bool)
-> (NodeEvaluationPoint -> NodeEvaluationPoint -> Bool)
-> (NodeEvaluationPoint -> NodeEvaluationPoint -> Bool)
-> (NodeEvaluationPoint
    -> NodeEvaluationPoint -> NodeEvaluationPoint)
-> (NodeEvaluationPoint
    -> NodeEvaluationPoint -> NodeEvaluationPoint)
-> Ord NodeEvaluationPoint
NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
NodeEvaluationPoint -> NodeEvaluationPoint -> Ordering
NodeEvaluationPoint -> NodeEvaluationPoint -> NodeEvaluationPoint
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NodeEvaluationPoint -> NodeEvaluationPoint -> NodeEvaluationPoint
$cmin :: NodeEvaluationPoint -> NodeEvaluationPoint -> NodeEvaluationPoint
max :: NodeEvaluationPoint -> NodeEvaluationPoint -> NodeEvaluationPoint
$cmax :: NodeEvaluationPoint -> NodeEvaluationPoint -> NodeEvaluationPoint
>= :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
$c>= :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
> :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
$c> :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
<= :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
$c<= :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
< :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
$c< :: NodeEvaluationPoint -> NodeEvaluationPoint -> Bool
compare :: NodeEvaluationPoint -> NodeEvaluationPoint -> Ordering
$ccompare :: NodeEvaluationPoint -> NodeEvaluationPoint -> Ordering
$cp1Ord :: Eq NodeEvaluationPoint
Ord, Int -> NodeEvaluationPoint -> ShowS
[NodeEvaluationPoint] -> ShowS
NodeEvaluationPoint -> String
(Int -> NodeEvaluationPoint -> ShowS)
-> (NodeEvaluationPoint -> String)
-> ([NodeEvaluationPoint] -> ShowS)
-> Show NodeEvaluationPoint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NodeEvaluationPoint] -> ShowS
$cshowList :: [NodeEvaluationPoint] -> ShowS
show :: NodeEvaluationPoint -> String
$cshow :: NodeEvaluationPoint -> String
showsPrec :: Int -> NodeEvaluationPoint -> ShowS
$cshowsPrec :: Int -> NodeEvaluationPoint -> ShowS
Show, (forall x. NodeEvaluationPoint -> Rep NodeEvaluationPoint x)
-> (forall x. Rep NodeEvaluationPoint x -> NodeEvaluationPoint)
-> Generic NodeEvaluationPoint
forall x. Rep NodeEvaluationPoint x -> NodeEvaluationPoint
forall x. NodeEvaluationPoint -> Rep NodeEvaluationPoint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NodeEvaluationPoint x -> NodeEvaluationPoint
$cfrom :: forall x. NodeEvaluationPoint -> Rep NodeEvaluationPoint x
Generic, NodeEvaluationPoint -> ()
(NodeEvaluationPoint -> ()) -> NFData NodeEvaluationPoint
forall a. (a -> ()) -> NFData a
rnf :: NodeEvaluationPoint -> ()
$crnf :: NodeEvaluationPoint -> ()
NFData )

-- We have to expand the type-synonym AnnTerm in a couple places because no partial application
class (DynCase (Term gs) l) => InsertAt' gs l f where
  insertAt'    :: (MonadAnnotater a m) => NodeEvaluationPoint -> AnnTerm a gs l -> (f :&: a) (AnnTerm a gs) i -> m (AnnTerm a gs i)
  canInsertAt' :: NodeEvaluationPoint -> Proxy l -> (f :&: a) (AnnTerm a gs) i -> Bool

instance {-# OVERLAPPABLE #-} (f :-<: gs, DynCase (Term gs) l) => InsertAt' gs l f where
  insertAt' :: NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) f a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
insertAt'    _ _ t :: (:&:) f a (AnnTerm a gs) i
t = AnnTerm a gs i -> m (AnnTerm a gs i)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnTerm a gs i -> m (AnnTerm a gs i))
-> AnnTerm a gs i -> m (AnnTerm a gs i)
forall a b. (a -> b) -> a -> b
$ (:&:) f a (AnnTerm a gs) i -> AnnTerm a gs i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
       (a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' (:&:) f a (AnnTerm a gs) i
t
  canInsertAt' :: NodeEvaluationPoint
-> Proxy l -> (:&:) f a (AnnTerm a gs) i -> Bool
canInsertAt' _ _ _ = Bool
False

instance {-# OVERLAPPING #-} (ListF :-<: gs, All HFunctor gs, KDynCase (Sum gs) l, KDynCase (Sum gs) [l], Typeable l) => InsertAt' gs l ListF where
  insertAt' :: NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) ListF a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
insertAt' EnterEvalPoint e :: AnnTerm a gs l
e t :: (:&:) ListF a (AnnTerm a gs) i
t = case (:&:) ListF a (AnnTerm a gs) i -> Maybe (i :~: [l])
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase (:&:) ListF a (AnnTerm a gs) i
t :: Maybe (_ :~: [l]) of
                                   Nothing -> AnnTerm a gs i -> m (AnnTerm a gs i)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnTerm a gs i -> m (AnnTerm a gs i))
-> AnnTerm a gs i -> m (AnnTerm a gs i)
forall a b. (a -> b) -> a -> b
$ (:&:) ListF a (AnnTerm a gs) i -> AnnTerm a gs i
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 gs) i
t
                                   Just p :: i :~: [l]
p  -> (i :~: [l])
-> ((i ~ [l]) => m (AnnTerm a gs i)) -> m (AnnTerm a gs i)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith i :~: [l]
p (((i ~ [l]) => m (AnnTerm a gs i)) -> m (AnnTerm a gs i))
-> ((i ~ [l]) => m (AnnTerm a gs i)) -> m (AnnTerm a gs i)
forall a b. (a -> b) -> a -> b
$ ((:&:) ListF a (AnnTerm a gs) [l]
 -> Cxt NoHole (Sum gs :&: a) (K ()) [l])
-> m ((:&:) ListF a (AnnTerm a gs) [l])
-> m (Cxt NoHole (Sum gs :&: a) (K ()) [l])
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (:&:) ListF a (AnnTerm a gs) [l]
-> Cxt NoHole (Sum gs :&: a) (K ()) [l]
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
       (a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' (m ((:&:) ListF a (AnnTerm a gs) [l]) -> m (AnnTerm a gs i))
-> m ((:&:) ListF a (AnnTerm a gs) [l]) -> m (AnnTerm a gs i)
forall a b. (a -> b) -> a -> b
$ ListF (AnnTerm a gs) [l] -> m ((:&:) ListF a (AnnTerm a gs) [l])
forall a (m :: * -> *) (f :: (* -> *) -> * -> *) (e :: * -> *) l.
MonadAnnotater a m =>
f e l -> m ((:&:) f a e l)
annM (ListF (AnnTerm a gs) [l] -> m ((:&:) ListF a (AnnTerm a gs) [l]))
-> ListF (AnnTerm a gs) [l] -> m ((:&:) ListF a (AnnTerm a gs) [l])
forall a b. (a -> b) -> a -> b
$ AnnTerm a gs l
-> Cxt NoHole (Sum gs :&: a) (K ()) [l] -> ListF (AnnTerm a gs) [l]
forall l (e :: * -> *). Typeable l => e l -> e [l] -> ListF e [l]
ConsF AnnTerm a gs l
e ((:&:) ListF a (AnnTerm a gs) i -> AnnTerm a gs i
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 gs) i
t)
  insertAt' _              _ t :: (:&:) ListF a (AnnTerm a gs) i
t = AnnTerm a gs i -> m (AnnTerm a gs i)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnTerm a gs i -> m (AnnTerm a gs i))
-> AnnTerm a gs i -> m (AnnTerm a gs i)
forall a b. (a -> b) -> a -> b
$ (:&:) ListF a (AnnTerm a gs) i -> AnnTerm a gs i
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 gs) i
t

  canInsertAt' :: NodeEvaluationPoint
-> Proxy l -> (:&:) ListF a (AnnTerm a gs) i -> Bool
canInsertAt' EnterEvalPoint _ = Proxy [l] -> forall i (e :: * -> *). (:&:) ListF a e i -> Bool
forall (f :: (* -> *) -> * -> *) l.
KDynCase f l =>
Proxy l -> forall i (e :: * -> *). f e i -> Bool
kIsSort (Proxy [l]
forall k (t :: k). Proxy t
Proxy :: Proxy [l])
  canInsertAt' _              _ = Bool -> (:&:) ListF a (AnnTerm a gs) i -> Bool
forall a b. a -> b -> a
const Bool
False

instance {-# OVERLAPPING #-} (All (InsertAt' gs l) fs, DynCase (Term gs) l) => InsertAt' gs l (Sum fs) where
  insertAt' :: NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) (Sum fs) a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
insertAt' p :: NodeEvaluationPoint
p e :: AnnTerm a gs l
e = Proxy (InsertAt' gs l)
-> (forall (f :: (* -> *) -> * -> *).
    InsertAt' gs l f =>
    (:&:) f a (AnnTerm a gs) i -> m (AnnTerm a gs i))
-> (:&:) (Sum fs) a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) a (e :: * -> *) l t.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => (:&:) f a e l -> t)
-> (:&:) (Sum fs) a e l
-> t
caseCxt' (Proxy (InsertAt' gs l)
forall k (t :: k). Proxy t
Proxy @(InsertAt' gs l)) (NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) f a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
forall (gs :: [(* -> *) -> * -> *]) l (f :: (* -> *) -> * -> *) a
       (m :: * -> *) i.
(InsertAt' gs l f, MonadAnnotater a m) =>
NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) f a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
insertAt' NodeEvaluationPoint
p AnnTerm a gs l
e)
  canInsertAt' :: NodeEvaluationPoint
-> Proxy l -> (:&:) (Sum fs) a (AnnTerm a gs) i -> Bool
canInsertAt' p :: NodeEvaluationPoint
p e :: Proxy l
e = Proxy (InsertAt' gs l)
-> (forall (f :: (* -> *) -> * -> *).
    InsertAt' gs l f =>
    (:&:) f a (AnnTerm a gs) i -> Bool)
-> (:&:) (Sum fs) a (AnnTerm a gs) i
-> Bool
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) a (e :: * -> *) l t.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => (:&:) f a e l -> t)
-> (:&:) (Sum fs) a e l
-> t
caseCxt' (Proxy (InsertAt' gs l)
forall k (t :: k). Proxy t
Proxy @(InsertAt' gs l)) (NodeEvaluationPoint
-> Proxy l -> (:&:) f a (AnnTerm a gs) i -> Bool
forall (gs :: [(* -> *) -> * -> *]) l (f :: (* -> *) -> * -> *) a
       i.
InsertAt' gs l f =>
NodeEvaluationPoint
-> Proxy l -> (:&:) f a (AnnTerm a gs) i -> Bool
canInsertAt' NodeEvaluationPoint
p Proxy l
e)

class InsertAt gs l where
  insertAt    :: (MonadAnnotater a m) => NodeEvaluationPoint -> AnnTerm a gs l -> AnnTerm a gs i -> m (AnnTerm a gs i)
  canInsertAt :: NodeEvaluationPoint -> Proxy l -> AnnTerm a gs i -> Bool

-- TODO: When this constraint is replace with All, it asks for a bunch of other constraints.
instance (InsertAt' gs l (Sum gs)) => InsertAt gs l where
 insertAt :: NodeEvaluationPoint
-> AnnTerm a gs l -> AnnTerm a gs i -> m (AnnTerm a gs i)
insertAt p :: NodeEvaluationPoint
p e :: AnnTerm a gs l
e t :: AnnTerm a gs i
t       = NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) (Sum gs) a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
forall (gs :: [(* -> *) -> * -> *]) l (f :: (* -> *) -> * -> *) a
       (m :: * -> *) i.
(InsertAt' gs l f, MonadAnnotater a m) =>
NodeEvaluationPoint
-> AnnTerm a gs l
-> (:&:) f a (AnnTerm a gs) i
-> m (AnnTerm a gs i)
insertAt' NodeEvaluationPoint
p AnnTerm a gs l
e (AnnTerm a gs i -> (:&:) (Sum gs) a (AnnTerm a gs) i
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm AnnTerm a gs i
t)
 canInsertAt :: NodeEvaluationPoint -> Proxy l -> AnnTerm a gs i -> Bool
canInsertAt p :: NodeEvaluationPoint
p prox :: Proxy l
prox t :: AnnTerm a gs i
t = NodeEvaluationPoint
-> Proxy l -> (:&:) (Sum gs) a (AnnTerm a gs) i -> Bool
forall (gs :: [(* -> *) -> * -> *]) l (f :: (* -> *) -> * -> *) a
       i.
InsertAt' gs l f =>
NodeEvaluationPoint
-> Proxy l -> (:&:) f a (AnnTerm a gs) i -> Bool
canInsertAt' NodeEvaluationPoint
p Proxy l
prox (AnnTerm a gs i -> (:&:) (Sum gs) a (AnnTerm a gs) i
forall (f :: (* -> *) -> * -> *) t. HFix f t -> f (HFix f) t
unTerm AnnTerm a gs i
t)


insertBefore :: (InsertAt gs l, MonadAnnotater a m) => AnnTerm a gs l -> AnnTerm a gs i -> m (AnnTerm a gs i)
insertBefore :: AnnTerm a gs l -> AnnTerm a gs i -> m (AnnTerm a gs i)
insertBefore = NodeEvaluationPoint
-> AnnTerm a gs l -> AnnTerm a gs i -> m (AnnTerm a gs i)
forall (gs :: [(* -> *) -> * -> *]) l a (m :: * -> *) i.
(InsertAt gs l, MonadAnnotater a m) =>
NodeEvaluationPoint
-> AnnTerm a gs l -> AnnTerm a gs i -> m (AnnTerm a gs i)
insertAt NodeEvaluationPoint
EnterEvalPoint

canInsertBefore :: (InsertAt gs l) => Proxy l -> AnnTerm a gs i -> Bool
canInsertBefore :: Proxy l -> AnnTerm a gs i -> Bool
canInsertBefore = NodeEvaluationPoint -> Proxy l -> AnnTerm a gs i -> Bool
forall (gs :: [(* -> *) -> * -> *]) l a i.
InsertAt gs l =>
NodeEvaluationPoint -> Proxy l -> AnnTerm a gs i -> Bool
canInsertAt NodeEvaluationPoint
EnterEvalPoint