{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# OPTIONS_HADDOCK hide #-}
-- |
-- Module      : Data.Array.Accelerate.AST.Environment
-- Copyright   : [2008..2020] The Accelerate Team
-- License     : BSD3
--
-- Maintainer  : Trevor L. McDonell <trevor.mcdonell@gmail.com>
-- Stability   : experimental
-- Portability : non-portable (GHC extensions)
--

module Data.Array.Accelerate.AST.Environment
  where

import Data.Array.Accelerate.AST.Idx
import Data.Array.Accelerate.AST.LeftHandSide
import Data.Array.Accelerate.Error


-- Valuation for an environment
--
data Val env where
  Empty :: Val ()
  Push  :: Val env -> t -> Val (env, t)

-- Push a set of variables into an environment
--
push :: Val env -> (LeftHandSide s t env env', t) -> Val env'
push :: forall env (s :: * -> *) t env'.
Val env -> (LeftHandSide s t env env', t) -> Val env'
push Val env
env (LeftHandSideWildcard TupR s t
_, t
_     ) = Val env
Val env'
env
push Val env
env (LeftHandSideSingle s t
_  , t
a     ) = Val env
env Val env -> t -> Val (env, t)
forall env t. Val env -> t -> Val (env, t)
`Push` t
a
push Val env
env (LeftHandSidePair LeftHandSide s v1 env env'1
l1 LeftHandSide s v2 env'1 env'
l2, (v1
a, v2
b)) = Val env -> (LeftHandSide s v1 env env'1, v1) -> Val env'1
forall env (s :: * -> *) t env'.
Val env -> (LeftHandSide s t env env', t) -> Val env'
push Val env
env (LeftHandSide s v1 env env'1
l1, v1
a) Val env'1 -> (LeftHandSide s v2 env'1 env', v2) -> Val env'
forall env (s :: * -> *) t env'.
Val env -> (LeftHandSide s t env env', t) -> Val env'
`push` (LeftHandSide s v2 env'1 env'
l2, v2
b)

-- Projection of a value from a valuation using a de Bruijn index
--
prj :: Idx env t -> Val env -> t
prj :: forall env t. Idx env t -> Val env -> t
prj Idx env t
ZeroIdx       (Push Val env
_   t
v) = t
t
v
prj (SuccIdx Idx env t
idx) (Push Val env
val t
_) = Idx env t -> Val env -> t
forall env t. Idx env t -> Val env -> t
prj Idx env t
idx Val env
Val env
val


-- The type of shifting terms from one context into another
--
-- This is defined as a newtype, as a type synonym containing a forall
-- quantifier may give issues with impredicative polymorphism, which GHC
-- does not support.
--
newtype env :> env' = Weaken { forall env env'.
(env :> env') -> forall t'. Idx env t' -> Idx env' t'
(>:>) :: forall t'. Idx env t' -> Idx env' t' } -- Weak or Weaken

weakenId :: env :> env
weakenId :: forall env. env :> env
weakenId = (forall t'. Idx env t' -> Idx env t') -> env :> env
forall env env'.
(forall t'. Idx env t' -> Idx env' t') -> env :> env'
Weaken Idx env t' -> Idx env t'
forall a. a -> a
forall t'. Idx env t' -> Idx env t'
id

weakenSucc' :: env :> env' -> env :> (env', t)
weakenSucc' :: forall env env' t. (env :> env') -> env :> (env', t)
weakenSucc' (Weaken forall t'. Idx env t' -> Idx env' t'
f) = (forall t'. Idx env t' -> Idx (env', t) t') -> env :> (env', t)
forall env env'.
(forall t'. Idx env t' -> Idx env' t') -> env :> env'
Weaken (Idx env' t' -> Idx (env', t) t'
forall envs t s env. (envs ~ (env, s)) => Idx env t -> Idx envs t
SuccIdx (Idx env' t' -> Idx (env', t) t')
-> (Idx env t' -> Idx env' t') -> Idx env t' -> Idx (env', t) t'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Idx env t' -> Idx env' t'
forall t'. Idx env t' -> Idx env' t'
f)

weakenSucc :: (env, t) :> env' -> env :> env'
weakenSucc :: forall env t env'. ((env, t) :> env') -> env :> env'
weakenSucc (Weaken forall t'. Idx (env, t) t' -> Idx env' t'
f) = (forall t'. Idx env t' -> Idx env' t') -> env :> env'
forall env env'.
(forall t'. Idx env t' -> Idx env' t') -> env :> env'
Weaken (Idx (env, t) t' -> Idx env' t'
forall t'. Idx (env, t) t' -> Idx env' t'
f (Idx (env, t) t' -> Idx env' t')
-> (Idx env t' -> Idx (env, t) t') -> Idx env t' -> Idx env' t'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Idx env t' -> Idx (env, t) t'
forall envs t s env. (envs ~ (env, s)) => Idx env t -> Idx envs t
SuccIdx)

weakenEmpty :: () :> env'
weakenEmpty :: forall env'. () :> env'
weakenEmpty = (forall t'. Idx () t' -> Idx env' t') -> () :> env'
forall env env'.
(forall t'. Idx env t' -> Idx env' t') -> env :> env'
Weaken ((forall t'. Idx () t' -> Idx env' t') -> () :> env')
-> (forall t'. Idx () t' -> Idx env' t') -> () :> env'
forall a b. (a -> b) -> a -> b
$ \(VoidIdx Idx env' t'
x) -> Idx env' t'
x

sink :: forall env env' t. env :> env' -> (env, t) :> (env', t)
sink :: forall env env' t. (env :> env') -> (env, t) :> (env', t)
sink (Weaken forall t'. Idx env t' -> Idx env' t'
f) = (forall t'. Idx (env, t) t' -> Idx (env', t) t')
-> (env, t) :> (env', t)
forall env env'.
(forall t'. Idx env t' -> Idx env' t') -> env :> env'
Weaken Idx (env, t) t' -> Idx (env', t) t'
forall t'. Idx (env, t) t' -> Idx (env', t) t'
g
  where
    g :: Idx (env, t) t' -> Idx (env', t) t'
    g :: forall t'. Idx (env, t) t' -> Idx (env', t) t'
g Idx (env, t) t'
ZeroIdx      = Idx (env', t) t'
forall envt t env. (envt ~ (env, t)) => Idx envt t
ZeroIdx
    g (SuccIdx Idx env t'
ix) = Idx env' t' -> Idx (env', t) t'
forall envs t s env. (envs ~ (env, s)) => Idx env t -> Idx envs t
SuccIdx (Idx env' t' -> Idx (env', t) t')
-> Idx env' t' -> Idx (env', t) t'
forall a b. (a -> b) -> a -> b
$ Idx env t' -> Idx env' t'
forall t'. Idx env t' -> Idx env' t'
f Idx env t'
Idx env t'
ix

infixr 9 .>
(.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
.> :: forall env2 env3 env1.
(env2 :> env3) -> (env1 :> env2) -> env1 :> env3
(.>) (Weaken forall t'. Idx env2 t' -> Idx env3 t'
f) (Weaken forall t'. Idx env1 t' -> Idx env2 t'
g) = (forall t'. Idx env1 t' -> Idx env3 t') -> env1 :> env3
forall env env'.
(forall t'. Idx env t' -> Idx env' t') -> env :> env'
Weaken (Idx env2 t' -> Idx env3 t'
forall t'. Idx env2 t' -> Idx env3 t'
f (Idx env2 t' -> Idx env3 t')
-> (Idx env1 t' -> Idx env2 t') -> Idx env1 t' -> Idx env3 t'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Idx env1 t' -> Idx env2 t'
forall t'. Idx env1 t' -> Idx env2 t'
g)

sinkWithLHS :: HasCallStack => LeftHandSide s t env1 env1' -> LeftHandSide s t env2 env2' -> env1 :> env2 -> env1' :> env2'
sinkWithLHS :: forall (s :: * -> *) t env1 env1' env2 env2'.
HasCallStack =>
LeftHandSide s t env1 env1'
-> LeftHandSide s t env2 env2' -> (env1 :> env2) -> env1' :> env2'
sinkWithLHS (LeftHandSideWildcard TupR s t
_) (LeftHandSideWildcard TupR s t
_) env1 :> env2
k = env1 :> env2
env1' :> env2'
k
sinkWithLHS (LeftHandSideSingle s t
_)   (LeftHandSideSingle s t
_)   env1 :> env2
k = (env1 :> env2) -> (env1, t) :> (env2, t)
forall env env' t. (env :> env') -> (env, t) :> (env', t)
sink env1 :> env2
k
sinkWithLHS (LeftHandSidePair LeftHandSide s v1 env1 env'1
a1 LeftHandSide s v2 env'1 env1'
b1) (LeftHandSidePair LeftHandSide s v1 env2 env'1
a2 LeftHandSide s v2 env'1 env2'
b2) env1 :> env2
k = LeftHandSide s v2 env'1 env1'
-> LeftHandSide s v2 env'1 env2'
-> (env'1 :> env'1)
-> env1' :> env2'
forall (s :: * -> *) t env1 env1' env2 env2'.
HasCallStack =>
LeftHandSide s t env1 env1'
-> LeftHandSide s t env2 env2' -> (env1 :> env2) -> env1' :> env2'
sinkWithLHS LeftHandSide s v2 env'1 env1'
b1 LeftHandSide s v2 env'1 env2'
LeftHandSide s v2 env'1 env2'
b2 ((env'1 :> env'1) -> env1' :> env2')
-> (env'1 :> env'1) -> env1' :> env2'
forall a b. (a -> b) -> a -> b
$ LeftHandSide s v1 env1 env'1
-> LeftHandSide s v1 env2 env'1 -> (env1 :> env2) -> env'1 :> env'1
forall (s :: * -> *) t env1 env1' env2 env2'.
HasCallStack =>
LeftHandSide s t env1 env1'
-> LeftHandSide s t env2 env2' -> (env1 :> env2) -> env1' :> env2'
sinkWithLHS LeftHandSide s v1 env1 env'1
a1 LeftHandSide s v1 env2 env'1
LeftHandSide s v1 env2 env'1
a2 env1 :> env2
k
sinkWithLHS LeftHandSide s t env1 env1'
_ LeftHandSide s t env2 env2'
_ env1 :> env2
_ = Format (env1' :> env2') (env1' :> env2') -> env1' :> env2'
forall r a. HasCallStack => Format r a -> a
internalError Format (env1' :> env2') (env1' :> env2')
"left hand sides do not match"

weakenWithLHS :: forall s t env env'. LeftHandSide s t env env' -> env :> env'
weakenWithLHS :: forall (s :: * -> *) t env env'.
LeftHandSide s t env env' -> env :> env'
weakenWithLHS = (env' :> env') -> LeftHandSide s t env env' -> env :> env'
forall env2 arrs env1.
(env2 :> env') -> LeftHandSide s arrs env1 env2 -> env1 :> env'
go env' :> env'
forall env. env :> env
weakenId
  where
    go :: env2 :> env' -> LeftHandSide s arrs env1 env2 -> env1 :> env'
    go :: forall env2 arrs env1.
(env2 :> env') -> LeftHandSide s arrs env1 env2 -> env1 :> env'
go env2 :> env'
k (LeftHandSideWildcard TupR s arrs
_) = env2 :> env'
env1 :> env'
k
    go env2 :> env'
k (LeftHandSideSingle s arrs
_)   = ((env1, arrs) :> env') -> env1 :> env'
forall env t env'. ((env, t) :> env') -> env :> env'
weakenSucc env2 :> env'
(env1, arrs) :> env'
k
    go env2 :> env'
k (LeftHandSidePair LeftHandSide s v1 env1 env'1
l1 LeftHandSide s v2 env'1 env2
l2) = (env'1 :> env') -> LeftHandSide s v1 env1 env'1 -> env1 :> env'
forall env2 arrs env1.
(env2 :> env') -> LeftHandSide s arrs env1 env2 -> env1 :> env'
go ((env2 :> env') -> LeftHandSide s v2 env'1 env2 -> env'1 :> env'
forall env2 arrs env1.
(env2 :> env') -> LeftHandSide s arrs env1 env2 -> env1 :> env'
go env2 :> env'
k LeftHandSide s v2 env'1 env2
l2) LeftHandSide s v1 env1 env'1
l1