suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Removed some Racket code; want this core Redexy

Browse Source
This commit is contained in:
William J. Bowman 2015-10-01 10:30:52 -04:00
parent 5d5ec00052
commit 0ea4c0447b
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 11 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
curnel/redex-core.rkt
View File

@ -159,23 +159,28 @@
(term ())))
;; Get the list of constructors for the inducitvely defined type x_D
;; NB: Depends on clause order
(define-metafunction ttL
Σ-ref-constructors : Σ x -> (x ...) or #f
;; NB: Depends on clause order
[(Σ-ref-constructors ∅ x_D) #f]
[(Σ-ref-constructors (Σ (x_D : t_D ((x : t) ...))) x_D)
(x ...)]
[(Σ-ref-constructors (Σ (x_1 : t_1 any)) x_D)
(Σ-ref-constructors Σ x_D)])
;; NB: Depends on clause order
(define-metafunction ttL
sequence-index-of : any (any ...) -> natural
[(sequence-index-of any_0 (any_0 any ...))
0]
[(sequence-index-of any_0 (any_1 any ...))
,(add1 (term (sequence-index-of any_0 (any ...))))])
;; Get the index of the constructor x_ci in the list of constructors for x_D
(define-metafunction ttL
Σ-constructor-index : Σ x x -> natural or #f
Σ-constructor-index : Σ x x -> natural
[(Σ-constructor-index Σ x_D x_ci)
,(for/fold ([i 0])
([c (term (Σ-ref-constructors Σ x_D))])
#:break (eq? (term x_ci) c)
(add1 i))])
(sequence-index-of x_ci (Σ-ref-constructors Σ x_D))])
;;; ------------------------------------------------------------------------
;;; Universe typing