module test_mini_cecil_semantics.

import mini_cecil_abstract_syntax
	env store algebra_with_store mini_cecil_semantics.

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) algebraVIS H Store V Store).

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

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

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

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

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

test 7 V :-
	empty_store Empty_Store,
	(alloc (varType (ty "Int")) (inInteger 541) Empty_Store L Store),
	(evalExpr (varExpr "x")
		algebraVIS
		(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))
		   algebraVIS H Store V Store').

test 9 V :-
	a_state H Store,
	(evalExpr (procCallExpr "inc" ((varExpr "i")::nil))
		 algebraVIS 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")))
			 algebraVIS H Store V Store').

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

test 12 V :-
	a_state H Store,
	(evalResultExpr (return (msgExpr "add" ((varExpr "i")::
						(intLiteral 1)::nil)))
		 algebraVIS 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") algebraVIS H Store V Store).

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

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

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


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

observe N H Store :-
	a_program N 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))
	      )).

a_program 3 (programDecl 
                ((classDecl "Cell" ((varDecl "i" (ty "Int"))::nil))::nil)
                ((methodDecl "change" 
                        ((methodFormalDecl "c" (ty "Cell"))::
                         (methodFormalDecl "v" (ty "Int"))::nil)
                   (ty "Void") 
                   (body (setFieldStmt "c" "i" (varExpr "v"))
                         (return (msgExpr "theVoid" nil))))::
                 (methodDecl "get" 
                        ((methodFormalDecl "c" (ty "Cell"))::nil)
                   (ty "Int") 
                   (body (exprStmt (msgExpr "theVoid" nil))
                         (return (getExpr (varExpr "c") "i"))))::nil)
                nil 
                (mainDecl ((varDecl "x"  (ty "Cell"))::
                                (varDecl "y" (ty "Cell"))::nil)
                    (seqStmt nil)
                   ((varDecl "Ans"  (ty "Int"))::nil)
                    (seqStmt nil))).


a_program 4 (programDecl 
                ((classDecl "Cell" ((varDecl "i" (ty "Int"))::nil))::nil)
                ((methodDecl "change" 
                        ((methodFormalDecl "c" (ty "Cell"))::
                         (methodFormalDecl "v" (ty "Int"))::nil)
                   (ty "Void") 
                   (body (setFieldStmt "c" "i" (varExpr "v"))
                         (return (msgExpr "theVoid" nil))))::
                 (methodDecl "get" 
                        ((methodFormalDecl "c" (ty "Cell"))::nil)
                   (ty "Int") 
                   (body (exprStmt (msgExpr "theVoid" nil))
                         (return (getExpr (varExpr "c") "i"))))::nil)
		nil
                (mainDecl ((varDecl "x"  (ty "Cell"))::
                                (varDecl "y" (ty "Cell"))::nil)
                    (seqStmt 
                      ((assignStmt "x" (newExpr  "Cell" ((intLiteral 4)::nil)))
                       ::(assignStmt "y" (varExpr "x"))::nil))
                   ((varDecl "Ans"  (ty "Int"))::nil)
                    (seqStmt nil))).

a_program 5 (programDecl 
                ((classDecl "Cell" ((varDecl "i" (ty "Int"))::nil))::nil)
                ((methodDecl "change" 
                        ((methodFormalDecl "c" (ty "Cell"))::
                         (methodFormalDecl "v" (ty "Int"))::nil)
                   (ty "Void") 
                   (body (setFieldStmt "c" "i" (varExpr "v"))
                         (return (msgExpr "theVoid" nil))))::
                 (methodDecl "get" 
                        ((methodFormalDecl "c" (ty "Cell"))::nil)
                   (ty "Int") 
                   (body (exprStmt (msgExpr "theVoid" nil))
                         (return (getExpr (varExpr "c") "i"))))::nil)
                nil 
                (mainDecl ((varDecl "x"  (ty "Cell"))::
                                (varDecl "y" (ty "Cell"))::nil)
                    (seqStmt 
                      ((assignStmt "x" (newExpr  "Cell" ((intLiteral 4)::nil)))
                       ::(assignStmt "y" (varExpr "x"))::nil))
                   ((varDecl "Ans"  (ty "Int"))::nil)
                    (assignStmt "Ans" (msgExpr "get" ((varExpr "y")::nil))))).

a_program 6 (programDecl 
                ((classDecl "Cell" ((varDecl "i" (ty "Int"))::nil))::nil)
                ((methodDecl "change" 
                        ((methodFormalDecl "c" (ty "Cell"))::
                         (methodFormalDecl "v" (ty "Int"))::nil)
                   (ty "Void") 
                   (body (setFieldStmt "c" "i" (varExpr "v"))
                         (return (msgExpr "theVoid" nil))))::
                 (methodDecl "get" 
                        ((methodFormalDecl "c" (ty "Cell"))::nil)
                   (ty "Int") 
                   (body (exprStmt (msgExpr "theVoid" nil))
                         (return (getExpr (varExpr "c") "i"))))::nil)
                nil 
                (mainDecl ((varDecl "x"  (ty "Cell"))::
                                (varDecl "y" (ty "Cell"))::nil)
                   (seqStmt 
                      ((assignStmt "x" (newExpr  "Cell" ((intLiteral 4)::nil)))
                       ::(assignStmt "y" (varExpr "x"))::nil))
                   ((varDecl "Ans"  (ty "Int"))::nil)
		   (seqStmt
	            ((exprStmt
		     (msgExpr "change" ((varExpr "x")::(intLiteral 541)::nil)))
		    ::
                    (assignStmt "Ans" (msgExpr "get" ((varExpr "y")::nil)))::
		    nil)))).