diff --git a/Cargo.lock b/Cargo.lock index 1d98201d..179f85da 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -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", diff --git a/crates/kind-checker/src/compiler/mod.rs b/crates/kind-checker/src/compiler/mod.rs index af7ab379..a31075c0 100644 --- a/crates/kind-checker/src/compiler/mod.rs +++ b/crates/kind-checker/src/compiler/mod.rs @@ -91,16 +91,20 @@ fn mk_ctr_name_from_str(ident: &str) -> Box { mk_single_ctr(format!("{}.", ident)) } -fn range_to_num(range: Range) -> Box { - Box::new(Term::U6O { - numb: u60::new(range.encode().0), - }) +fn range_to_num(lhs: bool, range: Range) -> Box { + if lhs { + mk_var("orig") + } else { + Box::new(Term::U6O { + numb: u60::new(range.encode().0), + }) + } } fn set_origin(ident: &Ident) -> Box { 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::>>() ], ), @@ -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 Box(exprs: T) -> Box where - T: Iterator>, + T: DoubleEndedIterator>, { - 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 ], )], diff --git a/crates/kind-parser/src/expr.rs b/crates/kind-parser/src/expr.rs index 03b8aa3e..73a43078 100644 --- a/crates/kind-parser/src/expr.rs +++ b/crates/kind-parser/src/expr.rs @@ -288,6 +288,17 @@ impl<'a> Parser<'a> { })) } + fn parse_nat(&mut self, num: u128) -> Result, 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, 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), diff --git a/crates/kind-pass/src/desugar/expr.rs b/crates/kind-pass/src/desugar/expr.rs index 9de3cd48..356f404d 100644 --- a/crates/kind-pass/src/desugar/expr.rs +++ b/crates/kind-pass/src/desugar/expr.rs @@ -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); diff --git a/crates/kind-pass/src/lib.rs b/crates/kind-pass/src/lib.rs index 3c65f2e3..c57f7f57 100644 --- a/crates/kind-pass/src/lib.rs +++ b/crates/kind-pass/src/lib.rs @@ -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; diff --git a/crates/kind-tests/Teste.kind2 b/crates/kind-tests/Teste.kind2 deleted file mode 100644 index b02617b2..00000000 --- a/crates/kind-tests/Teste.kind2 +++ /dev/null @@ -1,2 +0,0 @@ -Main : U60 -Main = HVM.log 222 2 \ No newline at end of file diff --git a/crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.golden b/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden similarity index 83% rename from crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.golden rename to crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden index 03404ae8..77387559 100644 --- a/crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.golden +++ b/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden @@ -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) = ? diff --git a/crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.kind2 b/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.kind2 similarity index 100% rename from crates/kind-tests/suite/checker/issues/HvmReducesTooMuch.kind2 rename to crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.kind2 diff --git a/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden b/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden similarity index 84% rename from crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden rename to crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden index 92cce827..b225f210 100644 --- a/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden +++ b/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden @@ -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------ diff --git a/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.kind2 b/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.kind2 similarity index 100% rename from crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.kind2 rename to crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.kind2 diff --git a/crates/kind-tests/suite/checker/issues/RecordFieldDependency.golden b/crates/kind-tests/suite/issues/checker/RecordFieldDependency.golden similarity index 100% rename from crates/kind-tests/suite/checker/issues/RecordFieldDependency.golden rename to crates/kind-tests/suite/issues/checker/RecordFieldDependency.golden diff --git a/crates/kind-tests/suite/checker/issues/RecordFieldDependency.kind2 b/crates/kind-tests/suite/issues/checker/RecordFieldDependency.kind2 similarity index 100% rename from crates/kind-tests/suite/checker/issues/RecordFieldDependency.kind2 rename to crates/kind-tests/suite/issues/checker/RecordFieldDependency.kind2 diff --git a/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden b/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden new file mode 100644 index 00000000..44eb6e03 --- /dev/null +++ b/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden @@ -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 | + + diff --git a/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.kind2 b/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.kind2 new file mode 100644 index 00000000..a15f8e24 --- /dev/null +++ b/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.kind2 @@ -0,0 +1,28 @@ +Doit3times (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 (a: t) (b: t) : Type diff --git a/crates/kind-tests/suite/eval/issues/CallStr.golden b/crates/kind-tests/suite/issues/eval/CallStr.golden similarity index 100% rename from crates/kind-tests/suite/eval/issues/CallStr.golden rename to crates/kind-tests/suite/issues/eval/CallStr.golden diff --git a/crates/kind-tests/suite/eval/issues/CallStr.kind2 b/crates/kind-tests/suite/issues/eval/CallStr.kind2 similarity index 100% rename from crates/kind-tests/suite/eval/issues/CallStr.kind2 rename to crates/kind-tests/suite/issues/eval/CallStr.kind2 diff --git a/crates/kind-tests/tests/mod.rs b/crates/kind-tests/tests/mod.rs index 5b561a4e..c9c83ad7 100644 --- a/crates/kind-tests/tests/mod.rs +++ b/crates/kind-tests/tests/mod.rs @@ -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> { diff --git a/crates/kind-tree/src/concrete/expr.rs b/crates/kind-tree/src/concrete/expr.rs index ef259888..c5ce7ba1 100644 --- a/crates/kind-tree/src/concrete/expr.rs +++ b/crates/kind-tree/src/concrete/expr.rs @@ -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) } diff --git a/crates/kind-tree/src/desugared/mod.rs b/crates/kind-tree/src/desugared/mod.rs index 60a43b53..f88c49af 100644 --- a/crates/kind-tree/src/desugared/mod.rs +++ b/crates/kind-tree/src/desugared/mod.rs @@ -375,6 +375,21 @@ impl Display for AppBinding { } } +pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box], acc: u128) -> Option { + 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::() ), 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::() - ) + if args.is_empty() { + write!(f, "{}", name) + } else { + write!( + f, + "({}{})", + name, + args.iter().map(|x| format!(" {}", x)).collect::() + ) + } } } Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),