bmaude.maude

***(
BMaude Prototype
Uruçu-Amarela February 2018
Author: Christiano Braga
http://www.ic.uff.br/~cbraga
Universidade Federal Fluminense, Brazil

The BMaude Prototype is a tool for the verification of B specifications
implemented in the Maude language .
)

-----------------------------
--- Generalized SMC machines.

fmod GSMC-SORTS is
    sorts SemComp .
endfm

view SemComp from TRIV to GSMC-SORTS is
    sort Elt to SemComp .
endv

fmod GSMC is
    ex SET{SemComp} * (op empty to noSemComp) .
    sorts Attrib Conf .
    op <_> : Set{SemComp} -> Conf [format(c! c! c! o)] .
endfm

fmod VALUE-SORT is
    sort Value .
endfm

fmod CONTROL-SORT is
    sort Control .
endfm

view Control from TRIV to CONTROL-SORT is
    sort Elt to Control .
endv

view Value from TRIV to VALUE-SORT is
    sort Elt to Value .
endv

--- Note: AI theories are not currently supported by Maude unification,
--- as of Alpha 115.
fmod GNELIST{X :: TRIV} is
    pr NAT .
    sorts GNeList{X} .
    subsort X$Elt < GNeList{X} .

    op __ : GNeList{X} GNeList{X} -> GNeList{X} [ctor assoc prec 25] .
endfm

--------------------------------------------------------------
--- GSMC semantics for basic programming language constructs .

fmod VALUE-STACK is
    pr GNELIST{Value} * (sort GNeList{Value} to NeValueStack) .
    sort ValueStack .
    subsort NeValueStack < ValueStack .
    op evs : -> ValueStack .
    op __ : ValueStack ValueStack -> ValueStack [ditto] .
endfm

fmod CONTROL-STACK is
    pr GNELIST{Control} * (sort GNeList{Control} to NeControlStack) .
    sort ControlStack .
    subsort NeControlStack < ControlStack .
    op ecs : -> ControlStack .
    op __ : ControlStack ControlStack -> ControlStack [ditto] .
endfm

fmod STORE-SORTS is
    sorts Loc Storable .
endfm

view Loc from TRIV to STORE-SORTS is
    sort Elt to Loc .
endv

view Storable from TRIV to STORE-SORTS is
    sort Elt to Storable .
endv

fmod STORE is
    pr NAT .
    ex MAP{Loc,Storable} * (sort Entry{Loc,Storable} to Cell,
       sort Map{Loc,Storable} to Store,
       op undefined to undefloc, op empty to noStore).
    ex SET{Loc} * (op empty to noLocs) .

    op loc : Nat -> Loc [ctor] .
    op newLoc : Store -> Loc .
    op $newLoc : Store Nat -> Loc .
    eq newLoc(noStore) = loc(0) .
    ceq newLoc(S:Store) = $newLoc(S:Store, 0) if S:Store =/= noStore .
    eq $newLoc(noStore, N:Nat) = loc(N:Nat + 1) .
    ceq $newLoc((S:Store, loc(N:Nat) |-> O:Storable), N':Nat) =
	$newLoc(S:Store, N:Nat) if N:Nat >= N':Nat .
    ceq $newLoc((S:Store, loc(N:Nat) |-> O:Storable), N':Nat) =
	$newLoc(S:Store, N':Nat) if N:Nat < N':Nat .

    op $free : Loc Store -> Store .
    eq $free(L:Loc, ((L:Loc |-> O:Storable), S:Store)) = S:Store .
    eq $free(L:Loc, S:Store) = S:Store [owise] .

    op free : Set{Loc} Store -> Store .
    eq free(noLocs, S:Store) = S:Store .
    eq free((L:Loc , SL:Set{Loc}), S:Store) =
       free(SL:Set{Loc}, $free(L:Loc, S:Store)) [owise] .
endfm

fmod ENV-SORTS is
    sorts Id Bindable .
endfm

view Id from TRIV to ENV-SORTS is sort Elt to Id . endv

view Bindable from TRIV to ENV-SORTS is sort Elt to Bindable . endv

fmod ENV is
    ex MAP{Id,Bindable} * (sort Entry{Id,Bindable} to Bind,
       sort Map{Id,Bindable} to Env,
       op undefined to undefid, op empty to noEnv).
endfm

fmod EXP is
    pr RAT .
    ex GSMC .  ex ENV .
    ex STORE . ex CONTROL-STACK .
    ex VALUE-STACK .

    sorts Exp NzExp Pred EnvAttrib StoreAttrib ControlAttrib ValueAttrib .
    subsort EnvAttrib StoreAttrib ControlAttrib ValueAttrib < Attrib  .
    subsort Id < Exp < Control .

    --- Arithmetic

    op rat : Rat -> Exp [ctor format(!g o)] .
    op boo : Bool -> Exp [ctor format(!g o)] .
    op add : Exp Exp -> Exp [format(! o)] .
    op sub : Exp Exp -> Exp [format(! o)] .
    op mul : Exp Exp -> Exp [format(! o)] .
    op div : Exp Exp -> Exp [format(! o)] .

    ops ADD SUB MUL DIV : -> Control [ctor] .

    --- Boolean expressions

    op gt : Exp Exp -> Exp [format(! o)] .
    op ge : Exp Exp -> Exp [format(! o)] .
    op lt : Exp Exp -> Exp [format(! o)] .
    op le : Exp Exp -> Exp [format(! o)] .
    op eq : Exp Exp -> Exp [format(! o)] .
    op neg : Exp -> Exp [format(! o)] .
    op and : Exp Exp -> Exp [format(! o)] .
    op or : Exp Exp -> Exp [format(! o)] .

    ops LT LE EQ NEG AND OR : -> Control [ctor] .

    --- Semantic components

    op env : -> EnvAttrib .
    op sto : -> StoreAttrib .
    op cnt : -> ControlAttrib .
    op val : -> ValueAttrib .
    op _:_ : EnvAttrib Env -> SemComp [ctor format(c! b! o o)] .
    op _:_ : StoreAttrib Store -> SemComp [ctor format(r! b! o o)] .
    op _:_ : ControlAttrib ControlStack -> SemComp [ctor format(c! b! o o)] .
    op _:_ : ValueAttrib ValueStack -> SemComp [ctor format(c! b! o o)] .

    op store : Rat -> Storable [ctor format(ru! o)] .
    op store : Bool -> Storable [ctor format(ru! o)] .
    op bind : Loc -> Bindable [ctor] .
    op bind : Rat -> Bindable [ctor] .
    op bind : Bool -> Bindable [ctor] .

    op val : Storable -> Value [ctor] .
    op val : Rat -> Value [ctor] .
    op val : Bool -> Value [ctor] .
    op val : Loc -> Value [ctor] .
    op val : Id -> Value [ctor] .

    var ... : Set{SemComp} .

    eq gt(E1:Exp, E2:Exp) = neg(le(E1:Exp, E2:Exp)) .
    eq ge(E1:Exp, E2:Exp) = neg(lt(E1:Exp, E2:Exp)) .

    eq [rat-exp] :
	< cnt : (rat(R:Rat) C:ControlStack), val : SK:ValueStack, ... > =
	< cnt : C:ControlStack,
	val : (val(R:Rat) SK:ValueStack), ... > [variant] .

    eq [bool-exp] :
	< cnt : (boo(B:Bool) C:ControlStack), val : SK:ValueStack, ... > =
	< cnt : C:ControlStack,
	val : (val(B:Bool) SK:ValueStack), ... > [variant] .

    eq [add-exp] :
	< cnt : (add(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E1:Exp E2:Exp ADD C:ControlStack), ... > [variant] .

    eq [add-exp] :
	< cnt : (ADD C:ControlStack),
	val : (val(R1:Rat) val(R2:Rat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R1:Rat + R2:Rat) SK:ValueStack), ... > [variant] .

    eq [sub-exp] :
	< cnt : (sub(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E1:Exp E2:Exp SUB C:ControlStack), ... > [variant] .

    eq [sub-exp] :
	< cnt : (SUB C:ControlStack),
	val : (val(R1:Rat) val(R2:Rat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R2:Rat - R1:Rat) SK:ValueStack), ... > [variant] .

    eq [mul-exp] :
	< cnt : (mul(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E1:Exp E2:Exp MUL C:ControlStack), ... > [variant] .

    eq [mul-exp] :
	< cnt : (MUL C:ControlStack),
	val : (val(R1:Rat) val(R2:Rat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R1:Rat * R2:Rat) SK:ValueStack), ... > [variant] .

    eq [div-exp] :
	< cnt : (div(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E1:Exp E2:Exp DIV C:ControlStack), ... > [variant] .

    eq [div-exp] :
	< cnt : (DIV C:ControlStack),
	val : (val(R1:Rat) val(R2:NzRat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R1:Rat / R2:NzRat) SK:ValueStack), ... > [variant] .

    eq [lt-exp] :
	< cnt : (lt(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E2:Exp E1:Exp LT C:ControlStack), ... > [variant] .

    eq [lt-exp] :
	< cnt : (LT C:ControlStack),
	val : (val(R1:Rat) val(R2:Rat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R1:Rat < R2:Rat) SK:ValueStack), ... > [variant] .

    eq [le-exp] :
	< cnt : (le(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E2:Exp E1:Exp LE C:ControlStack), ... > [variant] .

    eq [le-exp] :
	< cnt : (LE C:ControlStack),
	val : (val(R1:Rat) val(R2:Rat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R1:Rat <= R2:Rat) SK:ValueStack), ... > [variant] .

    eq [eq-exp] :
	< cnt : (eq(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E2:Exp E1:Exp EQ C:ControlStack), ... > [variant] .

    eq [eq-exp] :
	< cnt : (EQ C:ControlStack),
	val : (val(R1:Rat) val(R2:Rat) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(R1:Rat == R2:Rat) SK:ValueStack), ... > [variant] .

    eq [eq-exp] :
	< cnt : (EQ C:ControlStack),
	val : (val(B1:Bool) val(B2:Bool) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(B1:Bool == B2:Bool) SK:ValueStack), ... > [variant] .

    eq [neg-exp] :
	< cnt : (neg(E:Exp) C:ControlStack), ... > =
	< cnt : (E:Exp NEG C:ControlStack), ... > [variant] .

    eq [neg-exp] :
	< cnt : (NEG C:ControlStack),
	val : (val(B:Bool) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(not(B:Bool)) SK:ValueStack), ... > [variant] .

    eq [and-exp] :
	< cnt : (and(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E1:Exp E2:Exp AND C:ControlStack), ... > [variant] .

    eq [and-exp] :
	< cnt : (AND C:ControlStack),
	val : (val(B1:Bool) val(B2:Bool) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(B1:Bool and B2:Bool) SK:ValueStack), ... > [variant] .

    eq [or-exp] :
	< cnt : (or(E1:Exp, E2:Exp) C:ControlStack), ... > =
	< cnt : (E1:Exp E2:Exp OR C:ControlStack), ... > [variant] .

    eq [and-exp] :
	< cnt : (OR C:ControlStack),
	val : (val(B1:Bool) val(B2:Bool) SK:ValueStack), ... > =
	< cnt : C:ControlStack,
	val : (val(B1:Bool or B2:Bool) SK:ValueStack), ... > [variant] .

    eq [variable-exp] :
	< env : (I:Id |-> bind(L:Loc), E:Env),
	sto : (L:Loc |-> store(R:Rat), S:Store),
	cnt : (I:Id C:ControlStack), val : SK:ValueStack, ... > =
 	< env : (I:Id |-> bind(L:Loc), E:Env),
	sto : (L:Loc |-> store(R:Rat), S:Store),
	cnt : C:ControlStack ,
	val : (val(R:Rat) SK:ValueStack) , ... > [variant] .

    eq [variable-exp] :
	< env : (I:Id |-> bind(L:Loc), E:Env),
	sto : (L:Loc |-> store(B:Bool), S:Store),
	cnt : (I:Id C:ControlStack), val : SK:ValueStack, ... > =
 	< env : (I:Id |-> bind(L:Loc), E:Env),
	sto : (L:Loc |-> store(B:Bool), S:Store),
	cnt : C:ControlStack ,
	val : (val(B:Bool) SK:ValueStack) , ... > [variant] .

    eq [constant-rat-exp] :
	< env : (I:Id |-> bind(R:Rat), E:Env), cnt : (I:Id C:ControlStack),
	val : SK:ValueStack , ... > =
 	< env : (I:Id |-> bind(R:Rat), E:Env), cnt : C:ControlStack,
	val : (val(R:Rat) SK:ValueStack), ... > [variant] .

    eq [constant-bool-exp] :
 	< env : (I:Id |-> bind(B:Bool), E:Env), cnt : (I:Id C:ControlStack),
	val : SK:ValueStack, ... > =
	< env : (I:Id |-> bind(B:Bool), E:Env), cnt : C:ControlStack,
   	val : (val(B:Bool) SK:ValueStack), ... > [variant] .
endfm

mod CMD is
    ex EXP .

    sorts Cmd ExcAttrib Exc .
    subsort Cmd < Control .

    op nop : -> Cmd [ctor format(! o)] .
    op choice : Cmd Cmd -> Cmd [ctor assoc comm format(! o)] .
    op assign : Id Exp -> Cmd [ctor format(! o)] .
    op ASSIGN : -> Control [ctor] .
    op loop : Exp Cmd -> Cmd [ctor format(! o)] .
    op LOOP : -> Control [ctor] .
    op if : Exp Cmd Cmd -> Cmd [ctor format(! o)] .
    op IF : -> Control [ctor] .
    op val : Cmd -> Value [ctor] .

    var ... : Set{SemComp} . var E : Env . var S : Store .
    var C : ControlStack . var V : ValueStack .

    eq [nop-cmd] :
	< cnt : nop C, ... > = < cnt : C, ... > [variant] .

    rl [choice-cmd] :
	< cnt : choice(M1:Cmd, M2:Cmd) C, ... > =>
	< cnt : M1:Cmd C, ... > [narrowing] .

    eq [assign-cmd] :
	< env : (I:Id |-> bind(L:Loc), E),
	cnt : (assign(I:Id, E:Exp) C),
	val : V, ... > =
	< env : (I:Id |-> bind(L:Loc), E),
	cnt : (E:Exp ASSIGN C),
   	val : (val(I:Id) V), ... > [variant] .

    eq [assign-cmd] :
	< env : (I:Id |-> bind(L:Loc), E),
	sto : (L:Loc |-> T:Storable, S),
	cnt : (ASSIGN C),
	val : (val(R:Rat) val(I:Id) V), ... > =
	< env : (I:Id |-> bind(L:Loc), E),
	sto : (L:Loc |-> store(R:Rat), S),
	cnt : C,
	val : V, ... > [variant] .

    eq [assign-cmd] :
	< env : (I:Id |-> bind(L:Loc), E),
	sto : (L:Loc |-> T:Storable, S),
	cnt : (ASSIGN C),
   	val : (val(B:Bool) val(I:Id) V), ... > =
	< env : (I:Id |-> bind(L:Loc), E),
	sto : (L:Loc |-> store(B:Bool), S),
	cnt : C,
   	val : V, ... > [variant] .

    eq [loop] :
	< cnt : loop(E:Exp, K:Cmd) C, val : V, ... > =
	< cnt : E:Exp LOOP C,
	val : val(loop(E:Exp, K:Cmd)) V, ... > [variant] .

    rl [loop] :
	< cnt : LOOP C,
	val : val(true) val(loop(E:Exp, K:Cmd)) V, ... > =>
	< cnt : K:Cmd loop(E:Exp, K:Cmd) C,
	val : V, ... > [narrowing] .

    eq [loop] :
	< cnt : LOOP C,
	val : val(false) val(loop(E:Exp, K:Cmd)) V, ... > =
	< cnt : C, val : V, ... > [variant] .

    eq [if] :
       < cnt : if(E:Exp, K1:Cmd, K2:Cmd) C, val : V, ... > =
       < cnt : E:Exp IF C,
         val : val(if(E:Exp, K1:Cmd, K2:Cmd)) V, ... > [variant] .

    eq [if] :
       < cnt : IF C,
         val : val(true) val(if(E:Exp, K1:Cmd, K2:Cmd)) V, ... > =
       < cnt : K1:Cmd C,
         val : V, ... > [variant] .

    eq [if] :
       < cnt : IF C,
         val : val(false) val(if(E:Exp, K1:Cmd, K2:Cmd)) V, ... > =
       < cnt : K2:Cmd C,
         val : V, ... > [variant] .
endm

mod DEC is
    ex CMD .

    sorts Abs Blk Dec Formal Formals Actual Actuals LocsAttrib .
    subsort Actuals Dec < Control .
    subsort Formal < Formals .
    subsort Exp < Actual < Actuals .
    subsort Blk < Cmd .
    subsort Abs < Bindable .

    op cns : Id Exp -> Dec [ctor format(! o)] .
    op ref : Id Exp -> Dec [ctor format(! o)] .
    op prc : Id Blk -> Dec [ctor format(! o)] .
    op prc : Id Formals Blk -> Dec [ctor format(! o)] .
    op par : Id -> Formal [ctor format(! o)] .
    op vod : -> Formal [ctor format(! o)] .
    op for : Formals Formals -> Formals [ctor assoc format(! o)] .
    op dec : Dec Dec -> Dec [ctor format(! o)] .
    op blk : Cmd -> Blk [ctor format(! o)] .
    op blk : Dec Cmd -> Blk [ctor format(! o)] .
    op cal : Id -> Cmd [ctor format(! o)] .
    op cal : Id Actuals -> Cmd [ctor format(! o)] .
    op act : Actuals Actuals -> Actuals [ctor assoc format(! o)] .
    ops CNS REF CAL BLK FRE : -> Control [ctor] .

    op val : Env -> Value [ctor] .
    op val : Loc -> Value [ctor] .
    op val : Abs -> Value [ctor] .

    op abs : Blk -> Abs [ctor] .
    op abs : Formals Blk -> Abs [ctor] .
    op locs : -> LocsAttrib [ctor] .
    op _:_ : LocsAttrib Set{Loc} -> SemComp [ctor format(c! b! o o)] .

    var ... : Set{SemComp} . vars E E' : Env . var S : Store .
    var C : ControlStack . var V : ValueStack .

    eq [blk] :
	< cnt : blk(D:Dec, M:Cmd) C, env : E , val : V , ... > =
	< cnt : D:Dec M:Cmd BLK C, env : E , val : val(E) V , ... > [variant] .

    eq [blk] :
	< cnt : blk(M:Cmd) C, env : E , val : V , ... > =
	< cnt : M:Cmd BLK C, env : E , val : val(E) V , ... > [variant] .

    eq [blk] :
	< cnt : BLK C ,
	env : E' ,
	val : val(E) V ,
	locs : SL:Set{Loc},
	sto : S:Store, ... > =
	< cnt : C ,
	env : E ,
	val : V ,
	locs : noLocs,
	sto : free(SL:Set{Loc}, S:Store), ... > [variant] .

    eq [ref] :
	< cnt : ref(I:Id, X:Exp) C , val : V , ... > =
	< cnt : X:Exp REF C , val : val(I:Id) V , ... > [variant] .

    eq [ref] :
	< cnt : REF C, env : E ,
	sto : S ,
	val : val(R:Rat) val(I:Id) V ,
	locs : SL:Set{Loc} , ... > =
	< cnt : C ,
	env : insert(I:Id, bind(newLoc(S)), E) ,
	sto : insert(newLoc(S), store(R:Rat), S) ,
	val : V ,
	locs : (newLoc(S) , SL:Set{Loc}) , ... > [variant] .

    eq [cns] :
	< cnt : cns(I:Id, X:Exp) C , val : V , ... > =
	< cnt : X:Exp CNS C , val : val(I:Id) V , ... > [variant] .

    eq [cns] :
	< cnt : CNS C, env : E , val : val(R:Rat) val(I:Id) V , ... > =
	< cnt : C ,
	env : (I:Id |-> bind(R:Rat) , E) ,
	val : V , ... > [variant] .

    eq [prc] :
	< cnt : prc(I:Id, F:Formals, B:Blk) C, env : E, ... > =
	< cnt : C,
	env : insert(I:Id, abs(F:Formals, B:Blk), E), ... > [variant] .

    eq [prc] :
	< cnt : prc(I:Id, B:Blk) C, env : E, ... > =
	< cnt : C,
	env : insert(I:Id, abs(B:Blk), E), ... > [variant] .

    eq [dec] :
	< cnt : dec(D1:Dec, D2:Dec) C, ... > =
	< cnt : D1:Dec D2:Dec C , ... > [variant] .

    eq [cal] :
	< cnt : cal(I:Id) C, ... > =
	< cnt : I:Id CAL C, ... > [variant] .

    eq [cal] :
	< cnt : cal(I:Id, A:Actuals) C, ... > =
	< cnt : I:Id A:Actuals CAL C, ... > [variant] .

    eq [cal] :
	< cnt : CAL C,
	val : V1:ValueStack
	val(abs(F:Formals, B:Blk)) V2:ValueStack, ... > =
	< cnt : addDec(match(F:Formals,
	    V1:ValueStack), B:Blk) C,
	val : V2:ValueStack, ... > [variant] .

    eq [cal] :
	< cnt : CAL C,
	val : val(abs(B:Blk)) V:ValueStack, ... > =
	< cnt : B:Blk C,
	val : V:ValueStack, ... > [variant] .

    eq [prc-id] :
	< cnt : (I:Id C),
	env : (I:Id |-> A:Abs, E),
	val : V , ... > =
 	< cnt : C,
	env : (I:Id |-> A:Abs, E),
	val : (val(A:Abs) V), ... > [variant] .

    eq [act] :
	< cnt : act(E:Exp, A:Actuals) C, ... > =
	< cnt : A:Actuals E:Exp C, ... > [variant] .

    op match : Formals ValueStack -> Dec .
    eq match(par(I:Id), val(R:Rat)) = ref(I:Id, rat(R:Rat)) .
    eq match(par(I:Id), val(B:Bool)) = ref(I:Id, boo(B:Bool)) .
    eq match(for(F:Formal, L:Formals), (V:Value VS:ValueStack)) =
	dec(match(F:Formal, V:Value),
	  match(L:Formals, VS:ValueStack)) .

    op addDec : Dec Blk -> Blk .
    eq addDec(D:Dec, B:Blk) = blk(D:Dec, B:Blk) .
endm

mod OUT is
    ex DEC .

    sort OutAttrib .

    op out : -> OutAttrib [ctor] .
    op _:_ : OutAttrib ValueStack -> SemComp [ctor format(c! b! o o)] .
    op print : Exp -> Cmd [ctor format(! o)] .
    op PRINT : -> Control [ctor] .

    var ... : Set{SemComp} .

    op out : Conf -> NeValueStack [ctor] .
    eq out(< out : V:NeValueStack , ... >) = V:NeValueStack .

    eq [print] :
	< cnt : (print(E:Exp) C:ControlStack), ... > =
	< cnt : (E:Exp PRINT C:ControlStack), ... > [variant] .

    eq [print] :
	< cnt : (PRINT C:ControlStack),
	val : val(R:Rat) V:ValueStack,
	out : O:ValueStack, ... > =
	< cnt : C:ControlStack,
	val : V:ValueStack,
	out : val(R:Rat) O:ValueStack , ... > [variant] .
endm

mod EXIT is
    ex OUT .

    --- Sequences had to be moved "down" to this module because
    --- the evaluation of the next command only takes place if no
    --- exit was executed.
    op seq : Cmd Cmd -> Cmd [format(! o)] .

    op exit : Exp -> Cmd [format(! o)] .
    op EXT : -> Exc .
    op EXIT : -> Control .
    op CNT : -> Exc .
    op exc : -> ExcAttrib .
    op _:_ : ExcAttrib Exc -> SemComp [format(c! b! o o)] .

    var ... : Set{SemComp} . var E : Env . var S : Store .
    var C : ControlStack . var V : ValueStack .

    eq [exit-cmd] :
	< cnt : exit(X:Exp) C, ... > = < cnt : X:Exp EXIT C, ... > [variant] .

    --- Maybe define a flush operation that sets the semantic components
    --- to their identity values.
    eq [exit-cmd] :
	< cnt : EXIT C,
	env : E,
	sto : S,
	val : A:Value V,
	out : O:ValueStack,
	locs : SL:Set{Loc},
	exc : CNT, ... > =
	< cnt : ecs,
	env : noEnv,
	sto : noStore,
	val : evs,
	out : A:Value,
	locs : noLocs,
	exc : EXT, ... > [variant] .

    --- Sequences had to be moved "down" to this module because
    --- the evaluation of the next command only takes place if no
    --- exit was executed.
    eq [seq-cmd] :
	< cnt : seq(C1:Cmd, C2:Cmd) C, exc : CNT, ... > =
	< cnt : C1:Cmd C2:Cmd C, exc : CNT, ... > [variant] .

    eq [seq-cmd] :
	< cnt : seq(C1:Cmd, C2:Cmd) C, exc : EXT, ... > =
	< cnt : ecs, exc : EXT, ... > [variant] .
endm

--- Basic programming languages constructs.
mod BPLC is
    ex EXIT .

    var ... : Set{SemComp} .

    op getValue : Id Conf -> Storable .
    eq getValue(I:Id,
          < env : (I:Id |-> bind(L:Loc), E:Env) ,
          sto : (L:Loc |-> S:Storable, S:Store) ,
   	  ... >) = S:Storable .
endm

load model-checker

mod BPLC-MODEL-CHECKER is
	ex BPLC .
    pr MODEL-CHECKER .

    subsort Conf < State .

    var ... : Set{SemComp} .

    op valueOf : Id Rat Conf -> Bool .
    op valueOf : Id Bool Conf -> Bool .
    eq valueOf(I:Id, R:Rat,
	  < env : (I:Id |-> bind(L:Loc), E:Env) ,
	  sto : (L:Loc |-> store(R:Rat), S:Store) ,
	  ... >) = true .
    eq valueOf(I:Id, B:Bool,
	  < env : (I:Id |-> bind(L:Loc), E:Env) ,
	  sto : (L:Loc |-> store(B:Bool), S:Store) ,
	  ... >) = true .
endm

-----------------------------------------------------------------------
--- Abstract Machine Notation (AMN) and Generalized substitutions (GSL)

fmod GSL-SYNTAX is
    pr RAT .
    pr QID .

    sorts GSLIdentifiers GSLExpression GSLPredicate GSLSubstitution .
    subsort GSLIdentifiers < GSLPredicate < GSLExpression  .

    --- GSL expressions
    op bid : Qid -> GSLIdentifiers [ctor format(c! o)] .
    op grat : Rat -> GSLExpression [ctor format(!g o)] .
    op gboo : Bool -> GSLPredicate [ctor format(!g o)] .
    op _@+_ : GSLExpression GSLExpression -> GSLExpression
        [assoc comm ctor format(o b! o o)] .
    op _-_ : GSLExpression GSLExpression -> GSLExpression
        [assoc ctor format(o b! o o)] .
    op _*_ : GSLExpression GSLExpression -> GSLExpression
        [assoc comm ctor format(o b! o o)] .
    op _/_ : GSLExpression GSLExpression -> GSLExpression
        [ctor format(o b! o o)] .
    --- GSL predicates
    op _==_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc comm ctor format(o b! o o)] .
    op _<_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc ctor format(o b! o o)] .
    op _<=_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc ctor format(o b! o o)] .
    op _>_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc ctor format(o b! o o)] .
    op _>=_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc ctor format(o b! o o)] .
    op ~_ : GSLExpression -> GSLPredicate
        [ctor format(b! o o)] .
    op _/\_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc comm ctor format(o b! o o)] .
    op _\/_ : GSLExpression GSLExpression -> GSLPredicate
        [assoc comm ctor format(o b! o o)] .
    op _@:=_ : GSLIdentifiers GSLExpression -> GSLSubstitution
        [ctor format(o b! o o)] .
    op IF_THEN_END : GSLPredicate GSLSubstitution -> GSLSubstitution
          [ctor prec 13 format(nib! o b! o b! o)] .
    op IF_THEN_ELSE_END : GSLPredicate GSLSubstitution GSLSubstitution ->
          GSLSubstitution [ctor format(nib! o b! o b! o b! o)] .

    eq (IF P:GSLPredicate THEN S:GSLSubstitution END) =
	  (IF P:GSLPredicate THEN S:GSLSubstitution ELSE skip END) .

    op WHILE_DO_ : GSLPredicate GSLSubstitution -> GSLSubstitution
        [ctor prec 15 format(nib! o b! o++ --o)] .
    op _;_ : GSLSubstitution GSLSubstitution -> GSLSubstitution
        [ctor assoc format(o b! o o)] .
    op _OR_ : GSLSubstitution GSLSubstitution -> GSLSubstitution
        [ctor assoc comm prec 14 format(o nib! o o)] .

    eq S1:GSLSubstitution OR S2:GSLSubstitution =
	S1:GSLSubstitution [] S2:GSLSubstitution .

    op skip : -> GSLSubstitution [ctor format(b! o)] .

    --- Pre-condition GSLSubstitution
    op _|_ : GSLPredicate GSLSubstitution -> GSLSubstitution
        [ctor prec 10 format(o b! o o)] .

    --- Bounded choice GSLSubstitution
    op _[]_ : GSLSubstitution GSLSubstitution -> GSLSubstitution
        [ctor assoc comm prec 10 format(o b! b! o o)] .
    --- Guarded GSLSubstitution
    op _==>_ : GSLPredicate GSLSubstitution -> GSLSubstitution
        [ctor prec 10 format(o b! o o)] .

    --- Unbounded choice GSLSubstitution
    op @_._ : GSLIdentifiers GSLSubstitution -> GSLSubstitution
        [ctor prec 10 format(b! o b! o o)] .
    --- Print
    op @print : GSLExpression -> GSLSubstitution .

    --- BEGIN
    op BEGIN_END : GSLSubstitution -> GSLSubstitution [format(b! o b! o)] .
    eq BEGIN S:GSLSubstitution END = S:GSLSubstitution .
endfm

mod GSL-TO-BPLC is
    inc GSL-SYNTAX .
    pr BPLC .

    op gid : GSLIdentifiers -> Id [ctor] .

    op compile : GSLSubstitution -> Cmd .
    op compile : GSLIdentifiers -> Id .
    op compile : GSLExpression -> Exp .

    --- GSLExpressions
    eq compile(V:GSLIdentifiers) = gid(V:GSLIdentifiers) .

    eq compile(grat(R:Rat)) = rat(R:Rat) .

    eq compile(gboo(B:Bool)) = boo(B:Bool) .

    eq compile(E1:GSLExpression @+ E2:GSLExpression) =
	add(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression - E2:GSLExpression) =
	sub(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression * E2:GSLExpression) =
	mul(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression / E2:GSLExpression) =
	div(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    --- GSLPredicates
    eq compile(E1:GSLExpression == E2:GSLExpression) =
	eq(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression >= E2:GSLExpression) =
	ge(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression > E2:GSLExpression) =
	gt(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression <= E2:GSLExpression) =
	le(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression < E2:GSLExpression) =
	lt(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(~ E:GSLExpression) =
	neg(compile(E:GSLExpression)) .

    eq compile(E1:GSLExpression /\ E2:GSLExpression) =
	and(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    eq compile(E1:GSLExpression \/ E2:GSLExpression) =
	or(compile(E1:GSLExpression), compile(E2:GSLExpression)) .

    --- skip
    eq compile(skip) = nop .

    --- Simple assignment
    eq compile(V:GSLIdentifiers @:= E:GSLExpression) =
	assign(compile(V:GSLIdentifiers), compile(E:GSLExpression)) .

    --- Pre-condition
    eq compile(P:GSLPredicate | S:GSLSubstitution) =
	if(compile(P:GSLPredicate), compile(S:GSLSubstitution), exit(rat(0))) .

      --- Bounded choice
    eq compile(S1:GSLSubstitution [] S2:GSLSubstitution) =
	choice(compile(S1:GSLSubstitution), compile(S2:GSLSubstitution)) .

    --- Guarded GSLSubstitution
    eq compile(P:GSLPredicate ==> S:GSLSubstitution) =
	if(compile(P:GSLPredicate), compile(S:GSLSubstitution), nop) .

    --- TODO:
    --- Unbounded choice

    --- Sequences
    eq compile(S1:GSLSubstitution ; S2:GSLSubstitution) =
	seq(compile(S1:GSLSubstitution), compile(S2:GSLSubstitution)) .

    --- Conditional

    eq compile(IF P:GSLPredicate THEN S1:GSLSubstitution ELSE
	  S2:GSLSubstitution END) = if(compile(P:GSLPredicate),
	  compile(S1:GSLSubstitution), compile(S2:GSLSubstitution)) .

	--- While
    eq compile(WHILE P:GSLPredicate DO S:GSLSubstitution) =
	loop(compile(P:GSLPredicate), compile(S:GSLSubstitution)) .

    --- Print
    eq compile(@print (E:GSLExpression)) = print(compile(E:GSLExpression)) .
endm

fmod AMN-SYNTAX is
     ex GSL-SYNTAX .
     sorts AMNMachine AMNClauses AMNAbsVariables AMNAbsConstants
        AMNOperations AMNValuesClause AMNValuation AMNValSet AMNIdList
        AMNOperation AMNOpSet GSLActuals .

    subsort AMNAbsVariables AMNAbsConstants AMNOperations
	    AMNValuesClause < AMNClauses .

    subsort GSLIdentifiers < AMNIdList .
    subsort AMNValuation < AMNValSet .
    subsort AMNOperation < AMNOpSet .
    subsort GSLExpression < GSLActuals .

    op _,_ : GSLActuals GSLActuals -> GSLActuals [assoc] .

    op MACHINE_END : GSLIdentifiers -> AMNMachine .
    op MACHINE__END : GSLIdentifiers AMNClauses -> AMNMachine
        [prec 40 format(b!++ o o --nib! o)] .

    op __ : AMNClauses AMNClauses -> AMNClauses [ctor assoc comm prec 30] .
    op VARIABLES_ : AMNIdList -> AMNAbsVariables [ctor prec 25 format(nib! o o)] .
    op CONSTANTS_ : AMNIdList -> AMNAbsConstants [ctor prec 25 format(nib! o o)] .
    op _@,_ : AMNIdList AMNIdList -> AMNIdList [ctor assoc prec 10 format(o b! o o o)] .

    op VALUES_ : AMNValSet -> AMNValuesClause [ctor prec 25 format(nib! o++ o--)] .

    op _@=_ : GSLIdentifiers GSLExpression -> AMNValuation [ctor prec
	  10 format(nio b! o o)] .

    op _;_ : AMNValSet AMNValSet ->
    AMNValSet [ctor assoc comm prec 15 format(o b! o o)] .

    op OPERATIONS_ : AMNOpSet -> AMNOperations [ctor prec 25 format(nib! o++ o--)] .
    op _=_ : GSLIdentifiers GSLSubstitution -> AMNOperation
        [ctor prec 15 format(nio b! o++ o--)] .
    op _;_ : AMNOpSet AMNOpSet -> AMNOpSet [ctor assoc comm prec 20 format(o b! o o)] .
    op _(_)=_ : GSLIdentifiers AMNIdList GSLSubstitution -> AMNOperation
        [prec 20 format(o b! o b! b! o o)] .

--- TODO:
***(op _<-_(_)=_ : GSLIdentifiers GSLIdentifiers GSLSubstitution -> AMNOperation
    [prec 20 format(o b! o b! o o)] .
)
    op _(_) : GSLIdentifiers GSLActuals -> GSLSubstitution
        [prec 20 ctor format(b! o b! o o)] .
    op _() : GSLIdentifiers -> GSLSubstitution
        [prec 20 ctor format(b! b! o o)] .
endfm

mod AMN-TO-BPLC is
    ex AMN-SYNTAX .
    ex GSL-TO-BPLC .

    op compile : AMNMachine -> Dec .
    op compile : AMNClauses -> Dec .
    op compile : AMNAbsVariables AMNValuesClause -> Dec .
    op compileToRef : AMNIdList AMNValSet -> Dec .
    op compile : AMNAbsConstants AMNValuesClause -> Dec .
    op compileToCns : AMNIdList AMNValSet -> Dec .
    op compile : AMNOperations -> Dec .
    op compile : AMNOpSet -> Dec .
    op compile : GSLIdentifiers -> Id .
    op compileToFormals : AMNIdList -> Formals .

    --- AMNOperation call
    eq compile(I:GSLIdentifiers (E:GSLExpression)) =
	cal(compile(I:GSLIdentifiers), compile(E:GSLExpression)) .

    eq compile(I:GSLIdentifiers ()) =
	cal(compile(I:GSLIdentifiers)) .

    eq compile(I:GSLIdentifiers (A:GSLActuals)) =
	cal(compile(I:GSLIdentifiers), compile(A:GSLActuals)) .

    op compile : GSLActuals -> Actuals .

    eq compile(A1:GSLActuals, A2:GSLActuals) =
	act(compile(A1:GSLActuals), compile(A2:GSLActuals)) .

    --- GSLIdentifiers
    eq compile(P:GSLIdentifiers) = gid(P:GSLIdentifiers) .

    --- AMNOperations
    --- TODO: AMNOperation with return value.
    eq compile(P:GSLIdentifiers = S:GSLSubstitution) =
	prc(compile(P:GSLIdentifiers), blk(compile(S:GSLSubstitution))) .

    eq compile(P:GSLIdentifiers (FS:AMNIdList) = S:GSLSubstitution) =
	prc(compile(P:GSLIdentifiers),
          compileToFormals(FS:AMNIdList), blk(compile(S:GSLSubstitution))) .
    eq compileToFormals(F:GSLIdentifiers) = par(compile(F:GSLIdentifiers)) .
    eq compileToFormals(F:GSLIdentifiers @, FS:AMNIdList) =
	for(compileToFormals(F:GSLIdentifiers), compileToFormals(FS:AMNIdList)) .

    eq compile(O:AMNOperation ; OS:AMNOpSet) =
	dec(compile(O:AMNOperation), compile(OS:AMNOpSet)) .
    eq compile(OPERATIONS O:AMNOperation) = compile(O:AMNOperation) .
    eq compile(OPERATIONS OS:AMNOpSet) = compile(OS:AMNOpSet) .

    --- Variables
    eq compile(VARIABLES IS:AMNIdList, VALUES VS:AMNValSet) =
	compileToRef(IS:AMNIdList, VS:AMNValSet) .

    eq compileToRef(I:GSLIdentifiers , (I:GSLIdentifiers @= E:GSLExpression)) =
	ref(compile(I:GSLIdentifiers), compile(E:GSLExpression)) .

    eq compileToRef((I:GSLIdentifiers) ,
          ((I:GSLIdentifiers @= E:GSLExpression) ; VS:AMNValSet)) =
	ref(compile(I:GSLIdentifiers), compile(E:GSLExpression)) .

    eq compileToRef((I:GSLIdentifiers @, IS:AMNIdList) ,
          ((I:GSLIdentifiers @= E:GSLExpression) ; VS:AMNValSet)) =
	dec(ref(compile(I:GSLIdentifiers), compile(E:GSLExpression)),
          compileToRef(IS:AMNIdList, VS:AMNValSet)) .

    --- Constants
    eq compile(CONSTANTS IS:AMNIdList, VALUES VS:AMNValSet) =
	compileToCns(IS:AMNIdList, VS:AMNValSet) .

    eq compileToCns(I:GSLIdentifiers , (I:GSLIdentifiers @= E:GSLExpression)) =
	cns(compile(I:GSLIdentifiers), compile(E:GSLExpression)) .

    eq compileToCns((I:GSLIdentifiers) ,
          ((I:GSLIdentifiers @= E:GSLExpression) ; VS:AMNValSet)) =
	cns(compile(I:GSLIdentifiers), compile(E:GSLExpression)) .

    eq compileToCns((I:GSLIdentifiers @, IS:AMNIdList) ,
          ((I:GSLIdentifiers @= E:GSLExpression) ; VS:AMNValSet)) =
	dec(cns(compile(I:GSLIdentifiers), compile(E:GSLExpression)),
          compileToCns(IS:AMNIdList, VS:AMNValSet)) .

    --- AMNMachine

    eq compile( MACHINE I:GSLIdentifiers A:AMNAbsVariables
          C:AMNAbsConstants VS:AMNValuesClause OP:AMNOperations END) =
          dec(compile(A:AMNAbsVariables, VS:AMNValuesClause),
           dec(compile(C:AMNAbsConstants, VS:AMNValuesClause),
             compile(OP:AMNOperations))) .

    eq compile( MACHINE I:GSLIdentifiers A:AMNAbsVariables
          VS:AMNValuesClause OP:AMNOperations END) =
          dec(compile(A:AMNAbsVariables, VS:AMNValuesClause),
           compile(OP:AMNOperations)) .

    eq compile( MACHINE I:GSLIdentifiers C:AMNAbsConstants
          VS:AMNValuesClause OP:AMNOperations END) =
          dec(compile(C:AMNAbsConstants, VS:AMNValuesClause),
           compile(OP:AMNOperations)) .

    eq compile( MACHINE I:GSLIdentifiers OP:AMNOperations END) =
          compile(OP:AMNOperations) .
endm

mod RUN-AMN is
    inc AMN-TO-BPLC .
    inc BPLC .
    inc QID .

    op getValue : GSLIdentifiers Conf -> Storable .
    eq getValue(I:GSLIdentifiers, C:Conf) =
	getValue(compile(I:GSLIdentifiers), C:Conf) .

    op run : GSLSubstitution AMNMachine -> Conf .
    rl run(S:GSLSubstitution, M:AMNMachine) =>
	< cnt : blk(compile(M:AMNMachine), compile(S:GSLSubstitution)) ecs,
	env : noEnv, sto : noStore , val : evs ,
	locs : noLocs , out : evs , exc : CNT > .

    op runO : GSLSubstitution AMNMachine -> NeValueStack .
    crl runO(S:GSLSubstitution, M:AMNMachine) => out(C:Conf)
      if  C:Conf := run(S:GSLSubstitution, M:AMNMachine) .
endm

mod AMN-MODEL-CHECKER is
    ex RUN-AMN .
    ex BPLC-MODEL-CHECKER .

    op valueOf : GSLIdentifiers Rat State -> Bool .
    op valueOf : GSLIdentifiers Bool State -> Bool .
    eq valueOf(I:GSLIdentifiers, R:Rat, S:State) =
	valueOf(compile(I:GSLIdentifiers), R:Rat, S:State) .
    eq valueOf(I:GSLIdentifiers, B:Bool, S:State) =
	valueOf(compile(I:GSLIdentifiers), B:Bool, S:State) .
    op _,_|=?_ : AMNMachine GSLSubstitution Formula -> ModelCheckResult .
    eq M:AMNMachine, S:GSLSubstitution |=? F:Formula =
	modelCheck(run(S:GSLSubstitution, M:AMNMachine), F:Formula) .
endm

--------------------
--- BMaude Prototype

fmod TOKEN is
     pr QID-LIST .

     sorts Token Bubble NeTokenList .
     op token : Qid -> Token
        [special
          (id-hook Bubble        (1 1)
        op-hook qidSymbol     (<Qids> : ~> Qid)
	id-hook Exclude       ( print ))] .

    op bubble : QidList -> Bubble
        [special
          (id-hook Bubble        (1 -1)
        op-hook qidListSymbol (__ : QidList QidList ~> QidList)
        op-hook qidSymbol     (<Qids> : ~> Qid)
	id-hook Exclude       ( OR IF THEN ELSE END BEGIN WHILE ; := = skip )
	  ) ] .

    op neTokenList : QidList -> NeTokenList
        [special
          (id-hook Bubble        (1 -1)
        op-hook qidListSymbol (__ : QidList QidList ~> QidList)
        op-hook qidSymbol     (<Qids> : ~> Qid)
        id-hook Exclude       ( . ))] .
endfm

fmod AMN-GRAMMAR is
    pr TOKEN .
    pr RAT .

    sorts VariablesDecl ConstantsDecl OperationsDecl OperationDeclList
        OperationDecl FormalsDecl SubstitutionDecl ExpressionDecl
        ValueDecl ValueDeclList ValuesDecl PredicateDecl ClausesDecl
        MachineDecl Expression .

    subsort ValueDecl < ValueDeclList .
    subsort VariablesDecl ConstantsDecl OperationsDecl ValuesDecl < ClausesDecl .
    subsort OperationDecl < OperationDeclList .
    subsort PredicateDecl < ExpressionDecl .
    sort TokenList .
    subsort Token < TokenList .

    op _,_ : TokenList TokenList -> TokenList [assoc prec 5] .
    op MACHINE__END : Token ClausesDecl -> MachineDecl [prec 80] .
    op __ : ClausesDecl ClausesDecl -> ClausesDecl [assoc comm prec 70] .
    op VARIABLES_ : TokenList -> VariablesDecl [prec 60] .
    op CONSTANTS_ : TokenList -> ConstantsDecl [prec 60] .
    op VALUES_ : ValueDecl -> ValuesDecl [prec 60] .
    op VALUES_ : ValueDeclList -> ValuesDecl  [prec 60] .
    op _=_ : Token Token -> ValueDecl  [prec 40] .
    op _=_ : Token ExpressionDecl -> ValueDecl  [prec 40] .
    op _;_ : ValueDeclList ValueDeclList -> ValueDeclList  [assoc prec 50] .
    op OPERATIONS_ : OperationDeclList -> OperationsDecl  [prec 60] .
    op _=_ : Token SubstitutionDecl -> OperationDecl [prec 50] .
    op _`(_`)=_ : Token TokenList SubstitutionDecl -> OperationDecl  [prec 50] .
    op _;_ : OperationDeclList OperationDeclList -> OperationDeclList  [assoc prec 60] .

    --- GSL Substitutions
    op _:=_ : Token Token -> SubstitutionDecl [prec 40] .
    op _:=_ : Token ExpressionDecl -> SubstitutionDecl [prec 40] .

    op _() : Token -> SubstitutionDecl .
    op _(_) : Token Bubble -> SubstitutionDecl .
    op print : Token -> SubstitutionDecl .
    op print : ExpressionDecl -> SubstitutionDecl .
    op skip : -> SubstitutionDecl .

    --- GSL expressions
    --- op -_ : ExpressionDecl -> ExpressionDecl [ditto] .
    op _+_ : Token Token -> ExpressionDecl [gather(e E) prec 15] .
    op _+_ : Token ExpressionDecl -> ExpressionDecl [gather(e E) prec 15] .
    op _+_ : ExpressionDecl Token -> ExpressionDecl [gather(e E) prec 15] .
    op _+_ : ExpressionDecl ExpressionDecl -> ExpressionDecl [gather(e E) prec 15] .

    op _-_ : Token Token -> ExpressionDecl  [gather(e E) prec 15] .
    op _-_ : Token ExpressionDecl -> ExpressionDecl [gather(e E) prec 15] .
    op _-_ : ExpressionDecl Token -> ExpressionDecl [gather(e E) prec 15] .
    op _-_ : ExpressionDecl ExpressionDecl -> ExpressionDecl [gather(e E) prec 15] .

    op _*_ : Token Token -> ExpressionDecl [gather(e E) prec 10] .
    op _*_ : Token ExpressionDecl -> ExpressionDecl [gather(e E) prec 10] .
    op _*_ : ExpressionDecl Token -> ExpressionDecl [gather(e E) prec 10] .
    op _*_ : ExpressionDecl ExpressionDecl -> ExpressionDecl [gather(e E) prec 10] .

    op _/_ : Token Token -> ExpressionDecl [prec 20] .
    op _/_ : Token ExpressionDecl -> ExpressionDecl [prec 20] .
    op _/_ : ExpressionDecl Token -> ExpressionDecl [prec 20] .
    op _/_ : ExpressionDecl ExpressionDecl -> ExpressionDecl [prec 20] .

    --- GSL predicates
    ops true false : -> PredicateDecl .
    op _==_ : Token Token -> PredicateDecl [prec 30] .
    op _==_ : Token ExpressionDecl -> PredicateDecl [prec 30] .
    op _==_ : ExpressionDecl Token -> PredicateDecl [prec 30] .
    op _==_ : ExpressionDecl ExpressionDecl -> PredicateDecl [prec 30] .
    op _/\_ : PredicateDecl PredicateDecl -> PredicateDecl [assoc comm prec 35] .
    op ~ : PredicateDecl -> PredicateDecl .

    --- Conditional
    op _|_ : PredicateDecl SubstitutionDecl -> SubstitutionDecl [prec 40] .
    op IF_THEN_END : PredicateDecl SubstitutionDecl -> SubstitutionDecl [prec 40] .

    op IF_THEN_ELSE_END : PredicateDecl SubstitutionDecl
	  SubstitutionDecl -> SubstitutionDecl [prec 40] .

    --- Sequences
    op _;_ : SubstitutionDecl SubstitutionDecl -> SubstitutionDecl [assoc prec 50] .
    op _OR_ : SubstitutionDecl SubstitutionDecl -> SubstitutionDecl [assoc prec 50] .

    --- While loop
    op WHILE_DO_ : PredicateDecl SubstitutionDecl -> SubstitutionDecl [prec 40] .
    op BEGIN_END : SubstitutionDecl -> SubstitutionDecl [prec 35] .
endfm

fmod PROCESS-AMN-DECL is
    inc TOKEN .
    inc AMN-SYNTAX .
    pr META-LEVEL .
    pr CONVERSION .

    op processPreMachine : Term ~> AMNMachine .
    eq processPreMachine('MACHINE__END['token[I:Qid], T:Term]) =
        MACHINE processPreIdentifiers(I:Qid) processPreClauses(T:Term) END .

    op processPreClauses : Term ~> AMNClauses .
    op processPreClauses : TermList ~> AMNClauses .
    eq processPreClauses('VARIABLES_['token[I:Qid]]) =
        VARIABLES processPreIdentifiers(I:Qid) .

    eq processPreClauses('VARIABLES_['_`,_[IS:TermList]]) =
        VARIABLES processPreVariableList(IS:TermList) .

    eq processPreClauses('CONSTANTS_['token[I:Qid]]) =
        CONSTANTS processPreIdentifiers(I:Qid) .

    eq processPreClauses('CONSTANTS_['_`,_[IS:TermList]]) =
        CONSTANTS processPreVariableList(IS:TermList) .

    eq processPreClauses('VALUES_['_=_[TL:TermList]]) =
        VALUES processPreValueDecl('_=_[TL:TermList]) .

    eq processPreClauses('VALUES_['_;_[TL:TermList]]) =
        VALUES processPreValueDeclList(TL:TermList) .

    eq processPreClauses('OPERATIONS_['_=_[TL:TermList]]) =
        OPERATIONS processPreOperationDecl('_=_[TL:TermList]) .

    eq processPreClauses('OPERATIONS_['_`(_`)=_[TL:TermList]]) =
        OPERATIONS processPreOperationDecl('_`(_`)=_[TL:TermList]) .

    eq processPreClauses('OPERATIONS_['_;_[OS:TermList]]) =
        OPERATIONS processPreOperationDeclList(OS:TermList) .

    eq processPreClauses('__[TL:TermList]) =
        processPreClauses(TL:TermList) .

    eq processPreClauses((T:Term, TL:TermList)) =
        processPreClauses(T:Term) processPreClauses(TL:TermList) .

    op processPreValueDecl : Term ~> AMNValuation .
    eq processPreValueDecl('_=_['token[I:Qid], T:Term]) =
        processPreIdentifiers(I:Qid) @= processPreExpression(T:Term) .

    eq processPreValueDecl('_;_[T:Term, TL:NeTermList]) =
        processPreValueDecl(T:Term) ;
        processPreValueDeclList(TL:NeTermList) .

    op processPreValueDeclList : TermList ~> AMNValSet .
    eq processPreValueDeclList(T:Term) = processPreValueDecl(T:Term) .

    eq processPreValueDeclList((T:Term, TL:NeTermList)) =
        processPreValueDecl(T:Term) ;
        processPreValueDeclList(TL:NeTermList) .

    op processPreOperationDecl : Term ~> AMNOperation .
    eq processPreOperationDecl('_=_['token[O:Qid], T:Term]) =
        (processPreIdentifiers(O:Qid) =
          processPreSubstitution(T:Term)) .

    eq processPreOperationDecl('_`(_`)=_['token[O:Qid], TL:TermList, T:Term]) =
        (processPreIdentifiers(O:Qid) (processPreVariableList(TL:TermList)) =
          processPreSubstitution(T:Term)) .

    op processPreOperationDeclList : TermList ~> AMNOpSet .

    ceq processPreOperationDeclList(F:Qid[TL:TermList]) =
         processPreOperationDecl(F:Qid[TL:TermList]) if F:Qid =/= '_;_ .

    eq processPreOperationDeclList('_;_[OS:TermList]) =
        processPreOperationDeclList(OS:TermList) .

    eq processPreOperationDeclList((T:Term, TL:NeTermList)) =
        processPreOperationDecl(T:Term) ;
        processPreOperationDeclList(TL:NeTermList) .

    op processPreVariableList : TermList ~> AMNIdList .
    eq processPreVariableList('token[I:Qid]) = processPreIdentifiers(I:Qid) .
    eq processPreVariableList('_`,_['token[I1:Qid] , 'token[I2:Qid]]) =
        processPreIdentifiers(I1:Qid) @, processPreIdentifiers(I2:Qid) .

    eq processPreVariableList('_`,_['token[I:Qid] , TL:TermList]) =
        processPreIdentifiers(I:Qid) @,
        processPreVariableList(TL:TermList) .
    eq processPreVariableList(('token[I:Qid] , TL:TermList)) =
        processPreIdentifiers(I:Qid) @,
        processPreVariableList(TL:TermList) .

    op processPreIdentifiers : Qid -> GSLIdentifiers .
    ceq processPreIdentifiers(I:Qid) = bid(downTerm(I:Qid, 'processPreIdentifiersError))
      if downTerm(I:Qid, 'processPreIdentifiersError) =/= 'processPreIdentifiersError .

    op processPreSubstitution : Term -> GSLSubstitution .

    eq processPreSubstitution('skip.SubstitutionDecl) = (skip).GSLSubstitution .

    eq processPreSubstitution('_:=_['token[I:Qid], T:Term]) =
        (processPreIdentifiers(I:Qid) @:= processPreExpression(T:Term)) .

    ---     eq processPreSubstitution('token[I:Qid]) = (processPreIdentifiers(I:Qid) ()) .

    eq processPreSubstitution('_`(`)['token[I:Qid]]) =
        (processPreIdentifiers(I:Qid) ()) .

    eq processPreSubstitution('_`(_`)['token[I:Qid], 'bubble[Q:Qid]]) =
   	(processPreIdentifiers(I:Qid) (processPreActuals(Q:Qid))) .

    eq processPreSubstitution('_`(_`)['token[I:Qid], 'bubble['__[TL:TermList]]]) =
	(processPreIdentifiers(I:Qid) (processPreActuals(TL:TermList))) .

    op processPreActuals : TermList -> GSLActuals .
    eq processPreActuals(Q:Qid) = processPreExpression(Q:Qid) .
    eq processPreActuals((TL1:TermList, ''`,.Qid , TL2:TermList)) =
	makeGSLExpression(TL1:TermList) , processPreActuals(TL2:TermList) .
    eq processPreActuals(TL:TermList) = makeGSLExpression(TL:TermList) [owise] .

    op makeGSLExpression : TermList -> GSLExpression .
    eq makeGSLExpression(Q:Qid) = processPreExpression(Q:Qid) .

    ceq makeGSLExpression(TL:TermList) =
	processPreExpression(getTerm(metaParse(upModule('AMN-GRAMMAR,
	false), makeExprDeclQidList(TL:TermList), 'ExpressionDecl)))
    if (metaParse(upModule('AMN-GRAMMAR, false),
	makeExprDeclQidList(TL:TermList), 'ExpressionDecl) ::
	ResultPair) .

    op makeExprDeclQidList : TermList -> QidList .
    eq makeExprDeclQidList((empty).TermList) = (nil).QidList .
    ceq makeExprDeclQidList(Q:Qid) = downTerm(Q:Qid, 'error)
    if downTerm(Q:Qid, 'error) =/= 'error .
    eq makeExprDeclQidList((Q:Qid , TL:TermList)) =
	makeExprDeclQidList(Q:Qid) makeExprDeclQidList(TL:TermList) .

    eq processPreSubstitution('IF_THEN_END[T1:Term, T2:Term]) =
	IF processPrePredicate(T1:Term)
	THEN processPreSubstitution(T2:Term) END .

    eq processPreSubstitution('print[T:Term]) =
        @print(processPreExpression(T:Term)) .

    eq processPreSubstitution('IF_THEN_ELSE_END[T1:Term, T2:Term, T3:Term]) =
        IF processPrePredicate(T1:Term)
        THEN processPreSubstitution(T2:Term)
        ELSE processPreSubstitution(T3:Term)
        END .

    eq processPreSubstitution('_|_[T1:Term, T2:Term]) =
        processPrePredicate(T1:Term) | processPreSubstitution(T2:Term) .

    eq processPreSubstitution('WHILE_DO_[T1:Term, T2:Term]) =
        WHILE processPrePredicate(T1:Term)
        DO processPreSubstitution(T2:Term) .

    eq processPreSubstitution('BEGIN_END[T:Term]) =
        BEGIN processPreSubstitution(T:Term) END .

    eq processPreSubstitution('_;_[T1:Term, T2:Term]) =
        processPreSubstitution(T1:Term) ;
        processPreSubstitution(T2:Term) .

    eq processPreSubstitution('_OR_[T1:Term, T2:Term]) =
        processPreSubstitution(T1:Term) OR
        processPreSubstitution(T2:Term) .

    op processPreExpression : Qid -> GSLExpression .

    eq processPreExpression(I:Qid) =
        if (metaParse(upModule('RAT, false), downTerm(I:Qid, 'Qid), 'Rat)  :: ResultPair)
	then grat(downTerm(getTerm(metaParse(upModule('RAT, false),
		  downTerm(I:Qid, 'Qid), 'Rat)), 1/2))
	else
	if metaParse(upModule('RAT, false), downTerm(I:Qid, 'Qid), 'Bool) :: ResultPair
	  then gboo(downTerm(getTerm(metaParse(upModule('BOOL, false),
		    downTerm(I:Qid, 'Qid), 'Bool)), true))
	  else processPreIdentifiers(I:Qid)
	  fi
	fi .

    op processPreExpression : Term -> GSLExpression .
    eq processPreExpression('token[I:Qid]) =
        if (metaParse(upModule('RAT, false), downTerm(I:Qid, 'Qid), 'Rat)  :: ResultPair)
	then grat(downTerm(getTerm(metaParse(upModule('RAT, false),
		  downTerm(I:Qid, 'Qid), 'Rat)), 1/2))
	else
	if metaParse(upModule('RAT, false), downTerm(I:Qid, 'Qid), 'Bool) :: ResultPair
	  then gboo(downTerm(getTerm(metaParse(upModule('BOOL, false),
		    downTerm(I:Qid, 'Qid), 'Bool)), true))
	  else processPreIdentifiers(I:Qid)
	  fi
	fi .

    eq processPreExpression('_+_[T1:Term, T2:Term]) =
        processPreExpression(T1:Term) @+ processPreExpression(T2:Term) .

    eq processPreExpression('_-_[T1:Term, T2:Term]) =
        processPreExpression(T1:Term) - processPreExpression(T2:Term) .

    eq processPreExpression('_*_[T1:Term, T2:Term]) =
        processPreExpression(T1:Term) * processPreExpression(T2:Term) .

    eq processPreExpression('_/_[T1:Term, T2:Term]) =
        processPreExpression(T1:Term) / processPreExpression(T2:Term) .

    op processPrePredicate : Term ~> GSLPredicate .
    eq processPrePredicate('true.PredicateDecl) = gboo(true) .
    eq processPrePredicate('false.PredicateDecl) = gboo(false) .
    eq processPrePredicate('token[I:Qid]) = processPreIdentifiers(I:Qid) .
    eq processPrePredicate('~[T:Term]) =
        ~ processPrePredicate(T:Term) .
    eq processPrePredicate('_/\_[T1:Term,T2:Term]) =
        processPrePredicate(T1:Term) /\ processPrePredicate(T2:Term) .
    eq processPrePredicate('_==_[T1:Term,T2:Term]) =
        processPreExpression(T1:Term) == processPreExpression(T2:Term) .
endfm

mod BMAUDE is
    pr RUN-AMN .
    pr PROCESS-AMN-DECL .
endm

mod BMAUDE-PRINTING is
    pr QID-LIST .
    pr META-LEVEL .
    pr AMN-MODEL-CHECKER .
    pr BMAUDE .
    pr BPLC .
    pr INT .

    op printQidList : QidList -> QidList .
    eq printQidList(nil) = (nil).QidList .
    eq printQidList(Q:Qid QL:QidList) = printToken(Q:Qid) printQidList(QL:QidList) .

    op printToken : Qid -> Qid .
    eq printToken('MACHINE) = '\b '\! 'MACHINE '\o .
    eq printToken('VARIABLES) = '\b '\! 'VARIABLES '\o .
    eq printToken('CONSTANTS) = '\b '\! 'CONSTANTS '\o .
    eq printToken('VALUES) = '\b '\! 'VALUES '\o .
    eq printToken('OPERATIONS) = '\b '\! 'OPERATIONS '\o .
    eq printToken('WHILE) = '\b '\! 'WHILE '\o .
    eq printToken('DO) = '\b '\! 'DO '\o .
    eq printToken('OR) = '\b '\! 'OR '\o .
    eq printToken('IF) = '\b '\! 'IF '\o .
    eq printToken('THEN) = '\b '\! 'THEN '\o .
    eq printToken('ELSE) = '\b '\! 'ELSE '\o .
    eq printToken('END) = '\b '\! 'END '\o .
    eq printToken('BEGIN) = '\b '\! 'BEGIN '\o .
    eq printToken('print) = '\b '\! 'print '\o .
    eq printToken(':=) = '\b '\! ':= '\o .
    eq printToken('/\) = '\b '\! '/\ '\o .
    eq printToken('==) = '\b '\! '== '\o .
    eq printToken('~) = '\b '\! '~ '\o .
    eq printToken(';) = '\b '\! '; '\o .
    eq printToken('|) = '\b '\! '| '\o .
    eq printToken('`,) = '\b '\! '`, '\o .
    eq printToken('`() = '\b '\! '`( '\o .
    eq printToken('`)) = '\b '\! '`) '\o .
    eq printToken('`[) = '\b '\! '`[ '\o .
    eq printToken('`]) = '\b '\! '`] '\o .
    eq printToken('skip) = '\b '\! 'skip '\o .
    eq printToken(Q:Qid) = (Q:Qid) [owise] .

    op printInputWithError : QidList Nat -> QidList .
    op $printInputWithError : QidList Int QidList -> QidList .
    eq printInputWithError(QL:QidList, N:Nat) =
	$printInputWithError(QL:QidList, N:Nat, (nil).QidList) .
    eq $printInputWithError(QL:QidList, -1, (nil).QidList) = (nil).QidList .

    ceq $printInputWithError(QL1:QidList, -1, (QL2:QidList Q:Qid)) =
      QL2:QidList '\r '>>> Q:Qid '<<< 'HERE '\o
	printQidList(QL1:QidList)
    if QL2:QidList =/= nil .

    eq $printInputWithError(Q:Qid QL1:QidList, I:Int, QL2:QidList) =
	$printInputWithError(QL1:QidList, (I:Int + (- 1)), QL2:QidList
	printToken(Q:Qid)) .

    op printParseError : QidList ResultPair? -> Qid .
    eq printParseError('MACHINE Q:Qid QL:QidList , noParse(N:Nat)) =
	'BMaude: 'Error 'at 'position
	metaPrettyPrint(upModule('NAT, false), upTerm(N:Nat))
	'while 'parsing 'Machine Q:Qid ': '\n
	printInputWithError(('MACHINE Q:Qid QL:QidList), N:Nat) .

    eq printParseError(QL:QidList, ambiguity(T1:ResultPair, T2:ResultPair)) =
	'BMaude: '\r 'Ambiguous 'parse '\o '\n
	metaPrettyPrint(upModule('AMN-GRAMMAR, false), getTerm(T1:ResultPair)) '\n
	'\r 'vs. '\o '\n
	metaPrettyPrint(upModule('AMN-GRAMMAR, false), getTerm(T2:ResultPair)) .

    op printValSet : AMNValSet -> QidList .

    eq printValSet(I:GSLIdentifiers @= E:GSLExpression) =
	printGSLIdentifiers(I:GSLIdentifiers) printToken('=)
	printExpression(E:GSLExpression) .

    eq printValSet(V:AMNValuation ; VS:AMNValSet) =
	printValSet(V:AMNValuation) printToken(';) printValSet(VS:AMNValSet) .

    op printIdList : AMNIdList -> QidList .
    eq printIdList(I:GSLIdentifiers) = printGSLIdentifiers(I:GSLIdentifiers) .

    eq printIdList(I:GSLIdentifiers @, IL:AMNIdList) =
	printGSLIdentifiers(I:GSLIdentifiers) printToken('`,) '\s
	printIdList(IL:AMNIdList) .

    op printClause : AMNAbsVariables -> QidList .

    eq printClause(VARIABLES IL:AMNIdList) = '\n '\s
       printToken('VARIABLES) printIdList(IL:AMNIdList) '\o .

    op printClause : AMNAbsConstants -> QidList .

    eq printClause(CONSTANTS IL:AMNIdList) = '\n '\s
       printToken('CONSTANTS) printIdList(IL:AMNIdList) '\o .

    op printClause : AMNValuesClause -> QidList .

    eq printClause(VALUES VS:AMNValSet) = '\n '\s printToken('VALUES)
       printValSet(VS:AMNValSet) .

    op printPredicate : GSLPredicate -> QidList .

    eq printPredicate(gboo(B:Bool)) = '\g
       metaPrettyPrint(upModule('BOOL, false), upTerm(B:Bool)) '\o .

    eq printPredicate(I:GSLIdentifiers) =
       printGSLIdentifiers(I:GSLIdentifiers) .

    eq printPredicate(E1:GSLExpression == E2:GSLExpression) =
       printExpression(E1:GSLExpression) printToken('==)
       printExpression(E2:GSLExpression) .

    eq printPredicate(P1:GSLPredicate /\ P2:GSLPredicate) =
       printPredicate(P1:GSLPredicate) printToken('/\)
       printPredicate(P2:GSLPredicate) .

    eq printPredicate(~(P:GSLPredicate)) = printToken('~)
       printToken('`() printPredicate(P:GSLPredicate) printToken('`)) '\s .

    eq printPredicate(P:GSLPredicate) =
       metaPrettyPrint(upModule('BMAUDE, false), upTerm(P:GSLPredicate)) [owise] .

    op printExpression : GSLExpression -> QidList .

    eq printExpression(grat(R:Rat)) = '\g
       metaPrettyPrint(upModule('RAT, false), upTerm(R:Rat)) '\o .

    eq printExpression(I:GSLIdentifiers) = printGSLIdentifiers(I:GSLIdentifiers) .

    eq printExpression(P:GSLPredicate) = printPredicate(P:GSLPredicate) .

    eq printExpression(E1:GSLExpression @+ E2:GSLExpression) =
       printExpression(E1:GSLExpression) printToken('+)
       printExpression(E2:GSLExpression) .

    eq printExpression(E1:GSLExpression * E2:GSLExpression) =
       printExpression(E1:GSLExpression) printToken('*)
       printExpression(E2:GSLExpression) .

    eq printExpression(E1:GSLExpression - E2:GSLExpression) =
       printExpression(E1:GSLExpression) printToken('-)
       printExpression(E2:GSLExpression) .

    eq printExpression(E1:GSLExpression / E2:GSLExpression) =
       printExpression(E1:GSLExpression) printToken('/)
       printExpression(E2:GSLExpression) .

    eq printExpression(E:GSLExpression) =
       metaPrettyPrint(upModule('BMAUDE, false), upTerm(E:GSLExpression)) [owise] .

    op printActuals : GSLActuals -> QidList .
    eq printActuals(E:GSLExpression) = printExpression(E:GSLExpression) .
    eq printActuals((E:GSLExpression, A:GSLActuals)) =
	printExpression(E:GSLExpression) printToken('`,) printActuals(A:GSLActuals) .

    op printSubstitution : GSLSubstitution Nat -> QidList .

    eq printSubstitution(@print(I:GSLIdentifiers), N:Nat) =
       printToken('print) '`( printGSLIdentifiers(I:GSLIdentifiers) '`) .

    eq printSubstitution(skip, N:Nat) = printToken('skip) .

    eq printSubstitution((I:GSLIdentifiers ()), N:Nat) =
	printGSLIdentifiers(I:GSLIdentifiers) printToken('`() printToken('`)) .

    eq printSubstitution((I:GSLIdentifiers (A:GSLActuals)), N:Nat) =
   	printGSLIdentifiers(I:GSLIdentifiers) printToken('`()
   	printActuals(A:GSLActuals) printToken('`)) .

    eq printSubstitution((I:GSLIdentifiers @:= E:GSLExpression), N:Nat) =
	printGSLIdentifiers(I:GSLIdentifiers) printToken(':=)
	printExpression(E:GSLExpression) .

    eq printSubstitution((S1:GSLSubstitution [] S2:GSLSubstitution), N:Nat) =
	printSubstitution(S1:GSLSubstitution, N:Nat) '\s
	printToken('`[) printToken('`]) '\s
	printSubstitution(S2:GSLSubstitution, N:Nat) .

    eq printSubstitution((S1:GSLSubstitution OR S2:GSLSubstitution), N:Nat) =
	printSubstitution(S1:GSLSubstitution, N:Nat) '\s
	printToken('OR) '\s printSubstitution(S2:GSLSubstitution,
	N:Nat) .

    eq printSubstitution((S1:GSLSubstitution ; S2:GSLSubstitution), N:Nat) =
	printSubstitution(S1:GSLSubstitution, N:Nat)
	printToken(';) printSubstitution(S2:GSLSubstitution, N:Nat) .

    eq printSubstitution((P:GSLPredicate | S:GSLSubstitution), N:Nat) =
	'\n printSpaces(N:Nat) printPredicate(P:GSLPredicate)
	printToken('|) printSubstitution(S:GSLSubstitution, N:Nat) .

    eq printSubstitution((WHILE P:GSLPredicate DO S:GSLSubstitution), N:Nat) =
	'\n printSpaces(N:Nat) printToken('WHILE) printPredicate(P:GSLPredicate)
	printToken('DO)
	printSubstitution(S:GSLSubstitution, N:Nat + 1) .

    eq printSubstitution((IF P:GSLPredicate THEN S:GSLSubstitution END), N:Nat) =
	  '\n printSpaces(N:Nat) printToken('IF)
	  printPredicate(P:GSLPredicate) '\n printSpaces(N:Nat)
	  printToken('THEN) printSubstitution(S:GSLSubstitution, N:Nat
	  + 1) '\n printSpaces(N:Nat) printToken('END) .

    eq printSubstitution((IF P:GSLPredicate THEN S1:GSLSubstitution
	    ELSE S2:GSLSubstitution END), N:Nat) =
	  '\n printSpaces(N:Nat) printToken('IF)
   	  printPredicate(P:GSLPredicate) '\n printSpaces(N:Nat)
   	  printToken('THEN) printSubstitution(S1:GSLSubstitution,
   	  N:Nat + 1) '\n printSpaces(N:Nat) printToken('ELSE)
   	  printSubstitution(S2:GSLSubstitution, N:Nat + 1) '\n
   	  printSpaces(N:Nat) printToken('END) .

    eq printSubstitution(S:GSLSubstitution, N:Nat) =
       metaPrettyPrint(upModule('BMAUDE, false),
       upTerm(S:GSLSubstitution)) [owise] .

    op printOperation : AMNOperation Nat -> QidList .

    eq printOperation((I:GSLIdentifiers = S:GSLSubstitution), N:Nat) =
	'\n printSpaces(N:Nat) printGSLIdentifiers(I:GSLIdentifiers)
	'= printSubstitution(S:GSLSubstitution, N:Nat + 1) .

    eq printOperation((I:GSLIdentifiers(IL:AMNIdList) = S:GSLSubstitution), N:Nat) =
	'\n printSpaces(N:Nat)
	printGSLIdentifiers(I:GSLIdentifiers) '`(
	printIdList(IL:AMNIdList) '`) '=
	printSubstitution(S:GSLSubstitution, N:Nat + 1) .

    op printSpaces : Nat -> QidList .
    eq printSpaces(0) = (nil).QidList .
    eq printSpaces(N:Nat) = '\s printSpaces(sd(N:Nat, 1)) .

    op printOperations : AMNOpSet -> QidList .
    eq printOperations(O:AMNOperation) = printOperation(O:AMNOperation, 2) .
    eq printOperations(O:AMNOperation ; OS:AMNOpSet) =
	printOperation(O:AMNOperation, 2) '; '\n printOperations(OS:AMNOpSet) .

    op printClause : AMNOpSet -> QidList .
    eq printClause(OPERATIONS OS:AMNOpSet) =
	'\n '\s printToken('OPERATIONS)
        printOperations(OS:AMNOpSet) .

    op printClauses : AMNClauses -> QidList .
    eq printClauses(V:AMNAbsVariables) = printClause(V:AMNAbsVariables) .

    eq printClauses(T:AMNAbsConstants) = printClause(T:AMNAbsConstants) .

    eq printClauses(V:AMNValuesClause) = printClause(V:AMNValuesClause) .

    eq printClauses(OP:AMNOperations) = printClause(OP:AMNOperations) .

    eq printClauses(V:AMNAbsVariables C:AMNClauses) =
	printClause(V:AMNAbsVariables) printClauses(C:AMNClauses) .

    eq printClauses(T:AMNAbsConstants C:AMNClauses) =
   	printClause(T:AMNAbsConstants) printClauses(C:AMNClauses) .

    eq printClauses(V:AMNValuesClause C:AMNClauses) =
  	printClause(V:AMNValuesClause) printClauses(C:AMNClauses) .

    eq printClauses(OP:AMNOperations C:AMNClauses) =
   	printClause(OP:AMNOperations) printClauses(C:AMNClauses) .

    op printMachine : AMNMachine -> QidList .
    eq printMachine(MACHINE Q:GSLIdentifiers C:AMNClauses END) =
	printToken('MACHINE) printGSLIdentifiers(Q:GSLIdentifiers)
	printClauses(C:AMNClauses)
	--- metaPrettyPrint(upModule('BMAUDE, false), upTerm(C:AMNClauses))
	'\n printToken('END) .

    op printId : Id -> Qid .
    eq printId(gid(bid(Q:Qid))) = (Q:Qid).Qid .

    op printGSLIdentifiers : GSLIdentifiers -> Qid .
    eq printGSLIdentifiers(bid(Q:Qid)) = '\c (Q:Qid).Qid '\o .

    op printState : Env Store -> QidList .

    eq printState(noEnv, S:Store) = (nil).QidList .

    eq printState((I:Id |-> bind(L:Loc)) , ((L:Loc |-> store(R:Rat)), S:Store)) =
	printId(I:Id) '= metaPrettyPrint(upModule('RAT, false), upTerm(R:Rat)) .

    ceq printState(((I:Id |-> bind(L:Loc)), E:Env) ,
	  ((L:Loc |-> store(R:Rat)), S:Store)) =
	printId(I:Id) '=
	metaPrettyPrint(upModule('RAT, false), upTerm(R:Rat))
	printState(E:Env , (L:Loc |-> store(R:Rat), S:Store)) if E:Env
	=/= noEnv .

    eq printState((I:Id |-> bind(L:Loc)), (L:Loc |-> store(B:Bool),
   	S:Store)) = printId(I:Id) '= metaPrettyPrint(upModule('BOOL,
   	false), upTerm(B:Bool)) .

    ceq printState(((I:Id |-> bind(L:Loc)), E:Env) ,
	           ((L:Loc |-> store(B:Bool)), S:Store)) = printId(I:Id) '=
   	metaPrettyPrint(upModule('RAT, false), upTerm(B:Bool)) '`,
   	printState(E:Env , (L:Loc |-> store(B:Bool), S:Store)) if
   	E:Env =/= noEnv .

    eq printState(((I:Id |-> B:Bindable), E:Env) , S:Store) =
       printState(E:Env , S:Store) [owise] .

    op printCmd : Cmd -> QidList .
    eq printCmd(seq(C1:Cmd, C2:Cmd)) = printCmd(C1:Cmd) printToken(';) printCmd(C2:Cmd) .
    eq printCmd(assign(I:Id, E:Exp)) = printExp(I:Id) printToken(':=) printExp(E:Exp) .
    eq printCmd(if(E:Exp, C1:Cmd, C2:Cmd)) = printToken('IF) printExp(E:Exp) '... .

    eq printCmd(choice(C1:Cmd, C2:Cmd)) = printCmd(C1:Cmd)
       printToken('OR) printCmd(C2:Cmd) .

    eq printCmd(C:Cmd) = metaPrettyPrint(upModule('BMAUDE, false), upTerm(C:Cmd)) .

    op printExp : Exp -> QidList .

    eq printExp(rat(R:Rat)) = '\g metaPrettyPrint(upModule('RAT, false),
	  upTerm(R:Rat)) '\o .

    eq printExp(boo(B:Bool)) = '\g metaPrettyPrint(upModule('BOOL, false),
	  upTerm(B:Bool)) '\o .

    eq printExp(neg(E:Exp)) = printToken('~) printExp(E:Exp) .
    eq printExp(and(E1:Exp, E2:Exp)) = printExp(E1:Exp) printToken('/\) printExp(E2:Exp) .
    eq printExp(eq(E1:Exp, E2:Exp)) = printExp(E1:Exp) printToken('==) printExp(E2:Exp) .
    eq printExp(gid(I:GSLIdentifiers)) = printGSLIdentifiers(I:GSLIdentifiers) .
    eq printExp(E:Exp) = metaPrettyPrint(upModule('BMAUDE, false), upTerm(E:Exp)) .

    op printCnt : ControlStack ValueStack -> QidList .
    eq printCnt((LOOP C:ControlStack), (V:Value val(loop(E:Exp, K:Cmd)) VS:ValueStack)) =
	printToken('WHILE) printToken('`() printExp(E:Exp) printToken('`)) '... .

    eq printCnt((choice(K1:Cmd, K2:Cmd) C:ControlStack), VS:ValueStack) =
   	printCmd(K1:Cmd) printToken('OR) printCmd(K2:Cmd) .

    eq printCnt(C:ControlStack, VS:ValueStack) =
	'\n 'Constrol 'stack:
	metaPrettyPrint(upModule('BMAUDE, false),
	  upTerm(C:ControlStack))
	'\n 'Value 'stack:
	metaPrettyPrint(upModule('BMAUDE, false),
	upTerm(VS:ValueStack)) .

    op printConf : Conf -> QidList .

    eq printConf(< env : E:Env , sto : S:Store , exc : X:Exc , cnt :
	  C:ControlStack, val : V:ValueStack, ...:Set{SemComp} > ) =
      if X:Exc == CNT
	then printCnt(C:ControlStack, V:ValueStack) '`[ printState(E:Env, S:Store) '`]
	else 'abort fi .

    --- TODO: There is a parsing problem here:

    --- Warning: "bmaude.maude", line 544 (mod BMAUDE-PRINTING):
    --- multiple distinct parses for statement

    --- eq printConf(< exc : EXT, ...:Set{SemComp} >) = 'abort .

    op printTraceStep : TraceStep -> QidList .

    eq printTraceStep({T:Term, Y:Type, R:Rule}) =
       printConf(downTerm(T:Term, < noSemComp >)) .

    op printTrace : Trace Nat -> QidList .
    eq printTrace(nil, N:Nat) = (nil).QidList .
    eq printTrace(TS:TraceStep, N:Nat) =
	'\b 'State metaPrettyPrint(upModule('NAT, false), upTerm(N:Nat)) ': '\o '\n
	printTraceStep(TS:TraceStep) .

    ceq printTrace(TS:TraceStep T:Trace, N:Nat) =
	'\b 'State metaPrettyPrint(upModule('NAT, false), upTerm(N:Nat)) ': '\o '\n
	printTraceStep(TS:TraceStep) '\n printTrace(T:Trace, (N:Nat + 1))
      if T:Trace =/= nil .

    op printTransitionList : TransitionList -> QidList .
    eq printTransitionList(nil) = (nil).QidList .
    eq printTransitionList({C:Conf, R:RuleName}) = printConf(C:Conf) .
    ceq printTransitionList({C:Conf, R:RuleName} TL:TransitionList) =
	printConf(C:Conf) '\b '-> '\o printTransitionList(TL:TransitionList)
      if TL:TransitionList =/= nil .

    op printModelCheckResult : ModelCheckResult -> QidList .
    eq printModelCheckResult(B:Bool) =
	'BMaude: '\b 'Model 'check 'result '\o '\n
	metaPrettyPrint(upModule('BOOL, false), upTerm(B:Bool)) .
    eq printModelCheckResult(counterexample(TL1:TransitionList, TL2:TransitionList)) =
	'BMaude: '\b 'Model 'check 'counter 'example '\o '\n
	'\b 'Path 'from 'the 'initial 'state: '\o
	'\n printTransitionList(TL1:TransitionList)
   	'\n '\b 'Loop: '\o
	'\n printTransitionList(TL2:TransitionList) .

    op printValueStack : ValueStack -> QidList .
    eq printValueStack(evs) = '\b 'No 'output. '\o .

    eq printValueStack(val(R:Rat) evs) =
       metaPrettyPrint(upModule('RAT, false), upTerm(R:Rat)) .

    eq printValueStack(val(B:Bool) evs) =
       metaPrettyPrint(upModule('BOOL, false), upTerm(B:Bool)) .

    eq printValueStack(V:Value VS:ValueStack) =
	printValueStack(V:Value) printValueStack(VS:ValueStack) .

    op printOut : Conf -> QidList .
    eq printOut(< out : O:ValueStack , ...:Set{SemComp} > ) =
       printValueStack(O:ValueStack) .

    op printExec : Term ~> QidList .
    ceq printExec(T:Term) = printOut(downTerm(T:Term, < noSemComp >))
      if downTerm(T:Term, < noSemComp >) =/= < noSemComp > .

    op printExecn : Term ~> QidList .
    ceq printExecn(T:Term) = printConf(downTerm(T:Term, < noSemComp >))
      if downTerm(T:Term, < noSemComp >) =/= < noSemComp > .
endm

mod BMAUDE-MODEL-CHECKER is
    pr AMN-MODEL-CHECKER .
    pr META-LEVEL .
    pr BMAUDE .

    op makeOpDeclSet : AMNIdList -> OpDeclSet .
    eq makeOpDeclSet(bid(Q:Qid)) = (op Q:Qid : 'Rat -> 'Prop [none] .) .
    eq makeOpDeclSet(I:GSLIdentifiers @, IL:AMNIdList) =
	makeOpDeclSet(I:GSLIdentifiers) makeOpDeclSet(IL:AMNIdList) .

    op makeEqSet : AMNIdList -> EquationSet .

    eq makeEqSet(bid(Q:Qid)) = (ceq '_|=_['S:State, Q:Qid['R:Rat]] =
	'true.Bool if 'valueOf['bid[upTerm(Q:Qid)],'R:Rat,'S:State] =
	'true.Bool [none] .) .

    eq makeEqSet(I:GSLIdentifiers @, IL:AMNIdList) =
   	makeEqSet(I:GSLIdentifiers) makeEqSet(IL:AMNIdList) .

    op makeMCModule : AMNMachine -> SModule .
    eq makeMCModule(MACHINE bid(Q:Qid) (VARIABLES I:AMNIdList) C:AMNClauses END) =
       (mod qid("MODEL-CHECK-" + string(Q:Qid)) is
            protecting 'RUN-AMN .
            protecting 'AMN-MODEL-CHECKER .
            protecting 'META-LEVEL .
            protecting 'GSL-SYNTAX .
            sorts none .
            none --- SubsortDeclSet
            --- op 'bid : 'Qid -> 'GSLIdentifiers [none] .
            makeOpDeclSet(I:AMNIdList)
            none --- MembAxSet
            makeEqSet(I:AMNIdList)
            none endm) .
endm

mod BMAUDE-COMMANDS is
    pr BMAUDE .
    pr META-LEVEL .
    pr BMAUDE-PRINTING .
    pr BMAUDE-MODEL-CHECKER .

    sorts Command Machine BMaudeState .
    subsort AMNMachine < Machine < Command .
    op noMachine : -> Machine .
    ops show idle : -> Command .
    op search___ : Nat GSLSubstitution Condition -> Command .
    op narrow__ : Nat GSLSubstitution -> Command .
    op error : -> [ModelCheckResult] .
    op dmc__ : GSLSubstitution Term -> Command .
    op mc__ : GSLSubstitution Term -> Command .
    op exec_ : GSLSubstitution -> Command .
    op dexec_ : GSLSubstitution -> Command .
    op exec__ : Nat GSLSubstitution -> Command .
    op dexec__ : Nat GSLSubstitution -> Command .
    op <_;_;_> : Command Machine QidList -> BMaudeState .
    var QIL : QidList .

    rl [load-machine] :
	< MACHINE bid(Q:Qid) C:AMNClauses END ; M:Machine ; QIL > =>
	< idle ; (MACHINE bid(Q:Qid) C:AMNClauses END) ;
	         'BMaude: '\b 'Machine Q:Qid 'loaded. '\o > .

    crl [search] :
	< search N:Nat S:GSLSubstitution C:Condition ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if T:ResultTriple? :: ResultTriple
 	then ('BMaude: '\b 'Search 'trace '\o '\n
	    printTrace(metaSearchPath(upModule('BMAUDE, false),
		upTerm(run(S:GSLSubstitution, M:AMNMachine)),
		'C:Conf, C:Condition, '+, unbounded, N:Nat), 1))
	else
	  (if (T:ResultTriple? == failure)
	    then
	      ('BMaude: '\b 'No 'solution 'while 'searching '\o
		printSubstitution(S:GSLSubstitution, 0))
	    else
	      ('BMaude: '\r 'Error 'while 'searching '\o
		printSubstitution(S:GSLSubstitution, 0))
	      fi)
	fi >
      if T:ResultTriple? :=
	  metaSearch(upModule('BMAUDE, false),
	    upTerm(run(S:GSLSubstitution, M:AMNMachine)),
	    'C:Conf, C:Condition, '*, unbounded, N:Nat) .

    crl [mc] :
	< mc S:GSLSubstitution T:Term ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if (T:ResultPair? :: ResultPair) and
	    (downTerm(getTerm(T:ResultPair?), error) :: ModelCheckResult)
 	then printModelCheckResult(downTerm(getTerm(T:ResultPair?), error))
	else
	  ('BMaude: '\r 'Error 'while 'model 'checking '\o
	    printSubstitution(S:GSLSubstitution, 0) '|=
	    metaPrettyPrint(upModule('META-LEVEL, false), T:Term))
	fi >
      if T:ResultPair? :=
          metaReduce(makeMCModule(M:AMNMachine),
	    '_`,_|=?_[upTerm(M:AMNMachine), upTerm(S:GSLSubstitution), T:Term]) .

    crl [dmc] :
	< dmc S:GSLSubstitution T:Term ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if (T:ResultPair? :: ResultPair) and
	    (downTerm(getTerm(T:ResultPair?), error) :: ModelCheckResult)
 	then metaPrettyPrint(makeMCModule(M:AMNMachine), getTerm(T:ResultPair?))
	else
	  ('BMaude: '\r 'Error 'while 'model 'checking '\o
	    metaPrettyPrint(upModule('BMAUDE, false), upTerm(S:GSLSubstitution)) '|=
	    metaPrettyPrint(upModule('META-LEVEL, false), T:Term))
	fi >
      if T:ResultPair? :=
          metaReduce(makeMCModule(M:AMNMachine),
	    '_`,_|=?_[upTerm(M:AMNMachine), upTerm(S:GSLSubstitution), T:Term]) .


    crl [exec-unbounded] :
	< exec S:GSLSubstitution ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if T:ResultPair? :: ResultPair
	then 'BMaude: '\b 'Execution 'result '\o '\n printExec(getTerm(T:ResultPair?))
	else ('BMaude: '\r 'Error 'while 'executing '\o
	    printSubstitution(S:GSLSubstitution, 0))
	fi >
      if T:ResultPair? :=
	  metaRewrite(upModule('BMAUDE, false),
            upTerm(run(S:GSLSubstitution, M:AMNMachine)), unbounded) .

    crl [dexec-unbounded] :
	< dexec S:GSLSubstitution ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if T:ResultPair? :: ResultPair
	then 'BMaude: '\b 'Execution 'result '\o '\n
	  metaPrettyPrint(upModule('BMAUDE, false), getTerm(T:ResultPair?))
	else ('BMaude: '\r 'Error 'while 'executing '\o
	    metaPrettyPrint(upModule('BMAUDE, false), upTerm(S:GSLSubstitution)) )
	fi >
      if T:ResultPair? :=
	  metaRewrite(upModule('BMAUDE, false),
            upTerm(run(S:GSLSubstitution, M:AMNMachine)), unbounded) .

    crl [dexec-bounded] :
	< dexec N:Nat S:GSLSubstitution ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if T:ResultPair? :: ResultPair
	then 'BMaude: '\b 'Execution 'result '\o '\n
	  metaPrettyPrint(upModule('BMAUDE, false), getTerm(T:ResultPair?))
	else ('BMaude: '\r 'Error 'while 'executing '\o
	    metaPrettyPrint(upModule('BMAUDE, false), upTerm(S:GSLSubstitution)) )
	fi >
      if T:ResultPair? :=
	  metaRewrite(upModule('BMAUDE, false),
            upTerm(run(S:GSLSubstitution, M:AMNMachine)), N:Nat) .

    crl [exec-bounded] :
	< exec N:Nat S:GSLSubstitution ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if T:ResultPair? :: ResultPair
	then 'BMaude: '\b 'Execution 'state '\o '\n printExecn(getTerm(T:ResultPair?))
	else ('BMaude: '\r 'Error 'while 'executing '\o
	    printSubstitution(S:GSLSubstitution, 0))
	fi >
      if T:ResultPair? :=
	  metaRewrite(upModule('BMAUDE, false),
            upTerm(run(S:GSLSubstitution, M:AMNMachine)), N:Nat) .

    crl [sexec] :
	< narrow N:Nat S:GSLSubstitution ; M:AMNMachine ; QIL > =>
	< idle ; M:AMNMachine ;
      if T:ResultTriple? :: ResultTriple
 	then ('BMaude: '\b 'symbolic 'execution 'state 'after
	    metaPrettyPrint(upModule('NAT, false), upTerm(N:Nat)) 'steps 'of
	    printSubstitution(S:GSLSubstitution, 0) '\o '\n
	    printExecn(getTerm(T:ResultTriple?)))
	else
	  (if (T:ResultTriple? == failure)
	    then
	      ('BMaude: '\b 'No 'solution 'while 'symbolic 'executing
		metaPrettyPrint(upModule('NAT, false), upTerm(N:Nat)) 'steps 'of '\o
		printSubstitution(S:GSLSubstitution, 0))
	    else
	      ('BMaude: '\r 'Error 'while 'symbolic 'executing
		metaPrettyPrint(upModule('NAT, false), upTerm(N:Nat)) 'steps 'of '\o
		printSubstitution(S:GSLSubstitution, 0))
	      fi)
	fi >
      if T:ResultTriple? :=
	  metaNarrow(upModule('BMAUDE, false),
	    upTerm(run(S:GSLSubstitution, M:AMNMachine)),
	    'C:Conf, '+, unbounded, N:Nat) .
endm

mod BMAUDE-SEARCH-CONDITION is
    pr QID-LIST .
    pr META-LEVEL .
    pr RAT .

    sort Condition? .
    subsort Condition < Condition? .

    op error : -> [Rat] .
    op error : -> Condition? .
    op parseSearchCondition : QidList -> Condition? .
    eq parseSearchCondition(nil) = nil .
    ceq parseSearchCondition(Q1:Qid '= Q2:Qid) =
      if (T:ResultPair? :: ResultPair and downTerm(getTerm(T:ResultPair?), error) :: Rat)
	then 'getValue['gid['bid[upTerm(Q1:Qid)]],'C:Conf] = 'store[getTerm(T:ResultPair?)]
	else error
	fi
      if T:ResultPair? := metaParse(upModule('RAT, false), Q2:Qid, 'Rat) .

    eq parseSearchCondition(Q1:Qid '= Q2:Qid 'and QIL:QidList) =
	parseSearchCondition(Q1:Qid '= Q2:Qid) /\ parseSearchCondition(QIL:QidList) .
endm

mod BMAUDE-INTERFACE is
    including LOOP-MODE * (sort State to LoopState).
    including META-LEVEL .
    including BMAUDE-COMMANDS .
    including BMAUDE-SEARCH-CONDITION .
    including BMAUDE-PRINTING .
    pr NAT .

    subsort BMaudeState < LoopState .

    op error : -> [Nat] .
    op error : -> [Formula] .
    op init : -> System .
    op init`B`Maude`no`banner : -> System .
    op banner : -> QidList .
    eq banner = '\g 'BMaude 'Prototype '\o '\n '`( '\y '\!
	  'Uruçu-Amarela 'February '2018 '\o '`) .
    eq init = [nil, < idle ; noMachine ; nil >, banner] .
    eq init`B`Maude`no`banner = [nil, < idle ; noMachine ; nil >, nil] .

    vars QIL QIL' QIL'' QIL1 QIL2 : QidList .

    rl [version] : ['version, B:BMaudeState, QIL] => [nil, B:BMaudeState, banner] .

    rl [say] : ['say QIL1, B:BMaudeState, QIL2] => [nil, B:BMaudeState, '\g QIL1] .

    crl [in] : ['MACHINE Q:Qid QIL, < idle ; M:Machine ; QIL' >, QIL''] =>
      if (T:ResultPair? :: ResultPair)
        then [nil, < processPreMachine(getTerm(T:ResultPair?)) ; M:Machine ; QIL' >, QIL'']
        else [nil, < idle ; noMachine ; nil >,
	    printParseError('MACHINE Q:Qid QIL,T:ResultPair?)]
        fi
      if T:ResultPair? :=
	  metaParse(upModule('AMN-GRAMMAR, false), 'MACHINE Q:Qid QIL, 'MachineDecl) .

    crl [view] : ['view 'machine, < idle ; M:Machine ; QIL' >, QIL''] =>
	[nil, < idle ; M:Machine ; QIL' >, printMachine(M:Machine)]
      if M:Machine =/= noMachine .

    crl [view] : ['view, < idle ; M:Machine ; QIL' >, QIL''] =>
	[nil, < idle ; M:Machine ; QIL' >, printMachine(M:Machine)]
      if M:Machine =/= noMachine .

    crl [no-machine-error] : [QIL, < idle ; noMachine ; QIL' >, QIL''] =>
        [nil, < idle ; noMachine ; QIL' >,
	  'BMaude: '\r 'Error 'no 'machine 'loaded. '\o ']
      if QIL =/= nil .

    crl [mc] : [('mc QIL1 '|= QIL2), < idle ; M:Machine ; QIL' >, QIL''] =>
      if ((P1:ResultPair? :: ResultPair) and (P2:ResultPair? :: ResultPair))
        then [nil,
          if processPreSubstitution(getTerm(P1:ResultPair?)) :: GSLSubstitution
	    then < mc processPreSubstitution(getTerm(P1:ResultPair?))
	      getTerm(P2:ResultPair?) ; M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o 'mc QIL1 '|= QIL2]
        fi
      if
	  P1:ResultPair? := metaParse(upModule('AMN-GRAMMAR, false), QIL1,
	    'SubstitutionDecl) /\
	  P2:ResultPair? := metaParse(makeMCModule(M:Machine), QIL2, 'Formula)
	    /\ M:Machine =/= noMachine .

    crl [dmc] : [('dmc QIL1 '|= QIL2), < idle ; M:Machine ; QIL' >, QIL''] =>
      if ((P1:ResultPair? :: ResultPair) and (P2:ResultPair? :: ResultPair))
        then [nil,
          if processPreSubstitution(getTerm(P1:ResultPair?)) :: GSLSubstitution
            then < dmc processPreSubstitution(getTerm(P1:ResultPair?))
	      getTerm(P2:ResultPair?) ; M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o 'mc QIL1 '|= QIL2]
        fi
      if
	  P1:ResultPair? :=
	     metaParse(upModule('AMN-GRAMMAR, false), QIL1, 'SubstitutionDecl) /\
	  P2:ResultPair? :=
	     metaParse(makeMCModule(M:Machine), QIL2, 'Formula)
	  /\ M:Machine =/= noMachine .

    crl [search] : [('search Q:Qid QIL1 'where QIL2),
	  < idle ; M:Machine ; QIL' >, QIL''] =>
      if ((downTerm(getTerm(P1:ResultPair?), error) :: Nat) and
	    (P2:ResultPair? :: ResultPair) and
	    (P3:Condition? :: Condition))
        then [nil,
          if processPreSubstitution(getTerm(P2:ResultPair?)) :: GSLSubstitution
	    then < search downTerm(getTerm(P1:ResultPair?), error)
	      processPreSubstitution(getTerm(P2:ResultPair?))
	      P3:Condition? ; M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o
	    'search Q:Qid QIL1 'where QIL2 ]
        fi
      if
	  P1:ResultPair? :=
	     metaParse(upModule('NAT, false), Q:Qid, 'Nat) /\
	  P2:ResultPair? :=
	     metaParse(upModule('AMN-GRAMMAR, false), QIL1, 'SubstitutionDecl) /\
	  P3:Condition? := parseSearchCondition(QIL2) .

    crl [exec-bounded] : [('dexecn Q:Qid QIL), < idle ; M:Machine ; QIL' >, QIL''] =>
      if (P1:ResultPair? :: ResultPair) and (P2:ResultPair? :: ResultPair)
        then [nil,
          if (processPreSubstitution(getTerm(P2:ResultPair?)) :: GSLSubstitution and
		downTerm(getTerm(P1:ResultPair?), error) :: Nat)
            then < dexec downTerm(getTerm(P1:ResultPair?), error)
	      processPreSubstitution(getTerm(P2:ResultPair?)) ; M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o 'exec Q:Qid QIL ]
        fi
      if
	  P1:ResultPair? := metaParse(upModule('NAT, false), Q:Qid, 'Nat) /\
	  P2:ResultPair? := metaParse(upModule('AMN-GRAMMAR, false), QIL,
	    'SubstitutionDecl) .

    crl [exec-bounded] : [('execn Q:Qid QIL), < idle ; M:Machine ; QIL' >, QIL''] =>
      if (P1:ResultPair? :: ResultPair) and (P2:ResultPair? :: ResultPair)
        then [nil,
          if (processPreSubstitution(getTerm(P2:ResultPair?)) :: GSLSubstitution and
		downTerm(getTerm(P1:ResultPair?), error) :: Nat)
            then < exec downTerm(getTerm(P1:ResultPair?), error)
	      processPreSubstitution(getTerm(P2:ResultPair?)) ; M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o 'exec '\s Q:Qid '\s QIL ]
        fi
      if
	  P1:ResultPair? := metaParse(upModule('NAT, false), Q:Qid, 'Nat) /\
	  P2:ResultPair? := metaParse(upModule('AMN-GRAMMAR, false), QIL,
	    'SubstitutionDecl) .

    crl [dexec-unbounded] : [('dexec QIL), < idle ; M:Machine ; QIL' >, QIL''] =>
      if P:ResultPair? :: ResultPair
        then [nil,
          if processPreSubstitution(getTerm(P:ResultPair?)) :: GSLSubstitution
            then < dexec processPreSubstitution(getTerm(P:ResultPair?)) ;
	      M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o 'exec '\s QIL ]
        fi
      if P:ResultPair? :=
	  metaParse(upModule('AMN-GRAMMAR, false), QIL, 'SubstitutionDecl) .

    crl [exec-unbounded] : [('exec QIL), < idle ; M:Machine ; QIL' >, QIL''] =>
      if P:ResultPair? :: ResultPair
        then [nil,
          if processPreSubstitution(getTerm(P:ResultPair?)) :: GSLSubstitution
            then < exec processPreSubstitution(getTerm(P:ResultPair?)) ; M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o 'exec '\s QIL ]
        fi
      if P:ResultPair? :=
	  metaParse(upModule('AMN-GRAMMAR, false), QIL, 'SubstitutionDecl) .

    crl [sexec] : [('sexec Q:Qid QIL1), < idle ; M:Machine ; QIL' >, QIL''] =>
      if ((downTerm(getTerm(P1:ResultPair?), error) :: Nat) and
	    (P2:ResultPair? :: ResultPair))
        then [nil,
          if processPreSubstitution(getTerm(P2:ResultPair?)) :: GSLSubstitution
            then < narrow downTerm(getTerm(P1:ResultPair?), error)
	      processPreSubstitution(getTerm(P2:ResultPair?)) ;
	      M:Machine ; QIL' >
            else < idle ; M:Machine ; QIL' >
              fi,
            QIL'']
        else [nil, < idle ; M:Machine ; nil >,
	    'BMaude: '\r 'Error 'while 'processing 'command '\o
	    'symexec '\s Q:Qid '\s QIL1]
        fi
      if
	  P1:ResultPair? := metaParse(upModule('NAT, false), Q:Qid, 'Nat) /\
	  P2:ResultPair? := metaParse(upModule('AMN-GRAMMAR, false), QIL1,
	    'SubstitutionDecl) .

    crl [com-error] : [Q:Qid QIL, < idle ; M:Machine ; QIL' > , QIL''] =>
        [nil, < idle ; M:Machine ; nil > ,
	  'BMaude: '\r 'Error 'no 'such 'command '\o Q:Qid QIL]
      if (Q:Qid =/= 'MACHINE) /\ (Q:Qid =/= 'show) /\
	  (Q:Qid =/= 'search) /\ (Q:Qid =/= 'exec) /\ (Q:Qid =/= 'execn) /\
	  (Q:Qid =/= 'sexec) /\ (Q:Qid =/= 'mc) .

    crl [out] : [nil, < idle ; M:Machine ; QIL' > , QIL''] =>
        [nil, < idle ; M:Machine ; nil > , QIL']
      if QIL' =/= nil .
endm

--- For internal debugging.
set trace off .
set trace condition off .
set trace substitution off .
set trace whole off .
set trace body off .
set trace builtin on .
set print conceal on .
--- From BPLC
print conceal abs prc if choice loop .