From 72bf161fecdd548f6cc55181971424ce9ab8c95a Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Fri, 29 Dec 2023 15:44:27 +0100 Subject: [PATCH] code: reduce the use of Box types in expressions --- lib/src/coq.rs | 37 +-- lib/src/expression.rs | 569 ++++++++++++++++++----------------- lib/src/thir_expression.rs | 595 +++++++++++++++++++------------------ lib/src/thir_ty.rs | 2 +- lib/src/top_level.rs | 89 +++--- lib/src/ty.rs | 20 +- 6 files changed, 675 insertions(+), 637 deletions(-) diff --git a/lib/src/coq.rs b/lib/src/coq.rs index 5a31c3154..b2c2bab2c 100644 --- a/lib/src/coq.rs +++ b/lib/src/coq.rs @@ -3,6 +3,7 @@ use crate::render::{ self, concat, curly_brackets, group, hardline, intersperse, line, nest, nil, optional_insert, optional_insert_vec, optional_insert_with, paren, text, Doc, }; +use std::rc::Rc; #[derive(Clone)] /// a list of coq top level items @@ -129,7 +130,7 @@ pub(crate) enum Expression<'a> { /// an (curried) application of a function to some arguments Application { /// the function that is applied - func: Box>, + func: Rc>, /// a nonempty list of arguments /// (we accept many arguments to control their indentation better, /// the application is curried when it gets printed) @@ -138,10 +139,10 @@ pub(crate) enum Expression<'a> { /// a (curried) function Function { parameters: Vec>, - body: Box>, + body: Rc>, }, Match { - scrutinee: Box>, + scrutinee: Rc>, arms: Vec<(Expression<'a>, Expression<'a>)>, }, /// a (curried) function type @@ -151,7 +152,7 @@ pub(crate) enum Expression<'a> { /// the type is curried when it gets printed) domains: Vec>, /// the image (range, co-domain) of functions of the type - image: Box>, + image: Rc>, }, /// a dependent product of types /// (like `forall (x : A), B(x)`) @@ -159,35 +160,35 @@ pub(crate) enum Expression<'a> { /// a list of arguments of `forall` args: Vec>, /// the expression for the resulting type - image: Box>, + image: Rc>, }, /// a product of two variables (they can be types or numbers) Product { /// left hand side - lhs: Box>, + lhs: Rc>, /// right hand side - rhs: Box>, + rhs: Rc>, }, Record { fields: Vec>, }, RecordField { - record: Box>, + record: Rc>, field: String, }, RecordUpdate { - record: Box>, + record: Rc>, field: String, - update: Box>, + update: Rc>, }, NotationsDot { - value: Box>, + value: Rc>, field: String, }, /// For example ltac:(...) or constr:(...) ModeWrapper { mode: String, - expr: Box>, + expr: Rc>, }, /// Set constant (the type of our types) Set, @@ -197,7 +198,7 @@ pub(crate) enum Expression<'a> { /// a list of arguments of `Sigma` args: Vec>, /// the expression for the resulting type - image: Box>, + image: Rc>, }, /// a string String(String), @@ -963,7 +964,7 @@ impl<'a> Expression<'a> { /// apply the expression as a function to one argument pub(crate) fn apply_arg(&self, name: &Option, arg: &Self) -> Self { Expression::Application { - func: Box::new(self.clone()), + func: Rc::new(self.clone()), args: vec![(name.clone(), arg.clone())], } } @@ -980,7 +981,7 @@ impl<'a> Expression<'a> { } Expression::Application { - func: Box::new(self.to_owned()), + func: Rc::new(self.to_owned()), args: args.to_vec(), } } @@ -998,14 +999,14 @@ impl<'a> Expression<'a> { pub(crate) fn arrows_from(&self, domains: &[Self]) -> Self { Expression::FunctionType { domains: domains.to_owned(), - image: Box::new(self.to_owned()), + image: Rc::new(self.to_owned()), } } pub(crate) fn multiply(lhs: Self, rhs: Self) -> Self { Expression::Product { - lhs: Box::new(lhs), - rhs: Box::new(rhs), + lhs: Rc::new(lhs), + rhs: Rc::new(rhs), } } diff --git a/lib/src/expression.rs b/lib/src/expression.rs index b1eda9bbb..5ee130692 100644 --- a/lib/src/expression.rs +++ b/lib/src/expression.rs @@ -1,11 +1,10 @@ -use core::panic; -use std::rc::Rc; - use crate::env::*; use crate::path::*; use crate::pattern::*; use crate::render::*; use crate::ty::*; +use core::panic; +use std::rc::Rc; /// Struct [FreshVars] represents a set of fresh variables #[derive(Debug)] @@ -26,7 +25,7 @@ impl FreshVars { #[derive(Clone, Debug, Eq, Hash, PartialEq)] pub(crate) struct MatchArm { pub(crate) pattern: Rc, - pub(crate) body: Box, + pub(crate) body: Rc, } /// [LoopControlFlow] represents the expressions responsible for @@ -54,14 +53,14 @@ pub(crate) enum Literal { #[derive(Clone, Debug, Eq, Hash, PartialEq)] pub(crate) struct Expr { - pub(crate) kind: ExprKind, + pub(crate) kind: Rc, pub(crate) ty: Option>, } /// Enum [ExprKind] represents the AST of rust terms. #[derive(Clone, Debug, Eq, Hash, PartialEq)] pub(crate) enum ExprKind { - Pure(Box), + Pure(Rc), LocalVar(String), Var(Path), Constructor(Path), @@ -81,8 +80,8 @@ pub(crate) enum ExprKind { Literal(Literal), NonHirLiteral(rustc_middle::ty::ScalarInt), Call { - func: Box, - args: Vec, + func: Rc, + args: Vec>, purity: Purity, from_user: bool, }, @@ -90,101 +89,101 @@ pub(crate) enum ExprKind { /// form once the monadic translation is done. MonadicOperator { name: String, - arg: Box, + arg: Rc, }, Lambda { args: Vec<(String, Option>)>, - body: Box, + body: Rc, is_for_match: bool, }, Array { - elements: Vec, + elements: Vec>, }, Tuple { - elements: Vec, + elements: Vec>, }, Let { is_monadic: bool, name: Option, - init: Box, - body: Box, + init: Rc, + body: Rc, }, LetIf { pat: Rc, - init: Box, + init: Rc, }, If { - condition: Box, - success: Box, - failure: Box, + condition: Rc, + success: Rc, + failure: Rc, }, Loop { - body: Box, + body: Rc, }, Match { - scrutinee: Box, + scrutinee: Rc, arms: Vec, }, #[allow(dead_code)] IndexedField { - base: Box, + base: Rc, index: u32, }, NamedField { - base: Box, + base: Rc, name: String, }, Index { - base: Box, - index: Box, + base: Rc, + index: Rc, }, ControlFlow(LoopControlFlow), StructStruct { path: Path, - fields: Vec<(String, Expr)>, - base: Option>, + fields: Vec<(String, Rc)>, + base: Option>, struct_or_variant: StructOrVariant, }, StructTuple { path: Path, - fields: Vec, + fields: Vec>, struct_or_variant: StructOrVariant, }, StructUnit { path: Path, struct_or_variant: StructOrVariant, }, - Use(Box), - Return(Box), + Use(Rc), + Return(Rc), /// Useful for error messages or annotations Message(String), } impl ExprKind { - pub(crate) fn tt() -> Self { - ExprKind::LocalVar("tt".to_string()).alloc(Some(CoqType::unit())) + pub(crate) fn tt() -> Rc { + Rc::new(ExprKind::LocalVar("tt".to_string())).alloc(Some(CoqType::unit())) } } impl Expr { /// The Coq value [tt] (the inhabitant of the [unit] type) is used as default /// value - pub(crate) fn tt() -> Self { - Expr { + pub(crate) fn tt() -> Rc { + Rc::new(Expr { kind: ExprKind::tt(), ty: Some(CoqType::unit().val()), - } + }) } - pub(crate) fn local_var(name: &str) -> Box { - Box::new(Expr { - kind: ExprKind::LocalVar(name.to_string()), + pub(crate) fn local_var(name: &str) -> Rc { + Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(name.to_string())), ty: None, }) } pub(crate) fn has_return(&self) -> bool { - match &self.kind { + match self.kind.as_ref() { ExprKind::Pure(expr) => expr.has_return(), ExprKind::LocalVar(_) => false, ExprKind::Var(_) => false, @@ -206,15 +205,15 @@ impl Expr { args, purity: _, from_user: _, - } => func.has_return() || args.iter().any(Self::has_return), + } => func.has_return() || args.iter().any(|arg| arg.has_return()), ExprKind::MonadicOperator { name: _, arg } => arg.has_return(), ExprKind::Lambda { args: _, body, is_for_match, } => *is_for_match && body.has_return(), - ExprKind::Array { elements } => elements.iter().any(Self::has_return), - ExprKind::Tuple { elements } => elements.iter().any(Self::has_return), + ExprKind::Array { elements } => elements.iter().any(|element| element.has_return()), + ExprKind::Tuple { elements } => elements.iter().any(|element| element.has_return()), ExprKind::Let { is_monadic: _, name: _, @@ -251,7 +250,7 @@ impl Expr { path: _, fields, struct_or_variant: _, - } => fields.iter().any(Self::has_return), + } => fields.iter().any(|field| field.has_return()), ExprKind::StructUnit { path: _, struct_or_variant: _, @@ -263,39 +262,39 @@ impl Expr { } } -fn pure(e: Expr) -> Expr { - Expr { +fn pure(e: Rc) -> Rc { + Rc::new(Expr { ty: e.ty.clone(), - kind: ExprKind::Pure(Box::new(e)), - } + kind: Rc::new(ExprKind::Pure(e)), + }) } /// creates a monadic let statement with [e1] as the initializer /// and the result of [f] as the body fn monadic_let_in_stmt( fresh_vars: FreshVars, - e1: Expr, - f: impl FnOnce(FreshVars, Expr) -> (Expr, FreshVars), -) -> (Expr, FreshVars) { - match e1.kind { - ExprKind::Pure(e) => f(fresh_vars, *e), + e1: Rc, + f: impl FnOnce(FreshVars, Rc) -> (Rc, FreshVars), +) -> (Rc, FreshVars) { + match e1.kind.as_ref() { + ExprKind::Pure(e) => f(fresh_vars, e.clone()), ExprKind::Let { is_monadic, name, init, body, } => { - let (body, fresh_vars) = monadic_let_in_stmt(fresh_vars, *body, f); + let (body, fresh_vars) = monadic_let_in_stmt(fresh_vars, body.clone(), f); ( - Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { - is_monadic, - name, - init, - body: Box::new(body), - }, - }, + kind: Rc::new(ExprKind::Let { + is_monadic: *is_monadic, + name: name.clone(), + init: init.clone(), + body, + }), + }), fresh_vars, ) } @@ -303,21 +302,21 @@ fn monadic_let_in_stmt( let (var_name, fresh_vars) = fresh_vars.next(); let (body, fresh_vars) = f( fresh_vars, - Expr { - kind: ExprKind::LocalVar(var_name.clone()), + Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(var_name.clone())), ty: None, - }, + }), ); ( - Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: true, name: Some(var_name), - init: Box::new(e1), - body: Box::new(body), - }, - }, + init: e1, + body, + }), + }), fresh_vars, ) } @@ -326,31 +325,27 @@ fn monadic_let_in_stmt( fn monadic_let( fresh_vars: FreshVars, - e1: Expr, - f: impl FnOnce(FreshVars, Expr) -> (Expr, FreshVars), -) -> (Expr, FreshVars) { + e1: Rc, + f: impl FnOnce(FreshVars, Rc) -> (Rc, FreshVars), +) -> (Rc, FreshVars) { let (e1, fresh_vars) = mt_expression(fresh_vars, e1); monadic_let_in_stmt(fresh_vars, e1, f) } fn monadic_optional_let( fresh_vars: FreshVars, - e1: Option>, - f: impl FnOnce(FreshVars, Option>) -> (Expr, FreshVars), -) -> (Expr, FreshVars) { + e1: Option>, + f: impl FnOnce(FreshVars, Option>) -> (Rc, FreshVars), +) -> (Rc, FreshVars) { match e1 { None => f(fresh_vars, None), - Some(e1) => monadic_let(fresh_vars, *e1, |fresh_vars, e1| { - f(fresh_vars, Some(Box::new(e1))) - }), + Some(e1) => monadic_let(fresh_vars, e1, |fresh_vars, e1| f(fresh_vars, Some(e1))), } } -fn monadic_lets( - fresh_vars: FreshVars, - es: Vec, - f: Box) -> (Expr, FreshVars)>, -) -> (Expr, FreshVars) { +type DynLetFn = Box>) -> (Rc, FreshVars)>; + +fn monadic_lets(fresh_vars: FreshVars, es: Vec>, f: DynLetFn) -> (Rc, FreshVars) { match &es[..] { [] => f(fresh_vars, vec![]), [e1, es @ ..] => monadic_let(fresh_vars, e1.clone(), |fresh_vars, e1| { @@ -371,82 +366,89 @@ fn monadic_lets( /// may lead to infinite loops because of the mutual recursion between /// the functions. In practice this means translating every subexpression /// before translating the expression itself. -pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVars) { +pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Rc) -> (Rc, FreshVars) { let ty = expr.ty.clone().map(mt_ty); - match expr.kind { + + match expr.kind.as_ref() { ExprKind::Pure(_) => panic!("Expressions should not be monadic yet."), - ExprKind::LocalVar(_) => (pure(expr), fresh_vars), - ExprKind::Var(_) => (pure(expr), fresh_vars), - ExprKind::Constructor(_) => (pure(expr), fresh_vars), + ExprKind::LocalVar(_) => (pure(expr.clone()), fresh_vars), + ExprKind::Var(_) => (pure(expr.clone()), fresh_vars), + ExprKind::Constructor(_) => (pure(expr.clone()), fresh_vars), ExprKind::VarWithTy { path, ty_name, ty: var_ty, } => ( - pure(Expr { - kind: ExprKind::VarWithTy { - path, - ty_name, - ty: mt_ty(var_ty), - }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::VarWithTy { + path: path.clone(), + ty_name: ty_name.clone(), + ty: mt_ty(var_ty.clone()), + }), ty, - }), + })), fresh_vars, ), ExprKind::VarWithSelfTy { path, self_ty } => ( - pure(Expr { - kind: ExprKind::VarWithSelfTy { - path, - self_ty: mt_ty(self_ty), - }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::VarWithSelfTy { + path: path.clone(), + self_ty: mt_ty(self_ty.clone()), + }), ty, - }), + })), fresh_vars, ), - ExprKind::AssociatedFunction { .. } => (pure(expr), fresh_vars), - ExprKind::Literal { .. } => (pure(expr), fresh_vars), - ExprKind::NonHirLiteral { .. } => (pure(expr), fresh_vars), + ExprKind::AssociatedFunction { .. } => (pure(expr.clone()), fresh_vars), + ExprKind::Literal { .. } => (pure(expr.clone()), fresh_vars), + ExprKind::NonHirLiteral { .. } => (pure(expr.clone()), fresh_vars), ExprKind::Call { func, args, purity, from_user, - } => monadic_let(fresh_vars, *func, |fresh_vars, func| { - monadic_lets( - fresh_vars, - args, - Box::new(move |fresh_vars, args| { - ( - { - let expr = Expr { - kind: ExprKind::Call { - func: Box::new(func), - args, - purity, - from_user, - }, - ty, - }; - match purity { - Purity::Pure => pure(expr), - Purity::Effectful => expr, - } - }, - fresh_vars, - ) - }), - ) - }), + } => { + let purity = *purity; + let from_user = *from_user; + + monadic_let(fresh_vars, func.clone(), |fresh_vars, func| { + monadic_lets( + fresh_vars, + args.clone(), + Box::new(move |fresh_vars, args| { + ( + { + let call = Rc::new(Expr { + kind: Rc::new(ExprKind::Call { + func: func.clone(), + args, + purity, + from_user, + }), + ty, + }); + + match purity { + Purity::Pure => pure(call), + Purity::Effectful => call, + } + }, + fresh_vars, + ) + }), + ) + }) + } ExprKind::MonadicOperator { name, arg } => { - let (arg, fresh_vars) = mt_expression(fresh_vars, *arg); + let (arg, fresh_vars) = mt_expression(fresh_vars, arg.clone()); ( - Expr { - kind: ExprKind::MonadicOperator { - name, - arg: Box::new(arg), - }, + Rc::new(Expr { + kind: Rc::new(ExprKind::MonadicOperator { + name: name.clone(), + arg, + }), ty, - }, + }), fresh_vars, ) } @@ -455,41 +457,41 @@ pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVa body, is_for_match, } => { - let (body, _) = mt_expression(FreshVars::new(), *body); + let (body, _) = mt_expression(FreshVars::new(), body.clone()); ( - pure(Expr { - kind: ExprKind::Lambda { - args, - body: Box::new(body), - is_for_match, - }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::Lambda { + args: args.clone(), + body, + is_for_match: *is_for_match, + }), ty, - }), + })), fresh_vars, ) } ExprKind::Array { elements } => monadic_lets( fresh_vars, - elements, + elements.clone(), Box::new(|fresh_vars, elements| { ( - pure(Expr { - kind: ExprKind::Array { elements }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::Array { elements }), ty, - }), + })), fresh_vars, ) }), ), ExprKind::Tuple { elements } => monadic_lets( fresh_vars, - elements, + elements.clone(), Box::new(|fresh_vars, elements| { ( - pure(Expr { - kind: ExprKind::Tuple { elements }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::Tuple { elements }), ty, - }), + })), fresh_vars, ) }), @@ -500,150 +502,151 @@ pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVa init, body, } => { - if is_monadic { + if *is_monadic { panic!("The let statement should not be monadic yet.") } - let (init, _fresh_vars) = mt_expression(FreshVars::new(), *init); - let (body, _fresh_vars) = mt_expression(FreshVars::new(), *body); - let body = Box::new(body); - let pure_init: Option> = get_pure_from_stmt(init.clone()); + let (init, _fresh_vars) = mt_expression(FreshVars::new(), init.clone()); + let (body, _fresh_vars) = mt_expression(FreshVars::new(), body.clone()); + let pure_init: Option> = get_pure_from_stmt(init.clone()); ( match pure_init { - Some(pure_init) => Expr { - kind: ExprKind::Let { + Some(pure_init) => Rc::new(Expr { + kind: Rc::new(ExprKind::Let { is_monadic: false, - name, + name: name.clone(), init: pure_init, body, - }, + }), ty, - }, - None => Expr { - kind: ExprKind::Let { + }), + None => Rc::new(Expr { + kind: Rc::new(ExprKind::Let { is_monadic: true, - name, - init: Box::new(init), + name: name.clone(), + init, body, - }, + }), ty, - }, + }), }, fresh_vars, ) } - ExprKind::LetIf { pat, init } => monadic_let(fresh_vars, *init, |fresh_vars, init| { - ( - Expr { - kind: ExprKind::LetIf { - pat, - init: Box::new(init), - }, - ty: ty.clone(), - }, - fresh_vars, - ) - }), + ExprKind::LetIf { pat, init } => { + monadic_let(fresh_vars, init.clone(), |fresh_vars, init| { + ( + Rc::new(Expr { + kind: Rc::new(ExprKind::LetIf { + pat: pat.clone(), + init, + }), + ty: ty.clone(), + }), + fresh_vars, + ) + }) + } ExprKind::If { condition, success, failure, - } => monadic_let(fresh_vars, *condition, |fresh_vars, condition| { - let (success, _fresh_vars) = mt_expression(FreshVars::new(), *success); - let (failure, _fresh_vars) = mt_expression(FreshVars::new(), *failure); + } => monadic_let(fresh_vars, condition.clone(), |fresh_vars, condition| { + let (success, _fresh_vars) = mt_expression(FreshVars::new(), success.clone()); + let (failure, _fresh_vars) = mt_expression(FreshVars::new(), failure.clone()); ( - Expr { - kind: ExprKind::If { - condition: Box::new(condition), - success: Box::new(success), - failure: Box::new(failure), - }, + Rc::new(Expr { + kind: Rc::new(ExprKind::If { + condition, + success, + failure, + }), ty: ty.clone(), - }, + }), fresh_vars, ) }), ExprKind::Loop { body, .. } => { - let (body, fresh_vars) = mt_expression(fresh_vars, *body); + let (body, fresh_vars) = mt_expression(fresh_vars, body.clone()); ( - Expr { - kind: ExprKind::Loop { - body: Box::new(body), - }, + Rc::new(Expr { + kind: Rc::new(ExprKind::Loop { body }), ty, - }, + }), fresh_vars, ) } ExprKind::Match { scrutinee, arms } => { - monadic_let(fresh_vars, *scrutinee, |fresh_vars, scrutinee| { + monadic_let(fresh_vars, scrutinee.clone(), |fresh_vars, scrutinee| { ( - Expr { - kind: ExprKind::Match { - scrutinee: Box::new(scrutinee), + Rc::new(Expr { + kind: Rc::new(ExprKind::Match { + scrutinee, arms: arms .iter() .map(|MatchArm { pattern, body }| { let (body, _fresh_vars) = - mt_expression(FreshVars::new(), *body.clone()); + mt_expression(FreshVars::new(), body.clone()); MatchArm { pattern: pattern.clone(), - body: Box::new(body), + body, } }) .collect(), - }, + }), ty: ty.clone(), - }, + }), fresh_vars, ) }) } ExprKind::IndexedField { base, index } => { - monadic_let(fresh_vars, *base, |fresh_vars, base| { + monadic_let(fresh_vars, base.clone(), |fresh_vars, base| { ( - pure(Expr { - kind: ExprKind::IndexedField { - base: Box::new(base), - index, - }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::IndexedField { + base, + index: *index, + }), ty, - }), + })), fresh_vars, ) }) } ExprKind::NamedField { base, name } => { - monadic_let(fresh_vars, *base, |fresh_vars, base| { + monadic_let(fresh_vars, base.clone(), |fresh_vars, base| { ( - pure(Expr { - kind: ExprKind::NamedField { - base: Box::new(base), - name, - }, + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::NamedField { + base, + name: name.clone(), + }), ty: ty.clone(), - }), + })), + fresh_vars, + ) + }) + } + ExprKind::Index { base, index } => { + monadic_let(fresh_vars, base.clone(), |fresh_vars, base| { + ( + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::Index { + base, + index: index.clone(), + }), + ty, + })), fresh_vars, ) }) } - ExprKind::Index { base, index } => monadic_let(fresh_vars, *base, |fresh_vars, base| { - ( - pure(Expr { - kind: ExprKind::Index { - base: Box::new(base), - index, - }, - ty, - }), - fresh_vars, - ) - }), // control flow expressions are responsible for side effects, so they are monadic already ExprKind::ControlFlow(lcf_expression) => ( - Expr { - kind: ExprKind::ControlFlow(lcf_expression), + Rc::new(Expr { + kind: Rc::new(ExprKind::ControlFlow(*lcf_expression)), ty, - }, + }), fresh_vars, ), ExprKind::StructStruct { @@ -652,7 +655,13 @@ pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVa base, struct_or_variant, } => { - let fields_values: Vec = fields.iter().map(|(_, field)| field.clone()).collect(); + let path = path.clone(); + let fields = fields.clone(); + let base = base.clone(); + let struct_or_variant = *struct_or_variant; + let fields_values: Vec> = + fields.iter().map(|(_, field)| field.clone()).collect(); + monadic_lets( fresh_vars, fields_values, @@ -661,8 +670,8 @@ pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVa let fields_names: Vec = fields.iter().map(|(name, _)| name.clone()).collect(); ( - pure(Expr { - kind: ExprKind::StructStruct { + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::StructStruct { path, fields: fields_names .iter() @@ -671,9 +680,9 @@ pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVa .collect(), base, struct_or_variant, - }, + }), ty, - }), + })), fresh_vars, ) }) @@ -684,50 +693,55 @@ pub(crate) fn mt_expression(fresh_vars: FreshVars, expr: Expr) -> (Expr, FreshVa path, fields, struct_or_variant, - } => monadic_lets( - fresh_vars, - fields, - Box::new(move |fresh_vars, fields| { - ( - pure(Expr { - kind: ExprKind::StructTuple { - path, - fields, - struct_or_variant, - }, - ty, - }), - fresh_vars, - ) - }), - ), - ExprKind::StructUnit { .. } => (pure(expr), fresh_vars), - ExprKind::Use(expr) => monadic_let(fresh_vars, *expr, |fresh_vars, expr| { + } => { + let path = path.clone(); + let struct_or_variant = *struct_or_variant; + + monadic_lets( + fresh_vars, + fields.clone(), + Box::new(move |fresh_vars, fields| { + ( + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::StructTuple { + path, + fields, + struct_or_variant, + }), + ty, + })), + fresh_vars, + ) + }), + ) + } + ExprKind::StructUnit { .. } => (pure(expr.clone()), fresh_vars), + ExprKind::Use(expr) => monadic_let(fresh_vars, expr.clone(), |fresh_vars, expr| { ( - pure(Expr { - kind: ExprKind::Use(Box::new(expr)), + pure(Rc::new(Expr { + kind: Rc::new(ExprKind::Use(expr)), ty, - }), + })), fresh_vars, ) }), - ExprKind::Return(expr) => monadic_let(fresh_vars, *expr, |fresh_vars, expr| { + ExprKind::Return(expr) => monadic_let(fresh_vars, expr.clone(), |fresh_vars, expr| { ( - Expr { - kind: ExprKind::Return(Box::new(expr)), + Rc::new(Expr { + kind: Rc::new(ExprKind::Return(expr)), ty, - }, + }), fresh_vars, ) }), - ExprKind::Message(_) => (pure(expr), fresh_vars), + ExprKind::Message(_) => (pure(expr.clone()), fresh_vars), } } /// Get the pure part of a statement, if possible, as a statement. -fn get_pure_from_stmt(statement: Expr) -> Option> { - match statement.kind { - ExprKind::Pure(e) => Some(e), +fn get_pure_from_stmt(statement: Rc) -> Option> { + match statement.kind.as_ref() { + ExprKind::Pure(e) => Some(e.clone()), ExprKind::Let { is_monadic: true, .. } => None, @@ -736,28 +750,29 @@ fn get_pure_from_stmt(statement: Expr) -> Option> { name, init, body, - } => get_pure_from_stmt(*body).map(|body| { - Box::new(Expr { - kind: ExprKind::Let { + } => get_pure_from_stmt(body.clone()).map(|body| { + Rc::new(Expr { + kind: Rc::new(ExprKind::Let { is_monadic: false, - name, - init, + name: name.clone(), + init: init.clone(), body, - }, - ty: statement.ty, + }), + ty: statement.ty.clone(), }) }), _ => None, } } -pub(crate) fn compile_hir_id(env: &mut Env, hir_id: rustc_hir::hir_id::HirId) -> Expr { +pub(crate) fn compile_hir_id(env: &mut Env, hir_id: rustc_hir::hir_id::HirId) -> Rc { let local_def_id = hir_id.owner.def_id; let thir = env.tcx.thir_body(local_def_id); let Ok((thir, expr_id)) = thir else { panic!("thir failed to compile"); }; let thir = thir.borrow(); + crate::thir_expression::compile_expr(env, &thir, &expr_id) } diff --git a/lib/src/thir_expression.rs b/lib/src/thir_expression.rs index 88ddd8343..929b8af0e 100644 --- a/lib/src/thir_expression.rs +++ b/lib/src/thir_expression.rs @@ -12,16 +12,16 @@ use rustc_middle::ty::TyKind; use std::rc::Rc; impl ExprKind { - pub(crate) fn alloc(self, ty: Option>) -> Self { - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar("M.alloc".to_string()), + pub(crate) fn alloc(self: Rc, ty: Option>) -> Rc { + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("M.alloc".to_string())), ty: None, }), - args: vec![Expr { kind: self, ty }], + args: vec![Rc::new(Expr { kind: self, ty })], purity: Purity::Effectful, from_user: false, - } + }) } } @@ -59,23 +59,23 @@ pub(crate) fn compile_expr<'a>( env: &mut Env<'a>, thir: &rustc_middle::thir::Thir<'a>, expr_id: &rustc_middle::thir::ExprId, -) -> Expr { +) -> Rc { let expr = thir.exprs.get(*expr_id).unwrap(); let kind = compile_expr_kind(env, thir, expr_id); let ty = compile_type(env, &expr.ty).val(); - Expr { kind, ty: Some(ty) } + Rc::new(Expr { kind, ty: Some(ty) }) } impl Expr { - fn match_simple_call(&self, name_in: &[&str]) -> Option { + fn match_simple_call(self: Rc, name_in: &[&str]) -> Option> { if let ExprKind::Call { func, args, purity: _, from_user: _, - } = &self.kind + } = self.kind.as_ref() { - if let ExprKind::LocalVar(func) = &func.kind { + if let ExprKind::LocalVar(func) = func.kind.as_ref() { if name_in.contains(&func.as_str()) && args.len() == 1 { return Some(args.get(0).unwrap().clone()); } @@ -86,21 +86,21 @@ impl Expr { } /// Return the borrowed expression if the expression is a borrow. - fn match_borrow(&self) -> Option { + fn match_borrow(self: Rc) -> Option> { self.match_simple_call(&["borrow", "borrow_mut"]) } - fn match_deref(&self) -> Option { + fn match_deref(self: Rc) -> Option> { self.match_simple_call(&["deref"]) } - pub(crate) fn read(self) -> Self { + pub(crate) fn read(self: Rc) -> Rc { // If we read an allocated expression, we just return the expression. - if let Some(expr) = self.match_simple_call(&["M.alloc"]) { + if let Some(expr) = self.clone().match_simple_call(&["M.alloc"]) { return expr; } - Expr { + Rc::new(Expr { ty: match self.ty.clone() { None => None, Some(ty) => { @@ -122,35 +122,35 @@ impl Expr { } } }, - kind: ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar("M.read".to_string()), + kind: Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("M.read".to_string())), ty: None, }), args: vec![self], purity: Purity::Effectful, from_user: false, - }, - } + }), + }) } - fn copy(self) -> Self { - if self.match_simple_call(&["M.alloc"]).is_some() { + fn copy(self: Rc) -> Rc { + if self.clone().match_simple_call(&["M.alloc"]).is_some() { return self; } - Expr { + Rc::new(Expr { ty: self.ty.clone(), - kind: ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar("M.copy".to_string()), + kind: Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("M.copy".to_string())), ty: None, }), args: vec![self], purity: Purity::Effectful, from_user: false, - }, - } + }), + }) } } @@ -161,63 +161,63 @@ pub(crate) fn is_mutable_borrow_kind(borrow_kind: &BorrowKind) -> bool { } } -fn compile_borrow(borrow_kind: &BorrowKind, arg: Expr) -> ExprKind { +fn compile_borrow(borrow_kind: &BorrowKind, arg: Rc) -> Rc { let func = if is_mutable_borrow_kind(borrow_kind) { "borrow_mut".to_string() } else { "borrow".to_string() }; - if let Some(derefed) = arg.match_deref() { - if let Some(ty) = derefed.ty { + if let Some(derefed) = arg.clone().match_deref() { + if let Some(ty) = derefed.ty.clone() { if let Some((ref_name, _, _)) = ty.match_ref() { if (func == "borrow" && ref_name == "ref") || (func == "borrow_mut" && ref_name == "mut_ref") { - return derefed.kind; + return derefed.kind.clone(); } } } } - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar(func), + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(func)), ty: None, }), args: vec![arg], purity: Purity::Pure, from_user: false, - } + }) } -pub(crate) fn allocate_bindings(bindings: &[String], body: Box) -> Box { +pub(crate) fn allocate_bindings(bindings: &[String], body: Rc) -> Rc { bindings.iter().rfold(body, |body, binding| { - Box::new(Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(binding.clone()), - init: Box::new(Expr { - kind: ExprKind::LocalVar(binding.clone()).alloc(None), + init: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(binding.clone())).alloc(None), ty: None, }), body, - }, + }), }) }) } -fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> Box { +fn build_inner_match(patterns: Vec<(String, Rc)>, body: Rc) -> Rc { let default_match_arm = MatchArm { pattern: Rc::new(Pattern::Wild), - body: Box::new(Expr { - kind: ExprKind::Call { + body: Rc::new(Expr { + kind: Rc::new(ExprKind::Call { func: Expr::local_var("M.break_match"), args: vec![], purity: Purity::Effectful, from_user: false, - }, + }), ty: None, }), }; @@ -230,24 +230,24 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B name, is_with_ref, pattern, - } => Box::new(Expr { + } => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(name.clone()), init: match is_with_ref { - None => Box::new(Expr::local_var(&scrutinee).copy()), + None => Expr::local_var(&scrutinee).copy(), Some(is_with_ref) => { let func = if *is_with_ref { "borrow" } else { "borrow_mut" }; - Box::new(Expr { + Rc::new(Expr { ty: None, - kind: ExprKind::Call { + kind: Rc::new(ExprKind::Call { func: Expr::local_var(func), - args: vec![*Expr::local_var(&scrutinee)], + args: vec![Expr::local_var(&scrutinee)], purity: Purity::Pure, from_user: false, - } + }) .alloc(None), }) } @@ -258,12 +258,12 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B build_inner_match(vec![(scrutinee, pattern.clone())], body) } }, - }, + }), }), - Pattern::StructStruct(path, fields, struct_or_variant) => Box::new(Expr { + Pattern::StructStruct(path, fields, struct_or_variant) => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Match { - scrutinee: Box::new(Expr::local_var(&scrutinee).read()), + kind: Rc::new(ExprKind::Match { + scrutinee: Expr::local_var(&scrutinee).read(), arms: [ vec![MatchArm { pattern: Rc::new(Pattern::StructStruct( @@ -291,23 +291,23 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B fields.iter().enumerate().rfold( body, |body, (index, (field_name, _))| { - Box::new(Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(format!("γ{index}")), - init: Box::new(Expr { + init: Rc::new(Expr { ty: None, - kind: ExprKind::NamedField { + kind: Rc::new(ExprKind::NamedField { base: Expr::local_var(&scrutinee), name: format!( "{}.{field_name}", path.segments.last().unwrap(), ), - }, + }), }), body, - }, + }), }) }, ) @@ -319,12 +319,12 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B }, ] .concat(), - }, + }), }), - Pattern::StructTuple(path, patterns, struct_or_variant) => Box::new(Expr { + Pattern::StructTuple(path, patterns, struct_or_variant) => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Match { - scrutinee: Box::new(Expr::local_var(&scrutinee).read()), + kind: Rc::new(ExprKind::Match { + scrutinee: Expr::local_var(&scrutinee).read(), arms: [ vec![MatchArm { pattern: Rc::new(Pattern::StructTuple( @@ -345,23 +345,23 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B ); patterns.iter().enumerate().rfold(body, |body, (index, _)| { - Box::new(Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(format!("γ{index}")), - init: Box::new(Expr { + init: Rc::new(Expr { ty: None, - kind: ExprKind::NamedField { + kind: Rc::new(ExprKind::NamedField { base: Expr::local_var(&scrutinee), name: format!( "{}.{index}", path.segments.last().unwrap(), ), - }, + }), }), body, - }, + }), }) }) }, @@ -372,30 +372,30 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B }, ] .concat(), - }, + }), }), - Pattern::Deref(pattern) => Box::new(Expr { + Pattern::Deref(pattern) => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(scrutinee.clone()), - init: Box::new(Expr { + init: Rc::new(Expr { ty: None, - kind: ExprKind::Call { + kind: Rc::new(ExprKind::Call { func: Expr::local_var("deref"), args: vec![Expr::local_var(&scrutinee).read()], purity: Purity::Pure, from_user: false, - }, + }), }), body: build_inner_match(vec![(scrutinee.clone(), pattern.clone())], body), - }, + }), }), Pattern::Or(_) => panic!("Or pattern should have been flattened"), - Pattern::Tuple(patterns) => Box::new(Expr { + Pattern::Tuple(patterns) => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Match { - scrutinee: Box::new(Expr::local_var(&scrutinee).read()), + kind: Rc::new(ExprKind::Match { + scrutinee: Expr::local_var(&scrutinee).read(), arms: vec![MatchArm { pattern: Rc::new(Pattern::Tuple( patterns.iter().map(|_| Rc::new(Pattern::Wild)).collect(), @@ -411,25 +411,25 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B ); patterns.iter().enumerate().rfold(body, |body, (index, _)| { - Box::new(Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(format!("γ{index}")), init: { let init = (0..(patterns.len() - 1 - index)).fold( Expr::local_var(&scrutinee), |init, _| { - Box::new(Expr { + Rc::new(Expr { ty: None, - kind: ExprKind::Call { + kind: Rc::new(ExprKind::Call { func: Expr::local_var( "Tuple.Access.left", ), - args: vec![*init], + args: vec![init], purity: Purity::Pure, from_user: false, - }, + }), }) }, ); @@ -437,29 +437,29 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B if index == 0 { init } else { - Box::new(Expr { + Rc::new(Expr { ty: None, - kind: ExprKind::Call { + kind: Rc::new(ExprKind::Call { func: Expr::local_var("Tuple.Access.right"), - args: vec![*init], + args: vec![init], purity: Purity::Pure, from_user: false, - }, + }), }) } }, body, - }, + }), }) }) }, }], - }, + }), }), - Pattern::Lit(_) => Box::new(Expr { + Pattern::Lit(_) => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Match { - scrutinee: Box::new(Expr::local_var(&scrutinee).read()), + kind: Rc::new(ExprKind::Match { + scrutinee: Expr::local_var(&scrutinee).read(), arms: vec![ MatchArm { pattern: pattern.clone(), @@ -467,15 +467,15 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B }, default_match_arm.clone(), ], - }, + }), }), Pattern::Slice { init_patterns, slice_pattern, - } => Box::new(Expr { + } => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Match { - scrutinee: Box::new(Expr::local_var(&scrutinee).read()), + kind: Rc::new(ExprKind::Match { + scrutinee: Expr::local_var(&scrutinee).read(), arms: vec![ MatchArm { pattern: Rc::new(Pattern::Slice { @@ -510,23 +510,23 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B let body = match slice_pattern { None => body, - Some(_) => Box::new(Expr { + Some(_) => Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some("γ".to_string()), - init: Box::new(Expr { + init: Rc::new(Expr { ty: None, - kind: ExprKind::NamedField { + kind: Rc::new(ExprKind::NamedField { base: Expr::local_var(&scrutinee), name: format!( "[{}].slice", init_patterns.len() ), - }, + }), }), body, - }, + }), }), }; @@ -534,32 +534,32 @@ fn build_inner_match(patterns: Vec<(String, Rc)>, body: Box) -> B .iter() .enumerate() .rfold(body, |body, (index, _)| { - Box::new(Expr { + Rc::new(Expr { ty: body.ty.clone(), - kind: ExprKind::Let { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some(format!("γ{index}")), - init: Box::new(Expr { + init: Rc::new(Expr { ty: None, - kind: ExprKind::NamedField { + kind: Rc::new(ExprKind::NamedField { base: Expr::local_var(&scrutinee), name: format!("[{index}]",), - }, + }), }), body, - }, + }), }) }) }, }, default_match_arm.clone(), ], - }, + }), }), }) } -fn build_match(scrutinee: Expr, arms: Vec, _ty: Option>) -> ExprKind { +fn build_match(scrutinee: Rc, arms: Vec, _ty: Option>) -> Rc { let arms_with_flatten_patterns = arms.into_iter().flat_map(|MatchArm { pattern, body }| { pattern .flatten_ors() @@ -570,36 +570,38 @@ fn build_match(scrutinee: Expr, arms: Vec, _ty: Option>) - }) }); - ExprKind::Call { + Rc::new(ExprKind::Call { func: Expr::local_var("match_operator"), args: vec![ scrutinee, - Expr { - kind: ExprKind::Array { + Rc::new(Expr { + kind: Rc::new(ExprKind::Array { elements: arms_with_flatten_patterns - .map(|MatchArm { pattern, body }| Expr { - kind: ExprKind::Lambda { - args: vec![("γ".to_string(), None)], - body: build_inner_match(vec![("γ".to_string(), pattern)], body), - is_for_match: true, - }, - ty: None, + .map(|MatchArm { pattern, body }| { + Rc::new(Expr { + kind: Rc::new(ExprKind::Lambda { + args: vec![("γ".to_string(), None)], + body: build_inner_match(vec![("γ".to_string(), pattern)], body), + is_for_match: true, + }), + ty: None, + }) }) .collect(), - }, + }), ty: None, - }, + }), ], purity: Purity::Effectful, from_user: false, - } + }) } fn compile_expr_kind<'a>( env: &mut Env<'a>, thir: &rustc_middle::thir::Thir<'a>, expr_id: &rustc_middle::thir::ExprId, -) -> ExprKind { +) -> Rc { let expr = thir.exprs.get(*expr_id).unwrap(); let ty = compile_type(env, &expr.ty); @@ -607,17 +609,18 @@ fn compile_expr_kind<'a>( thir::ExprKind::Scope { value, .. } => compile_expr_kind(env, thir, value), thir::ExprKind::Box { value } => { let value = compile_expr(env, thir, value); - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar( + + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar( "(alloc.boxed.Box _ alloc.boxed.Box.Default.A)::[\"new\"]".to_string(), - ), + )), ty: None, }), args: vec![value], purity: Purity::Effectful, from_user: true, - } + }) } thir::ExprKind::If { cond, @@ -625,17 +628,17 @@ fn compile_expr_kind<'a>( else_opt, .. } => { - let condition = Box::new(compile_expr(env, thir, cond).read()); - let success = Box::new(compile_expr(env, thir, then)); + let condition = compile_expr(env, thir, cond).read(); + let success = compile_expr(env, thir, then); let failure = match else_opt { - Some(else_expr) => Box::new(compile_expr(env, thir, else_expr)), - None => Box::new(Expr::tt()), + Some(else_expr) => compile_expr(env, thir, else_expr), + None => Expr::tt(), }; - ExprKind::If { + Rc::new(ExprKind::If { condition, success, failure, - } + }) } thir::ExprKind::Call { fun, args, .. } => { let args = args @@ -643,39 +646,43 @@ fn compile_expr_kind<'a>( .map(|arg| compile_expr(env, thir, arg).read()) .collect(); let func = compile_expr(env, thir, fun); - let (purity, from_user) = match &func.match_simple_call(&["M.alloc"]) { - Some(Expr { - kind: ExprKind::Constructor(_), - .. - }) => (Purity::Pure, false), - _ => (Purity::Effectful, true), + let (purity, from_user) = { + let default = (Purity::Effectful, true); + + match func.clone().match_simple_call(&["M.alloc"]).as_ref() { + Some(expr) => match expr.kind.as_ref() { + ExprKind::Constructor(_) => (Purity::Pure, false), + _ => default, + }, + _ => default, + } }; - let func = Box::new(func.read()); + let func = func.read(); - ExprKind::Call { + Rc::new(ExprKind::Call { func, args, purity, from_user, - } + }) .alloc(Some(ty)) } thir::ExprKind::Deref { arg } => { let arg = compile_expr(env, thir, arg).read(); - if let Some(borrowed) = Expr::match_borrow(&arg) { - return borrowed.kind; + if let Some(borrowed) = Expr::match_borrow(arg.clone()) { + return borrowed.kind.clone(); } - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar("deref".to_string()), + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("deref".to_string())), ty: None, }), args: vec![arg], purity: Purity::Pure, from_user: false, - } + }) } thir::ExprKind::Binary { op, lhs, rhs } => { let left_ty = compile_type(env, &thir.exprs.get(*lhs).unwrap().ty); @@ -683,15 +690,15 @@ fn compile_expr_kind<'a>( let (path, purity) = path_of_bin_op(op, &left_ty, &right_ty); let lhs = compile_expr(env, thir, lhs); let rhs = compile_expr(env, thir, rhs); - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::Var(path), + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::Var(path)), ty: None, }), args: vec![lhs.read(), rhs.read()], purity, from_user: false, - } + }) .alloc(Some(ty)) } thir::ExprKind::LogicalOp { op, lhs, rhs } => { @@ -701,15 +708,15 @@ fn compile_expr_kind<'a>( }; let lhs = compile_expr(env, thir, lhs); let rhs = compile_expr(env, thir, rhs); - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::Var(path), + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::Var(path)), ty: None, }), args: vec![lhs.read(), rhs.read()], purity: Purity::Pure, from_user: false, - } + }) .alloc(Some(ty)) } thir::ExprKind::Unary { op, arg } => { @@ -718,74 +725,75 @@ fn compile_expr_kind<'a>( UnOp::Neg => (Path::new(&["UnOp", "neg"]), Purity::Effectful), }; let arg = compile_expr(env, thir, arg); - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::Var(path), + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::Var(path)), ty: None, }), args: vec![arg.read()], purity, from_user: false, - } + }) .alloc(Some(ty)) } thir::ExprKind::Cast { source } => { - let func = Box::new(Expr { - kind: ExprKind::LocalVar("cast".to_string()), + let func = Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("cast".to_string())), ty: None, }); let source = compile_expr(env, thir, source); - ExprKind::Call { + Rc::new(ExprKind::Call { func, args: vec![source.read()], purity: Purity::Effectful, from_user: false, - } + }) .alloc(Some(ty)) } thir::ExprKind::Use { source } => { let source = compile_expr(env, thir, source); - ExprKind::Use(Box::new(source)) + + Rc::new(ExprKind::Use(source)) } thir::ExprKind::NeverToAny { source } => { - let func = Box::new(Expr { - kind: ExprKind::LocalVar("never_to_any".to_string()), + let func = Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("never_to_any".to_string())), ty: None, }); let source = compile_expr(env, thir, source); - ExprKind::Call { + Rc::new(ExprKind::Call { func, args: vec![source.read()], purity: Purity::Effectful, from_user: false, - } + }) .alloc(Some(ty)) } thir::ExprKind::Pointer { source, cast } => { - let func = Box::new(Expr { - kind: ExprKind::LocalVar("pointer_coercion".to_string()), + let func = Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("pointer_coercion".to_string())), ty: None, }); let source = compile_expr(env, thir, source); - let cast = Expr { - kind: ExprKind::Message(format!("{cast:?}")), + let cast = Rc::new(Expr { + kind: Rc::new(ExprKind::Message(format!("{cast:?}"))), ty: None, - }; - ExprKind::Call { + }); + Rc::new(ExprKind::Call { func, args: vec![cast, source], purity: Purity::Pure, from_user: false, - } + }) } thir::ExprKind::Loop { body, .. } => { - let body = Box::new(compile_expr(env, thir, body)); - ExprKind::Loop { body } + let body = compile_expr(env, thir, body); + Rc::new(ExprKind::Loop { body }) } thir::ExprKind::Let { expr, pat } => { let pat = crate::thir_pattern::compile_pattern(env, pat); - let init = Box::new(compile_expr(env, thir, expr)); - ExprKind::LetIf { pat, init } + let init = compile_expr(env, thir, expr); + Rc::new(ExprKind::LetIf { pat, init }) } thir::ExprKind::Match { scrutinee, arms } => { let scrutinee = compile_expr(env, thir, scrutinee); @@ -794,28 +802,30 @@ fn compile_expr_kind<'a>( .map(|arm_id| { let arm = thir.arms.get(*arm_id).unwrap(); let pattern = crate::thir_pattern::compile_pattern(env, &arm.pattern); - let body = Box::new(compile_expr(env, thir, &arm.body)); + let body = compile_expr(env, thir, &arm.body); MatchArm { pattern, body } }) .collect(); build_match(scrutinee, arms, Some(ty.val())) } - thir::ExprKind::Block { block: block_id } => compile_block(env, thir, block_id).kind, + thir::ExprKind::Block { block: block_id } => { + compile_block(env, thir, block_id).kind.clone() + } thir::ExprKind::Assign { lhs, rhs } => { - let func = Box::new(Expr { - kind: ExprKind::LocalVar("assign".to_string()), + let func = Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("assign".to_string())), ty: None, }); let args = vec![ compile_expr(env, thir, lhs), compile_expr(env, thir, rhs).read(), ]; - ExprKind::Call { + Rc::new(ExprKind::Call { func, args, purity: Purity::Effectful, from_user: false, - } + }) } thir::ExprKind::AssignOp { op, lhs, rhs } => { let left_ty = compile_type(env, &thir.exprs.get(*lhs).unwrap().ty); @@ -824,76 +834,76 @@ fn compile_expr_kind<'a>( let lhs = compile_expr(env, thir, lhs); let rhs = compile_expr(env, thir, rhs); - ExprKind::Let { + Rc::new(ExprKind::Let { is_monadic: false, name: Some("β".to_string()), - init: Box::new(lhs), - body: Box::new(Expr { - kind: ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::Var(Path::new(&["assign"])), + init: lhs, + body: Rc::new(Expr { + kind: Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::Var(Path::new(&["assign"]))), ty: None, }), args: vec![ - Expr { - kind: ExprKind::LocalVar("β".to_string()), + Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("β".to_string())), ty: None, - }, - Expr { - kind: ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::Var(path), + }), + Rc::new(Expr { + kind: Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::Var(path)), ty: None, }), args: vec![ - Expr { - kind: ExprKind::LocalVar("β".to_string()), + Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("β".to_string())), ty: None, - } + }) .read(), rhs.read(), ], purity, from_user: false, - }, + }), ty: None, - }, + }), ], purity: Purity::Effectful, from_user: false, - }, + }), ty: None, }), - } + }) } thir::ExprKind::Field { lhs, variant_index, name, } => { - let base = Box::new(compile_expr(env, thir, lhs)); + let base = compile_expr(env, thir, lhs); let ty = thir.exprs.get(*lhs).unwrap().ty; match ty.ty_adt_def() { Some(adt_def) => { let variant = adt_def.variant(*variant_index); let name = variant.fields.get(*name).unwrap().name.to_string(); - ExprKind::NamedField { base, name } + Rc::new(ExprKind::NamedField { base, name }) } - None => ExprKind::Message("Unknown Field".to_string()), + None => Rc::new(ExprKind::Message("Unknown Field".to_string())), } } thir::ExprKind::Index { lhs, index } => { - let base = Box::new(compile_expr(env, thir, lhs)); - let index = Box::new(compile_expr(env, thir, index)); - ExprKind::Index { base, index } + let base = compile_expr(env, thir, lhs); + let index = compile_expr(env, thir, index); + Rc::new(ExprKind::Index { base, index }) } thir::ExprKind::VarRef { id } => { let name = to_valid_coq_name(env.tcx.hir().opt_name(id.0).unwrap().as_str()); - ExprKind::LocalVar(name) + Rc::new(ExprKind::LocalVar(name)) } thir::ExprKind::UpvarRef { var_hir_id, .. } => { let name = to_valid_coq_name(env.tcx.hir().opt_name(var_hir_id.0).unwrap().as_str()); - ExprKind::LocalVar(name) + Rc::new(ExprKind::LocalVar(name)) } thir::ExprKind::Borrow { borrow_kind, arg } => { let arg = compile_expr(env, thir, arg); @@ -906,52 +916,54 @@ fn compile_expr_kind<'a>( rustc_middle::mir::Mutability::Mut => "addr_of_mut".to_string(), }; let arg = compile_expr(env, thir, arg); - ExprKind::Call { - func: Box::new(Expr { - kind: ExprKind::LocalVar(func), + Rc::new(ExprKind::Call { + func: Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(func)), ty: None, }), args: vec![arg], purity: Purity::Pure, from_user: false, - } + }) + } + thir::ExprKind::Break { .. } => Rc::new(ExprKind::ControlFlow(LoopControlFlow::Break)), + thir::ExprKind::Continue { .. } => { + Rc::new(ExprKind::ControlFlow(LoopControlFlow::Continue)) } - thir::ExprKind::Break { .. } => ExprKind::ControlFlow(LoopControlFlow::Break), - thir::ExprKind::Continue { .. } => ExprKind::ControlFlow(LoopControlFlow::Continue), thir::ExprKind::Return { value } => { let value = match value { Some(value) => compile_expr(env, thir, value).read(), None => Expr::tt(), }; - ExprKind::Return(Box::new(value)) + Rc::new(ExprKind::Return(value)) } - thir::ExprKind::ConstBlock { did, .. } => ExprKind::Var(compile_def_id(env, *did)), + thir::ExprKind::ConstBlock { did, .. } => Rc::new(ExprKind::Var(compile_def_id(env, *did))), thir::ExprKind::Repeat { value, count } => { - let func = Box::new(Expr { - kind: ExprKind::LocalVar("repeat".to_string()), + let func = Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("repeat".to_string())), ty: None, }); let args = vec![ compile_expr(env, thir, value).read(), - Expr { - kind: ExprKind::LocalVar(count.to_string()), + Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(count.to_string())), ty: None, - }, + }), ]; - ExprKind::Call { + Rc::new(ExprKind::Call { func, args, purity: Purity::Pure, from_user: false, - } + }) .alloc(Some(ty)) } - thir::ExprKind::Array { fields } => ExprKind::Array { + thir::ExprKind::Array { fields } => Rc::new(ExprKind::Array { elements: fields .iter() .map(|field| compile_expr(env, thir, field).read()) .collect(), - } + }) .alloc(Some(ty)), thir::ExprKind::Tuple { fields } => { let elements: Vec<_> = fields @@ -961,7 +973,7 @@ fn compile_expr_kind<'a>( if elements.is_empty() { ExprKind::tt() } else { - ExprKind::Tuple { elements }.alloc(Some(ty)) + Rc::new(ExprKind::Tuple { elements }).alloc(Some(ty)) } } thir::ExprKind::Adt(adt_expr) => { @@ -992,27 +1004,27 @@ fn compile_expr_kind<'a>( StructOrVariant::Struct }; if fields.is_empty() { - return ExprKind::StructUnit { + return Rc::new(ExprKind::StructUnit { path, struct_or_variant, - } + }) .alloc(Some(ty)); } if is_a_tuple { let fields = fields.into_iter().map(|(_, pattern)| pattern).collect(); - ExprKind::StructTuple { + Rc::new(ExprKind::StructTuple { path, fields, struct_or_variant, - } + }) .alloc(Some(ty)) } else { - ExprKind::StructStruct { + Rc::new(ExprKind::StructStruct { path, fields, base: None, struct_or_variant, - } + }) .alloc(Some(ty)) } } @@ -1039,19 +1051,19 @@ fn compile_expr_kind<'a>( None => None, }) .collect(); - let body = Box::new(compile_expr(env, &thir, &expr_id).read()); + let body = compile_expr(env, &thir, &expr_id).read(); let body = args .iter() .enumerate() .rfold(body, |body, (index, (pattern, _))| { let ty = body.ty.clone(); - Box::new(Expr { + Rc::new(Expr { kind: build_match( - Expr { - kind: ExprKind::LocalVar(format!("α{index}")).alloc(None), + Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar(format!("α{index}"))).alloc(None), ty: None, - }, + }), vec![MatchArm { pattern: pattern.clone(), body, @@ -1067,34 +1079,38 @@ fn compile_expr_kind<'a>( .map(|(index, (_, ty))| (format!("α{index}"), Some(ty.clone()))) .collect(); - ExprKind::Lambda { + Rc::new(ExprKind::Lambda { args, body, is_for_match: false, - } + }) .alloc(Some(ty)) } thir::ExprKind::Literal { lit, neg } => match lit.node { rustc_ast::LitKind::Str(symbol, _) => { - ExprKind::Literal(Literal::String(symbol.to_string())) + Rc::new(ExprKind::Literal(Literal::String(symbol.to_string()))) + } + rustc_ast::LitKind::Char(c) => { + Rc::new(ExprKind::Literal(Literal::Char(c))).alloc(Some(ty)) } - rustc_ast::LitKind::Char(c) => ExprKind::Literal(Literal::Char(c)).alloc(Some(ty)), - rustc_ast::LitKind::Int(i, _) => ExprKind::Literal(Literal::Integer { + rustc_ast::LitKind::Int(i, _) => Rc::new(ExprKind::Literal(Literal::Integer { value: i, neg: *neg, - }) + })) .alloc(Some(ty)), - rustc_ast::LitKind::Bool(c) => ExprKind::Literal(Literal::Bool(c)).alloc(Some(ty)), - _ => ExprKind::Literal(Literal::Error), + rustc_ast::LitKind::Bool(c) => { + Rc::new(ExprKind::Literal(Literal::Bool(c))).alloc(Some(ty)) + } + _ => Rc::new(ExprKind::Literal(Literal::Error)), }, - thir::ExprKind::NonHirLiteral { lit, .. } => ExprKind::NonHirLiteral(*lit), + thir::ExprKind::NonHirLiteral { lit, .. } => Rc::new(ExprKind::NonHirLiteral(*lit)), thir::ExprKind::ZstLiteral { .. } => match &expr.ty.kind() { TyKind::FnDef(def_id, generic_args) => { let key = env.tcx.def_key(def_id); let symbol = key.get_opt_name(); let parent = env.tcx.opt_parent(*def_id).unwrap(); let parent_kind = env.tcx.opt_def_kind(parent).unwrap(); - match parent_kind { + Rc::new(match parent_kind { DefKind::Impl { .. } => { let parent_type = env.tcx.type_of(parent).subst(env.tcx, generic_args); let ty = compile_type(env, &parent_type); @@ -1125,7 +1141,7 @@ fn compile_expr_kind<'a>( println!("expression: {:#?}", expr); ExprKind::Message("unimplemented parent_kind".to_string()) } - } + }) .alloc(Some(ty)) } _ => { @@ -1134,35 +1150,41 @@ fn compile_expr_kind<'a>( .sess .struct_span_warn(expr.span, error_message) .emit(); - ExprKind::Message(error_message.to_string()) + Rc::new(ExprKind::Message(error_message.to_string())) } }, thir::ExprKind::NamedConst { def_id, substs, .. } => { let path = compile_def_id(env, *def_id); if substs.is_empty() { - return ExprKind::Var(path); + return Rc::new(ExprKind::Var(path)); } let self_ty = substs.type_at(0); let self_ty = crate::thir_ty::compile_type(env, &self_ty); - ExprKind::VarWithSelfTy { path, self_ty } + Rc::new(ExprKind::VarWithSelfTy { path, self_ty }) + } + thir::ExprKind::ConstParam { def_id, .. } => { + Rc::new(ExprKind::Var(compile_def_id(env, *def_id))) + } + thir::ExprKind::StaticRef { def_id, .. } => { + Rc::new(ExprKind::Var(compile_def_id(env, *def_id))) + } + thir::ExprKind::InlineAsm(_) => Rc::new(ExprKind::LocalVar("InlineAssembly".to_string())), + thir::ExprKind::OffsetOf { .. } => Rc::new(ExprKind::LocalVar("OffsetOf".to_string())), + thir::ExprKind::ThreadLocalRef(def_id) => { + Rc::new(ExprKind::Var(compile_def_id(env, *def_id))) } - thir::ExprKind::ConstParam { def_id, .. } => ExprKind::Var(compile_def_id(env, *def_id)), - thir::ExprKind::StaticRef { def_id, .. } => ExprKind::Var(compile_def_id(env, *def_id)), - thir::ExprKind::InlineAsm(_) => ExprKind::LocalVar("InlineAssembly".to_string()), - thir::ExprKind::OffsetOf { .. } => ExprKind::LocalVar("OffsetOf".to_string()), - thir::ExprKind::ThreadLocalRef(def_id) => ExprKind::Var(compile_def_id(env, *def_id)), thir::ExprKind::Yield { value } => { - let func = Box::new(Expr { - kind: ExprKind::LocalVar("yield".to_string()), + let func = Rc::new(Expr { + kind: Rc::new(ExprKind::LocalVar("yield".to_string())), ty: None, }); let args = vec![compile_expr(env, thir, value)]; - ExprKind::Call { + Rc::new(ExprKind::Call { func, args, purity: Purity::Effectful, from_user: false, - } + }) } } } @@ -1172,7 +1194,7 @@ fn compile_stmts<'a>( thir: &rustc_middle::thir::Thir<'a>, stmt_ids: &[rustc_middle::thir::StmtId], expr_id: Option, -) -> Expr { +) -> Rc { stmt_ids.iter().rev().fold( { match &expr_id { @@ -1181,7 +1203,6 @@ fn compile_stmts<'a>( } }, |body, stmt_id| { - let body = Box::new(body); let stmt = thir.stmts.get(*stmt_id).unwrap(); match &stmt.kind { thir::StmtKind::Let { @@ -1200,28 +1221,28 @@ fn compile_stmts<'a>( name, pattern: None, .. - } => ExprKind::Let { + } => Rc::new(ExprKind::Let { is_monadic: false, name: Some(name.clone()), - init: Box::new(init.copy()), + init: init.copy(), body, - }, + }), _ => build_match(init, vec![MatchArm { pattern, body }], ty.clone()), }; - Expr { kind, ty } + Rc::new(Expr { kind, ty }) } thir::StmtKind::Expr { expr: expr_id, .. } => { - let init = Box::new(compile_expr(env, thir, expr_id)); + let init = compile_expr(env, thir, expr_id); let ty = body.ty.clone(); - Expr { - kind: ExprKind::Let { + Rc::new(Expr { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: None, init, body, - }, + }), ty, - } + }) } } }, @@ -1232,7 +1253,7 @@ fn compile_block<'a>( env: &mut Env<'a>, thir: &rustc_middle::thir::Thir<'a>, block_id: &rustc_middle::thir::BlockId, -) -> Expr { +) -> Rc { let block = thir.blocks.get(*block_id).unwrap(); compile_stmts(env, thir, &block.stmts, block.expr) } diff --git a/lib/src/thir_ty.rs b/lib/src/thir_ty.rs index cef023434..d7f4a9ae9 100644 --- a/lib/src/thir_ty.rs +++ b/lib/src/thir_ty.rs @@ -32,7 +32,7 @@ pub(crate) fn compile_type<'a>(env: &Env<'a>, ty: &rustc_middle::ty::Ty<'a>) -> .collect(); Rc::new(CoqType::Application { func: Rc::new(CoqType::Path { - path: Box::new(path.suffix_last_with_dot_t()), + path: Rc::new(path.suffix_last_with_dot_t()), }), args, is_alias: false, diff --git a/lib/src/top_level.rs b/lib/src/top_level.rs index a161e718c..3de2b24c8 100644 --- a/lib/src/top_level.rs +++ b/lib/src/top_level.rs @@ -39,7 +39,7 @@ struct HirFnSigAndBody<'a> { struct FnSigAndBody { args: Vec<(String, Rc)>, ret_ty: Rc, - body: Option>, + body: Option>, } #[derive(Debug, Eq, Hash, PartialEq)] @@ -70,7 +70,7 @@ struct FunDefinition { enum ImplItemKind { Const { ty: Rc, - body: Option>, + body: Option>, is_dead_code: bool, }, Definition { @@ -136,7 +136,7 @@ enum TopLevelItem { Const { name: String, ty: Rc, - value: Option>, + value: Option>, }, Definition { name: String, @@ -391,7 +391,7 @@ fn compile_top_level_item(tcx: &TyCtxt, env: &mut Env, item: &Item) -> Vec)], body: &rustc_hir::Body, ret_ty: Rc, -) -> Option> { +) -> Option> { if env.axiomatize { return None; } let body = compile_hir_id(env, body.value.hir_id).read(); let has_return = body.has_return(); let body = if has_return { - Box::new(Expr { - kind: ExprKind::Let { + Rc::new(Expr { + kind: Rc::new(ExprKind::Let { is_monadic: false, name: Some("return_".to_string()), - init: Box::new(Expr { - kind: ExprKind::VarWithTy { + init: Rc::new(Expr { + kind: Rc::new(ExprKind::VarWithTy { path: Path::local("M.return_"), ty_name: "R".to_string(), ty: ret_ty, - }, + }), ty: None, }), - body: Box::new(Expr { - kind: ExprKind::MonadicOperator { + body: Rc::new(Expr { + kind: Rc::new(ExprKind::MonadicOperator { name: "M.catch_return".to_string(), - arg: Box::new(body), - }, + arg: body, + }), ty: None, }), - }, + }), ty: None, }) } else { - Box::new(body) + body }; let body = crate::thir_expression::allocate_bindings( &args @@ -1072,8 +1072,9 @@ fn mt_impl_item(item: Rc) -> Rc { let body = match body { None => body.clone(), Some(body) => { - let body = mt_expression(FreshVars::new(), *body.clone()).0; - Some(Box::new(body)) + let body = mt_expression(FreshVars::new(), body.clone()).0; + + Some(body) } }; Rc::new(ImplItemKind::Const { @@ -1097,8 +1098,8 @@ impl FnSigAndBody { body: match &self.body { None => self.body.clone(), Some(body) => { - let (body, _fresh_vars) = mt_expression(FreshVars::new(), *body.clone()); - Some(Box::new(body)) + let (body, _fresh_vars) = mt_expression(FreshVars::new(), body.clone()); + Some(body) } }, }) @@ -1144,8 +1145,8 @@ fn mt_top_level_item(item: Rc) -> Rc { value: match value { None => value.clone(), Some(value) => { - let (value, _fresh_vars) = mt_expression(FreshVars::new(), *value.clone()); - Some(Box::new(value)) + let (value, _fresh_vars) = mt_expression(FreshVars::new(), value.clone()); + Some(value) } }, }), @@ -1428,7 +1429,7 @@ impl FunDefinition { .collect::>(), ] .concat(), - image: Box::new(coq::Expression::Unit), + image: Rc::new(coq::Expression::Unit), }, }, )) @@ -1472,7 +1473,7 @@ impl FunDefinition { ), ] .concat(), - image: Box::new( + image: Rc::new( // return type ret_ty // argument types @@ -1692,7 +1693,7 @@ impl TraitBound { fn to_coq<'a>(&self, self_ty: coq::Expression<'a>) -> coq::Expression<'a> { coq::Expression::Application { - func: Box::new( + func: Rc::new( coq::Expression::Variable { ident: Path::concat(&[self.name.to_owned(), Path::new(&["Trait"])]), no_implicit: false, @@ -2450,9 +2451,9 @@ fn struct_field_value<'a>(name: String) -> coq::Expression<'a> { coq::Expression::just_name("Ref.map").apply_many(&[ coq::Expression::Function { parameters: vec![coq::Expression::just_name("α")], - body: Box::new(coq::Expression::just_name("Some").apply( + body: Rc::new(coq::Expression::just_name("Some").apply( &coq::Expression::RecordField { - record: Box::new(coq::Expression::just_name("α")), + record: Rc::new(coq::Expression::just_name("α")), field: name.to_owned(), }, )), @@ -2462,11 +2463,11 @@ fn struct_field_value<'a>(name: String) -> coq::Expression<'a> { coq::Expression::just_name("β"), coq::Expression::just_name("α"), ], - body: Box::new(coq::Expression::just_name("Some").apply( + body: Rc::new(coq::Expression::just_name("Some").apply( &coq::Expression::RecordUpdate { - record: Box::new(coq::Expression::just_name("α")), + record: Rc::new(coq::Expression::just_name("α")), field: name, - update: Box::new(coq::Expression::just_name("β")), + update: Rc::new(coq::Expression::just_name("β")), }, )), }, @@ -2487,14 +2488,14 @@ fn enum_struct_field_value<'a>( coq::Expression::just_name("Ref.map").apply_many(&[ coq::Expression::Function { parameters: vec![coq::Expression::just_name("α")], - body: Box::new(coq::Expression::Match { - scrutinee: Box::new(coq::Expression::just_name("α")), + body: Rc::new(coq::Expression::Match { + scrutinee: Rc::new(coq::Expression::just_name("α")), arms: [ vec![( coq::Expression::just_name(constructor_name) .apply(&coq::Expression::just_name("α")), coq::Expression::just_name("Some").apply(&coq::Expression::RecordField { - record: Box::new(coq::Expression::just_name("α")), + record: Rc::new(coq::Expression::just_name("α")), field: format!("{constructor_name}.{field_name}"), }), )], @@ -2508,8 +2509,8 @@ fn enum_struct_field_value<'a>( coq::Expression::just_name("β"), coq::Expression::just_name("α"), ], - body: Box::new(coq::Expression::Match { - scrutinee: Box::new(coq::Expression::just_name("α")), + body: Rc::new(coq::Expression::Match { + scrutinee: Rc::new(coq::Expression::just_name("α")), arms: [ vec![( coq::Expression::just_name(constructor_name) @@ -2517,9 +2518,9 @@ fn enum_struct_field_value<'a>( coq::Expression::just_name("Some").apply( &coq::Expression::just_name(constructor_name).apply( &coq::Expression::RecordUpdate { - record: Box::new(coq::Expression::just_name("α")), + record: Rc::new(coq::Expression::just_name("α")), field: format!("{constructor_name}.{field_name}"), - update: Box::new(coq::Expression::just_name("β")), + update: Rc::new(coq::Expression::just_name("β")), }, ), ), @@ -2547,8 +2548,8 @@ fn enum_tuple_field_value( coq::Expression::just_name("Ref.map").apply_many(&[ coq::Expression::Function { parameters: vec![coq::Expression::just_name("α")], - body: Box::new(coq::Expression::Match { - scrutinee: Box::new(coq::Expression::just_name("α")), + body: Rc::new(coq::Expression::Match { + scrutinee: Rc::new(coq::Expression::just_name("α")), arms: [ vec![( coq::Expression::just_name(constructor_name).apply_many( @@ -2575,8 +2576,8 @@ fn enum_tuple_field_value( coq::Expression::just_name("β"), coq::Expression::just_name("α"), ], - body: Box::new(coq::Expression::Match { - scrutinee: Box::new(coq::Expression::just_name("α")), + body: Rc::new(coq::Expression::Match { + scrutinee: Rc::new(coq::Expression::just_name("α")), arms: [ vec![( coq::Expression::just_name(constructor_name).apply_many( @@ -2754,7 +2755,7 @@ impl TypeStructStruct { // .collect() // ] // .concat(), - // image: Box::new( + // image: Rc::new( // coq::Expression::just_name("t") // .arrows_from(&[ // coq::Expression::just_name("A"), @@ -2846,7 +2847,7 @@ impl TypeStructStruct { ]), &[struct_projection_pattern()], &coq::Expression::NotationsDot { - value: Box::new( + value: Rc::new( coq::Expression::just_name("α"), ), field: name.to_owned(), diff --git a/lib/src/ty.rs b/lib/src/ty.rs index b72828d17..2ec921f10 100644 --- a/lib/src/ty.rs +++ b/lib/src/ty.rs @@ -12,10 +12,10 @@ use std::rc::Rc; pub(crate) enum CoqType { Var(String), Path { - path: Box, + path: Rc, }, PathInTrait { - path: Box, + path: Rc, self_ty: Rc, }, Application { @@ -44,7 +44,7 @@ impl CoqType { pub(crate) fn path(segments: &[&str]) -> Rc { Rc::new(CoqType::Path { - path: Box::new(Path::new(segments)), + path: Rc::new(Path::new(segments)), }) } @@ -72,7 +72,7 @@ impl CoqType { } = &*self { if let CoqType::Path { path, .. } = &**func { - let Path { segments } = *path.clone(); + let Path { segments } = path.as_ref(); if segments.len() == 1 && args.len() == 1 { let name = segments.first().unwrap(); if name == "ref" || name == "mut_ref" { @@ -179,13 +179,13 @@ pub(crate) fn compile_type(env: &Env, ty: &Ty) -> Rc { let coq_path = compile_qpath(env, qpath); let func = Rc::new(match self_ty { Some(self_ty) => CoqType::PathInTrait { - path: Box::new(coq_path.clone()), + path: Rc::new(coq_path.clone()), self_ty, }, None => match is_variable { Some(name) => CoqType::Var(name), None => CoqType::Path { - path: Box::new(if is_alias { + path: Rc::new(if is_alias { coq_path.clone() } else { coq_path.suffix_last_with_dot_t() @@ -212,7 +212,7 @@ pub(crate) fn compile_type(env: &Env, ty: &Ty) -> Rc { segments.push("Default".to_string()); segments.push(name); Rc::new(CoqType::Path { - path: Box::new(Path { segments }), + path: Rc::new(Path { segments }), }) } else { Rc::new(CoqType::Infer) @@ -362,11 +362,11 @@ impl CoqType { no_implicit: false, }, CoqType::Path { path } => coq::Expression::Variable { - ident: *path.clone(), + ident: path.as_ref().clone(), no_implicit: false, }, CoqType::PathInTrait { path, self_ty } => coq::Expression::Variable { - ident: *path.clone(), + ident: path.as_ref().clone(), no_implicit: false, } .apply_many_args(&[ @@ -387,7 +387,7 @@ impl CoqType { if *is_alias { coq::Expression::ModeWrapper { mode: "ltac".to_string(), - expr: Box::new(application), + expr: Rc::new(application), } } else { application