1 files changed, 8 insertions, 0 deletions
diff --git a/src/CHAD/EnvDescr.hs b/src/CHAD/EnvDescr.hs
index de615a1..4c287d7 100644
--- a/src/CHAD/EnvDescr.hs
+++ b/src/CHAD/EnvDescr.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -9,11 +10,13 @@
 module CHAD.EnvDescr where
 
 import Data.Kind (Type)
+import Data.Some
 import GHC.TypeLits (Symbol)
 
 import Analysis.Identity (ValId(..))
 import AST.Env
 import AST.Types
+import AST.Weaken
 import CHAD.Types
 import Data
 
@@ -35,6 +38,11 @@ descrList :: Descr env sto -> SList STy env
 descrList DTop = SNil
 descrList (des `DPush` (t, _, _)) = t `SCons` descrList des
 
+descrPrj :: Descr env sto -> Idx env t -> (STy t, Maybe (ValId t), Some Storage)
+descrPrj (_ `DPush` (ty, vid, sto)) IZ = (ty, vid, Some sto)
+descrPrj (des `DPush` _) (IS i) = descrPrj des i
+descrPrj DTop i = case i of {}
+
 -- | This could have more precise typing on the output storage.
 subDescr :: Descr env sto -> Subenv env env'
          -> (forall sto'. Descr env' sto'