Tip.Core

Contents

• Constructing expressions
• Predicates and examinations on expressions
• Substition and refreshing
• Making new locals and functions
• Matching
• Data types
• Operations on theories
• Topologically sorting definitions

Description

Synopsis

• module Tip.Types
• (===) :: Expr a -> Expr a -> Expr a
• (=/=) :: Expr a -> Expr a -> Expr a
• oppositeQuant :: Quant -> Quant
• gentleNeg :: 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
• applyTypeIn :: Ord a => ((Type a -> Type a) -> f a -> f a) -> [a] -> [Type a] -> f a -> f a
• applyType :: Ord a => [a] -> [Type a] -> Type a -> Type a
• applyTypeInExpr :: Ord a => [a] -> [Type a] -> Expr a -> Expr a
• applyTypeInDecl :: Ord a => [a] -> [Type a] -> Decl a -> Decl a
• applyPolyType :: Ord a => PolyType a -> [Type a] -> ([Type a], Type a)
• gblType :: Ord a => Global a -> ([Type a], Type a)
• makeLets :: [(Local a, Expr a)] -> Expr a -> Expr a
• collectLets :: Expr a -> ([(Local a, Expr a)], Expr a)
• litView :: Expr a -> Maybe Lit
• boolView :: Expr a -> Maybe Bool
• forallView :: Expr a -> ([Local a], Expr a)
• 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]
• free :: Ord a => Expr a -> [Local a]
• locals :: 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
• theoryTypes :: (UniverseBi (t a) (Type a), Ord a) => t 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
• theoryGoals :: Theory a -> ([Formula a], [Formula a])
• partitionGoals :: [Formula a] -> ([Formula a], [Formula 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
  • defines :: f a -> a
  • uses :: f a -> [a]
• data (f :+: g) a
  • = InL (f a)
  • | InR (g a)

Documentation

Constructing expressions

Predicates and examinations on expressions

Substition and refreshing

Making new locals and functions

Matching

Data types

Operations on theories

Topologically sorting definitions