module mini_cecil_semantics.

import maps mini_cecil_abstract_syntax algebra_with_store
	visibles_with_store env store
	mini_cecil_type_checking_helpers string_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).


type methodFormal_to_decl	methodFormal -> decl -> o.
methodFormal_to_decl (methodFormalDecl Name Type) (varDecl Name Type).


type decl_to_methodFormal	decl -> methodFormal -> o.
decl_to_methodFormal (varDecl Name Type) (methodFormalDecl Name Type).



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

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

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

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

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

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

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


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


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

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


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

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

     ((new_name ClassId CreatorName),
      (evalExprList Exprs A H Store Vs AfterExprsStore),
      (evaluate_in_algebra A
	CreatorName Vs AfterExprsStore Ans Store'))
=> % ---------------------------------------------
     (evalExpr (newExpr ClassId Exprs) A H Store Ans Store').

     ((get_name FieldName Getter),
      (evalExpr Expr A H Store (inLocation Loc) AfterExprStore),
      (evaluate_in_algebra A
	Getter ((inLocation Loc)::nil) AfterExprStore Ans Store'))
=> % ---------------------------------------------
     (evalExpr (getExpr Expr FieldName) A H Store Ans Store').

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


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

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

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

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


     (evalStmt (seqStmt nil) A H Store Store).

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



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

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


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


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



%%% 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).

    ((P D Store After1Env After1Store),
     (elaborateList P Ds After1Store RestEnv Store'),
     (Env = (overlay RestEnv After1Env)))
=> % ---------------------------------------------
     (elaborateList P (D::Ds) Store Env Store').


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




%%% elaborateProcedure
type elaborateProcedure	procedure -> (environ string bindable)
				-> (environ string bindable)
				-> o.
(elaborateProcedure (procedureDecl PName Decls ReturnType Body) OldEnv
	  (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).

    ((elaborateProcedure P OldEnv Env'),
     (elaborateProcedureList Ps Env' NewEnv))
=> % ----------------------------------------------
     (elaborateProcedureList (P::Ps) OldEnv NewEnv).



%%% compileClass, has to make sure algebra A' can handle new_, get_, and set_
%%% methods.  The get_ and set_ methods are handled ploymorphically in the
%%% algebra module imported above.  The new_ method is put into the algebra
%%% merely to transport the names of the fields to the time when they will be
%%% used; no real compilation is done.
type compileClass	class -> algebra -> algebra -> o.
     ((new_name CName CreatorMethodName),
      (mappred decl_to_methodFormal Decls MFDecls),
      A' = (add_compiled_method A CreatorMethodName MFDecls
			  (body (seqStmt nil) (return true)))) % body not used
=> % --------------------------------------------
     (compileClass (classDecl CName Decls) A A').
	

%%% compileMethod  (which doesn't really do any "compilation")
type compileMethod	method -> algebra -> algebra -> o.
(compileMethod (methodDecl MName MFDecls RetType Body)
	A
        (add_compiled_method A MName MFDecls Body)).


%%% Have to add clauses to evaluate_in_algebra here,
%%% because only in a module that understands how to evaluate procBodys
%%% can the body of a method be processeed.

    ((search_for_method A MName Actuals MFDecls Body),
     (split_string 4 MName "new_" ClassId), !,
     (mappred (mf \ fn \ (sigma (t \ (mf = (methodFormalDecl fn t)))))
	       MFDecls FieldNames),
     (makeAbstractValueTuple FieldNames Actuals Tuple),
     (alloc (ty ClassId) (inObjectTuple ClassId Tuple) Store Result Store'))
=> % ---------------------------------------------------------
     (evaluate_in_algebra A MName Actuals Store (inLocation Result) Store').

   ((search_for_method A MName Actuals MFDecls Body),
    (mappred methodFormal_to_decl MFDecls Decls),
    (bind_formals_to_actuals Decls Actuals
	empty_environ Store BodyEnv AfterBindingStore),
    (evalBody Body
	      A    % using the same algebra allows mutually recursive methods
	      BodyEnv AfterBindingStore Result Store'))
=> % ---------------------------------------------------------
     (evaluate_in_algebra A MName Actuals Store Result Store').



type compileList	(T -> algebra -> algebra -> o)
		 	 -> (list T) -> algebra -> algebra -> o.

    (compileList CF nil A A).

    ((CF D A A''), (compileList CF Ds A'' A'))
=> % -----------------------------------------
     (compileList CF (D::Ds) A A').
	

%%% runProgram
type runProgram		program
				-> (environ string bindable) -> (store value)
				-> o.
    ((compileList compileClass Classes algebraVIS AwithClasses),
     (compileList compileMethod Methods AwithClasses A),
     (elaborateProcedureList Procs empty_environ ProcEnv),
     empty_store EmptyStore,
     (runMain Main A ProcEnv EmptyStore ResEnv ResStore))
=> % --------------------------------------------------------------
     (runProgram (programDecl Classes Methods Procs Main) ResEnv ResStore).