From: Ferruccio Guidi Date: Thu, 17 Jun 2021 11:50:05 +0000 (+0200) Subject: update in alpha_1 X-Git-Tag: make_still_working~142 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=caf822cbe34e204e6d1b72e272373b561c1a565a update in alpha_1 + type of terms redefined + Makefile added to lambdadelta/bin + a correction static_2/syntax/term.ma --- diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabst_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabst_1.ma new file mode 100644 index 000000000..163477eeb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabst_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λα ****************************************) + +notation "hvbox( ⓛ term 55 T )" + non associative with precedence 55 + for @{ 'SnAbst $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma deleted file mode 100644 index 72707b02e..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( -𝛌. break term 55 T )" - non associative with precedence 55 - for @{ 'SnAbstNeg $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma deleted file mode 100644 index 28f6c95ed..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( § term 90 l. break term 55 T )" - non associative with precedence 55 - for @{ 'SnGRef $l $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma deleted file mode 100644 index 130526cb6..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( ① [ term 46 I ]. break term 55 T )" - non associative with precedence 55 - for @{ 'SnItem1 $I $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma deleted file mode 100644 index 89516d493..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( # term 90 i. break term 55 T )" - non associative with precedence 55 - for @{ 'SnLRef $i $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma deleted file mode 100644 index 219df4d52..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( 𝛑[ term 46 p ] break term 55 T1. break term 55 T2 )" - non associative with precedence 55 - for @{ 'SnProj $p $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma deleted file mode 100644 index 5ed5322d2..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( -𝛑 term 55 T1. break term 55 T2 )" - non associative with precedence 55 - for @{ 'SnProjNeg $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma deleted file mode 100644 index a1b9213e4..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( +𝛑 term 55 T1. break term 55 T2 )" - non associative with precedence 55 - for @{ 'SnProjPos $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma deleted file mode 100644 index c16c15c06..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( ⋆ term 90 s. break term 55 T )" - non associative with precedence 55 - for @{ 'SnStar $s $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/item.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/item.ma deleted file mode 100644 index 7f7441d38..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/item.ma +++ /dev/null @@ -1,38 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* THE FORMAL SYSTEM α: MATITA SOURCE FILES - * Initial invocation : - Patience on me to gain peace and perfection! - - * Developed since : 2014 July 25 - *) - -include "ground/lib/bool.ma". -include "ground/lib/arith.ma". - -(* ITEMS ********************************************************************) - -(* unary items *) -inductive item1: Type[0] ≝ - | Char: nat → item1 (* character: starting at 0 *) - | LRef: nat → item1 (* reference by index: starting at 0 *) - | GRef: nat → item1 (* reference by position: starting at 0 *) - | Decl: item1 (* global abstraction *) -. - -(* binary items *) -inductive item2: Type[0] ≝ - | Abst: item2 (* local abstraction *) - | Abbr: bool → item2 (* local (Ⓣ) or global (Ⓕ) abbreviation *) - | Proj: bool → item2 (* local (Ⓣ) or global (Ⓕ) projection *) -. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma index 4334a0918..697150232 100644 --- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma +++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma @@ -12,69 +12,46 @@ (* *) (**************************************************************************) -include "static_2/notation/functions/snitem2_3.ma". -include "static_2/notation/functions/star_0.ma". -include "static_2/notation/functions/snabstpos_2.ma". -include "static_2/notation/functions/snabbr_3.ma". -include "static_2/notation/functions/snabbrpos_2.ma". -include "static_2/notation/functions/snabbrneg_2.ma". -include "alpha_1/notation/functions/snitem1_2.ma". -include "alpha_1/notation/functions/snstar_2.ma". -include "alpha_1/notation/functions/snlref_2.ma". -include "alpha_1/notation/functions/sngref_2.ma". -include "alpha_1/notation/functions/snabstneg_1.ma". -include "alpha_1/notation/functions/snproj_3.ma". -include "alpha_1/notation/functions/snprojpos_2.ma". -include "alpha_1/notation/functions/snprojneg_2.ma". -include "alpha_1/syntax/item.ma". +(* THE FORMAL SYSTEM λα: MATITA SOURCE FILES + * Initial invocation: - Patience on me to gain peace and perfection! - + * Conceived since: 2014 July 25 + * Developed since: 2021 June 17 + *) + +include "ground/arith/nat.ma". +include "static_2/notation/functions/star_1.ma". +include "static_2/notation/functions/gref_1.ma". +include "static_2/notation/functions/snappl_2.ma". +include "static_2/notation/functions/snabbr_2.ma". +include "alpha_1/notation/functions/snabst_1.ma". (* TERMS ********************************************************************) (* terms *) inductive term: Type[0] ≝ - | TAtom: term (* atomic item construction *) - | TUnit: item1 → term → term (* unary item construction *) - | TPair: item2 → term → term → term (* binary item construction *) + | TChar: nat → term (* character: starts at 0 *) + | TGRef: nat → term (* reference by level: starts at 0 *) + | TAbst: term → term (* abstraction: scope *) + | TAbbr: term → term → term (* abbreviation: definition, scope *) + | TCons: term → term → term (* group: body, tail *) . -interpretation "top (term)" - 'Star = TAtom. +interpretation + "character (terms)" + 'Star c = (TChar c). -interpretation "term construction (unary)" - 'SnItem1 I T = (TUnit I T). +interpretation + "reference (terms)" + 'GRef l = (TGRef l). -interpretation "term construction (binary)" - 'SnItem2 I T1 T2 = (TPair I T1 T2). +interpretation + "group (terms)" + 'SnAppl T1 T2 = (TCons T1 T2). -interpretation "character (term)" - 'SnStar s T = (TUnit (Char s) T). +interpretation + "abbreviation (terms)" + 'SnAbbr T1 T2 = (TAbbr T1 T2). -interpretation "local reference (term)" - 'SnLRef i T = (TUnit (LRef i) T). - -interpretation "global reference (term)" - 'SnGRef l T = (TUnit (GRef l) T). - -interpretation "negative abbreviation (term)" - 'SnAbbrNeg T = (TUnit Decl T). - -interpretation "positive abstraction (term)" - 'SnAbstPos T1 T2 = (TPair Abst T1 T2). - -interpretation "abbreviation (term)" - 'SnAbbr p T1 T2 = (TPair (Abbr p) T1 T2). - -interpretation "positive abbreviation (term)" - 'SnAbbrPos T1 T2 = (TPair (Abbr true) T1 T2). - -interpretation "negative abbreviation (term)" - 'SnAbbrNeg T1 T2 = (TPair (Abbr false) T1 T2). - -interpretation "projection (term)" - 'SnProj p T1 T2 = (TPair (Proj p) T1 T2). - -interpretation "positive projection (term)" - 'SnProjPos T1 T2 = (TPair (Proj true) T1 T2). - -interpretation "negative projection (term)" - 'SnProjNeg T1 T2 = (TPair (Proj false) T1 T2). +interpretation + "abstraction (terms)" + 'SnAbst T = (TAbst T). diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma deleted file mode 100644 index 63ddda16f..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "alpha_1/syntax/term.ma". - -(* TERMS ********************************************************************) - -let rec tappend T U on T ≝ match T with -[ TAtom ⇒ U -| TUnit I T ⇒ ①[I].(tappend T U) -| TPair I V T ⇒ ②[I]V.(tappend T U) -]. - -interpretation "append (term)" 'plus T U = (tappend T U). diff --git a/matita/matita/contribs/lambdadelta/bin/Makefile b/matita/matita/contribs/lambdadelta/bin/Makefile new file mode 100644 index 000000000..74274ddb3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/Makefile @@ -0,0 +1,10 @@ +H=@ + +BINARIES = inline xhtbl index roles recomm + +all: $(BINARIES:%=rec@all@%) +clean: $(BINARIES:%=rec@clean@%) + +rec@%: + $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) + diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma index 0a6f97872..cec29d172 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma @@ -49,7 +49,7 @@ interpretation 'SnItem2 I T1 T2 = (TPair I T1 T2). interpretation - "term binding construction (binary)" + "term binding construction (binary)" 'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2). interpretation