From 59dd901fbe76fc1dfc2d0fd3b725c47735f4bb1c Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 22 Mar 2026 00:33:50 -0300 Subject: 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 --- lib/sublanguage.ml | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 lib/sublanguage.ml (limited to 'lib/sublanguage.ml') 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 -- cgit v1.2.3