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
+ let universe = automation_cache.AutomationCache.univ in
+ let universe, index_cmd =
+ List.fold_left
+ (fun (universe,acc) key ->
+ let cands = Universe.get_candidates universe key in
+ let tys =
+ List.map
+ (fun t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph
+ in
+ ty)
+ cands
+ in
+ if List.for_all
+ (fun cty ->
+ not (fst(CicReduction.are_convertible [] ty cty
+ CicUniv.oblivion_ugraph))) tys
+ then
+ Universe.index universe key term,
+ GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)::acc
+ else
+ universe, acc)
+ (universe,[]) tkeys
in
let is_equational = is_equational_fact ty in
let select_cmd =
else
[]
in
- let universe = automation_cache.AutomationCache.univ in
- let universe = Universe.index_term_and_unfolded_term universe [] term ty in
let automation_cache =
if is_equational then
AutomationCache.add_term_to_active automation_cache [] [] [] term None
let lemmas =
LibrarySync.add_coercion ~add_composites ~pack_coercion_obj
uri arity saturations baseuri in
+ let status =
{ status with GrafiteTypes.coercions = CoercDb.dump () ;
- objects = lemmas @ status.GrafiteTypes.objects
- },
- lemmas
+ objects = lemmas @ status.GrafiteTypes.objects;
+ }
+ in
+ let db =
+ NCicCoercion.index_old_db (CoercDb.dump ())
+ (GrafiteTypes.get_coercions status)
+ in
+ let status = GrafiteTypes.set_coercions db status in
+ status, lemmas
let prefer_coercion s u =
CoercDb.prefer u;
uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
List.iter LibrarySync.remove_obj objs_to_remove;
CoercDb.restore past.GrafiteTypes.coercions;
+ NCicLibrary.time_travel (GrafiteTypes.get_library_db past)
;;
let initial_status lexicon_status baseuri = {
coercions = CoercDb.empty_coerc_db;
automation_cache = AutomationCache.empty ();
baseuri = baseuri;
- ng_status = GrafiteTypes.CommandMode lexicon_status;
+ ng_status = GrafiteTypes.CommandMode {
+ NEstatus.lstatus = lexicon_status;
+ NEstatus.rstatus = {
+ NRstatus.uhint_db = NCicUnifHint.empty_db;
+ NRstatus.coerc_db = NCicCoercion.empty_db;
+ NRstatus.library_db = NCicLibrary.time0;
+ NRstatus.dump = fun x -> x;
+ };
}
+}
let init baseuri =