From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:58:28 +0000 Subject: Take Hir for typecheck --- dhall/src/lib.rs | 10 ++++-- dhall/src/semantics/builtins.rs | 12 +++++--- dhall/src/semantics/mod.rs | 1 + dhall/src/semantics/nze/value.rs | 7 +++-- dhall/src/semantics/resolve.rs | 13 +++----- dhall/src/semantics/tck/env.rs | 12 +++----- dhall/src/semantics/tck/typecheck.rs | 60 +++++++++++++++++------------------- 7 files changed, 58 insertions(+), 57 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c2a2f19..2d261f9 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -79,7 +79,7 @@ impl Parsed { resolve::resolve(self) } pub fn skip_resolve(self) -> Result { - resolve::skip_resolve_expr(self) + Ok(Resolved(resolve::skip_resolve(&self.0)?)) } pub fn encode(&self) -> Result, EncodeError> { @@ -94,10 +94,10 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - Ok(Typed(typecheck(&self.to_expr())?)) + Ok(Typed(typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(typecheck_with(&self.to_expr(), ty.to_expr())?)) + Ok(Typed(typecheck_with(&self.0, ty.to_hir())?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -136,6 +136,10 @@ impl Normalized { normalize: false, }) } + /// Converts a value back to the corresponding Hir expression. + pub(crate) fn to_hir(&self) -> Hir { + self.0.to_hir_noenv() + } /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 715e045..b1d12aa 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, + skip_resolve, typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -115,9 +115,9 @@ macro_rules! make_type { }; } -pub(crate) fn type_of_builtin(b: Builtin) -> Expr { +pub(crate) fn type_of_builtin(b: Builtin) -> Hir { use Builtin::*; - match b { + let expr = match b { Bool | Natural | Integer | Double | Text => make_type!(Type), List | Optional => make_type!( Type -> Type @@ -200,7 +200,8 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { OptionalNone => make_type!( forall (A: Type) -> Optional A ), - } + }; + skip_resolve(&expr).unwrap() } // Ad-hoc macro to help construct closures @@ -264,7 +265,8 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { Value(Value), DoneAsIs, } - let make_closure = |e| typecheck(&e).unwrap().eval(&env); + let make_closure = + |e| typecheck(&skip_resolve(&e).unwrap()).unwrap().eval(&env); let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index a8c0659..ffa16ca 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -7,4 +7,5 @@ pub mod tck; pub(crate) use self::builtins::*; pub(crate) use self::hir::*; pub(crate) use self::nze::*; +pub(crate) use self::resolve::*; pub(crate) use self::tck::*; diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index a771b91..48acdb5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -327,9 +327,12 @@ impl Value { Hir::new(hir, self.0.span.clone()) } + pub fn to_hir_noenv(&self) -> Hir { + self.to_hir(VarEnv::new()) + } pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { - let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv); - type_with(tyenv, &expr).unwrap() + let hir = self.to_hir(tyenv.as_varenv()); + type_with(tyenv, &hir).unwrap() } pub fn to_tyexpr_noenv(&self) -> TyExpr { self.to_tyexpr_tyenv(&TyEnv::new()) diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs index e12e892..8c9bb05 100644 --- a/dhall/src/semantics/resolve.rs +++ b/dhall/src/semantics/resolve.rs @@ -6,7 +6,7 @@ use crate::error::{Error, ImportError}; use crate::semantics::{mkerr, Hir, HirKind, NameEnv}; use crate::syntax; use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL}; -use crate::{Normalized, Parsed, Resolved}; +use crate::{Normalized, Parsed, ParsedExpr, Resolved}; type Import = syntax::Import; @@ -162,13 +162,10 @@ pub(crate) fn resolve(parsed: Parsed) -> Result { resolve_with_env(&mut ResolveEnv::new(), parsed) } -pub(crate) fn skip_resolve_expr(parsed: Parsed) -> Result { - let Parsed(expr, _) = parsed; - let resolved = - traverse_resolve_expr(&mut NameEnv::new(), &expr, &mut |import| { - Err(ImportError::UnexpectedImport(import).into()) - })?; - Ok(Resolved(resolved)) +pub(crate) fn skip_resolve(expr: &ParsedExpr) -> Result { + traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import| { + Err(ImportError::UnexpectedImport(import).into()) + }) } pub trait Canonicalize { diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index af955f4..3b02074 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -21,9 +21,9 @@ pub(crate) struct TyEnv { } impl VarEnv { - // pub fn new() -> Self { - // VarEnv { size: 0 } - // } + pub fn new() -> Self { + VarEnv { size: 0 } + } pub fn size(&self) -> usize { self.size } @@ -116,9 +116,7 @@ impl TyEnv { items: self.items.insert_value(e, ty), } } - pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> { - let var = self.names.unlabel_var(var)?; - let ty = self.items.lookup_ty(&var); - Some((var, ty)) + pub fn lookup(&self, var: &AlphaVar) -> Type { + self.items.lookup_ty(&var) } } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index eb6a58c..ac113cd 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,11 +5,11 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr, - TyExprKind, Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv, + TyExpr, TyExprKind, Type, Value, ValueKind, }; use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span, }; use crate::Normalized; @@ -115,8 +115,8 @@ fn type_one_layer( ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), ExprKind::Builtin(b) => { - let t_expr = type_of_builtin(*b); - let t_tyexpr = type_with(env, &t_expr)?; + let t_hir = type_of_builtin(*b); + let t_tyexpr = typecheck(&t_hir)?; t_tyexpr.eval(env.as_nzenv()) } ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), @@ -761,25 +761,16 @@ fn type_one_layer( } /// `type_with` typechecks an expressio in the provided environment. -pub(crate) fn type_with( - env: &TyEnv, - expr: &Expr, -) -> Result { - let (tyekind, ty) = match expr.as_ref() { - ExprKind::Var(var) => match env.lookup(&var) { - Some((v, ty)) => (TyExprKind::Var(v), Some(ty)), - None => { - return mkerr( - ErrorBuilder::new(format!("unbound variable `{}`", var)) - .span_err(expr.span(), "not found in this scope") - .format(), - ) - } - }, - ExprKind::Const(Const::Sort) => { +pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { + let (tyekind, ty) = match hir.kind() { + HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))), + HirKind::Expr(ExprKind::Var(_)) => { + unreachable!("Hir should contain no unresolved variables") + } + HirKind::Expr(ExprKind::Const(Const::Sort)) => { (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } - ExprKind::Embed(p) => { + HirKind::Expr(ExprKind::Embed(p)) => { let val = p.clone().into_value(); ( val.to_tyexpr_noenv().kind().clone(), @@ -787,7 +778,7 @@ pub(crate) fn type_with( ) // return Ok(p.clone().into_value().to_tyexpr_noenv()) } - ekind => { + HirKind::Expr(ekind) => { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot)?; @@ -805,7 +796,13 @@ pub(crate) fn type_with( } ExprKind::Let(binder, annot, val, body) => { let val = if let Some(t) = annot { - t.rewrap(ExprKind::Annot(val.clone(), t.clone())) + Hir::new( + HirKind::Expr(ExprKind::Annot( + val.clone(), + t.clone(), + )), + t.span(), + ) } else { val.clone() }; @@ -818,16 +815,16 @@ pub(crate) fn type_with( } _ => ekind.traverse_ref(|e| type_with(env, e))?, }; - return type_one_layer(env, ekind, expr.span()); + return type_one_layer(env, ekind, hir.span()); } }; - Ok(TyExpr::new(tyekind, ty, expr.span())) + Ok(TyExpr::new(tyekind, ty, hir.span())) } /// 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(e: &Expr) -> Result { +pub(crate) fn typecheck(e: &Hir) -> Result { let res = type_with(&TyEnv::new(), e)?; // Ensure that the inferred type exists (i.e. this is not Sort) res.get_type()?; @@ -835,9 +832,8 @@ pub(crate) fn typecheck(e: &Expr) -> Result { } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. -pub(crate) fn typecheck_with( - expr: &Expr, - ty: Expr, -) -> Result { - typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty))) +pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { + let hir = + Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span()); + typecheck(&hir) } -- cgit v1.2.3