{-# LANGUAGE RankNTypes, DeriveTraversable #-}
-- |
-- Module      :  Data.Map.Justified.Tutorial
-- Copyright   :  (c) Matt Noonan 2017
-- License     :  BSD-style
-- Maintainer  :  matt.noonan@gmail.com
-- Portability :  portable
--
-- = Description
--
-- The examples below demonstrate how to use the types and functions in "Data.Map.Justified".
--
-- You should be able to simply load this module in @ghci@ to play along.
-- The import list is:
--
-- @
--  import Prelude hiding (lookup)
--  
--  import Data.Map.Justified
--  
--  import qualified Data.Map as M
--  
--  import Data.Traversable (for)
--  import Data.Char (toUpper)
--  import Control.Monad (forM_)
-- @

module Data.Map.Justified.Tutorial where

import Prelude hiding (lookup)

import Data.Map.Justified

import qualified Data.Map as M

import Data.Char (toUpper)
import Control.Monad (forM_)

-- | A simple "Data.Map" value used in several examples below.
--
-- @
--  test_table = M.fromList [ (1, "hello"), (2, "world") ]
-- @
test_table :: M.Map Int String
test_table = M.fromList [ (1, "hello"), (2, "world") ]

-- | This example shows how the @'Data.Map.Justified.member'@
-- function can be used to obtain a key whose type has been
-- augmented by a proof that the key is present in maps of a
-- certain type.
--
-- Where "Data.Map" may use a @'Maybe'@ type to ensure that
-- the user handles missing keys when performing a lookup,
-- here we use the @'Maybe'@ type to either tell the user
-- that a key is missing (by returning @'Nothing'@), or
-- actually give back evidence of the key's presence
-- (by returning @Just known_key@)
--
-- The @'Data.Map.Justified.withMap'@ function is used to
-- plumb a "Data.Map" @'Data.Map.Map'@ into a function that
-- expects a "Data.Map.Justified" @'Data.Map.Justified.Map'@.
-- In the code below, you can think of @table@ as @test_table@,
-- enhanced with the ability to use verified keys.
--
-- You can get from @table@ back to @test_table@ using the
-- function @'Data.Map.Justified.theMap'@.
--
-- @
--  example1 = withMap test_table $ \\table -> do
--
--    putStrLn "Is 1 a valid key?"
--    case member 1 table of
--      Nothing  -> putStrLn "  No, it was not found."
--      Just key -> putStrLn $ "  Yes, found key: " ++ show key
--
--    putStrLn "Is 5 a valid key?"
--    case member 5 table of
--      Nothing  -> putStrLn "  No, it was not found."
--      Just key -> putStrLn $ "  Yes, found key: " ++ show key
-- @
-- Output:
--
-- @
--  Is 1 a valid key?
--    Yes, found key: Key 1
--  Is 5 a valid key?
--    No, it was not found.
-- @
example1 :: IO ()
example1 = withMap test_table $ \table -> do

    putStrLn "Is 1 a valid key?"
    case member 1 table of
      Nothing  -> putStrLn "  No, it was not found."
      Just key -> putStrLn $ "  Yes, found key: " ++ show key

    putStrLn "Is 5 a valid key?"
    case member 5 table of
      Nothing  -> putStrLn "  No, it was not found."
      Just key -> putStrLn $ "  Yes, found key: " ++ show key

-- | Once you have obtained a verified key, how do you use it?
--
-- "Data.Map.Justified" has several functions that are similar
-- to ones found in "Data.Map" that operate over verified keys.
-- In this example, notice that we can extract values directly
-- from the map using @'Data.Map.Justified.lookup'@; since we already
-- proved that the key is present when we obtained a @Key ph k@
-- value, @'Data.Map.Justified.lookup'@ does not need to return a
-- @'Maybe'@ value.
--
-- @
--  example2 = withMap test_table $ \\table -> do
--  
--    case member 1 table of
--      Nothing  -> putStrLn "Sorry, I couldn't prove that the key is present."
--      Just key -> do
--        -- In this do-block, \'key\' represents the key 1, but carries type-level
--        -- evidence that the key is present. Lookups and updates can now proceed
--        -- without the possibility of error.
--        putStrLn ("Found key: " ++ show key)
--  
--        -- Note that lookup returns a value directly, not a \'Maybe\'!
--        putStrLn ("Value for key: " ++ lookup key table)
--  
--        -- If you update an already-mapped value, the set of valid keys does
--        -- not change. So the evidence that \'key\' could be found in \'table\'
--        -- is still sufficient to ensure that \'key\' can be found in the updated
--        -- table as well.
--        let table' = reinsert key "howdy" table
--        putStrLn ("Value for key in updated map: " ++ lookup key table')
-- @
-- Output:
--
-- @
--  Found key: Key 1
--  Value for key: hello
--  Value for key in updated map: howdy
-- @
example2 :: IO ()
example2 = withMap test_table $ \table -> do

  case member 1 table of
    Nothing  -> putStrLn "Sorry, I couldn't prove that the key is present."
    Just key -> do
      -- In this do-block, 'key' represents the key 1, but carries type-level
      -- evidence that the key is present. Lookups and updates can now proceed
      -- without the possibility of error.
      putStrLn ("Found key " ++ show key)

      -- Note that lookup returns a value directly, not a 'Maybe'!
      putStrLn ("Value for key: " ++ lookup key table)

      -- If you update an already-mapped value, the set of valid keys does
      -- not change. So the evidence that 'key' could be found in 'table'
      -- is still sufficient to ensure that 'key' can be found in the updated
      -- table as well.
      let table' = reinsert key "howdy" table
      putStrLn ("Value for key in updated map: " ++ lookup key table')

-- | It is a bit surprising to realize that a key of type @Key ph k@ can
-- be used to safely look up values in /any/ map of type @Map ph k v@,
-- not only the map that they key was originally found in!
--
-- This example makes use of that property to look up corresponding
-- elements of two /different/ (but related) tables, using the same
-- key evidence.
--
-- @
--  example3 = withMap test_table $ \\table -> do
--  
--    let uppercase = map toUpper
--        updated_table = fmap (reverse . uppercase) table
--    
--    for (keys table) $ \\key -> do
--      -- Although we are iterating over keys from the original table, they
--      -- can also be used to safely lookup values in the fmapped table.
--      -- Unlike (!) from Data.Map, Data.Map.Justified's (!) can not fail at runtime.
--      putStrLn ("In original table, " ++ show key ++ " maps to " ++ table ! key)
--      putStrLn ("In updated table,  " ++ show key ++ " maps to " ++ updated_table ! key)
--  
--    return ()
-- @
-- Output:
--
-- @
--  In original table, Key 1 maps to hello
--  In updated table,  Key 1 maps to OLLEH
--  In original table, Key 2 maps to world
--  In updated table,  Key 2 maps to DLROW
-- @
example3 :: IO ()
example3 = withMap test_table $ \table -> do

  let uppercase = map toUpper
      updated_table = fmap (reverse . uppercase) table
  
  forM_ (keys table) $ \key -> do
    -- Although we are iterating over keys from the original table, they
    -- can also be used to safely lookup values in the fmapped table.
    -- Unlike (!) from Data.Map, Data.Map.Justified's (!) can not fail at runtime.
    putStrLn ("In original table, " ++ show key ++ " maps to " ++ table ! key)
    putStrLn ("In updated table,  " ++ show key ++ " maps to " ++ updated_table ! key)

  return ()

-- | What if your set of keys can change over time?
--
-- If you were to insert a new key into a map, evidence that a key
-- exists is in the old map is no longer equivalent to evidence that
-- a key exists in the new map.
--
-- On the other hand, we know that if some @key@ exists in the old map,
-- then @key@ must still exist in the new map. So there should be a
-- way of "upgrading" evidence from the old map to the new. Furthermore,
-- we know that the key we just added must be in the new map.
--
-- The @'Data.Map.Justified.inserting'@ function inserts a value into a map
-- and feeds the new map into a continuation, along with the "upgrade" and
-- "new key" data.
--
-- @
--  example4 = withMap test_table $ \table -> do
--    inserting 3 "NEW" table $ \(newKey, upgrade, table') -> do
--      forM_ (keys table) $ \key -> do
--        putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.")
--        putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.")
--      putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)
-- @
-- Output:
--
-- @
--  Key 1 maps to hello in the old table.
--  Key 1 maps to hello in the new table.
--  Key 2 maps to world in the old table.
--  Key 2 maps to world in the new table.
--  Also, the new table maps Key 3 to NEW
-- @

example4 :: IO ()
example4 = withMap test_table $ \table -> do
  inserting 3 "NEW" table $ \(newKey, upgrade, table') -> do
    forM_ (keys table) $ \key -> do
      putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.")
      putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.")
    putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)
    
-- | The next example uses a directed graph, defined by this adjacency list.
--
-- @
--  adjacencies = M.fromList [ (1, [2,3]), (2, [1,5,3]), (3, [4]), (4, [3, 1]), (5, []) ]
-- @
adjacencies :: M.Map Int [Int]
adjacencies = M.fromList [ (1, [2,3]), (2, [1,5,3]), (3, [4]), (4, [3, 1]), (5, []) ]

-- | Sometimes, the values in a map may include references back to keys
-- in the map. A canonical example of this is the adjacency map representation of
-- a directed graph, where each node maps to its list of immediate successors.
-- The type would look something like
--
-- @
--  type Digraphy node = M.Map node [node]
-- @
--
-- If you want to do a computation with a @Digraphy node@, you probably want each
-- of the neighbor nodes to have keys in the @Digraphy node@ map. That is, you
-- may really want
--
-- @
--  type Digraph ph node = Map ph node [Key ph node]
--                             \/\\           \/\\
--                             |            |
--                             +-----+------+
--                                   |
--   (each neighbor should carry a proof that they are also in the map)
-- @
-- You can do this via @'Data.Map.Justified.withRecMap'@, which converts each
-- key reference of type @k@ in your map to a verified key of type @'Key' ph k@.
--
-- But what if a referenced key really is missing from the map? @'Data.Map.Justified.withRecMap'@
-- returns an @'Either'@ value to represent failure; if a key is missing, then the
-- result will be a value of the form @'Left' problems@, where @problems@ is an explanation
-- of where the missing keys are.
--
-- @
--  example5 = do
--     -- Print out the nodes in a graph 
--     putStrLn ("Finding nodes in the directed graph " ++ show adjacencies)
--     trial adjacencies
--  
--     -- Now add the (non-present) node 6 as a target of an edge from node 4 and try again:
--     let adjacencies' = M.adjust (6:) 4 adjacencies
--     putStrLn ("Finding nodes in the directed graph " ++ show adjacencies')
--     trial adjacencies'
--     
--    where
--      trial adj = either showComplaint showNodes (withRecMap adj (map theKey . keys))
--      
--      showNodes nodes = putStrLn ("  Nodes: " ++ show nodes)
--  
--      showComplaint problems = do
--        putStrLn "  The following edges are missing targets:"
--        let badPairs = concatMap (\\(src, tgts) -> [ (src,tgt) | (tgt, Missing) <- tgts ]) problems
--        forM_ badPairs $ \\(src,tgt) -> putStrLn ("    " ++ show src ++ " -> " ++ show tgt)
-- @
-- Output:
--
-- @
--  Finding nodes in the directed graph fromList [(1,[2,3]),(2,[1,5,3]),(3,[4]),(4,[3,1]),(5,[])]
--    Nodes: [1,2,3,4,5]
--  Finding nodes in the directed graph fromList [(1,[2,3]),(2,[1,5,3]),(3,[4]),(4,[6,3,1]),(5,[])]
--    The following edges are missing targets:
--      4 -> 6
-- @
example5 :: IO ()
example5 = do
   -- Print out the nodes in a graph 
   putStrLn ("Finding nodes in the directed graph " ++ show adjacencies)
   trial adjacencies

   -- Now add the (non-present) node 6 as a target of an edge from node 4 and try again:
   let adjacencies' = M.adjust (6:) 4 adjacencies
   putStrLn ("Finding nodes in the directed graph " ++ show adjacencies')
   trial adjacencies'
   
  where
    trial adj = either showComplaint showNodes (withRecMap adj (map theKey . keys))
    
    showNodes nodes = putStrLn ("  Nodes: " ++ show nodes)

    showComplaint problems = do
      putStrLn "  The following edges are missing targets:"
      let badPairs = concatMap (\(src, tgts) -> [ (src,tgt) | (tgt, Missing) <- tgts ]) problems
      forM_ badPairs $ \(src,tgt) -> putStrLn ("    " ++ show src ++ " -> " ++ show tgt)