contribution on delayed updating begins

we place it here for convenience

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma
new file mode 100644 (file)
index 0000000..0889615
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝗔 )"
+  non associative with precedence 75
+  for @{ 'EdgeLabelA }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma
new file mode 100644 (file)
index 0000000..980f431
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝗟 )"
+  non associative with precedence 75
+  for @{ 'EdgeLabelL }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma
new file mode 100644 (file)
index 0000000..d9d9182
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝗦 )"
+  non associative with precedence 75
+  for @{ 'EdgeLabelS }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/element_e_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/element_e_0.ma
new file mode 100644 (file)
index 0000000..09651c1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/element_e_0.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( 𝐞 )"
+  non associative with precedence 75
+  for @{ 'ElementE }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
new file mode 100644 (file)
index 0000000..8412e58
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( 𝗱❨ break term 46 a ❩ )"
+  non associative with precedence 75
+  for @{ 'NodeLabelD $a }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
new file mode 100644 (file)
index 0000000..1241db4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/arith/pnat.ma".
+include "delayed_updating/notation/functions/nodelabel_d_1.ma".
+include "delayed_updating/notation/functions/edgelabel_l_0.ma".
+include "delayed_updating/notation/functions/edgelabel_a_0.ma".
+include "delayed_updating/notation/functions/edgelabel_s_0.ma".
+
+(* LABEL ********************************************************************)
+
+inductive label: Type[0] ≝
+| label_node_d: pnat → label
+| label_edge_l: label
+| label_edge_a: label
+| label_edge_s: label
+.
+
+coercion label_node_d.
+
+interpretation
+  "variable reference by depth (label)"
+  'NodeLabelD p = (label_node_d p).
+
+interpretation
+  "name-free functional abstruction (label)"
+  'EdgeLabelL = (label_edge_l).
+
+interpretation
+  "application (label)"
+  'EdgeLabelA = (label_edge_a).
+
+interpretation
+  "side branch (label)"
+  'EdgeLabelS = (label_edge_s).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
new file mode 100644 (file)
index 0000000..6935596
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/lib/list.ma".
+include "delayed_updating/notation/functions/element_e_0.ma".
+include "delayed_updating/syntax/label.ma".
+
+(* PATH *********************************************************************)
+
+definition path ≝ list label.
+
+interpretation
+  "empty (paths)"
+  'ElementE = (list_nil label).

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 67c3571a48f954de4bd368b4c8b559d542c2ceb7..26a2656e38680b57173338f1ad9081af2affec15 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1535,17 +1535,17 @@ let predefined_classes = [
  ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; 
  ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
- ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
+ ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; "𝗔"; ] ;
  ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
  ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ;
  ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ;
  ["C"; "ℭ"; "∁"; "𝐂"; "ℂ"; "Ⓒ"; ] ;
- ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; ] ;
- ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; ] ;
+ ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; "𝗱"; ] ;
+ ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; "𝗗"; ] ;
  ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ;
  ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ;
  ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ;
- ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; ] ;
+ ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; "𝗙"; ] ;
  ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ;
  ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ;
  ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; "𝐡"; "ⓗ"; ] ;
@@ -1557,7 +1557,7 @@ let predefined_classes = [
  ["k"; "κ"; "𝕜"; "𝐤"; "𝛋"; "ⓚ"; ] ;
  ["K"; "𝕂"; "𝐊"; "Ⓚ"; ] ;
  ["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; "ⓛ"; ] ;
- ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; ] ;
+ ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; "𝗟"; ] ;
  ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; ] ;
  ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
  ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
@@ -1571,7 +1571,7 @@ let predefined_classes = [
  ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ;
  ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; ] ;
  ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ;
- ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; ] ;
+ ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; "𝗦"; ] ;
  ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ;
  ["T"; "𝕋"; "𝐓"; "Ⓣ"; "⊥"; ] ;
  ["u"; "𝕦"; "𝐮"; "ⓤ"; ] ;