A demonstration of "full" searching for logging contexts. Note, this currently hangs Idris2 with an infinite loop.

Treemember.idr

module Treemember
import Data.List
import Data.List1
import Data.String 
import Data.These
import Data.Maybe
import Data.So

import Libraries.Data.StringTrie
import Libraries.Data.StringMap

%default total

public export
find : List String -> StringTrie a -> Maybe a 
-- If our "path" has finished, and this node in the trie has some "data", return it. 
find [] (MkStringTrie (This x)) = Just x 
find [] (MkStringTrie (Both x _)) = Just x
-- If we still have some path left, search the children for the head of the path. 
find (y :: ys) (MkStringTrie (That children)) = (lookup y children) >>= (find ys)
find (y :: ys) (MkStringTrie (Both _ children)) = (lookup y children) >>= (find ys)
-- Otherwise, we can't find what we're looking for (path too short, or too long)
find _ _ = Nothing


public export
exists : List String -> StringTrie a -> Bool 
-- If our "path" has finished, and this node in the trie has some "data", return it. 
exists [] (MkStringTrie (This x)) = True 
exists [] (MkStringTrie (Both x _)) = True
-- If we still have some path left, search the children for the head of the path. 
exists (y :: ys) (MkStringTrie (That children)) = case (lookup y children) of 
    Just subtrie => exists ys subtrie
    _ => False
exists (y :: ys) (MkStringTrie (Both _ children)) = case (lookup y children) of 
    Just subtrie => exists ys subtrie
    _ => False
-- Otherwise, we can't find what we're looking for (path too short, or too long)
exists _ _ = False


-- Take a path through the trie, and return a node's name (if there is one).
public export
findold : List String -> StringTrie a -> Maybe a 
findold [] st = case node st of 
    This x   => Just x  -- nothing left to search, return this node's name. 
    That _   => Nothing -- no data, but our path has finished
    Both x _ => Just x  -- nothing left to search, return this node's name.
findold (y :: ys) st = case node st of
    This _        => Nothing -- We still have path left to search, but the trie has ended.
    That children => case (lookup y children) of 
        Just newtrie => (findold ys newtrie)   -- search the children 
        Nothing => Nothing
    Both _ children =>  case (lookup y children) of 
        Just newtrie => (findold ys newtrie)   -- search the children 
        Nothing => Nothing

public export
splitname : String -> List String 
splitname = forget . Data.String.split (== '.')

public export
insert : (String, String) -> StringTrie String -> StringTrie String
insert (name, docs) trie = let l = splitname name in 
    insert l docs trie

public export 
topics : StringTrie String 
topics = foldr insert StringTrie.empty [
    ("", "some documentation of this option"),
    ("auto", "some documentation of this option"),
    ("compile.casetree", "some documentation of this option"),
    ("compiler.inline.eval", "some documentation of this option"),
    ("coverage.empty", "some documentation of this option"),
    ("coverage.recover", "some documentation of this option"),
    ("declare.data", "some documentation of this option"),
    ("declare.data.constructor", "some documentation of this option"),
    ("declare.data.parameters", "some documentation of this option"),
    ("declare.def", "some documentation of this option"),
    ("declare.def.clause", "some documentation of this option"),
    ("declare.def.clause.impossible", "some documentation of this option"),
    ("declare.def.clause.with", "some documentation of this option"),
    ("declare.def.impossible", "some documentation of this option"),
    ("declare.def.lhs", "some documentation of this option"),
    ("declare.param", "some documentation of this option"),
    ("declare.record", "some documentation of this option"),
    ("declare.record.field", "some documentation of this option"),
    ("declare.record.projection", "some documentation of this option"),
    ("declare.type", "some documentation of this option"),
    ("elab", "some documentation of this option"),
    ("elab.ambiguous", "some documentation of this option"),
    ("elab.as", "some documentation of this option"),
    ("elab.case", "some documentation of this option"),
    ("elab.delay", "some documentation of this option"),
    ("elab.hole", "some documentation of this option"),
    ("elab.implementation", "some documentation of this option"),
    ("elab.interface", "some documentation of this option"),
    ("elab.interface.default", "some documentation of this option"),
    ("elab.local", "some documentation of this option"),
    ("elab.prun", "some documentation of this option"),
    ("elab.prune", "some documentation of this option"),
    ("elab.record", "some documentation of this option"),
    ("elab.retry", "some documentation of this option"),
    ("elab.rewrite", "some documentation of this option"),
    ("eval.casetree", "some documentation of this option"),
    ("eval.casetree.stuck", "some documentation of this option"),
    ("eval.eta", "some documentation of this option"),
    ("eval.stuck", "some documentation of this option"),
    ("idemode.hole", "some documentation of this option"),
    ("import", "some documentation of this option"),
    ("interaction.casesplit", "some documentation of this option"),
    ("interaction.generate", "some documentation of this option"),
    ("interaction.search", "some documentation of this option"),
    ("metadata.names", "some documentation of this option"),
    ("quantity", "some documentation of this option"),
    ("quantity.hole", "some documentation of this option"),
    ("specialise", "some documentation of this option"),
    ("totality", "some documentation of this option"),
    ("totality.positivity", "some documentation of this option"),
    ("totality.termination", "some documentation of this option"),
    ("totality.termination.calc", "some documentation of this option"),
    ("totality.termination.guarded", "some documentation of this option"),
    ("totality.termination.sizechange", "some documentation of this option"),
    ("totality.termination.sizechange.checkCall", "some documentation of this option"),
    ("totality.termination.sizechange.checkCall.inPath", "some documentation of this option"),
    ("totality.termination.sizechange.checkCall.inPathNot.restart", "some documentation of this option"),
    ("totality.termination.sizechange.checkCall.inPathNot.return", "some documentation of this option"),
    ("totality.termination.sizechange.inPath", "some documentation of this option"),
    ("totality.termination.sizechange.isTerminating", "some documentation of this option"),
    ("totality.termination.sizechange.needsChecking", "some documentation of this option"),
    ("ttc.write", "some documentation of this option"),
    ("unify.application", "some documentation of this option"),
    ("unify.constant", "some documentation of this option"),
    ("unify.delay", "some documentation of this option"),
    ("unify.equal", "some documentation of this option"),
    ("unify.head", "some documentation of this option"),
    ("unify.instantiate", "some documentation of this option"),
    ("unify.invertible", "some documentation of this option"),
    ("unify.meta", "some documentation of this option"),
    ("unify.noeta", "some documentation of this option"),
    ("unify.postpone", "some documentation of this option"),
    ("unify.retry", "some documentation of this option"),
    ("unify.search", "some documentation of this option"),
    ("unify.unsolved", "some documentation of this option")
]

topicsContains : String -> Bool
topicsContains = isJust (Treemember.find (Treemember.splitname logctx) Treemember.topics)


safelog : (logctx: String) 
    -> {auto known : IsJust (Treemember.find (Treemember.splitname logctx) Treemember.topics)} 
    -> String 
    -> IO () 
safelog logctx body = putStrLn (logctx ++ " " ++ body)

safelogbool : (logctx: String) 
    -> {auto known : topicsContains logctx = True} 
    -> String 
    -> IO () 
safelogbool logctx body = putStrLn (logctx ++ " " ++ body)

antilog : (logctx: String) 
    -> {auto known : Uninhabited (IsJust (Treemember.find (Treemember.splitname logctx) Treemember.topics))} 
    -> String 
    -> IO () 
antilog logctx body = putStrLn (logctx ++ " " ++ body)

main : IO ()
main = do 
    -- The following runtime checks all correctly return "Just ..."
    -- putStrLn (show $ find (splitname "core") topics)
    -- putStrLn (show $ find (splitname "core.elab") topics)
    -- putStrLn (show $ find (splitname "syntax") topics)
    -- The following type-level checks all fail to type-check. 
    safelogbool "eval.eta" "some higher level core" -- This doesn't typecheck, but it should
    -- safelog "syntax.elab" "this shouldn't work" -- This doesn't typecheck, and it shouldn't
    -- antilog "core" "some higher level core" -- This doesn't typecheck, and it shouldn't
    antilog "syntax.elab" "this shouldn't work" -- This doesn't typecheck, but it should