diff options
author | Nadrieril | 2020-02-14 18:55:27 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-14 18:55:27 +0000 |
commit | 51cf6a28fa56031dbeae0ff378f0ef84eff7fd3e (patch) | |
tree | ff452de7a7b4c15b18b1aa43b05a5afafdd5ef58 /dhall | |
parent | 350d1cf7d9c114b1334b2743071b0b99ea64c1ec (diff) |
Oops
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 12 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 18 |
2 files changed, 14 insertions, 16 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index ac15ac5..c7b8009 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,3 +1,4 @@ +use crate::error::TypeError; use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value}; use crate::syntax::{Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; @@ -25,16 +26,13 @@ impl TyExpr { pub fn ty(&self) -> &Type { &self.ty } - pub fn get_type_tyexpr(&self, env: &TyEnv) -> TyExpr { - self.ty() - .to_hir(env.as_varenv()) - .typecheck(env) - .expect("Internal type error") + pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> { + Ok(self.ty().to_hir(env.as_varenv()).typecheck(env)?) } /// Get the kind (the type of the type) of this value // TODO: avoid recomputing so much - pub fn get_kind(&self, env: &TyEnv) -> Option<Const> { - self.get_type_tyexpr(env).ty().as_const() + pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> { + Ok(self.get_type_tyexpr(env)?.ty().as_const()) } pub fn to_hir(&self) -> Hir { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index b3c9353..377b97e 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -53,7 +53,7 @@ fn type_one_layer( ExprKind::Lam(binder, annot, body) => { let body_ty = body.get_type_tyexpr( &env.insert_type(&binder.clone(), annot.eval(env)), - ); + )?; let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env) } @@ -139,7 +139,7 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - if x.get_kind(env) != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidListType"); } @@ -147,7 +147,7 @@ fn type_one_layer( Value::from_builtin(Builtin::List).app(t) } ExprKind::SomeLit(x) => { - if x.get_kind(env) != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } @@ -167,7 +167,7 @@ fn type_one_layer( }; // Check that the fields have a valid kind - match v.get_kind(env) { + match v.get_kind(env)? { Some(_) => {} None => return span_err("InvalidFieldType"), } @@ -315,7 +315,7 @@ fn type_one_layer( if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.get_kind(env) != Some(Const::Type) { + if y.get_kind(env)? != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.ty() != z.ty() { @@ -350,8 +350,8 @@ fn type_one_layer( ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - x.get_type_tyexpr(env), - y.get_type_tyexpr(env), + x.get_type_tyexpr(env)?, + y.get_type_tyexpr(env)?, ); type_one_layer(env, ekind, None, span.clone())?.eval(env) } @@ -413,7 +413,7 @@ fn type_one_layer( if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } - if l.get_kind(env) != Some(Const::Type) { + if l.get_kind(env)? != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -582,7 +582,7 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { - if record.get_kind(env) != Some(Const::Type) { + if record.get_kind(env)? != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); |