more printing

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java

@@ -22,7 +22,6 @@
 import org.key_project.util.collection.ImmutableList;
 
 import java.util.List;
-import java.util.Map;
 import java.util.stream.Collectors;
 
 /**
@@ -86,25 +85,41 @@ private void print(List<TextualJMLConstruct> spec) {
                 case TextualJMLClassAxiom c -> print(c.getModifiers(), c.getAxiom().first);
                 case TextualJMLClassInv c -> print(c.getModifiers(), c.getInv());
                 case TextualJMLDepends c -> print(c.getModifiers(), c.getDepends());
-                case TextualJMLFieldDecl c -> {}
+                case TextualJMLFieldDecl c -> {
+                }
                 case TextualJMLInitially c -> print(c.getModifiers(), c.getInv().first);
                 case TextualJMLMergePointDecl c -> print(c.getModifiers(), c.getMergeProc());
                 case TextualJMLMethodDecl c -> print(c.getModifiers(), c.getDecl());
                 case TextualJMLModifierList c -> print(c.getModifiers());
                 case TextualJMLRepresents c -> print(c.getModifiers(), c.getRepresents().first);
                 case TextualJMLSetStatement c -> print(c.getAssignment());
-                case TextualJMLSpecCase c -> print(c);
+                case TextualJMLSpecCase c -> print(c.getModifiers(), c);
                 default -> throw new IllegalStateException("Unexpected value: " + construct);
             }
         }
     }
 
     private void print(ImmutableList<JMLModifier> modifiers, ImmutableList<LabeledParserRuleContext> depends) {
-
+        printer.print("\n/*@ ");
+        print(modifiers);
+        printer.print(" ");
+        depends.forEach(it -> print(it.first));
+        printer.print("*/\n");
+    }
+
+    private void print(ImmutableList<JMLModifier> modifiers, TextualJMLSpecCase specCase) {
+        printer.print("/*@ ");
+        print(modifiers);
+        printer.print(" ");
+        printer.print(specCase.getBehavior().toString());
+        specCase.getClauses().forEach(it -> {
+                    print(it);
+                    printer.print("\n");
+                }
+        );
+        printer.print("\n*/");
     }
-    private void print(TextualJMLSpecCase c) {
 
-    }
 
     private void print(ImmutableList<JMLModifier> modifiers, @Nullable ParserRuleContext first) {
         if (first == null) return;

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java

@@ -95,6 +95,10 @@ public ImmutableList<LabeledParserRuleContext> getDecreases() {
         return getList(DECREASES);
     }
 
+    public Iterable<ParserRuleContext> getClauses() {
+        return clauses.stream().map(it -> it.ctx.first).collect(Collectors.toList());
+    }
+
     /**
      * Heap-independent clauses
      */