From 63ae3c930de89af6f85229a467caa3f53cb844a2 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Fri, 3 Apr 2026 16:17:38 -0300 Subject: format --- lib/drl/ast.ml | 36 ++++++++---------- lib/drl/executor.ml | 100 ++++++++++++++++++++++++------------------------- lib/drl/gate.ml | 81 +++++++++++++++++++-------------------- lib/drl/parser.ml | 7 ++-- lib/drl/sublanguage.ml | 16 ++++---- 5 files changed, 116 insertions(+), 124 deletions(-) (limited to 'lib/drl') 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) -- cgit v1.2.3