clock existentials

src/expr.rs

@@ -105,6 +105,8 @@ pub enum Expr<'a, R> {
     ClockApp(R, &'a Expr<'a, R>, Clock),
     TypeApp(R, &'a Expr<'a, R>, Type),
     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>),
 }
 
 impl<'a, R> Expr<'a, R> {
@@ -132,6 +134,8 @@ impl<'a, R> Expr<'a, R> {
             Expr::ClockApp(ref r, ref e, c) => Expr::ClockApp(f(r), arena.alloc(e.map_ext(arena, f)), c),
             Expr::TypeApp(ref r, ref e, ref ty) => Expr::TypeApp(f(r), arena.alloc(e.map_ext(arena, f)), ty.clone()),
             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))),
         }
     }
 
@@ -163,6 +167,8 @@ impl<'a, R> Expr<'a, R> {
             Expr::ClockApp(ref r, _, _) => r,
             Expr::TypeApp(ref r, _, _) => r,
             Expr::Binop(ref r, _, _, _) => r,
+            Expr::ExIntro(ref r, _, _) => r,
+            Expr::ExElim(ref r, _, _, _, _) => r,
         }
     }
 }
@@ -249,6 +255,10 @@ impl<'a, 'b, R> fmt::Display for PrettyExpr<'a, 'b, R> {
                 write!(f, "TypeApp({}, {})", self.for_expr(e), self.for_type(ty)),
             Expr::Binop(_, op, ref e1, ref e2) =>
                 write!(f, "Binop({:?}, {}, {})", op, self.for_expr(e1), self.for_expr(e2)),
+            Expr::ExIntro(_, c, ref e) =>
+                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)),
         }
     }
 }

src/interp.rs

@@ -183,6 +183,9 @@ pub fn interp<'a, 'b>(ctx: &InterpretationContext<'a, 'b>, expr: &'a Expr<'a, ()
             interp(ctx, e),
         Expr::Binop(_, op, e1, e2) =>
             interp_binop(op, interp(ctx, e1)?, interp(ctx, e2)?),
+        Expr::ExIntro(_, _, _) |
+        Expr::ExElim(_, _, _, _, _) =>
+            panic!("lol i've abandoned the interpreter"),
     }
 }
 

src/ir1.rs

@@ -464,7 +464,16 @@ impl<'a> Translator<'a> {
                 let e1p = self.translate(ctx.clone(), e1);
                 let e2p = self.translate(ctx, e2);
                 Expr::Op(Op::from_binop(op), self.alloc_slice([self.alloc(e1p), self.alloc(e2p)]))
-            }
+            },
+            HExpr::ExIntro(_, _, e) =>
+                // TODO: will probably need to package up the clock somehow
+                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 e2t = self.translate(new_ctx, e2);
+                Expr::LetIn(self.alloc(e1t), self.alloc(e2t))
+            },
         }
     }
 

src/parse.rs

@@ -97,6 +97,8 @@ make_node_enum!(ConcreteNode {
     ClockAppExpression: clockapp_expression,
     TypeAppExpression: typeapp_expression,
     BinopExpression: binop_expression,
+    ExIntro: ex_intro,
+    ExElim: ex_elim,
     Type: type,
     WrapType: wrap_type,
     BaseType: base_type,
@@ -109,6 +111,7 @@ make_node_enum!(ConcreteNode {
     BoxType: box_type,
     ForallType: forall_type,
     VarType: var_type,
+    ExType: ex_type,
     Kind: kind
 } with matcher ConcreteNodeMatcher);
 
@@ -136,7 +139,9 @@ make_field_enum!(Field {
     Ret: ret,
     Size: size,
     Coeff: coeff,
-    Kind: kind
+    Kind: kind,
+    BinderClock: binderclock,
+    BinderExpr: binderexpr
 } with matcher ConcreteFieldMatcher);
 
 pub struct Parser<'a, 'b> {
@@ -424,6 +429,18 @@ impl<'a, 'b, 'c> AbstractionContext<'a, 'b, 'c> {
                 let e2 = self.parse_expr(self.field(node, Field::Right))?;
                 Ok(Expr::Binop(node.range(), op, self.alloc(e1), self.alloc(e2)))
             },
+            Some(ConcreteNode::ExIntro) => {
+                let c = self.parse_clock(self.field(node, Field::Clock))?;
+                let e = self.parse_expr(self.field(node, Field::Expr))?;
+                Ok(Expr::ExIntro(node.range(), c, self.alloc(e)))
+            },
+            Some(ConcreteNode::ExElim) => {
+                let c = self.identifier(self.field(node, Field::BinderClock));
+                let x = self.identifier(self.field(node, Field::BinderExpr));
+                let e1 = self.parse_expr(self.field(node, Field::Bound))?;
+                let e2 = self.parse_expr(self.field(node, Field::Body))?;
+                Ok(Expr::ExElim(node.range(), c, x, self.alloc(e1), self.alloc(e2)))
+            },
             Some(_) =>
                 Err(ParseError::ExpectedExpression(node.range())),
             None => 
@@ -489,6 +506,11 @@ impl<'a, 'b, 'c> AbstractionContext<'a, 'b, 'c> {
                 let x = self.identifier(node);
                 Ok(Type::TypeVar(x))
             },
+            Some(ConcreteNode::ExType) => {
+                let c = self.identifier(self.field(node, Field::Binder));
+                let ty = self.parse_type(self.field(node, Field::Type))?;
+                Ok(Type::Exists(c, Box::new(ty)))
+            },
             Some(_) =>
                 Err(ParseError::ExpectedType(node.range())),
             None =>

src/typing.rs

@@ -146,6 +146,7 @@ pub enum Type {
     Box(Box<Type>),
     Forall(Symbol, Kind, Box<Type>), // forall (x : k). ty
     TypeVar(Symbol),
+    Exists(Symbol, Box<Type>),
 }
 
 fn mk_fresh(prefix: Symbol, interner: &mut DefaultStringInterner) -> Symbol {
@@ -196,6 +197,8 @@ impl Type {
             Type::Forall(_, _, _) => false,
             // TODO: perhaps if we add constraints...
             Type::TypeVar(_) => false,
+            // TODO: is this right? well, it's surely not unsafe, right?
+            Type::Exists(_, _) => false,
         }
     }
 
@@ -247,6 +250,16 @@ impl Type {
                     ToSubst::Type(ref ty) if x == y => ty.clone(),
                     _ => Type::TypeVar(y),
                 },
+            Type::Exists(y, ref ty) => {
+                if x == y {
+                    let new_name = mk_fresh(y, interner);
+                    let replacement = ToSubst::Clock(Clock::from_var(new_name));
+                    let freshened = ty.subst(y, &replacement, interner);
+                    Type::Exists(new_name, Box::new(freshened.subst(x, ts, interner)))
+                } else {
+                    Type::Exists(y, Box::new(ty.subst(x, ts, interner)))
+                }
+            },
         }
     }
 
@@ -283,6 +296,10 @@ impl Type {
                 } else {
                     Err(x)
                 },
+            Type::Exists(x, ref ty) => {
+                let new_ctx = Ctx::TypeVar(x, Kind::Clock, Rc::new(ctx.clone()));
+                ty.check_validity(&new_ctx)
+            },
         }
     }
 }
@@ -357,6 +374,11 @@ impl<'a> PrettyType<'a> {
                 }),
             Type::TypeVar(x) =>
                 write!(f, "{}", self.interner.resolve(x).unwrap()),
+            Type::Exists(x, ref ty) =>
+                parenthesize(f, prec > 0, |f| {
+                    write!(f, "? {}. ", self.interner.resolve(x).unwrap())?;
+                    self.for_type(ty).fmt_prec(f, 0)
+                }),
         }
     }
 }
@@ -432,6 +454,10 @@ impl Ctx {
         Ctx::TermVar(x, ty, Rc::new(self))
     }
 
+    fn with_type_var(self, x: Symbol, k: Kind) -> Ctx {
+        Ctx::TypeVar(x, k, Rc::new(self))
+    }
+
     // TODO: optimize this for the case that it's kept the same?
     fn box_strengthen(&self) -> Ctx {
         match *self {
@@ -543,6 +569,8 @@ pub enum TypeError<'a, R> {
     NonForallClockApp { range: R, purported_forall_clock: &'a Expr<'a, R>, actual_type: Type },
     NonForallTypeApp { range: R, purported_forall_type: &'a Expr<'a, R>, actual_type: Type },
     InvalidType { range: R, purported_type: Type, bad_symbol: Symbol },
+    InvalidClock { range: R, purported_clock: Clock, bad_symbol: Symbol },
+    ExElimNonExists { range: R, expr: &'a Expr<'a, R>, actual_type: Type },
 }
 
 impl<'a, R> TypeError<'a, R> {
@@ -705,6 +733,12 @@ impl<'a> PrettyTypeError<'a, tree_sitter::Range> {
             TypeError::InvalidType { ref purported_type, bad_symbol, .. } =>
                 write!(f, "invalid type \"{}\"; could not find \"{}\" in the context",
                        self.for_type(purported_type), self.interner.resolve(bad_symbol).unwrap()),
+            TypeError::InvalidClock { ref purported_clock, bad_symbol, .. } =>
+                write!(f, "invalid clock \"{}\"; could not find \"{}\" as a clock in the context",
+                       self.for_clock(purported_clock), self.interner.resolve(bad_symbol).unwrap()),
+            TypeError::ExElimNonExists { expr, ref actual_type, .. } =>
+                write!(f, "trying to exists-elim expression \"{}\" of type \"{}\", which is not an exists",
+                       self.for_expr(expr), self.for_type(actual_type)),
         }
     }
 }
@@ -780,17 +814,17 @@ impl<'a> Typechecker<'a> {
                     Err(err) =>
                         Err(TypeError::let_failure(r.clone(), x, e1, err)),
                 },
-            (_, &Expr::LetIn(ref r, x, Some(ref ty), e1, e2)) => {
-                if let Err(err) = self.check(ctx, e1, ty) {
+            (_, &Expr::LetIn(ref r, x, Some(ref e1_ty), e1, e2)) => {
+                if let Err(err) = self.check(ctx, e1, e1_ty) {
                     return Err(TypeError::LetCheckFailure {
                         range: r.clone(),
                         var: x,
-                        expected_type: ty.clone(),
+                        expected_type: e1_ty.clone(),
                         expr: e1,
                         err: Box::new(err)
                     });
                 }
-                let new_ctx = ctx.clone().with_var(x, ty.clone());
+                let new_ctx = ctx.clone().with_var(x, e1_ty.clone());
                 self.check(&new_ctx, e2, ty)
             },
             (&Type::Product(ref ty1, ref ty2), &Expr::Pair(_, e1, e2)) => {
@@ -806,6 +840,16 @@ impl<'a> Typechecker<'a> {
                     ty =>
                         Err(TypeError::unpairing_non_product(r.clone(), e0, ty)),
                 },
+            (_, &Expr::ExElim(ref r, c, x, e0, e)) =>
+                match self.synthesize(ctx, e0)? {
+                    Type::Exists(d, ty_var) => {
+                        let ty_substed = ty_var.subst(d, &ToSubst::Clock(Clock::from_var(c)), self.interner);
+                        let new_ctx = ctx.clone().with_type_var(c, Kind::Clock).with_var(x, ty_substed);
+                        self.check(&new_ctx, e, ty)
+                    },
+                    ty =>
+                        Err(TypeError::ExElimNonExists { range: r.clone(), expr: e0, actual_type: ty }),
+                },
             (&Type::Sum(ref ty1, _), &Expr::InL(_, e)) =>
                 self.check(ctx, e, ty1),
             (&Type::Sum(_, ref ty2), &Expr::InR(_, e)) =>
@@ -841,6 +885,16 @@ impl<'a> Typechecker<'a> {
             },
             (&Type::Box(ref ty), &Expr::Box(_, e)) =>
                 self.check(&ctx.box_strengthen(), e, ty),
+            (&Type::Exists(c, ref ty), &Expr::ExIntro(ref r, d, e)) => {
+                match ctx.lookup_type_var(d.var) {
+                    Some(Kind::Clock) => { }
+                    _ => {
+                        return Err(TypeError::InvalidClock { range: r.clone(), purported_clock: d, bad_symbol: d.var });
+                    }
+                }
+                let expected = ty.subst(c, &ToSubst::Clock(d), self.interner);
+                self.check(ctx, e, &expected)
+            },
             (_, _) => {
                 let synthesized = match self.synthesize(ctx, expr) {
                     Ok(ty) =>
@@ -964,17 +1018,17 @@ impl<'a> Typechecker<'a> {
                     Err(err) =>
                         Err(TypeError::let_failure(r.clone(), x, e1, err)),
                 },
-            &Expr::LetIn(ref r, x, Some(ref ty), e1, e2) => {
-                if let Err(err) = self.check(ctx, e1, ty) {
+            &Expr::LetIn(ref r, x, Some(ref e1_ty), e1, e2) => {
+                if let Err(err) = self.check(ctx, e1, e1_ty) {
                     return Err(TypeError::LetCheckFailure {
                         range: r.clone(),
                         var: x,
-                        expected_type: ty.clone(),
+                        expected_type: e1_ty.clone(),
                         expr: e1,
                         err: Box::new(err)
                     });
                 }
-                let new_ctx = ctx.clone().with_var(x, ty.clone());
+                let new_ctx = ctx.clone().with_var(x, e1_ty.clone());
                 self.synthesize(&new_ctx, e2)
             },
             &Expr::UnPair(ref r, x1, x2, e0, e) =>
@@ -985,7 +1039,17 @@ impl<'a> Typechecker<'a> {
                     },
                     ty =>
                         Err(TypeError::unpairing_non_product(r.clone(), e0, ty)),
-                }
+                },
+            &Expr::ExElim(ref r, c, x, e0, e) =>
+                match self.synthesize(ctx, e0)? {
+                    Type::Exists(d, ty) => {
+                        let ty_substed = ty.subst(d, &ToSubst::Clock(Clock::from_var(c)), self.interner);
+                        let new_ctx = ctx.clone().with_type_var(c, Kind::Clock).with_var(x, ty_substed);
+                        self.synthesize(&new_ctx, e)
+                    },
+                    ty =>
+                        Err(TypeError::ExElimNonExists { range: r.clone(), expr: e0, actual_type: ty }),
+                },
             &Expr::Case(ref r, e0, x1, e1, x2, e2) =>
                 match self.synthesize(ctx, e0)? {
                     Type::Sum(ty1, ty2) => {
@@ -1016,7 +1080,8 @@ impl<'a> Typechecker<'a> {
                     ty =>
                         Err(TypeError::UnboxingNonBox { range: r.clone(), expr: e, actual_type: ty }),
                 },
-            &Expr::ClockApp(ref r, e, c) => 
+            &Expr::ClockApp(ref r, e, c) =>
+                // TODO: check validity of c
                 match self.synthesize(ctx, e)? {
                     Type::Forall(x, Kind::Clock, ty) =>
                         Ok(ty.subst(x, &ToSubst::Clock(c), self.interner)),
@@ -1203,6 +1268,14 @@ fn subtype(ctx: &Ctx, ty1: &Type, ty2: &Type, interner: &mut DefaultStringIntern
         },
         (&Type::TypeVar(x1), &Type::TypeVar(x2)) =>
             x1 == x2,
+        (&Type::Exists(x1, ref ty1p), &Type::Exists(x2, ref ty2p)) => {
+            let fresh_name = mk_fresh(x1, interner);
+            let replacement = ToSubst::from_var(fresh_name, Kind::Clock);
+            let ty1p_subst = ty1p.subst(x1, &replacement, interner);
+            let ty2p_subst = ty2p.subst(x2, &replacement, interner);
+            let new_ctx = Ctx::TypeVar(fresh_name, Kind::Clock, Rc::new(ctx.clone()));
+            subtype(&new_ctx, &ty1p_subst, &ty2p_subst, interner)
+        },
         (_, _) =>
             false,
     }

tests/accept/exist.cky

@@ -0,0 +1,14 @@
+def package_stream : for a : type. for c : clock. ~^(c) a -> ?d. ~^(d) a =
+  \s. clock c and s;;
+
+def enum_stream : for a : type. for c : clock. ~^(c) a -> ~^(c) (index * a) =
+  let go: index -> ~^(c) a -> ~^(c) (index * a) =
+    &^(c) e. \i. \s.
+      let (x, sp) = %s in
+      (i, x) :: `(!(unbox e) (i .+. 1) !sp)
+  in go 0;;
+
+def enum_some_stream : for a : type. (?c. ~^(c) a) -> ?c. ~^(c) (index * a) =
+  \s.
+    let clock c and sp = s in
+    clock c and enum_stream $(a) @(c) sp;;