1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 type path_string_elem =
29 | Constant of UriManager.uri * int (* name, arity *)
30 | Bound of int * int (* rel, arity *)
31 | Variable (* arity is 0 *)
32 | Proposition (* arity is 0 *)
33 | Datatype (* arity is 0 *)
34 | Dead (* arity is 0 *)
37 let arity_of = function
43 type path = path_string_elem list;;
46 | Constant (uri,arity) ->
47 "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")"
49 "("^string_of_int i ^ "," ^ string_of_int arity^")"
51 | Proposition -> "Prop"
56 let path_string_of_term_with_jl =
57 let rec aux arity = function
58 | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable]
59 | Cic.Appl (Cic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
60 | Cic.Appl [] -> assert false
61 | Cic.Appl (hd::tl) ->
62 aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
63 | Cic.Cast (t,_) -> aux arity t
64 | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable]
65 (* I think we should CicSubstitution.subst Implicit t *)
66 | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *)
67 | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable]
68 | Cic.Rel i -> [Bound (i, arity)]
69 | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition]
70 | Cic.Sort _ -> assert (arity=0); [Datatype]
71 | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
72 [Constant (CicUtil.uri_of_term t, arity)]
73 | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead]
78 let compare_elem e1 e2 =
80 | Constant (u1,a1),Constant (u2,a2) ->
81 let x = UriManager.compare u1 u2 in
82 if x = 0 then Pervasives.compare a1 a2 else x
83 | e1,e2 -> Pervasives.compare e1 e2
86 let string_of_path l = String.concat "." (List.map ppelem l) ;;
88 module DiscriminationTreeIndexing =
92 module OrderedPathStringElement = struct
93 type t = path_string_elem
94 let compare = compare_elem
97 module PSMap = Map.Make(OrderedPathStringElement);;
101 module DiscriminationTree = Trie.Make(PSMap);;
103 type t = A.t DiscriminationTree.t
105 let empty = DiscriminationTree.empty;;
107 let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
109 let index tree term info =
110 let ps = path_string_of_term_with_jl term in
112 try DiscriminationTree.find ps tree with Not_found -> A.empty
114 DiscriminationTree.add ps (A.add info ps_set) tree
117 let remove_index tree term info =
118 let ps = path_string_of_term_with_jl term in
120 let ps_set = A.remove info (DiscriminationTree.find ps tree) in
121 if A.is_empty ps_set then DiscriminationTree.remove ps tree
122 else DiscriminationTree.add ps ps_set tree
123 with Not_found -> tree
126 let in_index tree term test =
127 let ps = path_string_of_term_with_jl term in
129 let ps_set = DiscriminationTree.find ps tree in
131 with Not_found -> false
134 (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
135 (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
136 skip all its progeny, thus you want to reach t.
138 You need to skip as many elements as the sum of all arieties contained
141 The input ariety is the one of f while the path is x.g....t
142 Should be the equivalent of after_t in the literature (handbook A.R.)
144 let rec skip arity path =
145 if arity = 0 then path else match path with
147 | m::tl -> skip (arity-1+arity_of m) tl
150 (* the equivalent of skip, but on the index, thus the list of trees
151 that are rooted just after the term represented by the tree root
152 are returned (we are skipping the root) *)
153 let skip_root = function DiscriminationTree.Node (value, map) ->
154 let rec get n = function DiscriminationTree.Node (v, m) as tree ->
155 if n = 0 then [tree] else
156 PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
158 PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
161 let retrieve unif tree term =
162 let path = path_string_of_term_with_jl term in
163 let rec retrieve path tree =
164 match tree, path with
165 | DiscriminationTree.Node (Some s, _), [] -> s
166 | DiscriminationTree.Node (None, _), [] -> A.empty
167 | DiscriminationTree.Node (_, map), Variable::path when unif ->
168 List.fold_left A.union A.empty
169 (List.map (retrieve path) (skip_root tree))
170 | DiscriminationTree.Node (_, map), node::path ->
172 (if not unif && node = Variable then A.empty else
173 try retrieve path (PSMap.find node map)
174 with Not_found -> A.empty)
176 match PSMap.find Variable map,skip (arity_of node) path with
177 | DiscriminationTree.Node (Some s, _), [] -> s
178 | n, path -> retrieve path n
179 with Not_found -> A.empty)
184 let retrieve_generalizations tree term = retrieve false tree term;;
185 let retrieve_unifiables tree term = retrieve true tree term;;