module mini_cecil_with_env.

import maps mini_cecil_abstract_syntax algebra visibles env.

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

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

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

%%% auxiliary functions
type	bind_formals_to_actuals (list string) -> (list value)
				-> (environ string bindable)
				-> (environ string bindable) -> o.

(bind_formals_to_actuals nil nil Env Env).
(bind_formals_to_actuals (Formal::Formals) (Actual::Actuals) OldEnv NewEnv) :-
	Env' = (overlay (bind Formal (inValue Actual)) OldEnv),
	(bind_formals_to_actuals Formals Actuals Env' NewEnv).


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

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


 (find H VName (inValue Ans))
=> % -----------------------
 (evalExpr (varExpr VName) H Ans).


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


(evalExpr true H (inTruthValue tt)).

(evalExpr false H (inTruthValue ff)).


 ((mappred (e \ v \ (evalExpr e H v)) Exprs Vs),
  (evaluate_in_algebra algebraVIS MsgName Vs Ans))
=> % ---------------------------------
 (evalExpr (msgExpr MsgName Exprs) H Ans).

 ((find H ProcName
          (inProcedureClosure
	    (makeProcClosure H' Formals Body))),
  (mappred (e \ v \ (evalExpr e H v)) Exprs Vs),
  (bind_formals_to_actuals Formals Vs H' H''),
  (evalBody Body H'' Ans))
=> % --------------------------------
 (evalExpr (procCallExpr ProcName Exprs) H Ans).


(evalBody (body (seqStmt nil) (return E)) H Ans) :-
	(evalExpr E H Ans).