summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/core.rs166
-rw-r--r--src/grammar.lalrpop5
-rw-r--r--src/grammar_util.rs20
-rw-r--r--src/lexer.rs62
-rw-r--r--src/typecheck.rs54
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:11:25 +0000