- (* needed by the retrieve_* functions, to know the arities of the
- * "functions" *)
-
- let ppelem = function
- | Constant uri -> UriManager.name_of_uri uri
- | Bound i -> string_of_int i
- | Variable -> "?"
- | Proposition -> "Prop"
- | Datatype -> "Type"
- | Dead -> "DEAD"
- ;;
- let pppath l = String.concat "::" (List.map ppelem l) ;;
- let elem_of_cic = function
- | Cic.Meta _ | Cic.Implicit _ -> Variable
- | Cic.Rel i -> Bound i
- | Cic.Sort (Cic.Prop) -> Proposition
- | Cic.Sort _ -> Datatype
- | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
- (try Constant (CicUtil.uri_of_term t)
- with Invalid_argument _ -> assert false)
- | Cic.Appl _ ->
- assert false (* should not happen *)
- | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _
- | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ ->
- HLog.debug "FIXME: the trie receives an invalid term";
- Dead
- (* assert false universe.ml removes these *)
- ;;
- let path_string_of_term arities =
- let set_arity arities k n =
- (assert (k<>Variable || n=0);
- if k = Dead then arities else (k,n)::(List.remove_assoc k arities))
- in
- let rec aux arities = function
- | Cic.Appl ((hd::tl) as l) ->
- let arities =
- set_arity arities (elem_of_cic hd) (List.length tl) in
- List.fold_left
- (fun (arities,path) t ->
- let arities,tpath = aux arities t in
- arities,path@tpath)
- (arities,[]) l
- | t -> arities, [elem_of_cic t]
- in
- aux arities
- ;;
- let compare_elem e1 e2 =
- match e1,e2 with
- | Constant u1,Constant u2 -> UriManager.compare u1 u2
- | e1,e2 -> Pervasives.compare e1 e2
- ;;
+let compare_elem e1 e2 =
+ match e1,e2 with
+ | Constant (u1,a1),Constant (u2,a2) ->
+ let x = UriManager.compare u1 u2 in
+ if x = 0 then Pervasives.compare a1 a2 else x
+ | e1,e2 -> Pervasives.compare e1 e2
+;;
+
+let string_of_path l = String.concat "." (List.map ppelem l) ;;
+
+module DiscriminationTreeIndexing =
+ functor (A:Set.S) ->
+ struct