From: Enrico Tassi Date: Fri, 18 Nov 2005 17:22:50 +0000 (+0000) Subject: fixed coercions undo X-Git-Tag: V_0_7_2_3~35 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59977ba4636f09f6b2c22c6af9adc5257f2d8a46;p=helm.git fixed coercions undo --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 1d3b1f94e..503d4a06a 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -614,8 +614,11 @@ let eval_coercion status coercion = let new_coercions = CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in let status = - List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status) + List.fold_left (fun s (uri,o,_) -> + let status = MatitaSync.add_obj uri o status in + {status with coercions = uri :: status.coercions}) status new_coercions in + let status = {status with coercions = coer_uri :: status.coercions} in let statement_of name = GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, (CicNotationPt.Ident (name, None))) @@ -1015,6 +1018,7 @@ let initial_status = proof_status = No_proof; options = default_options (); objects = []; + coercions = []; notation_ids = []; } diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index cbf305261..716aa04d2 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -229,13 +229,20 @@ module UriSet = Set.Make (OrderedUri) module IdSet = Set.Make (OrderedId) (** @return l2 \ l1 *) -let uri_list_diff l2 l1 = +let urixstring_list_diff l2 l1 = let module S = UriSet in let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in let diff = S.diff s2 s1 in S.fold (fun uri uris -> uri :: uris) diff [] +let uri_list_diff l2 l1 = + let module S = UriManager.UriSet in + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + (** @return l2 \ l1 *) let id_list_diff l2 l1 = let module S = IdSet in @@ -248,15 +255,16 @@ let remove_coercion uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) let time_travel ~present ~past = - let objs_to_remove = uri_list_diff present.objects past.objects in + let objs_to_remove = urixstring_list_diff present.objects past.objects in + let coercions_to_remove = uri_list_diff present.coercions past.coercions in let notation_to_remove = id_list_diff present.notation_ids past.notation_ids in let debug_list = ref [] in + List.iter remove_coercion coercions_to_remove; List.iter (fun (uri,p) -> MatitaMisc.safe_remove p; - remove_coercion uri; (try CicEnvironment.remove_obj uri with CicEnvironment.Object_not_found _ -> diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index df21e09f4..8bd32bb23 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -72,6 +72,7 @@ type status = { proof_status: proof_status; options: options; objects: (UriManager.uri * string) list; + coercions: UriManager.uri list; notation_ids: CicNotation.notation_id list; } diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index f27f2a11b..e54fe5c7e 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -62,6 +62,7 @@ type status = { proof_status: proof_status; (** logical status *) options: options; objects: (UriManager.uri * string) list; (** in-scope objects, with paths *) + coercions: UriManager.uri list; (** defined coercions *) notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) }