Clean polymorphic getProofObligations

nickbattle · Oct 18, 2023 · db1bc1a · db1bc1a
1 parent 9a9e51a
commit db1bc1a
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 26 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java
@@ -138,7 +138,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 		TCNameList pids = new TCNameList();
 		boolean matchNeeded = false;
-		boolean polymorphic = (typeParams != null && !typeParams.isEmpty());
 
 		for (POPatternList pl: paramPatternList)
 		{
@@ -153,12 +152,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 		}
 
-		if (polymorphic)
-		{
-			// Cannot generate POs for polymorphic fns (yet), so unchecked
-			// ctxt.push(new PONoCheckContext());
-		}
-
 		if (type.hasTotal())
 		{
 			ctxt.push(new POFunctionDefinitionContext(this, true));
@@ -207,12 +200,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 		ctxt.pop();
 
-		if (polymorphic)
-		{
-			// Cannot generate POs for polymorphic fns (yet), so unchecked
-			// ctxt.pop();
-		}
-
 		if (annotations != null) annotations.poAfter(this, obligations, ctxt);
 		return obligations;
 	}

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java
@@ -135,7 +135,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 				(annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList();
 		TCNameList pids = new TCNameList();
 		boolean matchNeeded = false;
-		boolean polymorphic = (typeParams != null && !typeParams.isEmpty());
 
 		for (POPatternListTypePair pltp: parameterPatterns)
 		{
@@ -150,12 +149,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 		}
 
-		if (polymorphic)
-		{
-			// Cannot generate POs for polymorphic fns (yet), so unchecked
-			// ctxt.push(new PONoCheckContext());
-		}
-
 		if (pids.hasDuplicates() || matchNeeded)
 		{
 			obligations.add(new ParameterPatternObligation(this, ctxt));
@@ -213,12 +206,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			ctxt.pop();
 		}
 
-		if (polymorphic)
-		{
-			// Cannot generate POs for polymorphic fns (yet), so unchecked
-			// ctxt.pop();
-		}
-
 		if (annotations != null) annotations.poAfter(this, obligations, ctxt);
 		return obligations;
 	}