summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/core/thunk.rs4
-rw-r--r--dhall/src/core/value.rs19
-rw-r--r--dhall/src/error/mod.rs6
-rw-r--r--dhall/src/phase/binary.rs7
-rw-r--r--dhall/src/phase/normalize.rs12
-rw-r--r--dhall/src/phase/typecheck.rs60
-rw-r--r--dhall/src/tests.rs1
7 files changed, 83 insertions, 26 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 5c569e1..5bc25f2 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -221,6 +221,10 @@ impl TypeThunk {
self.0.to_type()
}
+ pub fn to_typed(&self) -> Typed {
+ self.0.clone()
+ }
+
pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index d7b9149..26568b5 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,7 +47,7 @@ pub enum Value {
DoubleLit(NaiveDouble),
EmptyOptionalLit(TypeThunk),
NEOptionalLit(Thunk),
- // EmptyListLit(t) means `[] : List t`
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
EmptyListLit(TypeThunk),
NEListLit(Vec<Thunk>),
RecordLit(HashMap<Label, Thunk>),
@@ -58,6 +58,7 @@ pub enum Value {
// Invariant: this must not contain interpolations that are themselves TextLits, and
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Thunk>>),
+ Equivalence(TypeThunk, TypeThunk),
// Invariant: this must not contain a value captured by one of the variants above.
PartialExpr(ExprF<Thunk, X>),
}
@@ -196,6 +197,11 @@ impl Value {
.collect(),
))
}
+ Value::Equivalence(x, y) => rc(ExprF::BinOp(
+ dhall_syntax::BinOp::Equivalence,
+ x.normalize_to_expr_maybe_alpha(alpha),
+ y.normalize_to_expr_maybe_alpha(alpha),
+ )),
Value::PartialExpr(e) => {
rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
}
@@ -282,6 +288,10 @@ impl Value {
}
}
}
+ Value::Equivalence(x, y) => {
+ x.normalize_mut();
+ y.normalize_mut();
+ }
Value::PartialExpr(e) => {
// TODO: need map_mut_simple
e.map_ref_simple(|v| {
@@ -418,6 +428,9 @@ impl Shift for Value {
})
.collect::<Result<_, _>>()?,
),
+ Value::Equivalence(x, y) => {
+ Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+ }
Value::PartialExpr(e) => Value::PartialExpr(
e.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
@@ -533,6 +546,10 @@ impl Subst<Typed> for Value {
})
.collect(),
),
+ Value::Equivalence(x, y) => Value::Equivalence(
+ x.subst_shift(var, val),
+ y.subst_shift(var, val),
+ ),
}
}
}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index a0ee30a..3c00017 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -68,7 +68,6 @@ pub(crate) enum TypeMessage {
MissingRecordField(Label, Typed),
MissingUnionField(Label, Normalized),
BinOpTypeMismatch(BinOp, Typed),
- NoDependentTypes(Normalized, Normalized),
InvalidTextInterpolation(Typed),
Merge1ArgMustBeRecord(Typed),
Merge2ArgMustBeUnion(Typed),
@@ -86,7 +85,10 @@ pub(crate) enum TypeMessage {
RecordTypeMergeRequiresRecordType(Type),
RecordTypeMismatch(Type, Type, Type, Type),
UnionTypeDuplicateField,
- // Unimplemented,
+ EquivalenceArgumentMustBeTerm(bool, Typed),
+ EquivalenceTypeMismatch(Typed, Typed),
+ AssertMismatch(Typed, Typed),
+ AssertMustTakeEquivalence,
}
impl TypeError {
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 5e7eb40..719b1c7 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -119,6 +119,7 @@ fn cbor_value_to_dhall(
9 => RightBiasedRecordMerge,
10 => RecursiveRecordTypeMerge,
11 => ImportAlt,
+ 12 => Equivalence,
_ => {
Err(DecodeError::WrongFormatError("binop".to_owned()))?
}
@@ -211,6 +212,10 @@ fn cbor_value_to_dhall(
.collect::<Result<_, _>>()?,
)))
}
+ [U64(19), t] => {
+ let t = cbor_value_to_dhall(&t)?;
+ Assert(t)
+ }
[U64(24), hash, U64(mode), U64(scheme), rest..] => {
let mode = match mode {
0 => ImportMode::Code,
@@ -504,6 +509,7 @@ where
)
}
Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
+ Assert(x) => ser_seq!(ser; tag(19), expr(x)),
SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
EmptyListLit(x) => match x.as_ref() {
App(f, a) => match f.as_ref() {
@@ -541,6 +547,7 @@ where
RightBiasedRecordMerge => 9,
RecursiveRecordTypeMerge => 10,
ImportAlt => 11,
+ Equivalence => 12,
};
ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 395cf28..ecad063 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -508,9 +508,9 @@ where
fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
use BinOp::{
- BoolAnd, BoolEQ, BoolNE, BoolOr, ListAppend, NaturalPlus, NaturalTimes,
- RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge,
- TextAppend,
+ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
+ NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
+ RightBiasedRecordMerge, TextAppend,
};
use Value::{
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
@@ -626,6 +626,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
Ret::Value(RecordType(kvs))
}
+ (Equivalence, _, _) => Ret::Value(Value::Equivalence(
+ TypeThunk::from_thunk(x.clone()),
+ TypeThunk::from_thunk(y.clone()),
+ )),
+
_ => return None,
})
}
@@ -641,6 +646,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
ExprF::Embed(_) => unreachable!(),
ExprF::Var(_) => unreachable!(),
ExprF::Annot(x, _) => Ret::Thunk(x),
+ ExprF::Assert(_) => Ret::Expr(expr),
ExprF::Lam(x, t, e) => {
Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 2e4642c..297a096 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -60,18 +60,7 @@ fn tck_pi_type(
}
};
- let k = match function_check(ka, kb) {
- Ok(k) => k,
- Err(()) => {
- return Err(TypeError::new(
- ctx,
- NoDependentTypes(
- tx.to_normalized(),
- te.get_type()?.to_normalized(),
- ),
- ))
- }
- };
+ let k = function_check(ka, kb);
Ok(Typed::from_thunk_and_type(
Value::Pi(x.into(), TypeThunk::from_type(tx), TypeThunk::from_type(te))
@@ -164,14 +153,13 @@ fn tck_union_type(
))
}
-fn function_check(a: Const, b: Const) -> Result<Const, ()> {
- use dhall_syntax::Const::*;
- match (a, b) {
- (_, Type) => Ok(Type),
- (Kind, Kind) => Ok(Kind),
- (Sort, Sort) => Ok(Sort),
- (Sort, Kind) => Ok(Sort),
- _ => Err(()),
+fn function_check(a: Const, b: Const) -> Const {
+ use dhall_syntax::Const::Type;
+ use std::cmp::max;
+ if b == Type {
+ Type
+ } else {
+ max(a, b)
}
}
@@ -403,6 +391,19 @@ fn type_last_layer(
);
Ok(RetTypeOnly(x.get_type()?.into_owned()))
}
+ Assert(t) => {
+ match t.to_value() {
+ Value::Equivalence(x, y) if x == y => {}
+ Value::Equivalence(x, y) => {
+ return Err(mkerr(AssertMismatch(
+ x.to_typed(),
+ y.to_typed(),
+ )))
+ }
+ _ => return Err(mkerr(AssertMustTakeEquivalence)),
+ }
+ Ok(RetTypeOnly(t.to_type()))
+ }
BoolIf(x, y, z) => {
ensure_equal!(
x.get_type()?,
@@ -807,6 +808,24 @@ fn type_last_layer(
Ok(RetTypeOnly(l.get_type()?.into_owned()))
}
+ BinOp(Equivalence, l, r) => {
+ ensure_simple_type!(
+ l.get_type()?,
+ mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())),
+ );
+ ensure_simple_type!(
+ r.get_type()?,
+ mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())),
+ );
+
+ ensure_equal!(
+ l.get_type()?,
+ r.get_type()?,
+ mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()))
+ );
+
+ Ok(RetTypeOnly(Type::from_const(dhall_syntax::Const::Type)))
+ }
BinOp(o, l, r) => {
let t = builtin_to_type(match o {
BoolAnd => Bool,
@@ -821,6 +840,7 @@ fn type_last_layer(
RecursiveRecordMerge => unreachable!(),
RecursiveRecordTypeMerge => unreachable!(),
ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
+ Equivalence => unreachable!(),
})?;
ensure_equal!(
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 9784eec..15bc97a 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -107,6 +107,7 @@ pub fn run_test(
match feature {
Parser => {
+ // This exercices both parsing and binary decoding
// Compare parse/decoded
let expected_file_path = base_path + "B.dhallb";
let expected_file_path = PathBuf::from(&expected_file_path);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:13:25 +0000