Top.Types.Quantification

Contents

• Quantification
• Universal quantification
• Existential quantification
• Skolemization
• Pretty printing

Description

Synopsis

• 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 {
  • showTopLevelQuantors :: Bool
  • dontUseIdentifiers :: [String]
  • variablePrefix :: String
  • showAllTheSame :: Bool
  • useTheNameMap :: Bool
  }
• defaultOptions :: ShowQuantorOptions
• showQuantors :: ShowQuantors a => a -> String
• class Show a => ShowQuantors a where
  • showQuantorsWithout :: ShowQuantorOptions -> a -> String
• variableList :: [String]

Quantification

Universal quantification

Existential quantification

Skolemization

Pretty printing