From e3d3e20dfea253de291d5b31059cd55c0eaabf02 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Mon, 11 May 2026 23:10:27 -0300 Subject: Multigroup unified reference for hierarchical access --- lib/drl_verified/drl_verified.ml | 67 --------------------------------------- lib/drl_verified/drl_verified.mli | 23 -------------- 2 files changed, 90 deletions(-) delete mode 100644 lib/drl_verified/drl_verified.ml delete mode 100644 lib/drl_verified/drl_verified.mli (limited to 'lib/drl_verified') diff --git a/lib/drl_verified/drl_verified.ml b/lib/drl_verified/drl_verified.ml deleted file mode 100644 index 868af2a..0000000 --- a/lib/drl_verified/drl_verified.ml +++ /dev/null @@ -1,67 +0,0 @@ -(** 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) - -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 - -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 - -(** 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) - | 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) - | 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) - | None -> None) - | None -> None) - | Diff (q1, _) -> predicted_finite db q1 - | _ -> Some true diff --git a/lib/drl_verified/drl_verified.mli b/lib/drl_verified/drl_verified.mli deleted file mode 100644 index dac930e..0000000 --- a/lib/drl_verified/drl_verified.mli +++ /dev/null @@ -1,23 +0,0 @@ -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 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 -- cgit v1.2.3