| Safe Haskell | None |
|---|---|
| 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])
Domain of a kvar
Free variables in a refinement
reftFreeVars :: Reft -> HashSet Symbol Source #
Free variables of a refinement
Deconstruct a SortedReft
sortedReftConcKVars :: Symbol -> SortedReft -> ([Pred], [KVSub], [KVSub]) Source #
Split a SortedReft into its concrete and KVar components