From 7e3c7c88eacfdb473ec5e94a88de99ebce766404 Mon Sep 17 00:00:00 2001
From: Ellen Arvidsson <ellen@log-e.se>
Date: Mon, 5 May 2025 13:05:03 +0200
Subject: [PATCH] added type grammar to readme, add example, del spho loc

---
 README.md          | 27 ++++++++++++++++++++++++++-
 example/ex5.msph   | 21 +++++++++++++++++++++
 include/spho/loc.h | 34 ----------------------------------
 3 files changed, 47 insertions(+), 35 deletions(-)
 create mode 100644 example/ex5.msph
 delete mode 100644 include/spho/loc.h

diff --git a/README.md b/README.md
index eeb41ff..5f66243 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,26 @@
-# log-e-sappho
\ No newline at end of file
+# log-e-sappho
+
+experimental type system implementation
+
+## sappho grammar
+
+```
+s, t ::= s | t              (disjunction, a.k.a. union)
+       | s & t              (conjunction, a.k.a. intersection)
+       | s => t             (implication)
+       | s -> t             (arrow, a.k.a. function)
+       | forall x . t       (forall, polymorphic)
+       | box t              (box, modular logic)
+       | a [t..]            (type operator application)
+       | x                  (variable)
+       | n                  (nominal)
+       | true               (true, a.k.a. top)
+       | false              (false, a.k.a. bottom)
+       | { m : t }          (member, a.k.a. atomic record)
+
+
+x ∈ var
+n ∈ nominal
+a ∈ opname
+```
+
diff --git a/example/ex5.msph b/example/ex5.msph
new file mode 100644
index 0000000..5774e54
--- /dev/null
+++ b/example/ex5.msph
@@ -0,0 +1,21 @@
+nominal N
+nominal M
+
+
+type T[X, Y] = {
+	// body
+}
+
+type A = T[N, M] // binding X -> N, Y -> M
+type B = T[M, N] // binding X -> M, Y -> N
+
+// converted to
+
+type A = ⟨ X -> N, Y -> M ⟩ {
+	// body
+}
+type B = ⟨ X -> M, Y -> N ⟩ {
+	// body
+}
+
+
diff --git a/include/spho/loc.h b/include/spho/loc.h
deleted file mode 100644
index bf6e425..0000000
--- a/include/spho/loc.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#ifndef _SPHO_LOC_H
-#define _SPHO_LOC_H
-
-#define SPHO_LOCTYPE_LINE         1
-#define SPHO_LOCTYPE_LINE_COL     2
-
-
-struct spho_loc_line {
-  char          *fpath;
-  unsigned int  lineno;
-};
-
-struct spho_loc_line {
-  char          *fpath;
-  unsigned int  lineno;
-  unsigned int  colno;
-};
-
-union spho_loc_info {
-  struct spho_loc_line    line;
-};
-
-struct spho_loc {
-  struct spho_ctx         *ctx;
-  int                     loctype;
-  union spho_loc_info     locinfo;
-};
-
-char            *spho_loc_str(struct spho_loc *);
-struct spho_loc *spho_loc_create_line(struct spho_ctx *, char *, int);
-struct spho_loc *spho_loc_create_linecol(struct spho_ctx *, char *, int, int);
-void            spho_loc_destroy(struct spho_loc *);
-
-#endif