k/kernel/src/main/java/org/kframework/kompile/ResolveConfig.java at dapphub · 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
106
107
108
109
// Copyright (c) 2015-2016 K Team. All Rights Reserved.
package org.kframework.kompile;

import org.kframework.Collections;
import org.kframework.builtin.BooleanUtils;
import org.kframework.compile.GenerateSentencesFromConfigDecl;
import org.kframework.definition.Bubble;
import org.kframework.definition.Definition;
import org.kframework.definition.Module;
import org.kframework.definition.Sentence;
import org.kframework.kil.Import;
import org.kframework.kore.K;
import org.kframework.kore.KApply;
import org.kframework.parser.concrete2kore.ParseInModule;
import org.kframework.utils.errorsystem.KEMException;
import scala.collection.Set;

import java.util.List;
import java.util.function.BiFunction;
import java.util.function.Function;
import java.util.function.UnaryOperator;
import java.util.stream.Stream;

import static org.kframework.Collections.*;
import static org.kframework.definition.Constructors.*;
import static org.kframework.kore.KORE.*;

/**
 * Expands configuration declaration to KORE productions and rules.
 */
class ResolveConfig {
    private final Definition def;
    private final boolean isStrict;
    private final BiFunction<Module, Bubble, Stream<? extends K>> parseBubble;
    private Function<Module, ParseInModule> getParser;

    ResolveConfig(Definition def, boolean isStrict, BiFunction<Module, Bubble, Stream<? extends K>> parseBubble, Function<Module, ParseInModule> getParser) {
        this.def = def;
        this.isStrict = isStrict;
        this.parseBubble = parseBubble;
        this.getParser = getParser;
    }

    public Module apply(Module inputModule) {
        if (stream(inputModule.localSentences())
                .filter(s -> s instanceof Bubble)
                .map(b -> (Bubble) b)
                .filter(b -> b.sentenceType().equals("config")).count() == 0)
            return inputModule;


        Set<Sentence> importedConfigurationSortsSubsortedToCell = stream(inputModule.productions())
                .filter(p -> p.att().contains("cell"))
                .map(p -> Production(Sort("Cell"), Seq(NonTerminal(p.sort())))).collect(Collections.toSet());

        Module module = Module(inputModule.name(), (Set<Module>) inputModule.imports(),
                (Set<Sentence>) inputModule.localSentences().$bar(importedConfigurationSortsSubsortedToCell),
                inputModule.att());

        ParseInModule parser = getParser.apply(module);

        Set<Sentence> configDeclProductions = stream(module.localSentences())
                .parallel()
                .filter(s -> s instanceof Bubble)
                .map(b -> (Bubble) b)
                .filter(b -> b.sentenceType().equals("config"))
                .flatMap(b -> parseBubble.apply(module, b))
                .map(contents -> {
                    KApply configContents = (KApply) contents;
                    List<K> items = configContents.klist().items();
                    switch (configContents.klabel().name()) {
                    case "#ruleNoConditions":
                        return Configuration(items.get(0), BooleanUtils.TRUE, configContents.att());
                    case "#ruleEnsures":
                        return Configuration(items.get(0), items.get(1), configContents.att());
                    default:
                        throw KEMException.compilerError("Illegal configuration with requires clause detected.", configContents);
                    }
                })
                .flatMap(
                        configDecl -> stream(GenerateSentencesFromConfigDecl.gen(configDecl.body(), configDecl.ensures(), configDecl.att(), parser.getExtensionModule())))
                .collect(Collections.toSet());

        Set<Sentence> configDeclSyntax = stream(configDeclProductions).filter(Sentence::isSyntax).collect(Collections.toSet());
        Set<Sentence> configDeclRules = stream(configDeclProductions).filter(Sentence::isNonSyntax).collect(Collections.toSet());

        if (module.name().endsWith(Import.IMPORTS_SYNTAX_SUFFIX)) {
            Module mapModule;
            if (def.getModule("MAP$SYNTAX").isDefined()) {
                mapModule = def.getModule("MAP$SYNTAX").get();
            } else {
                throw KEMException.compilerError("Module Map must be visible at the configuration declaration, in module " + module.name());
            }
            return Module(module.name(), (Set<Module>) module.imports().$bar(Set(mapModule)),
                    (Set<Sentence>) module.localSentences().$bar(configDeclSyntax),
                    module.att());
        } else {
            Module mapModule;
            if (def.getModule("MAP").isDefined()) {
                mapModule = def.getModule("MAP").get();
            } else {
                throw KEMException.compilerError("Module Map must be visible at the configuration declaration, in module " + module.name());
            }
            return Module(module.name(), (Set<Module>) module.imports().$bar(Set(mapModule)),
                    (Set<Sentence>) module.localSentences().$bar(configDeclRules),
                    module.att());
        }
    }
}