From 700708122ee9ff8e398d45bca2fe992d651f1ea7 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 25 Apr 2026 09:06:18 +0000 Subject: [PATCH] expand-let: wrap multi-token continuation body so multi-line `let` works in WS (eigentrust pitfalls #5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit EigenTrust pitfall #5 (2026-04-23) reported that (let [tnew := [eigentrust-step c p alpha t]] match [rat-lt [linf-norm [sub-vec tnew t]] eps] | true -> tnew | false -> [eigentrust-iterate c p alpha eps [int- budget 1] tnew]) failed with `let: let with bracket bindings requires: (let [bindings...] body)`. Working `let` examples either kept the body on the same line as `let ...]` or used a bracket-grouped expression body — nested `match` inside the body did not parse. Root cause: the whole let form is wrapped in `(...)`. parse-reader's `group-items` applies its "brackets win" rule and DROPS the indent-open/indent-close markers around the body line. The body's continuation tokens (`match x | _ -> x`) end up spliced flat into the let's argument list, so `expand-let` saw `((x := 1) match x ...)` instead of the expected `((x := 1) )` shape. Branch 1 of `expand-let` rejected anything other than `(length rest) = 2`, hence the error. Fix: in `expand-let`'s bracket-bindings branch, when `rest` has more than 2 elements, treat all post-bindings tokens as the body and wrap them as a single application list. This matches the usual "continuation lines are indented further than `let`" convention that `defn` and `match` already honour at the top level. Bare let and empty-body let still raise as before. Test coverage in `tests/test-let-multiline-ws.rkt`: - Read-level shape checks (single-line, single-token continuation, bracket-grouped body, multi-token continuation) document the parser behavior the fix relies on - End-to-end `run-ns-ws-last` checks for: single-line, simple body, bracket-grouped body, multi-token application body, the eigentrust reproducer (multi-line match inside let body), and two-binding let with multi-token body - Empty-body let still raises Co-authored-by: kumavis <1474978+kumavis@users.noreply.github.com> --- .../data/cache/pnet/prologos/data/nat.pnet | 2 +- racket/prologos/macros.rkt | 21 ++- .../prologos/tests/test-let-multiline-ws.rkt | 120 ++++++++++++++++++ 3 files changed, 139 insertions(+), 4 deletions(-) create mode 100644 racket/prologos/tests/test-let-multiline-ws.rkt diff --git a/racket/prologos/data/cache/pnet/prologos/data/nat.pnet b/racket/prologos/data/cache/pnet/prologos/data/nat.pnet index 998e6358d..bbb45dc37 100644 --- a/racket/prologos/data/cache/pnet/prologos/data/nat.pnet +++ b/racket/prologos/data/cache/pnet/prologos/data/nat.pnet @@ -1 +1 @@ -(1 "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos:1771838514" #hasheq((add . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (apply . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0)))))))) (bool-to-nat . (#(struct:expr-Pi mw #(struct:expr-Bool) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Bool) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm true 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-nat-val 0))) #t)))) (clamp . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-hole) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::max) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::min) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))) (compose . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 4))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0))))))))))) (const . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 3))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-bvar 1))))))) (double . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-suc #(struct:expr-app #(struct:expr-fvar prologos::data::nat::double) #(struct:expr-bvar 0)))))) #t)))) (flip . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 4) #(struct:expr-bvar 3))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 4) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))))) (ge? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (gt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::lt?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (id . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 0) #(struct:expr-bvar 1))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 0) #(struct:expr-bvar 0))))) (le? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-fvar prologos::data::nat::zero?) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 1)) #(struct:expr-bvar 0))))))) (lt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)) (#(struct:expr-reduce-arm true 0 #(struct:expr-false)) #(struct:expr-reduce-arm false 0 #(struct:expr-true))) #t))))) (max . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 0)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 1))) #t))))) (min . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 0))) #t))))) (mult . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (nat-eq? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1))) #(struct:expr-reduce-arm false 0 #(struct:expr-false))) #t))))) (on . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 5)))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 1))) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)))))))))))) (pow . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pow) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (pred . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-bvar 0))) #t)))) (prologos::core::apply . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0)))))))) (prologos::core::compose . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 4))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0))))))))))) (prologos::core::const . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 3))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-bvar 1))))))) (prologos::core::flip . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 4) #(struct:expr-bvar 3))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 4) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))))) (prologos::core::id . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 0) #(struct:expr-bvar 1))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 0) #(struct:expr-bvar 0))))) (prologos::core::on . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 5)))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 1))) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)))))))))))) (prologos::data::nat::add . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::bool-to-nat . (#(struct:expr-Pi mw #(struct:expr-Bool) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Bool) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm true 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-nat-val 0))) #t)))) (prologos::data::nat::clamp . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-hole) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::max) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::min) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))) (prologos::data::nat::double . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-suc #(struct:expr-app #(struct:expr-fvar prologos::data::nat::double) #(struct:expr-bvar 0)))))) #t)))) (prologos::data::nat::ge? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (prologos::data::nat::gt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::lt?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (prologos::data::nat::le? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-fvar prologos::data::nat::zero?) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 1)) #(struct:expr-bvar 0))))))) (prologos::data::nat::lt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)) (#(struct:expr-reduce-arm true 0 #(struct:expr-false)) #(struct:expr-reduce-arm false 0 #(struct:expr-true))) #t))))) (prologos::data::nat::max . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 0)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 1))) #t))))) (prologos::data::nat::min . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 0))) #t))))) (prologos::data::nat::mult . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::nat-eq? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1))) #(struct:expr-reduce-arm false 0 #(struct:expr-false))) #t))))) (prologos::data::nat::pow . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pow) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::pred . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-bvar 0))) #t)))) (prologos::data::nat::sub . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pred) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::zero? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-true)) #(struct:expr-reduce-arm suc 1 #(struct:expr-false))) #t)))) (sub . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pred) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (zero? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-true)) #(struct:expr-reduce-arm suc 1 #(struct:expr-false))) #t))))) #hasheq((add . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (apply . #(struct:spec-entry (((A -> B) A -> B)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (bool-to-nat . #(struct:spec-entry ((Bool -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (clamp . #(struct:spec-entry ((Nat Nat -> Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (compose . #(struct:spec-entry (((B -> C) (A -> B) A -> C)) #f #f #(struct:srcloc "" 0 0 0) () ((B Type 0) (C Type 0) (A Type 0)) #f #f)) (const . #(struct:spec-entry ((A B -> A)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (double . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (flip . #(struct:spec-entry (((A -> B -> C) B A -> C)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0) (B Type 0) (C Type 0)) #f #f)) (ge? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (gt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (id . #(struct:spec-entry ((A -> A)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0)) #f #f)) (le? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (lt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (max . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (min . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (mult . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (nat-eq? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (on . #(struct:spec-entry (((B -> B -> C) (A -> B) A A -> C)) #f #f #(struct:srcloc "" 0 0 0) () ((B Type 0) (C Type 0) (A Type 0)) #f #f)) (pow . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (pred . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (sub . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (zero? . #(struct:spec-entry ((Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f))) #hasheq((Ordering . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (add . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 10 0 69)) (and . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 17 0 62)) (apply . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 25 0 23)) (bool-eq . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 38 0 66)) (bool-to-nat . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 119 0 74)) (clamp . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 126 0 54)) (compose . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 20 0 29)) (const . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 15 0 20)) (double . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 24 0 79)) (eq-ord . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (flip . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 30 0 26)) (ge? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 85 0 24)) (gt-ord . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (gt? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 80 0 24)) (id . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 10 0 15)) (implies . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 59 0 33)) (le? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 68 0 31)) (lt-ord . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (lt? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 73 0 73)) (max . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 108 0 66)) (min . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 101 0 66)) (mult . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 17 0 76)) (nand . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 49 0 30)) (nat-eq? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 90 0 80)) (nor . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 54 0 28)) (not . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 10 0 63)) (on . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 36 0 32)) (or . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 24 0 60)) (pow . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 57 0 92)) (pred . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 31 0 60)) (prologos::core::apply . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 25 0 23)) (prologos::core::compose . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 20 0 29)) (prologos::core::const . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 15 0 20)) (prologos::core::flip . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 30 0 26)) (prologos::core::id . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 10 0 15)) (prologos::core::on . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/core.prologos" 36 0 32)) (prologos::data::bool::and . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 17 0 62)) (prologos::data::bool::bool-eq . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 38 0 66)) (prologos::data::bool::implies . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 59 0 33)) (prologos::data::bool::nand . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 49 0 30)) (prologos::data::bool::nor . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 54 0 28)) (prologos::data::bool::not . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 10 0 63)) (prologos::data::bool::or . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 24 0 60)) (prologos::data::bool::xor . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 31 0 62)) (prologos::data::nat::add . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 10 0 69)) (prologos::data::nat::bool-to-nat . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 119 0 74)) (prologos::data::nat::clamp . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 126 0 54)) (prologos::data::nat::double . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 24 0 79)) (prologos::data::nat::ge? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 85 0 24)) (prologos::data::nat::gt? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 80 0 24)) (prologos::data::nat::le? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 68 0 31)) (prologos::data::nat::lt? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 73 0 73)) (prologos::data::nat::max . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 108 0 66)) (prologos::data::nat::min . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 101 0 66)) (prologos::data::nat::mult . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 17 0 76)) (prologos::data::nat::nat-eq? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 90 0 80)) (prologos::data::nat::pow . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 57 0 92)) (prologos::data::nat::pred . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 31 0 60)) (prologos::data::nat::sub . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 50 0 70)) (prologos::data::nat::zero? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 38 0 65)) (prologos::data::ordering::Ordering . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (prologos::data::ordering::eq-ord . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (prologos::data::ordering::gt-ord . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (prologos::data::ordering::lt-ord . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (sub . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 50 0 70)) (xor . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/bool.prologos" 31 0 62)) (zero? . #(struct:srcloc "/Users/avanti/dev/projects/prologos/racket/prologos/lib/prologos/data/nat.prologos" 38 0 65))) (add mult double pred zero? sub pow le? lt? gt? ge? nat-eq? min max bool-to-nat clamp) "prologos::data::nat" #hasheq(($compose . expand-compose-sexp) ($list-literal . expand-list-literal) ($lseq-literal . expand-lseq-literal) ($mixfix . expand-mixfix-form) ($pipe-gt . expand-pipe-block) ($quasiquote . expand-quasiquote) ($quote . expand-quote) (cond . expand-cond) (do . expand-do) (if . expand-if) (let . expand-let) (pipe2 . #(struct:preparse-macro pipe2 (pipe2 $x $f $g) ($g ($f $x)))) (pipe3 . #(struct:preparse-macro pipe3 (pipe3 $x $f $g $h) ($h ($g ($f $x))))) (twice . #(struct:preparse-macro twice (twice $f $x) ($f ($f $x)))) (unless . #(struct:preparse-macro unless (unless $cond $body) (if $cond unit $body))) (when . #(struct:preparse-macro when (when $cond $body) (if $cond $body unit))) (with-transient . expand-with-transient)) #hasheq((eq-ord . #(struct:ctor-meta Ordering () () () 1)) (false . #(struct:ctor-meta Bool () () () 1)) (gt-ord . #(struct:ctor-meta Ordering () () () 2)) (lt-ord . #(struct:ctor-meta Ordering () () () 0)) (suc . #(struct:ctor-meta Nat () (Nat) (#t) 1)) (true . #(struct:ctor-meta Bool () () () 0)) (unit . #(struct:ctor-meta Unit () () () 0)) (zero . #(struct:ctor-meta Nat () () () 0))) #hasheq((Bool . (true false)) (Nat . (zero suc)) (Ordering . (lt-ord eq-ord gt-ord)) (Unit . (unit))) #hasheq() #hasheq(((Posit32 . Posit64) . #t) ((Nat . Rat) . #t) ((Posit8 . Posit16) . #t) ((Posit16 . Posit64) . #t) ((Int . Rat) . #t) ((Posit16 . Posit32) . #t) ((Nat . Int) . #t) ((Posit8 . Posit64) . #t) ((Posit8 . Posit32) . #t)) #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq((add . (x y)) (and . (a b)) (apply . (A B f x)) (bool-eq . (a b)) (bool-to-nat . (b)) (clamp . (low high)) (compose . (B C A g f x)) (const . (A B x _)) (double . (n)) (flip . (A B C f b a)) (ge? . (x y)) (gt? . (x y)) (id . (A x)) (implies . (a b)) (le? . (x y)) (lt? . (x y)) (max . (x y)) (min . (x y)) (mult . (x y)) (nand . (a b)) (nat-eq? . (x y)) (nor . (a b)) (not . (b)) (on . (B C A f g x y)) (or . (a b)) (pow . (base exp)) (pred . (n)) (sub . (x y)) (xor . (a b)) (zero? . (n))) #hasheq() #hasheq() #hasheq()) \ No newline at end of file +(1 "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos:1776910266" #hasheq((add . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (apply . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0)))))))) (bool-to-nat . (#(struct:expr-Pi mw #(struct:expr-Bool) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Bool) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm true 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-nat-val 0))) #t)))) (clamp . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-hole) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::max) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::min) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))) (compose . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 4))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0))))))))))) (const . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 3))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-bvar 1))))))) (double . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-suc #(struct:expr-app #(struct:expr-fvar prologos::data::nat::double) #(struct:expr-bvar 0)))))) #t)))) (flip . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 4) #(struct:expr-bvar 3))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 4) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))))) (ge? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (gt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::lt?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (id . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 0) #(struct:expr-bvar 1))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 0) #(struct:expr-bvar 0))))) (le? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-fvar prologos::data::nat::zero?) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 1)) #(struct:expr-bvar 0))))))) (lt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)) (#(struct:expr-reduce-arm true 0 #(struct:expr-false)) #(struct:expr-reduce-arm false 0 #(struct:expr-true))) #t))))) (max . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 0)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 1))) #t))))) (min . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 0))) #t))))) (mult . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (nat-eq? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1))) #(struct:expr-reduce-arm false 0 #(struct:expr-false))) #t))))) (on . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 5)))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 1))) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)))))))))))) (pow . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pow) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (pred . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-bvar 0))) #t)))) (prologos::core::apply . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 1)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0)))))))) (prologos::core::compose . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 4))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-app #(struct:expr-bvar 1) #(struct:expr-bvar 0))))))))))) (prologos::core::const . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 3))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-lam mw #(struct:expr-bvar 1) #(struct:expr-bvar 1))))))) (prologos::core::flip . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 4) #(struct:expr-bvar 3))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-bvar 2))) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 4) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))))) (prologos::core::id . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-bvar 0) #(struct:expr-bvar 1))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-bvar 0) #(struct:expr-bvar 0))))) (prologos::core::on . (#(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-Pi mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 5)))))))) . #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam m0 #(struct:expr-Type #(struct:lzero)) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 2) #(struct:expr-Pi mw #(struct:expr-bvar 3) #(struct:expr-bvar 3))) #(struct:expr-lam mw #(struct:expr-Pi mw #(struct:expr-bvar 1) #(struct:expr-bvar 4)) #(struct:expr-lam mw #(struct:expr-bvar 2) #(struct:expr-lam mw #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-app #(struct:expr-bvar 3) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 1))) #(struct:expr-app #(struct:expr-bvar 2) #(struct:expr-bvar 0)))))))))))) (prologos::data::nat::add . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::bool-to-nat . (#(struct:expr-Pi mw #(struct:expr-Bool) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Bool) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm true 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-nat-val 0))) #t)))) (prologos::data::nat::clamp . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-hole) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::max) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::min) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))))) (prologos::data::nat::double . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-suc #(struct:expr-suc #(struct:expr-app #(struct:expr-fvar prologos::data::nat::double) #(struct:expr-bvar 0)))))) #t)))) (prologos::data::nat::ge? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (prologos::data::nat::gt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::lt?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)))))) (prologos::data::nat::le? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-app #(struct:expr-fvar prologos::data::nat::zero?) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 1)) #(struct:expr-bvar 0))))))) (prologos::data::nat::lt? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1)) (#(struct:expr-reduce-arm true 0 #(struct:expr-false)) #(struct:expr-reduce-arm false 0 #(struct:expr-true))) #t))))) (prologos::data::nat::max . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 0)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 1))) #t))))) (prologos::data::nat::min . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm false 0 #(struct:expr-bvar 0))) #t))))) (prologos::data::nat::mult . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::add) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::nat-eq? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 1)) #(struct:expr-bvar 0)) (#(struct:expr-reduce-arm true 0 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::le?) #(struct:expr-bvar 0)) #(struct:expr-bvar 1))) #(struct:expr-reduce-arm false 0 #(struct:expr-false))) #t))))) (prologos::data::nat::pow . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::mult) #(struct:expr-bvar 2)) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pow) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::pred . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-nat-val 0)) #(struct:expr-reduce-arm suc 1 #(struct:expr-bvar 0))) #t)))) (prologos::data::nat::sub . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pred) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (prologos::data::nat::zero? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-true)) #(struct:expr-reduce-arm suc 1 #(struct:expr-false))) #t)))) (sub . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Nat))) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-bvar 1)) #(struct:expr-reduce-arm suc 1 #(struct:expr-app #(struct:expr-fvar prologos::data::nat::pred) #(struct:expr-app #(struct:expr-app #(struct:expr-fvar prologos::data::nat::sub) #(struct:expr-bvar 2)) #(struct:expr-bvar 0))))) #t))))) (zero? . (#(struct:expr-Pi mw #(struct:expr-Nat) #(struct:expr-Bool)) . #(struct:expr-lam mw #(struct:expr-Nat) #(struct:expr-reduce #(struct:expr-bvar 0) (#(struct:expr-reduce-arm zero 0 #(struct:expr-true)) #(struct:expr-reduce-arm suc 1 #(struct:expr-false))) #t))))) #hasheq((add . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (apply . #(struct:spec-entry (((A -> B) A -> B)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (bool-to-nat . #(struct:spec-entry ((Bool -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (clamp . #(struct:spec-entry ((Nat Nat -> Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (compose . #(struct:spec-entry (((B -> C) (A -> B) A -> C)) #f #f #(struct:srcloc "" 0 0 0) () ((B Type 0) (C Type 0) (A Type 0)) #f #f)) (const . #(struct:spec-entry ((A B -> A)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (double . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (flip . #(struct:spec-entry (((A -> B -> C) B A -> C)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0) (B Type 0) (C Type 0)) #f #f)) (ge? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (gt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (id . #(struct:spec-entry ((A -> A)) #f #f #(struct:srcloc "" 0 0 0) () ((A Type 0)) #f #f)) (le? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (lt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (max . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (min . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (mult . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (nat-eq? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (on . #(struct:spec-entry (((B -> B -> C) (A -> B) A A -> C)) #f #f #(struct:srcloc "" 0 0 0) () ((B Type 0) (C Type 0) (A Type 0)) #f #f)) (pow . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (pred . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (sub . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f)) (zero? . #(struct:spec-entry ((Nat -> Bool)) #f #f #(struct:srcloc "" 0 0 0) () () #f #f))) #hasheq((Ordering . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (add . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 10 0 69)) (and . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 17 0 62)) (apply . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 25 0 23)) (bool-eq . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 38 0 66)) (bool-to-nat . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 119 0 74)) (clamp . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 126 0 54)) (compose . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 20 0 29)) (const . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 15 0 20)) (double . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 24 0 79)) (eq-ord . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (flip . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 30 0 26)) (ge? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 85 0 24)) (gt-ord . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (gt? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 80 0 24)) (id . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 10 0 15)) (implies . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 59 0 33)) (le? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 68 0 31)) (lt-ord . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (lt? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 73 0 73)) (max . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 108 0 66)) (min . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 101 0 66)) (mult . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 17 0 76)) (nand . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 49 0 30)) (nat-eq? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 90 0 80)) (nor . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 54 0 28)) (not . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 10 0 63)) (on . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 36 0 32)) (or . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 24 0 60)) (pow . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 57 0 92)) (pred . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 31 0 60)) (prologos::core::apply . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 25 0 23)) (prologos::core::compose . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 20 0 29)) (prologos::core::const . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 15 0 20)) (prologos::core::flip . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 30 0 26)) (prologos::core::id . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 10 0 15)) (prologos::core::on . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/core.prologos" 36 0 32)) (prologos::data::bool::and . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 17 0 62)) (prologos::data::bool::bool-eq . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 38 0 66)) (prologos::data::bool::implies . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 59 0 33)) (prologos::data::bool::nand . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 49 0 30)) (prologos::data::bool::nor . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 54 0 28)) (prologos::data::bool::not . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 10 0 63)) (prologos::data::bool::or . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 24 0 60)) (prologos::data::bool::xor . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 31 0 62)) (prologos::data::nat::add . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 10 0 69)) (prologos::data::nat::bool-to-nat . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 119 0 74)) (prologos::data::nat::clamp . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 126 0 54)) (prologos::data::nat::double . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 24 0 79)) (prologos::data::nat::ge? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 85 0 24)) (prologos::data::nat::gt? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 80 0 24)) (prologos::data::nat::le? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 68 0 31)) (prologos::data::nat::lt? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 73 0 73)) (prologos::data::nat::max . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 108 0 66)) (prologos::data::nat::min . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 101 0 66)) (prologos::data::nat::mult . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 17 0 76)) (prologos::data::nat::nat-eq? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 90 0 80)) (prologos::data::nat::pow . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 57 0 92)) (prologos::data::nat::pred . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 31 0 60)) (prologos::data::nat::sub . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 50 0 70)) (prologos::data::nat::zero? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 38 0 65)) (prologos::data::ordering::Ordering . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (prologos::data::ordering::eq-ord . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (prologos::data::ordering::gt-ord . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (prologos::data::ordering::lt-ord . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/ordering.prologos" 8 0 40)) (sub . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 50 0 70)) (xor . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/bool.prologos" 31 0 62)) (zero? . #(struct:srcloc "/home/user/prologos/racket/prologos/lib/prologos/data/nat.prologos" 38 0 65))) (add mult double pred zero? sub pow le? lt? gt? ge? nat-eq? min max bool-to-nat clamp) "prologos::data::nat" #hasheq(($compose . expand-compose-sexp) ($list-literal . expand-list-literal) ($lseq-literal . expand-lseq-literal) ($mixfix . expand-mixfix-form) ($pipe-gt . expand-pipe-block) ($quasiquote . expand-quasiquote) ($quote . expand-quote) (cond . expand-cond) (do . expand-do) (if . expand-if) (let . expand-let) (pipe2 . #(struct:preparse-macro pipe2 (pipe2 $x $f $g) ($g ($f $x)))) (pipe3 . #(struct:preparse-macro pipe3 (pipe3 $x $f $g $h) ($h ($g ($f $x))))) (twice . #(struct:preparse-macro twice (twice $f $x) ($f ($f $x)))) (unless . #(struct:preparse-macro unless (unless $cond $body) (if $cond unit $body))) (when . #(struct:preparse-macro when (when $cond $body) (if $cond $body unit))) (with-transient . expand-with-transient)) #hasheq((eq-ord . #(struct:ctor-meta Ordering () () () 1)) (false . #(struct:ctor-meta Bool () () () 1)) (gt-ord . #(struct:ctor-meta Ordering () () () 2)) (lt-ord . #(struct:ctor-meta Ordering () () () 0)) (suc . #(struct:ctor-meta Nat () (Nat) (#t) 1)) (true . #(struct:ctor-meta Bool () () () 0)) (unit . #(struct:ctor-meta Unit () () () 0)) (zero . #(struct:ctor-meta Nat () () () 0))) #hasheq((Bool . (true false)) (Nat . (zero suc)) (Ordering . (lt-ord eq-ord gt-ord)) (Unit . (unit))) #hasheq() #hasheq(((Posit16 . Posit32) . #t) ((Nat . Int) . #t) ((Posit8 . Posit64) . #t) ((Posit8 . Posit32) . #t) ((Posit32 . Posit64) . #t) ((Nat . Rat) . #t) ((Posit8 . Posit16) . #t) ((Posit16 . Posit64) . #t) ((Int . Rat) . #t)) #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq() #hasheq((add . (x y)) (and . (a b)) (apply . (A B f x)) (bool-eq . (a b)) (bool-to-nat . (b)) (clamp . (low high)) (compose . (B C A g f x)) (const . (A B x _)) (double . (n)) (flip . (A B C f b a)) (ge? . (x y)) (gt? . (x y)) (id . (A x)) (implies . (a b)) (le? . (x y)) (lt? . (x y)) (max . (x y)) (min . (x y)) (mult . (x y)) (nand . (a b)) (nat-eq? . (x y)) (nor . (a b)) (not . (b)) (on . (B C A f g x y)) (or . (a b)) (pow . (base exp)) (pred . (n)) (sub . (x y)) (xor . (a b)) (zero? . (n))) #hasheq() #hasheq() #hasheq()) \ No newline at end of file diff --git a/racket/prologos/macros.rkt b/racket/prologos/macros.rkt index 413deddc8..0ea0f8fc3 100644 --- a/racket/prologos/macros.rkt +++ b/racket/prologos/macros.rkt @@ -4305,10 +4305,25 @@ (cond ;; --- Branch 1: Bracket format — second element is a list --- [(list? (car rest)) - (unless (= (length rest) 2) - (error 'let "let with bracket bindings requires: (let [bindings...] body)")) + ;; The outer "(>= (length datum) 3)" check above guarantees + ;; (length rest) >= 2, so a bare `(let [bindings])` is rejected before + ;; we get here. Branch 1 thus always has a bindings list plus at least + ;; one body token. (define bindings-datum (car rest)) - (define body (cadr rest)) + ;; In WS mode, a multi-line body like + ;; (let [x := 1] + ;; match x | _ -> x) + ;; arrives here as `rest` = `((x := 1) match x $pipe _ -> x)` because + ;; the enclosing `(...)` makes brackets win over indent grouping in + ;; parse-reader's group-items, so the body's continuation tokens are + ;; spliced into the let's argument list. Treat any post-bindings tokens + ;; beyond the first as an implicit body application — matches the usual + ;; "continuation lines are indented further than `let`" rule that + ;; defn/match honour at the top level. + (define body + (cond + [(= (length rest) 2) (cadr rest)] + [else (cdr rest)])) (expand-let-bracket-bindings bindings-datum body)] ;; --- Branch 2: Inline := format — find := in rest --- diff --git a/racket/prologos/tests/test-let-multiline-ws.rkt b/racket/prologos/tests/test-let-multiline-ws.rkt new file mode 100644 index 000000000..6a05335e3 --- /dev/null +++ b/racket/prologos/tests/test-let-multiline-ws.rkt @@ -0,0 +1,120 @@ +#lang racket/base + +;;; +;;; Regression tests for multi-line `let` forms in WS mode. +;;; +;;; Background — the eigentrust pitfalls doc (2026-04-23) #5 reported that +;;; a multi-line `let` like +;;; +;;; (let [x := 1] +;;; match x | _ -> x) +;;; +;;; failed with +;;; +;;; let: let with bracket bindings requires: (let [bindings...] body) +;;; +;;; The bracket form `(let [bindings] body)` is the multi-binding shape; +;;; for a single binding the inline form `(let x := 1 body)` is also +;;; available. The bug surfaces specifically with the bracket form because +;;; that branch was the one that didn't re-group post-bindings tokens. +;;; +;;; Root cause — when the whole let form is wrapped in an explicit `(...)`, +;;; the WS reader's group-items applies its "brackets win" rule and DROPS +;;; the indent-open / indent-close markers around the body. The body's +;;; tokens (`match x | _ -> x`) end up spliced flat into the let's +;;; argument list, so `expand-let` saw `((x := 1) match x ...)` instead of +;;; the expected `((x := 1) )` shape. The bracket-bindings branch +;;; rejected anything other than rest-length 2, hence the error. +;;; +;;; Fix — `expand-let`'s bracket-bindings branch treats any post-bindings +;;; tokens beyond the first as an implicit body application, matching the +;;; usual "continuation lines are indented further than `let`" rule that +;;; defn / match honour at the top level. +;;; + +(require rackunit + "../parse-reader.rkt" + "test-support.rkt") + +;; --- Level 1 (preparse / read) helpers --------------------------------- + +(define (ws-read s) + (define in (open-input-string s)) + (prologos-read in)) + +;; ======================================== +;; Read-level: post-bindings tokens flow through +;; ======================================== + +(test-case "single-line let: unchanged read shape" + (define d (ws-read "(let [x := 1] x)")) + (check-equal? d '(let (x := 1) x))) + +(test-case "let with newline-then-single-token body: unchanged" + (define d (ws-read "(let [x := 1]\n x)")) + (check-equal? d '(let (x := 1) x))) + +(test-case "let with bracket-grouped body: unchanged" + (define d (ws-read "(let [x := 1]\n [add x 1])")) + (check-equal? d '(let (x := 1) (add x 1)))) + +(test-case "let with multi-token continuation body: tokens spliced flat" + ;; This documents the (intentional) parser behavior — `(...)` makes + ;; brackets win over indent grouping, so the body's continuation tokens + ;; arrive flat in `expand-let`'s `rest`. The expand-let branch is + ;; responsible for re-grouping them. + (define d (ws-read "(let [x := 1]\n match x | _ -> x)")) + (check-equal? d '(let (x := 1) match x $pipe _ -> x))) + +;; ======================================== +;; Process-string-ws: end-to-end elaboration +;; ======================================== +;; +;; We call run-ns-ws-last for its side effect of running the WS pipeline +;; (preparse + elaborate + type-check). Returning without raising is the +;; signal that the regression is fixed; the value isn't compared. + +(define (ws-runs? src) + (with-handlers ([exn:fail? (lambda (e) (raise e))]) + (run-ns-ws-last src) + #t)) + +(test-case "single-line let elaborates" + (check-true (ws-runs? "(let [x := 1] x)"))) + +(test-case "multi-line let with simple body elaborates" + (check-true (ws-runs? "(let [x := 1]\n x)"))) + +(test-case "multi-line let with application body elaborates" + (check-true (ws-runs? "(let [x := 1]\n [int+ x 2])"))) + +(test-case "multi-line let with multi-token application body elaborates" + ;; `int+ x 2` arrives flat at expand-let; the fix wraps it as the body. + (check-true (ws-runs? "(let [x := 1]\n int+ x 2)"))) + +(test-case "eigentrust reproducer: multi-line let with nested match body elaborates" + ;; The shape from the eigentrust pitfalls doc #5, scaled down to the + ;; minimum that exercises the same parser path. This is the case that + ;; previously failed with `let: let with bracket bindings requires...`. + (define src + (string-append + "(let [tnew := [int+ 1 2]]\n" + " match [int- tnew 3]\n" + " | -1 -> tnew\n" + " | _ -> [int- tnew 1])\n")) + (check-true (ws-runs? src))) + +(test-case "let with two bindings and multi-token body elaborates" + (define src + (string-append + "(let [x := 1 y := 2]\n" + " int+ x y)\n")) + (check-true (ws-runs? src))) + +;; ======================================== +;; Empty / bare let still raise +;; ======================================== + +(test-case "let with bindings but no body still raises" + (check-exn exn:fail? + (lambda () (run-ns-ws-last "(let [x := 1])"))))