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

fix: small fixes and added tests

Browse Source
This commit is contained in:
felipegchi 2022-11-15 18:49:58 -03:00
parent 7ea18ae113
commit 611b71382c
19 changed files with 241 additions and 87 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/kind-cli/tests/mod.rs
View File

@ -67,3 +67,37 @@ fn test_checker() -> Result<(), Error> {
})?;
Ok(())
}
#[test]
#[timeout(15000)]
fn test_eval() -> Result<(), Error> {
test_kind2(Path::new("./tests/suite/eval"), |path| {
let (rx, tx) = std::sync::mpsc::channel();
let root = PathBuf::from(".");
let mut session = Session::new(root, rx);
let check = driver::compile_book_to_hvm(&mut session, &PathBuf::from(path));
let diagnostics = tx.try_iter().collect::<Vec<DiagnosticFrame>>();
let render = RenderConfig::ascii(2);
kind_report::check_if_colors_are_supported(true);
match check {
Some(file) if diagnostics.is_empty() => {
driver::execute_file(&file).to_string()
},
_ => {
let mut res_string = String::new();
for diagnostic in diagnostics {
let diag = Into::<Diagnostic>::into(&diagnostic);
diag.render(&mut session, &render, &mut res_string).unwrap();
}
res_string
}
}
})?;
Ok(())
}

26
src/kind-cli/tests/suite/checker/derive/Eq.golden
View File

@ -1,25 +1 @@
ERROR Type mismatch
* Expected : ((motive _x3) (Equal.refl. t_ a_))
* Got : ((motive _x2) (Equal.refl. _x1 _x2))
* Context:
* _x1 : Type
* _x2 : _x1
* _x3 : _x1
* t_ : Type
* t_ = _x1
* a_ : t_
* a_ = _x3
* a_ = _x2
* motive : ((b : _x1) -> (Equal. _x1 _x2 b) -> Type)
* refl : ((motive _x2) (Equal.refl. _x1 _x2))
/--[tests/suite/checker/Eq.kind2:2:5]
|
1 | type Equal <t: Type> (a: t) ~ (b: t) {
2 | refl : Equal t a a
| v---
| \ Here!
3 | }
Ok!

9
src/kind-cli/tests/suite/checker/derive/Eq.kind2
View File

@ -1,6 +1,3 @@
Equal.match <t: Type> <a: t> <b: t> (scrutinizer: (Equal t a b)) -(motive: ((b : t) -> (Equal t a b) -> Type)) (_refl: (motive a (Equal.refl t a))) : (motive b scrutinizer)
Equal.match _x1 _x2 _x3 (Equal.refl t_ a_) motive refl = (refl :: ((motive a_) (Equal.refl t_ a_)))
Equal <t: Type> (a: t) (b: t) : Type
Equal.refl <t: Type> <a: t> : (Equal t a a)
type Equal <t: Type> (a: t) ~ (b: t) {
refl : Equal t a a
}

1
src/kind-cli/tests/suite/checker/derive/User.golden Normal file
View File

@ -0,0 +1 @@
Ok!

12
src/kind-cli/tests/suite/checker/derive/User.kind2 Normal file
View File

@ -0,0 +1,12 @@
record User {
constructor new
name : U60
ttt : U60
e : U60
}
Main : U60
Main =
let User.new (ttt = e) e .. = User.new 2 4 1
let User.new (ttt = f) .. = User.new 6 7 3
e

12
src/kind-cli/tests/suite/checker/derive/fail/IncompleteCase.golden Normal file
View File

@ -0,0 +1,12 @@
ERROR The case is not covering all the values inside of it!
/--[tests/suite/checker/derive/fail/IncompleteCase.kind2:11:9]
|
10 | let User.new (ttt = e) e .. = User.new 2 4 1
11 | let User.new (ttt = f) name = User.new 6 7 3
| v-------
| \ This is the incomplete case
12 | e
Hint: Need variables for 'e'

12
src/kind-cli/tests/suite/checker/derive/fail/IncompleteCase.kind2 Normal file
View File

@ -0,0 +1,12 @@
record User {
constructor new
name : U60
ttt : U60
e : U60
}
Main : U60
Main =
let User.new (ttt = e) e .. = User.new 2 4 1
let User.new (ttt = f) name = User.new 6 7 3
e

23
src/kind-cli/tests/suite/checker/derive/fail/Repeated.golden Normal file
View File

@ -0,0 +1,23 @@
ERROR Repeated named variable
/--[tests/suite/checker/derive/fail/Repeated.kind2:11:19]
|
10 | let User.new (ttt = e) e .. = User.new 2 4 1
11 | let User.new (ttt = f) ttt = User.new 6 7 3
| v-- v--
| | \ Second occurence
| \ First occurence
12 | e
ERROR The case is not covering all the values inside of it!
/--[tests/suite/checker/derive/fail/Repeated.kind2:11:9]
|
10 | let User.new (ttt = e) e .. = User.new 2 4 1
11 | let User.new (ttt = f) ttt = User.new 6 7 3
| v-------
| \ This is the incomplete case
12 | e
Hint: Need variables for 'e', 'name'

12
src/kind-cli/tests/suite/checker/derive/fail/Repeated.kind2 Normal file
View File

@ -0,0 +1,12 @@
record User {
constructor new
name : U60
ttt : U60
e : U60
}
Main : U60
Main =
let User.new (ttt = e) e .. = User.new 2 4 1
let User.new (ttt = f) ttt = User.new 6 7 3
e

1
src/kind-cli/tests/suite/eval/User.golden Normal file
View File

@ -0,0 +1 @@
4

12
src/kind-cli/tests/suite/eval/User.kind2 Normal file
View File

@ -0,0 +1,12 @@
record User {
constructor new
name : U60
ttt : U60
e : U60
}
Main : U60
Main =
let User.new (ttt = e) name .. = User.new 2 4 1
let User.new (ttt = f) .. = User.new 6 7 3
e

127
src/kind-derive/src/matching.rs
View File

@ -178,7 +178,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
let mut res: Vec<AppBinding> = [indice_names.as_slice()].concat();
res.push(AppBinding::explicit(mk_var(Ident::generate("scrutinizer"))));
let ret_ty = mk_app(mk_var(motive_ident), res, range);
let ret_ty = mk_app(mk_var(motive_ident.clone()), res, range);
let mut rules = Vec::new();
@ -190,30 +190,60 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
let spine_params: Vec<Ident>;
let spine: Vec<Ident>;
if cons.typ.is_none() {
irrelev = sum.indices.extend(&cons.args).map(|x| x.erased).to_vec();
spine_params = sum
.parameters
.extend(&sum.indices)
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}_", f)))
.to_vec();
spine = sum
.indices
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}_", f)))
.to_vec();
} else {
irrelev = cons.args.map(|x| x.erased).to_vec();
spine_params = sum
.parameters
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}_", f)))
.to_vec();
spine = cons
.args
.map(|x| x.name.with_name(|f| format!("{}_", f)))
.to_vec();
let mut args_indices: Vec<AppBinding>;
match &cons.typ {
Some(expr) => match &**expr {
Expr {
data: ExprKind::Constr(_, sp),
..
} => {
irrelev = cons.args.map(|x| x.erased).to_vec();
spine_params = sum
.parameters
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}", f)))
.to_vec();
spine = cons
.args
.map(|x| x.name.with_name(|f| format!("{}", f)))
.to_vec();
args_indices = sp
.iter()
.map(|x| match x {
Binding::Positional(expr) => AppBinding {
erased: false,
data: expr.clone(),
},
Binding::Named(_, _, _) => unreachable!(),
})
.collect::<Vec<AppBinding>>();
args_indices = args_indices[sum.parameters.len()..].into();
}
_ => unreachable!(),
},
None => {
irrelev = sum.indices.extend(&cons.args).map(|x| x.erased).to_vec();
spine_params = sum
.parameters
.extend(&sum.indices)
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}", f)))
.to_vec();
spine = sum
.indices
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}", f)))
.to_vec();
args_indices = sum
.indices
.clone()
.map(|x| AppBinding {
data: mk_var(x.name.clone()),
erased: false,
})
.to_vec();
}
}
pats.push(Box::new(Pat {
@ -245,18 +275,41 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
}));
}
let body = mk_app(
mk_var(cons.name.clone()),
spine
.iter()
.zip(irrelev)
.map(|(arg, erased)| AppBinding {
data: mk_var(arg.clone()),
erased,
})
.collect(),
cons.name.range,
);
let mut args = args_indices.clone();
args.push(AppBinding {
data: Box::new(Expr {
data: ExprKind::Constr(
cons_ident.clone(),
spine_params
.iter()
.cloned()
.map(|x| Binding::Positional(mk_var(x)))
.collect(),
),
range,
}),
erased: false,
});
let body = Box::new(Expr {
data: ExprKind::Ann(
mk_app(
mk_var(cons.name.clone()),
spine
.iter()
.zip(irrelev)
.map(|(arg, erased)| AppBinding {
data: mk_var(arg.clone()),
erased,
})
.collect(),
cons.name.range,
),
mk_app(mk_var(motive_ident.clone()), args, range),
),
range,
});
let rule = Box::new(Rule {
name: name.clone(),

2
src/kind-derive/src/open.rs
View File

@ -37,7 +37,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
})
};
let name = rec.name.add_segment("open");
let name = rec.name.add_segment(rec.constructor.to_str()).add_segment("open");
let mut types = Telescope::default();

5
src/kind-parser/src/expr.rs
View File

@ -1,6 +1,5 @@
use kind_span::{Locatable, Range};
use kind_tree::concrete::expr::*;
use kind_tree::concrete::pat::PatIdent;
use kind_tree::symbol::{Ident, QualifiedIdent};
use kind_tree::{Operator, Number, NumType};
@ -612,7 +611,7 @@ impl<'a> Parser<'a> {
Token::LowerId(_) => {
range = Some(self.range());
let name = self.parse_id()?;
bindings.push(CaseBinding::Field(PatIdent(name)));
bindings.push(CaseBinding::Field(name));
}
Token::LPar => {
let start = self.range();
@ -622,7 +621,7 @@ impl<'a> Parser<'a> {
let renamed = self.parse_id()?;
range = Some(self.range());
self.eat_closing_keyword(Token::RPar, start)?;
bindings.push(CaseBinding::Renamed(name, PatIdent(renamed)));
bindings.push(CaseBinding::Renamed(name, renamed));
}
Token::DotDot => {
ignore_rest_range = Some(self.range());

14
src/kind-pass/src/desugar/destruct.rs
View File

@ -1,6 +1,5 @@
use fxhash::FxHashMap;
use kind_span::{Locatable, Range};
use kind_tree::concrete::pat::PatIdent;
use kind_tree::concrete::{expr, CaseBinding, Destruct, TopLevel};
use kind_tree::desugared;
use kind_tree::symbol::Ident;
@ -16,7 +15,7 @@ impl<'a> DesugarState<'a> {
fields: &[(String, bool)],
cases: &[CaseBinding],
jump_rest: Option<Range>,
) -> Vec<Option<(Range, PatIdent)>> {
) -> Vec<Option<(Range, Ident)>> {
let mut ordered_fields = vec![None; fields.len()];
let mut names = FxHashMap::default();
@ -26,7 +25,7 @@ impl<'a> DesugarState<'a> {
for arg in cases {
let (name, alias) = match arg {
CaseBinding::Field(name) => (name.0.clone(), name.clone()),
CaseBinding::Field(name) => (name.clone(), name.clone()),
CaseBinding::Renamed(name, alias) => (name.clone(), alias.clone()),
};
@ -68,10 +67,11 @@ impl<'a> DesugarState<'a> {
) -> Box<desugared::Expr> {
match binding {
Destruct::Destruct(_, typ, case, jump_rest) => {
let entry = self.old_book.entries.get(&typ.to_string());
let count = self.old_book.count.get(&typ.to_string()).unwrap();
let record = if let Some(TopLevel::RecordType(record)) = entry {
let rec = count.is_record_cons_of.clone().and_then(|name| self.old_book.entries.get(&name.to_string()));
let record = if let Some(TopLevel::RecordType(record)) = rec {
record
} else {
self.send_err(PassError::LetDestructOnlyForRecord(typ.range));
@ -93,7 +93,7 @@ impl<'a> DesugarState<'a> {
for arg in ordered_fields {
if let Some((_, name)) = arg {
arguments.push(name.0)
arguments.push(name)
} else {
arguments.push(self.gen_name(jump_rest.unwrap_or(typ.range)))
}
@ -193,7 +193,7 @@ impl<'a> DesugarState<'a> {
for arg in ordered {
if let Some((_, name)) = arg {
arguments.push(name.0)
arguments.push(name)
} else {
arguments.push(self.gen_name(case.ignore_rest.unwrap_or(match_.typ.range)));
}

8
src/kind-pass/src/unbound/mod.rs
View File

@ -27,7 +27,10 @@ use crate::errors::PassError;
pub struct UnboundCollector {
pub errors: Sender<DiagnosticFrame>,
// Utils for keeping variables tracking and report duplicated ones.
pub context_vars: Vec<(Range, String)>,
pub top_level_defs: FxHashMap<String, Range>,
pub unbound_top_level: FxHashMap<String, FxHashSet<QualifiedIdent>>,
pub unbound: FxHashMap<String, Vec<Ident>>,
@ -331,8 +334,9 @@ impl Visitor for UnboundCollector {
fn visit_case_binding(&mut self, case_binding: &mut CaseBinding) {
match case_binding {
CaseBinding::Field(pat) => self.visit_pat_ident(pat),
CaseBinding::Renamed(_, pat) => self.visit_pat_ident(pat),
CaseBinding::Field(ident) | CaseBinding::Renamed(_, ident) => {
self.context_vars.push((ident.range, ident.to_string()))
}
}
}

8
src/kind-tree/src/concrete/expr.rs
View File

@ -43,8 +43,8 @@ impl AppBinding {
/// inside a match expression.
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
pub enum CaseBinding {
Field(PatIdent),
Renamed(Ident, PatIdent),
Field(Ident),
Renamed(Ident, Ident),
}
/// A match case with a constructor that will matches the
@ -328,8 +328,8 @@ impl Display for Sttm {
impl Display for CaseBinding {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
match self {
CaseBinding::Field(n) => write!(f, "{}", n.0),
CaseBinding::Renamed(m, n) => write!(f, "({} = {})", m, n.0),
CaseBinding::Field(n) => write!(f, "{}", n),
CaseBinding::Renamed(m, n) => write!(f, "({} = {})", m, n),
}
}
}

6
src/kind-tree/src/concrete/mod.rs
View File

@ -187,6 +187,7 @@ pub struct EntryMeta {
pub arguments: Telescope<Argument>,
pub is_ctr: bool,
pub range: Range,
pub is_record_cons_of: Option<QualifiedIdent>
}
/// A book stores definitions by name. It's generated
@ -467,6 +468,7 @@ impl SumTypeDecl {
arguments,
is_ctr: true,
range: self.name.range,
is_record_cons_of: None
}
}
}
@ -507,6 +509,7 @@ impl Constructor {
arguments,
is_ctr: true,
range: self.name.range,
is_record_cons_of: None
}
}
}
@ -544,6 +547,7 @@ impl RecordDecl {
arguments,
is_ctr: true,
range: self.name.range,
is_record_cons_of: None
}
}
@ -572,6 +576,7 @@ impl RecordDecl {
arguments,
is_ctr: true,
range: self.name.range,
is_record_cons_of: Some(self.name.clone())
}
}
}
@ -594,6 +599,7 @@ impl Entry {
arguments,
is_ctr: self.rules.is_empty(),
range: self.name.range,
is_record_cons_of: None
}
}
}

4
src/kind-tree/src/concrete/visitor.rs
View File

@ -197,10 +197,10 @@ pub fn walk_app_binding<T: Visitor>(ctx: &mut T, binding: &mut AppBinding) {
pub fn walk_case_binding<T: Visitor>(ctx: &mut T, binding: &mut CaseBinding) {
match binding {
CaseBinding::Field(ident) => ctx.visit_pat_ident(ident),
CaseBinding::Field(ident) => ctx.visit_ident(ident),
CaseBinding::Renamed(ident, rename) => {
ctx.visit_ident(ident);
ctx.visit_pat_ident(rename);
ctx.visit_ident(rename);
}
}
}