trs [-r] file


     trs  rewrites  terms given by the user, either interactively or through
     standard input.  Rewriting is done according to the TIL-code, which  is
     read  from  file.  The result of rewritings is written on standard out-

     Terms given by the user, must be in the form as in a PSF specification.
     trs  uses  inside  out  type  checking for deciding which item is to be
     used.  When there are items with the same  name  and  types  for  their
     arguments,  they  have  to be disambiguated by specifying the module it
     originates from, as in:
     which specifies item from module X.

     In rewriting the terms, trs uses the rightmost-innermost strategy.

     trs ends when an end of file is detected or when given an empty line.

     When an error has been found in parsing a term,  a  message  about  the
     error  is  generated  on standard error, followed by the term, with ???
     inserted after the place the error was found.  Due to infix  operators,
     the  ???   may  be placed a little further ahead in the term then where
     the error was found.

     There is a possibility for tracing in trs.  The command
            > trace on
     sets tracing on.  Tracing can be put off, by changing on to off in  the
     above command.  The space between > and trace is optional.

     Also some statistics on rewriting can be obtained with the command
            > stat
     This  gives  the  numbers  of  matches and the number of tries for each
     rewrite- rule done so far.  These numbers can be reset withe  the  com-
            > stat reset


     -h     Prints a help message.

     -r     Term rewriting is done with the equations in reverse order.

     -v     Displays the version number of trs.




     Bob Diertens, University of Amsterdam (