Switch Laurel AST to getIonSerializer% format

.gitignore

@@ -41,3 +41,4 @@ bin/
 
 ### Mac OS ###
 .DS_Store
+examples/.jqwik-database

Makefile

@@ -1,3 +1,3 @@
 generate-laurel-ast:
 	rm -rf verifier/src/main/java/org/strata/jverify/laurel
-	cd Strata/StrataCLI && lake exe strata javaGen Laurel org.strata.jverify.laurel ../../verifier/src/main/java
+	cd Strata && lake exe laurelJavaGen org.strata.jverify.laurel ../verifier/src/main/java

verifier/src/main/java/org/strata/jverify/laurel/AstNode.java

@@ -0,0 +1,10 @@
+package org.strata.jverify.laurel;
+
+public record AstNode<T extends ToIon>(T val, FileRange source) implements ToIon {
+    public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var s = ion.newEmptyStruct();
+        s.put("val", val().toIon(ion));
+        s.put("source", (source() != null ? source().toIon(ion) : ion.newNull()));
+        return s;
+    }
+}

verifier/src/main/java/org/strata/jverify/laurel/Body.java

@@ -1,31 +1,53 @@
 package org.strata.jverify.laurel;
 
-public sealed interface Body extends Node permits Body.Body_, Body.ExternalBody {
-    public record Body_(
-        SourceRange sourceRange,
-        StmtExpr body
-    ) implements Body {
+public sealed interface Body extends ToIon permits Body.Transparent, Body.Opaque, Body.Abstract, Body.External {
+    com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion);
+
+    public record Transparent(AstNode<StmtExpr> body) implements Body {
         @Override
-        public java.lang.String operationName() { return "Laurel.body"; }
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("Transparent"));
+        sexp.add(body().toIon(ion));
+        return sexp;
+        }
+    }
 
+    public record Opaque(java.util.List<Condition> postconditions, AstNode<StmtExpr> implementation, java.util.List<AstNode<StmtExpr>> modifies) implements Body {
         @Override
-        public com.amazon.ion.IonSexp toIon(IonSerializer $s) {
-            var sexp = $s.newOp("Laurel.body", sourceRange());
-            sexp.add($s.serialize(body()));
-            return sexp;
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("Opaque"));
+        var _l0 = ion.newEmptyList();
+        for (var e : postconditions()) _l0.add(e.toIon(ion));
+        sexp.add(_l0);
+        sexp.add((implementation() != null ? implementation().toIon(ion) : ion.newNull()));
+        var _l2 = ion.newEmptyList();
+        for (var e : modifies()) _l2.add(e.toIon(ion));
+        sexp.add(_l2);
+        return sexp;
         }
     }
 
-    public record ExternalBody(
-        SourceRange sourceRange
-    ) implements Body {
+    public record Abstract(java.util.List<Condition> postconditions) implements Body {
         @Override
-        public java.lang.String operationName() { return "Laurel.externalBody"; }
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("Abstract"));
+        var _l0 = ion.newEmptyList();
+        for (var e : postconditions()) _l0.add(e.toIon(ion));
+        sexp.add(_l0);
+        return sexp;
+        }
+    }
 
+    public record External() implements Body {
         @Override
-        public com.amazon.ion.IonSexp toIon(IonSerializer $s) {
-            var sexp = $s.newOp("Laurel.externalBody", sourceRange());
-            return sexp;
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("External"));
+
+        return sexp;
         }
     }
 }

verifier/src/main/java/org/strata/jverify/laurel/CompositeType.java

@@ -0,0 +1,18 @@
+package org.strata.jverify.laurel;
+
+public record CompositeType(Identifier name, java.util.List<Identifier> extending, java.util.List<Field> fields, java.util.List<Procedure> instanceProcedures) implements ToIon {
+    public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var s = ion.newEmptyStruct();
+        s.put("name", name().toIon(ion));
+        var _l_extending = ion.newEmptyList();
+        for (var e : extending()) _l_extending.add(e.toIon(ion));
+        s.put("extending", _l_extending);
+        var _l_fields = ion.newEmptyList();
+        for (var e : fields()) _l_fields.add(e.toIon(ion));
+        s.put("fields", _l_fields);
+        var _l_instanceProcedures = ion.newEmptyList();
+        for (var e : instanceProcedures()) _l_instanceProcedures.add(e.toIon(ion));
+        s.put("instanceProcedures", _l_instanceProcedures);
+        return s;
+    }
+}

verifier/src/main/java/org/strata/jverify/laurel/Condition.java

@@ -0,0 +1,11 @@
+package org.strata.jverify.laurel;
+
+public record Condition(AstNode<StmtExpr> condition, java.lang.String summary, boolean free) implements ToIon {
+    public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var s = ion.newEmptyStruct();
+        s.put("condition", condition().toIon(ion));
+        s.put("summary", (summary() != null ? ion.newString(summary()) : ion.newNull()));
+        s.put("free", ion.newBool(free()));
+        return s;
+    }
+}

verifier/src/main/java/org/strata/jverify/laurel/Constant.java

@@ -0,0 +1,11 @@
+package org.strata.jverify.laurel;
+
+public record Constant(Identifier name, AstNode<HighType> type, AstNode<StmtExpr> initializer) implements ToIon {
+    public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var s = ion.newEmptyStruct();
+        s.put("name", name().toIon(ion));
+        s.put("type", type().toIon(ion));
+        s.put("initializer", (initializer() != null ? initializer().toIon(ion) : ion.newNull()));
+        return s;
+    }
+}

verifier/src/main/java/org/strata/jverify/laurel/ConstrainedType.java

@@ -1,22 +1,13 @@
 package org.strata.jverify.laurel;
 
-public sealed interface ConstrainedType extends Node permits ConstrainedType.Of {
-    public record Of(
-        SourceRange sourceRange,
-        java.lang.String name, java.lang.String valueName, LaurelType base, StmtExpr constraint, StmtExpr witness
-    ) implements ConstrainedType {
-        @Override
-        public java.lang.String operationName() { return "Laurel.constrainedType"; }
-
-        @Override
-        public com.amazon.ion.IonSexp toIon(IonSerializer $s) {
-            var sexp = $s.newOp("Laurel.constrainedType", sourceRange());
-            sexp.add($s.serializeIdent(name()));
-            sexp.add($s.serializeIdent(valueName()));
-            sexp.add($s.serialize(base()));
-            sexp.add($s.serialize(constraint()));
-            sexp.add($s.serialize(witness()));
-            return sexp;
-        }
+public record ConstrainedType(Identifier name, AstNode<HighType> base, Identifier valueName, AstNode<StmtExpr> constraint, AstNode<StmtExpr> witness) implements ToIon {
+    public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var s = ion.newEmptyStruct();
+        s.put("name", name().toIon(ion));
+        s.put("base", base().toIon(ion));
+        s.put("valueName", valueName().toIon(ion));
+        s.put("constraint", constraint().toIon(ion));
+        s.put("witness", witness().toIon(ion));
+        return s;
     }
 }

verifier/src/main/java/org/strata/jverify/laurel/ContractType.java

@@ -0,0 +1,45 @@
+package org.strata.jverify.laurel;
+
+public sealed interface ContractType extends ToIon permits ContractType.Reads, ContractType.Modifies, ContractType.Precondition, ContractType.PostCondition {
+    com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion);
+
+    public record Reads() implements ContractType {
+        @Override
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("Reads"));
+
+        return sexp;
+        }
+    }
+
+    public record Modifies() implements ContractType {
+        @Override
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("Modifies"));
+
+        return sexp;
+        }
+    }
+
+    public record Precondition() implements ContractType {
+        @Override
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("Precondition"));
+
+        return sexp;
+        }
+    }
+
+    public record PostCondition() implements ContractType {
+        @Override
+        public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) {
+        var sexp = ion.newEmptySexp();
+        sexp.add(ion.newSymbol("PostCondition"));
+
+        return sexp;
+        }
+    }
+}