TTTAS 0.2 → 0.2.1
raw patch · 11 files changed
+49/−1001 lines, 11 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Language.TTTAS: (.:.) :: (Category2 cat) => cat b c -> cat a b -> cat a c
- Language.TTTAS: (>>>>) :: (Category2 cat) => cat a b -> cat b c -> cat a c
- Language.TTTAS: class Category2 cat
- Language.TTTAS: id2 :: (Category2 cat) => cat a a
+ Language.TTTAS: instance Functor (TrafoE m t s e a)
- Language.TTTAS: Trafo :: (forall env1. m env1 -> TrafoE m t s a b env1) -> Trafo m t s a b
+ Language.TTTAS: Trafo :: (forall env1. m env1 -> TrafoE m t s env1 a b) -> Trafo m t s a b
- Language.TTTAS: Trafo2 :: (forall env1. m env1 -> TrafoE2 m t a b env1) -> Trafo2 m t a b
+ Language.TTTAS: Trafo2 :: (forall env1. m env1 -> TrafoE2 m t env1 a b) -> Trafo2 m t a b
- 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 a b env1
+ 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: 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 a b env1
+ 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: castSRef :: m e -> Ref a e -> TrafoE m t s x (Ref a s) e
+ Language.TTTAS: castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s)
- Language.TTTAS: data TrafoE m t s a b env1
+ Language.TTTAS: data TrafoE m t s env1 a b
- Language.TTTAS: data TrafoE2 m t a b env1
+ Language.TTTAS: data TrafoE2 m t env1 a b
- Language.TTTAS: extEnv :: m (e, a) -> TrafoE m t s (t a s) (Ref a s) e
+ Language.TTTAS: extEnv :: m (e, a) -> TrafoE m t s e (t a s) (Ref a s)
- Language.TTTAS: updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s i (Ref a s) e
+ Language.TTTAS: updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s e i (Ref a s)
Files
- TTTAS.cabal +2/−2
- examples/.svn/all-wcprops +0/−17
- examples/.svn/entries +0/−52
- examples/.svn/format +0/−1
- examples/.svn/text-base/CSE.hs.svn-base +0/−196
- examples/.svn/text-base/CSE2.hs.svn-base +0/−279
- src/.svn/all-wcprops +0/−11
- src/.svn/entries +0/−40
- src/.svn/format +0/−1
- src/.svn/text-base/TTTAS.hs.svn-base +0/−390
- src/Language/TTTAS.hs +47/−12
TTTAS.cabal view
@@ -1,7 +1,7 @@ cabal-version: >=1.2 build-type: Simple name: TTTAS-version: 0.2+version: 0.2.1 license: LGPL license-file: COPYRIGHT maintainer: Arthur Baars <abaars@iti.upv.es>@@ -13,7 +13,7 @@ copyright: Universiteit Utrecht build-depends: base, haskell98 exposed-modules: Language.TTTAS -extensions: Arrows, GADTs+extensions: Arrows, GADTs, CPP hs-source-dirs: src extra-source-files: README, LICENSE-LGPL, TTTAS.bib ghc-options: -Wall
− examples/.svn/all-wcprops
@@ -1,17 +0,0 @@-K 25-svn:wc:ra_dav:version-url-V 45-/repos/TTTAS/!svn/ver/176/libs/TTTAS/examples-END-CSE.hs-K 25-svn:wc:ra_dav:version-url-V 52-/repos/TTTAS/!svn/ver/176/libs/TTTAS/examples/CSE.hs-END-CSE2.hs-K 25-svn:wc:ra_dav:version-url-V 53-/repos/TTTAS/!svn/ver/176/libs/TTTAS/examples/CSE2.hs-END
− examples/.svn/entries
@@ -1,52 +0,0 @@-8--dir-182-https://svn.cs.uu.nl:12443/repos/TTTAS/libs/TTTAS/examples-https://svn.cs.uu.nl:12443/repos/TTTAS----2008-11-10T15:55:53.352787Z-176-mviera---svn:special svn:externals svn:needs-lock------------c177dbc6-12b5-11dd-94d1-a1da357961af--CSE.hs-file-----2008-11-19T13:40:29.000000Z-9a16f565cd0f7f036f6bfbb5b623041b-2008-11-10T15:55:53.352787Z-176-mviera--CSE2.hs-file-----2008-11-19T13:40:29.000000Z-54f25ea2c292cf812b41a30d7b929569-2008-11-10T15:55:53.352787Z-176-mviera-
− examples/.svn/format
@@ -1,1 +0,0 @@-8
− examples/.svn/text-base/CSE.hs.svn-base
@@ -1,196 +0,0 @@-{-# OPTIONS -fglasgow-exts -farrows #-}--module CSE where--import TTTAS-import Prelude hiding (lookup)-import Control.Arrow--data Expr a env where- Var :: Ref a env -> Expr a env- IntVal :: Int -> Expr Int env- BoolVal :: Bool -> Expr Bool env - Cons :: Expr a env -> Expr [a] env - -> Expr [a] env- Nil :: Expr [a] env- Add :: Expr Int env -> Expr Int env - -> Expr Int env- LessThan :: Expr Int env -> Expr Int env - -> Expr Bool env - If :: Expr Bool env -> Expr a env - -> Expr a env -> Expr a env--eval :: Expr a env -> env -> a-eval (Var r) e = lookup r e-eval (IntVal i) _ = i-eval (BoolVal b) _ = b-eval (Add x y) e = eval x e + eval y e-eval (Cons x y) e = eval x e : eval y e-eval Nil _ = []-eval (LessThan x y) e = eval x e < eval y e-eval (If x y z) e = if eval x e - then eval y e- else eval z e--type Decls env = Env Expr env env--data TDecls env = forall env' . TDecls (Decls env') - (T env env')--a = Suc Zero-b = Zero-exampledecls :: Decls (((),Int),Int)-exampledecls = - Empty `Ext` (IntVal 4) - `Ext` (Add (Add (Var a) (IntVal 4)) - (Add (Var a) (IntVal 4)))--resdecls :: TDecls (((),Int),Int)-resdecls = cse exampledecls--evalDecls :: Decls env -> env-evalVar :: Ref a env -> TDecls env -> a-evalVar var (TDecls ds (T tt))- = lookup (tt var) (evalDecls ds)--value_a = evalVar a resdecls-value_b = evalVar b resdecls--evalDecls (ds :: Decls env) = - let result :: env- result = evalD ds- evalD :: Env Expr env def -> def- evalD Empty = ()- evalD (Ext ds e) = (evalD ds,eval e result)- in result--resdecls2 :: TDecls (((),Int),Int) -resdecls2 = -- TDecls- ( Empty `Ext` (IntVal 4) - `Ext` (Add (Var (Suc (Suc Zero))) - (Var (Suc (Suc Zero))))- `Ext` (Add (Var (Suc Zero)) - (Var (Suc Zero)))- )- ( T (\ref -> case ref of - Zero -> Zero - Suc Zero -> Suc (Suc Zero))- :: T (((), Int), Int) ((((), Int), Int), Int))--instance Show (Ref a env) where- show x = "#" ++ (show $ refint x) -refint :: Ref a env -> Int-refint Zero = 0-refint (Suc x) = 1 + refint x-instance Show (Expr a env) where- show (Var r) = "v" ++ (show $ refint r)- show (IntVal i) = show i- show (BoolVal i) = show i- show (Add x y) = "(" ++ show x ++ "+"++ show y ++ ")"- show (LessThan x y) = "(" ++ show x ++ "<"++ show y ++ ")"- show (If x y z) = "if" ++ show x ++ "then"++ show y ++ "else" ++ show z--equals :: Expr a env -> Expr b env -> Maybe (Equal a b)-equals (Var r1) (Var r2) = match r1 r2-equals (IntVal i1) (IntVal i2) - | i1==i2 = Just Eq-equals (LessThan x1 y1) (LessThan x2 y2) - = do Eq <- equals x1 x2 - Eq <- equals y1 y2 - return Eq --equals (BoolVal b1) (BoolVal b2) - | b1==b2 = Just Eq-equals (Add x1 y1) (Add x2 y2) = do- Eq <- equals x1 x2- Eq <- equals y1 y2 - return Eq -equals (If x1 y1 z1) (If x2 y2 z2) - = do- Eq <- equals x1 x2- Eq <- equals y1 y2 - Eq <- equals z1 z2 - return Eq -equals _ _ = Nothing--newtype Memo env env'- = Memo - ( forall x . Expr x env - -> Maybe (Ref x env')- )--emptyMemo :: Memo env ()-emptyMemo = Memo (const Nothing)--type TrafoCSE env = Trafo (Memo env) Expr--insertIfNew :: forall s a env . Expr a env - -> TrafoCSE env s (Expr a s) (Ref a s)-insertIfNew e = - Trafo- (\(Memo m :: Memo env env') -> case m e of- Nothing -> extEnv (extMemo e (Memo m)) - Just r -> castSRef (Memo m) r - )- -extMemo :: Expr a env -> Memo env env' - -> Memo env (env',a)-extMemo e (Memo m) - = Memo (\s -> case equals e s of- Just Eq -> Just Zero- Nothing -> fmap Suc (m s)- ) --app_cse :: Expr a env - -> TrafoCSE env s (T env s) (Ref a s) -app_cse (Var r) = proc (T tenv_s) -> - returnA -< tenv_s r--app_cse e@(IntVal i) = proc _ -> - insertIfNew e -< IntVal i --app_cse e@(LessThan x y) - = proc tt -> - do l <- app_cse x -< tt- r <- app_cse y -< tt- insertIfNew e -< LessThan (Var l) (Var r)-app_cse e@(BoolVal b) = proc _ -> - insertIfNew e -< BoolVal b -app_cse e@(Add x y) = proc tt -> - do l <- app_cse x -< tt- r <- app_cse y -< tt- insertIfNew e -< Add (Var l) (Var r)- -app_cse e@(If x y z) = proc tt -> - do b <- app_cse x -< tt- l <- app_cse y -< tt- r <- app_cse z -< tt- insertIfNew e -< If (Var b) (Var l) (Var r)- -cse_env :: Env Expr env env'- -> TrafoCSE env s- (T env s) - (Env Ref s env')--cse_env Empty = proc _ -> returnA -< Empty -cse_env (Ext es e) = proc tt ->- do renv <- cse_env es -< tt- r <- app_cse e -< tt- returnA -< Ext renv r --refTransformer :: Env Ref s env -> T env s-refTransformer refs = T (\r -> lookupEnv r refs)--trafo :: Decls env -> TrafoCSE env s () (T env s)-trafo decls = proc _ -> - mdo let tt = refTransformer refs- refs <- cse_env decls -< tt- returnA -< tt--cse :: forall env . Decls env -> TDecls env-cse decls- = case runTrafo (trafo decls) emptyMemo () of- Result _ t env -> TDecls env t-
− examples/.svn/text-base/CSE2.hs.svn-base
@@ -1,279 +0,0 @@-{-# OPTIONS -fglasgow-exts #-}-module CSE2 where-- import TTTAS--- data Expr1 a where- IntVal1 :: Int -> Expr1 Int- BoolVal1 :: Bool -> Expr1 Bool- Add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int- LessThan1 :: Expr1 Int -> Expr1 Int -> Expr1 Bool- If1 :: Expr1 Bool -> Expr1 a -> Expr1 a -> Expr1 a --- data Expr a env where- Var :: Ref a env -> Expr a env- IntVal :: Int -> Expr Int env- BoolVal :: Bool -> Expr Bool env - Add :: Expr Int env -> Expr Int env - -> Expr Int env- LessThan :: Expr Int env -> Expr Int env- -> Expr Bool env - If :: Expr Bool env -> Expr a env - -> Expr a env -> Expr a env-- -----------------------------EASY VERSION (Expr1 -> Env)- - newtype MapExpr1 env2- = MapExpr1 - ( forall x . Expr1 x - -> Maybe (Ref x env2)- )- - emptyExpr1 :: MapExpr1 env2 - emptyExpr1 = MapExpr1 (const Nothing)-- type TrafoCSE1 inp out = Trafo2 MapExpr1 Expr inp out-- data FinalExprs = forall env. FinalExprs (Env Expr env env)-- cse1 :: Expr1 t -> FinalExprs- cse1 e- = let result = runTrafo2 (app_cse1 e) emptyExpr1 undefined- in case result of - Result _ _ envs -> FinalExprs envs--- app_cse1 :: Expr1 a -> TrafoCSE1 t (Ref a) - app_cse1 e@(IntVal1 i) = arr2 (const (IntVal i)) - >>>> insertExpr1 e - app_cse1 e@(BoolVal1 b) = arr2 (const (BoolVal b)) - >>>> insertExpr1 e - app_cse1 e@(Add1 x y) = (app_cse1 x &&&& app_cse1 y) - >>>> arr2 (\(P (l,r)) -> Add (Var l) (Var r)) - >>>> insertExpr1 e- app_cse1 e@(LessThan1 x y) - = (app_cse1 x &&&& app_cse1 y) - >>>> arr2 (\(P (l,r)) -> LessThan (Var l) (Var r))- >>>> insertExpr1 e- app_cse1 e@(If1 x y z) = (app_cse1 x &&&& app_cse1 y &&&& app_cse1 z) - >>>> arr2 (\(P (P (b,l),r)) -> If (Var b) (Var l) (Var r)) - >>>> insertExpr1 e-- insertExpr1 :: Expr1 a -> TrafoCSE1 (Expr a) (Ref a)- insertExpr1 e = - Trafo2- (\(MapExpr1 m) -> case m e of- Nothing -> - case newERef1 e- of Trafo2 step -> step (MapExpr1 m)- Just r -> TrafoE2 (MapExpr1 m) - (\e (T t) env1 -> (t r, T t, env1))- )-- newERef1 :: Expr1 a - -> TrafoCSE1 (Expr a) (Ref a)- newERef1 e =- Trafo2 - (\(MapExpr1 m :: MapExpr1 env1) ->- let m2 = MapExpr1 (\s -> case matchExpr1 e s of- Just Eq -> Just Zero- Nothing -> fmap Suc (m s)- )- in TrafoE2 m2 - (\e (T t) env1 -> ( t Zero- , T (t . Suc) - , Ext env1 e- ) ) )-- matchExpr1 :: Expr1 a -> Expr1 b - -> Maybe (Equal a b)- matchExpr1 (IntVal1 i1) (IntVal1 i2) - | i1==i2 = Just Eq- matchExpr1 (BoolVal1 b1) (BoolVal1 b2) - | b1==b2 = Just Eq- matchExpr1 (Add1 x1 y1) (Add1 x2 y2) - = do- Eq <- matchExpr1 x1 x2- Eq <- matchExpr1 y1 y2 - return Eq - matchExpr1 (LessThan1 x1 y1) (LessThan1 x2 y2) - = do- Eq <- matchExpr1 x1 x2- Eq <- matchExpr1 y1 y2 - return Eq - matchExpr1 (If1 x1 y1 z1) (If1 x2 y2 z2) - = do- Eq <- matchExpr1 x1 x2- Eq <- matchExpr1 y1 y2 - Eq <- matchExpr1 z1 z2 - return Eq - matchExpr1 _ _ = Nothing-- --- little test1- n1 x = IntVal1 x- env1 = Add1 (Add1 (n1 2) (n1 3)) (Add1 (n1 4) (Add1 (n1 2) (n1 3)))-- res1 = show $ cse1 env1--- ----------------------------MORE COMPLICATED VERSION (Env -> Env)---- newtype MapExpr env env2- = MapExpr - ( forall x . Expr x env - -> Maybe (Ref x env2)- )-- emptyExpr :: MapExpr env env2 - emptyExpr = MapExpr (const Nothing)-- initExpr :: TrafoCSE env a b - -> Trafo2 Unit Expr a b- initExpr (Trafo2 st)- = Trafo2 (\_ -> case st emptyExpr of- TrafoE2 _ f -> TrafoE2 Unit f- )-- type TrafoCSE env inp out = Trafo2 (MapExpr env) Expr inp out--- newtype Mapping old new - = Mapping (Env Ref new old) -- map2trans :: Mapping env s -> T env s- map2trans (Mapping env) - = T (\r -> (lookupEnv r env))---- cse :: Env Expr env env -> FinalExprs- cse e- = let result = runTrafo2 - ( loop2 $ second2 $- arr2 (\menv_s -> map2trans menv_s) >>>> cse_env e - )- Unit -- meta-data- undefined -- input- in case result of - Result _ _ env -> FinalExprs env--- cse_env :: Env Expr env env'- -> Trafo2 Unit - Expr- (T env) - (Mapping env')-- cse_env (Ext es e) = (initExpr (app_cse e) &&&& cse_env es) - >>>> arr2 (\(P (r, (Mapping renv)))- -> Mapping (Ext renv r)- )- cse_env Empty = arr2 (const (Mapping Empty)) --- app_cse :: Expr a env -> TrafoCSE env (T env) (Ref a) - app_cse (Var r) = arr2 (\(T tenv_s) -> tenv_s r)- app_cse e@(IntVal i) = arr2 (const (IntVal i)) - >>>> insertExpr e - app_cse e@(BoolVal b) = arr2 (const (BoolVal b)) - >>>> insertExpr e - app_cse e@(Add x y) = (app_cse x &&&& app_cse y) - >>>> arr2 (\(P (l,r)) -> Add (Var l) (Var r)) - >>>> insertExpr e- app_cse e@(LessThan x y) - = (app_cse x &&&& app_cse y) - >>>> arr2 (\(P (l,r)) -> LessThan (Var l) (Var r))- >>>> insertExpr e- app_cse e@(If x y z) = (app_cse x &&&& app_cse y &&&& app_cse z) - >>>> arr2 (\(P (P (b,l),r)) -> If (Var b) (Var l) (Var r)) - >>>> insertExpr e-- insertExpr :: Expr a env -> TrafoCSE env (Expr a) (Ref a)- insertExpr e = - Trafo2- (\(MapExpr m) -> case m e of- Nothing -> - case newERef e- of Trafo2 step -> step (MapExpr m)- Just r -> TrafoE2 (MapExpr m) - (\e (T t) env1 -> (t r, T t, env1))- )-- newERef :: Expr a env- -> TrafoCSE env (Expr a) (Ref a)- newERef e =- Trafo2 - (\(MapExpr m :: MapExpr env env1) ->- let m2 = MapExpr (\s -> case matchExpr e s of- Just Eq -> Just Zero- Nothing -> fmap Suc (m s)- )- in TrafoE2 m2 - (\e (T t) env1 -> ( t Zero- , T (t . Suc) - , Ext env1 e- ) ) )--- matchExpr :: Expr a env -> Expr b env - -> Maybe (Equal a b)- matchExpr (Var r1) (Var r2) = match r1 r2- matchExpr (IntVal i1) (IntVal i2) - | i1==i2 = Just Eq- matchExpr (BoolVal b1) (BoolVal b2) - | b1==b2 = Just Eq- matchExpr (Add x1 y1) (Add x2 y2) = do- Eq <- matchExpr x1 x2- Eq <- matchExpr y1 y2 - return Eq - matchExpr (LessThan x1 y1) (LessThan x2 y2) - = do- Eq <- matchExpr x1 x2- Eq <- matchExpr y1 y2 - return Eq - matchExpr (If x1 y1 z1) (If x2 y2 z2) - = do- Eq <- matchExpr x1 x2- Eq <- matchExpr y1 y2 - Eq <- matchExpr z1 z2 - return Eq - matchExpr _ _ = Nothing--- --- little test2- vx = Var Zero- n x = IntVal x- env2 = Empty `Ext` (n 2)- `Ext` (Add (Add vx (n 3)) (Add (n 4) (Add vx (n 3))))- - res2 = show $ cse env2--- ------------------------- SHOW-- instance Show (Ref a env) where- show x = "#" ++ (show $ refint x)- - refint :: Ref a env -> Int- refint Zero = 0- refint (Suc x) = 1 + refint x-- instance Show (Expr a env) where- show (Var r) = show r- show (IntVal i) = show i- show (BoolVal i) = show i- show (Add x y) = "(" ++ show x ++ "+"++ show y ++ ")"- show (LessThan x y) = "(" ++ show x ++ "<"++ show y ++ ")"- show (If x y z) = "if" ++ show x ++ "then"++ show y ++ "else" ++ show z-- instance Show (Env Expr env1 env2) where- show (Ext es e) = (show e) ++ "|" ++ show es- show Empty = ""-- instance Show FinalExprs where- show (FinalExprs env) = show env-
− src/.svn/all-wcprops
@@ -1,11 +0,0 @@-K 25-svn:wc:ra_dav:version-url-V 40-/repos/TTTAS/!svn/ver/182/libs/TTTAS/src-END-TTTAS.hs-K 25-svn:wc:ra_dav:version-url-V 49-/repos/TTTAS/!svn/ver/182/libs/TTTAS/src/TTTAS.hs-END
− src/.svn/entries
@@ -1,40 +0,0 @@-8--dir-182-https://svn.cs.uu.nl:12443/repos/TTTAS/libs/TTTAS/src-https://svn.cs.uu.nl:12443/repos/TTTAS----2008-11-16T12:49:59.555940Z-182-emlempsi---svn:special svn:externals svn:needs-lock------------c177dbc6-12b5-11dd-94d1-a1da357961af--TTTAS.hs-file-----2008-11-19T13:40:28.000000Z-ffcb17fb9287eaeebae11573f5926849-2008-11-16T12:49:59.555940Z-182-emlempsi-
− src/.svn/format
@@ -1,1 +0,0 @@-8
− src/.svn/text-base/TTTAS.hs.svn-base
@@ -1,390 +0,0 @@-{-# OPTIONS -fglasgow-exts -farrows #-} - -{-| - Library for Typed Transformations of Typed Abstract Syntax. - - The library is documented in the paper: /Typed Transformations of Typed Abstract Syntax/ - - Bibtex entry: <http://www.cs.uu.nl/wiki/bin/viewfile/Center/TTTAS?rev=1;filename=TTTAS.bib> - - For more documentation see the TTTAS webpage: - <http://www.cs.uu.nl/wiki/bin/view/Center/TTTAS>. --} - -module TTTAS ( - -- * Typed References and Environments - - -- ** Typed References - Ref(..), Equal(..), - match, lookup, update, - - -- ** Declarations - Env(..), FinalEnv, T(..), - lookupEnv, updateEnv, - - -- * Transformation Library - - -- ** Trafo - Trafo(..), TrafoE(..), - - -- ** Create New References - Unit(..), - newSRef, extEnv, castSRef, updateSRef, - - -- ** Run a Trafo - Result(..), - runTrafo, - - -- ** Other Combinators - sequenceA, - - -- * Alternative Transformation Library - - -- ** Trafo2 - Trafo2(..), TrafoE2(..), - - -- ** Create New References - newSRef2, - - -- ** Run a Trafo2 - runTrafo2, - - -- ** Arrow-style Combinators - Pair(..), Arrow2(..), ArrowLoop2(..), - List(..), sequenceA2 - ) where - -import Unsafe.Coerce ( unsafeCoerce ) -import Prelude hiding (lookup) -import Control.Arrow - - --- | The 'Ref' type for represents typed indices which are --- labeled with both the type of value to which they --- refer and the type of the environment (a nested --- Cartesian product, growing to the right) in which --- this value lives. - -- The constructor 'Zero' expresses that the first - -- element of the environment has to be of type @a@. - -- The constructor 'Suc' does not care about the type - -- of the first element in the environment, - -- being polymorphic in the type @b@. -data Ref a env where - Zero :: Ref a (env',a) - Suc :: Ref a env' -> Ref a (env',b) - --- | The 'Equal' type encodes type equality. -data Equal :: * -> * -> * where - Eq :: Equal a a - --- | The function 'match' compares two references for equality. --- If they refer to the same element in the environment --- the value @Just Eq@ is returned, expressing the fact that --- the types of the referred values are the same too. -match :: Ref a env -> Ref b env -> Maybe (Equal a b) -match Zero Zero = Just Eq -match (Suc x) (Suc y) = match x y -match _ _ = Nothing - --- | The function 'lookup' returns the element indexed in the --- environment parameter by the 'Ref' parameter. The types --- guarantee that the lookup succeeds. -lookup :: Ref a env -> env -> a -lookup Zero (_,a) = a -lookup (Suc r) (e,_) = lookup r e - --- | The function 'update' takes an additional function as --- argument, which is used to update the value the --- reference addresses. -update :: (a -> a) -> Ref a env -> env -> env -update f Zero (e,a) = (e,f a) -update f (Suc r) (e,x) = (update f r e,x) - - --- | The type @Env term use def@ represents a sequence of --- instantiations of type @forall a. term a use@, where --- all the instances of @a@ are stored in the type parameter --- @def@. The type @use@ is a sequence containing the --- types to which may be referred from within terms of type --- @term a use@. -data Env term use def where - Empty :: Env t use () - Ext :: Env t use def' -> t a use - -> Env t use (def',a) - - -lookupEnv :: Ref a env -> Env t s env -> t a s -lookupEnv Zero (Ext _ t) = t -lookupEnv (Suc r) (Ext ts _) = lookupEnv r ts - -updateEnv :: (t a s -> t a s) -> Ref a env - -> Env t s env -> Env t s env -updateEnv f Zero (Ext ts t) - = Ext ts (f t) -updateEnv f (Suc r) (Ext ts t) - = Ext (updateEnv f r ts) t - --- | 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 --- to terms representing the right type. This kind of --- environment is the /final environment/ of a transformation. -type FinalEnv t usedef = Env t usedef usedef - --- | The type 'T' encodes a 'Ref'-transformer. It is usually used --- to transform references from an actual environment to --- the final one. -newtype T e s = T {unT :: forall x . Ref x e -> Ref x s} - --- | The type 'Trafo' is the type of the transformation steps on a heterogeneous collection. --- The argument @m@ stands for the type of the meta-data. --- A |Trafo| takes the meta-data on the current environment |env1| as input and --- yields meta-data for the (possibly extended) environment |env2|. --- The type @t@ is the type of the terms stored in the environment. --- The type variable @s@ represents the type of the final result, which we do expose. --- Its role is similar to the @s@ in the type @ST s a@. --- The arguments @a@ and @b@ are the Arrow's input and output, respectively. -data Trafo m t s a b = - Trafo (forall env1 . m env1 -> TrafoE m t s a b env1) - --- | The type 'TrafoE' is used to introduce an existential quantifier into --- 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. -data TrafoE m t s a b env1 = - forall env2 . TrafoE ( m env2) - ( a -> T env2 s -> Env t s env1 - -> ( b, T env1 s, Env t s env2) - ) - -data Unit s = Unit - --- | The Trafo 'newSRef' 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 'newSRef'; --- therefore we use the type 'Unit' for the meta-data. -newSRef :: Trafo Unit t s (t a s) (Ref a s) -newSRef - = Trafo (\ _-> extEnv Unit) - - --- | The function 'extEnv' returns a 'TrafoE' that extends the current environment. -extEnv :: m (e,a) -> TrafoE m t s (t a s) (Ref a s) e -extEnv m = TrafoE m $ \ta (T tr) env -> (tr Zero, T (tr . Suc), Ext env ta ) - --- | 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 x (Ref a s) e -castSRef m r = TrafoE m $ (\ _ (T t) decls -> (t r, T t, decls)) - --- | 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 i (Ref a s) e -updateSRef m r f = TrafoE m $ \i (T t) decls -> (t r, T t, updateEnv (f i) r decls) - - --- | 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. -data Result m t b - = forall s . Result (m s) (b s) (FinalEnv t s) - --- | The function 'runTrafo' takes as arguments the 'Trafo' we want to run, meta-information --- for the empty environment, and an input value. --- The result of 'runTrafo' (type 'Result') is the final environment (@Env t s s@) together --- with the resulting meta-data (@m s@), and the output value (@b s@). --- The rank-2 type for 'runTrafo' ensures that transformation steps cannot make --- any assumptions about the type of final environment (@s@). -runTrafo :: (forall s . Trafo m t s a (b s)) -> m () -> a - -> Result m t b -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) -> - Result (unsafeCoerce m2) - rb - (unsafeCoerce env2) - - -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)) ) - - -- |(>>>) :: Trafo m t s a b -> Trafo m t s b c -> Trafo m t s a c| - Trafo t1 >>> Trafo t2 = - Trafo - (\m1 -> case t1 m1 of - TrafoE m2 f1 -> case t2 m2 of - 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) - ) - ) - - -- |first :: Trafo m t s a b -> Trafo m t s (a, c) (b, c)| - first (Trafo tr) - = Trafo (\m1 -> case tr m1 of - TrafoE m2 f -> - TrafoE - m2 - (\ ~(a,c) tt env1 -> - let (b,tt1,env2) = f a tt env1 - in ((b,c),tt1, env2))) - -instance ArrowLoop (Trafo m t s) where - -- |loop :: Trafo m t s (a, x) (b, x) -> Trafo m t s a b| - loop (Trafo st) = - Trafo - (\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) - )) - --- | The combinator 'sequenceA' sequentially composes a list --- of 'Trafo's into a 'Trafo' that yields a list of outputs. --- Its use is analogous to the combinator 'sequence' combinator --- for 'Monad's. -sequenceA :: [Trafo m t s a b] -> Trafo m t s a [b] -sequenceA [] = arr (const []) -sequenceA (x:xs) - = proc a -> - do b <- x -< a - bs <- sequenceA xs -< a - returnA -< (b:bs) - - - - --- | 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|, --- and hence have kind |(* -> *)|. -data Trafo2 m t a b = - Trafo2 (forall env1 . m env1 -> TrafoE2 m t a b env1) -data TrafoE2 m t a b env1 = - 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) - ) - --- | 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 --- with the resulting meta-data (@m s@), and the output value (@b s@). --- The rank-2 type for 'runTrafo2' ensures that transformation steps cannot make --- any assumptions about the type of final environment (@s@). --- It is an alternative version of 'runTrafo' which does not use --- 'unsafeCoerce'. -runTrafo2 :: Trafo2 m t a b -> m () -> (forall s . a s) - -> Result m t b -runTrafo2 trafo m a = - case trafo of - Trafo2 trf -> case trf m of - TrafoE2 m2 f -> - let (rb, _, env2) = f a (T id) Empty - in Result m2 rb 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'; --- therefore we use the type 'Unit' for the meta-data. -newSRef2 :: Trafo2 Unit t (t a) (Ref a) -newSRef2 - = Trafo2 - (\Unit -> TrafoE2 - Unit - (\ta (T tr) env -> - ( tr Zero - , T (tr . Suc) - , Ext env ta - ) ) ) - -newtype Pair a b s = P (a s, b s) - -class Arrow2 arr where - arr2 :: (forall s . a s -> b s) -> arr a b - (>>>>) :: arr a b -> arr b c -> arr a c - first2 :: arr a b -> arr (Pair a c) (Pair b c) - second2 :: arr a b -> arr (Pair c a) (Pair c b) - (****) :: arr a b -> arr a' b' - -> arr (Pair a a') (Pair b b') - (&&&&) :: arr a b -> arr a b' -> arr a (Pair b b') - -class Arrow2 arr => ArrowLoop2 arr where - loop2 :: arr (Pair a c) (Pair b c) -> arr a b - - -instance Arrow2 (Trafo2 m t) where - arr2 f - = Trafo2 (\m -> TrafoE2 m (\a t e -> (f a, t, e)) ) - - (>>>>) (Trafo2 sa) (Trafo2 sb) = - Trafo2 - (\m1 -> - case sa m1 of - TrafoE2 m2 f1 -> case sb m2 of - 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) - )) - - first2 (Trafo2 s) - = Trafo2 - (\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) - ) - ) - - second2 f = arr2 swap >>>> first2 f >>>> arr2 swap - where swap ~(P (x, y)) = P (y, x) - - f **** g = first2 f >>>> second2 g - - f &&&& g = arr2 (\b -> P (b, b)) >>>> (f **** g) - - -instance ArrowLoop2 (Trafo2 m t) where - loop2 (Trafo2 st) = - Trafo2 - (\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) - ) - ) - - -newtype List a s = List [a s] - --- | The combinator 'sequenceA2' sequentially composes a list --- of 'Trafo2's into a 'Trafo2' that yields a 'List' of outputs. --- Its use is analogous to the combinator 'sequence' combinator --- for 'Monad's. -sequenceA2 :: [Trafo2 m t a b] -> Trafo2 m t a (List b) -sequenceA2 [] = arr2 (const (List [])) -sequenceA2 (x:xs) - = (x &&&& sequenceA2 xs) >>>> - arr2 (\(P (a,List as)) -> List (a:as)) -
src/Language/TTTAS.hs view
@@ -1,4 +1,5 @@ {-# OPTIONS -fglasgow-exts -XArrows #-} +{-# LANGUAGE CPP #-} {-| Library for Typed Transformations of Typed Abstract Syntax. @@ -50,16 +51,25 @@ runTrafo2, -- ** Arrow-style Combinators - Pair(..), Category2(..), Arrow2(..), (>>>>), ArrowLoop2(..), + Pair(..), Arrow2(..), ArrowLoop2(..), List(..), sequenceA2 ) where import Unsafe.Coerce ( unsafeCoerce ) -import Prelude hiding (lookup,id,(.)) import qualified Prelude as P -import Control.Arrow -import Control.Category +#if __GLASGOW_HASKELL__ >= 609 +import Control.Category +import Prelude hiding (lookup,(.), id) +#endif + +import Control.Arrow +#if __GLASGOW_HASKELL__ < 609 + hiding (pure) +import Prelude hiding (lookup) +#endif + + -- | The 'Ref' type for represents typed indices which are -- labeled with both the type of value to which they -- refer and the type of the environment (a nested @@ -146,7 +156,7 @@ -- Its role is similar to the @s@ in the type @ST s a@. -- The arguments @a@ and @b@ are the Arrow's input and output, respectively. data Trafo m t s a b = - Trafo (forall env1 . m env1 -> TrafoE m t s a b env1) + Trafo (forall env1 . m env1 -> TrafoE m t s env1 a b) -- | The type 'TrafoE' is used to introduce an existential quantifier into -- the definition of 'Trafo'. @@ -156,7 +166,7 @@ -- 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. -data TrafoE m t s a b env1 = +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) @@ -174,20 +184,24 @@ -- | The function 'extEnv' returns a 'TrafoE' that extends the current environment. -extEnv :: m (e,a) -> TrafoE m t s (t a s) (Ref a s) e +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 ) -- | 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 x (Ref a s) e +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)) -- | 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 i (Ref a s) e +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) +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') + -- | 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. data Result m t b @@ -210,8 +224,10 @@ rb (unsafeCoerce env2) +#if __GLASGOW_HASKELL__ >= 609 + instance Category (Trafo m t s) where - -- |(.) :: Trafo m t s a b -> Trafo m t s b c -> Trafo m t s a c| + -- |(.) :: Trafo m t s b c -> Trafo m t s a b -> Trafo m t s a c| Trafo t2 . Trafo t1 = Trafo (\m1 -> case t1 m1 of @@ -229,13 +245,32 @@ -- |id :: Trafo m t s a a| id = Trafo (\m -> TrafoE m (\a t e -> (a, t, e)) ) +#endif + 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)) ) +#if __GLASGOW_HASKELL__ < 609 + Trafo t1 >>> Trafo t2 = + Trafo + (\m1 -> case t1 m1 of + TrafoE m2 f1 -> case t2 m2 of + 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) + ) + ) + +#endif + -- |first :: Trafo m t s a b -> Trafo m t s (a, c) (b, c)| first (Trafo tr) = Trafo (\m1 -> case tr m1 of @@ -279,8 +314,8 @@ -- Note that the type variables |a| and |b| are now labelled with |s|, -- and hence have kind |(* -> *)|. data Trafo2 m t a b = - Trafo2 (forall env1 . m env1 -> TrafoE2 m t a b env1) -data TrafoE2 m t a b env1 = + Trafo2 (forall env1 . m env1 -> TrafoE2 m t env1 a b) +data TrafoE2 m t env1 a b = forall env2 . TrafoE2 (m env2) (forall s . a s -> T env2 s -> Env t s env1