From 59dd901fbe76fc1dfc2d0fd3b725c47735f4bb1c Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
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/drl/gate.ml | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100644 lib/drl/gate.ml

(limited to 'lib/drl/gate.ml')

diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml
new file mode 100644
index 0000000..222e935
--- /dev/null
+++ b/lib/drl/gate.ml
@@ -0,0 +1,82 @@
+(** Finiteness gate for DRL queries.
+
+    Converts Sakura types to Coq-extracted types and calls the
+    verified [predicted_finite] function. Rejects queries whose
+    result cannot be statically proven finite. *)
+
+(* -- string -> char list impedance --------------------------------- *)
+
+let string_to_chars (s : string) : char list =
+  List.init (String.length s) (String.get s)
+
+(* -- Sakura AST -> extracted AST ----------------------------------- *)
+
+let rec query_of_ast : Ast.query -> Drl_verified.query = function
+  | Ast.Base name ->
+    Drl_verified.Base (string_to_chars name)
+  | Ast.Const pairs ->
+    Drl_verified.Const
+      (List.map
+         (fun (k, v) ->
+           (string_to_chars k, value_of_ast_value v))
+         pairs)
+  | Ast.Select (filter, source) ->
+    Drl_verified.Select (query_of_ast filter, query_of_ast source)
+  | Ast.Join (attrs, q1, q2) ->
+    Drl_verified.Join
+      (List.map string_to_chars attrs, query_of_ast q1, query_of_ast q2)
+  | Ast.Cartesian (q1, q2) ->
+    Drl_verified.Cartesian (query_of_ast q1, query_of_ast q2)
+  | Ast.Project (attrs, q) ->
+    Drl_verified.Project (List.map string_to_chars attrs, query_of_ast q)
+  | Ast.Rename (renames, q) ->
+    Drl_verified.Rename
+      (List.map
+         (fun (o, n) -> (string_to_chars o, string_to_chars n))
+         renames,
+       query_of_ast q)
+  | Ast.Union (q1, q2) ->
+    Drl_verified.Union (query_of_ast q1, query_of_ast q2)
+  | Ast.Diff (q1, q2) ->
+    Drl_verified.Diff (query_of_ast q1, query_of_ast q2)
+  | Ast.Take (n, q) ->
+    Drl_verified.Take (n, query_of_ast q)
+
+and value_of_ast_value : Ast.value -> Drl_verified.literal = function
+  | Ast.Int n   -> Drl_verified.LitInt n
+  (* The Coq model has no float literal. This truncation is harmless:
+     the finiteness gate inspects only relation names and query structure,
+     never literal values. *)
+  | Ast.Float f -> Drl_verified.LitInt (int_of_float f)
+  | Ast.Str s   -> Drl_verified.LitStr (string_to_chars s)
+  | Ast.Bool b  -> Drl_verified.LitBool b
+
+(* -- database snapshot --------------------------------------------- *)
+
+let is_finite (c : Conventions.Cardinality.t) : bool =
+  match c with
+  | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite -> true
+  | Conventions.Cardinality.AlephZero | Conventions.Cardinality.Continuum -> false
+
+let database_snapshot (db : Management.Database.t) : Drl_verified.database =
+  Management.Database.RelationMap.fold
+    (fun name (rel : Relation.t) acc ->
+       let entry : Drl_verified.relation =
+         { rel_name   = string_to_chars name;
+           rel_finite = is_finite rel.cardinality }
+       in
+       (string_to_chars name, entry) :: acc)
+    db.relations
+    []
+
+(* -- public interface ---------------------------------------------- *)
+
+let admit (db : Management.Database.t) (ast : Ast.query) : (unit, string) result =
+  let vdb = database_snapshot db in
+  let vq = query_of_ast ast in
+  match Drl_verified.predicted_finite vdb vq with
+  | Some true -> Ok ()
+  | Some false ->
+    Error "query produces potentially infinite result; use Take to bound it"
+  | None ->
+    Error "referenced relation not found in finiteness check"
-- 
cgit v1.2.3