public static TermApiExt termApiExt() {
  return termApi;
} public interface LibraryManager {

  /**
   * Load a {@link org.logic2j.core.api.library.PLibrary}
   *
   * @param theLibrary
   * @return The content of the library
   */
  LibraryContent loadLibrary(PLibrary theLibrary);

  /**
   * @return The whole {@link PLibrary}'s content.
   */
  LibraryContent wholeContent();

} public interface OperatorManager {

  void addOperator(String operatorText, String associativity, int precedence);

  // TODO Unclear how this is an operation of a "manager". Rename method?
  int precedence(String operatorText, String associativity);

} public interface TermAdapter {

  enum FactoryMode {
    /**
     * Result will always be an atom (a {@link Struct} of 0-arity), will never be a {@link Var}iable.
     * In the case of null, will create an empty-string atom.
     */
    ATOM,

    /**
     * Result will be either an atom (a {@link Struct} of 0-arity), an object, but not a {@link Var}iable neither a
     * compound {@link Struct}.
     */
    LITERAL,

    /**
     * Result will be any {@link Term} (atom, number, {@link Var}iable), but not a compound {@link Struct}.
     */
    ANY_TERM,

    /**
     * Result can be any term plus compound structures.
     */
    COMPOUND
  }


  /**
   * Describe the form that data structures should take when represented as Prolog compounds (Struct<?>).
   * See TabularData and related classes.
   */
  enum AssertionMode {
    /**
     * Data is asserted as "named triples". For a dataset called myData, assertions will be such as:
     * myData(entityIdentifier, propertyName, propertyValue).
     */
    EAV_NAMED,
    /**
     * Data is asserted as "quads". The predicate is always "eavt(entity, attribute, value, transaction)".
     * The "transaction" identifier is the dataset name. For example:
     * eavt(entityIdentifier, propertyName, propertyValue, myData).
     */
    EAVT,
    /**
     * Data is asserted as full records with one argument per column, such as
     * "myData(valueOfColumn1, valueOfColumn2, valueOfColumn3, ..., valueOfColumnN)."
     * The order of columns obviously matters.
     * If your data is already triples, use this mode.
     * This is the least flexible form since changes to the tabularData (adding or removing or reordering columns) will change the assertions.
     */
    RECORD
  }

  /**
   * Convert: From regular Java Object to Prolog internal Term.
   * Convert from virtually any possible instance of singular {@link Object} into to a Prolog term
   * (usually a Struct but any object is valid in logic2j).
   * This is the highest-level factory for terms.
   *
   * @param theObject
   * @param theMode
   * @return A factorized and normalized {@link Term}.
   */
  Object toTerm(Object theObject, FactoryMode theMode);

  /**
   * Instantiate a Struct with arguments from virtually any class of {@link Object}
   * This is the highest-level factory for Struct.
   *
   * @param thePredicateName The predicate (functor)
   * @param theMode
   * @param theArguments
   * @return A factorized and normalized {@link Term}.
   */
  Struct<?> toStruct(String thePredicateName, FactoryMode theMode, Object... theArguments);

  /**
   * Instantiate a list of Terms from one (possibly large) {@link Object}.
   *
   * @param theObject
   * @return A List of terms.
   */
  List<Object> toTerms(Object theObject, AssertionMode theAssertionMode);

  /**
   * Convert: From Prolog internal Term to regular Java Object.
   *
   * @param theTargetClass Either very specific or quite general like Enum, or even Object
   * @return The converted instance
   */
  <T> T fromTerm(Object theTerm, Class<T> theTargetClass);


  Object getVariable(String theExpression);

  TermAdapter setVariable(String theExpression, Object theValue);
} public interface TermMapper {

  /**
   * Transform a Term into another.
   *
   * @param theTerm
   * @return The transformed version of theTerm
   */
  Object apply(Object theTerm);

} public interface TermMarshaller {

  /**
   * Formats a {@link Term} to its character representation.
   *
   * @param theTerm
   * @return The character representation of theTerm.
   */
  CharSequence marshall(Object theTerm);

} public interface TermUnmarshaller {

  /**
   * Parse a character stream into a {@link Term}.
   *
   * @param theChars
   * @return The new {@link Term} obtained from its textual representation.
   */
  Object unmarshall(CharSequence theChars);

} public interface PLibrary {

  String NO_DIRECT_INVOCATION_USE_REFLECTION = "no-direct-invocation-use-reflection";

  /**
   * The dispatcher allow direct invocation of the primitives, without the need for reflection,
   * for performance reasons.
   *
   * @param theMethodName
   * @param theGoalStruct
   * @param currentVars
   * @return
   */
  Object dispatch(String theMethodName, Struct<?> theGoalStruct, UnifyContext currentVars);

} public class DefaultTheoryManager implements TheoryManager {
  private static final org.slf4j.Logger logger = org.slf4j.LoggerFactory.getLogger(DefaultTheoryManager.class);

  public static final String INITIALIZATION_PREDICATE = "initialization";

  private final PrologImplementation prolog;

  private final TheoryContent wholeContent = new TheoryContent();

  private List<ClauseProvider> clauseProviders = new ArrayList<>();

  private List<DataFactProvider> dataFactProviders = new ArrayList<>();

  public DefaultTheoryManager(PrologImplementation theProlog) {
    this.prolog = theProlog;
    this.clauseProviders.add(this);
  }

  public TheoryContent load(CharSequence theTheoryText) {
    final Parser parser = new Parser(this.prolog.getOperatorManager(), this.prolog.getTermAdapter(), theTheoryText.toString());
    return loadAllClauses(parser);
  }

  public TheoryContent load(Reader theReader) {
    final Parser parser = new Parser(this.prolog.getOperatorManager(), this.prolog.getTermAdapter(), theReader);
    return loadAllClauses(parser);
  }

  @Override
  public TheoryContent load(File theFile) throws IOException {
    try (final FileReader reader = new FileReader(theFile)) {
      return load(reader);
    } catch (final InvalidTermException e) {
      throw new PrologNonSpecificException("Theory could not be loaded from file \"" + theFile + "\" into " + this.prolog + ": " + e, e);
    }
  }

  @Override
  public TheoryContent load(URL theTheory) {
    Object text;
    try {
      text = theTheory.getContent();
    } catch (final IOException e) {
      throw new InvalidTermException("Could not load theory from resource " + theTheory + ": " + e);
    }
    if (text instanceof InputStream) {
      // FIXME there will be encoding issues when using InputStream instead of Reader
      final Reader reader = new InputStreamReader((InputStream) text);
      return load(reader);
    }
    throw new InvalidTermException("Could not load theory from resource " + theTheory + ": could not getContent()");
  }

  /**
   * @param theClassloadableResource must start with "/" otherwise considered a URL
   */
  @Override
  public TheoryContent load(String theClassloadableResource) {
    if (theClassloadableResource == null) {
      throw new PrologNonSpecificException("Resource for rules content cannot be null");
    }
    final URL url;
    try {
      if (theClassloadableResource.startsWith("/")) {
        url = this.getClass().getResource(theClassloadableResource);
      } else {
        url = new URL(theClassloadableResource);
      }
      if (url == null) {
        throw new PrologNonSpecificException("No content at resource path: " + theClassloadableResource);
      }
      try (InputStream in = TypeUtils.safeCastNotNull("obtaining rules content from URL", url.getContent(), InputStream.class)) {
        // FIXME there will be encoding issues when using InputStream instead of Reader
        final Reader reader = new InputStreamReader(in);
        return load(reader);
      }
    } catch (final IOException e) {
      throw new InvalidTermException("Could not load theory from resource " + theClassloadableResource + ": " + e);
    }
  }

  @Override
  public List<ClauseProvider> getClauseProviders() {
    return Collections.unmodifiableList(this.clauseProviders);  // Make sure caller cannot modify it - we've had ConcurrentModificationException
  }

  public void setClauseProviders(List<ClauseProvider> theClauseProviders) {
    this.clauseProviders = theClauseProviders;
  }

  @Override
  public boolean hasDataFactProviders() {
    return !this.dataFactProviders.isEmpty();
  }

  @Override
  public Iterable<DataFactProvider> getDataFactProviders() {
    return this.dataFactProviders;
  }

  @Override
  public void addClauseProvider(ClauseProvider theNewProvider) {
    this.clauseProviders.add(theNewProvider);
  }

  @Override
  public void addDataFactProvider(DataFactProvider theNewProvider) {
    this.dataFactProviders.add(theNewProvider);
  }

  // ---------------------------------------------------------------------------
  // Accessors
  // ---------------------------------------------------------------------------

  /**
   * @param theContent to add
   */
  @Override
  public void addTheory(TheoryContent theContent) {
    this.wholeContent.addAll(theContent);
    final Object initializationGoal = this.wholeContent.getInitializationGoal();
    if (initializationGoal != null) {
      executeDirective(initializationGoal);
      this.wholeContent.setInitializationGoal(null); // Next file loaded should not re-use same!
    }
  }

  public void setDataFactProviders(List<DataFactProvider> theDataFactProviders) {
    this.dataFactProviders = theDataFactProviders;
  }

  private TheoryContent loadAllClauses(Parser theParser) {
    final TheoryContent content = new TheoryContent();
    // Need to split parsing into terms and loading Clauses into Content separately, because of import/1
    for (Object clauseTerm = theParser.nextTerm(true); clauseTerm != null; clauseTerm = theParser.nextTerm(true)) {
      logger.debug("Loading clause: {}", clauseTerm);
      if (clauseTerm instanceof CharSequence) {
        // Very rare case of facts being just a string (see "cut4" in our tests)
        clauseTerm = Struct.valueOf(clauseTerm.toString());
      }
      if (!(clauseTerm instanceof Struct)) {
        throw new InvalidTermException("Non-Struct term \"" + clauseTerm + "\" cannot be used for a Clause");
      }
      final Struct<?> clauseStruct = (Struct<?>) clauseTerm;
      if (isDirective(clauseStruct)) {
        // Identify directive
        final Object directiveGoal = clauseStruct.getArg(0);
        if (directiveGoal instanceof Struct<?> && ((Struct<?>) directiveGoal).getName() == INITIALIZATION_PREDICATE
                && ((Struct<?>) directiveGoal).getArity() == 1) {
          final Object goal = ((Struct<?>) directiveGoal).getArg(0);
          content.setInitializationGoal(goal);
        } else {
          executeDirective(directiveGoal);
        }
      } else {
        final Clause cl = new Clause(this.prolog, clauseTerm);
        content.add(cl);
      }

    }
    // End of loading
    return content;
  }

  private void executeDirective(Object directiveGoal) {
    directiveGoal = termApiExt().normalize(directiveGoal, this.prolog.getLibraryManager().wholeContent());
    // Execute right now
    final CountingSolutionListener countingListener = new CountingSolutionListener();
    this.prolog.getSolver().solveGoal(directiveGoal, countingListener);
    logger.debug("Execution of directive or initialization predicate \"{}\" gave {} solutions", directiveGoal, countingListener.count());
  }

  private boolean isDirective(Struct<?> clauseStruct) {
    return clauseStruct.getName() == Struct.FUNCTOR_CLAUSE && clauseStruct.getArity() == 1;
  }

  // ---------------------------------------------------------------------------
  // Implementation of ClauseProvider
  // ---------------------------------------------------------------------------

  /**
   * @param theGoal
   * @param currentVars Not used in this method
   * @return All {@link Clause}s from the {@link TheoryContent} that may match theGoal.
   */
  @Override
  public Iterable<Clause> listMatchingClauses(Object theGoal, UnifyContext currentVars) {
    return this.wholeContent.find(theGoal);
  }

  // ---------------------------------------------------------------------------
  // Methods of java.lang.Object
  // ---------------------------------------------------------------------------

  @Override
  public String toString() {
    return this.getClass().getSimpleName();
  }

} public interface TheoryManager extends ClauseProvider {

  // ---------------------------------------------------------------------------
  // Load Theories from various sources into a TheoryContent representation
  // ---------------------------------------------------------------------------

  /**
   * Load the {@link TheoryContent} from a File defining a theory;
   * this only loads and return the content, use {@link #addTheory(TheoryContent)} to make it
   * available to the {@link org.logic2j.core.impl.PrologImplementation}.
   *
   * @param theFile
   * @return The content of the theory
   * @throws java.io.IOException
   */
  TheoryContent load(File theFile) throws IOException;

  /**
   * Load from a URL.
   *
   * @param theTheory
   * @return The content of the theory
   */
  TheoryContent load(URL theTheory);

  /**
   * Load from a classloadable resource.
   *
   * @param theClassloadableResourceOrUrl
   * @return The content of the theory
   */
  TheoryContent load(String theClassloadableResourceOrUrl);

  /**
   * @return All clause providers, in same order as when registered.
   * TODO The actual ordering of ClauseProviders may not always be required: it is only
   * important when the same predicate is available from several providers (rare). Could we in certain cases use
   * multi-threaded access to all clause providers?
   */
  Iterable<ClauseProvider> getClauseProviders();

  boolean hasDataFactProviders();

  Iterable<DataFactProvider> getDataFactProviders();

  /**
   * @param theNewProvider
   */
  void addClauseProvider(ClauseProvider theNewProvider);

  /**
   * @param theNewProvider
   */
  void addDataFactProvider(DataFactProvider theNewProvider);

  // ---------------------------------------------------------------------------
  // Alter the current Prolog instance with content from theories
  // ---------------------------------------------------------------------------

  /**
   * @param theContent To be merged into this and made available to the {@link org.logic2j.core.impl.PrologImplementation}.
   */
  void addTheory(TheoryContent theContent);

} public class DefaultLibraryManager implements LibraryManager {
  private static final org.slf4j.Logger logger = org.slf4j.LoggerFactory.getLogger(DefaultLibraryManager.class);

  /**
   * Difference between number of args in Prolog's primitive invocation, and number of varargs
   * passed to Java implementation of the primitive: (UnifyContext currentVars, Object...)
   */
  private static final int NB_EXTRA_PARAMS = 1;

  private static final Struct<?> ATOM_CUT = new Struct<>(Struct.FUNCTOR_CUT);

  private final Prolog prolog;

  private final LibraryContent wholeContent = new LibraryContent();

  private final Map<Class<? extends PLibrary>, PLibrary> libraries = new HashMap<>();

  /**
   * @param theProlog
   */
  public DefaultLibraryManager(Prolog theProlog) {
    this.prolog = theProlog;
  }

  /**
   * @return The extra content loaded.
   * @note Won't load any instance of a {@link PLibrary} of the same class more than once - if asked more than once, we won't fail, just
   * log, and return no loaded content.
   */
  @Override
  public LibraryContent loadLibrary(PLibrary theLibrary) {
    if (alreadyLoaded(theLibrary)) {
      logger.warn("Library \"{}\" already has an instance of the same class loaded - nothing done", theLibrary);
      final LibraryContent extraContentIsEmpty = new LibraryContent();
      return extraContentIsEmpty;
    }
    final LibraryContent extraContent = loadLibraryInternal(theLibrary);
    mergeExtraContent(extraContent);

    // Load the theory text associated to the library, if any exists
    final URL associatedTheory = locationOfAssociatedTheory(theLibrary);
    if (associatedTheory != null) {
      final TheoryManager theoryManager = this.prolog.getTheoryManager();
      final TheoryContent theory = theoryManager.load(associatedTheory);
      theoryManager.addTheory(theory);
      logger.debug("Library \"{}\" loaded with extra content from {}", theLibrary, associatedTheory);
    } else {
      logger.debug("Library \"{}\" loaded; no associated theory found", theLibrary);
    }
    return extraContent;
  }

  private URL locationOfAssociatedTheory(PLibrary theLibrary) {
    final Class<? extends PLibrary> libraryClass = theLibrary.getClass();
    final String name = libraryClass.getSimpleName() + ".pro";
    final URL contentUrl = libraryClass.getResource(name);
    return contentUrl;
  }

  /**
   * @param theLibrary
   * @return True when one library of the same class was already loaded in this engine.
   */
  private boolean alreadyLoaded(PLibrary theLibrary) {
    return this.libraries.containsKey(theLibrary.getClass());
  }

  private void mergeExtraContent(LibraryContent loadedContent) {
    this.wholeContent.addAll(loadedContent);
    // TODO Houston we have a problem - we need to reassign all primitives upon loading libs!
    // It's actually unclear if when we load a new library, the new available functors would influence theories currently loaded.

    // We need to assignPrimitiveInfo(), but let's use the TermApi directly and invoke normalize() it won't harm to do a little more.
    termApiExt().normalize(Struct.ATOM_TRUE, this.wholeContent);
    termApiExt().normalize(Struct.ATOM_FALSE, this.wholeContent);
    termApiExt().normalize(ATOM_CUT, this.wholeContent);
  }

  /**
   * Introspect annotations within the {@link PLibrary} and return a description of it.
   * Look for {@link org.logic2j.core.api.library.annotation.Predicate} annotations; notice that a primitive may have several names (to allow for non-Java identifiers such as
   * \=)
   *
   * @param theLibrary
   * @return The content of the library loaded
   */
  private LibraryContent loadLibraryInternal(PLibrary theLibrary) {
    final LibraryContent content = new LibraryContent();
    logger.debug("Loading library {}", theLibrary);
    final Class<? extends PLibrary> libraryClass = theLibrary.getClass();

    // Load all annotated methods
    for (final Method method : libraryClass.getMethods()) {
      final Predicate predicateAnnotation = method.getAnnotation(Predicate.class);
      final Functor functorAnnotation = method.getAnnotation(Functor.class);

      // Handle the methods of interest
      if (predicateAnnotation != null || functorAnnotation != null) {
        final Class<?>[] paramTypes = method.getParameterTypes();
        final Class<?> returnType = method.getReturnType();
        final PrimitiveType type;
        String primitiveName;
        final String[] synonyms;
        if (predicateAnnotation != null) {
          if (returnType != Integer.TYPE) {
            throw new PrologNonSpecificException("Unexpected return type, require \"int\" for predicate " + method);
          }
          type = PrimitiveType.PREDICATE;
          primitiveName = predicateAnnotation.name();
          synonyms = predicateAnnotation.synonyms();
        } else if (functorAnnotation != null) {
          type = PrimitiveType.FUNCTOR;
          primitiveName = functorAnnotation.name();
          synonyms = functorAnnotation.synonyms();
        } else {
          throw new PrologNonSpecificException("Should not be here, annotation handling error");
        }

        // Check method arguments
        final int nbMethodParams = paramTypes.length;
        int i = 0;
        if (!(UnifyContext.class.isAssignableFrom(paramTypes[i]))) {
          throw new PrologNonSpecificException("Argument type at index " + i + " of method " + method + " not of proper " + UnifyContext.class);
        }
        i++;
        boolean varargs = false;
        if (i < nbMethodParams) {
          if (Object[].class.isAssignableFrom(paramTypes[i])) {
            varargs = true;
          } else {
            while (i < nbMethodParams) {
              if (!(Object.class.isAssignableFrom(paramTypes[i]))) {
                throw new PrologNonSpecificException("Argument type at index " + i + " of method " + method + " not of proper " + Term.class);
              }
              i++;
            }
          }
        }

        // Main name (default = method's name) for the primitive

        if (primitiveName == null || primitiveName.isEmpty()) {
          primitiveName = method.getName();
        }
        final String aritySignature = varargs ? Struct.VARARG_ARITY_SIGNATURE : Integer.toString(nbMethodParams - NB_EXTRA_PARAMS);
        final String key1 = primitiveName + '/' + aritySignature;
        final PrimitiveInfo desc = new PrimitiveInfo(type, theLibrary, primitiveName, method, varargs);
        content.putPrimitive(key1, desc);

        // All other accepted synonyms for this primitive
        for (final String synonym : synonyms) {
          final String key2 = synonym + '/' + aritySignature;
          final PrimitiveInfo desc2 = new PrimitiveInfo(type, theLibrary, primitiveName, method, varargs);
          content.putPrimitive(key2, desc2);
        }
      }
    }
    this.libraries.put(libraryClass, theLibrary);
    return content;
  }

  /**
   * @return The merged content of all the {@link PLibrary}es loaded by {@link #loadLibrary(PLibrary)} so far.
   */
  @Override
  public LibraryContent wholeContent() {
    return this.wholeContent;
  }

} @SuppressWarnings("StringEquality")
public class CoreLibrary extends LibraryBase {

  public CoreLibrary(PrologImplementation theProlog) {
    super(theProlog);
  }

  private static final ComparisonFunction COMPARISON_EQ = new ComparisonFunction() {

    @Override
    public boolean apply(Number val1, Number val2) {
      return val1.doubleValue() == val2.doubleValue();
    }

    @Override
    public boolean apply(CharSequence val1, CharSequence val2) {
      return val1.toString().compareTo(val2.toString()) == 0;
    }
  };

  private static final ComparisonFunction COMPARISON_NE = new ComparisonFunction() {

    @Override
    public boolean apply(Number val1, Number val2) {
      return val1.doubleValue() != val2.doubleValue();
    }

    @Override
    public boolean apply(CharSequence val1, CharSequence val2) {
      return val1.toString().compareTo(val2.toString()) != 0;
    }
  };

  private static final AggregationFunction AGGREGATION_PLUS = (val1, val2) -> {
    if (val1 instanceof Integer && val2 instanceof Integer) {
      return val1.intValue() + val2.intValue();
    }
    return (double) (val1.intValue() + val2.intValue());
  };

  private static final AggregationFunction AGGREGATION_MINUS = (val1, val2) -> {
    if (val1 instanceof Integer && val2 instanceof Integer) {
      return val1.intValue() - val2.intValue();
    }
    return (double) (val1.intValue() - val2.intValue());
  };

  private static final AggregationFunction AGGREGRATION_TIMES = (val1, val2) -> {
    if (val1 instanceof Integer && val2 instanceof Integer) {
      return val1.intValue() * val2.intValue();
    }
    return (double) (val1.intValue() * val2.intValue());
  };

  private static final AggregationFunction AGGREGATION_NEGATE = (val1, val2) -> {
    if (val1 instanceof Integer && val2 instanceof Integer) {
      return -val1.intValue();
    }
    return (double) -val1.intValue();
  };


  @Override
  public Object dispatch(String theMethodName, Struct<?> theGoalStruct, UnifyContext currentVars) {
    final Object result;
    // Argument methodName is {@link String#intern()}alized so OK to check by reference
    final Object[] goalStructArgs = theGoalStruct.getArgs();
    final int arity = goalStructArgs.length;
    if (arity == 0) {
      if (theMethodName == "fail") {
        result = fail(currentVars);
      } else if (theMethodName == "trueFunctor") {
        result = trueFunctor(currentVars);
      } else {
        result = NO_DIRECT_INVOCATION_USE_REFLECTION;
      }
    } else if (arity == 1) {
      final Object arg0 = goalStructArgs[0];
      if (theMethodName == "not") {
        result = not(currentVars, arg0);
      } else if (theMethodName == "atom") {
        result = atom(currentVars, arg0);
      } else if (theMethodName == "atomic") {
        result = atomic(currentVars, arg0);
      } else if (theMethodName == "var") {
        result = var(currentVars, arg0);
      } else if (theMethodName == "exists") {
        result = exists(currentVars, arg0);
      } else {
        result = NO_DIRECT_INVOCATION_USE_REFLECTION;
      }
    } else if (arity == 2) {
      final Object arg0 = goalStructArgs[0];
      final Object arg1 = goalStructArgs[1];
      if (theMethodName == "unify") {
        result = unify(currentVars, arg0, arg1);
      } /*
      else if (theMethodName == "expression_greater_equal_than") {
        result = expression_greater_equal_than(currentVars, arg0, arg1);
      }
      else if (theMethodName == "expression_greater_than") {
        result = expression_greater_than(currentVars, arg0, arg1);
      } else if (theMethodName == "expression_lower_than") {
        result = expression_lower_than(currentVars, arg0, arg1);
      } else if (theMethodName == "expression_lower_equal_than") {
        result = expression_lower_equal_than(currentVars, arg0, arg1);
      }
      */
      else if (theMethodName == "expression_equals") {
        result = expression_equals(currentVars, arg0, arg1);
      } else if (theMethodName == "is") {
        result = is(currentVars, arg0, arg1);
      } else if (theMethodName == "plus") {
        result = plus(currentVars, arg0, arg1);
      } else if (theMethodName == "minus") {
        result = minus(currentVars, arg0, arg1);
      } else if (theMethodName == "multiply") {
        result = multiply(currentVars, arg0, arg1);
      } else if (theMethodName == "notUnify") {
        result = notUnify(currentVars, arg0, arg1);
      } else if (theMethodName == "clause") {
        result = clause(currentVars, arg0, arg1);
      } else if (theMethodName == "predicate2PList") {
        result = predicate2PList(currentVars, arg0, arg1);
      } else if (theMethodName == "atom_length") {
        result = atom_length(currentVars, arg0, arg1);
      } else if (theMethodName == "length") {
        result = length(currentVars, arg0, arg1);
      } else if (theMethodName == "count") {
        result = count(currentVars, arg0, arg1);
      } else if (theMethodName == "distinct") {
        result = distinct(currentVars, arg0, arg1);
      } else {
        result = NO_DIRECT_INVOCATION_USE_REFLECTION;
      }
    } else if (arity == 3) {
      final Object arg0 = goalStructArgs[0];
      final Object arg1 = goalStructArgs[1];
      final Object arg2 = goalStructArgs[2];
      if (theMethodName == "findall") {
        result = findall(currentVars, arg0, arg1, arg2);
      } else if (theMethodName == "distinct") {
        result = distinct(currentVars, arg0, arg1, arg2);
      } else {
        result = NO_DIRECT_INVOCATION_USE_REFLECTION;
      }
    } else {
      result = NO_DIRECT_INVOCATION_USE_REFLECTION;
    }
    return result;
  }

  @Predicate(name = Struct.FUNCTOR_TRUE)
  // We can't name the method "true" it's a Java reserved word...
  public int trueFunctor(UnifyContext currentVars) {
    return notifySolution(currentVars);
  }

  @Predicate
  public int fail(@SuppressWarnings("unused") UnifyContext currentVars) {
    // Do not propagate a solution - that's all
    return Continuation.CONTINUE;
  }

  @Predicate
  public int var(UnifyContext currentVars, Object t1) {
    int continuation = Continuation.CONTINUE;
    if (t1 instanceof Var<?>) {
      final Var<?> var = (Var<?>) t1;
      if (var == Var.anon()) {
        notifySolution(currentVars);
      } else {
        final Object value = currentVars.reify(t1);
        if (value instanceof Var<?>) {
          continuation = notifySolution(currentVars);
        }
      }
    }
    return continuation;
  }

  @Predicate
  public int atom(UnifyContext currentVars, Object theTerm) {
    final Object value = currentVars.reify(theTerm);
    if (termApi().isAtom(value)) {
      return notifySolution(currentVars);
    }
    return Continuation.CONTINUE;
  }

  @Predicate
  public int atomic(UnifyContext currentVars, Object theTerm) {
    final Object value = currentVars.reify(theTerm);
    if (termApi().isAtomic(value)) {
      return notifySolution(currentVars);
    }
    return Continuation.CONTINUE;
  }

  @Predicate
  public int number(UnifyContext currentVars, Object theTerm) {
    final Object value = currentVars.reify(theTerm);
    ensureBindingIsNotAFreeVar(value, "number/1", 0);
    if (value instanceof Number) {
      return notifySolution(currentVars);
    }
    return Continuation.CONTINUE;
  }

  @Predicate(name = "=")
  public int unify(UnifyContext currentVars, Object t1, Object t2) {
    return unifyAndNotify(currentVars, t1, t2);
  }

  /**
   * Not unifyable
   * @param currentVars
   * @param t1
   * @param t2
   * @return success if t1 and t2 cannot be unified
   */
  @Predicate(name = "\\=")
  public int notUnify(UnifyContext currentVars, Object t1, Object t2) {
    final UnifyContext after = currentVars.unify(t1, t2);
    if (after == null) {
      // Not unified
      return notifySolution(currentVars);
    }
    // Unified
    return Continuation.CONTINUE;
  }

  // Surprisingly enough the operator \+ means "not provable".
  @Predicate(synonyms = "\\+")
  public int not(UnifyContext currentVars, Object theGoal) {

    final NotListener callListener = new NotListener();

    Solver solver = getProlog().getSolver();
    solver.solveGoal(theGoal, currentVars.withListener(callListener));
    final int continuation;
    if (callListener.exists()) {
      continuation = Continuation.CONTINUE;
    } else {
      // Not found - notify a solution (that's the purpose of not/1 !)
      continuation = notifySolution(currentVars);
    }
    return continuation;
  }

  @Predicate
  public int atom_length(UnifyContext currentVars, Object theAtom, Object theLength) {
    final Object value = currentVars.reify(theAtom);
    ensureBindingIsNotAFreeVar(value, "atom_length/2", 0);
    final String atomText = value.toString();
    final Long atomLength = (long) atomText.length();
    return unify(currentVars, atomLength, theLength);
  }

  /**
   * Check existence of subGoal. Without binding its variables, and stopping any solving after the first solution
   * of subGoal is proven. This is a most efficient implementation but may have dubious effects - maybe to study
   * a little in details...
   *
   * @param currentVars
   * @param theGoal
   * @return
   */
  @Predicate
  public int exists(UnifyContext currentVars, final Object theGoal) {
    final CountingSolutionListener listenerForSubGoal = new CountingSolutionListener() {
      @Override
      public int onSolution(UnifyContext currentVars) {
        super.onSolution(currentVars);
        // Upon the first solution found, notify the engine to stop generating
        return Continuation.USER_ABORT;
      }
    };
    // Now solve the target sub goal
    final Object effectiveGoal = currentVars.reify(theGoal);
    getProlog().getSolver().solveGoal(effectiveGoal, currentVars.withListener(listenerForSubGoal));

    // And unify with result
    final int counted = listenerForSubGoal.count();
    // Note: won't ever be greater than one due to our listener that stops generation
    if (counted > 0) {
      return notifySolution(currentVars);
    }
    return Continuation.CONTINUE;
  }

  private void collectReifiedResults(UnifyContext currentVars, final Object theTemplate, Object theGoal, final Collection<Object> javaResults) {
    final SolutionListener listenerForSubGoal = vars -> {
      final Object templateReified = vars.reify(theTemplate);
      javaResults.add(templateReified);
      return Continuation.CONTINUE;
    };
    // Now solve the target sub goal
    final Object effectiveGoal = currentVars.reify(theGoal);
    getProlog().getSolver().solveGoal(effectiveGoal, currentVars.withListener(listenerForSubGoal));
  }


  @Predicate
  public int count(UnifyContext currentVars, final Object theGoal, final Object theNumber) {
    final CountingSolutionListener listenerForSubGoal = new CountingSolutionListener();
    // Now solve the target sub goal
    final Object effectiveGoal = currentVars.reify(theGoal);
    getProlog().getSolver().solveGoal(effectiveGoal, currentVars.withListener(listenerForSubGoal));

    // And unify with result of counting (as Integer)
    final Integer counted = listenerForSubGoal.count();
    return unify(currentVars, theNumber, counted);
  }

  @Predicate
  public int findall(UnifyContext currentVars, final Object theTemplate, final Object theGoal,
                     final Object theResult) {
    final ArrayList<Object> allReifiedResults = new ArrayList<>(100); // Our internal collection of results
    collectReifiedResults(currentVars, theTemplate, theGoal, allReifiedResults);

    // Convert all results into a prolog list structure
    // Note on var indexes: all variables present in the projection term will be
    // copied into the resulting plist, so there's no need to reindex.
    // However, the root level Struct that makes up the list does contain a bogus
    // index value but -1.
    final Struct<?> plist = PrologLists.createPList(allReifiedResults);

    // And unify with result
    return unify(currentVars, theResult, plist);
  }

  /**
   * distinct/2
   * @param currentVars
   * @param theTemplate
   * @param theGoal
   * @param theResult
   * @return
   */
  @Predicate
  public int distinct(UnifyContext currentVars, final Object theTemplate, final Object theGoal,
                      final Object theResult) {
    final LinkedHashSet<Object> distinctReifiedResults = new LinkedHashSet<>(100); // Our internal collection of results
    collectReifiedResults(currentVars, theTemplate, theGoal, distinctReifiedResults);

    // Convert all results into a prolog list structure
    // Note on var indexes: all variables present in the projection term will be
    // copied into the resulting plist, so there's no need to reindex.
    // However, the root level Struct that makes up the list does contain a bogus
    // index value but -1.
    final Struct<?> plist = PrologLists.createPList(distinctReifiedResults);

    // And unify with result
    return unify(currentVars, theResult, plist);
  }

  /**
   * distinct/2
   * @param currentVars
   * @param theTemplate
   * @param theGoal
   * @return
   */
  @Predicate
  public int distinct(UnifyContext currentVars, final Object theTemplate, final Object theGoal) {
    final LinkedHashSet<Object> distinctReifiedResults = new LinkedHashSet<>(100); // Our internal collection of results
    collectReifiedResults(currentVars, theTemplate, theGoal, distinctReifiedResults);

    for (Object element: distinctReifiedResults) {
      final int result = unifyAndNotify(currentVars, theTemplate, element);
      if (result != Continuation.CONTINUE) {
        return result;
      }
    }
    return Continuation.CONTINUE;
  }

  /**
   * @param currentVars
   * @param theList
   * @param theLength
   * @return Length of a prolog list
   */
  @Predicate
  public int length(UnifyContext currentVars, Object theList, Object theLength) {
    final Object value = currentVars.reify(theList);
    ensureBindingIsNotAFreeVar(value, "length/2", 0);
    if (!PrologLists.isList(value)) {
      throw new InvalidTermException("A Prolog list is required for length/2,  was " + value);
    }
    final ArrayList<Object> javalist = PrologLists.javaListFromPList(((Struct<?>) value), new ArrayList<>(), Object.class);
    final Integer listLength = javalist.size();
    return unify(currentVars, listLength, theLength);
  }

  @Predicate
  public int clause(UnifyContext currentVars, Object theHead, Object theBody) {
    final Object headValue = currentVars.reify(theHead);
    final Object[] clauseHeadAndBody = new Object[2];
    for (final ClauseProvider cp : getProlog().getTheoryManager().getClauseProviders()) {
      for (final Clause clause : cp.listMatchingClauses(headValue, currentVars)) {
        // Clone the clause so that we can unify against its bindings
        clause.headAndBodyForSubgoal(currentVars, clauseHeadAndBody);
        final Object clauseHead = clauseHeadAndBody[0];
        final UnifyContext varsAfterHeadUnified = currentVars.unify(headValue, clauseHead);
        final boolean headUnified = varsAfterHeadUnified != null;
        if (headUnified) {
          // Determine body
          final boolean isRule = clauseHeadAndBody[1] != null;
          final Object clauseBody = isRule ? clauseHeadAndBody[1] : Struct.ATOM_TRUE;
          // Unify Body
          final UnifyContext varsAfterBodyUnified = varsAfterHeadUnified.unify(clauseBody, theBody);
          if (varsAfterBodyUnified != null) {
            final int continuation = notifySolution(varsAfterBodyUnified);
            if (continuation != Continuation.CONTINUE) {
              return continuation;
            }
          }
        }
      }
    }
    return Continuation.CONTINUE;
  }

  @Predicate(name = "=..")
  public int predicate2PList(UnifyContext currentVars, Object thePredicate, Object theList) {
    final Object predicateValue = currentVars.reify(thePredicate);
    if (predicateValue instanceof Var<?>) {
      // thePredicate is still free, going ot match from theList
      final Object listValue = currentVars.reify(theList);
      ensureBindingIsNotAFreeVar(listValue, "=../2", 1);
      final Struct<?> lst2 = (Struct<?>) listValue;
      final Struct<?> flattened = PrologLists.predicateFromPList(lst2);

      return unify(currentVars, predicateValue, flattened);
    } else {
      // thePredicate is bound
      if (predicateValue instanceof Struct) {
        final Struct<?> struct = (Struct<?>) predicateValue;
        final int arity = struct.getArity();
        final ArrayList<Object> elems = new ArrayList<>(1 + arity);
        elems.add(struct.getName());
        for (Object arg : struct.getArgs()) {
          elems.add(arg);
        }
        final Struct<?> plist = PrologLists.createPList(elems);
        return unify(currentVars, plist, theList);
      }
    }
    return Continuation.CONTINUE;
  }

  @Predicate
  public int is(UnifyContext currentVars, Object t1, Object t2) {
    final Object evaluated = termApiExt().evaluate(t2, currentVars);
    if (evaluated == null) {
      // No solution
      return Continuation.CONTINUE;
    }
    return unify(currentVars, t1, evaluated);
  }

  // ---------------------------------------------------------------------------
  // Binary numeric predicates
  // ---------------------------------------------------------------------------

  /**
   * Compare numbers or chars.
   */
  private interface ComparisonFunction {
    boolean apply(Number val1, Number val2);

    boolean apply(CharSequence str1, CharSequence str2);
  }

  /**
   * For all binary predicates that compare numeric values.
   *
   * @param currentVars
   * @param t1
   * @param t2
   * @param theEvaluationFunction
   * @return The {@link Continuation} as returned by the solution notified.
   */
  private int binaryComparisonPredicate(UnifyContext currentVars, Object t1, Object t2,
                                        ComparisonFunction theEvaluationFunction) {
    final Object effectiveT1 = termApiExt().evaluate(t1, currentVars);
    final Object effectiveT2 = termApiExt().evaluate(t2, currentVars);
    int continuation = Continuation.CONTINUE;
    if (effectiveT1 instanceof Number && effectiveT2 instanceof Number) {
      final boolean condition = theEvaluationFunction.apply((Number) effectiveT1, (Number) effectiveT2);
      if (condition) {
        continuation = notifySolution(currentVars);
      }
      return continuation;
    }
    if (effectiveT1 instanceof CharSequence && effectiveT2 instanceof CharSequence) {
      final boolean condition = theEvaluationFunction.apply((CharSequence) effectiveT1, (CharSequence) effectiveT2);
      if (condition) {
        continuation = notifySolution(currentVars);
      }
      return continuation;
    }
    return continuation;
  }

/*
  @Predicate(name = ">=")
  public int expression_greater_equal_than(UnifyContext currentVars, Object t1, Object t2) {
    return binaryComparisonPredicate(currentVars, t1, t2, COMPARISON_GE);
  }

  @Predicate(name = ">")
  public int expression_greater_than(UnifyContext currentVars, Object t1, Object t2) {
    return binaryComparisonPredicate(currentVars, t1, t2, COMPARE_GT);
  }

  @Predicate(name = "<")
  public int expression_lower_than(UnifyContext currentVars, Object t1, Object t2) {
    return binaryComparisonPredicate(currentVars, t1, t2, COMPARISON_LT);
  }

  @Predicate(name = "=<")
  public int expression_lower_equal_than(UnifyContext currentVars, Object t1, Object t2) {
    return binaryComparisonPredicate(currentVars, t1, t2, COMPARISON_LE);
  }
*/

  @Predicate(name = "=:=")
  public int expression_equals(UnifyContext currentVars, Object t1, Object t2) {
    return binaryComparisonPredicate(currentVars, t1, t2, COMPARISON_EQ);
  }

  @Predicate(name = "=\\=")
  public int expression_not_equals(UnifyContext currentVars, Object t1, Object t2) {
    return binaryComparisonPredicate(currentVars, t1, t2, COMPARISON_NE);
  }

  // ---------------------------------------------------------------------------
  // Functors
  // ---------------------------------------------------------------------------


  private interface AggregationFunction {
    Number apply(Number val1, Number val2);
  }

  private Object binaryFunctor(UnifyContext currentVars, Object theTerm1, Object theTerm2,
                               AggregationFunction theEvaluationFunction) {
    final Object t1 = termApiExt().evaluate(theTerm1, currentVars);
    final Object t2 = termApiExt().evaluate(theTerm2, currentVars);
    if (t1 instanceof Number && t2 instanceof Number) {
      if (t1 instanceof Integer && t2 instanceof Integer) {
        return theEvaluationFunction.apply((Number) t1, (Number) t2).intValue();
      }
      return theEvaluationFunction.apply((Number) t1, (Number) t2).doubleValue();
    }
    throw new InvalidTermException("Could not apply binaryFunctor because 2 terms are not Numbers: " + t1 + " and " + t2);
  }

  @Functor(name = "+")
  public Object plus(UnifyContext currentVars, Object t1, Object t2) {
    return binaryFunctor(currentVars, t1, t2, AGGREGATION_PLUS);
  }

  /**
   * @param currentVars
   * @param t1
   * @param t2
   * @return Binary minus (subtract)
   */
  @Functor(name = "-")
  public Object minus(UnifyContext currentVars, Object t1, Object t2) {
    return binaryFunctor(currentVars, t1, t2, AGGREGATION_MINUS);
  }

  /**
   * @param t1
   * @param t2
   * @return Binary multiply
   */
  @Functor(name = "*")
  public Object multiply(UnifyContext currentVars, Object t1, Object t2) {
    return binaryFunctor(currentVars, t1, t2, AGGREGRATION_TIMES);
  }

  /**
   * @param currentVars
   * @param t1
   * @return Unary minus (negate)
   */
  @Functor(name = "-")
  public Object minus(UnifyContext currentVars, Object t1) {
    return binaryFunctor(currentVars, t1, 0L, AGGREGATION_NEGATE);
  }
} public class IOLibrary extends LibraryBase {
  /**
   * Name of the logger to which all logging events go.
   */
  private static final String LOGIC2J_PROLOG_LOGGER = "org.logic2j.logger";
  private static final org.slf4j.Logger logger = org.slf4j.LoggerFactory.getLogger(LOGIC2J_PROLOG_LOGGER);

  private static final String QUOTE = "'";

  final PrintStream writer = System.out;

  public IOLibrary(PrologImplementation theProlog) {
    super(theProlog);
  }

  @Override
  public Object dispatch(String theMethodName, Struct<?> theGoalStruct, UnifyContext currentVars) {
    final Object result;
    final Object[] args = theGoalStruct.getArgs();
    // Argument methodName is {@link String#intern()}alized so OK to check by reference
    if (theMethodName == "write") {
      result = write(currentVars, args);
    } else if (theMethodName == "nl") {
      result = nl(currentVars);
    } else if (theMethodName == "nolog") {
      result = nolog(currentVars, args);
    } else if (theMethodName == "debug") {
      result = debug(currentVars, args);
    } else if (theMethodName == "info") {
      result = info(currentVars, args);
    } else if (theMethodName == "warn") {
      result = warn(currentVars, args);
    } else if (theMethodName == "error") {
      result = error(currentVars, args);
    } else {
      result = NO_DIRECT_INVOCATION_USE_REFLECTION;
    }
    return result;
  }

  @Predicate
  public int write(UnifyContext currentVars, Object... terms) {
    for (final Object term : terms) {
      final Object value = currentVars.reify(term);
      final String formatted = getProlog().getTermMarshaller().marshall(value).toString();
      final String unquoted = IOLibrary.unquote(formatted);
      this.writer.print(unquoted);
    }
    return notifySolution(currentVars);
  }

  @Predicate
  public int nl(UnifyContext currentVars) {
    this.writer.println();
    return notifySolution(currentVars);
  }

  @Predicate
  public int debug(UnifyContext currentVars, Object... terms) {
    if (logger.isDebugEnabled()) {
      final String substring = formatForLog(currentVars, terms);
      logger.debug(substring);
    }
    return notifySolution(currentVars);
  }

  @Predicate
  public int info(UnifyContext currentVars, Object... terms) {
    if (logger.isInfoEnabled()) {
      final String substring = formatForLog(currentVars, terms);
      logger.info(substring);
    }
    return notifySolution(currentVars);
  }

  @Predicate
  public int warn(UnifyContext currentVars, Object... terms) {
    if (logger.isWarnEnabled()) {
      final String substring = formatForLog(currentVars, terms);
      logger.warn(substring);
    }
    return notifySolution(currentVars);
  }

  @Predicate
  public int error(UnifyContext currentVars, Object... terms) {
    if (logger.isErrorEnabled()) {
      final String substring = formatForLog(currentVars, terms);
      logger.error(substring);
    }
    return notifySolution(currentVars);
  }

  private String formatForLog(UnifyContext currentVars, Object... terms) {
    final StringBuilder sb = new StringBuilder("P ");
    for (final Object term : terms) {
      Object value = currentVars.reify(term);
      final String format = getProlog().getTermMarshaller().marshall(value).toString();
      sb.append(format);
      sb.append(' ');
    }
    final String substring = sb.substring(0, sb.length() - 1);
    return substring;
  }

  /**
   * Replace any logging predicate by "nolog" to avoid any overhead with logging.
   *
   * @param currentVars
   * @param terms
   * @return This predicate succeeds with one solution, {@link Continuation#CONTINUE}
   */
  @Predicate
  public int nolog(UnifyContext currentVars, Object... terms) {
    // Do nothing, but succeeds!
    return notifySolution(currentVars);
  }

  private static String unquote(String st) {
    if (st.startsWith(QUOTE) && st.endsWith(QUOTE)) {
      return st.substring(1, st.length() - 1);
    }
    return st;
  }

}
import static org.logic2j.engine.model.TermApiLocator.termApiExt;
import org.logic2j.core.api.LibraryManager;
import org.logic2j.core.api.OperatorManager;
import org.logic2j.core.api.TermAdapter;
import org.logic2j.core.api.TermMapper;
import org.logic2j.core.api.TermMarshaller;
import org.logic2j.core.api.TermUnmarshaller;
import org.logic2j.core.api.library.PLibrary;
import org.logic2j.core.impl.theory.DefaultTheoryManager;
import org.logic2j.core.impl.theory.TheoryManager;
import org.logic2j.core.library.DefaultLibraryManager;
import org.logic2j.core.library.impl.CoreLibrary;
import org.logic2j.core.library.impl.IOLibrary;
import org.logic2j.engine.predicates.impl.generator.Digit;
import org.logic2j.engine.predicates.impl.math.compare.GE;
import org.logic2j.engine.predicates.impl.math.compare.GT;
import org.logic2j.engine.predicates.impl.math.compare.LE;
import org.logic2j.engine.predicates.impl.math.compare.LT;
import org.logic2j.engine.predicates.impl.math.function.Format;
import org.logic2j.engine.predicates.impl.math.function.LowerCase;
import org.logic2j.engine.predicates.impl.math.function.UpperCase;
import org.logic2j.engine.solver.holder.GoalHolder;
/*
 * logic2j - "Bring Logic to your Java" - Copyright (c) 2017 Laurent.Tettoni@gmail.com
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU Lesser Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Foobar is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU Lesser Public License for more details.
 *
 * You should have received a copy of the GNU Lesser Public License
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 */
package org.logic2j.core.impl;



/**
 * Reference implementation of logic2j's {@link PrologImplementation} API.
 */
public class PrologReferenceImplementation implements PrologImplementation {

  /**
   * Describe the level of initialization of the Prolog system, between bare minimum, and full-featured.
   * This enum is not in the {@link PrologImplementation} interface since it's particular to the reference implementation.
   */
  public enum InitLevel {
    /**
     * A completely bare prolog engine, not functional for running programs (misses core predicates such as true/1, fail/1, !/1 (cut),
     * =/2, call/1, not/1, etc. Yet unification and inference of user predicates will work. No libraries loaded at all.
     */
    L0_BARE,
    /**
     * This is the default initialization level, it loads the {@link org.logic2j.core.library.impl.CoreLibrary},
     * containing (among others), core predicates such as
     * true/1, fail/1, !/1 (cut), =/2, call/1, not/1, findall/3, etc.
     */
    L1_CORE_LIBRARY,
    /**
     * Higher level libraries loaded, such as {@link org.logic2j.core.library.impl.IOLibrary}.
     */
    L2_BASE_LIBRARIES,
  }

  // ---------------------------------------------------------------------------
  // Define all sub-features of this reference implementation and initialize with default, reference implementations
  // ---------------------------------------------------------------------------

  private TermAdapter termAdapter = new DefaultTermAdapter();