SchemaValue2.idr

logEvent : Event -> List PlaceholderValue -> Maybe String
logEvent e vals = loop (messageSpec e) vals (title e ++ ": ")
  where
    loop : Schema -> List PlaceholderValue -> String -> Maybe String
    loop [] [] out = pure out
    loop (IntVar :: xs) (IntVal i :: ys) out = loop xs ys (out ++ show i)
    loop (StrVar :: xs) (StrVal s :: ys) out = loop xs ys (out ++ s)
    loop (StrCst x :: xs) ys out = loop xs ys (out ++ x)
    loop _ _ _ = Nothing