REPIUS is a tool that (fully or partially) inverts a constructor TRS
written in a .trs
file and unravels the resulting
inverse CTRS.
The prototype (Ver. 0.x) was developed following the approach in [NSS05a] and optionally employs unraveling
transformations as a post-process of inversion.
The current version was wholly implemented, introducing a new approach to
tail-recursive functions into the previous approach to full inversion
[NSS05b].
The MSV transformation [NV12] can be
optionally applied to inverted systems.
The partial inversion approach [NSS05a] will be implemented
as an extension.
The current implementation is based on the technique in [NV11].
-noinversion
, -version
and
-verbose
were added.
du
operator.
!! The download version is now outdated. !!
This is written in OCaml and compiled by
OCaml-Java (ocamljava 1.4
).
repius.jar (Jun 27, 2012)
Note: Java 1.6 is required.
java -jar repius.jar
filename
java -jar repius.jar -ieice05 [--sp]
filename
The suboption --sp
provides the special rules for each inverses.
-noinversion
-msv
[--depth
n]--depth
n specifies the
depth of leftmost innermost basic narrowing trees used in
the transformation, e.g., --depth1
.
The default depth is 2 * m + 1 where m
is the maximum number of conditions in rewrite rules.
-U
[--original
|
--optimized
]-msv
is specified.
The default is Ohlebusch's one.
Marchiori's original one is used if the suboption
--original
is specified, and the optimized one
is used if the suboption --optimized
is used.
-version
-verbose
.trs
format if this option is specified.
-
opt are ignored.
Repius recognizes .trs
format files,
CTRSs in which satisfy
all of the following:
du
operator (see pack.trs
)du(single(t1)) -> pair(u1,u2)
, du(pair(t1,t2)) -> single(u1)
, or du(pair(t1,t2)) ->
pair(u1,u2)
, name | .fct style | .trs style | remarks | wui |
---|---|---|---|---|
snoc | snoc.fct | snoc.trs | ||
reverse | reverse.fct | reverse.trs | ||
snocrev | snocrev.fct | snocrev.trs | ||
double | double.fct | double.trs | ||
mirror | mirror.fct | mirror.trs | ||
zip | zip.fct | zip.trs | ||
inc | inc.fct | inc.trs | ||
unbin | unbin.fct | unbin.trs | ||
octbin | octbin.fct | octbin.trs | ||
treelist | treelist.fct | treelist.trs | ||
treepaths | treepaths.fct | treepaths.trs | ||
pack | pack.fct | pack.trs | ||
pack-bin | packbin.fct | packbin.trs | ||
print-sexp | printsexp.fct | printsexp.trs | ||
print-xml | printxml.fct | printxml.trs |
name | .fct style | .trs style | remarks | wui |
---|---|---|---|---|
reverse2 | reverse2.fct | reverse2.trs | ||
unbin2 | unbin2.fct | unbin2.trs | ||
unbin3 | unbin3.fct | unbin3.trs | ||
treelist2 | treelist2.fct | treelist2.trs |
name | .fct style | .trs style | remarks | wui |
---|---|---|---|---|
inv-reverse | inv-reverse.fct | inv-reverse.trs | ||
inv-unbin | inv-unbin.fct | inv-unbin.trs | ||
inv-treepaths | inv-treepaths.fct | inv-treepaths.trs |
name | .fct style | .trs style | remarks | wui |
---|---|---|---|---|
lrinv-reverse | lrinv-reverse.fct | lrinv-reverse.trs | ||
lrinv-unbin | lrinv-unbin.fct | lrinv-unbin.trs | ||
lrinv-treepaths | lrinv-treepaths.fct | lrinv-treepaths.trs |
name | .fct style | .trs style | remarks | wui |
---|---|---|---|---|
snoc-tail | snoc-tail.fct | snoc-tail.trs | ||
reverse-tail | reverse-tail.fct | reverse-tail.trs | ||
snocrev-tail | snocrev-tail.fct | snocrev-tail.trs | ||
double-tail | double-tail.fct | double-tail.trs | ||
mirror-tail | mirror-tail.fct | mirror-tail.trs | ||
zip-tail | zip-tail.fct | zip-tail.trs | ||
inc-tail | inc-tail.fct | inc-tail.trs | ||
unbin-tail | unbin-tail.fct | unbin-tail.trs | ||
octbin-tail | octbin-tail.fct | octbin-tail.trs | ||
treepaths-tail1 | treepaths-tail1.fct | treepaths-tail1.trs | ||
treepaths-tail2 | treepaths-tail2.fct | treepaths-tail2.trs | ||
pack-tail | pack-tail.fct | pack-tail.trs | ||
pack-bin-tail | packbin-tail.fct | packbin-tail.trs | ||
print-sexp-tail1 | printsexp-tail1.fct | printsexp-tail1.trs | ||
print-sexp-tail2 | printsexp-tail2.fct | printsexp-tail2.trs | ||
print-xml-tail1 | printxml-tail1.fct | printxml-tail1.trs | ||
print-xml-tail2 | printxml-tail2.fct | printxml-tail2.trs | ||
print-xml-tail3 | printxml-tail3.fct | printxml-tail3.trs |
name | .fct style | .trs style | remarks | wui |
---|---|---|---|---|
exp | exp.fct | exp.trs |
nishida @ is.nagoya-u.ac.jp