# An Overview of AsmGofer

(Wolfram Schulte and Joachim Schmid)

AsmGofer is an advanced Abstract State Machine (ASM) programming system, which runs under several platforms (Unix-based or MS-based operating systems). The aim of the AsmGofer system is to provide a modern ASM interpreter embedded in the well known functional programming language Gofer. Gofer is a subset of Haskell -- the de-facto standard for strongly typed lazy functional programming languages. The purpose of this short introduction is to give a brief overview of the main features of AsmGofer and to describe its use:

#### Instead of an introduction: An example

An AsmGofer program (better called "script") is a collection of signatures, rules, functions and data structures which we are interested in computing. The order in which these entities are given is not significant. Here is a very simple example of an AsmGofer script for a depth first traversal of a directed graph. For simplicity we assume that the nodes of the graph are labelled with integers. The edges are given with a successor function.
```  type Node = Int
succs :: Node -> {Node}```
The range of the successor function is defined using the data structure set, i.e. {Node}. A set is a special version of the commonly used data structure list. An example graph might be a graph that connects 1 to 2 and 3 (i.e. the successors are described by the set {2,3}), 2 to 3 and 4, 3 to 2, 4 to 5, 6 to 1 and for any other node there are no successors.
```  succs 1 = {2,3}
succs 2 = {3,4}
succs 3 = {2}
succs 4 = {5}
succs 6 = {1}
succs _ = {}```
When traversing the graph, we have to remember the visited nodes. We store them in a dynamic function, which is initially nowhere defined (i.e. described by the empty association list).
```  visited :: Dynamic (Node -> Bool)
visited = initAssocs "visited" []```
Remark: the name "visited" is only used for error reporting. This will be eliminated in the future.
For example, let us compute all reachable nodes starting from the node with number 1. We introduce a dynamic variable called todo, that holds all nodes that are still to be processed.
```  todo :: Dynamic [Node]
todo = initVal "todo" [1]```
The traversal of the graph is performed by the following rule called traverse (++ is list concatenation, head and tail select the head and tail of the list.)
```  traverse :: Rule()
traverse = if todo == [] then
skip
else
todo := expr2list(succs(head todo)) ++ tail todo
else
todo := tail todo
```
Notice the absence of syntactic sugar - AsmGofer is, by design, rather terse. There are no mandatory signatures, although the language is strongly typed. For reasons of readablity we nevertheless gave signatures such as
`  succs:: Node -> {Node}`
There are no semicolons at the end of definitions - the parsing algorithm makes intelligent use of layout. Function application is just denoted by juxtaposition, instead of writing
`  f(x)`
we wrote
`  f x`

#### The AsmGofer Environment

The AsmGofer system is interactive. It is invoked from a shell by the command
`  asmgofer [file]`
where `file' (an optional parameter) is the pathname of a file containing an AsmGofer script. We assume that we have stored the previous definitions in a file called "traverse.gs" and that we have called asmgofer with the latter. After parsing and context checking the prompt
`  ?`
occurs, indicating that you are talking to the AsmGofer command interpreter. This activity is called a ``session''. The basic action is to evaluate expressions, supplied by the user at the terminal, in the environment established by the current script. For example evaluating the dynamic function
`  todo`
in the context of the given script produces
```  ? todo [1]
(6 reductions, 29 cells)
```
The first line shows the result, the last line shows the number of reductions and and storage cells needed. The set of names in scope at any time are those of all currently loaded scripts, together with the names of the standard environment (this is the asmgofer prelude), which are always inscope. For instance, we can also evaluate
```  ? todo ++ todo [1,1]
(13 reductions, 42 cells)
```
Remark: Alternatively we could have written
`  \$\$ ++ \$\$`
since \$\$ always denotes the value of the last evaluation. If we want to fire the traverse rule once, we evaluate
```  ? fire1(traverse)
() (42 reductions, 99 cells, 1 steps)
```
which means that the ASM described by the loaded script has made one (non-visible) step -- the result is the empty tuple. Notice that you have to evaluate rules. You can not fire rules by themselves. You can inspect the extension of the visited state as an association list by entering
```  ? assocs(visited)
[(1,True)] (7 reductions, 28 cells)
```
If we want to run the ASM until a fixpoint occurs, you enter:
```  ? fixpoint(traverse)
(208 reductions, 448 cells, 6 steps)
```
For more functions see, the appendix.

Any command not beginning with `:' is assumed to be an expression to be evaluated. The following commands are available during a session
 :load load scripts from specified files, clear all files except prelude :load load last specified files, clear all files except prelude :also load additional scripts files :reload repeat last load command :project use project file :project use last project :edit edit file :edit edit last file :type print type of expression :? display this list of commands :set set command line options :set help on command line options :names [pat] list names currently in scope :info describe named objects (the *pattern matches any string) :find edit file containing definition of name :!command command shell escape :cd dir change directory :gc force garbage collection :quit exit AsmGofer interpreter

Comands may be abbreviated to ":c" where 'c' is the first character of the full command. The AsmGofer compiler works in conjunction with an editor and scripts are automatically recompiled after edits, and any syntax or type errors signaled immediately. The polymorphic type system permits a high proportion of logical errors to be detected at compile time. The location of the prelude must be specified in the variable GOFER. The editor can be specified in the variable EDITLINE. In my installation these variables are specified as follows:
```  export GOFER=/usr/AsmGofer2/Preludes/prelude-asm
export EDITLINE=vi +%d %s
```

#### The AsmGofer Language Extensions

AsmGofer is a conservative extension of Gofer. Although we had to change the run time system (to introduce updatable functions) no changes to the type system were made. New syntactic constructs are
```  <expr> ::= ...
|   forall <quals> do <exp>
|   choose <quals> do <exp>
|   create <var>,...,<var> <expr>
|   <exp> := <exp>
|   skip
```
The types are
```  skip :: Rule ()
(:=) :: AsmTerm a => a -> a -> Rule ()
forall <quals> do <exp> :: Rule ()
choose <quals> do <exp> :: Rule ()
create <var>,...,<var> <expr> :: Rule ()
```
The Rule type is builtin. It guarantees parallel evaluation. The effect of a rule is only visible if rules are fired! Suppose we want to reset the state in our previous example. Then we could write:
```  ? fire1 (do todo := {1}
forall x <-: dom(visited) do
visited(x) := false
)
```
Note that the already existing "do" works as block...endblock. The primitive choose among is not supported in the current release. There is already an experimental version of it available, but it is not yet stable.

#### A final note

ASMs only allow variables and first order functions to be dynamic. However, since Gofer supports higher order functions, not any type is a legal AsmTerm. Therfore the user sometimes has to specify that terms of a particular types can be used in the ASM extension, i.e. the user must specify the type as an AsmTerm type. For an example see below. Furthermore, to check whether updates are consistent, we have to check them for equality and for reasons of efficiency we also require an ordering on the domain. However, since Gofer supports higher order functions, there is no builtin equality (and order). As a consequence, as soon as you use more complex types than the basic types Int, Float, Char or String you must give instances for the class Eq (and AsmOrd). If you do not give an instance for Eq (and AsmOrd) structural equality is the default.
Suppose you want to model a crossing having 4 traffic lights each one can show the colours red, ornage and green, and you want them initially in the state orange then you could write -- Asm(Gofer) Declarations
```  data Where = N | E | W | S
data Colour = Red
| Orange
| Green
trafficLights :: Where -> Colour
trafficLights = initAssocs "trafficLights" [(x,Orange) | x <- [N,E,W,S]]

instance AsmTerm Where
instance AsmTerm Colour
```
Now you can write:
```  ? fire1 (do trafficLights(N) := Red
trafficLights(N) := Orange)
ERROR: inconsistent update
*** dynamic function : "trafficLights"
*** expression (new) : Orange
*** expression (old) : Red
```
which is -- as expected -- an inconsitent update. Note that you can use the value asmDefault to delete something, e.g.
```  ? fire (do trafficLights(N):= asmDefault)
()
? assocs trafficLights
[(East,Orange),(W,Orange),(S,Orange)]
```
Alternatively you can say that a normal value should play the role of asmDefault, i.e. instead of specifying that any trafficLight is Orange you say that Orange is the default. If you change the running example to
```  trafficLights :: Where -> Colour
trafficLights = initAssocs "trafficLights" []
```
(Asm)Gofer Declarations:
```  instance AsmTerm Where
instance AsmTerm Colour where
asmDefault = Orange
```
you can evaluate
```  ? trafficLights(N)
Orange
```

#### The AsmGofer Prelude

The prelude contains the signatures and definitions of all functions available in AsmGofer. For details see the prelude directory in the distribution.