language-garden
所属分类:编程语言基础
开发工具:OCaml
文件大小:0KB
下载次数:0
上传日期:2023-09-14 10:38:40
上 传 者:
sh-1993
说明: 一个小型编程语言实现的花园,
(A garden of small programming language implementations ,)
文件列表:
compile-arith-verified/ (0, 2023-12-09)
compile-arith-verified/ArithExprs.lean (4791, 2023-12-09)
compile-arith/ (0, 2023-12-09)
compile-arith/bin/ (0, 2023-12-09)
compile-arith/bin/Main.ml (2867, 2023-12-09)
compile-arith/bin/dune (120, 2023-12-09)
compile-arith/dune (54, 2023-12-09)
compile-arith/lib/ (0, 2023-12-09)
compile-arith/lib/AnfLang.ml (2224, 2023-12-09)
compile-arith/lib/Arith.ml (464, 2023-12-09)
compile-arith/lib/StackLang.ml (1958, 2023-12-09)
compile-arith/lib/Translation.ml (273, 2023-12-09)
compile-arith/lib/TreeLang.ml (1540, 2023-12-09)
compile-arith/lib/TreeLangLexer.mll (499, 2023-12-09)
compile-arith/lib/TreeLangParser.mly (708, 2023-12-09)
compile-arith/lib/TreeToAnf.ml (2204, 2023-12-09)
compile-arith/lib/TreeToAnf.mli (1101, 2023-12-09)
compile-arith/lib/TreeToStack.ml (987, 2023-12-09)
compile-arith/lib/TreeToStack.mli (159, 2023-12-09)
compile-arith/lib/dune (118, 2023-12-09)
compile-arith/test/ (0, 2023-12-09)
compile-arith/test/Properties.ml (3491, 2023-12-09)
compile-arith/test/dune (203, 2023-12-09)
compile-arith/test/tests.t (3711, 2023-12-09)
compile-arithcond/ (0, 2023-12-09)
compile-arithcond/bin/ (0, 2023-12-09)
compile-arithcond/bin/Main.ml (3582, 2023-12-09)
compile-arithcond/bin/dune (132, 2023-12-09)
compile-arithcond/dune (62, 2023-12-09)
compile-arithcond/lib/ (0, 2023-12-09)
compile-arithcond/lib/AnfLang.ml (3580, 2023-12-09)
compile-arithcond/lib/ArithCond.ml (464, 2023-12-09)
compile-arithcond/lib/StackLang.ml (4482, 2023-12-09)
compile-arithcond/lib/Translation.ml (273, 2023-12-09)
... ...
# Language garden
Some toy programming language implementations, mostly implemented in OCaml.
These projects are mostly my attempt to understand different techniques and
approaches to implementing programming languages. Perhaps from these seedlings
something new and interesting might germinate?
## Implementations
### Elaboration
Elaboration is an approach to implementing language front-ends where a complicated,
user friendly _surface language_ is type checked and lowered to a simpler, typed
_core language_. This approach to type checking is particularly popular and
useful for implementing dependently typed programming languages, but is more
widely applicable as well.
- [**elab-dependent**](https://github.com/brendanzab/language-garden/blob/master/./elab-dependent/):
An elaborator for a small dependently typed lambda calculus.
- [**elab-dependent-sugar**](https://github.com/brendanzab/language-garden/blob/master/./elab-dependent-sugar/):
An elaborator for a small dependently typed lambda calculus with syntactic sugar.
- [**elab-record-patching**](https://github.com/brendanzab/language-garden/blob/master/./elab-record-patching/):
An elaborator of a dependently typed lambda calculus with singletons and record patching.
- [**elab-stlc-abstract**](https://github.com/brendanzab/language-garden/blob/master/./elab-stlc-abstract):
An LCF-style elaborator that moves the construction of well-typed terms behind
a trusted interface.
- [**elab-stlc-unification**](https://github.com/brendanzab/language-garden/blob/master/./elab-stlc-unification):
An elaborator for a simply typed lambda calculus where type annotations can be omitted.
### Compilation
These are related to compilation. Mainly to stack-machines, but I’m interested
in exploring more approaches in the future, and other compilation passes
related to compiling functional programming languages.
- [**compile-arith**](https://github.com/brendanzab/language-garden/blob/master/./compile-arith/):
Compiling arithmetic expressions to stack machine instructions and A-Normal Form.
- [**compile-arithcond**](https://github.com/brendanzab/language-garden/blob/master/./compile-arithcond/):
Compiling arithmetic and conditional expressions to stack machine instructions and A-Normal Form.
- [**compile-arith-verified**](https://github.com/brendanzab/language-garden/blob/master/./compile-arith-verified/):
A formally verified arithmetic expression compiler and decompiler in Lean 4.
- [**compile-closure-conv**](https://github.com/brendanzab/language-garden/blob/master/./compile-closure-conv):
Typed closure conversion and lambda lifting for a simply typed lambda calculus
with booleans and integers.
### Languages
Miscellaneous programming language experiments.
- [**lang-datalog**](https://github.com/brendanzab/language-garden/blob/master/./lang-datalog/):
A simple Datalog interpreter.
- [**lang-fractal-growth**](https://github.com/brendanzab/language-garden/blob/master/./lang-fractal-growth/):
Experiments with using grammars and rewriting systems to model fractal growth.
- [**lang-lc-interpreters**](https://github.com/brendanzab/language-garden/blob/master/./lang-lc-interpreters/):
A comparison of lambda calculus interpreters using different approaches to
name binding.
- [**lang-shader-graphics**](https://github.com/brendanzab/language-garden/blob/master/./lang-shader-graphics/):
An embedded DSL for describing procedural graphics, based on signed distance
functions. These can be rendered on the CPU or compiled to GLSL shaders.
### Work in progress projects
While most of the above projects need more work put into them, the following
projects need more work put into them and a more incomplete in comparison.
- [**wip-elab-builtins**](https://github.com/brendanzab/language-garden/blob/master/./wip-elab-builtins/):
An elaborator that supports built-in types and operations.
- [**wip-compile-stratify**](https://github.com/brendanzab/language-garden/blob/master/./wip-compile-stratify/):
Compiling a dependently typed lambda calculus into a stratified intermediate
language.
- [**wip-compile-uncurry**](https://github.com/brendanzab/language-garden/blob/master/./wip-compile-uncurry/):
Compiling single-parameter functions to multiparameter functions.
## Development setup
### With Nix
Using [Nix] is not required, but can be useful for setting up a development
shell with the packages and tools used in this project. With [Nix flakes]
enabled:
```sh
nix run .#arith -- compile --target=anf <<< "1 + 2 * 27"
```
[nix-direnv] can be used to load development tools into your shell
automatically. Once it’s installed, run the following commands to enable it in
the project directory:
```sh
echo "use flake" > .envrc
direnv allow
```
You’ll want to locally exclude the `.envrc`, or add it to your global gitignore.
After that, [dune] can be used to build, test, and run the projects:
```sh
dune build
dune test
dune exec arith -- compile --target=anf <<< "1 + 2 * 27"
```
[dune]: https://dune.build
[Nix]: https://nixos.org
[Nix flakes]: https://nixos.wiki/wiki/Flakes
[nix-direnv]: https://github.com/nix-community/nix-direnv
### With opam
Alternatively, [opam] package definitions are provided in the [`./opam`](https://github.com/brendanzab/language-garden/blob/master/./opam)
directory. They drive the Nix flake, so _should_ be up to date. I don’t use opam
however, so I’m not sure what the workflow is.
[opam]: opam.ocaml.org
近期下载者:
相关文件:
收藏者: