blob: 868af2ad022fe2436df1308135be0f4b2a88b2f9 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
(** 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
|
