-let add_coercion ~basedir ~add_composites status uri =
- let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
- {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
- compounds
-
-module OrderedUri =
-struct
- type t = UriManager.uri * string
- let compare (u1, _) (u2, _) = UriManager.compare u1 u2
-end
+let uris_for_inductive_type uri obj =
+ match obj with
+ | Cic.InductiveDefinition(types,_,_,_) ->
+ let suri = UriManager.string_of_uri uri in
+ let uris,_ =
+ List.fold_left
+ (fun (acc,i) (_,_,_,constructors)->
+ let is = string_of_int i in
+ let newacc,_ =
+ List.fold_left
+ (fun (acc,j) _ ->
+ let js = string_of_int j in
+ UriManager.uri_of_string
+ (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1)
+ (acc,1) constructors
+ in
+ newacc,i+1)
+ ([],1) types
+ in uris
+ | _ -> [uri]
+;;
+
+let add_obj ~pack_coercion_obj uri obj status =
+ let lemmas = LibrarySync.add_obj ~pack_coercion_obj uri obj in
+ let add_to_universe (universe,status) uri =
+ let term = CicUtil.term_of_uri uri in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
+ let tkeys = Universe.keys [] ty in
+ let index_cmd =
+ List.map
+ (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
+ tkeys
+ in
+ let universe = Universe.index_term_and_unfolded_term universe [] term ty
+ in
+ let status = GrafiteTypes.add_moo_content index_cmd status in
+ (universe,status)
+ in
+ let uris_to_index =
+ if is_a_variant obj then []
+ else (uris_for_inductive_type uri obj) @ lemmas
+ in
+ let universe,status =
+ List.fold_left add_to_universe
+ (status.GrafiteTypes.universe,status)
+ uris_to_index
+ in
+ {status with
+ GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
+ GrafiteTypes.universe = universe},
+ lemmas