parse properties with optional labels

See #342.

src/Disco/AST/Surface.hs

@@ -160,8 +160,9 @@ type Docs = [DocThing]
 data DocThing
   = DocString   [String]    -- ^ A documentation string, i.e. a block
                             --   of @||| text@ items
-  | DocProperty Property    -- ^ An example/doctest/property of the
-                            --   form @!!! forall (x1:ty1) ... . property@
+  | DocProperty (Maybe String) Property
+                            -- ^ An optionally labelled example/doctest/property of the
+                            --   form @!!![label] property@
 deriving instance ForallTerm Show  UD => Show DocThing
 
 -- | A property is a universally quantified term of the form

src/Disco/Parser.hs

@@ -495,7 +495,7 @@ parseTopLevel = L.nonIndented sc $
 parseDocThing :: Parser DocThing
 parseDocThing
   =   DocString   <$> some parseDocString
-  <|> DocProperty <$> parseProperty
+  <|> parseProperty
 
 -- | Parse one line of documentation beginning with @|||@.
 parseDocString :: Parser String
@@ -511,10 +511,11 @@ parseDocString = label "documentation" $ L.nonIndented sc $
 
 -- | Parse a top-level property/unit test, which is just @!!!@
 --   followed by an arbitrary term.
-parseProperty :: Parser Term
-parseProperty = label "property" $ L.nonIndented sc $ do
-  _ <- symbol "!!!"
-  indented parseTerm
+parseProperty :: Parser DocThing
+parseProperty = label "property" $ L.nonIndented sc $
+  DocProperty
+    <$> lexeme (string "!!!" *> optional (char '[' *> some (noneOf "[]") <* char ']'))
+    <*> indented parseTerm
 
 -- | Parse a single top-level declaration (either a type declaration
 --   or single definition clause).

src/Disco/Typecheck.hs

@@ -328,7 +328,7 @@ checkProperties docs =
     <$> (traverse . traverse) checkProperty properties
   where
     properties :: Ctx Term [Property]
-    properties = fmap (\ds -> [p | DocProperty p <- ds]) docs
+    properties = fmap (\ds -> [p | DocProperty _ p <- ds]) docs  -- XXX
 
 -- | Check the types of the terms embedded in a property.
 checkProperty