Emi/JSON-Lang
1
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

Add a notation of cantions

Browse source
This commit is contained in:
Emi Simpson 2023-03-05 20:54:48 -05:00
parent 1cf1acaa08
commit 8d3edb1ea8
Signed by: Emi
GPG key ID: A12F2C2FFDC3D847
1 changed files with 60 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

87
ir.py
View file

@ -83,6 +83,14 @@ class IRProp:
return repr(self)
def __repr__(self) -> str:
return f'{self.name}({",".join(str(arg) for arg in self.arguments)})'
def __contains__(self, var: str) -> bool:
"""
Test if a variable with a given name exists in this term
>>> 'x1' in IRProp('friends', [IRProp('John'), IRProp('mother_of', [IRVar('x1')])])
True
"""
return any(var in term for term in self.arguments)
@dataclass(frozen=True)
class IRVar:
@ -111,6 +119,17 @@ class IRVar:
return repr(self)
def __repr__(self) -> str:
return f'*{self.name}'
def __contains__(self, var: str) -> bool:
"""
Test if a variable with a given name exists in this term
>>> 'x1' in IRVar('x1')
True
>>> 'x1' in IRVar('x2')
False
"""
return var == self.name
@dataclass(frozen=True)
class IRNeg:
@ -137,6 +156,14 @@ class IRNeg:
return repr(self)
def __repr__(self) -> str:
return f'¬{self.inner}'
def __contains__(self, var: str) -> bool:
"""
Test if a variable with a given name exists in this term
>>> 'x1' in IRNeg(IRProp('round', [IRVar('x1')]))
True
"""
return var in self.inner
IRTerm: TypeAlias = IRVar | IRProp | IRNeg
Clause: TypeAlias = Sequence[IRTerm]
@ -155,37 +182,43 @@ kismesis(Karkat(), Karkat())
"""
def unify(t1: IRTerm, t2: IRTerm) -> Result[Substitutions, UnificationError]:
"""
Attempt to find a substitution that unifies two terms
"""
Attempt to find a substitution that unifies two terms
If successful, the returned substitutions will cause both term to be equal, when
applied to both.
If successful, the returned substitutions will cause both term to be equal, when
applied to both.
If this method fails, then the pair of subterms which caused the unification to fail
are returned.
If this method fails, then the pair of subterms which caused the unification to fail
are returned.
>>> unify(
... IRProp('imaginary', [IRProp('Rufio')]),
... IRProp('imaginary', [IRVar('x1')])
... )
Ok((Rufio()/x1,))
>>> unify(
... IRProp('imaginary', [IRProp('Rufio')]),
... IRProp('imaginary', [IRVar('x1')])
... )
Ok((Rufio()/x1,))
>>> unify(
... IRProp('dating', [IRProp('Jade'), IRVar('x1')]),
... IRProp('dating', [IRVar('x1'), IRProp('John')])
... )
Err(UnificationMismatch(term1=Jade(), term2=John()))
"""
match (t1, t2):
case (IRVar(v1), IRVar(v2)) if v1 == v2:
return Ok(tuple())
case (IRVar(v), t_other) | (t_other, IRVar(v)):#type:ignore #TODO if v not in t_other:
return Ok((Subst(v, t_other),))
case (IRProp(n1, a1), IRProp(n2, a2)) if n1 == n2 and len(a1) == len(a2):
return unify_clauses(a1, a2)
case (IRNeg(i1), IRNeg(i2)):
return unify(i1, i2)
return Err(UnificationMismatch(t1, t2))
>>> unify(
... IRProp('dating', [IRProp('Jade'), IRVar('x1')]),
... IRProp('dating', [IRVar('x1'), IRProp('John')])
... )
Err(UnificationMismatch(term1=Jade(), term2=John()))
>>> unify(
... IRProp('mother_of', [IRVar('x1')]),
... IRVar('x1')
... )
Err(UnificationMismatch(term1=mother_of(*x1), term2=*x1))
"""
match (t1, t2):
case (IRVar(v1), IRVar(v2)) if v1 == v2:
return Ok(tuple())
case (IRVar(v), t_other) | (t_other, IRVar(v)) if v not in t_other: #type: ignore
return Ok((Subst(v, t_other),))
case (IRProp(n1, a1), IRProp(n2, a2)) if n1 == n2 and len(a1) == len(a2):
return unify_clauses(a1, a2)
case (IRNeg(i1), IRNeg(i2)):
return unify(i1, i2)
return Err(UnificationMismatch(t1, t2))
def unify_clauses(c1: Clause, c2: Clause) -> Result[Substitutions, UnificationError]:
"""