use lift in cli and web; sprinting

cli/src/main.rs

@@ -36,10 +36,13 @@ fn run_files(
     }
     // type check
     announce_phase(verbose, title, "tyck");
-    ZydecoFile::tyck(m.clone())?;
+    let ctx = ZydecoFile::tyck(m.clone())?;
 
-    // if not dry run, link and eval
+    // if not dry run: lift, link and eval
     if !dry_run {
+        // lift (monad transformation)
+        announce_phase(verbose, title, "lift");
+        let m = ZydecoFile::lift(m, ctx.clone())?;
         // link
         announce_phase(verbose, title, "link");
         let sem_m = ZydecoFile::link(m.inner())?;

web/src/main.rs

@@ -48,7 +48,8 @@ fn ZydecoUI() -> Html {
 fn run(input: &str) -> Result<String, String> {
     let p = ZydecoFile::parse_src(input, PathBuf::new())?;
     let p = ZydecoFile::elab(p)?;
-    ZydecoFile::tyck(p.clone())?;
+    let ctx = ZydecoFile::tyck(p.clone())?;
+    let p = ZydecoFile::lift(p, ctx.clone())?;
     let p = ZydecoFile::link(p.inner)?;
     let p = ZydecoFile::eval_os(p, &[]);
     let s = match p.entry {

zydeco-lang/src/lib.rs

@@ -30,21 +30,15 @@ pub mod statics {
     pub mod err;
     pub mod elab;
     pub mod tyck;
+    pub mod lift;
     mod fmt;
     pub use self::{
         elab::Elaboration,
+        lift::{MonadTransTerm, MonadTransType, MonadTrans},
         tyck::{Ctx, Seal, TypeCheck},
     };
 }
 
-/// monad transformers
-pub mod lift {
-    mod r#type;
-    mod term;
-    pub use r#type::MonadTransType;
-    pub use term::MonadTransTerm;
-}
-
 pub mod library {
     pub mod syntax;
     mod builtins;

zydeco-lang/src/library/link.rs

@@ -108,7 +108,7 @@ impl From<&ss::TermComputation> for SynComp {
                 Dtor { body, dtorv: dtor.clone() }.into()
             }
             ss::TermComputation::BeginBlock(BeginBlock { monad, body }) => {
-                use crate::lift::MonadTransTerm;
+                use crate::statics::MonadTransTerm;
                 (&body.inner_ref().lift(monad.inner_ref())).into()
             }
             ss::TermComputation::TyAbsTerm(Abs { param: _, body }) => body.inner_ref().into(),

zydeco-lang/src/statics/lift.rs

@@ -0,0 +1,25 @@
+use crate::prelude::*;
+use crate::statics::{err::*, syntax::*, tyck::*};
+
+/// monad transformers
+mod r#type;
+mod term;
+
+pub trait MonadTransType {
+    fn lift(&self, ty_m: Type, ctx: Ctx, span: &Span) -> Result<Type, TyckError>;
+    fn alg(&self, m: RcValue, ctx: Ctx, span: &Span) -> Result<TermComputation, TyckError>;
+}
+
+pub trait MonadTransTerm: Clone {
+    fn lift(&self, m: &TermValue) -> Self;
+}
+
+pub trait MonadTrans {
+    fn lift(self, ctx: Ctx) -> Self;
+}
+
+impl MonadTrans for Sp<Program> {
+    fn lift(self, _ctx: Ctx) -> Self {
+        todo!()
+    }
+}

zydeco-lang/src/lift/term.rs → zydeco-lang/src/statics/lift/term.rs

@@ -1,9 +1,4 @@
-use crate::prelude::*;
-use crate::statics::syntax::*;
-
-pub trait MonadTransTerm: Clone {
-    fn lift(&self, m: &TermValue) -> Self;
-}
+use super::*;
 
 // Note: no type level transformation is performed here since we're gonna remove them right after anyway
 

zydeco-lang/src/lift/type.rs → zydeco-lang/src/statics/lift/type.rs

@@ -1,10 +1,4 @@
-use crate::prelude::*;
-use crate::statics::{err::*, syntax::*, tyck::*};
-
-pub trait MonadTransType {
-    fn lift(&self, ty_m: Type, ctx: Ctx, span: &Span) -> Result<Type, TyckError>;
-    fn alg(&self, m: RcValue, ctx: Ctx, span: &Span) -> Result<TermComputation, TyckError>;
-}
+use super::*;
 
 impl MonadTransType for Type {
     fn lift(&self, ty_m: Type, ctx: Ctx, span: &Span) -> Result<Type, TyckError> {

zydeco-lang/src/statics/tyck/computation.rs

@@ -174,7 +174,7 @@ impl TypeCheck for Sp<TermComputation> {
                 Step::Done(ty.inner_clone().subst(diff, &ctx)?)
             }
             TermComputation::BeginBlock(BeginBlock { monad, body }) => {
-                use crate::lift::MonadTransType;
+                use crate::statics::MonadTransType;
                 let ty_u_monad = monad.syn(ctx.clone())?;
                 let ty_monad =
                     ty_u_monad.clone().elim_thunk(ctx.clone(), span).ok_or_else(|| {

zydeco-lang/src/zydeco.rs

@@ -8,7 +8,7 @@ use crate::{
         syntax as ps,
     },
     prelude::*,
-    statics::{syntax as ss, tyck, Ctx, Elaboration, Seal, TypeCheck},
+    statics::{syntax as ss, tyck, Ctx, Elaboration, MonadTrans, Seal, TypeCheck},
     syntax::Env,
     utils::span::FileInfo,
 };
@@ -57,14 +57,14 @@ impl ZydecoFile {
         let p = Elaboration::elab(p).map_err(|e| format!("{}", e))?;
         Ok(p)
     }
-    pub fn tyck(m: Sp<ss::Program>) -> Result<(), String> {
-        m.syn(Ctx::default()).map_err(|e| format!("{}", e))?;
-        Ok(())
+    pub fn tyck(m: Sp<ss::Program>) -> Result<Ctx, String> {
+        let Seal((ctx, _ty)) = m.syn(Ctx::default()).map_err(|e| format!("{}", e))?;
+        Ok(ctx)
+    }
+    pub fn lift(m: Sp<ss::Program>, ctx: Ctx) -> Result<Sp<ss::Program>, String> {
+        let m = m.lift(ctx);
+        Ok(m)
     }
-    // pub fn lift(m: Sp<ss::Program>) -> Result<ss::Program, String> {
-    //     let m = m.lift(Ctx::default());
-    //     Ok(m)
-    // }
     pub fn link(m: ss::Program) -> Result<ls::Program, String> {
         let m: ls::Program = m.into();
         Ok(m)