racket / racket/redex

Contract violation error in complicated binding forms

Open
#233 2 comments 0 reactions 0 assignees View on GitHub

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

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.