diff options
author | Nadrieril | 2020-02-17 18:12:44 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-17 18:12:44 +0000 |
commit | 2f65c02a995f6b6d4c755197fc074782f6bb100d (patch) | |
tree | ebe6373d5344b90f1a3e77b1a772e1ccadc6be81 /dhall/src | |
parent | 73571249f9bcf8efe84708a4a9f8665af62e44f0 (diff) |
Rename TyExpr to Tir
Diffstat (limited to '')
-rw-r--r-- | dhall/src/lib.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/resolve/hir.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/tck/mod.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tir.rs (renamed from dhall/src/semantics/tck/tyexpr.rs) | 13 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 33 |
5 files changed, 29 insertions, 31 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 144cac5..3fbc251 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -22,9 +22,7 @@ use crate::error::{EncodeError, Error, TypeError}; use crate::semantics::parse; use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; -use crate::semantics::{ - typecheck, typecheck_with, Hir, TyExpr, Value, ValueKind, -}; +use crate::semantics::{typecheck, typecheck_with, Hir, Tir, Value, ValueKind}; use crate::syntax::binary; use crate::syntax::{Builtin, Expr}; @@ -44,7 +42,7 @@ pub struct Resolved(Hir); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(TyExpr); +pub struct Typed(Tir); /// A normalized expression. /// 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<TyExpr, TypeError> { + pub fn typecheck(&self, env: &TyEnv) -> Result<Tir, TypeError> { 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/tyexpr.rs b/dhall/src/semantics/tck/tir.rs index f6591ba..800d1b7 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -15,8 +15,9 @@ pub(crate) struct Type { } /// A hir expression plus its inferred type. +/// Stands for "Typed intermediate representation" #[derive(Debug, Clone)] -pub(crate) struct TyExpr { +pub(crate) struct Tir { hir: Hir, ty: Type, } @@ -105,9 +106,9 @@ impl Type { } } -impl TyExpr { +impl Tir { pub fn from_hir(hir: &Hir, ty: Type) -> Self { - TyExpr { + Tir { hir: hir.clone(), ty, } @@ -134,7 +135,7 @@ impl TyExpr { self.as_hir().to_expr_tyenv(env) } - /// Eval the TyExpr. It will actually get evaluated only as needed on demand. + /// Eval the Tir. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into<NzEnv>) -> Value { self.as_hir().eval(env.into()) } @@ -172,12 +173,12 @@ impl TyExpr { .to_universe(), )) } - /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as + /// 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 TyExpr fully and recursively; + /// Eval a closed Tir fully and recursively; pub fn rec_eval_closed_expr(&self) -> Value { let val = self.eval_closed_expr(); val.normalize(); 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<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind<TyExpr>, + ekind: ExprKind<Tir>, span: Span, ) -> Result<Type, TypeError> { 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<Type>, -) -> Result<TyExpr, TypeError> { - let tyexpr = match hir.kind() { - HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)), +) -> Result<Tir, TypeError> { + 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<TyExpr, TypeError> { +pub(crate) fn typecheck(hir: &Hir) -> Result<Tir, TypeError> { 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<TyExpr, TypeError> { +pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<Tir, TypeError> { let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } |