Source file Index.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127

(* This file is free software, part of Logtk. See file "license" for more details. *)

(** {1 Generic term indexing} *)

type term = Term.t
type subst = Subst.t

module T = Term

(** {2 Leaf} *)

(** A leaf maps terms to a set of elements *)

module type LEAF = Index_intf.LEAF

module MakeLeaf(X : Set.OrderedType) : LEAF with type elt = X.t = struct
  module S = Set.Make(X)

  type t = S.t T.Map.t

  type elt = X.t

  let empty = T.Map.empty

  let find_ leaf t =
    try T.Map.find t leaf with Not_found -> S.empty

  let add leaf t data =
    let set = find_ leaf t in
    let set = S.add data set in
    T.Map.add t set leaf

  let remove_if leaf t set_filter =
    try
      let set = T.Map.find t leaf in
      let set = set_filter set in
      if S.is_empty set
      then T.Map.remove t leaf
      else T.Map.add t set leaf
    with Not_found ->
      leaf

  let remove leaf t data =
    remove_if leaf t (fun set -> S.remove data set)

  let update_leaf leaf t data_filter =
    remove_if leaf t (fun set -> S.filter data_filter set)

  let is_empty = T.Map.is_empty

  let iter leaf f =
    T.Map.iter (fun t set -> S.iter (fun elt -> f t elt) set) leaf

  let fold leaf acc f =
    T.Map.fold (fun t set acc -> S.fold (fun elt acc -> f acc t elt) set acc) leaf acc

  let size leaf =
    T.Map.fold (fun _ set acc -> S.cardinal set + acc) leaf 0

  let fold_unify (leaf,sc_l) t k =
    T.Map.iter
      (fun t' set ->
         try
           let subst = Unif.FO.unify_full (t',sc_l) t in
           S.iter (fun data -> k (t', data, subst)) set
         with Unif.Fail -> ())
      leaf

  let fold_unify_complete ~unif_alg (leaf,sc_l) t k =
    T.Map.iter
      (fun t' set ->
         let substs = unif_alg (t',sc_l) t in
         S.iter (fun data -> k (t', data, substs)) set)
      leaf

  let fold_match ?(subst=Subst.empty) (leaf,sc_l) t k =
    T.Map.iter
      (fun t' set ->
         try
           let subst = Unif.FO.matching ~subst ~pattern:(t',sc_l) t in
           S.iter
             (fun data -> k (t', data, subst))
             set
         with Unif.Fail -> ())
      leaf

  let fold_matched ?(subst=Subst.empty) (leaf,sc_l) t k =
    T.Map.iter
      (fun t' set ->
         try
           let subst = Unif.FO.matching ~subst ~pattern:t (t',sc_l) in
           S.iter
             (fun data -> k (t', data, subst))
             set
         with Unif.Fail -> ())
      leaf
end

(** {2 Term index} *)

module type TERM_IDX = Index_intf.TERM_IDX

(** {2 Subsumption Index} *)

module type CLAUSE = Index_intf.CLAUSE

(** A subsumption index (non perfect!) *)

module type SUBSUMPTION_IDX = Index_intf.SUBSUMPTION_IDX

(** {2 Specialized rewriting index} *)

module type EQUATION = Index_intf.EQUATION

module type UNIT_IDX = Index_intf.UNIT_IDX

module BasicEquation = struct
  type t = T.t * T.t
  type rhs = T.t
  let compare (l1,r1)(l2,r2) =
    let c = T.compare l1 l2 in
    if c <> 0 then c else T.compare r1 r2
  let extract (l,r) = l,r,true
  let priority _ = 1
end