Tidy PO listing and subtype obligation tweak

nickbattle · Oct 28, 2023 · 7ca363c · 7ca363c
1 parent ba820f4
commit 7ca363c
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 9 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java
@@ -129,6 +129,7 @@ public void renumber(int from)
 
 	public void typeCheck(TCModule tcmodule, MultiModuleEnvironment menv)
 	{
+		renumber();
 		for (ProofObligation po: this)
 		{
 			try
@@ -142,7 +143,7 @@ public void typeCheck(TCModule tcmodule, MultiModuleEnvironment menv)
 			{
 				Console.err.println(po.toString());
 				TypeChecker.printErrors(Console.err);
-				Console.err.println(e.getMessage());
+				Console.err.println(e.toString());
 			}
 		}
 	}
@@ -205,22 +206,19 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env
 
 			switch (message.number)
 			{
-				case 3350:	// "Polymorphic function has not been instantiated"
-					iter.remove();
-					obligation.isCheckable = false;			// No point
-					break;
-
 				case 3182:	// "Name 'xxx' is not in scope"
 					if (message.message.startsWith("Name 'measure_"))
 					{
 						// Probably an implicit missing measure
 						iter.remove();
-						obligation.isCheckable = false;		// No point
+						obligation.status = POStatus.FAILED;
+						obligation.isCheckable = false;
+						obligation.countermessage = "Error: Missing measure function";
 					}
 					break;
 
-				case 3433:	// Parameter type @T not defined, just ignore
-				case 3336:	// "Illegal use of RESULT reserved identifier"
+				case 3433:	// Parameter type @T not defined
+				case 3336:	// Illegal use of RESULT reserved identifier
 					iter.remove();
 					break;
 

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java
@@ -298,6 +298,11 @@ else if (etype instanceof TCNamedType)
 					sb.append(s);
 					sb.append(")");
 				}
+				else
+				{
+					sb.append(prefix);
+					addIs(sb, exp, etype);
+				}
 			}
 			else if (etype instanceof TCRecordType)
 			{