Fix field names in Isabelle translation (#3795)

Author: unp1

keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/FieldHandler.java

@@ -12,6 +12,7 @@
 import java.util.regex.Pattern;
 
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.JavaDLFieldNames;
 
 import org.key_project.logic.Name;
 import org.key_project.logic.Namespace;
@@ -58,8 +59,11 @@ public boolean canHandle(Operator op) {
     public StringBuilder handle(IsabelleMasterHandler trans, Term term) {
         if (trans.isNewSymbol(term)) {
             Operator op = term.op();
-            Matcher m = Pattern.compile("<(.*?)>").matcher(op.name().toString());
-            String fieldName = op.name().toString().replace("::$", "_").replace(".", "_");
+            Matcher m =
+                Pattern.compile(Pattern.quote("" + JavaDLFieldNames.IMPLICIT_NAME_PREFIX) + "(.*?)")
+                        .matcher(op.name().toString());
+            String fieldName = op.name().toString()
+                    .replace(JavaDLFieldNames.IMPLICIT_FIELD_INFIX, "_").replace(".", "_");
             if (m.find()) {
                 fieldName = m.group(1);
             }

keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/translation/ObserverFunctionHandler.java

@@ -9,6 +9,7 @@
 import java.util.regex.Pattern;
 
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.JavaDLFieldNames;
 import de.uka.ilkd.key.logic.op.ObserverFunction;
 
 import org.key_project.logic.Term;
@@ -33,16 +34,23 @@ public boolean canHandle(Operator op) {
     @Override
     public StringBuilder handle(IsabelleMasterHandler trans, Term term) {
         if (trans.isNewSymbol(term)) {
-            Operator op = term.op();
-            Matcher m = Pattern.compile("<(.*?)>").matcher(op.name().toString());
+            String opName = term.op().name().toString();
+            Matcher m = Pattern
+                    .compile(Pattern.quote("" + JavaDLFieldNames.IMPLICIT_NAME_PREFIX) + "(.*?)")
+                    .matcher(opName);
             String functionName;
             if (m.find()) {
                 functionName =
-                    op.name().toString().replace("<" + m.group(1) + ">", "_" + m.group(1))
-                            .replace("::", "_").replace("$", "").replace(".", "_");
+                    opName.replace(JavaDLFieldNames.IMPLICIT_NAME_PREFIX + m.group(1),
+                        "_" + m.group(1))
+                            .replace(JavaDLFieldNames.SEPARATOR, "_")
+                            .replace(JavaDLFieldNames.IMPLICIT_NAME_PREFIX + "", "")
+                            .replace(".", "_");
             } else {
                 functionName =
-                    op.name().toString().replace("::", "_").replace("$", "").replace(".", "_");
+                    opName.replace(JavaDLFieldNames.SEPARATOR, "_")
+                            .replace(JavaDLFieldNames.FIELD_PREFIX + "", "")
+                            .replace(".", "_");
             }
             trans.addSymbolAndDeclaration(term, new StringBuilder(functionName));
         }