2021-09-26 20:06:22 +03:00
|
|
|
MiniJuvix <!-- [](https://github.com/heliaxdev/MiniJuvix/actions) -->
|
2021-12-30 18:53:36 +03:00
|
|
|
[](LICENSE) [](https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml)
|
2021-09-26 20:06:22 +03:00
|
|
|
=========
|
2021-09-26 19:59:51 +03:00
|
|
|
|
|
|
|
|
This repository aims to be a conservative Haskell project of a tiny
|
|
|
|
|
language with dependent types based on the Juvix project. The primary
|
|
|
|
|
purpose is to be a laboratory to study/experiment in implementing a
|
2021-09-26 20:06:22 +03:00
|
|
|
functional language with dependent types.
|
2021-09-26 19:59:51 +03:00
|
|
|
|
2021-10-26 15:50:52 +03:00
|
|
|
In this branch `qtt`, MiniJuvix aims to be programming language based
|
2021-12-30 18:53:36 +03:00
|
|
|
on Quantitative type theory. Some Haskell code has been generated
|
|
|
|
|
automatically by `agda2hs`. In the future, we want to prove properties
|
|
|
|
|
about the Minijuvix programs directly in Agda.
|
2021-10-26 15:50:52 +03:00
|
|
|
|
2021-09-26 19:59:51 +03:00
|
|
|
The following is a tentative project structure, but it can change at
|
2021-09-26 20:29:17 +03:00
|
|
|
any moment. See below the file project structure. The diagram shows
|
|
|
|
|
the design of the compiler related with the project structure.
|
|
|
|
|
|
|
|
|
|
<p align="center">
|
2021-12-30 18:53:36 +03:00
|
|
|
<img src="docs/minijuvix.png">
|
2021-09-26 20:29:17 +03:00
|
|
|
</p>
|
|
|
|
|
|
2021-12-30 18:53:36 +03:00
|
|
|
In the picture, syntax transformations are denoted by pᵢ and checking
|
|
|
|
|
operations are denoted by cᵢ .
|
2021-09-26 19:59:51 +03:00
|
|
|
|
