Skip to content

Commit

Permalink
Change AddBracketsTest to manually specify top sort.
Browse files Browse the repository at this point in the history
  • Loading branch information
Scott-Guest committed Nov 14, 2023
1 parent d04a883 commit 64c7f50
Showing 1 changed file with 15 additions and 12 deletions.
27 changes: 15 additions & 12 deletions kernel/src/test/java/org/kframework/unparser/AddBracketsTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,19 @@
package org.kframework.unparser;

import static org.junit.Assert.*;
import static org.kframework.Collections.*;

import com.google.common.collect.Lists;
import java.io.File;
import java.util.Set;
import org.junit.Before;
import org.junit.Test;
import org.kframework.attributes.Source;
import org.kframework.builtin.Sorts;
import org.kframework.definition.Definition;
import org.kframework.definition.Module;
import org.kframework.kompile.Kompile;
import org.kframework.kore.K;
import org.kframework.kore.Sort;
import org.kframework.main.GlobalOptions;
import org.kframework.parser.ParserUtils;
import org.kframework.parser.TreeNodesToKORE;
Expand Down Expand Up @@ -75,8 +76,9 @@ public void testLambda() {
+ " syntax Id ::= r\"(?<![A-Za-z0-9\\\\_])[A-Za-z\\\\_][A-Za-z0-9\\\\_]*\" [token,"
+ " autoreject]\n"
+ "endmodule\n";
unparserTest(def, "( lambda z . ( z z ) ) lambda x . lambda y . ( x y )");
unparserTest(def, "a ( ( lambda x . lambda y . x ) y z )");
Sort expSort = new org.kframework.kore.ADT.Sort("Exp", Seq());
unparserTest(def, "( lambda z . ( z z ) ) lambda x . lambda y . ( x y )", expSort);
unparserTest(def, "a ( ( lambda x . lambda y . x ) y z )", expSort);
}

@Test
Expand All @@ -89,26 +91,27 @@ public void testPriorityAndAssoc() {
+ " syntax Exp ::= \"(\" Exp \")\" [bracket]\n"
+ " syntax priority _*__TEST > _+__TEST\n"
+ "endmodule\n";
unparserTest(def, "1 + 1 + 1 + 1");
unparserTest(def, "1 + ( 1 + 1 ) + 1");
unparserTest(def, "1 + ( 1 + ( 1 + 1 ) )");
unparserTest(def, "1 + 1 * 1");
unparserTest(def, "( 1 + 1 ) * 1");
Sort expSort = new org.kframework.kore.ADT.Sort("Exp", Seq());
unparserTest(def, "1 + 1 + 1 + 1", expSort);
unparserTest(def, "1 + ( 1 + 1 ) + 1", expSort);
unparserTest(def, "1 + ( 1 + ( 1 + 1 ) )", expSort);
unparserTest(def, "1 + 1 * 1", expSort);
unparserTest(def, "( 1 + 1 ) * 1", expSort);
}

private void unparserTest(String def, String pgm) {
private void unparserTest(String def, String pgm, Sort topSort) {
Module test = parseModule(def);
ParseInModule parser =
RuleGrammarGenerator.getCombinedGrammar(gen.getProgramsGrammar(test), true, files);
K parsed = parseTerm(pgm, parser);
K parsed = parseTerm(pgm, parser, topSort);
KPrint kprint = new KPrint();
String unparsed = kprint.unparseTerm(parsed, test);
assertEquals(pgm, unparsed);
}

private K parseTerm(String pgm, ParseInModule parser) {
private K parseTerm(String pgm, ParseInModule parser, Sort topSort) {
Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> result =
parser.parseString(pgm, Sorts.KItem(), Source.apply("generated by AddBracketsTest"));
parser.parseString(pgm, topSort, Source.apply("generated by AddBracketsTest"));
assertEquals(0, result._2().size());
return new TreeNodesToKORE(Outer::parseSort, false).down(result._1().right().get());
}
Expand Down

0 comments on commit 64c7f50

Please sign in to comment.