fcl module
- class cls.fcl.Apply(target: Type, function_type: Type, argument_type: Type)[source]
The Apply class represents a type inference rule that applies a function to its argument.
- Parameters
- _abc_impl = <_abc._abc_data object>
- is_combinator: bool = False
- class cls.fcl.Combinator(target: Type, combinator: object)[source]
A representation of a combinator rule.
A Combinator has two attributes:
- Parameters
target (Type) – The target type.
is_combinator (bool) – indicates if this is a combinator.
combinator (object) – The combinator.
- _abc_impl = <_abc._abc_data object>
- combinator: object
- is_combinator: bool = True
- class cls.fcl.Failed(target: Type)[source]
A representation of a failed rule.
A Failed rule represents a situation in which the application of the rule has failed.
- Parameters
target (Type) – The target type the rule failed to apply to.
is_combinator (bool) – indicates if this is a combinator.
- _abc_impl = <_abc._abc_data object>
- is_combinator: bool = False
- class cls.fcl.FiniteCombinatoryLogic(repository: dict[object, cls.types.Type], subtypes: Subtypes, processes=2)[source]
A class to represent finite combinatory logic.
- repositorydict[object, Type]
The repository of objects and their respective types.
- subtypesSubtypes
The subtypes of the objects in the repository.
- processesint, optional
The number of processes to use when splitting the repository. Defaults to the number of CPU cores.
- _accumulate_covers(target: Type, to_cover: set[cls.types.Type], combinator: object, combinator_type: list[list[tuple[list[cls.types.Type], cls.types.Type]]]) tuple[collections.deque[collections.deque[cls.fcl.Rule]], bool][source]
Computes all the covers necessary for a given combinators type, a set of types that need to be covered and a target Type that needs to be inhabitated and converts the covers into a segmented list of lists of rules that the inhabitation machine can process. Note: The partial from _inhabit_cover fixes the first two arguments. This can intuitively be understood as us checking all combinators in the repository against the target and using the cover machine to find out if the combinator can allow us to cover the target.
- Parameters
target – The Type to compute covers for.
to_cover – A list of types for the target to be covered. Recursively computed by organized.
combinator – The combinator that we are preparing for the cover machine.
combinator_type – The type of the combinator.
- Returns
- _check_continue_cover(splits: list[tuple[tuple[list[cls.types.Type], cls.types.Type], set[cls.types.Type]]], to_cover: set[cls.types.Type], current_result: tuple[list[cls.types.Type], cls.types.Type]) Callable[[list['MultiArrow']], tuple[list['MultiArrow'], list['CoverMachineInstruction']]][source]
Contains all the parts of the StepRelation where CheckContinueCover is the current head. (p.46 f.)
- Parameters
splits –
to_cover –
current_result –
- Returns
- _check_cover(splits: list[tuple[tuple[list[cls.types.Type], cls.types.Type], set[cls.types.Type]]], to_cover: set[cls.types.Type]) Callable[[list['MultiArrow']], tuple[list['MultiArrow'], list['CoverMachineInstruction']]][source]
Contains all the parts of the Step Relation where CheckCover is the current head. (p.46 f.)
- Parameters
splits –
to_cover –
- Returns
- static _commit_multi_arrow(combinator: object, m: tuple[list[cls.types.Type], cls.types.Type]) deque[Rule][source]
Converts a MultiArrow into a set of rules that the inhabitation machine can process. This is done by expanding the MultiArrow to nested Arrows and creating the corresponding “Apply” rules. Finally, after all Apply rules the combinator entails have been computed, the combinator itself is added as a rule as well.
Note: This ordering created here is the reason why popLeft is equivalent to dropTargets.
- Parameters
combinator – The combinator being evaluated.
m – The type of the combinator being evaluated.
- Returns
The resulting rules for the inhabitation machine to process.
- static _commit_updates(target: Type, combinator: object, covers: Sequence[tuple[list[cls.types.Type], cls.types.Type]]) deque[deque[Rule]][source]
Takes the output produced by the cover machine and converts it into a list of lists, with each sublist representing an ordered set of Apply rules and a Combinator rule, which can be added to the G_targets set. The ordering is the ordering given on the bottom of page 69.
The MultiArrows that get expanded to Rules are not just the contents of the cover, but use the given target instead of their own target. (Lemma 27, p. 63)
- Parameters
target – The target type to create new rules for.
combinator – The combinator object that will become a rule and is associated with the created rules.
covers – The list of MultiArrows computed by the cover machine.
- Returns
The resulting list of lists, representing the segmented rules.
- _compute_fail_existing(rules: set[cls.fcl.Rule], target: Type) tuple[bool, bool][source]
Computes if the target or a supertype of it have already failed/been uninhabited [1]. Also computes if the target has already been a target in the set of rules or has already failed [2]. A supertype being uninhabited also proves that all of its subtypes are uninhabitable.
If a Failed(target) is found, that means it was failed and existing. If a Failed(supertype of target) is found, that means it failed, but we must check for existence. If neither was the case, we know it was not failed so far, but must still check for existence. The last case is the remaining combination.
- Parameters
rules – This is the set of stable rules, referred to as G_stable in the algorithm.
target – This is the type to compute for.
- Returns
Tuple of Booleans, consisting of ([1], [2]) / (failed, existing).
- _continue_cover(splits: list[tuple[tuple[list[cls.types.Type], cls.types.Type], set[cls.types.Type]]], to_cover: set[cls.types.Type], current_result: tuple[list[cls.types.Type], cls.types.Type]) Callable[[list['MultiArrow']], tuple[list['MultiArrow'], list['CoverMachineInstruction']]][source]
Contains all the parts of the Step Relation where ContinueCover is the current head. (p.46 f.)
- Parameters
splits –
to_cover –
current_result –
- Returns
- _cover(splits: list[tuple[tuple[list[cls.types.Type], cls.types.Type], set[cls.types.Type]]], to_cover: set[cls.types.Type]) Callable[[list['MultiArrow']], tuple[list['MultiArrow'], list['CoverMachineInstruction']]][source]
Contains all the parts of the Step Relation where Cover is the current head. (p.46 f.)
- Parameters
splits –
to_cover –
- Returns
- static _cover_machine(state: list['MultiArrow'], program: list[collections.abc.Callable[[list['MultiArrow']], tuple[list['MultiArrow'], list['CoverMachineInstruction']]]]) list['MultiArrow'][source]
Receives an initial state (cover) and a list of program instructions. These get processed in turn, by popping the head instruction. Each instruction itself is a callable, and the instructions implement the step relation. This function serves as a loop that keeps executing the instructions and manages the program stack and output state. (p.46 f.)
- Parameters
state – A list of MultiArrows
program – The stack of program instructions. Every Instruction
is a callable and contains the actual step relation for the cover machine (p.46f.). The step relation is given across the functions _cover, _continue_cover, _check_continue_cover and _check_cover. :return: The output stack, which is a List of MultiArrows, which represents the computed cover.
- _dcap(sigma: Type, tau: Type) Type[source]
Given two types, checks if one is a subtype of the other. If yes, returns the more specific type, e.g. the subtype. If no, returns the intersection of the two.
- Parameters
sigma – The first type to check.
tau – The second type to check.
- Returns
The resulting type (for merging that part of the MultiArrow).
- static _ground_types_of(rules: set[cls.fcl.Rule]) set[cls.types.Type][source]
- _inhabitation_machine(stable: set[cls.fcl.Rule], targets: deque[deque[Rule]])[source]
Implements the actual inhabitation machine. This calls _inhabitation_step until the list of candidate rules to include in the tree grammar is empty (targets). Variable stable contains the rules that are part of the final computed tree grammar. The contents of stable are, in fact, stable, as in the list is only appended too, and previously committed members of the list do not get modified or removed. (p.69 f.)
- Parameters
stable –
targets –
- Returns
- _inhabitation_step(stable: set[cls.fcl.Rule], targets: deque[deque[Rule]]) bool[source]
Implements the inhabitation machine’s state transition function (p.68).
- Parameters
stable –
targets –
- Returns
- _merge_multi_arrow(arrow1: tuple[list[cls.types.Type], cls.types.Type], arrow2: tuple[list[cls.types.Type], cls.types.Type]) tuple[list[cls.types.Type], cls.types.Type][source]
Merges two MultiArrows into a single MultiArrow with correct types. The MultiArrows have the same length. Each pair of types at the same spot is merged by _dcap, which selects the most specific type possible at that position (the subtype, or their intersection if there is no inheritance). (p.46)
- Parameters
arrow1 – The first MultiArrow.
arrow2 – The second MultiArrow.
- Returns
The resulting MultiArrow from merging arrow1 and arrow2.
- _omega_rules(target: Type) set[cls.fcl.Rule][source]
- static _partition_cover(covered: set[cls.types.Type], to_cover: set[cls.types.Type]) tuple[set[cls.types.Type], set[cls.types.Type]][source]
This helper function partitions the elements of to_cover into two lists: If they are in covered, they get added to in_covered, if they aren’t, they get added to not_in_covered. The idea is that elements that have already been covered are handled different then those that still need to be covered. This function computes exactly those sets. (p.45)
- Parameters
covered – The set of types that are currently already
covered. :param to_cover: The set of types that still needs to be covered. :return: The partitioned sets based on the membership in covered.
- static _prune(rules: set[cls.fcl.Rule]) set[cls.fcl.Rule][source]
- _reduce_multi_arrows(ms: list[tuple[list[cls.types.Type], cls.types.Type]]) list[tuple[list[cls.types.Type], cls.types.Type]][source]
This function eliminates all MultiArrows from the given set (cover) that are redundant when considering subtyping.
- Parameters
ms – The List of MultiArrows that we want to reduce to a minimal necessary size.
- Returns
The reduced List.
- static _split_repo(c: object, ty: Type) tuple[object, list[list[tuple[list[cls.types.Type], cls.types.Type]]]][source]
- static _still_possible(splits: list[tuple[tuple[list[cls.types.Type], cls.types.Type], set[cls.types.Type]]], to_cover: set[cls.types.Type]) bool[source]
This helper function checks each element of to_cover with regard to if it still could be covered by the content of splits. This is very intuitive, we check for the existence of a MultiArrow whose target is the type to be covered, with the left part not mattering. (p.46)
- Parameters
splits – The list of MultiArrows (rules if you will) that
can be used to cover the types in to_cover. :param to_cover: The list of Types to check coverability. :return: False, if there is any type in to_cover that can not be produced by any MultiArrow in splits at all. Else, True. (All types could at this step still be covered)
- inhabit(*targets: Type) InhabitationResult[source]
- static split_ty(ty: Type) list[list[tuple[list[cls.types.Type], cls.types.Type]]][source]
- class cls.fcl.InhabitationResult(targets: list[cls.types.Type], rules: set[cls.fcl.Rule])[source]
The InhabitationResult class is used to represent the inhabitation result, which is a process of finding terms that have a specific type. It stores a list of Type objects (targets) and a set of Rule objects (rules) that define the types and the terms.
The class provides several properties and methods to work with the result.
- static apply_result(result: dict[cls.types.Type, cls.enumeration.Enumeration[cls.fcl.Tree]], r: Apply) Enumeration[Tree][source]
The apply_result method is a static methods that is used to create Enumeration objects for Apply rules.
- check_empty(target: Type) bool[source]
The check_empty method checks if a target type is in the inhabitation result.
- Parameters
target (Type) – is the target to check.
- Returns
True if there are no terms with the type, and False otherwise.
- Return type
bool
- static combinator_result(r: Combinator) Enumeration[Tree][source]
The combinator_result method is a static methods that is used to create Enumeration objects for Combinator rules.
- property enumeration_map: dict[cls.types.Type, cls.enumeration.Enumeration[cls.fcl.Tree]]
The enumeration_map property is a cached property that returns a dictionary where the keys are the target types, and the values are the Enumeration objects that contain the terms of the specific types.
- Returns
a dictionary.
- Return type
dict[Type, Enumeration[Tree]]
- property evaluated: Enumeration[Union[Any, list[Any]]]
The `evaluated`property is a cached property that returns the evaluated result of the raw targets.
- Returns
If the number of targets is 1, the raw target is evaluated and returned as a single value.
Otherwise, the raw targets are evaluated and returned as a list of values. :rtype: Enumeration[Any | list[Any]]
- property grouped_rules: dict[cls.types.Type, set[cls.fcl.Rule]]
The grouped_rules property is a cached property that groups the rules based on their target type.
- Returns
It returns a dictionary where the keys are the target types, and the values are the sets of rules
that have the same target type. :rtype: dict[Type, set[Rule]]
- property infinite: bool
This property signals whether the result is infinite.
- Returns
True if the result is infinite, meaning that the terms with the target types can generate more terms of the same type, and False otherwise.
- Return type
bool
- property non_empty: bool
This property shows if the inhabitation result has solutions for the targets.
- Returns
True if there are any terms for the targets types, and False otherwise.
- Return type
bool
- property raw: Enumeration[cls.fcl.Tree | list[cls.fcl.Tree]]
The raw property is a cached property that returns an Enumeration object that contains either a Tree or a list of Tree objects. The terms are either single terms or lists of terms.
- Returns
Enumeration of resulting terms.
- Return type
Enumeration[Tree | list[Tree]]
- rules: set[cls.fcl.Rule]
- size() int[source]
The size method returns the size of the result.
- Returns
If the result is infinite, it returns -1. Otherwise, it returns the number of terms that have the target types.
- Return type
int
- targets: list[cls.types.Type]
- class cls.fcl.Rule(*, target: Type, is_combinator: bool)[source]
Abstract base class for rules.
A Rule is an abstract representation of a specific aspect of a type in a type system. It has two attributes:
- Parameters
target (Type) – The target type the rule applies to.
is_combinator (bool) – Whether the rule is a combinator.
- _abc_impl = <_abc._abc_data object>
- is_combinator: bool
- class cls.fcl.Tree(rule: ~cls.fcl.Rule, children: tuple['Tree', ...] = <factory>)[source]
A class representing a tree of type rules.
- Parameters
rule (Rule) – The root rule of the tree.
children (tuple) – The children of the tree, represented as a tuple of Tree objects. Default value is an empty tuple.
- class Evaluator(outer: Tree, results: list[Any])[source]
The Evaluator class implements a computation step that evaluates a Tree instance.
- Parameters
outer (Tree) – The Tree instance being evaluated.
results (list) – A list to store the result of the evaluation.
- _abc_impl = <_abc._abc_data object>
- children: tuple['Tree', ...]