diff --git a/Readme.md b/Readme.md index c5ce443..6dabf26 100755 --- 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 - -# 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 new file mode 100644 index 0000000..fa4b74d --- /dev/null +++ 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 new file mode 100644 index 0000000..a482278 --- /dev/null +++ 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 deleted file mode 100644 index 9b7133b..0000000 --- a/docs/String.md +++ /dev/null @@ -1,18 +0,0 @@ -# String Operation - -Definition of replacement: - -$[a/b]c := \begin{cases} - xa[a/b]y, \exist x, y,(b\not\subset x)\land (c=xby) \\ - c, \text{otherwise} -\end{cases}$ - -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/Syntax.md b/docs/Syntax.md new file mode 100644 index 0000000..a6c4c44 --- /dev/null +++ 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 index ec11b23..8238190 100644 --- a/src/prog.rs +++ b/src/prog.rs @@ -80,7 +80,7 @@ pub fn eval_raw(expr: &Box, context: &Box) -> String { let args = macap .args .iter() - .map(|x| eval(x, context)) + .map(|x| eval_raw(x, context)) .collect::>(); // add vars to the context for (result, name) in args.iter().zip(mac.args.iter()) {