From: Alberto Griggio <griggio@fbk.eu>
Date: Mon, 20 Jun 2005 18:01:42 +0000 (+0000)
Subject: discrimination trees
X-Git-Tag: INDEXING_NO_PROOFS~111
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=101ecc0bc98f6f979d08200ae562ce89bffc0670;p=helm.git

discrimination trees
---

diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml
new file mode 100644
index 000000000..8753782d4
--- /dev/null
+++ b/helm/ocaml/paramodulation/discrimination_tree.ml
@@ -0,0 +1,238 @@
+type path_string_elem = Cic.term;;
+type path_string = path_string_elem list;;
+
+
+(* needed by the retrieve_* functions, to know the arities of the "functions" *)
+let arities = Hashtbl.create 11;;
+
+
+let rec path_string_of_term = function
+  | Cic.Meta _ -> [Cic.Implicit None]
+  | Cic.Appl ((hd::tl) as l) ->
+      if not (Hashtbl.mem arities hd) then
+        Hashtbl.add arities hd (List.length tl);
+      List.concat (List.map path_string_of_term l)
+  | term -> [term]
+;;
+
+
+module OrderedPathStringElement = struct
+  type t = path_string_elem
+
+  let compare = Pervasives.compare
+end
+
+module PSMap = Map.Make(OrderedPathStringElement);;
+
+
+module DiscriminationTree = struct
+  type key = path_string
+  type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t)
+
+  let empty = Node (None, PSMap.empty)
+
+  let rec find l t =
+    match (l, t) with
+    | [], Node (None, _) -> raise Not_found
+    | [], Node (Some v, _) -> v
+    | x::r, Node (_, m) -> find r (PSMap.find x m)
+        
+  let rec mem l t =
+    match (l, t) with
+    | [], Node (None, _) -> false
+    | [], Node (Some _, _) -> true
+    | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
+
+  let add l v t =
+    let rec ins = function
+      | [], Node (_, m) -> Node (Some v, m)
+      | x::r, Node (v, m) ->
+	  let t' = try PSMap.find x m with Not_found -> empty in
+	  let t'' = ins (r, t') in
+	  Node (v, PSMap.add x t'' m)
+    in
+    ins (l, t)
+
+  let rec remove l t =
+    match (l, t) with
+    | [], Node (_, m) -> Node (None, m)
+    | x::r, Node (v, m) -> 
+	try
+	  let t' = remove r (PSMap.find x m) in
+	  Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
+	with Not_found ->
+	  t
+
+  let rec fold f t acc =
+    let rec traverse revp t acc = match t with
+      | Node (None, m) -> 
+	  PSMap.fold (fun x -> traverse (x::revp)) m acc
+      | Node (Some v, m) -> 
+	  f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
+    in
+    traverse [] t acc
+
+end
+
+
+let index tree equality =
+  let _, (_, l, r, ordering), _, _ = equality in
+  let psl = path_string_of_term l
+  and psr = path_string_of_term r in
+  match ordering with
+  | Utils.Gt -> DiscriminationTree.add psl (Utils.Left, equality) tree
+  | Utils.Lt -> DiscriminationTree.add psr (Utils.Right, equality) tree
+  | _ ->
+      let tree = DiscriminationTree.add psl (Utils.Left, equality) tree in
+      DiscriminationTree.add psr (Utils.Right, equality) tree
+;;
+
+
+let remove_index tree equality =
+  let _, (_, l, r, ordering), _, _ = equality in
+  let psl = path_string_of_term l
+  and psr = path_string_of_term r in
+  match ordering with
+  | Utils.Gt -> DiscriminationTree.remove psl tree
+  | Utils.Lt -> DiscriminationTree.remove psr tree
+  | _ ->
+      let tree = DiscriminationTree.remove psl tree in
+      DiscriminationTree.remove psr tree
+;;
+
+
+let in_index tree equality =
+  let _, (_, l, r, ordering), _, _ = equality in
+  let psl = path_string_of_term l
+  and psr = path_string_of_term r in
+  let meta_convertibility = Inference.meta_convertibility_eq equality in
+  let ok ps =
+    try let _, eq = DiscriminationTree.find ps tree in meta_convertibility eq
+    with Not_found -> false
+  in
+  (ok psl) || (ok psr)
+;;
+
+
+let head_of_term = function
+  | Cic.Appl (hd::tl) -> hd
+  | term -> term
+;;
+
+
+let rec subterm_at_pos pos term =
+  match pos with
+  | [] -> term
+  | index::pos ->
+      match term with
+      | Cic.Appl l ->
+          (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found)
+      | _ -> raise Not_found
+;;
+
+
+let next_t pos term =
+  let t = subterm_at_pos pos term in
+  try
+    let t2 = subterm_at_pos [1] t in
+    pos @ [1]
+  with Not_found ->
+    match pos with
+    | [] -> [1]
+    | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
+;;
+
+
+let rec after_t pos term =
+  let pos' =
+    match pos with
+    | [] -> raise Not_found
+    | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
+  in
+  try
+    let t = subterm_at_pos pos' term in pos'
+  with Not_found ->
+    let pos, _ =
+      List.fold_right
+        (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false)
+    in
+    after_t pos term
+;;
+
+
+let retrieve_generalizations tree term =
+  let rec retrieve tree term pos = 
+    match tree with
+    | DiscriminationTree.Node (value, map) ->
+        let res =
+          try
+            let hd_term = head_of_term (subterm_at_pos pos term) in
+            let n = PSMap.find hd_term map in
+            match n with
+            | DiscriminationTree.Node (Some s, _) -> [s]
+            | DiscriminationTree.Node (None, _) ->
+                retrieve n term (next_t pos term)
+          with Not_found ->
+            []
+        in
+        try
+          let n = PSMap.find (Cic.Implicit None) map in
+          res @ (retrieve n term (after_t pos term))
+        with Not_found ->
+          res
+  in
+  retrieve tree term []
+;;
+
+
+let jump_list = function
+  | DiscriminationTree.Node (value, map) ->
+      let rec get n tree =
+        match tree with
+        | DiscriminationTree.Node (v, m) ->
+            if n = 0 then
+              [tree]
+            else
+              PSMap.fold
+                (fun k v res ->
+                   let a = try Hashtbl.find arities k with Not_found -> 0 in
+                   (get (n-1 + a) v) @ res) m []
+      in
+      PSMap.fold
+        (fun k v res ->
+           let arity = try Hashtbl.find arities k with Not_found -> 0 in
+           (get arity v) @ res)
+        map []
+;;
+
+
+let retrieve_unifiables tree term =
+  let rec retrieve tree term pos =
+    match tree with
+    | DiscriminationTree.Node (value, map) ->
+        let res = 
+          try
+            match subterm_at_pos pos term with
+            | Cic.Meta _ ->
+                List.concat
+                  (List.map
+                     (fun t -> retrieve t term (next_t pos term))
+                     (jump_list tree))
+            | subterm ->
+                let hd_term = head_of_term subterm in
+                let n = PSMap.find hd_term map in
+                match n with
+                | DiscriminationTree.Node (Some s, _) -> [s]
+                | DiscriminationTree.Node (None, _) ->
+                    retrieve n term (next_t pos term)
+          with Not_found ->
+            []
+        in
+        try
+          let n = PSMap.find (Cic.Implicit None) map in
+          res @ (retrieve n term (after_t pos term))
+        with Not_found ->
+          res
+  in
+  retrieve tree term []
+;;