PasteRack.org
Paste # 59065
2017-08-08 22:53:26

Fork as a new paste.

Paste viewed 64 times.


Embed:

strange redex error

  1. #lang racket
  2. (require redex)
  3. (define-language DML
  4.   (var variable-not-otherwise-mentioned)
  5.   ;; Term-level pieces
  6.   (base-val integer boolean)
  7.   (expr var
  8.         op
  9.         base-val
  10.         (expr expr ...)
  11.         (i-app expr idx ...)
  12.         (λ [(var type) ...] expr)
  13.         (Iλ [(var sort) ...] val))
  14.   (op + - * and or not > < = length fold)
  15.   (val var
  16.        op
  17.        base-val
  18.        (λ [(var type) ...] expr)
  19.        (Iλ [(var sort) ...] val))
  20.   ;; Type-level pieces
  21.   (type base-type
  22.         (-> [type ...] type)
  23.         (Π [(var sort) ...] type))
  24.   (base-type Int Bool)
  25.   ;; Index-level pieces
  26.   (idx var
  27.        natural
  28.        {Shp idx ...}
  29.        {+ idx ...}
  30.        {++ idx ...})
  31.   (sort Nat List)  #:binding-forms
  32.   (λ [(var type) ...] val #:refers-to var ...)
  33.   (Π [(var sort) ...] type #:refers-to var ...))
  34.  
  35. (redex-match
  36.    DML
  37.    (Π any Int)
  38.    (term (Π [(l Nat) (s List)]
  39.             Int)))

=>