// TODO: use BaseNative
/*static class MyNative implements Prolog.Native {
  public boolean yo(Prolog p, Lisp term) {
    new Map<S, Lisp> m;
    
    if (nlMatch("$n = a random number between $a and $b inc.", term, m)) {
      int a = parseInt(m.get("a").raw());
      int b = parseInt(m.get("b").raw());
      int n = a+random(b-a+1);
      ret p.unify(m.get("n"), lisp(str(n)));
    }
    
    ret false;
  }
}*/

static class IsQuoted extends Prolog.BaseNative {
  *() { super("isQuoted($x)"); }
  
  boolean yo() {
    Lisp x = get("x");
    ret !(x instanceof Prolog.Var) && x.isLeaf() && isQuoted(x.head);
  }
}

static class IsWord extends Prolog.BaseNative {
  *() { super("isWord($x)"); }
  
  boolean yo() {
    Lisp x = get("x");
    ret !(x instanceof Prolog.Var) && x.isLeaf() && isExtendedIdentifier(x.head);
  }
}

static class IntMul extends Prolog.BaseNative {
  *() { super("$a = intmul($x, $y)"); }
  
  boolean yo() {
    BigInteger x = bigint(m.get("x").raw());
    BigInteger y = bigint(m.get("y").raw());
    ret p.unify(m.get("a"), lisp(str(x.multiply(y))));
  }
}

static class IntDiv extends Prolog.BaseNative {
  *() { super("$a = intdiv($x, $y)"); }
  
  boolean yo() {
    BigInteger x = bigint(m.get("x").raw());
    BigInteger y = bigint(m.get("y").raw());
    ret p.unify(m.get("a"), lisp(str(x.divide(y))));
  }
}

static class IntAdd extends Prolog.BaseNative {
  *() { super("$a = intadd($x, $y)"); }
  
  boolean yo() {
    BigInteger x = bigint(m.get("x").raw());
    BigInteger y = bigint(m.get("y").raw());
    ret p.unify(m.get("a"), lisp(str(x.add(y))));
  }
}

static class IntMinus extends Prolog.BaseNative {
  *() { super("$a = intminus($x, $y)"); }
  
  boolean yo() {
    BigInteger x = bigint(m.get("x").raw());
    BigInteger y = bigint(m.get("y").raw());
    ret p.unify(m.get("a"), lisp(str(x.subtract(y))));
  }
}

static class LessThan extends Prolog.BaseNative {
  *() { super("$x is less than $y"); }
  
  boolean yo() {
    BigInteger x = bigint(m.get("x").raw());
    BigInteger y = bigint(m.get("y").raw());
    ret x.compareTo(y) < 0;
  }
}

static class GreaterThan extends Prolog.BaseNative {
  *() { super("$x is greater than $y"); }
  
  boolean yo() {
    BigInteger x = bigint(m.get("x").raw());
    BigInteger y = bigint(m.get("y").raw());
    ret x.compareTo(y) > 0;
  }
}

// TODO: fix
static class HeadExists extends Prolog.BaseNative {
  *() { super("head $h exists in theory $t"); }
  
  boolean yo() {
    Lisp head = get("h");
    S theoryName = unq("t");
    Lisp theory = getParsedTheory(theoryName);
    
    // TODO: this is probably inefficient
    for (Lisp rule : theory) {
      Prolog.Clause clause = p.clause(rule);
      if (p.unifyOrRollback(head, clause.head))
        ret true;
    }
    ret false;
  }
}

static class TheoriesList extends Prolog.BaseNative {
  *() { super("$x = all theory names"); }
  
  boolean yo() {
    ret unify("x", nlMinimalList(getTheoryNames()));
  }
}

static class tocons extends Prolog.BaseNative {
  *() { super("$x = tocons($y)"); }
  
  boolean yo() {
    Lisp y = m.get("y");
    ret unify("x", nlToCons(y));
  }
}

static class fromcons extends Prolog.BaseNative {
  *() { super("$x = fromcons($y)"); }
  
  boolean yo() {
    Lisp y = m.get("y");
    ret unify("x", nlFromCons(y));
  }
}

static class operator extends Prolog.BaseNative {
  *() { super("$x = operator($y)"); }
  
  boolean yo() {
    Lisp y = get("y");
    ret unify("x", lisp(quote(y.head)));
  }
}

static class Unquote extends Prolog.BaseNative {
  *() { super("$x = unquote($y)"); }
  
  boolean yo() {
    Lisp y = get("y");
    ret unify("x", lisp(unquote(y.head)));
  }
}


static class arg extends Prolog.BaseNative {
  *() { super("$x = arg $i in $y"); }
  
  boolean yo() {
    Lisp y = m.get("y");
    int i = parseInt(m.get("i").raw());
    if (i-1 >= 0 && i-1 < y.size())
      ret unify("x", y.get(i-1));
    else
      ret false;
  }
}

static class Arity extends Prolog.BaseNative {
  *() { super("$x = arity of $y"); }
  
  boolean yo() {
    Lisp y = m.get("y");
    ret unify("x", lisp(str(y.size())));
  }
}

static class RemoveWord extends Prolog.BaseNative {
  *() { super("$x = removeWord($word, $y)"); }
  
  boolean yo() {
    Lisp y = get("y");
    S word = unq("word");
    ret unify("x", nlRemoveWord(word, y));
  }
}

static class GetTheory extends Prolog.BaseNative {
  *() { super("$x = theory $name"); }
  
  boolean yo() {
    S name = unq("name");
    Lisp parsed = getParsedTheory(name);
    ret parsed != null && unify("x", parsed);
  }
}

static class TextOfTheory extends Prolog.BaseNative {
  *() { super("$x = text of theory $name"); }
  
  boolean yo() {
    S name = unq("name");
    S text = getTheoryFromBot(name);
    ret text != null && unify("x", lisp(quote(text)));
  }
}

static class Solve1 extends Prolog.BaseNative {
  *() { super("solve1 $text in $theories"); }
  
  boolean yo() {
    Lisp question = get("text");
    Lisp t = m.get("theories");
    L<S> theoryNames = nlParseStringList(t);
    
    Prolog sub = newSubProlog(theoryNames, false);
    
    new IdentityHashMap<Lisp, S> varMap;
    Lisp exported = exportVars(question, varMap);
    if (showLog) {
      p.log("Exported: " + exported);
      p.log("Var map: " + structure(varMap));
    }
    sub.start(exported);
    sub.startTime = p.startTime;
    Map<S, Lisp> solution = sub.nextSolution();
    if (solution == null) ret false;
    ret unifyForeign(varMap, solution);
  }
}

static class Think extends Prolog.BaseNative {
  *() { super("think $x"); }
  
  boolean yo() {
    p.think(m.get("x"));
    ret true;
  }
}

static class MemorizeImpl extends Prolog.BaseNative {
  *() { super("memorize_impl $x"); }
  
  boolean yo() {
    Lisp x = m.get("x");
    if (!p.isClosedTerm(x)) {
      if (p.showStuff)
        p.log("Not a closed term, can't memorize: " + nlUnparse(x));
      ret false;
    }
    if (p.outTheory != null)
      incrementTheory(p.outTheory, x);
    p.think(lisp("[]", "memorized", x));
    ret true;
  }
}

static class RewriteWithTheory extends Prolog.BaseNative {
  *() { super("rewrite with theory $x"); }
  
  boolean yo() {
    S theoryName = unq("x");
    S text = findTheory(theoryName);
    if (text == null) {
      // clause succeeds even if theory not found
      if (p.showStuff)
        p.log(format("Warning: rewrite theory * not found", theoryName));
    } else {
      L<Prolog.Clause> rewriteTheory = getProgram(text);
      if (p.showStuff)
        for (Prolog.Clause c : rewriteTheory)
          p.log("  REW " + p.showClause(c));
      L<Lisp> rewritten = p.rewriteWith(rewriteTheory);
      if (p.showStuff)
        p.log("Got " + l(rewritten) + " rewritten terms.");
      for (Lisp term : rewritten) {
        if (p.showStuff)
          p.log("Adding rewritten term: " + nlUnparse(term));
        p.addClause(term, "rewritten");
      }
    }
    ret true;
  }
}

static class NLSafeParse extends Prolog.BaseNative {
  *() { super("$x = nlSafeParse($y)"); }
  
  boolean yo() {
    S input = unq("y");
    ret unify("x", nlSafeParse(input));
  }
}

// ignores case
static class StartsWith extends Prolog.BaseNative {
  *() { super("$x starts with $y"); }
  
  boolean yo() {
    S x = unq("x"), y = unq("y");
    ret swic(x, y);
  }
}

// ignores case
static class EndsWith extends Prolog.BaseNative {
  *() { super("$x ends with $y"); }
  
  boolean yo() {
    S x = unq("x"), y = unq("y");
    ret endsWithIgnoreCase(x, y);
  }
}