diff options
Diffstat (limited to 'lib/drl')
| -rw-r--r-- | lib/drl/executor.ml | 12 | ||||
| -rw-r--r-- | lib/drl/gate.ml | 79 | ||||
| -rw-r--r-- | lib/drl/sublanguage.ml | 9 |
3 files changed, 9 insertions, 91 deletions
diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml index 1172553..41bdde5 100644 --- a/lib/drl/executor.ml +++ b/lib/drl/executor.ml @@ -24,22 +24,22 @@ module Make (Storage : Management.Physical.S) = struct let common = List.filter_map (fun (n, _) -> - if List.exists (fun (m, _) -> m = n) filter.Relation.schema then + if List.exists (fun (m, _) -> m = n) filter#schema then Some n else None) - source.Relation.schema + source#schema in - let source_attrs = List.map fst source.Relation.schema in + let source_attrs = List.map fst source#schema in Result.bind (wrap (Alg.equijoin storage common source filter)) (fun joined -> wrap (Alg.project storage source_attrs joined)) - 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.Multigroup.multigroup) + (q : Ast.query) : (Relation.ephemeral, error) Result.t = let ( >>= ) = Result.bind in match q with | Ast.Base name -> ( - match Ops.get_relation db ~name with + match Ops.get_relation db name with | None -> Error (RelationNotFound name) | Some rel -> Ok rel) | Ast.Const pairs -> diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml deleted file mode 100644 index a314bce..0000000 --- a/lib/drl/gate.ml +++ /dev/null @@ -1,79 +0,0 @@ -(** 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. *) - -(* -- string -> char list impedance --------------------------------- *) - -let string_to_chars (s : string) : char list = - List.init (String.length s) (String.get s) - -(* -- 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.Const 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) - | Ast.Join (attrs, q1, 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) - | Ast.Project (attrs, 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) - -and value_of_ast_value : Ast.value -> Drl_verified.literal = function - | 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 - -(* -- 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 - -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 [] - -(* -- public interface ---------------------------------------------- *) - -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" diff --git a/lib/drl/sublanguage.ml b/lib/drl/sublanguage.ml index 29047c3..f47129f 100644 --- a/lib/drl/sublanguage.ml +++ b/lib/drl/sublanguage.ml @@ -15,12 +15,9 @@ module Make (Storage : Management.Physical.S) = struct | Error (Parser.ParseError s) -> Error (Exec.ParseError s) 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_types.Query rel) - | Error e -> Error e) + match Exec.execute storage db ast with + | Ok rel -> Ok (Sublanguage_types.Query (rel :> Relation.relation)) + | Error e -> Error e let sexp_of_error = Exec.sexp_of_error end |