path: root/proof/drl_verified.ml

(** val negb : bool -> bool **)

let negb = function
| true -> false
| false -> true

(** val fst : ('a1 * 'a2) -> 'a1 **)

let fst = function
| (x, _) -> x

(** val snd : ('a1 * 'a2) -> 'a2 **)

let snd = function
| (_, y) -> y

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

let rec app l m =
  match l with
  | [] -> m
  | a :: l1 -> a :: (app l1 m)

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
| [] -> []
| a :: l0 -> (f a) :: (map f l0)

(** val firstn : int -> 'a1 list -> 'a1 list **)

let rec firstn n l =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> [])
    (fun n0 -> match l with
               | [] -> []
               | a :: l0 -> a :: (firstn n0 l0))
    n

(** val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list **)

let rec flat_map f = function
| [] -> []
| x :: l0 -> app (f x) (flat_map f l0)

(** val existsb : ('a1 -> bool) -> 'a1 list -> bool **)

let rec existsb f = function
| [] -> false
| a :: l0 -> (||) (f a) (existsb f l0)

(** val forallb : ('a1 -> bool) -> 'a1 list -> bool **)

let rec forallb f = function
| [] -> true
| a :: l0 -> (&&) (f a) (forallb f l0)

(** val filter : ('a1 -> bool) -> 'a1 list -> 'a1 list **)

let rec filter f = function
| [] -> []
| x :: l0 -> if f x then x :: (filter f l0) else filter f l0

(** val find : ('a1 -> bool) -> 'a1 list -> 'a1 option **)

let rec find f = function
| [] -> None
| x :: tl -> if f x then Some x else find f tl

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

(** val append : char list -> char list -> char list **)

let rec append s1 s2 =
  match s1 with
  | [] -> s2
  | c::s1' -> c::(append s1' s2)

type attr_name = char list

type domain_name = char list

type schema = (attr_name * domain_name) list

(** val has_attr : attr_name -> schema -> bool **)

let has_attr a s =
  existsb (fun p -> eqb a (fst p)) s

(** val attr_names : schema -> attr_name list **)

let attr_names s =
  map fst s

(** val filter_schema : attr_name list -> schema -> schema **)

let filter_schema attrs s =
  filter (fun p -> existsb (eqb (fst p)) attrs) s

(** val merge_schema : schema -> schema -> schema **)

let merge_schema s1 s2 =
  app s1 (filter (fun p -> negb (has_attr (fst p) s1)) s2)

(** val remove_attrs : attr_name list -> schema -> schema **)

let remove_attrs attrs s =
  filter (fun p -> negb (existsb (eqb (fst p)) attrs)) s

(** val rename_in_schema :
    (attr_name * attr_name) list -> schema -> schema **)

let rename_in_schema renames s =
  map (fun p ->
    let a = fst p in
    let d = snd p in
    (match find (fun r -> eqb a (fst r)) renames with
     | Some p0 -> let (_, a') = p0 in (a', d)
     | None -> (a, d)))
    s

type value (* AXIOM TO BE REALIZED *)

(** val value_eqb : value -> value -> bool **)

let value_eqb =
  failwith "AXIOM TO BE REALIZED (Sakura.Relation.value_eqb)"

type tuple = (attr_name * value) list

(** val tuple_lookup : attr_name -> tuple -> value option **)

let rec tuple_lookup a = function
| [] -> None
| p :: rest ->
  let (a', v) = p in if eqb a a' then Some v else tuple_lookup a rest

(** val project_tuple : attr_name list -> tuple -> tuple **)

let project_tuple attrs t =
  filter (fun p -> existsb (eqb (fst p)) attrs) t

(** val rename_tuple : (attr_name * attr_name) list -> tuple -> tuple **)

let rename_tuple renames t =
  map (fun p ->
    let a = fst p in
    let v = snd p in
    (match find (fun r -> eqb a (fst r)) renames with
     | Some p0 -> let (_, a') = p0 in (a', v)
     | None -> (a, v)))
    t

(** val merge_tuples : tuple -> tuple -> tuple **)

let merge_tuples t1 t2 =
  app t1 (filter (fun p -> negb (existsb (eqb (fst p)) (map fst t1))) t2)

(** val tuples_agree_on : attr_name list -> tuple -> tuple -> bool **)

let tuples_agree_on attrs t1 t2 =
  forallb (fun a ->
    match tuple_lookup a t1 with
    | Some v1 ->
      (match tuple_lookup a t2 with
       | Some v2 -> value_eqb v1 v2
       | None -> false)
    | None -> (match tuple_lookup a t2 with
               | Some _ -> false
               | None -> true))
    attrs

type relation = { rel_name : char list; rel_schema : schema;
                  rel_tuples : tuple list }

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_schema : database -> query -> schema option **)

let rec predicted_schema db = function
| Base name ->
  (match db_lookup name db with
   | Some r -> Some r.rel_schema
   | None -> None)
| Const pairs ->
  Some
    (map (fun p -> ((fst p),
      ('a'::('b'::('s'::('t'::('r'::('a'::('c'::('t'::[])))))))))) pairs)
| Select (_, source) -> predicted_schema db source
| Join (attrs, q1, q2) ->
  (match predicted_schema db q1 with
   | Some s1 ->
     (match predicted_schema db q2 with
      | Some s2 ->
        Some
          (merge_schema s1
            (remove_attrs (attr_names s1) (remove_attrs attrs s2)))
      | None -> None)
   | None -> None)
| Cartesian (q1, q2) ->
  (match predicted_schema db q1 with
   | Some s1 ->
     (match predicted_schema db q2 with
      | Some s2 -> Some (merge_schema s1 s2)
      | None -> None)
   | None -> None)
| Project (attrs, q') ->
  (match predicted_schema db q' with
   | Some s -> Some (filter_schema attrs s)
   | None -> None)
| Rename (renames, q') ->
  (match predicted_schema db q' with
   | Some s -> Some (rename_in_schema renames s)
   | None -> None)
| Union (q1, _) -> predicted_schema db q1
| Diff (q1, _) -> predicted_schema db q1
| Take (_, q') -> predicted_schema db q'

(** val literal_to_value : literal -> value **)

let literal_to_value =
  failwith "AXIOM TO BE REALIZED (Sakura.Drl.literal_to_value)"

(** val eval_const : (attr_name * literal) list -> relation **)

let eval_const pairs =
  let tuple0 = map (fun p -> ((fst p), (literal_to_value (snd p)))) pairs in
  let sch =
    map (fun p -> ((fst p),
      ('a'::('b'::('s'::('t'::('r'::('a'::('c'::('t'::[])))))))))) pairs
  in
  { rel_name = ('c'::('o'::('n'::('s'::('t'::[]))))); rel_schema = sch;
  rel_tuples = (tuple0 :: []) }

(** val semijoin : relation -> relation -> relation **)

let semijoin filter_rel source =
  let common =
    filter (fun a -> has_attr a filter_rel.rel_schema)
      (attr_names source.rel_schema)
  in
  let matches = fun t ->
    existsb (fun ft -> tuples_agree_on common t ft) filter_rel.rel_tuples
  in
  { rel_name = source.rel_name; rel_schema = source.rel_schema; rel_tuples =
  (filter matches source.rel_tuples) }

(** val equijoin : attr_name list -> relation -> relation -> relation **)

let equijoin attrs left right =
  let joined =
    flat_map (fun lt ->
      flat_map (fun rt ->
        if tuples_agree_on attrs lt rt then (merge_tuples lt rt) :: [] else [])
        right.rel_tuples)
      left.rel_tuples
  in
  let new_schema =
    merge_schema left.rel_schema
      (remove_attrs (attr_names left.rel_schema)
        (remove_attrs attrs right.rel_schema))
  in
  { rel_name =
  (append ('j'::('o'::('i'::('n'::('_'::[])))))
    (append left.rel_name (append ('_'::[]) right.rel_name)));
  rel_schema = new_schema; rel_tuples = joined }

(** val cartesian : relation -> relation -> relation **)

let cartesian left right =
  let joined =
    flat_map (fun lt -> map (fun rt -> merge_tuples lt rt) right.rel_tuples)
      left.rel_tuples
  in
  { rel_name =
  (append ('c'::('a'::('r'::('t'::('_'::[])))))
    (append left.rel_name (append ('_'::[]) right.rel_name)));
  rel_schema = (merge_schema left.rel_schema right.rel_schema); rel_tuples =
  joined }

(** val project : attr_name list -> relation -> relation **)

let project attrs r =
  { rel_name = (append ('p'::('r'::('o'::('j'::('_'::[]))))) r.rel_name);
    rel_schema = (filter_schema attrs r.rel_schema); rel_tuples =
    (map (project_tuple attrs) r.rel_tuples) }

(** val rename : (attr_name * attr_name) list -> relation -> relation **)

let rename renames r =
  { rel_name =
    (append ('r'::('e'::('n'::('a'::('m'::('e'::('_'::[]))))))) r.rel_name);
    rel_schema = (rename_in_schema renames r.rel_schema); rel_tuples =
    (map (rename_tuple renames) r.rel_tuples) }

(** val rel_union : relation -> relation -> relation **)

let rel_union r1 r2 =
  { rel_name =
    (append ('u'::('n'::('i'::('o'::('n'::('_'::[]))))))
      (append r1.rel_name (append ('_'::[]) r2.rel_name)));
    rel_schema = r1.rel_schema; rel_tuples =
    (app r1.rel_tuples r2.rel_tuples) }

(** val rel_diff : relation -> relation -> relation **)

let rel_diff r1 r2 =
  let in_r2 = fun t ->
    existsb (fun t2 -> tuples_agree_on (attr_names r1.rel_schema) t t2)
      r2.rel_tuples
  in
  { rel_name =
  (append ('d'::('i'::('f'::('f'::('_'::[])))))
    (append r1.rel_name (append ('_'::[]) r2.rel_name)));
  rel_schema = r1.rel_schema; rel_tuples =
  (filter (fun t -> negb (in_r2 t)) r1.rel_tuples) }

(** val take : int -> relation -> relation **)

let take n r =
  { rel_name = (append ('t'::('a'::('k'::('e'::('_'::[]))))) r.rel_name);
    rel_schema = r.rel_schema; rel_tuples = (firstn n r.rel_tuples) }

(** val eval : database -> query -> relation option **)

let rec eval db = function
| Base name -> db_lookup name db
| Const pairs -> Some (eval_const pairs)
| Select (filter_q, source_q) ->
  (match eval db filter_q with
   | Some filter_rel ->
     (match eval db source_q with
      | Some source_rel -> Some (semijoin filter_rel source_rel)
      | None -> None)
   | None -> None)
| Join (attrs, q1, q2) ->
  (match eval db q1 with
   | Some r1 ->
     (match eval db q2 with
      | Some r2 -> Some (equijoin attrs r1 r2)
      | None -> None)
   | None -> None)
| Cartesian (q1, q2) ->
  (match eval db q1 with
   | Some r1 ->
     (match eval db q2 with
      | Some r2 -> Some (cartesian r1 r2)
      | None -> None)
   | None -> None)
| Project (attrs, q') ->
  (match eval db q' with
   | Some r -> Some (project attrs r)
   | None -> None)
| Rename (renames, q') ->
  (match eval db q' with
   | Some r -> Some (rename renames r)
   | None -> None)
| Union (q1, q2) ->
  (match eval db q1 with
   | Some r1 ->
     (match eval db q2 with
      | Some r2 -> Some (rel_union r1 r2)
      | None -> None)
   | None -> None)
| Diff (q1, q2) ->
  (match eval db q1 with
   | Some r1 ->
     (match eval db q2 with
      | Some r2 -> Some (rel_diff r1 r2)
      | None -> None)
   | None -> None)
| Take (n, q') ->
  (match eval db q' with
   | Some r -> Some (take n r)
   | None -> None)