1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-24 07:57:58 +03:00
Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
Go to file
Jonathan Prieto-Cubides 8853b30cd5 Added agda ignores
2021-10-18 16:45:34 +02:00
.github/workflows Delete ci.yml 2021-09-26 19:29:17 +02:00
doc First commit, initial project template. 2021-09-26 18:59:51 +02:00
notes First commit, initial project template. 2021-09-26 18:59:51 +02:00
src First commit, initial project template. 2021-09-26 18:59:51 +02:00
workflows First commit, initial project template. 2021-09-26 18:59:51 +02:00
.ghci First commit, initial project template. 2021-09-26 18:59:51 +02:00
.gitignore Added agda ignores 2021-10-18 16:45:34 +02:00
.hlint.yaml First commit, initial project template. 2021-09-26 18:59:51 +02:00
CHANGELOG.md First commit, initial project template. 2021-09-26 18:59:51 +02:00
LICENSE First commit, initial project template. 2021-09-26 18:59:51 +02:00
Makefile First commit, initial project template. 2021-09-26 18:59:51 +02:00
MiniJuvix.cabal First commit, initial project template. 2021-09-26 18:59:51 +02:00
README.md Delete ci.yml 2021-09-26 19:29:17 +02:00
stack.yaml First commit, initial project template. 2021-09-26 18:59:51 +02:00

MiniJuvix GPL-3.0-only license Haskell CI

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 functional language with dependent types.

The following is a tentative project structure, but it can change at any moment. See below the file project structure. The diagram shows the design of the compiler related with the project structure.

In the picture, syntax transformations are denoted by pᵢ (e.g. passes in the Juvix Translate library) and checking operations are denoted by cᵢ (e.g. found in the Juvix Core library), and both families of items are the priority of this project.

$ tree src/
...
src
 ├─ app
 │ ├─ Main.hs
 │ └─ Options.hs
 ├─ MiniJuvix
 │ ├─ Pipeline.hs
 │ ├─ Parser
 │ ├─ Syntax
 │ │ ├─ Sugared.hs
 │ │ ├─ Desugared.hs
 │ │ ├─ Core.hs
 │ │ └─ Eval.hs

 │ ├─ Typing
 │ │ ├─ Scopechecking.hs
 │ │ ├─ Coverage.hs
 │ │ ├─ Typechecking.hs
 │ │ ├─ Termination.hs
 │ │ └─ Erasure.hs
 │ └─ Utils
 │   ├─ Parsing.hs
 │   ├─ Pretty.hs
 │   ├─ File.hs
 │   └─ Version.hs
 └─ test
     └─ Spec.hs
...