CommonPrimitiveType.java

package edu.udel.cis.vsl.civl.model.common.type;

import edu.udel.cis.vsl.civl.model.IF.CIVLInternalException;
import edu.udel.cis.vsl.civl.model.IF.CIVLSource;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLPrimitiveType;
import edu.udel.cis.vsl.civl.model.IF.type.CIVLType;
import edu.udel.cis.vsl.civl.util.IF.Singleton;
import edu.udel.cis.vsl.sarl.IF.SymbolicUniverse;
import edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression;
import edu.udel.cis.vsl.sarl.IF.expr.NumericExpression;
import edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicTupleType;
import edu.udel.cis.vsl.sarl.IF.type.SymbolicType;

/**
 * Implementation of {@link CIVLPrimitiveType}.
 * 
 * @author Timothy K. Zirkel (zirkel)
 * 
 */
public class CommonPrimitiveType extends CommonType
		implements
			CIVLPrimitiveType {

	private PrimitiveTypeKind kind;

	private NumericExpression sizeofExpression;

	private BooleanExpression facts;

	/**
	 * Constructs new primitive type instance with given parameters
	 * 
	 * @param kind
	 *            the kind of primitive type; may not be null
	 * @param symbolicType
	 *            the symbolic type corresponding to this primitive type; may be
	 *            null here but then must be set later
	 * @param sizeofExpression
	 *            the value that will be returned when evaluating "sizeof" this
	 *            type; null indicates this type should never occur in a sizeof
	 *            expression and if it does an exception will be thrown
	 * @param facts
	 *            boolean predicates concerned with this type which must hold,
	 *            e.g., sizeof(t)>0 or sizeof(t)=1
	 * 
	 */
	public CommonPrimitiveType(PrimitiveTypeKind kind,
			SymbolicType symbolicType, NumericExpression sizeofExpression,
			BooleanExpression facts) {
		super();
		this.dynamicType = symbolicType;
		this.kind = kind;
		this.sizeofExpression = sizeofExpression;
		this.facts = facts;
	}

	/**
	 * @return The actual primitive type (int, bool, real, or string).
	 */
	public PrimitiveTypeKind primitiveTypeKind() {
		return kind;
	}

	/**
	 * @param The
	 *            actual primitive type (int, bool, real, or string).
	 */
	public void setPrimitiveType(PrimitiveTypeKind primitiveType) {
		this.kind = primitiveType;
	}

	@Override
	public String toString() {
		switch (kind) {
			case INT :
				return "int";
			case BOOL :
				return "$bool";
			case REAL :
				return "$real";
			case SCOPE :
				return "$scope";
			case STATE :
				return "$state";
			case PROCESS :
				return "$proc";
			case DYNAMIC :
				return "$dynamicType";
			case VOID :
				return "void";
			case CHAR :
				return "char";
			case MEMORY :
				return "$memory";
			default :
				throw new CIVLInternalException(
						"Unknown primitive type kind: " + kind,
						(CIVLSource) null);
		}
	}

	@Override
	public boolean isNumericType() {
		return kind == PrimitiveTypeKind.INT || kind == PrimitiveTypeKind.REAL;
	}

	@Override
	public boolean isIntegerType() {
		return kind == PrimitiveTypeKind.INT;
	}

	@Override
	public boolean isRealType() {
		return kind == PrimitiveTypeKind.REAL;
	}

	@Override
	public boolean isProcessType() {
		return kind == PrimitiveTypeKind.PROCESS;
	}

	@Override
	public boolean isStateType() {
		return kind == PrimitiveTypeKind.STATE;
	}

	@Override
	public boolean isScopeType() {
		return kind == PrimitiveTypeKind.SCOPE;
	}

	@Override
	public boolean isBoolType() {
		return kind == PrimitiveTypeKind.BOOL;
	}

	@Override
	public boolean hasState() {
		return false;
	}

	@Override
	public boolean isVoidType() {
		return kind == PrimitiveTypeKind.VOID;
	}

	@Override
	public NumericExpression getSizeof() {
		return sizeofExpression;
	}

	@Override
	public BooleanExpression getFacts() {
		return facts;
	}

	public void setDynamicType(SymbolicType dynamicType) {
		this.dynamicType = dynamicType;
	}

	@Override
	public SymbolicType getDynamicType(SymbolicUniverse universe) {
		if (dynamicType == null && kind != PrimitiveTypeKind.VOID)
			throw new CIVLInternalException(
					"no dynamic type specified for primitive type " + kind,
					(CIVLSource) null);
		return dynamicType;
	}

	@Override
	public boolean isCharType() {
		return kind == PrimitiveTypeKind.CHAR;
	}

	@Override
	public SymbolicExpression initialValue(SymbolicUniverse universe) {
		switch (this.kind) {
			case BOOL :
				return universe.bool(false);
			case DYNAMIC :
				return null;
			case INT :
				return universe.integer(0);
			case PROCESS :
				return universe.tuple((SymbolicTupleType) this.dynamicType,
						new Singleton<SymbolicExpression>(
								universe.integer(-2)));
			case STATE :
				return universe.tuple((SymbolicTupleType) this.dynamicType,
						new Singleton<SymbolicExpression>(
								universe.integer(-1)));
			case REAL :
				return universe.rational(0);
			case SCOPE :
				return universe.tuple((SymbolicTupleType) this.dynamicType,
						new Singleton<SymbolicExpression>(
								universe.integer(-2)));
			case CHAR :
				return universe.character('\0');
			default :
		}
		return null;
	}

	@Override
	public TypeKind typeKind() {
		return TypeKind.PRIMITIVE;
	}

	@Override
	public CIVLType copyAs(CIVLPrimitiveType type, SymbolicUniverse universe) {
		return type;
	}

	@Override
	public boolean isScalar() {
		return true;
	}
}