diff --git a/TTTAS.cabal b/TTTAS.cabal --- a/TTTAS.cabal +++ b/TTTAS.cabal @@ -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 @@ -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 diff --git a/examples/.svn/all-wcprops b/examples/.svn/all-wcprops deleted file mode 100644 --- a/examples/.svn/all-wcprops +++ /dev/null @@ -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 diff --git a/examples/.svn/entries b/examples/.svn/entries deleted file mode 100644 --- a/examples/.svn/entries +++ /dev/null @@ -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 - diff --git a/examples/.svn/format b/examples/.svn/format deleted file mode 100644 --- a/examples/.svn/format +++ /dev/null @@ -1,1 +0,0 @@ -8 diff --git a/examples/.svn/text-base/CSE.hs.svn-base b/examples/.svn/text-base/CSE.hs.svn-base deleted file mode 100644 --- a/examples/.svn/text-base/CSE.hs.svn-base +++ /dev/null @@ -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 - diff --git a/examples/.svn/text-base/CSE2.hs.svn-base b/examples/.svn/text-base/CSE2.hs.svn-base deleted file mode 100644 --- a/examples/.svn/text-base/CSE2.hs.svn-base +++ /dev/null @@ -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 - diff --git a/src/.svn/all-wcprops b/src/.svn/all-wcprops deleted file mode 100644 --- a/src/.svn/all-wcprops +++ /dev/null @@ -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 diff --git a/src/.svn/entries b/src/.svn/entries deleted file mode 100644 --- a/src/.svn/entries +++ /dev/null @@ -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 - diff --git a/src/.svn/format b/src/.svn/format deleted file mode 100644 --- a/src/.svn/format +++ /dev/null @@ -1,1 +0,0 @@ -8 diff --git a/src/.svn/text-base/TTTAS.hs.svn-base b/src/.svn/text-base/TTTAS.hs.svn-base deleted file mode 100644 --- a/src/.svn/text-base/TTTAS.hs.svn-base +++ /dev/null @@ -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: - - For more documentation see the TTTAS webpage: - . --} - -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)) - diff --git a/src/Language/TTTAS.hs b/src/Language/TTTAS.hs --- a/src/Language/TTTAS.hs +++ b/src/Language/TTTAS.hs @@ -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