| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Solutions
Contents
Description
This module contains the top-level SOLUTION data types, including various indices used for solving.
- type Solution = Sol () QBind
- type GSolution = Sol (((Symbol, Sort), Expr), GBind) QBind
- data Sol b a
- updateGMap :: Sol b a -> HashMap KVar b -> Sol b a
- updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution
- sScp :: Sol b a -> HashMap KVar IBindEnv
- type CMap a = HashMap SubcId a
- type Hyp = ListNE Cube
- data Cube = Cube {}
- data QBind
- data GBind
- data EQual = EQL {}
- eQual :: Qualifier -> [Symbol] -> EQual
- trueEqual :: EQual
- qbToGb :: QBind -> GBind
- gbToQbs :: GBind -> [QBind]
- gbEquals :: GBind -> [[EQual]]
- equalsGb :: [[EQual]] -> GBind
- emptyGMap :: GSolution -> GSolution
- qbExprs :: QBind -> [Expr]
- type Cand a = [(Expr, a)]
- fromList :: SymEnv -> [(KVar, a)] -> [(KVar, b)] -> [(KVar, Hyp)] -> HashMap KVar IBindEnv -> Sol a b
- update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
- lookupQBind :: Sol a QBind -> KVar -> QBind
- lookup :: Sol a QBind -> KVar -> Either Hyp QBind
- glookup :: GSolution -> KVar -> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind))
- qb :: [EQual] -> QBind
- qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
- qbFilter :: (EQual -> Bool) -> QBind -> QBind
- gbFilterM :: Monad m => ([EQual] -> m Bool) -> GBind -> m GBind
- result :: Sol a QBind -> HashMap KVar Expr
- resultGradual :: GSolution -> HashMap KVar (Expr, [Expr])
- data Index = FastIdx {}
- data KIndex = KIndex {}
- data BindPred = BP {}
- data BIndex
Solution tables
type Solution = Sol () QBind Source #
The Solution data type --------------------------------------------------
A Sol contains the various indices needed to compute a solution,
in particular, to compute lhsPred for any given constraint.
Solution elements
type Hyp = ListNE Cube Source #
A Cube is a single constraint defining a KVar ---------------------------
Constructors
| Cube | |
Instantiated Qualifiers ---------------------------------------------------
Equal elements
Gradual Solution elements
Solution Candidates (move to SolverMonad?)
Constructor
fromList :: SymEnv -> [(KVar, a)] -> [(KVar, b)] -> [(KVar, Hyp)] -> HashMap KVar IBindEnv -> Sol a b Source #
Create a Solution ---------------------------------------------------------
Update
update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind) Source #
Update Solution -----------------------------------------------------------
Lookup
lookupQBind :: Sol a QBind -> KVar -> QBind Source #
Read / Write Solution at KVar ---------------------------------------------
Manipulating QBind
Conversion for client
Fast Solver (DEPRECATED as unsound)
A Index is a suitably indexed version of the cosntraints that lets us 1. CREATE a monolithic "background formula" representing all constraints, 2. ASSERT each lhs via bits for the subc-id and formulas for dependent cut KVars
Constructors
| FastIdx | |
Fields
| |
A KIndex uniquely identifies each *use* of a KVar in an (LHS) binder