com.cyc.cycjava.cycl.inference
Class inference_completeness_utilities

java.lang.Object
  com.cyc.tool.subl.util.SubLTrampolineFile
      com.cyc.tool.subl.util.SubLTranslatedFile
          com.cyc.cycjava.cycl.inference.inference_completeness_utilities

All Implemented Interfaces:

CommonSymbols, SubLFile

public final class inference_completeness_utilities
extends SubLTranslatedFile

Nested Class Summary

Nested classes/interfaces inherited from class com.cyc.tool.subl.util.SubLTranslatedFile

SubLTranslatedFile.SubL

Field Summary

static SubLObject	$const10$isa
static SubLSymbol	$kw1$_MEMOIZED_ITEM_NOT_FOUND_
static SubLSymbol	$kw9$IGNORE
static SubLSymbol	$sym0$INFERENCE_MINIMIZE_EXTENT_
static SubLSymbol	$sym11$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_VIA_BACKCHAIN_GAFS
static SubLSymbol	$sym2$INFERENCE_COMPLETE_EXTENT_ASSERTED_FOR_VALUE_IN_ARG_GAFS
static SubLSymbol	$sym3$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_GAFS
static SubLSymbol	$sym4$INFERENCE_COMPLETE_EXTENT_DECIDABLE_GAFS
static SubLSymbol	$sym5$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_FOR_ARG_GAFS
static SubLSymbol	$sym6$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_FOR_VALUE_IN_ARG_GAFS
static SubLSymbol	$sym7$INFERENCE_COMPLETE_EXTENT_DECIDABLE_FOR_VALUE_IN_ARG_GAFS
static SubLSymbol	$sym8$INFERENCE_COMPLETELY_DECIDABLE_COLLECTION_GAFS
static SubLFile	me
static java.lang.String	myName

Fields inherited from class com.cyc.tool.subl.util.SubLTranslatedFile

EMPTY_SUBL_OBJECT_ARRAY

Fields inherited from interface com.cyc.tool.subl.jrtl.nativeCode.subLisp.CommonSymbols

ANSWER_TAG, APPEND_KEYWORD, APPEND_STACK_TRACES_TO_ERROR_MESSAGES, AREF, ASSEMBLE_FIXNUMS_TO_INTEGER, ATOM, BIGNUMP, BINARY_KEYWORD, BINDING_TYPE, BOOLEANP, CAAR, CADR, CAND, CAR, CCATCH, CDEC, CDESTRUCTURING_BIND, CDO, CDO_ALL_SYMBOLS, CDO_EXTERNAL_SYMBOLS, CDO_SYMBOLS, CDOHASH, CDOLIST, CDOTIMES, CDR, CHAR, CHAR_E_SYMBOL, CHAR_EQUAL_SYMBOL, CHAR_GREATER_THAN_OR_EQUAL_SYMBOL, CHAR_GREATER_THAN_SYMBOL, CHAR_GT_SYMBOL, CHAR_GTE_SYMBOL, CHAR_LESS_THAN_OR_EQUAL_SYMBOL, CHAR_LESS_THAN_SYMBOL, CHAR_LT_SYMBOL, CHAR_LTE_SYMBOL, CHAR_NE_SYMBOL, CHAR_NOT_EQUAL_SYMBOL, CHARACTERP, CHECK_TYPE, CINC, CLET, CMULTIPLE_VALUE_BIND, CNOT, CONS, CONSP, CONSTANT, COR, CPOP, CPROGV, CPUSH, CPUSHNEW, CREATE_KEYWORD, CSETF, CSETQ, CSOME, CTIME, CUNWIND_PROTECT, CVS_ID, DEBUG_IO, DECLAIM, DECLARE, DEFCONSTANT, DEFINE, DEFLEXICAL, DEFMACRO, DEFPARAMETER, DEFVAR, DIRECTION_KEYWORD, DYNAMIC, EIGHT_INTEGER, EIGHTEEN_INTEGER, ELEMENT_TYPE_KEYWORD, ELEVEN_INTEGER, END_KEYWORD, ENFORCE_MUST, ENFORCE_TYPE, EQ, EQL, EQUAL, EQUALP, ERROR, ERROR_KEYWORD, ERROR_OUTPUT, EVAL, EXTERNAL_FORMAT_KEYWORD, EXTERNAL_KEYWORD, FIF, FIFTEEN_INTEGER, FIRST, FIVE_INTEGER, FIXNUMP, FLOATP, FOUR_INTEGER, FOURTEEN_INTEGER, FUNCTION, FUNCTION_SPEC_P, FUNCTIONP, FUNLESS, FWHEN, GET, GETHASH, GETHASH_WITHOUT_VALUES, GUID_P, HASH_TABLE_ITERATOR_P, HASH_TABLE_P, IDENTITY, IF_DOES_NOT_EXIST_KEYWORD, IF_EXISTS_KEYWORD, IGNORE, INITIALIZATION_TYPE, INITIALIZER, INPUT_KEYWORD, INPUT_STREAM_P, INTEGERP, INTERNAL_KEYWORD, IO_KEYWORD, KEYWORDP, KILL_KEYWORD, LAMBDA_SYMBOL, LEXICAL, LIST, LISTP, LISTS, LOCK_P, LONG_BIGNUM_P, MACRO_ENV, MACRO_FORM, MEDIUM_BIGNUM_P, MEMBER, MINUS_ONE_INTEGER, MULTIPLE_VALUE_LIST, MUST, NCONC, NEW_VERSION_KEYWORD, NIL, NINE_INTEGER, NINETEEN_INTEGER, NREVERSE, NTH, NTH_VALUE, NULL, NULL_INPUT, NULL_OUTPUT, NUM_E_SYMBOL, NUM_GT_SYMBOL, NUM_GTE_SYMBOL, NUM_LT_SYMBOL, NUM_LTE_SYMBOL, NUM_NE_SYMBOL, NUMBERP, ONE_HUNDRED_THIRTY_SEVEN_INTEGER, ONE_HUNDRED_TWENTY_SEVEN_INTEGER, ONE_INTEGER, ONE_THOUSAND_INTEGER, OPTIONAL_SYMBOL, OTHERWISE, OUTPUT_KEYWORD, OUTPUT_STREAM_P, OVERWRITE_KEYWORD, PACKAGEP, PCASE, PCOND, PIF, PROBE_KEYWORD, PROCESS_TO_END, PROCESSP, PROCLAIM, PROGN, PUNLESS, PWHEN, QUERY_IO, QUIT, QUOTE, RENAME_AND_DELETE_KEYWORD, REST_SYMBOL, RET, RET_NIL, RET_T, RETURN_TAG, REVERSE, RW_LOCK_P, SECOND, SEQUENCEP, SEVEN_INTEGER, SEVENTEEN_INTEGER, SHORT_BIGNUM_P, SHOW_STACK_TRACES, SIX_INTEGER, SIXTEEN_INTEGER, SIXTY_FOUR_INTEGER, SORT, SSS, STANDARD_INPUT, STANDARD_OUTPUT, START_KEYWORD, STREAMP, STRING_E_SYMBOL, STRING_EQUAL_SYMBOL, STRING_GREATER_THAN_OR_EQUAL_SYMBOL, STRING_GREATER_THAN_SYMBOL, STRING_GT_SYMBOL, STRING_GTE_SYMBOL, STRING_LESS_THAN_OR_EQUAL_SYMBOL, STRING_LESS_THAN_SYMBOL, STRING_LT_SYMBOL, STRING_LTE_SYMBOL, STRING_NE_SYMBOL, STRING_NOT_EQUAL_SYMBOL, STRINGP, STRUCTURE_P, SUPERSEDE_KEYWORD, SUSPEND_TYPE_CHECKING, SYMBOL_FUNCTION, SYMBOL_VALUE, SYMBOLP, T, TEN_INTEGER, TERMINAL_IO, TEXT_KEYWORD, THIRTEEN_INTEGER, THIRTY_FOUR_INTEGER, THIRTY_THREE_INTEGER, THIRTY_TWO_INTEGER, THREE_INTEGER, TRACE_OUTPUT, TRUE, TWELVE_INTEGER, TWENTY_INTEGER, TWO_HUNDRED_FIFTY_FOUR_INTEGER, TWO_HUNDRED_FORTY_FOUR_INTEGER, TWO_INTEGER, UNDECLARED, UNPROVIDED, VALUES, VECTOR, VECTORP, WITH_ERROR_HANDLER, WITH_STATIC_AREA, WITH_THREAD_PRIVATE_AREA, WITH_WORKING_AREA, WORLD, ZERO_DOUBLE, ZERO_INTEGER

Method Summary

static SubLObject	completeness_constraint_mt(SubLObject mt) Assuming that we are doing inference in MT, return the mt in which we look for completeness assertions.
static SubLObject	declare_inference_completeness_utilities_file()
void	declareFunctions() Declares the mapping between functions and symbols for all named functions defined in the file.
static SubLObject	inference_complete_asentP(SubLObject asent, SubLObject mt)
static SubLObject	inference_complete_extent_asserted_for_value_in_arg_gafs_internal(SubLObject predicate, SubLObject value, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_asserted_for_value_in_arg_gafs(SubLObject predicate, SubLObject value, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_asserted_gaf(SubLObject predicate, SubLObject mt)
static SubLObject	inference_complete_extent_decidable_for_value_in_arg_gafs_internal(SubLObject predicate, SubLObject value, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_decidable_for_value_in_arg_gafs(SubLObject predicate, SubLObject value, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_decidable_gafs_internal(SubLObject predicate, SubLObject mt)
static SubLObject	inference_complete_extent_decidable_gafs(SubLObject predicate, SubLObject mt)
static SubLObject	inference_complete_extent_enumerable_for_arg_gafs_internal(SubLObject predicate, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_enumerable_for_arg_gafs(SubLObject predicate, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_enumerable_for_value_in_arg_gafs_internal(SubLObject predicate, SubLObject value, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_enumerable_for_value_in_arg_gafs(SubLObject predicate, SubLObject value, SubLObject argnum, SubLObject mt)
static SubLObject	inference_complete_extent_enumerable_gafs_internal(SubLObject predicate, SubLObject mt)
static SubLObject	inference_complete_extent_enumerable_gafs(SubLObject predicate, SubLObject mt)
static SubLObject	inference_completely_asserted_asent_gaf(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_asserted_asent_gafs(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_asserted_asentP(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_decidable_asent_gaf(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_decidable_asent_gafs(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_decidable_asentP(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_enumerable_asent_gaf(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_enumerable_asent_gafs(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_enumerable_asentP(SubLObject asent, SubLObject mt)
static SubLObject	inference_completely_enumerable_collection_gaf(SubLObject collection, SubLObject mt)
static SubLObject	init_inference_completeness_utilities_file()
void	initializeVariables() Initializes all global variables and private internal variables for constants defined in the file.
void	runTopLevelForms() Runs all top-level forms in order.
static SubLObject	setup_inference_completeness_utilities_file()

Methods inherited from class com.cyc.tool.subl.util.SubLTranslatedFile

extractFunctionNamed

Methods inherited from class com.cyc.tool.subl.util.SubLTrampolineFile

checkType, enforceType, extractBinaryFunc, extractCount, extractEnd, extractEndUsingSize, extractPackage, extractStart, extractUnaryFunc, main

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

me

public static final SubLFile me

myName

public static final java.lang.String myName

See Also:

Constant Field Values

$sym0$INFERENCE_MINIMIZE_EXTENT_

public static final SubLSymbol $sym0$INFERENCE_MINIMIZE_EXTENT_

$kw1$_MEMOIZED_ITEM_NOT_FOUND_

public static final SubLSymbol $kw1$_MEMOIZED_ITEM_NOT_FOUND_

$sym2$INFERENCE_COMPLETE_EXTENT_ASSERTED_FOR_VALUE_IN_ARG_GAFS

public static final SubLSymbol $sym2$INFERENCE_COMPLETE_EXTENT_ASSERTED_FOR_VALUE_IN_ARG_GAFS

$sym3$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_GAFS

public static final SubLSymbol $sym3$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_GAFS

$sym4$INFERENCE_COMPLETE_EXTENT_DECIDABLE_GAFS

public static final SubLSymbol $sym4$INFERENCE_COMPLETE_EXTENT_DECIDABLE_GAFS

$sym5$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_FOR_ARG_GAFS

public static final SubLSymbol $sym5$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_FOR_ARG_GAFS

$sym6$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_FOR_VALUE_IN_ARG_GAFS

public static final SubLSymbol $sym6$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_FOR_VALUE_IN_ARG_GAFS

$sym7$INFERENCE_COMPLETE_EXTENT_DECIDABLE_FOR_VALUE_IN_ARG_GAFS

public static final SubLSymbol $sym7$INFERENCE_COMPLETE_EXTENT_DECIDABLE_FOR_VALUE_IN_ARG_GAFS

$sym8$INFERENCE_COMPLETELY_DECIDABLE_COLLECTION_GAFS

public static final SubLSymbol $sym8$INFERENCE_COMPLETELY_DECIDABLE_COLLECTION_GAFS

$kw9$IGNORE

public static final SubLSymbol $kw9$IGNORE

$const10$isa

public static final SubLObject $const10$isa

$sym11$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_VIA_BACKCHAIN_GAFS

public static final SubLSymbol $sym11$INFERENCE_COMPLETE_EXTENT_ENUMERABLE_VIA_BACKCHAIN_GAFS

Method Detail

inference_complete_extent_asserted_gaf

public static final SubLObject inference_complete_extent_asserted_gaf(SubLObject predicate,
                                                                      SubLObject mt)

Returns:

nil or gaf-assertion?; a gaf assertion justifying the fact that PREDICATE's extent is completely asserted in MT and its genlMts. If there is more than one such assertion, the inferentially strongest one will be returned.

inference_complete_extent_asserted_for_value_in_arg_gafs_internal

public static final SubLObject inference_complete_extent_asserted_for_value_in_arg_gafs_internal(SubLObject predicate,
                                                                                                 SubLObject value,
                                                                                                 SubLObject argnum,
                                                                                                 SubLObject mt)

Returns:

list of gaf-assertion?; a list of gaf assertions, each of which independently justify the fact that PREDICATE's extent for VALUE in ARGNUM is completely asserted in MT and its genlMts. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_complete_extent_asserted_for_value_in_arg_gafs

public static final SubLObject inference_complete_extent_asserted_for_value_in_arg_gafs(SubLObject predicate,
                                                                                        SubLObject value,
                                                                                        SubLObject argnum,
                                                                                        SubLObject mt)

inference_complete_extent_enumerable_gafs_internal

public static final SubLObject inference_complete_extent_enumerable_gafs_internal(SubLObject predicate,
                                                                                  SubLObject mt)

Returns:

list of gaf-assertion?; a list of gaf assertions, each of which independently justify the fact that PREDICATE's extent is completely enumerable in MT. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_complete_extent_enumerable_gafs

public static final SubLObject inference_complete_extent_enumerable_gafs(SubLObject predicate,
                                                                         SubLObject mt)

inference_complete_extent_decidable_gafs_internal

public static final SubLObject inference_complete_extent_decidable_gafs_internal(SubLObject predicate,
                                                                                 SubLObject mt)

Returns:

list of gaf-assertion?; a list of gaf assertions, each of which independently justify the fact that PREDICATE's extent is completely decidable in MT. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_complete_extent_decidable_gafs

public static final SubLObject inference_complete_extent_decidable_gafs(SubLObject predicate,
                                                                        SubLObject mt)

inference_complete_extent_enumerable_for_arg_gafs_internal

public static final SubLObject inference_complete_extent_enumerable_for_arg_gafs_internal(SubLObject predicate,
                                                                                          SubLObject argnum,
                                                                                          SubLObject mt)

Returns:

list of gaf-assertion?; a list of gaf assertions, each of which independently justify the fact that PREDICATE's extent is completely enumerable for ARGNUM in MT. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_complete_extent_enumerable_for_arg_gafs

public static final SubLObject inference_complete_extent_enumerable_for_arg_gafs(SubLObject predicate,
                                                                                 SubLObject argnum,
                                                                                 SubLObject mt)

inference_complete_extent_enumerable_for_value_in_arg_gafs_internal

public static final SubLObject inference_complete_extent_enumerable_for_value_in_arg_gafs_internal(SubLObject predicate,
                                                                                                   SubLObject value,
                                                                                                   SubLObject argnum,
                                                                                                   SubLObject mt)

Returns:

list of gaf-assertion?; a list of gaf assertions, each of which independently justify the fact that PREDICATE's extent is completely enumerable for VALUE in ARGNUM in MT. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_complete_extent_enumerable_for_value_in_arg_gafs

public static final SubLObject inference_complete_extent_enumerable_for_value_in_arg_gafs(SubLObject predicate,
                                                                                          SubLObject value,
                                                                                          SubLObject argnum,
                                                                                          SubLObject mt)

inference_complete_extent_decidable_for_value_in_arg_gafs_internal

public static final SubLObject inference_complete_extent_decidable_for_value_in_arg_gafs_internal(SubLObject predicate,
                                                                                                  SubLObject value,
                                                                                                  SubLObject argnum,
                                                                                                  SubLObject mt)

Returns:

list of gaf-assertion?; a list of gaf assertions, each of which independently justify the fact that PREDICATE's extent is completely decidable for ARGNUM in MT. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_complete_extent_decidable_for_value_in_arg_gafs

public static final SubLObject inference_complete_extent_decidable_for_value_in_arg_gafs(SubLObject predicate,
                                                                                         SubLObject value,
                                                                                         SubLObject argnum,
                                                                                         SubLObject mt)

inference_completely_enumerable_collection_gaf

public static final SubLObject inference_completely_enumerable_collection_gaf(SubLObject collection,
                                                                              SubLObject mt)

Returns:

nil or gaf-assertion?; a gaf assertion justifying the fact that COLLECTION is completely enumerable in MT. If there is more than one such assertion, the inferentially strongest one will be returned.

inference_complete_asentP

public static final SubLObject inference_complete_asentP(SubLObject asent,
                                                         SubLObject mt)

Returns:

boolean; whether all bindings for free variables in ASENT can be completely enumerated in MT. If ASENT is closed, return whether the truth of ASENT can be completely decided with no transformation.

inference_completely_asserted_asentP

public static final SubLObject inference_completely_asserted_asentP(SubLObject asent,
                                                                    SubLObject mt)

Returns:

boolean; whether all bindings for free variables in ASENT are completely asserted in MT. If ASENT is closed, return whether the truth of ASENT can be completely decided via assertion lookup.

inference_completely_asserted_asent_gaf

public static final SubLObject inference_completely_asserted_asent_gaf(SubLObject asent,
                                                                       SubLObject mt)

Returns:

nil or gaf-assertion?; if all bindings for free variables in ASENT are completely asserted in MT, or if ASENT is closed and its truth can be completely decided via assertion lookup, return a gaf assertion justifying this claim.

inference_completely_asserted_asent_gafs

public static final SubLObject inference_completely_asserted_asent_gafs(SubLObject asent,
                                                                        SubLObject mt)

Returns:

list of gaf-assertion?; if all bindings for free variables in ASENT are completely asserted in MT, or if ASENT is closed and its truth can be completely decided via assertion lookup, return a list of gaf assertion justifying this claim. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_completely_enumerable_asentP

public static final SubLObject inference_completely_enumerable_asentP(SubLObject asent,
                                                                      SubLObject mt)

Returns:

boolean; whether all bindings for free variables in ASENT can be completely enumerated in MT. If ASENT is closed, return whether the truth of ASENT can be completely decided with no transformation.

inference_completely_enumerable_asent_gaf

public static final SubLObject inference_completely_enumerable_asent_gaf(SubLObject asent,
                                                                         SubLObject mt)

Returns:

nil or gaf-assertion?; if all bindings for free variables in ASENT can be completely enumerated in MT, or if ASENT is closed and its truth can be completely decided with no transformation, return a gaf assertion justifying this claim.

inference_completely_enumerable_asent_gafs

public static final SubLObject inference_completely_enumerable_asent_gafs(SubLObject asent,
                                                                          SubLObject mt)

Returns:

list of gaf-assertion?; if all bindings for free variables in ASENT can be completely enumerated in MT, or if ASENT is closed and its truth can be completely decided with no transformation, return a list of gaf assertions justifying this claim. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

inference_completely_decidable_asentP

public static final SubLObject inference_completely_decidable_asentP(SubLObject asent,
                                                                     SubLObject mt)

Returns:

boolean; whether the truth of ASENT can be completely decided with no transformation.

inference_completely_decidable_asent_gaf

public static final SubLObject inference_completely_decidable_asent_gaf(SubLObject asent,
                                                                        SubLObject mt)

Returns:

nil or gaf-assertion?; if the truth of ASENT can be completely decided with no transformation, return a gaf assertion justifying this claim.

inference_completely_decidable_asent_gafs

public static final SubLObject inference_completely_decidable_asent_gafs(SubLObject asent,
                                                                         SubLObject mt)

Returns:

nil or gaf-assertion?; if the truth of ASENT can be completely decided with no transformation, return a list of gaf assertions justifying this claim. The list of assertions is returned in a partial order of strength, with the inferentially strongest assertion first.

completeness_constraint_mt

public static final SubLObject completeness_constraint_mt(SubLObject mt)

Assuming that we are doing inference in MT, return the mt in which we look for completeness assertions. If all mts are relevant, we need to be conservative and only look for universally true completeness assertions.

declare_inference_completeness_utilities_file

public static final SubLObject declare_inference_completeness_utilities_file()

init_inference_completeness_utilities_file

public static final SubLObject init_inference_completeness_utilities_file()

setup_inference_completeness_utilities_file

public static final SubLObject setup_inference_completeness_utilities_file()

declareFunctions

public void declareFunctions()

Description copied from interface: SubLFile

Declares the mapping between functions and symbols for all named functions defined in the file. Like CRTL define.

initializeVariables

public void initializeVariables()

Description copied from interface: SubLFile

Initializes all global variables and private internal variables for constants defined in the file. Like CRTL init.

runTopLevelForms

public void runTopLevelForms()

Description copied from interface: SubLFile

Runs all top-level forms in order. Like CRTL setup.