summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
m---------dhall-lang0
-rw-r--r--dhall/build.rs21
-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.rs20
-rw-r--r--dhall/src/phase/normalize.rs13
-rw-r--r--dhall/src/phase/typecheck.rs60
-rw-r--r--dhall/src/tests.rs1
-rw-r--r--dhall_generated_parser/build.rs1
-rw-r--r--dhall_generated_parser/src/dhall.pest.visibility3
-rw-r--r--dhall_syntax/src/core/expr.rs6
-rw-r--r--dhall_syntax/src/core/visitor.rs1
-rw-r--r--dhall_syntax/src/parser.rs12
-rw-r--r--dhall_syntax/src/printer.rs4
-rw-r--r--tests_buffer106
16 files changed, 146 insertions, 131 deletions
diff --git a/dhall-lang b/dhall-lang
-Subproject 9f259cd68870b912fbf2f2a08cd63dc3ccba9dc
+Subproject fb1c41ddec1d35dadd89a70780698e1a73e179b
diff --git a/dhall/build.rs b/dhall/build.rs
index b6df3d0..8b23dd9 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -94,8 +94,12 @@ fn main() -> std::io::Result<()> {
// Too slow in debug mode
path == "success/largeExpression"
// TODO: Inline headers
- || path == "success/unit/import/parenthesizeUsing"
|| path == "success/unit/import/inlineUsing"
+ || path == "success/unit/import/Headers"
+ || path == "success/unit/import/HeadersDoubleHash"
+ || path == "success/unit/import/HeadersDoubleHashPrecedence"
+ || path == "success/unit/import/HeadersHashPrecedence"
+ || path == "success/unit/import/HeadersInteriorHash"
// TODO: projection by expression
|| path == "success/recordProjectionByExpression"
|| path == "success/RecordProjectionByType"
@@ -117,6 +121,7 @@ fn main() -> std::io::Result<()> {
|| path == "success/largeExpression"
// TODO: Inline headers
|| path == "success/unit/import/inlineUsing"
+ || path == "success/unit/import/Headers"
// TODO: projection by expression
|| path == "success/recordProjectionByExpression"
|| path == "success/RecordProjectionByType"
@@ -140,13 +145,13 @@ fn main() -> std::io::Result<()> {
path.starts_with("failure/")
// Too slow in debug mode
|| path == "success/largeExpression"
- // Too much of a pain to implement; shouldn't make a difference
- // since lets disappear on normalization.
- || path == "success/multilet"
// See https://github.com/pyfisch/cbor/issues/109
|| path == "success/double"
+ || path == "success/unit/DoubleLitExponentNoDot"
+ || path == "success/unit/DoubleLitSecretelyInt"
// TODO: Inline headers
|| path == "success/unit/import/inlineUsing"
+ || path == "success/unit/import/Headers"
// TODO: projection by expression
|| path == "success/recordProjectionByExpression"
|| path == "success/RecordProjectionByType"
@@ -199,7 +204,7 @@ fn main() -> std::io::Result<()> {
|| path == "success/unit/EmptyToMap"
|| path == "success/unit/ToMap"
|| path == "success/unit/ToMapWithType"
- // Normalize field selection further by inspecting the argument
+ // TODO: Normalize field selection further by inspecting the argument
|| path == "success/simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0"
|| path == "success/simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1"
|| path == "success/simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection"
@@ -208,9 +213,12 @@ fn main() -> std::io::Result<()> {
|| path == "success/unit/RecursiveRecordMergeWithinFieldSelection0"
|| path == "success/unit/RecursiveRecordMergeWithinFieldSelection1"
|| path == "success/unit/RecursiveRecordMergeWithinFieldSelection2"
+ || path == "success/unit/RecursiveRecordMergeWithinFieldSelection3"
|| path == "success/unit/RightBiasedMergeWithinFieldSelection0"
|| path == "success/unit/RightBiasedMergeWithinFieldSelection1"
|| path == "success/unit/RightBiasedMergeWithinFieldSelection2"
+ || path == "success/unit/RightBiasedMergeWithinFieldSelection3"
+ || path == "success/unit/RightBiasedMergeEquivalentArguments"
},
)?;
@@ -229,7 +237,10 @@ fn main() -> std::io::Result<()> {
"Typecheck",
|path| {
false
+ // TODO: Enable imports in typecheck tests
|| path == "failure/importBoundary"
+ // Too slow
+ || path == "success/prelude"
// TODO: Inline headers
|| path == "failure/customHeadersUsingBoundVariable"
// TODO: projection by expression
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..f4a9cc1 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()))?
}
@@ -177,6 +178,19 @@ fn cbor_value_to_dhall(
let l = Label::from(l.as_str());
Field(x, l)
}
+ [U64(10), x, rest..] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let labels = rest
+ .iter()
+ .map(|s| match s {
+ String(s) => Ok(Label::from(s.as_str())),
+ _ => Err(DecodeError::WrongFormatError(
+ "projection".to_owned(),
+ )),
+ })
+ .collect::<Result<_, _>>()?;
+ Projection(x, labels)
+ }
[U64(11), Object(map)] => {
let map = cbor_map_to_dhall_opt_map(map)?;
UnionType(map)
@@ -211,6 +225,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 +522,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 +560,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..405677a 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -54,6 +54,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
}
(NaturalLit(0), b) => Ok((r, b.clone())),
(_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
+ _ if a == b => Ok((r, NaturalLit(0))),
_ => Err(()),
}
}
@@ -508,9 +509,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 +627,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 +647,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);
diff --git a/dhall_generated_parser/build.rs b/dhall_generated_parser/build.rs
index 74210bf..48605b6 100644
--- a/dhall_generated_parser/build.rs
+++ b/dhall_generated_parser/build.rs
@@ -67,6 +67,7 @@ fn main() -> std::io::Result<()> {
| merge ~ whsp1 ~ import_expression ~ whsp1 ~ import_expression ~ whsp ~ ^":" ~ whsp1 ~ application_expression
| empty_list_literal
| toMap ~ whsp1 ~ import_expression ~ whsp ~ ^":" ~ whsp1 ~ application_expression
+ | assert ~ whsp ~ ^":" ~ whsp1 ~ expression
| annotated_expression
}}"#
)?;
diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility
index de6dc8d..44a52c1 100644
--- a/dhall_generated_parser/src/dhall.pest.visibility
+++ b/dhall_generated_parser/src/dhall.pest.visibility
@@ -46,6 +46,7 @@ missing
NaN
Some_
toMap
+assert
# keyword
builtin
Optional
@@ -85,6 +86,7 @@ Location
# Text_show
# combine
# combine_types
+# equivalent
# prefer
lambda
forall
@@ -154,6 +156,7 @@ combine_types_expression
times_expression
equal_expression
not_equal_expression
+equivalent_expression
application_expression
first_application_expression
# import_expression
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index b293357..6522cb1 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -44,7 +44,7 @@ impl From<NaiveDouble> for f64 {
}
/// Constants for a pure type system
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
pub enum Const {
Type,
Kind,
@@ -99,6 +99,8 @@ pub enum BinOp {
BoolEQ,
/// `x != y`
BoolNE,
+ /// x === y
+ Equivalence,
}
/// Built-ins
@@ -175,6 +177,8 @@ pub enum ExprF<SubExpr, Embed> {
Let(Label, Option<SubExpr>, SubExpr, SubExpr),
/// `x : t`
Annot(SubExpr, SubExpr),
+ /// `assert : t`
+ Assert(SubExpr),
/// Built-in values
Builtin(Builtin),
// Binary operations
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 68ad956..18f76d9 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -148,6 +148,7 @@ where
),
Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
+ Assert(e) => Assert(v.visit_subexpr(e)?),
Embed(a) => return v.visit_embed_squash(a),
})
}
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 72dfcdd..9ae6dc8 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -311,6 +311,7 @@ fn can_be_shortcutted(rule: Rule) -> bool {
| times_expression
| equal_expression
| not_equal_expression
+ | equivalent_expression
| application_expression
| first_application_expression
| selector_expression
@@ -744,6 +745,7 @@ make_parser! {
token_rule!(forall<()>);
token_rule!(arrow<()>);
token_rule!(merge<()>);
+ token_rule!(assert<()>);
token_rule!(if_<()>);
token_rule!(in_<()>);
@@ -777,6 +779,9 @@ make_parser! {
[merge(()), expression(x), expression(y), expression(z)] => {
spanned(span, Merge(x, y, Some(z)))
},
+ [assert(()), expression(x)] => {
+ spanned(span, Assert(x))
+ },
[expression(e)] => e,
));
@@ -875,6 +880,13 @@ make_parser! {
rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
},
));
+ rule!(equivalent_expression<ParsedSubExpr> as expression; children!(
+ [expression(e)] => e,
+ [expression(first), expression(rest)..] => {
+ let o = crate::BinOp::Equivalence;
+ rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
+ },
+ ));
rule!(annotated_expression<ParsedSubExpr> as expression; span; children!(
[expression(e)] => e,
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 1d6c113..70b224e 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -44,6 +44,9 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
Annot(a, b) => {
write!(f, "{} : {}", a, b)?;
}
+ Assert(a) => {
+ write!(f, "assert : {}", a)?;
+ }
ExprF::BinOp(op, a, b) => {
write!(f, "{} {} {}", a, op, b)?;
}
@@ -286,6 +289,7 @@ impl Display for BinOp {
ImportAlt => "?",
RightBiasedRecordMerge => "⫽",
ListAppend => "#",
+ Equivalence => "≡",
})
}
}
diff --git a/tests_buffer b/tests_buffer
index ca578e4..c6366ba 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -2,90 +2,15 @@ parser:
./a%20b
./"a%20b"
text interpolation and escapes
-remove `double`
-remove imports/parenthesizeUsing
-remove multilet
-selection by expression unit tests
-split aslocation test into actual unit tests
+projection by expression unit tests
success/
- imports/
- Missing missing
- Headers https://example.com/foo using ./headers
- HeadersInteriorHash https://example.com/foo using (./headers sha256:0000000000000000000000000000000000000000000000000000000000000000)
- HeadersExteriorHash (https://example.com/foo using ./headers) sha256:0000000000000000000000000000000000000000000000000000000000000000
- HeadersHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000
- HeadersDoubleHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000 sha256:1111111111111111111111111111111111111111111111111111111111111111
- DoubleLitPositive 1.23
- DoubleLitNegative -1.23
- DoubleLitExponent 1.23e4
- DoubleLitExponentNoDot 1e4
- DoubleLitExponentNegative 1.23e-4
- DoubleLitInfinity Infinity
- DoubleLitNegInfinity -Infinity
- DoubleLitNaN NaN
- DoubleLitSecretelyInt 1.0
- DoubleLitZero 0.0
- BuiltinListBuild List/Build
- FunctionApplicationOneArg f x
- FunctionApplicationMultipleArgs f x y z
- Annotation x : T
- ListLitNonEmpty [x, y]
- ListLitNonEmptyAnnotated [x, y] : List T
- OptionalLitEmpty []: Optional T
- OptionalLitNonEmpty [x]: Optional T
- Field r.x
- FieldBuiltinName r.List
- FieldQuoted r.`x`
- Projection r.{x, y, z}
- Let let x: T = v in e
- LetNested let x: T = v in let y: U = w in e
- LetMulti let x: T = v let y: U = w in e
- LambdaUnicode λ(x : T) -> y
- FunctionTypePi forall(x: T) -> U
- FunctionTypePiUnicode ∀(x: T) -> U
- FunctionTypePiNested forall(x: T) -> ∀(y: U) -> V
- FunctionTypePiUnderscore forall(_: T) -> U
- FunctionTypeArrow T -> U
- RecordLit { x = 1, y = 2 }
- RecordType { x: T, y: U }
operators/
- ImportAlt x ? y
- ImportAltAssoc w ? x ? y ? z
- BoolOr x || y
- BoolOrAssoc w || x || y || z
- NaturalPlus x + y
- NaturalPlusAssoc w + x + y + z
- TextAppend x ++ y
- TextAppendAssoc w ++ x ++ y ++ z
- ListAppend x # y
- ListAppendAssoc w # x # y # z
- BoolAnd x && y
- BoolAndAssoc w && x && y && z
- NaturalTimes x * y
- NaturalTimesAssoc w * x * y * z
- BoolEQ x == y
- BoolEQAssoc w == x == y == z
- BoolNE x != y
- BoolNEAssoc w != x != y != z
- RecursiveRecordMerge x //\\ y
- RecursiveRecordMergeAssoc w //\\ x //\\ y //\\ z
- RecursiveRecordTypeMerge x /\ y
- RecursiveRecordTypeMergeAssoc w /\ x /\ y /\ z
- RightBiasedRecordMerge x // y
- RightBiasedRecordMergeAssoc w // x // y // z
- RecursiveRecordMergeUnicode x ∧ y
- RecursiveRecordMergeUnicodeAssoc w ∧ x /\ y ∧ z
- RightBiasedRecordMergeUnicode x ⫽ y
- RightBiasedRecordMergeUnicodeAssoc w ⫽ x // y ⫽ z
- RecursiveRecordTypeMergeUnicode x ⩓ y
- RecursiveRecordTypeMergeUnicodeAssoc w ⩓ x //\\ y ⩓ z
PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o
PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n
- PrecedenceNat a + b * d + e f * (g + h)
- PrecedenceBool a && b || c d == e || f != g && h || i
- PrecedenceRecord a // b c /\ d ⫽ e.{x} ∧ f
+ LetNoAnnot let x = y in e
+ LetAnnot let x: T = y in e
failure/
- ProjectionByExpressionNeedsParens r.{ x: T }
+ AssertNoAnnotation assert
binary decoding:
decode old-style optional literals ?
@@ -99,39 +24,22 @@ failure/
normalization:
variables across import boundaries
-Text/show ""
-Double/show -1.5e-10
+ Text/show ""
TextLitNested1 "${""}${x}"
TextLitNested2 "${"${x}"}"
TextLitNested3 "${"${""}"}${x}"
- EquivalenceDouble if b then NaN else NaN
- EquivalenceAlpha if b then \(x: T) -> x else \(y: T) -> y
typecheck:
something that involves destructuring a recordtype after merge
add some of the more complicated Prelude tests back, like List/enumerate
failure on old-style optional literal
-success/
- MergeEmptyAlternative merge { x = 1 } < x >.x
- MergeTrickyShadowing let _ = Bool in merge {_ = \(x: _) -> x} (<_: Bool>._ True)
- EquivalenceAlpha \(TODO: forall(x: Type) -> x) -> TODO : forall(y: Type) -> y
failure/
- MergeEmptyNeedsDirectAnnotation1 \(x: <>) -> (merge {=} x) : Bool
- MergeEmptyNeedsDirectAnnotation2 \(x: <>) -> let y: Bool = merge {=} x in 1
- MergeBoolIsNotUnion merge x True
- MergeOptionalIsNotUnion merge x (Some 1)
- MergeMissingHandler1 merge {=} < x >.x
- MergeMissingHandler2 merge {x=...,} <x|y>.x
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x
merge {x=...,y=...} <x>.x
merge {x=...,y=...} <x:T>.x
- MergeHandlerFreeVar merge { x = None } < x = Bool >
- UnionTypeDuplicateVariants1 <x, x>
- UnionTypeDuplicateVariants2 <x, x:T>
- UnionLitDuplicateVariants <x=1|x:T>
- RecordLitDuplicateFields { x: T, x: T }
- EquivalenceAlphaTrap \(TODO: forall(_: Type) -> _) -> TODO : forall(x: Type) -> _
+ MergeBoolIsNotUnion merge x True
+ MergeOptionalIsNotUnion merge x (Some 1)
equivalence:
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 04:32:10 +0000