1 files changed, 0 insertions, 67 deletions
diff --git a/proof/Drl.v b/proof/Drl.v
deleted file mode 100644
index fd179a1..0000000
--- a/proof/Drl.v
+++ /dev/null
@@ -1,67 +0,0 @@
-(** * DRL: Data Retrieval Language — Finiteness Gate
-
-    This file defines:
-    - The DRL query AST (mirroring [lib/drl/ast.ml])
-    - [predicted_finite]: statically decides whether a query can
-      produce an infinite result based on the cardinality flags of
-      the relations it references.
-
-    [predicted_finite] is extracted to OCaml and called by
-    [lib/drl/gate.ml] before every query execution.  Queries whose
-    result cannot be statically proven finite are rejected unless
-    wrapped in a [Take]. *)
-
-From Stdlib Require Import List.
-From Stdlib Require Import String.
-From Stdlib Require Import Bool.
-Require Import Schema.
-Require Import Relation.
-Import ListNotations.
-
-(* ================================================================== *)
-(** ** AST                                                             *)
-(* ================================================================== *)
-
-Inductive literal :=
-  | LitInt  : nat    -> literal
-  | LitStr  : string -> literal
-  | LitBool : bool   -> literal.
-
-Inductive query : Type :=
-  | Base      : string                           -> query
-  | Const     : list (attr_name * literal)       -> query
-  | Select    : query -> query                   -> query
-  | Join      : list attr_name -> query -> query -> query
-  | Cartesian : query -> query                   -> query
-  | Project   : list attr_name -> query          -> query
-  | Rename    : list (attr_name * attr_name) -> query -> query
-  | Union     : query -> query                   -> query
-  | Diff      : query -> query                   -> query
-  | Take      : nat -> query                     -> query.
-
-(* ================================================================== *)
-(** ** Finiteness Prediction                                           *)
-(* ================================================================== *)
-
-(** Conservatively predict whether a query produces a finite result.
-    Returns [Some true] if guaranteed finite, [Some false] if not,
-    [None] if a referenced relation is not found in the database. *)
-Fixpoint predicted_finite (db : database) (q : query) : option bool :=
-  match q with
-  | Base name =>
-    match db_lookup name db with
-    | Some r => Some (rel_finite r)
-    | None   => None
-    end
-  | Const _  => Some true
-  | Take _ _ => Some true
-  | Select _ source =>
-    predicted_finite db source
-  | Join _ q1 q2 | Cartesian q1 q2 | Union q1 q2 =>
-    match predicted_finite db q1, predicted_finite db q2 with
-    | Some f1, Some f2 => Some (f1 && f2)
-    | _,       _       => None
-    end
-  | Diff q1 _  => predicted_finite db q1
-  | Project _ q' | Rename _ q' => predicted_finite db q'
-  end.