From 2f65c02a995f6b6d4c755197fc074782f6bb100d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:12:44 +0000 Subject: Rename TyExpr to Tir --- dhall/src/semantics/tck/tir.rs | 193 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 dhall/src/semantics/tck/tir.rs (limited to 'dhall/src/semantics/tck/tir.rs') diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs new file mode 100644 index 0000000..800d1b7 --- /dev/null +++ b/dhall/src/semantics/tck/tir.rs @@ -0,0 +1,193 @@ +use crate::error::{ErrorBuilder, TypeError}; +use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv}; +use crate::syntax::{Builtin, Const, Span}; +use crate::{NormalizedExpr, ToExprOptions}; + +/// The type of a type. 0 is `Type`, 1 is `Kind`, etc... +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)] +pub(crate) struct Universe(u8); + +/// An expression representing a type +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct Type { + val: Value, + univ: Universe, +} + +/// A hir expression plus its inferred type. +/// Stands for "Typed intermediate representation" +#[derive(Debug, Clone)] +pub(crate) struct Tir { + hir: Hir, + ty: Type, +} + +impl Universe { + pub fn from_const(c: Const) -> Self { + Universe(match c { + Const::Type => 0, + Const::Kind => 1, + Const::Sort => 2, + }) + } + pub fn as_const(self) -> Option { + match self.0 { + 0 => Some(Const::Type), + 1 => Some(Const::Kind), + 2 => Some(Const::Sort), + _ => None, + } + } + pub fn next(self) -> Self { + Universe(self.0 + 1) + } +} + +impl Type { + pub fn new(val: Value, univ: Universe) -> Self { + Type { val, univ } + } + /// Creates a new Type and infers its universe by re-typechecking its value. + /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and + /// PiClosure. + pub fn new_infer_universe( + env: &TyEnv, + val: Value, + ) -> Result { + let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const(); + let u = match c { + Some(c) => c.to_universe(), + None => unreachable!( + "internal type error: this is not a type: {:?}", + val + ), + }; + Ok(Type::new(val, u)) + } + pub fn from_const(c: Const) -> Self { + Self::new(Value::from_const(c), c.to_universe().next()) + } + pub fn from_builtin(b: Builtin) -> Self { + use Builtin::*; + match b { + Bool | Natural | Integer | Double | Text => {} + _ => unreachable!("this builtin is not a type: {}", b), + } + + Self::new(Value::from_builtin(b), Universe::from_const(Const::Type)) + } + + /// Get the type of this type + pub fn ty(&self) -> Universe { + self.univ + } + + 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 Tir { + pub fn from_hir(hir: &Hir, ty: Type) -> Self { + Tir { + hir: hir.clone(), + ty, + } + } + + pub fn span(&self) -> Span { + self.as_hir().span() + } + pub fn ty(&self) -> &Type { + &self.ty + } + + pub fn to_hir(&self) -> Hir { + self.as_hir().clone() + } + pub fn as_hir(&self) -> &Hir { + &self.hir + } + /// Converts a closed expression back to the corresponding AST expression. + pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + self.as_hir().to_expr(opts) + } + pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + self.as_hir().to_expr_tyenv(env) + } + + /// Eval the Tir. It will actually get evaluated only as needed on demand. + pub fn eval(&self, env: impl Into) -> Value { + self.as_hir().eval(env.into()) + } + pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> { + if self.ty().as_const().is_none() { + return mkerr( + ErrorBuilder::new(format!( + "Expected a type, found: `{}`", + self.to_expr_tyenv(env), + )) + .span_err( + self.span(), + format!( + "this has type: `{}`", + self.ty().to_expr_tyenv(env) + ), + ) + .help(format!( + "An expression in type position must have type `Type`, \ + `Kind` or `Sort`", + )) + .format(), + ); + } + Ok(()) + } + /// Evaluate to a Type. + pub fn eval_to_type(&self, env: &TyEnv) -> Result { + self.ensure_is_type(env)?; + Ok(Type::new( + self.eval(env), + self.ty() + .as_const() + .expect("case handled in ensure_is_type") + .to_universe(), + )) + } + /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as + /// needed on demand. + pub fn eval_closed_expr(&self) -> Value { + self.eval(NzEnv::new()) + } + /// Eval a closed Tir fully and recursively; + pub fn rec_eval_closed_expr(&self) -> Value { + let val = self.eval_closed_expr(); + val.normalize(); + val + } +} + +impl From for Universe { + fn from(x: Const) -> Universe { + Universe::from_const(x) + } +} -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/tck/tir.rs | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/tck/tir.rs') diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index 800d1b7..908bf8f 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,5 +1,5 @@ use crate::error::{ErrorBuilder, TypeError}; -use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv}; +use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; use crate::syntax::{Builtin, Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; @@ -10,7 +10,7 @@ pub(crate) struct Universe(u8); /// An expression representing a type #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Type { - val: Value, + val: Nir, univ: Universe, } @@ -44,7 +44,7 @@ impl Universe { } impl Type { - pub fn new(val: Value, univ: Universe) -> Self { + pub fn new(val: Nir, univ: Universe) -> Self { Type { val, univ } } /// Creates a new Type and infers its universe by re-typechecking its value. @@ -52,7 +52,7 @@ impl Type { /// PiClosure. pub fn new_infer_universe( env: &TyEnv, - val: Value, + val: Nir, ) -> Result { let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const(); let u = match c { @@ -65,7 +65,7 @@ impl Type { Ok(Type::new(val, u)) } pub fn from_const(c: Const) -> Self { - Self::new(Value::from_const(c), c.to_universe().next()) + Self::new(Nir::from_const(c), c.to_universe().next()) } pub fn from_builtin(b: Builtin) -> Self { use Builtin::*; @@ -74,7 +74,7 @@ impl Type { _ => unreachable!("this builtin is not a type: {}", b), } - Self::new(Value::from_builtin(b), Universe::from_const(Const::Type)) + Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type)) } /// Get the type of this type @@ -82,19 +82,19 @@ impl Type { self.univ } - pub fn to_value(&self) -> Value { + pub fn to_nir(&self) -> Nir { self.val.clone() } - pub fn as_value(&self) -> &Value { + pub fn as_nir(&self) -> &Nir { &self.val } - pub fn into_value(self) -> Value { + pub fn into_nir(self) -> Nir { self.val } pub fn as_const(&self) -> Option { self.val.as_const() } - pub fn kind(&self) -> &ValueKind { + pub fn kind(&self) -> &NirKind { self.val.kind() } @@ -136,7 +136,7 @@ impl Tir { } /// Eval the Tir. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: impl Into) -> Value { + pub fn eval(&self, env: impl Into) -> Nir { self.as_hir().eval(env.into()) } pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> { @@ -175,11 +175,11 @@ impl Tir { } /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as /// needed on demand. - pub fn eval_closed_expr(&self) -> Value { + pub fn eval_closed_expr(&self) -> Nir { self.eval(NzEnv::new()) } /// Eval a closed Tir fully and recursively; - pub fn rec_eval_closed_expr(&self) -> Value { + pub fn rec_eval_closed_expr(&self) -> Nir { let val = self.eval_closed_expr(); val.normalize(); val -- cgit v1.2.3 From ebe43bd6f1fd6feb1564ab9837399de7808b67b5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:39:10 +0000 Subject: Borrow relevant Hir from Tir --- dhall/src/semantics/tck/tir.rs | 30 ++++++------------------------ 1 file changed, 6 insertions(+), 24 deletions(-) (limited to 'dhall/src/semantics/tck/tir.rs') diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index 908bf8f..aeb7bf9 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,7 +1,7 @@ use crate::error::{ErrorBuilder, TypeError}; use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; use crate::syntax::{Builtin, Const, Span}; -use crate::{NormalizedExpr, ToExprOptions}; +use crate::NormalizedExpr; /// The type of a type. 0 is `Type`, 1 is `Kind`, etc... #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)] @@ -17,8 +17,8 @@ pub(crate) struct Type { /// A hir expression plus its inferred type. /// Stands for "Typed intermediate representation" #[derive(Debug, Clone)] -pub(crate) struct Tir { - hir: Hir, +pub(crate) struct Tir<'hir> { + hir: &'hir Hir, ty: Type, } @@ -106,12 +106,9 @@ impl Type { } } -impl Tir { - pub fn from_hir(hir: &Hir, ty: Type) -> Self { - Tir { - hir: hir.clone(), - ty, - } +impl<'hir> Tir<'hir> { + pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self { + Tir { hir, ty } } pub fn span(&self) -> Span { @@ -127,10 +124,6 @@ impl Tir { pub fn as_hir(&self) -> &Hir { &self.hir } - /// Converts a closed expression back to the corresponding AST expression. - pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - self.as_hir().to_expr(opts) - } pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { self.as_hir().to_expr_tyenv(env) } @@ -173,17 +166,6 @@ impl Tir { .to_universe(), )) } - /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as - /// needed on demand. - pub fn eval_closed_expr(&self) -> Nir { - self.eval(NzEnv::new()) - } - /// Eval a closed Tir fully and recursively; - pub fn rec_eval_closed_expr(&self) -> Nir { - let val = self.eval_closed_expr(); - val.normalize(); - val - } } impl From for Universe { -- cgit v1.2.3