mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
merge: add mutter, setter and getter syntax (#485)
Add mutter, setter and getter syntax
This commit is contained in:
commit
6301f8377d
@ -150,7 +150,7 @@ pub fn compile_in_session<T>(
|
||||
eprintln!();
|
||||
|
||||
render_to_stderr(
|
||||
&render_config,
|
||||
render_config,
|
||||
&session,
|
||||
&Log::Checking(format!("The file '{}'", file)),
|
||||
);
|
||||
@ -168,12 +168,12 @@ pub fn compile_in_session<T>(
|
||||
contains_error = true;
|
||||
}
|
||||
|
||||
render_to_stderr(&render_config, &session, &diagnostic)
|
||||
render_to_stderr(render_config, &session, &diagnostic)
|
||||
}
|
||||
|
||||
if !contains_error {
|
||||
render_to_stderr(
|
||||
&render_config,
|
||||
render_config,
|
||||
&session,
|
||||
&if compiled {
|
||||
Log::Compiled(start.elapsed())
|
||||
@ -186,7 +186,7 @@ pub fn compile_in_session<T>(
|
||||
|
||||
res
|
||||
} else {
|
||||
render_to_stderr(&render_config, &session, &Log::Failed(start.elapsed()));
|
||||
render_to_stderr(render_config, &session, &Log::Failed(start.elapsed()));
|
||||
eprintln!();
|
||||
|
||||
match res {
|
||||
|
@ -288,6 +288,16 @@ impl<'a> Visitor for Subst<'a> {
|
||||
self.visit_expr(motive);
|
||||
}
|
||||
}
|
||||
ExprKind::SeqRecord(sec) => {
|
||||
use kind_tree::concrete::SeqOperation::*;
|
||||
self.visit_expr(&mut sec.expr);
|
||||
self.visit_expr(&mut sec.typ);
|
||||
match &mut sec.operation {
|
||||
Set(expr) => self.visit_expr(expr),
|
||||
Mut(expr) => self.visit_expr(expr),
|
||||
Get => (),
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -292,7 +292,7 @@ pub fn check_unbound_top_level(session: &mut Session, book: &mut Book) -> anyhow
|
||||
}
|
||||
|
||||
for unbound in unbound_names.values() {
|
||||
unbound_variable(session, book, &unbound);
|
||||
unbound_variable(session, book, unbound);
|
||||
failed = true;
|
||||
}
|
||||
|
||||
|
@ -879,6 +879,42 @@ impl<'a> Parser<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_seq(&mut self) -> Result<Box<Expr>, SyntaxDiagnostic> {
|
||||
let start = self.range();
|
||||
self.eat_variant(Token::Bang)?;
|
||||
let typ = self.parse_atom()?;
|
||||
let name = self.parse_atom()?;
|
||||
let mut fields = vec![];
|
||||
let mut end = self.range();
|
||||
while let Token::Dot = &self.get() {
|
||||
self.advance();
|
||||
end = self.range();
|
||||
fields.push(self.parse_id()?);
|
||||
}
|
||||
let operation = if self.check_and_eat(Token::Eq) {
|
||||
let expr = self.parse_expr(false)?;
|
||||
end = expr.range;
|
||||
SeqOperation::Set(expr)
|
||||
} else if self.check_and_eat(Token::AtEq) {
|
||||
let expr = self.parse_expr(false)?;
|
||||
end = expr.range;
|
||||
SeqOperation::Mut(expr)
|
||||
} else {
|
||||
SeqOperation::Get
|
||||
};
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::SeqRecord(
|
||||
SeqRecord {
|
||||
typ,
|
||||
expr: name,
|
||||
fields,
|
||||
operation,
|
||||
}
|
||||
),
|
||||
range: start.mix(end),
|
||||
}))
|
||||
}
|
||||
|
||||
/// The infinite hell of else ifs. But it's the most readable way
|
||||
/// to check if the queue of tokens match a pattern as we need
|
||||
/// some looakhead tokens.
|
||||
@ -904,6 +940,8 @@ impl<'a> Parser<'a> {
|
||||
self.parse_pi_or_lambda(false)
|
||||
} else if self.is_sigma_type() {
|
||||
self.parse_sigma_type()
|
||||
} else if self.check_actual(Token::Bang) {
|
||||
self.parse_seq()
|
||||
} else if self.check_actual(Token::Tilde) {
|
||||
self.parse_erased()
|
||||
} else {
|
||||
|
@ -175,7 +175,20 @@ impl<'a> Lexer<'a> {
|
||||
';' => self.single_token(Token::Semi, start),
|
||||
'$' => self.single_token(Token::Dollar, start),
|
||||
',' => self.single_token(Token::Comma, start),
|
||||
'+' => self.single_token(Token::Plus, start),
|
||||
'+' => {
|
||||
self.next_char();
|
||||
match self.peekable.peek() {
|
||||
Some('=') => self.single_token(Token::PlusEq, start),
|
||||
_ => (Token::Plus, self.mk_range(start)),
|
||||
}
|
||||
}
|
||||
'@' => {
|
||||
self.next_char();
|
||||
match self.peekable.peek() {
|
||||
Some('=') => self.single_token(Token::AtEq, start),
|
||||
_ => (Token::At, self.mk_range(start)),
|
||||
}
|
||||
}
|
||||
'-' => {
|
||||
self.next_char();
|
||||
match self.peekable.peek() {
|
||||
|
@ -75,6 +75,10 @@ pub enum Token {
|
||||
BangEq,
|
||||
Bang,
|
||||
|
||||
PlusEq,
|
||||
AtEq,
|
||||
At,
|
||||
|
||||
HashHash,
|
||||
Hash,
|
||||
|
||||
@ -181,6 +185,9 @@ impl fmt::Display for Token {
|
||||
Token::With => write!(f, "with"),
|
||||
Token::Return => write!(f, "return"),
|
||||
Token::Ask => write!(f, "ask"),
|
||||
Token::PlusEq => write!(f, "+="),
|
||||
Token::AtEq => write!(f, "@="),
|
||||
Token::At => write!(f, "@"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -1,6 +1,6 @@
|
||||
use kind_span::{Locatable, Range};
|
||||
use kind_tree::concrete::{self, expr, Literal, TopLevel};
|
||||
use kind_tree::desugared::{self};
|
||||
use kind_tree::desugared::{self, Expr};
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
|
||||
use crate::diagnostic::{PassDiagnostic, Sugar};
|
||||
@ -40,15 +40,15 @@ impl<'a> DesugarState<'a> {
|
||||
let list_ident = QualifiedIdent::new_static("Nat", None, range);
|
||||
let cons_ident = list_ident.add_segment("succ");
|
||||
let nil_ident = list_ident.add_segment("zero");
|
||||
|
||||
|
||||
let mut res = self.mk_desugared_ctr(range, nil_ident, Vec::new(), false);
|
||||
|
||||
for _ in 0..*num {
|
||||
res = self.mk_desugared_ctr(range, cons_ident.clone(), vec![res], false)
|
||||
}
|
||||
|
||||
|
||||
res
|
||||
},
|
||||
}
|
||||
Literal::NumU120(num) => {
|
||||
if !self.check_implementation("U120.new", range, Sugar::U120) {
|
||||
return desugared::Expr::err(range);
|
||||
@ -74,6 +74,111 @@ impl<'a> DesugarState<'a> {
|
||||
)
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_seq(
|
||||
&mut self,
|
||||
range: Range,
|
||||
sub: &expr::SeqRecord,
|
||||
) -> Box<desugared::Expr> {
|
||||
use concrete::SeqOperation::*;
|
||||
|
||||
let typ = self.desugar_expr(&sub.typ);
|
||||
|
||||
let mut value = vec![];
|
||||
self.desugar_record_field_sequence(range, &mut value, typ, &sub.fields);
|
||||
|
||||
if self.failed {
|
||||
return Expr::err(range)
|
||||
}
|
||||
|
||||
match &sub.operation {
|
||||
Set(expr) => {
|
||||
let value_ident = Ident::generate("_value");
|
||||
let expr = self.desugar_expr(&expr);
|
||||
|
||||
let mut result = value.iter().rfold(expr, |acc, (typ, field)| {
|
||||
let name = typ.add_segment(field.to_str()).add_segment("mut");
|
||||
|
||||
if self.failed || !self.check_implementation(name.to_str(), range, Sugar::Mutter(typ.to_string())) {
|
||||
return desugared::Expr::err(range);
|
||||
}
|
||||
|
||||
self.mk_desugared_ctr(
|
||||
range,
|
||||
name,
|
||||
vec![
|
||||
Expr::var(value_ident.clone()),
|
||||
Expr::lambda(range.clone(), value_ident.clone(), acc, false),
|
||||
],
|
||||
false,
|
||||
)
|
||||
});
|
||||
|
||||
if let desugared::ExprKind::Ctr { args, .. } = &mut result.data {
|
||||
args[0] = self.desugar_expr(&sub.expr);
|
||||
}
|
||||
|
||||
result
|
||||
}
|
||||
Mut(expr) => {
|
||||
let value_ident = Ident::generate("_value");
|
||||
let expr = self.desugar_expr(&expr);
|
||||
|
||||
let result = value.iter().rfold(expr, |acc, (typ, field)| {
|
||||
let name = typ.add_segment(field.to_str()).add_segment("mut");
|
||||
|
||||
if self.failed || !self.check_implementation(name.to_str(), range, Sugar::Mutter(typ.to_string())) {
|
||||
return desugared::Expr::err(range);
|
||||
}
|
||||
|
||||
Expr::lambda(
|
||||
name.range.clone(),
|
||||
value_ident.clone(),
|
||||
self.mk_desugared_ctr(
|
||||
range,
|
||||
name,
|
||||
vec![Expr::var(value_ident.clone()), acc],
|
||||
false,
|
||||
),
|
||||
false,
|
||||
)
|
||||
});
|
||||
|
||||
if self.failed {
|
||||
return Expr::err(range)
|
||||
}
|
||||
|
||||
let mut result = if let desugared::ExprKind::Lambda { body, .. } = result.data {
|
||||
body
|
||||
} else {
|
||||
self.send_err(PassDiagnostic::NeedsAField(
|
||||
sub.expr.range.clone()
|
||||
));
|
||||
return Expr::err(range)
|
||||
};
|
||||
|
||||
match &mut result.data {
|
||||
desugared::ExprKind::Ctr { args, .. } => {
|
||||
args[0] = self.desugar_expr(&sub.expr);
|
||||
}
|
||||
_ => (),
|
||||
}
|
||||
|
||||
result
|
||||
}
|
||||
Get => value
|
||||
.iter()
|
||||
.fold(self.desugar_expr(&sub.expr), |acc, (typ, field)| {
|
||||
let name = typ.add_segment(field.to_str()).add_segment("get");
|
||||
|
||||
if self.failed || !self.check_implementation(name.to_str(), range, Sugar::Getter(typ.to_string())) {
|
||||
return desugared::Expr::err(range);
|
||||
}
|
||||
|
||||
self.mk_desugared_ctr(range, name, vec![acc], false)
|
||||
}),
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_sttm(
|
||||
&mut self,
|
||||
bind_ident: &QualifiedIdent,
|
||||
@ -157,7 +262,10 @@ impl<'a> DesugarState<'a> {
|
||||
let pure = self.old_book.names.get(pure_ident.to_str());
|
||||
|
||||
if bind.is_none() || pure.is_none() {
|
||||
self.send_err(PassDiagnostic::NeedToImplementMethods(range, Sugar::DoNotation));
|
||||
self.send_err(PassDiagnostic::NeedToImplementMethods(
|
||||
range,
|
||||
Sugar::DoNotation,
|
||||
));
|
||||
return desugared::Expr::err(range);
|
||||
}
|
||||
|
||||
@ -249,7 +357,7 @@ impl<'a> DesugarState<'a> {
|
||||
type_name: &QualifiedIdent,
|
||||
var_name: &Ident,
|
||||
motive: &Option<Box<expr::Expr>>,
|
||||
next: &expr::Expr
|
||||
next: &expr::Expr,
|
||||
) -> Box<desugared::Expr> {
|
||||
let rec = self.old_book.entries.get(type_name.to_str());
|
||||
|
||||
@ -270,16 +378,23 @@ impl<'a> DesugarState<'a> {
|
||||
return desugared::Expr::err(range);
|
||||
}
|
||||
|
||||
let field_names : Vec<_> = record.fields.iter().map(|x| var_name.add_segment(x.0.to_str())).collect();
|
||||
let field_names: Vec<_> = record
|
||||
.fields
|
||||
.iter()
|
||||
.map(|x| var_name.add_segment(x.0.to_str()))
|
||||
.collect();
|
||||
|
||||
let irrelev = vec![false; field_names.len()];
|
||||
|
||||
let motive = motive.as_ref().map(|x| self.desugar_expr(x)).unwrap_or_else(|| self.gen_hole_expr(range));
|
||||
let motive = motive
|
||||
.as_ref()
|
||||
.map(|x| self.desugar_expr(x))
|
||||
.unwrap_or_else(|| self.gen_hole_expr(range));
|
||||
|
||||
let spine = vec![
|
||||
desugared::Expr::var(var_name.clone()),
|
||||
desugared::Expr::lambda(range, var_name.clone(), motive, false),
|
||||
desugared::Expr::unfold_lambda(&irrelev, &field_names, self.desugar_expr(next))
|
||||
desugared::Expr::unfold_lambda(&irrelev, &field_names, self.desugar_expr(next)),
|
||||
];
|
||||
|
||||
self.mk_desugared_fun(range, open_id, spine, false)
|
||||
@ -367,7 +482,13 @@ impl<'a> DesugarState<'a> {
|
||||
Pair { fst, snd } => self.desugar_pair(expr.range, fst, snd),
|
||||
Match(matcher) => self.desugar_match(expr.range, matcher),
|
||||
Subst(sub) => self.desugar_sub(expr.range, sub),
|
||||
Open { type_name, var_name, motive, next } => self.desugar_open(expr.range, type_name, var_name, motive, &next)
|
||||
Open {
|
||||
type_name,
|
||||
var_name,
|
||||
motive,
|
||||
next,
|
||||
} => self.desugar_open(expr.range, type_name, var_name, motive, &next),
|
||||
SeqRecord(sec) => self.desugar_seq(expr.range, sec),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -23,6 +23,7 @@ pub mod attributes;
|
||||
pub mod destruct;
|
||||
pub mod expr;
|
||||
pub mod top_level;
|
||||
pub mod record_field;
|
||||
|
||||
pub struct DesugarState<'a> {
|
||||
pub errors: Sender<Box<dyn Diagnostic>>,
|
||||
@ -43,7 +44,9 @@ pub fn desugar_book(
|
||||
name_count: 0,
|
||||
failed: false,
|
||||
};
|
||||
|
||||
state.desugar_book(book);
|
||||
|
||||
if state.failed {
|
||||
Err(GenericPassError.into())
|
||||
} else {
|
||||
|
97
crates/kind-pass/src/desugar/record_field.rs
Normal file
97
crates/kind-pass/src/desugar/record_field.rs
Normal file
@ -0,0 +1,97 @@
|
||||
use fxhash::FxHashMap;
|
||||
use kind_span::Range;
|
||||
use kind_tree::{
|
||||
concrete::{self, TopLevel},
|
||||
desugared::{self, Expr},
|
||||
symbol::{Ident, QualifiedIdent},
|
||||
telescope::Telescope,
|
||||
};
|
||||
|
||||
use crate::{subst::subst_on_expr, diagnostic::PassDiagnostic};
|
||||
|
||||
use super::DesugarState;
|
||||
|
||||
impl<'a> DesugarState<'a> {
|
||||
pub fn specialize_on_field(
|
||||
&mut self,
|
||||
typ: Box<desugared::Expr>,
|
||||
) -> Option<(
|
||||
QualifiedIdent,
|
||||
&Telescope<concrete::Argument>,
|
||||
Telescope<concrete::Argument>,
|
||||
Vec<Box<Expr>>,
|
||||
)> {
|
||||
match typ.data {
|
||||
desugared::ExprKind::Ctr { name, args } => {
|
||||
let Some(TopLevel::RecordType(record)) = self.old_book.entries.get(name.to_str()) else { return None };
|
||||
let entry_constructor = self.old_book.meta.get(
|
||||
record
|
||||
.name
|
||||
.add_segment(record.constructor.to_str())
|
||||
.to_str(),
|
||||
)?;
|
||||
Some((
|
||||
name,
|
||||
&record.parameters,
|
||||
entry_constructor
|
||||
.arguments
|
||||
.clone()
|
||||
.drop(record.parameters.len()),
|
||||
args,
|
||||
))
|
||||
}
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn desugar_record_field_sequence(
|
||||
&mut self,
|
||||
range: Range,
|
||||
res: &mut Vec<(QualifiedIdent, Ident)>,
|
||||
typ: Box<desugared::Expr>,
|
||||
fields: &[Ident],
|
||||
) -> bool {
|
||||
if fields.is_empty() {
|
||||
return true;
|
||||
}
|
||||
|
||||
if let Some((name, params, record_fields, args)) = self.specialize_on_field(typ.clone()) {
|
||||
if let Some(field) = record_fields
|
||||
.iter()
|
||||
.find(|x| x.name.to_str() == fields[0].to_str())
|
||||
{
|
||||
let key = field.name.clone();
|
||||
|
||||
let pair = params
|
||||
.iter()
|
||||
.zip(args)
|
||||
.map(|(k, v)| (k.name.to_string(), v))
|
||||
.collect::<FxHashMap<_, _>>();
|
||||
|
||||
let mut val = self.desugar_expr(
|
||||
&field
|
||||
.typ
|
||||
.clone()
|
||||
.unwrap_or_else(|| concrete::expr::Expr::typ(field.range)),
|
||||
);
|
||||
|
||||
subst_on_expr(&mut val, pair);
|
||||
res.push((name, key));
|
||||
self.desugar_record_field_sequence(range, res, val, &fields[1..]);
|
||||
return true;
|
||||
} else {
|
||||
self.send_err(PassDiagnostic::CannotFindTheField(
|
||||
fields[0].range,
|
||||
fields[0].to_string()
|
||||
));
|
||||
}
|
||||
} else {
|
||||
self.send_err(PassDiagnostic::CannotAccessType(
|
||||
fields[0].range,
|
||||
fields[0].to_string()
|
||||
));
|
||||
}
|
||||
|
||||
false
|
||||
}
|
||||
}
|
@ -23,6 +23,8 @@ pub enum Sugar {
|
||||
BoolIf,
|
||||
String,
|
||||
U120,
|
||||
Getter(String),
|
||||
Mutter(String),
|
||||
Match(String),
|
||||
}
|
||||
|
||||
@ -54,6 +56,9 @@ pub enum PassDiagnostic {
|
||||
DuplicatedAttributeArgument(Range, Range),
|
||||
CannotDerive(String, Range),
|
||||
AttributeDoesNotExists(Range),
|
||||
NeedsAField(Range),
|
||||
CannotFindTheField(Range, String),
|
||||
CannotAccessType(Range, String),
|
||||
}
|
||||
|
||||
// TODO: A way to build an error message with methods
|
||||
@ -85,6 +90,9 @@ impl Diagnostic for PassDiagnostic {
|
||||
PassDiagnostic::DuplicatedAttributeArgument(range, _) => Some(range.ctx),
|
||||
PassDiagnostic::CannotDerive(_, range) => Some(range.ctx),
|
||||
PassDiagnostic::AttributeDoesNotExists(range) => Some(range.ctx),
|
||||
PassDiagnostic::NeedsAField(range) => Some(range.ctx),
|
||||
PassDiagnostic::CannotFindTheField(range, _) => Some(range.ctx),
|
||||
PassDiagnostic::CannotAccessType(range, _) => Some(range.ctx),
|
||||
}
|
||||
}
|
||||
|
||||
@ -216,7 +224,9 @@ impl Diagnostic for PassDiagnostic {
|
||||
Sugar::BoolIf => "You must implement 'Bool.if' in order to use the if notation.".to_string(),
|
||||
Sugar::String => "You must implement 'String.cons' in order to use the string notation.".to_string(),
|
||||
Sugar::U120 => "You must implement 'U120.new' in order to use the u120 notation.".to_string(),
|
||||
Sugar::Match(_) => format!("You must implement 'match' in order to use the match notation (or derive match with #derive[match])."),
|
||||
Sugar::Match(_) => "You must implement 'match' in order to use the match notation (or derive match with #derive[match]).".to_string(),
|
||||
Sugar::Mutter(typ) => format!("You must derive 'mutters' for '{}' in order to use this syntax", typ),
|
||||
Sugar::Getter(typ) => format!("You must derive 'getters' for '{}' in order to use this syntax", typ)
|
||||
}],
|
||||
positions: vec![Marker {
|
||||
position: *expr_place,
|
||||
@ -574,7 +584,7 @@ impl Diagnostic for PassDiagnostic {
|
||||
}],
|
||||
},
|
||||
PassDiagnostic::DuplicatedAttributeArgument(first, sec) => DiagnosticFrame {
|
||||
code: 209,
|
||||
code: 210,
|
||||
severity: Severity::Warning,
|
||||
title: "Duplicated attribute argument".to_string(),
|
||||
subtitles: vec![],
|
||||
@ -593,6 +603,48 @@ impl Diagnostic for PassDiagnostic {
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassDiagnostic::NeedsAField(range) => DiagnosticFrame {
|
||||
code: 211,
|
||||
severity: Severity::Error,
|
||||
title: "This expression does not access any field.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: *range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassDiagnostic::CannotFindTheField(range, _) => DiagnosticFrame {
|
||||
code: 212,
|
||||
severity: Severity::Error,
|
||||
title: "Cannot find the field".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: *range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassDiagnostic::CannotAccessType(range, _) => DiagnosticFrame {
|
||||
code: 213,
|
||||
severity: Severity::Error,
|
||||
title: "Cannot access the type fields.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["This syntax only access some types, it does not make complete type directed syntax.".to_string()],
|
||||
positions: vec![Marker {
|
||||
position: *range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
@ -623,7 +675,10 @@ impl Diagnostic for PassDiagnostic {
|
||||
| AttributeExpectsAValue(_)
|
||||
| DuplicatedAttributeArgument(_, _)
|
||||
| CannotDerive(_, _)
|
||||
| AttributeDoesNotExists(_) => Severity::Error
|
||||
| NeedsAField(_)
|
||||
| CannotFindTheField(_, _)
|
||||
| CannotAccessType(_, _)
|
||||
| AttributeDoesNotExists(_) => Severity::Error,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -11,3 +11,4 @@ mod diagnostic;
|
||||
pub mod expand;
|
||||
pub mod inline;
|
||||
pub mod unbound;
|
||||
pub mod subst;
|
61
crates/kind-pass/src/subst.rs
Normal file
61
crates/kind-pass/src/subst.rs
Normal file
@ -0,0 +1,61 @@
|
||||
use fxhash::FxHashMap;
|
||||
use kind_tree::desugared::*;
|
||||
|
||||
pub fn subst_on_expr(expr: &mut Expr, substs: FxHashMap<String, Box<Expr>>) {
|
||||
subst(Default::default(), expr, &substs)
|
||||
}
|
||||
|
||||
fn subst(bindings: im_rc::HashSet<String>, expr: &mut Expr, substs: &FxHashMap<String, Box<Expr>>) {
|
||||
use ExprKind::*;
|
||||
|
||||
match &mut expr.data {
|
||||
Var { name } => {
|
||||
if !bindings.contains(name.to_str()) {
|
||||
if let Some(res) = substs.get(name.to_str()) {
|
||||
*expr = *res.clone();
|
||||
}
|
||||
}
|
||||
},
|
||||
All { param, typ, body, .. } => {
|
||||
subst(bindings.clone(), typ, substs);
|
||||
let mut on_body = bindings.clone();
|
||||
on_body.insert(param.to_string());
|
||||
subst(on_body.clone(), body, substs);
|
||||
},
|
||||
Lambda { param, body, .. } => {
|
||||
let mut on_body = bindings.clone();
|
||||
on_body.insert(param.to_string());
|
||||
subst(on_body.clone(), body, substs);
|
||||
},
|
||||
App { fun, args } => {
|
||||
subst(bindings.clone(), fun, substs);
|
||||
for arg in args.iter_mut() {
|
||||
subst(bindings.clone(), &mut arg.data, substs);
|
||||
}
|
||||
},
|
||||
Fun { name: _, args } | Ctr { name: _, args } => {
|
||||
for arg in args.iter_mut() {
|
||||
subst(bindings.clone(), arg, substs);
|
||||
}
|
||||
},
|
||||
Let { name, val, next } => {
|
||||
subst(bindings.clone(), val, substs);
|
||||
let mut on_body = bindings.clone();
|
||||
on_body.insert(name.to_string());
|
||||
subst(on_body.clone(), next, substs);
|
||||
},
|
||||
Ann { expr, typ } => {
|
||||
subst(bindings.clone(), expr, substs);
|
||||
subst(bindings.clone(), typ, substs);
|
||||
},
|
||||
Sub { expr, .. } => {
|
||||
subst(bindings.clone(), expr, substs);
|
||||
},
|
||||
Binary { left, right, .. } => {
|
||||
subst(bindings.clone(), left, substs);
|
||||
subst(bindings, right, substs);
|
||||
},
|
||||
_ => ()
|
||||
}
|
||||
}
|
||||
|
@ -471,13 +471,10 @@ impl Visitor for UnboundCollector {
|
||||
fn visit_literal(&mut self, range: Range, lit: &mut kind_tree::concrete::Literal) {
|
||||
use kind_tree::concrete::Literal::*;
|
||||
|
||||
match lit {
|
||||
String(_) => {
|
||||
let string = &mut QualifiedIdent::new_static("String", None, range);
|
||||
self.visit_qualified_ident(&mut string.add_segment("cons").to_generated());
|
||||
self.visit_qualified_ident(&mut string.add_segment("nil").to_generated());
|
||||
}
|
||||
_ => (),
|
||||
if let String(_) = lit {
|
||||
let string = &mut QualifiedIdent::new_static("String", None, range);
|
||||
self.visit_qualified_ident(&mut string.add_segment("cons").to_generated());
|
||||
self.visit_qualified_ident(&mut string.add_segment("nil").to_generated());
|
||||
}
|
||||
}
|
||||
|
||||
@ -635,6 +632,20 @@ impl Visitor for UnboundCollector {
|
||||
}
|
||||
}
|
||||
}
|
||||
ExprKind::SeqRecord(sec) => {
|
||||
use kind_tree::concrete::SeqOperation::*;
|
||||
|
||||
self.visit_expr(&mut sec.typ);
|
||||
|
||||
self.visit_expr(&mut sec.expr);
|
||||
|
||||
match &mut sec.operation {
|
||||
Set(expr) => self.visit_expr(expr),
|
||||
Mut(expr) => self.visit_expr(expr),
|
||||
Get => (),
|
||||
}
|
||||
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
1
crates/kind-tests/suite/run/GettersSyntax.golden
Normal file
1
crates/kind-tests/suite/run/GettersSyntax.golden
Normal file
@ -0,0 +1 @@
|
||||
100
|
20
crates/kind-tests/suite/run/GettersSyntax.kind2
Normal file
20
crates/kind-tests/suite/run/GettersSyntax.kind2
Normal file
@ -0,0 +1,20 @@
|
||||
type Sum {
|
||||
a
|
||||
b
|
||||
c
|
||||
}
|
||||
|
||||
#derive[getters]
|
||||
record Identity (t: Type) {
|
||||
value: t
|
||||
}
|
||||
|
||||
#derive[getters]
|
||||
record NoTypeVar {
|
||||
some_thing: Identity (Identity U60)
|
||||
}
|
||||
|
||||
Main : U60
|
||||
Main =
|
||||
let f = NoTypeVar.new (Identity.new (Identity.new 100))
|
||||
!NoTypeVar f .some_thing .value .value
|
1
crates/kind-tests/suite/run/MuttersSyntax.golden
Normal file
1
crates/kind-tests/suite/run/MuttersSyntax.golden
Normal file
@ -0,0 +1 @@
|
||||
(NoTypeVar.new (Identity.new (Identity.new 300)))
|
20
crates/kind-tests/suite/run/MuttersSyntax.kind2
Normal file
20
crates/kind-tests/suite/run/MuttersSyntax.kind2
Normal file
@ -0,0 +1,20 @@
|
||||
type Sum {
|
||||
a
|
||||
b
|
||||
c
|
||||
}
|
||||
|
||||
#derive[mutters]
|
||||
record Identity (t: Type) {
|
||||
value: t
|
||||
}
|
||||
|
||||
#derive[mutters]
|
||||
record NoTypeVar {
|
||||
some_thing: Identity (Identity U60)
|
||||
}
|
||||
|
||||
Main : NoTypeVar
|
||||
Main =
|
||||
let f = NoTypeVar.new (Identity.new (Identity.new 100))
|
||||
!NoTypeVar f .some_thing .value .value @= x => (+ x 200)
|
1
crates/kind-tests/suite/run/SettersSyntax.golden
Normal file
1
crates/kind-tests/suite/run/SettersSyntax.golden
Normal file
@ -0,0 +1 @@
|
||||
(NoTypeVar.new (Identity.new (Identity.new 400)))
|
20
crates/kind-tests/suite/run/SettersSyntax.kind2
Normal file
20
crates/kind-tests/suite/run/SettersSyntax.kind2
Normal file
@ -0,0 +1,20 @@
|
||||
type Sum {
|
||||
a
|
||||
b
|
||||
c
|
||||
}
|
||||
|
||||
#derive[mutters]
|
||||
record Identity (t: Type) {
|
||||
value: t
|
||||
}
|
||||
|
||||
#derive[mutters]
|
||||
record NoTypeVar {
|
||||
some_thing: Identity (Identity U60)
|
||||
}
|
||||
|
||||
Main : NoTypeVar
|
||||
Main =
|
||||
let f = NoTypeVar.new (Identity.new (Identity.new 100))
|
||||
!NoTypeVar f .some_thing .value .value = 400
|
@ -12,7 +12,7 @@ use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
/// A binding express the positional or named argument of
|
||||
/// a constructor or function.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Binding {
|
||||
Positional(Box<Expr>),
|
||||
Named(Range, Ident, Box<Expr>),
|
||||
@ -22,7 +22,7 @@ pub enum Binding {
|
||||
pub type Spine = Vec<Binding>;
|
||||
|
||||
/// A binding that is used inside applications.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct AppBinding {
|
||||
pub data: Box<Expr>,
|
||||
pub erased: bool,
|
||||
@ -46,7 +46,7 @@ impl AppBinding {
|
||||
|
||||
/// A case binding is a field or a rename of some field
|
||||
/// inside a match expression.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum CaseBinding {
|
||||
Field(Ident),
|
||||
Renamed(Ident, Ident),
|
||||
@ -56,7 +56,7 @@ pub enum CaseBinding {
|
||||
/// strutinizer, bindings to the names of each arguments and
|
||||
/// a right-hand side value. The ignore_rest flag useful to just
|
||||
/// fill all of the case bindings that are not used with a default name.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Case {
|
||||
pub constructor: Ident,
|
||||
pub bindings: Vec<CaseBinding>,
|
||||
@ -66,7 +66,7 @@ pub struct Case {
|
||||
|
||||
/// A match block that will be desugared
|
||||
/// into an eliminator of a datatype.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Match {
|
||||
pub typ: QualifiedIdent,
|
||||
pub scrutinee: Ident,
|
||||
@ -77,7 +77,7 @@ pub struct Match {
|
||||
}
|
||||
|
||||
/// Substitution
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Substitution {
|
||||
pub name: Ident,
|
||||
pub redx: usize,
|
||||
@ -85,7 +85,7 @@ pub struct Substitution {
|
||||
pub expr: Box<Expr>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Literal {
|
||||
/// The universe of types (e.g. Type)
|
||||
Type,
|
||||
@ -111,13 +111,13 @@ pub enum Literal {
|
||||
|
||||
/// A destruct of a single constructor. It's a flat destruct
|
||||
/// and just translates into a eliminator for records.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Destruct {
|
||||
Destruct(Range, QualifiedIdent, Vec<CaseBinding>, Option<Range>),
|
||||
Ident(Ident),
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum SttmKind {
|
||||
Expr(Box<Expr>, Box<Sttm>),
|
||||
Ask(Destruct, Box<Expr>, Box<Sttm>),
|
||||
@ -130,13 +130,28 @@ pub enum SttmKind {
|
||||
/// describes the idea of `sequence` inside a monad
|
||||
/// each monadic action contains a `next` element that is
|
||||
/// desugared into a 'monadic bind'.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Sttm {
|
||||
pub data: SttmKind,
|
||||
pub range: Range,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum SeqOperation {
|
||||
Set(Box<Expr>),
|
||||
Mut(Box<Expr>),
|
||||
Get
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct SeqRecord {
|
||||
pub typ: Box<Expr>,
|
||||
pub expr: Box<Expr>,
|
||||
pub fields: Vec<Ident>,
|
||||
pub operation: SeqOperation
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum ExprKind {
|
||||
/// Name of a variable
|
||||
Var { name: Ident },
|
||||
@ -210,12 +225,14 @@ pub enum ExprKind {
|
||||
type_name: QualifiedIdent,
|
||||
var_name: Ident,
|
||||
motive: Option<Box<Expr>>,
|
||||
next: Box<Expr>,
|
||||
next: Box<Expr>
|
||||
},
|
||||
|
||||
SeqRecord(SeqRecord)
|
||||
}
|
||||
|
||||
/// Describes a single expression inside Kind2.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Expr {
|
||||
pub data: ExprKind,
|
||||
pub range: Range,
|
||||
@ -292,25 +309,7 @@ impl Expr {
|
||||
range,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
impl Binding {
|
||||
pub fn to_app_binding(&self) -> AppBinding {
|
||||
match self {
|
||||
Binding::Positional(expr) => {
|
||||
AppBinding {
|
||||
data: expr.clone(),
|
||||
erased: false,
|
||||
}
|
||||
},
|
||||
Binding::Named(_, _, expr) => {
|
||||
AppBinding {
|
||||
data: expr.clone(),
|
||||
erased: false,
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Locatable for Binding {
|
||||
@ -485,34 +484,16 @@ impl Display for Match {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "match {} {}", self.typ, self.scrutinee)?;
|
||||
|
||||
if let Some(res) = &self.value {
|
||||
write!(f, " = {}", res)?;
|
||||
}
|
||||
|
||||
if !self.with_vars.is_empty() {
|
||||
write!(f, " with")?;
|
||||
for var in &self.with_vars {
|
||||
if let Some(ty) = &var.1 {
|
||||
write!(f, " ({} : {})", var.0, ty)?;
|
||||
} else {
|
||||
write!(f, " {}", var.0)?;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
match &self.motive {
|
||||
None => Ok(()),
|
||||
Some(res) => write!(f, " : {}", res),
|
||||
}?;
|
||||
write!(f, " {{ ")?;
|
||||
|
||||
for case in &self.cases {
|
||||
write!(f, "{}; ", case)?
|
||||
}
|
||||
|
||||
write!(f, "}}")?;
|
||||
|
||||
if let Some(res) = &self.motive {
|
||||
write!(f, " : {}", res)?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
write!(f, "}}")
|
||||
}
|
||||
}
|
||||
|
||||
@ -592,18 +573,8 @@ impl Display for Expr {
|
||||
args.iter().map(|x| format!(" {}", x)).collect::<String>()
|
||||
),
|
||||
Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),
|
||||
Open {
|
||||
type_name,
|
||||
var_name,
|
||||
motive: Some(motive),
|
||||
next,
|
||||
} => write!(f, "(open {} {} : {motive}; {})", type_name, var_name, next),
|
||||
Open {
|
||||
type_name,
|
||||
var_name,
|
||||
motive: None,
|
||||
next,
|
||||
} => write!(f, "(open {} {}; {})", type_name, var_name, next),
|
||||
Open { type_name, var_name, motive: Some(motive), next } => write!(f, "(open {} {} : {motive}; {})", type_name, var_name, next),
|
||||
Open { type_name, var_name, motive: None, next } => write!(f, "(open {} {}; {})", type_name, var_name, next),
|
||||
If { cond, then_, else_ } => {
|
||||
write!(f, "(if {} {{{}}} else {{{}}})", cond, then_, else_)
|
||||
}
|
||||
@ -620,6 +591,34 @@ impl Display for Expr {
|
||||
Match(matcher) => write!(f, "({})", matcher),
|
||||
Subst(subst) => write!(f, "({})", subst),
|
||||
Hole => write!(f, "_"),
|
||||
SeqRecord(rec) => {
|
||||
use SeqOperation::*;
|
||||
write!(f, "(!({}) {} {}", rec.typ, rec.expr, rec.fields.iter().map(|x| format!(".{}", x.to_str())).collect::<Vec<_>>().join(","))?;
|
||||
match &rec.operation {
|
||||
Set(expr) => write!(f, "+= {})", expr),
|
||||
Mut(expr) => write!(f, "@= {})", expr),
|
||||
Get => write!(f, ")")
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Binding {
|
||||
pub fn to_app_binding(&self) -> AppBinding {
|
||||
match self {
|
||||
Binding::Positional(expr) => {
|
||||
AppBinding {
|
||||
data: expr.clone(),
|
||||
erased: false,
|
||||
}
|
||||
},
|
||||
Binding::Named(_, _, expr) => {
|
||||
AppBinding {
|
||||
data: expr.clone(),
|
||||
erased: false,
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -22,7 +22,7 @@ pub mod visitor;
|
||||
pub use expr::*;
|
||||
|
||||
/// A value of a attribute
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum AttributeStyle {
|
||||
Ident(Range, Ident),
|
||||
String(Range, String),
|
||||
@ -34,7 +34,7 @@ pub enum AttributeStyle {
|
||||
/// that usually is on the top of a declaration
|
||||
/// and can be attached to a function declaration
|
||||
/// it express some compiler properties
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Attribute {
|
||||
pub name: Ident,
|
||||
pub args: Vec<AttributeStyle>,
|
||||
@ -48,7 +48,7 @@ pub struct Attribute {
|
||||
/// compiled.
|
||||
/// hide: that express a implicit argument (that will
|
||||
/// be discovered through unification).
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Argument {
|
||||
pub hidden: bool,
|
||||
pub erased: bool,
|
||||
@ -60,7 +60,7 @@ pub struct Argument {
|
||||
/// A rule is a equation that in the left-hand-side
|
||||
/// contains a list of patterns @pats@ and on the
|
||||
/// right hand side a value.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Rule {
|
||||
pub name: QualifiedIdent,
|
||||
pub pats: Vec<Box<Pat>>,
|
||||
@ -72,7 +72,7 @@ pub struct Rule {
|
||||
/// and has rules. The type of the function
|
||||
/// consists of the arguments @args@ and the
|
||||
/// return type @typ@.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Entry {
|
||||
pub name: QualifiedIdent,
|
||||
pub docs: Vec<String>,
|
||||
@ -86,7 +86,7 @@ pub struct Entry {
|
||||
|
||||
/// A single cosntructor inside the algebraic data
|
||||
/// type definition.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Constructor {
|
||||
pub name: Ident,
|
||||
pub docs: Vec<String>,
|
||||
@ -97,7 +97,7 @@ pub struct Constructor {
|
||||
|
||||
/// An algebraic data type definition that supports
|
||||
/// parametric and indexed data type definitions.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct SumTypeDecl {
|
||||
pub name: QualifiedIdent,
|
||||
pub docs: Vec<String>,
|
||||
@ -108,7 +108,7 @@ pub struct SumTypeDecl {
|
||||
}
|
||||
|
||||
/// A single constructor data type.
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct RecordDecl {
|
||||
pub name: QualifiedIdent,
|
||||
pub docs: Vec<String>,
|
||||
@ -126,7 +126,7 @@ impl RecordDecl {
|
||||
}
|
||||
|
||||
/// All of the structures
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum TopLevel {
|
||||
SumType(SumTypeDecl),
|
||||
RecordType(RecordDecl),
|
||||
@ -166,7 +166,7 @@ impl TopLevel {
|
||||
/// A module is a collection of top level entries
|
||||
/// that contains syntatic sugars. In the future
|
||||
/// it will contain a HashMap to local renames.
|
||||
#[derive(Clone, Debug, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Module {
|
||||
pub entries: Vec<TopLevel>,
|
||||
pub uses: FxHashMap<String, String>,
|
||||
|
@ -492,5 +492,15 @@ pub fn walk_expr<T: Visitor>(ctx: &mut T, expr: &mut Expr) {
|
||||
ExprKind::Hole => {}
|
||||
ExprKind::Subst(subst) => ctx.visit_substitution(subst),
|
||||
ExprKind::Match(matcher) => ctx.visit_match(matcher),
|
||||
ExprKind::SeqRecord(seq) => {
|
||||
ctx.visit_expr(&mut seq.expr);
|
||||
ctx.visit_expr(&mut seq.typ);
|
||||
|
||||
match &mut seq.operation {
|
||||
SeqOperation::Set(expr) => ctx.visit_expr(expr),
|
||||
SeqOperation::Mut(expr) => ctx.visit_expr(expr),
|
||||
SeqOperation::Get => (),
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user