From 77af0bbc171618f48531cc6b1d77e18089928885 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 20:54:15 +0200 Subject: Stop tracking the absence of Embed values at the type level --- dhall/src/core/thunk.rs | 12 ++++++------ dhall/src/core/value.rs | 10 +++++----- dhall/src/phase/mod.rs | 4 ++-- dhall/src/phase/normalize.rs | 21 +++++++++++---------- dhall/src/phase/typecheck.rs | 11 ++++------- 5 files changed, 28 insertions(+), 30 deletions(-) (limited to 'dhall') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index c18014e..4d193f9 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF, X}; +use dhall_syntax::{Const, ExprF}; use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; @@ -12,7 +12,7 @@ use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; use crate::phase::typecheck::type_of_const; -use crate::phase::{NormalizedSubExpr, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -30,7 +30,7 @@ enum ThunkInternal { /// Partially normalized value whose subexpressions have been thunked (this is returned from /// typechecking). Note that this is different from `Value::PartialExpr` because there is no /// requirement of WHNF here. - PartialExpr(ExprF), + PartialExpr(ExprF), /// Partially normalized value. /// Invariant: if the marker is `NF`, the value must be fully normalized Value(Marker, Value), @@ -123,7 +123,7 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_partial_expr(e: ExprF) -> Thunk { + pub fn from_partial_expr(e: ExprF) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } @@ -309,7 +309,7 @@ impl Shift for ThunkInternal { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +356,7 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, ), ), ThunkInternal::Value(_, v) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 8486d6e..88d7a20 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, X, + NaiveDouble, Natural, }; use crate::core::thunk::{Thunk, TypedThunk}; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, }; -use crate::phase::Typed; +use crate::phase::{Normalized, Typed}; /// A semantic value. The invariants ensure this value represents a Weak-Head /// Normal Form (WHNF). This means that this first constructor is the first constructor of the @@ -59,7 +59,7 @@ pub enum Value { TextLit(Vec>), Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprF), } impl Value { @@ -475,7 +475,7 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +500,7 @@ impl Subst for Value { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, )) } // Retry normalizing since substituting may allow progress diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 8c93889..7364949 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::fmt::Display; use std::path::Path; -use dhall_syntax::{Const, Import, SubExpr, X}; +use dhall_syntax::{Const, Import, SubExpr}; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; @@ -20,7 +20,7 @@ pub(crate) mod typecheck; pub type ParsedSubExpr = SubExpr; pub type DecodedSubExpr = SubExpr; pub type ResolvedSubExpr = SubExpr; -pub type NormalizedSubExpr = SubExpr; +pub type NormalizedSubExpr = SubExpr; #[derive(Debug, Clone)] pub struct Parsed(ParsedSubExpr, ImportRoot); diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 644f98c..f1045a5 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -2,14 +2,14 @@ use std::collections::HashMap; use dhall_syntax::{ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, - NaiveDouble, X, + NaiveDouble, }; use crate::core::context::NormalizationContext; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::Subst; -use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed}; pub type InputSubExpr = ResolvedSubExpr; pub type OutputSubExpr = NormalizedSubExpr; @@ -86,7 +86,7 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { // Empty string literal. [] => { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = + let txt: InterpolatedText = std::iter::empty().collect(); let s = txt.to_string(); Ok(( @@ -98,10 +98,11 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { // interpolations, there is a single Text item) in the literal. [InterpolatedTextContents::Text(s)] => { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = std::iter::once( - InterpolatedTextContents::Text(s.clone()), - ) - .collect(); + let txt: InterpolatedText = + std::iter::once(InterpolatedTextContents::Text( + s.clone(), + )) + .collect(); let s = txt.to_string(); Ok(( r, @@ -376,7 +377,7 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { } // Thunk subexpressions - let expr: ExprF = + let expr: ExprF = expr.as_ref().map_ref_with_special_handling_of_binders( |e| Thunk::new(ctx.clone(), e.clone()), |x, e| Thunk::new(ctx.skip(x), e.clone()), @@ -391,7 +392,7 @@ enum Ret<'a> { Value(Value), Thunk(Thunk), ThunkRef(&'a Thunk), - Expr(ExprF), + Expr(ExprF), } /// Performs an intersection of two HashMaps. @@ -636,7 +637,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { }) } -pub fn normalize_one_layer(expr: ExprF) -> Value { +pub fn normalize_one_layer(expr: ExprF) -> Value { use Value::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index ecf9793..96ff246 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -2,7 +2,6 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr, - X, }; use crate::core::context::{NormalizationContext, TypecheckContext}; @@ -214,7 +213,7 @@ macro_rules! make_type { }; } -fn type_of_builtin(b: Builtin) -> Expr { +fn type_of_builtin(b: Builtin) -> Expr { use dhall_syntax::Builtin::*; match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -398,7 +397,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF, + e: &ExprF, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -598,9 +597,7 @@ fn type_last_layer( } } Const(c) => Ok(RetWhole(Typed::from_const(*c))), - Builtin(b) => { - Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?)) - } + Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)), BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), @@ -1016,7 +1013,7 @@ pub fn typecheck(e: Resolved) -> Result { pub fn typecheck_with(e: Resolved, ty: &Type) -> Result { let expr: SubExpr<_> = e.0; - let ty: SubExpr<_> = ty.to_expr().absurd(); + let ty: SubExpr<_> = ty.to_expr(); type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } pub fn skip_typecheck(e: Resolved) -> Typed { -- cgit v1.2.3