package week13

class Tokenizer(s: String, delimiters: String) extends Iterator[String] {
  
  private var i = 0;
  private val n = s.length();

  def isDelimiter(ch: Char) = delimiters.indexOf(ch) >= 0;

  def isNeck(ch: Char) = ch == ':' && i < n && s.charAt(i) == '-';

  def hasNext: boolean = {
    while (i < n && s.charAt(i) <= ' ') { i = i + 1 }
    i < n
  }

  def next: String =
    if (hasNext) {
      val start = i;
      var ch = s.charAt(i); i = i + 1;
      if (isDelimiter(ch)) ch.toString()
      else if (isNeck(ch)) { i = i + 1; ":-" }
      else {
        while (i < n &&
	       s.charAt(i) > ' ' &&
	       !isDelimiter(s.charAt(i))){ i = i + 1 }
        s.substring(start, i)
      }
    } else "";

}

abstract class Interpreter {

  // Abstract methods.
  val prompt: String;
  val name: String;
  val commentDelim: String;
  def switchDebug: unit;
  def process(code: String): unit;
  def load(code: String): unit;
  def unloadLast: unit;  

  private var debug: boolean = false;
  private var loadedFilenames: List[String] = Nil;

  private def read(filename: String): String = {
    import java.io._;
    try {
      val stream = new BufferedReader(new FileReader(filename));
      val buffer = new StringBuffer();
      def loop: String = {
        val line = stream.readLine();
        if (line == null) {
          buffer.toString();
        } else {
          val inx = line.indexOf(commentDelim); // comment
          if (inx < 0) buffer.append(line)
          else if (inx > 0) buffer.append(line.substring(0, inx));
          loop
        }
      }
      loop
    } catch {
      case (exception: FileNotFoundException) =>
        Console.println("not found: " + filename);
        ""
      case (exception: IOException) =>
        Console.println("can't read: " + filename);
        ""
    }
  }

  private def help: Unit = {
    Console.println(":?       display this message");
    Console.println(":l<file> load file with name <file>");
    Console.println(":r       reload the last loaded file");
    Console.println(":d       switch to/from debug mode (# in prompt)");
    Console.println(":q       quit the interpreter");
  }
  
  def run: unit = {
    var filename = "";
    var iprompt = prompt;
    var continue = true;
    val in = new java.io.DataInputStream(System.in);
    Console.println(name + " (type \":?\" for help)");
    while (continue) {
      System.out.print(iprompt);
      val line = in.readLine();
      if (line.startsWith(":?"))
        help
      else if (line startsWith ":d") {
        switchDebug;
        debug = !debug;
        iprompt = if (debug) "#" + prompt else prompt
      }
      else if (line.startsWith(":q")) {
        continue = false
      } else if (line.startsWith(":l")) {
        filename = line.substring(2).trim();
        if (loadedFilenames.contains(filename))
          Console.println("warning: already loaded file (" + filename + ") can lead to inconstency.")
        else
          loadedFilenames = filename :: loadedFilenames;
        load(read(filename))
      } else if (line.startsWith(":r")) {
        if (loadedFilenames.isEmpty)
          Console.println("warning: no file loaded for now.")
        else {
          unloadLast;
          load(read(filename))
        }
      } else {
        process(line)
      }
    }
  }
  
}

object Terms {

  var debug = false;

  trait Term {
  
    def map(s: Subst): Term = this match {
      case Var(a) =>  lookup(s, a) match {
        case Some(b) => b map s
        case None => this
      }
      case Con(a, ts) =>  Con(a, ts map (t => t map s))
    }
    
    def vars: List[String] = this match {
      case Var(a) => List(a)
      case Con(a, ts) => (ts flatMap (t => t.vars)).removeDuplicates
    }

    def tailToString(t: Term): String = t match {
      case Con("nil", List()) => "]"
      case Con("cons", List(fst, snd)) => ", " + fst + tailToString(snd) 
      case _ => "|" + t + "]"
    }
    
    override def toString(): String = termToInt(this) match {
      case Some(n) => n.toString()
      case None => this match {
        case Var(a) => a
        case Con("nil", List()) => "[]"
        case Con("cons", List(fst, snd)) => "[" + fst + tailToString(snd) 
        case Con(a, ts) => a + (if (ts.isEmpty) "" else ts.mkString("(", ",", ")"));
      }
    }
  }
  case class Var(a: String) extends Term;
  case class Con(a: String, ts: List[Term]) extends Term;
  
  def termToInt(t: Term): Option[int] = t match {
    case Con("zero", List()) => Some(0)
    case Con("succ", List(u)) => termToInt(u) match {
      case None => None
      case Some(n) => Some(n + 1)
    }
    case _ => None
  }
  
  case class Binding(name: String, term: Term) {
    term match { case Var(n) if (name == n) => error("bad binding") case _ => () }
    override def toString() = name + " = " + term;
  }

  type Subst = List[Binding];
  
  def lookup(s: Subst, name: String): Option[Term] = s match {
    case List() => None
    case b :: s1 => if (name == b.name) Some(b.term) else lookup(s1, name)
  }

  private var count = 0;
  def newVar(prefix: String) = { count = count + 1; Var(prefix + count) }

  val NoTerm = Con("<none>", List());

  def unify1(x: Term, y: Term, s: Subst): Option[Subst] = Pair(x, y) match {
    case Pair(Var(a), Var(b)) if (a == b) =>
      Some(s)
    case Pair(Var(a), _) => lookup(s, a) match {
      case Some(x1) => unify(x1, y, s)
      case None => if ((y map s).vars contains a) None else Some(Binding(a, y) :: s)
    }
    case Pair(_, Var(b)) =>
      unify(y, x, s)
    case Pair(Con(a, xs), Con(b, ys)) if (a == b) =>
      unify(xs, ys, s)
    case _ => None
  }

  def unify(x: Term, y: Term, s: Subst): Option[Subst] = {
    val ss = unify1(x, y, s);
    if (debug) Console.println("unify " + x + " with " + y + " = " + ss);
    ss
  }

  def unify(xs: List[Term], ys: List[Term], s: Subst): Option[Subst] = Pair(xs, ys) match {
    case Pair(List(), List()) => Some(s)
    case Pair(x :: xs1, y :: ys1) =>
      unify(x, y, s) match {
	case Some(s1) => unify(xs1, ys1, s1)
	case None => None
      }
    case _ => None
  }
}

import Terms._;

object Programs {

  case class Clause(lhs: Term, rhs: List[Term]) {
    def vars =
      (lhs.vars ::: (rhs flatMap (t => t.vars))).removeDuplicates;
    def newInstance = {
      var s: Subst = List();
      for (val a <- vars) { s = Binding(a, newVar(a)) :: s }
      Clause(lhs map s, rhs map (t => t map s))
    }
    override def toString() =
      lhs.toString() + " :- " + rhs.mkString("", ",", "") + ".";
  }

  def list2stream[a](xs: List[a]): Stream[a] = xs match {
    case List() => Stream.empty
    case x :: xs1 => Stream.cons(x, list2stream(xs1))
  }
  def option2stream[a](xo: Option[a]): Stream[a] = xo match {
    case None => Stream.empty
    case Some(x) => Stream.cons(x, Stream.empty)
  }

  def solve(query: List[Term], clauses: List[Clause]): Stream[Subst] = {

    def solve2(query: List[Term], s: Subst): Stream[Subst] = query match {
      case List() =>
	Stream.cons(s, Stream.empty)
      case Con("not", qs) :: query1 =>
	if (solve1(qs, s).isEmpty) solve1(query1, s)
	else Stream.empty
      case q :: query1 =>
	for (val clause <- list2stream(clauses);
	     val s1 <- tryClause(clause.newInstance, q, s);
	     val s2 <- solve1(query1, s1)) yield s2
    }

    def solve1(query: List[Term], s: Subst): Stream[Subst] = {
      val ss = solve2(query, s);
      if (debug) Console.println("solved " + query + " = " + ss);
      ss
    }

    def tryClause(c: Clause, q: Term, s: Subst): Stream[Subst] = {
      if (debug) Console.println("trying " + c);
      for (val s1 <- option2stream(unify(q, c.lhs, s));
	   val s2 <- solve1(c.rhs, s1)) yield s2;
    }

    solve1(query, List())
  }
}

import Programs._;

class Parser(s: String) {
  val it = new Tokenizer(s, "(),.?[]|");

  var token: String = it.next;

  def syntaxError(msg: String) = error(msg + ", but " + token + " found");

  def rep[a](p: => a): List[a] = {
    val t = p;
    if (token == ",") { token = it.next; t :: rep(p) } else List(t)
  }

  def constructor: Term = {
    def intToTerm(n: int): Term =
      if (n == 0) Con("zero", List())
      else Con("succ", List(intToTerm(n - 1)));
    val a = token;
    token = it.next;
    try {
      intToTerm(Integer.parseInt(a))
    } catch {
      case _ => // NumberFormatException 
        Con(a,
	    if (token equals "(") {
	      token = it.next;
	      val ts: List[Term] = if (token equals ")") List() else rep(term);
	      if (token equals ")") token = it.next else syntaxError("`)' expected");
	      ts
	    } else List())
    }
  }

  private def toProlog(l: List[Term], tail: Term): Term = l match {
    case Nil => tail
    case x :: xs => Con("cons", List(x, toProlog(xs, tail)))
  }
  
  val prologNil = Con("nil", List());
  
  def listTerm: Term =
    if (token equals "]") {
      token = it.next;
      prologNil
    }
    else {
      var ts = List(term); 
      while (token equals ",") {
        token = it.next;
        ts = term :: ts;
      }
      val tail =
        if (token equals "|") {
          token = it.next;
          term
        }
        else
          prologNil;
      if (token equals "]") {
        token = it.next;
        toProlog(ts.reverse, tail)
      }
      else
        syntaxError("']' expected")
    }

  def term: Term = {
    val ch = token.charAt(0);
    if (ch == '[') { token = it.next; listTerm }
    else if (Character.isUpperCase(ch)) { val a = token; token = it.next; Var(a) }
    else if (it.isDelimiter(ch)) { syntaxError("term expected"); null }
    else constructor
  }

  def line: Clause = {
    val result =
      if (token equals "?") {
        token = it.next;
        Clause(NoTerm, rep(constructor));
      } else {
	Clause(
          constructor,
          if (token equals ":-") { token = it.next; rep(constructor) } else List())
      }
    if (token equals ".") token = it.next else syntaxError("`.' expected");
    if (debug) {
      if (result.lhs == NoTerm) Console.println("query " + result.rhs)
      else Console.println("add " + result)
    }
    result
  }

  def all: List[Clause] = if (token equals "") List() else line :: all;
}

object Prolog extends Interpreter {

  private var firstClauses: List[Clause] = List();
  private var lastClauses: List[Clause] = List();
  private def program = firstClauses ::: lastClauses;
  private var solutions: Stream[Subst] = Stream.empty;
  private var vs: List[String] = List();

  val name = "Mini-Prolog Interpreter";
  val prompt = "prolog> ";
  val commentDelim = "%";

  def switchDebug = Terms.debug = ! Terms.debug;

  def load(code: String): unit = {
    firstClauses = program;
    lastClauses = List();
    process(code)
  }

  def unloadLast: unit = {
    lastClauses = List();
  }

  def process(code: String): unit =
    try {
      new Parser(code).all foreach { c =>
        if (c.lhs == NoTerm) {
          c.rhs match {
            case List(Con("more", List())) =>
              if (! solutions.isEmpty)
                solutions = solutions.tail;
            case _ =>
              solutions = solve(c.rhs, program);
            vs = c.vars;
          }
          if (solutions.isEmpty) {
            Console.println("no")
          } else {
            val s: Subst = solutions.head
            .filter(b => vs contains b.name)
            .map(b => Binding(b.name, b.term map solutions.head))
            .reverse;
            if (s.isEmpty) Console.println("yes")
            else Console.println(s);
          }
        } else {
          lastClauses = lastClauses ::: List(c);
        }                                   }
    } catch { case exc => Console.println(exc) }

  def main(args: Array[String]): unit = {
    if (args.length > 0)
      load(args(0));
    run;
  }
  
}