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 --- proof/Extraction.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 proof/Extraction.v (limited to 'proof/Extraction.v') 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. -- cgit v1.2.3