%export +
||
|| THE IMPERATIVE LANGUAGE MIRANDA...
||




|| definitions of identifier, command, expressions etc.

ident	== [char]		|| variable names
state	== ident -> num		|| the state at a given time

command	== state -> state	|| commands do work on the state
aexp	== state -> num		|| arithmetic expression
bexp	== state -> bool	|| boolean expression

dummy	::= DUMMY		|| for making the commands more readable




|| some useful commands

skip :: command				|| the empty statement
  skip = id

becomes :: ident -> aexp -> command	|| the assignment statement
  (i $becomes e) s i' = e s,  if i'=i
                      = s i', if i'~=i

fby :: command -> command -> command	|| "followed by", ie, like semicolon
  fby = converse (.)

iff :: bexp -> dummy -> command -> dummy -> command -> dummy -> command
					|| if-then-else-endif
  iff b then c1 else c2 endif s = c1 s, if b s
                                = c2 s, otherwise

while :: bexp -> dummy -> command -> dummy -> command	|| while-do-endwhile
  while b do c endwhile = iff b then
				(c $fby
				 while b do
					c
				 endwhile
				)
			  else
				skip
			  endif

entangle :: bexp -> dummy -> command -> dummy -> command
					|| entangle-in-disentangle
  entangle b in c disentangle = iff b then
					(c $fby
					 entangle b in
						c
					 disentangle $fby
					 c
					)
				else
					c
				endif




|| some useful arithmetic expressions

constant :: num -> aexp		|| literal constant
  constant = const

var :: ident -> aexp		|| value of a variable
  var = converse id

plus, minus, times, divided_by, to_power :: aexp -> aexp -> aexp
  (e1 $plus       e2) s = e1 s + e2 s
  (e1 $minus      e2) s = e1 s - e2 s
  (e1 $times      e2) s = e1 s * e2 s
  (e1 $divided_by e2) s = e1 s / e2 s
  (e1 $to_power   e2) s = e1 s ^ e2 s




|| some useful boolean expressions

less_than, equals, greater_than, lesseq, noteq, greateq :: aexp -> aexp -> bexp
  (e1 $less_than    e2) s = e1 s <  e2 s
  (e1 $equals       e2) s = e1 s =  e2 s
  (e1 $greater_than e2) s = e1 s >  e2 s
  (e1 $lesseq       e2) s = e1 s <= e2 s
  (e1 $noteq        e2) s = e1 s ~= e2 s
  (e1 $greateq      e2) s = e1 s >= e2 s

and_b, or_b, xor, implies, equiv :: bexp -> bexp -> bexp
  (b1 $and_b   b2) s = b1 s &  b2 s
  (b1 $or_b    b2) s = b1 s \/ b2 s
  (b1 $xor     b2) s = b1 s ~= b2 s
  (b1 $implies b2) s = b1 s <= b2 s
  (b1 $equiv   b2) s = b1 s =  b2 s

not :: bexp -> bexp
  not = ((~).)




||
|| a useful user interface: with this, you just type (say) "run factorial 5".
|| NOTE: the command must use the in1/out1 convention,
||  that is, it finds its user input in "in1"
||  and delivers its output into "out1".
||
run :: command -> num -> num
  run c in1 = (("in1" $becomes constant in1) $fby c) undef "out1"





|| low-level support stuff.

then, else, endif, do, endwhile, in, disentangle :: dummy
  then        = DUMMY
  else        = DUMMY
  endif       = DUMMY
  do          = DUMMY
  endwhile    = DUMMY
  in          = DUMMY
  disentangle = DUMMY
