ffi: marshal Posit8/16/32/64, Int, and List across the Racket FFI#33
Merged
Conversation
The marshalling layer in foreign.rkt previously only handled atomic primitives (Nat, Bool, Unit, Char, String) plus pre-existing Int/Rat support. This commit extends it to: - Posit8/16/32/64: marshal as exact rational (semantic value), encoded via posit*-encode / posit*-to-rational. NaR contamination raises an error since rationals cannot represent NaR. - List <T>: marshal as a recursive cons/nil chain. Recognizes both the bare ((cons head) tail) form produced by foreign.rkt's own builder and the typed (((cons A) head) tail) form produced after elaboration of user code, plus namespace-qualified ::cons / ::nil names. base-type-name now returns either an atomic symbol or a list (List <inner>) for the polymorphic List type. The marshal dispatch uses cond + case so it cleanly handles both shapes. Tests: tests/test-foreign-marshal-ext.rkt (49 unit tests) covers roundtripping for each new type, NaR rejection, nested List (List Int), make-marshaller-pair end-to-end behaviour, and parse-foreign-type recognition of the new types in arrow positions.
Adds 14 end-to-end test cases to test-foreign.rkt that exercise the new marshallers through the full elaborator + reduction pipeline (the unit tests in test-foreign-marshal-ext.rkt only cover the marshal layer in isolation): - Int: add1, +, -, * with negatives and bignums. - Posit8/16/32/64: arithmetic round-trip with bit-pattern literals; Posit64 verified via type inference. - List: passing (List Int) / (List Nat) to Racket's `length`, `reverse`, and `list` constructor; tests cover empty lists, list-returning Racket calls, and round-trips through `reverse`. Tests that need List in scope use a `(ns t-foreign-list)` prefix so the prelude auto-imports the data::list module. Verified with the targeted- test runner: tests/test-foreign-marshal-ext.rkt + tests/test-foreign.rkt + tests/test-foreign-block.rkt all pass on Racket v9.1 (114 tests / 8s).
Run artifacts produced by tools/run-affected-tests.rkt while validating the FFI Posit/Int/List work against the locally-built Racket v9.1 host: - timings.jsonl: appends one entry for the targeted-test run (114 tests, 8.2s) - last-run-summary.txt: refreshed pointer to the same run - nat.pnet: cache rebuilt by the prelude reload under the new Racket version Pure artifact churn — no code changes.
kumavis
commented
Apr 28, 2026
Run-artifact diff isn't relevant to the FFI work — restore the file to its origin/main state so the PR shows only the FFI implementation + tests + the timings.jsonl entry. A follow-up PR will gitignore last-run-summary.txt entirely so this churn stops appearing on every branch.
There was a problem hiding this comment.
Pull request overview
Extends the Prologos↔Racket FFI marshalling layer to support additional numeric types (Int and Posit widths) and polymorphic List<T>, with accompanying unit and integration tests to validate roundtrips and type parsing.
Changes:
- Added marshalling support for
Posit8/16/32/64(as exact rationals) andList<T>(as cons/nil chains). - Updated type parsing so
base-type-namecan return a compound descriptor for(List <inner>). - Added a new unit test file for the extended marshalling surface and expanded the existing foreign integration tests.
Reviewed changes
Copilot reviewed 4 out of 5 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| racket/prologos/foreign.rkt | Implements Posit and List marshalling and updates base-type parsing/dispatch. |
| racket/prologos/tests/test-foreign.rkt | Adds elaborator-level integration tests covering Int/Posit/List foreign calls. |
| racket/prologos/tests/test-foreign-marshal-ext.rkt | New unit tests covering marshal-in/out, NaR rejection, List forms, and type parsing. |
| racket/prologos/data/cache/pnet/prologos/data/nat.pnet | Regenerated .pnet cache artifact included in the diff. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+178
to
+181
| [(Char) (char->rkt-char val)] | ||
| [(String) (string->rkt-string val)] | ||
| [(Posit8 Posit16 Posit32 Posit64) (posit->rational val)] | ||
| ;; Passthrough types: the Prologos IR value IS the Racket value |
There was a problem hiding this comment.
marshal-prologos->racket treats all Posit widths the same by calling posit->rational, so a Posit8-typed position will also accept an expr-posit16/32/64 (and vice versa). That silently defeats the width distinction and can hide type mismatches/precision issues. Consider dispatching per Posit type and rejecting mismatched IR constructors (e.g., Posit8 should only accept expr-posit8?).
| @@ -1 +1 @@ | |||
| (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 "<unknown>" 0 0 0) () () #f #f)) (apply . #(struct:spec-entry (((A -> B) A -> B)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (bool-to-nat . #(struct:spec-entry ((Bool -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (clamp . #(struct:spec-entry ((Nat Nat -> Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (compose . #(struct:spec-entry (((B -> C) (A -> B) A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (double . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (flip . #(struct:spec-entry (((A -> B -> C) B A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () () #f #f)) (gt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (id . #(struct:spec-entry ((A -> A)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () ((A Type 0)) #f #f)) (le? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (lt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (max . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (min . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (mult . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (nat-eq? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (on . #(struct:spec-entry (((B -> B -> C) (A -> B) A A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () () #f #f)) (pred . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (sub . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (zero? . #(struct:spec-entry ((Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 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 | |||
| (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 "<unknown>" 0 0 0) () () #f #f)) (apply . #(struct:spec-entry (((A -> B) A -> B)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (bool-to-nat . #(struct:spec-entry ((Bool -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (clamp . #(struct:spec-entry ((Nat Nat -> Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (compose . #(struct:spec-entry (((B -> C) (A -> B) A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (double . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (flip . #(struct:spec-entry (((A -> B -> C) B A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () () #f #f)) (gt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (id . #(struct:spec-entry ((A -> A)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () ((A Type 0)) #f #f)) (le? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (lt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (max . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (min . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (mult . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (nat-eq? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (on . #(struct:spec-entry (((B -> B -> C) (A -> B) A A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () () #f #f)) (pred . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (sub . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (zero? . #(struct:spec-entry ((Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 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(((Nat . Int) . #t) ((Posit8 . Posit64) . #t) ((Posit8 . Posit32) . #t) ((Posit32 . Posit64) . #t) ((Nat . Rat) . #t) ((Posit8 . Posit16) . #t) ((Posit16 . Posit64) . #t) ((Int . Rat) . #t) ((Posit16 . 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 | |||
There was a problem hiding this comment.
This .pnet cache file change appears to be a regenerated artifact (includes machine-local absolute paths and nondeterministic hasheq ordering). Since it’s unrelated to the FFI marshalling changes and likely to cause noisy diffs/merge conflicts, it should usually be reverted and kept out of the PR unless the cache is intentionally being updated as part of a controlled regeneration step.
Suggested change
| (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 "<unknown>" 0 0 0) () () #f #f)) (apply . #(struct:spec-entry (((A -> B) A -> B)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (bool-to-nat . #(struct:spec-entry ((Bool -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (clamp . #(struct:spec-entry ((Nat Nat -> Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (compose . #(struct:spec-entry (((B -> C) (A -> B) A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () ((A Type 0) (B Type 0)) #f #f)) (double . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (flip . #(struct:spec-entry (((A -> B -> C) B A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () () #f #f)) (gt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (id . #(struct:spec-entry ((A -> A)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () ((A Type 0)) #f #f)) (le? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (lt? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (max . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (min . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (mult . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (nat-eq? . #(struct:spec-entry ((Nat Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (on . #(struct:spec-entry (((B -> B -> C) (A -> B) A A -> C)) #f #f #(struct:srcloc "<unknown>" 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 "<unknown>" 0 0 0) () () #f #f)) (pred . #(struct:spec-entry ((Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (sub . #(struct:spec-entry ((Nat Nat -> Nat)) #f #f #(struct:srcloc "<unknown>" 0 0 0) () () #f #f)) (zero? . #(struct:spec-entry ((Nat -> Bool)) #f #f #(struct:srcloc "<unknown>" 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(((Nat . Int) . #t) ((Posit8 . Posit64) . #t) ((Posit8 . Posit32) . #t) ((Posit32 . Posit64) . #t) ((Nat . Rat) . #t) ((Posit8 . Posit16) . #t) ((Posit16 . Posit64) . #t) ((Int . Rat) . #t) ((Posit16 . 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()) |
Per copilot review on PR #33: this .pnet file is regenerated on every prelude load and contains machine-local absolute paths and nondeterministic hasheq ordering. Unrelated to the FFI work — restore to origin/main. If the cache content needs to be refreshed it should land in a controlled regeneration commit, not as drive-by churn from a Racket-version bump.
Per copilot review on PR #33: marshal-prologos->racket previously routed all Posit widths through a single posit->rational helper that inferred the width from the IR struct itself. As a result, a `Posit8`-typed foreign argument would silently accept an `expr-posit16` (and vice versa), defeating the width distinction and hiding precision/range mismatches. Fix: split into per-width converters (posit8->rational, posit16->rational, posit32->rational, posit64->rational), each of which only matches its own expr-posit*. The marshal-prologos->racket dispatch now picks the converter based on the *declared* type, so the IR width must agree. The width-dispatching wrapper posit->rational is retained as a public API but now takes the declared width as an argument. Tests: 4 new cases in test-foreign-marshal-ext.rkt assert that: - each declared Posit width rejects IR of every other width (12 cases) - per-width converters reject mismatched IR (4 cases) - the wrapper posit->rational accepts the declared width and rejects mismatches Existing coverage unchanged. 52 unit + 52 integration tests pass on Racket v9.1.
hierophantos
approved these changes
Apr 28, 2026
Contributor
hierophantos
left a comment
hierophantos
left a comment
There was a problem hiding this comment.
Approving. Substantive but well-scoped extension to foreign.rkt's marshaling layer:
- Posit8/16/32/64 ↔ exact rational with width-mismatch rejection and NaR contamination raising explicit errors (rather than silent corruption — the right call for a precision-sensitive type)
- List
<T>recursive cons/nil chain marshaling, handling both 2-arg(cons head tail)and 3-arg(cons A head tail)forms with namespace-qualified::cons/::nilrecognition
Audit-confirmed independently:
posit-impl.rktexports all neededposit*-to-rationalfunctionsbase-type-name's return-shape change (symbol → symbol-or-(List <inner>)) is contained — no external callers, only 2 internal inparse-foreign-typeitself- 145 LoC test-foreign.rkt diff is purely additive (14 new integration tests); 389 LoC test-foreign-marshal-ext.rkt is a new file (49 unit tests)
- 63 new tests covering happy path + width mismatch + NaR rejection + nested List + bignum roundtrip + integration through elaborator
Honest disclosure points (NaR rejection, width-mismatch errors) are exactly the kind of "fail loudly at the boundary" behavior an FFI marshaler should have.
Aware of the related FFI series (#32 EigenTrust example, #35 closures across FFI, #36 ZK research) — happy to look at those next as the foundation here lands.
hierophantos
added a commit
that referenced
this pull request
Apr 28, 2026
Three artifacts establishing FFI as a tracked Series: 1. docs/tracking/2026-04-28_FFI_MASTER.md (NEW) — FFI Series Master doc following established pattern (PM/SRE/BSP-LE/CIU/PPN). Polyglot-hub thesis, cross-series connections, progress tracker with Tracks 0-3 + future placeholders, design discipline, key invariants. 2. Issue #37 — "FFI: retire lambda-passing scaffolding via propagator-native callbacks (cell subscription)" — captures retirement direction from PR #35's design doc as a permanent tracked obligation. Names design questions deferred to phase-time mini-design. 3. MASTER_ROADMAP.org — added FFI Series entry between PReductions and Completed Standalone Tracks. Status: Track 0 ✅ pre-existing, Track 1 ✅ landed (PR #33 9ef3420), Track 2 🔄 pending merge (PR #35 awaiting lift-from-draft), Track 3 ⬜ tracked as #37. Forward vision: Prologos as polyglot hub. Each FFI track integrates with propagator-network discipline rather than bolting on parallel off-network bridges; pragmatic scaffolding when needed gets named and retirement-tracked (Track 3 / #37 is the canonical example). Dailies entry under "FFI Series started + retirement issue filed" captures the work + three lessons distilled (off-network-with- retirement-direction discipline, track-series-as-permanent-home for evolving infrastructure, external contributor work surfacing architectural opportunities).
5 tasks
kumavis
pushed a commit
that referenced
this pull request
May 6, 2026
…or spec-level resolution Companion to pitfall #32 / issue #60. Discovered during OCapN Phase 25.4 (commit f633e5a) while wiring verify-questioner-reply in bridge-interop-helpers.prologos. When module M3 :refer-all's M2, which :refer-all's M1 (defining type T), M3's function specs mentioning T fail to type-check against function calls returning T from M1: the spec's unqualified `T` and the body's fully-qualified `prologos::M1::T` are treated as different types by the elaborator, even though they reference the same definition. Type mismatch expected: [Pi [x BridgeStep] [Pi [y Nat] [Option PromiseState]]] got: [Pi [x BridgeStep] [Pi [y Nat] [Option prologos::ocapn::promise::PromiseState]]] Workaround: add an explicit `:refer [TypeName ...]` import in M3 (even though :refer-all transitively re-exports it). Cost: one line per affected module per affected type. Frequency in OCapN work: hit once in Phase 25.4 (PromiseState in bridge-interop-helpers). Lower impact than #60 because the workaround is mechanical (add the explicit refer line), but worth tracking because: 1. The error message looks like a tautology ("T != T") at first glance; needs careful reading to see the qualifier. 2. :refer-all chains are common in Prologos library modules. 3. Fixing it would make :refer-all behave as users expect. To be filed as a separate issue from #60 — different symptom, different mechanism, different fix surface.
kumavis
pushed a commit
that referenced
this pull request
May 6, 2026
kumavis
pushed a commit
that referenced
this pull request
May 6, 2026
…weak refs deferred
Plans Phases 31-34 of OCapN: distributed reference counting via
op:gc-export and op:gc-answer messages.
Key insight: CapTP GC is a protocol (explicit refcount-decrement
messages over the wire), NOT a host-language collection algorithm.
Weakmaps and finalization are NOT required for protocol correctness
— they're an ergonomic layer for automatic detection of "user
dropped this Refr" that would otherwise need explicit release calls.
Recommended phasing:
Phase 31 — Refcount tables in BridgeState
Two new fields: exports-refcount + imports-refcount.
Plain (Nat -> Nat) maps. Mechanical field additions.
Phase 32 — Outbound release-* API + wire bytes
User-facing release-import + release-answer on
ConnectionState. Returns ConnRelease(cs', bytes-list).
Manual call from user code.
Phase 33 — Inbound op:gc-* dispatch
Replace current "append to audit log" no-op arms with
real refcount-decrement + answer-table cleanup.
Phase 34 — DEFERRED: automatic release via Racket weak hash + finalizer
Hooks host-language GC. Layering on top of manual.
Estimate: ~half a day for Phases 31-33; Phase 34 is 1-2 days
when/if automatic release becomes worth the complexity.
Doc covers:
- What we already have (wire codec + audit-log dispatch)
- What's missing (refcount semantics, outbound API, real inbound dispatch)
- Why manual first (testability, deterministic failure modes, clean layering)
- Outbound timing (user signals completion, bridge doesn't unilaterally decide)
- Open questions for the implementation phase
- Risk summary against pitfalls #18, #32 (#60), #33 (#61)
No code changes — purely planning. Implementation comes when this
work is prioritized.
kumavis
pushed a commit
that referenced
this pull request
May 6, 2026
Adds refr-kind-remote-import-object, smart constructor refr-remote-import-object, predicate refr-remote-import-object?, and wire-shape support both directions: decode: <desc:import-object N> → refr-remote-import-object N encode: refr-remote-import-object N → <desc:import-object N> extract-refrs-from-tagged factored via dispatch-non-export-tag helper to avoid 3-deep nested match (pitfall #18 / #33). refr-to-syrup now uses a refr-syrup-tag dispatcher returning the desc:* tag name, then a single syrup-tagged construction. Phase 0 minimal scope: import-object refrs are recognized and round-trip on the wire; bs-incr-import-by-refr is unchanged so they do NOT auto-increment imports-refcount (the OCapN three-vat handoff GC story uses op:withdraw-gift and is deferred). Test "desc:import-object does NOT auto-increment imports-refcount" pins this design choice. Tests: +7 in test-ocapn-bridge.rkt (79 → 86 passing). Full OCapN unit suite (174 tests across 7 files) green.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The marshalling layer in foreign.rkt previously only handled atomic
primitives (Nat, Bool, Unit, Char, String) plus pre-existing Int/Rat
support. This commit extends it to:
via posit*-encode / posit*-to-rational. NaR contamination raises an
error since rationals cannot represent NaR.
bare ((cons head) tail) form produced by foreign.rkt's own builder
and the typed (((cons A) head) tail) form produced after elaboration
of user code, plus namespace-qualified ::cons / ::nil names.
base-type-name now returns either an atomic symbol or a list
(List ) for the polymorphic List type. The marshal dispatch
uses cond + case so it cleanly handles both shapes.
Tests: tests/test-foreign-marshal-ext.rkt (49 unit tests) covers
roundtripping for each new type, NaR rejection, nested List (List Int),
make-marshaller-pair end-to-end behaviour, and parse-foreign-type
recognition of the new types in arrow positions.