From 20c055cf729a70315b5d9ecaab5a533f242861d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 10 May 2024 13:07:08 +0000
Subject: [PATCH] Add `kdist` setup

---
 Makefile                                      |  9 +++
 pyproject.toml                                |  3 +
 src/ksoroban/kdist/__init__.py                |  0
 src/ksoroban/kdist/plugin.py                  | 58 +++++++++++++++++++
 .../kdist/soroban-semantics/soroban.md        |  4 ++
 5 files changed, 74 insertions(+)
 create mode 100644 src/ksoroban/kdist/__init__.py
 create mode 100644 src/ksoroban/kdist/plugin.py
 create mode 100644 src/ksoroban/kdist/soroban-semantics/soroban.md

diff --git a/Makefile b/Makefile
index 56b3e5e..7f5ed8d 100644
--- a/Makefile
+++ b/Makefile
@@ -20,6 +20,15 @@ poetry-install:
 	$(POETRY) install
 
 
+# Semantics
+
+kdist-build: poetry-install
+	$(POETRY) run kdist -v build soroban-semantics.llvm
+
+kdist-clean: poetry-install
+	$(POETRY) run kdist clean
+
+
 # Tests
 
 TEST_ARGS :=
diff --git a/pyproject.toml b/pyproject.toml
index a223b30..2a46790 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -10,6 +10,9 @@ authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
 ]
 
+[tool.poetry.plugins.kdist]
+soroban-semantics = "ksoroban.kdist.plugin"
+
 [tool.poetry.dependencies]
 python = "^3.10"
 pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.48", subdirectory = "pykwasm" }
diff --git a/src/ksoroban/kdist/__init__.py b/src/ksoroban/kdist/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/src/ksoroban/kdist/plugin.py b/src/ksoroban/kdist/plugin.py
new file mode 100644
index 0000000..d8b1346
--- /dev/null
+++ b/src/ksoroban/kdist/plugin.py
@@ -0,0 +1,58 @@
+from __future__ import annotations
+
+import shutil
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+from pyk.kbuild.utils import k_version
+from pyk.kdist.api import Target
+from pyk.ktool.kompile import kompile
+
+if TYPE_CHECKING:
+    from collections.abc import Callable, Mapping
+    from typing import Any, Final
+
+
+class SourceTarget(Target):
+    SRC_DIR: Final = Path(__file__).parent
+
+    def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        shutil.copytree(deps['wasm-semantics.source'] / 'wasm-semantics', output_dir / 'wasm-semantics')
+        shutil.copytree(self.SRC_DIR / 'soroban-semantics', output_dir / 'soroban-semantics')
+
+    def source(self) -> tuple[Path, ...]:
+        return (self.SRC_DIR,)
+
+    def deps(self) -> tuple[str]:
+        return ('wasm-semantics.source',)
+
+
+class KompileTarget(Target):
+    _kompile_args: Callable[[Path], Mapping[str, Any]]
+
+    def __init__(self, kompile_args: Callable[[Path], Mapping[str, Any]]):
+        self._kompile_args = kompile_args
+
+    def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        kompile_args = self._kompile_args(deps['soroban-semantics.source'])
+        kompile(output_dir=output_dir, verbose=verbose, **kompile_args)
+
+    def context(self) -> dict[str, str]:
+        return {'k-version': k_version().text}
+
+    def deps(self) -> tuple[str]:
+        return ('soroban-semantics.source',)
+
+
+__TARGETS__: Final = {
+    'source': SourceTarget(),
+    'llvm': KompileTarget(
+        lambda src_dir: {
+            'main_file': src_dir / 'soroban-semantics/soroban.md',
+            'syntax_module': 'SOROBAN',
+            'include_dirs': [src_dir],
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
+}
diff --git a/src/ksoroban/kdist/soroban-semantics/soroban.md b/src/ksoroban/kdist/soroban-semantics/soroban.md
new file mode 100644
index 0000000..43de8e7
--- /dev/null
+++ b/src/ksoroban/kdist/soroban-semantics/soroban.md
@@ -0,0 +1,4 @@
+```k
+module SOROBAN
+endmodule
+```