Syntax¶

Base OSF expressions¶

class fosf.syntax.base.DisjunctiveSort(*sorts)[source]¶

Bases: Sort

Parameters:: sorts (str | Sort)

add(*sorts)[source]¶

Parameters:: sorts (str | Sort)

freeze()[source]¶

Return type:: FrozenDisjunctiveSort

class fosf.syntax.base.Feature[source]¶

Bases: str

Represents a Feature symbol.

class fosf.syntax.base.FrozenDisjunctiveSort(*sorts)[source]¶

Bases: Sort

Parameters:: sorts (str | Sort)

thaw()[source]¶

Convert to a mutable DisjunctiveSort.

Return type:: DisjunctiveSort

class fosf.syntax.base.Sort(value)[source]¶

Bases: object

Parameters:: value (str | Sort)

class fosf.syntax.base.Tag[source]¶

Bases: str

Represents a Tag symbol.

Taxonomy¶

class fosf.syntax.taxonomy.BaseTaxonomy(edges)[source]¶

Bases: Generic[T, R]

Generic taxonomy over DAGs with bitvector encoding.

Parameters:: edges (Iterable[tuple[str | T, str | T] | tuple[str | T, str | T, float]])

BOT_PREFIX: str = 'bot'¶

DISJUNCTIVE_TYPE¶: alias of set

NODE_TYPE()¶

TOP_PREFIX: str = 'top'¶

property bot_code: int¶

code(node)[source]¶

Parameters:: node (T | str | Iterable[T])
Return type:: int

glb(*nodes)[source]¶

Parameters:: nodes (T | str)
Return type:: T | R

is_subsort(s, t)[source]¶

Parameters:

s (T | str)
t (T | str)

Return type:

bool

lower_bounds(s)[source]¶

Parameters:: s (str | Sort)
Return type:: set[T]

property top_code: int¶

class fosf.syntax.taxonomy.FuzzySortTaxonomy(edges, instances=None)[source]¶

Bases: SortTaxonomy

Parameters:

edges (Iterable[tuple[str | Sort, str | Sort] | tuple[str | Sort, str | Sort, float]])
instances (dict[str, dict[Sort, float]] | None)

add_instance(instance, sort, degree=1.0, check=True)[source]¶

Parameters:

instance (str)
sort (str | Sort)
degree (float)

degree(s: Sort | str, t: Sort | str) → float[source]¶

degree(s: Sort | str, t: Iterable[Sort | str]) → dict[Sort, float]

degree(s: Iterable[Sort | str], t: Sort | str | Iterable[Sort | str]) → dict[Sort, dict[Sort, float]]

Subsumption degree of s < t in the fuzzy taxonomy

Parameters:

s (Sort | str | Iterable[Sort | str])
t (Sort | str | Iterable[Sort | str])

membership_degree(instance, sort)[source]¶

Parameters:

instance (str)
sort (str | Sort | Iterable)

Return type:

float

class fosf.syntax.taxonomy.SortTaxonomy(edges, instances=None)[source]¶

Bases: BaseTaxonomy[Sort, DisjunctiveSort]

Parameters:

edges (Iterable[tuple[str | Sort, str | Sort] | tuple[str | Sort, str | Sort, float]])
instances (dict[str, dict[Sort, float]] | None)

BOT_PREFIX: str = 'bot'¶

DISJUNCTIVE_TYPE¶: alias of DisjunctiveSort

NODE_TYPE¶: alias of Sort

TOP_PREFIX: str = 'top'¶

add_instance(instance, sort)[source]¶

Parameters:

instance (str)
sort (str | Sort)

glb(*nodes)[source]¶

Parameters:: nodes (Sort | str)
Return type:: Sort | DisjunctiveSort

is_instance(instance, sort)[source]¶

Parameters:

instance (str)
sort (Sort)

is_subsort(s, t, any_subsort=True)[source]¶

Parameters:

s (Sort | str)
t (Sort | str)

Return type:

bool

class fosf.syntax.taxonomy.TagTaxonomy(edges)[source]¶

Bases: BaseTaxonomy[Tag, set[Tag]]

Parameters:: edges (Iterable[tuple[str | T, str | T] | tuple[str | T, str | T, float]])

BOT_PREFIX: str = 'X_bot'¶

DISJUNCTIVE_TYPE¶: alias of set

NODE_TYPE¶: alias of Tag

TOP_PREFIX: str = 'X_top'¶

Terms¶

class fosf.syntax.terms.NormalTerm(X, s=None, subterms=None)[source]¶

Bases: Term

Parameters:

X (Tag)
s (Sort)
subterms (dict[Feature, NormalTerm])

equivalent_to(other)[source]¶

Parameters:: other (NormalTerm)

iter_subterms()[source]¶

tag_to_sort()[source]¶

Return type:: dict[Tag, Sort]

to_clause()[source]¶

Return type:: RootedSolvedClause

class fosf.syntax.terms.Term(X, s=None, subterms=None)[source]¶

Bases: object

X:s(f1 -> t1, …, fn -> tn)

Parameters:

X (Tag)
s (Sort)
subterms (dict[Feature, list[Term]])

bfs()[source]¶

dfs()[source]¶

generate_constraints()[source]¶

iter_subterms()[source]¶

pretty_print(spaces=0, feature='')[source]¶: Pretty-print OSF Term.

sorts()[source]¶

Return type:: set[Sort]

tag_to_sort()[source]¶

Return type:: dict[Tag, set[Sort]]

tags()[source]¶

Return type:: set[Tag]

to_clause()[source]¶

Return type:: RootedClause

Constraints¶

class fosf.syntax.constraints.Clause(*constraints)[source]¶

Bases: object

Parameters:: constraints (Constraint)

add(*constraints)[source]¶

Parameters:: constraints (Constraint)

normalize(taxonomy)[source]¶

Parameters:: taxonomy (SortTaxonomy)
Return type:: SolvedClause

rename(base_tag='X', start=0)[source]¶

Return type:: Clause

sorts()[source]¶

Return type:: set[Sort]

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedClause

class fosf.syntax.constraints.Constraint[source]¶

Bases: ABC

tags: set[Tag] = {}¶

class fosf.syntax.constraints.EqualityConstraint(X, Y)[source]¶

Bases: Constraint

X = Y

Parameters:

X (Tag)
Y (Tag)

X: Tag¶

Y: Tag¶

class fosf.syntax.constraints.FeatureConstraint(X, f, Y)[source]¶

Bases: Constraint

X.f = Y

Parameters:

X (Tag)
f (Feature)
Y (Tag)

X: Tag¶

Y: Tag¶

f: Feature¶

class fosf.syntax.constraints.RootedClause(root, *constraints, ensure_rooted=False)[source]¶

Bases: Clause

Parameters:

root (Tag)
constraints (Constraint)

add(*constraints, ensure_rooted=False)[source]¶

Parameters:: constraints (Constraint)

constraints: set[Constraint]¶

normalize(taxonomy)[source]¶

Parameters:: taxonomy (SortTaxonomy)
Return type:: RootedSolvedClause

rename(base_tag='X', start=0)[source]¶

Return type:: RootedClause

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedClause

tags: set[Tag]¶

class fosf.syntax.constraints.RootedSolvedClause(root, *constraints)[source]¶

Bases: SolvedClause, RootedClause

Parameters:

root (Tag)
constraints (Constraint)

equivalent_to(other)[source]¶

Parameters:: other (RootedSolvedClause)

rename(base_tag='X', start=0)[source]¶

Return type:: RootedSolvedClause

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedSolvedClause

to_term()[source]¶

Return type:: NormalTerm

class fosf.syntax.constraints.SolvedClause(*constraints)[source]¶

Bases: Clause

Parameters:: constraints (Constraint)

add(*constraints)[source]¶

Parameters:: constraints (Constraint)

constraints: set[Constraint]¶

normalize(taxonomy)[source]¶

Parameters:: taxonomy (SortTaxonomy)
Return type:: SolvedClause

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedSolvedClause

tags: set[Tag]¶

class fosf.syntax.constraints.SortConstraint(X, s)[source]¶

Bases: Constraint

X : s

Parameters:

X (Tag)
s (Sort)

Theory¶

class fosf.syntax.theory.OsfTheory(taxonomy, definitions, tags=None, ensure_closed=False)[source]¶

Bases: object

Parameters:

taxonomy (SortTaxonomy)
definitions (dict[Sort, NormalTerm])
tags (dict[Tag, TheoryTag])
ensure_closed (bool)

features(X)[source]¶

Parameters:: X (Tag)
Return type:: dict[Feature, Tag]

sort(X)[source]¶

Parameters:: X (Tag)
Return type:: Sort

class fosf.syntax.theory.TheoryTag(tag, sort, features=None)[source]¶

Bases: object

Parameters:

tag (Tag)
sort (Sort)
features (dict[Feature, Tag])