From 9e32b487a1343ead9069ea76e40515ceb19d26d6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Feb 2006 18:22:12 +0000 Subject: [PATCH] Coercions are now hidden by default (in termAcicContent.ml) --- components/acic_content/termAcicContent.ml | 20 ++++++++++++++++- components/acic_content/termAcicContent.mli | 2 ++ matita/library/algebra/finite_groups.ma | 24 --------------------- matita/library/algebra/groups.ma | 24 --------------------- matita/library/algebra/monoids.ma | 16 -------------- matita/library/algebra/semigroups.ma | 8 ------- matita/matita.ml | 4 ++++ 7 files changed, 25 insertions(+), 73 deletions(-) diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml index fddd777f7..a25730e4d 100644 --- a/components/acic_content/termAcicContent.ml +++ b/components/acic_content/termAcicContent.ml @@ -66,6 +66,8 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) +let hide_coercions = ref true;; + let ast_of_acic0 term_info acic k = let k = k term_info in let id_to_uris = term_info.uri in @@ -117,7 +119,23 @@ let ast_of_acic0 term_info acic k = | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None), k s, k t)) - | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args)) + | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args)) + | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args)) + | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) -> + if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && + !hide_coercions + then + let rec last = + function + [] -> assert false + | [t] -> t + | _::tl -> last tl + in + idref aid (k (last tl)) + else + idref aid (Ast.Appl (List.map k args)) + | Cic.AAppl (aid,args) -> + idref aid (Ast.Appl (List.map k args)) | Cic.AConst (id,uri,substs) -> register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) diff --git a/components/acic_content/termAcicContent.mli b/components/acic_content/termAcicContent.mli index 1fd57e0d0..214d7f5d2 100644 --- a/components/acic_content/termAcicContent.mli +++ b/components/acic_content/termAcicContent.mli @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +val hide_coercions: bool ref + (** {2 Persistant state handling} *) type interpretation_id diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma index 2b731d302..2078cf1d7 100644 --- a/matita/library/algebra/finite_groups.ma +++ b/matita/library/algebra/finite_groups.ma @@ -44,30 +44,6 @@ record finite_enumerable_SemiGroup : Type ≝ is_finite_enumerable:> finite_enumerable semigroup }. -notation < "S" -for @{ 'semigroup_of_finite_enumerable_semigroup $S }. - -interpretation "Semigroup_of_finite_enumerable_semigroup" - 'semigroup_of_finite_enumerable_semigroup S -= - (cic:/matita/algebra/finite_groups/semigroup.con S). - -notation < "S" -for @{ 'magma_of_finite_enumerable_semigroup $S }. - -interpretation "Magma_of_finite_enumerable_semigroup" - 'magma_of_finite_enumerable_semigroup S -= - (cic:/matita/algebra/finite_groups/Magma_of_finite_enumerable_SemiGroup.con S). - -notation < "S" -for @{ 'type_of_finite_enumerable_semigroup $S }. - -interpretation "Type_of_finite_enumerable_semigroup" - 'type_of_finite_enumerable_semigroup S -= - (cic:/matita/algebra/finite_groups/Type_of_finite_enumerable_SemiGroup.con S). - interpretation "Finite_enumerable representation" 'repr S i = (cic:/matita/algebra/finite_groups/repr.con S (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i). diff --git a/matita/library/algebra/groups.ma b/matita/library/algebra/groups.ma index 57c43d4ae..5d3be8cb1 100644 --- a/matita/library/algebra/groups.ma +++ b/matita/library/algebra/groups.ma @@ -35,24 +35,6 @@ record Group : Type ≝ group_properties:> isGroup pregroup }. -(*notation < "G" -for @{ 'monoid $G }. - -interpretation "Monoid coercion" 'monoid G = - (cic:/matita/algebra/groups/monoid.con G).*) - -notation < "G" -for @{ 'type_of_group $G }. - -interpretation "Type_of_group coercion" 'type_of_group G = - (cic:/matita/algebra/groups/Type_of_Group.con G). - -notation < "G" -for @{ 'magma_of_group $G }. - -interpretation "magma_of_group coercion" 'magma_of_group G = - (cic:/matita/algebra/groups/Magma_of_Group.con G). - notation "hvbox(x \sup (-1))" with precedence 89 for @{ 'ginv $x }. @@ -203,12 +185,6 @@ record subgroup (G:Group) : Type ≝ embed:> monomorphism group G }. -notation < "G" -for @{ 'type_of_subgroup $G }. - -interpretation "Type_of_subgroup coercion" 'type_of_subgroup G = - (cic:/matita/algebra/groups/Type_of_subgroup.con _ G). - notation "hvbox(x \sub H)" with precedence 79 for @{ 'subgroupimage $H $x }. diff --git a/matita/library/algebra/monoids.ma b/matita/library/algebra/monoids.ma index 63b6430ec..a80ee5fb0 100644 --- a/matita/library/algebra/monoids.ma +++ b/matita/library/algebra/monoids.ma @@ -21,10 +21,6 @@ record PreMonoid : Type ≝ e: magma }. -notation < "M" for @{ 'pmmagma $M }. -interpretation "premonoid magma coercion" 'pmmagma M = - (cic:/matita/algebra/monoids/magma.con M). - record isMonoid (M:PreMonoid) : Prop ≝ { is_semi_group:> isSemiGroup M; e_is_left_unit: @@ -38,18 +34,6 @@ record Monoid : Type ≝ monoid_properties:> isMonoid premonoid }. -notation < "M" for @{ 'semigroup $M }. -interpretation "premonoid coercion" 'premonoid M = - (cic:/matita/algebra/monoids/premonoid.con M). - -notation < "M" for @{ 'typeofmonoid $M }. -interpretation "premonoid coercion" 'typeofmonoid M = - (cic:/matita/algebra/monoids/Type_of_Monoid.con M). - -notation < "M" for @{ 'magmaofmonoid $M }. -interpretation "premonoid coercion" 'magmaofmonoid M = - (cic:/matita/algebra/monoids/Magma_of_Monoid.con M). - notation "1" with precedence 89 for @{ 'munit }. diff --git a/matita/library/algebra/semigroups.ma b/matita/library/algebra/semigroups.ma index 73099286b..12ff95311 100644 --- a/matita/library/algebra/semigroups.ma +++ b/matita/library/algebra/semigroups.ma @@ -23,10 +23,6 @@ record Magma : Type ≝ op: carrier → carrier → carrier }. -notation < "M" for @{ 'carrier $M }. -interpretation "carrier coercion" 'carrier S = - (cic:/matita/algebra/semigroups/carrier.con S). - notation "hvbox(a break \middot b)" left associative with precedence 55 for @{ 'magma_op $a $b }. @@ -44,10 +40,6 @@ record SemiGroup : Type ≝ semigroup_properties:> isSemiGroup magma }. -notation < "S" for @{ 'magma $S }. -interpretation "magma coercion" 'magma S = - (cic:/matita/algebra/semigroups/magma.con S). - definition is_left_unit ≝ λS:SemiGroup. λe:S. ∀x:S. e·x = x. diff --git a/matita/matita.ml b/matita/matita.ml index 2cbb9a9a1..a8a031273 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -191,6 +191,10 @@ let _ = (fun _ -> CicNotation.set_active_notations (List.map fst (CicNotation.get_all_notations ()))); + addDebugItem "enable coercions hiding" + (fun _ -> TermAcicContent.hide_coercions := true); + addDebugItem "disable coercions hiding" + (fun _ -> TermAcicContent.hide_coercions := false); end (** Debugging }}} *) -- 2.39.2