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

feat: fixed erasure (wip app, pi and forall erasure)

Browse Source
This commit is contained in:
Felipe g 2022-11-10 20:15:15 -03:00
parent f68df12bd2
commit c011978fab
16 changed files with 288 additions and 354 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -62,9 +62,7 @@ fn mk_ctr(name: String, args: Vec<Box<Term>>) -> Box<Term> {
}
fn mk_var(ident: &str) -> Box<Term> {
Box::new(Term::Var {
name: ident.to_string(),
})
Box::new(Term::Var { name: ident.to_string() })
}
fn mk_u60(numb: u64) -> Box<Term> {
@ -72,10 +70,7 @@ fn mk_u60(numb: u64) -> Box<Term> {
}
fn mk_single_ctr(head: String) -> Box<Term> {
Box::new(Term::Ctr {
name: head,
args: vec![],
})
Box::new(Term::Ctr { name: head, args: vec![] })
}
fn mk_ctr_name(ident: &QualifiedIdent) -> Box<Term> {
@ -84,26 +79,15 @@ fn mk_ctr_name(ident: &QualifiedIdent) -> Box<Term> {
}
fn span_to_num(span: Span) -> Box<Term> {
Box::new(Term::Num {
numb: span.encode().0,
})
Box::new(Term::Num { numb: span.encode().0 })
}
fn set_origin(ident: &Ident) -> Box<Term> {
mk_quoted_ctr(
"Kind.Term.set_origin".to_owned(),
vec![
span_to_num(Span::Locatable(ident.range)),
mk_var(ident.to_str()),
],
)
mk_quoted_ctr("Kind.Term.set_origin".to_owned(), vec![span_to_num(Span::Locatable(ident.range)), mk_var(ident.to_str())])
}
fn lam(name: &Ident, body: Box<Term>) -> Box<Term> {
Box::new(Term::Lam {
name: name.to_string(),
body,
})
Box::new(Term::Lam { name: name.to_string(), body })
}
fn codegen_str(input: &str) -> Box<Term> {
@ -121,13 +105,7 @@ fn codegen_str(input: &str) -> Box<Term> {
)
}
fn codegen_all_expr(
lhs_rule: bool,
lhs: bool,
num: &mut usize,
quote: bool,
expr: &Expr,
) -> Box<Term> {
fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, expr: &Expr) -> Box<Term> {
use kind_tree::desugared::ExprKind::*;
match &expr.data {
@ -141,11 +119,7 @@ fn codegen_all_expr(
*num += 1;
mk_quoted_ctr(
eval_ctr(quote, TermTag::Var),
vec![
span_to_num(expr.span),
mk_u60(ident.encode()),
mk_u60((*num - 1) as u64),
],
vec![span_to_num(expr.span), mk_u60(ident.encode()), mk_u60((*num - 1) as u64)],
)
} else {
mk_var(ident.to_str())
@ -162,25 +136,24 @@ fn codegen_all_expr(
),
Lambda(name, body) => 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)),
],
),
App(head, spine) => spine.iter().fold(
codegen_all_expr(lhs_rule, lhs, num, quote, head),
|left, right| {
mk_quoted_ctr(
eval_ctr(quote, TermTag::App),
vec![
span_to_num(expr.span),
left,
codegen_all_expr(lhs_rule, lhs, num, quote, &right.clone()),
],
)
},
vec![span_to_num(expr.span), mk_u60(name.encode()), lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body))],
),
App(head, spine) => spine.iter().fold(codegen_all_expr(lhs_rule, lhs, num, quote, head), |left, right| {
mk_quoted_ctr(
eval_ctr(quote, TermTag::App),
vec![
span_to_num(expr.span),
left,
codegen_all_expr(
lhs_rule,
lhs,
num,
quote,
&right.data
),
],
)
}),
Ctr(name, spine) => mk_quoted_ctr(
eval_ctr(quote, TermTag::Ctr(spine.len())),
vec_preppend![
@ -190,11 +163,7 @@ fn codegen_all_expr(
],
),
Fun(name, spine) => {
let new_spine: Vec<Box<Term>> = spine
.iter()
.cloned()
.map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x))
.collect();
let new_spine: Vec<Box<Term>> = spine.iter().cloned().map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)).collect();
if quote {
mk_quoted_ctr(
eval_ctr(quote, TermTag::Fun(new_spine.len())),
@ -241,11 +210,8 @@ fn codegen_all_expr(
codegen_all_expr(lhs_rule, lhs, num, quote, expr),
],
),
Num(desugared::Num::U60(n)) => mk_quoted_ctr(
eval_ctr(quote, TermTag::Num),
vec![span_to_num(expr.span), mk_u60(*n)],
),
Num(desugared::Num::U120(n)) => todo!(),
Num(desugared::Num::U60(n)) => mk_quoted_ctr(eval_ctr(quote, TermTag::Num), vec![span_to_num(expr.span), mk_u60(*n)]),
Num(desugared::Num::U120(_)) => todo!(),
Binary(operator, left, right) => mk_quoted_ctr(
eval_ctr(quote, TermTag::Binary),
vec![
@ -255,10 +221,7 @@ fn codegen_all_expr(
codegen_all_expr(lhs_rule, lhs, num, quote, right),
],
),
Hole(num) => mk_quoted_ctr(
eval_ctr(quote, TermTag::Hole),
vec![span_to_num(expr.span), mk_u60(*num)],
),
Hole(num) => mk_quoted_ctr(eval_ctr(quote, TermTag::Hole), vec![span_to_num(expr.span), mk_u60(*num)]),
Hlp(_) => mk_quoted_ctr(eval_ctr(quote, TermTag::Hlp), vec![span_to_num(expr.span)]),
Str(input) => codegen_str(input),
Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"),
@ -294,17 +257,11 @@ fn codegen_vec<T>(exprs: T) -> Box<Term>
where
T: Iterator<Item = Box<Term>>,
{
exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| {
mk_ctr("List.cons".to_string(), vec![right, left])
})
exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| mk_ctr("List.cons".to_string(), vec![right, left]))
}
fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) {
let base_vars = lift_spine(
(0..rule.pats.len())
.map(|x| mk_var(&format!("x{}", x)))
.collect::<Vec<Box<lang::Term>>>(),
);
let base_vars = lift_spine((0..rule.pats.len()).map(|x| mk_var(&format!("x{}", x))).collect::<Vec<Box<lang::Term>>>());
file.rules.push(lang::Rule {
lhs: mk_ctr(
@ -346,11 +303,7 @@ fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) {
fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) {
let mut count = 0;
let lhs_args = rule
.pats
.iter()
.map(|x| codegen_pattern(&mut count, false, x))
.collect::<Vec<Box<Term>>>();
let lhs_args = rule.pats.iter().map(|x| codegen_pattern(&mut count, false, x)).collect::<Vec<Box<Term>>>();
file.rules.push(lang::Rule {
lhs: mk_ctr(
@ -367,21 +320,9 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
TermTag::HoasF(rule.name.to_string()).to_string(),
vec![
mk_var("orig"),
mk_var("a"),
mk_var("r"),
mk_var("log"),
mk_var("ret"),
],
),
rhs: mk_ctr(
"HVM.put".to_owned(),
vec![
mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]),
mk_var("ret"),
],
vec![mk_var("orig"), mk_var("a"), mk_var("r"), mk_var("log"), mk_var("ret")],
),
rhs: mk_ctr("HVM.put".to_owned(), vec![mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]), mk_var("ret")]),
});
} else {
file.rules.push(lang::Rule {
@ -397,13 +338,7 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) {
}
}
fn codegen_entry_rules(
count: &mut usize,
index: usize,
args: &mut Vec<Box<Term>>,
entry: &desugared::Rule,
pats: &[Box<desugared::Expr>],
) -> Box<Term> {
fn codegen_entry_rules(count: &mut usize, index: usize, args: &mut Vec<Box<Term>>, entry: &desugared::Rule, pats: &[Box<desugared::Expr>]) -> Box<Term> {
if pats.is_empty() {
mk_ctr(
"Kind.Rule.rhs".to_owned(),
@ -420,13 +355,7 @@ fn codegen_entry_rules(
let pat = &pats[0];
let expr = codegen_all_expr(true, false, count, false, pat);
args.push(expr.clone());
mk_ctr(
"Kind.Rule.lhs".to_owned(),
vec![
expr,
codegen_entry_rules(count, index + 1, args, entry, &pats[1..]),
],
)
mk_ctr("Kind.Rule.lhs".to_owned(), vec![expr, codegen_entry_rules(count, index + 1, args, entry, &pats[1..])])
}
}
@ -446,9 +375,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
rhs: codegen_type(&entry.args, &entry.typ),
});
let base_vars = (0..entry.args.len())
.map(|x| mk_var(&format!("x{}", x)))
.collect::<Vec<Box<lang::Term>>>();
let base_vars = (0..entry.args.len()).map(|x| mk_var(&format!("x{}", x))).collect::<Vec<Box<lang::Term>>>();
file.rules.push(lang::Rule {
lhs: mk_ctr(
@ -494,10 +421,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
codegen_rule_end(file, &entry.rules[0])
}
let rules = entry
.rules
.iter()
.map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats));
let rules = entry.rules.iter().map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats));
file.rules.push(lang::Rule {
lhs: mk_ctr("RuleOf".to_owned(), vec![mk_ctr_name(&entry.name)]),

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

@ -63,14 +63,8 @@ fn parse_name(term: &Term) -> Result<String, String> {
fn parse_qualified(term: &Term) -> Result<QualifiedIdent, String> {
match term {
Term::Num { numb } => Ok(QualifiedIdent::new_static(
&Ident::decode(*numb),
None,
Range::ghost_range(),
)),
Term::Ctr { name, args: _ } => {
Ok(QualifiedIdent::new_static(name, None, Range::ghost_range()))
}
Term::Num { numb } => Ok(QualifiedIdent::new_static(&Ident::decode(*numb), None, Range::ghost_range())),
Term::Ctr { name, args: _ } => Ok(QualifiedIdent::new_static(name, None, Range::ghost_range())),
_ => Err("Error while matching opt".to_string()),
}
}
@ -79,10 +73,7 @@ fn parse_expr(term: &Term) -> Result<Box<desugared::Expr>, String> {
parse_all_expr(Default::default(), term)
}
fn parse_all_expr(
names: im::HashMap<String, String>,
term: &Term,
) -> Result<Box<desugared::Expr>, String> {
fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box<desugared::Expr>, String> {
match term {
Term::Ctr { name, args } => match name.as_str() {
"Kind.Quoted.all" => Ok(Expr::all(
@ -103,16 +94,9 @@ fn parse_all_expr(
parse_all_expr(names, &args[3])?,
)),
"Kind.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
"Kind.Quoted.var" => Ok(Expr::var(Ident::new(
parse_name(&args[1])?,
parse_orig(&args[0])?,
))),
"Kind.Quoted.var" => Ok(Expr::var(Ident::new(parse_name(&args[1])?, parse_orig(&args[0])?))),
"Kind.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)),
"Kind.Quoted.ann" => Ok(Expr::ann(
parse_orig(&args[0])?,
parse_all_expr(names.clone(), &args[1])?,
parse_all_expr(names, &args[2])?,
)),
"Kind.Quoted.ann" => Ok(Expr::ann(parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, parse_all_expr(names, &args[2])?)),
"Kind.Quoted.sub" => Ok(Expr::sub(
parse_orig(&args[0])?,
Ident::generate(&parse_name(&args[1])?),
@ -123,43 +107,37 @@ fn parse_all_expr(
"Kind.Quoted.app" => Ok(Expr::app(
parse_orig(&args[0])?,
parse_all_expr(names.clone(), &args[1])?,
vec![parse_all_expr(names, &args[2])?],
)),
"Kind.Quoted.ctr" => Ok(Expr::ctr(
parse_orig(&args[1])?,
parse_qualified(&args[0])?,
{
let mut res = Vec::new();
for arg in parse_list(&args[2])? {
res.push(parse_all_expr(names.clone(), &arg)?);
vec![
desugared::AppBinding {
data: parse_all_expr(names, &args[2])?,
erased: false,
}
res
},
)),
"Kind.Quoted.fun" => Ok(Expr::fun(
parse_orig(&args[0])?,
parse_qualified(&args[1])?,
{
let mut res = Vec::new();
for arg in &args[1..] {
res.push(parse_all_expr(names.clone(), arg)?);
}
res
},
],
)),
"Kind.Quoted.ctr" => Ok(Expr::ctr(parse_orig(&args[1])?, parse_qualified(&args[0])?, {
let mut res = Vec::new();
for arg in parse_list(&args[2])? {
res.push(parse_all_expr(names.clone(), &arg)?);
}
res
})),
"Kind.Quoted.fun" => Ok(Expr::fun(parse_orig(&args[0])?, parse_qualified(&args[1])?, {
let mut res = Vec::new();
for arg in &args[1..] {
res.push(parse_all_expr(names.clone(), arg)?);
}
res
})),
"Kind.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
"Kind.Quoted.u60" => Ok(Expr::u60(parse_orig(&args[0])?)),
"Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120?
"Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120?
"Kind.Quoted.op2" => Ok(Expr::binary(
parse_orig(&args[0])?,
parse_op(&args[1])?,
parse_all_expr(names.clone(), &args[2])?,
parse_all_expr(names, &args[3])?,
)),
tag => Err(format!(
"Unexpected tag on transforming quoted term {:?}",
tag
)),
tag => Err(format!("Unexpected tag on transforming quoted term {:?}", tag)),
},
_ => Err("Unexpected term on transforming quoted term".to_string()),
}
@ -222,14 +200,8 @@ fn parse_type_error(expr: &Term) -> Result<TypeError, String> {
parse_all_expr(im::HashMap::new(), &args[2])?,
parse_all_expr(im::HashMap::new(), &args[3])?,
)),
"Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection(
ctx,
orig,
parse_all_expr(im::HashMap::new(), &args[2])?,
)),
"Kind.Error.Quoted.too_many_arguments" => {
Ok(TypeError::TooManyArguments(ctx, orig))
}
"Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection(ctx, orig, parse_all_expr(im::HashMap::new(), &args[2])?)),
"Kind.Error.Quoted.too_many_arguments" => Ok(TypeError::TooManyArguments(ctx, orig)),
"Kind.Error.Quoted.type_mismatch" => Ok(TypeError::TypeMismatch(
ctx,
orig,

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

@ -10,12 +10,7 @@ use kind_tree::symbol::{Ident, QualifiedIdent};
/// Derives an eliminator from a sum type declaration.
pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
let mk_var = |name: Ident| -> Box<Expr> {
Box::new(Expr {
data: ExprKind::Var(name),
range,
})
};
let mk_var = |name: Ident| -> Box<Expr> { Box::new(Expr { data: ExprKind::Var(name), range }) };
let mk_cons = |name: QualifiedIdent, spine: Vec<Binding>| -> Box<Expr> {
Box::new(Expr {
@ -24,7 +19,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
})
};
let mk_app = |left: Box<Expr>, right: Vec<Binding>, range: Range| -> Box<Expr> {
let mk_app = |left: Box<Expr>, right: Vec<AppBinding>, range: Range| -> Box<Expr> {
Box::new(Expr {
data: ExprKind::App(left, right),
range,
@ -60,26 +55,11 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
// The type
let all_args = sum.parameters.extend(&sum.indices);
let res_motive_ty = mk_cons(
sum.name.clone(),
all_args
.iter()
.cloned()
.map(|x| Binding::Positional(mk_var(x.name)))
.collect(),
);
let res_motive_ty = mk_cons(sum.name.clone(), all_args.iter().cloned().map(|x| Binding::Positional(mk_var(x.name))).collect());
let parameter_names: Vec<Binding> = sum
.parameters
.iter()
.map(|x| Binding::Positional(mk_var(x.name.clone())))
.collect();
let parameter_names: Vec<AppBinding> = sum.parameters.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect();
let indice_names: Vec<Binding> = sum
.indices
.iter()
.map(|x| Binding::Positional(mk_var(x.name.clone())))
.collect();
let indice_names: Vec<AppBinding> = sum.indices.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect();
// Sccrutinzies
@ -95,16 +75,13 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
let motive_ident = Ident::new_static("motive", range);
let motive_type = sum.parameters.extend(&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_type = sum
.parameters
.extend(&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)
});
types.push(Argument {
hidden: false,
@ -114,39 +91,33 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
range,
});
let params = sum
.parameters
.map(|x| Binding::Positional(mk_var(x.name.clone())));
let params = sum.parameters.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 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(), vars.as_slice()].concat());
let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) {
Some(ExprKind::Constr(_, spine)) => spine.to_vec(),
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"),
})
.collect(),
_ => [parameter_names.as_slice(), indice_names.as_slice()].concat(),
};
indices_of_cons.push(Binding::Positional(cons_inst));
indices_of_cons.push(AppBinding::explicit(cons_inst));
let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range);
let cons_type = cons.args.iter().rfold(cons_tipo, |out, arg| {
mk_pi(
arg.name.clone(),
arg.typ.clone().unwrap_or_else(mk_typ),
out,
)
});
let cons_type = cons
.args
.iter()
.rfold(cons_tipo, |out, arg| mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or_else(mk_typ), out));
types.push(Argument {
hidden: false,
@ -157,8 +128,8 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
});
}
let mut res: Vec<Binding> = [parameter_names.as_slice(), indice_names.as_slice()].concat();
res.push(Binding::Positional(mk_var(Ident::generate("scrutinizer"))));
let mut res: Vec<AppBinding> = [parameter_names.as_slice(), 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 mut rules = Vec::new();
@ -167,16 +138,11 @@ 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 spine_params: Vec<Ident> = sum
.parameters
.extend(&cons.args)
.map(|x| x.name.with_name(|f| format!("{}_", f)))
.to_vec();
let irrelev = cons.args.map(|x| x.hidden).to_vec();
let spine: Vec<Ident> = cons
.args
.map(|x| x.name.with_name(|f| format!("{}_", f)))
.to_vec();
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();
pats.push(Box::new(Pat {
data: concrete::pat::PatKind::App(
@ -211,7 +177,11 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
mk_var(cons.name.clone()),
spine
.iter()
.map(|arg| Binding::Positional(mk_var(arg.clone())))
.zip(irrelev)
.map(|(arg, erased)| AppBinding {
data: mk_var(arg.clone()),
erased,
})
.collect(),
cons.name.range,
);

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

@ -22,7 +22,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
})
};
let mk_app = |left: Box<Expr>, right: Vec<Binding>| -> Box<Expr> {
let mk_app = |left: Box<Expr>, right: Vec<AppBinding>| -> Box<Expr> {
Box::new(Expr {
data: ExprKind::App(left, right),
range,
@ -126,7 +126,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
mk_var(Ident::generate("fun_")),
spine
.iter()
.map(|arg| Binding::Positional(mk_var(arg.clone())))
.map(|arg| AppBinding { data: mk_var(arg.clone()), erased: false })
.collect(),
);

1
src/kind-driver/src/lib.rs
View File

@ -49,7 +49,6 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book>
pub fn erase_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
let concrete_book = to_book(session, path)?;
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
println!("Desugared: {}", desugared_book);
erasure::erase_book(
&desugared_book,
session.diagnostic_sender.clone(),

6
src/kind-driver/src/resolution.rs
View File

@ -152,7 +152,7 @@ fn parse_and_store_book_by_identifier<'a>(
match ident_to_path(&session.root, ident, true) {
Ok(Some(path)) => parse_and_store_book_by_path(session, &path, book),
Ok(None) => true,
Ok(None) => false,
Err(err) => {
session.diagnostic_sender.send(err).unwrap();
true
@ -179,8 +179,8 @@ fn parse_and_store_book_by_path<'a>(
return true;
}
};
let ctx_id = session.book_counter;
let ctx_id = session.book_counter;
session.add_path(Rc::new(path.to_path_buf()), input.clone());
let (mut module, mut failed) =
@ -200,7 +200,7 @@ fn parse_and_store_book_by_path<'a>(
}
}
failed |= expand_uses(&mut module, session.diagnostic_sender.clone());
expand_uses(&mut module, session.diagnostic_sender.clone());
module_to_book(&mut failed, session, &module, book);

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

@ -66,22 +66,16 @@ impl<'a> Parser<'a> {
unused = true;
}
if unused {
self.errs
.send(SyntaxError::UnusedDocString(start.mix(last)).into())
.unwrap()
self.errs.send(SyntaxError::UnusedDocString(start.mix(last)).into()).unwrap()
}
}
pub fn is_pi_type(&self) -> bool {
self.get().same_variant(&Token::LPar)
&& self.peek(1).is_lower_id()
&& self.peek(2).same_variant(&Token::Colon)
self.get().same_variant(&Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Colon)
}
pub fn is_named_parameter(&self) -> bool {
self.get().same_variant(&Token::LPar)
&& self.peek(1).is_lower_id()
&& self.peek(2).same_variant(&Token::Eq)
self.get().same_variant(&Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Eq)
}
pub fn is_lambda(&self) -> bool {
@ -89,9 +83,7 @@ impl<'a> Parser<'a> {
}
pub fn is_sigma_type(&self) -> bool {
self.get().same_variant(&Token::LBracket)
&& self.peek(1).is_lower_id()
&& self.peek(2).same_variant(&Token::Colon)
self.get().same_variant(&Token::LBracket) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Colon)
}
pub fn is_substitution(&self) -> bool {
@ -126,8 +118,7 @@ impl<'a> Parser<'a> {
pub fn parse_upper_id(&mut self) -> Result<QualifiedIdent, SyntaxError> {
let range = self.range();
let (start, end) =
eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?;
let (start, end) = eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?;
let ident = QualifiedIdent::new_static(start.as_str(), end, range);
Ok(ident)
}
@ -217,10 +208,7 @@ impl<'a> Parser<'a> {
"U60" => ExprKind::Lit(Literal::U60),
_ => ExprKind::Constr(id.clone(), vec![]),
};
Ok(Box::new(Expr {
range: id.range,
data,
}))
Ok(Box::new(Expr { range: id.range, data }))
}
fn parse_data(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxError> {
@ -283,10 +271,7 @@ impl<'a> Parser<'a> {
if self.check_actual(Token::RBracket) {
let range = self.advance().1.mix(range);
return Ok(Box::new(Expr {
range,
data: ExprKind::List(vec),
}));
return Ok(Box::new(Expr { range, data: ExprKind::List(vec) }));
}
vec.push(*self.parse_expr(false)?);
@ -316,10 +301,7 @@ impl<'a> Parser<'a> {
let end = self.eat_variant(Token::RBracket)?.1;
let range = range.mix(end);
Ok(Box::new(Expr {
range,
data: ExprKind::List(vec),
}))
Ok(Box::new(Expr { range, data: ExprKind::List(vec) }))
}
fn parse_paren(&mut self) -> Result<Box<Expr>, SyntaxError> {
@ -400,13 +382,39 @@ 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 start = self.range();
self.advance(); // '{'
let atom = self.parse_expr(true)?;
self.eat_closing_keyword(Token::RBrace, start)?;
(true, atom)
} else {
(false, self.parse_expr(false)?)
};
Ok(AppBinding { data, erased })
}
fn parse_call(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxError> {
if self.get().is_upper_id() {
self.parse_data(multiline)
} else {
let head = self.parse_atom()?;
let start = head.range;
let (end, spine) = self.parse_call_tail(start, multiline)?;
let mut spine = Vec::new();
let mut end = start;
while (!self.is_linebreak() || multiline) && !self.get().same_variant(&Token::Eof) {
if let Some(atom) = self.try_single(&|parser| parser.parse_app_binding())? {
end = atom.data.range;
spine.push(atom)
} else {
break;
}
}
if spine.is_empty() {
Ok(head)
} else {
@ -418,21 +426,15 @@ impl<'a> Parser<'a> {
}
}
fn parse_call_tail(
&mut self,
start: Range,
multiline: bool,
) -> Result<(Range, Vec<Binding>), SyntaxError> {
fn parse_call_tail(&mut self, start: Range, multiline: bool) -> Result<(Range, Vec<Binding>), SyntaxError> {
let mut spine = Vec::new();
let mut end = start;
while (!self.is_linebreak() || multiline) && !self.get().same_variant(&Token::Eof) {
let res = self.try_single(&|parser| parser.parse_binding())?;
match res {
Some(atom) => {
end = atom.locate();
spine.push(atom)
}
None => break,
if let Some(atom) = self.try_single(&|parser| parser.parse_binding())? {
end = atom.locate();
spine.push(atom)
} else {
break;
}
}
Ok((end, spine))
@ -478,12 +480,7 @@ impl<'a> Parser<'a> {
if self.get().is_upper_id() {
let upper = self.parse_upper_id()?;
let (range, bindings, ignore_rest) = self.parse_pat_destruct_bindings()?;
Ok(Destruct::Destruct(
upper.range.mix(range.unwrap_or(upper.range)),
upper,
bindings,
ignore_rest,
))
Ok(Destruct::Destruct(upper.range.mix(range.unwrap_or(upper.range)), upper, bindings, ignore_rest))
} else {
let name = self.parse_id()?;
Ok(Destruct::Ident(name))
@ -556,9 +553,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>, bool), SyntaxError> {
let mut ignore_rest_range = None;
let mut bindings = Vec::new();
let mut range = None;
@ -629,12 +624,7 @@ impl<'a> Parser<'a> {
None
};
let match_ = Box::new(Match {
typ,
scrutinizer,
cases,
motive,
});
let match_ = Box::new(Match { typ, scrutinizer, cases, motive });
Ok(Box::new(Expr {
data: ExprKind::Match(match_),

11
src/kind-pass/src/desugar/app.rs
View File

@ -175,13 +175,10 @@ impl<'a> DesugarState<'a> {
let mut new_spine = Vec::new();
let new_head = self.desugar_expr(head);
for arg in spine {
match arg {
Binding::Positional(v) => new_spine.push(self.desugar_expr(v)),
Binding::Named(r, _, v) => {
self.send_err(PassError::CannotUseNamed(head.range, *r));
new_spine.push(self.desugar_expr(v))
}
}
new_spine.push(desugared::AppBinding {
data: self.desugar_expr(&arg.data),
erased: arg.erased
})
}
desugared::Expr::app(range, new_head, new_spine)
}

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

@ -223,7 +223,7 @@ impl<'a> DesugarState<'a> {
let motive = if let Some(res) = &match_.motive {
self.desugar_expr(res)
} else {
let mut idx: Vec<Ident> = sum.indices.iter().map(|x| x.name.clone()).collect();
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)

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

@ -16,7 +16,7 @@ use fxhash::{FxHashMap, FxHashSet};
use kind_report::data::DiagnosticFrame;
use kind_span::Range;
use kind_tree::desugared::{Book, Entry, Expr, ExprKind, Rule};
use kind_tree::{desugared::{Book, Entry, Expr, ExprKind, Rule, self}, symbol::{QualifiedIdent}};
use crate::errors::PassError;
@ -211,41 +211,60 @@ impl<'a> ErasureState<'a> {
self.unify_loop(range, left, right, &mut Default::default(), relevance_unify)
}
pub fn erase_pat(&mut self, on: (Option<Range>, Relevance), pat: &Expr) {
pub fn erase_pat_spine(&mut self, on: (Option<Range>, Relevance), name: &QualifiedIdent, spine: &Vec<Box<Expr>>) -> Vec<Box<Expr>> {
let fun = match self.names.get(&name.to_string()) {
Some(res) => *res,
None => self.new_hole(name.range, name.to_string()),
};
if !self.unify(name.range, on, fun, true) {
self.err_irrelevant(None, name.range, None)
}
let entry = self.book.entrs.get(name.to_string().as_str()).unwrap();
let erased = entry.args.iter();
let irrelevances = erased.map(|arg| {
if on.1 == Relevance::Irrelevant {
on
} else if arg.erased {
(Some(arg.span), Relevance::Irrelevant)
} else {
(Some(arg.span), Relevance::Relevant)
}
});
spine
.iter()
.zip(irrelevances)
.map(|(arg, relev)| (self.erase_pat(relev, arg), relev.1.clone()))
.filter(|res| res.1 == Relevance::Relevant)
.map(|res| res.0)
.collect()
}
pub fn erase_pat(&mut self, on: (Option<Range>, Relevance), pat: &Expr) -> Box<Expr> {
use kind_tree::desugared::ExprKind::*;
match &pat.data {
Num(_) | Str(_) => (),
Num(_) | Str(_) => Box::new(pat.clone()),
Var(name) => {
self.ctx.insert(name.to_string(), (name.range, on));
Box::new(pat.clone())
}
Fun(name, spine) | Ctr(name, spine) => {
let fun = match self.names.get(&name.to_string()) {
Some(res) => *res,
None => self.new_hole(name.range, name.to_string()),
};
if !self.unify(name.range, on, fun, true) {
self.err_irrelevant(None, name.range, None)
}
let entry = self.book.entrs.get(name.to_string().as_str()).unwrap();
let erased = entry.args.iter();
let irrelevances = erased.map(|arg| {
if on.1 == Relevance::Irrelevant {
on
} else if arg.erased {
(Some(arg.span), Relevance::Irrelevant)
} else {
(Some(arg.span), Relevance::Relevant)
}
});
spine
.iter()
.zip(irrelevances)
.for_each(|(arg, relev)| self.erase_pat(relev, arg));
Fun(name, spine) => {
let spine = self.erase_pat_spine(on, &name, spine);
Box::new(Expr {
span: pat.span.clone(),
data: ExprKind::Fun(name.clone(), spine),
})
}
Ctr(name, spine) => {
let spine = self.erase_pat_spine(on, &name, spine);
Box::new(Expr {
span: pat.span.clone(),
data: ExprKind::Ctr(name.clone(), spine),
})
}
res => panic!("Internal Error: Not a pattern {:?}", res),
}
@ -313,7 +332,17 @@ impl<'a> ErasureState<'a> {
}
App(head, spine) => {
let head = self.erase_expr(on, head);
let spine = spine.iter().map(|x| self.erase_expr(on, x)).collect();
let spine = spine.iter().map(|x| {
let on = if x.erased {
(x.data.span.to_range(), Relevance::Irrelevant)
} else {
on.clone()
};
desugared::AppBinding {
data: self.erase_expr(&on, &x.data),
erased: x.erased
}
}).filter(|x| !x.erased).collect();
Box::new(Expr {
span: expr.span,
data: ExprKind::App(head, spine),
@ -414,26 +443,22 @@ impl<'a> ErasureState<'a> {
) -> Rule {
let ctx = self.ctx.clone();
args.iter()
let new_pats : Vec<_> = args.iter()
.zip(rule.pats.iter())
.for_each(|((range, erased), expr)| {
self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr)
});
.map(|((range, erased), expr)| {
(erased, self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr))
})
.filter(|(erased, _)| !*erased)
.map(|res| res.1)
.collect();
let body = self.erase_expr(place, &rule.body);
self.ctx = ctx;
let new_pats = args
.iter()
.zip(rule.pats.iter())
.filter(|((_, erased), _)| !*erased)
.map(|res| res.1)
.cloned();
Rule {
name: rule.name.clone(),
pats: new_pats.collect(),
pats: new_pats,
body,
span: rule.span,
}

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

@ -372,7 +372,7 @@ impl Visitor for UnboundCollector {
}
ExprKind::App(head, spine) => {
self.visit_expr(head);
visit_vec!(spine.iter_mut(), arg => self.visit_binding(arg));
visit_vec!(spine.iter_mut(), arg => self.visit_expr(&mut arg.data));
}
ExprKind::Ann(val, ty) => {
self.visit_expr(val);

7
src/kind-span/src/lib.rs
View File

@ -95,6 +95,13 @@ impl Span {
Span::Generated
}
pub fn to_range(&self) -> Option<Range> {
match self {
Span::Generated => None,
Span::Locatable(pos) => Some(pos.clone()),
}
}
/// Join two spans and keeps the syntax context of the
/// first locatable range. If it's generated then it
/// will be ignored and the other span will be the canonical

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

@ -16,7 +16,7 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
App(head, spine) => spine.iter().fold(compile_term(head), |func, arg| {
Box::new(Term::App {
func,
argm: compile_term(arg),
argm: compile_term(&arg.data),
})
}),
Fun(head, spine) | Ctr(head, spine) => Box::new(Term::Ctr {

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

@ -24,6 +24,21 @@ pub enum Binding {
/// Vector of bindings
pub type Spine = Vec<Binding>;
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
pub struct AppBinding {
pub data: Box<Expr>,
pub erased: bool
}
impl AppBinding {
pub fn explicit(data: Box<Expr>) -> AppBinding {
AppBinding {
data,
erased: false,
}
}
}
/// A case binding is a field or a rename of some field
/// inside a match expression.
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
@ -121,7 +136,7 @@ pub enum ExprKind {
/// A anonymous function that receives one argument
Lambda(Ident, Option<Box<Expr>>, Box<Expr>),
/// Application of a expression to a spine of expressions
App(Box<Expr>, Spine),
App(Box<Expr>, Vec<AppBinding>),
/// Declaration of a local variable
Let(Destruct, Box<Expr>, Box<Expr>),
/// Type ascription (x : y)
@ -362,6 +377,16 @@ impl Display for Binding {
}
}
impl Display for AppBinding {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
if self.erased {
write!(f, "{{{}}}", self.data)
} else {
write!(f, "{}", self.data)
}
}
}
impl Display for Expr {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
use ExprKind::*;

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

@ -35,6 +35,7 @@ macro_rules! visit_opt {
}
use kind_span::{Range, SyntaxCtxIndex};
pub(crate) use visit_opt;
pub(crate) use visit_vec;
@ -71,6 +72,10 @@ pub trait Visitor: Sized {
walk_ident(self, ident);
}
fn visit_app_binding(&mut self, ident: &mut AppBinding) {
walk_app_binding(self, ident);
}
fn visit_destruct(&mut self, ident: &mut Destruct) {
walk_destruct(self, ident);
}
@ -186,6 +191,10 @@ pub fn walk_binding<T: Visitor>(ctx: &mut T, binding: &mut Binding) {
}
}
pub fn walk_app_binding<T: Visitor>(ctx: &mut T, binding: &mut AppBinding) {
ctx.visit_expr(&mut binding.data)
}
pub fn walk_case_binding<T: Visitor>(ctx: &mut T, binding: &mut CaseBinding) {
match binding {
CaseBinding::Field(ident) => ctx.visit_pat_ident(ident),
@ -413,7 +422,7 @@ pub fn walk_expr<T: Visitor>(ctx: &mut T, expr: &mut Expr) {
ExprKind::App(expr, spine) => {
ctx.visit_expr(expr);
for arg in spine {
ctx.visit_binding(arg);
ctx.visit_app_binding(arg);
}
}
ExprKind::List(spine) => {

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

@ -17,6 +17,12 @@ use crate::{
/// as ((((a b) c) d) e) that looks like a spine.
pub type Spine = Vec<Box<Expr>>;
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
pub struct AppBinding {
pub data: Box<Expr>,
pub erased: bool
}
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
pub enum ExprKind {
/// Name of a variable
@ -26,7 +32,7 @@ pub enum ExprKind {
/// A anonymous function that receives one argument
Lambda(Ident, Box<Expr>),
/// Application of a expression to a spine of expressions
App(Box<Expr>, Spine),
App(Box<Expr>, Vec<AppBinding>),
/// Application of a function
Fun(QualifiedIdent, Spine),
/// Application of a Construtor
@ -113,7 +119,7 @@ impl Expr {
.fold(body, |body, ident| Expr::lambda(range, ident.clone(), body))
}
pub fn app(range: Range, ident: Box<Expr>, spine: Vec<Box<Expr>>) -> Box<Expr> {
pub fn app(range: Range, ident: Box<Expr>, spine: Vec<AppBinding>) -> Box<Expr> {
Box::new(Expr {
span: Span::Locatable(range),
data: ExprKind::App(ident, spine),
@ -306,6 +312,16 @@ impl Expr {
}
}
impl Display for AppBinding {
fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
if self.erased {
write!(f, "{{{}}}", self.data)
} else {
write!(f, "{}", self.data)
}
}
}
impl Display for Expr {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
use ExprKind::*;