tacas: Final touches

lorenzleutgeb · Oct 23, 2020 · 4cf83a5 · 4cf83a5
1 parent bbda68b
commit 4cf83a5
Show file tree

Hide file tree

Showing 20 changed files with 320 additions and 275 deletions.
diff --git a/typechecker/build.gradle.kts b/typechecker/build.gradle.kts
@@ -128,12 +128,14 @@ tasks.nativeImage {
     jarTask = tasks.shadowJar.get()
     arguments(
             "--no-fallback",
-            "--enable-all-security-services",
+            // "--enable-all-security-services",
             "--initialize-at-build-time=com.microsoft.z3.Native",
             "--report-unsupported-elements-at-runtime",
-            "-H:+ReportExceptionStackTraces",
-            "--static",
-            "-H:+StaticExecutableWithDynamicLibC"
+            "-H:+ReportExceptionStackTraces"
+            // "--static",
+            // "--libc=musl",
+            // "-H:+JNI"
+            // "-H:+StaticExecutableWithDynamicLibC"
     )
 }
 

diff --git a/typechecker/src/main/antlr/xyz/leutgeb/lorenz/lac/antlr/Annotation.g4 b/typechecker/src/main/antlr/xyz/leutgeb/lorenz/lac/antlr/Annotation.g4
@@ -19,7 +19,8 @@ index : NUMBER # rankIndex
       | PAREN_OPEN elements+=NUMBER* PAREN_CLOSE # otherIndex
       ;
 
-NUMBER : ('0' .. '9' );
+// NUMBER : ('0' .. '9' );
+NUMBER : '0' | ('1'..'9') ('0'..'9')*;
 SLASH : '/' ;
 TIMES : '*';
 CURLY_OPEN : '{';

diff --git a/typechecker/src/main/antlr/xyz/leutgeb/lorenz/lac/antlr/Splay.g4 b/typechecker/src/main/antlr/xyz/leutgeb/lorenz/lac/antlr/Splay.g4
@@ -11,11 +11,11 @@ program: (func)* EOF;
 // Function declaration (with list of arguments):
 func : signature? name=IDENTIFIER (args+=IDENTIFIER)* ASSIGN body=expression SEMICOLON?;
 
-signature : name=IDENTIFIER DOUBLECOLON (constraints DOUBLE_ARROW)? arrow;
+signature : name=IDENTIFIER DOUBLECOLON (constraints DOUBLE_ARROW)? from=productType ARROW to=namedType (PIPE annotatedAnnotation=combinedFunctionAnnotation)? ;
 
-arrow : from=productType ARROW to=namedType # simpleArrow
-      | from=productType PIPE fromAnnotation=annotation ARROW to=namedType PIPE toAnnotation=annotation # annotatedArrow
-      ;
+combinedFunctionAnnotation : SQUARE_OPEN with=functionAnnotation (COMMA CURLY_OPEN (without+=functionAnnotation (COMMA without+=functionAnnotation)*)? CURLY_CLOSE)? SQUARE_CLOSE ;
+
+functionAnnotation : from=annotation ARROW to=annotation ;
 
 variableType : IDENTIFIER ;
 
@@ -72,7 +72,7 @@ pattern : PAREN_OPEN left=IDENTIFIER COMMA middle=IDENTIFIER COMMA right=IDENTIF
 
 node: PAREN_OPEN left=expression COMMA middle=expression COMMA right=expression PAREN_CLOSE ;
 
-identifier : LEAF | IDENTIFIER | ANONYMOUS_IDENTIFIER | DERIVED_IDENTIFIER;
+identifier : LEAF | IDENTIFIER ;
 
 ANONYMOUS_IDENTIFIER : '_';
 DOT : '.';
@@ -116,11 +116,6 @@ BOOL : 'Bool' | 'Bo';
 TYC_ORD : 'Ord';
 TYC_EQ : 'Eq';
 
-// TODO(lorenz.leutgeb): Add greek alphabet and lowercase letters.
-
-SUBSCRIPT_NUMBER : [\u2080-\u2089];
-DERIVED_IDENTIFIER : '∂' SUBSCRIPT_NUMBER+;
-
 IDENTIFIER : (('A' .. 'Z' | 'a'..'z' | 'α' | 'β' | 'γ' | 'δ' | 'ε' | '∂') ( 'A'..'Z' | 'a'..'z' | 'α' | 'β' | 'γ' | 'δ' | 'ε' | '∂' | '0'..'9' | '_' | '\'' | '.' )*) ;
 TYPE : ('A'..'Z') ( 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' )*;
 NUMBER : '0' | ('1'..'9') ('0'..'9')*;

diff --git a/typechecker/src/main/gen/AnnotationLexer.java b/typechecker/src/main/gen/AnnotationLexer.java
@@ -147,33 +147,35 @@ public ATN getATN() {
   }
 
   public static final String _serializedATN =
-      "\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\24g\b\1\4\2\t\2\4"
+      "\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\24o\b\1\4\2\t\2\4"
           + "\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t"
           + "\13\4\f\t\f\4\r\t\r\4\16\t\16\4\17\t\17\4\20\t\20\4\21\t\21\4\22\t\22"
-          + "\4\23\t\23\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\6\3\6\3\7\3\7\3\b\3\b\3\t"
-          + "\3\t\3\n\3\n\3\13\3\13\3\f\3\f\3\f\3\r\3\r\3\r\3\r\5\rC\n\r\3\16\3\16"
-          + "\7\16G\n\16\f\16\16\16J\13\16\3\17\3\17\3\20\3\20\3\21\3\21\3\22\3\22"
-          + "\3\22\3\22\3\22\7\22W\n\22\f\22\16\22Z\13\22\3\22\3\22\3\22\3\22\3\22"
-          + "\3\23\6\23b\n\23\r\23\16\23c\3\23\3\23\3X\2\24\3\3\5\4\7\5\t\6\13\7\r"
-          + "\b\17\t\21\n\23\13\25\f\27\r\31\16\33\17\35\20\37\21!\22#\23%\24\3\2\5"
-          + "\6\2AAC\\aac|\b\2..\62<C\\aac}\177\177\5\2\13\f\16\17\"\"\2k\2\3\3\2\2"
-          + "\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3"
-          + "\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\2\27\3\2\2\2\2\31\3\2\2"
-          + "\2\2\33\3\2\2\2\2\35\3\2\2\2\2\37\3\2\2\2\2!\3\2\2\2\2#\3\2\2\2\2%\3\2"
-          + "\2\2\3\'\3\2\2\2\5)\3\2\2\2\7+\3\2\2\2\t-\3\2\2\2\13/\3\2\2\2\r\61\3\2"
-          + "\2\2\17\63\3\2\2\2\21\65\3\2\2\2\23\67\3\2\2\2\259\3\2\2\2\27;\3\2\2\2"
-          + "\31B\3\2\2\2\33D\3\2\2\2\35K\3\2\2\2\37M\3\2\2\2!O\3\2\2\2#Q\3\2\2\2%"
-          + "a\3\2\2\2\'(\4\62;\2(\4\3\2\2\2)*\7\61\2\2*\6\3\2\2\2+,\7,\2\2,\b\3\2"
-          + "\2\2-.\7}\2\2.\n\3\2\2\2/\60\7\177\2\2\60\f\3\2\2\2\61\62\7]\2\2\62\16"
-          + "\3\2\2\2\63\64\7_\2\2\64\20\3\2\2\2\65\66\7=\2\2\66\22\3\2\2\2\678\7."
-          + "\2\28\24\3\2\2\29:\7#\2\2:\26\3\2\2\2;<\7/\2\2<=\7@\2\2=\30\3\2\2\2>C"
-          + "\7\u21a8\2\2?@\7~\2\2@A\7/\2\2AC\7@\2\2B>\3\2\2\2B?\3\2\2\2C\32\3\2\2"
-          + "\2DH\t\2\2\2EG\t\3\2\2FE\3\2\2\2GJ\3\2\2\2HF\3\2\2\2HI\3\2\2\2I\34\3\2"
-          + "\2\2JH\3\2\2\2KL\7B\2\2L\36\3\2\2\2MN\7*\2\2N \3\2\2\2OP\7+\2\2P\"\3\2"
-          + "\2\2QR\7*\2\2RS\7,\2\2SX\3\2\2\2TW\5#\22\2UW\13\2\2\2VT\3\2\2\2VU\3\2"
-          + "\2\2WZ\3\2\2\2XY\3\2\2\2XV\3\2\2\2Y[\3\2\2\2ZX\3\2\2\2[\\\7,\2\2\\]\7"
-          + "+\2\2]^\3\2\2\2^_\b\22\2\2_$\3\2\2\2`b\t\4\2\2a`\3\2\2\2bc\3\2\2\2ca\3"
-          + "\2\2\2cd\3\2\2\2de\3\2\2\2ef\b\23\2\2f&\3\2\2\2\b\2BHVXc\3\2\3\2";
+          + "\4\23\t\23\3\2\3\2\3\2\7\2+\n\2\f\2\16\2.\13\2\5\2\60\n\2\3\3\3\3\3\4"
+          + "\3\4\3\5\3\5\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3\t\3\n\3\n\3\13\3\13\3\f\3\f"
+          + "\3\f\3\r\3\r\3\r\3\r\5\rK\n\r\3\16\3\16\7\16O\n\16\f\16\16\16R\13\16\3"
+          + "\17\3\17\3\20\3\20\3\21\3\21\3\22\3\22\3\22\3\22\3\22\7\22_\n\22\f\22"
+          + "\16\22b\13\22\3\22\3\22\3\22\3\22\3\22\3\23\6\23j\n\23\r\23\16\23k\3\23"
+          + "\3\23\3`\2\24\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\27\r\31\16"
+          + "\33\17\35\20\37\21!\22#\23%\24\3\2\5\6\2AAC\\aac|\b\2..\62<C\\aac}\177"
+          + "\177\5\2\13\f\16\17\"\"\2u\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2"
+          + "\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2"
+          + "\25\3\2\2\2\2\27\3\2\2\2\2\31\3\2\2\2\2\33\3\2\2\2\2\35\3\2\2\2\2\37\3"
+          + "\2\2\2\2!\3\2\2\2\2#\3\2\2\2\2%\3\2\2\2\3/\3\2\2\2\5\61\3\2\2\2\7\63\3"
+          + "\2\2\2\t\65\3\2\2\2\13\67\3\2\2\2\r9\3\2\2\2\17;\3\2\2\2\21=\3\2\2\2\23"
+          + "?\3\2\2\2\25A\3\2\2\2\27C\3\2\2\2\31J\3\2\2\2\33L\3\2\2\2\35S\3\2\2\2"
+          + "\37U\3\2\2\2!W\3\2\2\2#Y\3\2\2\2%i\3\2\2\2\'\60\7\62\2\2(,\4\63;\2)+\4"
+          + "\62;\2*)\3\2\2\2+.\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\60\3\2\2\2.,\3\2\2\2/"
+          + "\'\3\2\2\2/(\3\2\2\2\60\4\3\2\2\2\61\62\7\61\2\2\62\6\3\2\2\2\63\64\7"
+          + ",\2\2\64\b\3\2\2\2\65\66\7}\2\2\66\n\3\2\2\2\678\7\177\2\28\f\3\2\2\2"
+          + "9:\7]\2\2:\16\3\2\2\2;<\7_\2\2<\20\3\2\2\2=>\7=\2\2>\22\3\2\2\2?@\7.\2"
+          + "\2@\24\3\2\2\2AB\7#\2\2B\26\3\2\2\2CD\7/\2\2DE\7@\2\2E\30\3\2\2\2FK\7"
+          + "\u21a8\2\2GH\7~\2\2HI\7/\2\2IK\7@\2\2JF\3\2\2\2JG\3\2\2\2K\32\3\2\2\2"
+          + "LP\t\2\2\2MO\t\3\2\2NM\3\2\2\2OR\3\2\2\2PN\3\2\2\2PQ\3\2\2\2Q\34\3\2\2"
+          + "\2RP\3\2\2\2ST\7B\2\2T\36\3\2\2\2UV\7*\2\2V \3\2\2\2WX\7+\2\2X\"\3\2\2"
+          + "\2YZ\7*\2\2Z[\7,\2\2[`\3\2\2\2\\_\5#\22\2]_\13\2\2\2^\\\3\2\2\2^]\3\2"
+          + "\2\2_b\3\2\2\2`a\3\2\2\2`^\3\2\2\2ac\3\2\2\2b`\3\2\2\2cd\7,\2\2de\7+\2"
+          + "\2ef\3\2\2\2fg\b\22\2\2g$\3\2\2\2hj\t\4\2\2ih\3\2\2\2jk\3\2\2\2ki\3\2"
+          + "\2\2kl\3\2\2\2lm\3\2\2\2mn\b\23\2\2n&\3\2\2\2\n\2,/JP^`k\3\2\3\2";
   public static final ATN _ATN = new ATNDeserializer().deserialize(_serializedATN.toCharArray());
 
   static {

diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/FunctionDefinition.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/FunctionDefinition.java
@@ -17,12 +17,12 @@
 import guru.nidi.graphviz.engine.Graphviz;
 import guru.nidi.graphviz.model.Graph;
 import guru.nidi.graphviz.model.Node;
-import java.awt.*;
 import java.io.OutputStream;
 import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
@@ -66,7 +66,9 @@ public class FunctionDefinition {
   private FunctionSignature inferredSignature;
   private FunctionSignature annotatedSignature;
   // private FunctionAnnotation inferredAnnotation;
-  private Set<FunctionAnnotation> cfAnnotations;
+
+  @Deprecated private Set<FunctionAnnotation> cfAnnotations;
+
   private org.jgrapht.Graph<Identifier, SizeEdge> sizeAnalysis = null;
 
   public FunctionDefinition(
@@ -107,7 +109,7 @@ public void infer(UnificationContext context) throws UnificationError, TypeError
     // TODO(lorenz.leutgeb): Maybe do this in stub?
     if (annotatedSignature != null) {
       if (annotatedSignature.getType().getFrom().getElements().size() != arguments.size()) {
-        throw new TypeError();
+        throw new TypeError("expected " + arguments.size() + " for " + getFullyQualifiedName());
       }
       for (int i = 0; i < arguments.size(); i++) {
         Type ty = annotatedSignature.getType().getFrom().getElements().get(i);
@@ -256,28 +258,25 @@ public void stubAnnotations(
               Annotation.zero(inferredAnnotation.from.size(), "cfargszero"),
               Annotation.zero(inferredAnnotation.to.size(), "cfreturnzero"));
 
-      if (cf) {
-        this.cfAnnotations = Set.of(costFreeAnnotation, costFreeAnnotation2, zeroAnnotation);
-      } else {
-        this.cfAnnotations = emptySet();
-      }
+      Set<FunctionAnnotation> cfAnnotations =
+          cf ? Set.of(costFreeAnnotation, costFreeAnnotation2, zeroAnnotation) : emptySet();
+
+      final var combined = new CombinedFunctionAnnotation(inferredAnnotation, cfAnnotations);
       // TODO: Sort this out...
       if (infer || annotatedSignature.getAnnotation().isEmpty()) {
         inferredSignature =
             new FunctionSignature(
                 inferredSignature.getConstraints(),
                 inferredSignature.getType(),
-                Optional.of(inferredAnnotation));
+                Optional.of(combined));
       } else {
         inferredSignature =
             new FunctionSignature(
                 inferredSignature.getConstraints(),
                 inferredSignature.getType(),
                 annotatedSignature.getAnnotation());
       }
-      functionAnnotations.put(
-          getFullyQualifiedName(),
-          new CombinedFunctionAnnotation(inferredAnnotation, cfAnnotations));
+      functionAnnotations.put(getFullyQualifiedName(), combined);
     } else {
       if (predefined.withCost.from.size() != treeLikeArguments.size()) {
         throw new IllegalArgumentException(
@@ -301,8 +300,7 @@ public void stubAnnotations(
           new FunctionSignature(
               inferredSignature.getConstraints(),
               inferredSignature.getType(),
-              Optional.of(predefined.withCost));
-      cfAnnotations = predefined.withoutCost;
+              Optional.of(predefined));
     }
   }
 
@@ -314,34 +312,34 @@ public Set<TypeVariable> runaway() {
 
   public Obligation getTypingObligation(int cost) {
     return new Obligation(
-        new AnnotatingContext(treeLikeArguments(), inferredSignature.getAnnotation().get().from),
+        new AnnotatingContext(
+            treeLikeArguments(), inferredSignature.getAnnotation().get().withCost.from),
         body,
-        inferredSignature.getAnnotation().get().to,
+        inferredSignature.getAnnotation().get().withCost.to,
         cost);
   }
 
-  public String getAnnotationString() {
-    if (inferredSignature.getAnnotation().isEmpty()) {
-      throw new IllegalStateException();
-    }
-
+  public String getInferredSignatureString() {
     return moduleName
         + "."
         + name
-        + (arguments.isEmpty() ? "" : " ")
-        + String.join(" ", arguments)
-        + " | "
-        + new CombinedFunctionAnnotation(inferredSignature.getAnnotation().get(), cfAnnotations);
+        + " ∷ "
+        + inferredSignature.getType()
+        + inferredSignature.getAnnotation().map(Objects::toString).map(x -> " | " + x).orElse("");
   }
 
-  public String getMockedAnnotationString(CombinedFunctionAnnotation annotation) {
+  public String getAnnotatedSignatureString() {
     return moduleName
         + "."
         + name
-        + (arguments.isEmpty() ? "" : " ")
-        + String.join(" ", arguments)
-        + " | "
-        + annotation;
+        + " ∷ "
+        + inferredSignature.getType()
+        + annotatedSignature.getAnnotation().map(Objects::toString).map(x -> " | " + x).orElse("");
+  }
+
+  @Deprecated
+  public String getMockedAnnotationString(CombinedFunctionAnnotation annotation) {
+    return moduleName + "." + name + " ∷ " + inferredSignature.getType() + " | " + annotation;
   }
 
   public void printTo(PrintStream out) {
@@ -381,9 +379,14 @@ public void toGraph(OutputStream out) {
                       turn(
                           name,
                           inferredSignature.toString().replace(">", "\\>").replace("<", "\\<"),
-                          inferredSignature.getAnnotation().get().from.getNameAndId()
+                          inferredSignature.getAnnotation().get().withCost.from.getNameAndId()
                               + " → "
-                              + inferredSignature.getAnnotation().get().to.getNameAndId())));
+                              + inferredSignature
+                                  .getAnnotation()
+                                  .get()
+                                  .withCost
+                                  .to
+                                  .getNameAndId())));
       Graph result = body.toGraph(g, root);
       var viz = Graphviz.fromGraph(result);
       viz.render(Format.SVG).toOutputStream(out);
@@ -428,4 +431,8 @@ public String toString() {
         + " = "
         + body.terminalOrBox();
   }
+
+  public String getSimpleSignatureString() {
+    return moduleName + "." + name + " ∷ " + inferredSignature.getType();
+  }
 }
diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java
@@ -45,7 +45,7 @@ public class Program {
   // Note that this could also be List<Set<...>> since the order of nodes within the same
   // SCC doesn't really matter. However we chose to still sort them to get consistent outputs
   // without resorting in multiple places.
-  private final List<List<String>> order;
+  @Getter private final List<List<String>> order;
 
   @Getter @Setter private String name;
   private final Path basePath;
@@ -175,7 +175,7 @@ public Optional<Prover> proveWithTactics(
             prover.setWeakenAggressively(false);
           }
 
-          for (var cfAnnotation : fd.getCfAnnotations()) {
+          for (var cfAnnotation : fd.getInferredSignature().getAnnotation().get().withoutCost) {
             if (cfAnnotation.isZero()) {
               log.debug("Skipping {}", cfAnnotation);
               continue;
@@ -196,7 +196,7 @@ public Optional<Prover> proveWithTactics(
 
             if (tactics.containsKey(fd.getFullyQualifiedName())) {
               try {
-                log.info("Using tactic to prove cf typing!");
+                log.debug("Using tactic to prove cf typing!");
                 prover.read(cfRoot, tactics.get(fd.getFullyQualifiedName()));
               } catch (IOException e) {
                 throw new RuntimeException(e);
@@ -278,16 +278,24 @@ public void mockIngest(Optional<Map<Coefficient, KnownCoefficient>> solution) {
                                   .getInferredSignature()
                                   .getAnnotation()
                                   .get()
+                                  .withCost
                                   .from
                                   .substitute(solution.get()),
                               functionDefinitions
                                   .get(fqn)
                                   .getInferredSignature()
                                   .getAnnotation()
                                   .get()
+                                  .withCost
                                   .to
                                   .substitute(solution.get())),
-                          functionDefinitions.get(fqn).getCfAnnotations().stream()
+                          functionDefinitions
+                              .get(fqn)
+                              .getInferredSignature()
+                              .getAnnotation()
+                              .get()
+                              .withoutCost
+                              .stream()
                               .map(annotation -> annotation.substitute(solution.get()))
                               .collect(Collectors.toSet()))));
         }
@@ -334,47 +342,29 @@ private Set<String> calledFunctionNames() {
   public void printAllSimpleSignaturesInOrder(PrintStream out) {
     for (int i = 0; i < order.size(); i++) {
       final var stratum = order.get(i);
-      final var multiple = stratum.size() > 1;
-
-      if (multiple) {
-        out.println(stratum.stream().collect(joining(", ")) + ":");
-      }
-
       for (var fqn : stratum) {
         FunctionDefinition fd = functionDefinitions.get(fqn);
-        out.println(
-            (multiple ? "\t" : "")
-                + fd.getFullyQualifiedName()
-                + " ∷ "
-                + fd.getInferredSignature());
+        out.println(fd.getSimpleSignatureString());
       }
     }
   }
 
   public void printAllAnnotatedSignaturesInOrder(PrintStream out) {
     for (int i = 0; i < order.size(); i++) {
       final var stratum = order.get(i);
-
       for (var fqn : stratum) {
         FunctionDefinition fd = functionDefinitions.get(fqn);
-        if (fd.getInferredSignature().getAnnotation().isPresent()) {
-          out.println(fd.getFullyQualifiedName() + " ∷ " + fd.getAnnotatedSignature());
-        }
+        out.println(fd.getAnnotatedSignatureString());
       }
     }
   }
 
   public void printAllInferredSignaturesInOrder(PrintStream out) {
     for (int i = 0; i < order.size(); i++) {
       final var stratum = order.get(i);
-
       for (var fqn : stratum) {
         FunctionDefinition fd = functionDefinitions.get(fqn);
-        if (fd.getInferredSignature().getAnnotation().isPresent()) {
-          out.println(fd.getFullyQualifiedName() + " ∷ " + fd.getInferredSignature());
-        } else {
-          out.println(fd.getFullyQualifiedName() + " ∷ ?");
-        }
+        out.println(fd.getInferredSignatureString());
       }
     }
   }