Skip to content

Commit

Permalink
implement passing clocks around
Browse files Browse the repository at this point in the history 
(but this will break sampling because i haven't implemented global
clocks to have around yet + verification of the type of main yet)
  • Loading branch information
@jmgrosen
jmgrosen committed Jun 1, 2024
1 parent 4cebbe9 commit 98b7cb2
Show file tree
Hide file tree
Showing 7 changed files with 86 additions and 23 deletions.
9 changes: 9 additions & 0 deletions src/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,11 @@ pub enum Expr<'a, R> {
Binop(R, Binop, &'a Expr<'a, R>, &'a Expr<'a, R>),
ExIntro(R, Clock, &'a Expr<'a, R>),
ExElim(R, Symbol, Symbol, &'a Expr<'a, R>, &'a Expr<'a, R>),
// below this are expressions that are not exposed in the surface syntax

// TODO: this Symbol is in the typevar namespace. we should have
// newtypes for typevar vs termvar namespaces
ClockLam(R, Symbol, &'a Expr<'a, R>),
}

impl<'a, R> Expr<'a, R> {
Expand Down Expand Up @@ -136,6 +141,7 @@ impl<'a, R> Expr<'a, R> {
Expr::Binop(ref r, op, ref e1, ref e2) => Expr::Binop(f(r), op, arena.alloc(e1.map_ext(arena, f)), arena.alloc(e2.map_ext(arena, f))),
Expr::ExIntro(ref r, c, ref e) => Expr::ExIntro(f(r), c, arena.alloc(e.map_ext(arena, f))),
Expr::ExElim(ref r, x1, x2, ref e1, ref e2) => Expr::ExElim(f(r), x1, x2, arena.alloc(e1.map_ext(arena, f)), arena.alloc(e2.map_ext(arena, f))),
Expr::ClockLam(ref r, x, e) => Expr::ClockLam(f(r), x, arena.alloc(e.map_ext(arena, f))),
}
}

Expand Down Expand Up @@ -169,6 +175,7 @@ impl<'a, R> Expr<'a, R> {
Expr::Binop(ref r, _, _, _) => r,
Expr::ExIntro(ref r, _, _) => r,
Expr::ExElim(ref r, _, _, _, _) => r,
Expr::ClockLam(ref r, _, _) => r,
}
}
}
Expand Down Expand Up @@ -259,6 +266,8 @@ impl<'a, 'b, R> fmt::Display for PrettyExpr<'a, 'b, R> {
write!(f, "ExIntro({}, {})", self.for_clock(&c), self.for_expr(e)),
Expr::ExElim(_, x1, x2, ref e1, ref e2) =>
write!(f, "ExElim({}, {}, {}, {})", self.name(x1), self.name(x2), self.for_expr(e1), self.for_expr(e2)),
Expr::ClockLam(_, x, e) =>
write!(f, "ClockLam({}, {})", self.name(x), self.for_expr(e)),
}
}
}
Expand Down
3 changes: 2 additions & 1 deletion src/interp.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,8 @@ pub fn interp<'a, 'b>(ctx: &InterpretationContext<'a, 'b>, expr: &'a Expr<'a, ()
Expr::Binop(_, op, e1, e2) =>
interp_binop(op, interp(ctx, e1)?, interp(ctx, e2)?),
Expr::ExIntro(_, _, _) |
Expr::ExElim(_, _, _, _, _) =>
Expr::ExElim(_, _, _, _, _) |
Expr::ClockLam(_, _, _) =>
panic!("lol i've abandoned the interpreter"),
}
}
Expand Down
71 changes: 54 additions & 17 deletions src/ir1.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use std::{rc::Rc, collections::{HashMap, HashSet}, fmt};

use imbl as im;
use num::rational::Ratio;

use crate::expr::{Expr as HExpr, Symbol, Value as HValue, Binop as HBinop};
use crate::util::ArenaPlus;
Expand Down Expand Up @@ -121,6 +122,7 @@ pub enum Op {
AllocAndFill,
BuildClosure(Global),
LoadGlobal(Global),
ApplyCoeff(Ratio<u32>),
}

impl Op {
Expand Down Expand Up @@ -196,6 +198,7 @@ impl Op {
Op::AllocAndFill => None,
Op::BuildClosure(_) => None,
Op::LoadGlobal(_) => Some(0),
Op::ApplyCoeff(_) => Some(1),
}
}
}
Expand Down Expand Up @@ -298,26 +301,45 @@ impl<'a> Expr<'a> {

pub struct Translator<'a> {
pub globals: HashMap<Symbol, Global>,
pub global_clocks: HashMap<Symbol, Global>,
pub arena: &'a ArenaPlus<'a, Expr<'a>>,
}

pub enum Ctx {
Empty,
Var(Symbol, Rc<Ctx>),
TermVar(Symbol, Rc<Ctx>),
ClockVar(Symbol, Rc<Ctx>),
Silent(Rc<Ctx>),
}

impl Ctx {
fn lookup(&self, x: Symbol) -> Option<DebruijnIndex> {
fn lookup_termvar(&self, x: Symbol) -> Option<DebruijnIndex> {
match *self {
Ctx::Empty =>
None,
Ctx::Var(y, _) if x == y =>
Ctx::TermVar(y, _) if x == y =>
Some(DebruijnIndex::HERE),
Ctx::Var(_, ref next) =>
next.lookup(x).map(|i| i.shifted()),
Ctx::TermVar(_, ref next) =>
next.lookup_termvar(x).map(|i| i.shifted()),
Ctx::ClockVar(_, ref next) =>
next.lookup_termvar(x).map(|i| i.shifted()),
Ctx::Silent(ref next) =>
next.lookup(x).map(|i| i.shifted()),
next.lookup_termvar(x).map(|i| i.shifted()),
}
}

fn lookup_clockvar(&self, x: Symbol) -> Option<DebruijnIndex> {
match *self {
Ctx::Empty =>
None,
Ctx::TermVar(_, ref next) =>
next.lookup_clockvar(x).map(|i| i.shifted()),
Ctx::ClockVar(y, _) if x == y =>
Some(DebruijnIndex::HERE),
Ctx::ClockVar(_, ref next) =>
next.lookup_clockvar(x).map(|i| i.shifted()),
Ctx::Silent(ref next) =>
next.lookup_clockvar(x).map(|i| i.shifted()),
}
}
}
Expand All @@ -334,7 +356,7 @@ impl<'a> Translator<'a> {
pub fn translate<'b, R>(&self, ctx: Rc<Ctx>, expr: &'b HExpr<'b, R>) -> Expr<'a> {
match *expr {
HExpr::Var(_, x) =>
if let Some(idx) = ctx.lookup(x) {
if let Some(idx) = ctx.lookup_termvar(x) {
Expr::Var(idx)
} else if let Some(&glob) = self.globals.get(&x) {
Expr::Glob(glob)
Expand All @@ -352,7 +374,7 @@ impl<'a> Translator<'a> {
HExpr::Annotate(_, next, _) =>
self.translate(ctx, next),
HExpr::Lam(_, x, next) => {
let new_ctx = Rc::new(Ctx::Var(x, ctx));
let new_ctx = Rc::new(Ctx::TermVar(x, ctx));
Expr::Lam(None, 1, self.alloc(self.translate(new_ctx, next)))
},
HExpr::App(_, e1, e2) => {
Expand All @@ -365,7 +387,7 @@ impl<'a> Translator<'a> {
Expr::Adv(self.alloc(et))
},
HExpr::Lob(_, _, x, e) => {
let new_ctx = Rc::new(Ctx::Var(x, ctx));
let new_ctx = Rc::new(Ctx::TermVar(x, ctx));
let et = self.translate(new_ctx, e);
Expr::Lob(None, self.alloc(et))
},
Expand All @@ -376,7 +398,7 @@ impl<'a> Translator<'a> {
},
HExpr::LetIn(_, x, _, e1, e2) => {
let e1t = self.translate(ctx.clone(), e1);
let new_ctx = Rc::new(Ctx::Var(x, ctx));
let new_ctx = Rc::new(Ctx::TermVar(x, ctx));
let e2t = self.translate(new_ctx, e2);
Expr::LetIn(self.alloc(e1t), self.alloc(e2t))
},
Expand All @@ -390,7 +412,7 @@ impl<'a> Translator<'a> {
// in the high level language? i guess somewhat
// because i don't have patterns
let e1t = self.translate(ctx.clone(), e1);
let new_ctx = Rc::new(Ctx::Var(x2, Rc::new(Ctx::Var(x1, Rc::new(Ctx::Silent(ctx))))));
let new_ctx = Rc::new(Ctx::TermVar(x2, Rc::new(Ctx::TermVar(x1, Rc::new(Ctx::Silent(ctx))))));
let e2t = self.translate(new_ctx, e2);
Expr::LetIn(self.alloc(e1t), self.alloc(
Expr::LetIn(self.alloc(
Expand All @@ -415,9 +437,9 @@ impl<'a> Translator<'a> {
HExpr::Case(_, e0, x1, e1, x2, e2) => {
let e0t = self.translate(ctx.clone(), e0);
let new_ctx = Rc::new(Ctx::Silent(ctx));
let new_ctx1 = Rc::new(Ctx::Var(x1, new_ctx.clone()));
let new_ctx1 = Rc::new(Ctx::TermVar(x1, new_ctx.clone()));
let e1t = self.translate(new_ctx1, e1);
let new_ctx2 = Rc::new(Ctx::Var(x2, new_ctx));
let new_ctx2 = Rc::new(Ctx::TermVar(x2, new_ctx));
let e2t = self.translate(new_ctx2, e2);
// TODO: should really make this the same abstraction level as InL/InR...
Expr::LetIn(
Expand Down Expand Up @@ -455,9 +477,19 @@ impl<'a> Translator<'a> {
let et = self.translate(ctx, e);
Expr::Unbox(self.alloc(et))
},
HExpr::ClockApp(_, e, _) =>
// for now...
self.translate(ctx, e),
HExpr::ClockApp(_, e, c) => {
// TODO: factor out this lookup logic
let c_var_expr = self.alloc(if let Some(idx) = ctx.lookup_clockvar(c.var) {
Expr::Var(idx)
} else if let Some(&glob) = self.global_clocks.get(&c.var) {
Expr::Glob(glob)
} else {
panic!("couldn't find clock var??")
});
let c_expr = self.alloc(Expr::Op(Op::ApplyCoeff(c.coeff), self.alloc_slice([c_var_expr])));
let et = self.alloc(self.translate(ctx, e));
Expr::App(et, self.alloc_slice([c_expr]))
},
HExpr::TypeApp(_, e, _) =>
self.translate(ctx, e),
HExpr::Binop(_, op, e1, e2) => {
Expand All @@ -470,10 +502,15 @@ impl<'a> Translator<'a> {
self.translate(ctx, e),
HExpr::ExElim(_, _, x, e1, e2) => {
let e1t = self.translate(ctx.clone(), e1);
let new_ctx = Rc::new(Ctx::Var(x, ctx));
let new_ctx = Rc::new(Ctx::TermVar(x, ctx));
let e2t = self.translate(new_ctx, e2);
Expr::LetIn(self.alloc(e1t), self.alloc(e2t))
},
HExpr::ClockLam(_, x, e) => {
let new_ctx = Rc::new(Ctx::ClockVar(x, ctx));
let et = self.translate(new_ctx, e);
Expr::Lam(None, 1, self.alloc(et))
},
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -338,7 +338,7 @@ fn cmd_compile<'a>(toplevel: &mut TopLevel<'a>, file: Option<PathBuf>, out: Opti
let expr_under_arena = Arena::new();
let expr_ptr_arena = Arena::new();
let expr_arena = util::ArenaPlus { arena: &expr_under_arena, ptr_arena: &expr_ptr_arena };
let translator = ir1::Translator { globals: builtin_globals, arena: &expr_arena };
let translator = ir1::Translator { globals: builtin_globals, global_clocks: HashMap::new(), arena: &expr_arena };


let mut main = None;
Expand Down
18 changes: 15 additions & 3 deletions src/typing.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -790,10 +790,14 @@ impl<'a, 'b, R: Clone> Typechecker<'a, 'b, R> {
pub fn check<'c>(&mut self, ctx: &Ctx, expr: &'c Expr<'c, R>, ty: &Type) -> Result<&'b Expr<'b, R>, TypeError<'c, R>> {
match (ty, expr) {
// CAREFUL! positioning this here matters, with respect to
// the other non-expression-syntax-guided rules
// the other non-type-syntax-guided rules
// (particlarly lob)
(&Type::Forall(x, k, ref ty), _) =>
self.check(&Ctx::TypeVar(x, k, Rc::new(ctx.clone())), expr, ty),
(&Type::Forall(x, Kind::Type, ref ty), _) =>
self.check(&Ctx::TypeVar(x, Kind::Type, Rc::new(ctx.clone())), expr, ty),
(&Type::Forall(x, Kind::Clock, ref ty), _) => {
let expr_elab = self.check(&Ctx::TypeVar(x, Kind::Clock, Rc::new(ctx.clone())), expr, ty)?;
Ok(self.alloc(Expr::ClockLam(expr_elab.range().clone(), x, expr_elab)))
},
(&Type::Unit, &Expr::Val(ref r, Value::Unit)) =>
Ok(self.alloc(Expr::Val(r.clone(), Value::Unit))),
(&Type::Function(ref ty1, ref ty2), &Expr::Lam(ref r, x, e)) => {
Expand Down Expand Up @@ -1200,6 +1204,10 @@ impl<'a, 'b, R: Clone> Typechecker<'a, 'b, R> {
TopLevelDefKind::Let => &running_ctx,
TopLevelDefKind::Def => &Ctx::Empty,
};
// TODO: add clock globals to this somehow
if let Err(missing_symbol) = def.type_.check_validity(ctx) {
errs.push(TopLevelTypeError::InvalidType(def.name, def.type_.clone(), missing_symbol));
}
match self.check(ctx, &def.body, &def.type_) {
Ok(body_elab) => {
defs.push(TopLevelDef { body: body_elab, ..def.clone() });
Expand Down Expand Up @@ -1234,6 +1242,7 @@ impl<'a, 'b, R: Clone> Typechecker<'a, 'b, R> {
pub enum TopLevelTypeError<'b, R> {
TypeError(Symbol, TypeError<'b, R>),
CannotRedefine(Symbol, R),
InvalidType(Symbol, Type, Symbol),
}

#[derive(Debug)]
Expand Down Expand Up @@ -1263,6 +1272,9 @@ impl<'b> fmt::Display for PrettyFileTypeErrors<'b, tree_sitter::Range> {
err.pretty(self.interner, self.code))?,
TopLevelTypeError::CannotRedefine(name, _) =>
write!(f, "cannot redefine \"{}\"", self.interner.resolve(name).unwrap())?,
TopLevelTypeError::InvalidType(name, ref ty, missing) =>
write!(f, "the type \"{}\" of definition \"{}\" is invalid as the clock/type variable \"{}\" is not in the context",
ty.pretty(self.interner), self.interner.resolve(name).unwrap(), self.interner.resolve(missing).unwrap())?,
}
}
Ok(())
Expand Down
4 changes: 4 additions & 0 deletions src/wasm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -576,6 +576,10 @@ impl<'a, 'b> FuncTranslator<'a, 'b> {
(Op::LoadGlobal(Global(g)), _) => {
self.insns.push(wasm::Instruction::GlobalGet(self.translator.globals_offset + g));
},
(Op::ApplyCoeff(_coeff), &[clock]) => {
// TODO: actually apply the coefficient
self.translate(ctx, clock);
},
_ =>
panic!("did not expect {} arguments for op {:?}", args.len(), op)
}
Expand Down
2 changes: 1 addition & 1 deletion tests/accept/double_good.cky
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
def doubleup: ~^(k) sample -> ~^(2k) sample =
def doubleup: for k : clock. ~^(k) sample -> ~^(2k) sample =
&^(k) d. \s.
let (x, sp) = %s in
x :: `(x :: `(!(unbox d) !sp));;

0 comments on commit 98b7cb2

Please sign in to comment.