/*
 * ValidFunctionOpDeclChecker.java
 * ---------------------------------
 * Copyright (c) 2017
 * RESOLVE Software Research Group
 * School of Computing
 * Clemson University
 * All rights reserved.
 * ---------------------------------
 * This file is subject to the terms and conditions defined in
 * file 'LICENSE.txt', which is part of this source code package.
 */
package edu.clemson.cs.rsrg.typeandpopulate.sanitychecking;

import edu.clemson.cs.rsrg.absyn.declarations.operationdecl.OperationDec;
import edu.clemson.cs.rsrg.absyn.expressions.Exp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp.Operator;
import edu.clemson.cs.rsrg.absyn.expressions.mathexpr.VarExp;
import edu.clemson.cs.rsrg.parsing.data.Location;
import edu.clemson.cs.rsrg.statushandling.exception.SourceErrorException;

/**
 * <p>This is a sanity checker for making sure the {@link OperationDec}
 * is valid function operation declaration.</p>
 *
 * @author Yu-Shan Sun
 * @version 1.0
 */
public class ValidFunctionOpDeclChecker {

    // ===========================================================
    // Member Fields
    // ===========================================================

    /** <p>The function operation declaration to be checked.</p> */
    private final OperationDec myFunctionOperationDec;

    // ===========================================================
    // Constructors
    // ===========================================================

    /**
     * <p>Creates a sanity checker for checking the various different criteria
     * for being a valid function operation declaration.</p>
     *
     * @param functionOperation The associated function operation declaration.
     */
    public ValidFunctionOpDeclChecker(OperationDec functionOperation) {
        myFunctionOperationDec = functionOperation;
    }

    // ===========================================================
    // Public Methods
    // ===========================================================

    /**
     * <p>Checks to see if the provided {@link OperationDec} is a
     * valid function operation declaration. A valid function
     * operation declaration must have an {@code ensures} clause
     * of the form: {@code <FuncOpDeclName> = <Expression/Value>}.</p>
     *
     * @throws SourceErrorException This is thrown if it is not a valid
     * function operation declaration. The message will indicate why it is
     * not valid.
     */
    public final void checkFunctionOpDecl() {
        Location funcOpLoc = myFunctionOperationDec.getLocation();
        String funcOpName = myFunctionOperationDec.getName().getName();
        Exp ensuresExp = myFunctionOperationDec.getEnsures().getAssertionExp();

        // 1. Make sure we don't have "ensures true"
        if (!VarExp.isLiteralTrue(ensuresExp)) {
            
        }
        else {
            throw new SourceErrorException("Function operation: " + funcOpName + " cannot have 'ensures true;' as its specification.", funcOpLoc);
        }
    }

}
@@ -2885,27 +2885,257 @@
         
-%0A        %7D%0A
+// 2. Make sure it is an EqualsExp with the %22=%22 operator%0A            if (ensuresExp instanceof EqualsExp%0A                    && ((EqualsExp) ensuresExp).getOperator().equals(%0A                            Operator.EQUAL)) %7B%0A%0A            %7D%0A    
         
@@ -3141,16 +3141,20 @@
  else %7B%0A
+    
         
@@ -3214,21 +3214,332 @@
 n: %22
- + funcOpName
+%0A                        + funcOpName%0A                        + %22 must have an ensures clause of the form: '%22%0A                        + funcOpName + %22 = %3CExpression/Value%3E'%22, funcOpLoc);%0A            %7D%0A        %7D%0A        else %7B%0A            throw new SourceErrorException(%22Function operation: %22 + funcOpName%0A                   
  + %22
@@ -3590,16 +3590,36 @@
 ation.%22,
+%0A                   
  funcOpL

Must be an equals function expression