Improve user interaction with prover

frontend/src/main/java/org/kframework/ProofResult.java

@@ -0,0 +1,28 @@
+package org.kframework;
+
+import org.kframework.frontend.K;
+
+import java.util.List;
+
+public class ProofResult {
+    private List<K> results;
+
+    private Status status;
+
+    public enum Status {
+        PROVED, NOT_PROVED, EMPTY_SPEC
+    }
+
+    public ProofResult(List<K> results, Status status) {
+        this.results = results;
+        this.status = status;
+    }
+
+    public List<K> getResults() {
+        return results;
+    }
+
+    public Status getStatus() {
+        return status;
+    }
+}

frontend/src/main/scala/org/kframework/definition/outer.scala

@@ -255,6 +255,12 @@ case class Module(val name: String, val imports: Set[Module], unresolvedLocalSen
 
   lazy val rules: Set[Rule] = sentences collect { case r: Rule => r }
 
+  private val locationKey: String = "org.kframework.attributes.Source"
+
+  lazy val claims: Set[Rule] = rules.filter(r => {
+    r.att.contains("claim") || (r.att.attMap.contains(locationKey) && r.att.attMap.get(locationKey).toString.contains("spec.k"))
+  })
+
   lazy val localRules: Set[Rule] = localSentences collect { case r: Rule => r }
 
   // Check that productions with the same klabel have identical attributes

frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala

@@ -3,7 +3,7 @@ package org.kframework.rewriter
 import java.util.Optional
 
 import org.kframework.definition.{Module, Rule}
-import org.kframework.{RewriterResult, frontend}
+import org.kframework.{ProofResult, RewriterResult, frontend}
 
 trait RewriterConstructor extends (Module => Rewriter)
 
@@ -38,5 +38,6 @@ trait Rewriter {
 
   def executeAndMatch(k: frontend.K, depth: Optional[Integer], rule: Rule): Tuple2[RewriterResult, frontend.K]
 
-  def prove(rules: java.util.List[Rule]): java.util.List[frontend.K]
+//  def prove(rules: java.util.List[Rule]): java.util.List[frontend.K]
+  def prove(rules: java.util.List[Rule]): ProofResult
 }

java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java

@@ -3,6 +3,7 @@
 
 import org.apache.commons.lang3.tuple.Pair;
 import org.kframework.KapiGlobal;
+import org.kframework.ProofResult;
 import org.kframework.RewriterResult;
 import org.kframework.backend.java.MiniKoreUtils;
 import org.kframework.backend.java.compile.KOREtoBackendKIL;
@@ -172,7 +173,7 @@ public Tuple2<RewriterResult, K> executeAndMatch(K k, Optional<Integer> depth, R
         }
 
         @Override
-        public List<K> prove(List<Rule> rules) {
+        public ProofResult prove(List<Rule> rules) {
             TermContext termContext = TermContext.builder(rewritingContext).freshCounter(initCounterValue).build();
             KOREtoBackendKIL converter = new KOREtoBackendKIL(module, definition, termContext.global(), false);
             termContext.setKOREtoBackendKILConverter(converter);
@@ -212,10 +213,15 @@ public List<K> prove(List<Rule> rules) {
                     .flatMap(List::stream)
                     .collect(Collectors.toList());
 
-            return proofResults.stream()
-                    .map(ConstrainedTerm::term)
-                    .map(t -> (KItem) t)
-                    .collect(Collectors.toList());
+            List<K> filteredResults = proofResults.stream()
+                        .map(ConstrainedTerm::term)
+                        .map(t -> (KItem) t)
+                        .collect(Collectors.toList());
+
+            if (filteredResults.isEmpty()) {
+               return new ProofResult(filteredResults, ProofResult.Status.PROVED);
+            }
+            return new ProofResult(filteredResults, ProofResult.Status.NOT_PROVED);
         }
 
     }

java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java

@@ -1,6 +1,7 @@
 // Copyright (c) 2015-2016 K Team. All Rights Reserved.
 package org.kframework.backend.java.symbolic;
 
+import org.kframework.ProofResult;
 import org.kframework.attributes.Att;
 import org.kframework.backend.java.frontend.compile.ExpandMacros;
 import org.kframework.compile.NormalizeKSeq;
@@ -29,11 +30,14 @@
 import org.kframework.krun.modes.ExecutionMode;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.Stopwatch;
+import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.file.FileUtil;
 import scala.Function1;
+import scala.collection.JavaConverters;
 import scala.collection.Set;
 
+import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.List;
@@ -49,7 +53,7 @@
 /**
  * Class that implements the "--prove" option.
  */
-public class ProofExecutionMode implements ExecutionMode<List<K>> {
+public class ProofExecutionMode implements ExecutionMode<ProofResult> {
 
     private final KExceptionManager kem;
     private final KRunOptions options;
@@ -66,7 +70,7 @@ public ProofExecutionMode(KExceptionManager kem, KRunOptions options, Stopwatch
     }
 
     @Override
-    public List<K> execute(K k, Rewriter rewriter, CompiledDefinition compiledDefinition) {
+    public ProofResult execute(K k, Rewriter rewriter, CompiledDefinition compiledDefinition) {
         String proofFile = options.experimental.prove;
         Kompile kompile = new Kompile(compiledDefinition.kompileOptions, globalOptions, files, kem, sw, false);
         Module mod = kompile.parseModule(compiledDefinition, files.resolveWorkingDirectory(proofFile).getAbsoluteFile());
@@ -145,20 +149,25 @@ public K apply(KVariable k) {
 
         ExpandMacros macroExpander = new ExpandMacros(compiledDefinition.kompiledDefinition.mainModule(), kem, files, globalOptions, compiledDefinition.kompileOptions.transition, compiledDefinition.kompileOptions.experimental.smt);
 
-        List<Rule> rules = stream(mod.localRules())
-                .filter(r -> r.toString().contains("spec.k"))
-                .map(r -> new Rule(
-                        cellPlaceholderSubstitutionApplication.apply(r.body()),
-                        cellPlaceholderSubstitutionApplication.apply(r.requires()),
-                        cellPlaceholderSubstitutionApplication.apply(r.ensures()),
-                        r.att()))
-                .map(r -> (Rule) macroExpander.expand(r))
-                .map(r -> transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
-                .map(r -> transformFunction(Kompile::convertKSeqToKApply, r))
-                .map(r -> transform(NormalizeKSeq.self(), r))
-                //.map(r -> kompile.compileRule(compiledDefinition, r))
-                .collect(Collectors.toList());
-        return rewriter.prove(rules);
+        List<Rule> rules = JavaConverters.seqAsJavaList(mod.claims().toSeq());
+
+        if(rules.isEmpty()) {
+            return new ProofResult(new ArrayList<K>(), ProofResult.Status.EMPTY_SPEC);
+        }
+        else {
+            rules = rules.stream()
+                    .map(r -> new Rule(
+                            cellPlaceholderSubstitutionApplication.apply(r.body()),
+                            cellPlaceholderSubstitutionApplication.apply(r.requires()),
+                            cellPlaceholderSubstitutionApplication.apply(r.ensures()),
+                            r.att()))
+                    .map(r -> (Rule) macroExpander.expand(r))
+                    .map(r -> transformFunction(JavaBackend::ADTKVariableToSortedVariable, r))
+                    .map(r -> transformFunction(Kompile::convertKSeqToKApply, r))
+                    .map(r -> transform(NormalizeKSeq.self(), r))
+                    .collect(Collectors.toList());
+            return rewriter.prove(rules);
+        }
     }
 
     public static Rule transformFunction(Function<K, K> f, Rule r) {

k-distribution/tests/config.xml

@@ -32,5 +32,8 @@
   <include file="builtins/config.xml" directory="tests/builtins" skip="pdf" />
 
   <include file="issues/config.xml" directory="tests/issues" skip="pdf" />
-</tests>
+
+  <include file="prover/prover-io/config.xml" directory="tests/prover/prover-io" skip="pdf" />
+ </tests>
+
 

k-distribution/tests/prover/prover-io/config.xml

@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!-- Copyright (c) 2012-2016 K Team. All Rights Reserved. -->
+
+<tests>
+    <test
+            definition="iotest.k"
+            programs="."
+            results="."
+            extension="iotest"
+            >
+        <program name="p1.iotest">
+          <krun-option name="--prove" value="proof1.k" />
+          <krun-option name="--z3-executable" />
+        </program>
+        <program name="p1_without_attribute.iotest">
+          <krun-option name="--prove" value="proof1_without_attribute.k" />
+          <krun-option name="--z3-executable" />
+        </program>
+        <program name="p2.iotest">
+          <krun-option name="--prove" value="p2.k" />
+          <krun-option name="--z3-executable" />
+        </program>
+    </test>
+</tests>
+

k-distribution/tests/prover/prover-io/iotest.k

@@ -0,0 +1,16 @@
+require "domains.k"
+
+module IOTEST-SYNTAX
+    syntax Tok ::= "a" | "b" | "c"
+endmodule
+
+module IOTEST
+    imports IOTEST-SYNTAX
+
+    configuration <k> $PGM:Tok</k>
+
+    rule a => b
+
+    rule b => c
+endmodule
+

k-distribution/tests/prover/prover-io/p1.iotest

@@ -0,0 +1 @@
+a

k-distribution/tests/prover/prover-io/p1.iotest.out

@@ -0,0 +1 @@
+true

k-distribution/tests/prover/prover-io/p1_without_attribute.iotest

@@ -0,0 +1 @@
+a

k-distribution/tests/prover/prover-io/p1_without_attribute.iotest.out

@@ -0,0 +1,2 @@
+No Rules with attribute "claim" found
+

k-distribution/tests/prover/prover-io/proof1.k

@@ -0,0 +1,4 @@
+module PROOFTEST
+    imports IOTEST
+    rule <k> a => c </k>    [claim]
+endmodule

k-distribution/tests/prover/prover-io/proof1_without_attribute.k

@@ -0,0 +1,4 @@
+module PROOFTEST
+    imports IOTEST
+    rule <k> a => c </k>
+endmodule

kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala

@@ -8,7 +8,7 @@ import org.kframework.definition._
 import org.kframework.frontend.Unapply.KRewrite
 import org.kframework.frontend._
 import org.kframework.rewriter.SearchType
-import org.kframework.{RewriterResult, frontend}
+import org.kframework.{ProofResult, RewriterResult, frontend}
 
 import scala.collection._
 
@@ -206,5 +206,5 @@ class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter {
 
   override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ???
 
-  override def prove(rules: util.List[Rule]): util.List[K] = ???
+  override def prove(rules: util.List[Rule]): ProofResult = ???
 }

kernel/src/main/java/org/kframework/krun/KRun.java

@@ -3,6 +3,7 @@
 
 import org.apache.commons.io.output.ByteArrayOutputStream;
 import org.apache.commons.lang3.tuple.Pair;
+import org.kframework.ProofResult;
 import org.kframework.RewriterResult;
 import org.kframework.attributes.Source;
 import org.kframework.builtin.KLabels;
@@ -123,9 +124,18 @@ public int run(KompileMetaInfo kompileMetaInfo, CompiledDefinition compiledDef,
                 return (Integer) tuple._2();
             }
         } else if (options.experimental.prove != null) {
-            if (((List) result).isEmpty()) {
+            ProofResult proofResult = (ProofResult) result;
+            switch (proofResult.getStatus()) {
+            case PROVED:
                 System.out.println("true");
+                break;
+            case NOT_PROVED:
+                System.out.println("Claim(s) Couldn't Be Proven!");
+                break;
+            case EMPTY_SPEC:
+                System.out.println("No Rules with attribute \"claim\" found");
             }
+
         } else if (result instanceof Integer) {
             return (Integer) result;
         }