-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Generic abstract syntax, and utilities for embedded languages -- -- This library provides: -- -- -- -- Note: The library is probably mostly useful for data-flow languages, -- such as Feldspar. Currently, it does not support cyclic programs. -- -- [1] Data types a la carte, by Wouter Swierstra, in Journal -- of Functional Programming, 2008 -- -- [2] http://hackage.haskell.org/package/feldspar-language @package syntactic @version 0.1 -- | Generic representation of typed syntax trees -- -- As a simple demonstration, take the following simple language: -- -- 
--   data Expr1 a
--     where
--       Num1 :: Int -> Expr1 Int
--       Add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
--
-- -- Using the present library, this can be rewritten as follows: -- -- 
--   data Num2 a where Num2 :: Int -> Num2 (Full Int)
--   data Add2 a where Add2 :: Add2 (Int :-> Int :-> Full Int)
--   
--   type Expr2 a = ASTF (Num2 :+: Add2) a
--
-- -- Note that Num2 and Add2 are non-recursive. -- The only recursive data type here is AST, which is provided by -- the library. Now, the important point is that Expr1 and -- Expr2 are completely isomorphic! This is indicated by the -- following conversions: -- -- 
--   conv12 :: Expr1 a -> Expr2 a
--   conv12 (Num1 n)   = inject (Num2 n)
--   conv12 (Add1 a b) = inject Add2 :$: conv12 a :$: conv12 b
--   
--   conv21 :: Expr2 a -> Expr1 a
--   conv21 (project -> Just (Num2 n))           = Num1 n
--   conv21 ((project -> Just Add2) :$: a :$: b) = Add1 (conv21 a) (conv21 b)
--
-- -- A key property here is that the patterns in conv21 are -- actually complete. -- -- So, why should one use Expr2 instead of Expr1? The -- answer is that Expr2 can be processed by generic algorithms -- defined over AST, for example: -- -- 
--   countNodes :: ASTF domain a -> Int
--   countNodes = count
--     where
--       count :: AST domain a -> Int
--       count (Symbol _) = 1
--       count (a :$: b)  = count a + count b
--
-- -- Furthermore, although Expr2 was defined to use exactly the -- constructors Num2 and Add2, it is possible to leave -- the set of constructors open, leading to more modular and reusable -- code. This can be seen by relaxing the types of conv12 and -- conv21: -- -- 
--   conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a
--   conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a
--
-- -- This way of encoding open data types is taken from Data types a la -- carte, by Wouter Swierstra, in Journal of Functional -- Programming, 2008. However, we do not need Swierstra's fixed-point -- machinery for recursive data types. Instead we rely on AST -- being recursive. module Language.Syntactic.Syntax -- | The type of a fully applied constructor newtype Full a Full :: a -> Full a result :: Full a -> a -- | The type of a partially applied (or unapplied) constructor newtype (:->) a b Partial :: (a -> b) -> :-> a b -- | Fully or partially applied constructor -- -- This is a public alias for the hidden class ConsType'. The only -- instances are: -- -- 
--   instance ConsType' (Full a)
--   instance ConsType' b => ConsType' (a :-> b)
--
class ConsType' a => ConsType a -- | Maps a ConsType to a simpler form where :-> has been -- replaced by ->, and Full has been removed. This is -- a public alias for the hidden type ConsEval'. type ConsEval a = ConsEval' a -- | Returns the result type (Full removed) of a ConsType. -- This is a public alias for the hidden type EvalResult'. type EvalResult a = EvalResult' a -- | Make a constructor evaluation from a ConsEval representation consEval :: ConsType a => ConsEval a -> a -- | Semantic constructor application ($:) :: (a :-> b) -> a -> b -- | Generic abstract syntax tree, parameterized by a symbol domain -- -- In general, (AST dom (a :-> b)) represents a -- partially applied (or unapplied) constructor, missing at least one -- argument, while (AST dom (Full a)) represents a -- fully applied constructor, i.e. a complete syntax tree. It is not -- possible to construct a total value of type (AST dom -- a) that does not fulfill the constraint (ConsType -- a). -- -- Note that the hidden class ConsType' mentioned in the type of -- Symbol is interchangeable with ConsType. data AST dom a Symbol :: dom a -> AST dom a (:$:) :: AST dom (a :-> b) -> ASTF dom a -> AST dom b -- | Fully applied abstract syntax tree type ASTF dom a = AST dom (Full a) -- | Co-product of two symbol domains data (:+:) dom1 dom2 :: * -> * InjectL :: dom1 a -> (dom1 :+: dom2) a InjectR :: dom2 a -> (dom1 :+: dom2) a class :<: sub sup inject :: (:<: sub sup, ConsType a) => sub a -> sup a project :: :<: sub sup => sup a -> Maybe (sub a) -- | It is assumed that for all types A fulfilling -- (Syntactic A dom): -- -- 
--   eval a == eval (desugar $ (id :: A -> A) $ sugar a)
--
-- -- (using Language.Syntactic.Analysis.Evaluation.eval) class Typeable (Internal a) => Syntactic a dom | a -> dom where { type family Internal a; } desugar :: Syntactic a dom => a -> ASTF dom (Internal a) sugar :: Syntactic a dom => ASTF dom (Internal a) -> a -- | Syntactic type casting resugar :: (Syntactic a dom, Syntactic b dom, (Internal a) ~ (Internal b)) => a -> b -- | Data family for collecting the children of a constructor, for example: -- -- 
--   subTrees :: forall dom . SubTrees dom (Int :-> Bool :-> Full [Int])
--   subTrees = a :*: b :*: Nil
--     where
--       a = undefined :: ASTF dom Int
--       b = undefined :: ASTF dom Bool
--
-- -- (SubTrees a) is meaningful iff. (ConsType -- a) -- | Process an AST using a function that gets direct access to the -- top-most constructor and its sub-trees -- -- This function can be used to create AST traversal functions -- indexed by the symbol types, for example: -- -- 
--   class Count subDomain
--     where
--       count' :: Count domain => subDomain a -> SubTrees domain a -> Int
--   
--   instance (Count sub1, Count sub2) => Count (sub1 :+: sub2)
--     where
--       count' (InjectL a) args = count' a args
--       count' (InjectR a) args = count' a args
--   
--   count :: Count dom => ASTF dom a -> Int
--   count = processNode count'
--
-- -- Here, count represents some static analysis on an AST. -- Each constructor in the tree will be processed by count' -- indexed by the corresponding symbol type. That way, count' -- can be seen as an open-ended function on an open data type. The -- (Count domain) constraint on count' is to allow -- recursion over sub-trees. -- -- Let's say we have a symbol -- -- 
--   data Add a
--     where
--       Add :: Add (Int :-> Int :-> Full Int)
--
-- -- Then the Count instance for Add might look as -- follows: -- -- 
--   instance Count Add
--     where
--       count' Add (a :*: b :*: Nil) = 1 + count a + count b
--
processNode :: (forall a. ConsType a => dom a -> SubTrees dom a -> b) -> ASTF dom a -> b instance [overlap ok] Typeable1 Full instance [overlap ok] Typeable2 :-> instance [overlap ok] Eq a => Eq (Full a) instance [overlap ok] Show a => Show (Full a) instance [overlap ok] Typeable a => Syntactic (ASTF dom a) dom instance [overlap ok] expr1 :<: expr3 => expr1 :<: (expr2 :+: expr3) instance [overlap ok] expr1 :<: (expr1 :+: expr2) instance [overlap ok] expr :<: expr instance [overlap ok] sub :<: sup => sub :<: AST sup instance [overlap ok] ConsType' a => ConsType a instance [overlap ok] ConsType' b => ConsType' (a :-> b) instance [overlap ok] ConsType' (Full a) module Language.Syntactic.Analysis.Equality -- | Equality for expressions. The difference between Eq and -- ExprEq is that ExprEq allows comparison of expressions -- with different value types. It is assumed that when the types differ, -- the expressions also differ. The reason for allowing comparison of -- different types is that this is convenient when the types are -- existentially quantified. class ExprEq expr exprEq :: ExprEq expr => expr a -> expr b -> Bool eqSyn :: (Syntactic a dom, ExprEq dom) => a -> a -> Bool instance (ExprEq expr1, ExprEq expr2) => Eq ((:+:) expr1 expr2 a) instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2) instance ExprEq expr => Eq (AST expr a) instance ExprEq expr => ExprEq (AST expr) module Language.Syntactic.Analysis.Render -- | Render an expression as concrete syntax. A complete instance must -- define either of the methods render and renderPart. class Render expr render :: Render expr => expr a -> String renderPart :: Render expr => [String] -> expr a -> String -- | Print an expression printExpr :: Render expr => expr a -> IO () class Render expr => ToTree expr toTreePart :: ToTree expr => [Tree String] -> expr a -> Tree String -- | Show syntax tree using ASCII art showAST :: ToTree dom => AST dom a -> String -- | Print syntax tree using ASCII art drawAST :: ToTree dom => AST dom a -> IO () instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2) instance ToTree dom => ToTree (AST dom) instance (Render expr1, Render expr2) => Show ((:+:) expr1 expr2 a) instance (Render expr1, Render expr2) => Render (expr1 :+: expr2) instance Render expr => Show (AST expr a) instance Render expr => Render (AST expr) module Language.Syntactic.Analysis.Evaluation class Eval expr evaluate :: Eval expr => expr a -> a evalFull :: Eval expr => ASTF expr a -> a evalSyn :: (Syntactic a dom, Eval dom) => a -> Internal a instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2) instance Eval expr => Eval (AST expr) module Language.Syntactic.Analysis.Hash class ExprEq expr => ExprHash expr exprHash :: ExprHash expr => expr a -> Hash instance (ExprHash expr1, ExprHash expr2) => ExprHash (expr1 :+: expr2) instance ExprHash expr => ExprHash (AST expr) -- | Literal expressions module Language.Syntactic.Features.Literal data Literal a Literal :: a -> Literal (Full a) lit :: (Eq a, Show a, Typeable a, :<: Literal expr) => a -> ASTF expr a instance ExprHash Literal instance Eval Literal instance ToTree Literal instance Render Literal instance ExprEq Literal -- | Primitive functions module Language.Syntactic.Features.PrimFunc data PrimFunc a PrimFunc :: String -> (ConsEval (a :-> b)) -> PrimFunc (a :-> b) primFunc :: (Typeable a, :<: PrimFunc expr) => String -> (a -> b) -> ASTF expr a -> ASTF expr b primFunc2 :: (Typeable a, Typeable b, :<: PrimFunc expr) => String -> (a -> b -> c) -> ASTF expr a -> ASTF expr b -> ASTF expr c primFunc3 :: (Typeable a, Typeable b, Typeable c, :<: PrimFunc expr) => String -> (a -> b -> c -> d) -> ASTF expr a -> ASTF expr b -> ASTF expr c -> ASTF expr d primFunc4 :: (Typeable a, Typeable b, Typeable c, Typeable d, :<: PrimFunc expr) => String -> (a -> b -> c -> d -> e) -> ASTF expr a -> ASTF expr b -> ASTF expr c -> ASTF expr d -> ASTF expr e instance ExprHash PrimFunc instance Eval PrimFunc instance ToTree PrimFunc instance Render PrimFunc instance ExprEq PrimFunc -- | Conditional expressions module Language.Syntactic.Features.Condition data Condition a Condition :: Condition (Bool :-> (a :-> (a :-> Full a))) condition :: (:<: Condition expr, Syntactic a expr) => ASTF expr Bool -> a -> a -> a instance ExprHash Condition instance Eval Condition instance ToTree Condition instance Render Condition instance ExprEq Condition -- | Construction and selection of tuples module Language.Syntactic.Features.Tuple -- | Expressions for constructing tuples data Tuple a Tup2 :: Tuple (a :-> (b :-> Full (a, b))) Tup3 :: Tuple (a :-> (b :-> (c :-> Full (a, b, c)))) Tup4 :: Tuple (a :-> (b :-> (c :-> (d :-> Full (a, b, c, d))))) Tup5 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> Full (a, b, c, d, e)))))) Tup6 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> Full (a, b, c, d, e, f))))))) Tup7 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> Full (a, b, c, d, e, f, g)))))))) -- | Expressions for selecting elements of a tuple data Select a Sel1 :: Select (a :-> Full b) Sel2 :: Select (a :-> Full b) Sel3 :: Select (a :-> Full b) Sel4 :: Select (a :-> Full b) Sel5 :: Select (a :-> Full b) Sel6 :: Select (a :-> Full b) Sel7 :: Select (a :-> Full b) -- | Return the selected position, e.g. -- -- 
--   selectPos (Sel3 :: Select ((Int,Int,Int,Int) -> Int)) = 3
--
selectPos :: Select a -> Int instance (Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Syntactic e expr, Syntactic f expr, Syntactic g expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d, e, f, g) expr instance (Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Syntactic e expr, Syntactic f expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d, e, f) expr instance (Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Syntactic e expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d, e) expr instance (Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d) expr instance (Syntactic a expr, Syntactic b expr, Syntactic c expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c) expr instance (Syntactic a expr, Syntactic b expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b) expr instance ExprHash Select instance ToTree Select instance Render Select instance Eval Select instance ExprEq Select instance ExprHash Tuple instance Eval Tuple instance ToTree Tuple instance Render Tuple instance ExprEq Tuple -- | Annotations for syntax trees module Language.Syntactic.Features.Annotate -- | Annotating an expression with arbitrary information. -- -- This can be used to annotate every node of a syntax tree, which is -- done by changing -- -- 
--   AST dom a
--
-- -- to -- -- 
--   AST (Ann info dom) a
--
-- -- Injection/projection of an annotated tree is done using -- injectAnn / projectAnn. data Ann info expr a Ann :: info (EvalResult a) -> expr a -> Ann info expr a injectAnn :: (:<: sub sup, ConsType a) => info (EvalResult a) -> sub a -> AST (Ann info sup) a projectAnn :: :<: sub sup => AST (Ann info sup) a -> Maybe (info (EvalResult a), sub a) getInfo :: AST (Ann info sup) a -> info (EvalResult a) instance ExprHash expr => ExprHash (Ann info expr) instance Eval expr => Eval (Ann info expr) instance ToTree expr => ToTree (Ann info expr) instance Render expr => Render (Ann info expr) instance ExprEq expr => ExprEq (Ann info expr) -- | The syntactic library -- -- The basic functionality is provided by the module -- Language.Syntactic.Syntax. module Language.Syntactic -- | General binding constructs module Language.Syntactic.Features.Binding -- | Variable identifier newtype VarId VarId :: Integer -> VarId varInteger :: VarId -> Integer showVar :: VarId -> String -- | Variables data Variable a Variable :: VarId -> Variable (Full a) -- | Lambda binding data Lambda a Lambda :: VarId -> Lambda (b :-> Full (a -> b)) -- | Alpha-equivalence on Lambda expressions. Free variables are -- taken to be equvalent if they have the same identifier. eqLambda :: ExprEq dom => AST (Lambda :+: (Variable :+: dom)) a -> AST (Lambda :+: (Variable :+: dom)) b -> Reader [(VarId, VarId)] Bool -- | Evaluation of possibly open LambdaAST expressions evalLambdaM :: (Eval dom, MonadReader [(VarId, Dynamic)] m) => AST (Lambda :+: (Variable :+: dom)) (Full a) -> m a -- | Evaluation of closed Lambda expressions evalLambda :: Eval dom => AST (Lambda :+: (Variable :+: dom)) (Full a) -> a -- | The class of n-ary binding functions class NAry a where { type family NAryEval a; type family NAryDom a :: * -> *; } bindN :: NAry a => (forall b c. (Typeable b, Typeable c) => (AST (NAryDom a) (Full b) -> AST (NAryDom a) (Full c)) -> AST (NAryDom a) (Full (b -> c))) -> a -> AST (NAryDom a) (Full (NAryEval a)) -- | Let binding data Let a Let :: Let (a :-> ((a -> b) :-> Full b)) instance Eq VarId instance Ord VarId instance Num VarId instance Enum VarId instance Ix VarId instance ExprHash Let instance Eval Let instance ToTree Let instance Render Let instance ExprEq Let instance (NAryDom b ~ dom, Typeable a, NAry b, Typeable (NAryEval b)) => NAry (AST dom (Full a) -> b) instance NAry (AST dom (Full a)) instance ToTree Lambda instance Render Lambda instance ToTree Variable instance Render Variable instance Show VarId -- | This module provides binding constructs using higher-order syntax and -- a function for translating back to first-order syntax. Expressions -- constructed using the exported interface are guaranteed to have a -- well-behaved translation. module Language.Syntactic.Features.Binding.HigherOrder -- | Variables data Variable a -- | Evaluation of closed Lambda expressions evalLambda :: Eval dom => AST (Lambda :+: (Variable :+: dom)) (Full a) -> a -- | Let binding data Let a Let :: Let (a :-> ((a -> b) :-> Full b)) -- | Higher-order lambda binding data HOLambda dom a HOLambda :: (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOLambda dom (Full (a -> b)) type HOAST dom = AST (HOLambda dom :+: (Variable :+: dom)) -- | Lambda binding lambda :: (Typeable a, Typeable b) => (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b)) -- | N-ary lambda binding lambdaN :: (NAry a, (NAryDom a) ~ (HOLambda dom :+: (Variable :+: dom))) => a -> HOAST dom (Full (NAryEval a)) -- | Let binding let_ :: (Typeable a, Typeable b, :<: Let dom) => HOAST dom (Full a) -> (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full b) reifyM :: Typeable a => HOAST dom a -> State VarId (AST (Lambda :+: (Variable :+: dom)) a) -- | Translating expressions with higher-order binding to corresponding -- expressions using first-order binding reify :: Typeable a => HOAST dom a -> AST (Lambda :+: (Variable :+: dom)) a