summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/binary.rs22
-rw-r--r--dhall/src/expr.rs32
-rw-r--r--dhall/src/normalize.rs48
-rw-r--r--dhall/src/serde.rs2
-rw-r--r--dhall/src/traits/static_type.rs14
-rw-r--r--dhall/src/typecheck.rs65
-rw-r--r--dhall/tests/traits.rs4
-rw-r--r--dhall_proc_macros/src/quote.rs62
-rw-r--r--dhall_syntax/src/core.rs207
-rw-r--r--dhall_syntax/src/parser.rs24
-rw-r--r--dhall_syntax/src/printer.rs44
-rw-r--r--dhall_syntax/src/visitor.rs130
12 files changed, 351 insertions, 303 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 9c31d4c..0d9f28a 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -2,7 +2,7 @@ use dhall_syntax::*;
use itertools::*;
use serde_cbor::value::value as cbor;
-type ParsedExpr = SubExpr<X, Import>;
+type ParsedExpr = SubExpr<Label, X, Import>;
#[derive(Debug)]
pub enum DecodeError {
@@ -18,28 +18,32 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
}
fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
- use cbor::Value::*;
+ use cbor::Value::{Array, Bool, Null, Object, String, F64, I64, U64};
use dhall_syntax::{BinOp, Builtin, Const};
- use ExprF::*;
+ use ExprF::{
+ Annot, App, BoolIf, BoolLit, DoubleLit, Embed, EmptyListLit, Field,
+ IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, OldOptionalLit, Pi,
+ RecordLit, RecordType, SomeLit, TextLit, UnionLit, UnionType,
+ };
Ok(rc(match data {
String(s) => match Builtin::parse(s) {
Some(b) => ExprF::Builtin(b),
None => match s.as_str() {
"True" => BoolLit(true),
"False" => BoolLit(false),
- "Type" => Const(Const::Type),
- "Kind" => Const(Const::Kind),
- "Sort" => Const(Const::Sort),
+ "Type" => ExprF::Const(Const::Type),
+ "Kind" => ExprF::Const(Const::Kind),
+ "Sort" => ExprF::Const(Const::Sort),
_ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
},
},
- U64(n) => Var(V(Label::from("_"), *n as usize)),
+ U64(n) => ExprF::Var(Var(Label::from("_"), *n as usize)),
F64(x) => DoubleLit((*x).into()),
Bool(b) => BoolLit(*b),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
let l = Label::from(l.as_str());
- Var(V(l, *n as usize))
+ ExprF::Var(Var(l, *n as usize))
}
[U64(0), f, args..] => {
let mut f = cbor_value_to_dhall(&f)?;
@@ -92,7 +96,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
Err(DecodeError::WrongFormatError("binop".to_owned()))?
}
};
- BinOp(op, x, y)
+ ExprF::BinOp(op, x, y)
}
[U64(4), t] => {
let t = cbor_value_to_dhall(&t)?;
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 5bde68f..efc3928 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -23,15 +23,17 @@ macro_rules! derive_other_traits {
};
}
+type OutputSubExpr = SubExpr<Label, X, X>;
+
#[derive(Debug, Clone)]
pub(crate) struct Parsed(
- pub(crate) SubExpr<Span, Import>,
+ pub(crate) SubExpr<Label, Span, Import>,
pub(crate) ImportRoot,
);
derive_other_traits!(Parsed);
#[derive(Debug, Clone)]
-pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>);
+pub(crate) struct Resolved(pub(crate) SubExpr<Label, Span, Normalized>);
derive_other_traits!(Resolved);
pub(crate) use self::typed::TypedInternal;
@@ -57,12 +59,12 @@ impl std::fmt::Display for Normalized {
}
mod typed {
- use super::{Type, Typed};
+ use super::{OutputSubExpr, Type, Typed};
use crate::normalize::{Thunk, Value};
use crate::typecheck::{
TypeError, TypeInternal, TypeMessage, TypecheckContext,
};
- use dhall_syntax::{Const, Label, SubExpr, V, X};
+ use dhall_syntax::{Const, Label, Var};
use std::borrow::Cow;
#[derive(Debug, Clone)]
@@ -90,7 +92,7 @@ mod typed {
}
}
- pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ pub(crate) fn to_expr(&self) -> OutputSubExpr {
self.to_value().normalize_to_expr()
}
@@ -129,7 +131,7 @@ mod typed {
}
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.shift(delta, var),
@@ -139,7 +141,11 @@ mod typed {
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(
+ &self,
+ var: &Var<Label>,
+ val: &Typed,
+ ) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.subst_shift(var, val),
@@ -158,7 +164,7 @@ mod typed {
///
/// For a more general notion of "type", see [Type].
#[derive(Debug, Clone)]
-pub struct SimpleType(pub(crate) SubExpr<X, X>);
+pub struct SimpleType(pub(crate) OutputSubExpr);
derive_other_traits!(SimpleType);
pub(crate) use crate::typecheck::TypeInternal;
@@ -178,16 +184,16 @@ impl std::fmt::Display for Type {
// Exposed for the macros
#[doc(hidden)]
-impl From<SimpleType> for SubExpr<X, X> {
- fn from(x: SimpleType) -> SubExpr<X, X> {
+impl From<SimpleType> for OutputSubExpr {
+ fn from(x: SimpleType) -> OutputSubExpr {
x.0
}
}
// Exposed for the macros
#[doc(hidden)]
-impl From<SubExpr<X, X>> for SimpleType {
- fn from(x: SubExpr<X, X>) -> SimpleType {
+impl From<OutputSubExpr> for SimpleType {
+ fn from(x: OutputSubExpr) -> SimpleType {
SimpleType(x)
}
}
@@ -204,7 +210,7 @@ impl Normalized {
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
Normalized(TypedInternal::from_thunk_and_type(th, t))
}
- pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ pub(crate) fn to_expr(&self) -> OutputSubExpr {
self.0.to_expr()
}
pub(crate) fn to_value(&self) -> Value {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 8ae746d..3de12ee 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,13 +6,13 @@ use dhall_proc_macros as dhall;
use dhall_syntax::context::Context;
use dhall_syntax::{
rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
- InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
+ InterpolatedTextContents, Label, Natural, Span, SubExpr, Var, X,
};
use crate::expr::{Normalized, Type, Typed, TypedInternal};
-type InputSubExpr = SubExpr<Span, Normalized>;
-type OutputSubExpr = SubExpr<X, X>;
+type InputSubExpr = SubExpr<Label, Span, Normalized>;
+type OutputSubExpr = SubExpr<Label, X, X>;
impl Typed {
/// Reduce an expression to its normal form, performing beta reduction
@@ -38,11 +38,11 @@ impl Typed {
Normalized(internal)
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
Typed(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
Typed(self.0.subst_shift(var, val))
}
@@ -58,11 +58,11 @@ impl Typed {
#[derive(Debug, Clone)]
enum EnvItem {
Thunk(Thunk),
- Skip(V<Label>),
+ Skip(Var<Label>),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
use EnvItem::*;
match self {
Thunk(e) => Thunk(e.shift(delta, var)),
@@ -70,7 +70,7 @@ impl EnvItem {
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
match self {
EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -93,8 +93,8 @@ impl NormalizationContext {
.insert(x.clone(), EnvItem::Skip(x.into())),
))
}
- fn lookup(&self, var: &V<Label>) -> Value {
- let V(x, n) = var;
+ fn lookup(&self, var: &Var<Label>) -> Value {
+ let Var(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Thunk(t)) => t.to_value(),
Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
@@ -118,11 +118,11 @@ impl NormalizationContext {
NormalizationContext(Rc::new(ctx))
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
}
- fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
NormalizationContext(Rc::new(
self.0.map(|_, e| e.subst_shift(var, val)),
))
@@ -144,7 +144,7 @@ pub(crate) enum Value {
NaturalSuccClosure,
Pi(Label, TypeThunk, TypeThunk),
- Var(V<Label>),
+ Var(Var<Label>),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -403,7 +403,7 @@ impl Value {
Value::AppliedBuiltin(b, vec![])
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -500,7 +500,7 @@ impl Value {
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -616,7 +616,7 @@ mod thunk {
OutputSubExpr, Value,
};
use crate::expr::Typed;
- use dhall_syntax::{Label, V};
+ use dhall_syntax::{Label, Var};
use std::cell::{Ref, RefCell};
use std::rc::Rc;
@@ -693,7 +693,7 @@ mod thunk {
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -707,7 +707,7 @@ mod thunk {
}
}
- fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -805,11 +805,15 @@ mod thunk {
apply_any(self.clone(), th)
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
self.0.borrow().shift(delta, var).into_thunk()
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(
+ &self,
+ var: &Var<Label>,
+ val: &Typed,
+ ) -> Self {
self.0.borrow().subst_shift(var, val).into_thunk()
}
}
@@ -855,14 +859,14 @@ impl TypeThunk {
self.normalize_nf().normalize_to_expr()
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
}
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs
index 96bc765..bc76c49 100644
--- a/dhall/src/serde.rs
+++ b/dhall/src/serde.rs
@@ -11,7 +11,7 @@ impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T {
}
}
-struct Deserializer<'a>(Cow<'a, SubExpr<X, X>>);
+struct Deserializer<'a>(Cow<'a, SubExpr<Label, X, X>>);
impl serde::de::Error for Error {
fn custom<T>(msg: T) -> Self
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index f90b8df..c3f323b 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -32,7 +32,7 @@ pub trait SimpleStaticType {
fn get_simple_static_type() -> SimpleType;
}
-fn mktype(x: SubExpr<X, X>) -> SimpleType {
+fn mktype(x: SubExpr<Label, X, X>) -> SimpleType {
x.into()
}
@@ -106,22 +106,22 @@ impl SimpleStaticType for String {
impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) {
fn get_simple_static_type() -> SimpleType {
- let ta: SubExpr<_, _> = A::get_simple_static_type().into();
- let tb: SubExpr<_, _> = B::get_simple_static_type().into();
+ let ta: SubExpr<_, _, _> = A::get_simple_static_type().into();
+ let tb: SubExpr<_, _, _> = B::get_simple_static_type().into();
mktype(dhall::subexpr!({ _1: ta, _2: tb }))
}
}
impl<T: SimpleStaticType> SimpleStaticType for Option<T> {
fn get_simple_static_type() -> SimpleType {
- let t: SubExpr<_, _> = T::get_simple_static_type().into();
+ let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
mktype(dhall::subexpr!(Optional t))
}
}
impl<T: SimpleStaticType> SimpleStaticType for Vec<T> {
fn get_simple_static_type() -> SimpleType {
- let t: SubExpr<_, _> = T::get_simple_static_type().into();
+ let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
mktype(dhall::subexpr!(List t))
}
}
@@ -142,8 +142,8 @@ impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType
for std::result::Result<T, E>
{
fn get_simple_static_type() -> SimpleType {
- let tt: SubExpr<_, _> = T::get_simple_static_type().into();
- let te: SubExpr<_, _> = E::get_simple_static_type().into();
+ let tt: SubExpr<_, _, _> = T::get_simple_static_type().into();
+ let te: SubExpr<_, _, _> = E::get_simple_static_type().into();
mktype(dhall::subexpr!(< Ok: tt | Err: te>))
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8b7f011..63041bb 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -14,13 +14,16 @@ use dhall_syntax::*;
use self::TypeMessage::*;
+type InputSubExpr = SubExpr<Label, Span, Normalized>;
+type OutputSubExpr = SubExpr<Label, X, X>;
+
impl Resolved {
pub fn typecheck(self) -> Result<Typed, TypeError> {
type_of(self.0)
}
pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
- let expr: SubExpr<_, _> = self.0;
- let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
+ let expr = self.0;
+ let ty = ty.to_expr().embed_absurd().note_absurd();
type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
/// Pretends this expression has been typechecked. Use with care.
@@ -43,7 +46,7 @@ impl Typed {
}
impl Normalized {
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
Normalized(self.0.shift(delta, var))
}
pub(crate) fn to_type(self) -> Type {
@@ -55,7 +58,7 @@ impl Type {
pub(crate) fn to_normalized(&self) -> Normalized {
self.0.to_normalized()
}
- pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ pub(crate) fn to_expr(&self) -> OutputSubExpr {
self.0.to_expr()
}
pub(crate) fn to_value(&self) -> Value {
@@ -73,10 +76,10 @@ impl Type {
fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
- pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
Type(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
Type(self.0.subst_shift(var, val))
}
@@ -124,7 +127,7 @@ impl TypeInternal {
fn to_normalized(&self) -> Normalized {
self.to_typed().normalize()
}
- fn to_expr(&self) -> SubExpr<X, X> {
+ fn to_expr(&self) -> OutputSubExpr {
self.to_normalized().to_expr()
}
fn to_value(&self) -> Value {
@@ -148,14 +151,14 @@ impl TypeInternal {
_ => None,
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.shift(delta, var))),
Const(c) => Const(*c),
}
}
- fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -173,12 +176,12 @@ impl PartialEq for TypeInternal {
#[derive(Debug, Clone)]
pub(crate) enum EnvItem {
- Type(V<Label>, Type),
+ Type(Var<Label>, Type),
Value(Normalized),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
use EnvItem::*;
match self {
Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -205,8 +208,8 @@ impl TypecheckContext {
pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self {
TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
}
- pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> {
- let V(x, n) = var;
+ pub(crate) fn lookup(&self, var: &Var<Label>) -> Option<Cow<'_, Type>> {
+ let Var(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
Some(EnvItem::Value(t)) => Some(t.get_type()?),
@@ -238,8 +241,12 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
}
}
-fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
- let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
+fn match_vars(
+ vl: &Var<Label>,
+ vr: &Var<Label>,
+ ctx: &[(&Label, &Label)],
+) -> bool {
+ let (Var(xL, mut nL), Var(xR, mut nR)) = (vl, vr);
for &(xL2, xR2) in ctx {
match (nL, nR) {
(0, 0) if xL == xL2 && xR == xR2 => return true,
@@ -265,8 +272,8 @@ where
use dhall_syntax::ExprF::*;
fn go<'a, S, T>(
ctx: &mut Vec<(&'a Label, &'a Label)>,
- el: &'a SubExpr<S, X>,
- er: &'a SubExpr<T, X>,
+ el: &'a SubExpr<Label, S, X>,
+ er: &'a SubExpr<Label, T, X>,
) -> bool
where
S: ::std::fmt::Debug,
@@ -350,9 +357,9 @@ fn type_of_const(c: Const) -> Result<Type, TypeError> {
}
}
-fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
+fn type_of_builtin(b: Builtin) -> InputSubExpr {
use dhall_syntax::Builtin::*;
- match b {
+ rc(match b {
Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
List | Optional => dhall::expr!(
Type -> Type
@@ -432,7 +439,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
OptionalNone => dhall::expr!(
forall (A: Type) -> Optional A
),
- }
+ })
+ .note_absurd()
}
macro_rules! ensure_equal {
@@ -619,10 +627,7 @@ impl TypeIntermediate {
/// Takes an expression that is meant to contain a Type
/// and turn it into a type, typechecking it along the way.
-fn mktype(
- ctx: &TypecheckContext,
- e: SubExpr<Span, Normalized>,
-) -> Result<Type, TypeError> {
+fn mktype(ctx: &TypecheckContext, e: InputSubExpr) -> Result<Type, TypeError> {
Ok(type_with(ctx, e)?.to_type())
}
@@ -645,7 +650,7 @@ enum Ret {
/// succeeded, or an error if type-checking failed
fn type_with(
ctx: &TypecheckContext,
- e: SubExpr<Span, Normalized>,
+ e: InputSubExpr,
) -> Result<Typed, TypeError> {
use dhall_syntax::ExprF::{
Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
@@ -756,7 +761,7 @@ fn type_last_layer(
mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
});
- Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
+ Ok(RetType(tb.subst_shift(&x.into(), &a)))
}
Annot(x, t) => {
let t = t.to_type();
@@ -937,9 +942,7 @@ fn type_last_layer(
}
}
Const(c) => Ok(RetTyped(const_to_typed(c))),
- Builtin(b) => {
- Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
- }
+ Builtin(b) => Ok(RetType(mktype(ctx, type_of_builtin(b))?)),
BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -998,7 +1001,7 @@ fn type_last_layer(
/// `typeOf` 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.
-fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
+fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
let ctx = TypecheckContext::new();
let e = type_with(&ctx, e)?;
// Ensure `e` has a type (i.e. `e` is not `Sort`)
@@ -1009,7 +1012,7 @@ fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
/// The specific type error
#[derive(Debug)]
pub(crate) enum TypeMessage {
- UnboundVariable(V<Label>),
+ UnboundVariable(Var<Label>),
InvalidInputType(Normalized),
InvalidOutputType(Normalized),
NotAFunction(Typed),
diff --git a/dhall/tests/traits.rs b/dhall/tests/traits.rs
index 6604c06..cf68d7d 100644
--- a/dhall/tests/traits.rs
+++ b/dhall/tests/traits.rs
@@ -1,11 +1,11 @@
#![feature(proc_macro_hygiene)]
use dhall::de::SimpleStaticType;
use dhall_proc_macros;
-use dhall_syntax::{SubExpr, X};
+use dhall_syntax::{Label, SubExpr, X};
#[test]
fn test_static_type() {
- fn mktype(x: SubExpr<X, X>) -> dhall::expr::SimpleType {
+ fn mktype(x: SubExpr<Label, X, X>) -> dhall::expr::SimpleType {
x.into()
}
diff --git a/dhall_proc_macros/src/quote.rs b/dhall_proc_macros/src/quote.rs
index eaf4946..d0deaad 100644
--- a/dhall_proc_macros/src/quote.rs
+++ b/dhall_proc_macros/src/quote.rs
@@ -7,7 +7,7 @@ use std::collections::BTreeMap;
pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
let input_str = input.to_string();
- let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote();
+ let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote();
let no_import =
|_: &Import| -> X { panic!("Don't use import in dhall::expr!()") };
let expr = expr.map_embed(no_import);
@@ -17,7 +17,7 @@ pub fn expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
pub fn subexpr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
let input_str = input.to_string();
- let expr: SubExpr<_, Import> = parse_expr(&input_str).unwrap().unnote();
+ let expr: SubExpr<_, _, Import> = parse_expr(&input_str).unwrap().unnote();
let no_import =
|_: &Import| -> X { panic!("Don't use import in dhall::subexpr!()") };
let expr = expr.map_embed(no_import);
@@ -31,60 +31,59 @@ pub fn quote_exprf<TS>(expr: ExprF<TS, Label, X>) -> TokenStream
where
TS: quote::ToTokens + std::fmt::Debug,
{
- use dhall_syntax::ExprF::*;
match expr {
- Var(_) => unreachable!(),
- Pi(x, t, b) => {
+ ExprF::Var(_) => unreachable!(),
+ ExprF::Pi(x, t, b) => {
let x = quote_label(&x);
quote! { dhall_syntax::ExprF::Pi(#x, #t, #b) }
}
- Lam(x, t, b) => {
+ ExprF::Lam(x, t, b) => {
let x = quote_label(&x);
quote! { dhall_syntax::ExprF::Lam(#x, #t, #b) }
}
- App(f, a) => {
+ ExprF::App(f, a) => {
quote! { dhall_syntax::ExprF::App(#f, #a) }
}
- Annot(x, t) => {
+ ExprF::Annot(x, t) => {
quote! { dhall_syntax::ExprF::Annot(#x, #t) }
}
- Const(c) => {
+ ExprF::Const(c) => {
let c = quote_const(c);
quote! { dhall_syntax::ExprF::Const(#c) }
}
- Builtin(b) => {
+ ExprF::Builtin(b) => {
let b = quote_builtin(b);
quote! { dhall_syntax::ExprF::Builtin(#b) }
}
- BinOp(o, a, b) => {
+ ExprF::BinOp(o, a, b) => {
let o = quote_binop(o);
quote! { dhall_syntax::ExprF::BinOp(#o, #a, #b) }
}
- NaturalLit(n) => {
+ ExprF::NaturalLit(n) => {
quote! { dhall_syntax::ExprF::NaturalLit(#n) }
}
- BoolLit(b) => {
+ ExprF::BoolLit(b) => {
quote! { dhall_syntax::ExprF::BoolLit(#b) }
}
- SomeLit(x) => {
+ ExprF::SomeLit(x) => {
quote! { dhall_syntax::ExprF::SomeLit(#x) }
}
- EmptyListLit(t) => {
+ ExprF::EmptyListLit(t) => {
quote! { dhall_syntax::ExprF::EmptyListLit(#t) }
}
- NEListLit(es) => {
+ ExprF::NEListLit(es) => {
let es = quote_vec(es);
quote! { dhall_syntax::ExprF::NEListLit(#es) }
}
- RecordType(m) => {
+ ExprF::RecordType(m) => {
let m = quote_map(m);
quote! { dhall_syntax::ExprF::RecordType(#m) }
}
- RecordLit(m) => {
+ ExprF::RecordLit(m) => {
let m = quote_map(m);
quote! { dhall_syntax::ExprF::RecordLit(#m) }
}
- UnionType(m) => {
+ ExprF::UnionType(m) => {
let m = quote_opt_map(m);
quote! { dhall_syntax::ExprF::UnionType(#m) }
}
@@ -95,22 +94,21 @@ where
// Returns an expression of type SubExpr<_, _>. Expects interpolated variables
// to be of type SubExpr<_, _>.
fn quote_subexpr(
- expr: &SubExpr<X, X>,
+ expr: &SubExpr<Label, X, X>,
ctx: &Context<Label, ()>,
) -> TokenStream {
- use dhall_syntax::ExprF::*;
match expr.as_ref().map_ref_with_special_handling_of_binders(
|e| quote_subexpr(e, ctx),
|l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
|_| unreachable!(),
Label::clone,
) {
- Var(V(ref s, n)) => {
+ ExprF::Var(Var(ref s, n)) => {
match ctx.lookup(s, n) {
// Non-free variable; interpolates as itself
Some(()) => {
let s: String = s.into();
- let var = quote! { dhall_syntax::V(#s.into(), #n) };
+ let var = quote! { dhall_syntax::Var(#s.into(), #n) };
rc(quote! { dhall_syntax::ExprF::Var(#var) })
}
// Free variable; interpolates as a rust variable
@@ -119,7 +117,7 @@ fn quote_subexpr(
// TODO: insert appropriate shifts ?
let v: TokenStream = s.parse().unwrap();
quote! { {
- let x: dhall_syntax::SubExpr<_, _> = #v.clone();
+ let x: dhall_syntax::SubExpr<_, _, _> = #v.clone();
x
} }
}
@@ -129,22 +127,24 @@ fn quote_subexpr(
}
}
-// Returns an expression of type Expr<_, _>. Expects interpolated variables
-// to be of type SubExpr<_, _>.
-fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream {
- use dhall_syntax::ExprF::*;
+// Returns an expression of type Expr<_, _, _>. Expects interpolated variables
+// to be of type SubExpr<_, _, _>.
+fn quote_expr(
+ expr: &Expr<Label, X, X>,
+ ctx: &Context<Label, ()>,
+) -> TokenStream {
match expr.map_ref_with_special_handling_of_binders(
|e| quote_subexpr(e, ctx),
|l, e| quote_subexpr(e, &ctx.insert(l.clone(), ())),
|_| unreachable!(),
Label::clone,
) {
- Var(V(ref s, n)) => {
+ ExprF::Var(Var(ref s, n)) => {
match ctx.lookup(s, n) {
// Non-free variable; interpolates as itself
Some(()) => {
let s: String = s.into();
- let var = quote! { dhall_syntax::V(#s.into(), #n) };
+ let var = quote! { dhall_syntax::Var(#s.into(), #n) };
quote! { dhall_syntax::ExprF::Var(#var) }
}
// Free variable; interpolates as a rust variable
@@ -153,7 +153,7 @@ fn quote_expr(expr: &Expr<X, X>, ctx: &Context<Label, ()>) -> TokenStream {
// TODO: insert appropriate shifts ?
let v: TokenStream = s.parse().unwrap();
quote! { {
- let x: dhall_syntax::SubExpr<_, _> = #v.clone();
+ let x: dhall_syntax::SubExpr<_, _, _> = #v.clone();
x.unroll()
} }
}
diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index a186d19..c8a2425 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,19 +60,7 @@ pub enum Const {
/// The `Int` field is a DeBruijn index.
/// See dhall-lang/standard/semantics.md for details
#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct V<Label>(pub Label, pub usize);
-
-// This is only for the specific `Label` type, not generic
-impl From<Label> for V<Label> {
- fn from(x: Label) -> V<Label> {
- V(x, 0)
- }
-}
-impl<'a> From<&'a Label> for V<Label> {
- fn from(x: &'a Label) -> V<Label> {
- V(x.clone(), 0)
- }
-}
+pub struct Var<Label>(pub Label, pub usize);
// Definition order must match precedence order for
// pretty-printing to work correctly
@@ -137,44 +125,52 @@ pub enum Builtin {
TextShow,
}
-pub type ParsedExpr = SubExpr<X, Import>;
-pub type ResolvedExpr = SubExpr<X, X>;
+pub type ParsedExpr = SubExpr<Label, X, Import>;
+pub type ResolvedExpr = SubExpr<Label, X, X>;
pub type DhallExpr = ResolvedExpr;
// Each node carries an annotation. In practice it's either X (no annotation) or a Span.
#[derive(Debug)]
-pub struct SubExpr<Note, Embed>(Rc<(Expr<Note, Embed>, Option<Note>)>);
+pub struct SubExpr<VarLabel, Note, Embed>(
+ Rc<(Expr<VarLabel, Note, Embed>, Option<Note>)>,
+);
-impl<Note, Embed: PartialEq> std::cmp::PartialEq for SubExpr<Note, Embed> {
+impl<VarLabel: PartialEq, Note, Embed: PartialEq> std::cmp::PartialEq
+ for SubExpr<VarLabel, Note, Embed>
+{
fn eq(&self, other: &Self) -> bool {
self.0.as_ref().0 == other.0.as_ref().0
}
}
-impl<Note, Embed: Eq> std::cmp::Eq for SubExpr<Note, Embed> {}
+impl<VarLabel: Eq, Note, Embed: Eq> std::cmp::Eq
+ for SubExpr<VarLabel, Note, Embed>
+{
+}
-pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Embed>;
+pub type Expr<VarLabel, Note, Embed> =
+ ExprF<SubExpr<VarLabel, Note, Embed>, VarLabel, Embed>;
/// Syntax tree for expressions
// Having the recursion out of the enum definition enables writing
// much more generic code and improves pattern-matching behind
// smart pointers.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ExprF<SubExpr, Label, Embed> {
+pub enum ExprF<SubExpr, VarLabel, Embed> {
Const(Const),
/// `x`
/// `x@n`
- Var(V<Label>),
+ Var(Var<VarLabel>),
/// `λ(x : A) -> b`
- Lam(Label, SubExpr, SubExpr),
+ Lam(VarLabel, SubExpr, SubExpr),
/// `A -> B`
/// `∀(x : A) -> B`
- Pi(Label, SubExpr, SubExpr),
+ Pi(VarLabel, SubExpr, SubExpr),
/// `f a`
App(SubExpr, SubExpr),
/// `let x = r in e`
/// `let x : t = r in e`
- Let(Label, Option<SubExpr>, SubExpr, SubExpr),
+ Let(VarLabel, Option<SubExpr>, SubExpr, SubExpr),
/// `x : t`
Annot(SubExpr, SubExpr),
/// Built-in values
@@ -235,11 +231,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
visit_under_binder: impl FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
- ) -> Result<ExprF<SE2, L2, E2>, Err>
- where
- L: Ord,
- L2: Ord,
- {
+ ) -> Result<ExprF<SE2, L2, E2>, Err> {
self.visit(visitor::TraverseRefWithBindersVisitor {
visit_subexpr,
visit_under_binder,
@@ -253,11 +245,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
- ) -> Result<ExprF<SE2, L2, E2>, Err>
- where
- L: Ord,
- L2: Ord,
- {
+ ) -> Result<ExprF<SE2, L2, E2>, Err> {
self.visit(visitor::TraverseRefVisitor {
visit_subexpr,
visit_embed,
@@ -271,11 +259,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
mut map_under_binder: impl FnMut(&'a L, &'a SE) -> SE2,
map_embed: impl FnOnce(&'a E) -> E2,
mut map_label: impl FnMut(&'a L) -> L2,
- ) -> ExprF<SE2, L2, E2>
- where
- L: Ord,
- L2: Ord,
- {
+ ) -> ExprF<SE2, L2, E2> {
trivial_result(self.traverse_ref_with_special_handling_of_binders(
|x| Ok(map_subexpr(x)),
|l, x| Ok(map_under_binder(l, x)),
@@ -289,11 +273,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
mut map_subexpr: impl FnMut(&'a SE) -> SE2,
map_embed: impl FnOnce(&'a E) -> E2,
mut map_label: impl FnMut(&'a L) -> L2,
- ) -> ExprF<SE2, L2, E2>
- where
- L: Ord,
- L2: Ord,
- {
+ ) -> ExprF<SE2, L2, E2> {
trivial_result(self.traverse_ref(
|x| Ok(map_subexpr(x)),
|x| Ok(map_embed(x)),
@@ -306,7 +286,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
) -> Result<ExprF<SE2, L, E>, Err>
where
- L: Ord + Clone,
+ L: Clone,
E: Clone,
{
self.traverse_ref(
@@ -321,26 +301,31 @@ impl<SE, L, E> ExprF<SE, L, E> {
map_subexpr: impl Fn(&'a SE) -> SE2,
) -> ExprF<SE2, L, E>
where
- L: Ord + Clone,
+ L: Clone,
E: Clone,
{
self.map_ref(map_subexpr, E::clone, L::clone)
}
}
-impl<N, E> Expr<N, E> {
+impl<L, N, E> Expr<L, N, E> {
fn traverse_embed<E2, Err>(
&self,
visit_embed: impl FnMut(&E) -> Result<E2, Err>,
- ) -> Result<Expr<N, E2>, Err>
+ ) -> Result<Expr<L, N, E2>, Err>
where
+ L: Clone,
N: Clone,
{
self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed))
}
- fn map_embed<E2>(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr<N, E2>
+ fn map_embed<E2>(
+ &self,
+ mut map_embed: impl FnMut(&E) -> E2,
+ ) -> Expr<L, N, E2>
where
+ L: Clone,
N: Clone,
{
trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
@@ -348,52 +333,52 @@ impl<N, E> Expr<N, E> {
pub fn squash_embed<E2>(
&self,
- f: impl FnMut(&E) -> SubExpr<N, E2>,
- ) -> SubExpr<N, E2>
+ f: impl FnMut(&E) -> SubExpr<L, N, E2>,
+ ) -> SubExpr<L, N, E2>
where
+ L: Clone,
N: Clone,
{
trivial_result(self.visit(&mut visitor::SquashEmbedVisitor(f)))
}
}
-impl<E: Clone> Expr<X, E> {
- pub fn note_absurd<N>(&self) -> Expr<N, E> {
+impl<L: Clone, E: Clone> Expr<L, X, E> {
+ pub fn note_absurd<N>(&self) -> Expr<L, N, E> {
self.visit(&mut visitor::NoteAbsurdVisitor)
}
}
-impl<N: Clone> Expr<N, X> {
- pub fn embed_absurd<E>(&self) -> Expr<N, E> {
+impl<L: Clone, N: Clone> Expr<L, N, X> {
+ pub fn embed_absurd<E>(&self) -> Expr<L, N, E> {
self.visit(&mut visitor::EmbedAbsurdVisitor)
}
}
-impl<N, E> SubExpr<N, E> {
- pub fn as_ref(&self) -> &Expr<N, E> {
+impl<V, N, E> SubExpr<V, N, E> {
+ pub fn as_ref(&self) -> &Expr<V, N, E> {
&self.0.as_ref().0
}
- pub fn new(x: Expr<N, E>, n: N) -> Self {
+ pub fn new(x: Expr<V, N, E>, n: N) -> Self {
SubExpr(Rc::new((x, Some(n))))
}
- pub fn from_expr_no_note(x: Expr<N, E>) -> Self {
+ pub fn from_expr_no_note(x: Expr<V, N, E>) -> Self {
SubExpr(Rc::new((x, None)))
}
- pub fn unnote(&self) -> SubExpr<X, E>
+ pub fn unnote(&self) -> SubExpr<V, X, E>
where
+ V: Clone,
E: Clone,
{
SubExpr::from_expr_no_note(
self.as_ref().visit(&mut visitor::UnNoteVisitor),
)
}
-}
-impl<N: Clone, E> SubExpr<N, E> {
- pub fn rewrap<E2>(&self, x: Expr<N, E2>) -> SubExpr<N, E2>
+ pub fn rewrap<E2>(&self, x: Expr<V, N, E2>) -> SubExpr<V, N, E2>
where
N: Clone,
{
@@ -403,8 +388,9 @@ impl<N: Clone, E> SubExpr<N, E> {
pub fn traverse_embed<E2, Err>(
&self,
visit_embed: impl FnMut(&E) -> Result<E2, Err>,
- ) -> Result<SubExpr<N, E2>, Err>
+ ) -> Result<SubExpr<V, N, E2>, Err>
where
+ V: Clone,
N: Clone,
{
Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?))
@@ -413,8 +399,9 @@ impl<N: Clone, E> SubExpr<N, E> {
pub fn map_embed<E2>(
&self,
map_embed: impl FnMut(&E) -> E2,
- ) -> SubExpr<N, E2>
+ ) -> SubExpr<V, N, E2>
where
+ V: Clone,
N: Clone,
{
self.rewrap(self.as_ref().map_embed(map_embed))
@@ -423,8 +410,12 @@ impl<N: Clone, E> SubExpr<N, E> {
pub fn map_subexprs_with_special_handling_of_binders<'a>(
&'a self,
map_expr: impl FnMut(&'a Self) -> Self,
- map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self,
- ) -> Self {
+ map_under_binder: impl FnMut(&'a V, &'a Self) -> Self,
+ ) -> Self
+ where
+ V: Clone,
+ N: Clone,
+ {
match self.as_ref() {
ExprF::Embed(_) => SubExpr::clone(self),
// This calls ExprF::map_ref
@@ -432,7 +423,7 @@ impl<N: Clone, E> SubExpr<N, E> {
map_expr,
map_under_binder,
|_| unreachable!(),
- Label::clone,
+ V::clone,
)),
}
}
@@ -441,26 +432,34 @@ impl<N: Clone, E> SubExpr<N, E> {
/// capture by shifting variable indices
/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
/// for details
- pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub fn shift(&self, delta: isize, var: &Var<V>) -> Self
+ where
+ V: Clone + PartialEq,
+ N: Clone,
+ {
match self.as_ref() {
ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
_ => self.map_subexprs_with_special_handling_of_binders(
|e| e.shift(delta, var),
- |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
+ |x: &V, e| e.shift(delta, &var.shift(1, &Var::new(x.clone()))),
),
}
}
- pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
+ pub fn subst_shift(&self, var: &Var<V>, val: &Self) -> Self
+ where
+ V: Clone + PartialEq,
+ N: Clone,
+ {
match self.as_ref() {
ExprF::Var(v) if v == var => val.clone(),
ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
_ => self.map_subexprs_with_special_handling_of_binders(
|e| e.subst_shift(var, val),
- |x: &Label, e| {
+ |x: &V, e| {
e.subst_shift(
- &var.shift(1, &x.into()),
- &val.shift(1, &x.into()),
+ &var.shift(1, &Var::new(x.clone())),
+ &val.shift(1, &Var::new(x.clone())),
)
},
),
@@ -468,26 +467,26 @@ impl<N: Clone, E> SubExpr<N, E> {
}
}
-impl<N: Clone> SubExpr<N, X> {
- pub fn embed_absurd<T>(&self) -> SubExpr<N, T> {
+impl<L: Clone, N: Clone> SubExpr<L, N, X> {
+ pub fn embed_absurd<T>(&self) -> SubExpr<L, N, T> {
self.rewrap(self.as_ref().embed_absurd())
}
}
-impl<E: Clone> SubExpr<X, E> {
- pub fn note_absurd<N>(&self) -> SubExpr<N, E> {
+impl<L: Clone, E: Clone> SubExpr<L, X, E> {
+ pub fn note_absurd<N>(&self) -> SubExpr<L, N, E> {
SubExpr::from_expr_no_note(self.as_ref().note_absurd())
}
}
-impl<N, E> Clone for SubExpr<N, E> {
+impl<L, N, E> Clone for SubExpr<L, N, E> {
fn clone(&self) -> Self {
SubExpr(Rc::clone(&self.0))
}
}
// Should probably rename this
-pub fn rc<E>(x: Expr<X, E>) -> SubExpr<X, E> {
+pub fn rc<L, E>(x: Expr<L, X, E>) -> SubExpr<L, X, E> {
SubExpr::from_expr_no_note(x)
}
@@ -501,18 +500,35 @@ fn add_ui(u: usize, i: isize) -> usize {
}
}
-impl<Label: PartialEq + Clone> V<Label> {
- pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
- let V(x, n) = var;
- let V(y, m) = self;
+impl<L> Var<L> {
+ fn new(x: L) -> Self {
+ Var(x, 0)
+ }
+}
+impl<L: PartialEq + Clone> Var<L> {
+ pub fn shift(&self, delta: isize, var: &Var<L>) -> Self {
+ let Var(x, n) = var;
+ let Var(y, m) = self;
if x == y && n <= m {
- V(y.clone(), add_ui(*m, delta))
+ Var(y.clone(), add_ui(*m, delta))
} else {
- V(y.clone(), *m)
+ Var(y.clone(), *m)
}
}
}
+// This is only for the specific `Label` type, not generic
+impl From<Label> for Var<Label> {
+ fn from(x: Label) -> Var<Label> {
+ Var(x, 0)
+ }
+}
+impl<'a> From<&'a Label> for Var<Label> {
+ fn from(x: &'a Label) -> Var<Label> {
+ Var(x.clone(), 0)
+ }
+}
+
/// `shift` is used by both normalization and type-checking to avoid variable
/// capture by shifting variable indices
/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
@@ -520,9 +536,9 @@ impl<Label: PartialEq + Clone> V<Label> {
///
pub fn shift<N, E>(
delta: isize,
- var: &V<Label>,
- in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+ var: &Var<Label>,
+ in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
where
N: Clone,
{
@@ -531,8 +547,8 @@ where
pub fn shift0_multiple<N, E>(
deltas: &HashMap<Label, isize>,
- in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+ in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
where
N: Clone,
{
@@ -542,16 +558,15 @@ where
fn shift0_multiple_inner<N, E>(
ctx: &Context<Label, ()>,
deltas: &HashMap<Label, isize>,
- in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+ in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
where
N: Clone,
{
- use crate::ExprF::*;
match in_expr.as_ref() {
- Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
+ ExprF::Var(Var(y, m)) if ctx.lookup(y, *m).is_none() => {
let delta = deltas.get(y).unwrap_or(&0);
- in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
+ in_expr.rewrap(ExprF::Var(Var(y.clone(), add_ui(*m, *delta))))
}
_ => in_expr.map_subexprs_with_special_handling_of_binders(
|e| shift0_multiple_inner(ctx, deltas, e),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 83ccc1e..bdef553 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -8,7 +8,13 @@ use std::rc::Rc;
use dhall_generated_parser::{DhallParser, Rule};
-use crate::ExprF::*;
+use crate::ExprF::{
+ Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, Embed,
+ EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit,
+ OldOptionalLit, Pi, Projection, RecordLit, RecordType, SomeLit, TextLit,
+ UnionLit, UnionType,
+};
+
use crate::*;
// This file consumes the parse tree generated by pest and turns it into
@@ -16,10 +22,10 @@ use crate::*;
// their own crate because they are quite general and useful. For now they
// are here and hopefully you can figure out how they work.
-type ParsedExpr = Expr<Span, Import>;
-type ParsedSubExpr = SubExpr<Span, Import>;
-type ParsedText = InterpolatedText<SubExpr<Span, Import>>;
-type ParsedTextContents = InterpolatedTextContents<SubExpr<Span, Import>>;
+type ParsedExpr = Expr<Label, Span, Import>;
+type ParsedSubExpr = SubExpr<Label, Span, Import>;
+type ParsedText = InterpolatedText<ParsedSubExpr>;
+type ParsedTextContents = InterpolatedTextContents<ParsedSubExpr>;
pub type ParseError = pest::error::Error<Rule>;
@@ -504,17 +510,17 @@ make_parser! {
rule!(identifier<ParsedSubExpr> as expression; span; children!(
[variable(v)] => {
- spanned(span, Var(v))
+ spanned(span, ExprF::Var(v))
},
[builtin(e)] => e,
));
- rule!(variable<V<Label>>; children!(
+ rule!(variable<Var<Label>>; children!(
[label(l), natural_literal(idx)] => {
- V(l, idx)
+ Var(l, idx)
},
[label(l)] => {
- V(l, 0)
+ Var(l, 0)
},
));
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index e3b180b..9cc1b46 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,7 +3,9 @@ use itertools::Itertools;
use std::fmt::{self, Display};
/// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
+impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
+ for ExprF<SE, L, E>
+{
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
use crate::ExprF::*;
match self {
@@ -13,9 +15,10 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
BoolIf(a, b, c) => {
write!(f, "if {} then {} else {}", a, b, c)?;
}
- Pi(a, b, c) if &String::from(a) == "_" => {
- write!(f, "{} → {}", b, c)?;
- }
+ // TODO: arrow type
+ // Pi(a, b, c) if &String::from(a) == "_" => {
+ // write!(f, "{} → {}", b, c)?;
+ // }
Pi(a, b, c) => {
write!(f, "∀({} : {}) → {}", a, b, c)?;
}
@@ -124,21 +127,25 @@ enum PrintPhase {
// Wraps an Expr with a phase, so that phase selsction can be done
// separate from the actual printing
#[derive(Clone)]
-struct PhasedExpr<'a, S, A>(&'a SubExpr<S, A>, PrintPhase);
+struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
-impl<'a, S: Clone, A: Display + Clone> Display for PhasedExpr<'a, S, A> {
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
+ for PhasedExpr<'a, L, S, A>
+{
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
self.0.as_ref().fmt_phase(f, self.1)
}
}
-impl<'a, S: Clone, A: Display + Clone> PhasedExpr<'a, S, A> {
- fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, S, A> {
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
+ PhasedExpr<'a, L, S, A>
+{
+ fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
PhasedExpr(self.0, phase)
}
}
-impl<S: Clone, A: Display + Clone> Expr<S, A> {
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
fn fmt_phase(
&self,
f: &mut fmt::Formatter,
@@ -172,11 +179,12 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
// Annotate subexpressions with the appropriate phase, defaulting to Base
let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
Pi(a, b, c) => {
- if &String::from(&a) == "_" {
- Pi(a, b.phase(Operator), c)
- } else {
- Pi(a, b, c)
- }
+ // TODO: arrow type
+ // if &String::from(&a) == "_" {
+ // Pi(a, b.phase(Operator), c)
+ // } else {
+ Pi(a, b, c)
+ // }
}
Merge(a, b, c) => Merge(
a.phase(Import),
@@ -212,7 +220,9 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
}
}
-impl<S: Clone, A: Display + Clone> Display for SubExpr<S, A> {
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
+ for SubExpr<L, S, A>
+{
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
self.as_ref().fmt_phase(f, PrintPhase::Base)
}
@@ -474,9 +484,9 @@ impl Display for Scheme {
}
}
-impl<Label: Display> Display for V<Label> {
+impl<Label: Display> Display for Var<Label> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- let V(x, n) = self;
+ let Var(x, n) = self;
x.fmt(f)?;
if *n != 0 {
write!(f, "@{}", n)?;
diff --git a/dhall_syntax/src/visitor.rs b/dhall_syntax/src/visitor.rs
index 7fdf217..a8e5a8c 100644
--- a/dhall_syntax/src/visitor.rs
+++ b/dhall_syntax/src/visitor.rs
@@ -48,8 +48,6 @@ pub trait ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>: Sized {
impl<'a, T, Ret, SE1, L1, E1>
GenericVisitor<&'a ExprF<SE1, L1, E1>, Result<Ret, T::Error>> for T
where
- L1: Ord,
- T::L2: Ord,
T: ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>,
{
fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> Result<Ret, T::Error> {
@@ -69,31 +67,27 @@ where
})
}
fn btmap<'a, V, Ret, SE, L, E>(
- x: &'a BTreeMap<L, SE>,
+ x: &'a BTreeMap<Label, SE>,
mut v: V,
- ) -> Result<BTreeMap<V::L2, V::SE2>, V::Error>
+ ) -> Result<BTreeMap<Label, V::SE2>, V::Error>
where
- L: Ord,
- V::L2: Ord,
V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
{
x.iter()
- .map(|(k, x)| Ok((v.visit_label(k)?, v.visit_subexpr(x)?)))
+ .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
.collect()
}
fn btoptmap<'a, V, Ret, SE, L, E>(
- x: &'a BTreeMap<L, Option<SE>>,
+ x: &'a BTreeMap<Label, Option<SE>>,
mut v: V,
- ) -> Result<BTreeMap<V::L2, Option<V::SE2>>, V::Error>
+ ) -> Result<BTreeMap<Label, Option<V::SE2>>, V::Error>
where
- L: Ord,
- V::L2: Ord,
V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
{
x.iter()
.map(|(k, x)| {
Ok((
- v.visit_label(k)?,
+ k.clone(),
match x {
Some(x) => Some(v.visit_subexpr(x)?),
None => None,
@@ -104,9 +98,14 @@ where
}
let mut v = self;
- use crate::ExprF::*;
+ use crate::ExprF::{
+ Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit,
+ Embed, EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit,
+ NaturalLit, OldOptionalLit, Pi, Projection, RecordLit, RecordType,
+ SomeLit, TextLit, UnionLit, UnionType,
+ };
T::visit_resulting_exprf(match input {
- Var(V(l, n)) => Var(V(v.visit_label(l)?, *n)),
+ ExprF::Var(Var(l, n)) => ExprF::Var(Var(v.visit_label(l)?, *n)),
Lam(l, t, e) => {
let t = v.visit_subexpr(t)?;
let (l, e) = v.visit_binder(l, e)?;
@@ -150,20 +149,16 @@ where
RecordType(kts) => RecordType(btmap(kts, v)?),
RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
UnionType(kts) => UnionType(btoptmap(kts, v)?),
- UnionLit(k, x, kts) => UnionLit(
- v.visit_label(k)?,
- v.visit_subexpr(x)?,
- btoptmap(kts, v)?,
- ),
+ UnionLit(l, x, kts) => {
+ UnionLit(l.clone(), v.visit_subexpr(x)?, btoptmap(kts, v)?)
+ }
Merge(x, y, t) => Merge(
v.visit_subexpr(x)?,
v.visit_subexpr(y)?,
opt(t, |e| v.visit_subexpr(e))?,
),
- Field(e, l) => Field(v.visit_subexpr(e)?, v.visit_label(l)?),
- Projection(e, ls) => {
- Projection(v.visit_subexpr(e)?, vec(ls, |l| v.visit_label(l))?)
- }
+ Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
+ Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
Embed(a) => return v.visit_embed_squash(a),
})
}
@@ -314,8 +309,6 @@ where
impl<'a, T, SE1, SE2, L1, L2, E1, E2>
GenericVisitor<&'a ExprF<SE1, L1, E1>, ExprF<SE2, L2, E2>> for T
where
- L1: Ord,
- L2: Ord,
T: ExprFInFallibleVisitor<'a, SE1, SE2, L1, L2, E1, E2>,
{
fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> ExprF<SE2, L2, E2> {
@@ -337,8 +330,6 @@ where
SE: 'a,
L: 'a,
E: 'a,
- L: Ord,
- L2: Ord,
F1: FnMut(&'a SE) -> Result<SE2, Err>,
F2: FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
F4: FnOnce(&'a E) -> Result<E2, Err>,
@@ -377,8 +368,6 @@ where
SE: 'a,
L: 'a,
E: 'a,
- L: Ord,
- L2: Ord,
F1: FnMut(&'a SE) -> Result<SE2, Err>,
F3: FnOnce(&'a E) -> Result<E2, Err>,
F4: FnMut(&'a L) -> Result<L2, Err>,
@@ -398,10 +387,11 @@ where
pub struct TraverseEmbedVisitor<F1>(pub F1);
-impl<'a, 'b, N, E, E2, Err, F1>
- ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, Label, Label, E, E2>
+impl<'a, 'b, L, N, E, E2, Err, F1>
+ ExprFFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, N, E2>, L, L, E, E2>
for &'b mut TraverseEmbedVisitor<F1>
where
+ L: Clone + 'a,
N: Clone + 'a,
F1: FnMut(&E) -> Result<E2, Err>,
{
@@ -409,50 +399,48 @@ where
fn visit_subexpr(
&mut self,
- subexpr: &'a SubExpr<N, E>,
- ) -> Result<SubExpr<N, E2>, Self::Error> {
+ subexpr: &'a SubExpr<L, N, E>,
+ ) -> Result<SubExpr<L, N, E2>, Self::Error> {
Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?))
}
fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
(self.0)(embed)
}
- fn visit_label(&mut self, label: &'a Label) -> Result<Label, Self::Error> {
- Ok(Label::clone(label))
+ fn visit_label(&mut self, label: &'a L) -> Result<L, Self::Error> {
+ Ok(L::clone(label))
}
}
pub struct SquashEmbedVisitor<F1>(pub F1);
-impl<'a, 'b, N, E1, E2, F1>
- ExprFVeryGenericVisitor<'a, SubExpr<N, E2>, SubExpr<N, E1>, Label, E1>
+impl<'a, 'b, L, N, E1, E2, F1>
+ ExprFVeryGenericVisitor<'a, SubExpr<L, N, E2>, SubExpr<L, N, E1>, L, E1>
for &'b mut SquashEmbedVisitor<F1>
where
+ L: Clone + 'a,
N: Clone + 'a,
- F1: FnMut(&E1) -> SubExpr<N, E2>,
+ F1: FnMut(&E1) -> SubExpr<L, N, E2>,
{
type Error = X;
- type SE2 = SubExpr<N, E2>;
- type L2 = Label;
+ type SE2 = SubExpr<L, N, E2>;
+ type L2 = L;
type E2 = E2;
fn visit_subexpr(
&mut self,
- subexpr: &'a SubExpr<N, E1>,
+ subexpr: &'a SubExpr<L, N, E1>,
) -> Result<Self::SE2, Self::Error> {
Ok(subexpr.as_ref().visit(&mut **self)?)
}
- fn visit_label(
- &mut self,
- label: &'a Label,
- ) -> Result<Self::L2, Self::Error> {
- Ok(Label::clone(label))
+ fn visit_label(&mut self, label: &'a L) -> Result<Self::L2, Self::Error> {
+ Ok(L::clone(label))
}
fn visit_binder(
mut self,
- label: &'a Label,
- subexpr: &'a SubExpr<N, E1>,
+ label: &'a L,
+ subexpr: &'a SubExpr<L, N, E1>,
) -> Result<(Self::L2, Self::SE2), Self::Error> {
Ok((self.visit_label(label)?, self.visit_subexpr(subexpr)?))
}
@@ -460,7 +448,7 @@ where
fn visit_embed_squash(
self,
embed: &'a E1,
- ) -> Result<SubExpr<N, E2>, Self::Error> {
+ ) -> Result<SubExpr<L, N, E2>, Self::Error> {
Ok((self.0)(embed))
}
@@ -468,7 +456,7 @@ where
// Useful to change the result type, and/or avoid some loss of info
fn visit_resulting_exprf(
result: ExprF<Self::SE2, Self::L2, Self::E2>,
- ) -> Result<SubExpr<N, E2>, Self::Error> {
+ ) -> Result<SubExpr<L, N, E2>, Self::Error> {
// TODO: don't lose note
Ok(SubExpr::from_expr_no_note(result))
}
@@ -476,57 +464,69 @@ where
pub struct UnNoteVisitor;
-impl<'a, 'b, N, E>
- ExprFInFallibleVisitor<'a, SubExpr<N, E>, SubExpr<X, E>, Label, Label, E, E>
+impl<'a, 'b, L, N, E>
+ ExprFInFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, X, E>, L, L, E, E>
for &'b mut UnNoteVisitor
where
+ L: Clone + 'a,
E: Clone + 'a,
{
- fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, E>) -> SubExpr<X, E> {
+ fn visit_subexpr(
+ &mut self,
+ subexpr: &'a SubExpr<L, N, E>,
+ ) -> SubExpr<L, X, E> {
SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
}
fn visit_embed(self, embed: &'a E) -> E {
E::clone(embed)
}
- fn visit_label(&mut self, label: &'a Label) -> Label {
- Label::clone(label)
+ fn visit_label(&mut self, label: &'a L) -> L {
+ L::clone(label)
}
}
pub struct NoteAbsurdVisitor;
-impl<'a, 'b, N, E>
- ExprFInFallibleVisitor<'a, SubExpr<X, E>, SubExpr<N, E>, Label, Label, E, E>
+impl<'a, 'b, L, N, E>
+ ExprFInFallibleVisitor<'a, SubExpr<L, X, E>, SubExpr<L, N, E>, L, L, E, E>
for &'b mut NoteAbsurdVisitor
where
+ L: Clone + 'a,
E: Clone + 'a,
{
- fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X, E>) -> SubExpr<N, E> {
+ fn visit_subexpr(
+ &mut self,
+ subexpr: &'a SubExpr<L, X, E>,
+ ) -> SubExpr<L, N, E> {
SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
}
fn visit_embed(self, embed: &'a E) -> E {
E::clone(embed)
}
- fn visit_label(&mut self, label: &'a Label) -> Label {
- Label::clone(label)
+ fn visit_label(&mut self, label: &'a L) -> L {
+ L::clone(label)
}
}
pub struct EmbedAbsurdVisitor;
-impl<'a, 'b, N, E>
- ExprFInFallibleVisitor<'a, SubExpr<N, X>, SubExpr<N, E>, Label, Label, X, E>
+impl<'a, 'b, L, N, E>
+ ExprFInFallibleVisitor<'a, SubExpr<L, N, X>, SubExpr<L, N, E>, L, L, X, E>
for &'b mut EmbedAbsurdVisitor
where
+ L: Clone + 'a,
N: Clone + 'a,
{
- fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, X>) -> SubExpr<N, E> {
+ fn visit_subexpr(
+ &mut self,
+ subexpr: &'a SubExpr<L, N, X>,
+ ) -> SubExpr<L, N, E> {
subexpr.rewrap(subexpr.as_ref().visit(&mut **self))
}
fn visit_embed(self, embed: &'a X) -> E {
match *embed {}
}
- fn visit_label(&mut self, label: &'a Label) -> Label {
- Label::clone(label)
+ fn visit_label(&mut self, label: &'a L) -> L {
+ L::clone(label)
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 12:20:06 +0000