[ :doc ] Adding projections to the record doc

src/Core/Context.idr

@@ -1172,6 +1172,15 @@ clearCtxt
     resetElab : Options -> Options
     resetElab = record { elabDirectives = defaultElab }
 
+export
+getFieldNames : Context -> Namespace -> List Name
+getFieldNames ctxt recNS
+  = let nms = resolvedAs ctxt in
+    keys $ flip filterBy nms $ \ n =>
+      case isRF n of
+        Nothing => False
+        Just (ns, field) => ns == recNS
+
 -- Find similar looking names in the context
 getSimilarNames : {auto c : Ref Ctxt Defs} -> Name -> Core (List String)
 getSimilarNames nm = case userNameRoot nm of

src/Core/Name.idr

@@ -91,6 +91,12 @@ isSourceName (CaseBlock _ _) = False
 isSourceName (WithBlock _ _) = False
 isSourceName (Resolved _) = False
 
+export
+isRF : Name -> Maybe (Namespace, String)
+isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n)
+isRF (RF n) = Just (emptyNS, n)
+isRF _ = Nothing
+
 export
 isUN : Name -> Maybe String
 isUN (UN str) = Just str

src/Idris/Doc/String.idr

@@ -233,25 +233,59 @@ getDocsForName fc n
                                    , annotate Declarations $ vcat $ map (indent 2) docs]]
              pure (vcat (params ++ constraints ++ meths ++ insts))
 
+    getFieldDoc : Name -> Core (Doc IdrisDocAnn)
+    getFieldDoc nm
+      = do syn <- get Syn
+           defs <- get Ctxt
+           Just def <- lookupCtxtExact nm (gamma defs)
+                -- should never happen, since we know that the DCon exists:
+                | Nothing => pure Empty
+           ty <- resugar [] =<< normaliseHoles defs [] (type def)
+           let prettyName = pretty (nameRoot nm)
+           let projDecl = hsep [ fun nm prettyName, colon, prettyTerm ty ]
+           let [(_, str)] = lookupName nm (docstrings syn)
+                  | _ => pure projDecl
+           pure $ annotate (Decl nm)
+                $ vcat [ projDecl
+                       , annotate DocStringBody $ vcat (reflowDoc str)
+                       ]
+
+    getFieldsDoc : Name -> Core (List (Doc IdrisDocAnn))
+    getFieldsDoc recName
+      = do let (Just ns, n) = displayName recName
+               | _ => pure []
+           let recNS = ns <.> mkNamespace n
+           defs <- get Ctxt
+           let fields = getFieldNames (gamma defs) recNS
+           syn <- get Syn
+           case fields of
+             [] => pure []
+             [proj] => pure [header "Projection" <++> annotate Declarations !(getFieldDoc proj)]
+             projs => pure [vcat [header "Projections"
+                                 , annotate Declarations $
+                                      vcat $ map (indent 2) $ !(traverse getFieldDoc projs)]]
+
     getExtra : Name -> GlobalDef -> Core (List (Doc IdrisDocAnn))
-    getExtra n d
-        = do syn <- get Syn
-             let [] = lookupName n (ifaces syn)
-                 | [ifacedata] => pure <$> getIFaceDoc ifacedata
-                 | _ => pure [] -- shouldn't happen, we've resolved ambiguity by now
-             case definition d of
-               PMDef _ _ _ _ _
-                   => pure [showTotal n (totality d)]
-               TCon _ _ _ _ _ _ cons _
-                   => do let tot = [showTotal n (totality d)]
-                         cdocs <- traverse (getDConDoc <=< toFullNames) cons
-                         let cdoc = case cdocs of
-                              [] => []
-                              [doc] => [header "Constructor" <++> annotate Declarations doc]
-                              docs => [vcat [header "Constructors"
-                                      , annotate Declarations $ vcat $ map (indent 2) docs]]
-                         pure (tot ++ cdoc)
-               _ => pure []
+    getExtra n d = do
+      do syn <- get Syn
+         let [] = lookupName n (ifaces syn)
+             | [ifacedata] => pure <$> getIFaceDoc ifacedata
+             | _ => pure [] -- shouldn't happen, we've resolved ambiguity by now
+         case definition d of
+           PMDef _ _ _ _ _ => pure [showTotal n (totality d)]
+           TCon _ _ _ _ _ _ cons _ =>
+             do let tot = [showTotal n (totality d)]
+                cdocs <- traverse (getDConDoc <=< toFullNames) cons
+                cdoc <- case cdocs of
+                  [] => pure []
+                  [doc] => pure
+                         $ (header "Constructor" <++> annotate Declarations doc)
+                         :: !(getFieldsDoc n)
+                  docs => pure [vcat [header "Constructors"
+                                     , annotate Declarations $
+                                         vcat $ map (indent 2) docs]]
+                pure (tot ++ cdoc)
+           _ => pure []
 
     showCategory : GlobalDef -> Doc IdrisDocAnn -> Doc IdrisDocAnn
     showCategory d = case definition d of

src/Libraries/Data/NameMap.idr

@@ -327,6 +327,18 @@ export
   neutral = empty
 
 
+treeFilterBy : (Key -> Bool) -> Tree n v -> NameMap v
+treeFilterBy test = loop empty where
+
+  loop : NameMap v -> Tree _ v -> NameMap v
+  loop acc (Leaf k v)
+    = let True = test k | _ => acc in
+      insert k v acc
+  loop acc (Branch2 t1 _ t2)
+    = loop (loop acc t1) t2
+  loop acc (Branch3 t1 _ t2 _ t3)
+    = loop (loop (loop acc t1) t2) t3
+
 treeFilterByM : Monad m => (Key -> m Bool) -> Tree n v -> m (NameMap v)
 treeFilterByM test = loop empty where
 
@@ -342,6 +354,11 @@ treeFilterByM test = loop empty where
          acc <- loop acc t2
          loop acc t3
 
+export
+filterBy : (Name -> Bool) -> NameMap v -> NameMap v
+filterBy test Empty = Empty
+filterBy test (M _ t) = treeFilterBy test t
+
 export
 filterByM : Monad m => (Name -> m Bool) -> NameMap v -> m (NameMap v)
 filterByM test Empty = pure Empty

tests/Main.idr

@@ -162,7 +162,7 @@ idrisTestsEvaluator = MkTestPool "Evaluation" []
 idrisTests : TestPool
 idrisTests = MkTestPool "Misc" []
        -- Documentation strings
-      ["docs001", "docs002",
+      ["docs001", "docs002", "docs003",
        -- Eta equality
        "eta001",
        -- Modules and imports

tests/idris2/docs002/expected

@@ -19,4 +19,7 @@ Doc> Doc.WrappedInt : Type
 Doc> Doc.SimpleRec : Type
   Totality: total
   Constructor: MkSimpleRec : Int -> String -> SimpleRec
+  Projections:
+    a : SimpleRec -> Int
+    b : SimpleRec -> String
 Doc> Bye for now!

tests/idris2/docs003/RecordDoc.idr

@@ -0,0 +1,12 @@
+module RecordDoc
+
+record A (a : Type) where
+  anA : a
+
+record Tuple (a, b : Type) where
+  proj1 : a
+  proj2 : b
+
+record Singleton {0 a : Type} (v : a) where
+  value : a
+  0 equal : value = v

tests/idris2/docs003/expected

@@ -0,0 +1,19 @@
+1/1: Building RecordDoc (RecordDoc.idr)
+RecordDoc> 
+RecordDoc> RecordDoc.A : Type -> Type
+  Totality: total
+  Constructor: __mkA : _
+  Projection: anA : A a -> a
+RecordDoc> RecordDoc.Tuple : Type -> Type -> Type
+  Totality: total
+  Constructor: __mkTuple : _
+  Projections:
+    proj1 : Tuple a b -> a
+    proj2 : Tuple a b -> b
+RecordDoc> RecordDoc.Singleton : a -> Type
+  Totality: total
+  Constructor: __mkSingleton : _
+  Projections:
+    equal : ({rec:0} : Singleton v) -> value rec = v
+    value : Singleton v -> a
+RecordDoc> Bye for now!

tests/idris2/docs003/input

@@ -0,0 +1,5 @@
+:browse RecordDoc
+:doc A
+:doc Tuple
+:doc Singleton
+:q

tests/idris2/docs003/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner RecordDoc.idr < input
+
+rm -rf build