From 8d961585c4ff785d558d5b4c84adf656595ca487 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 26 Jan 2009 17:12:38 +0000 Subject: [PATCH] maction support added to notation, adopted for = AKA = \sub t deactivated the library/formal_topology directory since it is completely broken and outdated --- helm/software/matita/core_notation.moo | 18 ++++++-- .../software/matita/library/algebra/groups.ma | 4 +- .../models/increasing_supremum_stabilizes.ma | 2 +- .../library/dama/property_exhaustivity.ma | 2 +- helm/software/matita/library/dama/supremum.ma | 2 +- .../matita/library/datatypes/categories.ma | 4 +- .../matita/library/datatypes/subsets.ma | 4 ++ helm/software/matita/library/depends | 6 --- ...ic_pairs.ma => basic_pairs.ma.dontcompile} | 0 ...ies.ma => basic_topologies.ma.dontcompile} | 0 ...aces.ma => concrete_spaces.ma.dontcompile} | 0 ...es.ma => formal_topologies.ma.dontcompile} | 0 ...{relations.ma => relations.ma.dontcompile} | 0 ... => saturations_reductions.ma.dontcompile} | 0 .../software/matita/library/logic/equality.ma | 6 +-- helm/software/matita/matitaMathView.ml | 44 +++++++++++++++++-- 16 files changed, 68 insertions(+), 24 deletions(-) rename helm/software/matita/library/formal_topology/{basic_pairs.ma => basic_pairs.ma.dontcompile} (100%) rename helm/software/matita/library/formal_topology/{basic_topologies.ma => basic_topologies.ma.dontcompile} (100%) rename helm/software/matita/library/formal_topology/{concrete_spaces.ma => concrete_spaces.ma.dontcompile} (100%) rename helm/software/matita/library/formal_topology/{formal_topologies.ma => formal_topologies.ma.dontcompile} (100%) rename helm/software/matita/library/formal_topology/{relations.ma => relations.ma.dontcompile} (100%) rename helm/software/matita/library/formal_topology/{saturations_reductions.ma => saturations_reductions.ma.dontcompile} (100%) diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 8709f0265..fc6a15b06 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -47,9 +47,12 @@ notation < "hvbox(a break \to b)" right associative with precedence 20 for @{ \Pi $_:$a.$b }. -notation "hvbox(a break = b)" +notation > "hvbox(a break = b)" non associative with precedence 45 -for @{ 'eq $a $b }. +for @{ 'eq ? $a $b }. +notation < "hvbox(a break maction (=) (=\sub t) b)" + non associative with precedence 45 +for @{ 'eq $t $a $b }. notation "hvbox(a break \leq b)" non associative with precedence 45 @@ -67,9 +70,13 @@ notation "hvbox(a break \gt b)" non associative with precedence 45 for @{ 'gt $a $b }. -notation "hvbox(a break \neq b)" +notation > "hvbox(a break \neq b)" + non associative with precedence 45 +for @{ 'neq ? $a $b }. + +notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" non associative with precedence 45 -for @{ 'neq $a $b }. +for @{ 'neq $t $a $b }. notation "hvbox(a break \nleq b)" non associative with precedence 45 @@ -232,3 +239,6 @@ notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. notation > "⊩ " with precedence 60 for @{'Vdash ?}. notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. +notation < "maction (mstyle color #ff0000 (­…­)) (t)" +non associative with precedence 90 for @{'hide $t}. + diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index f257951bc..d6e77ae8d 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -218,8 +218,8 @@ definition left_coset_eq ≝ λG.λC,C':left_coset G. ∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'. -interpretation "Left cosets equality" 'eq C C' = - (cic:/matita/algebra/groups/left_coset_eq.con _ C C'). +interpretation "Left cosets equality" 'eq t C C' = + (cic:/matita/algebra/groups/left_coset_eq.con t C C'). definition left_coset_disjoint ≝ λG.λC,C':left_coset G. diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma index 6dc55e142..46aa96eb1 100644 --- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma +++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma @@ -58,7 +58,7 @@ letin m ≝ (hide ? ( rewrite > (?:x = O); [2: cases Hx; lapply (os_le_to_nat_le ?? H1); apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin). - |1: intros; unfold Type_of_ordered_set in sg; + |1: intros; unfold Type_OF_ordered_set in sg a; whd in a:(? %); lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P; simplify in P:(???%); lapply (le_transitive ??? P H1) as W; lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);] diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma index 4dec6442e..f76660190 100644 --- a/helm/software/matita/library/dama/property_exhaustivity.ma +++ b/helm/software/matita/library/dama/property_exhaustivity.ma @@ -115,7 +115,7 @@ intros; split; qed. lemma hint_mah1: - ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C). + ∀C. Type_OF_ordered_uniform_space__1 C → hos_carr (os_r C). intros; assumption; qed. coercion hint_mah1 nocomposites. diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma index be8495970..2ce417ecc 100644 --- a/helm/software/matita/library/dama/supremum.ma +++ b/helm/software/matita/library/dama/supremum.ma @@ -121,7 +121,7 @@ interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)). lemma hint_nat : - Type_of_ordered_set nat_ordered_set → + Type_OF_ordered_set nat_ordered_set → hos_carr (os_l (nat_ordered_set)). intros; assumption; qed. diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma index 65bc8ac6b..f5b23dfdd 100644 --- a/helm/software/matita/library/datatypes/categories.ma +++ b/helm/software/matita/library/datatypes/categories.ma @@ -80,8 +80,8 @@ qed. coercion Leibniz. *) -interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y). -interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y). +interpretation "setoid1 eq" 'eq t x y = (eq_rel1 _ (eq1 t) x y). +interpretation "setoid eq" 'eq t x y = (eq_rel _ (eq t) x y). interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r). interpretation "setoid symmetry" 'invert r = (sym ____ r). notation ".= r" with precedence 50 for @{'trans $r}. diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma index 7c9a13195..8c7963d67 100644 --- a/helm/software/matita/library/datatypes/subsets.ma +++ b/helm/software/matita/library/datatypes/subsets.ma @@ -26,6 +26,8 @@ theorem transitive_subseteq_operator: ∀A. transitive ? (subseteq_operator A). assumption. qed. +(* + definition powerset_setoid: setoid → setoid1. intros (T); constructor 1; @@ -136,3 +138,5 @@ definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A). qed. interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a). + +*) \ No newline at end of file diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index c06799274..aaf7d6869 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,4 +1,3 @@ -formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma dama/sandwich.ma dama/ordered_uniform.ma Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma @@ -16,7 +15,6 @@ technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic nat/div_and_mod_diseq.ma nat/lt_arith.ma logic/cprop_connectives.ma logic/connectives.ma algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma -formal_topology/saturations_reductions.ma datatypes/subsets.ma formal_topology/relations.ma nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma @@ -26,7 +24,6 @@ dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_s didactic/exercises/substitution.ma nat/minus.ma didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma -formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma logic/connectives.ma Q/nat_fact/times.ma nat/factorization.ma @@ -65,11 +62,9 @@ nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma didactic/support/natural_deduction.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma -formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma didactic/exercises/shannon.ma nat/minus.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma -formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma nat/minus.ma nat/compare.ma nat/le_arith.ma Q/ratio/ratio.ma Q/fraction/fraction.ma nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma @@ -79,7 +74,6 @@ nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma -formal_topology/relations.ma datatypes/subsets.ma higher_order_defs/relations.ma logic/connectives.ma nat/factorization.ma nat/ord.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile similarity index 100% rename from helm/software/matita/library/formal_topology/basic_pairs.ma rename to helm/software/matita/library/formal_topology/basic_pairs.ma.dontcompile diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile similarity index 100% rename from helm/software/matita/library/formal_topology/basic_topologies.ma rename to helm/software/matita/library/formal_topology/basic_topologies.ma.dontcompile diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile similarity index 100% rename from helm/software/matita/library/formal_topology/concrete_spaces.ma rename to helm/software/matita/library/formal_topology/concrete_spaces.ma.dontcompile diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile similarity index 100% rename from helm/software/matita/library/formal_topology/formal_topologies.ma rename to helm/software/matita/library/formal_topology/formal_topologies.ma.dontcompile diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma.dontcompile similarity index 100% rename from helm/software/matita/library/formal_topology/relations.ma rename to helm/software/matita/library/formal_topology/relations.ma.dontcompile diff --git a/helm/software/matita/library/formal_topology/saturations_reductions.ma b/helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile similarity index 100% rename from helm/software/matita/library/formal_topology/saturations_reductions.ma rename to helm/software/matita/library/formal_topology/saturations_reductions.ma.dontcompile diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index cc181dfbf..73728dc92 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -19,11 +19,11 @@ inductive eq (A:Type) (x:A) : A \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "leibnitz's equality" - 'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y). + 'eq t x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y). (*CSC: the URI must disappear: there is a bug now *) interpretation "leibnitz's non-equality" - 'neq x y = (cic:/matita/logic/connectives/Not.con - (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)). + 'neq t x y = (cic:/matita/logic/connectives/Not.con + (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y)). theorem eq_rect': \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type. diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 7cb2aa7cb..19eeaf0d7 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -65,9 +65,11 @@ let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in (distance < 4.) +let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML" let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" let href_ds = Gdome.domString "href" +let maction_ds = Gdome.domString "maction" let xref_ds = Gdome.domString "xref" let domImpl = Gdome.domImplementation () @@ -163,6 +165,17 @@ let hrefs_of_elt elt = else None +let rec has_maction (elt :Gdome.element) = + (* fix this comparison *) + if elt#get_tagName#to_string = "m:maction" then + true + else + match elt#get_parentNode with + | Some node when node#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE -> + has_maction (new Gdome.element_of_node node) + | _ -> false +;; + class clickableMathView obj = let text_width = 80 in object (self) @@ -176,7 +189,8 @@ object (self) method private cic_info = _cic_info val normal_cursor = Gdk.Cursor.create `LEFT_PTR - val href_cursor = Gdk.Cursor.create `HAND1 + val href_cursor = Gdk.Cursor.create `HAND2 + val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW initializer self#set_font_size !current_font_size; @@ -221,7 +235,11 @@ object (self) button_press_y <- GdkEvent.Button.y gdk_button; selection_changed <- false end else if button = right_button then - self#popup_contextual_menu (GdkEvent.Button.time gdk_button); + self#popup_contextual_menu + (self#get_element_at + (int_of_float (GdkEvent.Button.x gdk_button)) + (int_of_float (GdkEvent.Button.y gdk_button))) + (GdkEvent.Button.time gdk_button); false method private element_over_cb (elt_opt, _, _, _) = @@ -233,6 +251,9 @@ object (self) in match elt_opt with | Some elt -> + if has_maction elt then + Gdk.Window.set_cursor (win ()) maction_cursor + else (match hrefs_of_elt elt with | Some ((_ :: _) as hrefs) -> Gdk.Window.set_cursor (win ()) href_cursor; @@ -274,22 +295,36 @@ object (self) | [] -> assert false (* this method is invoked only if there's a sel. *) | node :: _ -> self#tactic_text_pattern_of_node node - method private popup_contextual_menu time = + method private popup_contextual_menu element time = let menu = GMenu.menu () in let add_menu_item ?(menu = menu) ?stock ?label () = GMenu.image_menu_item ?stock ?label ~packing:menu#append () in let check = add_menu_item ~label:"Check" () in let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in + let hyperlinks_menu_item = GMenu.menu_item ~label:"Hyperlinks" () in menu#append reductions_menu_item; menu#append tactics_menu_item; + menu#append hyperlinks_menu_item; let reductions = GMenu.menu () in let tactics = GMenu.menu () in + let hyperlinks = GMenu.menu () in reductions_menu_item#set_submenu reductions; tactics_menu_item#set_submenu tactics; + hyperlinks_menu_item#set_submenu hyperlinks; let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in + (match element with + | None -> hyperlinks_menu_item#misc#set_sensitive false + | Some elt -> + match hrefs_of_elt elt, href_callback with + | Some l, Some f -> + List.iter + (fun h -> + let item = add_menu_item ~menu:hyperlinks ~label:h () in + connect_menu_item item (fun () -> f h)) l + | _ -> hyperlinks_menu_item#misc#set_sensitive false); menu#append (GMenu.separator_item ()); let copy = add_menu_item ~stock:`COPY () in let gui = get_gui () in @@ -329,9 +364,10 @@ object (self) (match self#get_element_at x y with | None -> () | Some elt -> + if has_maction elt then ignore(self#action_toggle elt) else (match hrefs_of_elt elt with | Some hrefs -> self#invoke_href_callback hrefs gdk_button - | None -> ignore (self#action_toggle elt))) + | None -> ())) end; false -- 2.39.2