Data.Logic.Classes.Term

Documentation

class (Ord term, Variable v, Function f v) => Term term v f | term -> v f where

Methods

vt :: v -> term

Build a term which is a variable reference.

fApp :: f -> [term] -> term

Build a term by applying terms to an atomic function. f (atomic function) is one of the type parameters, this package is mostly indifferent to its internal structure.

foldTerm :: (v -> r) -> (f -> [term] -> r) -> term -> r

A fold for the term data type, which understands terms built from a variable and a term built from the application of a primitive function to other terms.

zipTerms :: (v -> v -> Maybe r) -> (f -> [term] -> f -> [term] -> Maybe r) -> term -> term -> Maybe r

Instances

Term TermType String Function

(Variable v, Function f v) => Term (NormalTerm v f) v f

(Variable v, Function f v) => Term (CTerm v f) v f

(Variable v, Function f v) => Term (PTerm v f) v f

class (Eq f, Ord f, Skolem f v, Data f, Pretty f) => Function f v

Instances

Function Function String

convertTerm :: forall term1 v1 f1 term2 v2 f2. (Term term1 v1 f1, Term term2 v2 f2) => (v1 -> v2) -> (f1 -> f2) -> term1 -> term2

showTerm :: forall term v f. (Term term v f, Show v, Show f) => term -> String

prettyTerm :: forall v f term. Term term v f => (v -> Doc) -> (f -> Doc) -> term -> Doc

fvt :: (Term term v f, Ord v) => term -> Set v

tsubst :: (Term term v f, Ord v) => Map v term -> term -> term

funcs :: (Term term v f, Ord f) => term -> Set (f, Int)