From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:23:59 +0000 Subject: Add Hir as untyped alternative to TyExpr --- dhall/src/semantics/tck/tyexpr.rs | 70 +++++++-------------------------------- 1 file changed, 12 insertions(+), 58 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 1886646..fa578c0 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,17 +1,13 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; +use crate::semantics::{ + rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value, +}; use crate::syntax::{ExprKind, Span, V}; use crate::Normalized; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; -/// Stores an alpha-normalized variable. -#[derive(Debug, Clone, Copy)] -pub struct AlphaVar { - idx: usize, -} - #[derive(Debug, Clone)] pub(crate) enum TyExprKind { Var(AlphaVar), @@ -27,15 +23,6 @@ pub(crate) struct TyExpr { span: Span, } -impl AlphaVar { - pub(crate) fn new(idx: usize) -> Self { - AlphaVar { idx } - } - pub(crate) fn idx(&self) -> usize { - self.idx - } -} - impl TyExpr { pub fn new(kind: TyExprKind, ty: Option, span: Span) -> Self { TyExpr { @@ -58,17 +45,19 @@ impl TyExpr { } } + pub fn to_hir(&self) -> Hir { + let kind = match self.kind() { + TyExprKind::Var(v) => HirKind::Var(v.clone()), + TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())), + }; + Hir::new(kind, self.span()) + } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - tyexpr_to_expr(self, opts, &mut NameEnv::new()) + self.to_hir().to_expr(opts) } pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { - let opts = ToExprOptions { - normalize: true, - alpha: false, - }; - let mut env = env.as_nameenv().clone(); - tyexpr_to_expr(self, opts, &mut env) + self.to_hir().to_expr_tyenv(env) } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. @@ -88,41 +77,6 @@ impl TyExpr { } } -fn tyexpr_to_expr<'a>( - tyexpr: &'a TyExpr, - opts: ToExprOptions, - env: &mut NameEnv, -) -> NormalizedExpr { - rc(match tyexpr.kind() { - TyExprKind::Var(v) if opts.alpha => { - ExprKind::Var(V("_".into(), v.idx())) - } - TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)), - TyExprKind::Expr(e) => { - let e = e.map_ref_maybe_binder(|l, tye| { - if let Some(l) = l { - env.insert_mut(l); - } - let e = tyexpr_to_expr(tye, opts, env); - if let Some(_) = l { - env.remove_mut(); - } - e - }); - - match e { - ExprKind::Lam(_, t, e) if opts.alpha => { - ExprKind::Lam("_".into(), t, e) - } - ExprKind::Pi(_, t, e) if opts.alpha => { - ExprKind::Pi("_".into(), t, e) - } - e => e, - } - } - }) -} - impl std::fmt::Debug for TyExpr { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let mut x = fmt.debug_struct("TyExpr"); -- cgit v1.2.3 From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:53:55 +0000 Subject: Remove most TyExpr from normalization --- dhall/src/semantics/tck/tyexpr.rs | 11 +++-------- 1 file changed, 3 insertions(+), 8 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 fa578c0..29099c5 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,8 +1,6 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{ - rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value, -}; -use crate::syntax::{ExprKind, Span, V}; +use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value}; +use crate::syntax::{ExprKind, Span}; use crate::Normalized; use crate::{NormalizedExpr, ToExprOptions}; @@ -56,13 +54,10 @@ impl TyExpr { pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { self.to_hir().to_expr(opts) } - pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { - self.to_hir().to_expr_tyenv(env) - } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: &NzEnv) -> Value { - Value::new_thunk(env, self.clone()) + Value::new_thunk(env, self.to_hir()) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. -- cgit v1.2.3 From ad085a20bc257d03a52708d920cfc65f0e9051e6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:07:03 +0000 Subject: Remove all types from Value --- dhall/src/semantics/tck/tyexpr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 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 29099c5..05fa4b5 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -66,8 +66,8 @@ impl TyExpr { } /// Eval a closed TyExpr fully and recursively; pub fn rec_eval_closed_expr(&self) -> Value { - let mut val = self.eval_closed_expr(); - val.normalize_mut(); + let val = self.eval_closed_expr(); + val.normalize(); val } } -- cgit v1.2.3 From f6732982c522dd579d378ab4820001d5ae107c43 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:18:32 +0000 Subject: Automate conversion between envs --- dhall/src/semantics/tck/tyexpr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 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 05fa4b5..edba477 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -56,8 +56,8 @@ impl TyExpr { } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: &NzEnv) -> Value { - Value::new_thunk(env, self.to_hir()) + pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value { + Value::new_thunk(env.into(), self.to_hir()) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. -- cgit v1.2.3 From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:30:32 +0000 Subject: Remove types from NzEnv --- dhall/src/semantics/tck/tyexpr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 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 edba477..a1666a4 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -56,13 +56,13 @@ impl TyExpr { } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. - pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value { + pub fn eval(&self, env: impl Into) -> Value { Value::new_thunk(env.into(), self.to_hir()) } /// 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 { - self.eval(&NzEnv::new()) + self.eval(NzEnv::new()) } /// Eval a closed TyExpr fully and recursively; pub fn rec_eval_closed_expr(&self) -> Value { -- cgit v1.2.3 From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/semantics/tck/tyexpr.rs | 3 +-- 1 file changed, 1 insertion(+), 2 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 a1666a4..d46ab87 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,7 +1,6 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value}; use crate::syntax::{ExprKind, Span}; -use crate::Normalized; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; @@ -10,7 +9,7 @@ pub(crate) type Type = Value; pub(crate) enum TyExprKind { Var(AlphaVar), // Forbidden ExprKind variants: Var, Import, Embed - Expr(ExprKind), + Expr(ExprKind), } // An expression with inferred types at every node and resolved variables. -- cgit v1.2.3 From 7b649b8647c60f1c02050805520f307edff0a94f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 19:48:11 +0000 Subject: Only store type at root node in tyexpr --- dhall/src/semantics/tck/tyexpr.rs | 43 ++++++++++++++++----------------------- 1 file changed, 18 insertions(+), 25 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 d46ab87..b49ea3e 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,39 +1,30 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value}; -use crate::syntax::{ExprKind, Span}; +use crate::semantics::{Hir, HirKind, NzEnv, Value,TyEnv}; +use crate::syntax::Span; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; -#[derive(Debug, Clone)] -pub(crate) enum TyExprKind { - Var(AlphaVar), - // Forbidden ExprKind variants: Var, Import, Embed - Expr(ExprKind), -} - -// An expression with inferred types at every node and resolved variables. +// A hir expression plus its inferred type. #[derive(Clone)] pub(crate) struct TyExpr { - kind: Box, + hir: Hir, ty: Option, - span: Span, } impl TyExpr { - pub fn new(kind: TyExprKind, ty: Option, span: Span) -> Self { + pub fn new(kind: HirKind, ty: Option, span: Span) -> Self { TyExpr { - kind: Box::new(kind), + hir: Hir::new(kind, span), ty, - span, } } - pub fn kind(&self) -> &TyExprKind { - &*self.kind + pub fn kind(&self) -> &HirKind { + self.hir.kind() } pub fn span(&self) -> Span { - self.span.clone() + self.as_hir().span() } pub fn get_type(&self) -> Result { match &self.ty { @@ -41,22 +32,24 @@ impl TyExpr { None => Err(TypeError::new(TypeMessage::Sort)), } } + pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { + Ok(self.get_type()?.to_tyexpr_tyenv(env)) + } pub fn to_hir(&self) -> Hir { - let kind = match self.kind() { - TyExprKind::Var(v) => HirKind::Var(v.clone()), - TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())), - }; - Hir::new(kind, self.span()) + self.as_hir().clone() + } + pub fn as_hir(&self) -> &Hir { + &self.hir } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - self.to_hir().to_expr(opts) + self.as_hir().to_expr(opts) } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into) -> Value { - Value::new_thunk(env.into(), self.to_hir()) + self.as_hir().eval(&env.into()) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. -- cgit v1.2.3 From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:17:41 +0000 Subject: Simplify conversions to/from TyExpr --- dhall/src/semantics/tck/tyexpr.rs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 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 b49ea3e..dc14cd2 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,6 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{Hir, HirKind, NzEnv, Value,TyEnv}; -use crate::syntax::Span; +use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value}; +use crate::syntax::{Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; @@ -33,7 +33,12 @@ impl TyExpr { } } pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { - Ok(self.get_type()?.to_tyexpr_tyenv(env)) + Ok(self.get_type()?.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) -> Result, TypeError> { + Ok(self.get_type_tyexpr(env)?.get_type()?.as_const()) } pub fn to_hir(&self) -> Hir { -- cgit v1.2.3 From 350d1cf7d9c114b1334b2743071b0b99ea64c1ec Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:56:38 +0000 Subject: TyExpr always carries a type --- dhall/src/semantics/tck/tyexpr.rs | 41 ++++++++++++--------------------------- 1 file changed, 12 insertions(+), 29 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 dc14cd2..ac15ac5 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,4 +1,3 @@ -use crate::error::{TypeError, TypeMessage}; use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value}; use crate::syntax::{Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; @@ -6,39 +5,36 @@ use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; // A hir expression plus its inferred type. -#[derive(Clone)] +#[derive(Debug, Clone)] pub(crate) struct TyExpr { hir: Hir, - ty: Option, + ty: Type, } impl TyExpr { - pub fn new(kind: HirKind, ty: Option, span: Span) -> Self { + pub fn new(kind: HirKind, ty: Type, span: Span) -> Self { TyExpr { hir: Hir::new(kind, span), ty, } } - pub fn kind(&self) -> &HirKind { - self.hir.kind() - } pub fn span(&self) -> Span { self.as_hir().span() } - pub fn get_type(&self) -> Result { - match &self.ty { - Some(t) => Ok(t.clone()), - None => Err(TypeError::new(TypeMessage::Sort)), - } + pub fn ty(&self) -> &Type { + &self.ty } - pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { - Ok(self.get_type()?.to_hir(env.as_varenv()).typecheck(env)?) + pub fn get_type_tyexpr(&self, env: &TyEnv) -> TyExpr { + self.ty() + .to_hir(env.as_varenv()) + .typecheck(env) + .expect("Internal type error") } /// Get the kind (the type of the type) of this value // TODO: avoid recomputing so much - pub fn get_kind(&self, env: &TyEnv) -> Result, TypeError> { - Ok(self.get_type_tyexpr(env)?.get_type()?.as_const()) + pub fn get_kind(&self, env: &TyEnv) -> Option { + self.get_type_tyexpr(env).ty().as_const() } pub fn to_hir(&self) -> Hir { @@ -68,16 +64,3 @@ impl TyExpr { val } } - -impl std::fmt::Debug for TyExpr { - fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let mut x = fmt.debug_struct("TyExpr"); - x.field("kind", self.kind()); - if let Some(ty) = self.ty.as_ref() { - x.field("type", &ty); - } else { - x.field("type", &None::<()>); - } - x.finish() - } -} -- cgit v1.2.3 From 51cf6a28fa56031dbeae0ff378f0ef84eff7fd3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 14 Feb 2020 18:55:27 +0000 Subject: Oops --- dhall/src/semantics/tck/tyexpr.rs | 12 +++++------- 1 file changed, 5 insertions(+), 7 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 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 { + 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 { - self.get_type_tyexpr(env).ty().as_const() + pub fn get_kind(&self, env: &TyEnv) -> Result, TypeError> { + Ok(self.get_type_tyexpr(env)?.ty().as_const()) } pub fn to_hir(&self) -> Hir { -- cgit v1.2.3 From d65d639ff93691adbf0a208edb99736003bc64bd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:05:26 +0000 Subject: Factor some tck code to avoid needing get_type_tyexpr --- dhall/src/semantics/tck/tyexpr.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 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 c7b8009..dfb4397 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -26,13 +26,15 @@ impl TyExpr { pub fn ty(&self) -> &Type { &self.ty } - pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { - 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) -> Result, TypeError> { - Ok(self.get_type_tyexpr(env)?.ty().as_const()) + Ok(self + .ty() + .to_hir(env.as_varenv()) + .typecheck(env)? + .ty() + .as_const()) } pub fn to_hir(&self) -> Hir { @@ -48,7 +50,7 @@ impl TyExpr { /// Eval the TyExpr. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into) -> Value { - self.as_hir().eval(&env.into()) + self.as_hir().eval(env.into()) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. -- cgit v1.2.3 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 From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:06:23 +0000 Subject: Start requiring Universe to build a Type --- dhall/src/semantics/tck/tyexpr.rs | 117 +++++++++++++++++++++++++++++++------- 1 file changed, 98 insertions(+), 19 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 4999899..3c47a81 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,8 +1,12 @@ -use crate::error::TypeError; -use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv}; +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 { @@ -16,12 +20,64 @@ pub(crate) struct TyExpr { 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) + } + pub fn previous(self) -> Option { + if self.0 == 0 { + None + } else { + Some(Universe(self.0 - 1)) + } + } +} + impl Type { + pub fn new(val: Value, _u: Universe) -> Self { + Type { val } + } pub fn from_const(c: Const) -> Self { - Value::from_const(c).into() + Self::new(Value::from_const(c), c.to_universe().next()) } pub fn from_builtin(b: Builtin) -> Self { - Value::from_builtin(b).into() + 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 + // TODO: avoid recomputing so much + pub fn ty(&self, env: &TyEnv) -> Result, TypeError> { + Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const()) + } + /// Get the type of this type + // TODO: avoid recomputing so much + pub fn ty_univ(&self, env: &TyEnv) -> Result { + Ok(match self.ty(env)? { + Some(c) => c.to_universe(), + // TODO: hack, might explode + None => Const::Sort.to_universe().next(), + }) } pub fn to_value(&self) -> Value { @@ -49,9 +105,9 @@ impl Type { } impl TyExpr { - pub fn new(kind: HirKind, ty: Type, span: Span) -> Self { + pub fn from_hir(hir: &Hir, ty: Type) -> Self { TyExpr { - hir: Hir::new(kind, span), + hir: hir.clone(), ty, } } @@ -62,16 +118,6 @@ impl TyExpr { pub fn ty(&self) -> &Type { &self.ty } - /// Get the kind (the type of the type) of this value - // TODO: avoid recomputing so much - pub fn get_kind(&self, env: &TyEnv) -> Result, TypeError> { - Ok(self - .ty() - .to_hir(env.as_varenv()) - .typecheck(env)? - .ty() - .as_const()) - } pub fn to_hir(&self) -> Hir { self.as_hir().clone() @@ -79,18 +125,51 @@ impl TyExpr { pub fn as_hir(&self) -> &Hir { &self.hir } - /// Converts a value back to the corresponding AST expression. + /// 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 TyExpr. 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: impl Into) -> Type { - self.eval(env).into() + 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 TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. -- cgit v1.2.3 From c451c18103b871e563b12c524bc3feec5451154c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:48:35 +0000 Subject: Avoid recomputing universes in tck --- dhall/src/semantics/tck/tyexpr.rs | 49 ++++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 24 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 3c47a81..f6591ba 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -11,6 +11,7 @@ pub(crate) struct Universe(u8); #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Type { val: Value, + univ: Universe, } /// A hir expression plus its inferred type. @@ -39,18 +40,28 @@ impl Universe { pub fn next(self) -> Self { Universe(self.0 + 1) } - pub fn previous(self) -> Option { - if self.0 == 0 { - None - } else { - Some(Universe(self.0 - 1)) - } - } } impl Type { - pub fn new(val: Value, _u: Universe) -> Self { - Type { val } + 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()) @@ -66,18 +77,8 @@ impl Type { } /// Get the type of this type - // TODO: avoid recomputing so much - pub fn ty(&self, env: &TyEnv) -> Result, TypeError> { - Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const()) - } - /// Get the type of this type - // TODO: avoid recomputing so much - pub fn ty_univ(&self, env: &TyEnv) -> Result { - Ok(match self.ty(env)? { - Some(c) => c.to_universe(), - // TODO: hack, might explode - None => Const::Sort.to_universe().next(), - }) + pub fn ty(&self) -> Universe { + self.univ } pub fn to_value(&self) -> Value { @@ -184,8 +185,8 @@ impl TyExpr { } } -impl From for Type { - fn from(x: Value) -> Type { - Type { val: x } +impl From for Universe { + fn from(x: Const) -> Universe { + Universe::from_const(x) } } -- cgit v1.2.3 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/tyexpr.rs | 192 -------------------------------------- 1 file changed, 192 deletions(-) delete mode 100644 dhall/src/semantics/tck/tyexpr.rs (limited to 'dhall/src/semantics/tck/tyexpr.rs') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs deleted file mode 100644 index f6591ba..0000000 --- a/dhall/src/semantics/tck/tyexpr.rs +++ /dev/null @@ -1,192 +0,0 @@ -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. -#[derive(Debug, Clone)] -pub(crate) struct TyExpr { - 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 TyExpr { - pub fn from_hir(hir: &Hir, ty: Type) -> Self { - TyExpr { - 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 TyExpr. 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 TyExpr (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 TyExpr 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