Contract violation error in complicated binding forms
Nobody has claimed this yet.
- Dominant language
- Racket
- Stars
- 112
- Forks
- 42
- PR merge metrics
- No merged PRs in 30d
Description
I was trying to specify a language that has a sort of rudimentary module system. The idea is that a module consists of 0 or more imports (which are themselves modules), 0 or more definitions, and an expression. The names defined in the definitions are exported to clients of the module.
While working on this, I managed to trigger a contract violation error from substitution. Here's a cut-down version of what I was writing:
#lang racket
(require redex)
(define-language L
(x variable-not-otherwise-mentioned)
(e number x)
(decl (define x e) (define-const x number))
(imports (import prog ...))
(prog (unit
imports
decl ...
e))
#:binding-forms
(define x e) #:exports x
(define-const x number) #:exports x
(import prog_imports
#:...bind (imported-vars prog_imports (shadow imported-vars prog_imports))) #:exports imported-vars
(unit imports_libs decl_def #:...bind (defined-vars decl_def (shadow defined-vars decl_def)) e #:refers-to (shadow imports_libs defined-vars ...))
)
(define test-program
(term (unit (import) (define-const x 1) (define y x) y)))
(term (substitute ,test-program y 444) #:lang L)
yields
; map: contract violation
; expected: list?
; given: (term-and-table '((define-const x«1» 1) ((define y«0» x«1») ())) '((y y«0») (x x«1»)))
; Context (plain; to see better errortrace context, re-run with C-u prefix):
; /home/dtc/racket/collects/racket/private/map.rkt:257:2 gen-map
; .../private/map.rkt:40:19 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:334:0 pass-...
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:438:2 interp-betas
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:661:0 rec-freshen-spec
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:165:0 safe-subst
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1550:37
; .../private/map.rkt:40:19 loop
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1843:16 metafunc
; /home/dtc/racket/share/pkgs/redex-lib/redex/private/term.rkt:80:18
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by running the cut-down reproduction in issue #233 and compare the failure with redex/private/binding-forms.rkt, especially pass-... and interp-betas, using the reported stack trace as a guide. The work is done when this binding form no longer triggers a map contract violation during substitution and the example produces the expected substitution result.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100