From 82d50e8734e0caad0b34ae32493ab831e7ec7fae Mon Sep 17 00:00:00 2001 From: NanoTech Date: Thu, 8 Dec 2016 14:59:02 -0600 Subject: Seperate built-in types and functions from Expr --- src/core.rs | 166 ++++++++++++++++++++++++---------------------------- src/grammar.lalrpop | 5 +- src/grammar_util.rs | 20 +------ src/lexer.rs | 62 ++++++++------------ src/typecheck.rs | 54 ++++++++--------- 5 files changed, 130 insertions(+), 177 deletions(-) (limited to 'src') 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>, Box>), /// `Annot x t ~ x : t` Annot(Box>, Box>), - /// `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>, Box>), /// `BoolIf x y z ~ if x then y else z` BoolIf(Box>, Box>, Box>), - /// `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>, Box>), /// `NaturalTimes x y ~ x * y` NaturalTimes(Box>, Box>), - /// `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>, Box>), - /// `List ~ List` - List, /// `ListLit t [x, y, z] ~ [x, y, z] : List t` ListLit(Box>, Vec>), - /// `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>, Vec>), - /// `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(&self) -> Option> { - 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::().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 for Expr<'i, S, A> { + fn from(t: BuiltinType) -> Self { + Expr::BuiltinType(t) + } +} + +impl<'i, S, A> From 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>, @@ -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(e: Expr) -> Expr 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(e: Expr) -> Expr 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(e: Expr) -> Expr 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> 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(eL0: &Expr, eR0: &Expr) -> 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 -- cgit v1.2.3