path: root/lib/drl_verified/drl_verified.ml

(** 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