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

diff --git a/proof/Extraction.v b/proof/Extraction.v
new file mode 100644
index 0000000..dc93c21
--- /dev/null
+++ b/proof/Extraction.v
@@ -0,0 +1,17 @@
+(** * Extraction to OCaml — finiteness gate only
+
+    Extracts [predicted_finite] to [lib/drl_verified/drl_verified.ml].
+    To regenerate: cd proof && make *)
+
+From Stdlib Require Import Extraction.
+From Stdlib Require Import ExtrOcamlBasic.
+From Stdlib Require Import ExtrOcamlString.
+From Stdlib Require Import ExtrOcamlNatInt.
+
+Require Import Schema.
+Require Import Relation.
+Require Import Drl.
+
+Set Extraction Output Directory "../lib/drl_verified".
+
+Extraction "drl_verified" predicted_finite.