Safe Haskell	None
Language	Haskell98

Camfort.Specification.Units.Environment

Contents

Operations on unit environments

Synopsis

Documentation

data UnitInfo Source #

Constructors

Parametric (String, Int)
ParametricUse (String, Int, Int)
UnitName String
Undetermined String
UnitlessI
UnitMul UnitInfo UnitInfo
UnitPow UnitInfo Double

Instances

Eq UnitInfo Source #
Methods (==) :: UnitInfo -> UnitInfo -> Bool # (/=) :: UnitInfo -> UnitInfo -> Bool #
Data UnitInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnitInfo -> c UnitInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnitInfo # toConstr :: UnitInfo -> Constr # dataTypeOf :: UnitInfo -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c UnitInfo) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnitInfo) # gmapT :: (forall b. Data b => b -> b) -> UnitInfo -> UnitInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnitInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnitInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> UnitInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnitInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo #
Ord UnitInfo Source #
Methods compare :: UnitInfo -> UnitInfo -> Ordering # (<) :: UnitInfo -> UnitInfo -> Bool # (<=) :: UnitInfo -> UnitInfo -> Bool # (>) :: UnitInfo -> UnitInfo -> Bool # (>=) :: UnitInfo -> UnitInfo -> Bool # max :: UnitInfo -> UnitInfo -> UnitInfo # min :: UnitInfo -> UnitInfo -> UnitInfo #
Show UnitInfo Source #
Methods showsPrec :: Int -> UnitInfo -> ShowS # show :: UnitInfo -> String # showList :: [UnitInfo] -> ShowS #

type EqualityConstrained = Bool Source #

data Solver Source #

Constructors

LAPACK
Custom

Instances

Eq Solver Source #
Methods (==) :: Solver -> Solver -> Bool # (/=) :: Solver -> Solver -> Bool #
Data Solver Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Solver -> c Solver # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Solver # toConstr :: Solver -> Constr # dataTypeOf :: Solver -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Solver) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Solver) # gmapT :: (forall b. Data b => b -> b) -> Solver -> Solver # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Solver -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Solver -> r # gmapQ :: (forall d. Data d => d -> u) -> Solver -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Solver -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Solver -> m Solver # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Solver -> m Solver # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Solver -> m Solver #
Read Solver Source #
Methods readsPrec :: Int -> ReadS Solver # readList :: ReadS [Solver] # readPrec :: ReadPrec Solver # readListPrec :: ReadPrec [Solver] #
Show Solver Source #
Methods showsPrec :: Int -> Solver -> ShowS # show :: Solver -> String # showList :: [Solver] -> ShowS #

data AssumeLiterals Source #

Constructors

Poly
Unitless
Mixed

Instances

Eq AssumeLiterals Source #
Methods (==) :: AssumeLiterals -> AssumeLiterals -> Bool # (/=) :: AssumeLiterals -> AssumeLiterals -> Bool #
Data AssumeLiterals Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AssumeLiterals -> c AssumeLiterals # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AssumeLiterals # toConstr :: AssumeLiterals -> Constr # dataTypeOf :: AssumeLiterals -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c AssumeLiterals) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssumeLiterals) # gmapT :: (forall b. Data b => b -> b) -> AssumeLiterals -> AssumeLiterals # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AssumeLiterals -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AssumeLiterals -> r # gmapQ :: (forall d. Data d => d -> u) -> AssumeLiterals -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AssumeLiterals -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AssumeLiterals -> m AssumeLiterals # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AssumeLiterals -> m AssumeLiterals # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AssumeLiterals -> m AssumeLiterals #
Read AssumeLiterals Source #
Methods readsPrec :: Int -> ReadS AssumeLiterals # readList :: ReadS [AssumeLiterals] # readPrec :: ReadPrec AssumeLiterals # readListPrec :: ReadPrec [AssumeLiterals] #
Show AssumeLiterals Source #
Methods showsPrec :: Int -> AssumeLiterals -> ShowS # show :: AssumeLiterals -> String # showList :: [AssumeLiterals] -> ShowS #

data UnitConstant Source #

Constructors

Unitful [(Name, Rational)]
UnitlessC Rational

Instances

Eq UnitConstant Source #
Methods (==) :: UnitConstant -> UnitConstant -> Bool # (/=) :: UnitConstant -> UnitConstant -> Bool #
Fractional UnitConstant Source #
Methods (/) :: UnitConstant -> UnitConstant -> UnitConstant # recip :: UnitConstant -> UnitConstant # fromRational :: Rational -> UnitConstant #
Data UnitConstant Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnitConstant -> c UnitConstant # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnitConstant # toConstr :: UnitConstant -> Constr # dataTypeOf :: UnitConstant -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c UnitConstant) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnitConstant) # gmapT :: (forall b. Data b => b -> b) -> UnitConstant -> UnitConstant # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnitConstant -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnitConstant -> r # gmapQ :: (forall d. Data d => d -> u) -> UnitConstant -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnitConstant -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnitConstant -> m UnitConstant # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnitConstant -> m UnitConstant # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnitConstant -> m UnitConstant #
Num UnitConstant Source #
Methods (+) :: UnitConstant -> UnitConstant -> UnitConstant # (-) :: UnitConstant -> UnitConstant -> UnitConstant # (*) :: UnitConstant -> UnitConstant -> UnitConstant # negate :: UnitConstant -> UnitConstant # abs :: UnitConstant -> UnitConstant # signum :: UnitConstant -> UnitConstant # fromInteger :: Integer -> UnitConstant #
Show UnitConstant Source #
Methods showsPrec :: Int -> UnitConstant -> ShowS # show :: UnitConstant -> String # showList :: [UnitConstant] -> ShowS #

newtype VarCol Source #

Constructors

VarCol Col

Instances

Eq VarCol Source #
Methods (==) :: VarCol -> VarCol -> Bool # (/=) :: VarCol -> VarCol -> Bool #
Show VarCol Source #
Methods showsPrec :: Int -> VarCol -> ShowS # show :: VarCol -> String # showList :: [VarCol] -> ShowS #
UpdateColInfo ProcedureEnv Source #
Methods updateColInfo :: Col -> Col -> ProcedureEnv -> ProcedureEnv Source #
UpdateColInfo Procedure Source #
Methods updateColInfo :: Col -> Col -> Procedure -> Procedure Source #
UpdateColInfo VarColEnv Source #
Methods updateColInfo :: Col -> Col -> VarColEnv -> VarColEnv Source #
UpdateColInfo VarCol Source #
Methods updateColInfo :: Col -> Col -> VarCol -> VarCol Source #

newtype VarBinder Source #

Constructors

VarBinder (Name, SrcSpan)

Instances

Show VarBinder Source #
Methods showsPrec :: Int -> VarBinder -> ShowS # show :: VarBinder -> String # showList :: [VarBinder] -> ShowS #
UpdateColInfo VarColEnv Source #
Methods updateColInfo :: Col -> Col -> VarColEnv -> VarColEnv Source #

type VarColEnv = [(VarBinder, (VarCol, [VarCol]))] Source #

data UnitVarCategory Source #

Constructors

Literal EqualityConstrained
Temporary
Variable
Argument
Magic

Instances

Eq UnitVarCategory Source #
Methods (==) :: UnitVarCategory -> UnitVarCategory -> Bool # (/=) :: UnitVarCategory -> UnitVarCategory -> Bool #
Show UnitVarCategory Source #
Methods showsPrec :: Int -> UnitVarCategory -> ShowS # show :: UnitVarCategory -> String # showList :: [UnitVarCategory] -> ShowS #

type DerivedUnitEnv = [(Name, UnitConstant)] Source #

type ProcedureNames = (String, Maybe Name, [Name]) Source #

type Procedure = (Maybe VarCol, [VarCol]) Source #

type ProcedureEnv = [(String, Procedure)] Source #

type LinearSystem = (Matrix Rational, [UnitConstant]) Source #

type Row = Int Source #

type Col = Int Source #

type DebugInfo = [(Col, (SrcSpan, String))] Source #

data UnitAnnotation a Source #

Constructors

UnitAnnotation
Fields prevAnnotation :: a unitSpec :: Maybe UnitStatement unitInfo :: Maybe UnitInfo unitBlock :: Maybe (Block (Analysis (UnitAnnotation a)))

Instances

Data a => Data (UnitAnnotation a) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnitAnnotation a -> c (UnitAnnotation a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (UnitAnnotation a) # toConstr :: UnitAnnotation a -> Constr # dataTypeOf :: UnitAnnotation a -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (UnitAnnotation a)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (UnitAnnotation a)) # gmapT :: (forall b. Data b => b -> b) -> UnitAnnotation a -> UnitAnnotation a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnitAnnotation a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnitAnnotation a -> r # gmapQ :: (forall d. Data d => d -> u) -> UnitAnnotation a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnitAnnotation a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnitAnnotation a -> m (UnitAnnotation a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnitAnnotation a -> m (UnitAnnotation a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnitAnnotation a -> m (UnitAnnotation a) #
Show a => Show (UnitAnnotation a) Source #
Methods showsPrec :: Int -> UnitAnnotation a -> ShowS # show :: UnitAnnotation a -> String # showList :: [UnitAnnotation a] -> ShowS #

dbgUnitAnnotation :: UnitAnnotation t -> [Char] Source #

mkUnitAnnotation :: a -> UnitAnnotation a Source #

data UnitEnv Source #

Constructors

UnitEnv

Fields

_report :: [String]
_varColEnv :: VarColEnv
_derivedUnitEnv :: DerivedUnitEnv
_procedureEnv :: ProcedureEnv
_calls :: ProcedureEnv
_unitVarCats :: [UnitVarCategory]
_reorderedCols :: [Int]
_underdeterminedCols :: [Int]
_linearSystem :: LinearSystem
_debugInfo :: DebugInfo
_tmpRowsAdded :: [Int]
_tmpColsAdded :: [Int]
_success :: Bool
_evUnitsAdded :: (Int, [String])
_evCriticals :: [Int]
_puname :: Maybe ProgramUnitName
_hasDeclaration :: [Name]

Instances

Show UnitEnv Source #
Methods showsPrec :: Int -> UnitEnv -> ShowS # show :: UnitEnv -> String # showList :: [UnitEnv] -> ShowS #

emptyUnitEnv :: UnitEnv Source #

varColEnv :: forall cat. ArrowApply cat => Lens cat UnitEnv VarColEnv Source #

unitVarCats :: forall cat. ArrowApply cat => Lens cat UnitEnv [UnitVarCategory] Source #

underdeterminedCols :: forall cat. ArrowApply cat => Lens cat UnitEnv [Int] Source #

tmpRowsAdded :: forall cat. ArrowApply cat => Lens cat UnitEnv [Int] Source #

tmpColsAdded :: forall cat. ArrowApply cat => Lens cat UnitEnv [Int] Source #

success :: forall cat. ArrowApply cat => Lens cat UnitEnv Bool Source #

report :: forall cat. ArrowApply cat => Lens cat UnitEnv [String] Source #

reorderedCols :: forall cat. ArrowApply cat => Lens cat UnitEnv [Int] Source #

puname :: forall cat. ArrowApply cat => Lens cat UnitEnv (Maybe ProgramUnitName) Source #

procedureEnv :: forall cat. ArrowApply cat => Lens cat UnitEnv ProcedureEnv Source #

linearSystem :: forall cat. ArrowApply cat => Lens cat UnitEnv LinearSystem Source #

hasDeclaration :: forall cat. ArrowApply cat => Lens cat UnitEnv [Name] Source #

evUnitsAdded :: forall cat. ArrowApply cat => Lens cat UnitEnv (Int, [String]) Source #

evCriticals :: forall cat. ArrowApply cat => Lens cat UnitEnv [Int] Source #

derivedUnitEnv :: forall cat. ArrowApply cat => Lens cat UnitEnv DerivedUnitEnv Source #

debugInfo :: forall cat. ArrowApply cat => Lens cat UnitEnv DebugInfo Source #

calls :: forall cat. ArrowApply cat => Lens cat UnitEnv ProcedureEnv Source #

unitMult :: UnitConstant -> UnitConstant -> UnitConstant Source #

unitScalarMult :: Rational -> UnitConstant -> UnitConstant Source #

convertUnit :: UnitInfo -> State UnitEnv UnitConstant Source #

toUnitInfo :: UnitOfMeasure -> UnitInfo Source #

(<<) :: MonadState f m => Lens (->) f [o] -> o -> m () infix 2 Source #

(<<++) :: MonadState f m => Lens (->) f [a] -> a -> m () infix 2 Source #

Operations on unit environments

addCol :: UnitVarCategory -> State UnitEnv Int Source #

addRow :: State UnitEnv Int Source #

addRow' :: UnitConstant -> State UnitEnv Int Source #

liftUnitEnv :: (Matrix Rational -> Matrix Rational) -> UnitEnv -> UnitEnv Source #

resetTemps :: State UnitEnv () Source #

lookupCaseInsensitive :: String -> [(String, a)] -> Maybe a Source #

lookupWithoutSrcSpan :: Name -> [(VarBinder, a)] -> Maybe a Source #

lookupWithSrcSpan :: Name -> SrcSpan -> [(VarBinder, a)] -> Maybe a Source #

trim :: [(t, Rational)] -> [(t, Rational)] Source #

data Consistency a Source #

Constructors

Ok a
Bad a Int (UnitConstant, [Rational])

Instances

Show a => Show (Consistency a) Source #
Methods showsPrec :: Int -> Consistency a -> ShowS # show :: Consistency a -> String # showList :: [Consistency a] -> ShowS #

efmap :: (a -> a) -> Consistency a -> Consistency a Source #

ifDebug :: (?debug :: Bool, Monad m) => m a -> m () Source #