Mustache templating in Idris

AboutMe.mustache

Hello, my name ist {{name}} and I am {{age}} years old.

Mustache.idr

module Mustache

import SimpleParser
import Data.SortedMap
import Providers

%default total
%access public

data Part = Var String | Txt String

Tpl : Type
Tpl = List Part

partial
mustacheParser : Parser Tpl
mustacheParser = many (varParser <|> tplParser)
  where partial varParser : Parser Part
        varParser = do
          string "{{"
          v <- ident
          string "}}"
          return (Var v)
        partial tplParser : Parser Part
        tplParser = map (Txt . pack) (many1 (sat (/= '{')))

mustacheVars : Tpl -> List String
mustacheVars [] = []
mustacheVars (Txt _ :: m) = mustacheVars m
mustacheVars (Var v :: m) = v :: mustacheVars m

hasKeys : Ord k => List k -> SortedMap k v -> Bool
hasKeys []        m = True
hasKeys (k :: ks) m = isJust (lookup k m) && hasKeys ks m

private
render' : Tpl -> SortedMap String String -> String
render' [] m = ""
render' (Txt s :: ts) m = s <+> render' ts m
render' (Var v :: ts) m with (lookup v m)
  | Nothing = render' ts m
  | Just v  = v <+> render' ts m

render : (tpl : Tpl) -> (m : SortedMap String String) ->
         {auto p : hasKeys (mustacheVars tpl) m = True} -> String
render tpl m = render' tpl m

partial
tplFromFile : String -> IO (Provider Tpl)
tplFromFile fname = do
  str <- readFile fname
  case parse mustacheParser str of
    Left err => return (Error err)
    Right (tpl, "") => return (Provide tpl)
    Right (tpl, s) => return (Error $ "input left: " <+> s)

MustacheExample.idr

module MustacheExample

import Mustache
import Data.SortedMap

%language TypeProviders

info : SortedMap String String
info = fromList [("name","Tim Baumann"),("age","19")]

%provide (aboutMeTpl : Tpl) with (tplFromFile "AboutMe.mustache")

main : IO ()
main = putStrLn $ render aboutMeTpl info


incompleteInfo : SortedMap String String
incompleteInfo = fromList [("name", "Max Mustermann"), ("year-of-birth", "1990")]

-- doesn't compile
--about : String
--about = render aboutMeTpl incompleteInfo