module test_mini_cecil_with_env_and_store.

import mini_cecil_abstract_syntax
	env store algebra_with_store mini_cecil_with_env_and_store.

type test	int -> value -> o. % tests that sould succeed
type failtest	int -> value -> o. % tests that should fail (\Prolog says no)

test 1 V :-
	(evalExpr (intLiteral 3) H Store V Store).

test 2 V :-
	(evalExpr true H Store V Store).

test 3 V :-
	(evalExpr false H Store V Store).

test 4 V :-
	(evalExpr (msgExpr "theVoid" nil) H Store V Store).

test 5 V :-
	(evalExpr (msgExpr "and" (true::false::nil)) H Store V Store).

test 6 V :-
	(evalExpr
	 (msgExpr "add" ((msgExpr "1" nil)::(intLiteral 4)::nil))
		H Store V Store).

test 7 V :-
	empty_store Empty_Store,
	(alloc (varType (ty "Int")) (inInteger 541) Empty_Store L Store),
	(evalExpr (varExpr "x")
		(bind "x" (inValue (inLocation L)))
		Store V Store).

% an environment and store to use for tests...

type a_state	(environ string bindable) -> (store value) -> o.
a_state	TheEnv TheStore :-
	empty_store Empty_Store,
	(alloc (varType (ty "Int")) (inInteger 541) Empty_Store Li Store1),
	(alloc (varType (ty "Int")) (inInteger 227) Store1 Ln Store2),
	(alloc (varType (ty "Bool")) (inTruthValue tt) Store2 Lb Store3),
	TheStore = Store3,
	TheEnv =
	(overlay (bind "i" (inValue (inLocation Li)))
	(overlay (bind "n" (inValue (inLocation Ln)))
	(overlay (bind "b" (inValue (inLocation Lb)))
	(overlay (bind "inc"
		  (inProcedureClosure
			(makeProcClosure
				empty_environ
				((varDecl "y" (ty "Int"))::nil)
				(body
				  (seqStmt nil)
				  (return (msgExpr "add"
					    ((varExpr "y")::
					     (intLiteral 1)::nil)))))))
	empty_environ)))).

test 8 V :-
	a_state H Store,
	(evalExpr (msgExpr "add"
				((msgExpr "1" nil)::
				 (msgExpr "mult" ((varExpr "i")::
						  (varExpr "n")::nil))::
				 nil))
		    H Store V Store').

test 9 V :-
	a_state H Store,
	(evalExpr (procCallExpr "inc" ((varExpr "i")::nil)) H Store V Store').

test 10 V :-
	a_state H Store,
	(evalBody (body (assignStmt "i"
			 (msgExpr "add" ((varExpr "i")::
					 (intLiteral 1)::
					 nil)))
			(return (varExpr "i")))
			H Store V Store').

test 11 V :-
	a_state H Store,
	(evalExpr (varExpr "i") H Store V Store).

test 12 V :-
	a_state H Store,
	(evalResultExpr (return (msgExpr "add" ((varExpr "i")::
						(intLiteral 1)::nil)))
		H Store V Store').

type a_program	int -> program -> o.
a_program 1 (programDecl nil nil nil
	     (mainDecl
		((varDecl "i" (ty "Int"))::
			(varDecl "n" (ty "Int"))::
			(varDecl "b" (ty "Bool"))::nil)
		(seqStmt
		  ((assignStmt "i" (intLiteral 541))::
		   (assignStmt "n" (intLiteral 227))::
		   (assignStmt "b" true)::nil))
		((varDecl "y" (ty "Int"))::nil)
		(seqStmt
		  ((assignStmt "y" (varExpr "i"))::nil)
		))).

test 13 V :-
	a_program 1 P,
	(runProgram P H Store),
        (evalExpr (varExpr "i") H Store V Store).

test 14 V :-
	a_program 1 P,
	(runProgram P H Store),
        (evalExpr (varExpr "y") H Store V Store).

failtest 1 V :-  % should fail
	(evalExpr (varExpr "x") empty_environ Store V Store').

failtest 2 V :-
	a_state H Store,
	(evalExpr (varExpr "x") H Store V Store).


type observe	int -> (environ string bindable) -> (store value) -> o.

observe 1 H Store :-
	a_program 1 P,
	(runProgram P H Store).


a_program 2 (programDecl nil nil
	     ((procedureDecl "inc" ((varDecl "y" (ty "Int"))::nil) (ty "Int")
		(body
		  (seqStmt nil)
		  (return (msgExpr "add"
			    ((varExpr "y")::
			     (intLiteral 1)::nil)))))::
	      nil)
	     (mainDecl
		((varDecl "i" (ty "Int"))::
			(varDecl "n" (ty "Int"))::
			(varDecl "b" (ty "Bool"))::nil)
		(seqStmt
		  ((assignStmt "i" (intLiteral 541))::
		   (assignStmt "n" (intLiteral 227))::
		   (assignStmt "b" true)::nil))
		((varDecl "y" (ty "Int"))::nil)
		(seqStmt
		  ((assignStmt "y" (procCallExpr "inc" ((varExpr "i")::nil)))
	           ::nil))
	      )).

observe 2 H Store :-
	a_program 2 P,
	(runProgram P H Store).