/**
 * Implementation of quant.h
 *
 * Note: copied over the includes from interp.c, for now.
 */

#include "std-macros.h"
#include "parse-tree.h"
#include "tokens.h"
#include "sym.h"
#include "sym-aux.h"
#include "type-preds.h"
#include "type.h"
#include "str.h"
#include "interp.h"
#include "list.h"
#include "vlist.h"
#include "quant.h"
#include "universe.h"
#include "token-mapping.h"

/*
 * Evaluate a universal or existential quantifier.  See the notes in
 * documentation/contrib/pcorwin/executing-quantifiers.pdf.
 *
 * Note that this implementation utilizes a form of DeMorgan's law. From
 * the notes on executing quantifiers:
 *    forall (x:t) p <=> not (exists (x:t) not p)
 *    exists (x:t) p <=> not (forall (x:t) not p)
 *typeNameNode->components.atom.val.text
 * What follows is a pretty straightforward implementation of forall,
 * with some negations added in for handling an exists case.
 */
ValueStruct doQuant(nodep t) {
    ValueStruct result,
		testResult,
		suchThatResult,
		list,
		individualVal,
		lval;
    nodep in;
    int i,o,so;
    SymtabEntry* sym;
    Symtab* st;
    Value** saveftos;
    bool isForall = (t->header.name == YFORALL);
    bool hasSuchThat = false;

    /*
     * initialize result bool structure
     */
    result = MakeVal(RVAL, BoolType);    
    result->val.BoolVal = true;

    /**
     * get the symtab ready, save the display, etc.
     */
    PushSymtab();
    MoveToSymtab(st = t->components.decl.kind.quant.symtab);
    saveftos = GetFTos();
    PushActRec(o = st->Offset);
    SaveDisplay(st->Level, so = (o - 1));

    /*
     * is this an "in" quantifier? e.g., of the format:
     * forall (val in list) expression
     * Note that the "in" could be the such that form; check to make sure it's YIN
     */
    if ((in = t->components.decl.kind.quant.in) && (in->header.name == YIN)){
	/*
	 * Find the symtab entry for this text identifier
	 */
	sym = LookupString(t->components.decl.kind.quant.vars->components.atom.val.text);

	switch (in->header.name) {
	    case YIN:
		/*
		 * Find the list.
		 */
		list = interpExpr(in->components.unop.operand);

		/*
	         * if something came back, it's a list and we've got list content...
		 * Note: if we have a nil list, true makes sense here (and so we do nothing).
		 */
		if (list && isListType(list->type) && list->val.ListVal) {
		    /*
		     * Get the memory address where we'll store the contents of the element identifier
		     */
		    lval = MakeVal(LVAL, sym->Type);
		    lval->val.LVal = GetAddr(sym);

		    /*
		     * for each element in the list...
		     *    get the ith value
		     *    add it to the symtab to link it with the val name for expr interp
		     *    interp the expr
		     *    keep track of the result
		     */
		    for (i = 1; (i <= ListLen(list->val.ListVal)) && result->val.BoolVal; i++) {
			individualVal = (ValueStruct)GetListNth(list->val.ListVal, i);
//			doAssmnt(lval, individualVal, false, null);
			*(lval->val.LVal) = individualVal;
			testResult = interpExpr(t->components.decl.kind.quant.expr);
			if (testResult == null) {
			    // be good a citizen
			    RestoreDisplay(st->Level, so);
			    SetFTos(saveftos);
			    PopSymtab();
			    return null;
			}
			/*
			 * slap in some DeMorgan's law, if we need to, as we store the result
			 */
			result->val.BoolVal = isForall ? testResult->val.BoolVal :
				!(testResult->val.BoolVal);
		    } // end for
		} // end if list with content
		/*
		 * slap in some DeMorgan's law, if we need to
		 */
		if (!isForall) {
		    result->val.BoolVal = !(result->val.BoolVal);
		}
		break;
	} // end switch
    } // end if in
    /* must be an unbounded case? e.g., forall (i:integer), but could be forall (i:integer | i expr) */
    else {
	if ((in = t->components.decl.kind.quant.in) && (in->header.name == '|')) {
	    hasSuchThat = true;
	}

	// quant expression stuff in here? if (in = t->components.decl.kind.quant.vars) 
	/*
	 * Find the symtab entry for this text identifier
	 */
	sym = LookupString(t->components.decl.kind.quant.vars->components.decl.kind.var.vars->components.atom.val.text);

	if (sym) {
	    lval = MakeVal(LVAL, sym->Type);
	    lval->val.LVal = GetAddr(sym);

	  if (lval->type) {
	    list = UniverseGetValueStructFromType(lval->type->components.type.resolvedname);
	    /* 
	     ********** START BLOCK
	     */
		/*
	         * if something came back, it's a list and we've got list content...
		 * Note: if we have a nil list, true makes sense here (and so we do nothing).
		 */
		if (list && list->val.ListVal) {
		    /* if we have an exists here, start this puppy out as false */
		    if (!isForall)
			result->val.BoolVal = false;

		    /*
		     * for each element in the list...
		     *    get the ith value
		     *    add it to the symtab to link it with the val name for expr interp
		     *    interp the expr
		     *    if we're dealing with a suchthat, the following equivalence holds and must be taken into account:
		     *       forall (i:integer | p1) p2 <=> forall (i:integer) if p1 then p2
		     *    keep track of the result
		     *
		     * Note: although performance-wise it may make sense to evaluate p1 first, for now
		     *       for clarity of code we're leaving it so we eval p2 first in a suchthat case.
		     */
		    for (i = 1; (i <= ListLen(list->val.ListVal)) && (result->val.BoolVal || !isForall); i++) {
			individualVal = (ValueStruct)GetListNth(list->val.ListVal, i);
			//doAssmnt(lval, individualVal, false, null);
			/* 
			 * Note that the following code is very similar to Bind, and we don't call Bind
			 * because we don't want to bother considering inserting this value... or do we?
			 * TODO. *(fv->val.LVal) = av;
			 */

			*(lval->val.LVal) = individualVal;

			/*
			 * First evaluate the suchthat, if we have one
			 */
			if (hasSuchThat) {
			    suchThatResult = interpExpr(in->components.unop.operand);
			    if (suchThatResult == null) {
				// be good a citizen
				RestoreDisplay(st->Level, so);
				SetFTos(saveftos);
				PopSymtab();
				return null;
			    }
			} // end if hasSuchThat

			/*
			 * recall forall (i:integer | p1) p2 <=> forall (i:integer) if p1 then p2
			 * or in other words, if suchThatResult is false, make sure testResult is true.
			 */
			if (hasSuchThat && isForall && (suchThatResult->val.BoolVal == false)) {
			    testResult = MakeVal(RVAL, BoolType);
			    testResult->val.BoolVal = true;
			}
			/*
			 * If we have no such that then we need to proceed and do some evaluation.
			 * Also, if we have a suchthat and the suchthat expr evaluated to true, proceed.
			 */
			else { 

			    testResult = interpExpr(t->components.decl.kind.quant.expr);
			    if (testResult == null) {
				// be good a citizen
				RestoreDisplay(st->Level, so);
				SetFTos(saveftos);
				PopSymtab();
				return null;
			    } // end if testResult == null
			}

			/* carry on the right value depending on whether exists or forall */
		        if (isForall) {
			    result->val.BoolVal = result->val.BoolVal && testResult->val.BoolVal;
			}
			/* exists */
			else {
			    result->val.BoolVal = result->val.BoolVal || testResult->val.BoolVal;
			}
		    } // end for
		} // end if list with content

	    /********* END BLOCK *******/
	  }
	}
    } // end if unbounded quantifier case?

    // be good a citizen
    RestoreDisplay(st->Level, so);
    SetFTos(saveftos);
    PopSymtab();

    return result;
} // end function doQuant