end
module MetadataSet = Set.Make (OrderedMetadata)
-module StringSet = Set.Make (String)
+module UriManagerSet = UriManager.UriSet
module S = MetadataSet
(fun set term -> aux (next_pos pos) set term)
set tl
| Cic.Const (uri, subst) ->
- let set = S.add (`Obj (string_of_uri uri, pos)) set in
+ let set = S.add (`Obj (uri, pos)) set in
List.fold_left
(fun set (_, term) -> aux (next_pos pos) set term)
set subst
| Cic.MutInd (uri, typeno, subst) ->
- let uri = UriManager.string_of_uriref (uri, [typeno]) in
+ let uri = UriManager.uri_of_uriref uri typeno None in
let set = S.add (`Obj (uri, pos)) set in
List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
set subst
| Cic.MutConstruct (uri, typeno, consno, subst) ->
- let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
+ let uri = UriManager.uri_of_uriref uri typeno (Some consno) in
let set = S.add (`Obj (uri, pos)) set in
List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
set subst
let compute_type pos uri typeno (name, _, ty, constructors) =
let consno = ref 0 in
let type_metadata =
- (UriManager.string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
+ (UriManager.uri_of_uriref uri typeno None, name, (compute_term pos ty))
in
let constructors_metadata =
List.map
(fun (name, term) ->
incr consno;
- let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
+ let uri = UriManager.uri_of_uriref uri typeno (Some !consno) in
(uri, name, (compute_term pos term)))
constructors
in
S.fold
(fun metadata uris ->
match metadata with
- | `Obj (uri, _) -> StringSet.add uri uris
+ | `Obj (uri, _) -> UriManagerSet.add uri uris
| _ -> uris)
- type_metadata StringSet.empty
+ type_metadata UriManagerSet.empty
in
S.union
(S.filter
(function
- | `Obj (uri, _) when StringSet.mem uri uris -> false
+ | `Obj (uri, _) when UriManagerSet.mem uri uris -> false
| _ -> true)
body_metadata)
type_metadata
S.empty
params
in
- [ UriManager.string_of_uri uri,
+ [ uri,
UriManager.name_of_uri uri,
S.union metadata var_metadata ]
| Cic.InductiveDefinition (types, params, _, _) ->