Safe Haskell	Safe-Inferred
Language	Haskell2010

CoALP.RewTree

Description

Construction of a rewriting tree

Synopsis

Documentation

rew :: (Eq a, Eq b, Eq c, Ord c, Freshable c, Freshable d) => Program a b c -> Clause a b c -> Subst a b c -> RewTree a b c d

Construct a rewriting tree given program P, clause C and substitution σ

	rew (P, C, σ)

according to Definition 3.3

extrew :: (Eq a, Eq b, Eq c, Ord c, Freshable c, Freshable d) => Program a b c -> RewTree a b c d -> Subst a b c -> RewTree a b c d

Given rewriting tree rew(P, C, σ) and X = T(wi) ∈ V_R construct new rewriting tree T_X accroding to Definition 3.5

getVrs :: RewTree a b c d -> [(Vr d, Term a b c, Int)]

Get Transition Variables in breath-first search manner

for GC3 is fine to proceed in DFS, however for displaying the search up-to-depth n the BFS is necessary

loops :: (Eq a, Freshable d) => RewTree a b c d -> [(Term a b c, Term a b c, Int)]

Given rewriting tree compute loops as described in the Definition 5.2