pyk.kast.inner module

final class KApply(label: str | KLabel, args: Iterable[KInner])

final class KApply(label: str | KLabel, *args: KInner)

Bases: KInner

Represent the application of a KLabel in a K AST to arguments.

args: tuple[KInner, ...]

property arity: int

Return the count of the arguments.

property is_cell: bool

Return whether this is a cell-label application (based on heuristic about label names).

label: KLabel

let(*, label: str | KLabel | None = None, args: Iterable[KInner] | None = None) → KApply

Return a copy of this KApply with either the label or the arguments updated.

let_terms(terms: Iterable[KInner]) → KApply

match(term: KInner) → Subst | None

property terms: tuple[KInner, ...]

final class KAs(pattern: KInner, alias: KInner)

Bases: KInner

Represent a K #as pattern in the K AST format, with the original pattern and the variabl alias.

alias: KInner

let(*, pattern: KInner | None = None, alias: KInner | None = None) → KAs

Return a copy of this KAs with potentially the pattern or alias updated.

let_terms(terms: Iterable[KInner]) → KAs

match(term: KInner) → Subst | None

pattern: KInner

property terms: tuple[KInner, KInner]

class KInner

Bases: KAst

Represent the AST of a given K inner term.

This class represents the AST of a given term. The nodes in the AST should be coming from a given KDefinition, so that they can be checked for well-typedness.

static from_dict(dct: Mapping[str, Any]) → KInner

Deserialize a given KInner into a more specific type from a dictionary.

static from_json(s: str) → KInner

abstract let_terms(terms: Iterable[KInner]) → KI

Set children of this given KInner.

final map_inner(f: Callable[[KInner], KInner]) → KI

Apply a transformation to all children of this given KInner.

abstract match(term: KInner) → Subst | None

Perform syntactic pattern matching and return the substitution.

Parameters:

term – Term to match.

Returns:

Substitution instantiating self to the term.

abstract property terms: tuple[KInner, ...]

Returns the children of this given KInner.

final to_dict() → dict[str, Any]

final class KLabel(name: str, params: Iterable[str | KSort])

final class KLabel(name: str, *params: str | KSort)

Bases: KAst

Represents a symbol that can be applied in a K AST, potentially with sort parameters.

apply(args: Iterable[KInner]) → KApply

apply(*args: KInner) → KApply

Construct a KApply with this KLabel as the AST head and the supplied parameters as the arguments.

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

let(*, name: str | None = None, params: Iterable[str | KSort] | None = None) → KLabel

Return a copy of this KLabel with potentially the name or sort parameters updated.

name: str

params: tuple[KSort, ...]

to_dict() → dict[str, Any]

final class KRewrite(lhs: KInner, rhs: KInner)

Bases: KInner

Represent a K rewrite in the K AST.

apply(term: KInner) → KInner

Attempt rewriting once at every position in a term bottom-up.

Parameters:

term – Term to rewrite.

Returns:

The term with rewrites applied at every node once starting from the bottom.

apply_top(term: KInner) → KInner

Rewrite a given term at the top

Parameters:

term – Term to rewrite.

Returns:

The term with the rewrite applied once at the top.

let(*, lhs: KInner | None = None, rhs: KInner | None = None) → KRewrite

Return a copy of this KRewrite with potentially the LHS or RHS updated.

let_terms(terms: Iterable[KInner]) → KRewrite

lhs: KInner

match(term: KInner) → Subst | None

replace(term: KInner) → KInner

Similar to apply but using exact syntactic matching instead of pattern matching.

replace_top(term: KInner) → KInner

Similar to apply_top but using exact syntactic matching instead of pattern matching.

rhs: KInner

property terms: tuple[KInner, KInner]

final class KSequence(items: Iterable[KInner])

final class KSequence(*items: KInner)

Bases: KInner, Sequence[KInner]

Represent a associative list of K as a cons-list of KItem for sequencing computation in K AST format.

property arity: int

Return the count of KSequence items.

items: tuple[KInner, ...]

let(*, items: Iterable[KInner] | None = None) → KSequence

Return a copy of this KSequence with the items potentially updated.

let_terms(terms: Iterable[KInner]) → KSequence

match(term: KInner) → Subst | None

property terms: tuple[KInner, ...]

final class KSort(name: str)

Bases: KAst

Store a simple sort name.

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

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

Return a new KSort with the name potentially updated.

name: str

to_dict() → dict[str, Any]

final class KToken(token: str, sort: str | KSort)

Bases: KInner

Represent a domain-value in K AST.

let(*, token: str | None = None, sort: str | KSort | None = None) → KToken

Return a copy of the KToken with the token or sort potentially updated.

let_terms(terms: Iterable[KInner]) → KToken

match(term: KInner) → Subst | None

sort: KSort

property terms: tuple[()]

token: str

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

Bases: KInner

Represent a logical variable in a K AST, with a name and optionally a sort.

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

Return a copy of this KVariable with potentially the name or sort updated.

let_sort(sort: KSort | None) → KVariable

Return a copy of this KVariable with just the sort updated.

let_terms(terms: Iterable[KInner]) → KVariable

match(term: KInner) → Subst

name: str

sort: KSort | None

property terms: tuple[()]

class Subst(subst: Mapping[str, KInner] = FrozenDict({}))

Bases: Mapping[str, KInner]

Represents a substitution, which is a binding of variables to values of KInner.

apply(term: KInner) → KInner

Apply the given substitution to KInner, replacing free variable occurances with their valuations defined in this Subst.

compose(other: Subst) → Subst

Union two substitutions together, preferring the assignments in self if present in both.

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

Deserialize a Subst from a given dictionary representing it.

static from_pred(pred: KInner) → Subst

Given a generic matching logic predicate, attempt to extract a Subst from it.

property is_identity: bool

minimize() → Subst

Return a new substitution with any identity items removed.

property ml_pred: KInner

Turn this Subst into a matching logic predicate using {_#Equals_} operator.

property pred: KInner

Turn this Subst into a boolean predicate using _==K_ operator.

to_dict() → dict[str, Any]

Serialize a Subst to a dictionary representation.

unapply(term: KInner) → KInner

Replace occurances of valuations from this Subst with the variables that they are assigned to.

union(other: Subst) → Subst | None

Union two substitutions together, failing with None if there are conflicting assignments.

bottom_up(f: Callable[[KInner], KInner], kinner: KInner) → KInner

Traverse a term from the bottom moving upward, updating it using a given transformation.

Parameters:

• f – Transformation to apply at each node in the term.

• kinner – Original term to transform.

Returns:

The transformed term.

bottom_up_with_summary(f: Callable[[KInner, list[A]], tuple[KInner, A]], kinner: KInner) → tuple[KInner, A]

Traverse a term from the bottom moving upward, potentially both transforming it and collecting information about it.

Parameters:

• f – Function to apply at each AST node to transform it and collect summary.

• kinner – KInner to apply this transformation to.

Returns:

A tuple of the transformed term and the summarized results.

build_assoc(unit: KInner, label: str | KLabel, terms: Iterable[KInner]) → KInner

Build an associative list.

Parameters:

• unit – The empty variant of the given list type.

• label – The associative list join operator.

• terms – List (potentially empty) of terms to join in an associative list.

Returns:

The list of terms joined using the supplied label, or the unit element in the case of no terms.

build_cons(unit: KInner, label: str | KLabel, terms: Iterable[KInner]) → KInner

Build a cons list.

Parameters:

• unit – The empty variant of the given list type.

• label – The associative list join operator.

• terms – List (potentially empty) of terms to join in an associative list.

Returns:

The list of terms joined using the supplied label, terminated with the unit element.

collect(callback: Callable[[KInner], None], kinner: KInner) → None

Collect information about a given term when traversing it bottom up using a side-effect function.

Parameters:

callback – Function supplied by user which has side-effect of collecting desired information at each AST node.

top_down(f: Callable[[KInner], KInner], kinner: KInner) → KInner

Traverse a term from the top moving downward, updating it using a given transformation.

Parameters:

• f – Transformation to apply at each node in the term.

• kinner – Original term to transform.

Returns:

The transformed term.

var_occurrences(term: KInner) → dict[str, list[KVariable]]

Collect the list of occurrences of each variable in a given term.

Parameters:

term – Term to collect variables from.

Returns:

Dictionary with keys a variable names and value as list of all occurrences of that variable.