{-# LANGUAGE NoMonomorphismRestriction #-}

-- Deriving type-safe printf in direct-style, using
-- shift/reset with effectful typing (supporting the answer-type
-- modification and polymorphism)

module Derive5 where

import Control.Monad

import ShiftResetGenuine

-- Constructors and deconstructors of a particular sequence
-- See the end of derive5.ml

nilA :: Monadish m => a -> m s s a
nilA = ret

{-
consA :: (Monadish m) =>
         h -> (sigma -> m a b tau) -> (h -> m b g sigma) -> m a g tau
-}
consA h t = \f -> f h >== \x -> t x

un_consA x = reset (x (\h -> shift (\t -> ret (h,t))))


-- The example of the de-construction:

l0 = consA 'a' nilA
l0r = fst $ run $ un_consA l0
-- 'a'

l1 = consA 5 (consA 'a' (consA 'f' nilA))
(h1,l11) = run $ un_consA l1
-- h1 is 5
(h2,l12) = run $ un_consA l11
-- h2 is 'a'

nilS :: String
nilS = ""
consS :: String -> String -> String
consS = (++)

-- litP4 :: (Monadish m) => String -> (t -> m a g String) -> t -> m a g String
litP4 str = \tD arg -> tD arg >== ret . consS str 

intP4 = \tD arg ->
  un_consA arg >== \(n,l2) ->
  tD l2 >== ret . consS (show (n::Int)) 

charP4 = \tD arg ->
  un_consA arg >== \(c,l2) ->
  tD l2 >== ret . consS (show (c::Char)) 

nilDP        = \x -> x nilS
consDP d acc = \x -> d acc x

desc0 = consDP (litP4 "lit") $ consDP intP4 nilDP
desc0r = run $ desc0 (consA 1 nilA)
-- "lit1"

descP4 = consDP intP4
    (consDP (litP4 "-th character after ")
       (consDP charP4
          (consDP (litP4 " is ")
             (consDP charP4
                nilDP))))

descr4 = run $ descP4 (consA 5 (consA 'a' (consA 'f' nilA)))
-- "5-th character after 'a' is 'f'"

t0 = \h -> reset (shift (\k -> desc0 k) >== \f -> f h)

{-
 We would like the argument sequence to be just the application of the
 arguments. We would like to transform
  (xxx x1 x2 x3)
to (fun f -> f x1 x2 x3), which is needed as an argument to descP4.
We can do that if we enclose the whole printf expression in reset.
-}

-- Apply a monadish f to the pure argument x
app fm x = fm >== \f -> f x

t1 = (shift descP4) `app` 5 `app` 'a' `app` 'f'
-- t1 :: C String String String

t1r = run $ reset t1
-- "5-th character after 'a' is 'f'"

-- A different take, viewing un_consA as `reading' from a sequence

is_nilA1 _ = ()

un_consA1 arg = shift (\k -> ret $ \y -> k (y,arg))

litP5 = litP4

-- Inline un_consA1 into intP4
intP5 = \tD arg ->
  shift (\k -> ret $ \y -> k (y,arg)) >== \(n,arg) ->
  tD arg >== ret . consS (show (n::Int)) 

charP5 = \tD arg ->
  un_consA1 arg >== \(c,l2) ->
  tD l2 >== ret . consS (show (c::Char)) 

nilDP5 _ = ret nilS

desc05 = consDP (litP5 "lit") $ consDP intP5 nilDP5
desc05r = run $ (reset (desc05 ()) `app` 5)
-- "lit5"

descP5 = consDP intP5
    (consDP (litP5 "-th character after ")
       (consDP charP5
          (consDP (litP5 " is ")
             (consDP charP5
                nilDP5))))

printf5 desc = reset (desc ())

descr5 = run $ printf5 descP5 `app` 5 `app` 'a' `app` 'f'
-- "5-th character after 'a' is 'f'"

-- After several transformations described in the paper (eta-reductions mainly)

intP6 = \tD () ->
  shift (\k -> ret k) >== \n ->
  tD () >== ret . consS (show (n::Int)) 


litP7 str = \() -> ret str

intP7 = \() ->
  shift (\k -> ret k) >== \n ->
  ret (show (n::Int))

charP7 = \() ->
  shift (\k -> ret k) >== \c ->
  ret (show (c::Char))


infixr 7 ^^^ 
-- Lifted string concatenation
f ^^^ g = \() -> f () >== \s1 ->
                 g () >== \s2 ->
		 ret (s1 ++ s2)


printf7 desc = reset $ desc ()

descP7 = intP7 ^^^ (litP7 "-th character after ") ^^^ charP7 ^^^
	 (litP7 " is ") ^^^ charP7


descr7 = run $ printf7 descP7 `app` 5 `app` 'a' `app` 'f'
-- "5-th character after 'a' is 'f'"