Skip to content

ffi: marshal Posit8/16/32/64, Int, and List across the Racket FFI #33

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hierophantos merged 6 commits into from
Apr 28, 2026
Merged

ffi: marshal Posit8/16/32/64, Int, and List across the Racket FFI #33

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b9a6461
ffi: marshal Posit8/16/32/64, Int, and List across the Racket FFI
claude Apr 28, 2026
a4c2004
ffi/tests: integration tests for Int / Posit / List foreign types
claude Apr 28, 2026
e29f89b
chore: refresh benchmark + .pnet cache artifacts from Racket 9.1 run
claude Apr 28, 2026
c9d9917
chore: drop last-run-summary.txt churn from this PR
claude Apr 28, 2026
e65551e
chore: drop nat.pnet cache artifact from this PR
claude Apr 28, 2026
ff6540b
ffi: strict per-width Posit marshal-in dispatch
claude Apr 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions racket/prologos/data/benchmarks/timings.jsonl
View file
Open in desktop

Large diffs are not rendered by default.

276 changes: 231 additions & 45 deletions racket/prologos/foreign.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,22 +5,37 @@
;;; Converts between Prologos values (Church/Peano encoded) and Racket values.
;;;
;;; Supported base types:
;;; Nat ↔ exact non-negative integer
;;; Bool ↔ boolean
;;; Unit ↔ void
;;; Char ↔ char
;;; String ↔ string
;;; Nat ↔ exact non-negative integer
;;; Int ↔ exact integer
;;; Rat ↔ exact rational
;;; Bool ↔ boolean
;;; Unit ↔ void
;;; Char ↔ char
;;; String ↔ string
;;; Posit8/16/32/64 ↔ exact rational (semantic value; NaR raises an error)
;;; List <T> ↔ list of marshalled elements (recursive in T)
;;;

(require racket/match
racket/string
"syntax.rkt")
"syntax.rkt"
"posit-impl.rkt")

(provide marshal-prologos->racket
marshal-racket->prologos
nat->integer
integer->nat
bool->boolean
int->integer
integer->int
posit->rational
posit8->rational
posit16->rational
posit32->rational
posit64->rational
rational->posit
prologos-list->racket-list
racket-list->prologos-list
parse-foreign-type
make-marshaller-pair
base-type-name)
Expand Down Expand Up @@ -70,22 +85,140 @@
[(expr-string v) v]
[_ (error 'foreign "Cannot marshal to string — not a String literal: ~a" e)]))

;; Per-width Prologos Posit → Racket exact rational converters. Each rejects
;; mismatched IR widths so a `Posit8`-typed slot won't silently accept an
;; `expr-posit16` (and vice versa). NaR contamination raises an error since
;; rationals cannot represent NaR.
(define (posit8->rational e)
(match e
[(expr-posit8 v)
(let ([r (posit8-to-rational v)])
(when (eq? r 'nar) (error 'foreign "Cannot marshal Posit8 NaR to rational"))
r)]
[_ (error 'foreign "Cannot marshal to rational — not a Posit8 literal: ~a" e)]))

(define (posit16->rational e)
(match e
[(expr-posit16 v)
(let ([r (posit16-to-rational v)])
(when (eq? r 'nar) (error 'foreign "Cannot marshal Posit16 NaR to rational"))
r)]
[_ (error 'foreign "Cannot marshal to rational — not a Posit16 literal: ~a" e)]))

(define (posit32->rational e)
(match e
[(expr-posit32 v)
(let ([r (posit32-to-rational v)])
(when (eq? r 'nar) (error 'foreign "Cannot marshal Posit32 NaR to rational"))
r)]
[_ (error 'foreign "Cannot marshal to rational — not a Posit32 literal: ~a" e)]))

(define (posit64->rational e)
(match e
[(expr-posit64 v)
(let ([r (posit64-to-rational v)])
(when (eq? r 'nar) (error 'foreign "Cannot marshal Posit64 NaR to rational"))
r)]
[_ (error 'foreign "Cannot marshal to rational — not a Posit64 literal: ~a" e)]))

;; Width-dispatching wrapper: caller passes the declared Posit width.
(define (posit->rational width e)
(case width
[(8) (posit8->rational e)]
[(16) (posit16->rational e)]
[(32) (posit32->rational e)]
[(64) (posit64->rational e)]
[else (error 'foreign "Unknown Posit width: ~a" width)]))

;; Helpers: recognize cons/nil names regardless of namespace qualification.
(define (list-cons-name? name)
(and (symbol? name)
(let ([s (symbol->string name)])
(or (string=? s "cons")
(let ([len (string-length s)])
(and (>= len 6)
(string=? (substring s (- len 6)) "::cons")))))))

(define (list-nil-name? name)
(and (symbol? name)
(let ([s (symbol->string name)])
(or (string=? s "nil")
(let ([len (string-length s)])
(and (>= len 5)
(string=? (substring s (- len 5)) "::nil")))))))

;; Walk a Prologos List value (cons/nil chain) into a Racket list of element exprs.
;; Recognizes both forms:
;; - (cons head tail) — 2-arg form, no type argument
;; - (cons A head tail) — 3-arg form with implicit type argument
;; - nil / (expr-nil) — bare nil
;; - (nil A) — nil applied to type argument
;; Errors on a stuck or non-list expression.
(define (prologos-list->racket-list e)
(let loop ([cur e] [acc '()])
(cond
;; (expr-nil) — built-in nil node
[(expr-nil? cur)
(reverse acc)]
;; bare 'nil / qualified ::nil fvar
[(and (expr-fvar? cur) (list-nil-name? (expr-fvar-name cur)))
(reverse acc)]
;; (nil A) — nil with type argument
[(and (expr-app? cur)
(let ([f (expr-app-func cur)])
(and (expr-fvar? f) (list-nil-name? (expr-fvar-name f)))))
(reverse acc)]
;; cons applications: 2-arg ((cons head) tail) or 3-arg (((cons A) head) tail)
[(expr-app? cur)
(define head-app (expr-app-func cur))
(define tail (expr-app-arg cur))
(cond
;; ((cons head) tail) — 2-arg
[(and (expr-app? head-app)
(let ([f (expr-app-func head-app)])
(and (expr-fvar? f) (list-cons-name? (expr-fvar-name f)))))
(loop tail (cons (expr-app-arg head-app) acc))]
;; (((cons A) head) tail) — 3-arg with type
[(and (expr-app? head-app)
(expr-app? (expr-app-func head-app))
(let ([f (expr-app-func (expr-app-func head-app))])
(and (expr-fvar? f) (list-cons-name? (expr-fvar-name f)))))
(loop tail (cons (expr-app-arg head-app) acc))]
[else
(error 'foreign "Cannot marshal to list — not a cons/nil chain: ~a" e)])]
[else
(error 'foreign "Cannot marshal to list — not a cons/nil chain: ~a" e)])))

(define (marshal-prologos->racket base-type val)
(case base-type
[(Nat) (nat->integer val)]
[(Int) (int->integer val)]
[(Rat) (rat->rational val)]
[(Bool) (bool->boolean val)]
[(Unit) (void)]
[(Char) (char->rkt-char val)]
[(String) (string->rkt-string val)]
;; Passthrough types: the Prologos IR value IS the Racket value
[(Path Keyword Passthrough) val]
(cond
;; Compound List type: (List <inner>)
[(and (pair? base-type) (eq? (car base-type) 'List))
(define inner (cadr base-type))
(map (lambda (e) (marshal-prologos->racket inner e))
(prologos-list->racket-list val))]
;; Atomic types
[(symbol? base-type)
(case base-type
[(Nat) (nat->integer val)]
[(Int) (int->integer val)]
[(Rat) (rat->rational val)]
[(Bool) (bool->boolean val)]
[(Unit) (void)]
[(Char) (char->rkt-char val)]
[(String) (string->rkt-string val)]
[(Posit8) (posit8->rational val)]
[(Posit16) (posit16->rational val)]
[(Posit32) (posit32->rational val)]
[(Posit64) (posit64->rational val)]
;; Passthrough types: the Prologos IR value IS the Racket value
Comment on lines +207 to +213

Copilot AI Apr 28, 2026

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?).

Copilot uses AI. Check for mistakes.
[(Path Keyword Passthrough) val]
[else
(define type-str (symbol->string base-type))
(if (string-prefix? type-str "Opaque:")
(if (expr-opaque? val) (expr-opaque-value val) val)
(error 'foreign "Unsupported marshal-in type: ~a" base-type))])]
[else
(define type-str (symbol->string base-type))
(if (string-prefix? type-str "Opaque:")
(if (expr-opaque? val) (expr-opaque-value val) val)
(error 'foreign "Unsupported marshal-in type: ~a" base-type))]))
(error 'foreign "Unsupported marshal-in type: ~a" base-type)]))

;; ========================================
;; Racket → Prologos marshalling
Expand All @@ -110,45 +243,98 @@
(error 'foreign "Cannot marshal from Racket: expected exact rational, got ~a" n))
(expr-rat n))

;; Convert a Racket exact rational (or integer) to a Prologos Posit literal of the given width.
(define (rational->posit width n)
(unless (or (exact-integer? n) (and (exact? n) (rational? n)))
(error 'foreign
"Cannot marshal to Posit~a: expected exact integer or rational, got ~a"
width n))
(case width
[(8) (expr-posit8 (posit8-encode n))]
[(16) (expr-posit16 (posit16-encode n))]
[(32) (expr-posit32 (posit32-encode n))]
[(64) (expr-posit64 (posit64-encode n))]
[else (error 'foreign "Unknown Posit width: ~a" width)]))

;; Build a Prologos List value from a Racket list of element exprs.
;; Uses the bare 'cons / (expr-nil) form (no implicit type argument), which the
;; reducer/elaborator accepts and pretty-printer recognizes.
(define (racket-list->prologos-list elems)
(foldr (lambda (e acc)
(expr-app (expr-app (expr-fvar 'cons) e) acc))
(expr-nil)
elems))

(define (marshal-racket->prologos base-type val)
(case base-type
[(Nat) (integer->nat val)]
[(Int) (integer->int val)]
[(Rat) (rational->rat val)]
[(Bool) (if val (expr-true) (expr-false))]
[(Unit) (expr-unit)]
[(Char) (expr-char val)]
[(String) (expr-string val)]
;; Passthrough types: result is already a Prologos IR value
[(Path Keyword Passthrough) val]
(cond
;; Compound List type: (List <inner>)
[(and (pair? base-type) (eq? (car base-type) 'List))
(define inner (cadr base-type))
(unless (list? val)
(error 'foreign "Cannot marshal to List — expected Racket list, got ~a" val))
(racket-list->prologos-list
(map (lambda (e) (marshal-racket->prologos inner e)) val))]
;; Atomic types
[(symbol? base-type)
(case base-type
[(Nat) (integer->nat val)]
[(Int) (integer->int val)]
[(Rat) (rational->rat val)]
[(Bool) (if val (expr-true) (expr-false))]
[(Unit) (expr-unit)]
[(Char) (expr-char val)]
[(String) (expr-string val)]
[(Posit8) (rational->posit 8 val)]
[(Posit16) (rational->posit 16 val)]
[(Posit32) (rational->posit 32 val)]
[(Posit64) (rational->posit 64 val)]
;; Passthrough types: result is already a Prologos IR value
[(Path Keyword Passthrough) val]
[else
(define type-str (symbol->string base-type))
(if (string-prefix? type-str "Opaque:")
(expr-opaque val (string->symbol (substring type-str 7)))
(error 'foreign "Unsupported marshal-out type: ~a" base-type))])]
[else
(define type-str (symbol->string base-type))
(if (string-prefix? type-str "Opaque:")
(expr-opaque val (string->symbol (substring type-str 7)))
(error 'foreign "Unsupported marshal-out type: ~a" base-type))]))
(error 'foreign "Unsupported marshal-out type: ~a" base-type)]))

;; ========================================
;; Type parsing for marshalling
;; ========================================

;; Extract base type symbol from a core type expression.
;; Returns one of: 'Nat, 'Bool, 'Unit, 'Posit8
;; Extract base type descriptor from a core type expression.
;; Returns either:
;; - a symbol for atomic types: 'Nat, 'Int, 'Rat, 'Bool, 'Unit, 'Char, 'String,
;; 'Posit8, 'Posit16, 'Posit32, 'Posit64, 'Path, 'Keyword, 'Passthrough,
;; 'Opaque:<tag>
;; - a list (List <inner>) for the polymorphic List type, where <inner> is
;; itself a base-type descriptor (atomic or nested List).
(define (base-type-name e)
(match e
[(expr-Nat) 'Nat]
[(expr-Bool) 'Bool]
[(expr-Unit) 'Unit]
[(expr-Posit8) 'Posit8]
[(expr-Nat) 'Nat]
[(expr-Bool) 'Bool]
[(expr-Unit) 'Unit]
[(expr-Posit8) 'Posit8]
[(expr-Posit16) 'Posit16]
[(expr-Posit32) 'Posit32]
[(expr-Posit64) 'Posit64]
[(expr-Int) 'Int]
[(expr-Rat) 'Rat]
[(expr-Char) 'Char]
[(expr-String) 'String]
[(expr-Int) 'Int]
[(expr-Rat) 'Rat]
[(expr-Char) 'Char]
[(expr-String) 'String]
;; Passthrough types: Path, Keyword — Racket functions operate on IR values directly
[(expr-Path) 'Path]
[(expr-Path) 'Path]
[(expr-Keyword) 'Keyword]
;; (List A) — recognize bare and namespace-qualified List names
[(expr-app (? (lambda (f)
(and (expr-fvar? f)
(let* ([n (symbol->string (expr-fvar-name f))]
[len (string-length n)])
(or (string=? n "List")
(and (>= len 6)
(string=? (substring n (- len 6)) "::List")))))))
inner)
(list 'List (base-type-name inner))]
;; Any other type: passthrough (the Racket function handles IR values directly)
[_ 'Passthrough]))

Expand Down
Loading
Loading