violet
所属分类：数值算法/人工智能
开发工具：Lean
文件大小：21KB
下载次数：0
上传日期：2023-05-31 15:46:41
上 传 者：
sh-1993
说明： 一种编程语言，半定理证明器
(A programming language, half theorem prover)
文件列表:
LICENSE (1519, 2023-07-13)
Main.lean (418, 2023-07-13)
Tests (0, 2023-07-13)
Tests\Parsing.lean (1975, 2023-07-13)
Violet.lean (3614, 2023-07-13)
Violet (0, 2023-07-13)
Violet\Ast (0, 2023-07-13)
Violet\Ast\Common.lean (98, 2023-07-13)
Violet\Ast\Core.lean (975, 2023-07-13)
Violet\Ast\Surface.lean (2619, 2023-07-13)
Violet\Core (0, 2023-07-13)
Violet\Core\Context.lean (2539, 2023-07-13)
Violet\Core\DBI.lean (511, 2023-07-13)
Violet\Core\Elaboration.lean (6193, 2023-07-13)
Violet\Core\Eval.lean (3861, 2023-07-13)
Violet\Core\Unification.lean (4244, 2023-07-13)
Violet\Core\Value.lean (1564, 2023-07-13)
Violet\Parser.lean (5955, 2023-07-13)
example (0, 2023-07-13)
example\AModule.vt (170, 2023-07-13)
example\Base.vt (25, 2023-07-13)
example\Core.vt (39, 2023-07-13)
example\Lib.vt (36, 2023-07-13)
example\leibniz.vt (322, 2023-07-13)
example\module_failed.vt (141, 2023-07-13)
example\test.vt (1284, 2023-07-13)
lake-manifest.json (441, 2023-07-13)
lakefile.lean (406, 2023-07-13)
lean-toolchain (36, 2023-07-13)
runtime (0, 2023-07-13)
runtime\build.zig (563, 2023-07-13)
runtime\src (0, 2023-07-13)
runtime\src\main.zig (34, 2023-07-13)
... ...
# violet
[](https://github.com/dannypsnl/violet/actions/workflows/ci.yaml)
> **Warning** The project still in early stage.
A programming language focuses on
- dependent type
- effect system
- semantic versioning
- separate compilation
### Usage
Load module into REPL
```
violet example/module.vt
```
#### Example
```
data Unit | unit
data Nat
| zero
| suc Nat
data Bool
| true
| false
def zero? (n : Nat) : Bool =>
match n
| zero => true
| suc _ => false
record T {
a : Nat,
b : Bool,
}
def t (x : Nat) : T => (x, zero? x)
```
### Develop
You will need to install lean, via any package manager would be fine. Especially recommend vscode plugin (https://marketplace.visualstudio.com/items?itemName=leanprover.lean4), install it and wait, it should install `elan`, `lean`, and `lake` for you.
Build the project
```shell
lake build
```
#### Theory
Here are some related theories we already applied or going to use.
- elaboration[^1]
- universe polymorphism[^2] will try mugen
- termination checker[^3] will use lexicographic recursion
- type class[^4]
- indexed data type[^5]
[^1]: Elaboration with first-class implicit function types: https://dl.acm.org/doi/10.1145/3408***3
[^2]: An Order-Theoretic Analysis of Universe Polymorphism: https://favonia.org/files/mugen.pdf
[^3]: foetus - Termination Checker for Simple Functional Programs: https://www2.tcs.ifi.lmu.de/~abel/foetus.pdf
[^4]: Tabled Typeclass Resolution: https://arxiv.org/pdf/2001.04301.pdf
[^5]: A SIMPLER ENCODING OF INDEXED TYPES: https://arxiv.org/pdf/2103.15408v4.pdf
近期下载者：
相关文件：
收藏者：