module Index(B : Orderings.Blob) = struct
module U = FoUtils.Utils(B)
- module Unif = FoUnif.Founif(B)
- module Pp = Pp.Pp(B)
+ (*module Unif = FoUnif.Founif(B)*)
+ (*module Pp = Pp.Pp(B)*)
module ClauseOT =
struct
type t = Terms.direction * B.t Terms.unit_clause
let compare (d1,uc1) (d2,uc2) =
- let c = Pervasives.compare d1 d2 in
+ let c = Stdlib.compare d1 d2 in
if c <> 0 then c else U.compare_unit_clause uc1 uc2
;;
end
let path_string_of =
let rec aux arity = function
| Terms.Leaf a -> [Constant (a, arity)]
- | Terms.Var i -> (* assert (arity = 0); *) [Variable]
+ | Terms.Var _i -> (* assert (arity = 0); *) [Variable]
(* FIXME : should this be allowed or not ?
| Terms.Node (Terms.Var _::_) ->
assert false *)
| Terms.Node ([] | [ _ ] ) -> assert false
- | Terms.Node (Terms.Node _::_) -> assert false
+ (* FIXME : if we can have a variable we can also have a term
+ | Terms.Node (Terms.Node _::_) as t -> assert false *)
| Terms.Node (hd::tl) ->
aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
in
match e1,e2 with
| Constant (a1,ar1), Constant (a2,ar2) ->
let c = B.compare a1 a2 in
- if c <> 0 then c else Pervasives.compare ar1 ar2
+ if c <> 0 then c else Stdlib.compare ar1 ar2
| Variable, Variable -> 0
| Constant _, Variable -> ~-1
| Variable, Constant _ -> 1
op t l (Terms.Left2Right, c)
| (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
op t r (Terms.Right2Left, c)
- | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
+ | (_,Terms.Equation (l,r,_,Terms.Incomparable),_vl,_) as c ->
op (op t l (Terms.Left2Right, c))
r (Terms.Right2Left, c)
- | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
+ | (_,Terms.Equation (l,_r,_,Terms.Invertible),_vl,_) as c ->
op t l (Terms.Left2Right, c)
- | (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false
+ | (_,Terms.Equation (_,_r,_,Terms.Eq),_,_) -> assert false
| (_,Terms.Predicate p,_,_) as c ->
op t p (Terms.Nodir, c)
;;