| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Numeric.Limp.Canon.Simplify.Subst
Description
Substitute an assignment into functions, constraints and programs
- substLinear :: (Ord z, Ord r, Rep c) => Assignment z r c -> Linear z r c -> (Linear z r c, R c)
- substConstraint1 :: (Ord z, Ord r, Rep c) => Assignment z r c -> Constraint1 z r c -> Constraint1 z r c
- substConstraint :: (Ord z, Ord r, Rep c) => Assignment z r c -> Constraint z r c -> Constraint z r c
- substProgram :: (Ord z, Ord r, Rep c) => Assignment z r c -> Program z r c -> Program z r c
Documentation
substLinear :: (Ord z, Ord r, Rep c) => Assignment z r c -> Linear z r c -> (Linear z r c, R c) Source #
Substitute assignment into linear function.
However, Linear isn't quite a linear function! That is, it doesn't have a constant summand.
So we must return the constant summand we lose.
Satisfies:
forall a b f. let (f', c') = substLinear a f in eval (a <> b) f == eval b f' + c'
subst (x := 5) in 2x + y (y, 10)
substConstraint1 :: (Ord z, Ord r, Rep c) => Assignment z r c -> Constraint1 z r c -> Constraint1 z r c Source #
Substitute assignment into a single linear constraint.
See substConstraint.
5 <= 2x + y <= 10 subst (y := 3) 2 <= 2x <= 7
substConstraint :: (Ord z, Ord r, Rep c) => Assignment z r c -> Constraint z r c -> Constraint z r c Source #
Substitute assignment into a set of linear constraints. Satisfies:
forall a b f. let c' = substConstraint a c in check (a <> b) c == check b c'
subst (x := 5) in 15 <= 2x + y <= 20 5 <= y <= 10
substProgram :: (Ord z, Ord r, Rep c) => Assignment z r c -> Program z r c -> Program z r c Source #
Substitute assignment into a program. What does this satisfy? Hm.