From 2ac5491b4481bb44f01af55df65dfaf491e754f1 Mon Sep 17 00:00:00 2001
From: Ellen Arvidsson <ellen@log-e.se>
Date: Wed, 9 Apr 2025 18:42:43 +0200
Subject: [PATCH] started writing c implementation of sappho

---
 CMakeLists.txt       | 27 +++++++++++++
 include/spho/data.h  |  4 ++
 include/spho/parse.h |  7 ++++
 include/spho/tp.h    | 94 ++++++++++++++++++++++++++++++++++++++++++++
 src/run/devcheck.c   |  0
 src/spho/tp.c        |  2 +
 6 files changed, 134 insertions(+)
 create mode 100644 CMakeLists.txt
 create mode 100644 include/spho/data.h
 create mode 100644 include/spho/parse.h
 create mode 100644 include/spho/tp.h
 create mode 100644 src/run/devcheck.c
 create mode 100644 src/spho/tp.c

diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 0000000..b72bfd6
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,27 @@
+cmake_minimum_required(VERSION 3.31)
+project(log-e-sappho C)
+
+set(CMAKE_C_STANDARD 99)
+set(CMAKE_C_STANDARD_REQUIRED True)
+
+set(INCLUDE_DIR include)
+set(SRC_DIR src)
+
+set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho)
+
+set(SPHO_HEADER
+  ${SPHO_HEADER_DIR}/data.h
+  ${SPHO_HEADER_DIR}/parse.h
+  ${SPHO_HEADER_DIR}/tp.h
+)
+
+set(SPHO_SRC
+  ${SRC_DIR}/spho/tp.c
+)
+
+add_library(spho STATIC ${SPHO_HEADER} ${SPHO_SRC})
+target_include_directories(spho PRIVATE ${INCLUDE_DIR})
+
+add_executable(devcheck ${SRC_DIR}/run/devcheck.c)
+target_link_libraries(devcheck spho)
+target_include_directories(devcheck PRIVATE ${INCLUDE_DIR})
diff --git a/include/spho/data.h b/include/spho/data.h
new file mode 100644
index 0000000..7440a4d
--- /dev/null
+++ b/include/spho/data.h
@@ -0,0 +1,4 @@
+#ifndef _SPHO_DATA_H
+#define _SPHO_DATA_H
+
+#endif
\ No newline at end of file
diff --git a/include/spho/parse.h b/include/spho/parse.h
new file mode 100644
index 0000000..f534f68
--- /dev/null
+++ b/include/spho/parse.h
@@ -0,0 +1,7 @@
+#ifndef _SPHO_PARSE_H
+#define _SPHO_PARSE_H
+
+
+
+
+#endif
\ No newline at end of file
diff --git a/include/spho/tp.h b/include/spho/tp.h
new file mode 100644
index 0000000..09a0d18
--- /dev/null
+++ b/include/spho/tp.h
@@ -0,0 +1,94 @@
+#ifndef _SPHO_TP_H
+#define _SPHO_TP_H
+
+#define SPHO_TP_FORM_UNKNOWN    0x00
+
+#define SPHO_TP_FORM_DISJ       0x10
+#define SPHO_TP_FORM_CONJ       0x11
+#define SPHO_TP_FORM_IMPL       0x12
+#define SPHO_TP_FORM_BOX        0x13
+#define SPHO_TP_FORM_FORALL     0x14
+#define SPHO_TP_FORM_ALIAS      0x15
+
+#define SPHO_TP_FORM_FALSE      0x20
+#define SPHO_TP_FORM_TRUE       0x21
+#define SPHO_TP_FORM_VAR        0x22
+#define SPHO_TP_FORM_NOM        0x23
+
+#define SPHO_TP_FORM_REC        0x23
+
+// TODO explain
+#define SPHO_TP_FORM_SUB        0x96
+
+/* base defs */
+struct spho_name {
+  char                str[128];
+};
+
+struct spho_var {
+  struct spho_name    name;
+};
+
+struct spho_alias {
+  struct spho_name    name;
+};
+
+struct spho_nominal {
+  struct spho_name    name;
+};
+
+struct spho_record {
+  struct spho_name    mname;
+  struct spho_tp      *tp;
+};
+
+/* type data */
+struct tp_bin_data {
+  struct spho_tp    *left;
+  struct spho_tp    *right;
+};
+
+struct tp_box_data {
+  struct spho_tp    *tp;
+};
+
+struct tp_forall_data {
+  struct spho_var   *var;
+  struct spho_tp    *tp;
+};
+
+struct tp_alias_data {
+  struct spho_alias       *alias;
+  struct spho_tp_list     *l;
+};
+
+struct tp_const_data {
+  struct spho_const       *c;
+};
+
+struct tp_nominal_data {
+  struct spho_nominal     *name;
+};
+
+struct tp_record_data {
+  struct spho_record      *r;
+};
+
+/* type data union */
+union tp_data {
+  struct tp_bin_data      binop;
+  struct tp_box_data      box;
+  struct tp_forall_data   fa;
+  struct tp_alias_data    alias;
+  struct tp_const_data    cnst;
+  struct tp_nominal_data  nom;
+  struct tp_record_data   rec;
+};
+
+/* sappho type */
+struct spho_tp {
+  int               form;
+  union tp_data     data;
+};
+
+#endif
\ No newline at end of file
diff --git a/src/run/devcheck.c b/src/run/devcheck.c
new file mode 100644
index 0000000..e69de29
diff --git a/src/spho/tp.c b/src/spho/tp.c
new file mode 100644
index 0000000..dac68f0
--- /dev/null
+++ b/src/spho/tp.c
@@ -0,0 +1,2 @@
+#include "spho/tp.h"
+