#include <setjmp.h>
#include <stdio.h>
#include <stdlib.h>
#include "std-macros.h"
#include "std-macros.h"
#include "parse-tree.h"
#include "parser.h"
#include "tokens.h"
#include "sym.h"
#include "sym-aux.h"
#include "type.h"
#include "interp.h"
#include "type-preds.h"
#include "parser-aux.h"
#include "list.h"
#include "typechk.hP"
#include "options.h"
#include "validate.h"
#include "token-mapping.h"

/*
 * Type check a validation invocation of the form
 *
 *     arith_expr(in_args) ?-> (out_args)
 *
 * by checking the calling part "arith_expr(op_args)" in the normal way, i.e.,
 * as a regular proc call.  Then check that the second set of op args is
 * compatible in number and type with the co-arity of the called op.
 */
TypeStruct chkValidationCall(nodep t, nodep tt) {
    TypeStruct pt;
    nodep desig;
    SymtabEntry* sym;
    TypeStruct rtn;

    /*
     * Leave if front part doesn't check.
     */
    if (not (pt = chkProcCall(t, tt))) {
	return null;
    }

    /*
     * Do the binding check for the back part, i.e., the output formals and
     * actuals.  This mimics the code at the end of doProcCall, but with the
     * focus here on the output parms, instead of the inputs.  In particular,
     * the last arg to the chkBindings functions is true here, as opposed to
     * false in doProcCall.
     *
     * TODO: Even though the conditional logic is in place, the code here
     * currently only works for name calls, pending proper storage of output
     * parm chain in an op type entry.  Cf. chkProcCall, which is currently
     * unused, for what needs to be done.
     */
    desig = chkProcDesig(t, &sym);

    if (sym) {
	return (rtn = chkBindingsNameCall(sym, desig, t, tt, true))
	    ? ValidationTupleType : null;
    }
    else {
	return (rtn = chkBindingsDesigCall(sym, desig, t, true))
	    ? ValidationTupleType : null;
    }
}


/*
 * Evaluate a validation invocation of the form
 *
 *     arith_expr(in_args) ?-> (out_args)
 *
 * The evaluation goes like this:
 *     (1) bind the in_args the way doProcCall does, including push of act rec
 *         and entry into proc scope
 *     (2) evaluate the precond expr in this bound-inputs context, producing a
 *         bool result
 *     (3) bind the out_args in the same way
 *     (4) evaluate the postcond expr in this bound-inputs/outputs context,
 *         producing another bool result
 *
 * The code here is heavily modified a version of interp.c:doProcCall.  It
 * might be worthwhile to try to parameterize doProcCall, so it would work for
 * both regular calls and validation calls.  However, given the rather
 * significant divergence of this code and doProcCall, the twain of the two is
 * likely never again to meet.
 */
ValueStruct doValidationCall(nodep t) {
    SymtabEntry *p, *fp;
    nodep ap, d;
    ValueStruct v1, v2;
    int i, o, so;
    Value** saveftos;
    jmp_buf **jbp;
    nodep pre, post;

    /*
     * Evaluate proc designator.
     */
    v1 = interpExpr(d = t->components.proccall.desig);

    /*
     * Check for a non-null procedure.  Type checking handles everything else
     * but this.
     */
    if (not (p = v1->val.ProcVal)) {
	lerror(t, "Attempt to call a null procedure.\n");
	longjmp(RuntimeError, NilProcStatus);
    }

    /*
     * Push storage for act rec, based on size of parm and local storage.
     * The detailed comment in doProcCall applies precislely here.
     */
    saveftos = GetFTos();
    PushActRec(o = p->Info.Op.Symtab->Offset);

    /*
     * Bind the input formals and actuals.  The separate binding function is
     * new here vis a vis doProcCall.  The binding code was functionized since
     * it needs to be called from two places here in doValidartionCall --
     * inputs binding and outputs binding.
     */
    BindValidationParms(t->components.proccall.actuals, p->Info.Op.InParms);

    /*
     * Bind the output formals and actuals.  It is important to note that
     * binding outputs here means there can be no side effects to output parms
     * in the precond eval.  This should really go without saying, particularly
     * since the type checker should prevent precond side effects of any form.
     * TODO: make the type checker in fact do this.g
     */
    BindValidationParms(t->components.proccall.returns, p->Info.Op.OutParms);

    /*
     * Move the Symtab context into the called proc.  Same as doProcCall.
     */
    PushSymtab();
    MoveToSymtab(p->Info.Op.Symtab);
    
    /*
     * Save the current display entry for this proc's level and update the
     * entry at this level.  Again, the doProcCall comment applies here.
     */
    SaveDisplay(p->Level, so = (o - 1));

    /*
     * If the precond is empty, set its value unconditionally to true,
     * otherwise evaluate the expr.
     */
    pre = p->Info.Op.precond;
    if ((pre == null) or (pre->components.decl.kind.pre.expr == null)) {
	v1 = MakeVal(RVAL, BoolType);
	v1->val.BoolVal = true;
    }
    else {

	/* Recursively execute the body of the non-empty precond.  This is
	 * fundamentally different than doProcCall.  There the op body is
	 * executed.  Here the precond and postcond exprs are executed.
	 */
	jbp = (jmp_buf **) StackAddr(p->Info.Op.Offset);
	*jbp = (jmp_buf *) malloc(sizeof(jmp_buf));
	if (not (v1 = ((ValueStruct) setjmp(**jbp))))
	    v1 = interpExpr(pre);
	free(*jbp);
    }

    /*
     * If the precond evaluates to true, evaluate the body of the postcond.
     * Otherwise, make the postcond a nil value.
     */
    if (v1 and v1->val.BoolVal == true) {

        post = p->Info.Op.postcond;

	/*
	 * If the postcond is empty, set its value unconditionally to nil,
	 * otherwise evaluate the expr.
	 */
	if (post->components.decl.kind.post.expr == null) {
	    v2 = TheNilValue;
	}
	else {
	    jbp = (jmp_buf **) StackAddr(p->Info.Op.Offset);
	    *jbp = (jmp_buf *) malloc(sizeof(jmp_buf));
	    if (not (v2 = ((ValueStruct) setjmp(**jbp))))
		v2 = interpExpr(post);
	    free(*jbp);
	}
    }
    else {
	v2 = MakeVal(RVAL, NilType);
    }

    /*
     * Restore display, as in doProcCall.
     */
    RestoreDisplay(p->Level, so);

    /*
     * Pop act rec by restoring entering ftos; restore calling symtab context.
     * Again as in doProcCall.
     */
    SetFTos(saveftos);
    PopSymtab();

    /*
     * Return a validation tuple with the computed precond and postcond vals.
     * This is specific to doValidationCall.  Here we return the two-tupe that
     * holds the evaluation results of the precond and poscond evals.
     */
    return BuildValidationTupleVal(v1, v2);
}

/*
 * Bind the given list of actuals to the given list of formals.  This called
 * twice -- once for inputs and once for outputs.  Other than that, the logic
 * is the same as in doProcCall.
 */
void BindValidationParms(nodep actuals, SymtabEntry* formals) {
    nodep ap;
    SymtabEntry* fp;
    int i;
    ValueStruct v1, v2;

    /*
     * Evaluate each actual and store value in corresponding formal.  
     */
    for (ap = actuals,
	 fp = formals,
	 i=1;
           ap && fp;
	     ap = ap->components.exprlist.next,
	     fp = fp->Info.Parm.Link,
	     i++) {

	/*
	 * Compute address of formal, in callED environment.  The callED stack
	 * environment is pointed to by ftos.  We havent yet moved into the
	 * callED symtab environment, but we get there through the threaded
	 * parm chain.
	 */
	v1 = MakeVal(LVAL, fp->Type);
	v1->val.LVal = GetFormalAddr(fp);

	/*
	 * Recursively eval actual in the callING environment.  The callING
	 * stack environment is pointed to by the current display entry, which
	 * the recursive call to inerpExpr will use via GetAddr.  And as noted
	 * above, we havent yet moved into the callED symtab environment.
	 *
	 * Note the different handling of call-by-val vs call-by-var parms.
	 * For the former, we compute an r-value, for the latter an l-value.
	 */
	if (ChkSymFlag(fp, varParm))
	    v2 = designator(ap->components.exprlist.expr);
	else
	    v2 = interpExpr(ap->components.exprlist.expr);

	/*
	 * Bind per the parm discipline -- call-by-value, call-by-var, call-by
	 * array.
	 */
	Bind(fp, v1, v2);
    }
}

/*
 * Construct the 2-tuple type returned by a successful chkValidationCall.  It's
 * a tupe of boolean and boolean.
 */
TypeStruct BuildValidationTupleType() {
    TypeStruct rtn = NewNode(TYPE_NODE, YRECORD, EmptyLoc);
    nodep f;

    rtn->components.type.kind.record.numfields = 2;
    rtn->components.type.kind.record.fieldstab = AllocSymtab(2);

    f = rtn->components.type.kind.record.fields = NewNode(
	DECL_NODE, ':', EmptyLoc);
    f->components.decl.kind.field.vars = null;
    f->components.decl.kind.field.type = BoolType;
    f->components.decl.kind.field.isinherited = false;

    f = f->components.decl.next = NewNode(
	DECL_NODE, ':', EmptyLoc);
    f->components.decl.kind.field.vars = null;
    f->components.decl.kind.field.type = BoolType;
    f->components.decl.kind.field.isinherited = false;
    f->components.decl.next = null;

    return rtn;
}

/*
 * Construct a 2-tuple value returned by a successful doValidationCall.
 * Initialize the 2 fields to the given boolean values v11 and v2.  These
 * values come from te evaulation of the precond and postcond exprs, resp.
 */
ValueStruct BuildValidationTupleVal(ValueStruct v1, ValueStruct v2) {
    ValueStruct rtn = MakeVal(RVAL, ValidationTupleType);
    List* l;

    /*
     * Insert the two field values in the struct val list.
     */
    l = rtn->val.StructVal = NewList();

    /*
     * If v1 and/or v2 = null, make them the nil value.
     */
    if (not v1) {
	v1 = TheNilValue;
    }
    if (not v2) {
	v2 = TheNilValue;
    }

    /*
     * Stick the values in the return tuple.
     */
    PutList(l, (ListElemData*) v1);
    PutList(l, (ListElemData*) v2);

    return rtn;    
}