HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-08-16 11:50:40 +03:00
Code Issues Packages Projects Releases Wiki Activity

fix: dependencies in order to make it easier to put on crates.io

Browse Source
This commit is contained in:
felipegchi 2023-01-27 08:50:02 -03:00
parent 776328a4c0
commit bd0ca5ff6c
20 changed files with 177 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
Cargo.lock generated
View File

@ -491,46 +491,17 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
[[package]]
name = "hvm"
version = "1.0.9-beta"
source = "git+https://github.com/Kindelia/HVM.git?rev=bd744430430a3ebeb69918572ed0be0a8dacb86a#bd744430430a3ebeb69918572ed0be0a8dacb86a"
dependencies = [
"backtrace",
"clap 3.2.23",
"crossbeam",
"highlight_error",
"im",
"instant",
"itertools",
"sysinfo",
]
[[package]]
name = "hvm"
version = "1.0.13-beta"
source = "git+https://github.com/Kindelia/HVM.git#30f6f35dcb9fad3d4585ab0b236313f6143249c9"
dependencies = [
"backtrace",
"clap 3.2.23",
"crossbeam",
"highlight_error",
"im",
"instant",
"itertools",
"sysinfo",
]
[[package]]
name = "im"
version = "15.1.0"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9"
checksum = "937a98729b61eb583f952d71b628ec656eb04c31704ccbd57165ad6cc6824e42"
dependencies = [
"bitmaps",
"rand_core 0.6.4",
"rand_xoshiro",
"sized-chunks",
"typenum",
"version_check",
"backtrace",
"clap 3.2.23",
"crossbeam",
"highlight_error",
"instant",
"itertools",
"sysinfo",
]
[[package]]
@ -653,7 +624,7 @@ name = "kind-checker"
version = "0.1.0"
dependencies = [
"fxhash",
"hvm 1.0.13-beta",
"hvm",
"im-rc",
"kind-report",
"kind-span",
@ -678,7 +649,7 @@ dependencies = [
"anyhow",
"dashmap",
"fxhash",
"hvm 1.0.13-beta",
"hvm",
"kind-checker",
"kind-parser",
"kind-pass",
@ -714,21 +685,6 @@ dependencies = [
"linked-hash-map",
]
[[package]]
name = "kind-query"
version = "0.1.0"
dependencies = [
"fxhash",
"kind-checker",
"kind-parser",
"kind-pass",
"kind-report",
"kind-span",
"kind-target-hvm",
"kind-tree",
"pathdiff",
]
[[package]]
name = "kind-report"
version = "0.1.0"
@ -749,7 +705,7 @@ version = "0.1.0"
name = "kind-target-hvm"
version = "0.1.0"
dependencies = [
"hvm 1.0.9-beta",
"hvm",
"kind-derive",
"kind-report",
"kind-span",
@ -793,7 +749,6 @@ name = "kind-tree"
version = "0.1.0"
dependencies = [
"fxhash",
"hvm 1.0.13-beta",
"kind-span",
"linked-hash-map",
]
@ -806,14 +761,14 @@ dependencies = [
"clap 4.0.29",
"kind-checker",
"kind-driver",
"kind-query",
"kind-report",
]
[[package]]
name = "kindelia_common"
version = "0.1.5"
source = "git+https://github.com/developedby/Kindelia/?branch=kdl-lang-crate#ff2f75e319c167cbc9d19cbc35fbe0d9a510b56a"
version = "0.1.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b8de1aea9d5b1e5bce50affa6c3d720f48a8bcf59bc8e53be68e6509740554cb"
dependencies = [
"bit-vec",
"hex",
@ -826,12 +781,14 @@ dependencies = [
[[package]]
name = "kindelia_lang"
version = "0.1.0"
source = "git+https://github.com/developedby/Kindelia/?branch=kdl-lang-crate#ff2f75e319c167cbc9d19cbc35fbe0d9a510b56a"
version = "0.1.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4306d4e6a8215201432d0c0b0010ec6374dd31982a02adab41fa491c453f909f"
dependencies = [
"hex",
"kindelia_common",
"serde",
"thiserror",
]
[[package]]

1
crates/kind-checker/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-checker"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Type checker for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

3
crates/kind-checker/src/report.rs
View File

@ -2,10 +2,11 @@
//! a Expr of the kind-tree package.
use kind_span::{EncodedRange, Range};
use kind_tree::backend::Term;
use kind_tree::symbol::{Ident, QualifiedIdent};
use kind_tree::{desugared, Operator};
use hvm::Term;
use crate::diagnostic::TypeDiagnostic;
use desugared::Expr;

1
crates/kind-cli/Cargo.toml
View File

@ -17,7 +17,6 @@ path = "src/main.rs"
kind-driver = { path = "../kind-driver", version = "0.1.0" }
kind-report = { path = "../kind-report", version = "0.1.0" }
kind-checker = { path = "../kind-checker", version = "0.1.0" }
kind-query = { path = "../kind-query", version = "0.1.0" }
clap = { version = "4.0.10", features = ["derive"] }
anyhow = "1.0.66"

94
crates/kind-cli/README.md Normal file
View File

@ -0,0 +1,94 @@
Kind2
=====
**Kind2** is a **functional programming language** and **proof assistant**.
It is a complete rewrite of [Kind1](https://github.com/kindelia/kind-legacy), based on
[HVM](https://github.com/kindelia/hvm), a **lazy**, **non-garbage-collected** and **massively parallel** virtual
machine. In [our benchmarks](https://github.com/kindelia/functional-benchmarks), its type-checker outperforms every
alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2
unleashes the [inherent parallelism of the Lambda
Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
the next century.
**Welcome to the inevitable parallel, functional future of computers!**
Examples
--------
Pure functions are defined via equations, as in [Haskell](https://www.haskell.org/):
```javascript
// Applies a function to every element of a list
map <a> <b> (list: List a) (f: a -> b) : List b
map a b Nil f = Nil
map a b (Cons head tail) f = Cons (f head) (map tail f)
```
Side-effective programs are written via monads, resembling [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
```javascript
// Prints the double of every number up to a limit
Main : IO (Result () String) {
ask limit = IO.prompt "Enter limit:"
for x in (List.range limit) {
IO.print "{} * 2 = {}" x (Nat.double x)
}
return Ok ()
}
```
Theorems can be proved inductively, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
```javascript
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
black_friday_theorem Nat.zero = Equal.refl
black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)
```
For more examples, check the [Wikind](https://github.com/kindelia/wikind).
Usage
-----
First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
```
cargo install kind2
```
### Warning:
New versions probably are not in `cargo`, so you can install the current version of kind2 by following these instructions:
1. Install Rust Nightly Toolchain
2. Clone the repository
3. `cargo install --path crates/kind-cli --force`
Then, use any of the commands below:
Command | Usage | Note
---------- | ------------------------- | --------------------------------------------------------------
Check | `kind2 check file.kind2` | Checks all definitions.
Eval | `kind2 eval file.kind2` | Runs using the type-checker's evaluator.
Run | `kind2 run file.kind2` | Runs using HVM's evaluator, on Rust-mode.
To-HVM | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to C.
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to [Kindelia](https://github.com/kindelia/kindelia).
Executables can be generated via HVM:
```
kind2 to-hvm file.kind2
hvm compile file.hvm
clang -O2 file.c -o file
./file
```
---
- If you need support related to Kind, email [support.kind@kindelia.org](mailto:support.kind@kindelia.org)
- For Feedbacks, email [kind@kindelia.org](mailto:kind@kindelia.org)
- To ask questions and join our community, check our [Discord Server](https://discord.gg/kindelia).

3
crates/kind-derive/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-derive"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Derive generator the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
@ -11,4 +12,4 @@ kind-span = { path = "../kind-span", version = "0.1.0" }
kind-tree = { path = "../kind-tree", version = "0.1.0" }
kind-report = { path = "../kind-report", version = "0.1.0" }
fxhash = "0.2.1"
im-rc = "*"
im-rc = "15.1.0"

5
crates/kind-driver/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-driver"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Driver for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
@ -14,8 +15,8 @@ kind-report = { path = "../kind-report", version = "0.1.0" }
kind-checker = { path = "../kind-checker", version = "0.1.0" }
kind-pass = { path = "../kind-pass", version = "0.1.0" }
kind-target-hvm = { path = "../kind-target-hvm" }
kind-target-kdl = { path = "../kind-target-kdl" }
kind-target-hvm = { path = "../kind-target-hvm", version = "0.1.0" }
kind-target-kdl = { path = "../kind-target-kdl", version = "0.1.0" }
hvm = "1.0.0"

3
crates/kind-driver/src/lib.rs
View File

@ -4,7 +4,8 @@ use kind_pass::{desugar, erasure, inline::inline_book};
use kind_report::report::FileCache;
use kind_span::SyntaxCtxIndex;
use kind_tree::{backend, concrete, desugared, untyped};
use hvm::language::{syntax as backend};
use kind_tree::{concrete, desugared, untyped};
use resolution::ResolutionError;
use session::Session;
use std::{path::PathBuf};

1
crates/kind-parser/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-parser"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Parser for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

1
crates/kind-pass/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-pass"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "A lot of compiler passes for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

1
crates/kind-query/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-query"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Query module for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

1
crates/kind-report/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-report"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Report module for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

1
crates/kind-span/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-span"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Describes locations for the Kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

3
crates/kind-target-hvm/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-target-hvm"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "HVM Code generator for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
@ -12,4 +13,4 @@ kind-tree = { path = "../kind-tree", version = "0.1.0" }
kind-report = { path = "../kind-report", version = "0.1.0" }
kind-derive = { path = "../kind-derive", version = "0.1.0" }
hvm = { git = "https://github.com/Kindelia/HVM.git", rev="bd744430430a3ebeb69918572ed0be0a8dacb86a" }
hvm = "1.0.0"

7
crates/kind-target-hvm/src/lib.rs
View File

@ -1,9 +1,8 @@
use hvm::u60;
use kind_tree::{
backend::{File, Rule, Term},
untyped,
};
use kind_tree::untyped;
use hvm::syntax::{File, Rule, Term};
pub fn compile_book(book: untyped::Book, trace: bool) -> File {
let mut file = File {

3
crates/kind-target-kdl/Cargo.toml
View File

@ -3,6 +3,7 @@ name = "kind-target-kdl"
version = "0.1.0"
edition = "2021"
license = "MIT"
description = "KDL target for the kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
@ -12,7 +13,7 @@ kind-tree = { path = "../kind-tree", version = "0.1.0" }
kind-report = { path = "../kind-report", version = "0.1.0" }
kind-derive = { path = "../kind-derive", version = "0.1.0" }
kindelia_lang = { git = "https://github.com/developedby/Kindelia/", branch = "kdl-lang-crate" }
kindelia_lang = "0.1.7"
linked-hash-map = "0.5.6"
tiny-keccak = "2.0.2"
fxhash = "0.2.1"

40
crates/kind-target-kdl/src/compile.rs
View File

@ -3,6 +3,7 @@ use std::{fmt::Display, sync::mpsc::Sender};
use fxhash::FxHashMap;
use kind_report::data::Diagnostic;
use kind_tree::{symbol::QualifiedIdent, untyped};
use kindelia_lang::ast::Name;
use linked_hash_map::LinkedHashMap;
use tiny_keccak::Hasher;
@ -13,6 +14,31 @@ use crate::{diagnostic::KdlDiagnostic, GenericCompilationToHVMError};
pub const KDL_NAME_LEN: usize = 12;
const U60_MAX: kdl::U120 = kdl::U120(0xFFFFFFFFFFFFFFF);
fn char_to_code(chr: char) -> Result<u128, String> {
let num = match chr {
'.' => 0,
'0'..='9' => 1 + chr as u128 - '0' as u128,
'A'..='Z' => 11 + chr as u128 - 'A' as u128,
'a'..='z' => 37 + chr as u128 - 'a' as u128,
'_' => 63,
_ => {
return Err(format!("Invalid Kindelia Name letter '{}'.", chr));
}
};
Ok(num)
}
pub fn from_str(name_txt: &str) -> Result<Name, String> {
let mut num: u128 = 0;
for (i, chr) in name_txt.chars().enumerate() {
if i >= Name::MAX_CHARS {
return Err("Too big".to_string())
}
num = (num << 6) + char_to_code(chr)?;
}
Ok(Name(num))
}
#[derive(Debug)]
pub struct File {
pub ctrs: LinkedHashMap<String, kdl::Statement>,
@ -108,7 +134,7 @@ pub fn compile_book(
.map(|x| x.to_string())
.unwrap_or_else(|| name_shortener(&entry.name, namespace).to_string());
if let Ok(new_name) = kdl::Name::from_str(&new_name) {
if let Ok(new_name) = from_str(&new_name) {
ctx.kdl_names.insert(name.clone(), new_name);
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(entry.name.range)));
@ -329,7 +355,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
body,
erased: _,
} => {
let name = kdl::Name::from_str(param.to_str());
let name = from_str(param.to_str());
if let Ok(name) = name {
let body = Box::new(compile_expr(ctx, body));
To::Lam { name, body }
@ -339,7 +365,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
}
}
From::Let { name, val, next } => {
let res_name = kdl::Name::from_str(name.to_str());
let res_name = from_str(name.to_str());
if let Ok(name) = res_name {
let expr = Box::new(compile_expr(ctx, next));
let func = Box::new(To::Lam { name, body: expr });
@ -358,7 +384,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
err_term()
}
From::Var { name } => {
let res_name = kdl::Name::from_str(name.to_str());
let res_name = from_str(name.to_str());
if let Ok(name) = res_name {
To::Var { name }
} else {
@ -418,7 +444,7 @@ fn compile_common_function(ctx: &mut CompileCtx, entry: &untyped::Entry) {
let mut args = Vec::new();
for (name, range, _strictness) in &entry.args {
if let Ok(name) = kdl::Name::from_str(name) {
if let Ok(name) = from_str(name) {
args.push(name)
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(*range)));
@ -476,8 +502,8 @@ fn compile_common_function(ctx: &mut CompileCtx, entry: &untyped::Entry) {
fn compile_u120_new(ctx: &mut CompileCtx, entry: &untyped::Entry) {
// U120.new hi lo = (hi << 60) | lo
let hi_name = kdl::Name::from_str("hi").unwrap();
let lo_name = kdl::Name::from_str("lo").unwrap();
let hi_name = kdl::Name::from_str_unsafe("hi");
let lo_name = kdl::Name::from_str_unsafe("lo");
let hi_var = kdl::Term::Var {
name: hi_name.clone(),
};

16
crates/kind-target-kdl/src/linearize.rs
View File

@ -24,7 +24,7 @@ pub struct LinearizeCtx {
impl LinearizeCtx {
fn create_name(&mut self) -> Name {
let name = Name::from_str(&format!("x{}", self.name_count)).unwrap();
let name = Name::from_str_unsafe(&format!("x{}", self.name_count));
self.name_count += 1;
name
}
@ -153,7 +153,7 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
.entry(*name)
.and_modify(|x| *x += 1)
.or_insert(1);
let name = Name::from_str(&format!("{}.{}", name, used - 1)).unwrap(); // TODO: Think if this errs or not
let name = Name::from_str_unsafe(&format!("{}.{}", name, used - 1)); // TODO: Think if this errs or not
Term::Var { name }
} else {
unreachable!("Unbound variable '{}' in kdl compilation", name.to_string());
@ -182,8 +182,8 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
if let Some(x) = got_1 {
ctx.name_table.insert(*nam1, x);
}
let nam0 = Name::from_str(&format!("{}{}", new_nam0, ".0")).unwrap();
let nam1 = Name::from_str(&format!("{}{}", new_nam1, ".0")).unwrap();
let nam0 = Name::from_str_unsafe(&format!("{}{}", new_nam0, ".0"));
let nam1 = Name::from_str_unsafe(&format!("{}{}", new_nam1, ".0"));
Term::Dup {
nam0,
nam1,
@ -274,7 +274,7 @@ pub fn dup_var(ctx: &mut LinearizeCtx, name: &Name, expr: Box<Term>, body: Box<T
0 => body,
// if used once just make a let (lambda then app)
1 => {
let name = Name::from_str(&format!("{}.0", name)).unwrap(); // TODO: handle err
let name = Name::from_str_unsafe(&format!("{}.0", name)); // TODO: handle err
let func = Box::new(Term::Lam { name, body });
let term = Term::App { func, argm: expr };
Box::new(term)
@ -287,12 +287,12 @@ pub fn dup_var(ctx: &mut LinearizeCtx, name: &Name, expr: Box<Term>, body: Box<T
// generate name for duplicated variables
for i in (aux_amount..(dup_times * 2)).rev() {
let i = i - aux_amount; // moved to 0,1,..
let key = Name::from_str(&format!("{}.{}", name, i)).unwrap();
let key = Name::from_str_unsafe(&format!("{}.{}", name, i));
vars.push(key);
}
// generate name for aux variables
for i in (0..aux_amount).rev() {
let key = Name::from_str(&format!("c.{}", i)).unwrap();
let key = Name::from_str_unsafe(&format!("c.{}", i));
vars.push(key);
}
// use aux variables to duplicate the variable
@ -318,7 +318,7 @@ fn dup_var_go(idx: u64, dup_times: u64, body: Box<Term>, vars: &mut Vec<Name>) -
} else {
let nam0 = vars.pop().unwrap();
let nam1 = vars.pop().unwrap();
let var_name = Name::from_str(&format!("c.{}", idx - 1)).unwrap();
let var_name = Name::from_str_unsafe(&format!("c.{}", idx - 1));
let expr = Box::new(Term::Var { name: var_name });
let dup = Term::Dup {
nam0,

3
crates/kind-tree/Cargo.toml
View File

@ -4,11 +4,10 @@ version = "0.1.0"
edition = "2021"
license = "MIT"
description = "Syntatic trees for Kind compiler"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
hvm = "1.0.0"
kind-span = { path = "../kind-span", version = "0.1.0" }
linked-hash-map = "0.5.6"
fxhash = "0.2.1"

1
crates/kind-tree/src/lib.rs
View File

@ -24,7 +24,6 @@ pub mod symbol;
use std::fmt::{Formatter, Display, Error};
pub use hvm::syntax as backend;
use symbol::Ident;
/// Attributes describes some compiler specific aspects