k/kernel/src/test/java/org/kframework/unparser/AddBracketsTest.java at master · https-github-com-goodman-ops/k · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
// Copyright (c) 2015-2019 K Team. All Rights Reserved.
package org.kframework.unparser;

import com.google.common.collect.Lists;
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.main.GlobalOptions;
import org.kframework.parser.TreeNodesToKORE;
import org.kframework.parser.concrete2kore.ParseInModule;
import org.kframework.parser.concrete2kore.ParserUtils;
import org.kframework.parser.concrete2kore.generator.RuleGrammarGenerator;
import org.kframework.parser.outer.Outer;
import org.kframework.utils.errorsystem.KEMException;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.file.FileUtil;
import scala.Tuple2;
import scala.util.Either;

import java.io.File;
import java.util.Set;

import static org.junit.Assert.*;

public class AddBracketsTest {

    private RuleGrammarGenerator gen;

    @Before
    public void setUp() throws  Exception{
        gen = makeRuleGrammarGenerator();
    }

    public RuleGrammarGenerator makeRuleGrammarGenerator() {
        String definitionText;
        FileUtil files = FileUtil.testFileUtil();
        ParserUtils parser = new ParserUtils(files::resolveWorkingDirectory, new KExceptionManager(new GlobalOptions()));
        File definitionFile = new File(Kompile.BUILTIN_DIRECTORY.toString() + "/kast.k");
        definitionText = files.loadFromWorkingDirectory(definitionFile.getPath());

        Definition baseK =
                parser.loadDefinition("K", "K", definitionText,
                        definitionFile,
                        definitionFile.getParentFile(),
                        Lists.newArrayList(Kompile.BUILTIN_DIRECTORY),
                        false, false);

        return new RuleGrammarGenerator(baseK);
    }

    private Module parseModule(String def) {
        return ParserUtils.parseMainModuleOuterSyntax(def, Source.apply("generated by AddBracketsTest"), "TEST");
    }

    @Test
    public void testLambda() {
        String def = "module TEST\n" +
                "  syntax Val ::= Id\n" +
                "               | \"lambda\" Id \".\" Exp\n" +
                "  syntax Exp ::= Val\n" +
                "               | Exp Exp      [left]\n" +
                "               | \"(\" Exp \")\"  [bracket]\n" +
                "  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 )");
    }

    @Test
    public void testPriorityAndAssoc() {
        String def = "module TEST\n" +
                "  syntax Exp ::= Exp \"+\" Exp [left]\n" +
                "  syntax Exp ::= Exp \"*\" Exp [left]\n" +
                "  syntax Exp ::= \"1\"\n" +
                "  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");
    }

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

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

}