Skip to content

Commit

Permalink
Add examples for MLC
Browse files Browse the repository at this point in the history
  • Loading branch information
kamil-adam committed May 13, 2023
1 parent 87446e6 commit b859bd2
Show file tree
Hide file tree
Showing 28 changed files with 356 additions and 7 deletions.
3 changes: 3 additions & 0 deletions docs/developers/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
# 📅 Revision history for HelTC

## 0.1.0.2 -- 2023-05-13
* Add examples for MLC

## 0.1.0.1 -- 2023-05-04
* Update libraries

Expand Down
2 changes: 1 addition & 1 deletion docs/license/LICENSE
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Copyright 2020-2022 WriteOnly Developers
Copyright 2020-2023 WriteOnly Developers

Licensed under the Apache License, Version 2.0, <LICENSE-APACHE or
http://apache.org/licenses/LICENSE-2.0> or the MIT license <LICENSE-MIT or
Expand Down
2 changes: 1 addition & 1 deletion docs/reports/heltc/HelVM-HelTC-HelTC.html
Original file line number Diff line number Diff line change
@@ -1 +1 @@
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>HelVM.HelTC.HelTC</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</span><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">HelVM.HelTC.HelTC</p></div><div id="interface"></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.24.2</p></div></body></html>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>HelVM.HelTC.HelTC</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</span><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">HelVM.HelTC.HelTC</p></div><div id="interface"></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.24.2</p></div></body></html>
2 changes: 1 addition & 1 deletion docs/reports/heltc/doc-index.html
Original file line number Diff line number Diff line change
@@ -1 +1 @@
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages (Index)</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</span><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.24.2</p></div></body></html>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages (Index)</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</span><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.24.2</p></div></body></html>
Binary file modified docs/reports/heltc/heltc.haddock
Binary file not shown.
2 changes: 1 addition & 1 deletion docs/reports/heltc/index.html
Original file line number Diff line number Diff line change
@@ -1 +1 @@
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</span><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"><div id="description"><h1>heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</h1><div class="doc"><p>Please see the README on GitHub at <a href="https://github.com/helvm/heltc#readme">https://github.com/helvm/heltc#readme</a></p></div></div><div id="module-list"><p class="caption">Modules</p><ul><li><span class="module details-toggle-control details-toggle" data-details-id="n.1">HelVM</span><details id="n.1" open="open"><summary class="hide-when-js-enabled">Submodules</summary><ul><li><span class="module details-toggle-control details-toggle" data-details-id="n.1.1">HelTC</span><details id="n.1.1" open="open"><summary class="hide-when-js-enabled">Submodules</summary><ul><li><span class="module"><span class="noexpander">&nbsp;</span><a href="HelVM-HelTC-HelTC.html">HelVM.HelTC.HelTC</a></span></li></ul></details></li></ul></details></li></ul></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.24.2</p></div></body></html>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</span><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"><div id="description"><h1>heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages</h1><div class="doc"><p>Please see the README on GitHub at <a href="https://github.com/helvm/heltc#readme">https://github.com/helvm/heltc#readme</a></p></div></div><div id="module-list"><p class="caption">Modules</p><ul><li><span class="module details-toggle-control details-toggle" data-details-id="n.1">HelVM</span><details id="n.1" open="open"><summary class="hide-when-js-enabled">Submodules</summary><ul><li><span class="module details-toggle-control details-toggle" data-details-id="n.1.1">HelTC</span><details id="n.1.1" open="open"><summary class="hide-when-js-enabled">Submodules</summary><ul><li><span class="module"><span class="noexpander">&nbsp;</span><a href="HelVM-HelTC-HelTC.html">HelVM.HelTC.HelTC</a></span></li></ul></details></li></ul></details></li></ul></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.24.2</p></div></body></html>
13 changes: 13 additions & 0 deletions examples/mlc/blynn/exp.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
; Based on https://crypto.stanford.edu/~blynn/lambda/

: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

; 2 \ f \ x f (f x)
; 3 \ f \ x f (f (f x))
: exp \ m \ n n m

exp 2 3; Compute 2^ 3.
15 changes: 15 additions & 0 deletions examples/mlc/blynn/factorial.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
; Based on https://crypto.stanford.edu/~blynn/lambda/

: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

: pred \ n \ f \ x n (\ g \ h h (g f)) (\ u x) (\ u u)
: mul \ m \ n \ f m (n f)
: is0 \ n n (\ _ F) T
: Y \ f (\ x x x) (\ x f (x x))
: fact Y (\ f \ n (is0 n) 1 (mul n (f (pred n))))

fact 4; Compute 4!
11 changes: 11 additions & 0 deletions examples/mlc/blynn/quote.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
; https://crypto.stanford.edu/~blynn/lambda/

: var \ m \ a \ b \ c a m
: app \ m \ n \ a \ b \ c b m n
: abs \ f \ a \ b \ c c f

; Our `quote` primitive lies outside lambda calculus:
; quote ((\ y y) x)

; Encoding terms in lambda calculus (without typing the raw encoding):
; app (abs (\ y var y)) (var x)
12 changes: 12 additions & 0 deletions examples/mlc/blynn/shallow.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
; https://crypto.stanford.edu/~blynn/lambda/

; Shallow encoding.
: var \ x \ i x
: app \ m \ n \ i i (m i) (n i)
: abs \ f \ i \ x f x i
: E \ q q (\ x x); A self-interpreter.

: qsucc abs (\ n abs(\ f abs(\ x app (var f) (app (app (var n) (var f)) (var x)))))
: q0 abs (\ f abs(\ x var x))

E (app qsucc (app qsucc q0)); Compute succ (succ 0).
12 changes: 12 additions & 0 deletions examples/mlc/blynn/supriseme-evaluate.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
; Based on https://crypto.stanford.edu/~blynn/lambda/

; See Mogensen, "Efficient Self-Interpretation in Lambda Calculus".
: Y \ f (\ x f(x x))(\ x f(x x))
: E Y (\ e \ m m (\ x x) (\ m \ n (e m)(e n)) (\ m \ v e (m v)))
: P Y (\ p \ m (\ x x(\ v p(\ a \ b \ c b m(v (\ a \ b b)))) m ))
: RR Y (\ r \ m m (\ x x) (\ m \ n (r m) (\ a \ b a) (r n)) (\ m (\ g \ x x g (\ a \ b \ c c (\ w g (P (\ a \ b \ c a w))(\ a \ b b)))) (\ v r (m v))))
: R \ m RR m (\ a \ b b)
; 1 \ f \ x f x
: succ \ n \ f \ x f (n f x)

; E (quote (succ (succ (succ 1)))); Self-interpreter demo.
12 changes: 12 additions & 0 deletions examples/mlc/blynn/supriseme-reduce.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
; Based on https://crypto.stanford.edu/~blynn/lambda/

; See Mogensen, "Efficient Self-Interpretation in Lambda Calculus".
: Y \ f (\ x f(x x))(\ x f(x x))
: E Y (\ e \ m m (\ x x) (\ m \ n (e m)(e n)) (\ m \ v e (m v)))
: P Y (\ p \ m (\ x x(\ v p(\ a \ b \ c b m(v (\ a \ b b)))) m ))
: RR Y (\ r \ m m (\ x x) (\ m \ n (r m) (\ a \ b a) (r n)) (\ m (\ g \ x x g (\ a \ b \ c c (\ w g (P (\ a \ b \ c a w))(\ a \ b b)))) (\ v r (m v))))
: R \ m RR m (\ a \ b b)
; 1 \ f \ x f x
: succ \ n \ f \ x f (n f x)

; R (quote (succ (succ (succ 1)))); Self-reducer demo.
42 changes: 42 additions & 0 deletions examples/mlc/justine/prelude.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
; https://justine.lol/lambda/

: if # 0
: omega # (0 0)
: pair ### ((0 2) 1)
: car # (0 $true)
: cdr # (0 $false)
: or ## ((0 0) 1)
: and ## ((0 1) 0)
: not ### ((2 0) 1)
: xor ## ((1 ## ((2 0) 1)) 0)
: bitxor ## ((1 0) ## ((2 0) 1))
: iszero ### ((2 # 1) 1)
: Y # (# (0 0) # (1 (0 0)))

: zero ## 0
: one ## (1 0)
: two ## (1 (1 0))
: three ## (1 (1 (1 0)))
: four ## (1 (1 (1 (1 0))))
: five ## (1 (1 (1 (1 (1 0)))))
: six ## (1 (1 (1 (1 (1 (1 0))))))
: seven ## (1 (1 (1 (1 (1 (1 (1 0)))))))
: eight ## (1 (1 (1 (1 (1 (1 (1 (1 0))))))))
: nine ## (1 (1 (1 (1 (1 (1 (1 (1 (1 0)))))))))

: pow ## (0 1)
: mul ### (2 (1 0))
: dec ### (((2 ## (0 (1 3))) # 1) # 0)
: sub ## ((0 $dec) 1)
: inc ### (1 ((2 1) 0))
: add #### ((3 1) ((2 1) 0))
: fac ## (((1 ## (0 (1 ## ((2 1) (1 0))))) #1) #0)
: min #### (((3 ## (0 1)) #1) ((2 ## (3 (0 1))) #1))
: div #### (((3 ## (0 1)) # 1) ((3 # (((3 ## (0 1)) # (3 (0 1))) #0)) 0))
: mod #### (((3 $cdr) ((3 # (((3 ### ((0 (2 (5 1))) 1)) #1) 1)) #1)) ##0)

: eq ## ((((1 # ((0 #0) #0)) ((0 ### (1 2)) ##0)) ###0) ##1)
: le ## (((1 ## (0 1)) ###1) ((0 ## (0 1)) ###0))
: lt ## (((0 ## (0 1)) ###0) ((1 ## (0 1)) ###1))
: odd # (# (0 0) ## ((0 ## 1) # ((0 ## 0) (2 2))))
: divides ## (((1 $cdr) ($omega #(((1 ### ((0 (2 ##0)) 1)) #(1 1)) ##1))) ##0)
7 changes: 7 additions & 0 deletions examples/mlc/list/list-of-char.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

, 'h , 'e , 'l , 'l , 'o .
7 changes: 7 additions & 0 deletions examples/mlc/list/list-of-int.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

, -1 , +2 , -3 , +4 .
7 changes: 7 additions & 0 deletions examples/mlc/list/list-of-nat.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

, 0 , 1 , 2 , 3 , 4 .
7 changes: 7 additions & 0 deletions examples/mlc/list/list-of-nil.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

, . , . , . , . .
7 changes: 7 additions & 0 deletions examples/mlc/list/list-of-pair.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

, (, true 1) , (, false 2) , (, true 3) , (, false 4) .
8 changes: 8 additions & 0 deletions examples/mlc/list/string-with-define.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

: hello "hello"
hello
7 changes: 7 additions & 0 deletions examples/mlc/list/string.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
: T \ x \ y y
: F \ x \ y x
: , \ x \ y \ f f x y
: . \ x T
: @ \ n \ f \ x f (n f x)

"hello"
10 changes: 10 additions & 0 deletions examples/mlc/lloyd/bool.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
; https://users $monash $edu/~lloyd/tildeFP/Lambda/Examples/

: TRUE \ a \ b a
: FALSE \ a \ b b

: AND \ p \ q p q FALSE
: OR \ p \ q p TRUE q
: NOT \ p \ a \ b p b a
: IF \ p \ a \ b p a b
; EQ \ x \ y if x = y then TRUE else FALSE ; Are you kidding?
1 change: 1 addition & 0 deletions examples/mlc/other/guard.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
: | \ guard \ body \ tail \ expression ? (guard expression) body (tail expression)
84 changes: 84 additions & 0 deletions examples/mlc/other/prelude.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
; Constants
: id \ x x
: T \ x \ y x
: F \ x \ y y

; Logic
: and \ p \ q p q p
: or \ p \ q p p q
: not \ p p F T
: nand \ p \ q not (and p q)
: nor \ p \ q not (or p q)
: if \ p \ a \ b p a b
: if \ p \ x \ y p x y

: compose \ f \ g \ x f (g x)

: pair \ x \ y \ f f x y
: , pair
: fst \ p p T
: snd \ p p F
: car fst
: cdr snd

; List
: cons \ x \ y \ f \ init f x (y f init)
; nil \ x \ init init
: nil F
; . nil
: null \ p p (\ x \ y F)
: repeat \ n \ x n (pair x) nil
: uncons \ xs \ f \ z xs (\ a \ b \ _ f a b) z

: fold \ f \ l \ init l f init
: map \ f \ l \ g \ init l (compose g f) init

: nilmap \ f \ a if (null a) (f a) nil

; Arithmetic add
: succ \ n \ f \ x f (n f x)
; add \ m \ n \ f \ x m f (n f x)
: add \ m \ n m succ n
; mul \ m \ n \ f m (n f)
: mul \ m \ n m (add n) 0
: pow \ b \ e e b

; 0 \ f \ x x
; 1 \ f \ x f x
; 2 \ f \ x f (f x)
; 3 \ f \ x f (f (f x))

; Arithmetic minus
: is0 \ n n (\ x F) T
: eq0 is0
: phi \ x cons (cdr x) (succ (cdr x))
: Φ phi
; pred \ n \ f \ x n (\ g \ h h (g f)) (\ u x) (\ u u)
; pred \ n n (\ g \ k is0 (g 1) k (add (g k) 1)) (\ v 0) 0
: pred \ n car (n Φ (cons 0 0))
: sub \ m \ n n pred m

; Compare
: leq \ m \ n is0 (sub m n)
: geq \ m \ n leq n m
: eq \ m \ n and (leq n m) (geq n m)
: neq \ m \ n nand (leq n m) (geq n m)
: lt \ m \ n and (leq n m) (not (geq n m))
: gt \ m \ n and (not (leq n m)) (geq n m)

; Other
: Y \ rec (\ x rec (x x)) (\ x rec (x x))
: fix Y
; I id
; S \ x \ y \ z x z (y z)
; K T
: B \ x \ y \ z x (y z)
: C \ x \ y \ z x z y
: W \ x \ y x y y
: ω \ x x x
: Δ \ x x x
: Ω ω ω

; List recursive
: reverse Y (\ rec \ ys \ xs uncons xs (\ x \ xs rec (cons x ys) xs) ys) nil
: fact Y (\ rec \ n (is0 n) 1 (mul n (rec (pred n))))
8 changes: 8 additions & 0 deletions examples/mlc/other/reverse.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
: Y \ f (\ x f (x x)) (\ x f (x x))

: cons \ a \ b \ f f a b
: nil \ x \ y y

: uncons \ xs \ f \ z xs (\ a \ b \ _ f a b) z

: reverse Y (\ c \ ys \ xs uncons xs (\ x \ xs c (cons x ys) xs) ys) nil
21 changes: 21 additions & 0 deletions examples/mlc/other/rmk35.mlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
; https://www.cl.cam.ac.uk/~rmk35/lambda_calculus/lambda_calculus.html

: Y \ f (\ x f (x x)) (\ x f (x x))
: id \ x x
: compose \ f \ g \ x f (g x)
: T \ x \ y x
: F \ x \ y y
: if \ p \ x \ y p x y
: pair \ x \ y \ f f x y
: fst \ p p (\ x \ y x)
: snd \ p p (\ x \ y y)
: cons \ x \ y \ f \ init f x (y f init)
: nil \ f \ init init
: fold \ f \ l \ init l f init
: map \ f \ l \ g \ init l (compose g f) init
: succ \ n \ f \ x f (n f x)
: add \ n \ m \ f \ x n f (m f x)
: mul \ n \ m \ f \ x n (m f) x
: pow \ n \ m m n
: pred \ n \ f \ x n (\ g \ h h (g f)) (\ u x) (\ u u)
: eq0 \ n n (\ x F) T
Loading

0 comments on commit b859bd2

Please sign in to comment.