#1 cleaned and fixed

polystat · Jul 1, 2021 · 0d31699 · 0d31699
1 parent 5255e13
commit 0d31699
Show file tree

Hide file tree

Showing 17 changed files with 149 additions and 30 deletions.
diff --git a/src/main/java/org/polystat/XMIR.java b/src/main/java/org/polystat/XMIR.java
@@ -67,11 +67,12 @@ public XMIR(final Path src, final Path tmp) {
     @Override
     public XML apply(final String locator) throws Exception {
         final String[] parts = locator.split("\\.");
-        final Path xml = this.temp.resolve("test.xml");
+        final String name = parts[1];
+        final Path xml = this.temp.resolve(String.format("%s.xml", name));
         if (!Files.exists(xml)) {
             new Syntax(
-                "test",
-                new InputOf(this.sources.resolve("test.eo")),
+                name,
+                new InputOf(this.sources.resolve(String.format("%s.eo", name))),
                 new OutputTo(xml)
             ).parse();
             new Xsline(

diff --git a/src/main/java/org/polystat/far/Expr.java b/src/main/java/org/polystat/far/Expr.java
@@ -39,6 +39,11 @@
  */
 public final class Expr {
 
+    /**
+     * None.
+     */
+    public static final String NEVER = "N";
+
     /**
      * The expression.
      */
@@ -86,7 +91,7 @@ public String find() {
             }
             final String kid = new Expr(join, ands[1]).find();
             if (!kid.isEmpty()) {
-                result = String.format("%s > %s", out, kid);
+                result = String.format("%s ➜ %s", out, kid);
                 break;
             }
         }
@@ -105,7 +110,7 @@ private static Collection<Map<String, String>> parse(final String txt) {
             new ArrayList<>(ors.length);
         for (final String item : ors) {
             final String[] taus = item.substring(1, item.length() - 1)
-                .split(" & ");
+                .split(" ∧ ");
             final Map<String, String> opts = new HashMap<>(taus.length);
             for (final String tau : taus) {
                 final String[] eqs = tau.split("=");
@@ -137,8 +142,16 @@ private static String print(final Map<String, String> map) {
     private boolean matches(final Map<String, String> map) {
         boolean matches = true;
         for (final Map.Entry<String, String> ent : this.already.entrySet()) {
-            if (map.containsKey(ent.getKey())
-                && !map.get(ent.getKey()).equals(ent.getValue())) {
+            final String left = ent.getValue();
+            if (Expr.NEVER.equals(left)) {
+                matches = false;
+                break;
+            }
+            final String right = map.get(ent.getKey());
+            if (right == null) {
+                continue;
+            }
+            if (!right.equals(left)) {
                 matches = false;
                 break;
             }

diff --git a/src/main/java/org/polystat/far/Reverses.java b/src/main/java/org/polystat/far/Reverses.java
@@ -84,8 +84,8 @@ public Collection<String> errors(final String locator) throws IOException {
         final ByteArrayOutputStream baos = new ByteArrayOutputStream();
         new Xsline(obj, new OutputTo(baos), new Spy.Verbose(), new ListOf<>())
             .with(Reverses.xsl("expected.xsl").with("expected", "\\perp"))
+            .with(Reverses.xsl("data-to-attrs.xsl"))
             .with(Reverses.xsl("reverses.xsl"))
-            .with(Reverses.xsl("inject-tau-numbers.xsl"))
             .with(
                 Reverses.xsl("calculate.xsl").with(
                     (href, base) -> new StreamSource(
@@ -104,15 +104,16 @@ public Collection<String> errors(final String locator) throws IOException {
                 ),
                 (before, after) -> !after.nodes("//r").isEmpty()
             )
-            .with(Reverses.xsl("remove-input-perps.xsl"))
             .with(Reverses.xsl("remove-outsiders.xsl"))
             .with(Reverses.xsl("taus-to-tree.xsl"))
+            .with(Reverses.xsl("unmatch-data.xsl").with("never", Expr.NEVER))
             .with(
                 Reverses.xsl("remove-conflicts.xsl"),
                 (before, after) -> !before.toString().equals(after.toString())
             )
             .with(Reverses.xsl("opts-to-boolean-expressions.xsl"))
             .with(Reverses.xsl("expressions-to-inputs.xsl"))
+            .with(Reverses.xsl("remove-input-perps.xsl"))
             .pass();
         XML out = new XMLDocument(
             baos.toString(StandardCharsets.UTF_8.name())

diff --git a/src/main/resources/org/polystat/far/data-to-attrs.xsl b/src/main/resources/org/polystat/far/data-to-attrs.xsl
@@ -0,0 +1,54 @@
+<?xml version="1.0"?>
+<!--
+The MIT License (MIT)
+
+Copyright (c) 2020-2021 Polystat.org
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+-->
+<xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="data-to-attrs" version="2.0">
+  <xsl:strip-space elements="*"/>
+  <xsl:template match="o[o[@name='@']]">
+    <xsl:copy>
+      <xsl:apply-templates select="@*|node()"/>
+      <xsl:for-each select=".//o[@base and @data and not(o)]">
+        <xsl:element name="o">
+          <xsl:attribute name="name">
+            <xsl:text>&#x3BA;</xsl:text>
+            <xsl:text>-</xsl:text>
+            <xsl:value-of select="count(./preceding::*) + count(ancestor::*) + 1"/>
+            <xsl:text>-</xsl:text>
+            <xsl:value-of select="@line"/>
+          </xsl:attribute>
+          <xsl:attribute name="line">
+            <xsl:value-of select="@line"/>
+          </xsl:attribute>
+          <xsl:attribute name="data">
+            <xsl:value-of select="text()"/>
+          </xsl:attribute>
+        </xsl:element>
+      </xsl:for-each>
+    </xsl:copy>
+  </xsl:template>
+  <xsl:template match="node()|@*">
+    <xsl:copy>
+      <xsl:apply-templates select="node()|@*"/>
+    </xsl:copy>
+  </xsl:template>
+</xsl:stylesheet>
diff --git a/src/main/resources/org/polystat/far/expressions-to-inputs.xsl b/src/main/resources/org/polystat/far/expressions-to-inputs.xsl
@@ -59,7 +59,6 @@ SOFTWARE.
               </xsl:if>
               <xsl:value-of select="text()"/>
             </xsl:for-each>
-            <xsl:value-of select="."/>
           </xsl:element>
         </xsl:element>
       </xsl:otherwise>

diff --git a/src/main/resources/org/polystat/far/opts-to-boolean-expressions.xsl b/src/main/resources/org/polystat/far/opts-to-boolean-expressions.xsl
@@ -34,19 +34,19 @@ SOFTWARE.
           <xsl:attribute name="x">
             <xsl:value-of select="$x"/>
           </xsl:attribute>
-          <xsl:for-each select="$o/opts">
+          <xsl:for-each select="$o/opts[opt[@x=$x or @x='\any']]">
             <xsl:if test="position() &gt; 1">
               <xsl:text> and </xsl:text>
             </xsl:if>
             <xsl:text>(</xsl:text>
-            <xsl:for-each select="opt[@x=$x or @x='\any']">
+            <xsl:for-each select="opt[@x=$x or @x='\any' and tau]">
               <xsl:if test="position() &gt; 1">
                 <xsl:text> or </xsl:text>
               </xsl:if>
               <xsl:text>(</xsl:text>
               <xsl:for-each select="tau">
                 <xsl:if test="position() &gt; 1">
-                  <xsl:text> &amp; </xsl:text>
+                  <xsl:text> &#x2227; </xsl:text>
                 </xsl:if>
                 <xsl:text>&#x1D70F;</xsl:text>
                 <xsl:variable name="parts" select="tokenize(@i, ':')"/>

diff --git a/src/main/resources/org/polystat/far/remove-false-inputs.xsl b/src/main/resources/org/polystat/far/remove-false-inputs.xsl
@@ -30,7 +30,7 @@ SOFTWARE.
   <xsl:template match="input[@found!='']">
     <xsl:copy>
       <xsl:attribute name="found">
-        <xsl:variable name="parts" select="tokenize(@found, ' &gt; ')"/>
+        <xsl:variable name="parts" select="tokenize(@found, ' &#x279C; ')"/>
         <xsl:value-of select="$parts[count($parts)]"/>
       </xsl:attribute>
       <xsl:apply-templates select="node()|@* except @found"/>

diff --git a/src/main/resources/org/polystat/far/remove-input-perps.xsl b/src/main/resources/org/polystat/far/remove-input-perps.xsl
@@ -24,7 +24,7 @@ SOFTWARE.
 -->
 <xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="remove-input-perps" version="2.0">
   <xsl:strip-space elements="*"/>
-  <xsl:template match="opt[@x = '\perp']">
+  <xsl:template match="input[a[@x = '\perp']]">
     <!-- just delete it -->
   </xsl:template>
   <xsl:template match="node()|@*">

diff --git a/src/main/resources/org/polystat/far/reverses.xsl b/src/main/resources/org/polystat/far/reverses.xsl
@@ -24,7 +24,6 @@ SOFTWARE.
 -->
 <xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="reverses" version="2.0">
   <xsl:strip-space elements="*"/>
-  <xsl:param name="out"/>
   <xsl:template name="r">
     <xsl:param name="result" select="''"/>
     <xsl:param name="o" as="node()"/>
@@ -34,6 +33,9 @@ SOFTWARE.
         <xsl:element name="r">
           <xsl:attribute name="f" select="$o/@base"/>
           <xsl:attribute name="pos" select="position()"/>
+          <xsl:attribute name="tau">
+            <xsl:value-of select="count($o/preceding::*) + count($o/ancestor::*)"/>
+          </xsl:attribute>
           <xsl:copy-of select="$result"/>
         </xsl:element>
       </xsl:variable>
@@ -43,6 +45,11 @@ SOFTWARE.
             <xsl:copy-of select="$i"/>
           </xsl:element>
         </xsl:when>
+        <xsl:when test="text()=$attr/@data">
+          <xsl:element name="opts">
+            <xsl:copy-of select="$i"/>
+          </xsl:element>
+        </xsl:when>
         <xsl:otherwise>
           <xsl:call-template name="r">
             <xsl:with-param name="result">

diff --git a/src/main/resources/org/polystat/far/rules.txt b/src/main/resources/org/polystat/far/rules.txt
@@ -2,3 +2,6 @@
 .add(y) -> {{0 y}}
 .div(\perp) -> {{\any \perp} {\perp \any} {\any 0}}
 .div(y) -> {{y 1}}
+.eq(true) -> {{0 0} {17 17}}
+.eq(false) -> {{19 0} {0 19}}
+.if(\perp) -> {{true \perp \any} {false \any \perp}}
diff --git a/src/main/resources/org/polystat/far/taus-to-tree.xsl b/src/main/resources/org/polystat/far/taus-to-tree.xsl
@@ -22,7 +22,7 @@ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
 -->
-<xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="remove-input-perps" version="2.0">
+<xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="taus-to-tree" version="2.0">
   <xsl:strip-space elements="*"/>
   <xsl:template match="opt[not(empty(text()))]">
     <xsl:copy>

diff --git a/...s/org/polystat/far/inject-tau-numbers.xsl → ...sources/org/polystat/far/unmatch-data.xsl b/...s/org/polystat/far/inject-tau-numbers.xsl → ...sources/org/polystat/far/unmatch-data.xsl
@@ -22,14 +22,21 @@ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
 -->
-<xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="inject-tau-numbers" version="2.0">
+<xsl:stylesheet xmlns:xsl="http://www.w3.org/1999/XSL/Transform" id="match-data" version="2.0">
   <xsl:strip-space elements="*"/>
-  <xsl:template match="r[not(@tau)]">
+  <xsl:param name="never"/>
+  <xsl:template match="tau">
     <xsl:copy>
-      <xsl:attribute name="tau">
-        <xsl:value-of select="count(./preceding::*) + count(ancestor::*) + 1"/>
-      </xsl:attribute>
-      <xsl:apply-templates select="node()|@*"/>
+      <xsl:apply-templates select="@*|node() except text()"/>
+      <xsl:variable name="opt" select="parent::opt"/>
+      <xsl:choose>
+        <xsl:when test="$opt/parent::opts/parent::o[@data and @data!=$opt/@x and $opt/@x!='\any']">
+          <xsl:value-of select="$never"/>
+        </xsl:when>
+        <xsl:otherwise>
+          <xsl:value-of select="text()"/>
+        </xsl:otherwise>
+      </xsl:choose>
     </xsl:copy>
   </xsl:template>
   <xsl:template match="node()|@*">

diff --git a/src/test/java/org/polystat/PolystatTest.java b/src/test/java/org/polystat/PolystatTest.java
@@ -55,7 +55,7 @@ public void saysHello() throws Exception {
     public void analyzesOneEolangProgram() throws Exception {
         final Path sources = Files.createTempDirectory("sources");
         Files.write(
-            sources.resolve("test.eo"),
+            sources.resolve("foo.eo"),
             new TextOf(
                 new ResourceOf("org/polystat/tests/div-by-zero.eo")
             ).asString().getBytes(StandardCharsets.UTF_8)

diff --git a/src/test/java/org/polystat/XMIRTest.java b/src/test/java/org/polystat/XMIRTest.java
@@ -45,7 +45,7 @@ public final class XMIRTest {
     public void interpretsOneEolangProgram() throws Exception {
         final Path sources = Files.createTempDirectory("sources");
         Files.write(
-            sources.resolve("test.eo"),
+            sources.resolve("foo.eo"),
             new TextOf(
                 new ResourceOf("org/polystat/tests/div-by-zero.eo")
             ).asString().getBytes(StandardCharsets.UTF_8)

diff --git a/src/test/java/org/polystat/far/ExprTest.java b/src/test/java/org/polystat/far/ExprTest.java
@@ -37,23 +37,31 @@ public final class ExprTest {
     @Test
     public void solvesSimpleExpression() {
         final Expr expr = new Expr(
-            "((a=1 & b=2) or (b=3)) and ((a=7) or (b=2 & d=7))"
+            "((a=1 ∧ b=2) or (b=3)) and ((a=7) or (b=2 ∧ d=7))"
         );
         MatcherAssert.assertThat(
             expr.find(),
-            Matchers.equalTo("a=1 b=2 > a=1 b=2 d=7")
+            Matchers.equalTo("a=1 b=2 ➜ a=1 b=2 d=7")
         );
     }
 
     @Test
     public void failsSimpleExpression() {
         final Expr expr = new Expr(
-            "((a=1 & b=2) or (d=4)) and ((d=5 & a=7) or (b=6 & d=1))"
+            "((a=1 ∧ b=2) or (d=4)) and ((d=5 ∧ a=7) or (b=6 ∧ d=1))"
         );
         MatcherAssert.assertThat(
             expr.find(),
             Matchers.equalTo("")
         );
     }
 
+    @Test
+    public void ignoresNever() {
+        final Expr expr = new Expr(
+            String.format("((a=1 ∧ b=%s)) and ((a=1))", Expr.NEVER)
+        );
+        MatcherAssert.assertThat(expr.find(), Matchers.equalTo(""));
+    }
+
 }
diff --git a/src/test/java/org/polystat/far/ReversesTest.java b/src/test/java/org/polystat/far/ReversesTest.java
@@ -43,10 +43,10 @@
 public final class ReversesTest {
 
     @Test
-    public void findsReversesInSimpleXml() throws Exception {
+    public void findsBugsInSimpleXml() throws Exception {
         final Path sources = Files.createTempDirectory("sources");
         Files.write(
-            sources.resolve("test.eo"),
+            sources.resolve("foo.eo"),
             new TextOf(
                 new ResourceOf("org/polystat/tests/div-by-zero.eo")
             ).asString().getBytes(StandardCharsets.UTF_8)
@@ -62,4 +62,19 @@ public void findsReversesInSimpleXml() throws Exception {
         Logger.debug(this, "Bugs found: %s", bugs);
     }
 
+    @Test
+    public void findsNoBugsInSimpleXml() throws Exception {
+        final Path sources = Files.createTempDirectory("sources2");
+        Files.write(
+            sources.resolve("bar.eo"),
+            new TextOf(
+                new ResourceOf("org/polystat/tests/no-div-by-zero.eo")
+            ).asString().getBytes(StandardCharsets.UTF_8)
+        );
+        final Path temp = Files.createTempDirectory("temp2");
+        final Reverses reverses = new Reverses(new XMIR(sources, temp));
+        final Collection<String> bugs = reverses.errors("\\Phi.bar");
+        MatcherAssert.assertThat(bugs, Matchers.emptyIterable());
+    }
+
 }
diff --git a/src/test/resources/org/polystat/tests/no-div-by-zero.eo b/src/test/resources/org/polystat/tests/no-div-by-zero.eo
@@ -0,0 +1,11 @@
++package org.polystat
+
+[a b] > bar
+  if. > @
+    eq.
+      b
+      0
+    "Oops"
+    div.
+      a
+      b