in uris
| _ -> [uri]
;;
+
+let is_equational_fact ty =
+ let rec aux ctx t =
+ match CicReduction.whd ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ let s,u =
+ CicTypeChecker.type_of_aux' [] ctx src CicUniv.oblivion_ugraph
+ in
+ if fst (CicReduction.are_convertible ctx s (Cic.Sort Cic.Prop) u) then
+ false
+ else
+ aux (Some (name,Cic.Decl src)::ctx) tgt
+ | Cic.Appl [ Cic.MutInd (u,_,_) ; _; _; _] -> LibraryObjects.is_eq_URI u
+ | _ -> false
+ in
+ aux [] ty
+;;
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 add_to_universe (automation_cache,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
(fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
tkeys
in
- let universe = Universe.index_term_and_unfolded_term universe [] term ty
+ let is_equational = is_equational_fact ty in
+ let select_cmd =
+ if is_equational then
+ [ GrafiteAst.Select(HExtlib.dummy_floc,uri) ]
+ 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
+ else
+ automation_cache
in
+ let automation_cache =
+ { automation_cache with AutomationCache.univ = universe } in
let status = GrafiteTypes.add_moo_content index_cmd status in
- (universe,status)
+ let status = GrafiteTypes.add_moo_content select_cmd status in
+ (automation_cache,status)
in
let uris_to_index =
if is_a_variant obj then []
else (uris_for_inductive_type uri obj) @ lemmas
in
- let universe,status =
+ let automation_cache,status =
List.fold_left add_to_universe
- (status.GrafiteTypes.automation_cache.AutomationCache.univ,status)
+ (status.GrafiteTypes.automation_cache,status)
uris_to_index
in
- let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in
{status with
GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
- GrafiteTypes.automation_cache = cache },
+ GrafiteTypes.automation_cache = automation_cache},
lemmas
let add_coercion ~pack_coercion_obj ~add_composites status uri arity
proof_status = GrafiteTypes.No_proof;
objects = [];
coercions = CoercDb.empty_coerc_db;
- automation_cache = AutomationCache.empty;
+ automation_cache = AutomationCache.empty ();
baseuri = baseuri;
ng_status = GrafiteTypes.CommandMode lexicon_status;
}