started writing c implementation of sappho

This commit is contained in:
Ellen Arvidsson 2025-04-09 18:42:43 +02:00
parent 549443c670
commit 2ac5491b44
6 changed files with 134 additions and 0 deletions

27
CMakeLists.txt Normal file
View file

@ -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})

4
include/spho/data.h Normal file
View file

@ -0,0 +1,4 @@
#ifndef _SPHO_DATA_H
#define _SPHO_DATA_H
#endif

7
include/spho/parse.h Normal file
View file

@ -0,0 +1,7 @@
#ifndef _SPHO_PARSE_H
#define _SPHO_PARSE_H
#endif

94
include/spho/tp.h Normal file
View file

@ -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

0
src/run/devcheck.c Normal file
View file

2
src/spho/tp.c Normal file
View file

@ -0,0 +1,2 @@
#include "spho/tp.h"