Previous Up Next

Interface for module Red

The module contains functions and data-structures related to reduction. They are based on term rewriting and insofar independent of the transducer. On the other hand the module takes already care of the specific form of terms used (taking parameters for instance).
typeqterm=intlist
valqmatch:(qtermנqtermנqtermנqterm)→(qtermנqtermנqtermנqterm)
valqmatch_all:(qtermנqtermנqtermנqterm)→(qtermנqtermנqtermנqterm)list
valqsubst:(qtermנqterm)→qtermqterm
valqsubst_all:(qtermנqterm)→qtermqtermlist
valqrewrite:(qtermנqterm)listqtermqterm(∗ internal use ∗)
valqonestep:(qtermנqterm)listqtermqtermlist

valqoverlap:(qtermנqtermנqtermנqterm)→(qtermנqtermנqtermנqterm)
valqcrit_pairs:((qtermנqterm)נ(qtermנqterm))→(qtermנqterm)list
valqpair_is_joinable_or_equal:(qtermנqterm)list→(qtermנqterm)→bool
valqpair_is_joinable_or_equal2:
((qtermנqterm)list)נ((qtermנqterm)list)→
(qtermנqterm)→bool
valqhas_diamondprop:(qtermנqterm)listbool
valqhas_swappingdiamondprop:((qtermנqterm)list)נ((qtermנqterm)list)→bool

valqnorm:(qtermנqterm)listqtermqterm
valqnorm_starstate:(qtermנqterm)listintlistlistintlistlist
valnormalize_rewrite_eqns:(qtermנqterm)list→(qtermנqterm)list

typeαvsubst

exceptionNo_Match

valv_appvsubst→αterm→αterm
valtermmatch:(αterm)נ(αterm)→αvsubst(∗ t1σ = t2 ∗)
valterms_match:((αterm)נ(αterm))list→αvsubst
valrule_o_termrule→αterm→αtermlist
valone_or_0_step:(αrule)list→αterm→(αterm)list
valreduce_until:(αrule)list→(αtermbool)→αterm→(αterm)list

A function for diagnosis
valprint_vsubst:(α→string)→αvsubstunit


Previous Up Next