diff --git a/docs/developers/CHANGELOG.md b/docs/developers/CHANGELOG.md index 13ac887..d3bcff8 100644 --- a/docs/developers/CHANGELOG.md +++ b/docs/developers/CHANGELOG.md @@ -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 diff --git a/docs/license/LICENSE b/docs/license/LICENSE index 7a2aa31..6443e70 100644 --- a/docs/license/LICENSE +++ b/docs/license/LICENSE @@ -1,4 +1,4 @@ -Copyright 2020-2022 WriteOnly Developers +Copyright 2020-2023 WriteOnly Developers Licensed under the Apache License, Version 2.0, or the MIT license HelVM.HelTC.HelTC
heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages
Safe HaskellNone
LanguageHaskell2010

HelVM.HelTC.HelTC

\ No newline at end of file +HelVM.HelTC.HelTC
heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages
Safe HaskellNone
LanguageHaskell2010

HelVM.HelTC.HelTC

\ No newline at end of file diff --git a/docs/reports/heltc/doc-index.html b/docs/reports/heltc/doc-index.html index 6fa781e..28972c3 100644 --- a/docs/reports/heltc/doc-index.html +++ b/docs/reports/heltc/doc-index.html @@ -1 +1 @@ -heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages (Index)
heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages
\ No newline at end of file +heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages (Index)
heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages
\ No newline at end of file diff --git a/docs/reports/heltc/heltc.haddock b/docs/reports/heltc/heltc.haddock index 19fb25b..a66e8c9 100644 Binary files a/docs/reports/heltc/heltc.haddock and b/docs/reports/heltc/heltc.haddock differ diff --git a/docs/reports/heltc/index.html b/docs/reports/heltc/index.html index e70fe29..e4bd452 100644 --- a/docs/reports/heltc/index.html +++ b/docs/reports/heltc/index.html @@ -1 +1 @@ -heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages
heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages

heltc-0.1.0.1: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages

Please see the README on GitHub at https://github.com/helvm/heltc#readme

Modules

\ No newline at end of file +heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages
heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages

heltc-0.1.0.2: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages

Please see the README on GitHub at https://github.com/helvm/heltc#readme

Modules

\ No newline at end of file diff --git a/examples/mlc/blynn/exp.mlc b/examples/mlc/blynn/exp.mlc new file mode 100644 index 0000000..ff79c1f --- /dev/null +++ b/examples/mlc/blynn/exp.mlc @@ -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. diff --git a/examples/mlc/blynn/factorial.mlc b/examples/mlc/blynn/factorial.mlc new file mode 100644 index 0000000..636120d --- /dev/null +++ b/examples/mlc/blynn/factorial.mlc @@ -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! diff --git a/examples/mlc/blynn/quote.mlc b/examples/mlc/blynn/quote.mlc new file mode 100644 index 0000000..307f52b --- /dev/null +++ b/examples/mlc/blynn/quote.mlc @@ -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) diff --git a/examples/mlc/blynn/shallow.mlc b/examples/mlc/blynn/shallow.mlc new file mode 100644 index 0000000..20cbf64 --- /dev/null +++ b/examples/mlc/blynn/shallow.mlc @@ -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). diff --git a/examples/mlc/blynn/supriseme-evaluate.mlc b/examples/mlc/blynn/supriseme-evaluate.mlc new file mode 100644 index 0000000..f079880 --- /dev/null +++ b/examples/mlc/blynn/supriseme-evaluate.mlc @@ -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. diff --git a/examples/mlc/blynn/supriseme-reduce.mlc b/examples/mlc/blynn/supriseme-reduce.mlc new file mode 100644 index 0000000..71d045b --- /dev/null +++ b/examples/mlc/blynn/supriseme-reduce.mlc @@ -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. diff --git a/examples/mlc/justine/prelude.mlc b/examples/mlc/justine/prelude.mlc new file mode 100644 index 0000000..78fcf8e --- /dev/null +++ b/examples/mlc/justine/prelude.mlc @@ -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) diff --git a/examples/mlc/list/list-of-char.mlc b/examples/mlc/list/list-of-char.mlc new file mode 100644 index 0000000..6750e18 --- /dev/null +++ b/examples/mlc/list/list-of-char.mlc @@ -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 . diff --git a/examples/mlc/list/list-of-int.mlc b/examples/mlc/list/list-of-int.mlc new file mode 100644 index 0000000..5a23502 --- /dev/null +++ b/examples/mlc/list/list-of-int.mlc @@ -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 . diff --git a/examples/mlc/list/list-of-nat.mlc b/examples/mlc/list/list-of-nat.mlc new file mode 100644 index 0000000..79b3a97 --- /dev/null +++ b/examples/mlc/list/list-of-nat.mlc @@ -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 . diff --git a/examples/mlc/list/list-of-nil.mlc b/examples/mlc/list/list-of-nil.mlc new file mode 100644 index 0000000..531ebea --- /dev/null +++ b/examples/mlc/list/list-of-nil.mlc @@ -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) + +, . , . , . , . . diff --git a/examples/mlc/list/list-of-pair.mlc b/examples/mlc/list/list-of-pair.mlc new file mode 100644 index 0000000..3db0cb0 --- /dev/null +++ b/examples/mlc/list/list-of-pair.mlc @@ -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) . diff --git a/examples/mlc/list/string-with-define.mlc b/examples/mlc/list/string-with-define.mlc new file mode 100644 index 0000000..4f12555 --- /dev/null +++ b/examples/mlc/list/string-with-define.mlc @@ -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 diff --git a/examples/mlc/list/string.mlc b/examples/mlc/list/string.mlc new file mode 100644 index 0000000..5a9c652 --- /dev/null +++ b/examples/mlc/list/string.mlc @@ -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" diff --git a/examples/mlc/lloyd/bool.mlc b/examples/mlc/lloyd/bool.mlc new file mode 100644 index 0000000..4bbe492 --- /dev/null +++ b/examples/mlc/lloyd/bool.mlc @@ -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? diff --git a/examples/mlc/other/guard.mlc b/examples/mlc/other/guard.mlc new file mode 100644 index 0000000..2390e9f --- /dev/null +++ b/examples/mlc/other/guard.mlc @@ -0,0 +1 @@ +: | \ guard \ body \ tail \ expression ? (guard expression) body (tail expression) diff --git a/examples/mlc/other/prelude.mlc b/examples/mlc/other/prelude.mlc new file mode 100644 index 0000000..d1df38e --- /dev/null +++ b/examples/mlc/other/prelude.mlc @@ -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)))) diff --git a/examples/mlc/other/reverse.mlc b/examples/mlc/other/reverse.mlc new file mode 100644 index 0000000..dae58d8 --- /dev/null +++ b/examples/mlc/other/reverse.mlc @@ -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 diff --git a/examples/mlc/other/rmk35.mlc b/examples/mlc/other/rmk35.mlc new file mode 100644 index 0000000..5a622ad --- /dev/null +++ b/examples/mlc/other/rmk35.mlc @@ -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 diff --git a/examples/mlc/other/wikipedia.mlc b/examples/mlc/other/wikipedia.mlc new file mode 100644 index 0000000..8baf1a8 --- /dev/null +++ b/examples/mlc/other/wikipedia.mlc @@ -0,0 +1,48 @@ +; Based on https://en.wikipedia.org/wiki/Lambda_calculus + +; 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 +: if \ p \ a \ b p a b + +; Pair +: pair \ x \ y \ f f x y +: first \ p p T +: second \ p p F + +; List +: nil \ x T +: null \ p p (\ x \ y F) +: repeat \ n \ x n (pair x) nil + +; Arithmetic - succ +: succ \ n \ f \ x f (n f x) +; plus \ m \ n \ f \ x m f (n f x) +: plus \ m \ n m succ n +; mult \ m \ n \ f m (n f) +: mult \ m \ n m (plus n) 0 +: pow \ b \ e e b + +; Natural numbers +; 0 \ f \ x x +; 1 \ f \ x f x +; 2 \ f \ x f (f x) +; 3 \ f \ x f (f (f x)) + +; Arithmetic - pred +: is0 \ n n (\ x F) T +: Φ \ x pair (second x) (succ (second 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 (plus (g k) 1)) (\ v 0) 0 +: pred \ n first (n Φ (pair 0 0)) +: sub \ m \ n n pred m + +; Compare +: leq \ m \ n is0 (sub m n) diff --git a/examples/mlc/other/zhiayang.mlc b/examples/mlc/other/zhiayang.mlc new file mode 100644 index 0000000..19894d4 --- /dev/null +++ b/examples/mlc/other/zhiayang.mlc @@ -0,0 +1,7 @@ +; https://github.com/zhiayang/lambda + +: S \ x \ y \ z x z (y z) +: K \ x \ y x +: I \ x x + +; S K K == I diff --git a/heltc.cabal b/heltc.cabal index b67f5f3..e5df645 100644 --- a/heltc.cabal +++ b/heltc.cabal @@ -1,7 +1,7 @@ cabal-version: 2.4 name: heltc -version: 0.1.0.1 +version: 0.1.0.2 synopsis: HELCT - Heavenly Esoteric Little C Transpiler to Esoteric Languages description: Please see the README on GitHub at @@ -12,7 +12,7 @@ license: Apache-2.0 license-file: docs/license/LICENSE-APACHE author: Kamil Adam maintainer: kamil.adam.zabinski@gmail.com -copyright: 2020-2021 WriteOnly Developers +copyright: 2020-2023 WriteOnly Developers category: Language build-type: Simple @@ -136,7 +136,7 @@ test-suite heltc-test hspec , hspec-core , hspec-expectations-pretty-diff - , hspec-golden + , hspec-golden > 0.1.0.0 , hspec-slow , heltc