NAME
Ani - An Interpreter for Action Notation.

SYNOPSIS
~/ani/ani

DESCRIPTION
Action semantics is a formalism for the specification of programming
languages [1,2]. In action semantics the meaning of a program is an
action. Ani is an interpreter for actions: given an action, Ani will
perform it. The outcome of the performance can be visualized through
a convenient output. 

SOME FEATURES
'A1 or A2' is pseudo-nondeterministic.

The sort operations 'meet' and 'join' can be used to construct
new sorts. Also the 'subsort' relation is defined.

'the <user_def_sort>' == 'the datum'.

OUTPUT
The result of the interpretation of an action has the fol-
lowing format:

Outcome Completed!
Transients { 0 --> 40 }
{ 1 --> 50.0 }
{ 2 --> 40 }
Bindings { y --> 2 }
{ z --> cell 0 }
Storage { cell 0 --> 10.0 }
Commitment Uncommitted action!

For example, the interpretation of the action

bind "x" to 4 or bind "y" to true

has the two possible outputs below:

Outcome Completed!
Transients empty-transients
Bindings { y --> true }
Storage empty-storage
Commitment Uncommitted action!

Outcome Completed!
Transients empty-transients
Bindings { x --> 4 }
Storage empty-storage
Commitment Uncommitted action!

If an action diverges Ani diverges, and in this case, there
is no output (the action 'diverge' is interpreted as
'unfolding unfold').

USAGE
After load the interpreter, you will see the interpreter
prompt 'Ani '. To see information about Ani type 'help
Ani;'. The following examples illustrate how to use Ani:

Example 1. To interpret the action 'give 4 then complete':

Ani ia "give 4 then complete";

Example 2. To interpret the action 'bind "x" to 4.0':

Ani ia "bind \"x\" to 4.0";

Example 3. To interpret the action 'fail or diverge', that
is in a file called 'crazy':

Ani iaf "crazy";

Example 4. If an action is in its action tree form
(abstract syntax tree for): 

Ani iat f02;

where 'f02' is an SML value of type '(int * int) AST'
(in this case the action notation parser will be 
by passed).

Example 5. You can generate the action tree that
stands for the action 'complete' typing:

Ani gat "complete" "f03";

This will create a file called 'f03.an.sml' that 
contains a value 'f03' of type '(int * int) AST'. 
This file can be load directly into Ani (type 
'use "f03.an.sml";').

Example 6. To generate the action tree file from a file that already
contains an action use:

Ani gatf "d04";

Example 7. You can pretty print an action tree to a file using
the patf function:

Ani patf at "f07";

This will create the file 'f07.an' that contains a
pretty printed form of the action tree 'at'. This
action can be interpreted by using iaf (see Example 3).

VALUES AVAILABLE AT TOP LEVEL
gat "<action>" "<filename>"
Takes an action and a file name. Generates the
correspondent action tree and writes it into a file named
'<filename>.an.sml'. This file is ready to be loaded
into Ani.

gatf "<filename>"
Takes a file that contains an action ('<filename>.an'). Gen-
erates the correspondent action tree and writes it into a file
named '<filename>.an.sml'. This file is ready to be
loaded into Ani.

ia "<action>"
Interprets the action <action>.

iaf "<filename>"
Interprets the action in the file '<filename>.an'.

iat <ASTvalue>
Interprets the action tree <ASTvalue>.

parse "<action>"
Parses the action <action>.

parsef "<filename>"
Parses the action in the file '<filename>.an'.

pat <ASTvalue>
Pretty prints the action tree <ASTvalue>.

patf <ASTvalue> "<filename>"
Pretty prints the action tree <ASTvalue> in
the file '<filename>.an'. After this, you can use 
'iaf "<filename>";' to interpret the action in the file.

The following useful Unix commands are also available at top
level:

cd "<cd_arguments>"
ls "<ls_argumenst>"
more "<more_arguments>"
pwd "<pwd_arguments>"

After the interpretation of an action, the following Ani
commands can be used to inspect the contents of transients,
bindings and storage and the commitment status, in the form
they are represented internally.

give transients
give bindings
give storage
give commitment

The following table gives the types and abbreviations used
for values available at top level:

=============================================================
Name Type
-------------------------------------------------------------
gat string -> string -> unit
gatf string -> unit 
ia string -> unit 
iaf string -> unit 
iat (int * int) ActionAST.AST -> unit
parse string -> ANParser.result
parsef string -> unit 
pat 'a ActionAST.AST -> unit
patf 'a ActionAST.AST -> string -> unit

cd string -> unit
ls string -> unit 
more string -> unit 
pwd 'a -> unit
=============================================================


DATA NOTATION
The following data notation sorts and operations are imple-
mented in Ani:

_ is _ if _ then _ else _

meet(_,_) join(_,_) subsort(_,_)

not(_) conjunction(_,_) disjunction(_,_)

natural(_) successor(_) predecessor(_) 
sum(_,_) difference(_,_) product(_,_) 
quotient(_,_) isLessThan(_,_) isGreaterThan(_,_)
negation(_)

emptyList list(_,_) concatenation(_,_) 
reverse(_) headOf(_) tailOf(_) 
lengthOf(_) componentsOf(_)

emptySet set(_) intersection(_,_)
union(_,_) disjointUnion(_,_) differenceSet(_,_)
sizeOf(_) isIn(_,_) isSubsetOf(_,_)

emptyMap mapTo(_,_) merge(_,_) 
overlay(_,_) omission(_,_) domainOf(_) 
rangeOf(_) at(_,_)

cellNotIn(_,_)

Individual sorts are defined as well as the following sorts;

datum abstraction distinguishable
number real integer
natural truthValue transients
token bindings cell
storage list listOf(_) 
set setOf(_) map 
mapOf(_,_) meet(_,_) join(_,_) 

FILES
~/ani/ani Ani executable file
~/ani/CONDITIONS copyright note
~/ani/FILES directory tree of Ani files
~/ani/HISTORY history of this and previous versions
~/ani/INSTALLATION installation guide
~/ani/MANUAL this file (manual page)
~/ani/README general information on Ani
~/ani/actions/ many examples of actions
~/ani/parser/ action notation parser source files
~/ani/src/ action notation interpreter source files 

STANDARD ML
Standard ML of New Jersey, Version 75, November 11, 1991.

VERSION
Version 0.13 22 February 1992 (beta version).

AUTHOR
Hermano Moura (moura@dcs.glasgow.ac.uk)
University of Glasgow
Department of Computing Science

Deryck Brown (University of Glasgow) provided the action notation
parser used by Ani.

SEE ALSO
ag (actioneer generator).

REFERENCES
[1] Peter D. Mosses. "Action Semantics". Cambridge University Press,
1992. In preparation.

[2] David A. Watt. "Programming Language Syntax and Semantics".
Prentice Hall, 1991.