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, 26 insertions, 0 deletions

diff --git a/proof/Relation.v b/proof/Relation.v
new file mode 100644
index 0000000..f7c087d
--- /dev/null
+++ b/proof/Relation.v
@@ -0,0 +1,26 @@
+(** * Relation: minimal model for finiteness checking
+
+    A relation is reduced to the two fields that [predicted_finite]
+    actually inspects: its name (for database lookup) and its
+    finiteness flag (for the gate decision). *)
+
+From Stdlib Require Import List.
+From Stdlib Require Import String.
+Require Import Schema.
+Import ListNotations.
+
+Record relation := mkRelation {
+  rel_name   : string;
+  rel_finite : bool;
+}.
+
+(** A database is a named collection of relations. *)
+Definition database := list (string * relation).
+
+(** Look up a relation by name. *)
+Fixpoint db_lookup (name : string) (db : database) : option relation :=
+  match db with
+  | []            => None
+  | (n, r) :: rest =>
+    if String.eqb name n then Some r else db_lookup name rest
+  end.