Numeric.Limp.Canon.Simplify.Subst

Substitute an assignment into functions, constraints and programs

Documentation

substLinear :: (Ord z, Ord r, Rep c) => Assignment z r c -> Linear z r c -> (Linear z r c, R c)

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

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

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

Substitute assignment into a program. What does this satisfy? Hm.