Skip to content

Commit

Permalink
Monolithic reformat
Browse files Browse the repository at this point in the history
  • Loading branch information
@Baltoli
Baltoli committed Oct 26, 2023
1 parent 359d0a9 commit 0a70ab5
Show file tree
Hide file tree
Showing 288 changed files with 34,339 additions and 29,032 deletions.
126 changes: 63 additions & 63 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,83 +2,83 @@
package org.kframework.backend.haskell;

import com.google.inject.Inject;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import org.kframework.attributes.Att;
import org.kframework.backend.kore.KoreBackend;
import org.kframework.compile.Backend;
import org.kframework.kompile.KompileOptions;
import org.kframework.main.GlobalOptions;
import org.kframework.main.Tool;
import org.kframework.utils.Stopwatch;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.errorsystem.KEMException;
import org.kframework.utils.errorsystem.KExceptionManager;
import org.kframework.utils.file.FileUtil;

import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.Set;
import java.util.HashSet;

public class HaskellBackend extends KoreBackend {

private final KompileOptions kompileOptions;
private final GlobalOptions globalOptions;
private final FileUtil files;
private final HaskellKompileOptions haskellKompileOptions;

@Inject
public HaskellBackend(
KompileOptions kompileOptions,
GlobalOptions globalOptions,
HaskellKompileOptions haskellKompileOptions,
FileUtil files,
KExceptionManager kem,
Tool tool) {
super(kompileOptions, files, kem, false, tool);
this.files = files;
this.haskellKompileOptions = haskellKompileOptions;
this.kompileOptions = kompileOptions;
this.globalOptions = globalOptions;
}
private final KompileOptions kompileOptions;
private final GlobalOptions globalOptions;
private final FileUtil files;
private final HaskellKompileOptions haskellKompileOptions;

@Inject
public HaskellBackend(
KompileOptions kompileOptions,
GlobalOptions globalOptions,
HaskellKompileOptions haskellKompileOptions,
FileUtil files,
KExceptionManager kem,
Tool tool) {
super(kompileOptions, files, kem, false, tool);
this.files = files;
this.haskellKompileOptions = haskellKompileOptions;
this.kompileOptions = kompileOptions;
this.globalOptions = globalOptions;
}

@Override
public void accept(Backend.Holder h) {
Stopwatch sw = new Stopwatch(globalOptions);
String kore = getKompiledString(h.def, true);
h.def = null;
files.saveToKompiled("definition.kore", kore);
sw.printIntermediate(" Print definition.kore");
ProcessBuilder pb = files.getProcessBuilder();
List<String> args = new ArrayList<>();
if (haskellKompileOptions.noHaskellBinary) {
args.add("kore-parser");
args.add("--no-print-definition");
args.add("definition.kore");
} else {
args.add(haskellKompileOptions.haskellBackendCommand);
args.add("definition.kore");
args.add("--module");
args.add(kompileOptions.mainModule(files));
args.add("--output");
args.add("haskellDefinition.bin");
args.add("--serialize");
}
try {
Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
int exit = p.waitFor();
if (exit != 0) {
throw KEMException.criticalError("Haskell backend reported errors validating compiled definition.\nExamine output to see errors.");
}
} catch (IOException | InterruptedException e) {
throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
}
sw.printIntermediate(" Validate def");
@Override
public void accept(Backend.Holder h) {
Stopwatch sw = new Stopwatch(globalOptions);
String kore = getKompiledString(h.def, true);
h.def = null;
files.saveToKompiled("definition.kore", kore);
sw.printIntermediate(" Print definition.kore");
ProcessBuilder pb = files.getProcessBuilder();
List<String> args = new ArrayList<>();
if (haskellKompileOptions.noHaskellBinary) {
args.add("kore-parser");
args.add("--no-print-definition");
args.add("definition.kore");
} else {
args.add(haskellKompileOptions.haskellBackendCommand);
args.add("definition.kore");
args.add("--module");
args.add(kompileOptions.mainModule(files));
args.add("--output");
args.add("haskellDefinition.bin");
args.add("--serialize");
}

@Override
public Set<Att.Key> excludedModuleTags() {
return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
try {
Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
int exit = p.waitFor();
if (exit != 0) {
throw KEMException.criticalError(
"Haskell backend reported errors validating compiled definition.\n"
+ "Examine output to see errors.");
}
} catch (IOException | InterruptedException e) {
throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
}
sw.printIntermediate(" Validate def");
}

@Override
public Set<Att.Key> excludedModuleTags() {
return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
}
}
119 changes: 60 additions & 59 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,80 +6,81 @@
import com.google.inject.Module;
import com.google.inject.TypeLiteral;
import com.google.inject.multibindings.MapBinder;
import java.util.Collections;
import java.util.List;
import java.util.function.Function;
import org.apache.commons.lang3.tuple.Pair;
import org.kframework.definition.Definition;
import org.kframework.main.AbstractKModule;
import org.kframework.rewriter.Rewriter;

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

/**
* Created by traiansf on 9/13/18.
*/
/** Created by traiansf on 9/13/18. */
public class HaskellBackendKModule extends AbstractKModule {

@Override
public List<Module> getKompileModules() {
List<Module> mods = super.getKompileModules();
mods.add(new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
installHaskellBackend(binder());
}
@Override
public List<Module> getKompileModules() {
List<Module> mods = super.getKompileModules();
mods.add(
new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
installHaskellBackend(binder());
}
});
return mods;
}
return mods;
}

private void installHaskellBackend(Binder binder) {
MapBinder<String, org.kframework.compile.Backend> mapBinder = MapBinder.newMapBinder(
binder, String.class, org.kframework.compile.Backend.class);
mapBinder.addBinding("haskell").to(HaskellBackend.class);
}
private void installHaskellBackend(Binder binder) {
MapBinder<String, org.kframework.compile.Backend> mapBinder =
MapBinder.newMapBinder(binder, String.class, org.kframework.compile.Backend.class);
mapBinder.addBinding("haskell").to(HaskellBackend.class);
}

@Override
public List<Pair<Class<?>, Boolean>> krunOptions() {
return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
}
@Override
public List<Pair<Class<?>, Boolean>> krunOptions() {
return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
}

@Override
public List<Pair<Class<?>, Boolean>> kompileOptions() {
return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
}
@Override
public List<Pair<Class<?>, Boolean>> kompileOptions() {
return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
}

@Override
public List<Module> getKRunModules() {
return Collections.singletonList(new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellRewriter(binder());
}
@Override
public List<Module> getKRunModules() {
return Collections.singletonList(
new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellRewriter(binder());
}
});
}

private void installHaskellRewriter(Binder binder) {
bindOptions(HaskellBackendKModule.this::krunOptions, binder);
}

MapBinder<String, Function<Definition, Rewriter>> rewriterBinder = MapBinder.newMapBinder(
binder, TypeLiteral.get(String.class), new TypeLiteral<Function<Definition, Rewriter>>() {
});
rewriterBinder.addBinding("haskell").to(HaskellRewriter.class);
}
private void installHaskellRewriter(Binder binder) {
bindOptions(HaskellBackendKModule.this::krunOptions, binder);

MapBinder<String, Function<Definition, Rewriter>> rewriterBinder =
MapBinder.newMapBinder(
binder,
TypeLiteral.get(String.class),
new TypeLiteral<Function<Definition, Rewriter>>() {});
rewriterBinder.addBinding("haskell").to(HaskellRewriter.class);
}

@Override
public List<Module> getKProveModules() {
return Collections.singletonList(new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellBackend(binder());
installHaskellRewriter(binder());
}
@Override
public List<Module> getKProveModules() {
return Collections.singletonList(
new AbstractModule() {
@Override
protected void configure() {
binder().requireAtInjectOnConstructors();
installHaskellBackend(binder());
installHaskellRewriter(binder());
}
});
}
}
}
58 changes: 33 additions & 25 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,31 +9,39 @@

@RequestScoped
public class HaskellKRunOptions {
@Inject
public HaskellKRunOptions() {}

@Parameter(names="--haskell-backend-command", descriptionKey = "command",
description="Command to run the Haskell backend execution engine.", hidden = true)
public String haskellBackendCommand = "kore-exec";

@Parameter(names="--haskell-backend-home", descriptionKey = "directory",
description="Directory where the Haskell backend source installation resides.", hidden = true)
public String haskellBackendHome = System.getenv("KORE_HOME");

@Parameter(names="--default-claim-type", descriptionKey = "type", converter = SentenceTypeConverter.class,
description="Default type for claims. Values: [all-path|one-path].")
public ModuleToKORE.SentenceType defaultClaimType = ModuleToKORE.SentenceType.ALL_PATH;

public static class SentenceTypeConverter extends BaseEnumConverter<ModuleToKORE.SentenceType> {

public SentenceTypeConverter(String optionName) {
super(optionName);
}

@Override
public Class<ModuleToKORE.SentenceType> enumClass() {
return ModuleToKORE.SentenceType.class;
}
@Inject
public HaskellKRunOptions() {}

@Parameter(
names = "--haskell-backend-command",
descriptionKey = "command",
description = "Command to run the Haskell backend execution engine.",
hidden = true)
public String haskellBackendCommand = "kore-exec";

@Parameter(
names = "--haskell-backend-home",
descriptionKey = "directory",
description = "Directory where the Haskell backend source installation resides.",
hidden = true)
public String haskellBackendHome = System.getenv("KORE_HOME");

@Parameter(
names = "--default-claim-type",
descriptionKey = "type",
converter = SentenceTypeConverter.class,
description = "Default type for claims. Values: [all-path|one-path].")
public ModuleToKORE.SentenceType defaultClaimType = ModuleToKORE.SentenceType.ALL_PATH;

public static class SentenceTypeConverter extends BaseEnumConverter<ModuleToKORE.SentenceType> {

public SentenceTypeConverter(String optionName) {
super(optionName);
}

@Override
public Class<ModuleToKORE.SentenceType> enumClass() {
return ModuleToKORE.SentenceType.class;
}
}
}
22 changes: 16 additions & 6 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,21 @@
@RequestScoped
public class HaskellKompileOptions {

@Inject
public HaskellKompileOptions() {}
@Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
public String haskellBackendCommand = "kore-exec";
@Inject
public HaskellKompileOptions() {}

@Parameter(names="--no-haskell-binary", description="Use the textual KORE format in the haskell backend instead of the binary KORE format. This is a development option, but may be necessary on MacOS due to known issues with the binary format.")
public boolean noHaskellBinary = false;
@Parameter(
names = "--haskell-backend-command",
description = "Command to run the Haskell backend execution engine.",
descriptionKey = "command",
hidden = true)
public String haskellBackendCommand = "kore-exec";

@Parameter(
names = "--no-haskell-binary",
description =
"Use the textual KORE format in the haskell backend instead of the binary KORE format."
+ " This is a development option, but may be necessary on MacOS due to known issues"
+ " with the binary format.")
public boolean noHaskellBinary = false;
}
Loading

0 comments on commit 0a70ab5

Please sign in to comment.