Safe Haskell	Safe-Inferred
Language	Haskell2010

CoALP.DerTree

Contents

Tree constructions
Rewritng tree variable

Description

Construction of a derivation tree

Synopsis

Tree constructions

der :: (Eq a, Eq b, Eq d, Ord c, Freshable c, Freshable d) => Program a b c -> Clause a b c -> DerTree a b c d

Given a program P and a clause C construct derivation tree

	der(P, C)

according to definition 3.6

trans :: (Eq a, Eq b, Ord c, Eq d, Freshable c, Freshable d) => Program a b c -> RewTree a b c d -> Vr d -> (RewTree a b c d, Maybe (Int, Subst a b c, Term a b c))

Given a program P, rewriting tree rew(P, C, σ) at position w and rewriting tree variable X_k construct the rewritng tree

	Trans(P, D(w), X_k) = rew(P, C, σ'σ)

and return the external resolvent σ, contraction measure, and the originating clause according to Definition 3.5

clauseProj :: (Eq a, Eq b, Ord c) => Program a b c -> Maybe (Int, Subst a b c, Term a b c) -> GuardingContext a b c

Given program P and external resolvent of a transition with its measure conpute clause projection

	π(D(w)) = {P(k), t', v | ... }

accorging to definition 5.4

Rewritng tree variable

newtype Vr a

Type of Rew tree Variable

Constructors

Vr
Fields unVr :: a

Instances

Functor Vr
Eq a => Eq (Vr a)
(Integral a, Show a) => Show (Vr a)
NFData (Vr d)
NFData (OrNode (Clause a b c) (Term a b c) (Vr d))
NFData (Term a b c) => NFData (AndNode (Clause a b c) (Term a b c) (Vr d))