- let arities = Hashtbl.create 11;;
-
- let shared_implicit = [Cic.Implicit None]
-
- let rec path_string_of_term = function
- | Cic.Meta _ -> shared_implicit
- | Cic.Appl ((hd::tl) as l) ->
- if not (Hashtbl.mem arities hd) then
- Hashtbl.add arities hd (List.length tl);
- List.concat (List.map path_string_of_term l)
- | term -> [term]
+ let ppelem = function
+ | Function -> "Fun"
+ | Constant uri -> UriManager.name_of_uri uri
+ | Bound i -> string_of_int i
+ | Variable -> "?"
+ | Proposition -> "Prop"
+ | Datatype -> "Type"
+ ;;
+ let pppath l = String.concat "::" (List.map ppelem l) ;;
+ let elem_of_cic = function
+ | Cic.Meta _ -> Variable
+ | Cic.Lambda _ -> Function
+ | Cic.Rel i -> Bound i
+ | Cic.Sort (Cic.Prop) -> Proposition
+ | Cic.Sort _ -> Datatype
+ | term ->
+ try Constant (CicUtil.uri_of_term term)
+ with Invalid_argument _ -> Variable (* HACK! *)
+ ;;
+ let path_string_of_term arities =
+ let set_arity n = function
+ | Variable -> Hashtbl.replace arities Variable 0
+ | e -> Hashtbl.replace arities e n
+ in
+ let rec aux = function
+ | Cic.Appl ((hd::tl) as l) ->
+(*
+ if Hashtbl.mem arities (elem_of_cic hd) then
+ begin
+ let n = Hashtbl.find arities (elem_of_cic hd) in
+ if n <> List.length tl then
+ begin
+ prerr_endline
+ (String.concat " "
+ (List.map (fun x -> ppelem (elem_of_cic x)) l))
+ end;
+ assert(n = List.length tl)
+ end;
+*)
+ set_arity (List.length tl) (elem_of_cic hd);
+(* Hashtbl.replace arities (elem_of_cic hd) (List.length tl); *)
+ List.concat (List.map aux l)
+ | t -> [elem_of_cic t]
+ in
+ aux
+ ;;
+ let compare_elem e1 e2 =
+ match e1,e2 with
+ | Constant u1,Constant u2 -> UriManager.compare u1 u2
+ | e1,e2 -> Pervasives.compare e1 e2