diff --git a/cli-impl/src/test/resources/negative/ExprTyckError.txt b/cli-impl/src/test/resources/negative/ExprTyckError.txt index 44f3bb8299..66a7b99fcb 100644 --- a/cli-impl/src/test/resources/negative/ExprTyckError.txt +++ b/cli-impl/src/test/resources/negative/ExprTyckError.txt @@ -46,7 +46,7 @@ In file $FILE:2:19 -> │ ╰──────╯ Error: The following abstraction is not good: - \ x ⇒ x + fn x ⇒ x because the type being expected is not a Pi/Path type, but instead: Type 0 @@ -225,11 +225,11 @@ In file $FILE:3:4 -> Error: The following application is not good: match a { - | _ ⇒ \ x ⇒ x + | _ ⇒ fn x ⇒ x } 1 because the type of what you applied is not a Pi/Path type, but instead: 2 error(s), 0 warning(s). diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt index 85c4828312..c2ded0f29a 100644 --- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt +++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt @@ -281,7 +281,7 @@ In file $FILE:11:12 -> │ ╰───────────────────────────╯ Error: Cannot check the expression - pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _) + pmap (fn _ ⇒ x :> _) (++-assoc' _ _ _) of type (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m o _ ys zs) diff --git a/cli-impl/src/test/resources/shared/src/data/sum/base.aya b/cli-impl/src/test/resources/shared/src/data/sum/base.aya index 79e2b1e74f..1da8af224c 100644 --- a/cli-impl/src/test/resources/shared/src/data/sum/base.aya +++ b/cli-impl/src/test/resources/shared/src/data/sum/base.aya @@ -11,7 +11,7 @@ def Sum-rec (P : Type) (lrec : A -> P) (rrec : B -> P) - : P => Sum-ind e (fn _e => P) (fn a _p => lrec a) (fn b _p => rrec b) + : P => Sum-ind e (fn _ => P) (fn a, _ => lrec a) (fn b, _ => rrec b) def Sum-ind (e : Sum A B) diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya b/cli-impl/src/test/resources/shared/src/relation/binary/path.aya index d5f6007a33..a826e4e9ef 100644 --- a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya +++ b/cli-impl/src/test/resources/shared/src/relation/binary/path.aya @@ -8,7 +8,7 @@ def refl {a : A} : a = a => \i => a def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \i => f (p i) def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl -def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i +def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i, a => p a i def pmapd {A : I -> Type} (B : ∀ i -> A i -> Type) (f : ∀ i -> ∀ (a : A i) -> B i a) {a b : _} (p : Path A a b) diff --git a/cli-impl/src/test/resources/success/src/PLFA.aya b/cli-impl/src/test/resources/success/src/PLFA.aya index f258bc4341..e2b38d301b 100644 --- a/cli-impl/src/test/resources/success/src/PLFA.aya +++ b/cli-impl/src/test/resources/success/src/PLFA.aya @@ -12,7 +12,7 @@ def deMorgan-law => Fn (A B : Type) -> (neg (Sig (neg A) ** (neg B))) -> Sum A B @suppress(MostGeneralSolution) def LEM=>deMorgan-law (lem : LEM) : deMorgan-law => - fn tyA tyB np => + fn tyA, tyB, np => Sum-rec (lem tyA) _ (fn A => A) @@ -23,7 +23,7 @@ def LEM=>deMorgan-law (lem : LEM) : deMorgan-law => (fn ¬B => exfalso (np (¬A, ¬B)))) def deMorgan-law=>imply-as-lor (dml : deMorgan-law) : imply-as-lor => - fn tyA tyB f => + fn tyA, tyB, f => dml (neg tyA) tyB (fn p => p.1 (fn A => exfalso (p.2 (f A)))) def imply-as-lor=>LEM (ial : imply-as-lor) : LEM => @@ -32,7 +32,7 @@ def imply-as-lor=>LEM (ial : imply-as-lor) : LEM => @suppress(MostGeneralSolution) def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law => // f : ((A -> B) -> A) - fn tyA tyB f => Sum-rec + fn tyA, tyB, f => Sum-rec (imply-as-lor=>LEM ial tyA) _ (fn A => A) @@ -40,7 +40,7 @@ def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law => @suppress(MostGeneralSolution) def peirce-law=>double-neg-elim (pl : peirce-law) : double-neg-elim => - fn tyA ¬¬A => + fn tyA, ¬¬A => pl tyA Empty (fn ¬A => exfalso (¬¬A ¬A)) @suppress(MostGeneralSolution) diff --git a/cli-impl/src/test/resources/success/src/Pattern.aya b/cli-impl/src/test/resources/success/src/Pattern.aya index 35a0beb245..6980139943 100644 --- a/cli-impl/src/test/resources/success/src/Pattern.aya +++ b/cli-impl/src/test/resources/success/src/Pattern.aya @@ -53,5 +53,5 @@ module PullRequest1268 { // unpi: D d0 -> d1 @suppress(LocalShadow) def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a, b - | a => fn b D => id D + | a => fn b, D => id D } diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java index 15b9d70de9..b5bad20143 100644 --- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java +++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java @@ -115,7 +115,6 @@ yield visitConcreteCalls(assoc, yield checkParen(outer, visitLambda(dummyCls), Outer.BinOp); } - // TODO case Expr.IrrefutableLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp); case Expr.Hole expr -> { if (!expr.explicit()) yield Doc.symbol(Constants.ANONYMOUS_PREFIX); @@ -492,13 +491,6 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep( private @NotNull Doc visitLambda(@NotNull Pattern.Clause clause) { var prelude = MutableList.of(LAMBDA); prelude.append(clause(clause)); - var body = clause.expr.get().data(); - - if (!(body instanceof Expr.Hole hole && !hole.explicit())) { - prelude.append(FN_DEFINED_AS); - prelude.append(term(Outer.Free, body)); - } - return Doc.sep(prelude); } } diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java index 2e9c4f0948..94f9bfad4a 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java @@ -30,7 +30,13 @@ public sealed interface Pattern extends AyaDocile { void forEach(@NotNull PosedConsumer<@NotNull Pattern> f); interface Salt { } + + /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.IrrefutableLam] in desugarer. + /// + /// @see Pattern.Bind + /// @see Pattern.CalmFace interface Refutable { + /// Returns the [LocalVar] this [Pattern] introduced, with [SourcePos] {@param pos} if it doesn't have one. @NotNull LocalVar toLocalVar(@NotNull SourcePos pos); }