idp_engine.Interpret

Methods to ground / interpret a theory in a data structure

  • expand quantifiers

  • replace symbols interpreted in the structure by their interpretation

This module also includes methods to:

  • substitute a node by another in an AST tree

  • instantiate an expresion, i.e. replace a variable by a value

This module monkey-patches the ASTNode class and sub-classes.

( see docs/zettlr/Substitute.md )

add_def_constraints(self, instantiables, problem, result)[source]

result is updated with the constraints for this definition.

The instantiables (of the definition) are expanded in problem.

Parameters

  • instantiables (Dict[SymbolDeclaration, List[Expression]]) – the constraints without the quantification

  • problem (Theory) – contains the structure for the expansion/interpretation of the constraints

  • result (Dict[SymbolDeclaration, Definition, List[Expression]]) – a mapping from (Symbol, Definition) to the list of constraints

extension(self, interpretations, extensions)[source]

returns the extension of a Type, given some interpretations.

Normally, the extension is already in extensions. However, for Concept[T->T], an additional filtering is applied.

Parameters

  • interpretations (Dict[str, SymbolInterpretation]) –

  • symbols (the known interpretations of types and) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Returns

a superset of the extension of self, and a function that, given arguments, returns an Expression that says whether the arguments are in the extension of self

Return type

Extension