| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Sorts
Contents
Description
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
- intSort :: Sort
- realSort :: Sort
- boolSort :: Sort
- strSort :: Sort
- funcSort :: Sort
- setSort :: Sort -> Sort
- bitVecSort :: Sort
- mapSort :: Sort -> Sort -> Sort
- listFTyCon :: FTycon
- isListTC :: FTycon -> Bool
- fTyconSymbol :: FTycon -> Located Symbol
- symbolFTycon :: LocSymbol -> FTycon
- fTyconSort :: FTycon -> Sort
- fApp :: Sort -> [Sort] -> Sort
- fApp' :: Sort -> ListNE Sort
- fAppTC :: FTycon -> [Sort] -> Sort
- fObj :: LocSymbol -> Sort
- sortSubst :: HashMap Symbol Sort -> Sort -> Sort
- functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
- mkFFunc :: Int -> [Sort] -> Sort
- bkFFunc :: Sort -> Maybe (Int, [Sort])
Embedding to Fixpoint Types
sortFTycon :: Sort -> Maybe FTycon Source
bitVecSort :: Sort Source
fTyconSymbol :: FTycon -> Located Symbol Source
symbolFTycon :: LocSymbol -> FTycon Source
fTyconSort :: FTycon -> Sort Source