Skip to content

Commit

Permalink
parse: use compute constants! IDEA is so good!
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed May 31, 2024
1 parent e0f5305 commit b9d2255
Showing 1 changed file with 48 additions and 48 deletions.
96 changes: 48 additions & 48 deletions cli-impl/src/test/java/org/aya/test/literate/HighlighterTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,57 +20,57 @@ public class HighlighterTest {
| S n, m => S (add n m)
""";

highlightAndTest(code,
highlightAndTest("open inductive Nat\n| O | S Nat\n\ndef add Nat Nat : Nat\n| n, 0 => n\n| S n, m => S (add n m)\n",
keyword(0, 3, "open"),
whatever(),
def(10, 12, "Nat", "nat", HighlightInfo.DefKind.Data),
def(15, 17, "Nat", "nat", HighlightInfo.DefKind.Data),
whatever(), // |
def(16, 16, "O", "zero", HighlightInfo.DefKind.Con),
def(21, 21, "O", "zero", HighlightInfo.DefKind.Con),
whatever(), // |
def(20, 20, "S", "suc", HighlightInfo.DefKind.Con),
ref(22, 24, "Nat", "nat", HighlightInfo.DefKind.Data),
def(25, 25, "S", "suc", HighlightInfo.DefKind.Con),
ref(27, 29, "Nat", "nat", HighlightInfo.DefKind.Data),
whatever(), // def
def(31, 33, "add", HighlightInfo.DefKind.Fn),
ref(35, 37, "Nat", "nat", HighlightInfo.DefKind.Data),
ref(39, 41, "Nat", "nat", HighlightInfo.DefKind.Data),
def(36, 38, "add", HighlightInfo.DefKind.Fn),
ref(40, 42, "Nat", "nat", HighlightInfo.DefKind.Data),
ref(44, 46, "Nat", "nat", HighlightInfo.DefKind.Data),
whatever(), // :
ref(45, 47, "Nat", "nat", HighlightInfo.DefKind.Data),
ref(50, 52, "Nat", "nat", HighlightInfo.DefKind.Data),
whatever(), // |
localDef(51, 51, "n", "n'"),
litInt(54, 54, 0),
localDef(56, 56, "n", "n'"),
litInt(59, 59, 0),
whatever(), // =>
localRef(59, 59, "n", "n'"),
localRef(64, 64, "n", "n'"),
whatever(), // |
ref(63, 63, "S", "suc", HighlightInfo.DefKind.Con),
ref(68, 68, "S", "suc", HighlightInfo.DefKind.Con),
// Note: n' is still available here, so use another name
localDef(65, 65, "n", "n''"),
localDef(68, 68, "m", "m'"),
localDef(70, 70, "n", "n''"),
localDef(73, 73, "m", "m'"),
whatever(), // =>
ref(73, 73, "S", "suc", HighlightInfo.DefKind.Con),
ref(78, 78, "S", "suc", HighlightInfo.DefKind.Con),
whatever(), // (
ref(76, 78, "add", HighlightInfo.DefKind.Fn),
localRef(80, 80, "n", "n''"),
localRef(82, 82, "m", "m'"),
ref(81, 83, "add", HighlightInfo.DefKind.Fn),
localRef(85, 85, "n", "n''"),
localRef(87, 87, "m", "m'"),
whatever() // )
);
}

@Test public void unformatTest() {
@Language("Aya") String code = """
open
data Nat |
inductive Nat |
O | S Nat
""";

highlightAndTest(code,
highlightAndTest(" open\ninductive Nat |\nO | S Nat\n",
keyword(3, 6, "open"),
keyword(8, 11, "data"),
def(14, 16, "Nat", "nat", HighlightInfo.DefKind.Data),
keyword(8, 16, "inductive"),
def(19, 21, "Nat", "nat", HighlightInfo.DefKind.Data),
whatever(),
def(20, 20, "O", HighlightInfo.DefKind.Con),
def(25, 25, "O", HighlightInfo.DefKind.Con),
whatever(),
def(24, 24, "S", HighlightInfo.DefKind.Con),
ref(26, 28, "Nat", "nat", HighlightInfo.DefKind.Data));
def(29, 29, "S", HighlightInfo.DefKind.Con),
ref(31, 33, "Nat", "nat", HighlightInfo.DefKind.Data));
}

@Test public void incorrectTest() {
Expand All @@ -81,10 +81,10 @@ open inductive List (A : Type)
| cons A (List A)
""";

highlightAndTest(code,
highlightAndTest("open inductive List (A : Type)\n| nil\n| cons A (List A)\n",
whatever(),
whatever(),
def(10, 13, "L1st", "list", HighlightInfo.DefKind.Data));
def(15, 18, "L1st", "list", HighlightInfo.DefKind.Data));
});
}

Expand Down Expand Up @@ -116,40 +116,40 @@ open inductive Either (A B : Type)
def constA {A : Type} (a b : A) : A => a
""";

highlightAndTest(code,
highlightAndTest("open inductive Either (A B : Type)\n| Left A\n| Right B\n\ndef constA {A : Type} (a b : A) : A => a\n",
keyword(0, 3, "open"),
keyword(5, 8, "data"),
def(10, 15, "Either", "DefEither", HighlightInfo.DefKind.Data),
keyword(5, 13, "inductive"),
def(15, 20, "Either", "DefEither", HighlightInfo.DefKind.Data),
whatever(), // (
localDef(18, 18, "A", "LocalA"),
localDef(20, 20, "B", "LocalB"),
localDef(23, 23, "A", "LocalA"),
localDef(25, 25, "B", "LocalB"),
whatever(), // :
keyword(24, 27, "Type"),
keyword(29, 32, "Type"),
whatever(), // )
whatever(), // |
def(32, 35, "Left", HighlightInfo.DefKind.Con),
localRef(37, 37, "A", "LocalA"),
def(37, 40, "Left", HighlightInfo.DefKind.Con),
localRef(42, 42, "A", "LocalA"),
whatever(), // |
def(41, 45, "Right", HighlightInfo.DefKind.Con),
localRef(47, 47, "B", "LocalB"),
def(46, 50, "Right", HighlightInfo.DefKind.Con),
localRef(52, 52, "B", "LocalB"),

keyword(50, 52, "def"),
def(54, 59, "constA", HighlightInfo.DefKind.Fn),
keyword(55, 57, "def"),
def(59, 64, "constA", HighlightInfo.DefKind.Fn),
whatever(), // {
localDef(62, 62, "A", "LocalA'"),
localDef(67, 67, "A", "LocalA'"),
whatever(), // :
keyword(66, 69, "Type"),
keyword(71, 74, "Type"),
whatever(), // }
whatever(), // (
localDef(73, 73, "a", "Locala"),
localDef(75, 75, "b"),
localDef(78, 78, "a", "Locala"),
localDef(80, 80, "b"),
whatever(), // :
localRef(79, 79, "A", "LocalA'"),
localRef(84, 84, "A", "LocalA'"),
whatever(), // )
whatever(), // :
localRef(84, 84, "A", "LocalA'"),
localRef(89, 89, "A", "LocalA'"),
whatever(), // =>
localRef(89, 89, "a", "Locala"));
localRef(94, 94, "a", "Locala"));
}

@Test public void variables() {
Expand All @@ -159,7 +159,7 @@ open inductive Either (A B : Type)
def id (a : A) : A => a
""";

highlightAndTest(code,
highlightAndTest("variable A : Type\n\ndef id (a : A) : A => a\n",
keyword(0, 7, "variable"),
def(9, 9, "A", "GA", HighlightInfo.DefKind.Generalized),
whatever(), // :
Expand Down

0 comments on commit b9d2255

Please sign in to comment.