# Pastebin nr3WBA5a
## Tauto is a system for defining equivalencies. Very simply, it collects facts
## in the form of domain:sign binaries, and associates them with each other.
## Facts have no external meaning; they simply are defined as sharing
## referents. 
##
## After equivalencies are defined, Tauto can then be queried for equivalencies on any fact.

import tables, sets, strutils, future

const BOTTOM = "%"
const DELIMITER = "/"

type
  Referent* = range[int.low..0]
  Domain = string
  Sign = string
  Proposal* = tuple[domain: Domain, sign: Sign]
  Statement* = tuple[domain: Domain, sign: Sign, referent: Referent]
  StatementTable = TableRef[string, Statement]
  DomainIndex = TableRef[Sign, StatementTable]
  ReferentIndex = TableRef[Referent, HashSet[Statement]]
  Host = ref HostObj
  HostObj = object
    name: string
    domainIndex: DomainIndex
    referentIndex: ReferentIndex

var registry = newTable[string, Referent]()

let newSymbol = iterator: int =
  for n in countdown(-1, int.low):
    yield n

proc newReferent(): Referent =
  newSymbol()

proc newHost(name: string = ""): Host =
  var
    di: DomainIndex = newTable[Domain, StatementTable]()
    ri: ReferentIndex = newTable[Referent, HashSet[Statement]]()

  let hostRef = newReferent()
  registry[name] = hostRef

  var h = Host(name: name, domainIndex: di, referentIndex: ri)
  new(h)
  return h

proc getName(host: Host): Sign =
  let 
    referent = registry[host.name]
    ri = host.referentIndex
  if referent in ri:
    # The host might contain multiple names for itself, so simply return the
    # first one.
    for statement in ri[referent]:
      if statement.domain != BOTTOM:
        return statement.sign
  else:
    return "%" & DELIMITER & host.name

proc `$`(s: Statement): string =
  s.domain & DELIMITER & s.sign

proc setDefault(idx: DomainIndex, domain: Domain): var StatementTable = 
  if not (domain in idx):
    idx[domain] = newTable[Sign, Statement]()
  idx[domain]
proc setDefault(idx: ReferentIndex, referent: Referent): var HashSet[Statement] = 
  if not (referent in idx):
    idx[referent] = initSet[Statement]()
  idx[referent]

type LogicError = object of Exception

proc propose*(host: Host, proposals: seq[Proposal]): Referent {.raises: [LogicError, KeyError].} = 
  ## Accepts a series of proposals, being a sequence of domain-sign binaries
  ## that are proposed to be equivalent.
  # Look for an existing referent to expand upon.
  for proposal in proposals:
    let
      domain = proposal.domain
      sign = proposal.sign
    case domain:
      of BOTTOM:
        result = registry[sign]
      else: 
        if domain in host.domainIndex and sign in host.domainIndex[domain]:
          let fromDomain = host.domainIndex[domain][sign].referent
          if result == 0:
            result = fromDomain
          elif result != fromDomain:
            # If more than one existing referent is found, we are proposing that
            # two things known to be distinct are equivalent. This is a
            # contradiction.
            raise newException(LogicError, "Multiple referents found in proposal.")
  # Otherwise, create a new entity.
  if result == 0:
    result = newReferent()

  for proposal in proposals:
    let
      domain = proposal.domain
      sign = proposal.sign
      statement = (domain, sign, result)

    host.domainIndex.setDefault(domain)[sign] = statement
    host.referentIndex.setDefault(result).incl(statement)

proc retrieve*(host: Host, domain: Domain, sign: Sign): HashSet[Statement] =
  ## Given a domain-sign binary, attempt to resolve it to a reference entity
  ## and return all the statements pertaining to that referent (that is, all
  ## the statements equivalent to the given binary).
  if domain in host.domainIndex and sign in host.domainIndex[domain]:
    let statement = host.domainIndex[domain][sign]
    return host.referentIndex[statement.referent]
  else: 
    return initSet[Statement](1)

when isMainModule:

  type 
    TautoUI = object
      host: Host

  proc prompt(ui: TautoUI): string =
    "[" & ui.host.getName & "] >> " 

  proc newProposal(ui: TautoUI, proposalString: string): Proposal =
    let 
      splitString = proposalString.strip().split(sep=DELIMITER, maxsplit=1)
      token = splitString[0]
    case splitString.len:
      of 1:
        (ui.host.name, token)
      else:
        (token, splitString[1])

  proc propose(ui: TautoUI, commandString: string) =
    let proposals = lc[ 
      ui.newProposal(proposalString) | (proposalString <- commandString.split(sep=',')), 
      Proposal ]
    try:
      discard ui.host.propose(proposals)
      echo "ok"
    except LogicError:
      echo "Error: " & $getCurrentExceptionMsg()

  proc render(ui: TautoUI, s: Statement): string =
    ## Render a statement into a string.
    # If the statement's domain is of the auto-assigned form, do a lookup for a
    # native name of the domain.
    if s.domain == ui.host.name:
      let renderedDomain = ui.host.getName()
      let naturalized = (renderedDomain, s.sign, s.referent) 
      return $naturalized
    else:
      return $s

  proc retrieve(ui: TautoUI, proposalString: string) =
    let proposal = ui.newProposal(proposalString)
    let retrievedStatements = ui.host.retrieve(proposal.domain, proposal.sign)
    for statement in retrievedStatements.items:
      echo ui.render(statement)
  
  proc debug(ui: TautoUI) =
    echo ".."
    for value in ui.host.referentIndex.values:
      echo $value
    echo ".."

  proc main*(ui: var TautoUI) =
    ## The main UI. Accepts commands to propose new equivalencies and query
    ## existing ones.
    echo "TAUTO"
    while true:
      stdout.write(ui.prompt)
      try:
        let 
          input = stdin.readLine.string
          stripped = input.strip()
        if stripped.len > 0:
          if stripped[0] == '/' and stripped.len > 1:
            # Command mode
            let 
              splitCommand = stripped[1..stripped.high].split()
              command = splitCommand[0]
            case command:
              of "ok":
                break
              of "s":
                let hostName = splitCommand[1]
                var host = newHost(hostName)
                ui.host = host
              else: discard
          else:
            let 
              splitInput = input.split(maxsplit=1)
              command = splitInput[0]
            case command:
              of "!", "p": 
                ui.propose(splitInput[1])
              of "?", "q":
                if splitInput.len == 1:
                  ui.debug()
                else:
                  ui.retrieve(splitInput[1])
              else:
                echo "?"
      except IOError:
        echo "ok"
        break

  let host = newHost("ENG")
  var ui = TautoUI(host: host)
  ui.main()