Update demos and adds <|

This commit is contained in:
2026-05-13 19:39:15 -05:00
parent 8f7684a1bb
commit e3dcf5edd7
14 changed files with 333 additions and 127 deletions

View File

@@ -0,0 +1,58 @@
!import "../lib/base.tri" !Local
!import "../lib/list.tri" !Local
!import "../lib/io.tri" !Local
-- Interaction Tree Effect Runtime
--
-- The IO system is an interaction-tree effect runtime interpreted by a
-- small-step machine with a cooperative scheduler. Primitive actions
-- (putStr, readFile, writeFile, ...) are tagged nodes in an interaction
-- tree. Sequencing is performed by the single generic `bind` constructor.
--
-- pure x -- lift a pure value into IO
-- bind action k -- run action, then apply k to its result
-- thenIO a b -- run a, discard its result, then run b
-- mapIO action f -- run action, then apply f to its result inside pure
--
-- The runtime supports several effects beyond basic IO:
-- ask -- read the current environment
-- local f action -- run action with environment transformed by f
-- get -- read the current mutable state
-- put s -- replace the mutable state
-- fork action -- spawn a concurrent task, returning a handle
-- await handle -- wait for a forked task to complete
-- yield -- yield control to the scheduler
-- sleep ms -- suspend current task for N milliseconds
--
-- File operations return a Result tree (see lib/base.tri):
-- ok value -- pair true (pair value t)
-- err code -- pair false (pair code t)
--
-- Use onReadFile / onWriteFile for convenient branching.
--
-- See demos/interactionTrees/ for smaller focused examples.
-- Cooperative async demo.
-- fork runs an action in the background.
-- sleep suspends the current task for N milliseconds.
-- await waits for a forked task and returns its value.
--
-- Here the child sleeps for 2 s while the parent prints immediately.
-- The parent's message appears first, proving interleaving.
asyncDemo = (
bind (fork
(bind (sleep 2000) (_ :
bind (putStrLn "2000ms done sleeping!") (_ :
pure "child2000 done"))))
(handle2000 :
bind (fork
(bind (sleep 5000) (_ :
bind (putStrLn "5000ms done sleeping!") (_ :
pure "child5000 done"))))
(handle5000 :
bind (putStrLn "Parent first!") (_ :
bind (await handle5000) (_ :
await handle2000)))))
main = io asyncDemo

View File

@@ -0,0 +1,20 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Environment effects: ask and local.
-- ask reads the current environment value.
-- local f action runs action with the env transformed by f.
--
-- The CLI starts with an empty (Leaf) environment. This demo uses
-- local to inject a real string so that ask returns something readable.
main = io <|
(bind
local (_ : "sandbox")
(bind ask (env :
bind (putStrLn (append "working in env: " env)) (_ :
pure "inside-done"))))
(outside :
bind (putStrLn (append "local returned: " outside)) (_ :
pure t))

View File

@@ -0,0 +1,18 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Basic fork and await.
-- fork spawns a concurrent task and returns a handle.
-- await blocks until the task completes and returns its value.
worker = (msg :
bind (putStrLn (append "working: " msg)) (_ :
pure (append msg "-result")))
main = io <|
(bind (fork (worker "job1")) (h1 :
bind (fork (worker "job2")) (h2 :
bind (await h1) (r1 :
bind (await h2) (r2 :
putStrLn (append "Got " (append r1 (append " and " r2))))))))

View File

@@ -0,0 +1,10 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Greet and return a pure value.
-- putStrLn writes to stdout; pure lifts "done" into IO.
main = io (bind
(putStrLn (append "Hello, " "tricu"))
(_ : pure ""))

View File

@@ -0,0 +1,16 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- readFile returns a Result. matchResult branches on ok / err.
-- Run with --allow-read PATH or --unsafe-io.
safeRead = (path :
bind (readFile path)
(result :
matchResult
(err rest : pure "ERROR: Unable to read file")
(contents rest : pure contents)
result))
main = io (safeRead "demos/interactionTrees/greet.tri")

View File

@@ -0,0 +1,23 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Transform an IO result.
-- mapIO applies a pure function to the value produced by an action.
-- Run with --allow-read PATH or --unsafe-io.
safeRead = (path :
bind (readFile path)
(result :
matchResult
(err rest : pure "missing")
(contents rest : pure contents)
result))
shout = (path :
mapIO (safeRead path)
(text : append text "!!!"))
main = io (bind
(shout "demos/interactionTrees/greet.tri")
(text : putStrLn text))

View File

@@ -0,0 +1,22 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Mutable state via get and put.
-- get reads the current state.
-- put replaces the state.
--
-- The CLI starts with an empty (Leaf) state. This demo puts
-- readable strings and prints them back out.
main = io <|
bind (put "idle") (_ :
bind get (s1 :
bind (putStrLn (append "state: " s1)) (_ :
bind (put "running") (_ :
bind get (s2 :
bind (putStrLn (append "state: " s2)) (_ :
bind (put "done") (_ :
bind get (s3 :
bind (putStrLn (append "state: " s3)) (_ :
pure t)))))))))

View File

@@ -0,0 +1,20 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Write a file, then read it back.
-- thenIO discards the writeFile Result and continues.
-- Run with --unsafe-io (needs both read and write permissions).
writeThenRead = (path text :
thenIO
(writeFile path text)
(readFile path))
main = io <|
(bind (writeThenRead "/tmp/tricu-demo.txt" "hello from tricu")
(result :
matchResult
(err rest : putStrLn "error")
(contents rest : putStrLn contents)
result))

View File

@@ -0,0 +1,33 @@
!import "../../lib/base.tri" !Local
!import "../../lib/list.tri" !Local
!import "../../lib/io.tri" !Local
-- Cooperative scheduling with yield.
-- yield returns control to the scheduler so other tasks can run.
--
-- Two tasks print alternately because each yields after every line.
--chatter = (name n :
-- bind (putStrLn (append name " says 1")) (_ :
-- bind yield (_ :
-- bind (putStrLn (append name " says 2")) (_ :
-- bind yield (_ :
-- bind (putStrLn (append name " says 3")) (_ :
-- pure n))))))
chatter = name n : bind <|
putStrLn (append name " says 1") (_ :
bind yield (_ :
bind (putStrLn (append name " says 2")) (_ :
bind yield (_ :
bind (putStrLn (append name " says 3")) (_ :
pure n)))))
main = io <|
bind (fork (chatter "A" "doneA")) (ha :
bind (fork (chatter "B" "doneB")) (hb :
bind yield (_ :
bind (await ha) (a :
bind (await hb) (b :
putStrLn (append "Finished: " (append a (append " " b))))))))

View File

@@ -1,86 +0,0 @@
!import "../lib/base.tri" !Local
!import "../lib/list.tri" !Local
!import "../lib/io.tri" !Local
-- Monadic IO in tricu
--
-- The IO system is a free monad interpreted by the host. Primitive actions
-- (putStr, readFile, writeFile, ...) do not carry their own continuations.
-- Sequencing is performed by the single generic `bind` constructor.
--
-- pure x -- lift a pure value into IO
-- bind action k -- run action, then apply k to its result
-- thenIO a b -- run a, discard its result, then run b
-- mapIO action f -- run action, then apply f to its result inside pure
--
-- File operations return a Result tree (see lib/base.tri):
-- ok value -- pair true (pair value t)
-- err code -- pair false (pair code t)
--
-- Use onReadFile / onWriteFile for convenient branching.
-- ----------------------------------------------------------------------------
-- Example 1: Greet and return a pure value.
-- putStrLn writes to stdout; pure lifts "done" into IO.
-- ----------------------------------------------------------------------------
greet = (name :
bind (putStrLn (append "Hello, " name))
(_ : pure "done"))
-- ----------------------------------------------------------------------------
-- Example 2: Read a file safely.
-- readFile returns a Result. matchResult branches on ok / err.
-- ----------------------------------------------------------------------------
safeRead = (path :
bind (readFile path)
(result :
matchResult
(err rest : pure "missing")
(contents rest : pure contents)
result))
-- ----------------------------------------------------------------------------
-- Example 3: Write, then read back.
-- thenIO discards the writeFile Result and continues.
-- ----------------------------------------------------------------------------
writeThenRead = (path text :
thenIO
(writeFile path text)
(readFile path))
-- ----------------------------------------------------------------------------
-- Example 4: Transform an IO result.
-- mapIO applies a pure function to the value produced by an action.
-- ----------------------------------------------------------------------------
shout = (path :
mapIO (safeRead path)
(text : append text "!!!"))
-- ----------------------------------------------------------------------------
-- Example 5: Cooperative async.
-- fork runs an action in the background.
-- sleep suspends the current task for N milliseconds.
-- await waits for a forked task and returns its value.
--
-- Here the child sleeps for 2 s while the parent prints immediately.
-- The parent's message appears first, proving interleaving.
-- ----------------------------------------------------------------------------
asyncDemo = (
bind (fork
(bind (sleep 2000) (_ :
bind (putStrLn "Done sleeping!") (_ :
pure "child done"))))
(handle :
bind (putStrLn "Parent first!") (_ :
await handle)))
-- ----------------------------------------------------------------------------
-- Main action - run the async demo.
-- ----------------------------------------------------------------------------
main = io asyncDemo