X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=850c23ddd119fccd49301a521c4e15515e5aeb77;hb=31afc64440b7da53bb79e6f1524d47bf0fb56aaf;hp=f14e3d1269044d63e15eec3e931c8bc7ab9e1c1b;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index f14e3d126..850c23ddd 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -27,6 +27,58 @@ open Printf open MatitaTypes +(** given a uri and a type list (the contructors types) builds a list of pairs + * (name,uri) that is used to generate authomatic aliases **) +let extract_alias types uri = + fst(List.fold_left ( + fun (acc,i) (name, _, _, cl) -> + ((name, UriManager.string_of_uriref (uri,[i])) + :: + (fst(List.fold_left ( + fun (acc,j) (name,_) -> + (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) + ) (acc,1) cl))),i+1 + ) ([],0) types) + +(** adds a (name,uri) list l to a disambiguation environment e **) +let env_of_list l e = + let module DT = DisambiguateTypes in + let module DTE = DisambiguateTypes.Environment in + List.fold_left ( + fun e (name,uri) -> + DTE.add + (DT.Id name) + (uri,fun _ _ _ -> CicUtil.term_of_uri uri) + e + ) e l + +let add_aliases_for_object status suri = + let uri = UriManager.uri_of_string suri in + let name = UriManager.name_of_uri uri in + let new_env = env_of_list [(name,suri)] status.aliases in + {status with aliases = new_env } + +let add_aliases_for_inductive_def status types suri = + let uri = UriManager.uri_of_string suri in + (* aliases for the constructors and types *) + let aliases = env_of_list (extract_alias types uri) status.aliases in + (* aliases for the eliminations principles *) + let base = String.sub suri 0 (String.length suri - 4) in + let alisases = + env_of_list + (List.fold_left ( + fun acc suffix -> + if List.exists ( + fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix + ) status.objects then + let u = base ^ suffix in + (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc + else + acc + ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases + in + {status with aliases = aliases } + let paths_and_uris_of_obj uri status = let basedir = get_string_option status "basedir" in let innertypesuri = UriManager.innertypesuri_of_uri uri in @@ -103,9 +155,10 @@ let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = let obj = Cic.Constant (name, body, ty, params, attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd ~uri ~body ~ty; + MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in MatitaLog.message (sprintf "%s constant defined" suri); + let status = add_aliases_for_object status suri in { status with objects = new_stuff @ status.objects } end @@ -126,9 +179,10 @@ let add_inductive_def let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.put_inductive_definition uri (obj, ugraph); - MetadataDb.index_inductive_def ~dbd ~uri ~types:types; + MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in MatitaLog.message (sprintf "%s inductive type defined" suri); + let status = add_aliases_for_inductive_def status types suri in let status = { status with objects = new_stuff @ status.objects } in let elim sort status = try @@ -146,7 +200,43 @@ let add_inductive_def status [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; end - + +let add_record_def (suri, params, ty, fields) status = + let module CTC = CicTypeChecker in + let uri = UriManager.uri_of_string suri in + let buri = UriManager.buri_of_uri uri in + let record_spec = suri, params, ty, fields in + let types, leftno, obj, ugraph = CicRecord.inductive_of_record record_spec in + let status = add_inductive_def ~uri ~types ~leftno ~ugraph status in + let projections = CicRecord.projections_of record_spec in + let status = + List.fold_left ( + fun status (suri, name, t) -> + try + let ty, ugraph = + CTC.type_of_aux' [] [] t CicUniv.empty_ugraph + in + (* THIS MUST BE IN SYNC WITH CicRecord *) + let uri = UriManager.uri_of_string suri in + let t = Unshare.unshare t in + let ty = Unshare.unshare ty in + let status = add_constant ~uri ~body:t ~ty ~ugraph status in + add_aliases_for_object status suri + with + | CTC.TypeCheckerFailure s -> + MatitaLog.message + ("Unable to create projection " ^ name ^ " cause: " ^ s); + status + | Http_getter_types.Key_not_found s -> + let depend = UriManager.uri_of_string s in + let depend = UriManager.name_of_uri depend in + MatitaLog.message + ("Unable to create projection " ^ name ^ " cause uses " ^ depend); + status + ) status projections + in + status + module OrderedUri = struct type t = UriManager.uri * string @@ -170,21 +260,25 @@ let delta_status status1 status2 = in diff status1.objects status2.objects +let remove_coercion uri = + CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) + let time_travel ~present ~past = let list_of_objs_to_remove = List.rev (delta_status past present) in (* List.rev is just for the debugging code, which otherwise may list both * something.ind and something.ind#xpointer ... (ask Enrico :-) *) let debug_list = ref [] in - List.iter (fun (x,p) -> - remove_object_from_disk x p; + List.iter (fun (uri,p) -> + remove_object_from_disk uri p; + remove_coercion uri; (try - CicEnvironment.remove_obj x + CicEnvironment.remove_obj uri with CicEnvironment.Object_not_found _ -> MatitaLog.debug (sprintf "time_travel removes from cache %s that is not in" - (UriManager.string_of_uri x))); - let l = MatitaDb.remove_uri x in - debug_list := UriManager.string_of_uri x :: !debug_list @ l) + (UriManager.string_of_uri uri))); + let l = MatitaDb.remove_uri uri in + debug_list := UriManager.string_of_uri uri :: !debug_list @ l) list_of_objs_to_remove; (* this is debug code