loa

commit 8f5f7a310b42fc1144b6696334a175c68a38cbb3
parent 13a9ecc93ef4334db0fca4aa33e38b2fa759ebfc
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date:   Wed,  7 Feb 2024 15:12:32 -0300

Add a proto-specification of the data model

Diffstat:
A
coding/NOTES.md
 | 
46
++++++++++++++++++++++++++++++++++++++++++++++

1 file changed, 46 insertions(+), 0 deletions(-)
diff --git a/coding/NOTES.md b/coding/NOTES.md
@@ -0,0 +1,46 @@
+- AllwoodZipper2010
+
+# Model
+
+The state of the machine consists of the following:
+
+- `cursor`: the structure built so far. Starts as `empty`.
+- A `focus`: if there at least one hole in the structure, a pointer to the first one.
+
+All data structures can have child values replaced with a *hole*, which
+has a type corresponding to the shape of what can fill that hole. When
+focused on a hole with a certain type, the machine expects the next
+instruction to indicate a constructor of that type. For example:
+
+- If the hole is for a **number**, it expects a number.
+- If the hole is for a **symbol**, it expects a symbol.
+- If the hole if for a list, it expects **empty** or **cons**.
+
+When meeting such an instruction, the machine will then *fill* the hole
+with a *template* for that constructor. That just means it will put a
+value in the hole using that constructor, but with its arguments being
+holes of the appropriate types.
+
+The possible types for holes are those that have more than one
+constructor, as all others can be filled automatically. So, that means these:
+
+- Number
+- Symbol
+- Lists
+
+When there is no hole in the structure at the `cursor`, the available
+instructions are those that apply constructors using the current structure
+as an argument. This means a single one: `top`.
+
+```
+	top := (attitude | assumption) * top | empty
+```
+
+So the machine will create a new `top` with the one at `cursor` as its
+argument, and a hole for the other argument.
+
+Finally, when a hole is filled with an atomic value (i.e., there's no
+subhole), the `focus` goes to the next available hole.
+
+Every node in the structure must be verified for its legality conditions
+as soon as possible; i.e., as soon as all its holes are filled.