PasteRack.org
Paste # 16641
2017-08-08 22:52:19

Fork as a new paste.

Paste viewed 59 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.   ;; Add more primops as they are needed.
  15.   ;; TODO: how to handle curried primops?
  16.   (op + - * and or not > < = length fold)
  17.   (val var
  18.        op
  19.        base-val
  20.        (λ [(var type) ...] expr)
  21.        (Iλ [(var sort) ...] val))
  22.   ;; Type-level pieces
  23.   (type base-type
  24.         (-> [type ...] type)
  25.         (Π [(var sort) ...] type))
  26.   (base-type Int Bool)
  27.   ;; Index-level pieces
  28.   ;; Delimiting indices with {} is convention, not enforced by Racket/Redex.
  29.   (idx var
  30.        natural
  31.        {Shp idx ...}
  32.        {+ idx ...}
  33.        {++ idx ...})
  34.   (sort Nat List)  #:binding-forms
  35.   (λ [(var type) ...] val #:refers-to var ...)
  36.   (Π [(var sort) ...] type #:refers-to var ...))
  37.  
  38. (redex-match
  39.    DML
  40.    (Π any type)
  41.    (term (Π [(l Nat) (s List)]
  42.             Int)))

=>