churchrepl 1.0.2

使用：

当呼叫丘吉尔时，将打开新的REPL。

churchrepl [-f --file file [file ...]] [-v --verbose]

标志：

（可选）在加载普通repl之前从文件中读取定义和表达式。

-f|--file file [file ...]

（可选）打印调试和详细输出。

-v|--verbose

church repl文件结构：

ebnf语法如下*：

(* church-lambda EBNF *)
                  (* --- meta --- *)
 program = {line};
 line = (define | function);
 define = "@" alias ":" function;

                  (* --- lambdas --- *)
 function = lambda | application;
 lambda = "λ" variable "." expr;
 application = '(' expr  expr ')';
 expr = (lambda | application | variable | alias );

                  (* --- primitives --- *)
 variable = /[a-z]/;
 alias = /[_A-Z][_A-Z0-9]*/;

一个简单的示例程序：

@ID: λx.x
@APPLY: λf.λx.(f x)
@TRUE: λx.λy.x
@FALSE: λx.λy.y
@ZERO: λf.λx.x
@SUCC: λn.λf.λx.(f ((n f) x))
@ONE: (SUCC ZERO)
@TWO: (SUCC ONE)
@THREE: (SUCC TWO)
@FOUR: (SUCC THREE)
(SUCC ZERO)
(SUCC ONE)
(SUCC TWO)
(SUCC THREE)
(SUCC FOUR)

注：就本程序而言，λ（lambda，unicode u03bb）相当于反斜杠。 使用REPL时，使用反斜杠可能更容易。