// h18.9/29 (鈴)
package tiny_prolog;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;

/** Prolog 処理系の (構文解析より後段の) 内部データ構造と手続き。
 * <p>
 * Prolog プログラムは，
 * 述語クラス Pred の各インスタンスが保持する節のリストとして表現される。
 * 大域的なシンボルテーブル等はない。
 * <p>
 * プログラムを「実行」するメソッドは，Goals#iterator() である。
 * 環境クラス Env のインスタンスなどの動的データ構造は，
 * 直接，間接にこのメソッドを遂行する過程で作られ，使われる。
 */
public class Core
{
    /** 汎用の２項組。
     * 基本的なデータ型としてフィールド first, second への直接参照を許す。
     * second は Lisp の cdr に相当する。
     * 連結リストの最後の要素の second の値は普通は null である。
     * 文字列表現は Prolog のリストに準ずる。
     */
    public static class Pair<First, Second> {
        public First first;
        public Second second;

        public Pair (First first, Second second) {
            this.first = first;
            this.second = second;
        }

        @Override
        public String toString() {
            return "[" + toStringWithoutParens() + "]";
        }

        /** 両端のカッコを省いた文字列表現 */
        protected String toStringWithoutParens() {
            if (second == null) {
                return str(first);
            } else if (second instanceof Pair) {
                return (str(first) + ", " + 
                        ((Pair) second).toStringWithoutParens());
            } else {
                return str(first) + " | " + str(second);
            }
        }
    }

    /** 引数の文字列値を返す便宜関数。
     * null には "[]" を返す。
     * 空文字列，大文字か数字か負号で始まる文字列，空白を含む文字列は，
     * 前後に ' を付ける。
     */
    public static String str(Object x) {
        if (x == null) return "[]";
        else if (x instanceof String) {
            String s  = (String) x;
            int n = s.length();
            if (n == 0) return "''";
            else {
                char c = s.charAt(0);
                if (Character.isUpperCase(c) || Character.isDigit(c)
                    || c == '-') {
                    return "'" + s + "'";
                } else {
                    for (int i = 0; i < n; i++) {
                        c = s.charAt(i);
                        if (Character.isWhitespace(c)) {
                            return "'" + s + "'";
                        }
                    }
                    return s;
                }
            }
        }
        return x.toString();
    }


    /** 変数。名前だけ保持する。変数値はここには保持しない。
     */
    public static class Var {
        private final String name;

        public Var (String name) {
            this.name = name;
        }

        @Override
        public String toString() {
            return name;
        }
    }

    /** 述語。
     * 述語の定義として節 (clause) のリストを保持する。
     * ここで節とは Goal と IBody の Pair とする。
     */
    public static class Pred {
        private final ArrayList<Pair<Goal, IBody>> defs;
        private final String name;

        public Pred (String name) {
            this.name = name;
            defs = new ArrayList<Pair<Goal, IBody>> ();
        }

        @Override
        public String toString() {
            return name;
        }
    }

    /** 節の本体 */
    private static interface IBody {}

    /** 節の本体としてのコールバック */
    public static interface ICallback extends IBody {
        public boolean call(CallbackEnv env);
    }
    
    /** ゴール，つまり述語項。
     * 述語に対する節の定義を主要なメソッドとする。
     */
    public static class Goal {
        private final Pred pred;
        private final Object[] args;
        
        /** 述語と項の配列を引数として述語項を構築する。
         * カット演算子以外，両引数とも null であってはならない。
         * ただし，項の配列の各要素は null であってもよい (Prolog の
         * 空リスト扱いされる)。
         */
        public Goal (Pred pred, Object[] args) {
            this.pred = pred;
            this.args = args;
        }

        /** 自身を頭部，引数を本体とした節を定義する。
         * 本体がないときは null を与える。
         * si はラテン語で「もしも」を意味する。
         */
        public void si(Goals body) {
            pred.defs.add(new Pair<Goal, IBody> (this, body));
        }

        /** コールバックを定義する。
         */
        public void calls(ICallback callback) {
            assert callback != null;
            pred.defs.add(new Pair<Goal, IBody> (this, callback));
        }

        @Override
        public String toString() {
            StringBuilder buf = new StringBuilder ();
            buf.append(str(pred));
            buf.append('(');
            boolean f = true;
            for (Object x: args) {
                if (f) {
                    f = false;
                } else {
                    buf.append(", ");
                }
                buf.append(str(x));
            }
            buf.append(')');
            return buf.toString();
        }
    }

    /** カット演算子 */
    public static class Cut extends Goal {
        private Cut () {
            super(null, null);
        }

        @Override
        public String toString() {
            return "!";
        }
    }

    /** カット演算子の唯一のインスタンス */
    public static final Cut CUT = new Cut ();

    /** Goal のリスト。
     * Pair の具体型であり，第１引数として Goal インスタンス，
     * 第２引数として null または Goals インスタンスをとる。
     */
    public static class Goals extends Pair<Goal, Goals>
        implements IBody, Iterable<Env>
    {
        public Goals (Goal goal, Goals rest) {
            super(goal, rest);
            assert goal != null;
        }
        
        /** 解決結果の環境を与えるイテレータを構築する。 */
        public Iterator<Env> iterator() {
            return new Resolver (this);
        }

        /** 文字列表現。Pair の具体型だが前後のカッコを省く。*/
        @Override
        public String toString() {
            return toStringWithoutParens();
        }
    }

    /** 環境 */
    public static final class Env {
        private final HashMap<Var, Pair<Object, Env>> table;

        private Env () {
            table = new HashMap<Var, Pair<Object, Env>> ();
        }

        private void put(Var x, Pair<Object, Env> pair) {
            table.put(x, pair);
        }

        private Pair<Object, Env> _get(Var x) {
            return table.get(x);
        }

        private void remove(Var x) {
            table.remove(x);
        }
    
        private void clear() {
            table.clear();
        }

        private Pair<Object, Env> dereference(Object t) {
            Env env = this;
            while (t instanceof Var) {
                Pair<Object, Env> p = env._get((Var) t);
                if (p == null) break;
                t = p.first;
                env = p.second;
            }
            return new Pair<Object, Env> (t, env);
        }

        /** 項の値を得る */
        public Object get(Object t) {
            Pair<Object, Env> p = dereference(t);
            t = p.first;
            Env env = p.second;
            if (t instanceof Goal) {
                Goal g = (Goal) t;
                return new Goal (g.pred, (Object[]) env.get(g.args));
            }
            else if (t instanceof Goals) {
                Goals g = (Goals) t;
                return new Goals ((Goal) env.get(g.first),
                                  (Goals) env.get(g.second));
            }
            else if (t instanceof Pair) {
                Pair c = (Pair) t;
                return new Pair<Object, Object> (env.get(c.first), 
                                                 env.get(c.second));
            }
            else if (t instanceof Object[]) {
                Object[] a = (Object[]) t;
                int n = a.length;
                Object[] r = new Object[n];
                for (int i = 0; i < n; i++) r[i] = env.get(a[i]);
                return r;
            }
            else {
                return t;
            }
        }
    }

    /** コールバック用の環境 */
    public static final class CallbackEnv {
        private Env env;
        private List<Pair<Var, Env>> trail;

        private CallbackEnv (Env env, List<Pair<Var, Env>> tail) {
            this.env = env;
            this.trail = trail;
        }

        /** 項の値を得る */
        public Object get(Object t) {
            return env.get(t);
        }

        /** 二つの項を単一化し，その成否を返す */
        public boolean unify(Object t, Object u) {
            return Core.unify(t, env, u, env, trail, env);
        }
    }

    /** 単一化関数 */
    private static boolean unify(Object x, Env xEnv, Object y, Env yEnv,
                                 List<Pair<Var, Env>> trail, Env tmpEnv)
    {
        for (;;) {
            if (x instanceof Var) {
                Var xVar = (Var) x;
                Pair<Object, Env> xp = xEnv._get(xVar);
                if (xp == null) {
                    Pair<Object, Env> yp = yEnv.dereference(y);
                    if (xVar != yp.first || xEnv != yp.second) {
                        xEnv.put(xVar, yp);
                        if (xEnv != tmpEnv) {
                            trail.add(new Pair<Var, Env> (xVar, xEnv));
                        }
                    }
                    return true;
                } else {
                    xp = xp.second.dereference(xp.first);
                    x = xp.first;
                    xEnv = xp.second;
                }
            } else if (y instanceof Var) {
                Object t = x;
                x = y;
                y = t;
                Env u = xEnv;
                xEnv = yEnv;
                yEnv = u;
            } else {
                break;
            }
        }
        if ((x instanceof Goal) && (y instanceof Goal)) {
            Goal xg = (Goal) x;
            Goal yg = (Goal) y;
            if (xg.pred != yg.pred) return false;
            x = xg.args;
            y = yg.args;
        }
        if ((x instanceof Object[]) && (y instanceof Object[])) {
            Object[] xa = (Object[]) x;
            Object[] ya = (Object[]) y;
            if (xa.length != ya.length) return false;
            for (int i = 0; i < xa.length; i++) {
                if (! unify(xa[i], xEnv, ya[i], yEnv, trail, tmpEnv))
                    return false;
            }
            return true;
        } 
        else if ((x instanceof Pair) && (y instanceof Pair)) {
            Pair xc = (Pair) x;
            Pair yc = (Pair) y;
            return (unify(xc.first, xEnv, yc.first, yEnv, trail, tmpEnv) &&
                    unify(xc.second, xEnv, yc.second, yEnv, trail, tmpEnv));
        }
        else if (x == null) {
            return y == null;
        }
        else {
            return x.equals(y);
        }
    }

    /** Goals を解決するイテレータ */
    private static class Resolver implements Iterator<Env> {
        private Env env;
        private ResolveBody iter;

        private Resolver (Goals body) {
            env = new Env ();
            boolean[] cut = new boolean[] { false };
            iter = new ResolveBody (body, env, cut);
        }

        public boolean hasNext() { 
            return iter.hasNext();
        }

        public Env next() {
            return env;
        }
        
        public void remove() {
            throw new UnsupportedOperationException ();
        }
    }

    /** Resolver の内部実装 */
    private static class ResolveBody {
        private final Goals body;
        private final Env env;
        private final boolean[] cut;
        private int q;
        //
        private Goal goal;
        private Goals rest;
        //
        private ResolveBody i0;
        private Iterator<Pair<Goal, IBody>> i1;
        private ResolveBody i2;
        private ResolveBody i3;
        private ResolveBody i4;
        //
        private Env dEnv;
        private boolean[] dCut;
        private ArrayList<Pair<Var, Env>> trail;

        private ResolveBody (Goals body, Env env, boolean[] cut) {
            this.body = body;
            this.env = env;
            this.cut = cut;
            q = 0;
        }

        private boolean hasNext() {
            for (;;) {
                switch (q) {
                case 0:
                    if (body == null) {
                        q  = 1;
                        return true;
                    } else {
                        goal = body.first;
                        rest = body.second;
                        if (goal == CUT) {
                            i0 = new ResolveBody (rest, env, cut);
                            q = 2;
                        } else {
                            dEnv = new Env ();
                            dCut = new boolean[] { false };
                            i1 = goal.pred.defs.iterator();
                            q = 3;
                        }
                    }
                    break;
                case 1:         // 終端...繰り返しの終わり
                    return false;
                case 2:
                    if (i0.hasNext()) return true;
                    i0 = null;
                    cut[0] = true;
                    q = 1;
                    return false;
                case 3:
                    if (i1.hasNext()) {
                        Pair<Goal, IBody> def = i1.next();
                        Goal dHead = def.first;
                        IBody dBody = def.second;
                        if (dCut[0] || cut[0]) {
                            dEnv = null; dCut = null; i1 = null;
                            q = 1;
                            return false;
                        }
                        trail = new ArrayList<Pair<Var, Env>> ();
                        if (unify(goal, env, dHead, dEnv, trail, dEnv)) {
                            if (dBody instanceof ICallback) {
                                ICallback cb = (ICallback) dBody;
                                CallbackEnv ce = new CallbackEnv (dEnv, trail);
                                if (cb.call(ce)) {
                                    i2 = new ResolveBody (rest, env, cut);
                                    q = 4;
                                } else {
                                    q = 5; // バックトラックへ
                                }
                            } else {
                                i3 = new ResolveBody
                                    ((Goals) dBody, dEnv, dCut);
                                q = 6;
                            }
                        } else {
                            q = 5; // バックトラックへ
                        }
                    } else {
                        dEnv = null; dCut = null; i1 = null;
                        q = 1;
                        return false;
                    }
                    break;
                case 4:
                    if (i2.hasNext()) return true;
                    i2 = null;
                    q = 5;      // バックトラックへフォールスルー
                case 5:
                    for (Pair<Var, Env> ve: trail) ve.second.remove(ve.first);
                    trail = null;
                    dEnv.clear();
                    q = 3;
                    break;
                case 6:
                    if (i3.hasNext()) {
                        i4 =  new ResolveBody (rest, env, cut);
                        q = 7;  // 最内ループへフォールスルー
                    } else {
                        i3 = null;
                        q = 5;  // バックトラックへ
                        break;
                    }
                case 7:
                    if (i4.hasNext()) return true;
                    i4 = null;
                    if (cut[0]) dCut[0] = true;
                    q = 6;
                    break;
                default:
                    throw new RuntimeException ("impossible state: " + q);
                }
            }
        }
    }
}