Skip to content

Commit e8faba8

Browse files
andreistefanescuandreistefanescu
committed
Merge pull request runtimeverification#1957 from kframework/feature/k-api
Parser @API interface Former-commit-id: a80a3c8d9e9ac4093d6e860ecba1457917f7ab3a [formerly f8bda96cec66dc65176e9c7f81f5a076b15dfac5] Former-commit-id: 2ca45f2a191531e4be2b2f25c0212db03d0fe448
2 parents 8e3c3ec + a67e11e commit e8faba8

7 files changed

Lines changed: 135 additions & 3 deletions

File tree

‎kernel/src/main/java/org/kframework/Parser.java‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework;
3+
4+
import org.kframework.attributes.Source;
5+
import org.kframework.definition.Module;
6+
import org.kframework.kore.K;
7+
import org.kframework.kore.Sort;
8+
import org.kframework.parser.concrete2kore.ParseInModule;
9+
import org.kframework.utils.errorsystem.ParseFailedException;
10+
import scala.Option;
11+
import scala.Tuple2;
12+
import scala.util.Either;
13+
import scala.util.control.Exception;
14+
15+
import java.util.HashSet;
16+
import java.util.Set;
17+
18+
/**
19+
* Parses a string with a particular start symbol/sort.
20+
* Constructed via the static {@link #from methods}
21+
*/
22+
@API
23+
public class Parser {
24+
private final ParseInModule parseInModule;
25+
26+
private Parser(Module module) {
27+
this.parseInModule = new ParseInModule(module);
28+
}
29+
30+
/**
31+
* Parses a string with a particular start symbol/sort.
32+
*
33+
* @param startSymbol the start symbol/sort
34+
* @param toParse the String to parse
35+
* @param fromSource the Source of the String toParse
36+
* @return a pair: the left projection is a parsed string as a K, if successful;
37+
* the right projection is the set of issues encountered while parsing
38+
*/
39+
@SuppressWarnings("unchecked")
40+
public Tuple2<Option<K>, Set<Warning>> apply(Sort startSymbol, String toParse, Source fromSource) {
41+
Tuple2<Either<Set<ParseFailedException>, K>, Set<ParseFailedException>> res = parseInModule.parseString(toParse, startSymbol, fromSource);
42+
43+
Set<Warning> problemSet = new HashSet<>();
44+
problemSet.addAll((Set<Warning>) (Object) res._2());
45+
if (res._1().isLeft())
46+
problemSet.addAll((Set<Warning>) (Object) res._1().left().get());
47+
return Tuple2.apply(res._1().right().toOption(), problemSet);
48+
}
49+
50+
/**
51+
* Parses a string with a particular start symbol/sort.
52+
*
53+
* @param startSymbol the start symbol/sort
54+
* @param toParse the String to parse
55+
* @return a pair: the left projection is a parsed string as a K, if successful;
56+
* the right projection is the set of issues encountered while parsing
57+
*/
58+
public Tuple2<Option<K>, Set<Warning>> apply(Sort startSymbol, String toParse) {
59+
return apply(startSymbol, toParse, Source.apply("generated"));
60+
}
61+
62+
public static Parser from(Module module) {
63+
return new Parser(module);
64+
}
65+
}

‎kernel/src/main/java/org/kframework/parser/concrete2kore/ParseInModule.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ public class ParseInModule implements Serializable {
4646
private final Module parsingModule;
4747
private volatile Grammar grammar = null;
4848
private final boolean strict;
49-
ParseInModule(Module seedModule) {
49+
public ParseInModule(Module seedModule) {
5050
this(seedModule, seedModule, seedModule, seedModule, true);
5151
}
5252

‎kernel/src/test/java/org/kframework/ParserTest.java‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework;
3+
4+
import static org.junit.Assert.*;
5+
6+
import org.junit.Test;
7+
import org.kframework.definition.*;
8+
import org.kframework.kore.K;
9+
import org.kframework.kore.Sort;
10+
import scala.Option;
11+
import scala.Tuple2;
12+
13+
import java.util.Set;
14+
15+
import static org.kframework.kore.KORE.*;
16+
import static org.kframework.Collections.*;
17+
18+
public class ParserTest {
19+
private static final Sort xSort = Sort("X");
20+
Module m = Module.apply("TEST", Set(
21+
Production.apply(xSort, Seq(Terminal.apply("x")), Att().add("klabel", "x"))
22+
));
23+
24+
@Test
25+
public void simpleNoWarning() {
26+
Tuple2<Option<K>, Set<Warning>> actual = Parser.from(m).apply(xSort, "x");
27+
assertTrue("The parse should succeed, but was " + actual, actual._1().isDefined());
28+
assertTrue("There should be no warnings, but were: " + actual._2(), actual._2().isEmpty());
29+
assertEquals(KApply(KLabel("x")), actual._1().get());
30+
}
31+
32+
@Test
33+
public void simpleFailedParse() {
34+
Tuple2<Option<K>, Set<Warning>> actual = Parser.from(m).apply(xSort, "y");
35+
assertTrue("The parse should fail, but was " + actual, actual._1().isEmpty());
36+
assertTrue("There should be one error, but were: " + actual._2(), actual._2().size() == 1);
37+
}
38+
}

‎kore/src/main/java/org/kframework/API.java‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework;
3+
4+
import java.lang.annotation.ElementType;
5+
import java.lang.annotation.Target;
6+
7+
/**
8+
* Marker for classes we consider as part fo the K API.
9+
* It is particularly important for these classes to be well-documented.
10+
*/
11+
@Target(ElementType.TYPE)
12+
public @interface API {
13+
14+
}

‎kore/src/main/java/org/kframework/Warning.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework;
3+
4+
@API
5+
public interface Warning {
6+
7+
}

‎kore/src/main/java/org/kframework/utils/errorsystem/ParseFailedException.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
// Copyright (c) 2014-2015 K Team. All Rights Reserved.
22
package org.kframework.utils.errorsystem;
33

4+
import org.kframework.Warning;
5+
46
@SuppressWarnings("serial")
5-
public class ParseFailedException extends KEMException {
7+
public class ParseFailedException extends KEMException implements Warning {
68
KException exception;
79

810
public ParseFailedException(KException kException) {

‎kore/src/main/scala/org/kframework/definition/outer.scala‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,9 @@ trait GeneratingListSubsortProductions extends Sorting {
7777
}
7878

7979
object Module {
80+
def apply(name: String, unresolvedLocalSentences: Set[Sentence]): Module = {
81+
new Module(name, Set(), unresolvedLocalSentences, Att())
82+
}
8083
def apply(name: String, imports: Set[Module], unresolvedLocalSentences: Set[Sentence], @(Nonnull@param) att: Att = Att()): Module = {
8184
new Module(name, imports, unresolvedLocalSentences, att)
8285
}
@@ -354,9 +357,12 @@ case class RegexTerminal(precedeRegex: String, regex: String, followRegex: Strin
354357
}
355358
}
356359

360+
object Terminal {
361+
def apply(value: String): Terminal = Terminal(value, Seq())
362+
}
363+
357364
case class Terminal(value: String, followRegex: Seq[String]) extends TerminalLike // hooked
358365
with TerminalToString {
359-
def this(value: String) = this(value, Seq())
360366

361367
lazy val pattern = new RunAutomaton(BasicAutomata.makeString(value), false)
362368
lazy val followPattern =

0 commit comments

Comments
 (0)