X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=47744f66e0332e962b2feace6b5f42cb0399a8df;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=d318d11a73cb504b788dd98aa45cf18d66f635ba;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index d318d11a7..47744f66e 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -53,69 +53,107 @@ let uris_for_inductive_type uri obj = ([],1) types 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 refinement_toolkit uri obj status = - let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in - let add_to_universe (universe,status) 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 (automation_cache,status) uri = let term = CicUtil.term_of_uri uri in - let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in -(* prop filtering - let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in - prerr_endline (CicPp.ppterm term); - prerr_endline (CicPp.ppterm sort); - let tkeys = - if sort = Cic.Sort(Cic.Prop) then Universe.keys [] ty - else [] - 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 = + if is_equational then + [ GrafiteAst.Select(HExtlib.dummy_floc,uri) ] + else + [] in -(* prop filtering - let universe = - if sort = Cic.Sort(Cic.Prop) then - Universe.index_term_and_unfolded_term universe [] term ty - else universe -*) - let universe = Universe.index_term_and_unfolded_term universe [] term ty + 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 + else (uris_for_inductive_type uri obj) @ lemmas in - let universe,status = + let automation_cache,status = List.fold_left add_to_universe - (status.GrafiteTypes.universe,status) + (status#automation_cache,status) uris_to_index in - {status with - GrafiteTypes.objects = uri::status.GrafiteTypes.objects; - GrafiteTypes.universe = universe}, - lemmas + (status + #set_objects (uri :: lemmas @ status#objects)) + #set_automation_cache automation_cache, + lemmas -let add_coercion refinement_toolkit ~add_composites status uri arity +let add_coercion ~pack_coercion_obj ~add_composites status uri arity saturations baseuri = - let compounds = - LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity - saturations baseuri 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 - -module UriSet = Set.Make (OrderedUri) + let lemmas = + LibrarySync.add_coercion ~add_composites ~pack_coercion_obj + uri arity saturations baseuri in + let status = + (status + #set_coercions (CoercDb.dump ())) ; + #set_objects (lemmas @ status#objects) + in + let status = NCicCoercion.index_old_db (CoercDb.dump ()) status in + status, lemmas +let prefer_coercion status u = + CoercDb.prefer u; + status#set_coercions (CoercDb.dump ()) + (** @return l2 \ l1 *) let uri_list_diff l2 l1 = let module S = UriManager.UriSet in @@ -124,30 +162,22 @@ let uri_list_diff l2 l1 = let diff = S.diff s2 s1 in S.fold (fun uri uris -> uri :: uris) diff [] -let time_travel ~present ~past = - let objs_to_remove = - uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in - let coercions_to_remove = - uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions - in - List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove; - List.iter LibrarySync.remove_obj objs_to_remove - -let initial_status baseuri = { - GrafiteTypes.moo_content_rev = []; - proof_status = GrafiteTypes.No_proof; -(* options = GrafiteTypes.no_options; *) - objects = []; - coercions = []; - universe = Universe.empty; - baseuri = baseuri; - } +let initial_status lexicon_status baseuri = + (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus +;; +let time_travel ~present ?(past=initial_status present present#baseuri) () = + let objs_to_remove = + uri_list_diff present#objects past#objects in + List.iter LibrarySync.remove_obj objs_to_remove; + CoercDb.restore past#coercions; + NCicLibrary.time_travel past +;; -let init baseuri = - LibrarySync.remove_all_coercions (); +let init lexicon_status = + CoercDb.restore CoercDb.empty_coerc_db; LibraryObjects.reset_defaults (); - initial_status baseuri + initial_status lexicon_status ;; let pop () = LibrarySync.pop ();