diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index abd2bc7..47b9cab 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -424,33 +424,46 @@ tests = "parser" :- [ "top level" :- [ parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;" - `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _, - PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]), + `([PD $ MkPDecl [] + (PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _, + PD $ MkPDecl [] + (PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]), parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $ - `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _, - PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]), + `([PD $ MkPDecl [] + (PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _, + PD $ MkPDecl [] + (PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]), note "empty input", parsesAs input "" [], parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;", parseMatch input "namespace a {}" - `([PD $ PNs $ MkPNamespace [< "a"] [] _]), + `([PD $ MkPDecl [] (PNs $ MkPNamespace [< "a"] [] _) _]), parseMatch input "namespace a.b.c {}" - `([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] _]), + `([PD $ MkPDecl [] + (PNs $ MkPNamespace [< "a", "b", "c"] [] _) _]), parseMatch input "namespace a {namespace b {}}" - `([PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] [] _] _]), + `([PD (MkPDecl [] + (PNs $ MkPNamespace [< "a"] + [MkPDecl [] (PNs $ MkPNamespace [< "b"] [] _) _] _) _)]), parseMatch input "namespace a {def x = 't ∷ {t}}" - `([PD $ PNs $ MkPNamespace [< "a"] - [PDef $ MkPDef (PQ Any _) "x" Nothing - (Ann (Tag "t" _) (Enum ["t"] _) _) _] _]), + `([PD (MkPDecl [] + (PNs $ MkPNamespace [< "a"] + [MkPDecl [] + (PDef $ MkPDef (PQ Any _) "x" Nothing + (Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _)]), parseMatch input "namespace a {def x = 't ∷ {t}} def y = a.x" - `([PD $ PNs $ MkPNamespace [< "a"] - [PDef $ MkPDef (PQ Any _) "x" Nothing - (Ann (Tag "t" _) (Enum ["t"] _) _) _] _, - PD $ PDef $ MkPDef (PQ Any _) "y" Nothing - (V (MakePName [< "a"] "x") {}) _]), + `([PD (MkPDecl [] + (PNs $ MkPNamespace [< "a"] + [MkPDecl [] + (PDef $ MkPDef (PQ Any _) "x" Nothing + (Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _), + PD (MkPDecl [] + (PDef $ MkPDef (PQ Any _) "y" Nothing + (V (MakePName [< "a"] "x") Nothing _) _) _)]), parseMatch input #" load "a.quox"; def b = a.b "# `([PLoad "a.quox" _, - PD $ PDef $ MkPDef (PQ Any _) "b" Nothing - (V (MakePName [< "a"] "b") {}) _]) + PD (MkPDecl [] + (PDef $ MkPDef (PQ Any _) "b" Nothing + (V (MakePName [< "a"] "b") Nothing _) _) _)]) ] ]