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/resolve/hir.rs | 4 +- dhall/src/semantics/tck/mod.rs | 4 +- dhall/src/semantics/tck/tir.rs | 193 +++++++++++++++++++++++++++++++++++ dhall/src/semantics/tck/tyexpr.rs | 192 ---------------------------------- dhall/src/semantics/tck/typecheck.rs | 33 +++--- 5 files changed, 213 insertions(+), 213 deletions(-) create mode 100644 dhall/src/semantics/tck/tir.rs delete mode 100644 dhall/src/semantics/tck/tyexpr.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index b5db66f..ae65fff 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,5 +1,5 @@ use crate::error::TypeError; -use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value}; +use crate::semantics::{type_with, NameEnv, NzEnv, Tir, TyEnv, Value}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{NormalizedExpr, ToExprOptions}; @@ -70,7 +70,7 @@ impl Hir { } /// Typecheck the Hir. - pub fn typecheck(&self, env: &TyEnv) -> Result { + pub fn typecheck(&self, env: &TyEnv) -> Result { type_with(env, self, None) } diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs index 1df2a48..93c8f48 100644 --- a/dhall/src/semantics/tck/mod.rs +++ b/dhall/src/semantics/tck/mod.rs @@ -1,6 +1,6 @@ pub mod env; -pub mod tyexpr; +pub mod tir; pub mod typecheck; pub(crate) use env::*; -pub(crate) use tyexpr::*; +pub(crate) use tir::*; pub(crate) use typecheck::*; 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) + } +} 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) - } -} diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 45b3168..7bf15af 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,8 +5,8 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv, - TyExpr, Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv, + Type, Value, ValueKind, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -69,7 +69,7 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind, + ekind: ExprKind, span: Span, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); @@ -91,8 +91,7 @@ fn type_one_layer( ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); - let t_tyexpr = typecheck(&t_hir)?; - t_tyexpr.eval_to_type(env)? + typecheck(&t_hir)?.eval_to_type(env)? } ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool), ExprKind::Lit(LitKind::Natural(_)) => { @@ -712,9 +711,9 @@ pub(crate) fn type_with( env: &TyEnv, hir: &Hir, annot: Option, -) -> Result { - let tyexpr = match hir.kind() { - HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)), +) -> Result { + let tir = match hir.kind() { + HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } @@ -753,7 +752,7 @@ pub(crate) fn type_with( ); let ty = Type::new(ty_hir.eval(env), u); - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = type_with(env, annot, None)?; @@ -765,7 +764,7 @@ pub(crate) fn type_with( let ks = annot.ty().as_const().unwrap(); let kt = body.ty().as_const().unwrap(); let ty = Type::from_const(function_check(ks, kt)); - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => { let val_annot = annot @@ -777,39 +776,39 @@ pub(crate) fn type_with( let body_env = env.insert_value(&binder, val_nf, val.ty().clone()); let body = type_with(&body_env, body, None)?; let ty = body.ty().clone(); - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } HirKind::Expr(ekind) => { let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?; let ty = type_one_layer(env, ekind, hir.span())?; - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } }; if let Some(annot) = annot { - if *tyexpr.ty() != annot { + if *tir.ty() != annot { return mk_span_err( hir.span(), &format!( "annot mismatch: {} != {}", - tyexpr.ty().to_expr_tyenv(env), + tir.ty().to_expr_tyenv(env), annot.to_expr_tyenv(env) ), ); } } - Ok(tyexpr) + Ok(tir) } /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck(hir: &Hir) -> Result { +pub(crate) fn typecheck(hir: &Hir) -> Result { type_with(&TyEnv::new(), hir, None) } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. -pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { +pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3