PositivityChecker for Haskell

build-aprove.xml

@@ -760,4 +760,21 @@
 			</classpath>
 		</java>
 	</target>
+
+
+
+	<target name="test-all-files">
+		<apply executable="java" failonerror="true">
+			<arg value="-ea" />
+			<arg value="-jar" />
+			<arg path="dist/lib/aprove.jar" />
+			<arg value="-m" />
+			<arg value="-wst" />
+			<arg value="-p" />
+			<arg value="plain"	/>
+
+			<fileset dir="examples/Haskell/full_haskell" includes="**/*.hs" />
+
+		</apply>
+	</target>
 </project>

src/aprove/cli/Main.java

@@ -1,5 +1,6 @@
 package aprove.cli;
 
+import aprove.input.Programs.haskell.StrictPositivityException;
 import gnu.getopt.*;
 
 import java.io.*;
@@ -23,6 +24,8 @@
 import aprove.verification.oldframework.Logic.*;
 import aprove.verification.oldframework.Utility.GenericStructures.*;
 
+import static aprove.verification.complexity.TruthValue.ComplexityYNM.MAYBE;
+
 public class Main {
 
     private final static String HTML_FOOTER = "</BODY></HTML>";

src/aprove/input/Programs/haskell/GraphBuilder.java

@@ -0,0 +1,275 @@
+package aprove.input.Programs.haskell;
+
+import aprove.verification.oldframework.Haskell.BasicTerms.Apply;
+import aprove.verification.oldframework.Haskell.BasicTerms.Cons;
+import aprove.verification.oldframework.Haskell.BasicTerms.Var;
+import aprove.verification.oldframework.Haskell.Declarations.DataDecl;
+import aprove.verification.oldframework.Haskell.Declarations.SynTypeDecl;
+import aprove.verification.oldframework.Haskell.HaskellObject;
+import aprove.verification.oldframework.Haskell.Modules.TyConsEntity;
+import aprove.verification.oldframework.Haskell.Typing.DataCon;
+
+import java.util.*;
+import java.util.stream.IntStream;
+
+public class GraphBuilder {
+    private final OccurrenceGraph graph;
+
+    private String currentDef;
+
+    private final Set<String> datatypeNames;
+
+    private Map<String, Integer> paramIndex;
+
+    private Map<String, TyConsEntity> preludeTyCons;
+
+    // should be read directly from Prelude
+    private Set<String> preludeNames = new LinkedHashSet<>(Set.of(
+            "IO", "Either", "IOResult", "FilePath", "Integer", "ReadS", "Obj", "ShowS",
+            "Int", "Rational", "WHNF", "Maybe", "IOError", "Nat", "Float", "IOFinished", "HugsException",
+            "IOErrorKind", "Char", "Ordering", "Double", "String", "AET", "Ratio"
+    ));
+
+    public GraphBuilder() {
+        this.datatypeNames = new HashSet<>();
+        this.graph = new OccurrenceGraph();
+    }
+
+    public OccurrenceGraph buildFromDataDecl(List<DataDecl> dataDecls, List<SynTypeDecl>  synTypeDecls, Map<String, TyConsEntity> preludeTyConsMap) {
+        this.preludeTyCons = preludeTyConsMap;
+        dataDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText()));
+        synTypeDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText()));
+        synTypeDecls.forEach(this::processSynTypes);
+        for (DataDecl d : dataDecls) {
+            processDataDecl(d, d.getDefType().getToken().getText());
+        }
+        return graph;
+    }
+
+    public OccurrenceGraph buildFromDataDecl(List<DataDecl> dataDecls, List<SynTypeDecl>  synTypeDecls) {
+        dataDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText()));
+        synTypeDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText()));
+        synTypeDecls.forEach(this::processSynTypes);
+        for (DataDecl d : dataDecls) {
+            processDataDecl(d, d.getDefType().getToken().getText());
+        }
+        return graph;
+    }
+
+    public OccurrenceGraph buildFromTyConsEntity(List<TyConsEntity> types) {
+        for (TyConsEntity entity : types) {
+            datatypeNames.add(entity.getName());
+        }
+
+        for (TyConsEntity entity : types) {
+            processDataDecl((DataDecl) entity.getValue(), entity.getName());
+        }
+
+        return graph;
+    }
+
+    private void processSynTypes(SynTypeDecl synTypeDecl) {
+        currentDef = synTypeDecl.getDefType().getToken().getText();
+        paramIndex = new HashMap<>();
+
+        if  (synTypeDecl.getDefType() instanceof Apply apply) {
+            //collect vars from data declaration
+            List<HaskellObject> vars = new ArrayList<>();
+            var _ = flattenApp(apply, vars);
+
+            //add vars to paramIndex with innermost index 0
+            IntStream.range(0, vars.size())
+                    .forEach(index -> paramIndex.put(((Var) vars.get(index)).getSymbol().toString(), index));
+        }
+
+        graph.addNode(
+                new OccurrenceGraph.DefNode(currentDef)
+        );
+
+        walkType(
+                synTypeDecl.getType(),
+                Occurrence.STRICT_POS,
+                new OccurrenceGraph.DefNode(currentDef)
+        );
+
+    }
+
+    private void processDataDecl(DataDecl dd, String name) {
+        //reset
+        currentDef = name;
+        paramIndex = new LinkedHashMap<>();
+
+        if (dd.getDefType() instanceof Apply apply) {
+
+            //collect vars from data declaration
+            List<HaskellObject> vars = new ArrayList<>();
+            var _ = flattenApp(apply, vars);
+
+            //add vars to paramIndex with innermost index 0
+            IntStream.range(0, vars.size())
+                    .forEach(index -> paramIndex.put(((Var) vars.get(index)).getSymbol().toString(), index));
+        }
+        //create node
+        graph.addNode(
+                new OccurrenceGraph.DefNode(currentDef)
+        );
+
+        for (DataCon ctor : dd.getDataCons()) {
+            processConstructor(ctor);
+        }
+
+    }
+
+    /**
+     * Collects arguments from a data declaration and returns the head of the function
+     *
+     * @param app  some Apply (e.g. Foo a b c)
+     * @param args array storing the arguments (e.g. Foo a b c => args = [a, b, c]
+     * @return head (Foo a b c => Foo)
+     */
+    private HaskellObject flattenApp(Apply app, List<HaskellObject> args) {
+        List<HaskellObject> reversed = new ArrayList<>();
+        HaskellObject current = app;
+
+        while (current instanceof Apply apply) {
+            reversed.add(apply.getArgument());
+            current = apply.getFunction();
+        }
+
+        for (int i = reversed.size() - 1; i >= 0; i--) {
+            args.add(reversed.get(i));
+        }
+
+        return current;
+    }
+
+    private void processConstructor(DataCon ctor) {
+        // e.g. data List a = Nil | Cons a (List a)
+        // => ctor = `Cons a (List a)`
+        // => ctor.getTypes() -> ['a', '(List a)']
+        for (var type : ctor.getTypes()) {
+            walkType(
+                    type,
+                    Occurrence.STRICT_POS,
+                    new OccurrenceGraph.DefNode(currentDef)
+            );
+        }
+    }
+
+    private void walkType(HaskellObject type, Occurrence pol, OccurrenceGraph.Node target) {
+        if (type instanceof Cons cons) {
+            walkCons(cons, pol, target);
+        } else if (type instanceof Var var) {
+            walkVar(var, pol, target);
+        } else if (type instanceof Apply apply) {
+            walkApply(apply, pol, target);
+        }
+    }
+
+    // e.g. Foo = mkFoo Bar => cons -> `Bar`
+    private void walkCons(Cons cons, Occurrence pol, OccurrenceGraph.Node target) {
+        String name = cons.getSymbol().toString();
+        if (datatypeNames.contains(name)) {
+            graph.addEdge(
+                    new OccurrenceGraph.DefNode(name),
+                    target,
+                    pol
+            );
+        } else if (preludeTyCons != null && preludeTyCons.containsKey(name)) {
+            TyConsEntity entity = preludeTyCons.get(name);
+            if (entity.getValue() instanceof SynTypeDecl synTypeDecl) {
+                walkType(synTypeDecl.getType(), pol, target);
+            } else if (entity.getValue() instanceof DataDecl dataDecl) {
+                processDataDecl(dataDecl, name);
+            }
+        }
+    }
+
+    private void walkVar(Var var, Occurrence pol, OccurrenceGraph.Node target) {
+        String name = var.getSymbol().toString();
+        if (paramIndex.containsKey(name)) {
+            int index = paramIndex.get(name);
+            graph.addEdge(
+                    new OccurrenceGraph.ArgNode(currentDef, index),
+                    target,
+                    pol
+            );
+        }
+    }
+
+
+    private void walkApply(Apply apply, Occurrence pol, OccurrenceGraph.Node target) {
+        List<HaskellObject> args = new ArrayList<>();
+        var head = flattenApp(apply, args);
+
+        if (head instanceof Cons cons) {
+
+            String name = cons.getSymbol().toString();
+
+            //check if arrow function
+            if (name.equals("->")) {
+                // System.out.println("WalkArrow called");
+                walkArrow(apply, pol, target);
+                return;
+            }
+
+
+            if (datatypeNames.contains(name)) {
+                graph.addEdge(
+                        new OccurrenceGraph.DefNode(name),
+                        target,
+                        pol
+                );
+            }
+
+            for (int i = 0; i < args.size(); i++) {
+                Occurrence argPol = pol.otimes(argPolarity(name));
+                var argTarget = argTarget(name, i, target);
+                walkType(args.get(i), argPol, argTarget);
+            }
+        } else if (head instanceof Var var) {
+            String name = var.getSymbol().toString();
+            walkType(head, pol, target);
+            if (paramIndex.containsKey(name)) {
+                int index = paramIndex.get(name);
+                target = new OccurrenceGraph.ArgNode(currentDef, index);
+            }
+            for (var a : args) {
+                walkType(a, pol.otimes(Occurrence.MIXED), target);
+            }
+        } else {
+            walkType(head, pol, target);
+            for (var a : args) {
+                walkType(a, pol.otimes(Occurrence.MIXED), target);
+            }
+        }
+    }
+
+    private Occurrence argPolarity(String name) {
+        if (datatypeNames.contains(name) || preludeNames.contains(name)) {
+//            return Occurrence.GUARD_POS;
+            return Occurrence.STRICT_POS;
+        }
+        return Occurrence.MIXED;
+    }
+
+    private OccurrenceGraph.Node argTarget(
+            String name, int argIndex, OccurrenceGraph.Node currentTarget
+    ) {
+        if (datatypeNames.contains(name) || preludeNames.contains(name)) {
+            return new OccurrenceGraph.ArgNode(name, argIndex);
+        }
+        return currentTarget;
+    }
+
+    private void walkArrow(Apply apply, Occurrence pol, OccurrenceGraph.Node target) {
+        var codomain = apply.getArgument();
+        if (apply.getFunction() instanceof Apply apply2) {
+            var domain = apply2.getArgument();
+            walkType(domain, pol.otimes(Occurrence.JUST_NEG), target);
+            walkType(codomain, pol, target);
+        } else {
+            //should not happen
+        }
+    }
+}

src/aprove/input/Programs/haskell/HaskellParserCheck.java

@@ -0,0 +1,7 @@
+package aprove.input.Programs.haskell;
+
+public class HaskellParserCheck extends RuntimeException {
+    public HaskellParserCheck(String message) {
+        super(message);
+    }
+}

src/aprove/input/Programs/haskell/Occurrence.java

@@ -0,0 +1,72 @@
+package aprove.input.Programs.haskell;
+
+/**
+ * Occurrence is a
+ * <a href="https://en.wikipedia.org/wiki/Complete_lattice">complete lattice</a>
+ * with least element 'MIXED' and greatest element 'UNUSED'.
+ */
+public enum Occurrence {
+    MIXED, // + and -
+    JUST_NEG,
+    JUST_POS,
+    STRICT_POS,
+    UNUSED; // does not occur
+
+    /**
+     * Simulates behavior of additive of the Occurrence semiring (a+b):
+     * 'UNUSED' is neutral (zero) and 'MIXED' is dominant
+     *
+     * @param other the other Occurrence (b) added to 'this' (a)
+     * @return 'this + other'
+     */
+    public Occurrence oplus(Occurrence other) {
+
+        if (this == MIXED || other == MIXED) return MIXED;          // dominant
+
+        if (this == UNUSED) return other;
+        if (other == UNUSED) return this;
+
+        if (this == JUST_NEG && other == JUST_NEG) return JUST_NEG;
+        if (this == JUST_NEG || other == JUST_NEG) return MIXED;
+
+        if (this == STRICT_POS) return other;
+        if (other == STRICT_POS) return this;
+
+        return JUST_POS;                                                // both JUST_POS
+    }
+
+    /**
+     * Simulates behavior of multiplicative of the Occurrence semiring (a*b):
+     * 'STRICT_POS' is neutral (one) and 'UNUSED' dominant
+     *
+     * @param other the other Occurrence (b) 'this' (a) is to be multiplied by
+     * @return 'this * other'
+     */
+    public Occurrence otimes(Occurrence other) {
+        if (this == UNUSED || other == UNUSED) return UNUSED;
+        if (this == MIXED || other == MIXED) return MIXED;
+        if (this == JUST_NEG && other == JUST_NEG) return JUST_POS;
+        if (this == JUST_NEG || other == JUST_NEG) return JUST_NEG;
+        if (this == JUST_POS || other == JUST_POS) return JUST_POS;
+        return STRICT_POS;
+    }
+
+    /**
+     * @return true => mixed, just negative or just positive,<p> false => strict positive, guarded positive or unused
+     */
+    public boolean isNotStrictlyPositive() {
+        return this == MIXED || this == JUST_NEG || this == JUST_POS;
+    }
+
+
+    public String toPrettyString() {
+        return switch (this) {
+            case MIXED -> "±";
+            case JUST_NEG -> "-";
+            case JUST_POS -> "+";
+            case STRICT_POS -> "++";
+//            case GUARD_POS -> "g+";
+            case UNUSED -> "0";
+        };
+    }
+}