-- |
-- Copyright : (c) 2010, 2011 Benedikt Schmidt
-- License : GPL v3 (see LICENSE)
--
-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>
--
-- Builtin rewriting rules.
module Term.Builtin.Rules (
-- * Rewriting rules
RRule(..)
, dhRules
, xorRules
, msetRules
, pairRules
, symEncRules
, asymEncRules
, signatureRules
-- * Convenience export
, module Term.Builtin.Signature
) where
import Term.LTerm
import Term.SubtermRule
import Term.Builtin.Signature
import Term.Builtin.Convenience
-- Rules for DH theory
----------------------------------------------------------------------
-- | The rewriting rules for Diffie-Hellman. This is a presentation due to Lankford
-- with the finite variant property.
dhRules :: [RRule LNTerm]
dhRules =
[ expo(x1,one) `RRule` x1
, expo(expo(x1,x2),x3) `RRule` expo(x1,(x2 *: x3))
, x1 *: one `RRule` x1
, inv (inv x1) `RRule` x1
, inv one `RRule` one
, x1 *: (inv x1) `RRule` one
, inv x1 *: inv x2 `RRule` inv (x1 *: x2)
, inv (x1 *: x2) *: x2 `RRule` inv x1
, inv (inv x1 *: x2) `RRule` (x1 *: inv x2)
, x1 *: (inv (x1) *: x2) `RRule` x2
, inv x1 *: (inv x2 *: x3) `RRule` (inv (x1 *: x2) *: x3)
, inv (x1 *: x2) *: (x2 *: x3) `RRule` (inv x1 *: x3)
]
-- | The rewriting rules for Xor.
xorRules :: [RRule LNTerm]
xorRules =
[ x1 +: x1 `RRule` zero
, x1 +: zero `RRule` x1
, x1 +: (x1 +: x2) `RRule` x2 ]
-- | The rewriting rules for multisets.
msetRules :: [RRule LNTerm]
msetRules = [ s1 # empty `RRule` s1 ]
-- | The rewriting rules for standard subterm operators that are builtin.
pairRules, symEncRules, asymEncRules, signatureRules :: [StRule]
pairRules =
[ fstC (pair (x1,x2)) `StRule` (RhsPosition [0,0])
, sndC (pair (x1,x2)) `StRule` (RhsPosition [0,1]) ]
symEncRules = [ sdec (senc (x1,x2), x2) `StRule` (RhsPosition [0,0]) ]
asymEncRules = [ adec (aenc (x1, pk x2), x2) `StRule` (RhsPosition [0,0]) ]
signatureRules = [ verify (sign (x1,x2), x1, pk x2) `StRule` (RhsGround trueC) ]