Merge pull request #31 from yeslogic/brendanzab/rename-cond-types

Rename conditional types to assertion types

Author: brendanzab

experiments/lean/src/ddl/binary/basic.lean

@@ -23,16 +23,16 @@ namespace ddl.binary
     | struct_nil {} : type
     | struct_cons : ℓ → type → type → type
     | array : type → host.expr ℓ → type
-    | cond : type → host.expr ℓ → type
+    | assert : type → host.expr ℓ → type
     | interp : type → host.expr ℓ → host.type ℓ → type
     | abs : kind → type → type
     | app : type → type → type
 
 
-  -- Abstraction and conditional type notation - note that we are using a
+  -- Abstraction and assertition type notation - note that we are using a
   -- nameless representation so we don't include the argument identifiers
   notation `Λ0: ` k `, ` t := type.abs k t
-  notation `{0: ` t ` | ` e ` }` := type.cond t e
+  notation `{0: ` t ` | ` e ` }` := type.assert t e
   -- Array type syntax
   notation `[ ` t `; ` e ` ]` := type.array t e
   -- Application operator

experiments/lean/src/ddl/binary/formation.lean

@@ -37,9 +37,9 @@ namespace ddl.binary
       | array {t e} :
           well_formed t →
           well_formed (array t e)
-      | cond {t e} :
+      | assert {t e} :
           well_formed t →
-          well_formed (cond t e)
+          well_formed (assert t e)
       | interp {t e th} :
           well_formed t →
           well_formed (interp t e th)

experiments/lean/src/ddl/binary/kinding.lean

@@ -33,7 +33,7 @@ namespace ddl.binary
           has_kind Γ t ★ →
           host.has_type e host.type.nat →
           has_kind Γ [ t; e ] ★
-      | cond {Γ t e} :
+      | assert {Γ t e} :
           has_kind Γ t ★ →
           host.has_type /- FIXME: add binding? -/ e host.type.bool →
           has_kind Γ {0: t | e } ★

experiments/lean/src/ddl/binary/monad.lean

@@ -16,7 +16,7 @@ namespace ddl.binary.type
     | (struct_nil)          f := struct_nil
     | (struct_cons l t₁ t₂) f := struct_cons l (bind t₁ f) (bind t₂ f)
     | (array t e)           f := array (bind t f) e
-    | (cond t e)            f := cond (bind t f) e
+    | (assert t e)            f := assert (bind t f) e
     | (interp t e th)       f := interp (bind t f) e th
     | (abs k t)             f := abs k (bind t f)
     | (app t₁ t₂)           f := app (bind t₁ f) (bind t₂ f)
@@ -45,7 +45,7 @@ namespace ddl.binary.type
             simp [bind, function.comp],
             rw [ht],
           },
-          case cond t e ht {
+          case assert t e ht {
             simp [bind, function.comp],
             rw [ht],
           },
@@ -85,7 +85,7 @@ namespace ddl.binary.type
             simp [bind] at ht,
             rw [ht]
           },
-          case cond t e ht {
+          case assert t e ht {
             simp [bind],
             simp [bind] at ht,
             rw [ht]

experiments/lean/src/ddl/binary/repr.lean

@@ -18,7 +18,7 @@ namespace ddl.binary
       | (struct_nil)          := host.type.struct_nil
       | (struct_cons l t₁ t₂) := host.type.struct_cons l t₁.repr t₂.repr
       | (array t e)           := host.type.array (t.repr)
-      | (cond t e)            := t.repr
+      | (assert t e)            := t.repr
       | (interp t e ht)       := ht
       | _                     := sorry
 
@@ -43,7 +43,7 @@ namespace ddl.binary
           case well_formed.array t₁ e hbtwf₁ hhtwf₁ {
             exact host.type.well_formed.array hhtwf₁,
           },
-          case well_formed.cond t₁ e hbtwf₁ hhtwf₁ {
+          case well_formed.assert t₁ e hbtwf₁ hhtwf₁ {
             exact hhtwf₁,
           },
           case well_formed.interp t₁ e ht hbtwf₁ hhtwf₁ {

experiments/lean/src/ddl/binary/subst.lean

@@ -18,7 +18,7 @@ namespace ddl.binary
       | i x (struct_nil) := struct_nil
       | i x (struct_cons l t₁ t₂) := struct_cons l (open_var i x t₁) (open_var i x t₂)
       | i x (array t e) := array (open_var i x t) e
-      | i x (cond t e) := cond (open_var i x t) e
+      | i x (assert t e) := assert (open_var i x t) e
       | i x (interp t e th) := interp (open_var i x t) e th
       | i x (abs k t) := abs k (open_var (i + 1) x t)
       | i x (app t₁ t₂) := app (open_var i x t₁) (open_var i x t₂)
@@ -32,7 +32,7 @@ namespace ddl.binary
       | i x (struct_nil) := struct_nil
       | i x (struct_cons l t₁ t₂) := struct_cons l (close_var i x t₁) (close_var i x t₂)
       | i x (array t e) := array (close_var i x t) e
-      | i x (cond t e) := cond (close_var i x t) e
+      | i x (assert t e) := assert (close_var i x t) e
       | i x (interp t e th) := interp (close_var i x t) e th
       | i x (abs k t) := abs k (close_var (i + 1) x t)
       | i x (app t₁ t₂) := app (close_var i x t₁) (close_var i x t₂)
@@ -51,7 +51,7 @@ namespace ddl.binary
         case struct_nil { admit },
         case struct_cons l t₁ t₂ ht₁ ht₂ { admit },
         case array t e ht { admit },
-        case cond t e ht { admit },
+        case assert t e ht { admit },
         case interp t e ht hht { admit },
         case abs k t ht { admit },
         case app t₁ t₂ ht₁ ht₂ { admit },
@@ -71,7 +71,7 @@ namespace ddl.binary
         case struct_nil { admit },
         case struct_cons l t₁ t₂ ht₁ ht₂ { admit },
         case array t e ht { admit },
-        case cond t e ht { admit },
+        case assert t e ht { admit },
         case interp t e ht hht { admit },
         case abs k t ht { admit },
         case app t₁ t₂ ht₁ ht₂ { admit },

src/nominal/ast.rs

@@ -108,7 +108,7 @@ pub enum Type<N> {
     /// so there is no need to generate new types for these
     Array(RcType<N>, host::RcExpr<N>),
     /// Types dependent on some kind of condition
-    Cond(RcType<N>, host::RcExpr<N>),
+    Assert(RcType<N>, host::RcExpr<N>),
     /// Interpreted types
     Interp(RcType<N>, host::RcExpr<N>, host::RcType<N>),
 }

src/nominal/compile/mod.rs

@@ -99,11 +99,11 @@ fn compile_ty(
 
             Type::path(path.clone())
         }
-        binary::Type::Cond(_, ref ty, ref pred_expr) => {
+        binary::Type::Assert(_, ref ty, ref pred_expr) => {
             let inner_path = path.append_child("Inner");
             let inner_ty = compile_ty(program, &inner_path, ty);
 
-            Type::Cond(Rc::new(inner_ty), pred_expr.clone())
+            Type::Assert(Rc::new(inner_ty), pred_expr.clone())
         }
         binary::Type::Interp(_, ref ty, ref conv_expr, ref conv_ty) => {
             let inner_path = path.append_child("Inner");

src/structural/ast/binary.rs

@@ -48,8 +48,8 @@ pub enum Type<N> {
     Union(Span, Vec<RcType<N>>),
     /// A struct type, with fields: eg. `struct { field : T, ... }`
     Struct(Span, Vec<Field<N, RcType<N>>>),
-    /// A type constrained by a predicate: eg. `T where x => x == 3`
-    Cond(Span, RcType<N>, host::RcExpr<N>),
+    /// A type that is constrained by a predicate: eg. `T where x => x == 3`
+    Assert(Span, RcType<N>, host::RcExpr<N>),
     /// An interpreted type
     Interp(Span, RcType<N>, host::RcExpr<N>, host::RcType<N>),
     /// Type abstraction: eg. `\(a : Type) -> T`
@@ -117,13 +117,13 @@ impl<N: Name> Type<N> {
         Type::Struct(span, fields)
     }
 
-    /// A type constrained by a predicate: eg. `T where x => x == 3`
-    pub fn cond<T1, E1>(span: Span, ty: T1, pred: E1) -> Type<N>
+    /// A type that is constrained by a predicate: eg. `T where x => x == 3`
+    pub fn assert<T1, E1>(span: Span, ty: T1, pred: E1) -> Type<N>
     where
         T1: Into<RcType<N>>,
         E1: Into<host::RcExpr<N>>,
     {
-        Type::Cond(span, ty.into(), pred.into())
+        Type::Assert(span, ty.into(), pred.into())
     }
 
     /// An interpreted type
@@ -186,7 +186,7 @@ impl<N: Name> Type<N> {
                 }
                 return;
             }
-            Type::Cond(_, ref mut ty, ref mut _pred) => {
+            Type::Assert(_, ref mut ty, ref mut _pred) => {
                 Rc::make_mut(ty).substitute(substs);
                 // Rc::make_mut(pred).substitute(substs);
                 return;
@@ -225,7 +225,7 @@ impl<N: Name> Type<N> {
             Type::Struct(_, ref mut fields) => for (i, field) in fields.iter_mut().enumerate() {
                 Rc::make_mut(&mut field.value).abstract_name_at(name, level + i as u32);
             },
-            Type::Cond(_, ref mut ty, ref mut pred) => {
+            Type::Assert(_, ref mut ty, ref mut pred) => {
                 Rc::make_mut(ty).abstract_name_at(name, level);
                 Rc::make_mut(pred).abstract_name_at(name, level + 1);
             }
@@ -264,7 +264,7 @@ impl<N: Name> Type<N> {
             Type::Array(_, ref mut elem_ty, _) => {
                 Rc::make_mut(elem_ty).instantiate_at(level, src);
             }
-            Type::Cond(_, ref mut ty, _) => {
+            Type::Assert(_, ref mut ty, _) => {
                 Rc::make_mut(ty).instantiate_at(level + 1, src);
             }
             Type::Interp(_, ref mut ty, _, _) => {
@@ -303,7 +303,7 @@ impl<N: Name> Type<N> {
 
                 Ok(Rc::new(host::Type::array(elem_repr_ty, size_expr)))
             }
-            Type::Cond(_, ref ty, _) => ty.repr(),
+            Type::Assert(_, ref ty, _) => ty.repr(),
             Type::Interp(_, _, _, ref repr_ty) => Ok(repr_ty.clone()),
             Type::Union(_, ref tys) => {
                 let repr_tys = tys.iter().map(|ty| ty.repr()).collect::<Result<_, _>>()?;

src/structural/check/mod.rs

@@ -286,7 +286,7 @@ pub fn kind_of<N: Name>(
         }
 
         // Conditional types
-        Type::Cond(_, ref ty, ref pred_expr) => {
+        Type::Assert(_, ref ty, ref pred_expr) => {
             expect_ty_kind(ctx, ty)?;
             let pred_ty = host::Type::arrow(ty.repr()?, host::Type::bool());
             expect_ty(ctx, pred_expr, pred_ty)?;

src/structural/parser/grammar.lalrpop

@@ -92,7 +92,7 @@ PrimaryType: RcType<String> = {
         let repr_ty = ty.repr().map_err(|err| {
             ParseError::User { error: GrammarError::from(err) }
         })?;
-        Ok(Type::cond(
+        Ok(Type::assert(
             Span::new(lo1, hi),
             ty,
             Expr::abs(

src/structural/parser/snapshots/tests.parse_ty_where.snap renamed to src/structural/parser/snapshots/tests.parse_ty_assert.snap

@@ -1,9 +1,9 @@
-Cond(
+Assert(
     Span {
         lo: BytePos(9),
         hi: BytePos(117)
     },
-    Cond(
+    Assert(
         Span {
             lo: BytePos(9),
             hi: BytePos(91)
@@ -16,7 +16,7 @@ Cond(
             [
                 Field {
                     name: "x",
-                    value: Cond(
+                    value: Assert(
                         Span {
                             lo: BytePos(33),
                             hi: BytePos(54)

src/structural/parser/tests.rs

@@ -114,7 +114,7 @@ fn parse_ty_empty_struct() {
 }
 
 #[test]
-fn parse_ty_where() {
+fn parse_ty_assert() {
     let src = "
         struct {
             x: u32 where x => x == 3,
@@ -123,7 +123,7 @@ fn parse_ty_where() {
         where x => x == 1
     ";
 
-    assert_snapshot!(parse_ty_where, binary::Type::from_str(src).unwrap());
+    assert_snapshot!(parse_ty_assert, binary::Type::from_str(src).unwrap());
 }
 
 #[test]