/* $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 */