Sublanguages improvement & Coq experiment (#53)

* separation and functor for sublanguages

* add coq experiment for termination

* fix tests with envelopes

* add timestamp and print responses to server on terminal

* remove coq experiment for trivial cases and rework gate

* refactor nesting with let*

* remove non-envelope sublang support and tests on server

* manip_err duplication purge and better format as s-expr

* abstract storage with dispatch for sublanguages

* dead code and minor refactor due to old non-envelope parsing on subl

* refactor server to use proper dml alg error and wire ephem relations

* remove (schema)

* change .gitignore to blacklist folders

1 files changed, 29 insertions, 0 deletions

diff --git a/lib/sublanguage.ml b/lib/sublanguage.ml
new file mode 100644
index 0000000..3df91f1
--- /dev/null
+++ b/lib/sublanguage.ml
@@ -0,0 +1,29 @@
+(** Effect classification for sublanguage operations.
+
+    Categorically:
+    - Query: a natural transformation between instance functors (DRL).
+      Side-effect-free; the database state is unchanged.
+    - Transition: a morphism in the category of database states (DDL,
+      DML, ICL, DCL, and future TCL). Produces a new state via
+      substitution (Harper, PFPL ch. 3-4).
+
+    Future sublanguages:
+    - TCL -> Transition (transaction boundaries are state morphisms
+      with atomicity constraints)
+    - PPL -> new effect class: potentially non-terminating computation
+      (Turing-complete; breaks the termination guarantee of DRL)
+    - ACL -> a functor restriction: narrows the admissible natural
+      transformations based on authorization context *)
+type result =
+  | Query of Relation.t
+  | Transition of Management.Database.t * string
+
+module type S = sig
+  type storage
+  type ast
+  type error
+  val name : string
+  val parse_sexp : Sexplib.Sexp.t -> (ast, error) Result.t
+  val execute : storage -> Management.Database.t -> ast -> (result, error) Result.t
+  val sexp_of_error : error -> Sexplib.Sexp.t
+end