From 43eeb5ca0d9fa6debe9a073378c7b5f05faf4108 Mon Sep 17 00:00:00 2001 From: felipegchi Date: Mon, 23 Jan 2023 09:52:36 -0300 Subject: [PATCH] feat: started the mutter, getter and setter feature --- crates/kind-derive/src/subst.rs | 14 +++ crates/kind-pass/src/desugar/expr.rs | 42 ++++++-- crates/kind-pass/src/unbound/mod.rs | 14 +++ crates/kind-tree/src/concrete/expr.rs | 130 +++++++++++------------ crates/kind-tree/src/concrete/mod.rs | 20 ++-- crates/kind-tree/src/concrete/visitor.rs | 1 + 6 files changed, 136 insertions(+), 85 deletions(-) diff --git a/crates/kind-derive/src/subst.rs b/crates/kind-derive/src/subst.rs index ca19e633..10cdfb1f 100644 --- a/crates/kind-derive/src/subst.rs +++ b/crates/kind-derive/src/subst.rs @@ -288,6 +288,20 @@ impl<'a> Visitor for Subst<'a> { self.visit_expr(motive); } } + ExprKind::SeqRecord(sec) => { + use kind_tree::concrete::SeqOperation::*; + + self.visit_ident(&mut sec.ident[0]); + + self.visit_expr(&mut sec.typ_); + + match &mut sec.operation { + Set(expr) => self.visit_expr(expr), + Mut(expr) => self.visit_expr(expr), + Get => (), + } + + }, } } } diff --git a/crates/kind-pass/src/desugar/expr.rs b/crates/kind-pass/src/desugar/expr.rs index 5105d88d..b18c0bac 100644 --- a/crates/kind-pass/src/desugar/expr.rs +++ b/crates/kind-pass/src/desugar/expr.rs @@ -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,14 @@ impl<'a> DesugarState<'a> { ) } + pub(crate) fn desugar_seq( + &mut self, + range: Range, + sub: &expr::SeqRecord, + ) -> Box { + todo!() + } + pub(crate) fn desugar_sttm( &mut self, bind_ident: &QualifiedIdent, @@ -157,7 +165,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 +260,7 @@ impl<'a> DesugarState<'a> { type_name: &QualifiedIdent, var_name: &Ident, motive: &Option>, - next: &expr::Expr + next: &expr::Expr, ) -> Box { let rec = self.old_book.entries.get(type_name.to_str()); @@ -270,16 +281,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 +385,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), } } } diff --git a/crates/kind-pass/src/unbound/mod.rs b/crates/kind-pass/src/unbound/mod.rs index a41aba85..8b2a7051 100644 --- a/crates/kind-pass/src/unbound/mod.rs +++ b/crates/kind-pass/src/unbound/mod.rs @@ -635,6 +635,20 @@ impl Visitor for UnboundCollector { } } } + ExprKind::SeqRecord(sec) => { + use kind_tree::concrete::SeqOperation::*; + + self.visit_expr(&mut sec.typ_); + + self.visit_ident(&mut sec.ident[0]); + + match &mut sec.operation { + Set(expr) => self.visit_expr(expr), + Mut(expr) => self.visit_expr(expr), + Get => (), + } + + }, } } } diff --git a/crates/kind-tree/src/concrete/expr.rs b/crates/kind-tree/src/concrete/expr.rs index a5e435c2..978a40e1 100644 --- a/crates/kind-tree/src/concrete/expr.rs +++ b/crates/kind-tree/src/concrete/expr.rs @@ -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), Named(Range, Ident, Box), @@ -22,7 +22,7 @@ pub enum Binding { pub type Spine = Vec; /// A binding that is used inside applications. -#[derive(Clone, Debug, Hash, PartialEq, Eq)] +#[derive(Clone, Debug)] pub struct AppBinding { pub data: Box, 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, @@ -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, } -#[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, Option), Ident(Ident), } -#[derive(Clone, Debug, Hash, PartialEq, Eq)] +#[derive(Clone, Debug)] pub enum SttmKind { Expr(Box, Box), Ask(Destruct, Box, Box), @@ -130,13 +130,27 @@ 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), + Mut(Box), + Get +} + +#[derive(Clone, Debug)] +pub struct SeqRecord { + pub typ_: Box, + pub ident: Vec, + pub operation: SeqOperation +} + +#[derive(Clone, Debug)] pub enum ExprKind { /// Name of a variable Var { name: Ident }, @@ -210,12 +224,14 @@ pub enum ExprKind { type_name: QualifiedIdent, var_name: Ident, motive: Option>, - next: Box, + next: Box }, + + 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 +308,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 +483,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 +572,8 @@ impl Display for Expr { args.iter().map(|x| format!(" {}", x)).collect::() ), 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 +590,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.ident.iter().map(|x| x.to_str()).collect::>().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, + } + }, } } } diff --git a/crates/kind-tree/src/concrete/mod.rs b/crates/kind-tree/src/concrete/mod.rs index ee524e0e..be5ac2a0 100644 --- a/crates/kind-tree/src/concrete/mod.rs +++ b/crates/kind-tree/src/concrete/mod.rs @@ -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, @@ -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>, @@ -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, @@ -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, @@ -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, @@ -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, @@ -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, pub uses: FxHashMap, diff --git a/crates/kind-tree/src/concrete/visitor.rs b/crates/kind-tree/src/concrete/visitor.rs index 67727256..d0e9e2be 100644 --- a/crates/kind-tree/src/concrete/visitor.rs +++ b/crates/kind-tree/src/concrete/visitor.rs @@ -492,5 +492,6 @@ pub fn walk_expr(ctx: &mut T, expr: &mut Expr) { ExprKind::Hole => {} ExprKind::Subst(subst) => ctx.visit_substitution(subst), ExprKind::Match(matcher) => ctx.visit_match(matcher), + ExprKind::SeqRecord(_) => todo!(), } }