(* $Id$ *)
-type path_string_elem =
- | Constant of NUri.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
-;;
+open Discrimination_tree
+
+module TermOT : Set.OrderedType with type t = NCic.term = struct
+ type t = NCic.term
+ let compare = Pervasives.compare
+end
+
+module TermSet = Set.Make(TermOT)
-type path = path_string_elem list;;
+module NCicIndexable : Indexable
+with type input = NCic.term and type constant_name = NUri.uri = struct
+
+type input = NCic.term
+type constant_name = NUri.uri
let ppelem = function
| Constant (uri,arity) ->
| Dead -> "Dead"
;;
-let path_string_of_term_with_jl =
+let path_string_of =
let rec aux arity = function
| NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
| NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
aux 0
;;
-let compare_elem e1 e2 =
+let compare e1 e2 =
match e1,e2 with
| Constant (u1,a1),Constant (u2,a2) ->
let x = NUri.compare u1 u2 in
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
- let compare = compare_elem
- end
-
- module PSMap = Map.Make(OrderedPathStringElement);;
-
- type key = PSMap.key
-
- module DiscriminationTree = Trie.Make(PSMap);;
-
- type t = A.t DiscriminationTree.t
-
- let empty = DiscriminationTree.empty;;
-
- let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
-
- 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
- DiscriminationTree.add ps (A.add info ps_set) tree
- ;;
-
- 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
- else DiscriminationTree.add ps ps_set tree
- with Not_found -> tree
- ;;
-
- 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
- ;;
-
- (* 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
- ;;
-
- (* 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 (_, map) ->
- let rec get n = function DiscriminationTree.Node (_, 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
- PSMap.fold (fun k v res -> (get (arity_of k) 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 _, 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_generalizations tree term = retrieve false tree term;;
- let retrieve_unifiables tree term = retrieve true tree term;;
- end
-;;
+end
+module DiscriminationTree = Make(NCicIndexable)(TermSet)
projects / helm.git / blobdiff