module TermOT : Set.OrderedType with type t = NCic.term = struct
type t = NCic.term
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module TermSet = Set.Make(TermOT)
module TermListOT : Set.OrderedType with type t = NCic.term list =
struct
type t = NCic.term list
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module TermListSet : Set.S with type elt = NCic.term list =
let path_string_of t =
let rec aux arity depth = function
| NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
+ | NCic.Appl (NCic.Match _::_) -> [Dead]
| NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
| NCic.Appl [] -> assert false
| NCic.Appl l when depth > 10 || List.length l > 50 -> [Variable]
| NCic.Appl (hd::tl) ->
aux (List.length tl) depth hd @
List.flatten (List.map (aux 0 (depth+1)) tl)
- | NCic.Lambda _ | NCic.Prod _ -> [Variable]
+ | NCic.Lambda _ -> [Variable]
(* I think we should CicSubstitution.subst Implicit t *)
| NCic.LetIn _ -> [Variable] (* z-reduce? *)
| NCic.Meta _ | NCic.Implicit _ -> assert (arity = 0); [Variable]
| NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
| NCic.Sort _ -> assert (arity=0); [Datatype]
| NCic.Const (u) -> [Constant (u, arity)]
- | NCic.Match _ -> [Dead]
+ (* Prod is used for coercions to funclass, ?->? *)
+ (* so it should not be unifiable with any other term *)
+ | NCic.Match _ | NCic.Prod _ -> [Dead]
in
aux 0 0 t
;;
match e1,e2 with
| Constant (u1,a1),Constant (u2,a2) ->
let x = NReference.compare u1 u2 in
- if x = 0 then Pervasives.compare a1 a2 else x
- | e1,e2 -> Pervasives.compare e1 e2
+ if x = 0 then Stdlib.compare a1 a2 else x
+ | e1,e2 -> Stdlib.compare e1 e2
;;
let string_of_path l = String.concat "." (List.map ppelem l) ;;