mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
fix: bugs with match derivation
This commit is contained in:
parent
7c30696479
commit
a68a8a90b2
@ -92,19 +92,23 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
});
|
||||
|
||||
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 type
|
||||
for cons in &sum.constructors {
|
||||
let vars: Vec<Binding> = cons.args.iter().map(|x| Binding::Positional(mk_var(x.name.clone()))).collect();
|
||||
|
||||
let cons_inst = mk_cons(sum.name.add_segment(cons.name.to_str()), [params.as_slice(), vars.as_slice()].concat());
|
||||
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(),
|
||||
);
|
||||
|
||||
let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) {
|
||||
Some(ExprKind::Constr(_, spine)) => spine
|
||||
.iter()
|
||||
.map(|x| match x {
|
||||
Binding::Positional(expr) => AppBinding::explicit(expr.clone()),
|
||||
Binding::Named(_, _, _) => todo!("Internal Error: Need to reorder"),
|
||||
Binding::Named(_, _, _) => todo!("Incomplete feature: Need to reorder"),
|
||||
})
|
||||
.collect(),
|
||||
_ => [parameter_names.as_slice(), indice_names.as_slice()].concat(),
|
||||
@ -114,8 +118,13 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
|
||||
let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range);
|
||||
|
||||
let cons_type = cons
|
||||
.args
|
||||
let args = if cons.typ.is_some() {
|
||||
cons.args.clone()
|
||||
} else {
|
||||
sum.indices.extend(&cons.args)
|
||||
};
|
||||
|
||||
let cons_type = args
|
||||
.iter()
|
||||
.rfold(cons_tipo, |out, arg| mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or_else(mk_typ), out));
|
||||
|
||||
@ -138,11 +147,24 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
let cons_ident = sum.name.add_segment(cons.name.to_str());
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
|
||||
let irrelev = cons.args.map(|x| x.hidden).to_vec();
|
||||
let irrelev: Vec<bool>;
|
||||
let spine_params: Vec<Ident>;
|
||||
let spine: Vec<Ident>;
|
||||
|
||||
let spine_params: Vec<Ident> = sum.parameters.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
|
||||
|
||||
let spine: Vec<Ident> = cons.args.map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
|
||||
if cons.typ.is_none() {
|
||||
irrelev = sum.indices.extend(&cons.args).map(|x| x.hidden).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.hidden).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();
|
||||
}
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
@ -186,12 +208,14 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
cons.name.range,
|
||||
);
|
||||
|
||||
rules.push(Box::new(Rule {
|
||||
let rule = Box::new(Rule {
|
||||
name: name.clone(),
|
||||
pats,
|
||||
body,
|
||||
range: cons.name.range,
|
||||
}))
|
||||
});
|
||||
|
||||
rules.push(rule)
|
||||
}
|
||||
// Rules
|
||||
|
||||
|
@ -554,7 +554,7 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
pub fn parse_pat_destruct_bindings(&mut self) -> Result<(Option<Range>, Vec<CaseBinding>, bool), SyntaxError> {
|
||||
pub fn parse_pat_destruct_bindings(&mut self) -> Result<(Option<Range>, Vec<CaseBinding>, Option<Range>), SyntaxError> {
|
||||
let mut ignore_rest_range = None;
|
||||
let mut bindings = Vec::new();
|
||||
let mut range = None;
|
||||
@ -587,7 +587,7 @@ impl<'a> Parser<'a> {
|
||||
return Err(SyntaxError::IgnoreRestShouldBeOnTheEnd(range));
|
||||
}
|
||||
}
|
||||
Ok((range, bindings, ignore_rest_range.is_some()))
|
||||
Ok((range, bindings, ignore_rest_range))
|
||||
}
|
||||
|
||||
pub fn parse_match(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
|
@ -15,7 +15,7 @@ impl<'a> DesugarState<'a> {
|
||||
type_info: (&Range, String),
|
||||
fields: &[(String, bool)],
|
||||
cases: &[CaseBinding],
|
||||
jump_rest: bool,
|
||||
jump_rest: Option<Range>,
|
||||
) -> Vec<Option<(Range, PatIdent)>> {
|
||||
let mut ordered_fields = vec![None; fields.len()];
|
||||
let mut names = FxHashMap::default();
|
||||
@ -51,7 +51,7 @@ impl<'a> DesugarState<'a> {
|
||||
.map(|(name, _)| name.clone())
|
||||
.collect();
|
||||
|
||||
if !jump_rest && !names.is_empty() {
|
||||
if jump_rest.is_none() && !names.is_empty() {
|
||||
self.send_err(PassError::NoFieldCoverage(*type_info.0, names))
|
||||
}
|
||||
|
||||
@ -95,7 +95,7 @@ impl<'a> DesugarState<'a> {
|
||||
if let Some((_, name)) = arg {
|
||||
arguments.push(name.0)
|
||||
} else {
|
||||
arguments.push(self.gen_name(typ.range))
|
||||
arguments.push(self.gen_name(jump_rest.unwrap_or(typ.range)))
|
||||
}
|
||||
}
|
||||
|
||||
@ -105,7 +105,7 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
let spine = vec![
|
||||
val,
|
||||
desugared::Expr::unfold_lambda(range, &irrelev, &arguments, next(self)),
|
||||
desugared::Expr::unfold_lambda(&irrelev, &arguments, next(self)),
|
||||
];
|
||||
|
||||
self.mk_desugared_fun(range, open_id, spine, false)
|
||||
@ -195,7 +195,7 @@ impl<'a> DesugarState<'a> {
|
||||
if let Some((_, name)) = arg {
|
||||
arguments.push(name.0)
|
||||
} else {
|
||||
arguments.push(self.gen_name(match_.typ.range));
|
||||
arguments.push(self.gen_name(case.ignore_rest.unwrap_or(match_.typ.range)));
|
||||
}
|
||||
}
|
||||
cases_args[index] = Some((case.constructor.range, arguments, &case.value));
|
||||
@ -207,10 +207,9 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
for (i, case_arg) in cases_args.iter().enumerate() {
|
||||
let case = &sum.constructors[i];
|
||||
if let Some((range, arguments, val)) = &case_arg {
|
||||
if let Some((_, arguments, val)) = &case_arg {
|
||||
let case: Vec<bool> = case.args.iter().map(|x| x.erased).rev().collect();
|
||||
lambdas.push(desugared::Expr::unfold_lambda(
|
||||
*range,
|
||||
&case,
|
||||
arguments,
|
||||
self.desugar_expr(val),
|
||||
|
@ -282,7 +282,7 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
}
|
||||
} else if entry.arguments.len() != spine.len() {
|
||||
println!("{}: {:?}", head, entry);
|
||||
println!("Ata {} {:?}", head, spine.iter().map(|x| x.to_string()).collect::<Vec<String>>());
|
||||
self.send_err(PassError::IncorrectArity(
|
||||
head.range,
|
||||
spine.iter().map(|x| x.range).collect(),
|
||||
|
@ -308,7 +308,7 @@ impl<'a> ErasureState<'a> {
|
||||
Lambda(name, body, erased) => {
|
||||
let ctx = self.ctx.clone();
|
||||
if *erased {
|
||||
self.ctx.insert(name.to_string(), (name.range, (Some(name.range), Relevance::Irrelevant)));
|
||||
self.ctx.insert(name.to_string(), (name.range, (None, Relevance::Irrelevant)));
|
||||
} else {
|
||||
self.ctx.insert(name.to_string(), (name.range, *on));
|
||||
}
|
||||
|
@ -57,7 +57,7 @@ pub struct Case {
|
||||
pub constructor: Ident,
|
||||
pub bindings: Vec<CaseBinding>,
|
||||
pub value: Box<Expr>,
|
||||
pub ignore_rest: bool,
|
||||
pub ignore_rest: Option<Range>,
|
||||
}
|
||||
|
||||
/// A match block that will be desugared
|
||||
@ -100,7 +100,7 @@ pub enum Literal {
|
||||
/// and just translates into a eliminator for records.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub enum Destruct {
|
||||
Destruct(Range, QualifiedIdent, Vec<CaseBinding>, bool),
|
||||
Destruct(Range, QualifiedIdent, Vec<CaseBinding>, Option<Range>),
|
||||
Ident(Ident),
|
||||
}
|
||||
|
||||
@ -284,7 +284,7 @@ impl Display for Destruct {
|
||||
for binding in bindings {
|
||||
write!(f, " {}", binding)?;
|
||||
}
|
||||
if *ignore {
|
||||
if ignore.is_some() {
|
||||
write!(f, " ..")?;
|
||||
}
|
||||
Ok(())
|
||||
@ -338,7 +338,7 @@ impl Display for Case {
|
||||
for bind in &self.bindings {
|
||||
write!(f, " {}", bind)?
|
||||
}
|
||||
if self.ignore_rest {
|
||||
if self.ignore_rest.is_some() {
|
||||
write!(f, " ..")?;
|
||||
}
|
||||
write!(f, " => {}; ", self.value)
|
||||
|
@ -112,12 +112,12 @@ impl Expr {
|
||||
})
|
||||
}
|
||||
|
||||
pub fn unfold_lambda(range: Range, irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
|
||||
pub fn unfold_lambda(irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
|
||||
idents
|
||||
.iter()
|
||||
.rev()
|
||||
.zip(irrelev)
|
||||
.fold(body, |body, (ident, irrelev)| Expr::lambda(range, ident.clone(), body, *irrelev))
|
||||
.fold(body, |body, (ident, irrelev)| Expr::lambda(ident.range, ident.clone(), body, *irrelev))
|
||||
}
|
||||
|
||||
pub fn app(range: Range, ident: Box<Expr>, spine: Vec<AppBinding>) -> Box<Expr> {
|
||||
|
Loading…
Reference in New Issue
Block a user