X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=74e2cf2e26ed75042b6c13125448839b35b23a0b;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=f23b42ecc1c58e95ccc6afc309f4ffefaf355b3c;hpb=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index f23b42ecc..74e2cf2e2 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -27,24 +27,136 @@ open Printf -let add_obj refinement_toolkit ~basedir uri obj status = - let lemmas = LibrarySync.add_obj refinement_toolkit uri obj basedir in - {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects}, - lemmas +let is_a_variant obj = + match obj with + | Cic.Constant(_,_,_,_,attrs) -> + List.exists (fun x -> x = `Flavour `Variant) attrs + | _ -> false -let add_coercion refinement_toolkit ~basedir ~add_composites status uri = - let compounds = LibrarySync.add_coercion ~add_composites ~basedir refinement_toolkit uri 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 +let uris_for_inductive_type uri obj = + match obj with + | Cic.InductiveDefinition(types,_,_,_) -> + let suri = UriManager.string_of_uri uri in + let uris,_ = + List.fold_left + (fun (acc,i) (_,_,_,constructors)-> + let is = string_of_int i in + let newacc,_ = + List.fold_left + (fun (acc,j) _ -> + let js = string_of_int j in + UriManager.uri_of_string + (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1) + (acc,1) constructors + in + newacc,i+1) + ([],1) types + in uris + | _ -> [uri] +;; -module UriSet = Set.Make (OrderedUri) +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 (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 + 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 + 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 + 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 automation_cache,status = + List.fold_left add_to_universe + (status.GrafiteTypes.automation_cache,status) + uris_to_index + in + {status with + GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects; + GrafiteTypes.automation_cache = automation_cache}, + lemmas +let add_coercion ~pack_coercion_obj ~add_composites status uri arity + saturations baseuri += + 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; + } + in + let estatus = + NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status) + in + let status = GrafiteTypes.set_estatus estatus status in + status, lemmas + +let prefer_coercion s u = + CoercDb.prefer u; + { s with GrafiteTypes.coercions = CoercDb.dump () } + (** @return l2 \ l1 *) let uri_list_diff l2 l1 = let module S = UriManager.UriSet in @@ -56,19 +168,34 @@ let uri_list_diff l2 l1 = 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 + List.iter LibrarySync.remove_obj objs_to_remove; + CoercDb.restore past.GrafiteTypes.coercions; + NCicLibrary.time_travel (GrafiteTypes.get_estatus past) +;; -let init () = - LibrarySync.remove_all_coercions (); - LibraryObjects.reset_defaults (); - { +let initial_status lexicon_status baseuri = { GrafiteTypes.moo_content_rev = []; proof_status = GrafiteTypes.No_proof; - options = GrafiteTypes.no_options; objects = []; - coercions = []; - } + coercions = CoercDb.empty_coerc_db; + automation_cache = AutomationCache.empty (); + baseuri = baseuri; + ng_status = GrafiteTypes.CommandMode (new NEstatus.status) +} + + +let init baseuri = + CoercDb.restore CoercDb.empty_coerc_db; + LibraryObjects.reset_defaults (); + initial_status baseuri + ;; +let pop () = + LibrarySync.pop (); + LibraryObjects.pop () +;; + +let push () = + LibrarySync.push (); + LibraryObjects.push () +;; +