*** equational-bc.maude

**** modular equational specification of the bc language
**** developed by C. Braga and J. Meseguer, May-Oct. 2003.

fmod RECORD is 
 sorts Index Component Field PreRecord Record .
 subsort Field < PreRecord .

 op null : -> PreRecord [ctor] .
 op _,_ : PreRecord PreRecord -> PreRecord [ctor assoc comm id: null] .
 op _:_ : [Index] [Component] -> [Field] [ctor] .
 op {_} : [PreRecord] -> [Record] [ctor] .
 op duplicated : [PreRecord] -> [Bool] .

 var I : Index . vars C C' : Component . var PR : PreRecord .

 eq duplicated((I : C),(I : C'), PR) = true .
 cmb {PR} : Record if duplicated(PR) =/= true .

 op _-_ : PreRecord Index -> PreRecord .
 eq ((I:Index : C:Component) , PR:PreRecord) - I:Index = PR:PreRecord .
 eq PR:PreRecord - I:Index = PR:PreRecord [owise] .
endfm

fmod CONF is
 inc RECORD .
 sorts Program Conf .
 var P : Program .  var R : Record .

 op <_,_> : Program Record -> Conf [ctor] .
endfm

fmod EMPTY-LIST is
 sort EmptyList .
 op nil : -> EmptyList [ctor] .
 op _,_ : EmptyList EmptyList -> EmptyList [prec 60 assoc id: nil] .
endfm

fmod VALUE is 
 sorts Value NzValue . 
 op no-value : -> [Value] . 

 op isTrue : Value -> Bool .
 op isEqualTo : Value Value -> Value .
 op lessThan : Value Value -> Value .    
 op greaterThan : Value Value -> Value . 
endfm

fmod VALUE-LIST is
  pr VALUE . 
  pr EMPTY-LIST .
  sort ValueList .
  subsorts Value  EmptyList < ValueList .
  op _,_ : ValueList ValueList -> ValueList [ctor ditto] . 
endfm

fmod VAR is 
 sorts SimpleVar ArrayVar Var . 
 subsorts SimpleVar ArrayVar < Var . 
endfm

fmod VAR-LIST is
  pr VAR . 
  pr EMPTY-LIST .
  sort SimpleVarList ArrayVarList VarList . 
  subsort Var < VarList .
  subsorts ArrayVar EmptyList < ArrayVarList < VarList . 
  subsorts SimpleVar EmptyList < SimpleVarList < VarList . 
  op _,_ : VarList VarList -> VarList [ctor ditto] .
  op _,_ : ArrayVarList ArrayVarList -> ArrayVarList [ctor ditto] .
  op _,_ : SimpleVarList SimpleVarList -> SimpleVarList [ctor ditto] .
endfm

fmod EXPR-SYNTAX is
 ex VALUE-LIST .
 ex VAR-LIST .
 pr RAT .
 sorts Expr ExprList .
 subsort Rat < Value .
 subsort NzRat < NzValue .
 subsorts NzValue Value < Expr .
 subsort Var < Expr .
 subsort Expr < ExprList .
 subsort ValueList VarList < ExprList .

 op _,_ : ExprList ExprList -> ExprList [ctor ditto] .

 op _[_] : SimpleVar ExprList -> ArrayVar [ctor] .

 --- Boolean operations
 op _<_ : Expr Expr -> Expr .
 op _>_ : Expr Expr -> Expr .
 ops _==_ : Expr Expr -> Expr .

 --- Arithmetic operations
 op _+_ : Expr Expr -> Expr [ditto] .
 op _-_ : Expr Expr -> Expr [ditto] .
 op _*_ : Expr Expr -> Expr [ditto] .
 op _/_ : Expr Expr -> Expr [ditto] .
 op _%_ : Expr Expr -> Expr .
endfm

--- The LOCATION module is an abstract interface for memory locations.

fmod LOCATION is
 sort Loc .
endfm

--- BASIC-ENVIRONMENT is an abstract interface for environment 
--- components.

fmod BASIC-ENVIRONMENT is
 ex RECORD .
 pr VAR .
 pr VALUE .
 inc LOCATION .

 sorts Env BVal .
 subsort Env < Component .
 subsort BVal < Value .

 op env : -> Index [ctor] .

 op newLoc : Env -> Loc .
 op find : Env Var -> [BVal] .
 op override : Env Var BVal -> Env .

 mb env : E:Env : Field .
endfm

--- STORE is an abstract interface for memory components.

fmod STORE is
 ex RECORD .
 pr VALUE .
 inc LOCATION .

 sorts Store SVal .
 subsort Store < Component .
 subsort SVal < Value .

 op st : -> Index [ctor] .
 op lookup : Store Loc -> [SVal] .
 op update : Store Loc SVal -> Store .

 mb st : S:Store : Field .
endfm

fmod ENV-STORE is
 inc BASIC-ENVIRONMENT .
 inc STORE .

 sort EnvStore .
 op <_,_> : Env Store -> EnvStore .
 op lookup-env-st : Env Store Var -> Value .
 op update-env-st : Env Store Var Value -> EnvStore .
endfm

fmod EXPR-SEMANTICS is
 ex EXPR-SYNTAX .
 ex CONF .
 inc ENV-STORE .

 subsort Expr < Program .
 subsort Loc < BVal .
 subsort Rat < SVal .

 *** The rem function is used to give the semantics for the _%_ operation.
 *** It should be lifted to Value so that extensions may overload it.
 op _rem_ : Value Value -> Value [ditto] .

 --- Evaluation of ExprList (needed for evaluating Array Variables).

 sort EvalResult .
 op er : ValueList Record -> EvalResult [ctor] .
 op eval : ExprList Record -> EvalResult .

 eq eval(nil,R:Record) = er(nil,R:Record) .
 ceq eval((E:Expr,EL:ExprList),R:Record) =
     er((V:Value,VL:ValueList),R'':Record) 
  if < V:Value , R':Record > := < E:Expr , R:Record > /\
     er(VL:ValueList,R'':Record) := eval(EL:ExprList,R':Record) .

 --- Simple variables.

 eq  < SV:SimpleVar,{(env : E:Env),(st : S:Store),PR:PreRecord} > =
     < lookup-env-st(E:Env, S:Store, SV:SimpleVar),{(env : E:Env),
						(st : S:Store),PR:PreRecord} > .

 --- Array Variables.
 --- op _[_] : SimpleVar Expr -> ArrayVar .

 ceq < SV:SimpleVar[EL:ExprList],{(env : E:Env),(st : S:Store), 
							PR:PreRecord} > =
     < lookup-env-st(E:Env,S:Store,SV:SimpleVar[VL:ValueList]),{(env : E:Env),
					       (st : S:Store),PR':PreRecord} > 
  if er(VL:ValueList,{(env : E:Env),(st : S':Store),PR':PreRecord}) :=
     eval(EL:ExprList,{(env : E:Env),(st : S:Store),PR:PreRecord}) .

 --- op _==_ : Expr Expr -> Expr .

 ceq < E1:Expr == E2:Expr,R:Record > =
     < isEqualTo(V1:Value,V2:Value),R'':Record >
  if < V1:Value,R':Record > := < E1:Expr,R:Record > /\
     < V2:Value,R'':Record > := < E2:Expr,R':Record > .

 --- op _+_ : Expr Expr -> Expr .

 ceq < E1:Expr + E2:Expr,R:Record > = < V1:Value + V2:Value,R'':Record > 
  if < V1:Value,R':Record > := < E1:Expr,R:Record > /\
     < V2:Value,R'':Record > := < E2:Expr,R':Record > .

 --- op _*_ : Expr Expr -> Expr .

 ceq < E1:Expr * E2:Expr,R:Record > = < V1:Value * V2:Value,R'':Record > 
  if < V1:Value,R':Record > := < E1:Expr,R:Record > /\
     < V2:Value , R'':Record > := < E2:Expr,R':Record > .

 --- op _-_ : Expr Expr -> Expr .

 ceq < E1:Expr - E2:Expr , R:Record > = < V1:Value - V2:Value , R'':Record > 
  if < V1:Value , R':Record > := < E1:Expr , R:Record > /\
     < V2:Value , R'':Record > := < E2:Expr , R':Record > .
  
 --- op _/_ : Expr Expr -> Expr .

 ceq < E1:Expr / E2:Expr , R:Record > = < V1:Value / V2:NzValue , R'':Record > 
  if < V1:Value , R':Record > := < E1:Expr , R:Record > /\
     < V2:NzValue , R'':Record > := < E2:Expr , R':Record > .

 --- op _%_ : Expr Expr -> Expr .

 ceq < E1:Expr % E2:Expr , R:Record > = < V1:Value rem V2:NzValue , 
								R'':Record > 
  if < V1:Value , R':Record > := < E1:Expr , R:Record > /\
     < V2:NzValue , R'':Record > := < E2:Expr , R':Record > .
 
 --- op _<_ : Expr Expr -> Expr .

 ceq < E1:Expr < E2:Expr , R:Record > = < lessThan(V1:Value,V2:Value) , 
								R'':Record > 
  if < V1:Value , R':Record > := < E1:Expr , R:Record > /\
     < V2:Value , R'':Record > := < E2:Expr , R':Record > .

 --- op _>_ : Expr Expr -> Expr .

 ceq < E1:Expr > E2:Expr , R:Record > = < greaterThan(V1:Value,V2:Value),
								R'':Record > 
  if < V1:Value , R':Record > := < E1:Expr , R:Record > /\
     < V2:Value , R'':Record > := < E2:Expr , R':Record > .
endfm

fmod STMT-SYNTAX is
 pr EXPR-SYNTAX .
 
 sorts Comp CtrlStmt AssignStmt Stmt Block .
 subsort CtrlStmt AssignStmt < Stmt .
 subsort Expr Stmt < Block .
 subsort Value < Comp < Block .

 op skip : -> Comp [ctor] .
 op _=_ : Var Expr -> AssignStmt [ctor prec 62] .
 op while(_)_ : Expr Block -> CtrlStmt [ctor prec 62] .
 op if(_)_ : Expr Block -> CtrlStmt [prec 62] .
 op if(_)_else_ : Expr Block Block -> CtrlStmt [ctor prec 62] .
 op for(_;_;_)_ : Stmt Expr Stmt Block -> CtrlStmt [prec 62] .
 op return_ : Expr -> CtrlStmt [ctor prec 62] . 
 op {} : -> Block .
 op {_} : Block -> Block .
 op _;_ : Block Block -> Block [ctor assoc prec 95] .
 op _;  : Block -> Block [prec 93] .

--- desugaring of abbreviated statement syntax

 eq {} = skip .
 eq { B:Block } = B:Block .
 eq B:Block ; = B:Block .
 eq skip ; B:Block = B:Block .
 eq if ( E:Expr ) B:Block = if ( E:Expr ) B:Block else skip .
 eq for (ST:Stmt ; E:Expr ; ST':Stmt ) BL:Block =
    (ST:Stmt ; while ( E:Expr ) (BL:Block ; ST':Stmt).Block) . 
endfm

fmod STMT-SEMANTICS is
 ex STMT-SYNTAX .
 ex EXPR-SEMANTICS .

 subsort Block < Program .

 --- Assignment 

 ceq < SV:SimpleVar = E:Expr ; B:Block , {(env : E:Env),(st : S:Store),
							PR:PreRecord} > =
     < C:Comp , {(env : E:Env),(st : S''':Store),PR'':PreRecord} >
  if < SV:SVal, {(env : E:Env),(st : S':Store),PR':PreRecord} > := 
     < E:Expr , {(env : E:Env),(st : S:Store),PR:PreRecord } > /\
     < E':Env , S'':Store > := 
	update-env-st(E:Env, S':Store, SV:SimpleVar, SV:SVal) /\
     < C:Comp, {(env : E':Env),(st : S''':Store),PR'':PreRecord} > :=
     < B:Block , {(env : E':Env),(st : S'':Store),PR':PreRecord} > .

 ceq < SV:SimpleVar[EL:ExprList] = E:Expr ; B:Block , 
       {(env : E:Env),(st : S:Store),PR:PreRecord} > =
     < C:Comp , {(env : E:Env),(st : N:Store),PR''':PreRecord} >
  if er(VL:ValueList, {(env : E:Env),(st : S':Store),PR':PreRecord}) :=
     eval(EL:ExprList, {(env : E:Env),(st : S:Store),PR:PreRecord }) /\
     < SV:SVal, {(env : E:Env),(st : S'':Store),PR'':PreRecord} > :=
     < E:Expr , {(env : E:Env),(st : S':Store),PR':PreRecord } > /\
     < E':Env, S''':Store > := 
         update-env-st(E:Env, S'':Store, SV:SimpleVar[VL:ValueList],SV:SVal) /\ 
     < C:Comp, {(env : E':Env),(st : N:Store),PR''':PreRecord} > := 
     < B:Block , {(env : E':Env),(st : S''':Store),PR'':PreRecord} > .

 --- op _;_ : Block Block -> Block [ctor assoc prec 95] .

 ceq < CS:CtrlStmt ; B:Block , R:Record > = < C2:Comp , R'':Record > 
  if < C1:Comp , R':Record > := < CS:CtrlStmt , R:Record > /\
     < C2:Comp, R'':Record > := < B:Block, R':Record > .
	
 --- op if(_)_else_ : Expr Block Block -> CtrlStmt [ctor prec 62] .

 ceq < if ( E:Expr ) B1:Block else B2:Block , R:Record > =
     < if isTrue(Vl:Value) then B1:Block else B2:Block fi , R':Record >
  if < Vl:Value , R':Record > := < E:Expr , R:Record > .

 --- op while(_)_ : Expr Block -> CtrlStmt [ctor prec 62] .

 ceq < while(E:Expr) BL:Block , R:Record > =
     < if isTrue(VL:Value) then BL:Block ; 
       while(E:Expr) BL:Block else skip fi ,
       R':Record > 
  if < VL:Value , R':Record > := < E:Expr , R:Record > .

 ---  op return_ : Expr -> CtrlStmt [ctor prec 62] . 

 ceq < return E:Expr , R:Record > = < VL:Value , R':Record > 
  if < VL:Value , R':Record > := < E:Expr , R:Record > .
endfm

fmod FUN-DECL-SYNTAX is
 ex STMT-SYNTAX .
 pr VAR-LIST .

 subsort SimpleVarList < ExprList .

 --- function definition

  op define_(){} : SimpleVar -> Stmt [prec 62] .
  op define_(){_} : SimpleVar Block -> Stmt [prec 62] .
  op define_(){auto_;} : SimpleVar SimpleVarList -> Stmt [prec 62] .
  op define_(){auto_;_} : SimpleVar SimpleVarList Block -> Stmt [prec 62] .
  op define_(_){} : SimpleVar SimpleVarList -> Stmt [prec 62] .
  op define_(_){_} : SimpleVar SimpleVarList Block -> Stmt [prec 62] .
  op define_(_){auto_;_} : SimpleVar SimpleVarList SimpleVarList 
						Block -> Stmt [ctor prec 62] .

 --- desugaring of abbreviated function definitions

 eq define F:SimpleVar (){} =
    define F:SimpleVar (nil){auto nil ; skip} .
 eq define F:SimpleVar (){ B:Block} =
    define F:SimpleVar (nil){auto nil ; B:Block} .
 eq define F:SimpleVar (){auto A:SimpleVarList ;} =
    define F:SimpleVar (nil){auto A:SimpleVarList ; skip} .
 eq define F:SimpleVar (){auto A:SimpleVarList ; B:Block} =
    define F:SimpleVar (nil){auto A:SimpleVarList ; B:Block} .
 eq define F:SimpleVar (P:SimpleVarList){ } =
    define F:SimpleVar (P:SimpleVarList){auto nil ; skip} .
 eq define F:SimpleVar (P:SimpleVarList){B:Block} =
    define F:SimpleVar (P:SimpleVarList){auto nil ; B:Block} .
endfm

fmod FUN-DECL-SEMANTICS is
 ex FUN-DECL-SYNTAX .
 ex STMT-SEMANTICS .

 sort Lambda .
 subsort Lambda < BVal .
 op lambda(_;_;_) : SimpleVarList VarList Block -> Lambda .

 ceq < define F:SimpleVar(P:SimpleVarList){auto A:VarList ; B:Block } ; 
								Q:Block , 
       { (env : E:Env), PR:PreRecord } > =
     < C:Comp , {(env : E:Env), PR':PreRecord } >
  if E':Env := override(E:Env, F:SimpleVar,
                        lambda(P:SimpleVarList ; A:VarList ; B:Block)) /\
     < C:Comp , {(env : E':Env),PR':PreRecord } > := 
     < Q:Block , {(env : E':Env),PR:PreRecord } > .
endfm

fmod FUN-CALL-SYNTAX is
 ex FUN-DECL-SYNTAX .

 op _() : SimpleVar -> Expr [prec 10] .
 op _(_) : SimpleVar ExprList -> Expr [ctor prec 10] .	

 eq F:SimpleVar() = F:SimpleVar(nil) .
endfm

fmod EXT-ENVIRONMENT is
 inc VAR-LIST .
 inc VALUE-LIST .
 inc ENV-STORE .

 op makeActualParams : Env Store SimpleVarList ValueList -> EnvStore .
 op initAutoVars : Env Store VarList -> EnvStore .
endfm

fmod FUN-CALL-SEMANTICS is
 ex FUN-DECL-SEMANTICS .
 ex FUN-CALL-SYNTAX .
 inc EXT-ENVIRONMENT .

 ceq < F:SimpleVar ( EL:ExprList ), {(env : E:Env),(st : S:Store),
							PR:PreRecord} > =
     < C:Comp , {(env : E:Env), (st : N':Store),(PR'':PreRecord)} >
  if er(VL:ValueList, {(env : E:Env),(st : S':Store),PR':PreRecord}) := 
     eval(EL:ExprList, {(env : E:Env),(st : S:Store),PR:PreRecord}) /\
     lambda(P:SimpleVarList ; A:VarList ; B:Block) := 
		find(E:Env, F:SimpleVar) /\
     < E':Env, S'':Store > := 
	makeActualParams(E:Env, S':Store, P:SimpleVarList, VL:ValueList) /\
     < E'':Env, N:Store > := initAutoVars(E':Env, S'':Store, A:VarList) /\
     < C:Comp , {(env : E'':Env),(st : N':Store),PR'':PreRecord} > := 
     < B:Block, {(env : E'':Env),(st : N:Store),PR':PreRecord} > . 
endfm

fmod BC-LOCATION is
 inc LOCATION .
 pr NAT .

 op loc : Nat -> Loc [ctor] .
endfm

fmod LOC-LIST is
 inc LOCATION .
 pr VALUE-LIST .
 sort LocList .
 subsort Loc EmptyList < LocList < ValueList .
 op _,_ : LocList LocList -> LocList [ctor ditto] .
endfm

fmod BC-STORE is
 inc STORE .
 pr BC-LOCATION .
 pr LOC-LIST .
 pr RAT .

 sort Cell CStore .
 subsort Cell < CStore .
 subsort Rat < SVal .

 op mt-st : -> CStore [ctor] .
 op [[_,_]] : Loc SVal -> Cell [ctor] .
 op __ : CStore CStore -> CStore [ctor assoc comm id: mt-st] .
 op _[_|->_] : CStore Loc SVal -> CStore .
 op _(_) : CStore Loc -> SVal .
 op <_> : [CStore] -> [Store] .
 op dupl : [CStore] -> [Bool] .

 eq dupl([[ L:Loc,SV:SVal ]] [[ L:Loc,SV1:SVal ]] CS:CStore) = true .
 cmb < CS:CStore > : Store if dupl(CS:CStore) =/= true .  

 eq lookup(< CS:CStore >, L:[Loc]) = CS:CStore ( L:[Loc] ) .
 eq update(< CS:CStore >, L:Loc, SV:SVal) = 
	< CS:CStore [ L:Loc |-> SV:SVal ] > . 

 eq ([[ L:Loc,SV:SVal ]] CS:CStore)(L:Loc) = SV:SVal .
 eq CS:CStore ( L:Loc ) = 0 [owise] .

 eq ([[ L:Loc , SV:SVal ]] CS:CStore)[ L:Loc |-> SV':SVal ] = 
        ([[ L:Loc , SV':SVal ]] CS:CStore)  .
 eq CS:CStore [ L:Loc |-> SV':SVal ] = 
	[[ L:Loc , SV':SVal ]] CS:CStore [owise] .
endfm

fmod BC-BASIC-ENVIRONMENT is
 inc BASIC-ENVIRONMENT .
 pr BC-LOCATION .

 sort Bind CEnv .
 subsort Bind < CEnv .
 subsort Nat Loc < BVal .

 op mt-env : -> CEnv [ctor] .
 op [_,_] : Var BVal -> Bind [ctor] .
 op __ : CEnv CEnv -> CEnv [ctor assoc comm id: mt-env] .
 op <_> : [CEnv] -> [Env] . 
 op dupl : [CEnv] -> [Bool] .
 op newLocAux : Env Nat -> Loc .

 eq dupl([V:Var,BV:BVal] [V:Var,BV1:BVal] CE:CEnv) = true .
 cmb < CE:CEnv > : Env if dupl(CE:CEnv) =/= true .  

 eq newLoc(E:Env) = newLocAux(E:Env, 0) .
 ceq newLocAux(< CE:CEnv [V:Var,loc(N:Nat)] >, M:Nat) =
     newLocAux(< CE:CEnv >, N:Nat) if N:Nat > M:Nat .
 eq newLocAux(E:Env,M:Nat) = loc(s(M:Nat)) [owise] .

 eq find(< [V:Var, BV:BVal] CE:CEnv >,V:Var) = BV:BVal .
 eq find(E:Env,V:Var) = no-value [owise] .

 eq override(< [V:Var,BV:BVal] CE:CEnv >,V:Var,BV':BVal) = 
    < [V:Var,BV':BVal] CE:CEnv > .
 eq override(< CE:CEnv >, V:Var, BV':BVal) = 
    < [V:Var, BV':BVal] CE:CEnv > [owise] .
endfm

fmod BC-ENV-STORE is
 pr BC-BASIC-ENVIRONMENT .
 pr BC-STORE .
 inc ENV-STORE .

 eq lookup-env-st(< [ V:Var, L:Loc ] CE:CEnv > , 
    < [[ L:Loc, Vl:Value ]] CS:CStore > , V:Var) = Vl:Value .
 eq lookup-env-st(E:Env, M:Store, V:Var) = 0 [owise] .

 eq update-env-st(< [ V:Var, L:Loc ] CE:CEnv > , 
    < [[ L:Loc, Vl:Value ]] CS:CStore > , V:Var, Vl':Value) = 
    < < [ V:Var, L:Loc ] CE:CEnv > , < [[ L:Loc, Vl':Value ]] CS:CStore > > .
 eq update-env-st(< CE:CEnv > , < CS:CStore > , V:Var, Vl:Value) = 
    < < [ V:Var, newLoc(< CE:CEnv >) ] CE:CEnv > , 
      < [[ newLoc(< CE:CEnv >), Vl:Value ]] CS:CStore > > [owise] .
endfm

fmod BC-EXT-ENVIRONMENT is
 inc EXT-ENVIRONMENT .
 inc ENV-STORE .
 pr BC-BASIC-ENVIRONMENT .
 pr BC-STORE .

 eq makeActualParams(< CE:CEnv > , < CS:CStore > , nil, nil) =  
    < < CE:CEnv > , < CS:CStore > > .
 ceq makeActualParams(< CE:CEnv > , < CS:CStore > , 
	(SV:SimpleVar, SL:SimpleVarList), (V:Value, VL:ValueList)) = 
     makeActualParams(< CE':CEnv > , < CS':CStore > , 
	SL:SimpleVarList, VL:ValueList) 
  if < CE':CEnv > := override(< CE:CEnv >,SV:SimpleVar,newLoc(< CE:CEnv >)) /\
     < CS':CStore > := update(< CS:CStore >,newLoc(< CE:CEnv >), V:Value) .

 eq initAutoVars( < CE:CEnv > , < CS:CStore > , nil) = 
	< < CE:CEnv > , < CS:CStore > > .
 ceq initAutoVars( < CE:CEnv > , < CS:CStore > , (V:Var, VL:VarList)) = 
     	initAutoVars(< CE':CEnv > , < CS':CStore > , VL:VarList) 
  if < CE':CEnv > := override(< CE:CEnv >,V:Var,newLoc(< CE:CEnv >)) /\
     < CS':CStore > := update(< CS:CStore >,newLoc(< CE:CEnv >), 0) .
endfm


fmod BC-VALUE is
 inc VALUE .
 pr RAT .
 subsort Rat < Value .
 subsort NzRat < NzValue .

 eq isTrue(R:Rat) = (R:Rat == 1) .
 eq isEqualTo(R1:Rat, R2:Rat) = if (R1:Rat == R2:Rat) then 1 else 0 fi .
 eq greaterThan(R1:Rat,R2:Rat) = if R1:Rat > R2:Rat then 1 else 0 fi .
 eq lessThan(R1:Rat,R2:Rat) = if R1:Rat < R2:Rat then 1 else 0 fi .
endfm

fmod SHOW-INTERFACE is
 pr VALUE .
 op show : Value -> Value .
endfm

fmod PRINT is
 pr VALUE-LIST .
 ex FUN-CALL-SEMANTICS .
 inc SHOW-INTERFACE .
 
 subsort ValueList < Component .
 op output : -> Index .

 mb output : VL:ValueList : Field .

 op print : Expr -> Expr .

 ceq < print(E:Expr) , { (output : VL:ValueList) , PR:PreRecord } > =
     < skip , { (output : (VL':ValueList , show(V:Value))), PR':PreRecord } >
  if < V:Value , { (output : VL':ValueList) , PR':PreRecord } > := 
     < E:Expr , { (output : VL:ValueList) , PR:PreRecord } > .

 eq show(R:Rat) = R:Rat .
endfm

fmod BC is
 pr BC-ENV-STORE .
 pr BC-EXT-ENVIRONMENT .
 pr FUN-CALL-SEMANTICS .
 pr BC-VALUE .
 pr PRINT .
 pr QID .
 subsort Qid < SimpleVar .
endfm

fmod TEST is
 ex BC .

 op init : -> Record .
 eq init = { (env : < mt-env >) , (st : < mt-st >) , output : nil } .
endfm


red < define 'f('x){
        if ('x == 0) { return 1 ; } 
        else { return('x * 'f('x - 1)) ; } 
      } ;
      'f(20) , init > . 

--- p01
red < print('x + 'y) , init > .

--- p02
red < print('x + 1) , init > .

--- p03
red < 'y = 10 ; 'x = 10 ; print('x + 'y)  , init > .

--- p05
red < 'x = 10 ; 'y = 'x ; print('x + 'y) , init > .

--- p06
*** The syntax needs some polishing still...
red < 'x = 1732 ; *** 17324322343254731 ; 
                  *** This number breaks Maude my iBook: illegal instruction.
      'n = 0 ; 
      while ( 'x > 1 ) {
            if ('x % 2) { ('x = (3 * 'x + 1)) ; skip } 
            else { ('x = 'x / 2) ; skip } ;
            'n = 'n + 1 ;
      } ; print('n) , 
      init > .

--- p07
red < 'd = 40 ; 's = 10 ; 't = 5 ; 
      'd' = 'd ; 
      'd = 's * 't ; 
      if ('d > 'd') 1 else 0 , init > .

--- p09 

red < 'x = 10 ; 'y = 5 ; 
      define 'succ('x) { 
        return('x + 1) ;
      } ; 
      if ('x < 'succ('x)) print(1) else print(0) ;
      if ('y < 'succ('y)) print(1) else print(0) , init > .
      

--- p10

red < 'x = 10 ; 'y = 5 ;
      define 'square('x) {
        return('x * 'x) ;
      } ;
      'x = 2 * 'x * 'x + 'square('x) ;
      'y = 2 * 'y * 'y + 'square('y) ;
      print('x + 'y) , init > .

--- p12

red < 'x = 10 ; 'z = 'x ;
      define 'f('y) {
	auto 'x ;
        ('x = 5 ;
        return('x + 'y) ;)
      } ;
      'f('z) , init > .