プログラマー向けの（？）数理論理学（３）ウェブアプリ化

プログラマー向けの（？）数理論理学（３）ウェブアプリ化:

プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません（形式化数学についてはこちらの記事もどうぞ）。

この記事はプログラムの実装についての記事なので、プログラミングに興味のない方は飛ばして次の記事に進んでください。

なお、ソースコード全体はGitHubにあります。

https://github.com/pizyumi/rena

前回以前の記事

実装内容

ここまで作ってきたプログラムは実際の証明を行うツールとしては貧弱なので、幾つか便利な機能を追加してもう少し使いやすいものにしていきます。また、同時にウェブアプリ化も行います。

主な変更点や実装内容は下のようになります。

ウェブアプリ化
複数のコマンドの実行
コマンドのオートコンプリート
定理の名称や説明などの入力
定理の保存
保存した定理の閲覧

また、全体の外観は下のようになります。

ウェブアプリ化

今までのプログラムは単なるHTMLページとして実装しており、ウェブアプリにはなっていませんでした。

今後様々な機能を追加することを考えると、ウェブアプリ化しておいた方が間違いなく都合が良いですので、ウェブアプリ化を行います。

複数のコマンドの実行

今までコマンドは1つずつ順番に入力する方式でしたが、はっきり言って面倒です。

複数のコマンドを一気に実行できた方が便利です。

そこで下のようなテキストエリアと「再実行」ボタンを追加します。

「再実行」ボタンを押すと、それまでに作成した数学的言明や証明を表すオブジェクトを全て破棄し、テキストエリアに入力されているコマンドに従ってオブジェクトの作成を最初からやり直します。

コマンドのオートコンプリート

毎回コマンド名をフルで入力するのは面倒ですし、コマンド名を正確に覚えておくのも面倒ですので、コマンド入力テキストボックスにオートコンプリート機能を追加します。

定理の名称や説明などの入力

定理の名称や説明などの定理に関するメタデータを入力できるようにします。

取り敢えず定理の名称と説明だけを入力できるようにしましたが、今後更に項目を増やすこともあるかもしれません。

定理の保存

今まで、証明した定理の証明の内容を保存するような機能はありませんでした。

ユーザー側で何らかの形で自分で保存を行わなければならないのは面倒過ぎますので、証明した定理を保存できる機能を実装します。

「保存」ボタンを追加し、「保存」ボタンを押すと、現在作成している定理を保存するようにします。

保存した定理の閲覧

保存した定理は画面左側のリストに表示されるようにし、リスト内の定理をクリックするとその定理の内容が表示されるようにします。

また、「新規作成」ボタンをクリックすると、新しい定理の証明を開始することができます。

Git

実装内容が分かったところで早速プログラミング作業に入っていきたいと思いますが、今後のことを考えてGitを導入しておくことにしましょう。

プログラムを格納するための適当なフォルダを用意し、git initします。

C:\work2018\mathmatics>git init 
Initialized empty Git repository in C:/work2018/mathmatics/.git/

また、プログラムを格納するフォルダに下のような.gitignoreファイルを追加します。

asset/lib/ 
data/ 
data_back/ 
doc/ 
node_modules/

NPM

ウェブアプリ化に当たって、今後このプログラムはNode.jsアプリケーションとして実装していくことにします。

なので、まずプログラムを格納するフォルダにおいて下のようにnpm initします。

C:\work2018\mathmatics>npm init 
This utility will walk you through creating a package.json file. 
It only covers the most common items, and tries to guess sensible defaults. 
 
See `npm help json` for definitive documentation on these fields 
and exactly what they do. 
 
Use `npm install <pkg> --save` afterwards to install a package and 
save it as a dependency in the package.json file. 
 
Press ^C at any time to quit. 
name: (math) rena 
version: (1.0.0) 
description: fomalized mathmatics software 
entry point: (index.js) app.js 
test command: 
git repository: 
keywords: 
author: Yurina Washida 
license: (ISC) 
About to write to C:\work2018\mathmatics\package.json: 
 
{ 
  "name": "rena", 
  "version": "1.0.0", 
  "description": "fomalized mathmatics software", 
  "main": "app.js", 
  "scripts": { 
    "test": "echo \"Error: no test specified\" && exit 1" 
  }, 
  "author": "Yurina Washida", 
  "license": "ISC" 
} 
 
 
Is this ok? (yes) y

また、今後利用するパッケージをインストールするために下のようにnpm installします。

C:\work2018\mathmatics>npm install --save bluebird 
rena@1.0.0 C:\work2018\mathmatics 
`-- bluebird@3.5.2 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save body-parser 
rena@1.0.0 C:\work2018\mathmatics 
`-- body-parser@1.18.3 
  +-- bytes@3.0.0 
  +-- content-type@1.0.4 
  +-- debug@2.6.9 
  | `-- ms@2.0.0 
  +-- depd@1.1.2 
  +-- http-errors@1.6.3 
  | +-- inherits@2.0.3 
  | +-- setprototypeof@1.1.0 
  | `-- statuses@1.5.0 
  +-- iconv-lite@0.4.23 
  | `-- safer-buffer@2.1.2 
  +-- on-finished@2.3.0 
  | `-- ee-first@1.1.1 
  +-- qs@6.5.2 
  +-- raw-body@2.3.3 
  | `-- unpipe@1.0.0 
  `-- type-is@1.6.16 
    +-- media-typer@0.3.0 
    `-- mime-types@2.1.21 
      `-- mime-db@1.37.0 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save co 
rena@1.0.0 C:\work2018\mathmatics 
`-- co@4.6.0 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save express 
rena@1.0.0 C:\work2018\mathmatics 
`-- express@4.16.4 
  +-- accepts@1.3.5 
  | `-- negotiator@0.6.1 
  +-- array-flatten@1.1.1 
  +-- content-disposition@0.5.2 
  +-- cookie@0.3.1 
  +-- cookie-signature@1.0.6 
  +-- encodeurl@1.0.2 
  +-- escape-html@1.0.3 
  +-- etag@1.8.1 
  +-- finalhandler@1.1.1 
  | `-- statuses@1.4.0 
  +-- fresh@0.5.2 
  +-- merge-descriptors@1.0.1 
  +-- methods@1.1.2 
  +-- parseurl@1.3.2 
  +-- path-to-regexp@0.1.7 
  +-- proxy-addr@2.0.4 
  | +-- forwarded@0.1.2 
  | `-- ipaddr.js@1.8.0 
  +-- range-parser@1.2.0 
  +-- safe-buffer@5.1.2 
  +-- send@0.16.2 
  | +-- destroy@1.0.4 
  | +-- mime@1.4.1 
  | `-- statuses@1.4.0 
  +-- serve-static@1.13.2 
  +-- statuses@1.4.0 
  +-- utils-merge@1.0.1 
  `-- vary@1.1.2 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save fs-extra 
rena@1.0.0 C:\work2018\mathmatics 
`-- fs-extra@7.0.0 
  +-- graceful-fs@4.1.15 
  +-- jsonfile@4.0.0 
  `-- universalify@0.1.2 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save morgan 
rena@1.0.0 C:\work2018\mathmatics 
`-- morgan@1.9.1 
  +-- basic-auth@2.0.1 
  `-- on-headers@1.0.1 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save p-iteration 
rena@1.0.0 C:\work2018\mathmatics 
`-- p-iteration@1.1.7 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save strip-bom 
rena@1.0.0 C:\work2018\mathmatics 
`-- strip-bom@3.0.0 
 
npm WARN rena@1.0.0 No repository field. 
 
C:\work2018\mathmatics>npm install --save underscore 
rena@1.0.0 C:\work2018\mathmatics 
`-- underscore@1.9.1 
 
npm WARN rena@1.0.0 No repository field.

これで、下のような内容のpackage.jsonが作成されます。

{ 
  "name": "rena", 
  "version": "1.0.0", 
  "description": "fomalized mathmatics software", 
  "main": "app.js", 
  "scripts": { 
    "test": "echo \"Error: no test specified\" && exit 1" 
  }, 
  "author": "Yurina Washida", 
  "license": "ISC", 
  "dependencies": { 
    "bluebird": "^3.5.2", 
    "body-parser": "^1.18.3", 
    "co": "^4.6.0", 
    "express": "^4.16.4", 
    "fs-extra": "^7.0.0", 
    "morgan": "^1.9.1", 
    "p-iteration": "^1.1.7", 
    "strip-bom": "^3.0.0", 
    "underscore": "^1.9.1" 
  } 
}

フォルダ構造

プログラムを格納するフォルダの構造は下のようにします。

ここで/asset/libフォルダの配下にあるのはウェブページにおいて利用するライブラリであり、下のようなものです。

Vue.js
Bootstrap
jQuery
Popper.js
Underscore.js
axios

それぞれ適切に導入してください。

common.js

次にバックエンド側の共通的な処理を実装するcommon.jsファイルを追加します。下のようになります。

ファイル関係の処理やHTTPリクエストを返す処理などが実装されています。

var _ = require('underscore'); 
var bluebird = require('bluebird'); 
var fsextra = bluebird.promisifyAll(require('fs-extra')); 
var pi = require('p-iteration'); 
var stripbom = require('strip-bom'); 
 
var fs = bluebird.promisifyAll(require('fs')); 
var http = require('http'); 
var path = require('path'); 
 
var common = {}; 
 
common = _.extend(common, { 
  load_text_from_path: async (p) => { 
    return stripbom(await fs.readFileAsync(p, 'utf-8')); 
  }, 
  load_json_from_path: async (p) => { 
    return JSON.parse(await common.load_text_from_path(p)); 
  }, 
  save_text_to_path: async (p, text) => { 
    await fsextra.mkdirsAsync(path.dirname(p)); 
    await fs.writeFileAsync(p, text, 'utf-8'); 
  }, 
  save_json_to_path: async (p, json) => { 
    await common.save_text_to_path(p, JSON.stringify(json)); 
  }, 
  load_files_folders_from_path: async (p) => { 
    return _(await fs.readdirAsync(p)).map((v) => path.join(p, v)); 
  }, 
  load_files_from_path: async (p) => { 
    return pi.filterSeries(await common.load_files_folders_from_path(p), async (v) => (await fs.statAsync(v)).isFile()); 
  } 
}); 
 
common = _.extend(common, { 
  send_res_with_message: async (res, status, message) => { 
    res.type('text/plain; charset=utf-8'); 
    res.status(status); 
    res.send((message ? message : http.STATUS_CODES[status]) + '\r\n'); 
  }, 
  send_res_with_json: async (res, json) => { 
    res.json(json); 
  }, 
  send_res_with_html: async (res, html) => { 
    res.type('text/html; charset=utf-8'); 
    res.status(200); 
    res.send(html); 
  }, 
  send_res_with_html_from_path: async (res, p) => { 
    var html = await common.load_text_from_path(p); 
    await common.send_res_with_html(res, html); 
  } 
}); 
 
module.exports = common;

app.js

次にバックエンド本体を実装します。下のようになります。

Expressを利用してウェブアプリケーションを作成しています。

そして、主に下のようなルートを設定しています。

/・・・main.htmlを返します。
/list・・・保存されている全ての定理の名称のリストをJSON形式で返します。
/load・・・nameクエリに指定された名称の定理のデータをJSON形式で返します。
/save・・・受け取ったJSON形式のデータをnameクエリに指定された名称の定理のデータとして保存します。

var _ = require('underscore'); 
var bluebird = require('bluebird'); 
var bodyparser = require('body-parser'); 
var co = require('co'); 
var express = require('express'); 
var morgan = require('morgan'); 
 
var path = require('path'); 
 
var common = require('./common'); 
 
co(function* () { 
  var server = yield start_server(); 
  server.on('error', (err) => { 
    console.error(err); 
    process.exit(1); 
  }); 
 
  var end_server_once = _.once(end_server); 
 
  console.log('http server is running...press enter key to exit.'); 
  process.on('SIGTERM', () => { 
    co(function* () { 
      yield end_server_once(server); 
      process.exit(0); 
    }); 
  }); 
  process.stdin.on('data', (data) => { 
    if (data.indexOf('\n') !== -1) { 
      co(function* () { 
        yield end_server_once(server); 
        process.exit(0); 
      }); 
    } 
  }); 
}).catch((err) => { 
  console.error(err); 
  process.exit(1); 
}); 
 
function start_server () { 
  return co(function* () { 
    var server = yield create_server({}); 
    return server; 
  }); 
} 
 
function create_server (poption) { 
  return new bluebird((resolve, reject) => { 
    co(function* () { 
      var option = _.extend(poption, { 
        port: 3000 
      }); 
 
      var jsonparser = bodyparser.json(); 
 
      var app = express(); 
      app.set('x-powered-by', false); 
      app.set('case sensitive routing', true); 
      app.set('strict routing', true); 
      app.use(morgan('dev')); 
      app.use('/asset', express.static('asset')); 
      app.get('/', (req, res, next) => { 
        co(function* () { 
          var p = path.join('front', 'main.html'); 
          yield common.send_res_with_html_from_path(res, p); 
        }).catch(next); 
      }); 
      app.get('/list', (req, res, next) => { 
        co(function* () { 
          var p = 'data'; 
 
          var list = _(yield common.load_files_from_path(p)).map((e) => path.basename(e, path.extname(e))); 
          yield common.send_res_with_json(res, list); 
        }).catch(next); 
      }); 
      app.get('/load', (req, res, next) => { 
        co(function* () { 
          var name = req.query.name; 
 
          var p = path.join('data', name + '.json'); 
 
          var data = yield common.load_json_from_path(p); 
          yield common.send_res_with_json(res, data); 
        }).catch(next); 
      }); 
      app.post('/save', jsonparser, (req, res, next) => { 
        co(function* () { 
          var name = req.query.name; 
          var data = req.body; 
 
          var p = path.join('data', name + '.json'); 
 
          yield common.save_json_to_path(p, data); 
          yield common.send_res_with_message(res, 200); 
        }).catch(next); 
      }); 
      app.get('*', (req, res, next) => next({ status: 404 })); 
      app.post('*', (req, res, next) => next({ status: 404 })); 
      app.all('*', (req, res, next) => next({ status: 405 })); 
      app.use((err, req, res, next) => { 
        co(function* () { 
          if (err.status) { 
            yield common.send_res_with_message(res, err.status, err.message); 
          } 
          else { 
            yield common.send_res_with_message(res, 500); 
 
            console.error(err); 
          } 
        }).catch(next); 
      }); 
      var server = app.listen(option.port, () => { 
        resolve(server); 
      }); 
      server.once('error', (err) => { 
        reject(err); 
      }); 
    }).catch((err) => { 
      reject(err); 
    }); 
  }); 
} 
 
function end_server (server) { 
  return new bluebird((resolve, reject) => { 
    console.log('http server is closing...'); 
    server.close(() => { 
      console.log('http server closed.'); 
      resolve(server); 
    }); 
  }); 
}

main.html

次にmain.htmlHTMLページを追加します。下のようになります。

前回までの記事で作成していたHTMLページを改造したものになっていますが、原形を留めないほどに変わっています。

<!DOCTYPE html> 
<html lang="ja"> 
<head> 
  <meta charset="utf-8"> 
  <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no"> 
  <title>形式化数学</title> 
  <link rel="stylesheet" href="/asset/lib/bootstrap-4.0.0/css/bootstrap.min.css"> 
  <style> 
html { 
  height:100%; 
} 
 
body { 
  height:100%; 
} 
 
#main { 
  height:100%; 
  display: flex; 
  align-items: stretch; 
} 
 
#list { 
  width: 15%; 
} 
 
#split1 { 
  width: 2px; 
  background: black; 
} 
 
#proof { 
  width: 50%; 
  margin: 4px; 
} 
 
#split2 { 
  width: 2px; 
  height: 100%; 
  background: black; 
} 
 
#info { 
  width: 30%; 
} 
 
#err { 
  color: red; 
} 
 
.space { 
  width: 64px; 
} 
 
textarea { 
  height: 96px; 
} 
  </style> 
</head> 
<body> 
  <script src="/asset/lib/jquery-3.2.1/jquery-3.2.1.min.js"></script> 
  <script src="/asset/lib/popper-1.0.1/popper.min.js"></script> 
  <script src="/asset/lib/bootstrap-4.0.0/js/bootstrap.min.js"></script> 
  <script src="/asset/lib/vue-2.5.13/vue.min.js"></script> 
  <script src="/asset/lib/axios-0.17.1/axios.min.js"></script> 
  <script src="/asset/lib/underscore-1.8.3/underscore-min.js"></script> 
 
  <div id="main" v-show="loaded"> 
    <div id="list"> 
      <ul v-for="l in list" class="list-group" :key="l.id"> 
        <li class="list-group-item" @click="load_theorem(l.name)">{{ l.name }}</li> 
      </ul> 
      <button class="btn btn-primary" @click="new_theorem">新規作成</button> 
    </div> 
    <div id="split1"> 
    </div> 
    <div id="proof"> 
      <div> 
        <textarea class="form-control" v-model="inputs"></textarea> 
        <button class="btn btn-primary" @click="execute_commands">再実行</button> 
      </div> 
      <div> 
        <input class="form-control" type="text" autocomplete="on" list="commands" v-model="input" @keydown.enter="execute_command"> 
        <datalist id="commands"> 
          <option value="conj"> 
          <option value="disj"> 
          <option value="equiv"> 
          <option value="imp"> 
          <option value="imp_elim"> 
          <option value="imp_intro"> 
          <option value="neg"> 
          <option value="prem"> 
          <option value="prop"> 
        </datalist> 
        <div id="err">{{ err }}</div> 
        <button class="btn btn-primary" @click="execute_command">実行</button> 
      </div> 
      <table> 
        <tbody> 
          <tr v-for="output in outputs" :key="output.id"> 
            <td v-html="output.index"></td> 
            <td v-html="output.html"></td> 
            <td class="space"></td> 
            <td v-html="output.command"></td> 
          </tr> 
        </tbody> 
      </table> 
    </div> 
    <div id="split2"> 
    </div> 
    <div id="info"> 
      <div class="form-group"> 
        <label>名称：</label> 
        <input class="form-control" type="text" v-model="name"> 
      </div> 
      <div class="form-group"> 
        <label>説明：</label> 
        <textarea class="form-control" v-model="description"></textarea> 
      </div> 
      <button class="btn btn-primary" @click="save_theorem">保存</button> 
    </div> 
  </div> 
 
  <script src="/asset/js/math.js"></script> 
  <script src="/asset/js/interface.js"></script> 
  <script src="/asset/js/main.js"></script> 
</body> 
</html>

interface.js

次にinterface.jsを追加します。下のようになります。

主にコマンドを解釈するコードです。

function initialize_context (context) { 
    context.pindex = 0; 
    context.sindex = 0; 
    context.ss = new Map(); 
} 
 
function execute_command (context, command) { 
  var cs = command.split(' '); 
 
  if (cs[0] === 'prop') { 
    context.pindex++; 
    var p = create_proposition(context.pindex); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'neg') { 
    var objs = get_n_objects_from_args(context, 1, cs); 
    var p = create_negation(objs[0]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'conj') { 
    var objs = get_n_objects_from_args(context, 2, cs); 
    var p = create_conjunction(objs[0], objs[1]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'disj') { 
    var objs = get_n_objects_from_args(context, 2, cs); 
    var p = create_disjunction(objs[0], objs[1]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'imp') { 
    var objs = get_n_objects_from_args(context, 2, cs); 
    var p = create_implication(objs[0], objs[1]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'equiv') { 
    var objs = get_n_objects_from_args(context, 2, cs); 
    var p = create_equivalence(objs[0], objs[1]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'prem') { 
    var objs = get_n_objects_from_args(context, 1, cs); 
    var p = create_premise(objs[0]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'imp_elim') { 
    var objs = get_n_objects_from_args(context, 2, cs); 
    var p = create_implication_elimination(objs[0], objs[1]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else if (cs[0] === 'imp_intro') { 
    var objs = get_n_objects_from_args(context, 2, cs); 
    var p = create_implication_introduction(objs[0], objs[1]); 
 
    add_object(context, p); 
 
    return p; 
  } 
  else { 
    throw new Error('not supported command.'); 
  } 
} 
 
function add_object (context, obj) { 
  context.sindex++; 
  context.ss.set(context.sindex, obj); 
} 
 
function get_n_objects_from_args (context, n, cs) { 
  check_num_arguments(cs, n); 
 
  var objs = []; 
  for (var i = 0; i < n; i++) { 
    var idx = get_int_argument(cs[1 + i]); 
    check_in_range(idx, context.sindex); 
    var obj = context.ss.get(idx); 
    objs.push(obj); 
  } 
 
  return objs; 
} 
 
function check_num_arguments (cs, num) { 
  if (cs.length < num + 1) { 
    throw new Error('missing argument.'); 
  } 
} 
 
function get_int_argument (arg) { 
  var i = parseInt(arg); 
  if (isNaN(i)) { 
    throw new Error('not integer.'); 
  } 
  return i; 
} 
 
function check_in_range (arg, max) { 
  if (arg < 1 || arg > max) { 
    throw new Error('out of range.'); 
  } 
}

main.js

次にmain.jsを追加します。下のようになります。

主にVue.js関連部分が変わっています。

function get_query() 
{ 
    var vars = [], max = 0, hash = "", array = ""; 
    var url = window.location.search; 
 
    hash  = url.slice(1).split('&'); 
    max = hash.length; 
    for (var i = 0; i < max; i++) { 
        array = hash[i].split('='); 
        vars.push(array[0]); 
        vars[array[0]] = array[1]; 
    } 
 
    return vars; 
} 
 
var query = get_query(); 
var id = 0; 
 
var context = {}; 
 
initialize_context(context); 
 
var vm = new Vue({ 
  el: '#main', 
  data: { 
        loaded: false, 
    list: [], 
    input: '', 
    inputs: '', 
    outputs: [], 
    commands: [], 
    err: '', 
    name: '', 
    description: '' 
  }, 
  computed: { 
    command_text: function () { 
      return this.commands.join('\n'); 
    } 
  }, 
  methods:  { 
    execute_command: function () { 
      var command = this.input; 
      this.input = ''; 
 
      try { 
        var obj = execute_command(context, command); 
        if (obj != undefined && obj != null) { 
          id++; 
          this.outputs.unshift({ 
            id: id, 
            index: '[' + id + ']', 
            html: tohtml(obj), 
            command: command 
          }); 
          this.commands.push(command); 
          this.inputs = this.command_text; 
          this.err = ''; 
        } 
      } 
      catch (err) { 
        this.err = err.message; 
      } 
    }, 
    execute_commands: function () { 
      id = 0; 
      this.outputs = []; 
      this.commands = []; 
 
            initialize_context(context); 
 
      var commands = this.inputs.split('\n'); 
      for (var i = 0; i < commands.length; i++) { 
        try { 
          var obj = execute_command(context, commands[i]); 
          if (obj != undefined && obj != null) { 
            id++; 
            this.outputs.unshift({ 
              id: id, 
              index: '[' + id + ']', 
              html: tohtml(obj), 
              command: commands[i] 
            }); 
            this.commands.push(commands[i]); 
          } 
        } 
        catch (err) { 
        } 
      } 
    }, 
        load_theorem: function (name) { 
            window.location.href = '?name=' + name; 
        }, 
    save_theorem: function () { 
      var data = { 
        commands: this.commands, 
        name: this.name, 
        description: this.description 
      }; 
      axios.post('/save?name=' + this.name, data).then((res) => { 
        window.location.href = '?name=' + this.name; 
      }).catch((err) => { 
      }); 
    }, 
        new_theorem: function () { 
            window.location.href = '?name='; 
        } 
  } 
}); 
 
axios.get('/list', {}).then((res) => { 
    vm.list = _(res.data).map(function (e, i) { 
        return { 
            id: i, 
            name: e, 
            active: e === query.name 
        }; 
    }); 
 
    if (query.name) { 
        axios.get('/load?name=' + query.name, {}).then((res) => { 
            vm.name = res.data.name; 
            vm.description = res.data.description; 
 
            var commands = res.data.commands; 
            for (var i = 0; i < commands.length; i++) { 
                try { 
                    var obj = execute_command(context, commands[i]); 
                    if (obj != undefined && obj != null) { 
                        id++; 
                        vm.outputs.unshift({ 
                            id: id, 
                            index: '[' + id + ']', 
                            html: tohtml(obj), 
                            command: commands[i] 
                        }); 
                        vm.commands.push(commands[i]); 
                    } 
                } 
                catch (err) { 
                } 
            } 
            vm.inputs = vm.command_text; 
            vm.loaded = true; 
        }).catch((err) => { 
        }).finally(() => { 
        }); 
    } 
    else { 
        vm.loaded = true; 
    } 
}).catch((err) => { 
}).finally(() => { 
});

math.js

最後に、math.jsは前回までに作成したものと全く同じです。

プログラムの実行

これでプログラムが完成しました。

プログラムを実行するにはプログラムを格納しているフォルダでnode app.jsします。

C:\work2018\mathmatics>node app.js 
http server is running...press enter key to exit.

そして、ブラウザでhttp://localhost:3000/にアクセスすると、プログラムの画面が表示され、定理の証明を開始することができます。

今回はここまでにします。次回は証明図というものについて説明し、プログラムに証明図を表示する機能を追加したいと思います。

このブログを検索

IT音痴アラフィフおやじのストック記事倉庫