Skip to content

Decorators

Decorators for marking functions as axioms and goals.

Example:

    from dataclasses import dataclass
    from typedlogic import Fact
    from typedlogic.decorators import axiom, goal

    @dataclass
    class Dog(Fact):
        unique_name: str

    @dataclass
    class Cat(Fact):
        unique_name: str

    @axiom
    def disjointness(n: str):
        '''Nothing os both a dog and a cat'''
        assert not(Dog(n) and Cat(n))

    @goal
    def unit_test1():
        '''unit test: if Violet is a cat, then it must be provable that Violet is not a dog'''
        if Cat('Violet'):
           assert not Dog('Violet')

Note: when axioms are expressed directly in python programs, it is possible to use logical connectives such as and, or, as well as if...then to express implication.

When working directly with objects in the datamodel, it's necessary to use symbols such as & and ~.

axiom(func)

Decorator to mark a function as an axiom.

The marked function is not intended to be executed in a standard python environment.

The arguments to the function are treated as universally quantified variables

Example usage:

from dataclasses import dataclass
from typedlogic import Fact
from typedlogic.decorators import axiom, goal

@dataclass
class Dog(Fact):
    unique_name: str

@dataclass
class Cat(Fact):
    unique_name: str

@axiom
def disjointness(n: str):
    '''nothing is both a dog and a cat'''
    assert not(Dog(n) and Cat(n))

The arguments of the wrapped functions are treated as universal quantifiers (Forall x: ...)

Source code in src/typedlogic/decorators.py 
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
def axiom(func: Callable) -> Callable:
    """
    Decorator to mark a function as an axiom.

    The marked function is not intended to be executed in a standard python environment.

    The arguments to the function are treated as universally quantified variables

    Example usage:

        from dataclasses import dataclass
        from typedlogic import Fact
        from typedlogic.decorators import axiom, goal

        @dataclass
        class Dog(Fact):
            unique_name: str

        @dataclass
        class Cat(Fact):
            unique_name: str

        @axiom
        def disjointness(n: str):
            '''nothing is both a dog and a cat'''
            assert not(Dog(n) and Cat(n))

    The arguments of the wrapped functions are treated as universal quantifiers (Forall x: ...)

    """

    @wraps(func)
    def wrapper(*args, **kwargs):
        return func(*args, **kwargs)

    AXIOM_REGISTRY.append(func)
    return wrapper

goal(func)

Decorator to mark a function as a goal.

The prove_goals function in a Solver object will attempt to prove the goal.

The function is not intended to be called directly, but rather to be interpreted using logical semantics.

Source code in src/typedlogic/decorators.py 
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
def goal(func: Callable) -> Callable:
    """
    Decorator to mark a function as a goal.

    The `prove_goals` function in a Solver object will attempt to prove the goal.

    The function is not intended to be called directly, but rather to be interpreted
    using logical semantics.
    """

    @wraps(func)
    def wrapper(*args, **kwargs):
        return func(*args, **kwargs)

    # AXIOM_REGISTRY.append(func)
    return wrapper