From af6eef0c4929ca8400d215af4e1db5cbb0a4815b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 18 Jul 2011 16:31:09 +0000
Subject: [PATCH] Added castValueTo method to Type classes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3288 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/type/Type.java       | 19 +++++++++++++++++++
 prism/src/parser/type/TypeBool.java   | 12 ++++++++++++
 prism/src/parser/type/TypeClock.java  | 14 ++++++++++++++
 prism/src/parser/type/TypeDouble.java | 14 ++++++++++++++
 prism/src/parser/type/TypeInt.java    | 12 ++++++++++++
 5 files changed, 71 insertions(+)

diff --git a/prism/src/parser/type/Type.java b/prism/src/parser/type/Type.java
index 79da9a1f..cf4ca1b9 100644
--- a/prism/src/parser/type/Type.java
+++ b/prism/src/parser/type/Type.java
@@ -26,15 +26,34 @@
 
 package parser.type;
 
+import prism.PrismLangException;
+
 public abstract class Type 
 {
 	public abstract String getTypeString();
 	
+	/**
+	 * Returns true iff a variable of this type can be assigned a value that is of type {@code type}. 
+	 */
 	public boolean canAssign(Type type)
 	{
+		// Play safe: assume not possible, unless explicitly overridden.
 		return false;
 	}
 	
+	/**
+	 * Make sure that a value, stored as an Object (Integer, Boolean, etc.) is of this type.
+	 * Basically, implement some implicit casts, e.g. Integer -> Double.
+	 * This should only only work for combinations of types that satisfy {@code #canAssign(Type)}.
+	 * If not, an exception is thrown (but such problems should have been caught earlier by type checking)
+	 */
+	public Object castValueTo(Object value) throws PrismLangException
+	{
+		// Play safe: assume error unless explicitly overridden.
+		throw new PrismLangException("Cannot cast a value to type " + getTypeString());
+	}
+	
+	@Override
 	public String toString()
 	{
 		return getTypeString();
diff --git a/prism/src/parser/type/TypeBool.java b/prism/src/parser/type/TypeBool.java
index b92c8115..875c360f 100644
--- a/prism/src/parser/type/TypeBool.java
+++ b/prism/src/parser/type/TypeBool.java
@@ -26,6 +26,8 @@
 
 package parser.type;
 
+import prism.PrismLangException;
+
 public class TypeBool extends Type 
 {
 	private static TypeBool singleton;
@@ -54,8 +56,18 @@ public class TypeBool extends Type
 		return singleton;
 	}
 	
+	@Override
 	public boolean canAssign(Type type)
 	{
 		return (type instanceof TypeBool);
 	}
+	
+	@Override
+	public Object castValueTo(Object value) throws PrismLangException
+	{
+		if (value instanceof Integer)
+			return value;
+		else
+			throw new PrismLangException("Can't convert " + value.getClass() + " to type " + getTypeString());
+	}
 }
diff --git a/prism/src/parser/type/TypeClock.java b/prism/src/parser/type/TypeClock.java
index 5183c078..b75ea9c2 100644
--- a/prism/src/parser/type/TypeClock.java
+++ b/prism/src/parser/type/TypeClock.java
@@ -26,6 +26,8 @@
 
 package parser.type;
 
+import prism.PrismLangException;
+
 public class TypeClock extends Type 
 {
 	private static TypeClock singleton;
@@ -54,8 +56,20 @@ public class TypeClock extends Type
 		return singleton;
 	}
 	
+	@Override
 	public boolean canAssign(Type type)
 	{
 		return (type instanceof TypeClock);
 	}
+	
+	@Override
+	public Object castValueTo(Object value) throws PrismLangException
+	{
+		if (value instanceof Double)
+			return value;
+		if (value instanceof Integer)
+			return new Double(((Double) value).doubleValue());
+		else
+			throw new PrismLangException("Can't convert " + value.getClass() + " to type " + getTypeString());
+	}
 }
diff --git a/prism/src/parser/type/TypeDouble.java b/prism/src/parser/type/TypeDouble.java
index 93907811..122883da 100644
--- a/prism/src/parser/type/TypeDouble.java
+++ b/prism/src/parser/type/TypeDouble.java
@@ -26,6 +26,8 @@
 
 package parser.type;
 
+import prism.PrismLangException;
+
 public class TypeDouble extends Type 
 {
 	private static TypeDouble singleton;
@@ -54,8 +56,20 @@ public class TypeDouble extends Type
 		return singleton;
 	}
 	
+	@Override
 	public boolean canAssign(Type type)
 	{
 		return (type instanceof TypeDouble || type instanceof TypeInt);
 	}
+	
+	@Override
+	public Object castValueTo(Object value) throws PrismLangException
+	{
+		if (value instanceof Double)
+			return value;
+		if (value instanceof Integer)
+			return new Double(((Double) value).doubleValue());
+		else
+			throw new PrismLangException("Can't convert " + value.getClass() + " to type " + getTypeString());
+	}
 }
diff --git a/prism/src/parser/type/TypeInt.java b/prism/src/parser/type/TypeInt.java
index 6a43e89e..b464fb95 100644
--- a/prism/src/parser/type/TypeInt.java
+++ b/prism/src/parser/type/TypeInt.java
@@ -26,6 +26,8 @@
 
 package parser.type;
 
+import prism.PrismLangException;
+
 public class TypeInt extends Type 
 {
 	private static TypeInt singleton;
@@ -54,8 +56,18 @@ public class TypeInt extends Type
 		return singleton;
 	}
 	
+	@Override
 	public boolean canAssign(Type type)
 	{
 		return (type instanceof TypeInt);
 	}
+	
+	@Override
+	public Object castValueTo(Object value) throws PrismLangException
+	{
+		if (value instanceof Integer)
+			return value;
+		else
+			throw new PrismLangException("Can't convert " + value.getClass() + " to type " + getTypeString());
+	}
 }