Last active
January 7, 2018 00:42
-
-
Save iitalics/5f1291f78ac0ef498d6b41a1aeffd31d to your computer and use it in GitHub Desktop.
More sophisticated lazy language with pattern matching & eval interleaved
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket/base | |
(require redex) | |
(define-language Haskill | |
[x ::= variable-not-otherwise-mentioned] | |
[ctor ::= cons null A B C #t #f] | |
; expressions | |
[e ::= | |
x | |
ctor | |
(e e ...) | |
(fix (x) e) | |
(λ (p ...) e) | |
(case e [p e] ...) | |
(match m e e) ; note: used internally, not "surface syntax" | |
undefined] | |
[v ::= | |
ctor | |
(ctor e ...) | |
(λ (p ...) e)] | |
; patterns | |
[p ::= x ctor (ctor p ...)] | |
[vp ::= ctor (ctor p ...)] | |
; matching terms | |
[m ::= | |
[p = e] | |
(and m ...) | |
(ok Σ) | |
(fail)] | |
[Σ ::= ([x e] ...)] | |
; expression reduction context | |
[E ::= | |
(match (in-hole M [vp = E]) e e) | |
(E e ...) | |
hole] | |
; match reduction context | |
[M ::= | |
(and (ok Σ) ... M m ...) | |
hole] | |
; M inside E | |
[EM ::= (in-hole E (match M e e))]) | |
(define-metafunction Haskill | |
app* : (Σ ...) -> Σ | |
[(app* (([x_i e_i] ...) ...)) ([x_i e_i] ... ...)]) | |
(define-metafunction Haskill | |
subst* : Σ e -> e | |
[(subst* () e) e] | |
[(subst* ([x_1 e_1] [x_i e_i] ...) e) | |
(subst* ([x_i e_i] ...) (substitute e x_1 e_1))]) | |
(define-metafunction Haskill | |
split : vp v -> ([p e] ...) or #f | |
[(split ctor_1 ctor_1) ()] | |
[(split (ctor_1 p_i ..._n) (ctor_1 e_i ..._n)) ([p_i e_i] ...)] | |
[(split _ _) #f]) | |
(define rr | |
(reduction-relation Haskill | |
#:domain e | |
;; evaluation | |
(--> (in-hole E (fix (x) e)) | |
(in-hole E (substitute e x (fix (x) e))) | |
"E-fix") | |
(--> (in-hole E ((λ (p_i ..._n) e) e_i ..._n)) | |
(in-hole E (match (and [p_i = e_i] ...) e undefined)) | |
"E-beta") | |
(--> (in-hole E (case e [p_1 e_1] [p_i e_i] ...)) | |
(in-hole E (match [p_1 = e] e_1 (case e [p_i e_i] ...))) | |
"E-case") | |
(--> (in-hole E (case e)) | |
(in-hole E undefined) | |
"E-case-mt") | |
(--> (in-hole E (match (ok Σ) e_1 e_2)) | |
(in-hole E (subst* Σ e_1)) | |
"E-ok") | |
(--> (in-hole E (match (fail) e_1 e_2)) | |
(in-hole E e_2) | |
"E-fail") | |
;; pattern matching | |
(--> (in-hole EM [x = e]) | |
(in-hole EM (ok ([x e]))) | |
"M-bind") | |
(--> (in-hole EM [vp = v]) | |
(in-hole EM (and [p_i = e_i] ...)) | |
"M-split" | |
(where ([p_i e_i] ...) (split vp v))) | |
(--> (in-hole EM [vp = v]) | |
(in-hole EM (fail)) | |
"M-fail" | |
(where #f (split vp v))) | |
(--> (in-hole EM (and (ok Σ_i) ...)) | |
(in-hole EM (ok (app* (Σ_i ...)))) | |
"M-ok*") | |
(--> (in-hole EM (and (ok Σ_i) ... (fail) m ...)) | |
(in-hole EM (fail)) | |
"M-fail*") | |
)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment