From ec6b4df6d02ff30a7a1cd784831017b05b1d46dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 7 Jun 2005 17:37:16 +0000 Subject: [PATCH] added coercions --- helm/matita/matitaScript.ml | 9 +++++++-- helm/matita/matitaSync.ml | 16 ++++++++++------ helm/matita/tests/fix_betareduction.ma | 8 ++++++++ helm/matita/tests/match_inference.ma | 17 +++++++++++++++++ helm/matita/tests/mysql_escaping.ma | 3 +++ 5 files changed, 45 insertions(+), 8 deletions(-) create mode 100644 helm/matita/tests/fix_betareduction.ma create mode 100644 helm/matita/tests/match_inference.ma create mode 100644 helm/matita/tests/mysql_escaping.ma diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 99b7018e4..26a0f2487 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -93,8 +93,13 @@ let eval_with_engine status user_goal parsed_text st = let module UM = UriManager in DTE.fold ( fun k ((v,_) as value) acc -> - let v = UM.strip_xpointer (UM.uri_of_string v) in - if List.exists (fun (s,_) -> s = v) new_status.objects then + let b = + try + let v = UM.strip_xpointer (UM.uri_of_string v) in + List.exists (fun (s,_) -> s = v) new_status.objects + with UM.IllFormedUri _ -> false + in + if b then acc else DTE.add k value acc diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index fbcac945a..9a44742b7 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -170,21 +170,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 diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma new file mode 100644 index 000000000..32f298d60 --- /dev/null +++ b/helm/matita/tests/fix_betareduction.ma @@ -0,0 +1,8 @@ +alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". +alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +theorem a: + (\forall p: nat \to Prop. + \forall n: nat. p n \to p n ) \to (eq nat n n). +intro. +apply (H (\lambda n:nat.(eq nat n n))). \ No newline at end of file diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma new file mode 100644 index 000000000..a84b3c373 --- /dev/null +++ b/helm/matita/tests/match_inference.ma @@ -0,0 +1,17 @@ +inductive pos: Set \def +| one : pos +| next : pos \to pos. + +inductive nat:Set \def +| O : nat +| S : nat \to nat. + +inductive empty : Set \def . + +definition pos2nat : pos \to nat \def + \lambda x:pos . match x with + [ one \Rightarrow O + | (next z) \Rightarrow O]. + +definition empty2nat : empty \to nat \def + \lambda x : empty . S (match x in empty with []). \ No newline at end of file diff --git a/helm/matita/tests/mysql_escaping.ma b/helm/matita/tests/mysql_escaping.ma new file mode 100644 index 000000000..798ab2786 --- /dev/null +++ b/helm/matita/tests/mysql_escaping.ma @@ -0,0 +1,3 @@ +theorem a' : Prop \to Prop.intros.assumption.qed. + + -- 2.39.2