X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=23e3b048f45bd015a184d2b6273b9cd257c1406e;hb=63722506a5e378f3e05b46612cb91c132d994082;hp=850c23ddd119fccd49301a521c4e15515e5aeb77;hpb=2dde94202f728a388eabd91018d71c0bce0708cb;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 850c23ddd..23e3b048f 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -27,57 +27,60 @@ open Printf open MatitaTypes +let alias_diff ~from status = + let module Map = DisambiguateTypes.Environment in + Map.fold + (fun domain_item codomain_item acc -> + if not (Map.mem domain_item from.aliases) then + Map.add domain_item codomain_item acc + else + acc) + status.aliases Map.empty + +let set_proof_aliases status aliases = + let new_status = {status with aliases = aliases } in + let diff = alias_diff ~from:status new_status in + let moo_content_rev = + CicTextualParser2.EnvironmentP3.to_string diff :: + status.moo_content_rev in + {new_status with moo_content_rev = moo_content_rev} + (** 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])) + (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None)) :: (fst(List.fold_left ( fun (acc,j) (name,_) -> - (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) - ) (acc,1) cl))),i+1 + (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i + (Some 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 env_of_list l env = + let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in + DisambiguateTypes.env_of_list l' 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 } + set_proof_aliases status aliases + +let add_alias_for_constant 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 + set_proof_aliases status new_env + +let add_aliases_for_object status suri = + function + Cic.InductiveDefinition (types,_,_,_) -> + add_aliases_for_inductive_def status types suri + | Cic.Constant _ -> add_alias_for_constant status suri + | Cic.Variable _ + | Cic.CurrentProof _ -> assert false let paths_and_uris_of_obj uri status = let basedir = get_string_option status "basedir" in @@ -120,12 +123,9 @@ let save_object_to_disk status uri obj = (List.map Filename.dirname [innertypespath; xmlpath]); (* now write to disk *) ensure_path_exists innertypespath; - Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ; + Xml.pp ~gzip:true xmlinnertypes (Some innertypespath); ensure_path_exists xmlpath; Xml.pp ~gzip:true xml (Some xmlpath) ; - (* now register to the getter *) - Http_getter.register' innertypesuri (path_scheme_of innertypespath); - Http_getter.register' uri (path_scheme_of xmlpath); (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: (innertypesuri,innertypespath) :: (* now the optional body, both write and register *) @@ -133,109 +133,24 @@ let save_object_to_disk status uri obj = None,None -> [] | Some bodyxml,Some bodyuri-> ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ; - Http_getter.register' bodyuri (path_scheme_of xmlbodypath); - [bodyuri,xmlbodypath] + Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + [bodyuri, xmlbodypath] | _-> assert false) -let unregister_if_some = function - | Some u -> Http_getter.unregister' u | None -> () - -let remove_object_from_disk uri path = - Sys.remove path; - Http_getter.unregister' uri - -let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = +let add_obj uri obj status = let dbd = MatitaDb.instance () in let suri = UriManager.string_of_uri uri in if CicEnvironment.in_library uri then - command_error (sprintf "%s constant already defined" suri) + command_error (sprintf "%s already defined" suri) else begin - let name = UriManager.name_of_uri uri in - 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); + CicTypeChecker.typecheck_obj uri obj; 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 } + MatitaLog.message (sprintf "%s defined" suri); + let status = add_aliases_for_object status suri obj in + { status with objects = new_stuff @ status.objects; + proof_status = No_proof } end - -let split_obj = function - | Cic.Constant (name, body, ty, _, attrs) - | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) - | _ -> assert false - -let add_inductive_def - ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status -= - let dbd = MatitaDb.instance () in - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - command_error (sprintf "%s inductive type already defined" suri) - else begin - let name = UriManager.name_of_uri uri in - 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_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 - let obj = CicElim.elim_of ~sort uri 0 in - let (name, body, ty, attrs) = split_obj obj in - let suri = MatitaMisc.qualify status name ^ ".con" in - let uri = UriManager.uri_of_string suri in - (* TODO Zack: make CicElim returns a universe *) - let ugraph = CicUniv.empty_ugraph in - add_constant ~uri ?body ~ty ~attrs ~ugraph status; - with CicElim.Can_t_eliminate -> status - in - List.fold_left - (fun status sort -> elim sort status) - 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 @@ -269,7 +184,7 @@ let time_travel ~present ~past = * something.ind and something.ind#xpointer ... (ask Enrico :-) *) let debug_list = ref [] in List.iter (fun (uri,p) -> - remove_object_from_disk uri p; + MatitaMisc.safe_remove p; remove_coercion uri; (try CicEnvironment.remove_obj uri @@ -307,13 +222,25 @@ let time_travel ~present ~past = MatitaLog.debug "l2:"; List.iter MatitaLog.debug l2 -let alias_diff ~from status = - let module Map = DisambiguateTypes.Environment in - Map.fold - (fun domain_item codomain_item acc -> - if not (Map.mem domain_item from.aliases) then - Map.add domain_item codomain_item acc - else - acc) - status.aliases Map.empty +let remove uri = + let derived_uris_of_uri uri = + UriManager.innertypesuri_of_uri uri :: + (match UriManager.bodyuri_of_uri uri with + | None -> [] + | Some u -> [u]) + in + let to_remove = + uri :: + (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @ + derived_uris_of_uri uri + in + List.iter + (fun uri -> + (try + MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); + MatitaMisc.safe_remove (Http_getter.resolve' uri) + with Http_getter_types.Key_not_found _ -> ()); + remove_coercion uri; + ignore (MatitaDb.remove_uri uri)) + to_remove