correzioni Gabriel #3

tesi/tesi_unicode.org

@@ -1039,16 +1039,29 @@ A source program tₛ is a collection of pattern clauses pointing to
 tₛ(vₛ) produces a result /r/ belonging to the following grammar:
 | tₛ ::= (p → bb)^{i∈I}
 | tₛ(vₛ) → r
-| r ::= guard list * (Match bb \vert{} NoMatch \vert{} Absurd)
+| r ::= guard list * (Match (σ, bb) \vert{} NoMatch \vert{} Absurd)
+
+\begin{comment}
+TODO: running a value against a tree:
+| Leaf(bb) (vᵢ) := bb
+| Failure (vᵢ) := Failure
+| Unreachable (vᵢ) := Unreachable if source tree
+| Node(a, Cᵢ, C?) := C_min{i | Cᵢ(vᵢ(a)) ≠ ⊥}
+| Node (a, Cᵢ, None) :=  ⊥ if ∀Cᵢ, Cᵢ(vᵢ(a)) = ⊥ 
+| Node (a, Cᵢ, C?) :=  C?(vᵢ(a)) if ∀Cᵢ, Cᵢ(vᵢ(a)) = ⊥ 
+
+\end{comment}
+
 \begin{comment}
 TODO: understand how to explain guard
 \end{comment}
 We can define what it means to run an input value vₛ against a source
 program tₛ:
-| tₛ(vₛ) := ⊥ \quad \quad \quad if ∀i, pᵢ(vₛ) = ⊥
 | First((xᵢ)ⁱ) := x_min{i \vert{} xᵢ ≠ ⊥}  \quad  if ∃i, xᵢ ≠ ⊥ 
-| tₛ(vₛ) = Absurd if bb_min{pᵢ → bbᵢ \vert{} pᵢ(vₛ) ≠ ⊥} = /refutation clause/
+| tₛ(vₛ) := NoMatch \quad if ∀i, pᵢ(vₛ) = ⊥
-| tₛ(vₛ) = Match bb_min{pᵢ → bbᵢ \vert{} pᵢ(vₛ) ≠ ⊥}
+| tₛ(vₛ) = { Absurd if bb_{i₀} = . (refutation clause)
+| \quad \quad \quad \quad \quad Match (σ, bb_{i₀}) otherwise
+| \quad \quad \quad \quad \quad where iₒ = min{i \vert{} pᵢ(vₛ) ≠ ⊥}
 /guard/ and /bb/ expressions are treated as blackboxes of OCaml code.
 A sound approach for treating these blackboxes would be to inspect the
 OCaml compiler during translation to Lambda code and extract the
@@ -1376,7 +1389,7 @@ the wildcard submatrix.
 We formalize this intuition as follows
 *** Lemma (Groups):
     Let /m/ be a matrix with 
-    | Groups(m) = (k_r \to m_r)^k, m_{wild}
+    | Groups(m) = (kᵣ \to mᵣ)^k, m_{wild}
     For any value vector $(v_i)^l$ such that $v_0 = k(v'_l)^l$ for some
     constructor k,
     we have:
@@ -1399,7 +1412,7 @@ variable.
 Let (vᵢ)ⁱ be an input matrix with v₀ = Kᵥ(v'_{l})ˡ for some constructor Kᵥ.
 We have to show that:
 - if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then
-    m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ)
+  | m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ)
 - otherwise
     m(vᵢ)ⁱ = m_{wild}(tail(vᵢ)ⁱ)
 Let us call (rₖⱼ) the j-th row of the submatrix mₖ, and rⱼ_{wild}
@@ -1438,6 +1451,33 @@ By definition of (pᵢ)ⁱ(vᵢ)ⁱ we know that (pᵢⱼ)ⁱ(vᵢ) is equal to
 We prove this first case by a second case analysis on p₀ⱼ.
 
 TODO
+\begin{comment}
+GOAL:
+| (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ +++ tail(vᵢ)ⁱ
+case analysis on pₒⱼ:
+| pₒⱼ    | pᵢⱼ                   |
+|--------+-----------------------|
+| Kₖ(qₗ) | (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ  |
+| else   |  ⊥                    |
+that is exactly the same as  rₖⱼ :=  (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ  → eⱼ 
+But I am just putting together the definition given above (in the pdf).
+
+
+Second case, below:
+the wildcard matrix r_{jwild} is 
+| tail(aᵢ)ⁱ, (tail(pᵢⱼ)ⁱ  → eⱼ if p₀ⱼ is _ else ⊥)ʲ
+
+case analysis on p₀ⱼ:
+| pₒⱼ    | (pᵢⱼ)ⁱ                |
+|--------+-----------------------|
+| Kₖ(qₗ) | (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ  | not possible because we are in the second case
+| _      | (_)ˡ +++ tail(pᵢⱼ)ⁱ   |
+| else   |  ⊥                    |
+
+
+Both seems too trivial to be correct.
+
+\end{comment}
 
 In the second case (Kᵥ is distinct from Kₖ for all Kₖ ∈ constrs(pₒⱼ)ʲ),
 we have to prove that