summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck/tyexpr.rs
diff options
context:
space:
mode:
authorNadrieril2020-02-15 19:44:40 +0000
committerNadrieril2020-02-15 19:59:52 +0000
commitaa867b21f57f9bef2ec2b9d8450736f9111189ee (patch)
treeeab9042a53ceed53abd7982a83fd4d76cd869572 /dhall/src/semantics/tck/tyexpr.rs
parent5057144ed99bc4e1a76a0840dd39fc1bd862665c (diff)
Introduce proper Type struct
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs54
1 files changed, 50 insertions, 4 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index dfb4397..4999899 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,17 +1,53 @@
use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
-use crate::syntax::{Const, Span};
+use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
use crate::{NormalizedExpr, ToExprOptions};
-pub(crate) type Type = Value;
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+ val: Value,
+}
-// A hir expression plus its inferred type.
+/// A hir expression plus its inferred type.
#[derive(Debug, Clone)]
pub(crate) struct TyExpr {
hir: Hir,
ty: Type,
}
+impl Type {
+ pub fn from_const(c: Const) -> Self {
+ Value::from_const(c).into()
+ }
+ pub fn from_builtin(b: Builtin) -> Self {
+ Value::from_builtin(b).into()
+ }
+
+ pub fn to_value(&self) -> Value {
+ self.val.clone()
+ }
+ pub fn as_value(&self) -> &Value {
+ &self.val
+ }
+ pub fn into_value(self) -> Value {
+ self.val
+ }
+ pub fn as_const(&self) -> Option<Const> {
+ self.val.as_const()
+ }
+ pub fn kind(&self) -> &ValueKind {
+ self.val.kind()
+ }
+
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ self.val.to_hir(venv)
+ }
+ pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+ }
+}
+
impl TyExpr {
pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
TyExpr {
@@ -52,6 +88,10 @@ impl TyExpr {
pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
self.as_hir().eval(env.into())
}
+ /// Evaluate to a Type.
+ pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
+ self.eval(env).into()
+ }
/// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
pub fn eval_closed_expr(&self) -> Value {
@@ -64,3 +104,9 @@ impl TyExpr {
val
}
}
+
+impl From<Value> for Type {
+ fn from(x: Value) -> Type {
+ Type { val: x }
+ }
+}