HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-08-15 19:30:41 +03:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #435 from Kindelia/experimental

Browse Source 
fix: problem with u60 term in rule side and added Nat syntax sugar
This commit is contained in:
Felipe G 2022-12-05 09:39:13 -03:00 committed by GitHub
commit 2a4fda284c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
19 changed files with 170 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
Cargo.lock generated
View File

@ -512,8 +512,8 @@ dependencies = [
[[package]]
name = "hvm"
version = "1.0.9-beta"
source = "git+https://github.com/Kindelia/HVM.git#bd744430430a3ebeb69918572ed0be0a8dacb86a"
version = "1.0.12-beta"
source = "git+https://github.com/Kindelia/HVM.git#2a99dd6cee91c0f6af949db792ac2b128295c4af"
dependencies = [
"backtrace",
"clap 3.2.23",
@ -659,7 +659,7 @@ name = "kind-checker"
version = "0.1.0"
dependencies = [
"fxhash",
"hvm 1.0.9-beta (git+https://github.com/Kindelia/HVM.git)",
"hvm 1.0.12-beta",
"im-rc",
"kind-report",
"kind-span",
@ -668,7 +668,7 @@ dependencies = [
[[package]]
name = "kind-cli"
version = "0.3.1"
version = "0.3.2"
dependencies = [
"anyhow",
"clap 4.0.29",
@ -697,7 +697,7 @@ dependencies = [
"anyhow",
"dashmap",
"fxhash",
"hvm 1.0.9-beta (git+https://github.com/Kindelia/HVM.git)",
"hvm 1.0.12-beta",
"kind-checker",
"kind-parser",
"kind-pass",
@ -768,7 +768,7 @@ version = "0.1.0"
name = "kind-target-hvm"
version = "0.1.0"
dependencies = [
"hvm 1.0.9-beta (git+https://github.com/Kindelia/HVM.git?rev=bd744430430a3ebeb69918572ed0be0a8dacb86a)",
"hvm 1.0.9-beta",
"kind-derive",
"kind-report",
"kind-span",
@ -812,7 +812,7 @@ name = "kind-tree"
version = "0.1.0"
dependencies = [
"fxhash",
"hvm 1.0.9-beta (git+https://github.com/Kindelia/HVM.git)",
"hvm 1.0.12-beta",
"kind-span",
"linked-hash-map",
]
@ -843,9 +843,9 @@ dependencies = [
[[package]]
name = "libc"
version = "0.2.137"
version = "0.2.138"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "fc7fcc620a3bff7cdd7a365be3376c97191aeaccc2a603e600951e452615bf89"
checksum = "db6d7e329c562c5dfab7a46a2afabc8b987ab9a4834c9d1ca04dc54c1546cef8"
[[package]]
name = "linked-hash-map"
@ -1394,18 +1394,18 @@ dependencies = [
[[package]]
name = "serde"
version = "1.0.148"
version = "1.0.149"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e53f64bb4ba0191d6d0676e1b141ca55047d83b74f5607e6d8eb88126c52c2dc"
checksum = "256b9932320c590e707b94576e3cc1f7c9024d0ee6612dfbcf1cb106cbe8e055"
dependencies = [
"serde_derive",
]
[[package]]
name = "serde_derive"
version = "1.0.148"
version = "1.0.149"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a55492425aa53521babf6137309e7d34c20bbfbbfcfe2c7f3a047fd1f6b92c0c"
checksum = "b4eae9b04cbffdfd550eb462ed33bc6a1b68c935127d008b27444d08380f94e4"
dependencies = [
"proc-macro2",
"quote",

54
crates/kind-checker/src/compiler/mod.rs
View File

@ -91,16 +91,20 @@ fn mk_ctr_name_from_str(ident: &str) -> Box<Term> {
mk_single_ctr(format!("{}.", ident))
}
fn range_to_num(range: Range) -> Box<Term> {
Box::new(Term::U6O {
numb: u60::new(range.encode().0),
})
fn range_to_num(lhs: bool, range: Range) -> Box<Term> {
if lhs {
mk_var("orig")
} else {
Box::new(Term::U6O {
numb: u60::new(range.encode().0),
})
}
}
fn set_origin(ident: &Ident) -> Box<Term> {
mk_lifted_ctr(
"Kind.Term.set_origin".to_owned(),
vec![range_to_num(ident.range), mk_var(ident.to_str())],
vec![range_to_num(false, ident.range), mk_var(ident.to_str())],
)
}
@ -153,11 +157,11 @@ fn codegen_all_expr(
match &expr.data {
Typ => mk_lifted_ctr(
eval_ctr(quote, TermTag::Typ),
vec![range_to_num(expr.range)],
vec![range_to_num(lhs, expr.range)],
),
NumTypeU60 => mk_lifted_ctr(
eval_ctr(quote, TermTag::U60),
vec![range_to_num(expr.range)],
vec![range_to_num(lhs, expr.range)],
),
NumTypeF60 => todo!(),
Var { name } => {
@ -168,7 +172,7 @@ fn codegen_all_expr(
mk_lifted_ctr(
eval_ctr(quote, TermTag::Var),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
mk_u60(name.encode()),
mk_u60((*num - 1) as u64),
],
@ -185,7 +189,7 @@ fn codegen_all_expr(
} => mk_lifted_ctr(
eval_ctr(quote, TermTag::All),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
mk_u60(param.encode()),
codegen_all_expr(lhs_rule, lhs, num, quote, typ),
lam(param, codegen_all_expr(lhs_rule, lhs, num, quote, body)),
@ -198,7 +202,7 @@ fn codegen_all_expr(
} => mk_lifted_ctr(
eval_ctr(quote, TermTag::Lambda),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
mk_u60(param.encode()),
lam(param, codegen_all_expr(lhs_rule, lhs, num, quote, body)),
],
@ -209,7 +213,7 @@ fn codegen_all_expr(
mk_lifted_ctr(
eval_ctr(quote, TermTag::App),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
left,
codegen_all_expr(lhs_rule, lhs, num, quote, &right.data),
],
@ -220,7 +224,7 @@ fn codegen_all_expr(
eval_ctr(quote, TermTag::Ctr(args.len())),
vec_preppend![
mk_ctr_name(name),
if lhs { mk_var("orig") } else { range_to_num(expr.range) };
range_to_num(lhs, expr.range);
args.iter().cloned().map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)).collect::<Vec<Box<Term>>>()
],
),
@ -235,7 +239,7 @@ fn codegen_all_expr(
eval_ctr(quote, TermTag::Fun(new_spine.len())),
vec_preppend![
mk_ctr_name(name),
range_to_num(expr.range);
range_to_num(lhs, expr.range);
new_spine
],
)
@ -243,7 +247,7 @@ fn codegen_all_expr(
mk_ctr(
TermTag::HoasF(name.to_string()).to_string(),
vec_preppend![
range_to_num(expr.range);
range_to_num(lhs, expr.range);
new_spine
],
)
@ -252,7 +256,7 @@ fn codegen_all_expr(
Let { name, val, next } => mk_ctr(
eval_ctr(quote, TermTag::Let),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
mk_u60(name.encode()),
codegen_all_expr(lhs_rule, lhs, num, quote, val),
lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, next)),
@ -261,7 +265,7 @@ fn codegen_all_expr(
Ann { expr, typ } => mk_ctr(
eval_ctr(quote, TermTag::Ann),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
codegen_all_expr(lhs_rule, lhs, num, quote, expr),
codegen_all_expr(lhs_rule, lhs, num, quote, typ),
],
@ -274,7 +278,7 @@ fn codegen_all_expr(
} => mk_ctr(
eval_ctr(quote, TermTag::Sub),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
mk_u60(name.encode()),
mk_u60(*indx as u64),
mk_u60(*redx as u64),
@ -283,13 +287,13 @@ fn codegen_all_expr(
),
NumU60 { numb } => mk_lifted_ctr(
eval_ctr(quote, TermTag::NUMU60),
vec![range_to_num(expr.range), mk_u60(*numb)],
vec![range_to_num(lhs, expr.range), mk_u60(*numb)],
),
NumF60 { numb: _ } => todo!(),
Binary { op, left, right } => mk_lifted_ctr(
eval_ctr(quote, TermTag::Binary),
vec![
range_to_num(expr.range),
range_to_num(lhs, expr.range),
mk_single_ctr(operator_to_constructor(*op).to_owned()),
codegen_all_expr(lhs_rule, lhs, num, quote, left),
codegen_all_expr(lhs_rule, lhs, num, quote, right),
@ -297,12 +301,12 @@ fn codegen_all_expr(
),
Hole { num } => mk_lifted_ctr(
eval_ctr(quote, TermTag::Hole),
vec![range_to_num(expr.range), mk_u60(*num)],
vec![range_to_num(lhs, expr.range), mk_u60(*num)],
),
Str { val } => codegen_all_expr(lhs_rule, lhs, num, quote, &desugar_str(val, expr.range)),
Hlp(_) => mk_lifted_ctr(
eval_ctr(quote, TermTag::Hlp),
vec![range_to_num(expr.range)],
vec![range_to_num(lhs, expr.range)],
),
Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"),
}
@ -322,7 +326,7 @@ fn codegen_type(args: &[desugared::Argument], typ: &desugared::Expr) -> Box<lang
mk_lifted_ctr(
eval_ctr(true, TermTag::All),
vec![
range_to_num(arg.range),
range_to_num(false, arg.range),
mk_u60(arg.name.encode()),
codegen_expr(true, &arg.typ),
lam(&arg.name, codegen_type(&args[1..], typ)),
@ -335,9 +339,9 @@ fn codegen_type(args: &[desugared::Argument], typ: &desugared::Expr) -> Box<lang
fn codegen_vec<T>(exprs: T) -> Box<Term>
where
T: Iterator<Item = Box<Term>>,
T: DoubleEndedIterator<Item = Box<Term>>,
{
exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| {
exprs.rfold(mk_ctr("List.nil".to_string(), vec![]), |left, right| {
mk_ctr("List.cons".to_string(), vec![right, left])
})
}
@ -452,7 +456,7 @@ fn codegen_entry_rules(
format!("QT{}", index),
vec_preppend![
mk_ctr_name(&entry.name),
range_to_num(entry.range);
range_to_num(false, entry.range);
args
],
)],

12
crates/kind-parser/src/expr.rs
View File

@ -288,6 +288,17 @@ impl<'a> Parser<'a> {
}))
}
fn parse_nat(&mut self, num: u128) -> Result<Box<Expr>, SyntaxDiagnostic> {
let range = self.range();
self.advance();
Ok(Box::new(Expr {
range,
data: ExprKind::Lit {
lit: Literal::Nat(num),
},
}))
}
fn parse_num120(&mut self, num: u128) -> Result<Box<Expr>, SyntaxDiagnostic> {
let range = self.range();
self.advance();
@ -426,6 +437,7 @@ impl<'a> Parser<'a> {
Token::UpperId(_, _) => self.parse_single_upper(),
Token::LowerId(_) => self.parse_var(),
Token::Num60(num) => self.parse_num60(num),
Token::Nat(num) => self.parse_nat(num),
Token::Num120(num) => self.parse_num120(num),
Token::Char(chr) => self.parse_char(chr),
Token::Str(str) => self.parse_str(str),

13
crates/kind-pass/src/desugar/expr.rs
View File

@ -36,6 +36,19 @@ impl<'a> DesugarState<'a> {
Literal::NumTypeU60 => desugared::Expr::type_u60(range),
Literal::NumTypeF60 => desugared::Expr::type_f60(range),
Literal::NumU60(num) => desugared::Expr::num_u60(range, *num),
Literal::Nat(num) => {
let list_ident = QualifiedIdent::new_static("Nat", None, range);
let cons_ident = list_ident.add_segment("succ");
let nil_ident = list_ident.add_segment("zero");
let mut res = self.mk_desugared_ctr(range, nil_ident, Vec::new(), false);
for _ in 0..*num {
res = self.mk_desugared_ctr(range, cons_ident.clone(), vec![res], false)
}
res
},
Literal::NumU120(num) => {
if !self.check_implementation("U120.new", range, Sugar::U120) {
return desugared::Expr::err(range);

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

@ -1,8 +1,9 @@
//! A lot of transformations that we can apply into kind trees.
//! * [desugar][desugar] - That desugars the sugared tree into a version that does not contain a lot of constructions like match, inductive types etc.
//! * [erasure][erasure] - Erases all of the definitions that are marked as erased from the runtime.
//! * [expand][expand] - Expand some attributes and derivations of each construction.
//! * [expand][expand] - Expand some attributes and derivations of each construction.
//! * [unbound][unbound] - Collects all of the unbound definitions and check the linearity of them.
//! * [inline][inline] - Inlines expressions
pub mod desugar;
pub mod erasure;

2
crates/kind-tests/Teste.kind2
View File

@ -1,2 +0,0 @@
Main : U60
Main = HVM.log 222 2

2
crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.golden → crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden
View File

@ -5,7 +5,7 @@
* Context:
* n : Nat
/--[suite/checker/issues/HvmReducesTooMuch.kind2:13:29]
/--[suite/issues/checker/HvmReducesTooMuch.kind2:13:29]
|
12 | Beq_nat_refl (n: Nat) : Assert (Nat.count_layers n 0)
13 | Beq_nat_refl (Nat.succ n) = ?

0
crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.kind2 → crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.kind2
View File

4
crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden → crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden
View File

@ -1,6 +1,6 @@
ERROR Data constructors cannot return function types.
/--[suite/checker/issues/MatchDerivationWithAll.kind2:3:10]
/--[suite/issues/checker/MatchDerivationWithAll.kind2:3:10]
|
2 | type WithCtx (a: Type) {
3 | new: U60 -> (WithCtx a)
@ -12,7 +12,7 @@
ERROR This is not the type that is being declared.
/--[suite/checker/issues/MatchDerivationWithAll.kind2:2:6]
/--[suite/issues/checker/MatchDerivationWithAll.kind2:2:6]
|
2 | type WithCtx (a: Type) {
| v------

0
crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.kind2 → crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.kind2
View File

0
crates/kind-tests/suite/checker/issues/RecordFieldDependency.golden → crates/kind-tests/suite/issues/checker/RecordFieldDependency.golden
View File

0
crates/kind-tests/suite/checker/issues/RecordFieldDependency.kind2 → crates/kind-tests/suite/issues/checker/RecordFieldDependency.kind2
View File

14
crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden Normal file
View File

@ -0,0 +1,14 @@
INFO Inspection.
* Expected: (Equal _ 2n 5n)
/--[suite/issues/checker/U60ToNatDoesNotReduce.kind2:26:17]
|
25 | Test_anon_fun : (Equal (Nat.succ (Nat.succ (Nat.zero))) (U60.to_nat 5))
26 | Test_anon_fun = ?
| v
| \Here!
27 |

28
crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.kind2 Normal file
View File

@ -0,0 +1,28 @@
Doit3times <x> (f: (x -> x)) (n: x) : x
Doit3times f n = (f (f (f n)))
Nat.zero : (Nat)
U60.to_nat (x: U60) : (Nat)
U60.to_nat 0 = (Nat.zero)
U60.to_nat n = (Nat.succ (U60.to_nat (- n 1)))
Nat.add (a: (Nat)) (b: (Nat)) : (Nat)
Nat.add (Nat.succ a) b = (Nat.succ (Nat.add a b))
Nat.add (Nat.zero) b = b
Nat.succ (pred: (Nat)) : (Nat)
Nat : Type
Main : _
Main = (let a = (Doit3times ((x => (Nat.mul x x)) :: Nat -> Nat) (U60.to_nat 2)); a)
Nat.mul (a: (Nat)) (b: (Nat)) : (Nat)
Nat.mul (Nat.succ a) b = (Nat.add (Nat.mul a b) b)
Nat.mul (Nat.zero) b = (Nat.zero)
Test_anon_fun : (Equal (Nat.succ (Nat.succ (Nat.zero))) (U60.to_nat 5))
Test_anon_fun = ?
Equal <t> (a: t) (b: t) : Type

0
crates/kind-tests/suite/eval/issues/CallStr.golden → crates/kind-tests/suite/issues/eval/CallStr.golden
View File

0
crates/kind-tests/suite/eval/issues/CallStr.kind2 → crates/kind-tests/suite/issues/eval/CallStr.kind2
View File

25
crates/kind-tests/tests/mod.rs
View File

@ -71,6 +71,17 @@ fn test_checker() -> Result<(), Error> {
Ok(())
}
#[test]
#[timeout(30000)]
fn test_checker_issues() -> Result<(), Error> {
test_kind2(Path::new("./suite/issues/checker"), |path, session| {
let entrypoints = vec!["Main".to_string()];
let check = driver::type_check_book(session, path, entrypoints, Some(1));
check.map(|_| "Ok!".to_string()).ok()
})?;
Ok(())
}
#[test]
#[timeout(15000)]
fn test_eval() -> Result<(), Error> {
@ -85,6 +96,20 @@ fn test_eval() -> Result<(), Error> {
Ok(())
}
#[test]
#[timeout(15000)]
fn test_eval_issues() -> Result<(), Error> {
test_kind2(Path::new("./suite/issues/eval"), |path, session| {
let entrypoints = vec!["Main".to_string()];
let check = driver::erase_book(session, path, entrypoints)
.map(|file| driver::compile_book_to_hvm(file, false))
.map(|file| driver::execute_file(&file.to_string(), Some(1)).map_or_else(|e| e, |f| f));
check.ok()
})?;
Ok(())
}
#[test]
#[timeout(15000)]
fn test_kdl() -> Result<(), Error> {

5
crates/kind-tree/src/concrete/expr.rs
View File

@ -101,6 +101,8 @@ pub enum Literal {
NumU120(u128),
// A 60 bit floating point number literal
NumF60(u64),
// Naturals represented by u128
Nat(u128),
// A String literal
String(String),
}
@ -374,8 +376,9 @@ impl Display for Literal {
Literal::NumTypeF60 => write!(f, "F60"),
Literal::Char(c) => write!(f, "'{}'", c),
Literal::NumU60(numb) => write!(f, "{}", numb),
Literal::NumF60(_numb) => todo!(),
Literal::Nat(numb) => write!(f, "{}numb", numb),
Literal::NumU120(numb) => write!(f, "{}u120", numb),
Literal::NumF60(numb) => write!(f, "{}f60", numb),
Literal::String(str) => {
write!(f, "{:?}", str)
}

35
crates/kind-tree/src/desugared/mod.rs
View File

@ -375,6 +375,21 @@ impl Display for AppBinding {
}
}
pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box<Expr>], acc: u128) -> Option<u128> {
match name.to_str() {
"Nat.zero" if spine.len() == 0 => {
Some(acc)
}
"Nat.succ" if spine.len() == 1 => {
match &spine[0].data {
ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1),
_ => None
}
}
_ => None
}
}
impl Display for Expr {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
use ExprKind::*;
@ -407,15 +422,19 @@ impl Display for Expr {
args.iter().map(|x| format!(" {}", x)).collect::<String>()
),
Fun { name, args } | Ctr { name, args } => {
if args.is_empty() {
write!(f, "{}", name)
if let Some(res) = try_desugar_to_nat(name, args, 0) {
write!(f, "{res}n")
} else {
write!(
f,
"({}{})",
name,
args.iter().map(|x| format!(" {}", x)).collect::<String>()
)
if args.is_empty() {
write!(f, "{}", name)
} else {
write!(
f,
"({}{})",
name,
args.iter().map(|x| format!(" {}", x)).collect::<String>()
)
}
}
}
Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),