| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Utils
Description
This module has various utility functions for accessing queries. TODO: move the "clients" in Visitors into this module.
Synopsis
- kvarDomain :: SInfo a -> KVar -> [Symbol]
- reftFreeVars :: Reft -> HashSet Symbol
- sortedReftConcKVars :: Symbol -> SortedReft -> ([Pred], [KVSub], [KVSub])
- checkRegular :: [DataDecl] -> [DataDecl]
- orderDeclarations :: [DataDecl] -> [[DataDecl]]
Domain of a kvar
Free variables in a refinement
Deconstruct a SortedReft
sortedReftConcKVars :: Symbol -> SortedReft -> ([Pred], [KVSub], [KVSub]) Source #
Split a SortedReft into its concrete and KVar components
Operators on DataDecl
checkRegular :: [DataDecl] -> [DataDecl] Source #
checkRegular ds returns the subset of ds that are _not_ regular
orderDeclarations :: [DataDecl] -> [[DataDecl]] Source #
orderDeclarations sorts the data declarations such that each declarations
only refers to preceding ones.