@cicada-lang/mugda.sexp v0.1.13
Mugda
An implementation of the Mugda paper by Karl Mehltretter.
The "Mu" of the name "Mugda" comes from μ-operator (mu-operator) of general recursive function.
Notes about our implementation:
- Use S-expression as overall syntax, to expression ideas clearly.
- Close to the paper, so that the code is easy to be reviewed with the paper.
- Add comments about alternative ways to implement the same ideas.
- Do not follow bad naming conventions of the paper.
Usages
Use our server
mugda-server: A server that can run mugda code.
Run a file:
curl https://mu.cic.run --data-binary @docs/tests/basic/let.test.mu
Run multiline text (bash and zsh):
curl https://mu.cic.run --data-binary @- << END
(data Nat () ()
(zero () Nat)
(add1 ([prev Nat]) Nat))
(fn add (-> Nat Nat Nat)
[(x (zero)) x]
[(x (add1 y)) (add1 (add x y))])
(add (add1 zero) (add1 zero))
END
Command line tool
Install it by the following command:
npm install -g @cicada-lang/mugda.sexp
The command line program is called mu
.
open a REPL:
mu repl
or just:
mu
Run a file:
mu run docs/tests/basic/id.test.mu
Run a file and watch file change:
mu run docs/tests/basic/id.test.mu --watch
Run a URL:
- All files in this repo, can be fetched from:
https://cdn.mu.cic.run/<path>
, and any other http server that serves.mu
code would also work.
mu run https://cdn.mu.cic.run/docs/tests/basic/id.test.mu
Notes
Zero arity data constructor
When using zero arity data constructor, we must write them in ()
.
For example, zero
and (zero)
are the same.
But when using zero arity data constructor in pattern, we must write them in ()
.
For example, we should not write zero
but write (zero)
,
otherwise the interpreter can not distinguish pattern variable
from this zero arity data constructor.
Syntax of inductive datatype definition
The syntax of inductive datatype definition -- (data)
,
is learnt from "The Little Typer".
Examples
TODO
Please see docs/tests/ for more examples.
Development
npm install # Install dependencies
npm run build # Compile `src/` to `lib/`
npm run build:watch # Watch the compilation
npm run format # Format the code
npm run test # Run test
npm run test:watch # Watch the testing
Thanks
Thank you, Karl Mehltretter, for writing this paper.
Contributions
To make a contribution, fork this project and create a pull request.
Please read the STYLE-GUIDE.md before you change the code.
Remember to add yourself to AUTHORS. Your line belongs to you, you can write a little introduction to yourself but not too long.
It is assumed that all non draft PRs are ready to be merged. If your PR is not ready to be merged yet, please make it a draft PR:
During the development of your PR, you can make use of the TODO.md file to record ideas temporarily, and this file should be clean again at the end of your development.