diff options
author | Nadrieril | 2019-03-03 00:08:57 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-03 00:26:23 +0100 |
commit | b7ce3e60770be41d8ccf773541c586c75d2a4e38 (patch) | |
tree | 19fe6bcc070358f2d46a75f5df72adeaba4b08f8 /dhall | |
parent | 54d3f23e68bf6e769d8a96e40a2b0c4426e38507 (diff) |
Merge builtins in a single enum
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/core.rs | 104 | ||||
-rw-r--r-- | dhall/src/grammar.lalrpop | 9 | ||||
-rw-r--r-- | dhall/src/grammar_util.rs | 7 | ||||
-rw-r--r-- | dhall/src/lexer.rs | 52 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 65 |
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)?); |