/* 
 ******************************************************************
 * $Id: tfslib.h 260 2002-11-04 09:22:21Z clerger $
 * Copyright (C) 1999 by INRIA 
 * Author: Eric de la Clergerie <Eric.De_La_Clergerie@inria.fr>
 * ----------------------------------------------------------------
 *
 *  tfslib.h -- 
 *
 * ----------------------------------------------------------------
 * Description
 *   Header file to be included by C files generated by tfs2lib 
 * ----------------------------------------------------------------
 */


#include <stdarg.h>
#include "libdyalog.h"
#include "builtins.h"
#include "hash.h"

typedef Bool(*Tfs_Fun) (Sproto, Sproto);

#define TFS_X_CHAR 1
#define TFS_X_INT  2
#define TFS_X_SMB  4
#define TFS_X_COMPOUND  8

typedef struct Tfs_Escape {
    long key;
    fol_t type;
    int   escape;
} *Tfs_Escape;

char *Escape_Table;

typedef struct Tfs_Data {
  long key;
  short inv;
  fol_t left;
  fol_t right;
  Tfs_Fun fun;
} *Tfs_Data;

char *Unif_Table;
char *Subs_Table;

typedef struct Template {
    fol_t   skel;
    int     k;
    obj_t   env;
    Bool    maximal;
} Template;

static Template Template_Table[];

extern fkey_t push_layer_archive(const unsigned long, obj_t);
extern void folsmb_feature_set(fol_t,fol_t);
extern void folsmb_info_set(fol_t, obj_t, obj_t );

#define Bind_To_Template(Left,Right,Res,n)              \
    struct Template _o = Template_Table[n];             \
    Sdecl(Res);                                         \
    Res = _o.skel;                                      \
    Sk(Res) = push_layer_archive(_o.k,_o.env);        \
    V_LEVEL_DISPLAY(V_TFS,"Use template %&s\n",Res,Sk(Res));  \
    Unif_Bind(Left,Sk(Left),Res,Sk(Res));               \
    Unif_Bind(Right,Sk(Right),Res,Sk(Res))

static fol_t
Tfs_Symbol( const char* s, const int arity, fol_t module)
{
    if (!(module))
        module = FOLNIL;
    return find_module_folsmb(s,arity,module);
}

static fol_t
Tfs_Type(fol_t type, const int arity, const int deref) 
{
    type = find_module_folsmb(FEATURE_SPACE,arity,type);
    if (deref)
        folsmb_switch_derefterm(type);
    return type;
}


static void
set_features( fol_t type, int arity, ... )
{
    fol_t features;
    type = FOLSMB_MODULE(type);

    dyalog_printf("Adding feature info for %&f\n",type);
        
    if (arity == 0)        /* WARNING: Bug to correct  */
	features = find_folsmb("features", 0);
    else {
	va_list args;
	va_start(args,arity);
	FOLCMP_WRITE_START(find_folsmb("features",arity), arity);

	for ( ; arity > 0 ; arity-- ){
	    fol_t f= va_arg(args,fol_t);
	    fol_t type = va_arg(args,fol_t);
	    if ((type))
		f = (fol_t) folcmp_create_binary( ":", f, type);
	    FOLCMP_WRITE( f );
	}

	features = FOLCMP_WRITE_STOP;
    }
	
    folsmb_feature_set(type,features);

}

static void
set_intro(fol_t feature, fol_t type, int type_order, int feature_pos) 
{
    struct Template o = Template_Table[type_order];
    Sdecl(t);
    Trail;
    Sk(t) = push_layer_archive(o.k,o.env);
    t = o.skel;
    FOLCMP_WRITE_START( find_folsmb("$farg",3), 3);
    FOLCMP_WRITE(feature);
    FOLCMP_WRITE(t);
    FOLCMP_WRITE(FOLCMP_REF(t,feature_pos));
    rt_install_database( FOLCMP_WRITE_STOP, Sk(t) );
    Untrail;
    folsmb_info_set( feature, (obj_t) INFO_INTRO, (obj_t) type);
}

static void
set_deref(fol_t type)
{
    folsmb_switch_derefterm(type);
}

static void
Make_Template( int index, fol_t functor, unsigned long arity, Bool maximal, ... )
{    
  Sdecl(arg);
  Sdecl(o);
  int varindex = 0;
  va_list args;

  V_LEVEL_DISPLAY(V_TFS,"Template %d %&f\n",index,functor);
  
  va_start(args,maximal);

  Trail;
  Sk(o) = LSTACK_PUSH_VOID;
  if (arity == 0 && maximal ) {
    o = functor;
  } else {
    FOLCMP_WRITE_START(functor,arity);
    if (!maximal) {
	fol_t X = FOLVAR_FROM_INDEX(varindex++);
	FOLCMP_WRITE( X );
    }
    for( ; arity > 0 ; arity-- ) {
      int i = va_arg(args,int);
      fol_t X = FOLVAR_FROM_INDEX( varindex++ );
      if (i>=0) {
          struct Template entry = Template_Table[i];
          arg = entry.skel;
          Sk(arg) = push_layer_archive(entry.k,entry.env);
          TRAIL_UBIND(X,Sk(o),arg,Sk(arg));
      }
      FOLCMP_WRITE(X);
    }
    o = FOLCMP_WRITE_STOP;
  }
  
  Template_Table[index].skel = o;
  Template_Table[index].maximal = maximal;
  Collapse_Unwrap(o,Sk(o),
                  Template_Table[index].k,
                  Template_Table[index].env
                  );
  V_LEVEL_DISPLAY(V_TFS,"Template %d: done\n",index);
  Untrail;
}

static void
Add_Escape( const fol_t type, const int escape )
{
    long key = ((long) type) >> 16;
    Tfs_Escape data = (Tfs_Escape) Hash_Find( Escape_Table, key );
    if (!data) {
        struct Tfs_Escape box = { key: key, type: type, escape: escape };
        Hash_Insert( Escape_Table, (char *) &box, 0);
    } else {
        data->escape |= escape;
    }
}

static void 
AddTableEntry(const fol_t Left, const fol_t Right, const Tfs_Fun fun, char *Table)
{
    long SymbL = ((long) Left) >> 16;
    long SymbR = ((long) Right) >> 16;
    struct Tfs_Data data = { inv: (SymbL < SymbR), fun: fun, left: Left, right: Right};
    data.key = (data.inv) ? ((SymbL << 16) | SymbR) : ((SymbR << 16) | SymbL);
    Hash_Insert(Table, (char *) &data, 0);
}

static Bool
Tfs_Try_Escape( long key, fol_t func, int escape )
{
    Tfs_Escape data;
    return (FOLSMB_ARITY(func) == 1)
        && (data = (Tfs_Escape) Hash_Find( Escape_Table, key ))
        && (data->escape & escape);
}

static int
Escape_Code( fol_t t )
{
    if (FOLINTP(t)) {
        return TFS_X_INT;
    } else if (FOLCHARP(t)) {
        return TFS_X_CHAR;
    } else if (FOLSMBP(t)) {
        return TFS_X_SMB;
    } else if (FOLCMPP(t) && !FOLCMP_DEREFP(t)) {
        return TFS_X_COMPOUND;
    } else {
        return 0; 
    }
}

static Bool
Tfs_Escape_Unif( int escape, SP(X), SP(Right) ) 
{
    switch (escape) {
        case TFS_X_COMPOUND:
            /* need unification to perform occur-check
               could be removed when using cyclic terms
             */
            return Unify(X,Sk(X),Right,Sk(Right));
            break;
        default:
            Unif_Bind(X,Sk(X),Right,Sk(Right));
            Succeed;
            break;
    }
}

static Bool
Tfs_Unif_Aux( SP(Left), SP(Right) ) /* Left is a deref compound */
{
    fol_t funcL = FOLCMP_FUNCTOR(Left);
    long SymbL = ((long) funcL) >> 16;
    int escape = Escape_Code(Right);
    if (escape && Tfs_Try_Escape(SymbL,funcL,escape)) {
        return Tfs_Escape_Unif(escape,FOLCMP_REF(Left,1),Sk(Left),Right,Sk(Right));
    } else {
        fol_t funcR = FOL_FUNCTOR(Right);
        long SymbR = ((long) funcR) >> 16;
        short inv = (SymbL < SymbR);
        long key = inv ? ((SymbL << 16) | SymbR) : ((SymbR << 16) | SymbL);
        Tfs_Data data = (Tfs_Data) Hash_Find(Unif_Table, key);
        if (!data)
            return (Bool) 0;
        else if (inv == data->inv) 
            return (data->left == funcL) && (data->right == funcR)
                && (*data->fun)(Left,Sk(Left),Right,Sk(Right));
        else
            return (data->left == funcR) && (data->right == funcL)
                && (*data->fun)(Right,Sk(Right),Left,Sk(Left));
    }
    
}

Bool
Tfs_Unif( SP(Left), SP(Right))
{
    if (FOLCMPP(Left) && FOLCMP_DEREFP(Left)) {
        return Tfs_Unif_Aux(Left,Sk(Left),Right,Sk(Right));
    } else {
        return Tfs_Unif_Aux(Right,Sk(Right),Left,Sk(Left));
    }
}

Bool
Tfs_Subs(SP(Left), SP(Right))
{
    if (FOLCMPP(Left) && FOLCMP_DEREFP(Left)) {
        fol_t funcL = FOLCMP_FUNCTOR(Left);
        long SymbL = ((long) funcL) >> 16;
        int escape = Escape_Code( Right );
        if (escape && Tfs_Try_Escape(SymbL,funcL,escape)) {
            Subs_Bind(FOLCMP_REF(Left,1),Sk(Left), Right,Sk(Right));
            Succeed;
        } else {
            fol_t funcR = FOL_FUNCTOR(Right);
            long SymbR = ((long) funcR) >> 16;
            short inv = (SymbL < SymbR);
            long key = inv ? ((SymbL << 16) | SymbR) : ((SymbR << 16) | SymbL);
            Tfs_Data data = (Tfs_Data) Hash_Find(Subs_Table, key);
            if (!data)
                return (Bool) 0;
            else if (inv == data->inv) 
                return (data->left == funcL) && (data->right == funcR) &&
                    (*data->fun)(Left,Sk(Left),Right,Sk(Right));
            else
                Fail;
        }
    } else
        Fail;
}