From 174af2ba568de66e0d890825b8bda930b8e7bb96 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 10 Nov 2025 21:49:45 +0100 Subject: Move module hierarchy under CHAD. --- src/CHAD/EnvDescr.hs | 96 ---------------------------------------------------- 1 file changed, 96 deletions(-) delete mode 100644 src/CHAD/EnvDescr.hs (limited to 'src/CHAD/EnvDescr.hs') diff --git a/src/CHAD/EnvDescr.hs b/src/CHAD/EnvDescr.hs deleted file mode 100644 index 49ae0e6..0000000 --- a/src/CHAD/EnvDescr.hs +++ /dev/null @@ -1,96 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE StandaloneKindSignatures #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -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 - - -type Storage :: Symbol -> Type -data Storage s where - SAccum :: Storage "accum" -- ^ in the monad state as a mutable accumulator - SMerge :: Storage "merge" -- ^ just return and merge - SDiscr :: Storage "discr" -- ^ we happen to know this is a discrete type and won't need any contributions -deriving instance Show (Storage s) - --- | Environment description -data Descr env sto where - DTop :: Descr '[] '[] - DPush :: Descr env sto -> (STy t, Maybe (ValId t), Storage s) -> Descr (t : env) (s : sto) -deriving instance Show (Descr env sto) - -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' - -> Subenv (Select env sto "merge") (Select env' sto' "merge") - -> Subenv (D2AcE (Select env sto "accum")) (D2AcE (Select env' sto' "accum")) - -> Subenv (D1E env) (D1E env') - -> r) - -> r -subDescr DTop SETop k = k DTop SETop SETop SETop -subDescr (des `DPush` (t, vid, sto)) (SEYesR sub) k = - subDescr des sub $ \des' submerge subaccum subd1e -> - case sto of - SMerge -> k (des' `DPush` (t, vid, sto)) (SEYesR submerge) subaccum (SEYesR subd1e) - SAccum -> k (des' `DPush` (t, vid, sto)) submerge (SEYesR subaccum) (SEYesR subd1e) - SDiscr -> k (des' `DPush` (t, vid, sto)) submerge subaccum (SEYesR subd1e) -subDescr (des `DPush` (_, _, sto)) (SENo sub) k = - subDescr des sub $ \des' submerge subaccum subd1e -> - case sto of - SMerge -> k des' (SENo submerge) subaccum (SENo subd1e) - SAccum -> k des' submerge (SENo subaccum) (SENo subd1e) - SDiscr -> k des' submerge subaccum (SENo subd1e) - --- | Select only the types from the environment that have the specified storage -type family Select env sto s where - Select '[] '[] _ = '[] - Select (t : ts) (s : sto) s = t : Select ts sto s - Select (_ : ts) (_ : sto) s = Select ts sto s - -select :: Storage s -> Descr env sto -> SList STy (Select env sto s) -select _ DTop = SNil -select s@SAccum (DPush des (t, _, SAccum)) = SCons t (select s des) -select s@SMerge (DPush des (_, _, SAccum)) = select s des -select s@SDiscr (DPush des (_, _, SAccum)) = select s des -select s@SAccum (DPush des (_, _, SMerge)) = select s des -select s@SMerge (DPush des (t, _, SMerge)) = SCons t (select s des) -select s@SDiscr (DPush des (_, _, SMerge)) = select s des -select s@SAccum (DPush des (_, _, SDiscr)) = select s des -select s@SMerge (DPush des (_, _, SDiscr)) = select s des -select s@SDiscr (DPush des (t, _, SDiscr)) = SCons t (select s des) - -selectSub :: Storage s -> Descr env sto -> Subenv env (Select env sto s) -selectSub _ DTop = SETop -selectSub s@SAccum (DPush des (_, _, SAccum)) = SEYesR (selectSub s des) -selectSub s@SMerge (DPush des (_, _, SAccum)) = SENo (selectSub s des) -selectSub s@SDiscr (DPush des (_, _, SAccum)) = SENo (selectSub s des) -selectSub s@SAccum (DPush des (_, _, SMerge)) = SENo (selectSub s des) -selectSub s@SMerge (DPush des (_, _, SMerge)) = SEYesR (selectSub s des) -selectSub s@SDiscr (DPush des (_, _, SMerge)) = SENo (selectSub s des) -selectSub s@SAccum (DPush des (_, _, SDiscr)) = SENo (selectSub s des) -selectSub s@SMerge (DPush des (_, _, SDiscr)) = SENo (selectSub s des) -selectSub s@SDiscr (DPush des (_, _, SDiscr)) = SEYesR (selectSub s des) -- cgit v1.2.3-70-g09d2