From 88b1c716953c593219ef9869400b89f8423995c9 Mon Sep 17 00:00:00 2001 From: James Eversole Date: Thu, 23 Jan 2025 18:57:59 -0600 Subject: [PATCH] Add size demo --- README.md | 3 +++ demos/size.tri | 19 +++++++++++++++++++ demos/toSource.tri | 2 +- 3 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 demos/size.tri diff --git a/README.md b/README.md index bd7aa56..88e85bd 100644 --- a/README.md +++ b/README.md @@ -34,6 +34,9 @@ tricu > "Stem" tricu < -- We can even convert a term back to source code (/demos/toSource.tri) tricu < toSource not? tricu > "(t (t (t t) (t t t)) (t t (t t t)))" +tricu < -- or calculate its size (/demos/size.tri) +tricu < size not? +tricu > 12 ``` ## Installation and Use diff --git a/demos/size.tri b/demos/size.tri new file mode 100644 index 0000000..d21bfef --- /dev/null +++ b/demos/size.tri @@ -0,0 +1,19 @@ +compose = (\f g x : f (g x)) + +succ = y (\self : + triage + 1 + t + (triage + (t (t t)) + (\_ tail : t t (self tail)) + t)) + +size = (\x : + (y (\self x : + compose succ + (triage + (\x : x) + self + (\x y : compose (self x) (self y)) + x)) x 0)) diff --git a/demos/toSource.tri b/demos/toSource.tri index fec1d86..7ed5e25 100644 --- a/demos/toSource.tri +++ b/demos/toSource.tri @@ -43,4 +43,4 @@ toSource_ = y (\self arg : toSource = (\v : toSource_ v "") exampleOne = toSource true -- OUT: "(t t)" -exampleTwo = toSource not -- OUT: "(t (t (t t) (t t t)) (t t (t t t)))" +exampleTwo = toSource not? -- OUT: "(t (t (t t) (t t t)) (t t (t t t)))"