Bram
/
new-lang
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: Bram:cbf8e29a84f9d23f775a8e0c3bc395b1ab55352a
Branches Tags
Bram:main
Bram:dev
..
compare: Bram:0612e320b0dfc65fd0fb1f2fe1f95e2e1a99568e
Branches Tags
Bram:main
Bram:dev

No commits in common. "cbf8e29a84f9d23f775a8e0c3bc395b1ab55352a" and "0612e320b0dfc65fd0fb1f2fe1f95e2e1a99568e" have entirely different histories.
cbf8e29a84 ... 0612e320b0

11 changed files with 880 additions and 996 deletions
Show Stats Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1 +0,0 @@
__pycache__/

15
checker/__init__.py
View File

@ -1,15 +0,0 @@
"""
This module hosts various elements that are necessary to create a proof
checker.
"""
from .props import And, Implies, Prop
from .terms import Term, register_known_const
__all__ = [
"And",
"Implies",
"Prop",
"Term",
"register_known_const",
]

101
checker/context.py
View File

@ -1,101 +0,0 @@
"""
The Context helps handle multiple hypotheses in a given proof context.
"""
from __future__ import annotations
from .props import Prop
from dataclasses import dataclass
@dataclass(frozen=True)
class Context:
"""
Base Context that contains multiple assumptions for a given proof.
"""
props : set[Prop]
def contains(self, prop : Prop) -> bool:
"""
Determine whether a proposition is given in the context.
:param prop: The proposition to consider.
:type prop: Prop
:return: Whether the proposition is contained in the context.
:rtype: bool
"""
return prop in self.props
@classmethod
def empty(cls):
return cls(props=set())
def isempty(self) -> bool:
"""
Determine whether the context is empty.
"""
return len(self.props) == 0
def issubseteq(self, other : Context) -> bool:
"""
Determine whether this context is a subset of another context.
:param other: The potentially larger context.
:type other: Context
:return: Whether this context is a subset.
:rtype: bool
"""
return self.props.issubset(other.props)
def issuperseteq(self, other : Context) -> bool:
"""
Determine whether this context has another context as its subset.
:param other: The potentially contained context.
:type other: Context
:return: Whether the context is a subset of this one.
:rtype: bool
"""
return other.issubseteq(self)
def union(self, other : Context) -> Context:
"""
Create a context that contains the propositions of two contexts.
:param other: The other context.
:type other: Context
:return: A context containing the propositions of both contexts.
:type: Context
"""
return Context(props=self.props.union(other.props))
def with_prop(self, prop : Prop) -> Context:
"""
Add a new proposition to the context.
:param prop: Proposition to add.
:type prop: Prop
:return: A context with the proposition included.
:rtype: Context
"""
if prop in self.props:
return self
else:
new_props = [ p for p in self.props ]
new_props.append(prop)
return Context(props=set(new_props))
def without_prop(self, prop : Prop) -> Context:
"""
Remove a proposition from the context, if it was present at all.
:param prop: Proposition to remove.
:type prop: Prop
:return: A context without the proposition.
:rtype: Context
"""
if prop not in self.props:
return self
else:
new_props = [ p for p in self.props if p != prop ]
return Context(props=set(new_props))

10
checker/lib/__init__.py
View File

@ -1,10 +0,0 @@
"""
The library contains basic functions and proofs that you might want to
rely on.
"""
from .basic import kernel_from_int
__all__ = [
"kernel_from_int",
]

66
checker/lib/basic.py
View File

@ -1,66 +0,0 @@
"""
Library containing all the basic functions
"""
# from ..proof import Context, Proof
from ..props import Eq, Or, Prop
from ..terms import App, Const, A1, A2, L1, L2, L3, Lambda, Term, Var, register_known_const
# -----------------------------------------------------------------------------
# Identity function
# -----------------------------------------------------------------------------
# Always returns its input.
id_func = Lambda(lambda x : x)
register_known_const("id", id_func)
register_known_const("identity", id_func)
# # -----------------------------------------------------------------------------
# # Equality
# # -----------------------------------------------------------------------------
# equality = Lambda(Lambda(EqT(lhs=Var(1), rhs=Var(0))))
# register_known_const("eq", equality)
# register_known_const("==", equality)
# -----------------------------------------------------------------------------
# Bool
# -----------------------------------------------------------------------------
bool_t = L2(lambda x, y : x).normalize()
bool_f = L2(lambda x, y : y).normalize()
if_statement = L3(lambda x, y, z : A2(x, y, z)).normalize()
not_statement = L1(lambda b : A2(b, bool_f, bool_t)).normalize()
register_known_const("Bool.False", bool_f)
register_known_const("Bool.True", bool_t)
register_known_const("Bool.elim", if_statement)
register_known_const("Bool.if", if_statement)
register_known_const("Bool.not", not_statement)
def is_bool(x : Term) -> Prop:
return Or(Eq(x=x, y=bool_f), Eq(x=x, y=bool_t))
# -----------------------------------------------------------------------------
# Nat
# -----------------------------------------------------------------------------
zero = Const("Nat.Zero")
succ = Const("Nat.Succ")
def kernel_from_int(n : int) -> Term:
if n < 0:
raise ValueError(
"Int is not Nat"
)
t = zero
for _ in range(n):
t = A1(succ, t)
return t
# def is_nat(x : Term) -> Prop:
# return Or(
# Eq(x=x, y=zero),
# Eq(bool_f, bool_t) # TODO: Construct x = Succ n where isNat(n),
# )

268
checker/proof.py
View File

@ -1,268 +0,0 @@
"""
The proofs module contains various methods to construct a proof.
"""
from __future__ import annotations
from dataclasses import dataclass
from .context import Context
from .props import And, Eq, Or, Prop
class ProofCheckerFailedException(Exception):
pass
@dataclass(frozen=True)
class Proof:
"""
Base class to construct a proof.
"""
context : Context
statement : Prop
def check(self) -> None:
"""
Check whether the proof is self-sufficient. That is, the proof
relies on zero context in order to be considered true.
"""
if self.context.isempty():
return
else:
raise ProofCheckerFailedException(
f"Proof still relies on {len(self.context.props)} assumptions."
)
def and_l(proof : Proof, a : Prop, b : Prop) -> Proof:
"""
Create a proof that collects two hypotheses and collects them in a
logical AND proposition.
$$
Γ, A, B ⊢ C
--------------
Γ, A ∧ B ⊢ C
$$
:param proof: The original proof, including two statements to combine.
:type proof: Proof
:param a: The first proposition to combine.
:type a: Prop
:param b: The second proposition to combine.
:type b: Prop
:return: A proof that combines the two hypotheses in an AND proposition.
:rtype: Proof
:raises ProofCheckerFailedException: One of the two propositions was
not found in the context.
"""
if not proof.context.contains(a):
raise ProofCheckerFailedException(
f"Could not find proposition {a} in the proof's context."
)
if not proof.context.contains(b):
raise ProofCheckerFailedException(
f"Could not find proposition {b} in the proof's context."
)
return Proof(
context=proof.context.without_prop(a).without_prop(b).with_prop(And(a, b)),
statement=proof.statement,
)
def and_r(proof1 : Proof, proof2 : Proof) -> Proof:
"""
Create a proof that demonstrates that the statements of two proofs are
both true.
$$
Γ ⊢ A Γ' ⊢ B
---------------
Γ, Γ' ⊢ A ∧ B
$$
:param proof1: The first proof.
:type proof1: Proof
:param proof2: The second proof.
:type proof2: Proof
:return: A proof demonstrating that both proofs are true.
:rtype: Proof
"""
return Proof(
context=proof1.context.union(proof2.context),
statement=And(proof1.statement, proof2.statement),
)
def assume(statement : Prop) -> Proof:
"""
Gain a tautological proof that proves a statement by assuming
it's true.
:param statement: A propositional statement to prove.
:type statement: Prop
:return: A tautological proof.
:rtype: Proof
"""
return from_assumption(
ctx=Context.empty().with_prop(prop=statement),
statement=statement,
)
def from_assumption(ctx : Context, statement : Prop) -> Proof:
"""
Gain a proof by including the statement in the assumptions.
This is a trivial proof that one typically phrases as such:
$$
Γ, A ⊢ A
$$
:param ctx: The proof's context.
:type ctx: Context
:param statement: The statement to prove.
:type statement: Prop
:raises ProofCheckerFailedException: The statement was not included
as an assumption in the context.
"""
if not ctx.contains(statement):
raise ProofCheckerFailedException(
f"The statement {statement} was not included in the context."
)
return Proof(context=ctx, statement=statement)
def or_l(proof_a : Proof, proof_b : Proof, a : Prop, b : Prop) -> Proof:
"""
Create a proof that builds a generalized OR-statement in the context.
$$
Γ, A ⊢ C Γ, B ⊢ C
----------------------
Γ, A ∨ B ⊢ C
$$
:param proof_a: The first proof.
:type proof_a: Proof
:param proof_b: The second proof.
:type proof_b: Proof
:param a: The proposition from the first proof.
:type a: Prop
:param b: The proposition from the second proof.
:type b: Prop
:return: A proof demonstrating a statement given that either proposition
a or b is true.
:rtype: Proof
"""
statement = proof_a.statement
if statement != proof_b.statement:
raise ProofCheckerFailedException(
"For proof constructor `or_l`, the statements of the two proofs "
"must match: {proof_a.statement} and {proof_b.statement} do not "
"match."
)
if not proof_a.context.contains(a):
raise ProofCheckerFailedException(
f"Proposition {a} not found in context of the first proof."
)
if not proof_b.context.contains(b):
raise ProofCheckerFailedException(
f"Proposition {b} not found in context of the second proof."
)
return Proof(
context=(
proof_a.context.union(proof_b.context)
.without_prop(a).without_prop(b).with_prop(Or(a, b))
),
statement=proof_a.statement,
)
def or_r(proof : Proof, a : Prop, b : Prop) -> Proof:
"""
Create a proof that demonstrates that a generalization is true.
$$
Γ ⊢ A
-----------
Γ ⊢ A ∨ B
$$
:param proof: The proof that demonstrates that the generalization is
correct.
:type proof: Proof
:param a: The proposition on the left side of the OR-statement.
:type a: Prop
:param b: The proposition on the right side of the OR-statement.
:type b: Prop
:return: A proof demonstrating that either of the two statements is
correct.
:rtype: Proof
:raises ProofCheckerFailedException: Neither proposition is proven by
the proof.
"""
if proof.statement != a and proof.statement != b:
raise ProofCheckerFailedException(
f"The given proof proves neither {a} nor {b}."
)
return Proof(
context=proof.context,
statement=Or(a, b),
)
def reflexivity(eq : Eq) -> Proof:
"""
Create a proof that demonstrates that one value is equal to oneself.
Typically, the statement is written slightly differently, but
normalizes to the same value. (e.g. 2 + 3 = 4 + 1)
$$
-----------
Γ ⊢ t = t
$$
:param eq: The equality that can be normalized.
:type eq: Eq
:return: A proof demonstrating that the two sides are equal.
:rtype: Proof
:raises ProofCheckerFailedException: The proof checker was unable to
demonstrate that the two sides are equal.
"""
l = eq.x.normalize()
r = eq.x.normalize()
if l == r:
return Proof(
context=Context.empty(),
statement=eq,
)
else:
# diff_l, diff_r = l.reduce_on_equality(r)
raise ProofCheckerFailedException(
f"Could not normalize {eq.x} = {eq.y}, got stuck at {l} = {r}"
# f"Could not normalize {eq.x} = {eq.y}, got stuck at {diff_l} = {diff_r}"
)
def suppose(ctx : Context, proof : Proof) -> Proof:
"""
Create a proof with more assumptions than were originally necessary to
construct the proof.
$$
Γ ⊢ A
----------
Γ, Γ' ⊢ A
$$
:param ctx: Additional context with additional proofs.
:type ctx: Context
:param proof: The proof to give more assumptions and context.
:type proof: Proof
:return: The proof with additional context.
:rtype: Proof
"""
return Proof(
context=proof.context.union(ctx),
statement=proof.statement,
)

86
checker/props.py
View File

@ -1,86 +0,0 @@
"""
This module hosts propositions.
"""
from __future__ import annotations
from .terms import Term
from dataclasses import dataclass
class Prop:
"""
A proposition is a logical statement. It can be proven by the proof
checker, or it can be used as a hypothesis to prove another
proposition.
"""
def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
"""
Propositions can simplify the proof by creating simpler theorems
and sub-lemmas to prove instead. If this proposition is part of
the assumptions, this function helps transform the goal into
simpler sub-goals.
:return: Tuples of added assumptions with a new goal.
:rtype: list[list[tuple[list[Prop], Prop]]]
"""
return []
def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
"""
Determine which hypotheses are required in the context to prove
this proposition.
The function returns a list of various methods to prove the
proposition. If any of the methods is an empty list, it means
the proposition requires no assumptions and can instead be
computed.
:return: Methods to prove this proposition.
:rtype: list[tuple[list[Prop], Prop]]
"""
return []
@dataclass(frozen=True)
class And(Prop):
"""
The logical and-operator `P ^ Q`.
"""
P : Prop
Q : Prop
@dataclass(frozen=True)
class Eq(Prop):
"""
Compare whether two terms are equal.
"""
x : Term
y : Term
def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
return []
def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
return super().as_proof()
@dataclass(frozen=True)
class Implies(Prop):
"""
The logical operator `P -> Q`.
"""
P : Prop
Q : Prop
@dataclass(frozen=True)
class Or(Prop):
"""
The logical and-operator `P v Q`.
"""
P : Prop
Q : Prop

429
checker/terms.py
View File

@ -1,429 +0,0 @@
"""
Terms are values in an equation. They can be constants, variables,
functions, operators, and many more.
"""
from __future__ import annotations
from typing import Callable
import copy
from dataclasses import dataclass
# Known const values that can be substituted into other values.
_known_consts : dict[str, Term] = {}
# Known functions to normalize certain specific terms with given shapes.
_known_norms : list[Callable[[Term], Term]] = []
USABLE_VAR_NAMES = [
'x', 'y', 'z', 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l',
'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w',
'α', 'β', 'γ', 'δ', 'ε', 'ζ', 'η', 'θ', 'ι', 'κ',
# 'λ', # Avoid confusion
'μ', 'ν', 'ξ', 'ο', 'π', 'ρ', 'σ', 'τ', 'υ', 'φ', 'χ', 'ψ', 'ω'
]
def normalize(term : Term) -> Term:
"""
Create a normalization function. This function simplifies functions as
much as possible.
"""
def norm_iter(term : Term) -> Term:
"""
Normalize a single term. Use both the standard normalization scheme
"""
for func in _known_norms:
term = func(term)
return term
return traverse(f=norm_iter, term=term)
def register_known_const(name : str, value : Term) -> None:
_known_consts[name] = value
def register_known_norm(func : Callable[[Term], Term]) -> None:
_known_norms.append(func)
def std_norm_iter(term : Term) -> Term:
"""
Normalize a single term. Trust that all children values have
already been normalized, or that they will be normalized later on.
:param term: The term to normalize.
:type term: Term
:return: A normalized version of the term.
:rtype: Term
"""
match term:
case App():
match term.f:
case Lambda():
return term.f.substitute(value=term.x)
case _:
return term
case Const():
return _known_consts.get(term.name, term)
case Lambda():
return term
case Var():
return term
case Term():
return term
_known_norms.append(std_norm_iter)
def traverse(f : Callable[[Term], Term], term : Term) -> Term:
"""
Traverse through the tree back-and-forth, aiming to run the given
function as thoroughly as possible to manipulate the term tree.
The function quits once no more operations are created.
**WARNING:** This means the tree might traverse forever.
:param f: The traversal function that replaces terms.
:type f: Callable[[Term], Term]
:param term: The term to traverse.
:type term: Term
:return: The result of the traversed term.
:rtype: Term
"""
a, b = Term(), term
while a != b:
a, b = b, traverse_bottom_up(f=f, term=traverse_top_down(f=f, term=term))
return b
def traverse_bottom_up(f : Callable[[Term], Term], term : Term) -> Term:
"""
Traverse a term from the bottom up, replacing values with whatever the
inserted function returns.
:param f: The traversal function that replaces terms.
:type f: Callable[[Term], Term]
:param term: The term to traverse.
:type term: Term
:return: The result of the traversed term.
:rtype: Term
"""
match term:
case App():
return f(App(
f=traverse_bottom_up(f=f, term=term.f),
x=traverse_bottom_up(f=f, term=term.x)),
)
case Const():
return f(term)
case Lambda():
return term.replace_content(
traverse_bottom_up(f=f, term=term.out)
)
case Var():
return f(term)
case Term():
return f(term)
def traverse_top_down(f : Callable[[Term], Term], term : Term) -> Term:
"""
Traverse a term from the top down, replacing values with whatever the
inserted function returns.
:param f: The traversal function that replaces terms.
:type f: Callable[[Term], Term]
:param term: The term to traverse.
:type term: Term
:return: The result of the traversed term.
:rtype: Term
"""
t = f(term)
match t:
case App():
return App(
f=traverse_top_down(f=f, term=t.f),
x=traverse_top_down(f=f, term=t.x),
)
case Const():
return t
case Lambda():
return t.replace_content(traverse_top_down(f=f, term=t.out))
case Var():
return t
case Term():
return t
class Term:
"""
Base class for all terms.
"""
def __eq__(self, other) -> bool:
"""
Determine whether two terms are equal.
"""
return str(self) == str(other)
def __repr__(self) -> str:
"""
Create a representation of a term.
"""
return self.to_str(vars={})
def normalize(self) -> Term:
return normalize(term=self)
def to_str(self, vars : dict[str, Var]) -> str:
return "<undefined>"
@dataclass(frozen=True)
class App(Term):
"""
An App is the application of a function with an argument.
You could consider it the inverse of the lambda function.
"""
f : Term
x : Term
def __repr__(self) -> str:
"""
Create a representation of a term.
"""
return self.to_str(vars={})
def to_str(self, vars: dict[str, Var]) -> str:
f_str = self.f.to_str(vars=vars)
x_str = self.x.to_str(vars=vars)
return f_str + " " + (f"({x_str})" if " " in x_str else x_str)
A1 = lambda fn, a : App(f=fn, x=a)
A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c)
A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d)
A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e)
A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f)
A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g)
A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h)
@dataclass(frozen=True)
class Const(Term):
"""
Constants are 0-ary functions. They can represent variables, constants
or other values that generally take no input.
"""
name : str
def __repr__(self) -> str:
"""
Create a representation of a term.
"""
return self.to_str(vars={})
def to_str(self, vars: dict[str, Var]) -> str:
return self.name
class Lambda(Term):
"""
Lambdas a nameless 1-ary functions.
"""
out : Term
var : Var
def __init__(self, f : Callable[[Var], Term]) -> None:
self.var = Var()
self.out = f(self.var)
def __repr__(self) -> str:
"""
Create a representation of a term.
"""
return self.to_str(vars={})
def replace_content(self, term : Term) -> Lambda:
"""
Replace the content of the lambda function with the given term.
The new term may still contain the lambda's var as an argument.
:param term: The term to insert in a lambda function.
:type term: Term
:return: The new Lambda function.
:rtype: Lambda
"""
return Lambda(
lambda x : traverse_bottom_up(
f=lambda t : x if t is self.var else t,
term=term,
)
)
def substitute(self, value : Term) -> Term:
"""
Substitute all variables of a given index number.
:param value: The value to replace the variable with.
:type value: Term
:return: A resolved lambda where the term has been substituted.
:rtype: Term
"""
return traverse_bottom_up(
f=lambda t : value if t is self.var else t,
term=self.out,
)
def to_str(self, vars: dict[str, Var]) -> str:
char = ''
for c in USABLE_VAR_NAMES:
if c not in vars:
char = c
vars[c] = self.var
break
else:
raise ValueError(
f"Cannot represent a lambda function that's over {len(USABLE_VAR_NAMES)} layers deep!"
)
s = self.out.to_str(vars=vars)
del vars[char]
return "λ" + char + "." + (f"({s})" if " " in s else s)
L1 = lambda f : Lambda(lambda x : f(x))
L2 = lambda f : Lambda(lambda x : L1(lambda y : f(x, y)))
L3 = lambda f : Lambda(lambda x : L2(lambda y, z : f(x, y, z)))
L4 = lambda f : Lambda(lambda x : L3(lambda y, z, a : f(x, y, z, a)))
L5 = lambda f : Lambda(lambda x : L4(lambda y, z, a, b : f(x, y, z, a, b)))
L6 = lambda f : Lambda(lambda x : L5(lambda y, z, a, b, c : f(x, y, z, a, b, c)))
L7 = lambda f : Lambda(lambda x : L6(lambda y, z, a, b, c, d : f(x, y, z, a, b, c, d)))
L8 = lambda f : Lambda(lambda x : L7(lambda y, z, a, b, c, d, e : f(x, y, z, a, b, c, d, e)))
@dataclass(frozen=True)
class Var(Term):
"""
A variable is a value that can be substituted by a lambda function.
Each lambda function stores a unique var, which can then point to a new
structure later on.
"""
def __repr__(self) -> str:
"""
Create a representation of a term.
"""
return self.to_str(vars={})
def to_str(self, vars: dict[str, Var]) -> str:
for i, v in vars.items():
if v is self:
return i
else:
return "[ERROR:UNKNOWN_VAR]"
if __name__ == "__main__":
print("REPRESENTATIONS")
print(30 * "=")
# x
print(Const("x"))
# λx.(f x)
print(Lambda(lambda a : App(f=Const("f"), x=a)))
# λx.(λy.(x y))
print(Lambda(lambda b : Lambda(lambda c : App(f=b, x=c))))
# Nat.Succ (Nat.Succ Nat.Zero)
print(App(f=Const("Nat.Succ"), x=App(f=Const("Nat.Succ"), x=Const("Nat.Zero"))))
print("\nNORMALIZATIONS")
print(30 * "=")
# foo
a = App(f=Lambda(lambda x : x), x=Const("foo"))
print(a)
print(a.normalize())
# f x
b = App(
f=App(
f=Lambda(
lambda f : Lambda(
lambda x : App(
f=f, x=x
)
)
),
x=Const("f"),
),
x= Const("x"),
)
print(b)
print(b.normalize())
# a b c
c = App(
f=App(
f=App(
f=Lambda(
lambda x : Lambda(
lambda y : Lambda(
lambda z : App(
f=App(f=x, x=y), x=z
)
)
)
),
x=Const("a"),
),
x=Const("b"),
),
x=Const("c"),
)
print(c)
print(c.normalize())
#
d = L3(lambda x, y, z : A2(x, y, z))
print(d)
print(d.normalize())
print("\nSHORTHAND NOTATION")
print(30 * "=")
# λx.(λy.(λz.(x y z))
e = L3(lambda a, b, c : App(f=App(f=a, x=b), x=c))
print(e)
# λx.(λy.(λz.(x y z))
f = L3(lambda a, b, c : A3(L3(lambda a, b, c : A2(a, b, c)), a, b, c))
print(f)
print(f.normalize())
assert e == f.normalize()
# not
bool_t = L2(lambda x, y : x).normalize()
bool_f = L2(lambda x, y : y).normalize()
g = L1(lambda b : A2(b, bool_f, bool_t))
print(g)
print(g.normalize())

529
low.c Normal file
View File

@ -0,0 +1,529 @@
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>
// Structures defined in this file
typedef struct BlockHeader BlockHeader;
typedef struct Closure Closure;
typedef struct Frame Frame;
typedef struct Text Text;
typedef struct UnionType UnionType;
typedef struct Var Var;
// You can change this number to decide how much memory the program is allowed
// 0 - 193 bytes -> The program refuses to start
// 194 - 217 bytes -> The program starts but doesn't do anything
// 218 + bytes -> The program runs successfully
#define MEM_SIZE 193 //1024 * 1024 // 1 MB
#define EXIT_GRACEFULLY 0
#define EXIT_MEMORY_LIMIT_TOO_LOW 11
#define EXIT_COULD_NOT_INIT_MEMORY 12
#define EXIT_OUT_OF_MEMORY_DURING_INITIALIZATION 13
#define EXIT_IMPOSSIBLE_FUNCTION_PHASE 77
#define EXIT_IMPOSSIBLE_FUNCTION_ID 78
#define EXIT_IMPOSSIBLE_FUNCTION_NO_CONTINUATION 79
#define EXIT_IF_NULL(ptr) ({ \
if (!ptr) { \
free(memory); \
printf("Failed to initialize program: out of memory\n"); \
exit(EXIT_OUT_OF_MEMORY_DURING_INITIALIZATION); \
} \
})
/* ============================================================================
* MEMORY
* ============================================================================
*/
// Memory block structure
// This block functions as a header for memory allocations on the heap
typedef struct BlockHeader {
int free;
struct BlockHeader *next;
} BlockHeader;
#define BLOCK_SIZE(header) ({ \
size_t s; \
if (header->next) { \
s = (uint8_t *)(header->next) - (uint8_t *)header; \
} else { \
s = (uint8_t *)(stack_top) - (uint8_t *)header; \
} \
s - sizeof(BlockHeader); \
})
// Global memory pool
static uint8_t *memory = NULL;
static uintptr_t heap_base;
static uintptr_t heap_top;
static uintptr_t stack_base;
static uintptr_t stack_top;
// Initialize the custom memory manager
void init_memory() {
if (MEM_SIZE < sizeof(BlockHeader) + 1) {
printf("Memory limit is too low!\n");
exit(EXIT_MEMORY_LIMIT_TOO_LOW);
}
memory = (uint8_t *)malloc(MEM_SIZE);
if (!memory) {
printf("Memory allocation failed!\n");
exit(EXIT_COULD_NOT_INIT_MEMORY);
}
heap_base = (uintptr_t)memory;
heap_top = heap_base;
stack_base = (uintptr_t)(memory + MEM_SIZE);
stack_top = stack_base;
BlockHeader *curr = (BlockHeader *)heap_base;
curr->free = 1;
curr->next = NULL;
}
// Macro for allocating a number of bytes on the heap
#define HEAP_ALLOC(nbytes) ({ \
void *ptr = NULL; \
BlockHeader *curr = (BlockHeader *)heap_base; \
while(curr) { \
size_t size = (BLOCK_SIZE(curr)); \
if (curr->free && size >= (nbytes)) { \
/* If there's enough memory left over, split off into two */ \
if (size >= (nbytes) + sizeof(BlockHeader) + 1) { \
BlockHeader *new_block = (BlockHeader *)( \
(uint8_t *)curr + sizeof(BlockHeader) + (nbytes) \
); \
new_block->free = 1; \
new_block->next = curr->next; \
curr->next = new_block; \
if ((uint8_t *)heap_top < (uint8_t *)new_block) { \
heap_top = (uintptr_t)new_block + sizeof(BlockHeader); \
} \
} \
/* Assign block to new memory */ \
curr->free = 0; \
ptr = (uint8_t *)curr + sizeof(BlockHeader); \
break; \
} \
/* Otherwise, go to the next block */ \
curr = curr->next; \
} \
ptr; \
})
// Macro for freeing bytes at a given address on the heap
#define HEAP_FREE(ptr) ({ \
if (ptr) { \
BlockHeader *block = (BlockHeader *)( \
(uint8_t *)(ptr) - sizeof(BlockHeader) \
); \
block->free = 1; \
/* Merge adjacent free blocks */ \
BlockHeader *curr = (BlockHeader *)heap_base; \
while (curr) { \
if (curr->free && curr->next && curr->next->free) { \
curr->size += sizeof(BlockHeader) + curr->next->size; \
curr->next = curr->next->next; \
} else { \
curr = curr->next; \
} \
} \
} \
})
// Pointer for debugging: print the heap to stdout
#define HEAP_PRINT_WIDTH 60
#define HEAP_PRINT() ({ \
BlockHeader *curr = (BlockHeader *)heap_base; \
while (curr) { \
size_t size = BLOCK_SIZE(curr); \
printf("BlockHeader at address %ld (physical %p): %lu byte", \
(uint8_t *)curr - memory, curr, size \
); \
if (size == 1) { printf(" of "); } else { printf("s of "); } \
if (curr->free) { \
printf("free memory\n "); \
} else { \
printf("reserved memory\n "); \
} \
unsigned char *content = (uint8_t *)curr; \
for (int i = 0; i < size + sizeof(BlockHeader); i++) { \
if (i == sizeof(BlockHeader)) { printf("| "); } \
printf("%02X ", content[i]); \
if (i > HEAP_PRINT_WIDTH) { printf("..."); break; } \
} \
printf("\n "); \
for (int i = 0; i < size + sizeof(BlockHeader); i++) { \
if (i == sizeof(BlockHeader)) { printf("| "); } \
if (content[i] == 0) { printf(" "); \
} else if (content[i] >= 32 && content[i] < 127) { \
printf("%c ", content[i]); \
} else { printf("__ "); } \
if (i > HEAP_PRINT_WIDTH) { printf("..."); break; } \
} \
printf("\n"); \
curr = curr->next; \
} \
})
#define SPACE_FILL(n) for (int i=0; i<n; i++) { printf(" "); }
// Macro for allocating a number of bytes on the stack
#define STACK_ALLOC(nbytes) ({ \
void *ptr = NULL; \
if (stack_top >= heap_top + (nbytes)) { \
stack_top -= (nbytes); \
ptr = (void *)stack_top; \
} \
ptr; \
})
#define STACK_PRINT_VARIABLE_MAX 5
#define STACK_PRINT(topPtr) ({ \
Frame *cursor = topPtr; \
while (cursor) { \
Frame *next = cursor->cont; \
size_t size; \
if (next) { \
size = (uint8_t *)(next) - (uint8_t *)(cursor); \
} else { \
size = (uint8_t *)(stack_base) - (uint8_t *)(cursor); \
} \
printf("Stack layer at offset -%ld (phsyical %p): %ld byte", \
(uint8_t *)(stack_base) - (uint8_t *)(cursor), cursor, size \
); \
if (size == 1) { printf("\n "); } else { printf("s\n "); } \
unsigned char *content = (uint8_t *)cursor; \
printf("| Code ID"); SPACE_FILL(sizeof(CodeID)*3 - 7 - 1); \
printf("| Phase"); SPACE_FILL(sizeof(int)*3 - 5 - 2); \
printf("| Prev out"); SPACE_FILL(sizeof(Var *)*3-8 - 2); \
printf("| Continuation"); SPACE_FILL(sizeof(Frame *)*3-12 - 1); \
for (int i = 0; i < size - sizeof(Frame); i++) { \
printf("| Variable %d", i + 2); SPACE_FILL(2); \
if (i + 2 == STACK_PRINT_VARIABLE_MAX) { break; } \
} \
printf("|\n | "); \
for (int i = 0; i < sizeof(Frame); i++) { \
printf("%02X ", content[i]); \
} \
for (int i = sizeof(Frame); i < size; i++) { \
if ((i - sizeof(Frame)) % sizeof(Var) == 0) { printf("|"); } \
printf("%02X ", content[i]); \
if (i - sizeof(Frame) == STACK_PRINT_VARIABLE_MAX * sizeof(Var)) { \
break; \
} \
} \
printf("|\n"); \
cursor = cursor->cont; \
} \
})
// #define STACK_PRINT ({ \
// printf("Stack from base %p to top %p:\n", (void *)stack_base, (void *)stack_top); \
// uint8_t *curr = (uint8_t *)stack_top; \
// while ((uintptr_t)curr < stack_base) { \
// printf("Address %ld (physical %p): \n ", curr - memory, curr); \
// for (int i = 0; i < STACK_PRINT_WIDTH && (uintptr_t)(curr + i) < stack_base; i++) { \
// printf("%02X ", curr[i]); \
// } \
// printf("\n "); \
// for (int i = 0; i < STACK_PRINT_WIDTH && (uintptr_t)(curr + i) < stack_base; i++) { \
// if (curr[i] == 0) { \
// printf(" "); \
// } else if (curr[i] >= 32 && curr[i] < 127) { \
// printf("%c ", curr[i]); \
// } else { \
// printf("__ "); \
// } \
// } \
// printf("\n"); \
// curr += STACK_PRINT_WIDTH; \
// } \
// })
// Macro for freeing a number of bytes on the stack
#define STACK_FREE(nbytes) ({ \
stack_top += (nbytes); \
})
#define MEM_DIAGNOSTICS(curr) ({ \
printf("----------------------------\n"); \
printf("Heap base at address %ld (physical %p)\n", \
(uint8_t *)heap_base - (uint8_t *)memory, (uint8_t *)heap_base \
); \
printf("Heap top at address %ld (physical %p)\n", \
(uint8_t *)heap_top - (uint8_t *)memory, (uint8_t *)heap_top \
); \
HEAP_PRINT(); \
printf("----------------------------\n"); \
printf("Heap base at address %ld (physical %p)\n", \
(uint8_t *)heap_base - (uint8_t *)memory, (uint8_t *)heap_base \
); \
printf("Heap top at address %ld (physical %p)\n", \
(uint8_t *)heap_top - (uint8_t *)memory, (uint8_t *)heap_top \
); \
printf("Stack top at address %ld (physical %p)\n", \
(uint8_t *)stack_top - (uint8_t *)memory, (uint8_t *)stack_top \
); \
printf("Stack base at address %ld (physical %p)\n", \
(uint8_t *)stack_base - (uint8_t *)memory, (uint8_t *)stack_base \
); \
printf("----------------------------\n"); \
if (curr) { \
STACK_PRINT(curr); \
} else { \
printf("Stack is NULL!\n"); \
} \
printf("Stack top at address %ld (physical %p)\n", \
(uint8_t *)stack_top - (uint8_t *)memory, (uint8_t *)stack_top \
); \
printf("Stack base at address %ld (physical %p)\n", \
(uint8_t *)stack_base - (uint8_t *)memory, (uint8_t *)stack_base \
); \
printf("----------------------------\n"); \
})
/* ============================================================================
* VARIABLES & VALUES
* ============================================================================
*/
// Types of values that can be stored in the heap
typedef union {
int i;
char c;
Closure *f;
Text *t;
UnionType *u;
} Value;
#define HEAP_ALLOC_VALUE() HEAP_ALLOC(sizeof(Value))
// Types of variables stored in a frame
typedef enum {
ORIGINAL_VARIABLE,
MUTABLE_REFERENCE,
IMMUTABLE_REFERENCE
} VarType;
// Variable
typedef struct Var {
VarType var_type;
Value *value;
} Var;
#define HEAP_ALLOC_VARIABLE() HEAP_ALLOC(sizeof(Var))
// Names of functions
typedef enum {
CODE_F,
CODE_G,
CODE_H,
CODE_EXIT // Indicates termination
} CodeID;
// A closure can represent a function that has yet to gather all inputs
typedef struct Closure {
CodeID code_id;
Var variables[];
} Closure;
// A Text struct represents a string
typedef struct Text {
size_t len;
char s[];
} Text;
// A Union type represents a type that can be one of several values.
// For example:
// type Maybe a = Just a | Nothing
typedef struct UnionType {
int name;
Value values[];
} UnionType;
#define HEAP_ALLOC_CLOSURE(code_id, arity) ({ \
Closure *c = HEAP_ALLOC(sizeof(Closure) + arity * sizeof(Var)); \
if (c) { \
c->code_id = code_id; \
} \
c; \
})
#define HEAP_ALLOC_TEXT(length) ({ \
Text *t = HEAP_ALLOC(sizeof(Text) + length * sizeof(char)); \
if (t) { \
t->len = length; \
for (int i = 0; i < length; i++) { \
t->s[i] = '\0'; \
} \
} \
t; \
})
#define HEAP_ALLOC_UNION_TYPE(name, arity) ({ \
UnionType *u = HEAP_ALLOC(sizeof(UnionType) + arity * sizeof(Value)); \
if (u) { \
u->name = name; \
} \
u; \
})
// Function arity
#define ARITY_F 1
#define ARITY_G 1
#define ARITY_H 1
#define ARITY_EXIT 1
typedef struct Frame {
// Function to execute
CodeID code_id;
// Phase of the function
int phase;
// Return variable from previous frame
Var *prevOut;
// CPS-style next frame to execute
struct Frame *cont;
// Previously captured variables
Var variables[];
} Frame;
#define FRAME_SIZE(arity) sizeof(Frame) + (arity - 1) * sizeof(Var)
#define STACK_ALLOC_FRAME(code_name, arity) ({ \
Frame *f = STACK_ALLOC(FRAME_SIZE(arity)); \
if(f) { \
f->code_id = code_name; \
f->phase = 0; \
f->prevOut = NULL; \
f->cont = NULL; \
} \
f; \
})
#define STACK_FREE_FRAME(arity) STACK_FREE(FRAME_SIZE(arity))
int main(void) {
init_memory();
Text *t = HEAP_ALLOC_TEXT(50); EXIT_IF_NULL(t);
Value *v = HEAP_ALLOC_VALUE(); EXIT_IF_NULL(v);
Var *var = HEAP_ALLOC_VARIABLE(); EXIT_IF_NULL(var);
Frame *fnsh = STACK_ALLOC_FRAME(CODE_EXIT, ARITY_EXIT); EXIT_IF_NULL(fnsh);
Frame *curr = STACK_ALLOC_FRAME(CODE_H, ARITY_H); EXIT_IF_NULL(curr);
sprintf(t->s, "Kaokkokos shall prevail by the hands of Alkbaard!");
v->t = t;
var->var_type = ORIGINAL_VARIABLE;
var->value = v;
curr->prevOut = var;
curr->cont = fnsh;
// STACK_PRINT(curr);
while (curr) {
// MEM_DIAGNOSTICS(curr);
switch (curr->code_id) {
case CODE_F: {
// f(x) = print(x) and return x
Var *x = curr->prevOut;
Frame *next = curr->cont;
STACK_FREE_FRAME(ARITY_F);
if (x) {
printf("%s\n", x->value->t->s);
} else {
printf("NULL: Out of memory!\n");
}
curr = next;
break;
}
case CODE_G: {
// g(x) = String.upper(x)
Var *x = curr->prevOut;
Frame *next = curr->cont;
STACK_FREE_FRAME(ARITY_G);
if (x) {
for (int i = 0; i < x->value->t->len; i++) {
char c = x->value->t->s[i];
if (c >= 'a' && c <= 'z') {
x->value->t->s[i] = c - ('a' - 'A');
}
}
next->prevOut = x;
}
curr = next;
break;
}
case CODE_H : {
// h(x) = f(g(x))
Var *x = curr->prevOut;
Frame *next = curr->cont;
STACK_FREE_FRAME(ARITY_H);
if (x) {
Frame *f = STACK_ALLOC_FRAME(CODE_F, ARITY_F);
if (f) {
Frame *g = STACK_ALLOC_FRAME(CODE_G, ARITY_G);
if (g) {
f->cont = next;
g->prevOut = x;
g->cont = f;
curr = g;
} else {
// No memory available! Free f & exit this function
STACK_FREE_FRAME(ARITY_F);
next->prevOut = NULL;
curr = next;
}
} else {
// No memory available! Exit this function
next->prevOut = NULL;
curr = next;
}
} else {
// prevOut is NULL - we were out of memory!
curr = next;
}
break;
}
case CODE_EXIT: {
// HEAP_PRINT();
free(memory);
exit(EXIT_GRACEFULLY);
break;
}
default: {
free(memory);
printf("ERROR: Reached impossible function id!\n");
exit(EXIT_IMPOSSIBLE_FUNCTION_ID);
break;
}
}
}
free(memory);
printf("ERROR: Reached function with no continuation!\n");
return EXIT_IMPOSSIBLE_FUNCTION_NO_CONTINUATION;
}

351
proof.py Normal file
View File

@ -0,0 +1,351 @@
from __future__ import annotations
from typing import Any, Callable, Union
from dataclasses import dataclass
# -----------------------------------------------------------------------------
# Terms
# -----------------------------------------------------------------------------
class Term:
pass
@dataclass(frozen=True)
class App(Term):
f : Term
x : Term
def __repr__(self):
match self.f:
case App(f=Const("Nat.add"), x=a):
return f"{a} + {self.x}"
case App(f=Const("List.cons"), x=a):
return f"{a} :: {self.x}"
case Const("Nat.Succ"):
cursor, i = self, 0
while True:
match cursor:
case App(f=Const("Nat.Succ")):
cursor = cursor.x
i += 1
case Const("Nat.Zero"):
return str(i)
case _:
xs = str(cursor)
if " " in xs:
xs = "(" + xs + ")"
return "{xs} + {i}"
case _:
fs = str(self.f)
xs = str(self.x)
if " " in fs:
fs = "(" + fs + ")"
if " " in xs:
xs = "(" + xs + ")"
return f"{fs} xs"
A0 = lambda fn : Const(fn)
A1 = lambda fn, a : App(f=A0(fn), x=a)
A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c)
A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d)
A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e)
A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f)
A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g)
A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h)
@dataclass(frozen=True)
class Const(Term):
name : str
def __repr__(self) -> str:
match self.name:
case "List.Nil":
return "[]"
case "Nat.Zero":
return "0"
case _:
return self.name
# --- Bool constructors ---
def Truth() -> Term:
return A0("Bool.Truth")
def Contradiction() -> Term:
return A0("Bool.Contradiction")
# --- List constructors ---
def Nil() -> Term:
return A0("List.Nil")
def Cons(head : Term, tail : Term) -> Term:
return A2("List.Cons", head, tail)
# --- Nat constructors ---
def Zero() -> Term:
return A0("Nat.Zero")
def Succ(n : Term) -> Term:
return A1("Nat.Succ", n)
def kernel_from_int(n : int) -> Term:
if n == 0:
return Zero()
elif n < 0:
raise ValueError("Int is not Nat")
else:
return Succ(kernel_from_int(n-1))
# -----------------------------------------------------------------------------
# Propositions
# -----------------------------------------------------------------------------
class Prop:
pass
@dataclass(frozen=True)
class Contradict(Prop):
s : str
@dataclass(frozen=True)
class Eq(Prop):
lhs : Term
rhs : Term
@dataclass(frozen=True)
class Trivial(Prop):
pass
# def __repr__(self) -> str:
# return "<trivial>"
# -----------------------------------------------------------------------------
# Proofs
# -----------------------------------------------------------------------------
class Proof:
def apply(self, goal : Prop, ctx : Context) -> Prop:
return (
Contradict("Cannot prove using the base class")
)
@dataclass(frozen=True)
class Assumption(Proof):
def apply(self, goal : Prop, ctx : Context) -> Prop:
return (
Trivial() if goal in ctx.props else
Contradict(f"Couldn't find proposition `{goal}` in assumptions")
)
@dataclass(frozen=True)
class Refl(Proof):
def apply(self, goal : Prop, ctx : Context) -> Prop:
match goal:
case Eq():
l = normalize(goal.lhs)
r = normalize(goal.rhs)
if l == r:
return Trivial()
else:
# Reduce to differing parts
while True:
match ( l, r ):
case ( App(), App() ):
if l.x == r.x:
l, r = l.f, r.f
elif l.f == r.f:
l, r = l.x, r.x
else:
break
case _:
break
return Contradict(
f"Couldn't normalize {goal.lhs} = {goal.rhs} any further than to {l} = {r}"
)
case Prop():
return Contradict(
"Cannot prove base proposition"
)
# -----------------------------------------------------------------------------
# Context
# -----------------------------------------------------------------------------
# The context is a set of information you already know.
@dataclass(frozen=True)
class Context:
props : list[Prop]
def with_prop(self, prop : Prop):
return Context([ p for p in self.props ] + [ prop ])
# -----------------------------------------------------------------------------
# Normalization function
# -----------------------------------------------------------------------------
@dataclass(frozen=True)
class F:
arity : int
func : Callable[..., Term | None]
F_ = lambda a : lambda f : F(arity=a, func=f)
F0, F1, F2, F3 = F_(0), F_(1), F_(2), F_(3)
F4, F5, F6, F7 = F_(4), F_(5), F_(6), F_(7)
def apply_rules() -> dict[str, F]:
def __bool_not(x : Term) -> Term | None:
match x:
case Const("Bool.Truth"):
return Contradiction()
case Const("Bool.Contradiction"):
return Truth()
def __list_isempty(x : Term) -> Term | None:
match x:
case Const("List.Nil"):
return Truth()
case App(f=App(f=Const("List.Cons"))):
return Contradiction()
def __list_length(x : Term) -> Term | None:
match x:
case Const("List.Nil"):
return Zero()
case App(f=App(f=Const("List.Cons"), x=head), x=tail):
return Succ(A1("List.length", tail))
def __nat_add(x : Term, y : Term) -> Term | None:
match x:
case Const("Nat.Zero"):
return y
case App(f=Const("Nat.Succ"), x=x_):
return Succ(A2("Nat.add", x_, y))
def __nat_iszero(x : Term) -> Term | None:
match x:
case Const("Nat.Zero"):
return Truth()
case App(f=Const("Nat.Succ")):
return Contradiction()
return {
"Bool.not": F1(__bool_not),
"List.isEmpty": F1(__list_isempty),
"List.length": F1(__list_length),
"Nat.add" : F2(__nat_add),
"Nat.isZero" : F1(__nat_iszero),
}
def normalize(term : Term) -> Term:
match term:
case App():
f = normalize(term.f)
x = normalize(term.x)
cursor = term
items = [ term ]
while True:
match cursor.f:
case App():
cursor = cursor.f
items.append(cursor)
case Const():
name = cursor.f.name
rule = apply_rules().get(name, None)
if rule is None:
return App(f, x) # Unknown function
if len(items) != rule.arity:
# If len(items) is too small, we don't have
# enough inputs yet to evaluate the function
# If len(items) is too large, we already evaluated
# the function before and couldn't optimize.
return App(f, x)
out = rule.func(*reversed([i.x for i in items]))
return normalize(out) if out is not None else App(f, x)
case Const():
return term
case Term():
return term
# -----------------------------------------------------------------------------
# Proof checker
# -----------------------------------------------------------------------------
ProofCheck = Union["Proven", "ProveFailure"]
@dataclass(frozen=True)
class Proven:
pass
@dataclass(frozen=True)
class ProveFailure:
s : str
def check(goal: Prop, proof : Proof, ctx : Context) -> Prop:
return proof.apply(goal, ctx)
# -----------------------------------------------------------------------------
# -----------------------------------------------------------------------------
# -----------------------------------------------------------------------------
if __name__ == "__main__":
# 2 + 3 == 5
print(check(
Eq(
lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)),
rhs=kernel_from_int(5),
),
Refl(),
Context(props=[]),
))
# 2 + 3 == 7
print(check(
Eq(
lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)),
rhs=kernel_from_int(7),
),
Refl(),
Context(props=[]),
))
# 0 + x == x
print(check(
Eq(
lhs=A2("Nat.add", Zero(), Const("x")),
rhs=Const("x")
),
Refl(),
Context(props=[]),
))
# x + 0 == x
print(check(
Eq(
lhs=A2("Nat.add", Const("x"), Zero()),
rhs=Const("x")
),
Refl(),
Context(props=[]),
))

20
proof_checker.py
View File

@ -1,20 +0,0 @@
from checker import lib, proof, props
from checker.terms import App, Const
# Prove : true == not false
p = proof.reflexivity(
props.Eq(
x=Const("Bool.True"),
y=App(f=Const("Bool.not"), x=Const("Bool.False"))
)
)
p.check()
# Prove : false == not true
p = proof.reflexivity(
props.Eq(
x=Const("Bool.False"),
y=App(f=Const("Bool.not"), x=Const("Bool.True"))
)
)
p.check()