tamarin-prover-term-0.8.5.1: Term manipulation library for the tamarin prover.

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone

Term.Maude.Parser

Contents

Description

Pretty printing and parsing of Maude terms and replies.

Synopsis

pretty printing of terms for Maude

ppMaude :: Term MaudeLit -> ByteStringSource

ppMaude t pretty prints the term t for Maude.

ppTheory :: MaudeSig -> ByteStringSource

The term algebra and rewriting rules as a functional module in Maude.

parsing of Maude replies

parseUnifyReply :: MaudeSig -> ByteString -> Either String [MSubst]Source

parseUnifyReply reply takes a reply to a unification query returned by Maude and extracts the unifiers.

parseMatchReply :: MaudeSig -> ByteString -> Either String [MSubst]Source

parseMatchReply reply takes a reply to a match query returned by Maude and extracts the unifiers.

parseReduceReply :: MaudeSig -> ByteString -> Either String MTermSource

parseReduceReply l parses a single solution returned by Maude.