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 )
- get_def_constraints(self, problem, for_explain=False)[source]
returns the constraints for this definition.
The instantiables (of the definition) are expanded in problem.
- Parameters
problem (Theory) – contains the structure for the expansion/interpretation of the constraints
for_explain (Bool) – Use implications instead of equivalence, for rule-specific explanations
- Returns
a mapping from (Symbol, Definition) to the list of constraints
- Return type
Dict[SymbolDeclaration, Definition, List[Expression]]
- instantiate_definition(self, new_args, theory)[source]
Create an instance of the definition for new_args, and interpret it for theory.
- Parameters
new_args ([Expression]) – tuple of arguments to be applied to the defined symbol
theory (Theory) – the context for the interpretation
- Returns
a boolean expression
- Return type
Expression
- 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