module mini_cecil_with_env_and_store.

import maps mini_cecil_abstract_syntax algebra_with_store
	visibles_with_store env store
	mini_cecil_type_checking_helpers
	debug_write.

%%% semantic domains
kind    bindable	type.
kind	procedureClosure type.

type	inValue			value -> bindable.
type	inProcedureClosure	procedureClosure -> bindable.

type	makeProcClosure	(environ string bindable)  % birth environment
				-> (list decl)     % formal parameters
				-> procBody
				-> procedureClosure.

%%% auxiliary functions
type	bind_formal_to_actual decl -> value
				-> (environ string bindable) -> (store value)
				-> (environ string bindable) -> (store value)
				-> o.
(bind_formal_to_actual (varDecl VName T) Actual
		OldEnv OldStore NewEnv NewStore) :-
	(alloc (varType T) Actual OldStore Loc NewStore),
	NewEnv = (overlay (bind VName (inValue (inLocation Loc))) OldEnv).

type	bind_formals_to_actuals (list decl) -> (list value)
				-> (environ string bindable) -> (store value)
				-> (environ string bindable) -> (store value)
				-> o.
(bind_formals_to_actuals nil nil Env Store Env Store).
(bind_formals_to_actuals (Formal::Formals) (Actual::Actuals)
		OldEnv OldStore NewEnv NewStore) :-
	(bind_formal_to_actual Formal Actual OldEnv OldStore Env' Store'),
	(bind_formals_to_actuals Formals Actuals Env' Store' NewEnv NewStore).


%%% evaluation relations %%%%%%%%%%%

type	evalExpr	expression -> (environ string bindable)
				-> (store value) 
				-> value -> (store value) -> o.

type	evalExprList	(list expression) -> (environ string bindable)
				-> (store value) 
				-> (list value) -> (store value) -> o.

type	evalStmt	statement -> (environ string bindable)
				-> (store value) 
				-> (store value) -> o.

type	evalBody	procBody -> (environ string bindable)
				-> (store value)
				-> value -> (store value) -> o.

type	evalResultExpr	resultExpr -> (environ string bindable)
				-> (store value)
				-> value -> (store value) -> o.

%%% evalExpr
     ((find H VName (inValue (inLocation L))),
      (evaluate_in_algebra algebraVIS
	"get!var!value" ((inLocation L)::nil) Store Ans Store))
=> % ---------------------------------------------
     (evalExpr (varExpr VName) H Store Ans Store).


     (evalExpr (intLiteral N) H Store (inInteger N) Store).


     (evalExpr true H Store (inTruthValue tt) Store).

     (evalExpr false H Store (inTruthValue ff) Store).


     ((evalExprList Exprs H Store Vs AfterExprsStore),
      (evaluate_in_algebra algebraVIS MsgName Vs AfterExprsStore Ans Store'))
=> % --------------------------------------------------------------------
     (evalExpr (msgExpr MsgName Exprs) H Store Ans Store').

    ((find H ProcName
             (inProcedureClosure
	       (makeProcClosure ProcsEnv Formals Body))),
     (evalExprList Exprs H Store Vs AfterExprsStore),
     (bind_formals_to_actuals Formals Vs
		ProcsEnv AfterExprsStore BodyEnv AfterBindingStore),
     (evalBody Body BodyEnv AfterBindingStore Ans Store'))
=> % -------------------------------------------------------
     (evalExpr (procCallExpr ProcName Exprs) H Store Ans Store').


%%% evalExprList
(evalExprList nil H Store nil Store).
(evalExprList (E::Es) H Store (V::Vs) Store') :-
	(evalExpr E H Store V IntermediateStore),
	(evalExprList Es H IntermediateStore Vs Store').


%%% evalStmt
     (evalExpr E H Store Ans Store')
=> % --------------------------------------
     (evalStmt (exprStmt E) H Store Store').

     ((evalExpr E H Store V AfterExprStore),
      (find H VarName (inValue (inLocation L))),
	(evaluate_in_algebra  algebraVIS "set!var!value"
			((inLocation L)::V::nil)
			AfterExprStore Ignored Store'))
=> % ---------------------------------------------------
     (evalStmt (assignStmt VarName E) H Store Store').

     ((evalExpr E H Store Ans AfterExprStore),
      (set_name FieldName Setter),
      (find H VarName (inValue (inLocation L))),
      (evaluate_in_algebra algebraVIS Setter
			((inLocation L)::Ans::nil)
			AfterExprStore Ignored Store'))
=> % ------------------------------------------------------------
     (evalStmt (setFieldStmt VarName FieldName E) H Store Store').

     ((evalExpr E H Store (inTruthValue tt) AfterExprStore),
      (evalStmt S1 H AfterExprStore Store'))
=> % ------------------------------------------------------------
     (evalStmt (ifStmt E S1 S2) H Store Store').


     (evalStmt (seqStmt nil) H Store Store).

     ((evalStmt S H Store AfterSStore),
      (evalStmt (seqStmt SList) H AfterSStore Store'))
=> % ------------------------------------------------------------
     (evalStmt (seqStmt (S::SList)) H Store Store').



     ((evalExpr E H Store (inTruthValue ff) AfterExprStore),
      (evalStmt S2 H AfterExprStore Store'))
=> % ------------------------------------------------------------
     (evalStmt (ifStmt E S1 S2) H Store Store').

%%% evalBody
    ((evalStmt Stmt H Store AfterStmtStore),
     (evalResultExpr ResultExpr H AfterStmtStore Ans Store'))
=> % ---------------------------------------------------
    (evalBody (body Stmt ResultExpr) H Store Ans Store').


%%% evalResultExpr
    (evalExpr E H Store Ans Store')
=> % ---------------------------------------------------
    (evalResultExpr (return E) H Store Ans Store').


%%% elaborate
type elaborate		decl -> (store value)
				-> (environ string bindable)
				-> (store value) -> o.
(elaborate (varDecl VarName T) OldStore Env NewStore) :-
	(alloc (varType T) (unitialized (varType T)) OldStore Loc NewStore),
	Env = (bind VarName (inValue (inLocation Loc))).


%%% elaborateList
type elaborateList	(DeclForm -> Store -> (environ string bindable)
					-> Store -> o)
				-> (list DeclForm)
				-> Store -> (environ string bindable) -> Store
				-> o.
(elaborateList P nil Store empty_environ Store).
(elaborateList P (D::Ds) Store Env Store') :-
	(P D Store After1Env After1Store),
	(elaborateList P Ds After1Store RestEnv Store'),
	Env = (overlay RestEnv After1Env).

%%% runMain
type runMain		main -> (environ string bindable) -> (store value)
				-> (environ string bindable) -> (store value)
				-> o.
(runMain (mainDecl Decls1 Stmt1 Decls2 Stmt2) ProcEnv Store ResEnv ResStore) :-
	(elaborateList elaborate Decls1 Store LocalEnv1 AfterDecls1Store),
	Env1 = (overlay LocalEnv1 ProcEnv),
	(evalStmt Stmt1 Env1 AfterDecls1Store After1Store),
	(elaborateList elaborate Decls2 After1Store
		LocalEnv2 AfterDecls2Store),
	ResEnv = (overlay LocalEnv2 Env1),
	(evalStmt Stmt2 ResEnv AfterDecls2Store ResStore).


%%% elaborateProcedure
type elaborateProcedure	procedure -> (environ string bindable)
				-> (environ string bindable)
				-> o.
(elaborateProcedure (procedureDecl PName Decls ReturnType Body) OldEnv NewEnv)
	:-
	NewEnv =
	  (overlay
		(bind PName
			(inProcedureClosure
			 (makeProcClosure OldEnv Decls Body)))
	        OldEnv).

%%% elaborateProcedureList
type elaborateProcedureList	(list procedure)
				-> (environ string bindable)
				-> (environ string bindable)
				-> o.
(elaborateProcedureList nil Env Env).
(elaborateProcedureList (P::Ps) OldEnv NewEnv) :-
	(elaborateProcedure P OldEnv Env'),
	(elaborateProcedureList Ps Env' NewEnv).


%%% runProgram
type runProgram		program
				-> (environ string bindable) -> (store value)
				-> o.
(runProgram (programDecl nil nil Procs Main) ResEnv ResStore) :-
	(elaborateProcedureList Procs empty_environ ProcEnv),
	empty_store EmptyStore,
	(runMain Main ProcEnv EmptyStore ResEnv ResStore).