diff --git a/TTTAS.cabal b/TTTAS.cabal --- a/TTTAS.cabal +++ b/TTTAS.cabal @@ -1,7 +1,8 @@ cabal-version: >=1.2.3 build-type: Simple name: TTTAS -version: 0.4.2 + +version: 0.6.0 license: LGPL license-file: COPYRIGHT maintainer: Marcos Viera @@ -13,7 +14,8 @@ extra-source-files: README, LICENSE-LGPL, TTTAS.bib library build-depends: base >= 4 && < 5 - exposed-modules: Language.AbstractSyntax.TTTAS + exposed-modules: Language.AbstractSyntax.TTTAS, Language.AbstractSyntax.TTTAS2, + Language.AbstractSyntax.TTTAS.Common extensions: Arrows, KindSignatures, RankNTypes, GADTs, CPP hs-source-dirs: src ghc-options: -Wall diff --git a/examples/CSE.hs b/examples/CSE.hs deleted file mode 100644 --- a/examples/CSE.hs +++ /dev/null @@ -1,196 +0,0 @@ -{-# OPTIONS -fglasgow-exts -XGADTs -XArrows #-} - -module CSE where - -import Language.AbstractSyntax.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 _ -> - do rec 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/CSE1.hs b/examples/CSE1.hs new file mode 100644 --- /dev/null +++ b/examples/CSE1.hs @@ -0,0 +1,202 @@ +{-# LANGUAGE ExistentialQuantification, ScopedTypeVariables, RankNTypes, GADTs, Arrows #-} + + +module CSE where + +import Language.AbstractSyntax.TTTAS +import Prelude hiding (lookup) +import Control.Arrow + +ifThenElse c t e = case c of + True -> t + False -> e +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) + +data EmptyEnv s = EmptyEnv + +trafo :: Decls env -> TrafoCSE env s () (T env s) +trafo decls = proc _ -> + do rec 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/CSE2.hs b/examples/CSE2.hs --- a/examples/CSE2.hs +++ b/examples/CSE2.hs @@ -1,285 +1,206 @@ -{-# OPTIONS -fglasgow-exts -XGADTs #-} -module CSE2 where +{-# LANGUAGE ExistentialQuantification, ScopedTypeVariables, RankNTypes, GADTs, Arrows #-} - import Language.AbstractSyntax.TTTAS +-- We can't use arrow notation because RebindableSyntax +-- doesn't work well with Arrows (yet) +module CSE where - 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 +import Language.AbstractSyntax.TTTAS2 +import Prelude hiding (lookup) +-- import Control.Arrow +ifThenElse c t e = case c of + True -> t + False -> e +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 - 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 +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 - -----------------------------EASY VERSION (Expr1 -> Env) - - newtype MapExpr1 env2 - = MapExpr1 - ( forall x . Expr1 x - -> Maybe (Ref x env2) - ) - - emptyExpr1 :: MapExpr1 env2 - emptyExpr1 = MapExpr1 (const Nothing) +type Decls env = Env Expr env env - type TrafoCSE1 inp out = Trafo2 MapExpr1 Expr inp out +data TDecls env = forall env' . TDecls (Decls env') + (T env env') - data FinalExprs = forall env. FinalExprs (Env Expr 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))) - cse1 :: Expr1 t -> FinalExprs - cse1 e - = let result = runTrafo2 (app_cse1 e) emptyExpr1 undefined - in case result of - Result _ _ envs -> FinalExprs envs +resdecls :: TDecls (((),Int),Int) +resdecls = cse exampledecls - 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 +evalDecls :: Decls env -> env +evalVar :: Ref a env -> TDecls env -> a +evalVar var (TDecls ds (T tt)) + = lookup (tt var) (evalDecls ds) - 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 upds -> (t r, T t, env1, upds)) - ) +value_a = evalVar a resdecls +value_b = evalVar b resdecls - newERef1 :: Expr1 a - -> TrafoCSE1 (Expr a) (Ref a) - newERef1 e = - Trafo2 - (\(MapExpr1 m :: MapExpr1 env1) -> - let m2 = MapExpr1 (\s -> aux1 (matchExpr1 e s) m s) - in TrafoE2 m2 - (\e (T t) env1 upds -> ( t Zero - , T (t . Suc) - , Ext env1 e - , upds - ) ) ) +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 - aux1 :: Maybe (Equal a x) -> (Expr1 x -> Maybe (Ref x env1)) - -> Expr1 x -> Maybe (Ref x (env1,a)) - aux1 (Just Eq) _ _ = Just Zero - aux1 Nothing m s = fmap Suc (m s) +resdecls2 :: TDecls (((),Int),Int) +resdecls2 = - 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 + 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)) - --- little test1 - n1 x = IntVal1 x - env1 = Add1 (Add1 (n1 2) (n1 3)) (Add1 (n1 4) (Add1 (n1 2) (n1 3))) +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 - res1 = show $ cse1 env1 +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 - ----------------------------MORE COMPLICATED VERSION (Env -> Env) +newtype Memo env env' + = Memo + ( forall x . Expr x env + -> Maybe (Ref x env') + ) +emptyMemo :: Memo env () +emptyMemo = Memo (const Nothing) +type TrafoCSE2 env = Trafo (Memo env) Expr - newtype MapExpr env env2 - = MapExpr - ( forall x . Expr x env - -> Maybe (Ref x env2) - ) +insertIfNew :: forall s a env . Expr a env + -> TrafoCSE2 env (Expr a ) (Ref a ) +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) + ) - emptyExpr :: MapExpr env env2 - emptyExpr = MapExpr (const Nothing) +app_cse :: Expr a env + -> TrafoCSE2 env (T env) (Ref a) - initExpr :: TrafoCSE env a b - -> Trafo2 Unit Expr a b - initExpr (Trafo2 st) - = Trafo2 (\_ -> case st emptyExpr of - TrafoE2 _ f -> TrafoE2 Unit f - ) +app_cse (Var r) = arr (\(T tenv_s) -> tenv_s r) +app_cse e@(IntVal i) = arr (const (IntVal i)) + >>> insertIfNew e +app_cse e@(BoolVal b) = arr (const (BoolVal b)) + >>> insertIfNew e +app_cse e@(Add x y) = (app_cse x &&& app_cse y) + >>> arr (\(P (l,r)) -> Add (Var l) (Var r)) + >>> insertIfNew e - type TrafoCSE env inp out = Trafo2 (MapExpr env) Expr inp out +app_cse e@(LessThan x y) + = (app_cse x &&& app_cse y) + >>> arr (\(P (l,r)) -> LessThan (Var l) (Var r)) + >>> insertIfNew e - newtype Mapping old new - = Mapping (Env Ref new old) - - map2trans :: Mapping env s -> T env s - map2trans (Mapping env) - = T (\r -> (lookupEnv r env)) - +app_cse e@(If x y z) = (app_cse x &&& app_cse y &&& app_cse z) + >>> arr (\(P (P (b,l),r)) -> If (Var b) (Var l) (Var r)) + >>> insertIfNew e + +newtype EEnv r e1 e2 = EEnv (Env r e2 e1) - 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' + -> TrafoCSE2 env + (T env ) + (EEnv Ref env') - cse_env :: Env Expr env env' - -> Trafo2 Unit - Expr - (T env) - (Mapping env') +cse_env Empty = arr (const (EEnv Empty)) - cse_env (Ext es e) = (initExpr (app_cse e) &&&& cse_env es) - >>>> arr2 (\(P (r, (Mapping renv))) - -> Mapping (Ext renv r) +cse_env (Ext es e) = (app_cse e &&& cse_env es) + >>> arr (\(P (r, (EEnv renv))) + -> EEnv (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 upds -> (t r, T t, env1, upds)) - ) - - newERef :: Expr a env - -> TrafoCSE env (Expr a) (Ref a) - newERef e = - Trafo2 - (\(MapExpr m :: MapExpr env env1) -> - let m2 = MapExpr (\s -> aux (matchExpr e s) m s) - in TrafoE2 m2 - (\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)) - aux (Just Eq) _ _ = Just Zero - aux Nothing m s = fmap Suc (m s) +refTransformer :: Env Ref s env -> T env s +refTransformer refs = T (\r -> lookupEnv r refs) - 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 - +data EmptyEnv s = EmptyEnv - --- 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 +trafo :: Decls env -> TrafoCSE2 env EmptyEnv (T env ) +trafo decls = loop $ arr (\(P (_,EEnv refs)) -> refTransformer refs) >>> (arr id &&& cse_env decls) - ------------------------- 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 +cse :: forall env . Decls env -> TDecls env +cse decls + = case runTrafo (trafo decls) emptyMemo EmptyEnv of + Result _ t env -> TDecls env t diff --git a/src/Language/AbstractSyntax/TTTAS.hs b/src/Language/AbstractSyntax/TTTAS.hs --- a/src/Language/AbstractSyntax/TTTAS.hs +++ b/src/Language/AbstractSyntax/TTTAS.hs @@ -1,6 +1,6 @@ -{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs #-} -{-# LANGUAGE CPP #-} +{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs #-} + {-| Library for Typed Transformations of Typed Abstract Syntax. @@ -10,18 +10,15 @@ For more documentation see the TTTAS webpage: . + + For an example see examples/CSE1.hs + -} module Language.AbstractSyntax.TTTAS ( -- * Typed References and Environments - - -- ** Typed References - Ref(..), Equal(..), - match, lookup, update, - - -- ** Declarations - Env(..), FinalEnv, T(..), - lookupEnv, updateEnv, + module Language.AbstractSyntax.TTTAS.Common, + -- * Transformation Library @@ -29,136 +26,34 @@ Trafo(..), TrafoE(..), -- ** Create New References - Unit(..), newSRef, extEnv, castSRef, updateSRef, - -- ** Update the Final Environment - updateFinalEnv, + -- ** State-like operations on the Final Environment + getFinalEnv, putFinalEnv, updateFinalEnv, -- ** Run a Trafo - Result(..), runTrafo, -- ** Other Combinators - sequenceA, + sequenceA, - -- * Alternative Transformation Library - - -- ** Trafo2 - Trafo2(..), TrafoE2(..), - -- ** 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 ) -import qualified Prelude as P -#if __GLASGOW_HASKELL__ >= 609 -import Control.Category +#if __GLASGOW_HASKELL__ >= 710 +import Prelude hiding (lookup,(.), id, sequenceA) +#else import Prelude hiding (lookup,(.), id) -#endif +#endif +import Unsafe.Coerce ( unsafeCoerce ) +import Control.Category import Control.Arrow -#if __GLASGOW_HASKELL__ < 609 - hiding (pure) -import Prelude hiding (lookup) -#endif +import Language.AbstractSyntax.TTTAS.Common --- | 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 -lookupEnv _ _ = error "Error: The impossible happened!" - -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 -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 --- 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 @@ -167,6 +62,10 @@ -- 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 env1 a b) @@ -175,22 +74,20 @@ -- 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, 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@), +-- transformation starts and the "final environment" (@FinalEnv t s@) +-- with the updates thus far applied. +-- 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'. +-- environment, the environment (@Env t s env2@) constructed in this step and the final environment +-- (@FinalEnv t s@) possibly updated. data TrafoE m t s env1 a b = forall env2 . 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)) + ( a -> T env2 s -> Env t s env1 -> FinalEnv t s + -> ( b, T env1 s, Env t s env2, FinalEnv t s) ) -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'; @@ -200,20 +97,33 @@ = Trafo (\ _-> extEnv Unit) --- | The function 'updateFinalEnv' returns a 'Trafo' that introduces a function --- (@FinalEnv t s -> FinalEnv t s@) to update the final environment. + +-- | Change the final environment by the one passed in the input. +putFinalEnv :: Trafo m t s (FinalEnv t s) () +putFinalEnv = Trafo $ \m -> (TrafoE m (\fe t e _ -> ((), t, e, fe))) + +-- | Return as output the final environment. +getFinalEnv :: Trafo m t s () (FinalEnv t s) +getFinalEnv = Trafo $ \m -> (TrafoE m (\_ t e fe -> (fe, t, e, fe))) + +-- | The function 'updateFinalEnv' returns a 'Trafo' that updates the +-- final environment using the input function +-- (@FinalEnv t s -> FinalEnv t s@). updateFinalEnv :: Trafo m t s (FinalEnv t s -> FinalEnv t s) () -updateFinalEnv = Trafo $ \m -> (TrafoE m (\f' t e f -> ((), t, e, f' . f))) +updateFinalEnv = proc f -> + do fe <- getFinalEnv -< () + putFinalEnv -< f fe + -- Trafo $ \m -> (TrafoE m (\f t e fe -> ((), t, e, f fe))) -- | 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 f -> (tr Zero, T (tr P.. Suc), Ext env ta, f ) +extEnv m = TrafoE m $ \ta (T tr) env fe -> (tr Zero, T (tr . Suc), Ext env ta, fe ) -- | 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 f -> (t r, T t, decls, f)) +castSRef m r = TrafoE m $ (\ _ (T t) decls fe -> (t r, T t, decls, fe)) -- | The function 'updateSRef' returns a 'TrafoE' that updates the value pointed -- by the reference passed as parameter into the current environment. @@ -222,14 +132,11 @@ instance Functor (TrafoE m t s e a) where - 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') + fmap f (TrafoE m step) = TrafoE m $ \i t e fe -> case step i t e fe of + (i',t',e',fe') -> (f i',t',e',fe') --- | 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 @@ -240,15 +147,14 @@ -> 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 P.id of -- the function could also be passed as argument - (rb, _, env2, fenvs) -> - Result (unsafeCoerce m2) + TrafoE m2 f -> + let (rb, _, env2, fenv) = f a (T unsafeCoerce) Empty (unsafeCoerce env2) + in Result (unsafeCoerce m2) rb - (fenvs $ unsafeCoerce env2) + (unsafeCoerce fenv) -#if __GLASGOW_HASKELL__ >= 609 + instance Category (Trafo m t s) where -- |(.) :: Trafo m t s b c -> Trafo m t s a b -> Trafo m t s a c| Trafo t2 . Trafo t1 = @@ -268,32 +174,12 @@ -- |id :: Trafo m t s a a| id = Trafo (\m -> TrafoE m (\a t e f -> (a, t, e, f)) ) -#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 fs -> (f a, t, e, fs)) ) -#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 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'') - ) - ) - -#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 @@ -331,151 +217,4 @@ 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 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 -> 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 --- 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, 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'; --- 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 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 - id2 :: cat a a - (.:.) :: cat b c -> cat a b -> cat a c - -class Category2 arr => Arrow2 (arr :: (* -> *) -> (* -> *) -> *) where - arr2 :: (forall s . a s -> b s) -> arr a b - 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 Category2 (Trafo2 m t) where - id2 = Trafo2 (\m -> TrafoE2 m (\a t e u -> (a, t, e, u))) - - (.:.) (Trafo2 sb) (Trafo2 sa) = - Trafo2 - (\m1 -> - case sa m1 of - TrafoE2 m2 f1 -> case sb m2 of - TrafoE2 m3 f2 -> - TrafoE2 - m3 - (\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) - )) - - -(>>>>) :: Category2 cat => cat a b -> cat b c -> cat a c -f >>>> g = g .:. f - - -instance Arrow2 (Trafo2 m t) where - arr2 f - = Trafo2 (\m -> TrafoE2 m (\a t e u -> (f a, t, e, u)) ) - - - first2 (Trafo2 s) - = Trafo2 - (\m1 -> case s m1 of - TrafoE2 m2 f -> - TrafoE2 m2 - (\(P (a, c)) t2s e1 u1 -> - let (b,t12,e2,u2) = f a t2s e1 u1 - in (P (b, c),t12,e2,u2) - ) - ) - - second2 f = arr2 swap >>>> first2 f >>>> arr2 swap - where swap :: Pair c a s -> Pair a c s - 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 u -> - let (P (b, x),t1,e1,u1) = f1 (P (a, x)) t e u - in (b,t1,e1,u1) - ) - ) - - -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/AbstractSyntax/TTTAS/Common.hs b/src/Language/AbstractSyntax/TTTAS/Common.hs new file mode 100644 --- /dev/null +++ b/src/Language/AbstractSyntax/TTTAS/Common.hs @@ -0,0 +1,122 @@ +{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs #-} + + +{-| + 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 Language.AbstractSyntax.TTTAS.Common ( + -- * Typed References and Environments + + -- ** Typed References + Ref(..), Equal(..), + match, lookup, update, + + -- ** Declarations + Env(..), FinalEnv, T(..), + lookupEnv, updateEnv, + Unit(..), + Result(..), + + ) where + +import Prelude hiding (lookup) + + +-- | 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) + + +data Unit s = Unit + +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 +updateEnv f Zero (Ext ts t) + = 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 +-- 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 '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 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} + diff --git a/src/Language/AbstractSyntax/TTTAS2.hs b/src/Language/AbstractSyntax/TTTAS2.hs new file mode 100644 --- /dev/null +++ b/src/Language/AbstractSyntax/TTTAS2.hs @@ -0,0 +1,246 @@ +{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs #-} + + +{-| + 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: + . + + For an example see examples/CSE2.hs + + IMPORTANT: We would like to be able to use RebinadbleSyntax + to use Arrow's Syntax in this variant of TTTAS, + but this extension still doesn't work well with Arrows. +-} + +module Language.AbstractSyntax.TTTAS2 ( + -- * Typed References and Environments + module Language.AbstractSyntax.TTTAS.Common, + + -- * Transformation Library + + -- ** Trafo + Trafo(..), TrafoE(..), + + -- ** Create New References + newSRef, + extEnv, + castSRef, + updateSRef, + + -- ** State-like operations on the Final Environment + getFinalEnv, putFinalEnv, updateFinalEnv, + + -- ** Run a Trafo + runTrafo, + + -- ** Arrow-style Combinators + Pair(..), Arrow2(..), ArrowLoop2(..), + (>>>), + List(..), sequenceA, returnA + + ) where + +#if __GLASGOW_HASKELL__ >= 710 +import Prelude hiding (lookup, sequenceA) +#else +import Prelude hiding (lookup) +#endif + +import Language.AbstractSyntax.TTTAS.Common + + + + +-- | 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 Trafo m t a b = + Trafo (forall env1 . m env1 -> TrafoE m t env1 a b) +data TrafoE m t env1 a b = + forall env2 . TrafoE + (m env2) + (forall s . a s -> T env2 s -> Env t s env1 -> FinalEnv t s + -> (b s, T env1 s, Env t s env2, 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 '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'. +runTrafo :: Trafo m t a b -> m () -> (forall s . a s) + -> Result m t b +runTrafo trafo m a = + case trafo of + Trafo trf -> case trf m of + TrafoE m2 f -> + let (rb, _, env2, fenv) = f a (T id) Empty env2 + in Result m2 rb fenv + + +-- | 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. +newSRef :: Trafo Unit t (t a) (Ref a) +newSRef + = Trafo + (\Unit -> TrafoE + Unit + (\ta (T tr) env fenv -> + ( tr Zero + , T (tr . Suc) + , Ext env ta + , fenv + ) ) ) + + +-- | The function 'extEnv' returns a 'TrafoE' that extends the current environment. +extEnv :: m (e,a) -> TrafoE m t e (t a ) (Ref a ) +extEnv m = TrafoE m $ \ta (T tr) env fe -> (tr Zero, T (tr . Suc), Ext env ta, fe ) + +-- | 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 e x (Ref a) +castSRef m r = TrafoE m $ (\ _ (T t) decls fe -> (t r, T t, decls, fe)) + +data FUpd i t a = FUpd (forall s. i -> t a s -> t a s) +newtype SI i s = SI i + +-- | 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 -> FUpd i t a -> TrafoE m t e (SI i) (Ref a) +updateSRef m r (FUpd f) = TrafoE m $ \(SI i) (T t) decls fs -> (t r, T t, updateEnv (f i) r decls, fs) + + +newtype UpdFinalEnv t s = Upd (FinalEnv t s -> FinalEnv t s) + +newtype FinalEnv2 t s = Final (FinalEnv t s) + +-- | The function 'updateFinalEnv' returns a 'Trafo' that introduces a function +-- (@(UpdFinalEnv t)@) to update the final environment. +updateFinalEnv :: Trafo m t (UpdFinalEnv t) Unit +updateFinalEnv = Trafo $ \m -> (TrafoE m (\(Upd u) t e fe -> (Unit, t, e, u fe))) + +-- | Change the final environment by the one passed in the input. +putFinalEnv :: Trafo m t (FinalEnv2 t) Unit +putFinalEnv = Trafo $ \m -> (TrafoE m (\(Final fe) t e _ -> (Unit, t, e, fe))) + +-- | Return as output the final environment. +getFinalEnv :: Trafo m t Unit (FinalEnv2 t) +getFinalEnv = Trafo $ \m -> (TrafoE m (\_ t e fe -> ((Final fe), t, e, fe))) + +{- +-- | 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 = proc f -> + do fe <- getFinalEnv -< () + putFinalEnv -< f fe + -- Trafo $ \m -> (TrafoE m (\f t e fe -> ((), t, e, f fe))) +-} + +newtype Pair a b s = P (a s, b s) + +class Category2 (cat :: (* -> *) -> (* -> *) -> *) where + id2 :: cat a a + (.:.) :: cat b c -> cat a b -> cat a c + +class Category2 arr => Arrow2 (arr :: (* -> *) -> (* -> *) -> *) where + arr :: (forall s . a s -> b s) -> arr a b + first :: arr a b -> arr (Pair a c) (Pair b c) + second :: 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 + loop :: arr (Pair a c) (Pair b c) -> arr a b + + +instance Category2 (Trafo m t) where + id2 = Trafo (\m -> TrafoE m (\a t e u -> (a, t, e, u))) + + (.:.) (Trafo sb) (Trafo sa) = + Trafo + (\m1 -> + case sa m1 of + TrafoE m2 f1 -> case sb m2 of + TrafoE m3 f2 -> + TrafoE + m3 + (\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) + )) + + +(>>>) :: Category2 cat => cat a b -> cat b c -> cat a c +f >>> g = g .:. f + + +instance Arrow2 (Trafo m t) where + arr f + = Trafo (\m -> TrafoE m (\a t e u -> (f a, t, e, u)) ) + + + first (Trafo s) + = Trafo + (\m1 -> case s m1 of + TrafoE m2 f -> + TrafoE m2 + (\(P (a, c)) t2s e1 u1 -> + let (b,t12,e2,u2) = f a t2s e1 u1 + in (P (b, c),t12,e2,u2) + ) + ) + + second f = arr swap >>> first f >>> arr swap + where swap :: Pair c a s -> Pair a c s + swap ~(P (x, y)) = P (y, x) + + f *** g = first f >>> second g + + f &&& g = arr (\b -> P (b, b)) >>> (f *** g) + + +instance ArrowLoop2 (Trafo m t) where + loop (Trafo st) = + Trafo + (\m -> case st m of + TrafoE m1 f1 -> + TrafoE m1 + (\a t e u -> + let (P (b, x),t1,e1,u1) = f1 (P (a, x)) t e u + in (b,t1,e1,u1) + ) + ) + + +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. +sequenceA :: [Trafo m t a b] -> Trafo m t a (List b) +sequenceA [] = arr (const (List [])) +sequenceA (x:xs) + = (x &&& sequenceA xs) >>> + arr (\(P (a,List as)) -> List (a:as)) + +returnA :: Arrow2 arr => arr a a +returnA = arr id + +