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