blob: fd179a17679ec0f4162eacf6ac439d7ad2557d2e (
plain) (
tree)
|
|
(** * 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.
|
