cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright(c) 2014-2016 Galois, Inc.
Safe HaskellSafe



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.



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

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

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).