/* 
 ******************************************************************
 * $Id: tree-indexing.h 514 2006-03-06 16:44:41Z clerger $
 * Copyright (C) 1998, 2006 by INRIA 
 * Author: Eric de la Clergerie <Eric.De_La_Clergerie@inria.fr>
 * ----------------------------------------------------------------
 *
 *  tree-indexing.h -- Header file for tree-indexing.c
 *
 * ----------------------------------------------------------------
 * Description
 * 
 * ----------------------------------------------------------------
 */

typedef void *Closure;
typedef Bool (* ClosedFn) (tabobj_t,Closure);

#define INDEXATION_MAX_DEPTH        5

typedef struct Trailed_HashScan {
    boxtype type;               /* HASH_SCAN */
    HashScan scan;
} *Trailed_HashScan;

typedef struct Resume {
    boxtype type;               /* INDEXATION */
    struct Resume *prev;
    int depth;
    Closure closure;
    fol_t A;
    struct ResumeInfo {
        fol_t   *arg;
        fol_t   *stop;
        fkey_t  k;
    } info[INDEXATION_MAX_DEPTH+2];
} *Resume;

typedef struct Undo {
    boxtype type;
    union {
        int forward;
        struct Upward {
            fol_t *stop;
            fkey_t k;
        } upward;
    }  value;
} *Undo;

#define IP ((Resume) REG(I_IP))
#define LVALUE_IP (LVALUE_REG(I_IP))

inline extern void
Untrail_Forward(Undo undo)
{
    int pop = undo->value.forward;
            
    V_DISPLAY( "\tundo forward %d\n", pop );
            
    for (; pop ; pop--, (IP->info[IP->depth].arg)--, IP->depth++);
    (IP->info[IP->depth].arg)--;
}

inline extern void
Untrail_Upward(Undo undo)
{
    struct Upward *s=&(undo->value.upward);
    int depth = (IP->depth)--;
    
    V_DISPLAY( "\tundo pushing : restoring %&s from depth %d\n",
               DFOLINT(0), s->k, depth);
    
    IP->info[depth] = (struct ResumeInfo) { arg  : s->stop, stop : s->stop, k: s->k };
}