pyk.kast.outer module

class KAssoc(value)

Bases: Enum

An enumeration.

LEFT = 'Left'

NON_ASSOC = 'NonAssoc'

RIGHT = 'Right'

final class KBubble(sentence_type: str, contents: str, att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents an unparsed chunk of AST in user-defined syntax.

att: KAtt

contents: str

let(*, sentence_type: str | None = None, contents: str | None = None, att: KAtt | None = None) → KBubble

let_att(att: KAtt) → KBubble

sentence_type: str

to_dict() → dict[str, Any]

final class KClaim(body: KInner, requires: KInner = KToken(token='true', sort=KSort(name='Bool')), ensures: KInner = KToken(token='true', sort=KSort(name='Bool')), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KRuleLike

Represents a K claim, typically a transition with pre/post-conditions.

att: KAtt

body: KInner

property dependencies: list[str]

Return the dependencies of this claim (list of other claims needed to help prove this one or speed up this ones proof).

ensures: KInner

property is_circularity: bool

Return whether this claim is a circularity (must be used coinductively to prove itself).

property is_trusted: bool

Return whether this claim is trusted (does not need to be proven to be considered true).

let(*, body: KInner | None = None, requires: KInner | None = None, ensures: KInner | None = None, att: KAtt | None = None) → KClaim

let_att(att: KAtt) → KClaim

requires: KInner

to_dict() → dict[str, Any]

final class KContext(body: KInner, requires: KInner = KToken(token='true', sort=KSort(name='Bool')), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a K evaluation context, used for isolating chunks of computation and focusing on them.

att: KAtt

body: KInner

let(*, body: KInner | None = None, requires: KInner | None = None, att: KAtt | None = None) → KContext

let_att(att: KAtt) → KContext

requires: KInner

to_dict() → dict[str, Any]

final class KDefinition(main_module_name: str, all_modules: Iterable[KFlatModule], requires: Iterable[KRequire] = (), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KOuter, WithKAtt, Iterable[KFlatModule]

Represents an entire K definition, with file imports and modules in place, and a given module called out as main module.

add_cell_map_items(kast: KInner) → KInner

Wrap cell-map items in the syntactical wrapper that the frontend generates for them (see KDefinition.remove_cell_map_items).

add_ksequence_under_k_productions(kast: KInner) → KInner

Inject a KSequence under the given term if it’s a subsort of K and is being used somewhere that sort K is expected (determined by inspecting the definition).

add_sort_params(kast: KInner) → KInner

Return a given term with the sort parameters on the KLabel filled in (which may be missing because of how the frontend works), best effort.

property alias_rules: tuple[KRule, ...]

Returns the KRule sentences which are alias transitively imported by the main module of this definition.

property all_module_names: tuple[str, ...]

Return the name of all modules in this KDefinition.

all_modules: tuple[KFlatModule, ...]

property all_modules_dict: dict[str, KFlatModule]

Returns a dictionary of all the modules (with names as keys) defined in this definition.

att: KAtt

property brackets: FrozenDict[KSort, KProduction]

property cell_collection_productions: tuple[KProduction, ...]

Returns the KProduction which are cell collection declarations transitively imported by the main module of this definition.

property constructors: tuple[KProduction, ...]

Returns the KProduction which are constructor declarations transitively imported by the main module of this definition.

empty_config(sort: KSort) → KInner

Given a cell-sort, compute an “empty” configuration for it (all the constructor structure of the configuration in place, but variables in cell positions).

static from_dict(d: Mapping[str, Any]) → KDefinition

property function_labels: tuple[str, ...]

Returns the label names of all the KProduction which are function symbols for all modules in this definition.

property functions: tuple[KProduction, ...]

Returns the KProduction which are function declarations transitively imported by the main module of this definition.

greatest_common_subsort(sort1: KSort, sort2: KSort) → KSort | None

Compute the greatest-lower-bound of two sorts in the sort lattice using very simple approach, returning None on failure (not necessarily meaning there isn’t a glb).

init_config(sort: KSort) → KInner

Return an initialized configuration as the user declares it in the semantics, complete with configuration variables in place.

instantiate_cell_vars(term: KInner) → KInner

Given a partially-complete configuration, find positions where there could be more cell structure but instead there are variables and instantiate more cell structure.

least_common_supersort(sort1: KSort, sort2: KSort) → KSort | None

Compute the lowest-upper-bound of two sorts in the sort lattice using very simple approach, returning None on failure (not necessarily meaning there isn’t a lub).

property left_assocs: FrozenDict[str, frozenset[str]]

let(*, main_module_name: str | None = None, all_modules: Iterable[KFlatModule] | None = None, requires: Iterable[KRequire] | None = None, att: KAtt | None = None) → KDefinition

let_att(att: KAtt) → KDefinition

property macro_rules: tuple[KRule, ...]

Returns the KRule sentences which are alias or macro transitively imported by the main module of this definition.

main_module: InitVar[KFlatModule]

main_module_name: str

module(name: str) → KFlatModule

Return the module associated with a given name.

property module_names: tuple[str, ...]

Return the list of module names transitively imported by the main module of this definition.

property modules: tuple[KFlatModule, ...]

Returns the list of modules transitively imported by th emain module of this definition.

property overloads: FrozenDict[str, frozenset[str]]

Return a mapping from symbols to the sets of symbols that overload them.

property priorities: FrozenDict[str, frozenset[str]]

Return a mapping from symbols to the sets of symbols with lower priority.

production_for_cell_sort(sort: KSort) → KProduction

Return the production for a given cell-declaration syntax from the cell’s declared sort.

property productions: tuple[KProduction, ...]

Returns the KProduction transitively imported by the main module of this definition.

remove_cell_map_items(kast: KInner) → KInner

Remove cell-map syntactical wrapper items that the frontend generates (see KDefinition.add_cell_map_items).

requires: tuple[KRequire, ...]

resolve_sorts(label: KLabel) → tuple[KSort, tuple[KSort, ...]]

Compute the result and argument sorts for a given production based on a KLabel.

property right_assocs: FrozenDict[str, frozenset[str]]

property rules: tuple[KRule, ...]

Returns the KRule sentences transitively imported by the main module of this definition.

property semantic_rules: tuple[KRule, ...]

Returns the KRule sentences which are topmost transitively imported by the main module of this definition.

property sentence_by_unique_id: dict[str, KSentence]

sort(kast: KInner) → KSort | None

Compute the sort of a given term using best-effort simple sorting algorithm, returns None on algorithm failure.

sort_strict(kast: KInner) → KSort

Compute the sort of a given term using best-effort simple sorting algorithm, dies on algorithm failure.

sort_vars(kast: KInner, sort: KSort | None = None) → KInner

Return the original term with all the variables having the sorts added or specialized, failing if recieving conflicting sorts for a given variable.

property subsort_table: FrozenDict[KSort, frozenset[KSort]]

Return a mapping from sorts to all their proper subsorts.

subsorts(sort: KSort) → frozenset[KSort]

Return all subsorts of a given KSort by inspecting the definition.

property symbols: FrozenDict[str, KProduction]

property syntax_productions: tuple[KProduction, ...]

Returns the KProduction which are syntax declarations transitively imported by the main module of this definition.

property syntax_symbols: FrozenDict[str, KProduction]

to_dict() → dict[str, Any]

final class KFlatModule(name: str, sentences: Iterable[KSentence] = (), imports: Iterable[KImport] = (), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KOuter, WithKAtt, Iterable[KSentence]

Represents a K module, with a name, list of imports, and list of sentences.

att: KAtt

property cell_collection_productions: tuple[KProduction, ...]

Return all the KProduction sentences from this module that are cell collection declarations.

property claims: tuple[KClaim, ...]

Return all the KClaim declared in this module.

property constructors: tuple[KProduction, ...]

Return all the KProduction sentences from this module that are constructor declarations.

static from_dict(d: Mapping[str, Any]) → KFlatModule

property functions: tuple[KProduction, ...]

Return all the KProduction sentences from this module that are function declarations.

imports: tuple[KImport, ...]

let(*, name: str | None = None, sentences: Iterable[KSentence] | None = None, imports: Iterable[KImport] | None = None, att: KAtt | None = None) → KFlatModule

let_att(att: KAtt) → KFlatModule

map_sentences(f: Callable[[S], S], *, of_type: type[S]) → KFlatModule

map_sentences(f: Callable[[KSentence], KSentence], *, of_type: None = None) → KFlatModule

name: str

property productions: tuple[KProduction, ...]

Return all the KProduction sentences from this module.

property rules: tuple[KRule, ...]

Return all the KRule declared in this module.

property sentence_by_unique_id: dict[str, KSentence]

sentences: tuple[KSentence, ...]

property syntax_productions: tuple[KProduction, ...]

Return all the KProduction sentences from this module that contain KLabel (are EBNF syntax declarations).

property syntax_sorts: tuple[KSyntaxSort, ...]

Return all the KSyntaxSort sentences from this module.

to_dict() → dict[str, Any]

final class KFlatModuleList(main_module: str, modules: Iterable[KFlatModule])

Bases: KOuter

Represents a list of K modules, as returned by the prover parser for example, with a given module called out as the main module.

static from_dict(d: Mapping[str, Any]) → KFlatModuleList

let(*, main_module: str | None = None, modules: Iterable[KFlatModule] | None = None) → KFlatModuleList

main_module: str

modules: tuple[KFlatModule, ...]

to_dict() → dict[str, Any]

final class KImport(name: str, public: bool = True)

Bases: KOuter

Represents a K module import, used for inheriting all the sentences of the imported module into this one.

static from_dict(d: Mapping[str, Any]) → KImport

let(*, name: str | None = None, public: bool | None = None) → KImport

name: str

public: bool

to_dict() → dict[str, Any]

final class KNonTerminal(sort: KSort, name: str | None = None)

Bases: KProductionItem

Represents a non-terminal of a given sort in EBNF productions, for defining arguments to to production.

let(*, sort: KSort | None = None, name: str | None = None) → KNonTerminal

name: str | None

sort: KSort

to_dict() → dict[str, Any]

class KOuter

Bases: KAst

Represents K definitions in KAST format.

Outer syntax is K specific datastructures, including modules, definitions, imports, user-syntax declarations, rules, contexts, and claims.

final class KProduction(sort: str | KSort, items: Iterable[KProductionItem] = (), params: Iterable[str | KSort] = (), klabel: str | KLabel | None = None, att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a production in K’s EBNF grammar definitions, as a sequence of ProductionItem.

property argument_sorts: list[KSort]

Return the sorts of the non-terminal positions of the productions.

property as_subsort: tuple[KSort, KSort] | None

Return a pair (supersort, subsort) if self is a subsort production, and None otherwise.

att: KAtt

property default_format: Format

property is_prefix: bool

The production is of the form t* "(" (n ("," n)*)? ")".

Here, t is a terminal other than "(", "," or ")", and n a non-terminal.

Example: syntax Int ::= "mul" "(" Int "," Int ")"

property is_record: bool

The production is prefix with labelled nonterminals.

items: tuple[KProductionItem, ...]

klabel: KLabel | None

let(*, sort: str | KSort | None = None, items: Iterable[KProductionItem] | None = None, params: Iterable[str | KSort] | None = None, klabel: str | KLabel | None = None, att: KAtt | None = None) → KProduction

let_att(att: KAtt) → KProduction

property non_terminals: tuple[KNonTerminal, ...]

Return the non-terminals of the production.

params: tuple[KSort, ...]

sort: KSort

to_dict() → dict[str, Any]

class KProductionItem

Bases: KOuter

Represents the elements used to declare components of productions in EBNF style.

static from_dict(d: Mapping[str, Any]) → KProductionItem

final class KRegexTerminal(regex: str)

Bases: KProductionItem

Represents a regular-expression terminal in EBNF production, to be matched against input text.

let(*, regex: str | None = None) → KRegexTerminal

regex: str

to_dict() → dict[str, Any]

final class KRequire(require: str)

Bases: KOuter

Represents a K file import of another file.

static from_dict(d: Mapping[str, Any]) → KRequire

let(*, require: str | None = None) → KRequire

require: str

to_dict() → dict[str, Any]

final class KRule(body: KInner, requires: KInner = KToken(token='true', sort=KSort(name='Bool')), ensures: KInner = KToken(token='true', sort=KSort(name='Bool')), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KRuleLike

Represents a K rule definition, typically a conditional rewrite/transition.

att: KAtt

body: KInner

ensures: KInner

let(*, body: KInner | None = None, requires: KInner | None = None, ensures: KInner | None = None, att: KAtt | None = None) → KRule

let_att(att: KAtt) → KRule

property priority: int

requires: KInner

to_dict() → dict[str, Any]

class KRuleLike

Bases: KSentence

Represents something with rule-like structure (with body, requires, and ensures clauses).

body: KInner

ensures: KInner

abstract let(*, body: KInner | None = None, requires: KInner | None = None, ensures: KInner | None = None, att: KAtt | None = None) → RL

requires: KInner

class KSentence

Bases: KOuter, WithKAtt

Represents an individual declaration in a K module.

static from_dict(d: Mapping[str, Any]) → KSentence

property label: str

Return a (hopefully) unique label associated with the given KSentence.

Returns:

Unique label for the given sentence, either (in order): - User supplied label attribute (or supplied in rule label),or - Unique identifier computed and inserted by the frontend.

property source: str | None

Return the source assigned to this sentence, or None.

property unique_id: str | None

Return the unique ID assigned to this sentence, or None.

final class KSortSynonym(new_sort: KSort, old_sort: KSort, att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a sort synonym, allowing declaring a new name for a given sort.

att: KAtt

let(*, old_sort: KSort | None = None, new_sort: KSort | None = None, att: KAtt | None = None) → KSortSynonym

let_att(att: KAtt) → KSortSynonym

new_sort: KSort

old_sort: KSort

to_dict() → dict[str, Any]

final class KSyntaxAssociativity(assoc: KAssoc, tags: Iterable[str] = frozenset({}), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a standalone declaration of operator associativity for tagged productions.

assoc: KAssoc

att: KAtt

let(*, assoc: KAssoc | None = None, tags: Iterable[str] | None = None, att: KAtt | None = None) → KSyntaxAssociativity

let_att(att: KAtt) → KSyntaxAssociativity

tags: frozenset[str]

to_dict() → dict[str, Any]

final class KSyntaxLexical(name: str, regex: str, att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a named piece of lexical syntax, definable as a regular expression.

att: KAtt

let(*, name: str | None = None, regex: str | None = None, att: KAtt | None = None) → KSyntaxLexical

let_att(att: KAtt) → KSyntaxLexical

name: str

regex: str

to_dict() → dict[str, Any]

final class KSyntaxPriority(priorities: Iterable[Iterable[str]] = (), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a standalone declaration of syntax priorities, using productions tags.

att: KAtt

let(*, priorities: Iterable[Iterable[str]] | None = None, att: KAtt | None = None) → KSyntaxPriority

let_att(att: KAtt) → KSyntaxPriority

priorities: tuple[frozenset[str], ...]

to_dict() → dict[str, Any]

final class KSyntaxSort(sort: KSort, params: Iterable[str | KSort] = (), att: KAtt = KAtt(atts=FrozenDict({})))

Bases: KSentence

Represents a sort declaration, potentially parametric.

att: KAtt

let(*, sort: KSort | None = None, params: Iterable[str | KSort] | None = None, att: KAtt | None = None) → KSyntaxSort

let_att(att: KAtt) → KSyntaxSort

params: tuple[KSort, ...]

sort: KSort

to_dict() → dict[str, Any]

final class KTerminal(value: str)

Bases: KProductionItem

Represents a string literal component of a production in EBNF grammar.

let(*, value: str | None = None) → KTerminal

to_dict() → dict[str, Any]

value: str

read_kast_definition(path: str | PathLike) → KDefinition

Read a KDefinition from disk, failing if it’s not actually a KDefinition.