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: problems with open and erasure of lambdas

Browse Source
This commit is contained in:
Felipe g 2022-11-11 08:01:57 -03:00
parent c011978fab
commit 7c30696479
14 changed files with 73 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/kind-checker/src/compiler/mod.rs
View File

@ -134,7 +134,7 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp
lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body)),
],
),
Lambda(name, body) => mk_quoted_ctr(
Lambda(name, body, erased) => mk_quoted_ctr(
eval_ctr(quote, TermTag::Lambda),
vec![span_to_num(expr.span), mk_u60(name.encode()), lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body))],
),

1
src/kind-checker/src/report.rs
View File

@ -86,6 +86,7 @@ fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box
parse_orig(&args[0])?,
Ident::generate(&parse_name(&args[1])?),
parse_all_expr(names, &args[2])?,
false // TODO: Fix
)),
"Kind.Quoted.let" => Ok(Expr::let_(
parse_orig(&args[0])?,

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

@ -7,7 +7,7 @@ use kind_tree::concrete::*;
use kind_tree::concrete::{self};
use kind_tree::symbol::{Ident, QualifiedIdent};
pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
let mk_var = |name: Ident| -> Box<Expr> {
Box::new(Expr {
data: ExprKind::Var(name),
@ -36,19 +36,19 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
})
};
let name = sum.name.add_segment("open");
let name = rec.name.add_segment("open");
let mut types = Telescope::default();
for arg in sum.parameters.iter() {
for arg in rec.parameters.iter() {
types.push(arg.to_implicit())
}
// The type
let all_args = sum.parameters.clone();
let all_args = rec.parameters.clone();
let res_motive_ty = mk_cons(
sum.name.clone(),
rec.name.clone(),
all_args
.iter()
.cloned()
@ -66,7 +66,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
let cons_tipo = mk_var(Ident::generate("_res"));
let cons_type = sum.fields.iter().rfold(cons_tipo, |out, (name, _, typ)| {
let cons_type = rec.fields.iter().rfold(cons_tipo, |out, (name, _, typ)| {
mk_pi(name.clone(), typ.clone(), out)
});
@ -94,7 +94,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
let mut pats: Vec<Box<Pat>> = Vec::new();
let spine: Vec<Ident> = sum
let spine: Vec<Ident> = rec
.fields
.iter()
.map(|(name, _, _)| name.with_name(|f| format!("{}_", f)))
@ -102,7 +102,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
pats.push(Box::new(Pat {
data: concrete::pat::PatKind::App(
sum.name.add_segment(sum.constructor.to_str()),
rec.name.add_segment(rec.constructor.to_str()),
spine
.iter()
.cloned()
@ -137,7 +137,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
range,
})];
Entry {
let entry = Entry {
name,
docs: Vec::new(),
args: types,
@ -145,5 +145,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
rules,
range,
attrs: Vec::new(),
}
};
entry
}

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

@ -133,7 +133,7 @@ impl<'a> Parser<'a> {
let end_range = expr.range;
Ok(Box::new(Expr {
data: ExprKind::Lambda(ident, None, expr),
data: ExprKind::Lambda(ident, None, expr, false),
range: name_span.mix(end_range),
}))
}
@ -152,7 +152,7 @@ impl<'a> Parser<'a> {
let body = self.parse_expr(false)?;
Ok(Box::new(Expr {
range: range.mix(body.range),
data: ExprKind::Lambda(ident, Some(typ), body),
data: ExprKind::Lambda(ident, Some(typ), body, false),
}))
} else if self.check_and_eat(Token::RightArrow) {
let body = self.parse_expr(false)?;
@ -384,15 +384,16 @@ impl<'a> Parser<'a> {
fn parse_app_binding(&mut self) -> Result<AppBinding, SyntaxError> {
self.ignore_docs();
let (erased, data) = if self.get().same_variant(&Token::LBrace) {
let (erased, data) = /*if self.get().same_variant(&Token::LBrace) {
let start = self.range();
self.advance(); // '{'
let atom = self.parse_expr(true)?;
let atom = self.parse_atom()?;
self.eat_closing_keyword(Token::RBrace, start)?;
(true, atom)
} else {
(false, self.parse_expr(false)?)
};
} else {*/
(false, self.parse_atom()?)
// }
;
Ok(AppBinding { data, erased })
}
@ -594,6 +595,7 @@ impl<'a> Parser<'a> {
self.advance(); // 'match'
let typ = self.parse_upper_id()?;
let scrutinizer = self.parse_expr(false)?;
self.eat_variant(Token::LBrace)?;

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

@ -69,6 +69,7 @@ impl<'a> DesugarState<'a> {
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 {
record
@ -100,9 +101,11 @@ impl<'a> DesugarState<'a> {
let open_id = typ.add_segment("open");
let irrelev = count.arguments.map(|x| x.erased).to_vec();
let spine = vec![
val,
desugared::Expr::unfold_lambda(range, &arguments, next(self)),
desugared::Expr::unfold_lambda(range, &irrelev, &arguments, next(self)),
];
self.mk_desugared_fun(range, open_id, spine, false)
@ -174,6 +177,7 @@ impl<'a> DesugarState<'a> {
self.send_err(PassError::DuplicatedNamed(range, case.constructor.range));
} else {
let sum_c = &sum.constructors[index];
let ordered = self.order_case_arguments(
(&case.constructor.range, case.constructor.to_string()),
&sum_c
@ -204,8 +208,10 @@ 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 {
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),
))
@ -226,7 +232,7 @@ impl<'a> DesugarState<'a> {
let mut idx: Vec<Ident> = sum.parameters.extend(&sum.indices).iter().map(|x| x.name.clone()).collect();
idx.push(Ident::generate("_val"));
idx.iter().rfold(self.gen_hole_expr(), |expr, l| {
desugared::Expr::lambda(l.range, l.clone(), expr)
desugared::Expr::lambda(l.range, l.clone(), expr, false)
})
};

8
src/kind-pass/src/desugar/expr.rs
View File

@ -51,7 +51,7 @@ impl<'a> DesugarState<'a> {
this.mk_desugared_fun(
range,
bind_ident.clone(),
vec![expr, desugared::Expr::lambda(range, name, next)],
vec![expr, desugared::Expr::lambda(range, name, next, false)],
false,
)
};
@ -150,7 +150,7 @@ impl<'a> DesugarState<'a> {
let spine = vec![
self.desugar_expr(typ),
desugared::Expr::lambda(range, name, self.desugar_expr(body)),
desugared::Expr::lambda(range, name, self.desugar_expr(body), true),
];
self.mk_desugared_ctr(range, sigma, spine, false)
@ -244,8 +244,8 @@ impl<'a> DesugarState<'a> {
self.desugar_expr(left),
self.desugar_expr(right),
),
Lambda(ident, _typ, body) => {
desugared::Expr::lambda(expr.range, ident.clone(), self.desugar_expr(body))
Lambda(ident, _typ, body, erased) => {
desugared::Expr::lambda(expr.range, ident.clone(), self.desugar_expr(body), *erased)
}
Ann(val, typ) => {
desugared::Expr::ann(expr.range, self.desugar_expr(val), self.desugar_expr(typ))

8
src/kind-pass/src/desugar/top_level.rs
View File

@ -266,9 +266,7 @@ impl<'a> DesugarState<'a> {
// inductive types can be used in patterns.
}
let (hidden, _erased) = entry.arguments.count_implicits();
let fill_hidden = spine.len() == entry.arguments.len() - hidden;
let fill_hidden = spine.len() == entry.arguments.len() - entry.hiddens;
let mut new_spine = Vec::new();
@ -284,12 +282,12 @@ impl<'a> DesugarState<'a> {
}
}
} else if entry.arguments.len() != spine.len() {
println!("{}", pat);
println!("{}: {:?}", head, entry);
self.send_err(PassError::IncorrectArity(
head.range,
spine.iter().map(|x| x.range).collect(),
entry.arguments.len(),
hidden,
entry.hiddens,
));
return desugared::Expr::err(pat.range);
} else {

20
src/kind-pass/src/erasure/mod.rs
View File

@ -305,16 +305,24 @@ impl<'a> ErasureState<'a> {
Box::new(expr.clone())
}
Lambda(name, body) => {
Lambda(name, body, erased) => {
let ctx = self.ctx.clone();
self.ctx.insert(name.to_string(), (name.range, *on));
if *erased {
self.ctx.insert(name.to_string(), (name.range, (Some(name.range), Relevance::Irrelevant)));
} else {
self.ctx.insert(name.to_string(), (name.range, *on));
}
let body = self.erase_expr(on, body);
self.ctx = ctx;
Box::new(Expr {
span: expr.span,
data: ExprKind::Lambda(name.clone(), body),
})
if *erased {
body
} else {
Box::new(Expr {
span: expr.span,
data: ExprKind::Lambda(name.clone(), body, *erased),
})
}
}
Let(name, val, body) => {
let ctx = self.ctx.clone();

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

@ -361,7 +361,7 @@ impl Visitor for UnboundCollector {
self.visit_expr(body);
self.context_vars.pop();
}
ExprKind::Lambda(ident, binder, body) => {
ExprKind::Lambda(ident, binder, body, erased) => {
match binder {
Some(x) => self.visit_expr(x),
None => (),

2
src/kind-target-hvm/src/lib.rs
View File

@ -9,7 +9,7 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
Var(name) => Box::new(Term::Var {
name: name.to_string(),
}),
Lambda(binder, body) => Box::new(Term::Lam {
Lambda(binder, body, _erased) => Box::new(Term::Lam {
name: binder.to_string(),
body: compile_term(body),
}),

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

@ -134,7 +134,7 @@ pub enum ExprKind {
/// The dependent product space (e.g. [x : Int] -> y)
Sigma(Option<Ident>, Box<Expr>, Box<Expr>),
/// A anonymous function that receives one argument
Lambda(Ident, Option<Box<Expr>>, Box<Expr>),
Lambda(Ident, Option<Box<Expr>>, Box<Expr>, bool),
/// Application of a expression to a spine of expressions
App(Box<Expr>, Vec<AppBinding>),
/// Declaration of a local variable
@ -402,8 +402,10 @@ impl Display for Expr {
head,
spine.iter().map(|x| format!(" {}", x)).collect::<String>()
),
Lambda(binder, None, body) => write!(f, "({} => {})", binder, body),
Lambda(binder, Some(typ), body) => write!(f, "(({} : {}) => {})", binder, typ, body),
Lambda(binder, None, body, false) => write!(f, "({} => {})", binder, body),
Lambda(binder, Some(typ), body, false) => write!(f, "(({} : {}) => {})", binder, typ, body),
Lambda(binder, None, body, true) => write!(f, "({{{}}} => {})", binder, body),
Lambda(binder, Some(typ), body, true) => write!(f, "({{{} : {}}} => {})", binder, typ, body),
Pair(fst, snd) => write!(f, "($ {} {})", fst, snd),
App(head, spine) => write!(
f,

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

@ -548,13 +548,13 @@ impl RecordDecl {
}
pub fn extract_book_info_of_constructor(&self) -> EntryMeta {
let mut arguments = Telescope::default();
let mut arguments;
let mut hiddens = 0;
let mut erased = 0;
hiddens += self.parameters.0.len();
erased += self.parameters.0.len();
arguments = arguments.extend(&self.parameters);
hiddens += self.parameters.len();
erased += self.parameters.len();
arguments = self.parameters.map(|x| x.to_implicit());
let field_args: Vec<Argument> = self
.fields

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

@ -411,7 +411,7 @@ pub fn walk_expr<T: Visitor>(ctx: &mut T, expr: &mut Expr) {
ctx.visit_qualified_ident(ident);
ctx.visit_sttm(sttm)
}
ExprKind::Lambda(ident, binder, body) => {
ExprKind::Lambda(ident, binder, body, _erased) => {
ctx.visit_ident(ident);
match binder {
Some(x) => ctx.visit_expr(x),

16
src/kind-tree/src/desugared/mod.rs
View File

@ -30,7 +30,7 @@ pub enum ExprKind {
/// The dependent function space (e.g. (x : Int) -> y)
All(Ident, Box<Expr>, Box<Expr>),
/// A anonymous function that receives one argument
Lambda(Ident, Box<Expr>),
Lambda(Ident, Box<Expr>, bool),
/// Application of a expression to a spine of expressions
App(Box<Expr>, Vec<AppBinding>),
/// Application of a function
@ -98,25 +98,26 @@ impl Expr {
})
}
pub fn lambda(range: Range, ident: Ident, body: Box<Expr>) -> Box<Expr> {
pub fn lambda(range: Range, ident: Ident, body: Box<Expr>, erased: bool) -> Box<Expr> {
Box::new(Expr {
span: Span::Locatable(range),
data: ExprKind::Lambda(ident, body),
data: ExprKind::Lambda(ident, body, erased),
})
}
pub fn identity_lambda(ident: Ident) -> Box<Expr> {
Box::new(Expr {
span: Span::Generated,
data: ExprKind::Lambda(ident.clone(), Self::var(ident)),
data: ExprKind::Lambda(ident.clone(), Self::var(ident), false),
})
}
pub fn unfold_lambda(range: Range, idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
pub fn unfold_lambda(range: Range, irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
idents
.iter()
.rev()
.fold(body, |body, ident| Expr::lambda(range, ident.clone(), body))
.zip(irrelev)
.fold(body, |body, (ident, irrelev)| Expr::lambda(range, ident.clone(), body, *irrelev))
}
pub fn app(range: Range, ident: Box<Expr>, spine: Vec<AppBinding>) -> Box<Expr> {
@ -334,7 +335,8 @@ impl Display for Expr {
Num(self::Num::U120(n)) => write!(f, "{}u120", n),
All(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
Var(name) => write!(f, "{}", name),
Lambda(binder, body) => write!(f, "({} => {})", binder, body),
Lambda(binder, body, false) => write!(f, "({} => {})", binder, body),
Lambda(binder, body, true) => write!(f, "({{{}}} => {})", binder, body),
Sub(name, _, redx, expr) => write!(f, "({} ## {}/{})", expr, name, redx),
App(head, spine) => write!(
f,