[DAG-copy] Implement deep-copying the AST without unfolding the DAG

After certain replacements, e.g., formula substitution, the AST becomes a directed acyclic graph.
On copying wewant to preserve this structure.
The identification of duplicates is non-local since duplicates may appear everywhere in the AST/DAG.

The implementation introduces a new visitor to keep track of duplicate nodes
and makes copying a two-step process:
1. Cloning a node and its internal container types via Object::clone
2. Deep-copying AST child nodes using the visitor

Author: Steffen Märcker

prism/src/parser/ast/ASTElement.java

@@ -186,7 +186,25 @@ public String getEndString()
 	/**
 	 * Perform a deep copy.
 	 */
-	public abstract ASTElement deepCopy();
+	public ASTElement deepCopy()
+	{
+		try {
+			return new DeepCopy().copy(this);
+		} catch (PrismLangException e) {
+			throw new Error(e);
+		}
+	}
+
+	/**
+	 * Perform a deep copy of all internal ASTElements using a deep copy visitor.
+	 * This method is usually called after {@code clone()} and must return the receiver.
+	 *
+	 * @param copier the copy visitor
+	 * @returns the receiver with deep-copied subcomponents
+	 * @throws PrismLangException
+	 * @see #clone()
+	 */
+	public abstract ASTElement deepCopy(DeepCopy copier) throws PrismLangException;
 
 	/**
 	 * Perform a shallow copy of the receiver and

prism/src/parser/ast/Command.java

@@ -137,19 +137,14 @@ public String toString()
 		s += "] " + guard + " -> " + updates;
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public Command deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Command ret = new Command();
-		ret.setSynch(getSynch());
-		ret.setSynchIndex(getSynchIndex());
-		ret.setGuard(getGuard().deepCopy());
-		ret.setUpdates((Updates)getUpdates().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		guard   = copier.copy(guard);
+		updates = copier.copy(updates);
+
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/ConstantList.java

@@ -429,24 +429,17 @@ public String toString()
 
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public ConstantList deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		int i, n;
-		ConstantList ret = new ConstantList();
-		n = size();
-		for (i = 0; i < n; i++) {
-			Expression constantNew = (getConstant(i) == null) ? null : getConstant(i).deepCopy();
-			ret.addConstant((ExpressionIdent)getConstantNameIdent(i).deepCopy(), constantNew, getConstantType(i));
-		}
-		ret.setPosition(this);
-		return ret;
+		copier.copyAll(constants);
+		copier.copyAll(nameIdents);
+
+		return this;
 	}
 
-@SuppressWarnings("unchecked")
+	@SuppressWarnings("unchecked")
 	@Override
 	public ConstantList clone()
 	{

prism/src/parser/ast/Declaration.java

@@ -138,17 +138,13 @@ public String toString()
 		return s;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public Declaration deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Declaration ret = new Declaration(getName(), (DeclarationType)getDeclType().deepCopy());
-		if (getStart() != null)
-			ret.setStart(getStart().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		declType = copier.copy(declType);
+		start    = copier.copy(start);
+
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/DeclarationArray.java

@@ -29,6 +29,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationArray extends DeclarationType
@@ -121,18 +122,14 @@ public String toString()
 		return "array [" + low + ".." + high + "] of " + subtype;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationArray deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Expression lowCopy = (low == null) ? null : low.deepCopy();
-		Expression highCopy = (high == null) ? null : high.deepCopy();
-		DeclarationType subtypeCopy = (DeclarationType) subtype.deepCopy();
-		DeclarationArray ret = new DeclarationArray(lowCopy, highCopy, subtypeCopy);
-		ret.setPosition(this);
-		return ret;
+		low     = copier.copy(low);
+		high    = copier.copy(high);
+		subtype = copier.copy(subtype);
+
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/DeclarationBool.java

@@ -29,6 +29,7 @@
 
 import parser.type.TypeBool;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationBool extends DeclarationType
@@ -75,14 +76,10 @@ public String toString()
 		return "bool";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+	@Override
+	public DeclarationBool deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		DeclarationBool ret = new DeclarationBool();
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/DeclarationClock.java

@@ -28,6 +28,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationClock extends DeclarationType
@@ -78,15 +79,10 @@ public String toString()
 		return "clock";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationClock deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		DeclarationClock ret = new DeclarationClock();
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/DeclarationInt.java

@@ -29,6 +29,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationInt extends DeclarationType
@@ -106,17 +107,13 @@ public String toString()
 		return "[" + low + ".." + high + "]";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationInt deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Expression lowCopy = (low == null) ? null : low.deepCopy();
-		Expression highCopy = (high == null) ? null : high.deepCopy();
-		DeclarationInt ret = new DeclarationInt(lowCopy, highCopy);
-		ret.setPosition(this);
-		return ret;
+		low = copier.copy(low);
+		high = copier.copy(high);
+
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/DeclarationIntUnbounded.java

@@ -28,6 +28,7 @@
 
 import parser.type.*;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 public class DeclarationIntUnbounded extends DeclarationType
@@ -78,15 +79,10 @@ public String toString()
 		return "int";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationIntUnbounded deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		DeclarationIntUnbounded ret = new DeclarationIntUnbounded();
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override

prism/src/parser/ast/Expression.java

@@ -78,10 +78,11 @@ public String getResultName()
 
 	// Override version of deepCopy() from superclass ASTElement (to reduce casting).
 
-	/**
-	 * Perform a deep copy.
-	 */
-	public abstract Expression deepCopy();
+	@Override
+	public Expression deepCopy()
+	{
+		return (Expression) super.deepCopy();
+	}
 
 	// Utility methods: