Safe Haskell | None |
---|---|
Language | Haskell98 |
This module contains the data types, operations and serialization functions for representing Fixpoint's implication (i.e. subtyping) and well-formedness constraints in Haskell. The actual constraint solving is done by the `fixpoint.native` which is written in Ocaml.
- data Sort
- newtype Sub = Sub [(Int, Sort)]
- data FTycon
- type TCEmb a = HashMap a FTycon
- sortFTycon :: Sort -> Maybe FTycon
- intFTyCon :: FTycon
- boolFTyCon :: FTycon
- realFTyCon :: FTycon
- numFTyCon :: FTycon
- strFTyCon :: FTycon
- setFTyCon :: FTycon
- mapFTyCon :: FTycon
- basicSorts :: [Sort]
- intSort :: Sort
- realSort :: Sort
- boolSort :: Sort
- strSort :: Sort
- funcSort :: Sort
- setSort :: Sort -> Sort
- bitVecSort :: Sort
- mapSort :: Sort -> Sort -> Sort
- listFTyCon :: FTycon
- isListTC :: FTycon -> Bool
- sizeBv :: FTycon -> Maybe Int
- isFirstOrder :: Sort -> Bool
- mappendFTC :: FTycon -> FTycon -> FTycon
- fTyconSymbol :: FTycon -> Located Symbol
- symbolFTycon :: LocSymbol -> FTycon
- fTyconSort :: FTycon -> Sort
- symbolNumInfoFTyCon :: LocSymbol -> Bool -> Bool -> FTycon
- fApp :: Sort -> [Sort] -> Sort
- fAppTC :: FTycon -> [Sort] -> Sort
- fObj :: LocSymbol -> Sort
- unFApp :: Sort -> ListNE Sort
- unAbs :: Sort -> Sort
- sortSubst :: HashMap Symbol Sort -> Sort -> Sort
- functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
- mkFFunc :: Int -> [Sort] -> Sort
- bkFFunc :: Sort -> Maybe (Int, [Sort])
- isNumeric :: Sort -> Bool
- isReal :: Sort -> Bool
- isString :: Sort -> Bool
- data DataField = DField {}
- data DataCtor = DCtor {}
- data DataDecl = DDecl {}
Embedding to Fixpoint Types
Sorts ---------------------------------------------------------------------
FInt | |
FReal | |
FNum | numeric kind for Num tyvars |
FFrac | numeric kind for Fractional tyvars |
FObj !Symbol | uninterpreted type |
FVar !Int | fixpoint type variable |
FFunc !Sort !Sort | function |
FAbs !Int !Sort | type-abstraction |
FTC !FTycon | |
FApp !Sort !Sort | constructed type |
Eq Sort Source # | |
Data Sort Source # | |
Ord Sort Source # | |
Show Sort Source # | |
Generic Sort Source # | |
Monoid Sort Source # | |
Binary Sort Source # | |
NFData Sort Source # | |
Hashable Sort Source # | |
Fixpoint Sort Source # | |
Elaborate Sort Source # | |
Defunc Sort Source # | |
Elaborate (Symbol, Sort) Source # | |
Defunc (Symbol, Sort) Source # | |
type Rep Sort Source # | |
boolFTyCon :: FTycon Source #
realFTyCon :: FTycon Source #
basicSorts :: [Sort] Source #
bitVecSort :: Sort Source #
listFTyCon :: FTycon Source #
isFirstOrder :: Sort -> Bool Source #
symbolFTycon :: LocSymbol -> FTycon Source #
fTyconSort :: FTycon -> Sort Source #