text: /*
   * ATTENTION: The "eval" devtool has been used (maybe by default in mode: "development").
   * This devtool is neither made for production nor for readable output files.
   * It uses "eval()" calls to create a separate source file in the browser devtools.
   * If you are trying to read the output file, select a different devtool (https://webpack.js.org/configuration/devtool/)
   * or disable the default devtool with "devtool: false".
   * If you are looking for production-ready output files, see mode: "production" (https://webpack.js.org/configuration/mode/).
   */
  /******/ (() => { // webpackBootstrap
  /******/ 	"use strict";
  /******/ 	var __webpack_modules__ = ({
  
  /***/ "./js/deBrujin.js":
  /*!************************!*\
    !*** ./js/deBrujin.js ***!
    \************************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.deBrujinFreeVar = exports.deBrujinIndex = exports.deBrujinApplication = exports.deBrujinLambda = exports.deBrujinExpression = void 0;\nconst util_1 = __webpack_require__(/*! ./util */ \"./js/util.js\");\nconst error_1 = __webpack_require__(/*! ./error */ \"./js/error.js\");\nconst expression_1 = __webpack_require__(/*! ./expression */ \"./js/expression.js\");\nclass deBrujinExpression {\n    constructor(className) {\n        this.className = className;\n    }\n    toString() {\n        return this.getString(true);\n    }\n    static parse(str) {\n        let cs = str.split(\"\");\n        let left = null;\n        while (cs.length > 0) {\n            let t = cs.shift();\n            switch (t) {\n                case \"(\": {\n                    let count = 1;\n                    let content = \"\";\n                    while (true) {\n                        if (cs.length === 0)\n                            throw new error_1.LambdaParseError(\"Too many LPAREN '('\");\n                        let t1 = cs.shift();\n                        if (t1 === \"(\")\n                            count++;\n                        if (t1 === \")\")\n                            count--;\n                        if (count === 0)\n                            break;\n                        content += t1;\n                    }\n                    if (left === null)\n                        left = this.parse(content);\n                    else\n                        left = new deBrujinApplication(left, this.parse(content));\n                    break;\n                }\n                case \"\\\\\":\n                case \"\\u00a5\":\n                case \"λ\": {\n                    let ret = new deBrujinLambda(this.parse(cs.join(\"\")));\n                    if (left === null)\n                        return ret;\n                    else\n                        return new deBrujinApplication(left, ret);\n                }\n                case \" \":\n                    break;\n                default: {\n                    let ret;\n                    if (t.match(/^[0-9]$/) !== null) {\n                        let content = t;\n                        while (cs.length > 0) {\n                            if (cs[0].match(/^[0-9]$/) === null)\n                                break;\n                            content += cs.shift();\n                        }\n                        ret = new deBrujinIndex(parseInt(content));\n                    }\n                    else if (t.match(/^[a-zA-Z]$/) !== null) {\n                        let content = t;\n                        while (cs.length > 0) {\n                            if (cs[0].match(/^[a-zA-Z0-9]$/) === null)\n                                break;\n                            content += cs.shift();\n                        }\n                        ret = new deBrujinFreeVar(content);\n                    }\n                    else {\n                        throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n                    }\n                    if (left === null)\n                        left = ret;\n                    else\n                        left = new deBrujinApplication(left, ret);\n                }\n            }\n        }\n        if (left === null)\n            throw new error_1.LambdaParseError(\"No contents in Expression\");\n        return left;\n    }\n    toLambda() {\n        return this.getLambda(deBrujinFreeVar.toVariables(this.getFV()));\n    }\n}\nexports.deBrujinExpression = deBrujinExpression;\nclass deBrujinLambda extends deBrujinExpression {\n    constructor(expr) {\n        super(\"deBrujinLambda\");\n        this.expr = expr;\n    }\n    getString(noParens) {\n        return util_1.putParens(\"\\\\ \" + this.expr.getString(true), noParens);\n    }\n    getLambda(vars) {\n        let v = expression_1.Variable.getNew(vars);\n        vars.unshift(v);\n        let ret = this.expr.getLambda(vars);\n        vars.shift();\n        return new expression_1.LambdaAbstraction(v, ret);\n    }\n    getFV() {\n        return this.expr.getFV();\n    }\n}\nexports.deBrujinLambda = deBrujinLambda;\nclass deBrujinApplication extends deBrujinExpression {\n    constructor(left, right) {\n        super(\"deBrujinApplication\");\n        this.left = left;\n        this.right = right;\n    }\n    getString(noParens) {\n        return util_1.putParens(this.left.getString(this.left instanceof deBrujinApplication) +\n            \" \" +\n            this.right.getString(false), noParens);\n    }\n    getLambda(vars) {\n        return new expression_1.Application(this.left.getLambda(vars), this.right.getLambda(vars));\n    }\n    getFV() {\n        return this.left.getFV().concat(this.right.getFV());\n    }\n}\nexports.deBrujinApplication = deBrujinApplication;\nclass deBrujinIndex extends deBrujinExpression {\n    constructor(index) {\n        super(\"deBrujinIndex\");\n        this.index = index;\n    }\n    getString(noParens) {\n        return this.index.toString();\n    }\n    getLambda(vars) {\n        if (this.index < vars.length)\n            return vars[this.index];\n        else\n            throw new error_1.TranslateError(\"de Brujin Index must be less than # of ancestor lambdas.\");\n    }\n    getFV() {\n        return [];\n    }\n}\nexports.deBrujinIndex = deBrujinIndex;\nclass deBrujinFreeVar extends deBrujinExpression {\n    constructor(name) {\n        super(\"deBrujinFreeVar\");\n        this.name = name;\n    }\n    getString(noParens) {\n        return this.name;\n    }\n    getLambda(vars) {\n        if (this.name.length === 1)\n            return this.toVariable();\n        else\n            return expression_1.Macro.get(this.name, false);\n    }\n    toVariable() {\n        return new expression_1.Variable(this.name);\n    }\n    static toVariables(fvs) {\n        let ret = [];\n        for (let fv of fvs) {\n            ret.push(fv.toVariable());\n        }\n        return ret;\n    }\n    getFV() {\n        return [this];\n    }\n}\nexports.deBrujinFreeVar = deBrujinFreeVar;\n\n\n//# sourceURL=webpack://lambda-friends/./js/deBrujin.js?");
  
  /***/ }),
  
  /***/ "./js/error.js":
  /*!*********************!*\
    !*** ./js/error.js ***!
    \*********************/
  /***/ ((__unused_webpack_module, exports) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.TranslateError = exports.GraphParseError = exports.TexError = exports.TypeError = exports.MacroError = exports.ReductionError = exports.SubstitutionError = exports.LambdaParseError = exports.LambdaFriendsError = void 0;\n// 例外の抽象クラス\nclass LambdaFriendsError {\n    constructor(name, message) {\n        // if (typeof Error.captureStackTrace === \"function\"){\n        //   Error.captureStackTrace(this,this.constructor);\n        // }\n        if (message === undefined) {\n            this.name = \"LambdaFriendsError\";\n            this.message = name;\n        }\n        else {\n            this.name = name;\n            this.message = message;\n        }\n    }\n    toString() {\n        // return this.stack;\n        return this.name + \": \" + this.message;\n    }\n}\nexports.LambdaFriendsError = LambdaFriendsError;\n// Parse中の例外\nclass LambdaParseError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"LambdaParseError\", message);\n    }\n}\nexports.LambdaParseError = LambdaParseError;\n// Substitutionの例外\nclass SubstitutionError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"SubstitutionError\", message);\n    }\n}\nexports.SubstitutionError = SubstitutionError;\n// Reductionの例外\nclass ReductionError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"ReductionError\", message);\n    }\n}\nexports.ReductionError = ReductionError;\n// Macroの例外\nclass MacroError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"MacroError\", message);\n    }\n}\nexports.MacroError = MacroError;\n// Typeの例外\nclass TypeError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"TypeError\", message);\n    }\n}\nexports.TypeError = TypeError;\n// TexにParseする際の例外\nclass TexError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"TexError\", message);\n    }\n}\nexports.TexError = TexError;\n// GraphをParseする際の例外\nclass GraphParseError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"GraphParseError\", message);\n    }\n}\nexports.GraphParseError = GraphParseError;\n// 他言語との変換時のエラー\nclass TranslateError extends LambdaFriendsError {\n    constructor(message) {\n        super(\"TranslateError\", message);\n    }\n}\nexports.TranslateError = TranslateError;\n\n\n//# sourceURL=webpack://lambda-friends/./js/error.js?");
  
  /***/ }),
  
  /***/ "./js/expression.js":
  /*!**************************!*\
    !*** ./js/expression.js ***!
    \**************************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.Fix = exports.Case = exports.Let = exports.If = exports.List = exports.Application = exports.LambdaAbstraction = exports.Macro = exports.Nil = exports.ConstOp = exports.ConstBool = exports.ConstInt = exports.Const = exports.Variable = exports.Symbol = exports.Expression = void 0;\nconst type_1 = __webpack_require__(/*! ./type */ \"./js/type.js\");\nconst error_1 = __webpack_require__(/*! ./error */ \"./js/error.js\");\nconst lambda_friends_1 = __webpack_require__(/*! ./lambda-friends */ \"./js/lambda-friends.js\");\nconst redex_1 = __webpack_require__(/*! ./redex */ \"./js/redex.js\");\nconst Util = __webpack_require__(/*! ./util */ \"./js/util.js\");\nconst deBrujin_1 = __webpack_require__(/*! ./deBrujin */ \"./js/deBrujin.js\");\n// 型の連立方程式と証明木の組\nclass TypeResult {\n    constructor(eqs, proofTree) {\n        this.eqs = eqs;\n        this.proofTree = proofTree;\n    }\n}\n// ラムダ項（抽象クラス）\nclass Expression {\n    // type: Type;\n    constructor(className) {\n        this.className = className;\n    }\n    parseChurchNum() {\n        if (!(this instanceof LambdaAbstraction))\n            return null;\n        const f = this.boundvar;\n        let e = this.expr;\n        let n = 0;\n        if (!(e instanceof LambdaAbstraction))\n            return null;\n        const x = e.boundvar;\n        if (f.equals(x))\n            return null;\n        e = e.expr;\n        while (e instanceof Application) {\n            n++;\n            if (!e.left.equals(f))\n                return null;\n            e = e.right;\n        }\n        if (e.equals(x))\n            return n;\n        else\n            return null;\n    }\n    parseChurchBool() {\n        const t = new LambdaAbstraction(new Variable(\"x\"), new LambdaAbstraction(new Variable(\"y\"), new Variable(\"x\")));\n        const f = new LambdaAbstraction(new Variable(\"x\"), new LambdaAbstraction(new Variable(\"y\"), new Variable(\"y\")));\n        if (this.equalsAlpha(t))\n            return true;\n        else if (this.equalsAlpha(f))\n            return false;\n        else\n            return null;\n    }\n    toLMNtal() {\n        throw new error_1.TypeError(\"Expression '\" +\n            this +\n            \"' cannot be converted into LMNtal (untyped only).\");\n    }\n    toSKI() {\n        throw new error_1.TypeError(\"Expression '\" +\n            this +\n            \"' cannot be converted to SKI combinators (untyped only).\");\n    }\n    getDeBrujin(vars) {\n        throw new error_1.TypeError(\"Expression '\" +\n            this +\n            \"' cannot be converted to de Brujin indexes (untyped only).\");\n    }\n    toDeBrujin() {\n        return this.getDeBrujin([]);\n    }\n}\nexports.Expression = Expression;\n// 終端記号（未解析）\nclass Symbol extends Expression {\n    constructor(name, className) {\n        if (className === undefined)\n            super(\"Symbol\");\n        else\n            super(className);\n        this.name = name;\n    }\n    equals(expr) {\n        return (expr instanceof Symbol &&\n            expr.className === this.className &&\n            expr.name === this.name);\n    }\n    equalsAlpha(expr) {\n        return (expr instanceof Symbol &&\n            expr.className === this.className &&\n            expr.name === this.name);\n    }\n    toString(noParens) {\n        return this.name;\n    }\n    toTexString(noParens) {\n        throw new error_1.TexError(\"class Symbol does not have tex string\");\n    }\n    getFV() {\n        return this.freevars;\n    }\n    substitute(x, expr) {\n        throw new error_1.SubstitutionError(\"Undefined Substitution\");\n    }\n    getEquations(gamma, type, noParens) {\n        throw new error_1.TypeError(\"Undefined Type\");\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Symbols must not appear in parsed Expression\");\n    }\n    getTypedRedex(noParens) {\n        throw new error_1.ReductionError(\"Symbols must not appear in parsed Expression\");\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Symbols must not appear in parsed Expression\");\n    }\n    extractMacros() {\n        throw new error_1.ReductionError(\"Symbols must not appear in parsed Expression\");\n    }\n}\nexports.Symbol = Symbol;\n// 変数 x\nclass Variable extends Symbol {\n    constructor(name) {\n        super(name, \"Variable\");\n        this.freevars = [this];\n    }\n    substitute(x, expr) {\n        if (this.equals(x))\n            return expr;\n        else\n            return this;\n    }\n    getEquations(gamma, type, noParens) {\n        for (let g of gamma) {\n            if (g.equals(this)) {\n                // (var)\n                let str = \"\\\\AxiomC{}\\n\";\n                str += \"\\\\RightLabel{\\\\scriptsize(var)}\\n\";\n                str +=\n                    \"\\\\UnaryInfC{$\" +\n                        Variable.gammaToTexString(gamma) +\n                        \" \\\\vdash \" +\n                        this.name +\n                        \" : \" +\n                        type.toTexString() +\n                        \" $}\\n\";\n                return new TypeResult([new type_1.TypeEquation(g.type, type)], str);\n            }\n        }\n        throw new error_1.TypeError(\"free variable is not allowed: \" + this);\n    }\n    toTexString(noParens) {\n        return this.name;\n    }\n    static union(a, b, c) {\n        if (c === undefined) {\n            let ret = [];\n            for (let v of a) {\n                ret.push(v);\n            }\n            for (let v of Variable.dif(b, a)) {\n                ret.push(v);\n            }\n            return ret;\n        }\n        else {\n            return Variable.union(Variable.union(a, b), c);\n        }\n    }\n    static dif(a, b) {\n        let ret = [];\n        for (let ta of a) {\n            if (!Variable.contains(b, ta))\n                ret.push(ta);\n        }\n        return ret;\n    }\n    static contains(a, b) {\n        for (let ta of a) {\n            if (ta.equals(b)) {\n                return true;\n            }\n        }\n        return false;\n    }\n    static gammaToTexString(gamma) {\n        if (gamma.length === 0)\n            return \"\";\n        let ret = gamma[0].name + \" : \" + gamma[0].type.toTexString();\n        for (let i = 1; i < gamma.length; i++) {\n            ret += \",~\" + gamma[i].name + \" : \" + gamma[i].type.toTexString();\n        }\n        return ret;\n    }\n    static getNew(used) {\n        let alphabet = \"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ\".split(\"\");\n        for (let a of alphabet) {\n            let z = new Variable(a);\n            if (!Variable.contains(used, z)) {\n                return z;\n            }\n        }\n        throw new error_1.SubstitutionError(\"No more Variables available\");\n    }\n    getRedexes(etaAllowed, noParens) {\n        return [];\n    }\n    getTypedRedex(noParens) {\n        return null;\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        return null;\n    }\n    extractMacros() {\n        return this;\n    }\n    toLMNtal() {\n        return \"fv(\" + this.name + \")\";\n    }\n    toSKI() {\n        return this;\n    }\n    getDeBrujin(vars) {\n        for (let i = 0; i < vars.length; i++) {\n            if (vars[i].equals(this)) {\n                return new deBrujin_1.deBrujinIndex(i);\n            }\n        }\n        return new deBrujin_1.deBrujinFreeVar(this.name);\n    }\n}\nexports.Variable = Variable;\n// 定数 c\nclass Const extends Symbol {\n    constructor(name, className) {\n        super(name, className);\n        this.freevars = [];\n    }\n    substitute(x, expr) {\n        return this;\n    }\n    getEquations(gamma, type, noParens) {\n        // (con)\n        let str = \"\\\\AxiomC{}\\n\";\n        str += \"\\\\RightLabel{\\\\scriptsize(con)}\\n\";\n        str +=\n            \"\\\\UnaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult([new type_1.TypeEquation(this.type, type)], str);\n    }\n    toString(noParens) {\n        return \"[\" + this.name + \"]\";\n    }\n    toTexString(noParens) {\n        return this.name + \"^{\" + this.type.toTexString() + \"}\";\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getTypedRedex(noParens) {\n        return null;\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    extractMacros() {\n        return this;\n    }\n}\nexports.Const = Const;\n// int型定数 c^{int}\nclass ConstInt extends Const {\n    constructor(value) {\n        super(value.toString(), \"ConstInt\");\n        this.value = value;\n        this.type = new type_1.TypeInt();\n    }\n}\nexports.ConstInt = ConstInt;\n// bool型定数 c^{bool}\nclass ConstBool extends Const {\n    constructor(value) {\n        super(value.toString(), \"ConstBool\");\n        this.value = value;\n        this.type = new type_1.TypeBool();\n    }\n}\nexports.ConstBool = ConstBool;\n// 関数型定数 c^{op} （前置記法・2項演算）\nclass ConstOp extends Const {\n    constructor(funcName) {\n        super(funcName, \"ConstOp\");\n        switch (funcName) {\n            case \"+\":\n                this.value = (x, y) => new ConstInt(x.value + y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeInt()));\n                break;\n            case \"-\":\n                this.value = (x, y) => new ConstInt(x.value - y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeInt()));\n                break;\n            case \"*\":\n                this.value = (x, y) => new ConstInt(x.value * y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeInt()));\n                break;\n            case \"/\":\n                this.value = (x, y) => {\n                    if (y.value === 0)\n                        throw new error_1.ReductionError(\"Dividing by '0' is not allowed\");\n                    else\n                        return new ConstInt(Math.floor(x.value / y.value));\n                };\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeInt()));\n                break;\n            case \"%\":\n                this.value = (x, y) => {\n                    if (y.value === 0)\n                        throw new error_1.ReductionError(\"Dividing by '0' is not allowed\");\n                    else\n                        return new ConstInt(x.value - Math.floor(x.value / y.value) * 4);\n                };\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeInt()));\n                break;\n            case \"<\":\n                this.value = (x, y) => new ConstBool(x.value < y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \">\":\n                this.value = (x, y) => new ConstBool(x.value > y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \"<=\":\n                this.value = (x, y) => new ConstBool(x.value <= y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \">=\":\n                this.value = (x, y) => new ConstBool(x.value >= y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \"==\":\n                this.value = (x, y) => new ConstBool(x.value == y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \"=\":\n                this.value = (x, y) => new ConstBool(x.value == y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \"!=\":\n                this.value = (x, y) => new ConstBool(x.value != y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeFunc(new type_1.TypeInt(), new type_1.TypeBool()));\n                break;\n            case \"eq\":\n                this.value = (x, y) => new ConstBool(x.value == y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeBool()));\n                break;\n            case \"xor\":\n                this.value = (x, y) => new ConstBool(x.value != y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeBool()));\n                break;\n            case \"or\":\n                this.value = (x, y) => new ConstBool(x.value || y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeBool()));\n                break;\n            case \"and\":\n                this.value = (x, y) => new ConstBool(x.value && y.value);\n                this.type = new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeBool()));\n                break;\n            case \"nor\":\n                this.value = (x, y) => new ConstBool(!(x.value || y.value));\n                this.type = new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeBool()));\n                break;\n            case \"nand\":\n                this.value = (x, y) => new ConstBool(!(x.value && y.value));\n                this.type = new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeFunc(new type_1.TypeBool(), new type_1.TypeBool()));\n                break;\n            default:\n                throw new error_1.LambdaParseError(\"Undefined function: \" + funcName);\n        }\n    }\n}\nexports.ConstOp = ConstOp;\n// 空リスト nil\nclass Nil extends Symbol {\n    substitute(x, expr) {\n        return this;\n    }\n    constructor() {\n        super(\"nil\", \"Nil\");\n        this.freevars = [];\n    }\n    getEquations(gamma, type, noParens) {\n        // (nil)\n        let t = type_1.TypeVariable.getNew();\n        let nType = new type_1.TypeList(t);\n        let str = \"\\\\AxiomC{}\\n\";\n        str += \"\\\\RightLabel{\\\\scriptsize(nil)}\\n\";\n        str +=\n            \"\\\\UnaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.name +\n                \" : \" +\n                nType.toTexString() +\n                \" $}\\n\";\n        return new TypeResult([new type_1.TypeEquation(type, nType)], str);\n    }\n    toString(noParens) {\n        return \"[\" + this.name + \"]\";\n    }\n    toTexString(noParens) {\n        return \"{\\\\rm \" + this.name + \"}\";\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    extractMacros() {\n        return this;\n    }\n}\nexports.Nil = Nil;\n// マクロ定義\nclass Macro extends Symbol {\n    constructor(name, expr, typed, type) {\n        super(name, \"Macro\");\n        this.freevars = [];\n        this.expr = expr;\n        this.typed = typed;\n        this.type = type;\n    }\n    static add(name, lf, typed) {\n        let expr = lf.expr;\n        if (!/^[a-zA-Z0-9!?]+$/.test(name)) {\n            throw new error_1.MacroError(\"<\" +\n                name +\n                \"> cannot be used as a name of macro. Available characters: [a-zA-Z0-9!?]\");\n        }\n        if (name.match(/^\\d+$/) !== null) {\n            throw new error_1.MacroError(\"<\" + name + \"> is already defined as a built-in macro.\");\n        }\n        const builtins = [\"true\", \"false\", \"S\", \"K\", \"I\"];\n        for (let b of builtins) {\n            if (b === name) {\n                throw new error_1.MacroError(\"<\" + name + \"> is already defined as a built-in macro.\");\n            }\n        }\n        let map = typed ? Macro.map : Macro.mapUntyped;\n        if (expr.getFV().length !== 0) {\n            throw new error_1.MacroError(\"<\" + name + \"> contains free variables: \" + expr.getFV());\n        }\n        let m = new Macro(name, expr, typed, lf.type);\n        map[name] = m;\n        return map[name];\n    }\n    static clear(typed) {\n        if (typed) {\n            Macro.map = {};\n        }\n        else {\n            Macro.mapUntyped = {};\n        }\n    }\n    static get(name, typed) {\n        let ret;\n        if (typed) {\n            ret = Macro.map[name];\n        }\n        else {\n            ret = Macro.mapUntyped[name];\n        }\n        if (ret === undefined) {\n            // 組み込みマクロ。typeがundefでいいかは疑問の余地あり\n            let f = (term) => new Macro(name, Util.makeAST(term, typed), typed, undefined);\n            if (name.match(/^\\d+$/) !== null)\n                return f(Util.makeChurchNum(parseInt(name)));\n            if (name === \"true\")\n                return f(\"\\\\xy.x\");\n            if (name === \"false\")\n                return f(\"\\\\xy.y\");\n            if (name === \"S\")\n                return f(\"\\\\fgx.fx(gx)\");\n            if (name === \"K\")\n                return f(\"\\\\xy.x\");\n            if (name === \"I\")\n                return f(\"\\\\x.x\");\n            // 発展の余地あり。typeを指定したundefマクロを許す？\n            return new Macro(name, undefined, typed, undefined);\n        }\n        else {\n            return new Macro(name, ret.expr, typed, ret.type);\n        }\n    }\n    static getMap(typed) {\n        return Object.assign({}, typed ? Macro.map : Macro.mapUntyped);\n    }\n    substitute(x, expr) {\n        return this;\n    }\n    toString(noParens) {\n        return \"<\" + this.name + \">\";\n    }\n    equalsAlpha(expr) {\n        // 再検討の余地あり\n        if (this.expr === undefined)\n            return this.equals(expr);\n        else\n            return this.expr.equalsAlpha(expr);\n    }\n    getEquations(gamma, type, noParens) {\n        // ????\n        if (this.expr === undefined)\n            throw new error_1.TypeError(this + \" is undefined.\");\n        else\n            return this.expr.getEquations(gamma, type, noParens);\n    }\n    toTexString(noParens) {\n        return \"\\\\,\\\\overline{\\\\bf \" + this.name + \"}\\\\,\";\n    }\n    getRedexes(etaAllowed, noParens) {\n        // let next = Macro.get(this.name,false);\n        // if (next.expr === undefined) return [];\n        // else return [new MacroRedex(next)];\n        if (this.expr === undefined)\n            return [];\n        else\n            return [new redex_1.MacroRedex(this)];\n    }\n    getTypedRedex(noParens) {\n        if (this.expr === undefined)\n            return null;\n        else\n            return new redex_1.MacroRedex(this);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        if (this.expr === undefined)\n            return null;\n        else\n            return new redex_1.MacroRedex(this);\n    }\n    extractMacros() {\n        if (this.expr === undefined)\n            return this;\n        else\n            return this.expr.extractMacros();\n    }\n    toLMNtal() {\n        if (this.expr === undefined)\n            return \"fv(\" + this.name + \")\";\n        else\n            return this.expr.toLMNtal();\n    }\n    toSKI() {\n        if (this.expr === undefined)\n            return this;\n        switch (this.name) {\n            case \"S\":\n            case \"K\":\n            case \"I\":\n                return this;\n            default:\n                return this.expr.toSKI();\n        }\n    }\n    getDeBrujin(vars) {\n        if (this.expr === undefined)\n            return new deBrujin_1.deBrujinFreeVar(this.name);\n        else\n            return this.expr.getDeBrujin(vars);\n    }\n}\nexports.Macro = Macro;\nMacro.map = {};\nMacro.mapUntyped = {};\n// ラムダ抽象 \\x.M\nclass LambdaAbstraction extends Expression {\n    constructor(boundvar, expr) {\n        super(\"LambdaAbstraction\");\n        this.freevars = undefined;\n        this.boundvar = boundvar;\n        this.expr = expr;\n    }\n    static parse(tokens, typed) {\n        let boundvars = [];\n        while (tokens.length > 0) {\n            let t = tokens.shift();\n            if (t.name === \".\") {\n                if (boundvars.length === 0)\n                    throw new error_1.LambdaParseError(\"Bound variables are expected.\");\n                let expr = Util.parseSymbols(tokens, typed);\n                while (boundvars.length > 0) {\n                    expr = new LambdaAbstraction(boundvars.pop(), expr);\n                }\n                return expr;\n            }\n            else if (t.name.match(/^[A-Za-z]$/) === null) {\n                throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n            }\n            else {\n                boundvars.push(new Variable(t.name));\n            }\n        }\n        throw new error_1.LambdaParseError(\"'.' is needed\");\n    }\n    toString(noParens) {\n        let boundvars = [this.boundvar];\n        let expr = this.expr;\n        while (expr instanceof LambdaAbstraction) {\n            boundvars.push(expr.boundvar);\n            expr = expr.expr;\n        }\n        let str = \"\\\\\" + boundvars.join(\"\") + \".\" + expr.toString(true);\n        if (!noParens)\n            str = \"(\" + str + \")\";\n        return str;\n    }\n    getFV() {\n        if (this.freevars !== undefined)\n            return this.freevars;\n        this.freevars = [];\n        return (this.freevars = Variable.dif(this.expr.getFV(), [this.boundvar]));\n    }\n    substitute(y, expr) {\n        if (this.boundvar.equals(y)) {\n            return this;\n        }\n        else if (!Variable.contains(expr.getFV(), this.boundvar)) {\n            return new LambdaAbstraction(this.boundvar, this.expr.substitute(y, expr));\n        }\n        else {\n            let uniFV = Variable.union(this.expr.getFV(), expr.getFV());\n            let z = Variable.getNew(uniFV);\n            return new LambdaAbstraction(z, this.expr.substitute(this.boundvar, z)).substitute(y, expr);\n        }\n    }\n    equals(expr) {\n        return (expr instanceof LambdaAbstraction &&\n            expr.boundvar.equals(this.boundvar) &&\n            expr.expr.equals(this.expr));\n    }\n    equalsAlpha(expr) {\n        if (!(expr instanceof LambdaAbstraction))\n            return false;\n        if (this.equals(expr))\n            return true;\n        let x = this.boundvar;\n        let m = this.expr;\n        let y = expr.boundvar;\n        let n = expr.expr;\n        let v = Variable.getNew(Variable.union(m.getFV(), n.getFV()));\n        return m.substitute(x, v).equalsAlpha(n.substitute(y, v));\n        // if (Variable.contains(m.getFV(),y)){\n        //   return n.equalsAlpha(m);\n        // } else {\n        //   return n.equalsAlpha(m.substitute(x,y));\n        // }\n    }\n    getEquations(gamma, type, noParens) {\n        // (abs)\n        let t0 = type_1.TypeVariable.getNew();\n        let t1 = type_1.TypeVariable.getNew();\n        this.boundvar.type = t1;\n        let next = this.expr.getEquations(gamma.concat(this.boundvar), t0, true);\n        let str = next.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(abs)}\\n\";\n        str +=\n            \"\\\\UnaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(next.eqs.concat(new type_1.TypeEquation(type, new type_1.TypeFunc(t1, t0))), str);\n    }\n    toTexString(noParens) {\n        let boundvars = [this.boundvar.toTexString(false)];\n        let expr = this.expr;\n        while (expr instanceof LambdaAbstraction) {\n            boundvars.push(expr.boundvar.toTexString(false));\n            expr = expr.expr;\n        }\n        let str = \"\\\\lambda \" + boundvars.join(\"\") + \".\" + expr.toTexString(true);\n        if (!noParens)\n            str = \"(\" + str + \")\";\n        return str;\n    }\n    isEtaRedex() {\n        return (this.expr instanceof Application &&\n            this.expr.right.equals(this.boundvar) &&\n            !Variable.contains(this.expr.left.getFV(), this.boundvar));\n    }\n    getRedexes(etaAllowed, noParens) {\n        let lParen = \"\", rParen = \"\";\n        if (!noParens) {\n            lParen = \"(\";\n            rParen = \")\";\n        }\n        let boundvars = [];\n        let la = this;\n        while (la.expr instanceof LambdaAbstraction) {\n            boundvars.push(la.boundvar);\n            la = la.expr;\n        }\n        if (etaAllowed === undefined) {\n            console.error(\"etaAllowed is undefined.\");\n            etaAllowed = false;\n        }\n        let eta = null;\n        if (etaAllowed && la.isEtaRedex()) {\n            eta = new redex_1.EtaRedex(la);\n            eta.next = ((prev) => {\n                let bvs = [].concat(boundvars);\n                let ret = prev;\n                while (bvs.length > 0) {\n                    let t = bvs.pop();\n                    ret = new LambdaAbstraction(t, ret);\n                }\n                return ret;\n            })(eta.next);\n            eta.addLeft(lParen + (boundvars.length > 0 ? \"\\\\\" + boundvars.join(\"\") + \".\" : \"\"));\n            eta.addRight(rParen);\n            eta.addTexLeft(lParen +\n                (boundvars.length > 0 ? \"\\\\lambda{\" + boundvars.join(\"\") + \"}.\" : \"\"));\n            eta.addTexRight(rParen);\n        }\n        let expr = la.expr;\n        boundvars.push(la.boundvar);\n        let ret = redex_1.Redex.makeNext(expr.getRedexes(etaAllowed, true), lParen + (boundvars.length > 0 ? \"\\\\\" + boundvars.join(\"\") + \".\" : \"\"), rParen, lParen +\n            (boundvars.length > 0 ? \"\\\\lambda{\" + boundvars.join(\"\") + \"}.\" : \"\"), rParen, (prev) => {\n            let bvs = [].concat(boundvars);\n            let ret = prev;\n            while (bvs.length > 0) {\n                let t = bvs.pop();\n                ret = new LambdaAbstraction(t, ret);\n            }\n            return ret;\n        });\n        if (eta !== null)\n            ret.push(eta);\n        return ret;\n    }\n    getTypedRedex(noParens) {\n        return null;\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        if (etaAllowed === undefined) {\n            console.error(\"etaAllowed is undefined.\");\n            etaAllowed = false;\n        }\n        // this is eta-redex\n        if (weak) {\n            if (etaAllowed && this.isEtaRedex()) {\n                return new redex_1.EtaRedex(this);\n            }\n            else {\n                return null;\n            }\n        }\n        let boundvars = [];\n        let la = this;\n        while (la.expr instanceof LambdaAbstraction) {\n            boundvars.push(la.boundvar);\n            la = la.expr;\n        }\n        let lParen = \"\", rParen = \"\";\n        if (!noParens) {\n            lParen = \"(\";\n            rParen = \")\";\n        }\n        // la is eta-redex\n        let outerRedex = null;\n        if (etaAllowed && la.isEtaRedex()) {\n            outerRedex = new redex_1.EtaRedex(la);\n        }\n        // console.log(`outer:${outerRedex}`);\n        let innerRedex = null;\n        if (!outerRedex || innermost) {\n            let expr = la.expr;\n            // inner-redex\n            innerRedex = expr.getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, true);\n            // console.log(`inner:${innerRedex}`);\n            if (innerRedex === null)\n                return outerRedex;\n        }\n        let ret = null;\n        if (innerRedex && (innermost || !outerRedex)) {\n            ret = innerRedex;\n            boundvars.push(la.boundvar);\n        }\n        else if (outerRedex) {\n            ret = outerRedex;\n        } // else { ret = null; }\n        if (ret === null)\n            return null;\n        ret.next = ((prev) => {\n            let bvs = [].concat(boundvars);\n            let ret = prev;\n            while (bvs.length > 0) {\n                let t = bvs.pop();\n                ret = new LambdaAbstraction(t, ret);\n            }\n            return ret;\n        })(ret.next);\n        ret.addLeft(lParen + (boundvars.length > 0 ? \"\\\\\" + boundvars.join(\"\") + \".\" : \"\"));\n        ret.addRight(rParen);\n        ret.addTexLeft(lParen +\n            (boundvars.length > 0 ? \"\\\\lambda{\" + boundvars.join(\"\") + \"}.\" : \"\"));\n        ret.addTexRight(rParen);\n        return ret;\n    }\n    extractMacros() {\n        return new LambdaAbstraction(this.boundvar, this.expr.extractMacros());\n    }\n    toLMNtal() {\n        let ret = this.expr.toLMNtal().split(\"fv(\" + this.boundvar.name + \")\");\n        let str = ret[0];\n        let links = [];\n        for (let i = 1; i < ret.length; i++) {\n            let r = lambda_friends_1.LambdaFriends.getNewLink();\n            links.push(r);\n            str += r + ret[i];\n        }\n        function connect(links) {\n            switch (links.length) {\n                case 0:\n                    return \"rm\";\n                case 1:\n                    return links[0];\n                case 2:\n                    return \"cp(\" + links[0] + \",\" + links[1] + \")\";\n                default: {\n                    let r = links.shift();\n                    return \"cp(\" + r + \",\" + connect(links) + \")\";\n                }\n            }\n        }\n        return \"lambda(\" + connect(links) + \",\" + str + \")\";\n    }\n    toSKI() {\n        if (!Variable.contains(this.expr.getFV(), this.boundvar)) {\n            return new Application(Macro.get(\"K\", false), this.expr.toSKI());\n        }\n        if (this.boundvar.equals(this.expr)) {\n            return Macro.get(\"I\", false);\n        }\n        if (this.expr instanceof Application) {\n            let f = (e) => new LambdaAbstraction(this.boundvar, e).toSKI();\n            return new Application(new Application(Macro.get(\"S\", false), f(this.expr.left)), f(this.expr.right));\n        }\n        if (this.expr instanceof LambdaAbstraction) {\n            let inner = this.expr.toSKI();\n            return new LambdaAbstraction(this.boundvar, inner).toSKI();\n        }\n        throw new error_1.TranslateError(\"Unknown kind of expression.\");\n    }\n    getDeBrujin(vars) {\n        vars.unshift(this.boundvar);\n        let ret = this.expr.getDeBrujin(vars);\n        vars.shift();\n        return new deBrujin_1.deBrujinLambda(ret);\n    }\n}\nexports.LambdaAbstraction = LambdaAbstraction;\n// 関数適用 MN\nclass Application extends Expression {\n    constructor(left, right) {\n        super(\"Application\");\n        this.left = left;\n        this.right = right;\n    }\n    isBetaRedex() {\n        return this.left instanceof LambdaAbstraction;\n    }\n    toString(noParens) {\n        let str = this.left.toString(this.left instanceof Application) +\n            this.right.toString(false);\n        if (!noParens)\n            str = \"(\" + str + \")\";\n        return str;\n    }\n    getFV() {\n        if (this.freevars === undefined)\n            return (this.freevars = Variable.union(this.left.getFV(), this.right.getFV()));\n        else\n            return this.freevars;\n    }\n    substitute(y, expr) {\n        return new Application(this.left.substitute(y, expr), this.right.substitute(y, expr));\n    }\n    equals(expr) {\n        return (expr instanceof Application &&\n            expr.left.equals(this.left) &&\n            expr.right.equals(this.right));\n    }\n    equalsAlpha(expr) {\n        return (expr instanceof Application &&\n            expr.left.equalsAlpha(this.left) &&\n            expr.right.equalsAlpha(this.right));\n    }\n    getEquations(gamma, type, noParens) {\n        // (app)\n        let t1 = type_1.TypeVariable.getNew();\n        let nextL = this.left.getEquations(gamma, new type_1.TypeFunc(t1, type), false);\n        let nextR = this.right.getEquations(gamma, t1, false);\n        let str = nextL.proofTree + nextR.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(app)}\\n\";\n        str +=\n            \"\\\\BinaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(nextL.eqs.concat(nextR.eqs), str);\n    }\n    toTexString(noParens) {\n        let str = this.left.toTexString(this.left instanceof Application) +\n            this.right.toTexString(false);\n        if (!noParens)\n            str = \"(\" + str + \")\";\n        return str;\n    }\n    getRedexes(etaAllowed, noParens) {\n        let b = this.left instanceof Application;\n        let leftRedexes = this.left.getRedexes(etaAllowed, b);\n        let left = redex_1.Redex.makeNext(leftRedexes, \"\", this.right.toString(false), \"\", this.right.toTexString(false), (prev) => new Application(prev, this.right));\n        let rightRedexes = this.right.getRedexes(etaAllowed, false);\n        let right = redex_1.Redex.makeNext(rightRedexes, this.left.toString(b), \"\", this.left.toTexString(b), \"\", (prev) => new Application(this.left, prev));\n        let ret = left.concat(right);\n        if (this.isBetaRedex()) {\n            ret.push(new redex_1.BetaRedex(this));\n        }\n        if (!noParens) {\n            ret = redex_1.Redex.makeNext(ret, \"(\", \")\", \"(\", \")\", (prev) => prev);\n        }\n        return ret;\n    }\n    getTypedRedex(noParens) {\n        // typed\n        let lParen = noParens ? \"\" : \"(\";\n        let rParen = noParens ? \"\" : \")\";\n        if (this.left instanceof LambdaAbstraction) {\n            // (app2)\n            return new redex_1.TypedRedex(this, this.left.expr.substitute(this.left.boundvar, this.right), \"app2\");\n        }\n        else if (this.left instanceof Application &&\n            this.left.left instanceof ConstOp &&\n            this.left.right instanceof Const) {\n            let op = this.left.left;\n            let left = this.left.right;\n            let right = this.right;\n            if (right instanceof Const) {\n                // (app5)\n                if (op.type.left.equals(left.type) &&\n                    op.type.right instanceof type_1.TypeFunc &&\n                    op.type.right.left.equals(right.type)) {\n                    return new redex_1.TypedRedex(this, op.value(left, right), \"app5\");\n                }\n                else {\n                    throw new error_1.ReductionError(op.type +\n                        \" cannot handle \" +\n                        left.type +\n                        \" and \" +\n                        right.type +\n                        \" as arguments\");\n                }\n            }\n            else {\n                // (app4)\n                let ret = right.getTypedRedex(false);\n                if (ret === null)\n                    return null;\n                ret.next = new Application(new Application(op, left), ret.next);\n                ret.addLeft(lParen + op.toString(false) + left.toString(false));\n                ret.addRight(rParen);\n                ret.addTexLeft(lParen + op.toTexString(false) + left.toTexString(false));\n                ret.addTexRight(rParen);\n                return ret;\n            }\n        }\n        else if (this.left instanceof ConstOp) {\n            // (app3)\n            let ret = this.right.getTypedRedex(false);\n            if (ret === null)\n                return null;\n            ret.next = new Application(this.left, ret.next);\n            ret.addLeft(lParen + this.left.toString(false));\n            ret.addRight(rParen);\n            ret.addTexLeft(lParen + this.left.toTexString(false));\n            ret.addTexRight(rParen);\n            return ret;\n        }\n        else {\n            // (app1)\n            let ret = this.left.getTypedRedex(false);\n            if (ret === null)\n                return null;\n            ret.next = new Application(ret.next, this.right);\n            ret.addLeft(lParen);\n            ret.addRight(rParen + this.right.toString(false));\n            ret.addTexLeft(lParen);\n            ret.addTexRight(rParen + this.right.toTexString(false));\n            return ret;\n        }\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        const b = this.left instanceof Application;\n        const p = (r) => {\n            if (r !== null && !noParens) {\n                r.addLeft(\"(\");\n                r.addRight(\")\");\n                r.addTexLeft(\"(\");\n                r.addTexRight(\")\");\n            }\n            return r;\n        };\n        const searchL = () => {\n            let ret = this.left.getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, b);\n            if (ret === null)\n                return null;\n            ret.next = new Application(ret.next, this.right);\n            ret.addRight(this.right.toString(false));\n            ret.addTexRight(this.right.toTexString(false));\n            return p(ret);\n        };\n        const searchR = () => {\n            let ret = this.right.getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, false);\n            if (ret === null)\n                return null;\n            ret.next = new Application(this.left, ret.next);\n            ret.addLeft(this.left.toString(b));\n            ret.addTexLeft(this.left.toTexString(b));\n            return p(ret);\n        };\n        let ret = null;\n        if (this.isBetaRedex()) {\n            ret = p(new redex_1.BetaRedex(this));\n            if (head || !innermost)\n                return ret;\n        }\n        if (head) {\n            return searchL();\n        }\n        let res = rightmost ? searchR() : searchL();\n        if (res !== null)\n            return res;\n        res = rightmost ? searchL() : searchR();\n        if (res !== null)\n            return res;\n        return ret;\n    }\n    extractMacros() {\n        return new Application(this.left.extractMacros(), this.right.extractMacros());\n    }\n    toLMNtal() {\n        return \"apply(\" + this.left.toLMNtal() + \",\" + this.right.toLMNtal() + \")\";\n    }\n    toSKI() {\n        return new Application(this.left.toSKI(), this.right.toSKI());\n    }\n    getDeBrujin(vars) {\n        return new deBrujin_1.deBrujinApplication(this.left.getDeBrujin(vars), this.right.getDeBrujin(vars));\n    }\n}\nexports.Application = Application;\n// リスト M::M\nclass List extends Expression {\n    constructor(head, tail) {\n        super(\"List\");\n        this.head = head;\n        this.tail = tail;\n    }\n    toString(noParens) {\n        let ret = this.head.toString(false) + \"::\" + this.tail.toString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    getFV() {\n        if (this.freevars === undefined)\n            return (this.freevars = Variable.union(this.head.getFV(), this.tail.getFV()));\n        else\n            return this.freevars;\n    }\n    substitute(y, expr) {\n        return new List(this.head.substitute(y, expr), this.tail.substitute(y, expr));\n    }\n    equals(expr) {\n        return (expr instanceof List &&\n            expr.head.equals(this.head) &&\n            expr.tail.equals(this.tail));\n    }\n    equalsAlpha(expr) {\n        return (expr instanceof List &&\n            expr.head.equalsAlpha(this.head) &&\n            expr.tail.equalsAlpha(this.tail));\n    }\n    getEquations(gamma, type, noParens) {\n        // (list) 再検討の余地あり？ 新しい型変数要る？\n        let t = type_1.TypeVariable.getNew();\n        let lt = new type_1.TypeList(t);\n        let nextH = this.head.getEquations(gamma, t, false);\n        let nextT = this.tail.getEquations(gamma, lt, false);\n        let str = nextH.proofTree + nextT.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(list)}\\n\";\n        str +=\n            \"\\\\BinaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                lt.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(nextH.eqs.concat(nextT.eqs, new type_1.TypeEquation(lt, type)), str);\n    }\n    toTexString(noParens) {\n        let ret = this.head.toTexString(false) + \"::\" + this.tail.toTexString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getTypedRedex(noParens) {\n        return null;\n    }\n    extractMacros() {\n        return new List(this.head.extractMacros(), this.tail.extractMacros());\n    }\n}\nexports.List = List;\n// if\nclass If extends Expression {\n    constructor(state, ifTrue, ifFalse) {\n        super(\"If\");\n        this.state = state;\n        this.ifTrue = ifTrue;\n        this.ifFalse = ifFalse;\n    }\n    getFV() {\n        return (this.freevars = Variable.union(this.state.getFV(), this.ifTrue.getFV(), this.ifFalse.getFV()));\n    }\n    toString(noParens) {\n        let ret = \"[if]\" +\n            this.state.toString(true) +\n            \"[then]\" +\n            this.ifTrue.toString(true) +\n            \"[else]\" +\n            this.ifFalse.toString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    substitute(y, expr) {\n        return new If(this.state.substitute(y, expr), this.ifTrue.substitute(y, expr), this.ifFalse.substitute(y, expr));\n    }\n    equals(expr) {\n        return (expr instanceof If &&\n            expr.state.equals(this.state) &&\n            expr.ifTrue.equals(this.ifTrue) &&\n            expr.ifFalse.equals(this.ifFalse));\n    }\n    equalsAlpha(expr) {\n        return (expr instanceof If &&\n            expr.state.equalsAlpha(this.state) &&\n            expr.ifTrue.equalsAlpha(this.ifTrue) &&\n            expr.ifFalse.equalsAlpha(this.ifFalse));\n    }\n    getEquations(gamma, type, noParens) {\n        // (if)\n        let nextS = this.state.getEquations(gamma, new type_1.TypeBool(), true);\n        let nextT = this.ifTrue.getEquations(gamma, type, true);\n        let nextF = this.ifFalse.getEquations(gamma, type, true);\n        let str = nextS.proofTree + nextT.proofTree + nextF.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(if)}\\n\";\n        str +=\n            \"\\\\TrinaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(nextS.eqs.concat(nextT.eqs, nextF.eqs), str);\n    }\n    toTexString(noParens) {\n        let ret = \"{\\\\bf if}~\" +\n            this.state.toTexString(true) +\n            \"~{\\\\bf then}~\" +\n            this.ifTrue.toTexString(true) +\n            \"~{\\\\bf else}~\" +\n            this.ifFalse.toTexString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getTypedRedex(noParens) {\n        if (this.state instanceof ConstBool) {\n            if (this.state.value) {\n                // (if2)\n                return new redex_1.TypedRedex(this, this.ifTrue, \"if2\");\n            }\n            else {\n                // (if3)\n                return new redex_1.TypedRedex(this, this.ifFalse, \"if3\");\n            }\n        }\n        else {\n            // (if1)\n            let ret = this.state.getTypedRedex(false);\n            if (ret === null)\n                return null;\n            ret.next = new If(ret.next, this.ifTrue, this.ifFalse);\n            ret.addLeft(\"([if]\");\n            ret.addRight(\"[then]\" +\n                this.ifTrue.toString(true) +\n                \"[else]\" +\n                this.ifFalse.toString(true) +\n                \")\");\n            ret.addTexLeft(\"({\\\\bf if}~\");\n            ret.addTexRight(\"~{\\\\bf then}~\" +\n                this.ifTrue.toTexString(true) +\n                \"~{\\\\bf else}~\" +\n                this.ifFalse.toTexString(true) +\n                \")\");\n            return ret;\n        }\n    }\n    static parse(tokens, typed) {\n        let state = [];\n        let i_num = 0, t_num = 0, e_num = 0;\n        while (true) {\n            if (tokens.length == 0)\n                throw new error_1.LambdaParseError(\"Illegal If statement\");\n            let t = tokens.shift();\n            switch (t.name) {\n                case \"if\":\n                    i_num++;\n                    break;\n                case \"then\":\n                    t_num++;\n                    break;\n                case \"else\":\n                    e_num++;\n                    break;\n            }\n            if (i_num === e_num && t_num === i_num + 1)\n                break;\n            state.push(t);\n        }\n        let stateExpr = Util.parseSymbols(state, typed);\n        let ifTrue = [];\n        (i_num = 0), (t_num = 0), (e_num = 0);\n        while (true) {\n            if (tokens.length == 0)\n                throw new error_1.LambdaParseError(\"Illegal If statement\");\n            let t = tokens.shift();\n            switch (t.name) {\n                case \"if\":\n                    i_num++;\n                    break;\n                case \"then\":\n                    t_num++;\n                    break;\n                case \"else\":\n                    e_num++;\n                    break;\n            }\n            if (i_num === t_num && e_num === i_num + 1)\n                break;\n            ifTrue.push(t);\n        }\n        let ifTrueExpr = Util.parseSymbols(ifTrue, typed);\n        let ifFalseExpr = Util.parseSymbols(tokens, typed);\n        return new If(stateExpr, ifTrueExpr, ifFalseExpr);\n    }\n    extractMacros() {\n        return new If(this.state.extractMacros(), this.ifTrue.extractMacros(), this.ifFalse.extractMacros());\n    }\n}\nexports.If = If;\n// let in\nclass Let extends Expression {\n    constructor(boundvar, left, right) {\n        super(\"Let\");\n        this.boundvar = boundvar;\n        this.left = left;\n        this.right = right;\n    }\n    getFV() {\n        if (this.freevars !== undefined)\n            return this.freevars;\n        let ret = [];\n        for (let fv of this.right.getFV()) {\n            if (!fv.equals(this.boundvar)) {\n                ret.push(fv);\n            }\n        }\n        return (this.freevars = Variable.union(ret, this.left.getFV()));\n    }\n    toString(noParens) {\n        let ret = \"[let]\" +\n            this.boundvar.toString(true) +\n            \"=\" +\n            this.left.toString(true) +\n            \"[in]\" +\n            this.right.toString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    substitute(y, expr) {\n        let left = this.left.substitute(y, expr);\n        if (this.boundvar.equals(y)) {\n            return new Let(this.boundvar, left, this.right);\n        }\n        else if (!Variable.contains(expr.getFV(), this.boundvar)) {\n            return new Let(this.boundvar, left, this.right.substitute(y, expr));\n        }\n        else {\n            let uniFV = Variable.union(this.right.getFV(), expr.getFV());\n            let z = Variable.getNew(uniFV);\n            if (z.equals(y)) {\n                return new Let(z, left, this.right.substitute(this.boundvar, z));\n            }\n            else {\n                return new Let(z, left, this.right.substitute(this.boundvar, z).substitute(y, expr));\n            }\n        }\n    }\n    equals(expr) {\n        return (expr instanceof Let &&\n            expr.boundvar.equals(this.boundvar) &&\n            expr.left.equals(this.left) &&\n            expr.right.equals(this.right));\n    }\n    equalsAlpha(expr) {\n        if (!(expr instanceof Let))\n            return false;\n        if (this.equals(expr))\n            return true;\n        let x = this.boundvar;\n        let m = this.right;\n        let y = expr.boundvar;\n        let n = expr.right;\n        return (!Variable.contains(m.getFV(), y) && n.equalsAlpha(m.substitute(x, y)));\n    }\n    getEquations(gamma, type, noParens) {\n        // (let)\n        let t1 = type_1.TypeVariable.getNew();\n        this.boundvar.type = t1;\n        let nextL = this.left.getEquations(gamma, t1, true);\n        let nextR = this.right.getEquations(gamma.concat(this.boundvar), type, true);\n        let str = nextL.proofTree + nextR.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(let)}\\n\";\n        str +=\n            \"\\\\TrinaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(nextL.eqs.concat(nextR.eqs), str);\n    }\n    toTexString(noParens) {\n        let ret = \"{\\\\bf let}~\" +\n            this.boundvar.toTexString(false) +\n            \" = \" +\n            this.left.toTexString(true) +\n            \"~{\\\\bf in}~\" +\n            this.right.toTexString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getTypedRedex(noParens) {\n        // (let)\n        return new redex_1.TypedRedex(this, this.right.substitute(this.boundvar, this.left), \"let\");\n    }\n    static parse(tokens, typed) {\n        let t = tokens.shift();\n        if (t.name.match(/^[A-Za-z]$/) === null)\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        let boundvar = new Variable(t.name);\n        if (tokens.shift().name !== \"=\")\n            throw new error_1.LambdaParseError(\"'=' is expected\");\n        let content = [];\n        let i = 1;\n        while (true) {\n            // console.log(i);\n            if (tokens.length == 0)\n                throw new error_1.LambdaParseError(\"Illegal Let statement\");\n            let t = tokens.shift();\n            if (t.name === \"let\")\n                i++;\n            else if (t.name === \"in\")\n                i--;\n            if (i == 0)\n                break;\n            content.push(t);\n        }\n        let contentExpr = Util.parseSymbols(content, typed);\n        let restExpr = Util.parseSymbols(tokens, typed);\n        return new Let(boundvar, contentExpr, restExpr);\n    }\n    extractMacros() {\n        return new Let(this.boundvar, this.left.extractMacros(), this.right.extractMacros());\n    }\n}\nexports.Let = Let;\n// case文 [case] M [of] [nil] -> M | x::x -> M\nclass Case extends Expression {\n    constructor(state, ifNil, head, tail, ifElse) {\n        super(\"Case\");\n        this.state = state;\n        this.ifNil = ifNil;\n        this.head = head;\n        this.tail = tail;\n        this.ifElse = ifElse;\n    }\n    getFV() {\n        if (this.freevars !== undefined)\n            return this.freevars;\n        else\n            return Variable.union(this.state.getFV(), this.ifNil.getFV(), Variable.dif(this.ifElse.getFV(), [this.head, this.tail]));\n    }\n    toString(noParens) {\n        let ret = \"[case]\" +\n            this.state.toString(true) +\n            \"[of][nil]->\" +\n            this.ifNil.toString(true) +\n            \"|\" +\n            this.head.toString(true) +\n            \"::\" +\n            this.tail.toString(true) +\n            \"->\" +\n            this.ifElse.toString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    substitute(y, expr) {\n        let state = this.state.substitute(y, expr);\n        let ifNil = this.ifNil.substitute(y, expr);\n        if (this.head.equals(y) || this.tail.equals(y)) {\n            return new Case(state, ifNil, this.head, this.tail, this.ifElse);\n        }\n        else if (!Variable.contains(expr.getFV(), this.head) &&\n            !Variable.contains(expr.getFV(), this.tail)) {\n            return new Case(state, ifNil, this.head, this.tail, this.ifElse.substitute(y, expr));\n        }\n        else {\n            let head = this.head;\n            let tail = this.tail;\n            let ifElse = this.ifElse;\n            if (Variable.contains(expr.getFV(), head)) {\n                let uniFV = Variable.union(this.ifElse.getFV(), expr.getFV());\n                let z = Variable.getNew(uniFV);\n                if (z.equals(y)) {\n                    ifElse = ifElse.substitute(head, z);\n                }\n                else {\n                    ifElse = ifElse.substitute(head, z).substitute(y, expr);\n                }\n                head = z;\n            }\n            if (Variable.contains(expr.getFV(), tail)) {\n                let uniFV = Variable.union(this.ifElse.getFV(), expr.getFV());\n                let z = Variable.getNew(uniFV);\n                if (z.equals(y)) {\n                    ifElse = ifElse.substitute(tail, z);\n                }\n                else {\n                    ifElse = ifElse.substitute(tail, z).substitute(y, expr);\n                }\n                tail = z;\n            }\n            return new Case(state, ifNil, head, tail, ifElse);\n        }\n    }\n    equals(expr) {\n        return (expr instanceof Case &&\n            expr.state.equals(this.state) &&\n            expr.ifNil.equals(this.ifNil) &&\n            expr.head.equals(this.head) &&\n            expr.tail.equals(this.tail) &&\n            expr.ifElse.equals(this.ifElse));\n    }\n    equalsAlpha(expr) {\n        return (expr instanceof Case &&\n            expr.state.equalsAlpha(this.state) &&\n            expr.ifNil.equalsAlpha(this.ifNil) &&\n            expr.head.equalsAlpha(this.head) &&\n            expr.tail.equalsAlpha(this.tail) &&\n            expr.ifElse.equalsAlpha(this.ifElse));\n    }\n    getEquations(gamma, type, noParens) {\n        // (case)\n        let t1 = type_1.TypeVariable.getNew();\n        let lt1 = new type_1.TypeList(t1);\n        this.head.type = t1;\n        this.tail.type = lt1;\n        let nextS = this.state.getEquations(gamma, lt1, true);\n        let nextN = this.ifNil.getEquations(gamma, type, true);\n        let nextE = this.ifElse.getEquations(gamma.concat(this.head, this.tail), type, true);\n        let str = nextS.proofTree + nextN.proofTree + nextE.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(case)}\\n\";\n        str +=\n            \"\\\\TrinaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(nextS.eqs.concat(nextN.eqs, nextE.eqs), str);\n    }\n    toTexString(noParens) {\n        let ret = \"{\\\\bf case} \" +\n            this.state.toTexString(true) +\n            \" {\\\\bf of} {\\\\rm nil} \\\\Rightarrow \" +\n            this.ifNil.toTexString(true) +\n            \" | \" +\n            this.head.toTexString(true) +\n            \"::\" +\n            this.tail.toTexString(true) +\n            \" \\\\Rightarrow \" +\n            this.ifElse.toTexString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getTypedRedex(noParens) {\n        if (this.state instanceof Nil) {\n            // (case2)\n            return new redex_1.TypedRedex(this, this.ifNil, \"case2\");\n        }\n        else if (this.state instanceof List) {\n            // (case3)\n            return new redex_1.TypedRedex(this, this.ifElse\n                .substitute(this.head, this.state.head)\n                .substitute(this.tail, this.state.tail), \"case3\");\n        }\n        else {\n            // (case1)\n            let ret = this.state.getTypedRedex(true);\n            if (ret === null)\n                return null;\n            ret.next = new Case(ret.next, this.ifNil, this.head, this.tail, this.ifElse);\n            ret.addLeft(\"([case]\");\n            ret.addRight(\"[of][nil]->\" +\n                this.ifNil +\n                \" | \" +\n                this.head +\n                \"::\" +\n                this.tail +\n                \"->\" +\n                this.ifElse +\n                \")\");\n            ret.addTexLeft(\"({\\\\bf case} \");\n            ret.addTexRight(\" {\\\\bf of} {\\\\rm nil} \\\\Rightarrow \" +\n                this.ifNil.toTexString(true) +\n                \" | \" +\n                this.head.toTexString(true) +\n                \"::\" +\n                this.tail.toTexString(true) +\n                \" \\\\Rightarrow \" +\n                this.ifElse.toTexString(true) +\n                \")\");\n            return ret;\n        }\n    }\n    static parse(tokens, typed) {\n        let state = [];\n        let i = 1;\n        while (true) {\n            if (tokens.length == 0)\n                throw new error_1.LambdaParseError(\"Illegal Case statement\");\n            let t = tokens.shift();\n            if (t.name === \"case\")\n                i++;\n            else if (t.name === \"of\")\n                i--;\n            if (i == 0)\n                break;\n            state.push(t);\n        }\n        let stateExpr = Util.parseSymbols(state, typed);\n        let t = tokens.shift();\n        if (t.name !== \"nil\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        t = tokens.shift();\n        if (t.name !== \"-\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        t = tokens.shift();\n        if (t.name !== \">\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        let ifNil = [];\n        i = 1;\n        while (true) {\n            if (tokens.length == 0)\n                throw new error_1.LambdaParseError(\"Too many [case]\");\n            let t = tokens.shift();\n            if (t.name === \"case\")\n                i++;\n            else if (t.name === \"|\")\n                i--;\n            if (i == 0)\n                break;\n            ifNil.push(t);\n        }\n        let ifNilExpr = Util.parseSymbols(ifNil, typed);\n        let head = new Variable(tokens.shift().name);\n        if (head.name.match(/^[A-Za-z]$/) === null)\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + head.name + \"'\");\n        t = tokens.shift();\n        if (t.name !== \":\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        t = tokens.shift();\n        if (t.name !== \":\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        let tail = new Variable(tokens.shift().name);\n        if (tail.name.match(/^[A-Za-z]$/) === null)\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + tail.name + \"'\");\n        t = tokens.shift();\n        if (t.name !== \"-\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        t = tokens.shift();\n        if (t.name !== \">\")\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        let ifElseExpr = Util.parseSymbols(tokens, typed);\n        return new Case(stateExpr, ifNilExpr, head, tail, ifElseExpr);\n    }\n    extractMacros() {\n        return new Case(this.state.extractMacros(), this.ifNil.extractMacros(), this.head, this.tail, this.ifElse.extractMacros());\n    }\n}\nexports.Case = Case;\n// 不動点演算子 [fix] x.M\nclass Fix extends Expression {\n    constructor(boundvar, expr) {\n        super(\"Fix\");\n        this.boundvar = boundvar;\n        this.expr = expr;\n    }\n    getFV() {\n        if (this.freevars !== undefined)\n            return this.freevars;\n        let ret = [];\n        for (let fv of this.expr.getFV()) {\n            if (!fv.equals(this.boundvar)) {\n                ret.push(fv);\n            }\n        }\n        return (this.freevars = ret);\n    }\n    toString(noParens) {\n        let ret = \"[fix]\" + this.boundvar.toString(false) + \".\" + this.expr.toString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    substitute(y, expr) {\n        if (this.boundvar.equals(y)) {\n            return this;\n        }\n        else if (!Variable.contains(expr.getFV(), this.boundvar)) {\n            return new Fix(this.boundvar, this.expr.substitute(y, expr));\n        }\n        else {\n            let uniFV = Variable.union(this.expr.getFV(), expr.getFV());\n            let z = Variable.getNew(uniFV);\n            return new Fix(z, this.expr.substitute(this.boundvar, z)).substitute(y, expr);\n        }\n    }\n    equals(expr) {\n        return (expr instanceof Fix &&\n            expr.boundvar.equals(this.boundvar) &&\n            expr.expr.equals(this.expr));\n    }\n    equalsAlpha(expr) {\n        if (!(expr instanceof Fix))\n            return false;\n        if (this.equals(expr))\n            return true;\n        let x = this.boundvar;\n        let m = this.expr;\n        let y = expr.boundvar;\n        let n = expr.expr;\n        if (Variable.contains(m.getFV(), y)) {\n            return n.equalsAlpha(m);\n        }\n        else {\n            return n.equalsAlpha(m.substitute(x, y));\n        }\n    }\n    getEquations(gamma, type, noParens) {\n        // (fix)\n        this.boundvar.type = type;\n        let next = this.expr.getEquations(gamma.concat(this.boundvar), type, true);\n        let str = next.proofTree;\n        str += \"\\\\RightLabel{\\\\scriptsize(fix)}\\n\";\n        str +=\n            \"\\\\UnaryInfC{$\" +\n                Variable.gammaToTexString(gamma) +\n                \" \\\\vdash \" +\n                this.toTexString(noParens) +\n                \" : \" +\n                type.toTexString() +\n                \" $}\\n\";\n        return new TypeResult(next.eqs, str);\n    }\n    toTexString(noParens) {\n        let ret = \"{\\\\bf fix}~\" +\n            this.boundvar.toTexString(true) +\n            \".\" +\n            this.expr.toTexString(true);\n        if (!noParens)\n            ret = \"(\" + ret + \")\";\n        return ret;\n    }\n    getRedexes(etaAllowed, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getUnTypedRedex(etaAllowed, rightmost, innermost, weak, head, noParens) {\n        throw new error_1.ReductionError(\"Untyped Reduction cannot handle typeof \" + this.className);\n    }\n    getTypedRedex(noParens) {\n        // (fix)\n        return new redex_1.TypedRedex(this, this.expr.substitute(this.boundvar, new Fix(new Variable(this.boundvar.name), this.expr)), \"fix\");\n    }\n    static parse(tokens, typed) {\n        let t = tokens.shift();\n        if (t.name.match(/^[A-Za-z]$/) === null)\n            throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n        let boundvar = new Variable(t.name);\n        if (tokens.shift().name !== \".\")\n            throw new error_1.LambdaParseError(\"'.' is expected\");\n        let contentExpr = Util.parseSymbols(tokens, typed);\n        return new Fix(boundvar, contentExpr);\n    }\n    extractMacros() {\n        return new Fix(this.boundvar, this.expr.extractMacros());\n    }\n}\nexports.Fix = Fix;\n\n\n//# sourceURL=webpack://lambda-friends/./js/expression.js?");
  
  /***/ }),
  
  /***/ "./js/graph.js":
  /*!*********************!*\
    !*** ./js/graph.js ***!
    \*********************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.ReductionNode = exports.GraphNode = void 0;\nconst error_1 = __webpack_require__(/*! ./error */ \"./js/error.js\");\nconst lambda_friends_1 = __webpack_require__(/*! ./lambda-friends */ \"./js/lambda-friends.js\");\nclass GraphNode {\n    constructor(label, info, isRoot) {\n        this.children = [];\n        this.label = label;\n        this.info = info;\n        this.id = info.nextId++;\n        this.isRoot = isRoot;\n        info.nodes.push(this);\n    }\n    toString() {\n        return this.label;\n    }\n    // 簡約グラフの同型性判定\n    equalsShape(n) {\n        if (this.info.nodes.length !== n.info.nodes.length ||\n            this.info.edges.length !== n.info.edges.length ||\n            this.info.allowMultipleEdges !== n.info.allowMultipleEdges)\n            return false;\n        return sub(this, n, []);\n        function sub(n1, n2, closed) {\n            if (n1.children.length !== n2.children.length)\n                return false;\n            closed.push({ n1: n1, n2: n2 });\n            let cs2 = [].concat(n2.children);\n            let ret = true;\n            for (let c1 of n1.children) {\n                let found = false;\n                for (let i = 0; i < cs2.length; i++) {\n                    let c2 = cs2[i];\n                    let pair = undefined;\n                    for (let c of closed) {\n                        if (c.n1.id === c1.id || c.n2.id === c2.id) {\n                            pair = c;\n                            break;\n                        }\n                    }\n                    if ((pair === undefined && sub(c1, c2, closed)) ||\n                        (pair !== undefined && pair.n1.id === c1.id && pair.n2.id === c2.id)) {\n                        cs2.splice(i, 1);\n                        found = true;\n                        break;\n                    }\n                }\n                if (!found) {\n                    ret = false;\n                    break;\n                }\n            }\n            for (let i = 0; i < closed.length; i++) {\n                if (closed[i].n1.id === n1.id) {\n                    closed.splice(i, 1);\n                    return ret;\n                }\n            }\n            throw new Error(\"Unexpected Error\");\n        }\n    }\n    // input: root -> a,b,c -> d; d -> e\n    // 多重辺が入力に存在する場合、自動で多重辺をオンにする\n    static parse(str) {\n        let stmts = str.split(\";\");\n        let info = new Info([], [], null, null, 0, false);\n        let nodes = {};\n        for (let stmt of stmts) {\n            let strs = stmt.split(\"->\");\n            let ps = str2nodes(strs[0]);\n            for (let i = 1; i < strs.length; i++) {\n                let cs = str2nodes(strs[i]);\n                for (let p of ps) {\n                    for (let c of cs) {\n                        if (info.hasEdge({ from: p, to: c }))\n                            info.allowMultipleEdges = true;\n                        info.edges.push({ from: p, to: c });\n                        p.children.push(c);\n                    }\n                }\n                ps = cs;\n            }\n        }\n        if (nodes[\"root\"] === undefined)\n            throw new error_1.GraphParseError(\"there must be a 'root' node.\");\n        return nodes[\"root\"];\n        // input: \" a, b, c \"\n        function str2nodes(str) {\n            let strs = str.split(\",\");\n            let rets = [];\n            for (let t of strs) {\n                t = t.trim();\n                if (t === \"\")\n                    continue;\n                if (!/^[a-z][a-z0-9]*$/.test(t))\n                    throw new error_1.GraphParseError(\"the name '\" +\n                        t +\n                        \"' cannot be used as node name, must be [a-z][a-z0-9]*\");\n                let n = nodes[t];\n                if (n === undefined) {\n                    n = nodes[t] = new GraphNode(t, info, t === \"root\");\n                }\n                rets.push(n);\n            }\n            return rets;\n        }\n    }\n    static search(n, allowMultipleEdges) {\n        let input;\n        let filename = \"graph_closure.csv\";\n        try {\n            let request = new XMLHttpRequest();\n            request.open(\"GET\", filename, false);\n            request.send(null);\n            input = request.responseText;\n        }\n        catch (e) {\n            if (false) {}\n            let fs = __webpack_require__(/*! fs */ \"fs\");\n            try {\n                fs.statSync(filename);\n            }\n            catch (e) {\n                console.error(\"File Not Found: \" + filename);\n                return;\n            }\n            input = fs.readFileSync(filename, \"utf8\");\n        }\n        let lines = input.split(\"\\n\");\n        for (let line of lines) {\n            let strs = line.split(\",\");\n            if (parseInt(strs[2]) === n.info.nodes.length &&\n                parseInt(strs[3]) === n.info.edges.length) {\n                let lf = new lambda_friends_1.LambdaFriends(strs[0], false, false, allowMultipleEdges);\n                // csvに書いてあるものは止まることを保証しておこう\n                while (true)\n                    if (lf.deepen() === null)\n                        break;\n                if (lf.root.equalsShape(n)) {\n                    return lf;\n                }\n            }\n        }\n        return null;\n    }\n}\nexports.GraphNode = GraphNode;\nclass Info {\n    constructor(nodes, edges, typed, etaAllowed, nextId, allowMultipleEdges) {\n        this.nodes = nodes;\n        this.edges = edges;\n        this.typed = typed;\n        this.etaAllowed = etaAllowed;\n        this.nextId = nextId;\n        this.allowMultipleEdges = allowMultipleEdges;\n    }\n    hasEdge(edge) {\n        for (let e of this.edges) {\n            if (e.from.id === edge.from.id && e.to.id === edge.to.id) {\n                return true;\n            }\n        }\n        return false;\n    }\n}\nclass ReductionNode extends GraphNode {\n    constructor(expr, parent, info, isRoot) {\n        super((expr = expr.extractMacros()).toString(true), info, isRoot);\n        this.expr = expr;\n        this.parent = parent;\n        if (parent === null)\n            this.depth = 0;\n        else\n            this.depth = parent.depth + 1;\n        if (info.typed) {\n            let r = this.expr.getTypedRedex(true);\n            this.nextrs = r ? [r] : [];\n        }\n        else {\n            this.nextrs = this.expr.getRedexes(info.etaAllowed, true);\n        }\n        this.isNormalForm = this.nextrs.length === 0;\n    }\n    static makeRoot(expr, typed, etaAllowed, allowMultipleEdges) {\n        return new ReductionNode(expr, null, new Info([], [], typed, etaAllowed, 0, allowMultipleEdges), true);\n    }\n    visit() {\n        let ans = { nodes: [], edges: [] };\n        for (let r of this.nextrs) {\n            let ret = this.find(r.next);\n            if (ret === null) {\n                let n = new ReductionNode(r.next, this, this.info, false);\n                this.children.push(n);\n                ans.nodes.push(n);\n                if (this.info.allowMultipleEdges ||\n                    !this.info.hasEdge({ from: this, to: n })) {\n                    ans.edges.push({ from: this, to: n });\n                    this.info.edges.push({ from: this, to: n });\n                }\n            }\n            else {\n                this.children.push(ret);\n                if (this.info.allowMultipleEdges ||\n                    !this.info.hasEdge({ from: this, to: ret })) {\n                    ans.edges.push({ from: this, to: ret });\n                    this.info.edges.push({ from: this, to: ret });\n                }\n            }\n        }\n        return ans;\n    }\n    find(expr) {\n        for (let n of this.info.nodes) {\n            if (n.expr.equalsAlpha(expr)) {\n                return n;\n            }\n        }\n        return null;\n    }\n}\nexports.ReductionNode = ReductionNode;\n\n\n//# sourceURL=webpack://lambda-friends/./js/graph.js?");
  
  /***/ }),
  
  /***/ "./js/lambda-friends.js":
  /*!******************************!*\
    !*** ./js/lambda-friends.js ***!
    \******************************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.LambdaFriends = void 0;\nconst expression_1 = __webpack_require__(/*! ./expression */ \"./js/expression.js\");\nconst type_1 = __webpack_require__(/*! ./type */ \"./js/type.js\");\nconst graph_1 = __webpack_require__(/*! ./graph */ \"./js/graph.js\");\nconst redex_1 = __webpack_require__(/*! ./redex */ \"./js/redex.js\");\nconst util_1 = __webpack_require__(/*! ./util */ \"./js/util.js\");\nconst deBrujin_1 = __webpack_require__(/*! ./deBrujin */ \"./js/deBrujin.js\");\nclass LambdaFriends {\n    constructor(str, typed, etaAllowed, allowMultipleEdges) {\n        let l = str.split(\"#\")[0].trim();\n        let names = [];\n        while (true) {\n            let ts = l.match(/^[^[]+?\\s*=\\s*/);\n            if (ts === null)\n                break;\n            let t = ts[0];\n            ts = l.split(t);\n            ts.shift();\n            l = ts.join(t);\n            names.push(t.split(/\\s*=\\s*$/)[0]);\n        }\n        this.expr = util_1.makeAST(l, typed);\n        this.original = this.expr;\n        this.type = this.getType(typed);\n        for (let name of names) {\n            expression_1.Macro.add(name, this, typed);\n        }\n        this.typed = typed;\n        this.etaAllowed = etaAllowed;\n        this.allowMultipleEdges = allowMultipleEdges;\n        this.processTex = \"\\\\begin{eqnarray*}\\n&& \";\n        this.curStep = 0;\n        this.root = graph_1.ReductionNode.makeRoot(this.expr, this.typed, this.etaAllowed, this.allowMultipleEdges);\n        this.curNodes = [this.root];\n        this.nextRedexes = undefined;\n    }\n    getRedexes() {\n        if (this.nextRedexes)\n            return this.nextRedexes;\n        if (this.typed) {\n            let r = this.expr.getTypedRedex(true);\n            return (this.nextRedexes = r ? [r] : []);\n        }\n        return (this.nextRedexes = this.expr\n            .getRedexes(this.etaAllowed, true)\n            .sort(redex_1.Redex.compare));\n    }\n    getLeftMostRedex() {\n        if (this.typed)\n            return this.expr.getTypedRedex(true);\n        return this.expr.getUnTypedRedex(this.etaAllowed, false, false, false, false, true);\n    }\n    getRedex(rightmost, innermost, weak, head) {\n        if (this.typed)\n            return this.expr.getTypedRedex(true);\n        return this.expr.getUnTypedRedex(this.etaAllowed, rightmost, innermost, weak, head, true);\n    }\n    reductionByStrategy(rightmost, innermost, weak, head) {\n        return this.reduction(this.getRedex(rightmost, innermost, weak, head));\n    }\n    reduction(redex) {\n        if (redex === undefined) {\n            // 簡約基指定のない場合、\n            redex = this.getLeftMostRedex();\n            if (!redex)\n                return null;\n        }\n        this.expr = redex.next;\n        this.nextRedexes = undefined;\n        this.processTex += redex.toTexString();\n        let ret;\n        if (redex.type === \"macro\") {\n            this.processTex += \" \\\\\\\\\\n&\\\\equiv& \";\n            ret = \"-: (macro) = \" + this.expr.toString(true);\n        }\n        else {\n            this.processTex +=\n                \" \\\\\\\\\\n&\\\\longrightarrow_{\" + redex.getTexRule() + \"}& \";\n            ret =\n                ++this.curStep +\n                    \": (\" +\n                    redex.rule +\n                    \") --> \" +\n                    this.expr.toString(true);\n        }\n        if (!this.hasNext()) {\n            ret += \"    (normal form)\\n\";\n            let n = this.parseChurchNum();\n            if (n !== null)\n                ret += \"  = \" + n + \" (as nat)\\n\";\n            let b = this.parseChurchBool();\n            if (b !== null)\n                ret += \"  = \" + b + \" (as bool)\\n\";\n            ret = ret.slice(0, -1);\n        }\n        return ret;\n    }\n    // グラフのノードを新たに1つ展開する（限界深度を指定してもよい）\n    deepen(maxDepth) {\n        if (this.curNodes.length === 0) {\n            // 展開完了\n            return null;\n        }\n        let t = this.curNodes.shift();\n        if (maxDepth !== undefined && t.depth >= maxDepth) {\n            // 限界深度に到達\n            this.curNodes.push(t);\n            return null;\n        }\n        let ret = t.visit();\n        for (let n of ret.nodes) {\n            this.curNodes.push(n);\n        }\n        return ret;\n    }\n    hasNext() {\n        return this.getLeftMostRedex() !== null;\n    }\n    isNormalForm(rightmost, innermost, weak, head) {\n        return this.getRedex(rightmost, innermost, weak, head) === null;\n    }\n    // 未展開のノードがまだあるか\n    hasNodes() {\n        return this.curNodes.length > 0;\n    }\n    getProofTree() {\n        return \"\\\\begin{prooftree}\\n\" + this.proofTree + \"\\\\end{prooftree}\";\n    }\n    getProcessTex() {\n        return (this.processTex +\n            this.expr.toTexString(true) +\n            (this.hasNext() ? \"\" : \"\\\\not\\\\longrightarrow\") +\n            \"\\n\\\\end{eqnarray*}\");\n    }\n    getType(typed) {\n        if (!typed)\n            return new type_1.TypeUntyped();\n        type_1.TypeVariable.maxId = undefined;\n        let target = type_1.TypeVariable.getNew();\n        let typeResult = this.expr.getEquations([], target, true);\n        let eqs = typeResult.eqs;\n        this.proofTree = typeResult.proofTree;\n        let ret = type_1.TypeEquation.get(target, type_1.TypeEquation.solve(eqs));\n        let vs = ret.getVariables();\n        // 't0,'t1,'t2,... から 'a,'b,'c,... に変換\n        let vars = [];\n        for (let v of vs) {\n            if (!type_1.TypeVariable.contains(vars, v))\n                vars.push(v);\n        }\n        let i = 0;\n        for (let v of vars) {\n            ret.replace(v, type_1.TypeVariable.getAlphabet(i));\n            i++;\n        }\n        return ret;\n    }\n    static parseMacroDef(str, typed) {\n        let l = str.split(\"#\")[0].trim();\n        let names = [];\n        while (true) {\n            let ts = l.match(/^[^[]+?\\s*=\\s*/);\n            if (ts === null)\n                break;\n            let t = ts[0];\n            ts = l.split(t);\n            ts.shift();\n            l = ts.join(t);\n            names.push(t.split(/\\s*=\\s*$/)[0]);\n        }\n        if (names.length === 0)\n            return null;\n        let lf = new LambdaFriends(l, typed, false, false); // ????\n        for (let name of names) {\n            expression_1.Macro.add(name, lf, typed);\n        }\n        // let name = names.shift();\n        // let ret = \"<\"+name+\">\"\n        // while (names.length>0){\n        //   let name = names.shift();\n        //   ret += \" and <\"+name+\">\";\n        // }\n        // ret += \" is defined as \"+lf.expr+\" : \"+lf.type;\n        return {\n            names: names,\n            expr: lf.expr.toString(true),\n            type: lf.type.toString(),\n        };\n    }\n    // return: file input log\n    static fileInput(textData, typed) {\n        let lines = textData.split(\"\\n\");\n        let errors = [];\n        let defs = [];\n        for (let l of lines) {\n            try {\n                let ret = LambdaFriends.parseMacroDef(l, typed);\n                if (ret !== null)\n                    defs.push(ret);\n            }\n            catch (e) {\n                errors.push(e.toString());\n            }\n        }\n        let indent = \"* \";\n        // let ret = \"# File input completed.\\n\";\n        // if (defs.length !== 0){\n        //   ret += \"## Finally, \"+defs.length+\" macros are successfully added.\\n\";\n        //   ret += indent + defs.join(\"\\n\"+indent) + \"\\n\\n\";\n        // }\n        // if (errors.length !== 0){\n        //   ret += \"## Unfortunately, \"+errors.length+\" macros are rejected due to some errors\\n\";\n        //   ret += indent + errors.join(\"\\n\"+indent) + \"\\n\";\n        // }\n        return { defs: defs, errs: errors };\n    }\n    static getMacroList(typed) {\n        let str = \"\";\n        let map = expression_1.Macro.getMap(typed);\n        for (let key in map) {\n            let e = map[key];\n            str +=\n                \"<\" +\n                    e.name +\n                    \"> is defined as \" +\n                    e.expr.toString(true) +\n                    \" : \" +\n                    e.type +\n                    \"\\n\";\n        }\n        return str;\n    }\n    static getMacroListAsObject(typed) {\n        return expression_1.Macro.getMap(typed);\n    }\n    static clearMacro(typed) {\n        return expression_1.Macro.clear(typed);\n    }\n    static graph2LF(str, allowMultipleEdges) {\n        return graph_1.GraphNode.search(graph_1.GraphNode.parse(str), allowMultipleEdges);\n    }\n    static lmntal2LF(str) {\n        return new LambdaFriends(util_1.parseLMNtal(str).toString(true), false, false, false);\n    }\n    static deBrujin2LF(str) {\n        return new LambdaFriends(deBrujin_1.deBrujinExpression.parse(str).toLambda().toString(true), false, false, false);\n    }\n    // typedだったらとりあえずnullを返すことにする\n    toLMNtal() {\n        LambdaFriends.nextLinkID = 0;\n        if (this.typed)\n            return null;\n        else\n            return this.original.toLMNtal();\n    }\n    // typedだったらとりあえずnullを返すことにする\n    toSKI() {\n        if (this.typed)\n            return null;\n        else\n            return this.original.toSKI().toString(true);\n    }\n    // typedだったらとりあえずnullを返すことにする\n    toDeBrujin() {\n        if (this.typed)\n            return null;\n        else\n            return this.original.toDeBrujin().toString();\n    }\n    toString() {\n        let ret = this.expr.toString(true) + (this.typed ? \" : \" + this.type : \"\");\n        if (!this.hasNext()) {\n            ret += \"    (normal form)\\n\";\n            let n = this.parseChurchNum();\n            if (n !== null)\n                ret += \"  = \" + n + \" (as nat)\\n\";\n            let b = this.parseChurchBool();\n            if (b !== null)\n                ret += \"  = \" + b + \" (as bool)\\n\";\n            ret = ret.slice(0, ret.length - 1);\n        }\n        return ret;\n    }\n    getOriginalString() {\n        return this.original.toString(true) + (this.typed ? \" : \" + this.type : \"\");\n    }\n    parseChurchNum() {\n        return this.expr.parseChurchNum();\n    }\n    parseChurchBool() {\n        return this.expr.parseChurchBool();\n    }\n    static getNewLink() {\n        return \"R\" + LambdaFriends.nextLinkID++;\n    }\n}\nexports.LambdaFriends = LambdaFriends;\n\n\n//# sourceURL=webpack://lambda-friends/./js/lambda-friends.js?");
  
  /***/ }),
  
  /***/ "./js/redex.js":
  /*!*********************!*\
    !*** ./js/redex.js ***!
    \*********************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.TypedRedex = exports.MacroRedex = exports.EtaRedex = exports.BetaRedex = exports.Redex = void 0;\nconst expression_1 = __webpack_require__(/*! ./expression */ \"./js/expression.js\");\nconst Util = __webpack_require__(/*! ./util */ \"./js/util.js\");\n// 簡約基\nclass Redex {\n    constructor(type) {\n        this.left = \"\";\n        this.right = \"\";\n        this.texLeft = \"\";\n        this.texRight = \"\";\n        this.type = type;\n    }\n    addLeft(s) {\n        this.left = s + this.left;\n    }\n    addRight(s) {\n        this.right += s;\n    }\n    addTexLeft(s) {\n        this.texLeft = s + this.texLeft;\n    }\n    addTexRight(s) {\n        this.texRight += s;\n    }\n    static makeNext(es, prefix, suffix, prefixTex, suffixTex, func) {\n        let ret = [].concat(es);\n        for (let e of ret) {\n            e.next = func(e.next);\n            e.addLeft(prefix);\n            e.addRight(suffix);\n            e.addTexLeft(prefixTex);\n            e.addTexRight(suffixTex);\n        }\n        return ret;\n    }\n    getName() {\n        return this.type;\n    }\n    getPos() {\n        return this.left.length;\n    }\n    // aの方が優先度高い → 負, 同等 → 0, bの方が優先度高い → 正\n    static compare(a, b) {\n        let ap = a.getPos();\n        let bp = b.getPos();\n        if (ap === bp) {\n            const f = (r) => {\n                if (r instanceof BetaRedex)\n                    return 0;\n                if (r instanceof EtaRedex)\n                    return 1;\n                if (r instanceof MacroRedex)\n                    return 2;\n                if (r instanceof TypedRedex)\n                    return 3;\n            };\n            return f(a) - f(b);\n        }\n        else\n            return ap - bp;\n    }\n}\nexports.Redex = Redex;\n// β基 : (\\x.M)N\nclass BetaRedex extends Redex {\n    constructor(e) {\n        super(\"beta\");\n        this.content = e;\n        this.la = e.left;\n        this.next = this.la.expr.substitute(this.la.boundvar, e.right);\n        this.arg = e.right;\n        this.rule = \"beta\";\n    }\n    toString() {\n        let boundvars = [];\n        let expr = this.la.expr;\n        while (expr instanceof expression_1.LambdaAbstraction) {\n            boundvars.push(expr.boundvar.toString(false));\n            expr = expr.expr;\n        }\n        let str = boundvars.join(\"\") + \".\" + expr.toString(true);\n        return (this.left +\n            \"(\\\\[\" +\n            this.la.boundvar.toString(false) +\n            \"]\" +\n            str +\n            \")[\" +\n            this.arg.toString(false) +\n            \"]\" +\n            this.right);\n    }\n    toTexString() {\n        let boundvars = [];\n        let expr = this.la.expr;\n        while (expr instanceof expression_1.LambdaAbstraction) {\n            boundvars.push(expr.boundvar.toTexString(false));\n            expr = expr.expr;\n        }\n        let str = boundvars.join(\"\") + \".\" + expr.toTexString(true);\n        return (this.texLeft +\n            \"(\\\\strut \\\\lambda{\\\\underline{\" +\n            this.la.boundvar.toTexString(false) +\n            \"}}\" +\n            str +\n            \")\\\\underline{\\\\strut \" +\n            this.arg.toTexString(false) +\n            \"}\" +\n            this.texRight);\n    }\n    toHTMLString() {\n        let boundvars = [];\n        let expr = this.la.expr;\n        while (expr instanceof expression_1.LambdaAbstraction) {\n            boundvars.push(expr.boundvar.toString(false));\n            expr = expr.expr;\n        }\n        let str = boundvars.join(\"\") + \".\" + expr.toString(true);\n        return (Util.htmlEscape(this.left) +\n            '(\\\\<span class=\"lf-beta lf-boundvar\">' +\n            Util.htmlEscape(this.la.boundvar.toString(false)) +\n            \"</span>\" +\n            Util.htmlEscape(str) +\n            ')<span class=\"lf-beta lf-arg\">' +\n            Util.htmlEscape(this.arg.toString(false)) +\n            \"</span>\" +\n            Util.htmlEscape(this.right));\n    }\n    getTexRule() {\n        return \"\\\\beta\";\n    }\n}\nexports.BetaRedex = BetaRedex;\n// η基 : (\\x.Mx)\nclass EtaRedex extends Redex {\n    constructor(e) {\n        super(\"eta\");\n        this.content = e;\n        this.app = e.expr;\n        this.next = this.app.left;\n        this.rule = \"eta\";\n    }\n    toString() {\n        return this.left + \"[\" + this.content + \"]\" + this.right;\n    }\n    toTexString() {\n        return (this.texLeft +\n            \"\\\\underline{\\\\strut \" +\n            this.content.toTexString(this.left + this.right === \"\") +\n            \"}\" +\n            this.texRight);\n    }\n    toHTMLString() {\n        return (Util.htmlEscape(this.left) +\n            '<span class=\"lf-eta\">' +\n            Util.htmlEscape(this.content.toString(this.left + this.right === \"\")) +\n            \"</span>\" +\n            Util.htmlEscape(this.right));\n    }\n    getTexRule() {\n        return \"\\\\eta\";\n    }\n}\nexports.EtaRedex = EtaRedex;\n// マクロ : <macro>\nclass MacroRedex extends Redex {\n    constructor(e) {\n        super(\"macro\");\n        this.content = e;\n        this.next = e.expr;\n        this.rule = \"macro\";\n    }\n    toString() {\n        return this.left + \"[<\" + this.content.name + \">]\" + this.right;\n    }\n    toTexString() {\n        return (this.texLeft +\n            \"\\\\underline{\\\\strut \" +\n            this.content.toTexString(false) +\n            \"}\" +\n            this.texRight);\n    }\n    toHTMLString() {\n        return (Util.htmlEscape(this.left) +\n            '<span class=\"lf-macro\">&lt;' +\n            Util.htmlEscape(this.content.name) +\n            \"&gt;</span>\" +\n            Util.htmlEscape(this.right));\n    }\n    getTexRule() {\n        return \"{\\\\rm m}\";\n    }\n}\nexports.MacroRedex = MacroRedex;\n// 型付きの簡約基（マクロ以外）\nclass TypedRedex extends Redex {\n    constructor(e, next, rule) {\n        super(\"typed\");\n        this.content = e;\n        this.next = next;\n        this.rule = rule;\n    }\n    toString() {\n        return (this.left +\n            \"[\" +\n            this.content.toString(this.left + this.right === \"\") +\n            \"]\" +\n            this.right);\n    }\n    toTexString() {\n        return (this.texLeft +\n            \"\\\\underline{\\\\strut \" +\n            this.content.toTexString(false) +\n            \"}\" +\n            this.texRight);\n    }\n    toHTMLString() {\n        return (Util.htmlEscape(this.left) +\n            '<span class=\"lf-typed\">' +\n            Util.htmlEscape(this.content.toString(this.left + this.right === \"\")) +\n            \"</span>\" +\n            Util.htmlEscape(this.right));\n    }\n    getTexRule() {\n        return \"{\\\\rm (\" + this.rule + \")}\";\n    }\n}\nexports.TypedRedex = TypedRedex;\n\n\n//# sourceURL=webpack://lambda-friends/./js/redex.js?");
  
  /***/ }),
  
  /***/ "./js/type.js":
  /*!********************!*\
    !*** ./js/type.js ***!
    \********************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.TypeUntyped = exports.TypeVariable = exports.TypeFunc = exports.TypeList = exports.TypeBool = exports.TypeInt = exports.TypeConstructor = exports.TypeEquation = exports.Type = void 0;\nconst error_1 = __webpack_require__(/*! ./error */ \"./js/error.js\");\nclass Type {\n    constructor(className) {\n        this.className = className;\n    }\n}\nexports.Type = Type;\nclass TypeEquation {\n    constructor(left, right) {\n        this.left = left;\n        this.right = right;\n    }\n    transform(eqs, next) {\n        if (this.left instanceof TypeConstructor &&\n            this.right instanceof TypeConstructor) {\n            // (a),(b)\n            return this.left.match(this.right);\n        }\n        if (this.left.equals(this.right)) {\n            // (c)\n            return [];\n        }\n        if (!(this.left instanceof TypeVariable)) {\n            // (d)\n            return [new TypeEquation(this.right, this.left)];\n        }\n        if (this.right.contains(this.left)) {\n            // (e)\n            throw new error_1.TypeError(\"Illegal type (\" +\n                this.right +\n                \" contains \" +\n                this.left +\n                \". Self-application?)\");\n        }\n        // (f)\n        for (var e of eqs) {\n            e.replace(this.left, this.right);\n        }\n        for (var e of next) {\n            e.replace(this.left, this.right);\n        }\n        return [this];\n    }\n    static isEqual(a, b) {\n        if (a.length !== b.length)\n            return false;\n        for (var ai of a) {\n            if (!TypeEquation.contains(ai, b))\n                return false;\n        }\n        return true;\n    }\n    static contains(a, b) {\n        for (var bi of b) {\n            if (a.equals(bi))\n                return true;\n        }\n        return false;\n    }\n    equals(e) {\n        return e.left.equals(this.left) && e.right.equals(this.right);\n    }\n    static get(t, eqs) {\n        for (var eq of eqs) {\n            if (eq.left.equals(t))\n                return eq.right;\n        }\n        throw new error_1.TypeError(\"Undefined TypeVariable: \" + t);\n    }\n    toString() {\n        return this.left + \" = \" + this.right;\n    }\n    replace(from, to) {\n        if (this.left.equals(from)) {\n            this.left = to;\n        }\n        else {\n            this.left.replace(from, to);\n        }\n        if (this.right.equals(from)) {\n            this.right = to;\n        }\n        else {\n            this.right.replace(from, to);\n        }\n    }\n    static solve(eqs) {\n        while (true) {\n            var prev = [].concat(eqs);\n            var next = [];\n            while (eqs.length > 0) {\n                var e = eqs.shift();\n                var ans = e.transform(eqs, next);\n                next = next.concat(ans);\n            }\n            eqs = [].concat(next);\n            if (TypeEquation.isEqual(prev, next))\n                break;\n        }\n        return eqs;\n    }\n}\nexports.TypeEquation = TypeEquation;\nclass TypeConstructor extends Type {\n}\nexports.TypeConstructor = TypeConstructor;\nclass TypeInt extends TypeConstructor {\n    constructor() {\n        super(\"TypeInt\");\n    }\n    toString() {\n        return \"int\";\n    }\n    toTexString() {\n        return \"{\\\\rm int}\";\n    }\n    equals(t) {\n        if (t instanceof TypeInt)\n            return true;\n        else\n            return false;\n    }\n    match(t) {\n        if (t instanceof TypeInt) {\n            return [];\n        }\n        else {\n            throw new error_1.TypeError(this + \" and \" + t + \" are not compatible.\");\n        }\n    }\n    contains(t) {\n        return false;\n    }\n    replace(from, to) { }\n    getVariables() {\n        return [];\n    }\n}\nexports.TypeInt = TypeInt;\nclass TypeBool extends TypeConstructor {\n    constructor() {\n        super(\"TypeBool\");\n    }\n    toString() {\n        return \"bool\";\n    }\n    toTexString() {\n        return \"{\\\\rm bool}\";\n    }\n    equals(t) {\n        if (t instanceof TypeBool)\n            return true;\n        else\n            return false;\n    }\n    match(t) {\n        if (t instanceof TypeBool) {\n            return [];\n        }\n        else {\n            throw new error_1.TypeError(this + \" and \" + t + \" are not compatible.\");\n        }\n    }\n    contains(t) {\n        return false;\n    }\n    replace(from, to) { }\n    getVariables() {\n        return [];\n    }\n}\nexports.TypeBool = TypeBool;\nclass TypeList extends TypeConstructor {\n    constructor(x) {\n        super(\"TypeList\");\n        this.content = x;\n    }\n    toString() {\n        return \"list(\" + this.content + \")\";\n    }\n    toTexString() {\n        return \"{\\\\rm list}(\" + this.content.toTexString() + \")\";\n    }\n    equals(t) {\n        if (t instanceof TypeList)\n            return this.content.equals(t.content);\n        else\n            return false;\n    }\n    match(t) {\n        if (t instanceof TypeList) {\n            return [new TypeEquation(this.content, t.content)];\n        }\n        else {\n            throw new error_1.TypeError(this + \" and \" + t + \" are not compatible.\");\n        }\n    }\n    contains(t) {\n        return this.content.contains(t);\n    }\n    replace(from, to) {\n        if (this.content.equals(from)) {\n            this.content = to;\n        }\n        else {\n            this.content.replace(from, to);\n        }\n    }\n    getVariables() {\n        return this.content.getVariables();\n    }\n}\nexports.TypeList = TypeList;\nclass TypeFunc extends TypeConstructor {\n    constructor(left, right) {\n        super(\"TypeFunc\");\n        this.left = left;\n        this.right = right;\n    }\n    toString() {\n        var ret;\n        if (this.left instanceof TypeFunc)\n            ret = \"(\" + this.left + \")\";\n        else\n            ret = this.left.toString();\n        return ret + \" -> \" + this.right;\n    }\n    toTexString() {\n        var ret;\n        if (this.left instanceof TypeFunc)\n            ret = \"(\" + this.left.toTexString() + \")\";\n        else\n            ret = this.left.toTexString();\n        return ret + \" \\\\rightarrow \" + this.right.toTexString();\n    }\n    equals(t) {\n        if (t instanceof TypeFunc)\n            return t.left.equals(this.left) && t.right.equals(this.right);\n        else\n            return false;\n    }\n    match(t) {\n        if (t instanceof TypeFunc) {\n            return [\n                new TypeEquation(this.left, t.left),\n                new TypeEquation(this.right, t.right),\n            ];\n        }\n        else {\n            throw new error_1.TypeError(this + \" and \" + t + \" are not compatible.\");\n        }\n    }\n    contains(t) {\n        return this.left.contains(t) || this.right.contains(t);\n    }\n    replace(from, to) {\n        if (this.left.equals(from)) {\n            this.left = to;\n        }\n        else {\n            this.left.replace(from, to);\n        }\n        if (this.right.equals(from)) {\n            this.right = to;\n        }\n        else {\n            this.right.replace(from, to);\n        }\n    }\n    getVariables() {\n        return this.left.getVariables().concat(this.right.getVariables());\n    }\n}\nexports.TypeFunc = TypeFunc;\nclass TypeVariable extends Type {\n    constructor(id) {\n        super(\"TypeVariable\");\n        this.id = id;\n    }\n    toString() {\n        if (this.id < 0)\n            return \"'\" + TypeVariable.alphabet[-this.id - 1];\n        return \"'t\" + this.id;\n    }\n    toTexString() {\n        if (this.id < 0)\n            return TypeVariable.texAlphabet[-this.id - 1];\n        return \"\\\\tau_{\" + this.id + \"}\";\n    }\n    equals(t) {\n        if (t instanceof TypeVariable)\n            return this.id === t.id;\n        else\n            return false;\n    }\n    static getNew() {\n        if (TypeVariable.maxId === undefined) {\n            TypeVariable.maxId = 0;\n            return new TypeVariable(0);\n        }\n        else {\n            TypeVariable.maxId++;\n            return new TypeVariable(TypeVariable.maxId);\n        }\n    }\n    contains(t) {\n        return this.equals(t);\n    }\n    replace(from, to) { }\n    getVariables() {\n        return [this];\n    }\n    static getAlphabet(i) {\n        return new TypeVariable(-i - 1);\n    }\n    static contains(a, b) {\n        for (var ta of a) {\n            if (ta.equals(b)) {\n                return true;\n            }\n        }\n        return false;\n    }\n}\nexports.TypeVariable = TypeVariable;\nTypeVariable.alphabet = \"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ\".split(\"\");\nTypeVariable.texAlphabet = [\n    \"\\\\alpha\",\n    \"\\\\beta\",\n    \"\\\\gamma\",\n    \"\\\\delta\",\n    \"\\\\varepsilon\",\n    \"\\\\zeta\",\n    \"\\\\eta\",\n    \"\\\\theta\",\n    \"\\\\iota\",\n    \"\\\\kappa\",\n    \"\\\\mu\",\n    \"\\\\nu\",\n    \"\\\\xi\",\n    \"\\\\pi\",\n    \"\\\\rho\",\n    \"\\\\sigma\",\n    \"\\\\upsilon\",\n    \"\\\\phi\",\n    \"\\\\chi\",\n    \"\\\\psi\",\n    \"\\\\omega\",\n    \"\\\\Gamma\",\n    \"\\\\Delta\",\n    \"\\\\Theta\",\n    \"\\\\Xi\",\n    \"\\\\Pi\",\n    \"\\\\Sigma\",\n    \"\\\\Phi\",\n    \"\\\\Psi\",\n    \"\\\\Omega\",\n].concat(TypeVariable.alphabet);\nclass TypeUntyped extends Type {\n    constructor() {\n        super(\"TypeUntyped\");\n    }\n    toString() {\n        return \"Untyped\";\n    }\n    toTexString() {\n        return \"{\\\\rm Untyped}\";\n    }\n    equals(t) {\n        if (t instanceof TypeUntyped)\n            return true;\n        else\n            return false;\n    }\n    contains(t) {\n        return false;\n    }\n    replace(from, to) { }\n    getVariables() {\n        return [];\n    }\n}\nexports.TypeUntyped = TypeUntyped;\n\n\n//# sourceURL=webpack://lambda-friends/./js/type.js?");
  
  /***/ }),
  
  /***/ "./js/util.js":
  /*!********************!*\
    !*** ./js/util.js ***!
    \********************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nexports.putParens = exports.htmlEscape = exports.makeTerms = exports.makeChurchNum = exports.parseLMNtal = exports.makeAST = exports.parseSymbols = void 0;\nconst error_1 = __webpack_require__(/*! ./error */ \"./js/error.js\");\nconst expression_1 = __webpack_require__(/*! ./expression */ \"./js/expression.js\");\n// 字句解析\nfunction tokenize(str, typed) {\n    let strs = str.split(\"\");\n    let tokens = [];\n    while (strs.length > 0) {\n        let c = strs.shift().trim();\n        if (c === \"\") {\n        }\n        else if (c === \"<\") {\n            // <macro>\n            let content = \"\";\n            while (true) {\n                if (strs.length == 0)\n                    throw new error_1.LambdaParseError(\"Too many LANGLE '<'\");\n                c = strs.shift();\n                if (c === \">\")\n                    break;\n                else\n                    content += c;\n            }\n            tokens.push(expression_1.Macro.get(content, typed));\n        }\n        else if (typed && c === \"[\") {\n            // [const]\n            let content = \"\";\n            while (true) {\n                if (strs.length == 0)\n                    throw new error_1.LambdaParseError(\"Too many LBRACKET '['\");\n                c = strs.shift();\n                if (c === \"]\")\n                    break;\n                else\n                    content += c;\n            }\n            let result = null;\n            switch (content) {\n                case \"nil\":\n                    result = new expression_1.Nil();\n                    break;\n                case \"false\":\n                case \"true\":\n                    result = new expression_1.ConstBool(content === \"true\");\n                    break;\n                case \"if\":\n                case \"then\":\n                case \"else\":\n                case \"let\":\n                case \"in\":\n                case \"case\":\n                case \"of\":\n                case \"fix\":\n                    result = new expression_1.Symbol(content);\n                    break;\n                default:\n                    if (content.match(/^\\d+$|^-\\d+$/) !== null) {\n                        result = new expression_1.ConstInt(parseInt(content));\n                    }\n                    else {\n                        result = new expression_1.ConstOp(content); // fail -> null\n                    }\n            }\n            if (result === null)\n                throw new error_1.LambdaParseError(\"Unknown Const: [\" + content + \"]\");\n            tokens.push(result);\n        }\n        else {\n            tokens.push(new expression_1.Symbol(c));\n        }\n    }\n    return tokens;\n}\n// 構文解析\nfunction parseSymbols(tokens, typed) {\n    let left = null;\n    while (tokens.length > 0) {\n        // 最初のSymbol\n        let first = tokens.shift();\n        if (first instanceof expression_1.Const ||\n            first instanceof expression_1.Nil ||\n            first instanceof expression_1.Macro) {\n            if (left === null)\n                left = first;\n            else\n                left = new expression_1.Application(left, first);\n            continue;\n        }\n        switch (first.name) {\n            case \"\\\\\":\n            case \"\\u00a5\":\n            case \"λ\": {\n                // abst\n                if (left === null)\n                    return expression_1.LambdaAbstraction.parse(tokens, typed);\n                else\n                    return new expression_1.Application(left, expression_1.LambdaAbstraction.parse(tokens, typed));\n            }\n            case \"(\": {\n                // application\n                let content = [];\n                let i = 1;\n                while (true) {\n                    if (tokens.length === 0)\n                        throw new error_1.LambdaParseError(\"Too many LPAREN '('\");\n                    let t = tokens.shift();\n                    if (t.name === \"(\")\n                        i++;\n                    else if (t.name === \")\")\n                        i--;\n                    if (i === 0)\n                        break;\n                    content.push(t);\n                }\n                let contentExpr = parseSymbols(content, typed);\n                if (left === null)\n                    left = contentExpr;\n                else\n                    left = new expression_1.Application(left, contentExpr);\n                break;\n            }\n            default: {\n                if (typed) {\n                    switch (first.name) {\n                        case \"if\": {\n                            // if statement\n                            return expression_1.If.parse(tokens, typed);\n                        }\n                        case \"let\": {\n                            // let statement\n                            return expression_1.Let.parse(tokens, typed);\n                        }\n                        case \"case\": {\n                            // case statement: [case] M [of] [nil] -> M | x::x -> M\n                            return expression_1.Case.parse(tokens, typed);\n                        }\n                        case \"fix\": {\n                            // fixed-point: [fix] x.M\n                            return expression_1.Fix.parse(tokens, typed);\n                        }\n                        case \":\": {\n                            // list\n                            let t = tokens.shift();\n                            if (t.name !== \":\")\n                                throw new error_1.LambdaParseError(\"Unexpected token: '\" + t + \"'\");\n                            return new expression_1.List(left, parseSymbols(tokens, typed));\n                        }\n                    }\n                }\n                if (first.name.match(/^[A-Za-z]$/) === null)\n                    throw new error_1.LambdaParseError(\"Unexpected token: '\" + first + \"'\");\n                // variable\n                if (left === null)\n                    left = new expression_1.Variable(first.name);\n                else\n                    left = new expression_1.Application(left, new expression_1.Variable(first.name));\n            }\n        }\n    }\n    if (left === null)\n        throw new error_1.LambdaParseError(\"No contents in Expression\");\n    return left;\n}\nexports.parseSymbols = parseSymbols;\n// 字句解析と構文解析 return: root node\nfunction makeAST(str, typed) {\n    return parseSymbols(tokenize(str, typed), typed);\n}\nexports.makeAST = makeAST;\n// Input : lambda(cp(L0,L1),lambda(L2,apply(apply(L1,L0),L2)))\n// Now   : lambda([L0,L1], lambda([L2],apply()))\n// Output: \\xy.xxy\nfunction parseLMNtal(str) {\n    return parse(str, [], {});\n    function parse(str, usedVars, map) {\n        str = str.trim();\n        let res = str.match(/^.+?(?=\\()/);\n        if (res === null) {\n            let ret = map[str];\n            if (ret === undefined)\n                throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. Unknown Token: \" + str);\n            return new expression_1.Variable(ret);\n        }\n        let atom = res[0].trim();\n        let args = parseArg(str.match(/\\(.+$/)[0]);\n        switch (atom) {\n            case \"lambda\": {\n                if (args.length !== 2)\n                    throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. lambda(X,A) should have 2 args.\");\n                let v = expression_1.Variable.getNew(usedVars);\n                let bvs = parseAbsArg(args[0]);\n                for (let bv of bvs)\n                    map[bv] = v.name;\n                return new expression_1.LambdaAbstraction(v, parse(args[1], usedVars.concat(v), Object.assign({}, map)));\n            }\n            case \"apply\": {\n                if (args.length !== 2)\n                    throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. apply(A,B) should have 2 args.\");\n                return new expression_1.Application(parse(args[0], [].concat(usedVars), Object.assign({}, map)), parse(args[1], [].concat(usedVars), Object.assign({}, map)));\n            }\n            case \"fv\": {\n                if (args.length !== 1)\n                    throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. fv(X) should have 1 arg.\");\n                if (args[0].length !== 1 || !args[0].match(/[a-z]/))\n                    return expression_1.Macro.get(args[0], false);\n                // throw new LambdaParseError(\"too long free variable name: \"+ args[0]);\n                return new expression_1.Variable(args[0]);\n            }\n            default:\n                throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. Unexpected atom name: \" + atom);\n        }\n    }\n    // Ex1: (L0,cp(L1,L2)) => [\"L0\",\"cp(L1,L2)\"]\n    // Ex2: (L0) => [\"L0\"]\n    // Ex3: ( ) => []\n    function parseArg(str) {\n        str = str.trim();\n        if (str[0] !== \"(\" || str[str.length - 1] !== \")\")\n            throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. Invalid Parentheses.\");\n        let level = 0;\n        let content = \"\";\n        let strs = [];\n        for (let i = 1; i < str.length - 1; i++) {\n            let t = str[i];\n            if (t === \"(\")\n                level++;\n            else if (t === \")\")\n                level--;\n            if (level === 0 && t === \",\") {\n                strs.push(content);\n                content = \"\";\n            }\n            else {\n                content += t;\n            }\n        }\n        if (level !== 0)\n            throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. Invalid Parentheses.\");\n        strs.push(content);\n        if (strs.length === 1) {\n            let s = strs[0].trim();\n            if (s === \"\")\n                return [];\n            else\n                return [s];\n        }\n        let ret = [];\n        for (let s of strs)\n            ret.push(s.trim());\n        return ret;\n    }\n    // Ex1: cp(L0,cp(L1,L2)) => [L0,L1,L2]\n    // Ex2: L0 => [L0]\n    // Ex3: rm => []\n    function parseAbsArg(str) {\n        str = str.trim();\n        let res = str.match(/^.+?(?=\\()/);\n        if (res === null) {\n            if (str === \"rm\")\n                return [];\n            else\n                return [str];\n        }\n        let atom = res[0].trim();\n        let args = parseArg(str.match(/\\(.+$/)[0]);\n        if (atom === \"rm\") {\n            if (args.length !== 0)\n                throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. rm() should have 0 args.\");\n            return [];\n        }\n        else if (atom === \"cp\") {\n            if (args.length !== 2)\n                throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. cp(A,B) should have 2 args.\");\n            return parseAbsArg(args[0].trim()).concat(parseAbsArg(args[1].trim()));\n        }\n        else {\n            throw new error_1.LambdaParseError(\"Malformed LMNtal Lambda Term. Unexpected atom name: \" + atom);\n        }\n    }\n}\nexports.parseLMNtal = parseLMNtal;\n// チャーチ数を表すExpression (string)の生成\nfunction makeChurchNum(n) {\n    let str = \"\\\\sz.\";\n    let content = n === 0 ? \"z\" : \"sz\";\n    for (let i = 1; i < n; i++) {\n        content = \"s(\" + content + \")\";\n    }\n    return str + content;\n}\nexports.makeChurchNum = makeChurchNum;\nfunction makeTerms(depth) {\n    return sub([], depth);\n    function sub(vs, depth) {\n        let ret = [].concat(vs);\n        if (depth === 0)\n            return ret;\n        let res = sub(vs, depth - 1);\n        // Application\n        for (let i = 0; i < res.length; i++)\n            for (let j = 0; j < res.length; j++)\n                ret.push(new expression_1.Application(res[i], res[j]));\n        // Lambda Abstraction\n        let newVar = expression_1.Variable.getNew(vs);\n        let res1 = sub(vs.concat(newVar), depth - 1);\n        for (let r of res1)\n            ret.push(new expression_1.LambdaAbstraction(newVar, r));\n        return ret;\n    }\n}\nexports.makeTerms = makeTerms;\nfunction htmlEscape(str) {\n    return str.replace(/[&'`\"<>]/g, function (match) {\n        return {\n            \"&\": \"&amp;\",\n            \"'\": \"&#x27;\",\n            \"`\": \"&#x60;\",\n            '\"': \"&quot;\",\n            \"<\": \"&lt;\",\n            \">\": \"&gt;\",\n        }[match];\n    });\n}\nexports.htmlEscape = htmlEscape;\nfunction putParens(str, noParens) {\n    if (noParens)\n        return str;\n    else\n        return \"(\" + str + \")\";\n}\nexports.putParens = putParens;\n\n\n//# sourceURL=webpack://lambda-friends/./js/util.js?");
  
  /***/ }),
  
  /***/ "./js/webui.js":
  /*!*********************!*\
    !*** ./js/webui.js ***!
    \*********************/
  /***/ ((__unused_webpack_module, exports, __webpack_require__) => {
  
  eval("\nObject.defineProperty(exports, \"__esModule\", ({ value: true }));\nconst lambda_friends_1 = __webpack_require__(/*! ./lambda-friends */ \"./js/lambda-friends.js\");\nlet cy = cytoscape({\n    container: document.getElementById(\"graph\"),\n    boxSelectionEnabled: false,\n    autounselectify: true,\n    style: [\n        {\n            selector: \"node\",\n            style: {\n                // 'content': 'data(label)',  /* must be specified if you want to display the node text */\n                /**\n                'text-opacity': 0.5,\n                'text-valign': 'center',\n                'text-halign': 'right',\n                */\n                label: \"data(label)\",\n                \"background-color\": \"#11479e\",\n            },\n        },\n        {\n            selector: \"edge\",\n            style: {\n                \"target-arrow-shape\": \"triangle\",\n                \"curve-style\": \"bezier\",\n                \"target-arrow-color\": \"#9dbaea\",\n                width: 3,\n                \"line-color\": \"#9dbaea\",\n            },\n        },\n        {\n            selector: \".goal\",\n            style: {\n                \"background-color\": \"#b3424a\",\n            },\n        },\n        {\n            selector: \".root\",\n            style: {\n                \"background-color\": \"#407f5d\",\n            },\n        },\n        {\n            selector: \".goal.root\",\n            style: {\n                \"background-color\": \"#d17200\",\n            },\n        },\n    ],\n});\n// Initial config for setting up modals\nMicroModal.init({\n    disableScroll: false,\n    awaitCloseAnimation: true,\n});\nconst defaultSteps = 100;\nlet steps = defaultSteps;\nlet typed = true;\nlet etaAllowed = false;\nlet allowMultipleEdges = false;\nlet curlf = undefined;\nlet input = document.getElementById(\"input\");\nlet oel = document.getElementById(\"output\");\nlet settingButton = document.getElementById(\"settingBtn\");\nlet untypedButton = document.getElementById(\"untyped\");\nlet typedButton = document.getElementById(\"typed\");\nlet etaEnableButton = document.getElementById(\"etaEnable\");\nlet etaDisableButton = document.getElementById(\"etaDisable\");\nlet multiEdgeEnableButton = (document.getElementById(\"multiEdgeEnable\"));\nlet multiEdgeDisableButton = (document.getElementById(\"multiEdgeDisable\"));\nlet leftmostButton = document.getElementById(\"leftmostBtn\");\nlet rightmostButton = (document.getElementById(\"rightmostBtn\"));\nlet outermostButton = (document.getElementById(\"outermostBtn\"));\nlet innermostButton = (document.getElementById(\"innermostBtn\"));\nlet strongButton = document.getElementById(\"strongBtn\");\nlet weakButton = document.getElementById(\"weakBtn\");\nlet headButton = document.getElementById(\"headBtn\");\nlet nonheadButton = document.getElementById(\"nonheadBtn\");\nlet fileInput = document.getElementById(\"fileInput\");\nlet fileReader = new FileReader();\nlet clearMacroButton = (document.getElementById(\"clearMacroBtn\"));\nlet translateDiv = document.getElementById(\"translate\");\nlet tabA = document.getElementById(\"tabA\");\n// let macroNameInput = <HTMLInputElement>document.getElementById(\"macroNameInput\");\n// let macroInput = <HTMLInputElement>document.getElementById(\"macroInput\");\n// let submitMacroBtn = <HTMLButtonElement>document.getElementById(\"submitMacro\");\nlet outputButtons = document.getElementById(\"outputBtns\");\nlet stepInput = document.getElementById(\"stepInput\");\nlet startGraph = document.getElementById(\"startGraph\");\nlet stopGraph = document.getElementById(\"stopGraph\");\nlet imgGraph = document.getElementById(\"imgGraph\");\nlet maxDepth = document.getElementById(\"maxDepth\");\nlet tabAbtn = document.getElementById(\"tabAbtn\");\nlet tabBbtn = document.getElementById(\"tabBbtn\");\nlet tabC1btn = document.getElementById(\"tabC1btn\");\nlet tabC2btn = document.getElementById(\"tabC2btn\");\nlet tabDbtn = document.getElementById(\"tabDbtn\");\nlet lmnInput = document.getElementById(\"lmnInput\");\nlet lmnSubmitBtn = document.getElementById(\"lmnSubmit\");\nlet lmnOutput = document.getElementById(\"lmnOutput\");\nlet deBrujinInput = document.getElementById(\"deBrujinInput\");\nlet deBrujinSubmitBtn = document.getElementById(\"deBrujinSubmit\");\nlet deBrujinOutput = document.getElementById(\"deBrujinOutput\");\nlet graphInput = document.getElementById(\"graphInput\");\nlet graphSubmitBtn = document.getElementById(\"graphSubmit\");\nlet graphOutput = document.getElementById(\"graphOutput\");\nfileInput.addEventListener(\"change\", function (ev) {\n    let target = ev.target;\n    let file = target.files[0];\n    let type = file.type; // MIMEタイプ\n    // let size = file.size; // ファイル容量（byte）\n    if (type !== \"text/plain\") {\n        alert(\"プレーンテキストを選択してください\");\n        fileInput.value = \"\";\n        return;\n    }\n    fileReader.readAsText(file);\n});\n// マクロファイル読み込み終了時に呼ぶ\nfunction fileLoaded(result) {\n    let ret = lambda_friends_1.LambdaFriends.fileInput(result, typed);\n    refreshMacroList();\n    let div = document.getElementById(\"fileInputLog\");\n    div.textContent = null;\n    if (ret.defs.length > 0) {\n        let div1 = document.createElement(\"div\");\n        let title1 = document.createElement(\"p\");\n        title1.innerText =\n            \"Finally, \" + ret.defs.length + \" macros are successfully added.\";\n        let list1 = document.createElement(\"ul\");\n        list1.className = \"code\";\n        for (let t of ret.defs) {\n            let li = document.createElement(\"li\");\n            let names = [].concat(t.names);\n            let name = names.shift();\n            let ret = \"<\" + name + \">\";\n            while (names.length > 0) {\n                let name = names.shift();\n                ret += \" = <\" + name + \">\";\n            }\n            li.innerText = ret + \" is defined as \" + t.expr + \".\"; // +\" : \"+t.type;\n            list1.appendChild(li);\n        }\n        div1.appendChild(title1);\n        div1.appendChild(list1);\n        div.appendChild(div1);\n    }\n    if (ret.errs.length > 0) {\n        let div2 = document.createElement(\"div\");\n        let title2 = document.createElement(\"p\");\n        title2.innerText =\n            \"Unfortunately, \" +\n                ret.errs.length +\n                \" macros are rejected due to some errors.\";\n        let list2 = document.createElement(\"ul\");\n        list2.className = \"code\";\n        for (let t of ret.errs) {\n            let li = document.createElement(\"li\");\n            li.innerText = t;\n            list2.appendChild(li);\n        }\n        div2.appendChild(title2);\n        div2.appendChild(list2);\n        div.appendChild(div2);\n    }\n    MicroModal.show(\"modal-1\", {\n        debugMode: true,\n        disableScroll: true,\n        awaitCloseAnimation: true,\n    });\n}\ndocument.getElementById(\"sampleInputBtn\").addEventListener(\"click\", () => {\n    let xhr = new XMLHttpRequest();\n    // xhr.open(\"GET\",\"https://nikosai.ml/lambda-friends/samples.txt\");\n    xhr.open(\"GET\", \"https://nikosai.ml/lambda-friends/samples.txt\");\n    xhr.setRequestHeader(\"Content-Type\", \"text/plain\");\n    xhr.onreadystatechange = function () {\n        if (xhr.readyState === 4) {\n            if (xhr.status === 200) {\n                fileLoaded(xhr.responseText);\n            }\n            else {\n                console.error(\"An error has occurred loading the sample file.\\nstatus = \" +\n                    xhr.status);\n            }\n        }\n    };\n    xhr.send();\n});\nfileReader.addEventListener(\"load\", () => fileLoaded(fileReader.result));\nsettingButton.onclick = function () {\n    MicroModal.show(\"modal-2\", {\n        debugMode: true,\n        disableScroll: true,\n        awaitCloseAnimation: true,\n    });\n};\nuntypedButton.onclick = function () {\n    untypedButton.className = \"btn btn-primary\";\n    typedButton.className = \"btn btn-default\";\n    typed = false;\n    etaEnableButton.disabled = false;\n    etaDisableButton.disabled = false;\n    multiEdgeEnableButton.disabled = false;\n    multiEdgeDisableButton.disabled = false;\n    refreshMacroList();\n};\ntypedButton.onclick = function () {\n    typedButton.className = \"btn btn-primary\";\n    untypedButton.className = \"btn btn-default\";\n    typed = true;\n    etaEnableButton.disabled = true;\n    etaDisableButton.disabled = true;\n    multiEdgeEnableButton.disabled = true;\n    multiEdgeDisableButton.disabled = true;\n    refreshMacroList();\n};\netaEnableButton.onclick = function () {\n    etaEnableButton.className = \"btn btn-primary\";\n    etaDisableButton.className = \"btn btn-default\";\n    etaAllowed = true;\n};\netaDisableButton.onclick = function () {\n    etaDisableButton.className = \"btn btn-primary\";\n    etaEnableButton.className = \"btn btn-default\";\n    etaAllowed = false;\n};\nmultiEdgeEnableButton.onclick = function () {\n    multiEdgeEnableButton.className = \"btn btn-primary\";\n    multiEdgeDisableButton.className = \"btn btn-default\";\n    allowMultipleEdges = true;\n};\nmultiEdgeDisableButton.onclick = function () {\n    multiEdgeDisableButton.className = \"btn btn-primary\";\n    multiEdgeEnableButton.className = \"btn btn-default\";\n    allowMultipleEdges = false;\n};\nlet rightmost = false;\nleftmostButton.onclick = function () {\n    leftmostButton.className = \"btn btn-primary\";\n    rightmostButton.className = \"btn btn-default\";\n    rightmost = false;\n};\nrightmostButton.onclick = function () {\n    rightmostButton.className = \"btn btn-primary\";\n    leftmostButton.className = \"btn btn-default\";\n    rightmost = true;\n};\nlet innermost = false;\noutermostButton.onclick = function () {\n    outermostButton.className = \"btn btn-primary\";\n    innermostButton.className = \"btn btn-default\";\n    innermost = false;\n};\ninnermostButton.onclick = function () {\n    innermostButton.className = \"btn btn-primary\";\n    outermostButton.className = \"btn btn-default\";\n    innermost = true;\n};\nlet weak = false;\nstrongButton.onclick = function () {\n    strongButton.className = \"btn btn-primary\";\n    weakButton.className = \"btn btn-default\";\n    weak = false;\n};\nweakButton.onclick = function () {\n    weakButton.className = \"btn btn-primary\";\n    strongButton.className = \"btn btn-default\";\n    weak = true;\n};\nlet head = false;\nheadButton.onclick = function () {\n    headButton.className = \"btn btn-primary\";\n    nonheadButton.className = \"btn btn-default\";\n    head = true;\n};\nnonheadButton.onclick = function () {\n    nonheadButton.className = \"btn btn-primary\";\n    headButton.className = \"btn btn-default\";\n    head = false;\n};\nclearMacroButton.onclick = function () {\n    lambda_friends_1.LambdaFriends.clearMacro(typed);\n    refreshMacroList();\n};\nstepInput.addEventListener(\"change\", function () {\n    let new_s = parseInt(stepInput.value);\n    if (!isNaN(new_s)) {\n        steps = new_s;\n    }\n    else {\n        steps = defaultSteps;\n    }\n});\nlet historyName = \"lf_history\";\n// ===== MAKESHIFT =====\nif (window.location.pathname.split(\"/\").slice(-1)[0] === \"fl.html\") {\n    historyName = \"lf_history_fl\";\n}\nlet history = JSON.parse(localStorage.getItem(historyName)) || [];\nlet historyNum = 0;\nlet workspace = [].concat(history);\nworkspace.unshift(\"\");\nlet submitInput = function () {\n    // console.log(localStorage.getItem(historyName));\n    let line = input.value;\n    if (line === \"\" && curlf !== undefined) {\n        if (graphActive)\n            launchGraph();\n        else if (!curlf.isNormalForm(rightmost, innermost, weak, head))\n            doContinual();\n        return;\n    }\n    if (line.trim() === \"\")\n        return;\n    if (continualRunning) {\n        continualStop = true;\n    }\n    history.unshift(line);\n    localStorage.setItem(historyName, JSON.stringify(history));\n    historyNum = 0;\n    workspace = [].concat(history);\n    workspace.unshift(\"\");\n    line = line.split(\"#\")[0];\n    line = line.trim();\n    try {\n        let ret = lambda_friends_1.LambdaFriends.parseMacroDef(line, typed);\n        if (ret === null) {\n            curlf = new lambda_friends_1.LambdaFriends(line, typed, etaAllowed, allowMultipleEdges);\n            curGraphDepth = 0;\n            graphClear();\n            cy.add(node2cyObj(curlf.root));\n            makeLayout();\n            outputLine(curlf.toString());\n            if (typed)\n                doContinual();\n            else\n                showContinueBtn();\n        }\n        else {\n            let names = [].concat(ret.names);\n            let name = names.shift();\n            let str = \"<\" + name + \">\";\n            while (names.length > 0) {\n                let name = names.shift();\n                str += \" = <\" + name + \">\";\n            }\n            str +=\n                \" is defined as \" + ret.expr + (typed ? \" : \" + ret.type : \"\") + \".\";\n            outputLine(str);\n            outputButtons.textContent = null;\n        }\n        refreshTex();\n    }\n    catch (e) {\n        outputLine(e.toString());\n        console.log(e);\n        outputButtons.textContent = null;\n    }\n    refreshMacroList();\n    input.value = \"\";\n};\ndocument.getElementById(\"submit\").onclick = submitInput;\ndocument.getElementById(\"input\").onkeydown = function (e) {\n    if (e.keyCode === 13) {\n        submitInput();\n        e.preventDefault();\n    }\n    else if (e.keyCode === 38) {\n        // up\n        if (historyNum < workspace.length - 1) {\n            workspace[historyNum] = input.value;\n            historyNum++;\n            input.value = workspace[historyNum];\n        }\n        e.preventDefault();\n    }\n    else if (e.keyCode === 40) {\n        // down\n        if (historyNum > 0) {\n            workspace[historyNum] = input.value;\n            historyNum--;\n            input.value = workspace[historyNum];\n        }\n        e.preventDefault();\n    }\n};\nlet graphStop = false;\nlet graphDepth;\nlet curGraphDepth = 0;\nlet graphRunning = false;\nstartGraph.onclick = launchGraph;\nfunction launchGraph() {\n    if (graphRunning)\n        return;\n    makeLayout();\n    if (curlf === undefined)\n        return;\n    graphStop = false;\n    graphRunning = true;\n    curGraphDepth += graphDepth || 10;\n    let f = () => setTimeout(() => {\n        if (graphStop) {\n            makeLayout();\n            graphRunning = false;\n            return;\n        }\n        let ret = curlf.deepen(curGraphDepth);\n        if (ret === null) {\n            makeLayout();\n            graphRunning = false;\n            return;\n        }\n        let ans = [];\n        for (let n of ret.nodes) {\n            ans.push(node2cyObj(n));\n        }\n        for (let e of ret.edges) {\n            ans.push({\n                group: \"edges\",\n                data: { source: e.from.id.toString(), target: e.to.id.toString() },\n            });\n        }\n        makeLayout();\n        cy.add(ans);\n        f();\n        makeLayout();\n    }, 0);\n    f();\n}\nstopGraph.onclick = function () {\n    graphStop = true;\n};\nimgGraph.onclick = function () {\n    let a = document.createElement(\"a\");\n    a.download =\n        (curlf ? curlf.original.toString(true) : \"lambda-friends\") + \".png\";\n    console.log(a.download);\n    a.href = cy.png({\n        full: true,\n    });\n    document.body.appendChild(a);\n    a.click();\n    document.body.removeChild(a);\n    // console.log(a);\n};\nmaxDepth.addEventListener(\"change\", function () {\n    let new_s = parseInt(maxDepth.value);\n    if (!isNaN(new_s)) {\n        graphDepth = new_s;\n    }\n    else {\n        graphDepth = undefined;\n    }\n});\nlet graphActive = false;\ntabAbtn.addEventListener(\"click\", () => {\n    graphActive = false;\n});\ntabBbtn.addEventListener(\"click\", () => {\n    graphActive = false;\n});\ntabC1btn.addEventListener(\"click\", () => {\n    graphActive = false;\n});\ntabC2btn.addEventListener(\"click\", () => {\n    graphActive = false;\n});\ntabDbtn.addEventListener(\"click\", () => {\n    setTimeout(makeLayout, 10);\n    graphActive = true;\n});\nlmnInput.onkeydown = function (e) {\n    if (e.keyCode === 13) {\n        submitLMNtal();\n        e.preventDefault();\n    }\n};\nlmnSubmitBtn.onclick = submitLMNtal;\nfunction submitLMNtal() {\n    let input = lmnInput.value;\n    try {\n        let ret = lambda_friends_1.LambdaFriends.lmntal2LF(input);\n        lmnOutput.innerText = \"Found: \" + ret.expr.toString(true);\n    }\n    catch (e) {\n        lmnOutput.innerText = e.toString();\n    }\n}\ndeBrujinInput.onkeydown = function (e) {\n    if (e.keyCode === 13) {\n        submitDeBrujin();\n        e.preventDefault();\n    }\n};\ndeBrujinSubmitBtn.onclick = submitDeBrujin;\nfunction submitDeBrujin() {\n    let input = deBrujinInput.value;\n    try {\n        let ret = lambda_friends_1.LambdaFriends.deBrujin2LF(input);\n        deBrujinOutput.innerText = \"Found: \" + ret.expr.toString(true);\n    }\n    catch (e) {\n        deBrujinOutput.innerText = e.toString();\n    }\n}\ngraphInput.onkeydown = function (e) {\n    if (e.keyCode === 13) {\n        submitGraph();\n        e.preventDefault();\n    }\n};\ngraphSubmitBtn.onclick = submitGraph;\nfunction submitGraph() {\n    let input = graphInput.value;\n    try {\n        let ret = lambda_friends_1.LambdaFriends.graph2LF(input, allowMultipleEdges);\n        if (ret === null)\n            graphOutput.innerText = \"Not Found\";\n        else\n            graphOutput.innerText = \"Found: \" + ret.expr.toString(true);\n    }\n    catch (e) {\n        graphOutput.innerText = e.toString();\n    }\n}\nfunction output(str) {\n    oel.innerHTML = htmlEscape(str);\n}\nfunction outputLine(str) {\n    oel.innerHTML = htmlEscape(str + \"\\n\");\n}\nfunction outputNext(str) {\n    oel.insertAdjacentHTML(\"beforeend\", htmlEscape(str));\n}\nfunction outputNextLine(str) {\n    oel.insertAdjacentHTML(\"beforeend\", htmlEscape(str + \"\\n\"));\n}\nfunction outputClear() {\n    oel.innerText = \"\";\n}\nfunction refreshMacroList() {\n    let tbody = document.getElementById(\"macroList\");\n    tbody.innerHTML = \"\";\n    let ret = lambda_friends_1.LambdaFriends.getMacroListAsObject(typed);\n    for (let r in ret) {\n        let m = ret[r];\n        tbody.innerHTML +=\n            \"<tr><th>\" +\n                htmlEscape(m.name) +\n                \"</th><td>\" +\n                htmlEscape(m.expr.toString(true)) +\n                \"</td>\" +\n                (typed ? \"<td>\" + htmlEscape(m.type.toString()) + \"</td>\" : \"\") +\n                \"</tr>\";\n    }\n}\nfunction htmlEscape(str) {\n    return str.replace(/[&'`\"<> \\n]/g, function (match) {\n        return {\n            \"&\": \"&amp;\",\n            \"'\": \"&#x27;\",\n            \"`\": \"&#x60;\",\n            '\"': \"&quot;\",\n            \"<\": \"&lt;\",\n            \">\": \"&gt;\",\n            \" \": \"&nbsp;\",\n            \"\\n\": \"<br>\",\n        }[match];\n    });\n}\nfunction refreshTex() {\n    translateDiv.textContent = null;\n    if (curlf === undefined)\n        return;\n    let header = document.createElement(\"h4\");\n    header.innerText = curlf.getOriginalString();\n    translateDiv.appendChild(header);\n    translateDiv.appendChild(makeTexDiv(\"これまでの簡約過程\", curlf.getProcessTex()));\n    if (typed)\n        translateDiv.appendChild(makeTexDiv(\"型付けの証明木\", curlf.getProofTree()));\n    else {\n        translateDiv.appendChild(makeTexDiv(\"LMNtalコード\", curlf.toLMNtal()));\n        translateDiv.appendChild(makeTexDiv(\"SKIコンビネータ\", curlf.toSKI()));\n        translateDiv.appendChild(makeTexDiv(\"de Brujin Index\", curlf.toDeBrujin()));\n    }\n}\nfunction makeTexDiv(title, content) {\n    let p = document.createElement(\"p\");\n    let btn = document.createElement(\"button\");\n    let span = document.createElement(\"span\");\n    let code = document.createElement(\"div\");\n    let inner = document.createElement(\"p\");\n    code.classList.add(\"code\");\n    p.appendChild(btn);\n    p.appendChild(span);\n    code.appendChild(inner);\n    inner.innerText = content;\n    span.innerText = title;\n    btn.type = \"button\";\n    btn.className = \"btn btn-default btn-sm\";\n    btn.innerText = \"クリップボードにコピー\";\n    // btn.setAttribute(\"data-toggle\",\"popover\");\n    // btn.setAttribute(\"data-content\",\"Copied!\");\n    // $(function(){$('[data-toggle=\"popover\"]').popover();});\n    btn.onclick = function () {\n        let s = document.getSelection();\n        s.selectAllChildren(code);\n        document.execCommand(\"copy\");\n        s.collapse(document.body, 0);\n    };\n    let div = document.createElement(\"div\");\n    div.appendChild(p);\n    div.appendChild(code);\n    return div;\n}\nlet continualRunning = false;\nlet continualStop = false;\nfunction doContinual() {\n    if (continualRunning)\n        return;\n    continualRunning = true;\n    continualStop = false;\n    outputButtons.textContent = null;\n    let start = performance.now();\n    let f = (n) => setTimeout(() => {\n        if (n === 0 ||\n            curlf.isNormalForm(rightmost, innermost, weak, head) ||\n            continualStop) {\n            showContinueBtn();\n            tabA.scrollTop = oel.offsetHeight - 15;\n            continualRunning = false;\n            console.log(`Elapsed Time (Wall Clock): ${performance.now() - start} [ms]`);\n            refreshTex();\n            return;\n        }\n        let res = curlf.reductionByStrategy(rightmost, innermost, weak, head);\n        outputNextLine(res);\n        tabA.scrollTop = oel.offsetHeight - 15;\n        // refreshTex();\n        f(n - 1);\n    }, 0);\n    f(steps);\n}\nfunction showContinueBtn() {\n    outputButtons.textContent = null;\n    // 「さらに続ける」ボタンを表示\n    if (!curlf.hasNext())\n        return;\n    if (curlf.isNormalForm(rightmost, innermost, weak, head)) {\n        let s = document.createElement(\"span\");\n        s.innerText = \"指定の評価戦略ではこれが正規形です。\";\n        outputButtons.appendChild(s);\n    }\n    else {\n        let b = document.createElement(\"button\");\n        b.type = \"button\";\n        b.className = \"btn btn-default btn-sm\";\n        b.innerText = steps + \"ステップ簡約する\";\n        b.onclick = doContinual;\n        outputButtons.textContent = null;\n        outputButtons.appendChild(b);\n    }\n    if (typed)\n        return;\n    let span = document.createElement(\"span\");\n    span.innerText = \"または、以下から簡約基を選ぶ：\";\n    outputButtons.appendChild(span);\n    let div = document.createElement(\"div\");\n    div.className = \"list-group\";\n    outputButtons.appendChild(div);\n    let rs = curlf.getRedexes();\n    // console.log(rs);\n    for (let r of rs) {\n        let b = document.createElement(\"button\");\n        b.className = \"list-group-item code\";\n        b.innerHTML = r.toHTMLString();\n        b.onclick = function () {\n            outputNextLine(curlf.reduction(r));\n            showContinueBtn();\n            tabA.scrollTop = oel.offsetHeight - 15;\n            refreshTex();\n        };\n        div.appendChild(b);\n    }\n}\nfunction graphClear() {\n    cy.remove(\"*\");\n}\nfunction node2cyObj(n) {\n    return {\n        group: \"nodes\",\n        data: { id: \"\" + n.id, label: \"\" + n.toString() },\n        classes: (n.isNormalForm ? \"goal \" : \"\") + (n.isRoot ? \"root\" : \"\"),\n    };\n}\nfunction makeLayout() {\n    cy.resize();\n    cy.elements()\n        .makeLayout({\n        name: \"dagre\",\n        nodeSpacing: 5,\n        animate: true,\n        randomize: false,\n        maxSimulationTime: 1500,\n    })\n        .run();\n}\n// ===== initialize =====\nuntypedButton.onclick(null);\netaDisableButton.onclick(null);\nmultiEdgeDisableButton.onclick(null);\nleftmostButton.onclick(null);\noutermostButton.onclick(null);\nstrongButton.onclick(null);\nnonheadButton.onclick(null);\nrefreshMacroList();\n// ===== MAKESHIFT =====\nif (window.location.pathname.split(\"/\").slice(-1)[0] === \"fl.html\") {\n    typedButton.onclick(null);\n}\n\n\n//# sourceURL=webpack://lambda-friends/./js/webui.js?");
  
  /***/ }),
  
  /***/ "fs":
  /*!*********************!*\
    !*** external "fs" ***!
    \*********************/
  /***/ ((module) => {
  
  module.exports = require("fs");;
  
  /***/ })
  
  /******/ 	});
  /************************************************************************/
  /******/ 	// The module cache
  /******/ 	var __webpack_module_cache__ = {};
  /******/ 	
  /******/ 	// The require function
  /******/ 	function __webpack_require__(moduleId) {
  /******/ 		// Check if module is in cache
  /******/ 		var cachedModule = __webpack_module_cache__[moduleId];
  /******/ 		if (cachedModule !== undefined) {
  /******/ 			return cachedModule.exports;
  /******/ 		}
  /******/ 		// Create a new module (and put it into the cache)
  /******/ 		var module = __webpack_module_cache__[moduleId] = {
  /******/ 			// no module.id needed
  /******/ 			// no module.loaded needed
  /******/ 			exports: {}
  /******/ 		};
  /******/ 	
  /******/ 		// Execute the module function
  /******/ 		__webpack_modules__[moduleId](module, module.exports, __webpack_require__);
  /******/ 	
  /******/ 		// Return the exports of the module
  /******/ 		return module.exports;
  /******/ 	}
  /******/ 	
  /************************************************************************/
  /******/ 	
  /******/ 	// startup
  /******/ 	// Load entry module and return exports
  /******/ 	// This entry module can't be inlined because the eval devtool is used.
  /******/ 	var __webpack_exports__ = __webpack_require__("./js/webui.js");
  /******/ 	
  /******/ })()
  ;