From d1cb38641e2b34f1aef11cc729bcee779bcf08b4 Mon Sep 17 00:00:00 2001 From: Michael Hueschen Date: Wed, 21 Feb 2024 22:03:13 -0700 Subject: [PATCH] PLAN.py: add optional tracing --- doc/plan/PLAN.py | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/doc/plan/PLAN.py b/doc/plan/PLAN.py index d34822e..3a6eea0 100644 --- a/doc/plan/PLAN.py +++ b/doc/plan/PLAN.py @@ -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("<>") case 'app': -- 2.45.2