diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java index f255c032396..28b3be6d948 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java @@ -5,7 +5,6 @@ import org.kframework.attributes.Att; import org.kframework.backend.kore.KoreBackend; import org.kframework.compile.Backend; -import org.kframework.kompile.CompiledDefinition; import org.kframework.kompile.KompileOptions; import org.kframework.main.Tool; import org.kframework.utils.errorsystem.KExceptionManager; @@ -26,15 +25,18 @@ public class HaskellBackend extends KoreBackend { private final KompileOptions kompileOptions; private final FileUtil files; + private final HaskellKompileOptions haskellKompileOptions; @Inject public HaskellBackend( KompileOptions kompileOptions, + HaskellKompileOptions haskellKompileOptions, FileUtil files, KExceptionManager kem, Tool tool) { super(kompileOptions, files, kem, EnumSet.of(HEAT_RESULT, COOL_RESULT_CONDITION), false, tool); this.files = files; + this.haskellKompileOptions = haskellKompileOptions; this.kompileOptions = kompileOptions; } @@ -46,13 +48,19 @@ public void accept(Backend.Holder h) { files.saveToKompiled("definition.kore", kore); ProcessBuilder pb = files.getProcessBuilder(); List args = new ArrayList<>(); - args.add("kore-exec"); - args.add("definition.kore"); - args.add("--module"); - args.add(kompileOptions.mainModule(files)); - args.add("--output"); - args.add("haskellDefinition.bin"); - args.add("--serialize"); + 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(); diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java index 3a327bf1d75..098f1cd1579 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java @@ -26,6 +26,7 @@ public List getKompileModules() { mods.add(new AbstractModule() { @Override protected void configure() { + bindOptions(HaskellBackendKModule.this::kompileOptions, binder()); installHaskellBackend(binder()); } }); @@ -43,6 +44,11 @@ public List, Boolean>> krunOptions() { return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true)); } + @Override + public List, Boolean>> kompileOptions() { + return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true)); + } + @Override public List getKRunModules() { return Collections.singletonList(new AbstractModule() { diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java new file mode 100644 index 00000000000..6a833d21779 --- /dev/null +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java @@ -0,0 +1,15 @@ +// Copyright (c) 2014-2019 K Team. All Rights Reserved. +package org.kframework.backend.haskell; + +import com.beust.jcommander.Parameter; +import org.kframework.utils.inject.RequestScoped; + +@RequestScoped +public class HaskellKompileOptions { + + @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.") + public String haskellBackendCommand = "kore-exec"; + + @Parameter(names="--no-haskell-binary", description="Do not force the haskell backend to use the binary format. Use the textual format instead. This is a development option. Sometime the binary format can cause issues.") + public boolean noHaskellBinary = false; +} diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java index 45eb349bd24..1466abd5b64 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java @@ -111,7 +111,9 @@ public RewriterResult execute(K k, Optional depth) { Module mod = getExecutionModule(module); ModuleToKORE converter = new ModuleToKORE(mod, def.topCellInitializer, kompileOptions); String koreOutput = getKoreString(k, mod, converter); - String defPath = files.resolveKompiled("haskellDefinition.bin").getAbsolutePath(); + String defPath = files.resolveKompiled("haskellDefinition.bin").exists() ? + files.resolveKompiled("haskellDefinition.bin").getAbsolutePath() : + files.resolveKompiled("definition.kore").getAbsolutePath(); String moduleName = mod.name(); files.saveToTemp("execute-initial.kore", koreOutput); @@ -191,7 +193,9 @@ public K search(K initialConfiguration, Optional depth, Optional