aliases:DisambiguateTypes.environment ->
universe:DisambiguateTypes.multiple_environment option ->
'a -> 'b)
- ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+ ~(drop_aliases: 'b -> 'b)
+ ~(drop_aliases_and_clear_diff: 'b -> 'b)
(thing: 'a)
=
assert (universe <> None);
in
let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
if use_mono_aliases && not instances then
- res
+ drop_aliases res
else if user_asked then
- res (* one shot aliases *)
+ drop_aliases res (* one shot aliases *)
else
- set_aliases aliases res
+ drop_aliases_and_clear_diff res
in
let rec aux =
function
CoercDb.use_coercions := saved_use_coercions;
raise exn
+type disambiguator_thing =
+ { do_it :
+ 'a 'b.
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ f:(?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b * bool) ->
+ drop_aliases:('b * bool -> 'b * bool) ->
+ drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }
+
let disambiguate_thing =
let profiler = CicUtil.profile "disambiguate_thing" in
- fun ~aliases ~universe
- ~(f:?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
- 'a -> 'b)
- ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
- (thing: 'a)
- -> profiler.CicUtil.profile
- (disambiguate_thing ~aliases ~universe ~f ~set_aliases) thing
-
-let disambiguate_thing ~aliases ~universe
- ~(f:?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
- 'a -> 'b)
- ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
- (thing: 'a)
-=
- Obj.magic disambiguate_thing ~aliases ~universe ~f ~set_aliases thing
+ { do_it =
+ fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+ -> profiler.CicUtil.profile
+ (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff) thing
+ }
+
+let drop_aliases (choices, user_asked) =
+ (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
+ user_asked
-let set_aliases aliases (choices, user_asked) =
- (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
+let drop_aliases_and_clear_diff (choices, user_asked) =
+ (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
user_asked
let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
let f =
Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
in
- disambiguate_thing ~aliases ~universe ~f ~set_aliases term
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff term
let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
assert (fresh_instances = None);
let f = Disambiguator.disambiguate_obj ~dbd ~uri in
- disambiguate_thing ~aliases ~universe ~f ~set_aliases obj
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff obj
let disambiguate_term status_ref term =
let status = !status_ref in
- let (aliases, metasenv, cic, _) =
+ let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases)
~metasenv:(MatitaMisc.get_proof_metasenv status) term)
in
let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status_ref := status;
cic
let disambiguate_lazy_term status_ref term =
(fun context metasenv ugraph ->
let status = !status_ref in
- let (aliases, metasenv, cic, ugraph) =
+ let (diff, metasenv, cic, ugraph) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~initial_ugraph:ugraph ~aliases:status.aliases
~universe:(Some status.multi_aliases) ~context ~metasenv term)
in
let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status_ref := status;
cic, metasenv, ugraph)
Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
- let (aliases, metasenv, cic, _) =
+ let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
| Intermediate _ -> assert false
in
let status = { status with proof_status = proof_status } in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status, cic
let disambiguate_command status = function