let alias_diff ~from status =
let module Map = DisambiguateTypes.Environment in
Map.fold
- (fun domain_item codomain_item acc ->
- if not (Map.mem domain_item from.aliases) then
- Map.add domain_item codomain_item acc
- else
- begin
- try
- let description1 = fst(Map.find domain_item from.aliases) in
- let description2 = fst(Map.find domain_item status.aliases) in
- if description1 <> description2 then
- Map.add domain_item codomain_item acc
- else
- acc
- with Not_found -> acc
- end)
+ (fun domain_item (description1,_ as codomain_item) acc ->
+ try
+ let description2,_ = Map.find domain_item from.aliases in
+ if description1 <> description2 then
+ Map.add domain_item codomain_item acc
+ else
+ acc
+ with
+ Not_found ->
+ Map.add domain_item codomain_item acc)
status.aliases Map.empty
+let alias_diff =
+ let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status
+
let set_proof_aliases status aliases =
- let new_status = {status with aliases = aliases } in
+ let new_status = { status with aliases = aliases } in
let diff = alias_diff ~from:status new_status in
- let textual_diff =
- if DisambiguateTypes.Environment.is_empty diff then
- ""
- else
- DisambiguatePp.pp_environment diff ^ "\n" in
- let moo_content_rev = textual_diff :: status.moo_content_rev in
- {new_status with moo_content_rev = moo_content_rev}
+ let multi_aliases =
+ DisambiguateTypes.Environment.fold DisambiguateTypes.Environment.cons
+ diff status.multi_aliases in
+ let new_status = { new_status with multi_aliases = multi_aliases } in
+ if DisambiguateTypes.Environment.is_empty diff then
+ new_status
+ else
+ add_moo_content (DisambiguatePp.commands_of_environment diff) new_status
(** given a uri and a type list (the contructors types) builds a list of pairs
* (name,uri) that is used to generate authomatic aliases **)
[bodyuri, xmlbodypath]
| _-> assert false)
+let typecheck_obj =
+ let profiler = CicUtil.profile "add_obj.typecheck_obj" in
+ fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj
+
let add_obj uri obj status =
let dbd = MatitaDb.instance () in
let suri = UriManager.string_of_uri uri in
if CicEnvironment.in_library uri then
command_error (sprintf "%s already defined" suri)
else begin
- CicTypeChecker.typecheck_obj uri obj; (* 1 *)
+ typecheck_obj uri obj; (* 1 *)
try
MetadataDb.index_obj ~dbd ~uri; (* 2 must be in the env *)
try
CicEnvironment.remove_obj uri; (* -1 *)
raise exc
end
+
+let add_obj =
+ let profiler = CicUtil.profile "add_obj" in
+ fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status
module OrderedUri =
struct