aboutsummaryrefslogtreecommitdiffstats
path: root/lib/drl
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--lib/drl/ast.ml36
-rw-r--r--lib/drl/executor.ml100
-rw-r--r--lib/drl/gate.ml81
-rw-r--r--lib/drl/parser.ml7
-rw-r--r--lib/drl/sublanguage.ml16
-rw-r--r--lib/drl_verified/drl_verified.ml99
-rw-r--r--lib/drl_verified/drl_verified.mli28
7 files changed, 172 insertions, 195 deletions
diff --git a/lib/drl/ast.ml b/lib/drl/ast.ml
index 2beb010..6b191bb 100644
--- a/lib/drl/ast.ml
+++ b/lib/drl/ast.ml
@@ -1,32 +1,28 @@
open Sexplib.Std
(** Literal values for Const nodes *)
-type value =
- | Int of int
- | Float of float
- | Str of string
- | Bool of bool
+type value = Int of int | Float of float | Str of string | Bool of bool
[@@deriving sexp]
(** Convert an AST value to an AbstractValue.t (Obj.t) via Obj.repr *)
let value_to_abstract : value -> Conventions.AbstractValue.t = function
- | Int n -> Obj.repr n
+ | Int n -> Obj.repr n
| Float f -> Obj.repr f
- | Str s -> Obj.repr s
- | Bool b -> Obj.repr b
+ | Str s -> Obj.repr s
+ | Bool b -> Obj.repr b
-type direction = Asc | Desc
-[@@deriving sexp]
+type direction = Asc | Desc [@@deriving sexp]
type query =
- | Base of string (** base relation by name *)
- | Const of (string * value) list (** constant single-tuple relation *)
- | Select of query * query (** σ semijoin: (filter, source) *)
- | Join of string list * query * query (** ⋈ natural equijoin on named attrs *)
- | Cartesian of query * query (** × Cartesian product *)
- | Project of string list * query (** π restrict columns *)
- | Rename of (string * string) list * query (** ρ rename (old,new) pairs *)
- | Union of query * query (** ∪ — compatible schemas assumed *)
- | Diff of query * query (** − *)
- | Take of int * query (** τ *)
+ | Base of string (** base relation by name *)
+ | Const of (string * value) list (** constant single-tuple relation *)
+ | Select of query * query (** σ semijoin: (filter, source) *)
+ | Join of string list * query * query
+ (** ⋈ natural equijoin on named attrs *)
+ | Cartesian of query * query (** × Cartesian product *)
+ | Project of string list * query (** π restrict columns *)
+ | Rename of (string * string) list * query (** ρ rename (old,new) pairs *)
+ | Union of query * query (** ∪ — compatible schemas assumed *)
+ | Diff of query * query (** − *)
+ | Take of int * query (** τ *)
[@@deriving sexp]
diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml
index 322fada..f1732eb 100644
--- a/lib/drl/executor.ml
+++ b/lib/drl/executor.ml
@@ -1,74 +1,74 @@
-module Make(Storage : Management.Physical.S) = struct
- module Alg = Algebra.Make(Storage)
- module Ops = Manipulation.Make(Storage)
+module Make (Storage : Management.Physical.S) = struct
+ module Alg = Algebra.Make (Storage)
+ module Ops = Manipulation.Make (Storage)
type error =
- | ParseError of string
+ | ParseError of string
| RelationNotFound of string
- | AlgebraError of Algebra.error
+ | AlgebraError of Algebra.error
let sexp_of_error e =
let open Sexplib.Sexp in
match e with
- | ParseError s -> List [Atom "parse-error"; Atom s]
- | RelationNotFound s -> List [Atom "relation-not-found"; Atom s]
- | AlgebraError (Algebra.StorageError s) -> List [Atom "storage-error"; Atom s]
- | AlgebraError (Algebra.GeneratorError s) -> List [Atom "generator-error"; Atom s]
+ | ParseError s -> List [ Atom "parse-error"; Atom s ]
+ | RelationNotFound s -> List [ Atom "relation-not-found"; Atom s ]
+ | AlgebraError (Algebra.StorageError s) ->
+ List [ Atom "storage-error"; Atom s ]
+ | AlgebraError (Algebra.GeneratorError s) ->
+ List [ Atom "generator-error"; Atom s ]
let wrap = Result.map_error (fun e -> AlgebraError e)
-
let ast_value_to_abstract = Ast.value_to_abstract
- let rec execute
- (storage : Storage.t)
- (db : Management.Database.t)
- (q : Ast.query)
- : (Relation.t, error) Result.t =
+ let rec execute (storage : Storage.t) (db : Management.Database.t)
+ (q : Ast.query) : (Relation.t, error) Result.t =
let ( >>= ) = Result.bind in
match q with
- | Ast.Base name ->
- (match Ops.get_relation db ~name with
- | None -> Error (RelationNotFound name)
- | Some rel -> Ok rel)
+ | Ast.Base name -> (
+ match Ops.get_relation db ~name with
+ | None -> Error (RelationNotFound name)
+ | Some rel -> Ok rel)
| Ast.Const pairs ->
- Ok (Alg.const_relation
- (List.map (fun (k, v) -> (k, ast_value_to_abstract v)) pairs))
+ Ok
+ (Alg.const_relation
+ (List.map (fun (k, v) -> (k, ast_value_to_abstract v)) pairs))
| Ast.Select (filter_q, source_q) ->
- execute storage db filter_q >>= fun filter ->
- execute storage db source_q >>= fun source ->
- (* semijoin = project(source attrs, equijoin on common attrs) *)
- let common = List.filter_map (fun (n, _) ->
- if List.exists (fun (m, _) -> m = n) filter.Relation.schema
- then Some n else None) source.Relation.schema in
- let source_attrs = List.map fst source.Relation.schema in
- wrap (Alg.equijoin storage common source filter) >>= fun joined ->
- wrap (Alg.project storage source_attrs joined)
+ execute storage db filter_q >>= fun filter ->
+ execute storage db source_q >>= fun source ->
+ (* semijoin = project(source attrs, equijoin on common attrs) *)
+ let common =
+ List.filter_map
+ (fun (n, _) ->
+ if List.exists (fun (m, _) -> m = n) filter.Relation.schema then
+ Some n
+ else None)
+ source.Relation.schema
+ in
+ let source_attrs = List.map fst source.Relation.schema in
+ wrap (Alg.equijoin storage common source filter) >>= fun joined ->
+ wrap (Alg.project storage source_attrs joined)
| Ast.Join (attrs, q1, q2) ->
- execute storage db q1 >>= fun r1 ->
- execute storage db q2 >>= fun r2 ->
- wrap (Alg.equijoin storage attrs r1 r2)
+ execute storage db q1 >>= fun r1 ->
+ execute storage db q2 >>= fun r2 ->
+ wrap (Alg.equijoin storage attrs r1 r2)
| Ast.Project (attrs, q) ->
- execute storage db q >>= fun rel ->
- wrap (Alg.project storage attrs rel)
+ execute storage db q >>= fun rel -> wrap (Alg.project storage attrs rel)
| Ast.Rename (renames, q) ->
- execute storage db q >>= fun rel ->
- wrap (Alg.rename storage renames rel)
+ execute storage db q >>= fun rel ->
+ wrap (Alg.rename storage renames rel)
| Ast.Cartesian (q1, q2) ->
- execute storage db q1 >>= fun r1 ->
- execute storage db q2 >>= fun r2 ->
- (* Cartesian product = join on no attrs *)
- wrap (Alg.equijoin storage [] r1 r2)
+ execute storage db q1 >>= fun r1 ->
+ execute storage db q2 >>= fun r2 ->
+ (* Cartesian product = join on no attrs *)
+ wrap (Alg.equijoin storage [] r1 r2)
| Ast.Union (q1, q2) ->
- execute storage db q1 >>= fun r1 ->
- execute storage db q2 >>= fun r2 ->
- wrap (Alg.union storage r1 r2)
+ execute storage db q1 >>= fun r1 ->
+ execute storage db q2 >>= fun r2 -> wrap (Alg.union storage r1 r2)
| Ast.Diff (q1, q2) ->
- execute storage db q1 >>= fun r1 ->
- execute storage db q2 >>= fun r2 ->
- wrap (Alg.diff storage r1 r2)
+ execute storage db q1 >>= fun r1 ->
+ execute storage db q2 >>= fun r2 -> wrap (Alg.diff storage r1 r2)
| Ast.Take (n, q) ->
- execute storage db q >>= fun rel ->
- wrap (Alg.take storage n rel)
+ execute storage db q >>= fun rel -> wrap (Alg.take storage n rel)
end
-module Memory = Make(Management.Physical.Memory)
+module Memory = Make (Management.Physical.Memory)
diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml
index 222e935..a314bce 100644
--- a/lib/drl/gate.ml
+++ b/lib/drl/gate.ml
@@ -1,8 +1,8 @@
(** Finiteness gate for DRL queries.
- Converts Sakura types to Coq-extracted types and calls the
- verified [predicted_finite] function. Rejects queries whose
- result cannot be statically proven finite. *)
+ Converts Sakura types to Coq-extracted types and calls the verified
+ [predicted_finite] function. Rejects queries whose result cannot be
+ statically proven finite. *)
(* -- string -> char list impedance --------------------------------- *)
@@ -12,71 +12,68 @@ let string_to_chars (s : string) : char list =
(* -- Sakura AST -> extracted AST ----------------------------------- *)
let rec query_of_ast : Ast.query -> Drl_verified.query = function
- | Ast.Base name ->
- Drl_verified.Base (string_to_chars name)
+ | Ast.Base name -> Drl_verified.Base (string_to_chars name)
| Ast.Const pairs ->
- Drl_verified.Const
- (List.map
- (fun (k, v) ->
- (string_to_chars k, value_of_ast_value v))
- pairs)
+ Drl_verified.Const
+ (List.map
+ (fun (k, v) -> (string_to_chars k, value_of_ast_value v))
+ pairs)
| Ast.Select (filter, source) ->
- Drl_verified.Select (query_of_ast filter, query_of_ast source)
+ Drl_verified.Select (query_of_ast filter, query_of_ast source)
| Ast.Join (attrs, q1, q2) ->
- Drl_verified.Join
- (List.map string_to_chars attrs, query_of_ast q1, query_of_ast q2)
+ Drl_verified.Join
+ (List.map string_to_chars attrs, query_of_ast q1, query_of_ast q2)
| Ast.Cartesian (q1, q2) ->
- Drl_verified.Cartesian (query_of_ast q1, query_of_ast q2)
+ Drl_verified.Cartesian (query_of_ast q1, query_of_ast q2)
| Ast.Project (attrs, q) ->
- Drl_verified.Project (List.map string_to_chars attrs, query_of_ast q)
+ Drl_verified.Project (List.map string_to_chars attrs, query_of_ast q)
| Ast.Rename (renames, q) ->
- Drl_verified.Rename
- (List.map
- (fun (o, n) -> (string_to_chars o, string_to_chars n))
- renames,
- query_of_ast q)
- | Ast.Union (q1, q2) ->
- Drl_verified.Union (query_of_ast q1, query_of_ast q2)
- | Ast.Diff (q1, q2) ->
- Drl_verified.Diff (query_of_ast q1, query_of_ast q2)
- | Ast.Take (n, q) ->
- Drl_verified.Take (n, query_of_ast q)
+ Drl_verified.Rename
+ ( List.map (fun (o, n) -> (string_to_chars o, string_to_chars n)) renames,
+ query_of_ast q )
+ | Ast.Union (q1, q2) -> Drl_verified.Union (query_of_ast q1, query_of_ast q2)
+ | Ast.Diff (q1, q2) -> Drl_verified.Diff (query_of_ast q1, query_of_ast q2)
+ | Ast.Take (n, q) -> Drl_verified.Take (n, query_of_ast q)
and value_of_ast_value : Ast.value -> Drl_verified.literal = function
- | Ast.Int n -> Drl_verified.LitInt n
+ | Ast.Int n -> Drl_verified.LitInt n
(* The Coq model has no float literal. This truncation is harmless:
the finiteness gate inspects only relation names and query structure,
never literal values. *)
| Ast.Float f -> Drl_verified.LitInt (int_of_float f)
- | Ast.Str s -> Drl_verified.LitStr (string_to_chars s)
- | Ast.Bool b -> Drl_verified.LitBool b
+ | Ast.Str s -> Drl_verified.LitStr (string_to_chars s)
+ | Ast.Bool b -> Drl_verified.LitBool b
(* -- database snapshot --------------------------------------------- *)
let is_finite (c : Conventions.Cardinality.t) : bool =
match c with
- | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite -> true
- | Conventions.Cardinality.AlephZero | Conventions.Cardinality.Continuum -> false
+ | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite
+ ->
+ true
+ | Conventions.Cardinality.AlephZero | Conventions.Cardinality.Continuum ->
+ false
let database_snapshot (db : Management.Database.t) : Drl_verified.database =
Management.Database.RelationMap.fold
(fun name (rel : Relation.t) acc ->
- let entry : Drl_verified.relation =
- { rel_name = string_to_chars name;
- rel_finite = is_finite rel.cardinality }
- in
- (string_to_chars name, entry) :: acc)
- db.relations
- []
+ let entry : Drl_verified.relation =
+ {
+ rel_name = string_to_chars name;
+ rel_finite = is_finite rel.cardinality;
+ }
+ in
+ (string_to_chars name, entry) :: acc)
+ db.relations []
(* -- public interface ---------------------------------------------- *)
-let admit (db : Management.Database.t) (ast : Ast.query) : (unit, string) result =
+let admit (db : Management.Database.t) (ast : Ast.query) : (unit, string) result
+ =
let vdb = database_snapshot db in
let vq = query_of_ast ast in
match Drl_verified.predicted_finite vdb vq with
| Some true -> Ok ()
| Some false ->
- Error "query produces potentially infinite result; use Take to bound it"
- | None ->
- Error "referenced relation not found in finiteness check"
+ Error "query produces potentially infinite result; use Take to bound it"
+ | None -> Error "referenced relation not found in finiteness check"
diff --git a/lib/drl/parser.ml b/lib/drl/parser.ml
index 36ce15a..76d4b4e 100644
--- a/lib/drl/parser.ml
+++ b/lib/drl/parser.ml
@@ -2,13 +2,12 @@ type error = ParseError of string
let of_sexp sexp =
match Ast.query_of_sexp sexp with
- | q -> Ok q
+ | q -> Ok q
| exception exn -> Error (ParseError (Printexc.to_string exn))
let of_string s =
match Sexplib.Sexp.of_string s |> Ast.query_of_sexp with
- | q -> Ok q
+ | q -> Ok q
| exception exn -> Error (ParseError (Printexc.to_string exn))
-let to_string q =
- Ast.sexp_of_query q |> Sexplib.Sexp.to_string_hum
+let to_string q = Ast.sexp_of_query q |> Sexplib.Sexp.to_string_hum
diff --git a/lib/drl/sublanguage.ml b/lib/drl/sublanguage.ml
index f57af95..ce69b56 100644
--- a/lib/drl/sublanguage.ml
+++ b/lib/drl/sublanguage.ml
@@ -1,9 +1,9 @@
module Make (Storage : Management.Physical.S) = struct
- module Exec = Executor.Make(Storage)
+ module Exec = Executor.Make (Storage)
type storage = Storage.t
- type ast = Ast.query
- type error = Exec.error
+ type ast = Ast.query
+ type error = Exec.error
let name = "drl"
@@ -15,12 +15,12 @@ module Make (Storage : Management.Physical.S) = struct
let execute storage db ast =
match Gate.admit db ast with
| Error msg -> Error (Exec.ParseError msg)
- | Ok () ->
- match Exec.execute storage db ast with
- | Ok rel -> Ok (Sublanguage.Query rel)
- | Error e -> Error e
+ | Ok () -> (
+ match Exec.execute storage db ast with
+ | Ok rel -> Ok (Sublanguage.Query rel)
+ | Error e -> Error e)
let sexp_of_error = Exec.sexp_of_error
end
-module Memory = Make(Management.Physical.Memory)
+module Memory = Make (Management.Physical.Memory)
diff --git a/lib/drl_verified/drl_verified.ml b/lib/drl_verified/drl_verified.ml
index b5aeaa7..868af2a 100644
--- a/lib/drl_verified/drl_verified.ml
+++ b/lib/drl_verified/drl_verified.ml
@@ -1,76 +1,67 @@
-
(** val eqb : char list -> char list -> bool **)
let rec eqb s1 s2 =
match s1 with
- | [] -> (match s2 with
- | [] -> true
- | _::_ -> false)
- | c1::s1' ->
- (match s2 with
- | [] -> false
- | c2::s2' -> if (=) c1 c2 then eqb s1' s2' else false)
+ | [] -> ( match s2 with [] -> true | _ :: _ -> false)
+ | c1 :: s1' -> (
+ match s2 with
+ | [] -> false
+ | c2 :: s2' -> if c1 = c2 then eqb s1' s2' else false)
type attr_name = char list
-
type relation = { rel_name : char list; rel_finite : bool }
-
type database = (char list * relation) list
(** val db_lookup : char list -> database -> relation option **)
let rec db_lookup name = function
-| [] -> None
-| p :: rest ->
- let (n, r) = p in if eqb name n then Some r else db_lookup name rest
+ | [] -> None
+ | p :: rest ->
+ let n, r = p in
+ if eqb name n then Some r else db_lookup name rest
-type literal =
-| LitInt of int
-| LitStr of char list
-| LitBool of bool
+type literal = LitInt of int | LitStr of char list | LitBool of bool
type query =
-| Base of char list
-| Const of (attr_name * literal) list
-| Select of query * query
-| Join of attr_name list * query * query
-| Cartesian of query * query
-| Project of attr_name list * query
-| Rename of (attr_name * attr_name) list * query
-| Union of query * query
-| Diff of query * query
-| Take of int * query
+ | Base of char list
+ | Const of (attr_name * literal) list
+ | Select of query * query
+ | Join of attr_name list * query * query
+ | Cartesian of query * query
+ | Project of attr_name list * query
+ | Rename of (attr_name * attr_name) list * query
+ | Union of query * query
+ | Diff of query * query
+ | Take of int * query
(** val predicted_finite : database -> query -> bool option **)
let rec predicted_finite db = function
-| Base name ->
- (match db_lookup name db with
- | Some r -> Some r.rel_finite
- | None -> None)
-| Select (_, source) -> predicted_finite db source
-| Join (_, q1, q2) ->
- (match predicted_finite db q1 with
- | Some f1 ->
- (match predicted_finite db q2 with
- | Some f2 -> Some ((&&) f1 f2)
+ | Base name -> (
+ match db_lookup name db with Some r -> Some r.rel_finite | None -> None)
+ | Select (_, source) -> predicted_finite db source
+ | Join (_, q1, q2) -> (
+ match predicted_finite db q1 with
+ | Some f1 -> (
+ match predicted_finite db q2 with
+ | Some f2 -> Some (f1 && f2)
+ | None -> None)
| None -> None)
- | None -> None)
-| Cartesian (q1, q2) ->
- (match predicted_finite db q1 with
- | Some f1 ->
- (match predicted_finite db q2 with
- | Some f2 -> Some ((&&) f1 f2)
+ | Cartesian (q1, q2) -> (
+ match predicted_finite db q1 with
+ | Some f1 -> (
+ match predicted_finite db q2 with
+ | Some f2 -> Some (f1 && f2)
+ | None -> None)
| None -> None)
- | None -> None)
-| Project (_, q0) -> predicted_finite db q0
-| Rename (_, q0) -> predicted_finite db q0
-| Union (q1, q2) ->
- (match predicted_finite db q1 with
- | Some f1 ->
- (match predicted_finite db q2 with
- | Some f2 -> Some ((&&) f1 f2)
+ | Project (_, q0) -> predicted_finite db q0
+ | Rename (_, q0) -> predicted_finite db q0
+ | Union (q1, q2) -> (
+ match predicted_finite db q1 with
+ | Some f1 -> (
+ match predicted_finite db q2 with
+ | Some f2 -> Some (f1 && f2)
+ | None -> None)
| None -> None)
- | None -> None)
-| Diff (q1, _) -> predicted_finite db q1
-| _ -> Some true
+ | Diff (q1, _) -> predicted_finite db q1
+ | _ -> Some true
diff --git a/lib/drl_verified/drl_verified.mli b/lib/drl_verified/drl_verified.mli
index 31acc7a..dac930e 100644
--- a/lib/drl_verified/drl_verified.mli
+++ b/lib/drl_verified/drl_verified.mli
@@ -1,29 +1,23 @@
-
val eqb : char list -> char list -> bool
type attr_name = char list
-
type relation = { rel_name : char list; rel_finite : bool }
-
type database = (char list * relation) list
val db_lookup : char list -> database -> relation option
-type literal =
-| LitInt of int
-| LitStr of char list
-| LitBool of bool
+type literal = LitInt of int | LitStr of char list | LitBool of bool
type query =
-| Base of char list
-| Const of (attr_name * literal) list
-| Select of query * query
-| Join of attr_name list * query * query
-| Cartesian of query * query
-| Project of attr_name list * query
-| Rename of (attr_name * attr_name) list * query
-| Union of query * query
-| Diff of query * query
-| Take of int * query
+ | Base of char list
+ | Const of (attr_name * literal) list
+ | Select of query * query
+ | Join of attr_name list * query * query
+ | Cartesian of query * query
+ | Project of attr_name list * query
+ | Rename of (attr_name * attr_name) list * query
+ | Union of query * query
+ | Diff of query * query
+ | Take of int * query
val predicted_finite : database -> query -> bool option
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 05:56:17 +0000