TTTAS 0.2.1 → 0.3.0
raw patch · 3 files changed
+96/−59 lines, 3 filesdep ~basePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base
API changes (from Hackage documentation)
+ Language.TTTAS: (>>>>) :: (Category2 cat) => cat a b -> cat b c -> cat a c
+ Language.TTTAS: Upd :: (FinalEnv t s -> FinalEnv t s) -> UpdFinalEnv t s
+ Language.TTTAS: newtype UpdFinalEnv t s
+ Language.TTTAS: updateFinalEnv :: Trafo m t s (FinalEnv t s -> FinalEnv t s) ()
+ Language.TTTAS: updateFinalEnv2 :: Trafo2 m t (UpdFinalEnv t) Unit
- Language.TTTAS: TrafoE :: (m env2) -> (a -> T env2 s -> Env t s env1 -> (b, T env1 s, Env t s env2)) -> TrafoE m t s env1 a b
+ Language.TTTAS: TrafoE :: (m env2) -> (a -> T env2 s -> Env t s env1 -> (FinalEnv t s -> FinalEnv t s) -> (b, T env1 s, Env t s env2, FinalEnv t s -> FinalEnv t s)) -> TrafoE m t s env1 a b
- Language.TTTAS: TrafoE2 :: (m env2) -> (forall s. a s -> T env2 s -> Env t s env1 -> (b s, T env1 s, Env t s env2)) -> TrafoE2 m t env1 a b
+ Language.TTTAS: TrafoE2 :: (m env2) -> (forall s. a s -> T env2 s -> Env t s env1 -> UpdFinalEnv t s -> (b s, T env1 s, Env t s env2, UpdFinalEnv t s)) -> TrafoE2 m t env1 a b
Files
- TTTAS.cabal +3/−3
- examples/CSE2.hs +12/−10
- src/Language/TTTAS.hs +81/−46
TTTAS.cabal view
@@ -1,7 +1,7 @@-cabal-version: >=1.2+cabal-version: >=1.2.3 build-type: Simple name: TTTAS-version: 0.2.1+version: 0.3.0 license: LGPL license-file: COPYRIGHT maintainer: Arthur Baars <abaars@iti.upv.es>@@ -11,7 +11,7 @@ category: stability: Stable copyright: Universiteit Utrecht-build-depends: base, haskell98+build-depends: base >= 2 && < 4.1.0.0, haskell98 exposed-modules: Language.TTTAS extensions: Arrows, GADTs, CPP hs-source-dirs: src
examples/CSE2.hs view
@@ -69,7 +69,7 @@ case newERef1 e of Trafo2 step -> step (MapExpr1 m) Just r -> TrafoE2 (MapExpr1 m) - (\e (T t) env1 -> (t r, T t, env1))+ (\e (T t) env1 upds -> (t r, T t, env1, upds)) ) newERef1 :: Expr1 a @@ -79,10 +79,11 @@ (\(MapExpr1 m :: MapExpr1 env1) -> let m2 = MapExpr1 (\s -> aux1 (matchExpr1 e s) m s) in TrafoE2 m2 - (\e (T t) env1 -> ( t Zero- , T (t . Suc) - , Ext env1 e- ) ) )+ (\e (T t) env1 upds -> ( t Zero+ , T (t . Suc) + , Ext env1 e+ , upds+ ) ) ) aux1 :: Maybe (Equal a x) -> (Expr1 x -> Maybe (Ref x env1)) -> Expr1 x -> Maybe (Ref x (env1,a))@@ -202,7 +203,7 @@ case newERef e of Trafo2 step -> step (MapExpr m) Just r -> TrafoE2 (MapExpr m) - (\e (T t) env1 -> (t r, T t, env1))+ (\e (T t) env1 upds -> (t r, T t, env1, upds)) ) newERef :: Expr a env@@ -212,10 +213,11 @@ (\(MapExpr m :: MapExpr env env1) -> let m2 = MapExpr (\s -> aux (matchExpr e s) m s) in TrafoE2 m2 - (\e (T t) env1 -> ( t Zero- , T (t . Suc) - , Ext env1 e- ) ) )+ (\e (T t) env1 upds -> ( t Zero+ , T (t . Suc) + , Ext env1 e+ , upds+ ) ) ) aux :: Maybe (Equal a x) -> (Expr x env -> Maybe (Ref x env1)) -> Expr x env -> Maybe (Ref x (env1,a))
src/Language/TTTAS.hs view
@@ -31,6 +31,9 @@ -- ** Create New References Unit(..), newSRef, extEnv, castSRef, updateSRef, + + -- ** Update the Final Environment + updateFinalEnv, -- ** Run a Trafo Result(..), @@ -47,12 +50,17 @@ -- ** Create New References newSRef2, + -- ** Update the Final Environment + UpdFinalEnv(..), updateFinalEnv2, + -- ** Run a Trafo2 runTrafo2, -- ** Arrow-style Combinators Pair(..), Arrow2(..), ArrowLoop2(..), + (>>>>), List(..), sequenceA2 + ) where import Unsafe.Coerce ( unsafeCoerce ) @@ -127,6 +135,7 @@ lookupEnv :: Ref a env -> Env t s env -> t a s lookupEnv Zero (Ext _ t) = t lookupEnv (Suc r) (Ext ts _) = lookupEnv r ts +lookupEnv _ _ = error "Error: The impossible happened!" updateEnv :: (t a s -> t a s) -> Ref a env -> Env t s env -> Env t s env @@ -134,7 +143,10 @@ = Ext ts (f t) updateEnv f (Suc r) (Ext ts t) = Ext (updateEnv f r ts) t +updateEnv _ _ _ + = error "Error: The impossible happened!" + -- | When the types @def@ and @use@ of an 'Env' coincide, -- we can be sure that the references in the terms do not -- point to values outside the environment but point @@ -162,14 +174,19 @@ -- the definition of 'Trafo'. -- It can be seen that a 'Trafo' is a function taking as arguments: the input (@a@), -- a 'Ref'-transformer (@T env2 s@) from the environment constructed in this step --- to the final environment and the environment (@Env t s env1@) where the --- current transformation starts. The function returns: the output (@b@), a --- 'Ref'-transformer (@T env1 s@) from the initial environment of this step to the final --- environment and the environment (@Env t s env2@) constructed in this step. +-- to the final environment, the environment (@Env t s env1@) where the current +-- transformation starts and a function (@FinalEnv t s -> FinalEnv t s@) to update +-- (modify) the final environment. The function returns: the output (@b@), +-- a 'Ref'-transformer (@T env1 s@) from the initial environment of this step to the final +-- environment, the environment (@Env t s env2@) constructed in this step and a function +-- (@FinalEnv t s -> FinalEnv t s@) to update (modify) the final environment. +-- NOTE: The function (@FinalEnv t s -> FinalEnv t s@) was introduced in version 0.3. +-- It's carried throw the transformation steps and can be modified (composed to another function) +-- using the function 'updateFinalEnv'. data TrafoE m t s env1 a b = forall env2 . TrafoE ( m env2) - ( a -> T env2 s -> Env t s env1 - -> ( b, T env1 s, Env t s env2) + ( a -> T env2 s -> Env t s env1 -> (FinalEnv t s -> FinalEnv t s) + -> ( b, T env1 s, Env t s env2, (FinalEnv t s -> FinalEnv t s)) ) data Unit s = Unit @@ -183,24 +200,30 @@ = Trafo (\ _-> extEnv Unit) +-- | The function 'updateFinalEnv' returns a 'Trafo' that introduces a function +-- (@FinalEnv t s -> FinalEnv t s@) to update the final environment. +updateFinalEnv :: Trafo m t s (FinalEnv t s -> FinalEnv t s) () +updateFinalEnv = Trafo $ \m -> (TrafoE m (\f' t e f -> ((), t, e, f' . f))) + + -- | The function 'extEnv' returns a 'TrafoE' that extends the current environment. extEnv :: m (e,a) -> TrafoE m t s e (t a s) (Ref a s) -extEnv m = TrafoE m $ \ta (T tr) env -> (tr Zero, T (tr P.. Suc), Ext env ta ) +extEnv m = TrafoE m $ \ta (T tr) env f -> (tr Zero, T (tr P.. Suc), Ext env ta, f ) -- | The function 'castSRef' returns a 'TrafoE' that casts the reference -- passed as parameter (in the constructed environment) to one in the final environment. castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s) -castSRef m r = TrafoE m $ (\ _ (T t) decls -> (t r, T t, decls)) +castSRef m r = TrafoE m $ (\ _ (T t) decls f -> (t r, T t, decls, f)) -- | The function 'updateSRef' returns a 'TrafoE' that updates the value pointed -- by the reference passed as parameter into the current environment. updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s e i (Ref a s) -updateSRef m r f = TrafoE m $ \i (T t) decls -> (t r, T t, updateEnv (f i) r decls) +updateSRef m r f = TrafoE m $ \i (T t) decls fs -> (t r, T t, updateEnv (f i) r decls, fs) instance Functor (TrafoE m t s e a) where - fmap f (TrafoE m step) = TrafoE m $ \i t e -> case step i t e of - (i',t',e') -> (f i',t',e') + fmap f (TrafoE m step) = TrafoE m $ \i t e fs -> case step i t e fs of + (i',t',e',fs') -> (f i',t',e',fs') -- | The type 'Result' is the type of the result of \"running\" a 'Trafo'. -- Because @s@ could be anything we have to hide it using existential quantification. @@ -218,11 +241,11 @@ runTrafo trafo m a = case trafo of Trafo trf -> case trf m of TrafoE m2 f -> - case f a (T unsafeCoerce) Empty of - (rb, _, env2) -> + case f a (T unsafeCoerce) Empty P.id of -- the function could also be passed as argument + (rb, _, env2, fenvs) -> Result (unsafeCoerce m2) rb - (unsafeCoerce env2) + (fenvs $ unsafeCoerce env2) #if __GLASGOW_HASKELL__ >= 609 @@ -235,15 +258,15 @@ TrafoE m3 f2 -> TrafoE m3 - (\a tt env1 -> - let (b,tt1, env2) = f1 a tt2 env1 - (c,tt2, env3) = f2 b tt env2 - in (c,tt1, env3) + (\a tt env1 fs -> + let (b,tt1, env2, fs') = f1 a tt2 env1 fs + (c,tt2, env3, fs'') = f2 b tt env2 fs' + in (c,tt1, env3, fs'') ) ) -- |id :: Trafo m t s a a| - id = Trafo (\m -> TrafoE m (\a t e -> (a, t, e)) ) + id = Trafo (\m -> TrafoE m (\a t e f -> (a, t, e, f)) ) #endif @@ -251,7 +274,7 @@ instance Arrow (Trafo m t s) where -- |arr :: (a -> b) -> Trafo m t s a b| - arr f = Trafo (\m -> TrafoE m (\a t e -> (f a, t, e)) ) + arr f = Trafo (\m -> TrafoE m (\a t e fs -> (f a, t, e, fs)) ) #if __GLASGOW_HASKELL__ < 609 @@ -262,10 +285,10 @@ TrafoE m3 f2 -> TrafoE m3 - (\a tt env1 -> - let (b,tt1, env2) = f1 a tt2 env1 - (c,tt2, env3) = f2 b tt env2 - in (c,tt1, env3) + (\a tt env1 fs -> + let (b,tt1, env2, fs') = f1 a tt2 env1 fs + (c,tt2, env3, fs'') = f2 b tt env2 fs' + in (c,tt1, env3, fs'') ) ) @@ -277,9 +300,9 @@ TrafoE m2 f -> TrafoE m2 - (\ ~(a,c) tt env1 -> - let (b,tt1,env2) = f a tt env1 - in ((b,c),tt1, env2))) + (\ ~(a,c) tt env1 fs -> + let (b,tt1,env2, fs') = f a tt env1 fs + in ((b,c),tt1, env2, fs'))) instance ArrowLoop (Trafo m t s) where @@ -289,9 +312,9 @@ (\m -> case st m of TrafoE m1 f1 -> TrafoE m1 - (\a t e -> - let ((b, x),t1,e1) = f1 ( (a, x)) t e - in (b,t1,e1) + (\a t e f -> + let ((b, x),t1,e1,f') = f1 (a, x) t e f + in (b,t1,e1,f') )) -- | The combinator 'sequenceA' sequentially composes a list @@ -309,6 +332,7 @@ + -- | Alternative version of 'Trafo' where the universal quantification -- over |s| is moved inside the quantification over |env2|. -- Note that the type variables |a| and |b| are now labelled with |s|, @@ -318,10 +342,12 @@ data TrafoE2 m t env1 a b = forall env2 . TrafoE2 (m env2) - (forall s . a s -> T env2 s -> Env t s env1 - -> (b s, T env1 s, Env t s env2) + (forall s . a s -> T env2 s -> Env t s env1 -> UpdFinalEnv t s + -> (b s, T env1 s, Env t s env2, UpdFinalEnv t s) ) +newtype UpdFinalEnv t s = Upd (FinalEnv t s -> FinalEnv t s) + -- | The function 'runTrafo2' takes as arguments the 'Trafo2' we want to run, meta-information -- for the empty environment, and an input value. -- The result of 'runTrafo2' (type 'Result') is the final environment (@Env t s s@) together @@ -336,9 +362,10 @@ case trafo of Trafo2 trf -> case trf m of TrafoE2 m2 f -> - let (rb, _, env2) = f a (T P.id) Empty - in Result m2 rb env2 + let (rb, _, env2, Upd upds) = f a (T P.id) Empty (Upd P.id) + in Result m2 rb (upds env2) + -- | The Trafo2 'newSRef2' takes a typed term as input, adds it to the environment -- and yields a reference pointing to this value. -- No meta-information on the environment is recorded by 'newSRef2'; @@ -348,12 +375,20 @@ = Trafo2 (\Unit -> TrafoE2 Unit - (\ta (T tr) env -> + (\ta (T tr) env upds -> ( tr Zero , T (tr P.. Suc) , Ext env ta + , upds ) ) ) + +-- | The function 'updateFinalEnv2' returns a 'Trafo2' that introduces a function +-- (@(UpdFinalEnv t)@) to update the final environment. +updateFinalEnv2 :: Trafo2 m t (UpdFinalEnv t) Unit +updateFinalEnv2 = Trafo2 $ \m -> (TrafoE2 m (\(Upd u') t e (Upd u) -> (Unit, t, e, (Upd $ u' P.. u)))) + + newtype Pair a b s = P (a s, b s) class Category2 cat where @@ -373,7 +408,7 @@ instance Category2 (Trafo2 m t) where - id2 = Trafo2 (\m -> TrafoE2 m (\a t e -> (a, t, e))) + id2 = Trafo2 (\m -> TrafoE2 m (\a t e u -> (a, t, e, u))) (.:.) (Trafo2 sb) (Trafo2 sa) = Trafo2 @@ -383,9 +418,9 @@ TrafoE2 m3 f2 -> TrafoE2 m3 - (\a t3s e1 -> let (b, t1s, e2) = f1 a t2s e1 - (c, t2s, e3) = f2 b t3s e2 - in (c, t1s, e3) + (\a t3s e1 u1 -> let (b, t1s, e2, u2) = f1 a t2s e1 u1 + (c, t2s, e3, u3) = f2 b t3s e2 u2 + in (c, t1s, e3, u3) )) @@ -395,7 +430,7 @@ instance Arrow2 (Trafo2 m t) where arr2 f - = Trafo2 (\m -> TrafoE2 m (\a t e -> (f a, t, e)) ) + = Trafo2 (\m -> TrafoE2 m (\a t e u -> (f a, t, e, u)) ) first2 (Trafo2 s) @@ -403,9 +438,9 @@ (\m1 -> case s m1 of TrafoE2 m2 f -> TrafoE2 m2 - (\(P (a, c)) t2s e1 -> - let (b,t12,e2) = f a t2s e1 - in (P (b, c),t12,e2) + (\(P (a, c)) t2s e1 u1 -> + let (b,t12,e2,u2) = f a t2s e1 u1 + in (P (b, c),t12,e2,u2) ) ) @@ -423,9 +458,9 @@ (\m -> case st m of TrafoE2 m1 f1 -> TrafoE2 m1 - (\a t e -> - let (P (b, x),t1,e1) = f1 (P (a, x)) t e - in (b,t1,e1) + (\a t e u -> + let (P (b, x),t1,e1,u1) = f1 (P (a, x)) t e u + in (b,t1,e1,u1) ) )