unification.js

//@flow

const unify = (() => {
  const isValueType = o =>
    typeof o === 'boolean'
    || typeof o === 'string'
    || (typeof o === 'number' && !isNaN(o))
  const toJson = elem => {
    if (Array.isArray(elem)) {
      const elems = elem.map(i => toJson(i))
      const list = String(elems.join(''))
      return `[${list}]`
    }
    if (typeof elem === 'string') {
      return `"${elem}"`
    }
    if (typeof elem === 'object' && elem !== null) {
      let results = ''
      for (const e in elem) {
        results += `${e}:${toJson(elem[e])}`
      }
      return results
    }
    if (typeof elem === 'undefined') {
      return 'undefined'
    } else if (elem === null) {
      return 'null'
    } else {
      return elem.toString()
    }
  }
  class DictFlag {
    toString() {
      return 'DICT_FLAG'
    }
  }
  const DICT_FLAG = new DictFlag()
  class Box {
    value: *
    constructor(v) {
      if (isValueType(v) || v === null) {
        this.value = v
      } else {
        throw `Can only box value types, not ${toJson(v)}`
      }
    }

    toString() {
      return toJson(this.value)
    }
  }
  let g_hidden_var_counter = 1
  const HIDDEN_VAR_PREFIX = '__HIDDEN__'
  const isHiddenVar = name =>
    name.slice(0, HIDDEN_VAR_PREFIX.length) === HIDDEN_VAR_PREFIX
  class Variable {
    name: string
    constructor(name: string, typeFunc) {
      this.typeFunc = typeFunc != null ? typeFunc : null
      this.isListVar = name[0] === '$'
      if (this.isListVar) {
        name = name.substring(1)
      }
      if (name === '_') {
        this.name = HIDDEN_VAR_PREFIX + g_hidden_var_counter
        g_hidden_var_counter += 1
      } else {
        this.name = name
      }
    }

    isHiddenVar() {
      return isHiddenVar(this.name)
    }

    toString() {
      return `Variable(${toJson(this.name)})`
    }
  }
  class TreeTin {
    changes = []
    varlist: {[string]: *}
    constructor(node, varlist) {
      this.node = node
      this.varlist = varlist
    }

    toString() {
      return toJson(this.node)
    }

    get(varName, maxDepth: number) {
      let vartin = this.varlist[varName]
      if (!vartin) {
        throw `Variable ${varName} not in this tin`
      }
      vartin = vartin.endOfChain()
      if (!vartin.node) {
        return new Variable(vartin.name)
      } else {
        return unboxit(vartin.node, vartin.varlist, maxDepth)
      }
    }

    getAll(maxDepth) {
      const j = {}
      for (const key in this.varlist) {
        if (!isHiddenVar(key)) {
          j[key] = this.get(key, maxDepth)
        }
      }
      return j
    }

    unbox(maxDepth) {
      return unboxit(this.node, this.varlist, maxDepth)
    }

    unify(tin) {
      if (!(tin instanceof TreeTin)) {
        tin = box(tin)
      }
      const changes = []
      const success = _unify(
        this.node,
        this.varlist,
        tin.node,
        tin.varlist,
        changes,
      )
      if (success) {
        this.changes.push(...changes)
        tin.changes.push(...changes)
        return [this, tin]
      } else {
        for (const change of changes) {
          change()
        }
        return null
      }
    }

    bind(varName, expr) {
      const vartin = this.varlist[varName].endOfChain()
      if (!vartin.isfree()) {
        return null
      }
      if (!(expr instanceof TreeTin)) {
        expr = box(expr)
      }
      const changes = []
      if (bind(vartin, expr.node, expr.varlist, changes)) {
        this.changes.push(...changes)
        expr.changes.push(...changes)
        return [this, expr]
      }
      return null
    }

    rollback() {
      for (const change of this.changes) {
        change()
      }
      this.changes.length = 0
    }
  }

  class VarTin {
    chainlength = 1
    name: string
    constructor(name: string, node, varlist, typeFunc) {
      this.name = name
      this.node = node != null ? node : null
      this.varlist = varlist != null ? varlist : null
      this.typeFunc = typeFunc != null ? typeFunc : null
    }

    endOfChain() {
      let t = this
      while (t.varlist instanceof VarTin) {
        t = t.varlist
      }
      return t
    }

    isfree() {
      const t = this.endOfChain()
      return t.node === null && t.varlist === null
    }

    isHiddenVar() {
      return isHiddenVar(this.name)
    }

    toString() {
      return `VarTin(${toJson(this.name)})`
    }

    unbox(maxDepth) {
      if (this.node) {
        return unboxit(this.node, this.varlist, maxDepth)
      } else {
        return new Variable(this.name)
      }
    }
  }
  const unboxit = (tree, varlist, maxDepth) => {
    let tin
    if (maxDepth == null) {
      maxDepth = -1
    }
    if (maxDepth === 0) {
      return tree
    }
    if (Array.isArray(tree)) {
      if (tree.length > 0 && tree[tree.length - 1] === DICT_FLAG) {
        const hash = {}
        const _ref = tree.slice(0, tree.length - 1)

        for (const e of _ref) {
          hash[unboxit(e[0], varlist, maxDepth - 1)] = unboxit(
            e[1],
            varlist,
            maxDepth - 1,
          )
        }

        return hash
      } else {
        return tree.map(i => unboxit(i, varlist, maxDepth - 1))
      }
    } else if (tree instanceof Box) {
      return tree.value
    } else if (tree instanceof Variable) {
      if (varlist !== void 0) {
        try {
          tin = get_tin(varlist, tree)
        } catch (error) {
          return tree
        }
        if (tin.node != null && tin.varlist != null) {
          return unboxit(tin.node, tin.varlist, maxDepth - 1)
        } else {
          return tree
        }
      } else {
        return tree
      }
    }
    throw `Unrecognized type '${typeof tree}' in unbox.`
  }
  const boxit = (elem, varlist) => {
    if (elem instanceof Variable) {
      if (varlist[elem.name] != null) {
        if (elem.typeFunc != null && varlist[elem.name].typeFunc != null) {
          if (elem.typeFunc !== varlist[elem.name].typeFunc) {
            throw 'A single variable can not be defined with two diffrent types!'
          }
        } else if (elem.typeFunc != null) {
          varlist[elem.name].typeFunc = elem.typeFunc
        }
      } else {
        varlist[elem.name] = new VarTin(elem.name, null, null, elem.typeFunc)
      }
      return elem
    } else if (elem instanceof Box) {
      return elem
    } else if (Array.isArray(elem)) {
      let hasListVar = false
      const ret = elem.map(i => {
        if (i instanceof Variable && i.isListVar) {
          if (hasListVar) {
            throw 'There can only be one list variable in an array!'
          }
          hasListVar = true
        }
        return boxit(i, varlist)
      })
      ret.hasListVar = hasListVar
      return ret
    } else if (typeof elem === 'object' && elem !== null) {
      const a = []
      for (const key in elem) {
        a.push([boxit(key, varlist), boxit(elem[key], varlist)])
      }
      a.push(DICT_FLAG)
      return a.sort()
    } else if (isValueType(elem || elem === null)) {
      return new Box(elem)
    } else {
      return `Unrecognized type '${typeof elem}' in box.`
    }
  }
  /**
   * This function boxes an object.
   * Before an object can be processed it must be "boxed"
   * this consits of wrapping all value types in objects
   * and converting all objects to arrays
   */
  const box = elem => {
    if (elem instanceof TreeTin) {
      return elem
    }
    const varlist = {}
    const tree = boxit(elem, varlist)
    return new TreeTin(tree, varlist)
  }
  const get_tin = (varlist, node) => {
    if (!(node instanceof Variable)) {
      throw 'Node must be a Variable to get_tin!'
    }
    if ((varlist != null ? varlist[node.name] : void 0) != null) {
      return varlist[node.name]
    }
    throw `Couldn't find node ${node.name} in varlist ${varlist}`
  }
  const bind = (t, node, varlist, changes) => {
    let called
    let unboxed
    t = t.endOfChain()
    if (!t.isfree()) {
      return false
    }
    if (t.typeFunc !== null) {
      unboxed = unboxit(node, varlist, t.typeFunc.maxDepth)
      if (unboxed instanceof Variable && Variable.typeFunc !== t.typeFunc) {
        return false
      } else if (!t.typeFunc(unboxed)) {
        return false
      }
    }
    t.node = node
    t.varlist = varlist
    called = false
    changes.push(() => {
      if (called) {
        return
      }
      called = true
      t.node = null
      t.varlist = null
      t.chainlength = 1
    })
    return true
  }
  const bind_tins = (t1, t2, changes) => {
    if (!t1.isfree() && !t2.isfree()) {
      return false
    } else if (t1.isfree() && !t2.isfree()) {
      return bind(t1, t2.node, t2.varlist, changes)
    } else if (!t1.isfree() && t2.isfree()) {
      return bind(t2, t1.node, t1.varlist, changes)
    } else if (t2.chainlength < t1.chainlength) {
      t2.chainlength += 1
      return bind(t2, null, t1, changes)
    } else {
      t1.chainlength += 1
      return bind(t1, null, t2, changes)
    }
  }
  const _unify = (n1, v1, n2, v2, changes) => {
    let idx
    let idx1
    let idx2
    let n1RealLength
    let n2RealLength
    let t1
    let t2
    if (changes == null) {
      changes = []
    }
    if (n1 === void 0 && n2 === void 0) {
      return true
    } else if (n1 === null && n2 === null) {
      return true
    } else if (n1 === null || n2 === null) {
      return false
    } else if (n1 instanceof Variable && n2 instanceof Variable) {
      t1 = get_tin(v1, n1)
      t2 = get_tin(v2, n2)
      if (bind_tins(t1, t2, changes)) {
        return true
      }
      return _unify(t1.node, t1.varlist, t2.node, t2.varlist, changes)
    } else if (n1 instanceof Variable) {
      t1 = get_tin(v1, n1)
      if (bind(t1, n2, v2, changes)) {
        return true
      }
      return _unify(t1.node, t1.varlist, n2, v2, changes)
    } else if (n2 instanceof Variable) {
      return _unify(n2, v2, n1, v1, changes)
    } else if (n1 instanceof Box && n2 instanceof Box) {
      return n1.value === n2.value
    } else if (Array.isArray(n1) && Array.isArray(n2)) {
      n1RealLength = n1.length - (n1.hasListVar ? 1 : 0)
      n2RealLength = n2.length - (n2.hasListVar ? 1 : 0)
      if (n1RealLength === n2RealLength) {
        if (n1.hasListVar) {
          n1 = removeListVars(n1, v1, changes)
          if (!n1) {
            return false
          }
        }
        if (n2.hasListVar) {
          n2 = removeListVars(n2, v2, changes)
          if (!n2) {
            return false
          }
        }
        idx = 0
        while (idx < n1.length) {
          if (!_unify(n1[idx], v1, n2[idx], v2, changes)) {
            return false
          }
          idx++
        }
        return true
      }
      if (n1RealLength > n2RealLength) {
        return _unify(n2, v2, n1, v1, changes)
      }
      n2 = removeListVars(n2, v2, changes)
      if (!n2) {
        return false
      }
      idx1 = 0
      idx2 = 0
      while (idx2 < n2.length) {
        if (n1[idx1] instanceof Variable && n1[idx1].isListVar) {
          if (
            !_unify(
              n1[idx1],
              v1,
              n2.slice(idx2, idx2 + n2RealLength - n1RealLength),
              v2,
              changes,
            )
          ) {
            return false
          }
          idx2 += n2RealLength - n1RealLength - 1
        } else if (!_unify(n1[idx1], v1, n2[idx2], v2, changes)) {
          return false
        }
        idx1++
        idx2++
      }
      return true
    }
    return n1 === n2
  }
  const removeListVars = (arr, varList, changes) => {
    const ret = []
    for (const i of arr) {
      if (i instanceof Variable && i.isListVar) {
        if (!_unify(i, varList, [], [], changes)) {
          return false
        }
      } else {
        ret.push(i)
      }
    }
    return ret
  }
  const exports = {}
  exports.box = box
  exports.variable = (name, typeFunc) => new Variable(name, typeFunc)
  exports.TreeTin = TreeTin
  exports.VarTin = VarTin
  exports.Box = Box
  exports.DICT_FLAG = DICT_FLAG
  exports.toJson = toJson
  exports.Variable = Variable
  return exports
})()

{
  const variable = unify.variable
  //create some data structures to be unified
  const rectangle1 = {
    location: [25, 35],
    size: [100, variable('height')],
    color: '#000000',
  }
  const rectangle2 = {
    location: variable('location'),
    size: [100, 100],
    color: '#000000',
  }
  //box the objects so they can be unified
  const boxedRect1 = unify.box(rectangle1)
  const boxedRect2 = unify.box(rectangle2)
  //preform the unification
  const result = boxedRect1.unify(boxedRect2)
  //check if unification succeeded and print the results
  if (result) {
    //print "rectangle1 height: 100" to the console
    console.log(`rectangle1  height: ${boxedRect1.get('height').toString()}`)
    //print "rectangle2 location: [25, 35]" to the console
    console.log(
      `rectangle2 location: [${boxedRect2.get('location')[0]}, ${
        boxedRect2.get('location')[1]
      }]`,
    )
  } else {
    console.log('Unification Failed!')
  }
}

{
  const variable = unify.variable
  function isNum(o) {return typeof o == 'number'}
  const expr1 = unify.box([variable('X', isNum), 1])
  const expr2 = unify.box(['string', 1])
  const expr3 = unify.box([1, 1])
  if (expr1.unify(expr2)) {
    console.log(`Unification successful! X=${expr1.get('X').toString()}`)
  } else {
    console.log('Unification unsuccessful!')
  }
  if (expr1.unify(expr3)) {
    console.log(`Unification successful! X=${expr1.get('X').toString()}`)
  } else {
    console.log('Unification unsuccessful!')
  }
  console.log(expr1, expr2, expr3)
  //The following should be written to the console
  //Unification unsuccessful!
  //Unification successful! X=1
}