summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core.rs104
-rw-r--r--dhall/src/grammar.lalrpop9
-rw-r--r--dhall/src/grammar_util.rs7
-rw-r--r--dhall/src/lexer.rs52
-rw-r--r--dhall/src/typecheck.rs65
5 files changed, 103 insertions, 134 deletions
diff --git a/dhall/src/core.rs b/dhall/src/core.rs
index ccaf0f5..c5b6d86 100644
--- a/dhall/src/core.rs
+++ b/dhall/src/core.rs
@@ -126,10 +126,8 @@ 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>>),
- /// Built-in types
- BuiltinType(BuiltinType),
- /// Built-in function values
- BuiltinValue(BuiltinValue),
+ /// Built-in values
+ Builtin(Builtin),
/// `BoolLit b ~ b`
BoolLit(bool),
/// `BoolAnd x y ~ x && y`
@@ -183,9 +181,9 @@ pub enum Expr<'i, S, A> {
FailedParse(String, Vec<Expr<'i, S, A>>),
}
-/// Built-in types
+/// Built-ins
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BuiltinType {
+pub enum Builtin {
/// `Bool ~ Bool`
Bool,
/// `Natural ~ Natural`
@@ -200,11 +198,6 @@ pub enum BuiltinType {
List,
/// `Optional ~ Optional`
Optional,
-}
-
-/// Built-in function values
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BuiltinValue {
/// `NaturalFold ~ Natural/fold`
NaturalFold,
/// `NaturalBuild ~ Natural/build`
@@ -246,15 +239,9 @@ 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)
+impl<'i, S, A> From<Builtin> for Expr<'i, S, A> {
+ fn from(t: Builtin) -> Self {
+ Expr::Builtin(t)
}
}
@@ -406,8 +393,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
match self {
&Var(a) => a.fmt(f),
&Const(k) => k.fmt(f),
- &BuiltinType(t) => t.fmt(f),
- &BuiltinValue(v) => v.fmt(f),
+ &Builtin(v) => v.fmt(f),
&BoolLit(true) => f.write_str("True"),
&BoolLit(false) => f.write_str("False"),
&IntegerLit(a) => a.fmt(f),
@@ -459,29 +445,30 @@ impl Display for Const {
}
}
-impl Display for BuiltinType {
- fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- <Self as fmt::Debug>::fmt(self, f)
- }
-}
-
-impl Display for BuiltinValue {
+impl Display for Builtin {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- use crate::BuiltinValue::*;
+ use crate::Builtin::*;
f.write_str(match *self {
+ Bool => "Bool",
+ Natural => "Natural",
+ Integer => "Integer",
+ Double => "Double",
+ Text => "Text",
+ List => "List",
+ Optional => "Optional",
+ NaturalFold => "Natural/fold",
+ NaturalBuild => "Natural/build",
+ NaturalIsZero => "Natural/isZero",
+ NaturalEven => "Natural/even",
+ NaturalOdd => "Natural/odd",
+ NaturalShow => "Natural/show",
ListBuild => "List/build",
ListFold => "List/fold",
+ ListLength => "List/length",
ListHead => "List/head",
- ListIndexed => "List/indexed",
ListLast => "List/last",
- ListLength => "List/length",
+ ListIndexed => "List/indexed",
ListReverse => "List/reverse",
- NaturalBuild => "Natural/build",
- NaturalEven => "Natural/even",
- NaturalFold => "Natural/fold",
- NaturalIsZero => "Natural/isZero",
- NaturalOdd => "Natural/odd",
- NaturalShow => "Natural/show",
OptionalFold => "Optional/fold",
})
}
@@ -658,8 +645,7 @@ pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i,
Let(f, mt2, bx(r2), bx(e2))
}
Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b),
- BuiltinType(t) => BuiltinType(t),
- BuiltinValue(v) => BuiltinValue(v),
+ Builtin(v) => Builtin(v),
BoolLit(a) => BoolLit(a),
BoolAnd(ref a, ref b) => shift_op2(BoolAnd, d, v, a, b),
BoolOr(ref a, ref b) => shift_op2(BoolOr, d, v, a, b),
@@ -756,8 +742,7 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E
Let(f, mt2, bx(r2), bx(b2))
}
Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b),
- BuiltinType(t) => BuiltinType(t),
- BuiltinValue(v) => BuiltinValue(v),
+ Builtin(v) => Builtin(v),
BoolLit(a) => BoolLit(a),
BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b),
BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b),
@@ -829,7 +814,7 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
T: Clone + fmt::Debug,
A: Clone + fmt::Debug,
{
- use crate::BuiltinValue::*;
+ use crate::Builtin::*;
use crate::Expr::*;
match *e {
Const(k) => Const(k),
@@ -854,12 +839,12 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
}
f2 => match (f2, normalize::<S, T, A>(a)) {
// fold/build fusion for `List`
- (App(box BuiltinValue(ListBuild), _), App(box App(box BuiltinValue(ListFold), _), box e2)) |
- (App(box BuiltinValue(ListFold), _), App(box App(box BuiltinValue(ListBuild), _), box e2)) |
+ (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
+ (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
// fold/build fusion for `Natural`
- (BuiltinValue(NaturalBuild), App(box BuiltinValue(NaturalFold), box e2)) |
- (BuiltinValue(NaturalFold), App(box BuiltinValue(NaturalBuild), box e2)) => normalize(&e2),
+ (Builtin(NaturalBuild), App(box Builtin(NaturalFold), box e2)) |
+ (Builtin(NaturalFold), App(box Builtin(NaturalBuild), box e2)) => normalize(&e2),
/*
App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
@@ -885,14 +870,14 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
go (Var "Zero") = True
go _ = False
*/
- (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
- (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
- (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
- (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
- (App(f@box BuiltinValue(ListBuild), box t), k) => {
+ (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
+ (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
+ (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
+ (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
+ (App(f@box Builtin(ListBuild), box t), k) => {
let labeled =
normalize::<_, T, _>(&app(app(app(k.clone(), app(
- BuiltinType(self::BuiltinType::List), t.clone())), "Cons"), "Nil"));
+ Builtin(self::Builtin::List), t.clone())), "Cons"), "Nil"));
fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
where S: Clone, A: Clone
@@ -922,20 +907,20 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
app(App(f, bx(t)), k)
}
}
- (App(box App(box App(box App(box BuiltinValue(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
+ (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
App(bx(App(cons.clone(), bx(y))), bx(ys))
);
normalize(&e2)
}
(App(f, x_), ListLit(t, ys)) => match *f {
- BuiltinValue(ListLength) =>
+ Builtin(ListLength) =>
NaturalLit(ys.len()),
- BuiltinValue(ListHead) =>
+ Builtin(ListHead) =>
normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
- BuiltinValue(ListLast) =>
+ Builtin(ListLast) =>
normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
- BuiltinValue(ListReverse) => {
+ Builtin(ListReverse) => {
let mut xs = ys;
xs.reverse();
normalize(&ListLit(t, xs))
@@ -972,8 +957,7 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
normalize(&b3)
}
Annot(ref x, _) => normalize(x),
- BuiltinType(t) => BuiltinType(t),
- BuiltinValue(v) => BuiltinValue(v),
+ Builtin(v) => Builtin(v),
BoolLit(b) => BoolLit(b),
BoolAnd(ref x, ref y) => {
with_binop(BoolAnd, Expr::bool_lit,
diff --git a/dhall/src/grammar.lalrpop b/dhall/src/grammar.lalrpop
index 150961f..250a45e 100644
--- a/dhall/src/grammar.lalrpop
+++ b/dhall/src/grammar.lalrpop
@@ -5,7 +5,8 @@ use std::iter::FromIterator;
use crate::core;
use crate::core::bx;
use crate::core::Expr::*;
-use crate::core::BuiltinType::*;
+use crate::core::Builtin;
+use crate::core::Builtin::*;
use crate::grammar_util::*;
use crate::lexer::*;
@@ -120,9 +121,9 @@ ExprF: BoxExpr<'input> = {
Text => bx(TextLit(<>)),
Label => bx(Var(core::V(<>, 0))), // FIXME support var@n syntax
Const => bx(Const(<>)),
- List => bx(BuiltinType(List)),
- Optional => bx(BuiltinType(Optional)),
- Builtin => bx(builtin_expr(<>)),
+ List => bx(Builtin(List)),
+ Optional => bx(Builtin(Optional)),
+ Builtin => bx(Builtin(<>)),
Bool => bx(BoolLit(<>)),
Record,
RecordLit,
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
index c546a13..2250acd 100644
--- a/dhall/src/grammar_util.rs
+++ b/dhall/src/grammar_util.rs
@@ -1,14 +1,7 @@
use crate::core::{Expr, X};
-use crate::lexer::Builtin;
pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
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::Type(t) => Expr::BuiltinType(t),
- Builtin::Value(v) => Expr::BuiltinValue(v),
- }
-}
diff --git a/dhall/src/lexer.rs b/dhall/src/lexer.rs
index 5b4dcaa..b5cbe6b 100644
--- a/dhall/src/lexer.rs
+++ b/dhall/src/lexer.rs
@@ -1,10 +1,8 @@
use nom::*;
use crate::core::Const;
-use crate::core::BuiltinType;
-use crate::core::BuiltinType::*;
-use crate::core::BuiltinValue;
-use crate::core::BuiltinValue::*;
+use crate::core::Builtin;
+use crate::core::Builtin::*;
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Keyword {
@@ -22,12 +20,6 @@ pub enum ListLike {
}
#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Builtin {
- Type(BuiltinType),
- Value(BuiltinValue),
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Tok<'i> {
Identifier(&'i str),
Keyword(Keyword),
@@ -209,25 +201,25 @@ named!(list_like<&str, ListLike>, alt!(
));
named!(builtin<&str, Builtin>, alt!(
- 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::Value(NaturalShow), ident_tag!("Natural/show")) |
- 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"))
+ value!(NaturalFold, ident_tag!("Natural/fold")) |
+ value!(NaturalBuild, ident_tag!("Natural/build")) |
+ value!(NaturalIsZero, ident_tag!("Natural/isZero")) |
+ value!(NaturalEven, ident_tag!("Natural/even")) |
+ value!(NaturalOdd, ident_tag!("Natural/odd")) |
+ value!(NaturalShow, ident_tag!("Natural/show")) |
+ value!(Natural, ident_tag!("Natural")) |
+ value!(Integer, ident_tag!("Integer")) |
+ value!(Double, ident_tag!("Double")) |
+ value!(Text, ident_tag!("Text")) |
+ value!(ListBuild, ident_tag!("List/build")) |
+ value!(ListFold, ident_tag!("List/fold")) |
+ value!(ListLength, ident_tag!("List/length")) |
+ value!(ListHead, ident_tag!("List/head")) |
+ value!(ListLast, ident_tag!("List/last")) |
+ value!(ListIndexed, ident_tag!("List/indexed")) |
+ value!(ListReverse, ident_tag!("List/reverse")) |
+ value!(OptionalFold, ident_tag!("Optional/fold")) |
+ value!(Bool, ident_tag!("Bool"))
));
named!(token<&str, Tok>, alt!(
@@ -360,7 +352,7 @@ fn test_lex() {
ParenL,
Identifier("b"),
Ascription,
- Builtin(self::Builtin::Type(crate::core::BuiltinType::Bool)),
+ Builtin(crate::core::Builtin::Bool),
ParenR,
Arrow,
Identifier("b"),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 62ff7d2..51ea848 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -7,8 +7,7 @@ use crate::context::Context;
use crate::core;
use crate::core::{Expr, V, X, bx, normalize, shift, subst};
use crate::core::{pi, app};
-use crate::core::BuiltinType::*;
-use crate::core::BuiltinValue::*;
+use crate::core::Builtin::*;
use crate::core::Const::*;
use crate::core::Expr::*;
@@ -71,7 +70,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 },
- (&BuiltinType(a), &BuiltinType(b)) => a == b,
+ (&Builtin(a), &Builtin(b)) => a == b,
(&Record(ref ktsL0), &Record(ref ktsR0)) => {
if ktsL0.len() != ktsR0.len() {
return false;
@@ -130,7 +129,7 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
e: &Expr<'i, S, X>,
- t: core::BuiltinType,
+ t: core::Builtin,
ef: EF,
l: &Expr<'i, S, X>,
r: &Expr<'i, S, X>)
@@ -140,17 +139,17 @@ fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
{
let tl = normalize(&type_with(ctx, l)?);
match tl {
- BuiltinType(lt) if lt == t => {}
+ Builtin(lt) if lt == t => {}
_ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))),
}
let tr = normalize(&type_with(ctx, r)?);
match tr {
- BuiltinType(rt) if rt == t => {}
+ Builtin(rt) if rt == t => {}
_ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))),
}
- Ok(BuiltinType(t))
+ Ok(Builtin(t))
}
/// Type-check an expression and return the expression'i type if type-checking
@@ -265,11 +264,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
}
}
- BuiltinType(t) => Ok(match t {
- List | Optional => pi("_", Const(Type), Const(Type)),
- Bool | Natural | Integer | Double | Text => Const(Type),
- }),
- BoolLit(_) => Ok(BuiltinType(Bool)),
+ BoolLit(_) => Ok(Builtin(Bool)),
BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r),
BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r),
BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r),
@@ -277,7 +272,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
BoolIf(ref x, ref y, ref z) => {
let tx = normalize(&type_with(ctx, x)?);
match tx {
- BuiltinType(Bool) => {}
+ Builtin(Bool) => {}
_ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
}
let ty = normalize(&type_with(ctx, y)?);
@@ -299,26 +294,26 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
}
Ok(ty)
}
- NaturalLit(_) => Ok(BuiltinType(Natural)),
- BuiltinValue(NaturalFold) =>
+ NaturalLit(_) => Ok(Builtin(Natural)),
+ Builtin(NaturalFold) =>
Ok(pi("_", Natural,
pi("natural", Const(Type),
pi("succ", pi("_", "natural", "natural"),
pi("zero", "natural", "natural"))))),
- BuiltinValue(NaturalBuild) =>
+ Builtin(NaturalBuild) =>
Ok(pi("_",
pi("natural", Const(Type),
pi("succ", pi("_", "natural", "natural"),
pi("zero", "natural", "natural"))),
Natural)),
- BuiltinValue(NaturalIsZero) |
- BuiltinValue(NaturalEven) |
- BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)),
+ Builtin(NaturalIsZero) |
+ Builtin(NaturalEven) |
+ Builtin(NaturalOdd) => Ok(pi("_", Natural, Bool)),
NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
- IntegerLit(_) => Ok(BuiltinType(Integer)),
- DoubleLit(_) => Ok(BuiltinType(Double)),
- TextLit(_) => Ok(BuiltinType(Text)),
+ IntegerLit(_) => Ok(Builtin(Integer)),
+ DoubleLit(_) => Ok(Builtin(Double)),
+ TextLit(_) => Ok(Builtin(Text)),
TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
ListLit(ref t, ref xs) => {
let s = normalize::<_, S, _>(&type_with(ctx, t)?);
@@ -334,33 +329,33 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
}
}
- Ok(App(bx(BuiltinType(List)), t.clone()))
+ Ok(App(bx(Builtin(List)), t.clone()))
}
- BuiltinValue(ListBuild) =>
+ Builtin(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")))),
- BuiltinValue(ListFold) =>
+ Builtin(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")))))),
- BuiltinValue(ListLength) =>
+ Builtin(ListLength) =>
Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
- BuiltinValue(ListHead) |
- BuiltinValue(ListLast) =>
+ Builtin(ListHead) |
+ Builtin(ListLast) =>
Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
- BuiltinValue(ListIndexed) => {
+ Builtin(ListIndexed) => {
let mut m = BTreeMap::new();
- m.insert("index", BuiltinType(Natural));
+ m.insert("index", Builtin(Natural));
m.insert("value", Expr::from("a"));
Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
}
- BuiltinValue(ListReverse) =>
+ Builtin(ListReverse) =>
Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
OptionalLit(ref t, ref xs) => {
let s = normalize::<_, S, _>(&type_with(ctx, t)?);
@@ -380,14 +375,18 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
}
}
- Ok(App(bx(BuiltinType(Optional)), t.clone()))
+ Ok(App(bx(Builtin(Optional)), t.clone()))
}
- BuiltinValue(OptionalFold) =>
+ Builtin(OptionalFold) =>
Ok(pi("a", Const(Type),
pi("_", app(Optional, "a"),
pi("optional", Const(Type),
pi("just", pi("_", "a", "optional"),
pi("nothing", "optional", "optional")))))),
+ Builtin(List) | Builtin(Optional) =>
+ Ok(pi("_", Const(Type), Const(Type))),
+ Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) =>
+ Ok(Const(Type)),
Record(ref kts) => {
for (k, t) in kts {
let s = normalize::<S, S, X>(&type_with(ctx, t)?);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 01:51:16 +0000