/* $Id: fol.h 566 2006-11-06 17:20:50Z clerger $
* Copyright (C) 1996 - 2004, 2006 Eric de la Clergerie
* ------------------------------------------------------------
*
* fol -- Implementation of First-Order Logic terms
*
* ------------------------------------------------------------
* Description
*
* union fol : the different kinds of fol objects
* { integer, symbol, variable, compound }
*
* struct folvar : fol variable information
* we maintain a table "folvar_tab" of variables
*
* struct folsmb : fol symbol information
* we maintain a table "folsmb_tab" of symbols
*
* Parameters
* FOLVAR_TAB_SIZE : number of possible variables
* ------------------------------------------------------------
*/
#ifndef FOL_READ
#define FOL_READ
/**********************************************************************
* Parameters
**********************************************************************/
#ifndef FOLVAR_TAB_SIZE
#define FOLVAR_TAB_SIZE 4096
#endif
#ifndef FOLCMP_HEAP_SIZE
#define FOLCMP_HEAP_SIZE 8192
#endif
/**********************************************************************
* Fols
**********************************************************************/
typedef union fol {
int_t integer;
header_t header;
struct folinfo {
obj_t tuple; /* when building also used to save tmp info */
unsigned long weight; /* when building also used to save tmp info */
unsigned long copy_cost;
long length;
struct {
unsigned generic:1;
unsigned feature_term:1;
unsigned deref_compound:1;
} flags;
} info;
struct folcmp {
struct folinfo info;
union fol *functor;
} compound;
} *fol_t;
#define FOLTAG( o ) (((long) o) & TAG_MASK)
#define Not_A_Fol ((fol_t) 0)
/* Fol Integers */
#define FOLINTP( n ) (INTEGERP( (obj_t) n ))
#define DFOLINT( n ) ((fol_t) BINT( n ))
#define CFOLINT( n ) (CINT( (obj_t) n ))
#define UDFOLINT( n ) ((fol_t) UBINT( n ))
#define UCFOLINT( n ) (UCINT( (obj_t) n ))
/* Fol floats */
#define FOLFLTP( f ) (FLOATP( (obj_t) f ))
#define DFOLFLT( f ) ((fol_t) BFLT( f ))
#define CFOLFLT( f ) (CFLT( (obj_t) f ))
/* Fol Chars */
#define FOLCHARP( c ) (CHARP( (obj_t) c ))
#define DFOLCHAR( c ) ((fol_t) BCHAR( c ))
#define CFOLCHAR( c ) (CCHAR( (obj_t) c ))
/* Fol variables */
#define FOLVARP( o ) PAIRP( o )
#define DFOLVAR( o ) ((fol_t) BPAIR( o ))
#define CFOLVAR( o ) ((folvar_t) CPAIR( o ))
/* Fol symbols */
#define DFOLSMB_SHIFT (TAG_SHIFT + 6)
#define DFOLSMBH ((obj_t)BCNST( 7 ))
#define FOLSMBP( o ) \
(((unsigned long)(o) & (unsigned long)((1 << (DFOLSMB_SHIFT)) -1)) == (unsigned long)DFOLSMBH)
#define DFOLSMB( i ) \
((fol_t)((unsigned long)DFOLSMBH + ((unsigned long)((unsigned long)(i) << DFOLSMB_SHIFT))))
#define CFOLSMB( i ) ((unsigned long)((unsigned long)(i)>>DFOLSMB_SHIFT))
/* Some symbols */
#define FOLNIL SIMPLE_FOLSMB_MAKE( 0, 0 ) /* the void list [] */
#define FOLCONS SIMPLE_FOLSMB_MAKE( 1, 2 ) /* the pair constructor . */
#define FOLCURLYCST SIMPLE_FOLSMB_MAKE( 2, 0 ) /* the {} constant */
#define FOLCURLYFUN SIMPLE_FOLSMB_MAKE( 2, 1 ) /* the {} unary functor */
#define FOLHOLE SIMPLE_FOLSMB_MAKE( 7, 0 ) /* the very special hole $$HOLE$$ */
#define FOLHILOG SIMPLE_FOLSMB_MAKE( 3, 0) /* the apply functor for hilog terms */
#define FOLCOMA SIMPLE_FOLSMB_MAKE( 4, 2) /* infix op ',' */
#define FOLSEMICOMA SIMPLE_FOLSMB_MAKE( 5, 2) /* infix op ';' */
#define FOLNUMBERVAR SIMPLE_FOLSMB_MAKE( 6, 1) /* *VAR*( n ) for numbervar */
#define FOLFSET SIMPLE_FOLSMB_MAKE( 8, 0) /* $SET$/2+n for finite set */
#define FOLTUPPLE SIMPLE_FOLSMB_MAKE( 10,1) /* $TUPPLE/1 for tupple */
#define FOLCLOSURE SIMPLE_FOLSMB_MAKE( 11, 2) /* $CLOSURE/2 for closure */
#define FOLLOOP SIMPLE_FOLSMB_MAKE( 12, 3) /* $LOOP/3 for infinite terms */
#define FOLEXTERN SIMPLE_FOLSMB_MAKE( 13, 2) /* $EXTERN/2 for pointers */
/* Fol compounds */
#define TAG_FOLCMP 0
#define DFOLCMP_SIZE sizeof(struct folcmp)
#define DFOLCMP( p ) ((fol_t)((long)p + TAG_FOLCMP))
#define CFOLCMP( p ) ((fol_t)((long)p - TAG_FOLCMP))
#define LIGHT_ALLOCATE_FOLCMP( _arity ) \
( { fol_t an_object ; \
an_object = (fol_t)GC_MALLOC( DFOLCMP_SIZE \
+ _arity*sizeof(fol_t) ); \
DFOLCMP( an_object ); } )
#define ALLOCATE_FOLCMP( _fun, _arity) \
( { fol_t an_object ; \
an_object = (fol_t)GC_MALLOC( DFOLCMP_SIZE \
+ _arity*sizeof(fol_t) ); \
an_object->compound.functor = _fun; \
DFOLCMP( an_object ); } )
#define FOLCMPP( f ) ((((long)f) & TAG_MASK) == TAG_FOLCMP)
#define FOLCMP( f ) (CFOLCMP( f )->compound)
#define FOLCMP_INFO( f ) (CFOLCMP( f )->info)
#define FOLCMP_FUNCTOR( f ) (FOLCMP( f ).functor)
#define FOLCMP_ARITY( f ) (FOLSMB_ARITY( FOLCMP_FUNCTOR( f ) ))
#define FOLCMP_NAME( f ) (FOLSMB_NAME(FOLCMP_FUNCTOR( f )))
#define FOLCMP_REF( f, i ) (&(FOLCMP( f ).functor))[ i ]
#define FOLCMP_SET( f, i, o ) ((FOLCMP_REF( f, i ) = o))
/* Fol compound info */
#define FOLINFO_FILL( o, _tuple, _weight, _copy, _length, _generic) \
({ struct folinfo *info ; \
info = (struct folinfo *) CFOLCMP( o ); \
info->tuple = _tuple; \
info->weight = _weight; \
info->copy_cost = _copy; \
info->length = _length; \
info->flags.generic = _generic; \
})
#define FOLINFO_TUPLE( o ) (FOLCMP_INFO( o ).tuple)
#define FOLINFO_WEIGHT( o ) (FOLCMP_INFO( o ).weight)
#define FOLINFO_COPY_COST( o ) (FOLCMP_INFO( o ).copy_cost)
#define FOLINFO_LENGTH( o ) (FOLCMP_INFO( o ).length)
#define FOLINFO_GENERIC( o ) (FOLCMP_INFO( o ).flags.generic)
#define FOLINFO_COPY_COST_SET(o, c) (FOLINFO_COPY_COST( o ) = c)
#define FOLINFO_FEATURE( o ) (FOLCMP_INFO( o ).flags.feature_term)
#define FOLINFO_DEREF( o ) (FOLCMP_INFO( o ).flags.deref_compound)
/* Fol pair */
#define FOLPAIRP( l ) \
(FOLCMPP( l ) && \
(unsigned long)FOLCMP_FUNCTOR( l ) == (unsigned long)FOLCONS)
#define FOLPAIR_CAR( l ) (FOLCMP_REF( l , 1))
#define FOLPAIR_CDR( l ) (FOLCMP_REF( l , 2))
/* Fol Finite Set */
#define FOLFSETP( l ) \
(FOLCMPP( l ) && \
FOLSMB_CONVERT_ARITY(FOLCMP_FUNCTOR( l ),0) == FOLFSET)
/* Fol Loop Term */
#define FOLLOOPP(l) \
(FOLCMPP( l ) && \
(unsigned long)FOLCMP_FUNCTOR( l ) == (unsigned long)FOLLOOP)
#define LOOP_BOUNDP(r) (FOLCMP_REF(r,3) == DFOLINT(1))
/**********************************************************************
* Folcmp
**********************************************************************/
#define H ( (fol_t *) REG(I_HEAP) )
#define H_STOP ( (fol_t *) REG(I_HEAP_STOP) )
#define LVALUE_H ( LVALUE_REG(I_HEAP) )
#define LVALUE_H_STOP ( LVALUE_REG(I_HEAP_STOP) )
#define FOLCMP_WRITE_START( f, n ) \
({ \
struct folcmp *p = ((struct folcmp *) H); \
p->info.weight = (unsigned long) H_STOP; \
p->functor = f; \
p->info.flags.deref_compound=0; \
LVALUE_H_STOP = REG_VALUE(H); \
LVALUE_H = REG_VALUE((fol_t *) (&p->functor + 1)); \
*H_STOP = (fol_t) H+n; \
p; \
})
#define FOLCMP_WRITE_LIGHT_START \
({ \
struct folcmp *p = ((struct folcmp *) H); \
p->info.weight = (unsigned long) H_STOP; \
p->info.flags.deref_compound=0; \
LVALUE_H_STOP = REG_VALUE(H); \
LVALUE_H = REG_VALUE((fol_t *) (&p->functor + 1)); \
p; \
})
#define FOLCMP_WRITE( v ) \
({ \
*H = v; \
LVALUE_H= REG_VALUE(H+1); \
})
#define FOLCMP_WRITE_STOP \
({ \
fol_t v = folcmp_find( DFOLCMP( (fol_t) H_STOP ) ); \
FOLCMP_WRITE_ABORT; \
v; \
})
#define FOLCMP_WRITE_LIGHT_STOP( f, n ) \
({ struct folcmp *p = (struct folcmp *) H_STOP; \
p->functor = f; \
FOLCMP_WRITE_STOP; \
})
#define FOLCMP_WRITE_ABORT \
({ \
LVALUE_H = REG_VALUE(H_STOP); \
LVALUE_H_STOP = REG_VALUE((fol_t *) ((struct folcmp *) H_STOP)->info.weight); \
})
/* the following defines may be used during term writing to set some flags */
#define FOLCMP_WRITE_SET_DEREF_FLAG \
({ \
((struct folinfo *) H_STOP)->flags.deref_compound = 1; \
})
#define FOLCMP_WRITE_SET_FEATURE_FLAG \
({ \
((struct folinfo *) H_STOP)->flags.feature_term = 1; \
})
/**********************************************************************
* Variable
**********************************************************************/
typedef struct folvar {
struct binding_box *unifbindings; /* pointer to local bindings (see trail.h) */
struct binding_box *subbindings; /* Idem */
unsigned long index;
} *folvar_t;
extern struct folvar folvar_tab[];
#define FOLVAR_SIZE sizeof(struct folvar)
#define FOLVAR( o ) (CFOLVAR( o ))
#define FOLVAR_INDEX( o ) (FOLVAR( o )->index)
#define FOLVAR_FROM_INDEX( i ) (DFOLVAR(&folvar_tab[i]))
#define FOLVAR_UNIF_REF( o ) (FOLVAR( o )->unifbindings)
#define FOLVAR_UNIF_SET( o, v) ((FOLVAR_UNIF_REF( o ) = v))
#define FOLVAR_SUB_REF( o ) (FOLVAR( o )->subbindings)
#define FOLVAR_SUB_SET( o, v) ((FOLVAR_SUB_REF( o ) = v))
/**********************************************************************
* Symbols
*
* op info = <prec:27> <prefix:1> <infix:1> <postfix:1> <lassoc:1> <rassoc:1>
**********************************************************************/
typedef struct folsmb {
char *name;
fol_t module;
unsigned int prefix, infix_or_postfix;
unsigned int is_feature:1;
unsigned int is_fset:1;
unsigned int is_hilog:1;
unsigned int to_quote:1;
unsigned int to_scan:1;
} *folsmb_t;
extern folsmb_t *folsmb_tab;
#define OPINFO_PREFIX 16
#define OPINFO_INFIX 8
#define OPINFO_POSTFIX 4
#define OPINFO_LASSOC 2
#define OPINFO_RASSOC 1
#define OPINFO_PREC(info) ((int) (info >> 5 ))
#define OPINFO_LPREC(info) (OPINFO_PREC(info) - ((info & OPINFO_LASSOC) ? 0 : 1))
#define OPINFO_RPREC(info) (OPINFO_PREC(info) - ((info & OPINFO_RASSOC) ? 0 : 1))
#define OPINFO_MAKE(_prec,_kind,_la,_ra) ((_prec << 5) | (_kind) | (_la) | (_ra))
#define FOLSMB_SIZE sizeof(struct folsmb)
#define FOLSMB_ARITY_SHIFT 8
#define FOLSMB_ARITY_MASK ((1 << FOLSMB_ARITY_SHIFT) - 1)
#define FOLSMB_ARITY( o ) (CFOLSMB( o ) & FOLSMB_ARITY_MASK)
#define FOLSMB_INDEX( o ) (CFOLSMB( o ) >> FOLSMB_ARITY_SHIFT)
#define SIMPLE_FOLSMB_MAKE( i, a) DFOLSMB( (i << FOLSMB_ARITY_SHIFT) + a )
// EVDLC 06/11/06 The following definition is a workaround of a bug for GCC 4.1.1
// The SIMPLE_FOLSMB_MAKE version raises an
// internal compiler error: in compare_values, at tree-vrp.c
#define FOLSMB_MAKE( i, a) \
({ unsigned long _tmp = (i << FOLSMB_ARITY_SHIFT) + a; \
DFOLSMB( _tmp ); \
})
#define FOLSMB( o ) folsmb_tab[FOLSMB_INDEX(o)]
#define FOLSMB_NAME( o ) FOLSMB( o )->name
#define FOLSMB_MODULE(o) FOLSMB( o )->module
#define FOLSMB_CONVERT_ARITY( s, a ) FOLSMB_MAKE( FOLSMB_INDEX( s ), a )
#define FOLSMB_PREFIX_P(o) ((FOLSMB_ARITY(o) == 1) && FOLSMB(o)->prefix)
#define FOLSMB_POSTFIX_P(o) ((FOLSMB_ARITY(o) == 1) && (FOLSMB(o)->infix_or_postfix & OPINFO_POSTFIX ))
#define FOLSMB_INFIX_P(o) ((FOLSMB_ARITY(o) == 2) && (FOLSMB(o)->infix_or_postfix & OPINFO_INFIX))
#define FOLSMB_PREFIX(o) FOLSMB(o)->prefix
#define FOLSMB_POSTFIX(o) FOLSMB(o)->infix_or_postfix
#define FOLSMB_INFIX(o) FOLSMB(o)->infix_or_postfix
#define FOLSMB_HILOG_P(o) (FOLSMB(o)->is_hilog)
#define FOLSMB_SET_HILOG(o) (FOLSMB(o)->is_hilog = 1)
#define FOLSMB_FSET(o) (FOLSMB(o)->is_fset)
#define FOLSMB_SET_FSET(o) (FOLSMB(o)->is_fset = 1)
/**********************************************************************
* Characters
**********************************************************************/
#define LA 1 /* layout character */
#define SC 2 /* solo character */
#define QT 4 /* quote */
#define DQ 8 /* double quote */
#define BQ 16 /* back quote */
#define GR 32 /* graphic char */
#define PC 64 /* ponctuation character */
#define DI 128 /* digit */
#define UL 256 /* underline */
#define CL 512 /* capital letter */
#define SL 1024 /* small letter */
#define CM 2048 /* comment character (%) */
#define EX 4096 /* extended character set*/
extern int char_type[];
extern char escape_symbol[];
extern char escape_char[];
/**********************************************************************
* FOLSMB INFO TYPES
**********************************************************************/
#define INFO_FEATURE BINT(3)
#define INFO_DECLARATION BINT(4)
#define INFO_DEREFTERM BINT(5)
#define INFO_SUBTYPES BINT(6)
#define INFO_INTRO BINT(7)
#define INFO_FSET BINT(8)
/**********************************************************************
* Macros
**********************************************************************/
#define FOLNILP( o ) ((unsigned long)(o) == (unsigned long)FOLNIL)
#define FOLCMP_SAMEFUNP( a, b) ((unsigned long)FOLCMP_FUNCTOR( a ) == (unsigned long)FOLCMP_FUNCTOR( b ))
#define FOL_NUMBERP(o) ( FOLINTP( o ) || FOLFLTP(o))
#define FOL_ICSTP( o ) ( FOLINTP( o ) || FOLCHARP( o ) || FOLFLTP( o ))
/* constants now have their last bit set to 1 */
#define FOL_CSTP( o ) ( (unsigned long) (o) & 1 )
#define FOL_LISTP( o ) ( FOLNILP( o ) || FOLPAIRP( o ) )
#define FOLCMP_GROUNDP( o ) (FOLINFO_TUPLE( o ) == BNIL)
#define FOL_GROUNDP( o ) \
( FOL_CSTP( o ) || \
(FOLCMPP( o ) && FOLCMP_GROUNDP( o )))
#define FOLCURLYFUN_P( o ) ( o == FOLCURLYFUN )
#define FOL_FUNCTOR( o ) (FOLCMPP( o ) ? FOLCMP_FUNCTOR( o ) : o)
#define FOL_ARITY( o ) (FOLCMPP( o ) ? FOLCMP_ARITY( o ) : 0)
#define FOL_TUPLE( o ) \
((FOLVARP( o ) ? MAKE_PAIR( o , BNIL) : \
(FOLCMPP( o ) ? (FOLCMP_DEREFP(o) ? MAKE_PAIR(o, BNIL) : FOLINFO_TUPLE( o )) : BNIL )))
#define FOL_WEIGHT( o ) \
((FOLVARP( o ) ? 0 : \
(FOLCMPP( o ) ? FOLINFO_WEIGHT( o ) : 1 )))
#define FOL_COPY_COST( o ) \
((FOLVARP( o ) ? 1 : \
(FOLCMPP( o ) ? FOLINFO_COPY_COST( o ) : 0 )))
#define FOL_LENGTH( o ) \
((FOLVARP( o ) ? -1 : \
(FOLCMPP( o ) ? FOLINFO_LENGTH( o ) : 0 )))
#define SFOL_EQ( o1, k1, o2, k2) ( o1 == o2 && k1 == k2 )
#define FOLSMB_CREATE( name ) find_folsmb( name , 0 )
#define FOLCMP_DEREFP( o ) (FOLINFO_DEREF(o))
#define FOL_DEREFP( o ) (FOLVARP(o) || (FOLCMPP(o) && FOLCMP_DEREFP(o)))
/* extract the var part of a deref term */
#define FOLCMP_DEREF_VAR( o ) (FOLCMP_REF(o,1))
#define FOL_DEREF_VAR( o ) (FOLVARP( o ) ? o : FOLCMP_DEREF_VAR(o))
#define FOL_UNIF_REF( o ) (FOLVAR_UNIF_REF( FOL_DEREF_VAR( o )))
#define FOL_SUBS_REF( o ) (FOLVAR_SUB_REF( FOL_DEREF_VAR( o )))
#define FOLCMP_FEATUREP( o ) (FOLINFO_FEATURE(o))
/* Address as Fol Integers
Address may correspond to char * and may not be aligned
(for instance with function DyALog_Format)
=> we do not assume 2 low bits are 00
on the other hand, we assume that the 2 highest bits (on left) are 00
should add an assert to test it !
2001/11/15 the assertion does not hold !
Solution
- aligned pointers are encoded as FOLINT (the two lowest bits used for tagging)
- unaligned pointers are encoded in a fol structure with functor
$EXTERN/2
So memory allocation is needed for some ptr but I donot see how to avoid it !
*/
fol_t encode_extern_ptr(const void *);
#define DYALOG_TO_POINTER(n) ((void *)(FOLINTP(n) ? ((((unsigned long) n) - TAG_INT )) : ((CFOLINT( FOLCMP_REF(n,1) ) << 8 ) | CFOLINT( FOLCMP_REF(n,2) ))))
#define POINTER_TO_DYALOG(p) (((long)p & TAG_MASK) ? encode_extern_ptr(p) : ((fol_t)(((unsigned long) p) | TAG_INT)))
#define FOL_POINTERP(x) (FOLINTP(x) || (FOLCMPP(x) && FOLCMP_FUNCTOR(x) == FOLEXTERN))
/**********************************************************************/
/* Name Spaces */
/**********************************************************************/
#define FEATURE_SPACE "$ft"
#define FSET_SPACE "$fset"
/**********************************************************************/
/* FSET defines */
/**********************************************************************/
// Could extend to 30 or even 31, but would need to modify too much stuff
#define FSET_BIT_PER_WORD 29
#define FSET_ARITY_TO_WORD(n) ((1+(n / FSET_BIT_PER_WORD)))
// this limit could be removed by switching to list representation
// for fset
#define FSET_MAX_ARITY 255
/**********************************************************************
* Externs
**********************************************************************/
extern fol_t find_folsmb( const char*, unsigned short);
extern fol_t find_module_folsmb( const char*, unsigned short, const fol_t module);
extern fol_t folcmp_make( unsigned short, fol_t, ...);
extern fol_t fol_create_generic_term( const fol_t, const unsigned long);
extern fol_t folcmp_create_pair( fol_t, fol_t);
extern fol_t folcmp_create_binary(const char *, const fol_t, const fol_t);
extern fol_t folcmp_create_unary(const char *, const fol_t);
extern fol_t folcmp_find( fol_t );
extern obj_t is_folsmb( const char *, unsigned short );
extern void dyalog_printf( const char *, ...);
extern Bool folsmb_prefix_p( fol_t );
extern Bool folsmb_postfix_p( fol_t );
extern Bool folsmb_infix_p( fol_t );
extern int folsmb_lprec( fol_t );
extern int folsmb_rprec( fol_t );
extern int folsmb_prec( fol_t );
extern obj_t folsmb_feature_info( fol_t );
extern void folsmb_feature_set( fol_t, fol_t);
extern obj_t folsmb_fset_info( fol_t );
extern void folsmb_fset_set( fol_t, fol_t);
extern void folsmb_info_set( fol_t, obj_t, obj_t );
extern void install_opmode_wrapper(int, char *,char *);
extern fol_t find_module_folsmb( const char *, const unsigned short, const fol_t);
extern fol_t find_folsmb(const char *, const unsigned short);
extern obj_t is_module_folsmb( const char *, const unsigned short, const fol_t);
extern void folsmb_switch_derefterm(fol_t);
extern Bool folsmb_derefterm_info(fol_t);
extern unsigned long hash_fol(const fol_t);
#endif /* FOL_READ */
