2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 module type Comparable =
17 val is_eq : t -> t -> bool
20 module C : Comparable =
23 let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
27 module C : Comparable =
30 let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
34 open Discrimination_tree
36 module ClauseOT : Set.OrderedType
37 with type t = Terms.direction * C.t Terms.unit_clause =
39 type t = Terms.direction * C.t Terms.unit_clause
40 let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) =
41 Pervasives.compare (d1,id1) (d2,id2)
44 module ClauseSet = Set.Make(ClauseOT)
46 module FotermIndexable : Indexable
47 with type input = C.t Terms.foterm and
48 type constant_name = C.t = struct
50 type input = C.t Terms.foterm
51 type constant_name = C.t
54 let rec aux arity = function
55 | Terms.Leaf a -> [Constant (a, arity)]
56 | Terms.Var i -> assert (arity = 0); [Variable]
57 | Terms.Node (Terms.Var _::_) -> assert false
58 | Terms.Node ([] | [ _ ] ) -> assert false
59 | Terms.Node (Terms.Node _::_) -> assert false
60 | Terms.Node (hd::tl) ->
61 aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
68 | Constant (a1,ar1), Constant (a2,ar2) ->
69 if C.is_eq a1 a2 then Pervasives.compare ar1 ar2
70 else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *)
71 | _ -> Pervasives.compare e1 e2
74 let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
78 module DiscriminationTree = Make(FotermIndexable)(ClauseSet)