babelsberg.rml

(* file assignment.rml *)

module babelsberg:
  (* Abstract syntax for the BabelsbergP language *)

  datatype Program = PROGRAM of Statement

  datatype Statement = SKIP
                     | ASSIGN of Variable * Exp
                     | ALWAYS of Constraint
		     | ONCE of Constraint
                     | SEQ of Statement * Statement
		     | IF of Exp * Statement * Statement
		     | WHILE of Exp * Statement

  datatype Constraint = CONSTRAINT of Rho * Exp
		      | COMPOUNDCONSTRAINT of Constraint * Constraint

  datatype Rho = WEAK | MEDIUM | REQUIRED

  datatype Exp = VALUE of Value
	       | VARIABLE of Variable
	       | OP of Exp * Op * Exp

  datatype Constant = REAL of real | TRUE | FALSE | NIL | STRING of string

  type Variable = string

  datatype Op =  ADD | SUB | MUL | DIV | LESSTHAN | LEQUAL | EQUAL | NEQUAL | GEQUAL | GREATERTHAN | AND | OR

(* Values stored in environments *)
  type Value   = Constant

(* Bindings and environments *)
type VarBnd      = (Variable * Value)
type Env         = VarBnd list
type Cstore      = Constraint

relation evalprogram: Program => ()
end

relation evalprogram: Program => () =
  rule	print "starting to evaluate\n" &
	step([], CONSTRAINT(REQUIRED, VALUE(TRUE)), statement) => (Env, Cstore)
	-------------------------------------
	evalprogram(PROGRAM(statement))
end

relation eval: (Env, Exp) => Value =
  axiom eval(_, VALUE(c)) => c
	
  rule	print "E-Var\n" &
	Util.lookupEnv(Env, x) => v
	----------------------
	eval(Env, VARIABLE(x)) => v

  rule	eval(Env, e1) => v1 &
	Util.should_short_circuit(op,v1) => (true, v) &
	print "E-Op (short circuit)\n"
	------------------------------
	eval(Env, OP(e1, op, e2)) => v

  rule	print "E-Op\n" &
	eval(Env, e1) => v1 &
	eval(Env, e2) => v2 &
	Util.apply_binop(op,v1,v2) => v
	------------------------------
	eval(Env, OP(e1, op, e2)) => v
end

relation models: Constraint => Env =
  rule	Print.printC(C) => Cstring &
	Solver.solve(Cstring) => Esolution &
	Print.parseEnvironment(Esolution, []) => E &
	print "\n"
	------------------------------
	models(C) => E
end

relation stayEnv: (Env, Rho) => Constraint =
  axiom stayEnv([], rho) => CONSTRAINT(REQUIRED, VALUE(TRUE))

  rule	print "StayEnv\n" &
	stayEnv(E0, rho) => C0 &
	stay(OP(VARIABLE(x), EQUAL, VALUE(v)), rho) => C1
	-------------------------------------------------
	stayEnv((x, v) :: E0, rho) => COMPOUNDCONSTRAINT(C0, C1)
end

relation stay: (Exp, Rho) => Constraint =
  axiom	stay(OP(VARIABLE(x), EQUAL, VALUE(v)), rho) => CONSTRAINT(WEAK, OP(VARIABLE(x), EQUAL, VALUE(v)))
end

relation step: (Env, Cstore, Statement) => (Env, Cstore) =
  rule	print "S-Asgn\n" &
	eval(Env,e) => v &
	stayEnv(Env, WEAK) => Cs &
	models(COMPOUNDCONSTRAINT(COMPOUNDCONSTRAINT(Cstore, Cs),
				  CONSTRAINT(REQUIRED, OP(VARIABLE(x), EQUAL, VALUE(v))))) => Env'
	-----------------------------------------------------------------------------------------------
	step(Env, Cstore, ASSIGN(x, e)) => (Env', Cstore)

  rule	print "S-Once\n" &
	stayEnv(Env, WEAK) => Cs &
	models(COMPOUNDCONSTRAINT(COMPOUNDCONSTRAINT(Cstore, Cs), C0)) => Env'
	----------------------------------------------------------------------
	step(Env, Cstore, ONCE(C0)) => (Env', Cstore)

  rule	print "S-Always\n" &
	step(Env, Cstore, ONCE(C0)) => (Env', Cstore)
	---------------------------------------------
	step(Env, Cstore, ALWAYS(C0)) => (Env', COMPOUNDCONSTRAINT(Cstore, C0))

  axiom step(Env, Cstore, SKIP) => (Env, Cstore)

  rule	print "S-SeqStep\n" &
	step(Env, Cstore, s1) => (Env', Cstore') &
	step(Env', Cstore', s2) => (Env'', Cstore'')
	--------------------------------------------------
	step(Env, Cstore, SEQ(s1, s2)) => (Env'', Cstore'')

  rule	eval(Env, e) => TRUE &
	print "S-IfThen\n" &
	step(Env, Cstore, s1) => (Env', Cstore')
	----------------------------------------
	step(Env, Cstore, IF(e, s1, s2)) => (Env', Cstore')

  rule	eval(Env, e) => v &
	not v = TRUE &
	print "S-IfElse\n" &
	step(Env, Cstore, s2) => (Env', Cstore')
	----------------------------------------
	step(Env, Cstore, IF(e, s1, s2)) => (Env', Cstore')

  rule	eval(Env, e) => TRUE &
	print "S-WhileDo\n" &
	step(Env, Cstore, s) => (Env', Cstore') &
	step(Env', Cstore', WHILE(e, s)) => (Env'', Cstore'')
	-----------------------------------------------------
	step(Env, Cstore, WHILE(e, s)) => (Env'', Cstore'')

  rule	eval(Env, e) => v &
	not v = TRUE &
	print "S-WhileSkip\n"
	-----------------------------------------------------
	step(Env, Cstore, WHILE(e, s)) => (Env, Cstore)
end

with "solver.rml"
with "printer.rml"
with "helper.rml"