summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/value.rs8
-rw-r--r--dhall/src/core/valuef.rs6
-rw-r--r--dhall/src/error/mod.rs8
-rw-r--r--dhall/src/phase/binary.rs49
-rw-r--r--dhall/src/phase/mod.rs22
-rw-r--r--dhall/src/phase/resolve.rs4
-rw-r--r--dhall/src/phase/typecheck.rs16
7 files changed, 54 insertions, 59 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 21ac288..49e30cd 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -9,7 +9,7 @@ use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{TypeError, TypeMessage};
use crate::phase::normalize::{apply_any, normalize_whnf};
use crate::phase::typecheck::{builtin_to_value, const_to_value};
-use crate::phase::{NormalizedSubExpr, Typed};
+use crate::phase::{NormalizedExpr, Typed};
#[derive(Debug, Clone, Copy)]
pub(crate) enum Form {
@@ -166,11 +166,11 @@ impl Value {
}
// TODO: rename `normalize_to_expr`
- pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
+ pub(crate) fn to_expr(&self) -> NormalizedExpr {
self.as_whnf().normalize_to_expr()
}
// TODO: rename `normalize_to_expr_maybe_alpha`
- pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
+ pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
self.as_whnf().normalize_to_expr_maybe_alpha(true)
}
pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
@@ -226,7 +226,7 @@ impl Value {
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
- ) -> NormalizedSubExpr {
+ ) -> NormalizedExpr {
self.as_nf().normalize_to_expr_maybe_alpha(alpha)
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 9ea2467..959f299 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,7 +7,7 @@ use dhall_syntax::{
use crate::core::value::Value;
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr};
+use crate::phase::{Normalized, NormalizedExpr};
/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
/// normalized on-demand.
@@ -52,7 +52,7 @@ impl ValueF {
}
/// Convert the value to a fully normalized syntactic expression
- pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
+ pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr {
self.normalize_to_expr_maybe_alpha(false)
}
/// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
@@ -60,7 +60,7 @@ impl ValueF {
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
- ) -> NormalizedSubExpr {
+ ) -> NormalizedExpr {
match self {
ValueF::Lam(x, t, e) => rc(ExprF::Lam(
x.to_label_maybe_alpha(alpha),
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 2ddaf3d..6d4e120 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{BinOp, Import, Label, ParseError, V};
use crate::core::context::TypecheckContext;
use crate::core::value::Value;
use crate::phase::resolve::ImportStack;
-use crate::phase::NormalizedSubExpr;
+use crate::phase::NormalizedExpr;
pub type Result<T> = std::result::Result<T, Error>;
@@ -22,9 +22,9 @@ pub enum Error {
#[derive(Debug)]
pub enum ImportError {
- Recursive(Import<NormalizedSubExpr>, Box<Error>),
- UnexpectedImport(Import<NormalizedSubExpr>),
- ImportCycle(ImportStack, Import<NormalizedSubExpr>),
+ Recursive(Import<NormalizedExpr>, Box<Error>),
+ UnexpectedImport(Import<NormalizedExpr>),
+ ImportCycle(ImportStack, Import<NormalizedExpr>),
}
#[derive(Debug)]
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 3746635..7dc9be2 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -4,28 +4,26 @@ use std::iter::FromIterator;
use dhall_syntax::map::DupTreeMap;
use dhall_syntax::{
- rc, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode, Integer,
- InterpolatedText, Label, Natural, Scheme, SubExpr, URL, V,
+ rc, Expr, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode,
+ Integer, InterpolatedText, Label, Natural, Scheme, URL, V,
};
use crate::error::{DecodeError, EncodeError};
-use crate::phase::DecodedSubExpr;
+use crate::phase::DecodedExpr;
-pub(crate) fn decode(data: &[u8]) -> Result<DecodedSubExpr, DecodeError> {
+pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
match serde_cbor::de::from_slice(data) {
Ok(v) => cbor_value_to_dhall(&v),
Err(e) => Err(DecodeError::CBORError(e)),
}
}
-pub(crate) fn encode<E>(expr: &SubExpr<E>) -> Result<Vec<u8>, EncodeError> {
+pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
serde_cbor::ser::to_vec(&Serialize::Expr(expr))
.map_err(|e| EncodeError::CBORError(e))
}
-fn cbor_value_to_dhall(
- data: &cbor::Value,
-) -> Result<DecodedSubExpr, DecodeError> {
+fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
use cbor::Value::*;
use dhall_syntax::{BinOp, Builtin, Const};
use ExprF::*;
@@ -382,7 +380,7 @@ fn cbor_map_to_dhall_map<'a, T>(
map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>,
) -> Result<T, DecodeError>
where
- T: FromIterator<(Label, DecodedSubExpr)>,
+ T: FromIterator<(Label, DecodedExpr)>,
{
map.into_iter()
.map(|(k, v)| -> Result<(_, _), _> {
@@ -399,7 +397,7 @@ fn cbor_map_to_dhall_opt_map<'a, T>(
map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>,
) -> Result<T, DecodeError>
where
- T: FromIterator<(Label, Option<DecodedSubExpr>)>,
+ T: FromIterator<(Label, Option<DecodedExpr>)>,
{
map.into_iter()
.map(|(k, v)| -> Result<(_, _), _> {
@@ -416,10 +414,10 @@ where
}
enum Serialize<'a, E> {
- Expr(&'a SubExpr<E>),
+ Expr(&'a Expr<E>),
CBOR(cbor::Value),
- RecordMap(&'a DupTreeMap<Label, SubExpr<E>>),
- UnionMap(&'a DupTreeMap<Label, Option<SubExpr<E>>>),
+ RecordMap(&'a DupTreeMap<Label, Expr<E>>),
+ UnionMap(&'a DupTreeMap<Label, Option<Expr<E>>>),
}
macro_rules! count {
@@ -439,7 +437,7 @@ macro_rules! ser_seq {
}};
}
-fn serialize_subexpr<S, E>(ser: S, e: &SubExpr<E>) -> Result<S::Ok, S::Error>
+fn serialize_subexpr<S, E>(ser: S, e: &Expr<E>) -> Result<S::Ok, S::Error>
where
S: serde::ser::Serializer,
{
@@ -449,7 +447,7 @@ where
use std::iter::once;
use self::Serialize::{RecordMap, UnionMap};
- fn expr<E>(x: &SubExpr<E>) -> self::Serialize<'_, E> {
+ fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> {
self::Serialize::Expr(x)
}
let cbor =
@@ -566,7 +564,7 @@ where
fn serialize_import<S, E>(
ser: S,
- import: &Import<SubExpr<E>>,
+ import: &Import<Expr<E>>,
) -> Result<S::Ok, S::Error>
where
S: serde::ser::Serializer,
@@ -675,12 +673,9 @@ impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
}
fn collect_nested_applications<'a, E>(
- e: &'a SubExpr<E>,
-) -> (&'a SubExpr<E>, Vec<&'a SubExpr<E>>) {
- fn go<'a, E>(
- e: &'a SubExpr<E>,
- vec: &mut Vec<&'a SubExpr<E>>,
- ) -> &'a SubExpr<E> {
+ e: &'a Expr<E>,
+) -> (&'a Expr<E>, Vec<&'a Expr<E>>) {
+ fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> {
match e.as_ref() {
ExprF::App(f, a) => {
vec.push(a);
@@ -694,15 +689,15 @@ fn collect_nested_applications<'a, E>(
(e, vec)
}
-type LetBinding<'a, E> = (&'a Label, &'a Option<SubExpr<E>>, &'a SubExpr<E>);
+type LetBinding<'a, E> = (&'a Label, &'a Option<Expr<E>>, &'a Expr<E>);
fn collect_nested_lets<'a, E>(
- e: &'a SubExpr<E>,
-) -> (&'a SubExpr<E>, Vec<LetBinding<'a, E>>) {
+ e: &'a Expr<E>,
+) -> (&'a Expr<E>, Vec<LetBinding<'a, E>>) {
fn go<'a, E>(
- e: &'a SubExpr<E>,
+ e: &'a Expr<E>,
vec: &mut Vec<LetBinding<'a, E>>,
- ) -> &'a SubExpr<E> {
+ ) -> &'a Expr<E> {
match e.as_ref() {
ExprF::Let(l, t, v, e) => {
vec.push((l, t, v));
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index bd8853a..ecc9213 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -1,7 +1,7 @@
use std::fmt::Display;
use std::path::Path;
-use dhall_syntax::{Builtin, Const, SubExpr};
+use dhall_syntax::{Builtin, Const, Expr};
use crate::core::value::Value;
use crate::core::valuef::ValueF;
@@ -16,19 +16,19 @@ pub(crate) mod parse;
pub(crate) mod resolve;
pub(crate) mod typecheck;
-pub type ParsedSubExpr = SubExpr<!>;
-pub type DecodedSubExpr = SubExpr<!>;
-pub type ResolvedSubExpr = SubExpr<Normalized>;
-pub type NormalizedSubExpr = SubExpr<Normalized>;
+pub type ParsedExpr = Expr<!>;
+pub type DecodedExpr = Expr<!>;
+pub type ResolvedExpr = Expr<Normalized>;
+pub type NormalizedExpr = Expr<Normalized>;
#[derive(Debug, Clone)]
-pub struct Parsed(ParsedSubExpr, ImportRoot);
+pub struct Parsed(ParsedExpr, ImportRoot);
/// An expression where all imports have been resolved
///
/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
#[derive(Debug, Clone)]
-pub struct Resolved(ResolvedSubExpr);
+pub struct Resolved(ResolvedExpr);
/// A typed expression
#[derive(Debug, Clone)]
@@ -102,10 +102,10 @@ impl Typed {
Typed::from_const(Const::Type)
}
- pub fn to_expr(&self) -> NormalizedSubExpr {
+ pub fn to_expr(&self) -> NormalizedExpr {
self.0.to_expr()
}
- pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
+ pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
self.0.to_expr_alpha()
}
pub(crate) fn to_value(&self) -> Value {
@@ -162,10 +162,10 @@ impl Normalized {
crate::phase::binary::encode(&self.to_expr())
}
- pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
+ pub(crate) fn to_expr(&self) -> NormalizedExpr {
self.0.to_expr()
}
- pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
+ pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
self.0.to_expr_alpha()
}
pub(crate) fn into_typed(self) -> Typed {
diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs
index 27ae7a3..b715e72 100644
--- a/dhall/src/phase/resolve.rs
+++ b/dhall/src/phase/resolve.rs
@@ -2,9 +2,9 @@ use std::collections::HashMap;
use std::path::{Path, PathBuf};
use crate::error::{Error, ImportError};
-use crate::phase::{Normalized, NormalizedSubExpr, Parsed, Resolved};
+use crate::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
-type Import = dhall_syntax::Import<NormalizedSubExpr>;
+type Import = dhall_syntax::Import<NormalizedExpr>;
/// A root from which to resolve relative imports.
#[derive(Debug, Clone, PartialEq, Eq)]
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index ab6d882..52a4e47 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -2,7 +2,7 @@ use std::cmp::max;
use std::collections::HashMap;
use dhall_syntax::{
- rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
+ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label,
};
use crate::core::context::TypecheckContext;
@@ -200,7 +200,7 @@ macro_rules! make_type {
fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
use dhall_syntax::Builtin::*;
- match b {
+ rc(match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
List | Optional => make_type!(
Type -> Type
@@ -280,14 +280,14 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
OptionalNone => make_type!(
forall (a: Type) -> Optional a
),
- }
+ })
}
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
let ctx = TypecheckContext::new();
Value::from_valuef_and_type(
ValueF::from_builtin(b),
- type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
+ type_with(&ctx, type_of_builtin(b)).unwrap(),
)
}
@@ -297,7 +297,7 @@ pub(crate) fn builtin_to_value(b: Builtin) -> Value {
/// normalized as well.
fn type_with(
ctx: &TypecheckContext,
- e: SubExpr<Normalized>,
+ e: Expr<Normalized>,
) -> Result<Value, TypeError> {
use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
@@ -791,13 +791,13 @@ fn type_last_layer(
/// `type_of` is the same as `type_with` with an empty context, meaning that the
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
-pub(crate) fn typecheck(e: SubExpr<Normalized>) -> Result<Value, TypeError> {
+pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> {
type_with(&TypecheckContext::new(), e)
}
pub(crate) fn typecheck_with(
- expr: SubExpr<Normalized>,
- ty: SubExpr<Normalized>,
+ expr: Expr<Normalized>,
+ ty: Expr<Normalized>,
) -> Result<Value, TypeError> {
typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 06:48:42 +0000