RuleAnnotations

The identifiers a theory gives its clauses in comments: a clause followed, on the line of its full stop, by a comment of a single word (h :- b. % r5, the clause spanning one line or more) is tagged with it (RULE). Under prologStrictCompatibility a clause so tagged is the defeasible rule or premise of that identifier, the others strict rules and axioms; otherwise the tag changes nothing. The comments are read with the lexer of 2P-Kt, which keeps them, and the clauses are those its parser gives.

Properties

Link copied to clipboard
const val RULE: String

The tag of a clause with its identifier

Functions

Link copied to clipboard
fun annotate(theory: Theory, text: String): Theory

The clauses of theory, parsed from text, tagged with the identifiers of their comments in text

Link copied to clipboard
fun of(clause: Clause): String?

The identifier clause is tagged with, if any

Link copied to clipboard
fun parse(text: String, operators: OperatorSet): Theory

text parsed with operators, its clauses tagged with the identifiers of their comments