From 00c5b497446d5415c36bfda5ebc0413da9d086dd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 8 Aug 2019 19:27:50 +0200 Subject: Upstream a bunch of tests See https://github.com/dhall-lang/dhall-lang/pull/698 --- tests_buffer | 105 ++++------------------------------------------------------- 1 file changed, 6 insertions(+), 99 deletions(-) diff --git a/tests_buffer b/tests_buffer index ca578e4..4f8a375 100644 --- a/tests_buffer +++ b/tests_buffer @@ -2,90 +2,13 @@ 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 failure/ - ProjectionByExpressionNeedsParens r.{ x: T } + AssertNoAnnotation assert binary decoding: decode old-style optional literals ? @@ -99,39 +22,23 @@ failure/ normalization: variables across import boundaries -Text/show "" -Double/show -1.5e-10 + Text/show "" + Double/show -1.5e-10 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 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 merge {x=...,y=...} .x - MergeHandlerFreeVar merge { x = None } < x = Bool > - UnionTypeDuplicateVariants1 - UnionTypeDuplicateVariants2 - UnionLitDuplicateVariants - RecordLitDuplicateFields { x: T, x: T } - EquivalenceAlphaTrap \(TODO: forall(_: Type) -> _) -> TODO : forall(x: Type) -> _ + MergeBoolIsNotUnion merge x True + MergeOptionalIsNotUnion merge x (Some 1) equivalence: -- cgit v1.2.3 From 071ba528cd8c6a222be345ddec7560bb45cca6be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 8 Aug 2019 19:33:07 +0200 Subject: Add support for dependent types --- dhall-lang | 2 +- dhall/build.rs | 5 +- dhall/src/core/thunk.rs | 4 ++ dhall/src/core/value.rs | 19 +++++++- dhall/src/error/mod.rs | 6 ++- dhall/src/phase/binary.rs | 7 +++ dhall/src/phase/normalize.rs | 12 +++-- dhall/src/phase/typecheck.rs | 60 ++++++++++++++++-------- dhall/src/tests.rs | 1 + dhall_generated_parser/build.rs | 1 + dhall_generated_parser/src/dhall.pest.visibility | 3 ++ dhall_syntax/src/core/expr.rs | 6 ++- dhall_syntax/src/core/visitor.rs | 1 + dhall_syntax/src/parser.rs | 12 +++++ dhall_syntax/src/printer.rs | 4 ++ 15 files changed, 114 insertions(+), 29 deletions(-) diff --git a/dhall-lang b/dhall-lang index 9f259cd..bf9783f 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit 9f259cd68870b912fbf2f2a08cd63dc3ccba9dc3 +Subproject commit bf9783fc4298d5d54897af1631d677b05dd19db5 diff --git a/dhall/build.rs b/dhall/build.rs index b6df3d0..c05df0d 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -199,7 +199,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" @@ -229,7 +229,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), RecordLit(HashMap), @@ -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>), + Equivalence(TypeThunk, TypeThunk), // Invariant: this must not contain a value captured by one of the variants above. PartialExpr(ExprF), } @@ -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::>()?, ), + 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 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::>()?, ))) } + [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> { 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::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) -> 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 { - 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 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 { Let(Label, Option, 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 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 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 Display for ExprF { 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 => "≡", }) } } -- cgit v1.2.3 From 4d94c3bbf955c5c32cee0651820484c4e4b6cd90 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 8 Aug 2019 19:45:52 +0200 Subject: Update dhall-lang submodule --- dhall-lang | 2 +- dhall/build.rs | 3 +++ dhall/src/phase/normalize.rs | 1 + 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/dhall-lang b/dhall-lang index bf9783f..9729d89 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit bf9783fc4298d5d54897af1631d677b05dd19db5 +Subproject commit 9729d8939a6c79adf9a26dd20978fba6ec39bbec diff --git a/dhall/build.rs b/dhall/build.rs index c05df0d..bcb5d1c 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -208,9 +208,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" }, )?; diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index ecad063..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) -> Value { } (NaturalLit(0), b) => Ok((r, b.clone())), (_, NaturalLit(0)) => Ok((r, NaturalLit(0))), + _ if a == b => Ok((r, NaturalLit(0))), _ => Err(()), } } -- cgit v1.2.3 From 80c8d87db595c91293af75d710464ac5379c7e28 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 10 Aug 2019 22:48:21 +0200 Subject: Update dhall-lang submodule --- dhall-lang | 2 +- dhall/build.rs | 13 +++++++++---- dhall/src/phase/binary.rs | 13 +++++++++++++ tests_buffer | 3 ++- 4 files changed, 25 insertions(+), 6 deletions(-) diff --git a/dhall-lang b/dhall-lang index 9729d89..fb1c41d 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit 9729d8939a6c79adf9a26dd20978fba6ec39bbec +Subproject commit fb1c41ddec1d35dadd89a70780698e1a73e179bd diff --git a/dhall/build.rs b/dhall/build.rs index bcb5d1c..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" diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 719b1c7..f4a9cc1 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -178,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::>()?; + Projection(x, labels) + } [U64(11), Object(map)] => { let map = cbor_map_to_dhall_opt_map(map)?; UnionType(map) diff --git a/tests_buffer b/tests_buffer index 4f8a375..c6366ba 100644 --- a/tests_buffer +++ b/tests_buffer @@ -7,6 +7,8 @@ success/ operators/ 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 + LetNoAnnot let x = y in e + LetAnnot let x: T = y in e failure/ AssertNoAnnotation assert @@ -23,7 +25,6 @@ failure/ normalization: variables across import boundaries Text/show "" - Double/show -1.5e-10 TextLitNested1 "${""}${x}" TextLitNested2 "${"${x}"}" TextLitNested3 "${"${""}"}${x}" -- cgit v1.2.3