mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Merge pull request #462 from felipegchi/experimental-specialize
Fixed specialization
This commit is contained in:
commit
27220f835a
@ -91,16 +91,14 @@ impl<'a> Parser<'a> {
|
|||||||
&& self.peek(2).same_variant(&Token::Colon)
|
&& self.peek(2).same_variant(&Token::Colon)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn is_substitution(&self) -> bool {
|
|
||||||
self.get().same_variant(&Token::HashHash)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn parse_substitution(&mut self) -> Result<Box<Expr>, SyntaxDiagnostic> {
|
fn parse_substitution(&mut self) -> Result<Box<Expr>, SyntaxDiagnostic> {
|
||||||
let start = self.range();
|
let start = self.range();
|
||||||
self.advance(); // '##'
|
self.advance(); // 'specialize'
|
||||||
let name = self.parse_id()?;
|
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()?;
|
let redx = self.parse_num_lit()?;
|
||||||
|
self.eat_id("in")?;
|
||||||
let expr = self.parse_expr(false)?;
|
let expr = self.parse_expr(false)?;
|
||||||
let range = start.mix(expr.range);
|
let range = start.mix(expr.range);
|
||||||
Ok(Box::new(Expr {
|
Ok(Box::new(Expr {
|
||||||
@ -129,7 +127,7 @@ impl<'a> Parser<'a> {
|
|||||||
Token::Num60(name) => Some(name.to_string()),
|
Token::Num60(name) => Some(name.to_string()),
|
||||||
_ => None,
|
_ => None,
|
||||||
})?;
|
})?;
|
||||||
|
|
||||||
let ident = Ident::new_static(&id, range);
|
let ident = Ident::new_static(&id, range);
|
||||||
Ok(ident)
|
Ok(ident)
|
||||||
}
|
}
|
||||||
@ -893,6 +891,8 @@ impl<'a> Parser<'a> {
|
|||||||
self.parse_if()
|
self.parse_if()
|
||||||
} else if self.check_actual_id("open") {
|
} else if self.check_actual_id("open") {
|
||||||
self.parse_open()
|
self.parse_open()
|
||||||
|
} else if self.check_actual_id("specialize") {
|
||||||
|
self.parse_substitution()
|
||||||
} else if self.check_actual(Token::Dollar) {
|
} else if self.check_actual(Token::Dollar) {
|
||||||
self.parse_sigma_pair()
|
self.parse_sigma_pair()
|
||||||
} else if self.is_lambda() {
|
} else if self.is_lambda() {
|
||||||
@ -901,8 +901,6 @@ impl<'a> Parser<'a> {
|
|||||||
self.parse_pi_or_lambda(false)
|
self.parse_pi_or_lambda(false)
|
||||||
} else if self.is_sigma_type() {
|
} else if self.is_sigma_type() {
|
||||||
self.parse_sigma_type()
|
self.parse_sigma_type()
|
||||||
} else if self.is_substitution() {
|
|
||||||
self.parse_substitution()
|
|
||||||
} else if self.check_actual(Token::Tilde) {
|
} else if self.check_actual(Token::Tilde) {
|
||||||
self.parse_erased()
|
self.parse_erased()
|
||||||
} else {
|
} else {
|
||||||
|
@ -105,7 +105,12 @@ impl UnboundCollector {
|
|||||||
self.top_level_defs
|
self.top_level_defs
|
||||||
.insert(sum.name.get_root(), sum.name.range);
|
.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());
|
self.type_defs.insert(sum.name.to_string(), res.collect());
|
||||||
|
|
||||||
for cons in &sum.constructors {
|
for cons in &sum.constructors {
|
||||||
@ -121,11 +126,18 @@ impl UnboundCollector {
|
|||||||
debug_assert!(rec.name.get_aux().is_none());
|
debug_assert!(rec.name.get_aux().is_none());
|
||||||
debug_assert!(name_cons.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 constructor = rec.get_constructor();
|
||||||
|
|
||||||
let cons = (constructor.name.to_string(), constructor.args.map(|x| x.name.to_string()).to_vec());
|
let cons = (
|
||||||
self.type_defs.insert(rec.name.to_string(), FxHashMap::from_iter([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
|
self.top_level_defs
|
||||||
.insert(rec.name.get_root(), rec.name.range);
|
.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 let Some(fst) = self.context_vars.iter().find(|x| x.1 == name) {
|
||||||
if self.emit_errs {
|
if self.emit_errs {
|
||||||
self.errors
|
self.errors
|
||||||
.send(Box::new(PassDiagnostic::RepeatedVariable(fst.0, ident.0.range)))
|
.send(Box::new(PassDiagnostic::RepeatedVariable(
|
||||||
|
fst.0,
|
||||||
|
ident.0.range,
|
||||||
|
)))
|
||||||
.unwrap()
|
.unwrap()
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
@ -239,16 +254,13 @@ impl Visitor for UnboundCollector {
|
|||||||
|
|
||||||
for cons in &entr.constructors {
|
for cons in &entr.constructors {
|
||||||
match repeated_names.get(&cons.name.to_string()) {
|
match repeated_names.get(&cons.name.to_string()) {
|
||||||
|
None => {
|
||||||
|
repeated_names.insert(cons.name.to_string(), cons.name.range);
|
||||||
|
},
|
||||||
Some(_) => {
|
Some(_) => {
|
||||||
failed = true;
|
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 {
|
if failed {
|
||||||
@ -390,7 +402,7 @@ impl Visitor for UnboundCollector {
|
|||||||
|
|
||||||
fn visit_match(&mut self, matcher: &mut kind_tree::concrete::expr::Match) {
|
fn visit_match(&mut self, matcher: &mut kind_tree::concrete::expr::Match) {
|
||||||
self.visit_qualified_ident(&mut matcher.typ);
|
self.visit_qualified_ident(&mut matcher.typ);
|
||||||
|
|
||||||
for name in &mut matcher.with_vars {
|
for name in &mut matcher.with_vars {
|
||||||
self.visit_ident(&mut name.0);
|
self.visit_ident(&mut name.0);
|
||||||
if let Some(res) = &mut name.1 {
|
if let Some(res) = &mut name.1 {
|
||||||
@ -400,7 +412,8 @@ impl Visitor for UnboundCollector {
|
|||||||
|
|
||||||
if let Some(opt) = &mut matcher.value {
|
if let Some(opt) = &mut matcher.value {
|
||||||
self.visit_expr(opt);
|
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 {
|
} else {
|
||||||
self.visit_ident(&mut matcher.scrutinee);
|
self.visit_ident(&mut matcher.scrutinee);
|
||||||
}
|
}
|
||||||
@ -531,9 +544,9 @@ impl Visitor for UnboundCollector {
|
|||||||
fst,
|
fst,
|
||||||
snd,
|
snd,
|
||||||
} => {
|
} => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
|
self.visit_qualified_ident(
|
||||||
"Sigma", None, expr.range,
|
&mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(),
|
||||||
).to_generated());
|
);
|
||||||
self.visit_expr(fst);
|
self.visit_expr(fst);
|
||||||
self.visit_expr(snd);
|
self.visit_expr(snd);
|
||||||
}
|
}
|
||||||
@ -542,9 +555,9 @@ impl Visitor for UnboundCollector {
|
|||||||
fst,
|
fst,
|
||||||
snd,
|
snd,
|
||||||
} => {
|
} => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
|
self.visit_qualified_ident(
|
||||||
"Sigma", None, expr.range,
|
&mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(),
|
||||||
).to_generated());
|
);
|
||||||
self.visit_expr(fst);
|
self.visit_expr(fst);
|
||||||
self.context_vars.push((ident.range, ident.to_string()));
|
self.context_vars.push((ident.range, ident.to_string()));
|
||||||
self.visit_expr(snd);
|
self.visit_expr(snd);
|
||||||
@ -595,16 +608,22 @@ impl Visitor for UnboundCollector {
|
|||||||
|
|
||||||
visit_vec!(args.iter_mut(), arg => self.visit_expr(arg));
|
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);
|
self.visit_qualified_ident(type_name);
|
||||||
|
|
||||||
if let Some(motive) = motive {
|
if let Some(motive) = motive {
|
||||||
self.visit_expr(motive)
|
self.visit_expr(motive)
|
||||||
}
|
}
|
||||||
|
|
||||||
if let Some(fields) = self.record_defs.get(type_name.to_str()) {
|
if let Some(fields) = self.record_defs.get(type_name.to_str()) {
|
||||||
for field in fields {
|
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();
|
self.context_vars.pop();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
},
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
20
crates/kind-tests/suite/checker/Subst.golden
Normal file
20
crates/kind-tests/suite/checker/Subst.golden
Normal file
@ -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!
|
||||||
|
|
||||||
|
|
11
crates/kind-tests/suite/checker/Subst.kind2
Normal file
11
crates/kind-tests/suite/checker/Subst.kind2
Normal file
@ -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
|
||||||
|
?
|
1
crates/kind-tests/suite/checker/SubstUnbound.golden
Normal file
1
crates/kind-tests/suite/checker/SubstUnbound.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
Ok!
|
68
crates/kind-tests/suite/checker/SubstUnbound.kind2
Normal file
68
crates/kind-tests/suite/checker/SubstUnbound.kind2
Normal file
@ -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
|
@ -7,7 +7,7 @@
|
|||||||
* n.fst : U60
|
* n.fst : U60
|
||||||
* n.snd : U60
|
* n.snd : U60
|
||||||
|
|
||||||
/--[suite/issues/checker/ISSUE457.kind2:10:16]
|
/--[suite/issues/checker/ISSUE-457.kind2:10:16]
|
||||||
|
|
|
|
||||||
9 | match Pair n {
|
9 | match Pair n {
|
||||||
10 | new => ?
|
10 | new => ?
|
||||||
@ -25,7 +25,7 @@
|
|||||||
* n.fst : U60
|
* n.fst : U60
|
||||||
* n.snd : U60
|
* n.snd : U60
|
||||||
|
|
||||||
/--[suite/issues/checker/ISSUE457.kind2:17:5]
|
/--[suite/issues/checker/ISSUE-457.kind2:17:5]
|
||||||
|
|
|
|
||||||
16 | open Pair n
|
16 | open Pair n
|
||||||
17 | ?
|
17 | ?
|
||||||
@ -43,7 +43,7 @@
|
|||||||
* fst : U60
|
* fst : U60
|
||||||
* snd : 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
|
21 | let Pair.new fst snd = n
|
||||||
22 | ?
|
22 | ?
|
20
crates/kind-tests/suite/issues/checker/ISSUE-461.golden
Normal file
20
crates/kind-tests/suite/issues/checker/ISSUE-461.golden
Normal file
@ -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!
|
||||||
|
|
||||||
|
|
11
crates/kind-tests/suite/issues/checker/ISSUE-461.kind2
Normal file
11
crates/kind-tests/suite/issues/checker/ISSUE-461.kind2
Normal file
@ -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
|
||||||
|
?
|
Loading…
Reference in New Issue
Block a user