]> matita.cs.unibo.it Git - helm.git/commitdiff
Revised discrimination tree implementation:
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 Sep 2008 08:11:53 +0000 (08:11 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 Sep 2008 08:11:53 +0000 (08:11 +0000)
- code size reduced, looking for unifiables or generalizations is
  almost the same and do not internally work with the query term,
  but its path representation that is now decorated with arieties to
  recover the tree structure when needed (jump to the sibling...)

- works with partial instantiation (no more global ariety list, but
  local to application heads). Stupid example:

  query: fold plus [] 0 = 0
  ==?==
  tree: fold ? [] 0 = 0

  since the 2nd arg is ? we skip the query subterm rooted in plus,
  but if plus is considered of ariety 2, we fail unifiing the following
  terms (we skip [] and 0 reaching the second 0 that is unified with
  [] and fails).

- term -> path string function fixed to clen up the input term, no more
  "FIXME: the trie received invalid term". Here there is room for improvements
  especially on beta redexes and terms beginning with an abstraction, but we
  need the substitutions operation, we should move the file elsewhere

- Big change:
  - if the query term is a meta, then the whole content of the tree is returned
  - in paramodulation this is dangerous, thus we added a small check in
    the paramodulation code (eq_indexing) instead of making the discrimination
    tree behave in a nasty way
  - the new implementation returns the same set of candidates on all test
    TPTP/Veloci and library/ (except for the aforementioned corner case).

helm/software/components/cic/discrimination_tree.ml
helm/software/components/cic/discrimination_tree.mli
helm/software/components/tactics/paramodulation/equality_indexing.ml
helm/software/components/tactics/paramodulation/equality_indexing.mli
helm/software/components/tactics/paramodulation/indexing.ml

index f5d61463024e3efe957406e6621cbb869de4816a..cb3a7d7456238086009a36d63670ca90fbab9371 100644 (file)
 
 (* $Id$ *)
 
-module DiscriminationTreeIndexing =  
-  functor (A:Set.S) -> 
-    struct
+type path_string_elem = 
+  | Constant of UriManager.uri * int (* name, arity *)
+  | Bound of int * int (* rel, arity *)
+  | Variable (* arity is 0 *)
+  | Proposition (* arity is 0 *) 
+  | Datatype (* arity is 0 *) 
+  | Dead (* arity is 0 *) 
+;;  
+      
+let arity_of = function
+  | Constant (_,a) 
+  | Bound (_,a) -> a
+  | _ -> 0 
+;;
 
-      type path_string_elem = 
-        | Constant of UriManager.uri 
-        | Bound of int | Variable | Proposition | Datatype | Dead;;
-      type path_string = path_string_elem list;;
+type path = path_string_elem list;;
+
+let ppelem = function
+  | Constant (uri,arity) -> 
+      "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")"
+  | Bound (i,arity) -> 
+      "("^string_of_int i ^ "," ^ string_of_int arity^")"
+  | Variable -> "?"
+  | Proposition -> "Prop"
+  | Datatype -> "Type"
+  | Dead -> "Dead"
+;;
 
+let path_string_of_term_with_jl =
+  let rec aux arity = function
+    | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable]
+    | Cic.Appl (Cic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
+    | Cic.Appl [] -> assert false
+    | Cic.Appl (hd::tl) ->
+        aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
+    | Cic.Cast (t,_) -> aux arity t
+    | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable]
+        (* I think we should CicSubstitution.subst Implicit t *)
+    | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *)
+    | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable]
+    | Cic.Rel i -> [Bound (i, arity)]
+    | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition]
+    | Cic.Sort _ -> assert (arity=0); [Datatype]
+    | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
+        [Constant (CicUtil.uri_of_term t, arity)]
+    | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead]
+  in 
+    aux 0
+;;
 
-      (* needed by the retrieve_* functions, to know the arities of the
-       * "functions" *)
-      
-      let ppelem = function
-        | Constant uri -> UriManager.name_of_uri uri
-        | Bound i -> string_of_int i
-        | Variable -> "?"
-        | Proposition -> "Prop"
-        | Datatype -> "Type"
-        | Dead -> "DEAD"
-      ;;
-      let pppath l = String.concat "::" (List.map ppelem l) ;;
-      let elem_of_cic = function
-        | Cic.Meta _ | Cic.Implicit _ -> Variable
-        | Cic.Rel i -> Bound i
-        | Cic.Sort (Cic.Prop) -> Proposition
-        | Cic.Sort _ -> Datatype
-        | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
-            (try Constant (CicUtil.uri_of_term t)
-            with Invalid_argument _ -> assert false)
-        | Cic.Appl _ -> 
-            assert false (* should not happen *)
-        | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _
-        | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> 
-            HLog.debug "FIXME: the trie receives an invalid term";
-            Dead
-            (* assert false universe.ml removes these *)
-      ;;
-      let path_string_of_term arities =
-       let set_arity arities k n = 
-         (assert (k<>Variable || n=0);
-          if k = Dead then arities else (k,n)::(List.remove_assoc k arities))
-        in
-        let rec aux arities = function
-          | Cic.Appl ((hd::tl) as l) ->
-              let arities = 
-               set_arity arities (elem_of_cic hd) (List.length tl) in
-             List.fold_left 
-               (fun (arities,path) t -> 
-                  let arities,tpath = aux arities t in
-                    arities,path@tpath)
-               (arities,[]) l
-          | t -> arities, [elem_of_cic t]
-        in 
-          aux arities
-      ;;
-      let compare_elem e1 e2 =
-        match e1,e2 with
-        | Constant u1,Constant u2 -> UriManager.compare u1 u2
-        | e1,e2 -> Pervasives.compare e1 e2
-      ;;
+let compare_elem e1 e2 =
+  match e1,e2 with
+  | Constant (u1,a1),Constant (u2,a2) -> 
+       let x = UriManager.compare u1 u2 in
+       if x = 0 then Pervasives.compare a1 a2 else x
+  | e1,e2 -> Pervasives.compare e1 e2
+;;
+
+let string_of_path l = String.concat "." (List.map ppelem l) ;;
+
+module DiscriminationTreeIndexing =  
+  functor (A:Set.S) -> 
+    struct
 
       module OrderedPathStringElement = struct
         type t = path_string_elem
@@ -98,212 +100,89 @@ module DiscriminationTreeIndexing =
 
       module DiscriminationTree = Trie.Make(PSMap);;
 
-      type t = A.t DiscriminationTree.t * (path_string_elem*int) list
-      let empty = DiscriminationTree.empty, [] ;;
+      type t = A.t DiscriminationTree.t
 
-      let iter (dt, _ ) f =
-        DiscriminationTree.iter (fun _ x -> f x) dt
-      ;;
+      let empty = DiscriminationTree.empty;;
+
+      let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
 
-      let index (tree,arity) term info =
-        let arity,ps = path_string_of_term arity term in
+      let index tree term info =
+        let ps = path_string_of_term_with_jl term in
         let ps_set =
-          try DiscriminationTree.find ps tree 
-          with Not_found -> A.empty in
-        let tree = DiscriminationTree.add ps (A.add info ps_set) tree in
-        tree,arity
+          try DiscriminationTree.find ps tree with Not_found -> A.empty 
+        in
+        DiscriminationTree.add ps (A.add info ps_set) tree
       ;;
 
-      let remove_index (tree,arity) term info =
-        let arity,ps = path_string_of_term arity term in
+      let remove_index tree term info =
+        let ps = path_string_of_term_with_jl term in
         try
           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
-          if A.is_empty ps_set then
-            DiscriminationTree.remove ps tree,arity
-          else
-            DiscriminationTree.add ps ps_set tree,arity
-        with Not_found ->
-          tree,arity
+          if A.is_empty ps_set then DiscriminationTree.remove ps tree
+          else DiscriminationTree.add ps ps_set tree
+        with Not_found -> tree
       ;;
 
-      let in_index (tree,arity) term test =
-        let arity,ps = path_string_of_term arity term in
+      let in_index tree term test =
+        let ps = path_string_of_term_with_jl term in
         try
           let ps_set = DiscriminationTree.find ps tree in
           A.exists test ps_set
-        with Not_found ->
-          false
-      ;;
-
-      let head_of_term = function
-        | Cic.Appl (hd::tl) -> hd
-        | term -> term
-      ;;
-
-      let rec skip_prods = function
-        | Cic.Prod (_,_,t) -> skip_prods t
-        | 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 Failure _ -> raise Not_found)
-                | _ -> raise Not_found
+        with Not_found -> false
       ;;
 
-
-      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
-            ignore(subterm_at_pos pos' term ); 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
+      (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is 
+         (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
+         skip all its progeny, thus you want to reach t.
+      
+         You need to skip as many elements as the sum of all arieties contained
+          in the progeny of f.
+      
+         The input ariety is the one of f while the path is x.g....t  
+         Should be the equivalent of after_t in the literature (handbook A.R.)
+       *)
+      let rec skip arity path =
+        if arity = 0 then path else match path with 
+        | [] -> assert false 
+        | m::tl -> skip (arity-1+arity_of m) tl
       ;;
 
-
-      let next_t pos term =
-        let t = subterm_at_pos pos term in
-          try
-            let _ = subterm_at_pos [1] t in
-              pos @ [1]
-          with Not_found ->
-            match pos with
-              | [] -> [1]
-              | pos -> after_t pos term
-      ;;     
-
-      let retrieve_generalizations (tree,arity) term =
-        let term = skip_prods term in
-        let rec retrieve tree term pos =
-          match tree with
-            | DiscriminationTree.Node (Some s, _) when pos = [] -> s
-            | DiscriminationTree.Node (_, map) ->
-                let res =
-                  let hd_term = 
-                    elem_of_cic (head_of_term (subterm_at_pos pos term)) 
-                  in
-                  if hd_term = Variable then A.empty else 
-                  try
-                    let n = PSMap.find hd_term map in
-                      match n with
-                        | DiscriminationTree.Node (Some s, _) -> s
-                        | DiscriminationTree.Node (None, _) ->
-                            let newpos = 
-                              try next_t pos term 
-                              with Not_found -> [] 
-                            in
-                              retrieve n term newpos
-                  with Not_found ->
-                    A.empty
-                in
-                  try
-                    let n = PSMap.find Variable map in
-                    let newpos = try after_t pos term with Not_found -> [-1] in
-                      if newpos = [-1] then
-                        match n with
-                          | DiscriminationTree.Node (Some s, _) -> A.union s res
-                          | _ -> res
-                      else
-                        A.union res (retrieve n term newpos)
-                  with Not_found ->
-                    res
+      (* the equivalent of skip, but on the index, thus the list of trees
+         that are rooted just after the term represented by the tree root
+         are returned (we are skipping the root) *)
+      let skip_root = function DiscriminationTree.Node (value, map) ->
+        let rec get n = function DiscriminationTree.Node (v, m) as tree ->
+           if n = 0 then [tree] else 
+           PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
         in
-          retrieve tree term []
+          PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
       ;;
 
-
-      let jump_list arities = 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 List.assoc k arities 
-                             with Not_found -> 0 
-                           in
-                             (get (n-1 + a) v) @ res) m []
-            in
-              PSMap.fold
-                (fun k v res ->
-                   let arity = 
-                    try 
-                      List.assoc k arities 
-                    with Not_found -> 0 in
-                     (get arity v) @ res)
-                map []
+      let retrieve unif tree term =
+        let path = path_string_of_term_with_jl term in
+        let rec retrieve path tree =
+          match tree, path with
+          | DiscriminationTree.Node (Some s, _), [] -> s
+          | DiscriminationTree.Node (None, _), [] -> A.empty 
+          | DiscriminationTree.Node (_, map), Variable::path when unif ->
+              List.fold_left A.union A.empty
+                (List.map (retrieve path) (skip_root tree))
+          | DiscriminationTree.Node (_, map), node::path ->
+              A.union
+                 (if not unif && node = Variable then A.empty else
+                  try retrieve path (PSMap.find node map)
+                  with Not_found -> A.empty)
+                 (try
+                    match PSMap.find Variable map,skip (arity_of node) path with
+                    | DiscriminationTree.Node (Some s, _), [] -> s
+                    | n, path -> retrieve path n
+                  with Not_found -> A.empty)
+       in
+        retrieve path tree
       ;;
 
-
-      let retrieve_unifiables (tree,arities) term =
-        let term = skip_prods term in
-        let rec retrieve tree term pos =
-          match tree with
-            | DiscriminationTree.Node (Some s, _) when pos = [] -> s
-            | DiscriminationTree.Node (_, map) ->
-                let subterm =
-                  try Some (subterm_at_pos pos term) with Not_found -> None
-                in
-                match subterm with
-                | None -> A.empty
-                | Some (Cic.Meta _) ->
-                      let newpos = try next_t pos term with Not_found -> [] in
-                      let jl = jump_list arities tree in
-                        List.fold_left
-                          (fun r s -> A.union r s)
-                          A.empty
-                          (List.map (fun t -> retrieve t term newpos) jl)
-                  | Some subterm ->
-                      let res = 
-                        let hd_term = elem_of_cic (head_of_term subterm) in
-                          if hd_term = Variable then
-                          A.empty else
-                        try
-                          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 ->
-                          A.empty
-                      in
-                        try
-                          let n = PSMap.find Variable map in
-                          let newpos = 
-                            try after_t pos term 
-                            with Not_found -> [-1] 
-                          in
-                            if newpos = [-1] then
-                              match n with
-                                | DiscriminationTree.Node (Some s, _) -> 
-                                    A.union s res
-                                | _ -> res
-                            else
-                              A.union res (retrieve n term newpos)
-                        with Not_found ->
-                          res
-      in
-        retrieve tree term []
+      let retrieve_generalizations tree term = retrieve false tree term;;
+      let retrieve_unifiables tree term = retrieve true tree term;;
   end
 ;;
 
index 94c51ec576ee4b1184da5889d8d926683ad90866..1b3ab8be5a90a73b8af4b11441c6a223a5d1ed47 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+type path
+
+val string_of_path : path -> string
+
 module DiscriminationTreeIndexing :
   functor (A : Set.S) ->
     sig
 
       type t 
-      val iter : t -> (A.t -> unit) -> unit
+      val iter : t -> (path -> A.t -> unit) -> unit
 
       val empty : t
       val index : t -> Cic.term -> A.elt -> t
index 01fecc0ed27f746100e019e962a1078fe835e9cb..f24ff1de1197ecee004540e70918768583012a6f 100644 (file)
@@ -36,7 +36,7 @@ module type EqualityIndex =
     val remove_index : t -> Equality.equality -> t
     val index : t -> Equality.equality -> t
     val in_index : t -> Equality.equality -> bool
-    val iter : t -> (PosEqSet.t -> unit) -> unit
+    val iter : t -> (Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
   end
 
 module DT = 
index 9fd06f3ff96e1a3f89bec485470c995f0d9a4932..31b5e26d1896930360e0f50b8b20e597f48c98c3 100644 (file)
@@ -34,7 +34,7 @@ module type EqualityIndex =
     val remove_index : t -> Equality.equality -> t
     val index : t -> Equality.equality -> t
     val in_index : t -> Equality.equality -> bool
-    val iter : t -> (PosEqSet.t -> unit) -> unit
+    val iter : t -> (Discrimination_tree.path -> PosEqSet.t -> unit) -> unit
   end
 
 module DT : EqualityIndex
index 89bb0462b893e266c6b9d969a103af8ca1c10c8e..9c471d3b351c6056144b32da87f5a4004745d63c 100644 (file)
@@ -441,7 +441,7 @@ let subsumption_aux_all use_unification env table target =
   in
   let leftr =
     match left with
-    | Cic.Meta _ when not use_unification -> []   
+    | Cic.Meta _ (*when not use_unification*) -> []   
     | _ ->
         let leftc = get_candidates predicate table left in
         find_all_matches ~unif_fun
@@ -449,7 +449,7 @@ let subsumption_aux_all use_unification env table target =
   in
   let rightr =
         match right with
-          | Cic.Meta _ when not use_unification -> [] 
+          | Cic.Meta _ (*when not use_unification*) -> [] 
           | _ ->
               let rightc = get_candidates predicate table right in
                 find_all_matches ~unif_fun