Source file Query_engine.ml

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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
open Base

module type S = sig
  val run_query : Query.dbix Query.expr -> Addr_set.t
end

module Make (Graphs : Forester_graphs.S) : S =
struct
  module Q = Query

  let query_rel mode pol rel addr =
    let fn =
      match pol with
      | Q.Incoming -> Addr_graph.safe_pred
      | Q.Outgoing -> Addr_graph.safe_succ
    in
    let gph = Graphs.get mode rel in
    Addr_set.of_list @@ fn gph addr

  let check_rel mode pol rel addr addr' =
    let gph = Graphs.get mode rel in
    match pol with
    | Q.Incoming -> Addr_graph.mem_edge gph addr' addr
    | Q.Outgoing -> Addr_graph.mem_edge gph addr addr'

  let rec check_query ~env (q : Query.dbix Query.expr) addr =
    match q with
    | Rel (mode, pol, rel, addr_val') ->
      let addr' = eval_addr ~env addr_val' in
      check_rel mode pol rel addr' addr
    | Isect qs -> check_isect ~env qs addr
    | Union qs -> check_union ~env qs addr
    | Complement q ->
      not @@ check_query ~env q addr
    | Union_fam (q, scope) ->
      let xs = Addr_set.to_list @@ run_query ~env q in
      xs |> List.exists @@ fun x ->
      check_query ~env:(x :: env) scope.body addr
    | Isect_fam (q, scope) ->
      let xs = Addr_set.to_list @@ run_query ~env q in
      xs |> List.exists @@ fun x ->
      check_query ~env:(x :: env) scope.body addr

  and eval_addr ~env : Q.dbix Q.addr_expr -> _ =
    function
    | Query.Addr addr -> addr
    | Query.Var ix ->
      begin
        match List.nth_opt env ix with
        | Some addr -> addr
        | None -> Reporter.fatalf Type_error "Bound variable not found in environment when evaluating query"
      end

  and check_isect ~env qs addr =
    qs |> List.for_all @@ fun q ->
    check_query ~env q addr

  and check_isect' qs addr =
    qs |> List.for_all @@ fun (env, q) ->
    check_query ~env q addr

  and check_union ~env qs addr =
    qs |> List.exists @@ fun q ->
    check_query ~env q addr

  and run_query ~env (q : Query.dbix Query.expr) : Addr_set.t =
    match q with
    | Rel (mode, pol, rel, addr_val) ->
      let addr = eval_addr ~env addr_val in
      query_rel mode pol rel addr
    | Isect qs -> run_isect ~env qs
    | Union qs -> run_union ~env qs
    | Complement q ->
      Addr_set.diff (Graphs.get_all_addrs ()) @@ run_query ~env q
    | Union_fam (q, scope) ->
      let xs = Addr_set.to_list @@ run_query ~env q in
      let qs =
        xs |> List.map @@ fun x ->
        x :: env, scope.body
      in
      run_union' qs
    | Isect_fam (q, scope) ->
      let xs = Addr_set.to_list @@ run_query ~env q in
      let qs =
        xs |> List.map @@ fun x ->
        x :: env, scope.body
      in
      run_isect' qs

  and run_isect ~env qs = run_isect' @@ List.map (fun q -> env, q) qs

  and run_union ~env qs = run_union' @@ List.map (fun q -> env, q) qs

  and run_union' qs =
    let alg (env, q) = Addr_set.union (run_query ~env q) in
    List.fold_right alg qs Addr_set.empty

  and run_isect' =
    function
    | [] -> Graphs.get_all_addrs ()
    | (env, q) :: qs ->
      run_query ~env q |> Addr_set.filter @@ check_isect' qs

  let run_query = run_query ~env:[]
end