Trie searching.

Treemember.idr

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

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

-- Take a path through the trie, and return a node's name (if there is one).
public export
triefind : List String -> StringTrie a -> Maybe a 
triefind [] 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.
triefind (y :: ys) st = case node st of
    This _        => Nothing -- We still have path left to search, but the trie has ended.
    That children => (lookup y children) >>= (triefind ys)   -- search the children 
    Both _ children => (lookup y children) >>= (triefind ys) -- search the children 

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

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 [
    ("core",      "Core documentation"), 
    ("core.elab", "Some elaboration stuff"), 
    ("syntax",    "Documentation of syntax")
]

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

antilog : (logctx: String) 
    -> {auto known : Uninhabited (IsJust (Treemember.triefind (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 $ triefind (splitname "core") topics)
    putStrLn (show $ triefind (splitname "core.elab") topics)
    putStrLn (show $ triefind (splitname "syntax") topics)
    -- The following type-level checks all fail to type-check. 
    safelog "core" "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