/*
example:

#include "proloc.h"
int main()
{
//--------------------------------

  DECLARE_VARIABLES;
  DECLARE_PREDICATE(parent);
  DECLARE_PREDICATE(grandparent);
  DECLARE_PREDICATE(child);

//--------------------------------

  parent(b,a); // fact:bはaの親
  parent(c,b); // fact:cはbの親
  grandparent(X,Y) <= parent(X,Z), parent(Z,Y); // rule:祖父母
  child(X,Y)       <= parent(Y,X); // rule:YがXの親ならXはYの子

//--------------------------------

  - grandparent(c,X); // cは誰の祖母(父)？
  - child(b,c); // bはcの子供？
  - parent(X,Y); // 誰が誰の親なのじゃ？
  - child(X,a); // aの子供は誰かいる？

  return 0;
}
*/

//
// Prologっぽいことをします。
//
// 諸注意。
//  ・ピリオドの代わりにセミコロンで。
//  ・:- の代わりに <= で。
//  ・引数が一つのfactを書くときは頭に * をつけて下さい。
//       *male(a); みたいな感じ。
//  ・functorは無し
//  ・述語の引数は3つまで。各地のコンストラクタをいじれば増やせる。
//  ・goalに複数渡すときは -( xxx, yyy, zzz ); と () をお忘れ無く。
//  ・変数名,定数名はアルファベット１文字で。
//  ・bcc32 5.51 と gcc 2.95 on cygwin で作成
//  ・いたるところでメモリリークしてます。
//

#include <deque>
#include <vector>
#include <iostream>
#include <algorithm>
#include <iterator>
#include <typeinfo>


namespace proloc
{
  using namespace std;

  //
  // 述語基底クラス。ここから使いたい述語名のクラスを派生する
  //
  class Pred
    {
    protected:
      //------ 実装クラス: Head部分の引数リストとtail部のリストを保持 --
      struct PredImpl
        {
          vector<int>      param;
          vector<PredImpl*> tail;
          virtual ~PredImpl() {}
          virtual PredImpl* Clone() const = 0;

        protected:
          PredImpl(int p1)
            { param.push_back(p1); }
          PredImpl(int p1,int p2)
            { param.push_back(p1); param.push_back(p2); }
          PredImpl(int p1,int p2,int p3)
            { param.push_back(p1); param.push_back(p2);
              param.push_back(p3); }
          PredImpl(const PredImpl& r)
            : param( r.param )
            {
              for( vector<PredImpl*>::const_iterator
                   i=r.tail.begin(), e=r.tail.end(); i!=e; ++i )
                tail.push_back( (*i)->Clone() );
            }
        };

    protected:
      //----- Predのインスタンスメソッド群。factやruleの記述用 --------
      Pred( PredImpl* i )
           : impl( i )
        {
          enroll( i );
        }
    public:
      operator PredImpl*() const
        {
          return const_cast<PredImpl*>(impl);
        }
      Pred& operator<=( PredImpl* i )
        {
          if( i != NULL )
            {
              impl->tail.push_back( i );
              disenroll( i );
            }
          return *this;
        }
      Pred& operator,( PredImpl* i )
        {
          return (*this <= i);
        }
      void operator*() {}
    private:
      PredImpl* impl;

    private:
      //----- factとruleのリストの管理 ------------------------
      typedef vector<PredImpl*>                 RFL;
      typedef vector<PredImpl*>::iterator       RFI;
      typedef vector<PredImpl*>::const_iterator RFIc;
      static RFL rulefact;
      static void enroll( PredImpl* i )
        {
          rulefact.push_back( i );
        }
      static void disenroll( PredImpl* i )
        {
          RFI it = find( rulefact.begin(), rulefact.end(), i );
          if( it != rulefact.end() )
            rulefact.erase( it );
        }

    public:
      typedef deque<PredImpl*> GOAL;

      //----- 問い合わせ処理への転送関数など ----------------------------
      void operator-()
        {
          ask_impl( *this );
        }
    private:
      friend void ask( const Pred&,PredImpl*,PredImpl*,PredImpl*,
                       PredImpl*,PredImpl*,PredImpl* );
      static void ask_impl( Pred& p )
        {
          disenroll( p );

          PredImpl* i = p;
          GOAL goal( i->tail.begin(), i->tail.end() );
          goal.push_front( i );

          cout << endl;
          cout << (Solve(goal, SST())?"OK!":"failed.") << endl;
        }

    private:
      //----- 代入の処理 -------------------------------------------
      typedef vector<pair<int,int> >                 SST;
      typedef vector<pair<int,int> >::iterator       SSI;
      typedef vector<pair<int,int> >::const_iterator SSIc;

      static bool PrintSst( const SST& sst )
        {
          // 表示
          static const char var[] = {
            'A','B','C','D','E','F','G','H','I','J','K','L','M','N','O',
            'P','Q','R','S','T','U','V','W','X','Y','Z' };
          static const char cst[] = {
            'a','b','c','d','e','f','g','h','i','j','k','l','m','n','o',
            'p','q','r','s','t','u','v','w','x','y','z' };
          for( SSIc i=sst.begin(), e=sst.end(); i!=e; ++i )
            cout << var[-(*i).first-1] << '=' << cst[(*i).second-1] << ',';
          if( sst.empty() )
            cout << "[no substitution]";
          cout << endl;
          return true;
        }

      static SST AddSst( const SST& sst, const SST& u )
        {
          // 最終GOAL変数への代入のみ残してappend
          SST res( sst );
          for( SSIc i=u.begin(), e=u.end(); i!=e; ++i )
            if( (*i).first >= -26 )
              res.push_back( *i );
          return res;
        }

      static void DoSst( GOAL& g, const SST& u )
        {
          // gに対して代入uの実行
          for( GOAL::iterator i=g.begin(), ie=g.end(); i!=ie; ++i )
            for( PRI
                 j=(*i)->param.begin(), je=(*i)->param.end(); j!=je; ++j )
              for( SSIc k=u.begin(), ke=u.end(); k!=ke; ++k )
                if( (*j) == (*k).first )
                  *j = (*k).second;
        }

      static void CopyGoal( GOAL& a, const GOAL& b )
        {
          a.clear();
          for( GOAL::const_iterator i=b.begin(), e=b.end(); i!=e; ++i )
            a.push_back( (*i)->Clone() );
        }

    private:
      //------ Unification ----------------------------------------
      typedef vector<int>                 PRM;
      typedef vector<int>::iterator       PRI;
      typedef vector<int>::const_iterator PRIc;

      static PredImpl* Rename( PredImpl* old )
        {
          static int shift = 0;
          shift -= 100;

          // 変数名のつけかえ
          PredImpl* ren = old->Clone();
          for( PRI i=ren->param.begin(), e=ren->param.end(); i!=e; ++i )
            if( (*i) < 0 )
              *i += shift;
          for( vector<PredImpl*>::iterator
               i=ren->tail.begin(), ie=ren->tail.end(); i!=ie; ++i )
            for( PRI
                 j=(*i)->param.begin(), je=(*i)->param.end(); j!=je; ++j )
              if( (*j) < 0 )
                *j += shift;
          return ren;
        }

      static bool CheckUnify( PRM p1, PRM p2, SST& u )
        {
          // Unify可能かどうか調べ、可能ならuにMGUを入れる
          PRI i1 = p1.begin();
          PRI i2 = p2.begin();
          PRI e1 = p1.end();
          PRI e2 = p2.end();
          for( ; i1!=e1 && i2!=e2; ++i1, ++i2 )
            {
              pair<int,int> nu;
              if( *i1>0 )
                if( *i2>0 )
                  {if(*i1!=*i2)break;continue;}
                else
                  nu = pair<int,int>(*i2,*i1);
              else
                if( *i2>0 )
                  nu = pair<int,int>(*i1,*i2);
                else
                  if( *i1<*i2 )
                    nu = pair<int,int>(*i1,*i2);
                  else
                    nu = pair<int,int>(*i2,*i1);
              u.push_back( nu );
              // 先頭の方のUnify結果を後ろに伝える
              PRI x1=i1, x2=i2;
              for( ++x1,++x2; x1!=e1 && x2!=e2; ++x1, ++x2 )
                {
                  if( *x1 == nu.first ) *x1 = nu.second;
                  if( *x2 == nu.first ) *x2 = nu.second;
                }
            }
          return (i1==e1 && i2==e2);
        }

    private:
      //------ 解く -----------------------------------------------
      static bool Solve( GOAL goal, SST sst )
        {
          if( goal.empty() )
            return PrintSst( sst );

          bool solved = false;
          SST u;
          GOAL ng;

          PredImpl* g = goal.front(); goal.pop_front();
          for( RFI i=rulefact.begin(), e=rulefact.end(); i!=e; ++i )
            if( typeid(*g) == typeid(**i) ) // 述語名のチェック
              {
                PredImpl* r = Rename(*i); // 変数名のつけかえ
                u.clear();
                if( CheckUnify(g->param, r->param, u) ) // MGUを探す
                  {
                    CopyGoal( ng, goal );
                    ng.insert(ng.begin(),r->tail.begin(),r->tail.end());
                    DoSst( ng, u );
                    solved |= Solve( ng, AddSst(sst,u) );
                  }
              }
          return solved;
        }
    };

  vector<Pred::PredImpl*> Pred::rulefact;

  //---- 問い合わせ処理の実装へ転送する関数 ------------------------------
  void ask( const Pred& p,
            Pred::PredImpl* i1=0, Pred::PredImpl* i2=0,
            Pred::PredImpl* i3=0, Pred::PredImpl* i4=0,
            Pred::PredImpl* i5=0, Pred::PredImpl* i6=0 )
    {
      Pred::ask_impl(( const_cast<Pred&>(p),i1,i2,i3,i4,i5,i6 ));
    }

  //---- 述語定義マクロ --------------------------------------------------
  #define DECLARE_PREDICATE(Px)                                \
    class Px : public proloc::Pred                             \
    {                                                          \
      typedef proloc::Pred super;                              \
      struct Impl : public PredImpl                            \
      {                                                        \
        Impl(int p1) : PredImpl(p1) {}                         \
        Impl(int p1,int p2) : PredImpl(p1,p2) {}               \
        Impl(int p1,int p2,int p3) : PredImpl(p1,p2,p3) {}     \
        Impl* Clone() const { return new Impl(*this); }        \
      };                                                       \
    public:                                                    \
      Px(int p1) : super( new Impl(p1) ) {}                    \
      Px(int p1,int p2) : super( new Impl(p1,p2) ) {}          \
      Px(int p1,int p2,int p3) : super( new Impl(p1,p2,p3) ) {}\
    }

  //---- 変数のフリをするint値の定義用マクロ -----------------------------
  #define DECLARE_VARIABLES                                              \
    const int a=1,b=2,c=3,d=4,e=5,f=6,g=7,h=8,i=9,j=10,k=11,l=12,m=13,   \
        n=14,o=15,p=16,q=17,r=18,s=19,t=20,u=21,v=22,w=23,x=24,y=25,z=26,\
        A=-1,B=-2,C=-3,D=-4,E=-5,F=-6,G=-7,H=-8,I=-9,J=-10,K=-11,L=-12,  \
        M=-13,N=-14,O=-15,P=-16,Q=-17,R=-18,S=-19,T=-20,U=-21,V=-22,     \
        W=-23,X=-24,Y=-25,Z=-26;                                         \
        {int tt=a-b-c-d-e-f-g-h-i-j-k-l-m-n-o-p-q-r-s-t-u-v-w-x-y-z-A-B- \
          C-D-E-F-G-H-I-J-K-L-M-N-O-P-Q-R-S-T-U-V-W-X-Y-Z; tt=0; }
}