~plan/plunder

d1cb38641e2b34f1aef11cc729bcee779bcf08b4 — Michael Hueschen a month ago 801e113 master
PLAN.py: add optional tracing
1 files changed, 17 insertions(+), 0 deletions(-)

M doc/plan/PLAN.py
M doc/plan/PLAN.py => doc/plan/PLAN.py +17 -0
@@ 9,6 9,11 @@ def Pin(item):  return Val( (item,) )
def App(f,x):   return Val( (f,x)   )
def Law(n,a,b): return Val( (n,a,b) )

tracing = False;
def print_trace(*args, **kwargs):
  if tracing:
      print(*args, **kwargs)

class Val:
    __match_args__ = ("val",)



@@ 63,6 68,7 @@ class Val:

# Index into a list (represented as App nodes)
def I(f, o, n):
    print_trace(f"I[{f}, {o}, {n}]");
    match (n, o.type):
        case (0, 'app'): return o.tail
        case (0, _):     return o


@@ 71,6 77,7 @@ def I(f, o, n):

# Arity of a value
def A(o):
    print_trace(f"A[{o}]");
    match o.type:
        case 'app': return A(o.head)-1
        case 'pin':


@@ 83,11 90,13 @@ def A(o):

# Cast to nat
def N(o):
    print_trace(f"N[{o}]");
    E(o)
    return (o if o.type == 'nat' else Nat(0))

# Run a law body
def R(n,e,b):
    print_trace(f"R[{n}, {e}, {b}]");
    if b.type == 'nat' and b.nat <= n:
        return I(b, e, n - b.nat)



@@ 97,6 106,7 @@ def R(n,e,b):
        case _:              return b

def L(i,n,e,x):
    print_trace(f"L[{i}, {n}, {e}, {x}]");
    match x.list:
        case [Val(1), v, b]:
            I(999, e, n-i).update(R(n,e,v))


@@ 105,16 115,19 @@ def L(i,n,e,x):
            return R(n,e,x)

def B(a,n,e,b,x):
    print_trace(f"B[{a}, {n}, {e}, {b}, {x}]");
    match x.list:
        case [Val(1), _, k]: return B(a, n+1, App(e, Hol()), b, k)
        case _:              return L(a+1,n,e,b)

# Case matching on nats
def C(z,p,n):
    print_trace(f"C[{z}, {p}, {n}]");
    return z if n==0 else App(p, Nat(n-1))

# Pattern match on PLAN values
def P(p,l,a,n,o):
    print_trace(f"P[{p}, {l}, {a}, {n}, {o}]");
    match o.type:
        case 'app': return App(App(a,o.head), o.tail)
        case 'pin': return App(p, o.item)


@@ 123,6 136,7 @@ def P(p,l,a,n,o):

# Simplify a closure by removing useless pins in the head.
def S(o):
    print_trace(f"S[{o}]");
    if o.type == 'app':
        match o.head.type:
            case 'app': return App(S(o.head), o.tail)


@@ 133,6 147,7 @@ def S(o):

# Execute one simplification step for a saturated expression
def X(k,e):
    print_trace(f"X[{k}, {e}]");
    match (k.type, k.nat):
        case ('app', _): return X(k.head, e)
        case ('pin', _): return X(k.item, e)


@@ 160,6 175,7 @@ def X(k,e):

# Force a full evaluation to Normal-Form
def F(o):
    print_trace(f"F[{o}]");
    E(o)
    if o.type == 'app':
        F(o.head)


@@ 168,6 184,7 @@ def F(o):

# Evaluate to Weak-Head-Normal-Form
def E(o):
    print_trace(f"E[{o}]");
    match o.type:
        case 'hol': raise Exception("<<loop>>")
        case 'app':