Safe Haskell | None |
---|---|
Language | Haskell2010 |
General functions for constructing and examining Tip syntax.
- module Tip.Types
- (===) :: Expr a -> Expr a -> Expr a
- (=/=) :: Expr a -> Expr a -> Expr a
- neg :: Expr a -> Expr a
- (/\) :: Expr a -> Expr a -> Expr a
- (\/) :: Expr a -> Expr a -> Expr a
- ands :: [Expr a] -> Expr a
- ors :: [Expr a] -> Expr a
- (==>) :: Expr a -> Expr a -> Expr a
- (===>) :: [Expr a] -> Expr a -> Expr a
- mkQuant :: Quant -> [Local a] -> Expr a -> Expr a
- bool :: Bool -> Expr a
- trueExpr :: Expr a
- falseExpr :: Expr a
- makeIf :: Expr a -> Expr a -> Expr a -> Expr a
- intLit :: Integer -> Expr a
- literal :: Lit -> Expr a
- intType :: Type a
- boolType :: Type a
- applyFunction :: Function a -> [Type a] -> [Expr a] -> Expr a
- applySignature :: Signature a -> [Type a] -> [Expr a] -> Expr a
- apply :: Expr a -> [Expr a] -> Expr a
- applyType :: Ord a => [a] -> [Type a] -> Type a -> Type a
- applyPolyType :: Ord a => PolyType a -> [Type a] -> ([Type a], Type a)
- litView :: Expr a -> Maybe Lit
- boolView :: Expr a -> Maybe Bool
- data DeepPattern a
- = DeepConPat (Global a) [DeepPattern a]
- | DeepVarPat (Local a)
- | DeepLitPat Lit
- patternMatchingView :: Ord a => [Local a] -> Expr a -> [([DeepPattern a], Expr a)]
- ifView :: Expr a -> Maybe (Expr a, Expr a, Expr a)
- projAt :: Expr a -> Maybe (Expr a, Expr a)
- projGlobal :: Expr a -> Maybe a
- atomic :: Expr a -> Bool
- occurrences :: Eq a => Local a -> Expr a -> Int
- signature :: Function a -> Signature a
- funcType :: Function a -> PolyType a
- bound :: Ord a => Expr a -> [Local a]
- locals :: Ord a => Expr a -> [Local a]
- free :: Ord a => Expr a -> [Local a]
- globals :: (UniverseBi (t a) (Global a), UniverseBi (t a) (Type a), Ord a) => t a -> [a]
- tyVars :: Ord a => Type a -> [a]
- freeTyVars :: Ord a => Expr a -> [a]
- exprType :: Ord a => Expr a -> Type a
- builtinType :: Ord a => Builtin -> [Type a] -> Type a
- freshLocal :: Name a => Type a -> Fresh (Local a)
- freshArgs :: Name a => Global a -> Fresh [Local a]
- refreshLocal :: Name a => Local a -> Fresh (Local a)
- freshen :: Name a => Expr a -> Fresh (Expr a)
- freshenNames :: (TransformBi a (f a), Name a) => [a] -> f a -> Fresh (f a)
- (//) :: Name a => Expr a -> Local a -> Expr a -> Fresh (Expr a)
- substMany :: Name a => [(Local a, Expr a)] -> Expr a -> Fresh (Expr a)
- letExpr :: Name a => Expr a -> (Local a -> Fresh (Expr a)) -> Fresh (Expr a)
- unsafeSubst :: Ord a => Expr a -> Local a -> Expr a -> Expr a
- updateLocalType :: Type a -> Local a -> Local a
- updateFuncType :: PolyType a -> Function a -> Function a
- matchTypesIn :: Ord a => [a] -> [(Type a, Type a)] -> Maybe [Type a]
- matchTypes :: Ord a => [(Type a, Type a)] -> Maybe [(a, Type a)]
- makeGlobal :: Ord a => a -> PolyType a -> [Type a] -> Maybe (Type a) -> Maybe (Global a)
- constructorType :: Datatype a -> Constructor a -> PolyType a
- destructorType :: Datatype a -> Type a -> PolyType a
- constructor :: Datatype a -> Constructor a -> [Type a] -> Global a
- projector :: Datatype a -> Constructor a -> Int -> [Type a] -> Global a
- discriminator :: Datatype a -> Constructor a -> [Type a] -> Global a
- mapDecls :: forall a b. (forall t. Traversable t => t a -> t b) -> Theory a -> Theory b
- topsort :: (Ord a, Definition f) => [f a] -> [[f a]]
- class Definition f where
- data (f :+: g) a
Documentation
module Tip.Types
Constructing expressions
Predicates and examinations on expressions
data DeepPattern a Source
A representation of Nested patterns, used in patternMatchingView
DeepConPat (Global a) [DeepPattern a] | |
DeepVarPat (Local a) | |
DeepLitPat Lit |
patternMatchingView :: Ord a => [Local a] -> Expr a -> [([DeepPattern a], Expr a)] Source
Match as left-hand side pattern-matching definitions
Stops at default patterns, for simplicity
projGlobal :: Expr a -> Maybe a Source
globals :: (UniverseBi (t a) (Global a), UniverseBi (t a) (Type a), Ord a) => t a -> [a] Source
freeTyVars :: Ord a => Expr a -> [a] Source
builtinType :: Ord a => Builtin -> [Type a] -> Type a Source
The result type of a built in function, applied to some types
Substition and refreshing
freshenNames :: (TransformBi a (f a), Name a) => [a] -> f a -> Fresh (f a) Source
(//) :: Name a => Expr a -> Local a -> Expr a -> Fresh (Expr a) Source
Substitution, of local variables
Since there are only rank-1 types, bound variables from lambdas and case never have a forall type and thus are not applied to any types.
unsafeSubst :: Ord a => Expr a -> Local a -> Expr a -> Expr a Source
Substitution, but without refreshing. Only use when the replacement expression contains no binders (i.e. no lambdas, no lets, no quantifiers), since the binders are not refreshed at every insertion point.
Making new locals and functions
updateLocalType :: Type a -> Local a -> Local a Source
updateFuncType :: PolyType a -> Function a -> Function a Source
Matching
Data types
constructorType :: Datatype a -> Constructor a -> PolyType a Source
destructorType :: Datatype a -> Type a -> PolyType a Source
constructor :: Datatype a -> Constructor a -> [Type a] -> Global a Source
discriminator :: Datatype a -> Constructor a -> [Type a] -> Global a Source
Operations on theories
mapDecls :: forall a b. (forall t. Traversable t => t a -> t b) -> Theory a -> Theory b Source
Topologically sorting definitions
topsort :: (Ord a, Definition f) => [f a] -> [[f a]] Source
class Definition f where Source
Definition Datatype | |
Definition Signature | |
Definition Function | |
(Definition f, Definition g) => Definition ((:+:) f g) |