docs

linsyking · Apr 2, 2023 · b87d307 · b87d307
1 parent 0f4024c
commit b87d307
Show file tree

Hide file tree

Showing 6 changed files with 208 additions and 107 deletions.
diff --git a/Readme.md b/Readme.md
@@ -1,88 +1,53 @@
-# Meow lang
-
-Meow lang is a programming language that is designed **not** to be easy to learn and use.
-
-Its main design purpose is to do experiments with "string replacement".
-
-## How to run
-
-```bash
-cargo run <your meow file path>
-
-# Now you can use the REPL to evaluate expressions
-```
-
-Run the example code:
-
-```
-no error found.
-> true()
-T
-> false()
-F
-> {var x = zero();succ(x)}
-S0
-> dr("a","aba","aba")
-aba
-> m()
-abcd
-```
-
-## Examples
-
-```meow
-true() {"T"}
-
-false() {"F"}
-
-zero() {"0"}
-
-succ(x) {"S"+x}
-
-pred(x) {
-    "S0" = "0";
-    x
-}
-
-dr(x,y,z) {
-    y = x;
-    x = y;
-    z
-}
-
-rep_test() {
-    "dd" = "d";
-    var x = {"dddd"};
-    var y = "dddd";
-    "x=" + x + ",y=" + y
-}
-
-encode(s) {
-    var rep = {
-        "\" = "\\";
-        "$" = "\$";
-        "^" = "\^";
-        s
-    };
-    "_^"+ rep +"_$"
-}
-
-decode(s) {
-    var rep = {
-        "_^" = "";
-        "_$" = "";
-        s
-    };
-    "\$" = "$";
-    "\^" = "^";
-    "\\" = "\";
-    rep
-}
-
-m(){
-    var s = "abcd";
-    var enc = encode(s);
-    var dec = decode(enc);
-    dec
-}
-```
+# Meow lang
+
+Meow lang is a programming language that is designed **not** to be easy to learn and use.
+
+Its main design purpose is to do experiments with "string replacement".
+
+## Formal Definition
+
+Currently the definition of replacement of strings are defined by the built-in `replace` function of `String`.
+
+## Concepts
+
+There are **no** functions in Meow. Instead, we have *macros*. A macro is a piece of code that can be evaluated to a string.
+
+The only available data type is **String**. (However, you can encode other data types inside String)
+
+## Simple Start
+
+```bash
+# First clone this repo and open it
+
+cargo run ./examples/syn.meow
+
+# Now you can use the REPL to evaluate expressions
+```
+
+Examples:
+
+```
+no error found.
+> true()
+T
+> false()
+F
+> {var x = zero();succ(x)}
+S0
+> dr("a","aba","aba")
+aba
+> if("T","xsa","ddd")
+xsa
+> eq("as","asas")
+F
+```
+
+## Tutorials
+
+- [Syntax](./docs/Syntax.md)
+- [Encoding](./docs/Encoding.md)
+- [Double Replacement Lemma](./docs/DRL.md)
+
+## Examples
+
+See [syn.meow](./examples/syn.meow).
diff --git a/docs/DRL.md b/docs/DRL.md
@@ -0,0 +1,9 @@
+# Double Replacement Lemma
+
+$[x/y]([y/x]y)=\begin{cases}
+    y, x\subset y\\
+    x, \text{otherwise}
+\end{cases}$
+
+Similar result:
+$[x/yy]([yy/x]y)=y$
diff --git a/docs/Encoding.md b/docs/Encoding.md
@@ -0,0 +1,60 @@
+# Encoding
+
+Think about two problems:
+
+1. How to write a macro to decide whether two strings are equal?
+2. How to write a `if` macro to do the conditional execution? More specifically, write a macro `if(c,x,y)`, it returns `x` if `c` is true, and `y` if `c` is false (assume that `c` can either be true or false).
+
+First, we define true and false by:
+
+```meow
+true() {"T"}
+
+false() {"F"}
+```
+
+They are represented by string literals.
+
+To directly implement the `eq` macro is quite hard.
+
+We have to first implement the `encode` and `decode` macro to help us.
+
+## Encoding
+
+Encoding means to encode a string into another string that has some special properties that we can use.
+
+We define it by this:
+
+$$
+\mathtt{encode}(s) = \mathtt{"\_\^{\,}"} + (\mathtt{["\backslash \backslash"/"\backslash"]["\backslash \$"/"\$"]["\backslash \^{\,}"/"\^{\,}"]}s) + \mathtt{"\_\$"}
+$$
+
+We can prove the following results:
+
+1. $|x|=1 \land x \neq \mathtt{"\backslash"} \Rightarrow $ $x\mathtt{"\^{\,}"} \not\subset \mathtt{["\backslash \backslash"/"\backslash"]["\backslash \$"/"\$"]["\backslash \^{\,}"/"\^{\,}"]}s$, $x\mathtt{"\$"} \not\subset \mathtt{["\backslash \backslash"/"\backslash"]["\backslash \$"/"\$"]["\backslash \^{\,}"/"\^{\,}"]}s$
+
+## Code
+
+```meow
+encode(s) {
+    var rep = {
+        "\" = "\\";
+        "$" = "\$";
+        "^" = "\^";
+        s
+    };
+    "_^"+ rep +"_$"
+}
+
+decode(s) {
+    var rep = {
+        "_^" = "";
+        "_$" = "";
+        s
+    };
+    "\$" = "$";
+    "\^" = "^";
+    "\\" = "\";
+    rep
+}
+```
diff --git a/docs/String.md b/docs/String.md
diff --git a/docs/Syntax.md b/docs/Syntax.md
@@ -0,0 +1,85 @@
+# Syntax
+
+The layout of the whole program is not stable, but the core expression syntax is (relatively more) stable.
+
+## Expression
+
+```
+Expression ::=
+            | Expression "+" Term
+            | Term
+
+Term ::=
+      | Literal
+      | MacroApplication
+      | VarName
+      | "{" BlockExpression "}"
+      | "(" Expression ")"
+```
+
+**All expressions can be evaluated to a string literal.**
+
+`literal` is simply a string literal, like `"abc"`, `"lol"`.
+
+Examples.
+
+```meow
+meow1() {
+    "a" + "b"
+}
+
+meow2() {
+    "a" = "b";
+    "babaa"
+}
+```
+
+`meow1` takes no argument, and it simply returns a string literal `"ab"`.
+
+In `meow2`, we see that we have multiple "commands" in the curly bracket.
+The syntax is like Rust, the last expression (which has no ";" at the end) in the block is the return value of the block.
+
+`X;Y` means `let X in Y`, so `X;Y;Z` means `let X in (let Y in Z)`.
+
+Different to many languages, `X=Y` requires that both `X` and `Y` are **expressions** (which is basically strings).
+
+`X=Y;Z` means that `let X=Y in Z`, which is $[Y/X]Z$ (string replacement).
+
+The replacement **only** takes place in the `in xxx`. Hence, in `let X in (let Y in Z)`, the replacement of `X` only takes place in `Z` rather than `Y` (but there is a way to let it happen in `Y`, see later explanation).
+
+`MacroApplication` is a macro name followed by a list of arguments, like `succ(a,b,c)`. The language is *by value*, so the arguments are evaluated before the macro is applied.
+
+## Evaluation Mode
+
+Evaluation has two modes. The **raw** mode and the **eval** mode.
+
+In raw mode, a string literal will be simply be what it is. In eval mode, a string literal will be changed according to current rules in the context.
+
+For example, consider the following macro:
+
+```meow
+meow() {
+    "dd" = "d";
+    var x = {"dddd"};
+    var y = "dddd";
+    "x=" + x + ",y=" + y
+}
+```
+
+Here `y` is raw mode evaluation while `x` is an eval mode evaluation. The thumb rule is that **only the last expression** in the block ({}) will be evaluated in eval mode.
+
+Therefore, `x` is actually evaluated twice while `y` is evaluated only once.
+
+The output of the code above:
+
+```
+x=d,y=dd
+```
+
+## Variable
+
+You can use `var` to declare a variable. The syntax is like `var x = "abc";`. The variable is only visible in the block where it is declared. The right hand side can be any expressions. Note that the right hand side is evaluated in **raw** mode (unless you use `var x = {"abc"}`).
+
+---
+
+Til now, you may think that this language is very weak/useless. It turns out that it is really weak. But it can also do many interesting things.
diff --git a/src/prog.rs b/src/prog.rs
@@ -80,7 +80,7 @@ pub fn eval_raw(expr: &Box<Expr>, context: &Box<Context>) -> String {
             let args = macap
                 .args
                 .iter()
-                .map(|x| eval(x, context))
+                .map(|x| eval_raw(x, context))
                 .collect::<Vec<String>>();
             // add vars to the context
             for (result, name) in args.iter().zip(mac.args.iter()) {