Seperate built-in types and functions from Expr

5 files changed, 130 insertions, 177 deletions

diff --git a/src/core.rs b/src/core.rs
index 0bc42d4..8b0156c 100644
--- a/src/core.rs
+++ b/src/core.rs
@@ -125,8 +125,10 @@ pub enum Expr<'i, S, A> {
     Let(&'i str, Option<Box<Expr<'i, S, A>>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
     ///  `Annot x t                                ~  x : t`
     Annot(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
-    ///  `Bool                                     ~  Bool`
-    Bool,
+    /// Built-in types
+    BuiltinType(BuiltinType),
+    /// Built-in function values
+    BuiltinValue(BuiltinValue),
     ///  `BoolLit b                                ~  b`
     BoolLit(bool),
     ///  `BoolAnd x y                              ~  x && y`
@@ -139,63 +141,25 @@ pub enum Expr<'i, S, A> {
     BoolNE(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
     ///  `BoolIf x y z                             ~  if x then y else z`
     BoolIf(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
-    ///  `Natural                                  ~  Natural`
-    Natural,
     ///  `NaturalLit n                             ~  +n`
     NaturalLit(Natural),
-    ///  `NaturalFold                              ~  Natural/fold`
-    NaturalFold,
-    ///  `NaturalBuild                             ~  Natural/build`
-    NaturalBuild,
-    ///  `NaturalIsZero                            ~  Natural/isZero`
-    NaturalIsZero,
-    ///  `NaturalEven                              ~  Natural/even`
-    NaturalEven,
-    ///  `NaturalOdd                               ~  Natural/odd`
-    NaturalOdd,
     ///  `NaturalPlus x y                          ~  x + y`
     NaturalPlus(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
     ///  `NaturalTimes x y                         ~  x * y`
     NaturalTimes(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
-    ///  `Integer                                  ~  Integer`
-    Integer,
     ///  `IntegerLit n                             ~  n`
     IntegerLit(Integer),
-    ///  `Double                                   ~  Double`
-    Double,
     ///  `DoubleLit n                              ~  n`
     DoubleLit(Double),
-    ///  `Text                                     ~  Text`
-    Text,
     ///  `TextLit t                                ~  t`
     TextLit(Builder),
     ///  `TextAppend x y                           ~  x ++ y`
     TextAppend(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
-    ///  `List                                     ~  List`
-    List,
     ///  `ListLit t [x, y, z]                      ~  [x, y, z] : List t`
     ListLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
-    ///  `ListBuild                                ~  List/build`
-    ListBuild,
-    ///  `ListFold                                 ~  List/fold`
-    ListFold,
-    ///  `ListLength                               ~  List/length`
-    ListLength,
-    ///  `ListHead                                 ~  List/head`
-    ListHead,
-    ///  `ListLast                                 ~  List/last`
-    ListLast,
-    ///  `ListIndexed                              ~  List/indexed`
-    ListIndexed,
-    ///  `ListReverse                              ~  List/reverse`
-    ListReverse,
-    ///  `Optional                                 ~  Optional`
-    Optional,
     ///  `OptionalLit t [e]                        ~  [e] : Optional t`
     ///  `OptionalLit t []                         ~  []  : Optional t`
     OptionalLit(Box<Expr<'i, S, A>>, Vec<Expr<'i, S, A>>),
-    ///  `OptionalFold                             ~  Optional/fold`
-    OptionalFold,
     ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
     Record(HashMap<&'i str, Expr<'i, S, A>>),
     ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
@@ -216,39 +180,54 @@ pub enum Expr<'i, S, A> {
     Embed(A),
 }
 
-impl<'i, S, A> Expr<'i, S, A> {
-    /// Clones the expression if it is a unit constructor
-    fn clone_unit<T, B>(&self) -> Option<Expr<'static, T, B>> {
-        use Expr::*;
-        match self {
-            &Bool          => Some(Bool),
-            &Natural       => Some(Natural),
-            &NaturalFold   => Some(NaturalFold),
-            &NaturalBuild  => Some(NaturalBuild),
-            &NaturalIsZero => Some(NaturalIsZero),
-            &NaturalEven   => Some(NaturalEven),
-            &NaturalOdd    => Some(NaturalOdd),
-            &Integer       => Some(Integer),
-            &Double        => Some(Double),
-            &Text          => Some(Text),
-            &List          => Some(List),
-            &ListBuild     => Some(ListBuild),
-            &ListFold      => Some(ListFold),
-            &ListLength    => Some(ListLength),
-            &ListHead      => Some(ListHead),
-            &ListLast      => Some(ListLast),
-            &ListIndexed   => Some(ListIndexed),
-            &ListReverse   => Some(ListReverse),
-            &Optional      => Some(Optional),
-            &OptionalFold  => Some(OptionalFold),
-            _              => None,
-        }
-    }
+/// Built-in types
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum BuiltinType {
+    ///  `Bool                                     ~  Bool`
+    Bool,
+    ///  `Natural                                  ~  Natural`
+    Natural,
+    ///  `Integer                                  ~  Integer`
+    Integer,
+    ///  `Double                                   ~  Double`
+    Double,
+    ///  `Text                                     ~  Text`
+    Text,
+    ///  `List                                     ~  List`
+    List,
+    ///  `Optional                                 ~  Optional`
+    Optional,
+}
 
-    /// Returns true if the expression is a unit constructor
-    pub fn is_unit(&self) -> bool {
-        self.clone_unit::<S, A>().is_some()
-    }
+/// Built-in function values
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum BuiltinValue {
+    ///  `NaturalFold                              ~  Natural/fold`
+    NaturalFold,
+    ///  `NaturalBuild                             ~  Natural/build`
+    NaturalBuild,
+    ///  `NaturalIsZero                            ~  Natural/isZero`
+    NaturalIsZero,
+    ///  `NaturalEven                              ~  Natural/even`
+    NaturalEven,
+    ///  `NaturalOdd                               ~  Natural/odd`
+    NaturalOdd,
+    ///  `ListBuild                                ~  List/build`
+    ListBuild,
+    ///  `ListFold                                 ~  List/fold`
+    ListFold,
+    ///  `ListLength                               ~  List/length`
+    ListLength,
+    ///  `ListHead                                 ~  List/head`
+    ListHead,
+    ///  `ListLast                                 ~  List/last`
+    ListLast,
+    ///  `ListIndexed                              ~  List/indexed`
+    ListIndexed,
+    ///  `ListReverse                              ~  List/reverse`
+    ListReverse,
+    ///  `OptionalFold                             ~  Optional/fold`
+    OptionalFold,
 }
 
 impl<'i> From<&'i str> for V<'i> {
@@ -263,6 +242,18 @@ impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
     }
 }
 
+impl<'i, S, A> From<BuiltinType> for Expr<'i, S, A> {
+    fn from(t: BuiltinType) -> Self {
+        Expr::BuiltinType(t)
+    }
+}
+
+impl<'i, S, A> From<BuiltinValue> for Expr<'i, S, A> {
+    fn from(t: BuiltinValue) -> Self {
+        Expr::BuiltinValue(t)
+    }
+}
+
 pub fn pi<'i, S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<'i, S, A>
     where Name: Into<&'i str>,
           Et: Into<Expr<'i, S, A>>,
@@ -509,11 +500,9 @@ shift d v (Note _ b) = b'
 -- and `shift` does nothing to a closed expression
 shift _ _ (Embed p) = Embed p
 */
-        e => if let Some(e2) = e.clone_unit() {
-            e2
-        } else {
-            panic!("Unimplemented shift case: {:?}", (d, v, e))
-        },
+        BuiltinType(t) => BuiltinType(t),
+        BuiltinValue(v) => BuiltinValue(v),
+        e => panic!("Unimplemented shift case: {:?}", (d, v, e)),
     }
 }
 
@@ -556,11 +545,9 @@ pub fn subst<'i, S, T, A>(v: V<'i>, a: Expr<'i, S, A>, b: Expr<'i, T, A>) -> Exp
             let a2 = subst(v, e, *a);
             ListLit(bx(a2), b2)
         }
-        (a, b) => if let Some(e2) = b.clone_unit() {
-            e2
-        } else {
-            panic!("Unimplemented subst case: {:?}", (v, a, b))
-        }
+        (_, BuiltinType(t)) => BuiltinType(t),
+        (_, BuiltinValue(v)) => BuiltinValue(v),
+        (a, b) => panic!("Unimplemented subst case: {:?}", (v, a, b)),
     }
 }
 
@@ -578,6 +565,7 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A>
           T: Clone + ::std::fmt::Debug,
           A: Clone + ::std::fmt::Debug,
 {
+    use BuiltinValue::*;
     use Expr::*;
     match e {
         Const(k) => Const(k),
@@ -633,9 +621,9 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A>
                         go (Var "Zero")          = True
                         go  _                    = False
                         */
-                (NaturalIsZero, NaturalLit(n)) => BoolLit(n == 0),
-                (NaturalEven, NaturalLit(n)) => BoolLit(n % 2 == 0),
-                (NaturalOdd, NaturalLit(n)) => BoolLit(n % 2 != 0),
+                (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
+                (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
+                (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
                 /*
                 App (App ListBuild t) k
                     | check     -> ListLit t (buildVector k')
@@ -697,10 +685,8 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A>
             let es2 = es.into_iter().map(normalize).collect();
             ListLit(bx(t2), es2)
         }
-        _ => if let Some(e2) = e.clone_unit() {
-            e2
-        } else {
-            panic!("Unimplemented normalize case: {:?}", e)
-        }
+        BuiltinType(t) => BuiltinType(t),
+        BuiltinValue(v) => BuiltinValue(v),
+        _ => panic!("Unimplemented normalize case: {:?}", e),
     }
 }
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 63c17ad..0a103d1 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -1,6 +1,7 @@
 use core;
 use core::bx;
 use core::Expr::*;
+use core::BuiltinType::*;
 use grammar_util::*;
 use lexer::*;
 
@@ -119,8 +120,8 @@ ExprF: BoxExpr<'input> = {
     Text => bx(TextLit(<>)),
     Label => bx(Var(core::V(<>, 0))), // FIXME support var@n syntax
     Const => bx(Const(<>)),
-    List => bx(List),
-    Optional => bx(Optional),
+    List => bx(BuiltinType(List)),
+    Optional => bx(BuiltinType(Optional)),
     Builtin => bx(builtin_expr(<>)),
     Bool => bx(BoolLit(<>)),
     Record,
diff --git a/src/grammar_util.rs b/src/grammar_util.rs
index 6927d33..49b7fb8 100644
--- a/src/grammar_util.rs
+++ b/src/grammar_util.rs
@@ -8,23 +8,7 @@ pub type ExprListFn<'i> = fn(BoxExpr<'i>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>
 
 pub fn builtin_expr<'i, S, A>(b: Builtin) -> Expr<'i, S, A> {
     match b {
-        Builtin::Natural => Expr::Natural,
-        Builtin::NaturalFold => Expr::NaturalFold,
-        Builtin::NaturalBuild => Expr::NaturalBuild,
-        Builtin::NaturalIsZero => Expr::NaturalIsZero,
-        Builtin::NaturalEven => Expr::NaturalEven,
-        Builtin::NaturalOdd => Expr::NaturalOdd,
-        Builtin::Integer => Expr::Integer,
-        Builtin::Double => Expr::Double,
-        Builtin::Text => Expr::Text,
-        Builtin::ListBuild => Expr::ListBuild,
-        Builtin::ListFold => Expr::ListFold,
-        Builtin::ListLength => Expr::ListLength,
-        Builtin::ListHead => Expr::ListHead,
-        Builtin::ListLast => Expr::ListLast,
-        Builtin::ListIndexed => Expr::ListIndexed,
-        Builtin::ListReverse => Expr::ListReverse,
-        Builtin::OptionalFold => Expr::OptionalFold,
-        Builtin::Bool => Expr::Bool,
+        Builtin::Type(t)  => Expr::BuiltinType(t),
+        Builtin::Value(v) => Expr::BuiltinValue(v),
     }
 }
diff --git a/src/lexer.rs b/src/lexer.rs
index 499f762..2a7e44b 100644
--- a/src/lexer.rs
+++ b/src/lexer.rs
@@ -1,6 +1,10 @@
 use nom;
 
 use core::Const;
+use core::BuiltinType;
+use core::BuiltinType::*;
+use core::BuiltinValue;
+use core::BuiltinValue::*;
 
 #[derive(Debug, PartialEq, Eq)]
 pub enum Keyword {
@@ -19,24 +23,8 @@ pub enum ListLike {
 
 #[derive(Debug, PartialEq, Eq)]
 pub enum Builtin {
-    Natural,
-    NaturalFold,
-    NaturalBuild,
-    NaturalIsZero,
-    NaturalEven,
-    NaturalOdd,
-    Integer,
-    Double,
-    Text,
-    ListBuild,
-    ListFold,
-    ListLength,
-    ListHead,
-    ListLast,
-    ListIndexed,
-    ListReverse,
-    OptionalFold,
-    Bool,
+    Type(BuiltinType),
+    Value(BuiltinValue),
 }
 
 #[derive(Debug, PartialEq, Eq)]
@@ -221,24 +209,24 @@ named!(list_like<&str, ListLike>, alt!(
 ));
 
 named!(builtin<&str, Builtin>, alt!(
-    value!(Builtin::NaturalFold, ident_tag!("Natural/fold")) |
-    value!(Builtin::NaturalBuild, ident_tag!("Natural/build")) |
-    value!(Builtin::NaturalIsZero, ident_tag!("Natural/isZero")) |
-    value!(Builtin::NaturalEven, ident_tag!("Natural/even")) |
-    value!(Builtin::NaturalOdd, ident_tag!("Natural/odd")) |
-    value!(Builtin::Natural, ident_tag!("Natural")) |
-    value!(Builtin::Integer, ident_tag!("Integer")) |
-    value!(Builtin::Double, ident_tag!("Double")) |
-    value!(Builtin::Text, ident_tag!("Text")) |
-    value!(Builtin::ListBuild, ident_tag!("List/build")) |
-    value!(Builtin::ListFold, ident_tag!("List/fold")) |
-    value!(Builtin::ListLength, ident_tag!("List/length")) |
-    value!(Builtin::ListHead, ident_tag!("List/head")) |
-    value!(Builtin::ListLast, ident_tag!("List/last")) |
-    value!(Builtin::ListIndexed, ident_tag!("List/indexed")) |
-    value!(Builtin::ListReverse, ident_tag!("List/reverse")) |
-    value!(Builtin::OptionalFold, ident_tag!("Optional/fold")) |
-    value!(Builtin::Bool, ident_tag!("Bool"))
+    value!(Builtin::Value(NaturalFold), ident_tag!("Natural/fold")) |
+    value!(Builtin::Value(NaturalBuild), ident_tag!("Natural/build")) |
+    value!(Builtin::Value(NaturalIsZero), ident_tag!("Natural/isZero")) |
+    value!(Builtin::Value(NaturalEven), ident_tag!("Natural/even")) |
+    value!(Builtin::Value(NaturalOdd), ident_tag!("Natural/odd")) |
+    value!(Builtin::Type(Natural), ident_tag!("Natural")) |
+    value!(Builtin::Type(Integer), ident_tag!("Integer")) |
+    value!(Builtin::Type(Double), ident_tag!("Double")) |
+    value!(Builtin::Type(Text), ident_tag!("Text")) |
+    value!(Builtin::Value(ListBuild), ident_tag!("List/build")) |
+    value!(Builtin::Value(ListFold), ident_tag!("List/fold")) |
+    value!(Builtin::Value(ListLength), ident_tag!("List/length")) |
+    value!(Builtin::Value(ListHead), ident_tag!("List/head")) |
+    value!(Builtin::Value(ListLast), ident_tag!("List/last")) |
+    value!(Builtin::Value(ListIndexed), ident_tag!("List/indexed")) |
+    value!(Builtin::Value(ListReverse), ident_tag!("List/reverse")) |
+    value!(Builtin::Value(OptionalFold), ident_tag!("Optional/fold")) |
+    value!(Builtin::Type(Bool), ident_tag!("Bool"))
 ));
 
 named!(token<&str, Tok>, alt!(
@@ -371,7 +359,7 @@ fn test_lex() {
                     ParenL,
                     Identifier("b"),
                     Ascription,
-                    Builtin(self::Builtin::Bool),
+                    Builtin(self::Builtin::Type(::core::BuiltinType::Bool)),
                     ParenR,
                     Arrow,
                     Identifier("b"),
diff --git a/src/typecheck.rs b/src/typecheck.rs
index 36d75e4..3bd80ae 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -5,8 +5,10 @@ use context::Context;
 use core;
 use core::{Expr, V, X, bx, normalize, shift, subst};
 use core::{pi, app};
-use core::Expr::*;
+use core::BuiltinType::*;
+use core::BuiltinValue::*;
 use core::Const::*;
+use core::Expr::*;
 
 use self::TypeMessage::*;
 
@@ -67,13 +69,7 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
             }
             (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
                 if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
-            (&Bool, &Bool) => true,
-            (&Natural, &Natural) => true,
-            (&Integer, &Integer) => true,
-            (&Double, &Double) => true,
-            (&Text, &Text) => true,
-            (&List, &List) => true,
-            (&Optional, &Optional) => true,
+            (&BuiltinType(a), &BuiltinType(b)) => a == b,
             (&Record(ref _ktsL0), &Record(ref _ktsR0)) => unimplemented!(),
             /*
                 let loop ((kL, tL):ktsL) ((kR, tR):ktsR)
@@ -219,22 +215,25 @@ type_with ctx e@(Annot x t       ) = do
             let nf_t' = Dhall.Core.normalize t'
             Left (TypeError ctx e (AnnotMismatch x nf_t nf_t'))
 */
-        &Bool => Ok(Const(Type)),
-        &BoolLit(_) => Ok(Bool),
+        &BuiltinType(t) => Ok(match t {
+            List | Optional => pi("_", Const(Type), Const(Type)),
+            Bool | Natural | Integer | Double | Text => Const(Type),
+        }),
+        &BoolLit(_) => Ok(BuiltinType(Bool)),
         &BoolAnd(ref l, ref r) => {
             let tl = normalize(type_with(ctx, l)?);
             match tl {
-                Bool => {}
+                BuiltinType(Bool) => {}
                 _    => return Err(TypeError::new(ctx, e, CantAnd((**l).clone(), tl))),
             }
 
             let tr = normalize(type_with(ctx, r)?);
             match tr {
-                Bool => {}
+                BuiltinType(Bool) => {}
                 _    => return Err(TypeError::new(ctx, e, CantAnd((**r).clone(), tr))),
             }
 
-            Ok(Bool)
+            Ok(BuiltinType(Bool))
         }
     /*
 type_with ctx e@(BoolOr  l r     ) = do
@@ -295,8 +294,7 @@ type_with ctx e@(BoolIf x y z    ) = do
         else Left (TypeError ctx e (IfBranchMismatch y z ty tz))
     return ty
         */
-    &Natural => Ok(Const(Type)),
-    &NaturalLit(_) => Ok(Natural),
+    &NaturalLit(_) => Ok(BuiltinType(Natural)),
     /*
 type_with _      NaturalFold       = do
     return
@@ -312,9 +310,9 @@ type_with _      NaturalBuild      = do
                     (Pi "zero" "natural" "natural") ) )
             Natural )
         */
-    &NaturalIsZero => Ok(pi("_", Natural, Bool)),
-    &NaturalEven => Ok(pi("_", Natural, Bool)),
-    &NaturalOdd => Ok(pi("_", Natural, Bool)),
+    &BuiltinValue(NaturalIsZero) => Ok(pi("_", Natural, Bool)),
+    &BuiltinValue(NaturalEven) => Ok(pi("_", Natural, Bool)),
+    &BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)),
     /*
 type_with ctx e@(NaturalPlus  l r) = do
     tl <- fmap Dhall.Core.normalize (type_with ctx l)
@@ -339,12 +337,9 @@ type_with ctx e@(NaturalTimes l r) = do
         _       -> Left (TypeError ctx e (CantMultiply r tr))
     return Natural
     */
-    &Integer => Ok(Const(Type)),
-    &IntegerLit(_) => Ok(Integer),
-    &Double => Ok(Const(Type)),
-    &DoubleLit(_) => Ok(Double),
-    &Text => Ok(Const(Type)),
-    &TextLit(_) => Ok(Text),
+    &IntegerLit(_) => Ok(BuiltinType(Integer)),
+    &DoubleLit(_) => Ok(BuiltinType(Double)),
+    &TextLit(_) => Ok(BuiltinType(Text)),
     /*
 type_with ctx e@(TextAppend l r  ) = do
     tl <- fmap Dhall.Core.normalize (type_with ctx l)
@@ -358,7 +353,6 @@ type_with ctx e@(TextAppend l r  ) = do
         _    -> Left (TypeError ctx e (CantTextAppend r tr))
     return Text
     */
-    &List => Ok(pi("_", Const(Type), Const(Type))),
     /*
 type_with ctx e@(ListLit t xs    ) = do
     s <- fmap Dhall.Core.normalize (type_with ctx t)
@@ -375,24 +369,24 @@ type_with ctx e@(ListLit t xs    ) = do
                 Left (TypeError ctx e (InvalidListElement i nf_t x nf_t')) )
     return (App List t)
                 */
-    &ListBuild =>
+    &BuiltinValue(ListBuild) =>
         Ok(pi("a", Const(Type),
             pi("_",
                 pi("list", Const(Type),
                     pi("cons", pi("_", "a", pi("_", "list", "list")),
                         pi("nil", "list", "list"))),
                 app(List, "a")))),
-    &ListFold =>
+    &BuiltinValue(ListFold) =>
         Ok(pi("a", Const(Type),
             pi("_", app(List, "a"),
                 pi("list", Const(Type),
                     pi("cons", pi("_", "a", pi("_", "list", "list")),
                         pi("nil", "list", "list")))))),
-    &ListLength =>
+    &BuiltinValue(ListLength) =>
         Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
-    &ListHead =>
+    &BuiltinValue(ListHead) =>
         Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
-    &ListLast =>
+    &BuiltinValue(ListLast) =>
         Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
         /*
 type_with _      ListIndexed       = do