From aa867b21f57f9bef2ec2b9d8450736f9111189ee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:44:40 +0000 Subject: Introduce proper Type struct --- dhall/src/semantics/tck/tyexpr.rs | 54 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 50 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/tck/tyexpr.rs') 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 { + 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) -> Value { self.as_hir().eval(env.into()) } + /// Evaluate to a Type. + pub fn eval_to_type(&self, env: impl Into) -> 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 for Type { + fn from(x: Value) -> Type { + Type { val: x } + } +} -- cgit v1.2.3