diff --git a/crates/kind-parser/src/expr.rs b/crates/kind-parser/src/expr.rs index 21f00f7e..399308a3 100644 --- a/crates/kind-parser/src/expr.rs +++ b/crates/kind-parser/src/expr.rs @@ -91,16 +91,14 @@ impl<'a> Parser<'a> { && self.peek(2).same_variant(&Token::Colon) } - fn is_substitution(&self) -> bool { - self.get().same_variant(&Token::HashHash) - } - fn parse_substitution(&mut self) -> Result, SyntaxDiagnostic> { let start = self.range(); - self.advance(); // '##' + self.advance(); // 'specialize' let name = self.parse_id()?; - self.eat_variant(Token::Slash)?; + self.eat_id("into")?; + self.eat_variant(Token::Hash)?; let redx = self.parse_num_lit()?; + self.eat_id("in")?; let expr = self.parse_expr(false)?; let range = start.mix(expr.range); Ok(Box::new(Expr { @@ -129,7 +127,7 @@ impl<'a> Parser<'a> { Token::Num60(name) => Some(name.to_string()), _ => None, })?; - + let ident = Ident::new_static(&id, range); Ok(ident) } @@ -893,6 +891,8 @@ impl<'a> Parser<'a> { self.parse_if() } else if self.check_actual_id("open") { self.parse_open() + } else if self.check_actual_id("specialize") { + self.parse_substitution() } else if self.check_actual(Token::Dollar) { self.parse_sigma_pair() } else if self.is_lambda() { @@ -901,8 +901,6 @@ impl<'a> Parser<'a> { self.parse_pi_or_lambda(false) } else if self.is_sigma_type() { self.parse_sigma_type() - } else if self.is_substitution() { - self.parse_substitution() } else if self.check_actual(Token::Tilde) { self.parse_erased() } else { diff --git a/crates/kind-pass/src/unbound/mod.rs b/crates/kind-pass/src/unbound/mod.rs index f205b669..a41aba85 100644 --- a/crates/kind-pass/src/unbound/mod.rs +++ b/crates/kind-pass/src/unbound/mod.rs @@ -105,7 +105,12 @@ impl UnboundCollector { self.top_level_defs .insert(sum.name.get_root(), sum.name.range); - let res = sum.constructors.iter().map(|x| (x.name.to_string(), x.args.map(|x| x.name.to_string()).to_vec())); + let res = sum.constructors.iter().map(|x| { + ( + x.name.to_string(), + x.args.map(|x| x.name.to_string()).to_vec(), + ) + }); self.type_defs.insert(sum.name.to_string(), res.collect()); for cons in &sum.constructors { @@ -121,11 +126,18 @@ impl UnboundCollector { debug_assert!(rec.name.get_aux().is_none()); debug_assert!(name_cons.get_aux().is_none()); - self.record_defs.insert(rec.name.to_string(), rec.fields.iter().map(|x| x.0.to_string()).collect()); + self.record_defs.insert( + rec.name.to_string(), + rec.fields.iter().map(|x| x.0.to_string()).collect(), + ); let constructor = rec.get_constructor(); - let cons = (constructor.name.to_string(), constructor.args.map(|x| x.name.to_string()).to_vec()); - self.type_defs.insert(rec.name.to_string(), FxHashMap::from_iter([cons])); + let cons = ( + constructor.name.to_string(), + constructor.args.map(|x| x.name.to_string()).to_vec(), + ); + self.type_defs + .insert(rec.name.to_string(), FxHashMap::from_iter([cons])); self.top_level_defs .insert(rec.name.get_root(), rec.name.range); @@ -169,7 +181,10 @@ impl Visitor for UnboundCollector { if let Some(fst) = self.context_vars.iter().find(|x| x.1 == name) { if self.emit_errs { self.errors - .send(Box::new(PassDiagnostic::RepeatedVariable(fst.0, ident.0.range))) + .send(Box::new(PassDiagnostic::RepeatedVariable( + fst.0, + ident.0.range, + ))) .unwrap() } } else { @@ -239,16 +254,13 @@ impl Visitor for UnboundCollector { for cons in &entr.constructors { match repeated_names.get(&cons.name.to_string()) { + None => { + repeated_names.insert(cons.name.to_string(), cons.name.range); + }, Some(_) => { failed = true; } - None => { - repeated_names.insert(cons.name.to_string(), cons.name.range); - } } - let name_cons = entr.name.add_segment(cons.name.to_str()); - self.context_vars - .push((name_cons.range, name_cons.to_string())); } if failed { @@ -390,7 +402,7 @@ impl Visitor for UnboundCollector { fn visit_match(&mut self, matcher: &mut kind_tree::concrete::expr::Match) { self.visit_qualified_ident(&mut matcher.typ); - + for name in &mut matcher.with_vars { self.visit_ident(&mut name.0); if let Some(res) = &mut name.1 { @@ -400,7 +412,8 @@ impl Visitor for UnboundCollector { if let Some(opt) = &mut matcher.value { self.visit_expr(opt); - self.context_vars.push((matcher.scrutinee.range, matcher.scrutinee.to_string())) + self.context_vars + .push((matcher.scrutinee.range, matcher.scrutinee.to_string())) } else { self.visit_ident(&mut matcher.scrutinee); } @@ -531,9 +544,9 @@ impl Visitor for UnboundCollector { fst, snd, } => { - self.visit_qualified_ident(&mut QualifiedIdent::new_static( - "Sigma", None, expr.range, - ).to_generated()); + self.visit_qualified_ident( + &mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(), + ); self.visit_expr(fst); self.visit_expr(snd); } @@ -542,9 +555,9 @@ impl Visitor for UnboundCollector { fst, snd, } => { - self.visit_qualified_ident(&mut QualifiedIdent::new_static( - "Sigma", None, expr.range, - ).to_generated()); + self.visit_qualified_ident( + &mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(), + ); self.visit_expr(fst); self.context_vars.push((ident.range, ident.to_string())); self.visit_expr(snd); @@ -595,16 +608,22 @@ impl Visitor for UnboundCollector { visit_vec!(args.iter_mut(), arg => self.visit_expr(arg)); } - ExprKind::Open { type_name, var_name, motive, next } => { + ExprKind::Open { + type_name, + var_name, + motive, + next, + } => { self.visit_qualified_ident(type_name); if let Some(motive) = motive { self.visit_expr(motive) } - + if let Some(fields) = self.record_defs.get(type_name.to_str()) { for field in fields { - self.context_vars.push((var_name.range, format!("{}.{}", var_name, field))) + self.context_vars + .push((var_name.range, format!("{}.{}", var_name, field))) } } @@ -615,7 +634,7 @@ impl Visitor for UnboundCollector { self.context_vars.pop(); } } - }, + } } } } diff --git a/crates/kind-tests/suite/checker/Subst.golden b/crates/kind-tests/suite/checker/Subst.golden new file mode 100644 index 00000000..e901ce44 --- /dev/null +++ b/crates/kind-tests/suite/checker/Subst.golden @@ -0,0 +1,20 @@ + INFO Inspection. + + * Expected: U60 + + * Context: + * awoo : Type + * awoo = U60 + * uuuhuuul : (List awoo) + * uuuhuuul = (List.nil awoo) + * ooooooo : (List U60) + * ooooooo = uuuhuuul + + /--[suite/checker/Subst.kind2:11:5] + | + 10 | let ooooooo = specialize awoo into #0 in uuuhuuul + 11 | ? + | v + | \Here! + + diff --git a/crates/kind-tests/suite/checker/Subst.kind2 b/crates/kind-tests/suite/checker/Subst.kind2 new file mode 100644 index 00000000..f196f30f --- /dev/null +++ b/crates/kind-tests/suite/checker/Subst.kind2 @@ -0,0 +1,11 @@ +type List (a: Type) { + cons (x: a) (xs: List a) + nil +} + +Rei : U60 +Rei = + let awoo = U60 + let uuuhuuul = ([] :: List awoo) + let ooooooo = specialize awoo into #0 in uuuhuuul + ? \ No newline at end of file diff --git a/crates/kind-tests/suite/checker/SubstUnbound.golden b/crates/kind-tests/suite/checker/SubstUnbound.golden new file mode 100644 index 00000000..db814b93 --- /dev/null +++ b/crates/kind-tests/suite/checker/SubstUnbound.golden @@ -0,0 +1 @@ +Ok! \ No newline at end of file diff --git a/crates/kind-tests/suite/checker/SubstUnbound.kind2 b/crates/kind-tests/suite/checker/SubstUnbound.kind2 new file mode 100644 index 00000000..6b138edf --- /dev/null +++ b/crates/kind-tests/suite/checker/SubstUnbound.kind2 @@ -0,0 +1,68 @@ +// A lot of thing here is just to test the substition + +type List (t: Type) { + Cons (head: t) (tail: List t) + Nil +} + +type Tree (t: Type) { + Empty + Single (value: t) + Concat (left: Tree t) (right: Tree t) +} + +record JustATest (t: Type) { + fst: t + snd: t +} + +// Generates a random list +Randoms (s: U60) (n: U60) : List U60 +Randoms s 0 = List.Nil +Randoms s l = List.Cons s (Randoms (% (+ (* s 1664525) 1013904223) 4294967296) (- l 1)) + +// Sums all elements in a concatenation tree +Sum (tree: Tree U60) : U60 +Sum (Tree.Empty t) = 0 +Sum (Tree.Single t a) = a +Sum (Tree.Concat t a b) = (+ (Sum a) (Sum b)) + +//// The initial pivot +Pivot : U60 +Pivot = 2147483648 + +QSort (p: U60) (s: U60) (l: List U60): Tree U60 +QSort p s List.Nil = Tree.Empty +QSort p s (List.Cons x List.Nil) = Tree.Single x +QSort p s (List.Cons x xs) = Split p s (List.Cons x xs) List.Nil List.Nil + +//// Splits list in two partitions +Split (p: U60) (s: U60) (l: List U60) (min: List U60) (max: List U60) : Tree U60 +Split p s List.Nil min max = + let s = (>> s 1) + let min = (QSort (- p s) s min) + let max = (QSort (+ p s) s max) + Tree.Concat min max + +Split p s (List.Cons x xs) min max = + Place p s (< p x) x xs min max + +//// Moves element to its partition + +Place (p: U60) (s: U60) (y: U60) (x: U60) (xs: List U60) (min: List U60) (max: List U60) : Tree U60 +Place p s 0 x xs min max = Split p s xs (List.Cons x min) max +Place p s _ x xs min max = Split p s xs min (List.Cons x max) + +//// Sorts and sums n random numbers +Main : U60 +Main = + let list = Randoms 1 254 + Sum (QSort Pivot Pivot list) + +Entry : U60 +Entry = + let a = 2 + let b = 4 + let c = 5 + let d = 6 + specialize d into #0 in d diff --git a/crates/kind-tests/suite/issues/checker/ISSUE457.golden b/crates/kind-tests/suite/issues/checker/ISSUE-457.golden similarity index 83% rename from crates/kind-tests/suite/issues/checker/ISSUE457.golden rename to crates/kind-tests/suite/issues/checker/ISSUE-457.golden index 988e9564..cba984a4 100644 --- a/crates/kind-tests/suite/issues/checker/ISSUE457.golden +++ b/crates/kind-tests/suite/issues/checker/ISSUE-457.golden @@ -7,7 +7,7 @@ * n.fst : U60 * n.snd : U60 - /--[suite/issues/checker/ISSUE457.kind2:10:16] + /--[suite/issues/checker/ISSUE-457.kind2:10:16] | 9 | match Pair n { 10 | new => ? @@ -25,7 +25,7 @@ * n.fst : U60 * n.snd : U60 - /--[suite/issues/checker/ISSUE457.kind2:17:5] + /--[suite/issues/checker/ISSUE-457.kind2:17:5] | 16 | open Pair n 17 | ? @@ -43,7 +43,7 @@ * fst : U60 * snd : U60 - /--[suite/issues/checker/ISSUE457.kind2:22:5] + /--[suite/issues/checker/ISSUE-457.kind2:22:5] | 21 | let Pair.new fst snd = n 22 | ? diff --git a/crates/kind-tests/suite/issues/checker/ISSUE457.kind2 b/crates/kind-tests/suite/issues/checker/ISSUE-457.kind2 similarity index 100% rename from crates/kind-tests/suite/issues/checker/ISSUE457.kind2 rename to crates/kind-tests/suite/issues/checker/ISSUE-457.kind2 diff --git a/crates/kind-tests/suite/issues/checker/ISSUE-461.golden b/crates/kind-tests/suite/issues/checker/ISSUE-461.golden new file mode 100644 index 00000000..6ce0d713 --- /dev/null +++ b/crates/kind-tests/suite/issues/checker/ISSUE-461.golden @@ -0,0 +1,20 @@ + INFO Inspection. + + * Expected: U60 + + * Context: + * awoo : Type + * awoo = U60 + * uuuhuuul : (List awoo) + * uuuhuuul = (List.nil awoo) + * ooooooo : (List U60) + * ooooooo = uuuhuuul + + /--[suite/issues/checker/ISSUE-461.kind2:11:5] + | + 10 | let ooooooo = specialize awoo into #0 in uuuhuuul + 11 | ? + | v + | \Here! + + diff --git a/crates/kind-tests/suite/issues/checker/ISSUE-461.kind2 b/crates/kind-tests/suite/issues/checker/ISSUE-461.kind2 new file mode 100644 index 00000000..f196f30f --- /dev/null +++ b/crates/kind-tests/suite/issues/checker/ISSUE-461.kind2 @@ -0,0 +1,11 @@ +type List (a: Type) { + cons (x: a) (xs: List a) + nil +} + +Rei : U60 +Rei = + let awoo = U60 + let uuuhuuul = ([] :: List awoo) + let ooooooo = specialize awoo into #0 in uuuhuuul + ? \ No newline at end of file