Package com.articulate.sigma

Class KifFileChecker

java.lang.Object
com.articulate.sigma.KifFileChecker
public class KifFileChecker extends Object
Headless KIF checker that mirrors SUMOjEdit.checkErrorsBody logic, but returns diagnostics as strings: "line:col: SEVERITY: message". No UI / jEdit dependencies.

  • Field Details

    • debug

      public static boolean debug

  • Constructor Details

    • KifFileChecker

      public KifFileChecker()

  • Method Details

    • showHelp

      public static void showHelp()
      Print CLI usage information.

    • main

      public static void main(String[] args)
      Command-line entry point. Usage examples: java com.articulate.sigma.KifFileChecker -h java com.articulate.sigma.KifFileChecker -c myfile.kif

    • check

      public static List<ErrRec> check(String contents)
      Check KIF content without a filename.
      Parameters:
      contents - the KIF text to check
      Returns:
      list of error and warning diagnostics

    • check

      public static List<ErrRec> check(String contents, String fileName)
      Runs syntax and semantic checks on KIF content, returning diagnostics.
      Parameters:
      contents - raw KIF text to check
      Returns:
      list of error/warning strings in "line:col: SEVERITY: message" format

    • formatKif

      public static String formatKif(String contents)
      Pretty-print KIF contents using the KIF parser and Formula.toString(). Key behavior: - We only rewrite the top-level formula spans. - Everything outside those spans (comments, blank lines, etc.) is copied EXACTLY as in the original text. - If a formula span contains a ';' comment, we DO NOT reformat it. We keep the original slice to avoid moving inline comments.

    • CheckQuantifiedVariableNotInStatement

      public static void CheckQuantifiedVariableNotInStatement(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)
      Check for quantified variables that do not appear in the statement body.
      Parameters:
      fileName - logical filename
      f - formula to check
      formulaText - raw text of the formula
      formulaStartLine - buffer line offset of the formula
      msgs - list to collect error records

    • CheckOrphanVars

      public static void CheckOrphanVars(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)
      Check for disconnected variable groups
      Parameters:
      fileName - logical filename
      f - formula to check
      formulaText - raw text of the formula
      formulaStartLine - buffer line offset of the formula
      msgs - list to collect error records

    • CheckExistentialInAntecedent

      public static void CheckExistentialInAntecedent(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)
      Check for existential quantifiers in antecedents (illegal).
      Parameters:
      fileName - logical filename
      f - formula to check
      formulaText - raw text of the formula
      formulaStartLine - buffer line offset
      msgs - list to collect error records

    • CheckSingleUseVariables

      public static void CheckSingleUseVariables(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)
      Check for variables that appear only once in a formula.
      Parameters:
      fileName - logical filename
      f - formula to check
      formulaText - raw text of the formula
      formulaStartLine - buffer line offset
      msgs - list to collect error records

    • CheckUnquantInConsequent

      public static void CheckUnquantInConsequent(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)
      Check for unquantified variables appearing in the consequent of implications.
      Parameters:
      fileName - logical filename
      f - formula to check
      formulaText - raw text of the formula
      formulaStartLine - buffer line offset
      msgs - list to collect error records

    • CheckFormulaPreprocess

      public static Set<Formula> CheckFormulaPreprocess(String fileName, KB kb, Formula f, int formulaStartLine, List<ErrRec> msgs)
      Run FormulaPreprocessor and record errors/warnings. Computes accurate absolute line/column using findLineInFormula() by locating the offending token inside the formula text.
      Parameters:
      fileName - logical filename
      kb - knowledge base
      f - formula to preprocess
      formulaStartLine - buffer line offset
      msgs - list to collect error records
      Returns:
      processed formula set

    • CheckSUMOtoTFAformErrors

      public static void CheckSUMOtoTFAformErrors(String fileName, KB kb, Formula f, int formulaStartLine, Set<Formula> processed, List<ErrRec> msgs)
      Correct invocation of SUMO→TFA translation errors. Mirrors SUMOjEdit.checkErrorsBody() behavior. Steps: (1) Clear errors for this formula (2) Run SUMOtoTFAform.process(f,false) (3) Collect any populated SUMOtoTFAform.errors (4) Compute line/column using token matching (5) Clear for next formula

    • CheckIsValidFormula

      public static void CheckIsValidFormula(String fileName, Formula f, int formulaStartLine, KB kb, String formulaText, List<ErrRec> msgs)
      Check if the formula is structurally valid in the KB. Computes absolute line/column by matching the offending token inside the formula text using findLineInFormula().
      Parameters:
      fileName - logical filename
      f - formula
      formulaStartLine - buffer line offset
      kb - knowledge base
      formulaText - raw text of the formula
      msgs - list to collect error records

    • CheckTermsBelowEntity

      public static void CheckTermsBelowEntity(String fileName, Formula f, int formulaStartLine, String formulaText, KB kb, Set<String> localIndividuals, Set<String> localSubclasses, List<ErrRec> msgs)
      Check that all terms are below Entity in the KB hierarchy.
      Parameters:
      fileName - logical filename
      f - formula
      formulaStartLine - buffer line offset
      formulaText - raw text of the formula
      kb - knowledge base
      localIndividuals - set of locally defined individuals
      localSubclasses - set of locally defined subclasses
      msgs - list to collect error records

    • CheckSyntaxErrors

      public static void CheckSyntaxErrors(String contents, String fileName, List<ErrRec> msgs)
      Check for syntax errors during parsing.
      Parameters:
      contents - KIF text
      fileName - logical filename
      msgs - list to collect error records

    • StringToKif

      public static KIF StringToKif(String contents, String fileName, List<ErrRec> errorList)
      Convert raw KIF string into a KIF object, collecting parse errors.
      Parameters:
      contents - KIF text
      fileName - logical filename
      msgs - list to collect error records
      Returns:
      parsed KIF object

    • extractBufferSlice

      public static String extractBufferSlice(String[] bufferLines, int startLine, int endLine)
      Extract a formula's exact text between line numbers.
      Parameters:
      bufferLines - full text split into lines
      startLine - starting line (1-based)
      endLine - ending line
      Returns:
      text slice containing the formula

    • findLineInFormula

      public static int[] findLineInFormula(String formulaText, String term)
      Find the relative line and column offset of a substring (e.g., error term) within a multi-line formula string.
      Parameters:
      formulaText - the full text of the formula
      term - the substring or token we are trying to locate (e.g. error term)
      Returns:
      an int array [lineOffsetWithinFormula, columnOffsetWithinLine], or [-1,-1] if not found.

    • harvestLocalFacts

      public static void harvestLocalFacts(Formula f, Set<String> localIndividuals, Set<String> localSubclasses)
      Recursively collect local individuals and subclasses from formulas.
      Parameters:
      f - formula to traverse
      localIndividuals - set to populate with individuals
      localSubclasses - set to populate with subclasses

    • isConst

      public static boolean isConst(String tok)
      Check if a token represents a constant rather than a variable or literal.
      Parameters:
      tok - token string
      Returns:
      true if constant, false otherwise

    • findFormulaInBuffer

      public static int findFormulaInBuffer(String formulaStr, String[] bufferLines)
      Find where a formula string appears in the buffer.
      Parameters:
      formulaStr - formula text
      bufferLines - full text split into lines
      Returns:
      1-based starting line index, or -1 if not found

    • getOffset

      public static int getOffset(String line)
      sigmaAntlr generates line offsets
      Parameters:
      line - error line text
      Returns:
      the line offset of where the error/warning begins

    • getLineNum

      public static int getLineNum(String line)
      Extract line number from a parser error line.
      Parameters:
      line - error line text
      Returns:
      line number or 0 if not found

    • parseKifError

      public static ErrRec parseKifError(String raw, String fileName)