module TermSet = Set.Make(TermOT)
module NCicIndexable : Indexable
-with type input = NCic.term and type constant_name = NUri.uri = struct
+with type input = NCic.term
+and type constant_name = NReference.reference = struct
type input = NCic.term
-type constant_name = NUri.uri
+type constant_name = NReference.reference
let ppelem = function
- | Constant (uri,arity) ->
- "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
+ | Constant (ref,arity) ->
+ "("^NReference.string_of_reference ref ^ "," ^ string_of_int arity^")"
| Bound (i,arity) ->
"("^string_of_int i ^ "," ^ string_of_int arity^")"
| Variable -> "?"
| Dead -> "Dead"
;;
-let path_string_of =
- let rec aux arity = function
+let path_string_of t =
+ let rec aux arity depth = function
| NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
| 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) hd @ List.flatten (List.map (aux 0) tl)
+ aux (List.length tl) depth hd @
+ List.flatten (List.map (aux 0 (depth+1)) tl)
| NCic.Lambda _ | NCic.Prod _ -> [Variable]
(* I think we should CicSubstitution.subst Implicit t *)
| NCic.LetIn _ -> [Variable] (* z-reduce? *)
| NCic.Rel i -> [Bound (i, arity)]
| NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
| NCic.Sort _ -> assert (arity=0); [Datatype]
- | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
+ | NCic.Const (u) -> [Constant (u, arity)]
| NCic.Match _ -> [Dead]
in
- aux 0
+ aux 0 0 t
;;
let compare e1 e2 =
match e1,e2 with
| Constant (u1,a1),Constant (u2,a2) ->
- let x = NUri.compare u1 u2 in
+ let x = NReference.compare u1 u2 in
if x = 0 then Pervasives.compare a1 a2 else x
| e1,e2 -> Pervasives.compare e1 e2
;;