Module Corelang__.Connector

val classify_atom : (string * 'a list) -> (string * 'a list, 'a * 'a) Stdlib.Either.t

アトムをコネクタかそうでないかで分類する

val partition_atoms : (string * Corelang__.Syntax.c_link list) list -> (string * Corelang__.Syntax.c_link list) list * (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) list

アトムのリストをコネクタかシンボルアトムかで分類する

val find_fusion : (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) -> (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) option

どちらか片方でも局所リンクに繋がれているような connector だった場合は Some で包んで返す

  • つまり，吸収可能なコネクタを識別する
  • 必ず，最初の要素が LocalLink であるようにする

Z[Y/X]

  • ただし，基本的に X は局所リンク（であるという前提）
  • 膜を貫く自由リンクが入ってきた場合は，自由リンクになるかも
val substitute_atom : (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) -> (string * Corelang__.Syntax.c_link list) -> string * Corelang__.Syntax.c_link list

p(X_1, ..., X_m)[Y/Z] ----> p(X_1, ..., X_m)[Y/Z]

val absorb_fusion : ((string * Corelang__.Syntax.c_link list) list * (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) list list * (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) list) -> ((string * Corelang__.Syntax.c_link list) list * (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) list list * (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) list) option

吸収可能なコネクタがあった場合は吸収して，Some で包んで返す

  • これは一個のコネクタに関してしか処理しない．再帰呼び出しは whileM とかを後で使う
  • free_connectors は元々のアトムのリスト中に出現したコネクタのリストを反転させたもののリストを反転させたもの
parameter symbol_atoms

シンボルアトムのリスト

parameter free_connectors

引数が全て自由リンクなコネクタ（substitution もできない）のリストのリスト

parameter connectors

引数に局所リンクが残っている（かも知れない）コネクタのリスト

returns

(シンボルアトムのリスト，引数が全て自由リンクなコネクタのリストのリスト)

val free_connector_of : (Corelang__.Syntax.c_link * Corelang__.Syntax.c_link) -> string * string

両方自由リンクに繋がれているコネクタを引数に取り，FreeLink コンストラクタを剥がす

  • 局所リンクが引数に来た場合はエラー
  • 必ず，吸収可能なコネクタを全て吸収し終えた後に呼ぶ
val normalize : (string * Corelang__.Syntax.c_link list) list -> (string * Corelang__.Syntax.c_link list) list * (string * string) list

どちらか片方でも閉じたリンクを繋げるコネクタを吸収させる

  • アトムのリストを左から舐めていって，すでに吸収可能なコネクタが存在しないことがわかったものは absorbed_atoms に追加してやる
  • コネクタの吸収は，必ず局所リンクを substitution するので 吸収可能なコネクタではなかったもの（両方とも自由リンクに接続されていたコネクタ）が， substitution によって，吸収可能になることはない
  • absorbed_atoms はアトムのリストのリストになっている