cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2014-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Numeric.NonLin

Description

Separate Non-Linear Constraints When we spot a non-linear expression, we name it and add it to a map.

If we see the same expression multiple times, then we give it the same name.

The body of the non-linear expression is not processed further, so the resulting map should not contain any of the newly minted names.

Synopsis

- nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS)
- data NonLinS
- nonLinSubst :: NonLinS -> Subst
- initialNonLinS :: NonLinS
- apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS)
- lookupNL :: Name -> NonLinS -> Maybe Expr

# Documentation

nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS) Source #

Factor-out non-linear terms, by naming them.

data NonLinS Source #

Instances

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

nonLinSubst :: NonLinS -> Subst Source #

Get the known non-linear terms.

initialNonLinS :: NonLinS Source #

The initial state for the linearization process.

apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS) Source #

Apply a substituin to the non-linear expression database. Returns `Nothing` if nothing was affected. Otherwise returns `Just`, and a substitution for non-linear expressions that became linear.

The definitions of NL terms do not contain other named NL terms, so it does not matter if the substitution contains bindings like `_a = e`.

There should be no bindings that mention NL term names in the definitions of the substition (i.e, things like `x = _a` are NOT ok).

lookupNL :: Name -> NonLinS -> Maybe Expr Source #