k/kernel/src/main/java/org/kframework/keq/KEqModule.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
package org.kframework.keq;

import com.google.inject.AbstractModule;
import com.google.inject.Module;
import com.google.inject.Provider;
import com.google.inject.Provides;
import com.google.inject.Scopes;
import com.google.inject.TypeLiteral;
import com.google.inject.multibindings.Multibinder;
import org.kframework.definition.Definition;
import org.kframework.kompile.BackendModule;
import org.kframework.kompile.Kompile;
import org.kframework.kompile.KompileOptions;
import org.kframework.kprove.ProofDefinitionBuilder;
import org.kframework.krun.api.io.FileSystem;
import org.kframework.krun.ioserver.filesystem.portable.PortableFileSystem;
import org.kframework.main.AnnotatedByDefinitionModule;
import org.kframework.main.FrontEnd;
import org.kframework.main.GlobalOptions;
import org.kframework.main.Tool;
import org.kframework.rewriter.Rewriter;
import org.kframework.unparser.PrintOptions;
import org.kframework.utils.errorsystem.KEMException;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.file.FileUtil;
import org.kframework.utils.inject.Annotations;
import org.kframework.utils.inject.Main;
import org.kframework.utils.inject.Options;
import org.kframework.utils.inject.RequestScoped;
import org.kframework.utils.inject.Spec1;
import org.kframework.utils.inject.Spec2;
import org.kframework.utils.options.DefinitionLoadingOptions;
import org.kframework.utils.options.SMTOptions;

import java.util.List;
import java.util.Map;
import java.util.function.Function;

public class KEqModule extends AbstractModule {
    public static class CommonModule extends AbstractModule {
        @Override
        protected void configure() {
            //bind backend implementations of tools to their interfaces
            install(new BackendModule());

            bind(FileUtil.class).in(Scopes.NO_SCOPE);
            bind(ProofDefinitionBuilder.class).in(Scopes.NO_SCOPE);
            bind(Kompile.class).in(Scopes.NO_SCOPE);
            bind(FileSystem.class).to(PortableFileSystem.class);
        }

        @Provides
        Function<Definition, Rewriter> getRewriter(KompileOptions options, Map<String, Provider<Function<Definition, Rewriter>>> map, KExceptionManager kem) {
            Provider<Function<Definition, Rewriter>> provider = map.get(options.backend);
            if (provider == null) {
                throw KEMException.criticalError("Backend " + options.backend + " does not support execution. Supported backends are: "
                        + map.keySet());
            }
            return provider.get();
        }
    }

    @Override
    protected void configure() {
        bind(FrontEnd.class).to(KEqFrontEnd.class);
        bind(Tool.class).toInstance(Tool.KEQ);

        Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder(), Object.class, Options.class);
        optionsBinder.addBinding().to(KEqOptions.class);
        Multibinder<Class<?>> experimentalOptionsBinder = Multibinder.newSetBinder(binder(), new TypeLiteral<Class<?>>() {}, Options.class);
    }

    @Provides @RequestScoped
    GlobalOptions globalOptions(KEqOptions options) {
        return options.global;
    }

    @Provides
    SMTOptions smtOptions(KEqOptions options) { return options.smt; }

    @Provides @RequestScoped
    PrintOptions printOptions(KEqOptions options) {
        return options.print;
    }

    public static class MainExecutionContextModule extends AnnotatedByDefinitionModule {

        private final List<Module> definitionSpecificModules;

        public MainExecutionContextModule(List<Module> definitionSpecificModules) {
            this.definitionSpecificModules = definitionSpecificModules;
        }

        @Override
        protected void configure() {
            exposeBindings(definitionSpecificModules, Main.class, Annotations::main);
        }

        @Provides
        DefinitionLoadingOptions defLoadingOptions(KEqOptions options) {
            return options.definitionLoading;
        }
    }

    public static class Spec1ExecutionContextModule extends AnnotatedByDefinitionModule {

        private final List<Module> definitionSpecificModules;

        public Spec1ExecutionContextModule(List<Module> definitionSpecificModules) {
            this.definitionSpecificModules = definitionSpecificModules;
        }

        @Override
        protected void configure() {
            exposeBindings(definitionSpecificModules, Spec1.class, Annotations::spec1);
        }

        @Provides
        DefinitionLoadingOptions defLoadingOptions(KEqOptions options) {
            return new DefinitionLoadingOptions(options.def1);
        }
    }

    public static class Spec2ExecutionContextModule extends AnnotatedByDefinitionModule {

        private final List<Module> definitionSpecificModules;

        public Spec2ExecutionContextModule(List<Module> definitionSpecificModules) {
            this.definitionSpecificModules = definitionSpecificModules;
        }

        @Override
        protected void configure() {
            exposeBindings(definitionSpecificModules, Spec2.class, Annotations::spec2);
        }

        @Provides
        DefinitionLoadingOptions defLoadingOptions(KEqOptions options) {
            return new DefinitionLoadingOptions(options.def2);
        }
    }
}