mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
commit
668233184f
@ -7,4 +7,5 @@ pub mod matching;
|
||||
pub mod open;
|
||||
pub mod subst;
|
||||
pub mod getters;
|
||||
pub mod setters;
|
||||
pub mod setters;
|
||||
pub mod mutters;
|
148
crates/kind-derive/src/mutters.rs
Normal file
148
crates/kind-derive/src/mutters.rs
Normal file
@ -0,0 +1,148 @@
|
||||
//! Module to derive mutters for record types
|
||||
|
||||
use kind_span::Range;
|
||||
|
||||
use kind_tree::concrete::expr::Expr;
|
||||
use kind_tree::concrete::pat::{Pat, PatIdent};
|
||||
use kind_tree::concrete::*;
|
||||
use kind_tree::concrete::{self};
|
||||
use kind_tree::symbol::{Ident};
|
||||
use kind_tree::telescope::Telescope;
|
||||
|
||||
pub fn derive_mutters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
|
||||
let mut types = Telescope::default();
|
||||
|
||||
for arg in rec.parameters.iter() {
|
||||
types.push(arg.to_implicit())
|
||||
}
|
||||
|
||||
// The type
|
||||
|
||||
let all_args = rec.parameters.clone();
|
||||
|
||||
let res_motive_ty = Expr::cons(
|
||||
rec.name.clone(),
|
||||
all_args
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(Expr::var(x.name)))
|
||||
.collect(),
|
||||
range
|
||||
);
|
||||
|
||||
// Sccrutinzies
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("scrutinee"),
|
||||
typ: Some(res_motive_ty.clone()),
|
||||
range,
|
||||
});
|
||||
|
||||
// Motive with indices
|
||||
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
|
||||
let fields_spine: Vec<_> = rec
|
||||
.fields
|
||||
.iter()
|
||||
.map(|(name, _, typ)| (name.clone(), typ.clone()))
|
||||
.collect();
|
||||
|
||||
let params_spine: Vec<_> = rec
|
||||
.parameters
|
||||
.iter()
|
||||
.map(|arg| {
|
||||
(
|
||||
arg.name.clone(),
|
||||
arg.typ.clone().unwrap_or_else(|| Expr::typ(arg.range.clone())),
|
||||
)
|
||||
})
|
||||
.collect();
|
||||
|
||||
let spine = [params_spine.as_slice(), fields_spine.as_slice()].concat();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
rec.name.add_segment(rec.constructor.to_str()),
|
||||
spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|(name, _)| Pat::var(name))
|
||||
.collect(),
|
||||
),
|
||||
range,
|
||||
}));
|
||||
|
||||
let mut entries = vec![];
|
||||
|
||||
let mut cons_name = rec.name.add_segment(rec.constructor.to_str());
|
||||
|
||||
cons_name.range = rec.constructor.range;
|
||||
|
||||
for (i, (arg, cons_typ)) in fields_spine.iter().enumerate() {
|
||||
let mut types = types.clone();
|
||||
|
||||
let place = rec.parameters.len() + i;
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("mut"),
|
||||
typ: Some(Expr::all(Ident::generate("_"), cons_typ.clone(), cons_typ.clone(), false, range)),
|
||||
range,
|
||||
});
|
||||
|
||||
let new_var = Ident::generate("_fn");
|
||||
|
||||
let mut pats = pats.clone();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(new_var.clone())),
|
||||
range,
|
||||
}));
|
||||
|
||||
let mut args: Vec<_> = spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(Expr::var(x.0)))
|
||||
.collect();
|
||||
|
||||
args[place] = Binding::Positional(Expr::app(Expr::var(new_var), vec![args[place].to_app_binding()], range));
|
||||
|
||||
let body = Box::new(Expr {
|
||||
data: ExprKind::Constr {
|
||||
name: cons_name.clone(),
|
||||
args,
|
||||
},
|
||||
range,
|
||||
});
|
||||
|
||||
let mut name = rec.name.add_segment(arg.to_str()).add_segment("mut");
|
||||
|
||||
name.range = rec.constructor.range;
|
||||
|
||||
let rules = vec![Box::new(Rule {
|
||||
name: name.clone(),
|
||||
pats: pats.clone(),
|
||||
body,
|
||||
range: rec.constructor.range,
|
||||
})];
|
||||
|
||||
let entry = Entry {
|
||||
name: name.clone(),
|
||||
docs: Vec::new(),
|
||||
args: types.clone(),
|
||||
typ: res_motive_ty.clone(),
|
||||
rules,
|
||||
range: rec.constructor.range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(rec.name.to_string().clone()),
|
||||
};
|
||||
|
||||
entries.push(entry)
|
||||
}
|
||||
|
||||
entries
|
||||
}
|
@ -8,6 +8,7 @@ use std::sync::mpsc::Sender;
|
||||
use fxhash::FxHashMap;
|
||||
use kind_derive::getters::derive_getters;
|
||||
use kind_derive::matching::derive_match;
|
||||
use kind_derive::mutters::derive_mutters;
|
||||
use kind_derive::open::derive_match_rec;
|
||||
use kind_derive::setters::derive_setters;
|
||||
use kind_report::data::Diagnostic;
|
||||
@ -36,6 +37,7 @@ pub enum Derive {
|
||||
Match,
|
||||
Getters,
|
||||
Setters,
|
||||
Mutters
|
||||
}
|
||||
|
||||
impl Display for Derive {
|
||||
@ -44,13 +46,17 @@ impl Display for Derive {
|
||||
Derive::Match => write!(f, "match"),
|
||||
Derive::Getters => write!(f, "getters"),
|
||||
Derive::Setters => write!(f, "setters"),
|
||||
Derive::Mutters => write!(f, "mutters"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn insert_or_report(channel: Channel, hashmap: &mut Derivations, key: Derive, range: Range) {
|
||||
if let Some(last_range) = hashmap.get(&key) {
|
||||
let err = Box::new(PassDiagnostic::DuplicatedAttributeArgument(*last_range, range));
|
||||
let err = Box::new(PassDiagnostic::DuplicatedAttributeArgument(
|
||||
*last_range,
|
||||
range,
|
||||
));
|
||||
channel.send(err).unwrap();
|
||||
} else {
|
||||
hashmap.insert(key, range);
|
||||
@ -62,6 +68,7 @@ fn string_to_derive(name: &str) -> Option<Derive> {
|
||||
"match" => Some(Derive::Match),
|
||||
"getters" => Some(Derive::Getters),
|
||||
"setters" => Some(Derive::Setters),
|
||||
"mutters" => Some(Derive::Mutters),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
@ -127,7 +134,10 @@ pub fn expand_sum_type(
|
||||
}
|
||||
other => {
|
||||
error_channel
|
||||
.send(Box::new(PassDiagnostic::CannotDerive(other.to_string(), val)))
|
||||
.send(Box::new(PassDiagnostic::CannotDerive(
|
||||
other.to_string(),
|
||||
val,
|
||||
)))
|
||||
.unwrap();
|
||||
failed = true;
|
||||
}
|
||||
@ -162,6 +172,12 @@ pub fn expand_record_type(
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
}
|
||||
Derive::Mutters => {
|
||||
for res in derive_mutters(rec.name.range, rec) {
|
||||
let info = res.extract_book_info();
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -210,8 +210,8 @@ pub enum ExprKind {
|
||||
type_name: QualifiedIdent,
|
||||
var_name: Ident,
|
||||
motive: Option<Box<Expr>>,
|
||||
next: Box<Expr>
|
||||
}
|
||||
next: Box<Expr>,
|
||||
},
|
||||
}
|
||||
|
||||
/// Describes a single expression inside Kind2.
|
||||
@ -292,7 +292,25 @@ 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 {
|
||||
@ -467,16 +485,34 @@ impl Display for Match {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "match {} {}", self.typ, self.scrutinee)?;
|
||||
|
||||
match &self.motive {
|
||||
None => Ok(()),
|
||||
Some(res) => write!(f, " : {}", res),
|
||||
}?;
|
||||
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)?;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
write!(f, " {{ ")?;
|
||||
|
||||
for case in &self.cases {
|
||||
write!(f, "{}; ", case)?
|
||||
}
|
||||
write!(f, "}}")
|
||||
|
||||
write!(f, "}}")?;
|
||||
|
||||
if let Some(res) = &self.motive {
|
||||
write!(f, " : {}", res)?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
@ -556,8 +592,18 @@ 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_)
|
||||
}
|
||||
|
@ -73,3 +73,12 @@ impl Display for Pat {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Pat {
|
||||
pub fn var(name: Ident) -> Box<Pat> {
|
||||
Box::new(Pat {
|
||||
range: name.range,
|
||||
data: PatKind::Var(PatIdent(name)),
|
||||
})
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue
Block a user