| Safe Haskell | Safe-Infered |
|---|
Top.Types.Quantification
Contents
Description
Universal and existential quantification of types
- newtype Quantification q a = Quantification ([Int], QuantorMap, a)
- type QuantorMap = [(Int, String)]
- withoutQuantors :: Quantification q a -> Bool
- showQuantor :: Show q => Quantification q a -> String
- noQuantifiers :: a -> Quantification q a
- quantifiers :: Quantification q a -> [Int]
- unquantify :: Quantification q a -> a
- introduceTypeVariables :: Substitutable a => Int -> Quantification q a -> (Int, a)
- introduceSkolemConstants :: Substitutable a => Int -> Quantification q a -> (Int, a)
- bindTypeVariables :: Substitutable a => [Int] -> a -> Quantification q a
- bindSkolemConstants :: HasSkolems a => [Int] -> a -> Quantification q a
- getQuantorMap :: Quantification q a -> QuantorMap
- data Universal
- type Forall = Quantification Universal
- instantiate, skolemize :: Substitutable a => Int -> Forall a -> (Int, a)
- generalize :: (Substitutable context, Substitutable a) => context -> a -> Forall a
- generalizeAll :: Substitutable a => a -> Forall a
- quantify :: Substitutable a => [Int] -> a -> Forall a
- unskolemize :: HasSkolems a => [Int] -> a -> Forall a
- data Existential
- type Exists = Quantification Existential
- open, reveal :: Substitutable a => Int -> Exists a -> (Int, a)
- close :: HasSkolems a => [Int] -> a -> Exists a
- unreveal :: Substitutable a => [Int] -> a -> Exists a
- skolemPrefix :: String
- makeSkolemConstant :: Int -> Tp
- fromSkolemString :: String -> Maybe Int
- skolemizeFTV :: Substitutable a => a -> a
- class HasSkolems a where
- allSkolems :: a -> [Int]
- changeSkolems :: [(Int, Tp)] -> a -> a
- data ShowQuantorOptions = ShowQuantorOptions {}
- defaultOptions :: ShowQuantorOptions
- showQuantors :: ShowQuantors a => a -> String
- class Show a => ShowQuantors a where
- showQuantorsWithout :: ShowQuantorOptions -> a -> String
- variableList :: [String]
Quantification
newtype Quantification q a Source
Constructors
| Quantification ([Int], QuantorMap, a) |
Instances
| IsSigmaPreds TpScheme | |
| IsTpScheme TpScheme | |
| (Substitutable a, ShowQuantors a, Show q) => Show (Quantification q a) | |
| HasTypes a => HasTypes (Quantification q a) | |
| Substitutable a => Substitutable (Quantification q a) | |
| (Substitutable a, ShowQuantors a, Show q) => ShowQuantors (Quantification q a) |
type QuantorMap = [(Int, String)]Source
withoutQuantors :: Quantification q a -> BoolSource
showQuantor :: Show q => Quantification q a -> StringSource
noQuantifiers :: a -> Quantification q aSource
quantifiers :: Quantification q a -> [Int]Source
unquantify :: Quantification q a -> aSource
introduceTypeVariables :: Substitutable a => Int -> Quantification q a -> (Int, a)Source
introduceSkolemConstants :: Substitutable a => Int -> Quantification q a -> (Int, a)Source
bindTypeVariables :: Substitutable a => [Int] -> a -> Quantification q aSource
bindSkolemConstants :: HasSkolems a => [Int] -> a -> Quantification q aSource
getQuantorMap :: Quantification q a -> QuantorMapSource
Universal quantification
Instances
type Forall = Quantification UniversalSource
instantiate, skolemize :: Substitutable a => Int -> Forall a -> (Int, a)Source
generalize :: (Substitutable context, Substitutable a) => context -> a -> Forall aSource
generalizeAll :: Substitutable a => a -> Forall aSource
quantify :: Substitutable a => [Int] -> a -> Forall aSource
unskolemize :: HasSkolems a => [Int] -> a -> Forall aSource
Existential quantification
data Existential Source
Instances
close :: HasSkolems a => [Int] -> a -> Exists aSource
unreveal :: Substitutable a => [Int] -> a -> Exists aSource
Skolemization
makeSkolemConstant :: Int -> TpSource
fromSkolemString :: String -> Maybe IntSource
skolemizeFTV :: Substitutable a => a -> aSource
class HasSkolems a whereSource
Instances
| HasSkolems Tp | |
| HasSkolems a => HasSkolems [a] |
Pretty printing
data ShowQuantorOptions Source
Constructors
| ShowQuantorOptions | |
Fields
| |
showQuantors :: ShowQuantors a => a -> StringSource
class Show a => ShowQuantors a whereSource
This class can deal with the pretty printing of (possibly nested) quantifiers.
Methods
showQuantorsWithout :: ShowQuantorOptions -> a -> StringSource
Instances
| ShowQuantors Tp | |
| (Substitutable qs, ShowQualifiers qs) => ShowQuantors (Sigma qs) | |
| (ShowQualifiers q, Show a) => ShowQuantors (Qualification q a) | |
| (Substitutable a, ShowQuantors a, Show q) => ShowQuantors (Quantification q a) |
variableList :: [String]Source
List of unique identifiers.(a, b, .., z, a1, b1 .., z1, a2, ..)