El tipo de las expresiones aritméticas: Valor de la resta

   data Expr = Lit Int
             | Suma Expr Expr
             | Op Expr
             | SiCero Expr Expr Expr
     deriving (Eq, Show)

   valor :: Expr -> Int
   valor (Lit n)        = n
   valor (Suma x y)     = valor x + valor y
   valor (Op x)         = - valor x
   valor (SiCero x y z) | valor x == 0 = valor y
                        | otherwise    = valor z

   resta :: Expr -> Expr -> Expr

   resta (Lit 42) (Lit 2)  ==  Suma (Lit 42) (Op (Lit 2))

   valor (resta x y) == valor x - valor y

module Valor_de_la_resta where
 
import Test.QuickCheck
 
data Expr = Lit Int
          | Suma Expr Expr
          | Op Expr
          | SiCero Expr Expr Expr
  deriving (Eq, Show)
 
valor :: Expr -> Int
valor (Lit n)        = n
valor (Suma x y)     = valor x + valor y
valor (Op x)         = - valor x
valor (SiCero x y z) | valor x == 0 = valor y
                     | otherwise    = valor z
 
resta :: Expr -> Expr -> Expr
resta x y = Suma x (Op y)
 
-- Comprobación de la propiedad
-- ============================
 
-- (exprArbitraria n) es una expresión aleatoria de tamaño n. Por
-- ejemplo,
--    λ> sample (exprArbitraria 3)
--    Op (Op (Lit 0))
--    SiCero (Lit 0) (Lit (-2)) (Lit (-1))
--    Op (Suma (Lit 3) (Lit 0))
--    Op (Lit 5)
--    Op (Lit (-1))
--    Op (Op (Lit 9))
--    Suma (Lit (-12)) (Lit (-12))
--    Suma (Lit (-9)) (Lit 10)
--    Op (Suma (Lit 8) (Lit 15))
--    SiCero (Lit 16) (Lit 9) (Lit (-5))
--    Suma (Lit (-3)) (Lit 1)
exprArbitraria :: Int -> Gen Expr
exprArbitraria n
  | n <= 1 = Lit <$> arbitrary
  | otherwise = oneof
                [ Lit <$> arbitrary
                , let m = div n 2
                  in Suma <$> exprArbitraria m <*> exprArbitraria m
                , Op <$> exprArbitraria (n - 1)
                , let m = div n 3
                  in SiCero <$> exprArbitraria m
                            <*> exprArbitraria m
                            <*> exprArbitraria m ]
 
-- Expr es subclase de Arbitrary
instance Arbitrary Expr where
  arbitrary = sized exprArbitraria
 
 
-- La propiedad es
prop_resta :: Expr -> Expr -> Property
prop_resta x y =
  valor (resta x y) === valor x - valor y
 
-- La comprobación es
--    λ> quickCheck prop_resta
--    +++ OK, passed 100 tests.

from dataclasses import dataclass
from random import choice, randint
 
from hypothesis import given
from hypothesis import strategies as st
 
 
@dataclass
class Expr:
    pass
 
@dataclass
class Lit(Expr):
    x: int
 
@dataclass
class Suma(Expr):
    x: Expr
    y: Expr
 
@dataclass
class Op(Expr):
    x: Expr
 
@dataclass
class SiCero(Expr):
    x: Expr
    y: Expr
    z: Expr
 
def valor(e: Expr) -> int:
    match e:
        case Lit(n):
            return n
        case Suma(x, y):
            return valor(x) + valor(y)
        case Op(x):
            return -valor(x)
        case SiCero(x, y, z):
            return valor(y) if valor(x) == 0 else valor(z)
    assert False
 
def resta(x: Expr, y: Expr) -> Expr:
    return Suma(x, Op(y))
 
# -- Comprobación de la propiedad
# -- ============================
 
# exprArbitraria(n) es una expresión aleatoria de tamaño n. Por
# ejemplo,
#    >>> exprArbitraria(3)
#    Op(x=Op(x=Lit(x=9)))
#    >>> exprArbitraria(3)
#    Op(x=SiCero(x=Lit(x=6), y=Lit(x=2), z=Lit(x=6)))
#    >>> exprArbitraria(3)
#    Suma(x=Lit(x=8), y=Lit(x=2))
def exprArbitraria(n: int) -> Expr:
    if n <= 1:
        return Lit(randint(0, 10))
    m = n // 2
    return choice([Lit(randint(0, 10)),
                   Suma(exprArbitraria(m), exprArbitraria(m)),
                   Op(exprArbitraria(n - 1)),
                   SiCero(exprArbitraria(m),
                          exprArbitraria(m),
                          exprArbitraria(m))])
 
# La propiedad es
@given(st.integers(min_value=1, max_value=10),
       st.integers(min_value=1, max_value=10))
def test_mismaForma(n1: int, n2: int) -> None:
    x = exprArbitraria(n1)
    y = exprArbitraria(n2)
    assert valor(resta(x, y)) == valor(x) - valor(y)
 
# La comprobación es
#    src> poetry run pytest -q valor_de_la_resta.py
#    1 passed in 0.21s