diff options
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/core/value.rs | 7 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 43 |
2 files changed, 29 insertions, 21 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 0af7c8c..5367c86 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -9,7 +9,7 @@ use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; -use crate::phase::typecheck::type_of_const; +use crate::phase::typecheck::const_to_value; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] @@ -110,10 +110,7 @@ impl Value { Value::from_valuef_and_type(v, Value::from_const(Const::Type)) } pub(crate) fn from_const(c: Const) -> Self { - match type_of_const(c) { - Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => Value::from_valuef_untyped(ValueF::Const(c)), - } + const_to_value(c) } pub fn const_type() -> Self { Value::from_const(Const::Type) diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index c47eb78..1ea87d1 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -129,16 +129,24 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> { +fn type_of_const(c: Const) -> Result<Value, TypeError> { match c { - Const::Type => Ok(Value::from_const(Const::Kind)), - Const::Kind => Ok(Value::from_const(Const::Sort)), + Const::Type => Ok(const_to_value(Const::Kind)), + Const::Kind => Ok(const_to_value(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } } } +pub(crate) fn const_to_value(c: Const) -> Value { + let v = ValueF::Const(c); + match type_of_const(c) { + Ok(t) => Value::from_valuef_and_type(v, t), + Err(_) => Value::from_valuef_untyped(v), + } +} + // Ad-hoc macro to help construct the types of builtins macro_rules! make_type { (Type) => { ExprF::Const(Const::Type) }; @@ -280,9 +288,12 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { } } -// TODO: this can't fail in practise -pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> { - type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) +pub(crate) fn builtin_to_value(b: Builtin) -> Value { + let ctx = TypecheckContext::new(); + Value::from_valuef_and_type( + ValueF::PartialExpr(ExprF::Builtin(b)), + type_with(&ctx, rc(type_of_builtin(b))).unwrap(), + ) } /// Type-check an expression and return the expression alongside its type if type-checking @@ -401,7 +412,7 @@ fn type_last_layer( RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { - if x.get_type()?.as_ref() != &builtin_to_type(Bool)? { + if x.get_type()?.as_ref() != &builtin_to_value(Bool) { return mkerr(InvalidPredicate(x.clone())); } @@ -523,14 +534,14 @@ fn type_last_layer( // )), } } - Const(c) => RetWhole(Value::from_const(*c)), - Builtin(b) => RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?), - BoolLit(_) => RetTypeOnly(builtin_to_type(Bool)?), - NaturalLit(_) => RetTypeOnly(builtin_to_type(Natural)?), - IntegerLit(_) => RetTypeOnly(builtin_to_type(Integer)?), - DoubleLit(_) => RetTypeOnly(builtin_to_type(Double)?), + Const(c) => RetWhole(const_to_value(*c)), + Builtin(b) => RetWhole(builtin_to_value(*b)), + BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)), + NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)), + IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)), + DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)), TextLit(interpolated) => { - let text_type = builtin_to_type(Text)?; + let text_type = builtin_to_value(Text); for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { @@ -665,7 +676,7 @@ fn type_last_layer( RetTypeOnly(Value::from_const(Type)) } BinOp(o, l, r) => { - let t = builtin_to_type(match o { + let t = builtin_to_value(match o { BoolAnd => Bool, BoolOr => Bool, BoolEQ => Bool, @@ -679,7 +690,7 @@ fn type_last_layer( RecursiveRecordTypeMerge => unreachable!(), ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"), Equivalence => unreachable!(), - })?; + }); if l.get_type()?.as_ref() != &t { return mkerr(BinOpTypeMismatch(*o, l.clone())); |