| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Camfort.Specification.Units.InferenceBackend
- pprint :: t -> [Char]
- debugInfoForNonZeros :: [Rational] -> State UnitEnv String
- errorMessage :: (?debug :: Bool) => Row -> UnitConstant -> [Rational] -> State UnitEnv String
- reportInconsistency :: (?debug :: Bool) => LinearSystem -> [Int] -> State UnitEnv ()
- extendConstraints :: [UnitConstant] -> State UnitEnv ()
- swapUnitVarCats :: Int -> Int -> [a] -> [a]
- swapUnitVarCats' :: Int -> Int -> [a] -> [a] -> Int -> [a]
- swapCols :: Int -> Int -> State UnitEnv ()
- class UpdateColInfo t where
- reorderVarCols :: State UnitEnv ()
- reduceRows :: Col -> LinearSystem -> LinearSystem
- solveSystemM :: (?solver :: Solver, ?debug :: Bool) => String -> State UnitEnv Bool
- checkUnderdeterminedM :: State UnitEnv ()
- checkUnderdetermined :: [UnitVarCategory] -> LinearSystem -> [Int]
- lookupVarsByColsFilterByArg :: Matrix Rational -> VarColEnv -> [UnitVarCategory] -> [Int] -> DebugInfo -> [String]
- firstNonZeroCoeff :: Matrix Rational -> [UnitVarCategory] -> Row -> Col
- checkUnderdetermined' :: [UnitVarCategory] -> LinearSystem -> Int -> [Int]
- propagateUnderdetermined :: Matrix Rational -> [Int] -> [Int]
- intrinsicsDict :: (?assumeLiterals :: AssumeLiterals) => [(String, String -> State UnitEnv ())]
- addPlain1ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addPlain2ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addPlain1Arg1ExtraIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addPlain2Arg1ExtraIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addProductIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addPowerIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addUnitlessIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addUnitlessSubIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addUnitlessResult0ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addUnitlessResult1ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addUnitlessResult2AnyArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- addUnitlessResult2SameArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv ()
- mustEqual :: (?assumeLiterals :: AssumeLiterals) => Bool -> VarCol -> VarCol -> State UnitEnv VarCol
- mustAddUp :: VarCol -> VarCol -> Rational -> Rational -> State UnitEnv VarCol
- sqrtUnits :: VarCol -> State UnitEnv VarCol
- anyUnits :: UnitVarCategory -> State UnitEnv VarCol
- inverse :: [Int] -> [Int]
- fixValue :: Eq a => (a -> a) -> a -> a
- moveElem :: Int -> Int -> [a] -> [a]
- incrElem :: Num a => a -> (Int, Int) -> Matrix a -> Matrix a
- moveCol :: Int -> Int -> Matrix a -> Matrix a
debugInfoForNonZeros :: [Rational] -> State UnitEnv String Source #
Print debug information for non-zero coefficients from the Gaussian matrix
errorMessage :: (?debug :: Bool) => Row -> UnitConstant -> [Rational] -> State UnitEnv String Source #
An attempt at getting some useful user information. Needs position information
reportInconsistency :: (?debug :: Bool) => LinearSystem -> [Int] -> State UnitEnv () Source #
extendConstraints :: [UnitConstant] -> State UnitEnv () Source #
swapUnitVarCats :: Int -> Int -> [a] -> [a] Source #
class UpdateColInfo t where Source #
Minimal complete definition
Methods
updateColInfo :: Col -> Col -> t -> t Source #
reorderVarCols :: State UnitEnv () Source #
reorderVarCols puts any variable columns to the end of the Gaussian matrix (along with the associated information)
reduceRows :: Col -> LinearSystem -> LinearSystem Source #
reduceRows is a core part of the polymorphic unit checking for procedures.
It is essentially an "optimisation" of the Gaussian matrix (not in the sense of performance), that elimiantes rows in the system such that there are as few variables as possible. Within a function, assuming everything is consistent, then this should generate a linear constraint between the parameters and the return as a single row in the matrix. This is then used by the interprocedural constraints to hookup call-sites with definitions (in a parametrically polymorphic way- i.e. lambda abstraction is polymorphic in its units, different to say ML).
checkUnderdeterminedM :: State UnitEnv () Source #
checkUnderdetermined :: [UnitVarCategory] -> LinearSystem -> [Int] Source #
lookupVarsByColsFilterByArg :: Matrix Rational -> VarColEnv -> [UnitVarCategory] -> [Int] -> DebugInfo -> [String] Source #
firstNonZeroCoeff :: Matrix Rational -> [UnitVarCategory] -> Row -> Col Source #
checkUnderdetermined' :: [UnitVarCategory] -> LinearSystem -> Int -> [Int] Source #
intrinsicsDict :: (?assumeLiterals :: AssumeLiterals) => [(String, String -> State UnitEnv ())] Source #
addPlain1ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addPlain2ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addPlain1Arg1ExtraIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addPlain2Arg1ExtraIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addProductIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addPowerIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addUnitlessIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addUnitlessSubIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addUnitlessResult0ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addUnitlessResult1ArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addUnitlessResult2AnyArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #
addUnitlessResult2SameArgIntrinsic :: (?assumeLiterals :: AssumeLiterals) => String -> State UnitEnv () Source #