diff options
Diffstat (limited to '')
| -rw-r--r-- | proof/drl_verified.ml | 411 |
1 files changed, 0 insertions, 411 deletions
diff --git a/proof/drl_verified.ml b/proof/drl_verified.ml deleted file mode 100644 index 137ad86..0000000 --- a/proof/drl_verified.ml +++ /dev/null @@ -1,411 +0,0 @@ -(** 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) |