Documentation

sh :: Pretty a => a -> String

data Constraint

occursType :: Token -> Type -> Bool

constraintToType :: Constraint -> (Bool, (String, Range, Type))

toConstraint :: Bool -> (String, Range, Type) -> Constraint

unifyType :: Type -> Constraint -> Result [(Token, Type)]

applyType :: [(Token, Type)] -> Token -> Maybe Type

apply :: [(Token, Type)] -> Type -> Type

unify' :: [(Type, Constraint)] -> Result [(Token, Type)]

tmpV :: Token

type Constraints = UniqueT Result (Type, [(Type, Constraint)])

not_supported :: (Show a, GetRange a) => a -> Constraints

getTypeC :: ConstMap -> THFFormula -> Constraints

getTypeCLF :: ConstMap -> THFLogicFormula -> Constraints

getTypeCBF :: ConstMap -> THFBinaryFormula -> Constraints

applyResult :: Int -> Type -> UniqueT Result Type

getTypeCUF :: ConstMap -> THFUnitaryFormula -> Constraints

genFn :: [Type] -> Type

insertAndIdx :: (Ord a, Eq b) => Map a [b] -> a -> b -> (Map a [b], Maybe Int)

intToStr :: Int -> String

flattenMap :: Map Constant [a] -> Map Constant a

type RewriteArg = Map Constant (Maybe Int)

rewriteVariableList' :: (RewriteFuns RewriteArg, RewriteArg) -> [THFVariable] -> Result [THFVariable]

rewriteConst' :: (RewriteFuns RewriteArg, RewriteArg) -> Constant -> Result THFUnitaryFormula

rewriteConst4needsConst :: (RewriteFuns Constant, Constant) -> Constant -> Result THFUnitaryFormula

needsConst :: Constant -> Named THFFormula -> Bool

infer :: ConstMap -> [Named THFFormula] -> Result (ConstMap, [Named THFFormula])

type_check :: TypeMap -> ConstMap -> [Named THFFormula] -> Result [[(Token, Type)]]