Skip to content

Commit

Permalink
[monad-trans] finished the draft version of monad trans; adding test …
Browse files Browse the repository at this point in the history 
…cases
  • Loading branch information
@LighghtEeloo
LighghtEeloo committed Apr 30, 2024
1 parent 3483508 commit fe35484
Show file tree
Hide file tree
Showing 5 changed files with 192 additions and 43 deletions.
5 changes: 2 additions & 3 deletions zydeco-lang/src/library/link.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,9 +107,8 @@ impl From<&ss::TermComputation> for SynComp {
let body = rc!(body.inner_ref().into());
Dtor { body, dtorv: dtor.clone() }.into()
}
ss::TermComputation::BeginBlock(BeginBlock { monad, body }) => {
use crate::statics::MonadTransTerm;
(&body.inner_ref().lift(monad.inner_ref())).into()
ss::TermComputation::BeginBlock(_) => {
unreachable!("BeginBlock not should have been lifted")
}
ss::TermComputation::TyAbsTerm(Abs { param: _, body }) => body.inner_ref().into(),
ss::TermComputation::TyAppTerm(App { body, arg: _ }) => body.inner_ref().into(),
Expand Down
139 changes: 135 additions & 4 deletions zydeco-lang/src/statics/lift.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,146 @@ pub trait MonadTransType {
}

pub trait MonadTransTerm: Clone {
fn lift(&self, m: &TermValue) -> Self;
type Out;
fn lift(&self, m: RcValue, ctx: Ctx) -> Self::Out;
}

pub trait MonadTrans {
fn lift(self, ctx: Ctx) -> Self;
fn trans(self, ctx: Ctx) -> Self;
}

impl MonadTrans for Sp<Program> {
fn lift(self, _ctx: Ctx) -> Self {
todo!()
fn trans(self, ctx: Ctx) -> Self {
let Program { module, entry } = self.inner;
let module = module.trans(ctx.clone());
let entry = (*rc!(entry).trans(ctx)).clone();
self.info.make(Program { module, entry })
}
}

impl MonadTrans for Sp<Module> {
fn trans(self, ctx: Ctx) -> Self {
let Module { name, data, codata, alias, define: old_define, define_ext } = self.inner;
let mut define = Vec::new();
for DeclSymbol { inner: Define { name, def }, public, external } in old_define {
let def = def.trans(ctx.clone());
define.push(DeclSymbol { inner: Define { name, def }, public, external });
}
self.info.make(Module { name, data, codata, alias, define, define_ext })
}
}

impl MonadTrans for RcValue {
fn trans(self, ctx: Ctx) -> Self {
let span = self.span().clone();
match self.inner_ref() {
TermValue::Annotation(Annotation { term, ty }) => {
let term = term.clone().trans(ctx.clone());
span.make_rc(Annotation { term, ty: ty.clone() }.into())
}
TermValue::Var(x) => {
let x = x.clone();
span.make_rc(TermValue::Var(x))
}
TermValue::Thunk(Thunk(body)) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Thunk(body).into())
}
TermValue::Ctor(Ctor { ctorv, args }) => {
let args = args.iter().map(|v| v.clone().trans(ctx.clone()));
span.make_rc(Ctor { ctorv: ctorv.clone(), args: args.collect() }.into())
}
TermValue::Literal(lit) => {
let lit = lit.clone();
span.make_rc(TermValue::Literal(lit))
}
TermValue::Pack(Pack { ty, body }) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Pack { ty: ty.clone(), body }.into())
}
}
}
}

impl MonadTrans for RcComp {
fn trans(self, ctx: Ctx) -> Self {
let span = self.span().clone();
// find only begin-block and call lift
match self.inner_ref() {
TermComputation::Annotation(Annotation { term, ty }) => {
let term = term.clone().trans(ctx.clone());
let ty = ty.clone();
span.make_rc(Annotation { term, ty }.into())
}
TermComputation::Abs(Abs { param, body }) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Abs { param: param.clone(), body }.into())
}
TermComputation::App(App { body, arg }) => {
let body = body.clone().trans(ctx.clone());
let arg = arg.clone().trans(ctx.clone());
span.make_rc(App { body, arg }.into())
}
TermComputation::Ret(Ret(body)) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Ret(body).into())
}
TermComputation::Do(Do { var, comp, body }) => {
let comp = comp.clone().trans(ctx.clone());
let body = body.clone().trans(ctx.clone());
span.make_rc(Do { var: var.clone(), comp, body }.into())
}
TermComputation::Force(Force(body)) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Force(body).into())
}
TermComputation::Let(Let { var, def, body }) => {
let def = def.clone().trans(ctx.clone());
let body = body.clone().trans(ctx.clone());
span.make_rc(Let { var: var.clone(), def, body }.into())
}
TermComputation::Rec(Rec { var, body }) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Rec { var: var.clone(), body }.into())
}
TermComputation::Match(Match { scrut, arms }) => {
let scrut = scrut.clone().trans(ctx.clone());
let arms = arms.iter().map(|arm| {
let Matcher { ctorv, vars, body } = arm;
let body = body.clone().trans(ctx.clone());
Matcher { ctorv: ctorv.clone(), vars: vars.clone(), body }
});
span.make_rc(Match { scrut, arms: arms.collect() }.into())
}
TermComputation::Comatch(Comatch { arms }) => {
let arms = arms.iter().map(|arm| {
let Comatcher { dtorv, body } = arm;
let body = body.clone().trans(ctx.clone());
Comatcher { dtorv: dtorv.clone(), body }
});
span.make_rc(Comatch { arms: arms.collect() }.into())
}
TermComputation::Dtor(Dtor { body, dtorv }) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Dtor { body, dtorv: dtorv.clone() }.into())
}
TermComputation::BeginBlock(BeginBlock { monad, body }) => {
span.make_rc(body.clone().lift(monad.clone(), ctx))
}
TermComputation::TyAbsTerm(Abs { param, body }) => {
let body = body.clone().trans(ctx.clone());
span.make_rc(Abs { param: param.clone(), body }.into())
}
TermComputation::TyAppTerm(App { body, arg }) => {
let body = body.clone().trans(ctx.clone());
let arg = arg.clone();
span.make_rc(App { body, arg }.into())
}
TermComputation::MatchPack(MatchPack { scrut, tvar, var, body }) => {
let scrut = scrut.clone().trans(ctx.clone());
let body = body.clone().trans(ctx.clone());
span.make_rc(MatchPack { scrut, tvar: tvar.clone(), var: var.clone(), body }.into())
}
}
}
}
86 changes: 52 additions & 34 deletions zydeco-lang/src/statics/lift/term.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,102 +2,120 @@ use super::*;

// Note: no type level transformation is performed here since we're gonna remove them right after anyway

impl MonadTransTerm for TermValue {
fn lift(&self, m: &TermValue) -> Self {
match self {
impl MonadTransTerm for Sp<TermValue> {
type Out = TermValue;
fn lift(&self, m: RcValue, ctx: Ctx) -> Self::Out {
match self.inner_ref() {
TermValue::Annotation(Annotation { term, ty }) => {
let span = term.span();
let term = span.make_rc(term.inner_ref().lift(m));
let term = span.make_rc(term.lift(m, ctx.clone()));
Annotation { term, ty: ty.clone() }.into()
}
TermValue::Var(x) => x.clone().into(),
TermValue::Thunk(Thunk(body)) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Thunk(body).into()
}
TermValue::Ctor(Ctor { ctorv, args }) => {
let args = args
.iter()
.map(|v| {
let span = v.span();
span.make_rc(v.inner_ref().lift(m))
span.make_rc(v.lift(m.clone(), ctx.clone()))
})
.collect();
Ctor { ctorv: ctorv.clone(), args }.into()
}
TermValue::Literal(lit) => lit.clone().into(),
TermValue::Pack(Pack { ty, body }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Pack { ty: ty.clone(), body }.into()
}
}
}
}

impl MonadTransTerm for TermComputation {
fn lift(&self, m: &TermValue) -> Self {
match self {
impl MonadTransTerm for Sp<TermComputation> {
type Out = TermComputation;
fn lift(&self, m: RcValue, ctx: Ctx) -> Self::Out {
match self.inner_ref() {
TermComputation::Annotation(Annotation { term, ty }) => {
let span = term.span();
let term = span.make_rc(term.inner_ref().lift(m));
let term = span.make_rc(term.lift(m, ctx.clone()));
Annotation { term, ty: ty.clone() }.into()
}
TermComputation::Abs(Abs { param, body }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Abs { param: param.clone(), body }.into()
}
TermComputation::App(App { body, arg }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let arg = span.make_rc(arg.inner_ref().lift(m));
let body = span.make_rc(body.lift(m.clone(), ctx.clone()));
let arg = span.make_rc(arg.lift(m, ctx.clone()));
App { body, arg }.into()
}
TermComputation::Ret(Ret(arg)) => {
// the return case uses the monad's return
let span = arg.span();
let arg = span.make_rc(arg.inner_ref().lift(m));
let monad = span.make_rc(Force(span.make_rc(m.clone())).into());
let arg = span.make_rc(arg.lift(m.clone(), ctx.clone()));
let monad = span.make_rc(Force(m).into());
let mret = span.make_rc(
Dtor { body: monad, dtorv: DtorV::new(format!("return"), span.clone()) }.into(),
);
App { body: mret, arg }.into()
}
TermComputation::Force(Force(body)) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Force(body).into()
}
TermComputation::Let(Let { var, def, body }) => {
let span = def.span();
let def = span.make_rc(def.inner_ref().lift(m));
let def = span.make_rc(def.lift(m.clone(), ctx.clone()));
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Let { var: var.clone(), def, body }.into()
}
TermComputation::Do(Do { var, comp, body }) => {
// Todo: ...
let span = comp.span();
let comp = span.make_rc(comp.inner_ref().lift(m));
let ty_body = self.syn(ctx.clone()).expect("synthesis of do body failed");
let alg =
ty_body.alg(m.clone(), ctx.clone(), span).expect("failed generating algebra");
let alg_app = span.make_rc(
Dtor {
body: span.make_rc(alg),
dtorv: DtorV::new(format!("bindA"), span.clone()),
}
.into(),
);
let comp = span.make_rc(comp.lift(m.clone(), ctx.clone()));
let thunk_comp: RcValue = span.make_rc(Thunk(comp).into());
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
Do { var: var.clone(), comp, body }.into()
let body = span.make_rc(body.lift(m, ctx.clone()));
let thunk_body: RcValue = span
.make_rc(Thunk(span.make_rc(Abs { param: var.clone(), body }.into())).into());
App {
body: self.span().make_rc(App { body: alg_app, arg: thunk_comp }.into()),
arg: thunk_body,
}
.into()
}
TermComputation::Rec(Rec { var, body }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Rec { var: var.clone(), body }.into()
}
TermComputation::Match(Match { scrut, arms }) => {
let span = scrut.span();
let scrut = span.make_rc(scrut.inner_ref().lift(m));
let scrut = span.make_rc(scrut.lift(m.clone(), ctx.clone()));
let arms = arms
.iter()
.map(|arm| {
let span = arm.body.span();
let body = span.make_rc(arm.body.inner_ref().lift(m));
let body = span.make_rc(arm.body.lift(m.clone(), ctx.clone()));
Matcher { ctorv: arm.ctorv.clone(), vars: arm.vars.clone(), body }
})
.collect();
Expand All @@ -108,39 +126,39 @@ impl MonadTransTerm for TermComputation {
.iter()
.map(|arm| {
let span = arm.body.span();
let body = span.make_rc(arm.body.inner_ref().lift(m));
let body = span.make_rc(arm.body.lift(m.clone(), ctx.clone()));
Comatcher { dtorv: arm.dtorv.clone(), body }
})
.collect();
Comatch { arms }.into()
}
TermComputation::Dtor(Dtor { body, dtorv }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Dtor { body, dtorv: dtorv.clone() }.into()
}
TermComputation::BeginBlock(BeginBlock { monad, body }) => {
let span = monad.span();
let monad = span.make_rc(monad.inner_ref().lift(m));
let monad = span.make_rc(monad.lift(m.clone(), ctx.clone()));
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
BeginBlock { monad, body }.into()
}
TermComputation::TyAbsTerm(Abs { param, body }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
Abs { param: param.clone(), body }.into()
}
TermComputation::TyAppTerm(App { body, arg }) => {
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
App { body, arg: arg.clone() }.into()
}
TermComputation::MatchPack(MatchPack { scrut, tvar, var, body }) => {
let span = scrut.span();
let scrut = span.make_rc(scrut.inner_ref().lift(m));
let scrut = span.make_rc(scrut.lift(m.clone(), ctx.clone()));
let span = body.span();
let body = span.make_rc(body.inner_ref().lift(m));
let body = span.make_rc(body.lift(m, ctx.clone()));
MatchPack { scrut, tvar: tvar.clone(), var: var.clone(), body }.into()
}
}
Expand Down
2 changes: 1 addition & 1 deletion zydeco-lang/src/zydeco.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ impl ZydecoFile {
Ok(ctx)
}
pub fn lift(m: Sp<ss::Program>, ctx: Ctx) -> Result<Sp<ss::Program>, String> {
let m = m.lift(ctx);
let m = m.trans(ctx);
Ok(m)
}
pub fn link(m: ss::Program) -> Result<ls::Program, String> {
Expand Down
3 changes: 2 additions & 1 deletion zydeco-lang/tests/nonzero-exit-code/motrans.zy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,8 @@ end
main
let e = {
with { ! mexnk @(String) } begin
ret 0
do x <- ret 0;
ret x
end
} in
! e .run @(OS) { fn e -> ! panic e } { fn a -> ! exit a }
Expand Down

0 comments on commit fe35484

Please sign in to comment.