mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-10-26 13:09:53 +03:00
Merge pull request #433 from Kindelia/experimental
fix: fixed problems with match deriver reaching a unreachable place a…
This commit is contained in:
commit
f7caea6652
@ -125,6 +125,8 @@ fn desugar_str(input: &str, range: Range) -> Box<desugared::Expr> {
|
||||
})
|
||||
}
|
||||
|
||||
// Codegen
|
||||
|
||||
fn codegen_str(input: &str) -> Box<Term> {
|
||||
input.chars().rfold(
|
||||
Box::new(Term::Ctr {
|
||||
|
@ -1,5 +1,6 @@
|
||||
///! This module describes tags for internal use
|
||||
/// during compilation
|
||||
|
||||
use core::fmt;
|
||||
|
||||
use kind_tree::Operator;
|
||||
|
@ -1,6 +1,6 @@
|
||||
[package]
|
||||
name = "kind-cli"
|
||||
version = "0.3.1"
|
||||
version = "0.3.2"
|
||||
edition = "2021"
|
||||
description = "A pure functional functional language that uses the HVM."
|
||||
repository = "https://github.com/Kindelia/Kind2"
|
||||
|
@ -3,12 +3,16 @@ use kind_span::Range;
|
||||
|
||||
pub(crate) enum DeriveError {
|
||||
CannotUseNamedVariable(Range),
|
||||
CannotUseAll(Range),
|
||||
InvalidReturnType(Range),
|
||||
}
|
||||
|
||||
impl Diagnostic for DeriveError {
|
||||
fn get_syntax_ctx(&self) -> Option<kind_span::SyntaxCtxIndex> {
|
||||
match self {
|
||||
DeriveError::CannotUseNamedVariable(range) => Some(range.ctx),
|
||||
DeriveError::CannotUseAll(range) => Some(range.ctx),
|
||||
DeriveError::InvalidReturnType(range) => Some(range.ctx),
|
||||
}
|
||||
}
|
||||
|
||||
@ -28,6 +32,34 @@ impl Diagnostic for DeriveError {
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
DeriveError::CannotUseAll(range) => DiagnosticFrame {
|
||||
code: 103,
|
||||
severity: Severity::Error,
|
||||
title: "Data constructors cannot return function types.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["Change all of the function types sequence for explicit arguments like 'cons : x -> T' to 'cons (name: x) : T'".to_string()],
|
||||
positions: vec![Marker {
|
||||
position: *range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
DeriveError::InvalidReturnType(range) => DiagnosticFrame {
|
||||
code: 103,
|
||||
severity: Severity::Error,
|
||||
title: "Data constructors cannot return this type".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["Replace it with the type that is being declarated at the current block".to_string()],
|
||||
positions: vec![Marker {
|
||||
position: *range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -7,6 +7,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent};
|
||||
use kind_tree::concrete::*;
|
||||
use kind_tree::concrete::{self};
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
pub fn derive_getters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
|
@ -1,3 +1,5 @@
|
||||
#![feature(let_chains)]
|
||||
|
||||
//! Utility to derive functions from their definitions.
|
||||
|
||||
pub mod errors;
|
||||
|
@ -6,116 +6,75 @@ use kind_report::data::Diagnostic;
|
||||
use kind_span::Range;
|
||||
|
||||
use kind_tree::concrete::expr::Expr;
|
||||
use kind_tree::concrete::pat::{Pat, PatIdent};
|
||||
use kind_tree::concrete::pat::{Pat, PatIdent, PatKind};
|
||||
use kind_tree::concrete::*;
|
||||
use kind_tree::concrete::{self};
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
use kind_tree::symbol::Ident;
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
use crate::errors::DeriveError;
|
||||
use crate::subst::substitute_in_expr;
|
||||
|
||||
/// Derives an eliminator from a sum type declaration.
|
||||
pub fn derive_match(
|
||||
range: Range,
|
||||
sum: &SumTypeDecl,
|
||||
) -> (concrete::Entry, Vec<Box<dyn Diagnostic>>) {
|
||||
let mut errs: Vec<Box<dyn Diagnostic>> = Vec::new();
|
||||
type Errs = Vec<Box<dyn Diagnostic>>;
|
||||
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Var { name },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_cons = |name: QualifiedIdent, args: Vec<Binding>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Constr { name, args },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_app = |fun: Box<Expr>, args: Vec<AppBinding>, range: Range| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::App { fun, args },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_pi = |name: Ident, typ: Box<Expr>, body: Box<Expr>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::All {
|
||||
param: Some(name),
|
||||
typ,
|
||||
body,
|
||||
pub fn to_app_binding(errs: &mut Errs, binding: &Binding) -> AppBinding {
|
||||
match binding {
|
||||
Binding::Positional(expr) => AppBinding {
|
||||
erased: false,
|
||||
data: expr.clone(),
|
||||
},
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_typ = || -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Lit { lit: Literal::Type },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let name = sum.name.add_segment("match");
|
||||
|
||||
let mut types = Telescope::default();
|
||||
|
||||
for arg in sum.parameters.iter() {
|
||||
types.push(arg.to_implicit())
|
||||
Binding::Named(_, name, expr) => {
|
||||
errs.push(Box::new(DeriveError::CannotUseNamedVariable(name.range)));
|
||||
AppBinding::explicit(expr.clone())
|
||||
}
|
||||
|
||||
for arg in sum.indices.iter() {
|
||||
types.push(arg.to_implicit())
|
||||
}
|
||||
}
|
||||
|
||||
// The type
|
||||
/// Derives an eliminator from a sum type declaration.
|
||||
pub fn derive_match(range: Range, sum: &SumTypeDecl) -> (concrete::Entry, Errs) {
|
||||
let mut errs: Errs = Vec::new();
|
||||
|
||||
let all_args = sum.parameters.extend(&sum.indices);
|
||||
let res_motive_ty = mk_cons(
|
||||
sum.name.clone(),
|
||||
all_args
|
||||
let new_entry_name = sum.name.add_segment("match");
|
||||
|
||||
let all_arguments = sum.parameters.extend(&sum.indices);
|
||||
|
||||
// Parameters and indices
|
||||
|
||||
let mut types = all_arguments.map(|x| x.to_implicit());
|
||||
|
||||
let all_bindings = all_arguments
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(mk_var(x.name)))
|
||||
.collect(),
|
||||
);
|
||||
|
||||
let indice_names: Vec<AppBinding> = sum
|
||||
.indices
|
||||
.iter()
|
||||
.map(|x| AppBinding::explicit(mk_var(x.name.clone())))
|
||||
.map(|x| Binding::Positional(Expr::var(x.name)))
|
||||
.collect();
|
||||
|
||||
// Sccrutinzies
|
||||
let current_return_type = Expr::cons(sum.name.clone(), all_bindings, range);
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("scrutinizer"),
|
||||
typ: Some(res_motive_ty.clone()),
|
||||
typ: Some(current_return_type.clone()),
|
||||
range,
|
||||
});
|
||||
|
||||
// Motive with indices
|
||||
// Motive
|
||||
|
||||
let motive_ident = Ident::new_static("motive", range);
|
||||
|
||||
let motive_type = sum.indices.iter().rfold(
|
||||
mk_pi(Ident::new_static("val_", range), res_motive_ty, mk_typ()),
|
||||
|out, arg| {
|
||||
mk_pi(
|
||||
arg.name.clone(),
|
||||
arg.typ.clone().unwrap_or_else(mk_typ),
|
||||
out,
|
||||
)
|
||||
},
|
||||
let motive_return = Expr::all(
|
||||
Ident::new_static("val_", range),
|
||||
current_return_type,
|
||||
Expr::typ(range),
|
||||
false,
|
||||
range,
|
||||
);
|
||||
|
||||
let motive_type = sum.indices.iter().rfold(motive_return, |out, arg| {
|
||||
let typ = arg.typ.clone().unwrap_or_else(|| Expr::typ(range));
|
||||
Expr::all(arg.name.clone(), typ, out, false, range)
|
||||
});
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: true,
|
||||
@ -124,39 +83,47 @@ pub fn derive_match(
|
||||
range,
|
||||
});
|
||||
|
||||
let params = sum
|
||||
.parameters
|
||||
.map(|x| Binding::Positional(mk_var(x.name.clone())));
|
||||
let indices = sum
|
||||
.indices
|
||||
.map(|x| Binding::Positional(mk_var(x.name.clone())));
|
||||
// Constructors
|
||||
|
||||
// Constructors type
|
||||
for cons in &sum.constructors {
|
||||
let vars: Vec<Binding> = cons
|
||||
.args
|
||||
let indice_names: Vec<AppBinding> = sum
|
||||
.indices
|
||||
.iter()
|
||||
.map(|x| Binding::Positional(mk_var(x.name.clone())))
|
||||
.map(|x| AppBinding::explicit(Expr::var(x.name.clone())))
|
||||
.collect();
|
||||
|
||||
let cons_inst = mk_cons(
|
||||
sum.name.add_segment(cons.name.to_str()),
|
||||
[
|
||||
params.as_slice(),
|
||||
if cons.typ.is_none() {
|
||||
indices.as_slice()
|
||||
} else {
|
||||
&[]
|
||||
},
|
||||
vars.as_slice(),
|
||||
]
|
||||
.concat(),
|
||||
);
|
||||
// Parameter binding telescope
|
||||
|
||||
let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) {
|
||||
Some(ExprKind::Constr { name: _, args }) => {
|
||||
let params = sum
|
||||
.parameters
|
||||
.map(|x| Binding::Positional(Expr::var(x.name.clone())));
|
||||
|
||||
let indices = sum
|
||||
.indices
|
||||
.map(|x| Binding::Positional(Expr::var(x.name.clone())));
|
||||
|
||||
// Types
|
||||
|
||||
for cons in &sum.constructors {
|
||||
// Constructor arguments bindings
|
||||
let vars = cons
|
||||
.args
|
||||
.map(|x| Binding::Positional(Expr::var(x.name.clone())));
|
||||
|
||||
let constructor_name = sum.name.add_segment(cons.name.to_str());
|
||||
|
||||
let default = &Telescope::default();
|
||||
let indices = &indices;
|
||||
|
||||
let partial_indices = if cons.typ.is_none() { indices } else { default };
|
||||
|
||||
let args = params.extend(partial_indices).extend(&vars);
|
||||
|
||||
let instantation_of_the_cons = Expr::cons(constructor_name.clone(), args.to_vec(), range);
|
||||
|
||||
let mut cons_indices = if let Some(res) = &cons.typ {
|
||||
if let ExprKind::Constr { args, .. } = &res.data {
|
||||
let mut new_args = Vec::with_capacity(args.len());
|
||||
for arg in &args[sum.parameters.len()..].to_vec() {
|
||||
for arg in &args[sum.parameters.len()..] {
|
||||
new_args.push(match arg {
|
||||
Binding::Positional(expr) => AppBinding::explicit(expr.clone()),
|
||||
Binding::Named(range, _, expr) => {
|
||||
@ -166,13 +133,20 @@ pub fn derive_match(
|
||||
});
|
||||
}
|
||||
new_args
|
||||
} else if let ExprKind::All { .. } = &res.data {
|
||||
errs.push(Box::new(DeriveError::CannotUseAll(res.range)));
|
||||
[indice_names.as_slice()].concat()
|
||||
} else {
|
||||
errs.push(Box::new(DeriveError::InvalidReturnType(res.range)));
|
||||
[indice_names.as_slice()].concat()
|
||||
}
|
||||
_ => [indice_names.as_slice()].concat(),
|
||||
} else {
|
||||
[indice_names.as_slice()].concat()
|
||||
};
|
||||
|
||||
indices_of_cons.push(AppBinding::explicit(cons_inst));
|
||||
cons_indices.push(AppBinding::explicit(instantation_of_the_cons));
|
||||
|
||||
let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range);
|
||||
let cons_tipo = Expr::app(Expr::var(motive_ident.clone()), cons_indices, range);
|
||||
|
||||
let args = if cons.typ.is_some() {
|
||||
cons.args.clone()
|
||||
@ -181,83 +155,68 @@ pub fn derive_match(
|
||||
};
|
||||
|
||||
let cons_type = args.iter().rfold(cons_tipo, |out, arg| {
|
||||
mk_pi(
|
||||
Expr::all(
|
||||
arg.name.clone(),
|
||||
arg.typ.clone().unwrap_or_else(mk_typ),
|
||||
arg.typ.clone().unwrap_or_else(|| Expr::typ(range)),
|
||||
out,
|
||||
arg.erased,
|
||||
range,
|
||||
)
|
||||
});
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::new_static(&format!("{}_", cons.name), range),
|
||||
typ: Some(cons_type),
|
||||
types.push(Argument::new_explicit(
|
||||
Ident::new_static(&format!("{}_", cons.name), range),
|
||||
cons_type,
|
||||
range,
|
||||
});
|
||||
));
|
||||
}
|
||||
|
||||
if !errs.is_empty() {
|
||||
let entry = Entry {
|
||||
name,
|
||||
docs: Vec::new(),
|
||||
args: types,
|
||||
typ: Box::new(Expr {
|
||||
let make_incomplete_entry = || {
|
||||
let typ = Box::new(Expr {
|
||||
data: ExprKind::Hole,
|
||||
range,
|
||||
}),
|
||||
});
|
||||
|
||||
Entry {
|
||||
name: new_entry_name.clone(),
|
||||
docs: Vec::new(),
|
||||
args: types.clone(),
|
||||
typ,
|
||||
rules: vec![],
|
||||
range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(sum.name.to_string()),
|
||||
}
|
||||
};
|
||||
return (entry, errs);
|
||||
|
||||
if !errs.is_empty() {
|
||||
return (make_incomplete_entry(), errs);
|
||||
}
|
||||
|
||||
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.clone()), res, range);
|
||||
let scrutinizer_ident = Expr::var(Ident::generate("scrutinizer"));
|
||||
|
||||
let mut return_args = indice_names.clone();
|
||||
return_args.push(AppBinding::explicit(scrutinizer_ident));
|
||||
|
||||
let return_type = Expr::app(Expr::var(motive_ident.clone()), return_args, range);
|
||||
|
||||
// Rules
|
||||
|
||||
let mut rules = Vec::new();
|
||||
|
||||
for cons in &sum.constructors {
|
||||
let cons_ident = sum.name.add_segment(cons.name.to_str());
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
let constructor_name = sum.name.add_segment(cons.name.to_str());
|
||||
|
||||
let irrelev: Vec<bool>;
|
||||
let spine_params: Vec<Ident>;
|
||||
let spine: Vec<Ident>;
|
||||
let params = sum.parameters.map(|x| x.name.add_underscore());
|
||||
|
||||
let mut args_indices: Vec<AppBinding>;
|
||||
let mut indices_and_args: Telescope<AppBinding>;
|
||||
|
||||
match &cons.typ {
|
||||
Some(expr) => match &**expr {
|
||||
Expr {
|
||||
data: ExprKind::Constr { args, .. },
|
||||
..
|
||||
} => {
|
||||
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 = args
|
||||
.iter()
|
||||
.map(|x| match x {
|
||||
Binding::Positional(expr) => AppBinding {
|
||||
erased: false,
|
||||
data: expr.clone(),
|
||||
},
|
||||
Binding::Named(_, _, _) => unreachable!(),
|
||||
})
|
||||
.collect::<Vec<AppBinding>>();
|
||||
args_indices = {
|
||||
let mut indices = args_indices[sum.parameters.len()..].to_vec();
|
||||
let args = if let Some(res) = &cons.typ {
|
||||
if let ExprKind::Constr { args, .. } = &res.data {
|
||||
indices_and_args =
|
||||
Telescope::new(args.clone()).map(|x| to_app_binding(&mut errs, x));
|
||||
|
||||
let mut indices = indices_and_args.to_vec()[sum.parameters.len()..].to_vec();
|
||||
|
||||
let renames = FxHashMap::from_iter(
|
||||
sum.parameters
|
||||
@ -270,44 +229,35 @@ pub fn derive_match(
|
||||
for indice in &mut indices {
|
||||
substitute_in_expr(&mut indice.data, &renames)
|
||||
}
|
||||
indices
|
||||
|
||||
indices_and_args = Telescope::new(indices);
|
||||
|
||||
cons.args.clone()
|
||||
} else {
|
||||
unreachable!(
|
||||
"Internal Error: I guess you're using something that is not a constructor!"
|
||||
)
|
||||
}
|
||||
} else {
|
||||
indices_and_args = sum.indices.map(|x| AppBinding::from_ident(x.name.clone()));
|
||||
sum.indices.extend(&cons.args)
|
||||
};
|
||||
}
|
||||
_ => 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();
|
||||
}
|
||||
}
|
||||
|
||||
let irrelevances = args.map(|x| x.erased).to_vec();
|
||||
let spine = args.map(|x| x.name.add_underscore());
|
||||
|
||||
let params_and_spine = params.extend(&spine);
|
||||
let mut pats = Vec::new();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
cons_ident.clone(),
|
||||
spine_params
|
||||
data: PatKind::App(
|
||||
constructor_name.clone(),
|
||||
params_and_spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| {
|
||||
Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(x)),
|
||||
data: PatKind::Var(PatIdent(x)),
|
||||
range,
|
||||
})
|
||||
})
|
||||
@ -317,55 +267,52 @@ pub fn derive_match(
|
||||
}));
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(Ident::generate("motive"))),
|
||||
data: PatKind::Var(PatIdent(Ident::generate("motive"))),
|
||||
range,
|
||||
}));
|
||||
|
||||
for cons2 in &sum.constructors {
|
||||
for cons in &sum.constructors {
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(cons2.name.clone())),
|
||||
data: PatKind::Var(PatIdent(cons.name.clone())),
|
||||
range,
|
||||
}));
|
||||
}
|
||||
|
||||
let mut args = args_indices.clone();
|
||||
let mut args = indices_and_args.clone();
|
||||
|
||||
args.push(AppBinding {
|
||||
data: Box::new(Expr {
|
||||
data: ExprKind::Constr {
|
||||
name: cons_ident.clone(),
|
||||
args: spine_params
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(mk_var(x)))
|
||||
.collect(),
|
||||
},
|
||||
args.push(AppBinding::explicit(Expr::cons(
|
||||
constructor_name.clone(),
|
||||
params_and_spine
|
||||
.map(|x| Binding::Positional(Expr::var(x.clone())))
|
||||
.to_vec(),
|
||||
range,
|
||||
}),
|
||||
erased: false,
|
||||
});
|
||||
)));
|
||||
|
||||
let body = Box::new(Expr {
|
||||
data: ExprKind::Ann {
|
||||
val: mk_app(
|
||||
mk_var(cons.name.clone()),
|
||||
let body_typ = Expr::app(Expr::var(motive_ident.clone()), args.to_vec(), range);
|
||||
|
||||
let body_val = Expr::app(
|
||||
Expr::var(cons.name.clone()),
|
||||
spine
|
||||
.iter()
|
||||
.zip(irrelev)
|
||||
.zip(irrelevances)
|
||||
.map(|(arg, erased)| AppBinding {
|
||||
data: mk_var(arg.clone()),
|
||||
data: Expr::var(arg.clone()),
|
||||
erased,
|
||||
})
|
||||
.collect(),
|
||||
cons.name.range,
|
||||
),
|
||||
typ: mk_app(mk_var(motive_ident.clone()), args, range),
|
||||
);
|
||||
|
||||
let body = Box::new(Expr {
|
||||
data: ExprKind::Ann {
|
||||
val: body_val,
|
||||
typ: body_typ,
|
||||
},
|
||||
range,
|
||||
});
|
||||
|
||||
let rule = Box::new(Rule {
|
||||
name: name.clone(),
|
||||
name: new_entry_name.clone(),
|
||||
pats,
|
||||
body,
|
||||
range: cons.name.range,
|
||||
@ -373,13 +320,12 @@ pub fn derive_match(
|
||||
|
||||
rules.push(rule)
|
||||
}
|
||||
// Rules
|
||||
|
||||
let entry = Entry {
|
||||
name,
|
||||
name: new_entry_name,
|
||||
docs: Vec::new(),
|
||||
args: types,
|
||||
typ: ret_ty,
|
||||
typ: return_type,
|
||||
rules,
|
||||
range,
|
||||
attrs: Vec::new(),
|
||||
|
@ -7,6 +7,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent};
|
||||
use kind_tree::concrete::*;
|
||||
use kind_tree::concrete::{self};
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
|
@ -7,6 +7,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent};
|
||||
use kind_tree::concrete::*;
|
||||
use kind_tree::concrete::{self};
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
pub fn derive_setters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
|
@ -4,6 +4,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent, PatKind};
|
||||
|
||||
use kind_tree::concrete::*;
|
||||
use kind_tree::symbol::QualifiedIdent;
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
use crate::errors::SyntaxDiagnostic;
|
||||
use crate::lexer::tokens::Token;
|
||||
|
@ -1,5 +1,6 @@
|
||||
use kind_tree::concrete::{Attribute, Constructor, RecordDecl, SumTypeDecl, Telescope};
|
||||
use kind_tree::concrete::{Attribute, Constructor, RecordDecl, SumTypeDecl};
|
||||
use kind_tree::symbol::Ident;
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
use crate::errors::SyntaxDiagnostic;
|
||||
use crate::lexer::tokens::Token;
|
||||
|
@ -1,7 +1,8 @@
|
||||
use kind_span::Range;
|
||||
use kind_tree::concrete::{self, Telescope};
|
||||
use kind_tree::concrete::{self};
|
||||
use kind_tree::desugared::{self, ExprKind};
|
||||
use kind_tree::symbol::QualifiedIdent;
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
use crate::errors::{PassError, Sugar};
|
||||
|
||||
|
@ -407,8 +407,12 @@ impl<'a> ErasureState<'a> {
|
||||
|
||||
self.ctx = backup;
|
||||
|
||||
if *erased {
|
||||
body
|
||||
} else {
|
||||
untyped::Expr::lambda(expr.range, param.clone(), body, *erased)
|
||||
}
|
||||
}
|
||||
Let { name, val, next } => {
|
||||
let backup = self.ctx.clone();
|
||||
|
||||
@ -497,9 +501,21 @@ impl<'a> ErasureState<'a> {
|
||||
App { fun, args } => {
|
||||
let fun = self.erase_expr(ambient, edge, fun);
|
||||
let mut spine = Vec::new();
|
||||
|
||||
for arg in args {
|
||||
spine.push(self.erase_expr(ambient, edge, &arg.data))
|
||||
let ambient = if arg.erased {
|
||||
Ambient::Irrelevant
|
||||
} else {
|
||||
ambient
|
||||
};
|
||||
|
||||
let res = self.erase_expr(ambient, edge, &arg.data);
|
||||
|
||||
if !arg.erased {
|
||||
spine.push(res)
|
||||
}
|
||||
}
|
||||
|
||||
untyped::Expr::app(expr.range, fun, spine)
|
||||
}
|
||||
Sub { expr, .. } => self.erase_expr(ambient, edge, expr),
|
||||
|
@ -13,21 +13,30 @@ use kind_derive::setters::derive_setters;
|
||||
use kind_report::data::Diagnostic;
|
||||
use kind_span::Locatable;
|
||||
use kind_span::Range;
|
||||
use kind_tree::concrete::Entry;
|
||||
use kind_tree::concrete::EntryMeta;
|
||||
use kind_tree::concrete::Module;
|
||||
use kind_tree::concrete::RecordDecl;
|
||||
use kind_tree::concrete::SumTypeDecl;
|
||||
use kind_tree::concrete::{Attribute, TopLevel};
|
||||
|
||||
use crate::errors::PassError;
|
||||
|
||||
/// Expands sum type and record definitions to a lot of
|
||||
/// helper definitions like eliminators and replace qualified identifiers
|
||||
/// by their module names.
|
||||
pub mod uses;
|
||||
|
||||
type Derivations = FxHashMap<Derive, Range>;
|
||||
type Channel = Sender<Box<dyn Diagnostic>>;
|
||||
|
||||
/// Tags for each one of the possible derivations.
|
||||
#[derive(Debug, Hash, PartialEq, Eq)]
|
||||
pub enum Derive {
|
||||
Match,
|
||||
Open,
|
||||
Getters,
|
||||
Setters
|
||||
Setters,
|
||||
}
|
||||
|
||||
impl Display for Derive {
|
||||
@ -41,25 +50,13 @@ impl Display for Derive {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn insert_or_report(
|
||||
channel: Sender<Box<dyn Diagnostic>>,
|
||||
hashmap: &mut FxHashMap<Derive, Range>,
|
||||
key: Derive,
|
||||
range: Range,
|
||||
) {
|
||||
match hashmap.get(&key) {
|
||||
Some(last_range) => {
|
||||
channel
|
||||
.send(Box::new(PassError::DuplicatedAttributeArgument(
|
||||
*last_range,
|
||||
range,
|
||||
)))
|
||||
.unwrap();
|
||||
}
|
||||
None => {
|
||||
pub fn insert_or_report(channel: Channel, hashmap: &mut Derivations, key: Derive, range: Range) {
|
||||
if let Some(last_range) = hashmap.get(&key) {
|
||||
let err = Box::new(PassError::DuplicatedAttributeArgument(*last_range, range));
|
||||
channel.send(err).unwrap();
|
||||
} else {
|
||||
hashmap.insert(key, range);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn string_to_derive(name: &str) -> Option<Derive> {
|
||||
@ -72,12 +69,11 @@ fn string_to_derive(name: &str) -> Option<Derive> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn expand_derive(
|
||||
error_channel: Sender<Box<dyn Diagnostic>>,
|
||||
attrs: &[Attribute],
|
||||
) -> Option<FxHashMap<Derive, Range>> {
|
||||
pub fn expand_derive(error_channel: Channel, attrs: &[Attribute]) -> Option<Derivations> {
|
||||
use kind_tree::concrete::AttributeStyle::*;
|
||||
|
||||
let mut failed = false;
|
||||
let mut def = FxHashMap::default();
|
||||
let mut defs = FxHashMap::default();
|
||||
|
||||
for attr in attrs {
|
||||
if attr.name.to_str() != "derive" {
|
||||
@ -85,36 +81,21 @@ pub fn expand_derive(
|
||||
}
|
||||
|
||||
if let Some(attr) = &attr.value {
|
||||
error_channel
|
||||
.send(Box::new(PassError::AttributeDoesNotExpectEqual(
|
||||
attr.locate(),
|
||||
)))
|
||||
.unwrap();
|
||||
let err = Box::new(PassError::AttributeDoesNotExpectEqual(attr.locate()));
|
||||
error_channel.send(err).unwrap();
|
||||
failed = true;
|
||||
}
|
||||
|
||||
use kind_tree::concrete::AttributeStyle::*;
|
||||
for arg in &attr.args {
|
||||
match arg {
|
||||
Ident(range, ident) => match string_to_derive(ident.to_str()) {
|
||||
Some(key) => {
|
||||
insert_or_report(error_channel.clone(), &mut def, key, *range)
|
||||
Ident(range, ident) if string_to_derive(ident.to_str()).is_some() => {
|
||||
// Duplicates work but it's something negligible
|
||||
let key = string_to_derive(ident.to_str()).unwrap();
|
||||
insert_or_report(error_channel.clone(), &mut defs, key, *range)
|
||||
}
|
||||
_ => {
|
||||
error_channel
|
||||
.send(Box::new(PassError::InvalidAttributeArgument(
|
||||
ident.locate(),
|
||||
)))
|
||||
.unwrap();
|
||||
failed = true;
|
||||
}
|
||||
},
|
||||
other => {
|
||||
error_channel
|
||||
.send(Box::new(PassError::InvalidAttributeArgument(
|
||||
other.locate(),
|
||||
)))
|
||||
.unwrap();
|
||||
let err = Box::new(PassError::InvalidAttributeArgument(other.locate()));
|
||||
error_channel.send(err).unwrap();
|
||||
failed = true;
|
||||
}
|
||||
}
|
||||
@ -124,20 +105,19 @@ pub fn expand_derive(
|
||||
if failed {
|
||||
None
|
||||
} else {
|
||||
Some(def)
|
||||
Some(defs)
|
||||
}
|
||||
}
|
||||
|
||||
pub fn expand_module(error_channel: Sender<Box<dyn Diagnostic>>, module: &mut Module) -> bool {
|
||||
pub fn expand_sum_type(
|
||||
error_channel: Channel,
|
||||
entries: &mut FxHashMap<String, (Entry, EntryMeta)>,
|
||||
sum: &SumTypeDecl,
|
||||
derivations: Derivations,
|
||||
) -> bool {
|
||||
let mut failed = false;
|
||||
|
||||
let mut entries = FxHashMap::default();
|
||||
|
||||
for entry in &module.entries {
|
||||
match entry {
|
||||
TopLevel::SumType(sum) => {
|
||||
if let Some(derive) = expand_derive(error_channel.clone(), &sum.attrs) {
|
||||
for (key, val) in derive {
|
||||
for (key, val) in derivations {
|
||||
match key {
|
||||
Derive::Match => {
|
||||
let (res, errs) = derive_match(sum.name.range, sum);
|
||||
@ -156,13 +136,19 @@ pub fn expand_module(error_channel: Sender<Box<dyn Diagnostic>>, module: &mut Mo
|
||||
}
|
||||
}
|
||||
}
|
||||
} else {
|
||||
failed = true;
|
||||
}
|
||||
}
|
||||
TopLevel::RecordType(rec) => {
|
||||
if let Some(derive) = expand_derive(error_channel.clone(), &rec.attrs) {
|
||||
for (key, val) in derive {
|
||||
|
||||
failed
|
||||
}
|
||||
|
||||
pub fn expand_record_type(
|
||||
error_channel: Channel,
|
||||
entries: &mut FxHashMap<String, (Entry, EntryMeta)>,
|
||||
rec: &RecordDecl,
|
||||
derivations: Derivations,
|
||||
) -> bool {
|
||||
let mut failed = false;
|
||||
|
||||
for (key, val) in derivations {
|
||||
match key {
|
||||
Derive::Open => {
|
||||
let res = derive_open(rec.name.range, rec);
|
||||
@ -189,6 +175,27 @@ pub fn expand_module(error_channel: Sender<Box<dyn Diagnostic>>, module: &mut Mo
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
failed
|
||||
}
|
||||
|
||||
pub fn expand_module(error_channel: Channel, module: &mut Module) -> bool {
|
||||
let mut failed = false;
|
||||
|
||||
let mut entries = FxHashMap::default();
|
||||
|
||||
for entry in &module.entries {
|
||||
match entry {
|
||||
TopLevel::SumType(sum) => {
|
||||
if let Some(derive) = expand_derive(error_channel.clone(), &sum.attrs) {
|
||||
failed |= expand_sum_type(error_channel.clone(), &mut entries, sum, derive)
|
||||
} else {
|
||||
failed = true;
|
||||
}
|
||||
}
|
||||
TopLevel::RecordType(rec) => {
|
||||
if let Some(derive) = expand_derive(error_channel.clone(), &rec.attrs) {
|
||||
failed |= expand_record_type(error_channel.clone(), &mut entries, rec, derive)
|
||||
} else {
|
||||
failed = true;
|
||||
}
|
||||
|
1
crates/kind-tests/suite/checker/derive/Eq.golden
Normal file
1
crates/kind-tests/suite/checker/derive/Eq.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
4
crates/kind-tests/suite/checker/derive/Eq.kind2
Normal file
4
crates/kind-tests/suite/checker/derive/Eq.kind2
Normal file
@ -0,0 +1,4 @@
|
||||
#derive[match]
|
||||
type Equal <t: Type> (a: t) ~ (b: t) {
|
||||
refl : Equal t a a
|
||||
}
|
@ -0,0 +1,26 @@
|
||||
ERROR Data constructors cannot return function types.
|
||||
|
||||
/--[suite/checker/issues/MatchDerivationWithAll.kind2:3:10]
|
||||
|
|
||||
2 | type WithCtx (a: Type) {
|
||||
3 | new: U60 -> (WithCtx a)
|
||||
| v-----------------
|
||||
| \Here!
|
||||
4 | }
|
||||
|
||||
Hint: Change all of the function types sequence for explicit arguments like 'cons : x -> T' to 'cons (name: x) : T'
|
||||
|
||||
ERROR This is not the type that is being declared.
|
||||
|
||||
/--[suite/checker/issues/MatchDerivationWithAll.kind2:2:6]
|
||||
|
|
||||
2 | type WithCtx (a: Type) {
|
||||
| v------
|
||||
| \This is the type that should be used instead
|
||||
:
|
||||
3 | new: U60 -> (WithCtx a)
|
||||
| v-----------------
|
||||
| \This is not the type that is being declared
|
||||
4 | }
|
||||
|
||||
|
@ -0,0 +1,4 @@
|
||||
#derive[match]
|
||||
type WithCtx (a: Type) {
|
||||
new: U60 -> (WithCtx a)
|
||||
}
|
1
crates/kind-tests/suite/eval/VecMatch.golden
Normal file
1
crates/kind-tests/suite/eval/VecMatch.golden
Normal file
@ -0,0 +1 @@
|
||||
3
|
20
crates/kind-tests/suite/eval/VecMatch.kind2
Normal file
20
crates/kind-tests/suite/eval/VecMatch.kind2
Normal file
@ -0,0 +1,20 @@
|
||||
type Nat {
|
||||
succ (pred : Nat)
|
||||
zero
|
||||
}
|
||||
|
||||
#derive[match]
|
||||
type Vec (t: Type) ~ (n: Nat) {
|
||||
cons <size : Nat> (x : t) (xs : Vec t size) : Vec t (Nat.succ size)
|
||||
nil : Vec t Nat.zero
|
||||
}
|
||||
|
||||
Vec.count <t> <n: Nat> (v: Vec t n) : U60
|
||||
Vec.count vec =
|
||||
match Vec vec {
|
||||
cons xs .. => (+ 1 (Vec.count xs))
|
||||
nil => 0
|
||||
}
|
||||
|
||||
Main : U60
|
||||
Main = Vec.count (Vec.cons 10 (Vec.cons 20 (Vec.cons 30 Vec.nil)))
|
@ -35,6 +35,13 @@ impl AppBinding {
|
||||
erased: false,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn from_ident(data: Ident) -> AppBinding {
|
||||
AppBinding {
|
||||
data: Expr::var(data),
|
||||
erased: false,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// A case binding is a field or a rename of some field
|
||||
@ -203,59 +210,78 @@ pub struct Expr {
|
||||
pub range: Range,
|
||||
}
|
||||
|
||||
impl Display for Operator {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
use Operator::*;
|
||||
|
||||
match self {
|
||||
Add => write!(f, "+"),
|
||||
Sub => write!(f, "-"),
|
||||
Mul => write!(f, "*"),
|
||||
Div => write!(f, "/"),
|
||||
Mod => write!(f, "%"),
|
||||
And => write!(f, "&"),
|
||||
Or => write!(f, "|"),
|
||||
Xor => write!(f, "^"),
|
||||
Shl => write!(f, "<<"),
|
||||
Shr => write!(f, ">>"),
|
||||
Ltn => write!(f, "<"),
|
||||
Lte => write!(f, "<="),
|
||||
Eql => write!(f, "=="),
|
||||
Gte => write!(f, ">="),
|
||||
Gtn => write!(f, ">"),
|
||||
Neq => write!(f, "!="),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Expr {
|
||||
pub fn traverse_pi_types(&self) -> String {
|
||||
match &self.data {
|
||||
ExprKind::All {
|
||||
pub fn var(name: Ident) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range: name.range.clone(),
|
||||
data: ExprKind::Var { name },
|
||||
})
|
||||
}
|
||||
|
||||
pub fn cons(name: QualifiedIdent, args: Spine, range: Range) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range,
|
||||
data: ExprKind::Constr { name, args },
|
||||
})
|
||||
}
|
||||
|
||||
pub fn all(
|
||||
param: Ident,
|
||||
typ: Box<Expr>,
|
||||
body: Box<Expr>,
|
||||
erased: bool,
|
||||
range: Range,
|
||||
) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range,
|
||||
data: ExprKind::All {
|
||||
param: Some(param),
|
||||
typ,
|
||||
body,
|
||||
erased,
|
||||
},
|
||||
})
|
||||
}
|
||||
|
||||
pub fn lambda(
|
||||
param: Ident,
|
||||
typ: Option<Box<Expr>>,
|
||||
body: Box<Expr>,
|
||||
erased: bool,
|
||||
range: Range,
|
||||
) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Lambda {
|
||||
param,
|
||||
typ,
|
||||
body,
|
||||
erased,
|
||||
} => {
|
||||
let tilde = if *erased { "~" } else { "" };
|
||||
match param {
|
||||
None => format!("{}{} -> {}", tilde, typ, body.traverse_pi_types()),
|
||||
Some(binder) => format!(
|
||||
"{}({} : {}) -> {}",
|
||||
tilde,
|
||||
binder,
|
||||
typ,
|
||||
body.traverse_pi_types()
|
||||
),
|
||||
}
|
||||
}
|
||||
ExprKind::Sigma { param, fst, snd } => match param {
|
||||
None => format!("{} -> {}", fst, snd.traverse_pi_types()),
|
||||
Some(binder) => format!("[{} : {}] -> {}", binder, fst, snd.traverse_pi_types()),
|
||||
},
|
||||
_ => format!("{}", self),
|
||||
range,
|
||||
})
|
||||
}
|
||||
|
||||
pub fn typ(range: Range) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Lit { lit: Literal::Type },
|
||||
range,
|
||||
})
|
||||
}
|
||||
|
||||
pub fn app(fun: Box<Expr>, args: Vec<AppBinding>, range: Range) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::App { fun, args },
|
||||
range,
|
||||
})
|
||||
}
|
||||
|
||||
pub fn hole(range: Range) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Hole,
|
||||
range,
|
||||
})
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
impl Locatable for Binding {
|
||||
@ -309,6 +335,36 @@ impl Locatable for Destruct {
|
||||
}
|
||||
}
|
||||
|
||||
impl Expr {
|
||||
pub fn traverse_pi_types(&self) -> String {
|
||||
match &self.data {
|
||||
ExprKind::All {
|
||||
param,
|
||||
typ,
|
||||
body,
|
||||
erased,
|
||||
} => {
|
||||
let tilde = if *erased { "~" } else { "" };
|
||||
match param {
|
||||
None => format!("{}{} -> {}", tilde, typ, body.traverse_pi_types()),
|
||||
Some(binder) => format!(
|
||||
"{}({} : {}) -> {}",
|
||||
tilde,
|
||||
binder,
|
||||
typ,
|
||||
body.traverse_pi_types()
|
||||
),
|
||||
}
|
||||
}
|
||||
ExprKind::Sigma { param, fst, snd } => match param {
|
||||
None => format!("{} -> {}", fst, snd.traverse_pi_types()),
|
||||
Some(binder) => format!("[{} : {}] -> {}", binder, fst, snd.traverse_pi_types()),
|
||||
},
|
||||
_ => format!("{}", self),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Literal {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
match self {
|
||||
@ -430,7 +486,7 @@ impl Display for Binding {
|
||||
impl Display for AppBinding {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
if self.erased {
|
||||
write!(f, "-({})", self.data)
|
||||
write!(f, "~({})", self.data)
|
||||
} else {
|
||||
write!(f, "{}", self.data)
|
||||
}
|
||||
@ -471,7 +527,7 @@ impl Display for Expr {
|
||||
typ: None,
|
||||
body,
|
||||
erased: true,
|
||||
} => write!(f, "(-({}) => {})", param, body),
|
||||
} => write!(f, "(~({}) => {})", param, body),
|
||||
Lambda {
|
||||
param,
|
||||
typ: Some(typ),
|
||||
|
@ -5,6 +5,8 @@
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
use crate::symbol::{Ident, QualifiedIdent};
|
||||
use crate::telescope::Telescope;
|
||||
|
||||
use expr::Expr;
|
||||
use fxhash::FxHashMap;
|
||||
use kind_span::{Locatable, Range};
|
||||
@ -18,48 +20,6 @@ pub mod visitor;
|
||||
|
||||
pub use expr::*;
|
||||
|
||||
/// A sequence of arguments that depends on the previous sequence
|
||||
/// it's similar to a iterated sigma type.
|
||||
#[derive(Debug, Clone, Hash, PartialEq, Eq)]
|
||||
pub struct Telescope<T>(Vec<T>);
|
||||
|
||||
impl<T> Default for Telescope<T> {
|
||||
fn default() -> Self {
|
||||
Self(Default::default())
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> Telescope<T> {
|
||||
pub fn new(vec: Vec<T>) -> Telescope<T> {
|
||||
Telescope(vec)
|
||||
}
|
||||
|
||||
pub fn len(&self) -> usize {
|
||||
self.0.len()
|
||||
}
|
||||
|
||||
pub fn push(&mut self, el: T) {
|
||||
self.0.push(el)
|
||||
}
|
||||
|
||||
pub fn as_slice(&self) -> &[T] {
|
||||
self.0.as_slice()
|
||||
}
|
||||
|
||||
pub fn to_vec(self) -> Vec<T> {
|
||||
self.0
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> Telescope<T>
|
||||
where
|
||||
T: Clone,
|
||||
{
|
||||
pub fn drop(self, num: usize) -> Telescope<T> {
|
||||
Telescope(self.0[num..].to_vec())
|
||||
}
|
||||
}
|
||||
|
||||
/// A value of a attribute
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub enum AttributeStyle {
|
||||
@ -207,9 +167,14 @@ pub struct EntryMeta {
|
||||
/// by joining a bunch of books that are already resolved.
|
||||
#[derive(Clone, Debug, Default)]
|
||||
pub struct Book {
|
||||
pub names: LinkedHashMap<String, QualifiedIdent>, // Ordered hashset
|
||||
pub entries: FxHashMap<String, TopLevel>, // Probably deterministic order everytime
|
||||
pub count: FxHashMap<String, EntryMeta>, // Stores some important information in order to desugarize
|
||||
// Ordered hashset
|
||||
pub names: LinkedHashMap<String, QualifiedIdent>,
|
||||
|
||||
// Probably deterministic order everytime
|
||||
pub entries: FxHashMap<String, TopLevel>,
|
||||
|
||||
// Stores some important information in order to desugarize
|
||||
pub count: FxHashMap<String, EntryMeta>,
|
||||
}
|
||||
|
||||
impl Book {
|
||||
@ -234,7 +199,7 @@ impl Display for Constructor {
|
||||
writeln!(f, " /// {}", doc)?;
|
||||
}
|
||||
write!(f, "{}", self.name)?;
|
||||
for arg in &self.args.0 {
|
||||
for arg in self.args.iter() {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
if let Some(res) = &self.typ {
|
||||
@ -255,13 +220,13 @@ impl Display for TopLevel {
|
||||
writeln!(f, "{}", attr)?;
|
||||
}
|
||||
write!(f, "type {}", sum.name)?;
|
||||
for arg in &sum.parameters.0 {
|
||||
for arg in sum.parameters.iter() {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
if !sum.indices.is_empty() {
|
||||
write!(f, " ~")?;
|
||||
}
|
||||
for arg in &sum.indices.0 {
|
||||
for arg in sum.indices.iter() {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
writeln!(f, " {{")?;
|
||||
@ -278,7 +243,7 @@ impl Display for TopLevel {
|
||||
writeln!(f, "{}", attr)?;
|
||||
}
|
||||
write!(f, "record {}", rec.name)?;
|
||||
for arg in &rec.parameters.0 {
|
||||
for arg in rec.parameters.iter() {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
writeln!(f, " {{")?;
|
||||
@ -344,7 +309,7 @@ impl Display for Entry {
|
||||
|
||||
write!(f, "{}", self.name.clone())?;
|
||||
|
||||
for arg in &self.args.0 {
|
||||
for arg in self.args.iter() {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
|
||||
@ -415,49 +380,11 @@ impl Locatable for AttributeStyle {
|
||||
}
|
||||
}
|
||||
|
||||
impl<A> Telescope<A> {
|
||||
pub fn extend(&self, other: &Telescope<A>) -> Telescope<A>
|
||||
where
|
||||
A: Clone,
|
||||
{
|
||||
Telescope([self.0.as_slice(), other.0.as_slice()].concat())
|
||||
}
|
||||
|
||||
pub fn map<B, F>(&self, f: F) -> Telescope<B>
|
||||
where
|
||||
F: FnMut(&A) -> B,
|
||||
{
|
||||
Telescope(self.0.iter().map(f).collect())
|
||||
}
|
||||
|
||||
pub fn is_empty(&self) -> bool {
|
||||
self.0.is_empty()
|
||||
}
|
||||
|
||||
pub fn iter(&self) -> std::slice::Iter<A> {
|
||||
self.0.iter()
|
||||
}
|
||||
|
||||
pub fn iter_mut(&mut self) -> std::slice::IterMut<A> {
|
||||
self.0.iter_mut()
|
||||
}
|
||||
}
|
||||
|
||||
impl<A> IntoIterator for Telescope<A> {
|
||||
type Item = A;
|
||||
|
||||
type IntoIter = std::vec::IntoIter<A>;
|
||||
|
||||
fn into_iter(self) -> Self::IntoIter {
|
||||
self.0.into_iter()
|
||||
}
|
||||
}
|
||||
|
||||
impl Telescope<Argument> {
|
||||
pub fn count_implicits(&self) -> (usize, usize) {
|
||||
let mut hiddens = 0;
|
||||
let mut erased = 0;
|
||||
for arg in &self.0 {
|
||||
for arg in self.iter() {
|
||||
if arg.hidden {
|
||||
hiddens += 1;
|
||||
}
|
||||
@ -504,20 +431,20 @@ impl Constructor {
|
||||
let mut hiddens = 0;
|
||||
let mut erased = 0;
|
||||
|
||||
hiddens += def.parameters.0.len();
|
||||
erased += def.parameters.0.len();
|
||||
hiddens += def.parameters.len();
|
||||
erased += def.parameters.len();
|
||||
|
||||
arguments = arguments.extend(&def.parameters.map(|x| x.to_implicit()));
|
||||
|
||||
// It tries to use all of the indices if no type
|
||||
// is specified.
|
||||
if self.typ.is_none() {
|
||||
hiddens += def.indices.0.len();
|
||||
erased += def.indices.0.len();
|
||||
hiddens += def.indices.len();
|
||||
erased += def.indices.len();
|
||||
arguments = arguments.extend(&def.indices.map(|x| x.to_implicit()));
|
||||
}
|
||||
|
||||
for arg in &self.args.0 {
|
||||
for arg in self.args.iter() {
|
||||
if arg.erased {
|
||||
erased += 1;
|
||||
}
|
||||
@ -541,7 +468,7 @@ impl Constructor {
|
||||
|
||||
impl RecordDecl {
|
||||
pub fn fields_to_arguments(&self) -> Telescope<Argument> {
|
||||
Telescope(
|
||||
Telescope::new(
|
||||
self.fields
|
||||
.iter()
|
||||
.map(|(name, _docs, typ)| {
|
||||
@ -593,7 +520,7 @@ impl RecordDecl {
|
||||
})
|
||||
.collect();
|
||||
|
||||
arguments = arguments.extend(&Telescope(field_args));
|
||||
arguments = arguments.extend(&Telescope::new(field_args));
|
||||
|
||||
EntryMeta {
|
||||
hiddens,
|
||||
@ -650,11 +577,3 @@ impl Argument {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<A> std::ops::Index<usize> for Telescope<A> {
|
||||
type Output = A;
|
||||
|
||||
fn index(&self, index: usize) -> &Self::Output {
|
||||
&self.0[index]
|
||||
}
|
||||
}
|
||||
|
@ -149,7 +149,7 @@ pub fn walk_literal<T: Visitor>( _: &mut T, _: Range, _: &mut Literal) {}
|
||||
|
||||
pub fn walk_constructor<T: Visitor>(ctx: &mut T, cons: &mut Constructor) {
|
||||
ctx.visit_ident(&mut cons.name);
|
||||
visit_vec!(&mut cons.args.0, arg => ctx.visit_argument(arg));
|
||||
visit_vec!(cons.args.get_vec(), arg => ctx.visit_argument(arg));
|
||||
visit_opt!(&mut cons.typ, arg => ctx.visit_expr(arg))
|
||||
}
|
||||
|
||||
@ -238,7 +238,7 @@ pub fn walk_argument<T: Visitor>(ctx: &mut T, argument: &mut Argument) {
|
||||
|
||||
pub fn walk_entry<T: Visitor>(ctx: &mut T, entry: &mut Entry) {
|
||||
ctx.visit_qualified_ident(&mut entry.name);
|
||||
for arg in &mut entry.args.0 {
|
||||
for arg in entry.args.iter_mut() {
|
||||
ctx.visit_argument(arg)
|
||||
}
|
||||
ctx.visit_expr(&mut entry.typ);
|
||||
@ -317,14 +317,14 @@ pub fn walk_top_level<T: Visitor>(ctx: &mut T, toplevel: &mut TopLevel) {
|
||||
super::TopLevel::SumType(sum) => {
|
||||
ctx.visit_qualified_ident(&mut sum.name);
|
||||
visit_vec!(&mut sum.attrs, arg => ctx.visit_attr(arg));
|
||||
visit_vec!(&mut sum.parameters.0, arg => ctx.visit_argument(arg));
|
||||
visit_vec!(&mut sum.indices.0, arg => ctx.visit_argument(arg));
|
||||
visit_vec!(sum.parameters.get_vec(), arg => ctx.visit_argument(arg));
|
||||
visit_vec!(sum.indices.get_vec(), arg => ctx.visit_argument(arg));
|
||||
visit_vec!(&mut sum.constructors, arg => ctx.visit_constructor(arg));
|
||||
}
|
||||
super::TopLevel::RecordType(rec) => {
|
||||
ctx.visit_qualified_ident(&mut rec.name);
|
||||
visit_vec!(&mut rec.attrs, arg => ctx.visit_attr(arg));
|
||||
visit_vec!(&mut rec.parameters.0, arg => ctx.visit_argument(arg));
|
||||
visit_vec!(rec.parameters.get_vec(), arg => ctx.visit_argument(arg));
|
||||
visit_vec!(&mut rec.fields, (name, _docs, typ) => {
|
||||
ctx.visit_ident(name);
|
||||
ctx.visit_expr(typ);
|
||||
|
@ -357,7 +357,7 @@ impl Expr {
|
||||
format!("{}{} -> {}", tilde, typ, body.traverse_pi_types())
|
||||
} else {
|
||||
let body = body.traverse_pi_types();
|
||||
format!("({}{} : {}) -> {}", tilde, param, typ, body)
|
||||
format!("{}({} : {}) -> {}", tilde, param, typ, body)
|
||||
}
|
||||
}
|
||||
_ => format!("{}", self),
|
||||
@ -368,7 +368,7 @@ impl Expr {
|
||||
impl Display for AppBinding {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
|
||||
if self.erased {
|
||||
write!(f, "-({})", self.data)
|
||||
write!(f, "~({})", self.data)
|
||||
} else {
|
||||
write!(f, "{}", self.data)
|
||||
}
|
||||
|
@ -14,11 +14,16 @@ pub mod desugared;
|
||||
/// The untyped AST.
|
||||
pub mod untyped;
|
||||
|
||||
/// Telescope (Iterated sigma type representation)
|
||||
pub mod telescope;
|
||||
|
||||
/// Describes symbols (identifiers) on the language. It will
|
||||
/// be really useful when we change the Symbol to take a number
|
||||
/// instead of a string due to optimizations.
|
||||
pub mod symbol;
|
||||
|
||||
use std::fmt::{Formatter, Display, Error};
|
||||
|
||||
pub use hvm::syntax as backend;
|
||||
use symbol::Ident;
|
||||
|
||||
@ -55,3 +60,28 @@ pub enum Operator {
|
||||
Gtn,
|
||||
Neq,
|
||||
}
|
||||
|
||||
impl Display for Operator {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
use Operator::*;
|
||||
|
||||
match self {
|
||||
Add => write!(f, "+"),
|
||||
Sub => write!(f, "-"),
|
||||
Mul => write!(f, "*"),
|
||||
Div => write!(f, "/"),
|
||||
Mod => write!(f, "%"),
|
||||
And => write!(f, "&"),
|
||||
Or => write!(f, "|"),
|
||||
Xor => write!(f, "^"),
|
||||
Shl => write!(f, "<<"),
|
||||
Shr => write!(f, ">>"),
|
||||
Ltn => write!(f, "<"),
|
||||
Lte => write!(f, "<="),
|
||||
Eql => write!(f, "=="),
|
||||
Gte => write!(f, ">="),
|
||||
Gtn => write!(f, ">"),
|
||||
Neq => write!(f, "!="),
|
||||
}
|
||||
}
|
||||
}
|
@ -171,6 +171,12 @@ impl Ident {
|
||||
new
|
||||
}
|
||||
|
||||
pub fn add_underscore(&self) -> Ident {
|
||||
let mut new = self.clone();
|
||||
new.data = Symbol::new(format!("{}_", new.data.data));
|
||||
new
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn to_str(&self) -> &str {
|
||||
&self.data.data
|
||||
|
89
crates/kind-tree/src/telescope.rs
Normal file
89
crates/kind-tree/src/telescope.rs
Normal file
@ -0,0 +1,89 @@
|
||||
/// A sequence of arguments that depends on the previous sequence
|
||||
/// it's similar to a iterated sigma type.
|
||||
#[derive(Debug, Clone, Hash, PartialEq, Eq)]
|
||||
pub struct Telescope<T>(Vec<T>);
|
||||
|
||||
impl<T> Default for Telescope<T> {
|
||||
fn default() -> Self {
|
||||
Self(Default::default())
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> Telescope<T> {
|
||||
pub fn new(vec: Vec<T>) -> Telescope<T> {
|
||||
Telescope(vec)
|
||||
}
|
||||
|
||||
pub fn len(&self) -> usize {
|
||||
self.0.len()
|
||||
}
|
||||
|
||||
pub fn push(&mut self, el: T) {
|
||||
self.0.push(el)
|
||||
}
|
||||
|
||||
pub fn as_slice(&self) -> &[T] {
|
||||
self.0.as_slice()
|
||||
}
|
||||
|
||||
pub fn to_vec(self) -> Vec<T> {
|
||||
self.0
|
||||
}
|
||||
|
||||
pub fn get_vec(&mut self) -> &mut Vec<T> {
|
||||
&mut self.0
|
||||
}
|
||||
|
||||
pub fn extend(&self, other: &Telescope<T>) -> Telescope<T>
|
||||
where
|
||||
T: Clone,
|
||||
{
|
||||
Telescope([self.as_slice(), other.as_slice()].concat())
|
||||
}
|
||||
|
||||
pub fn map<B, F>(&self, f: F) -> Telescope<B>
|
||||
where
|
||||
F: FnMut(&T) -> B,
|
||||
{
|
||||
Telescope(self.0.iter().map(f).collect())
|
||||
}
|
||||
|
||||
pub fn is_empty(&self) -> bool {
|
||||
self.0.is_empty()
|
||||
}
|
||||
|
||||
pub fn iter(&self) -> std::slice::Iter<T> {
|
||||
self.0.iter()
|
||||
}
|
||||
|
||||
pub fn iter_mut(&mut self) -> std::slice::IterMut<T> {
|
||||
self.0.iter_mut()
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> Telescope<T>
|
||||
where
|
||||
T: Clone,
|
||||
{
|
||||
pub fn drop(self, num: usize) -> Telescope<T> {
|
||||
Telescope(self.0[num..].to_vec())
|
||||
}
|
||||
}
|
||||
|
||||
impl<A> IntoIterator for Telescope<A> {
|
||||
type Item = A;
|
||||
|
||||
type IntoIter = std::vec::IntoIter<A>;
|
||||
|
||||
fn into_iter(self) -> Self::IntoIter {
|
||||
self.0.into_iter()
|
||||
}
|
||||
}
|
||||
|
||||
impl<A> std::ops::Index<usize> for Telescope<A> {
|
||||
type Output = A;
|
||||
|
||||
fn index(&self, index: usize) -> &Self::Output {
|
||||
&self.0[index]
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue
Block a user