e.rkt (1621B)
1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang 2 3 @; This file is NOT under the CC0 license, as it contains rules and definitions 4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the 5 @; permission to copy these rules, but did not ask for a relicensing under the 6 @; CC0 license. 7 8 @cases["e" #:first-sep "⩴" 9 @acase{x @P y @P z@tag*{variable}} 10 @acase{@num-e @tag*{number}} 11 @acase{@true-e @tag*{booleans}} 12 @acase{@false-e} 13 @acase{@null-e @tag*{null constant}} 14 @acase{@primop @tag*{primitive functions}} 15 @acase{@app[e @repeated{e}] @tag*{function application}} 16 @acase{@ifop[e e e] @tag*{conditional}} 17 @acase{@λe[(@repeated{x:τ}) e] @tag*{lambda function}} 18 @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e] 19 @tag*{variadic function}} 20 @acase{@λe[(@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e] 21 @tag*{variadic polymorpic function}} 22 @acase{@Λe[(@repeated{α}) e]@tag*{polymorphic abstraction}} 23 @acase{@Λe[(@repeated{α} @polydotα[α]) e] 24 @tag*{variadic polymorphic abstraction}} 25 @acase{@at[e @repeated{τ}] @tag*{polymorphic instantiation}} 26 @acase{@promisee[e] @tag*{create promise}} 27 @acase{@forcee[e] @tag*{force promise}}@;TODO: shouldn't it be a primop? 28 @acase{@syme[s] @tag*{symbol literal}} 29 @acase{@gensyme[] @tag*{fresh uninterned symbol}} 30 @acase{@eq?op[e e] @tag*{symbol equality}} 31 @acase{@mapop[e e]}] 32 33 #:sym 34 35 @$${ 36 \begin{aligned} 37 s & ∈ 𝒮\\ 38 @sym* & ∈ @𝒮* \\ 39 𝒮 & ⊂ @𝒮* 40 \end{aligned} 41 }