{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

-- | This module defines one function that takes a polymorphic parser and transforms it into a specific parser that recognises the same sentences as the input parser, but simultaneously constructs a parse tree annotated with position information.
module Reify (reify) where

import Control.Applicative
import Generics.MultiRec
import Satisfy
import Token
import ParsecInstance
import Annotations
import BoundsParser
import Eq1
import MultiRecShow ()
import qualified SavePos as S
import Any

import Generics.MultiRec
import Generics.MultiRec.HFix
import Control.Arrow ((***), second)
import Control.Monad.State

import qualified Text.Parsec as P

data Parser :: * -> (* -> *) -> * -> * where
  -- Primitives
  Satisfy :: (sym -> Bool) -> Parser sym fam sym

  -- Pointed
  Point :: a -> Parser sym fam a

  -- Functor
  Fmap :: (a -> b) -> Parser sym fam a -> Parser sym fam b

  -- Applicative
  Apply :: Parser sym fam (a -> b) -> Parser sym fam a -> Parser sym fam b
  
  -- Alternative
  Empty :: Parser sym fam a
  Or :: Parser sym fam a -> Parser sym fam a -> Parser sym fam a
  
  -- Annotate
  Ann :: (HFunctor (PF fam), Ix fam a) => Parser sym fam a -> Parser sym fam a
  Chainl :: (HFunctor (PF fam), Ix fam a) => Parser sym fam a -> Parser sym fam (a -> a -> a) -> Parser sym fam a

instance Functor (Parser sym fam) where
  fmap = Fmap

instance Applicative (Parser sym fam) where
  pure = Point
  (<*>) = Apply

instance Alternative (Parser sym fam) where
  empty = Empty
  (<|>) = Or

instance Satisfy (Parser sym fam) where
  type Input (Parser sym fam) = sym
  satisfy = Satisfy

instance HFunctor (PF fam) => S.SavePos (Parser sym fam) where
  type S.DataFam (Parser sym fam) = fam
  savePos = Ann
  chainl = Chainl

instance Show (Parser sym fam a) where
  show = showParser

showParser :: Parser sym fam a -> String
showParser p = case p of
  Satisfy _ -> "S"
  Point _   -> "P"
  Fmap _ p  -> {- "F" ++ -} show p
  Apply p q -> showParser p ++ " * " ++ showParser q
  Empty     -> "E"
  Or p q    -> showParser p ++ " + " ++ showParser q
  Ann p     -> "[" ++ showParser p ++ "]"
  Chainl p q  -> "L(" ++ showParser p ++ ", " ++ showParser q ++ ")"

-- discardPos :: Parser sym fam a -> SatisfyA sym a
-- discardPos p = case p of
--   Satisfy f -> satisfy f
--   Point x   -> pure x
--   Fmap f x  -> fmap f (discardPos x)
--   Apply f x -> discardPos f <*> discardPos x
--   Empty     -> empty
--   Or p q    -> discardPos p <|> discardPos q
--   Ann p     -> discardPos p
--   Chainl p q  -> chainl' (discardPos p) (discardPos q)

-- chainl' :: (Alternative f) => f a -> f (a -> a -> a) -> f a
-- chainl' p op = (\x f -> f x) <$> p <*> rest
--   where
--     rest = ((\f y r x -> r (f x y)) <$> op <*> p <*> rest) <|> pure id

toParsec' :: forall sym fam a. (Symbol sym, Show sym, Eq1 fam) => Parser sym fam a -> P.Parsec [sym] () (a, [AnyWithBounds fam])
toParsec' p = case p of
  Satisfy f   -> (\x -> (x, [])) <$> parsecSatisfy f
  Point x     -> return (x, [])
  Fmap f px   -> (f *** id) <$> toParsec' px
  Apply pf px -> (\(f, cs) (x, cs') -> (f x, cs ++ cs')) <$> toParsec' pf <*> toParsec' px
  Empty       -> empty
  Or p q      -> toParsec' p <|> toParsec' q
  Ann px      -> do
    lb <- getLeftBounds
    (x, cs) <- toParsec' px
    rb <- getRightBounds
    -- For some reason xpf needs to be defined in a separate let.
    let xpf = from x -- :: Str fam a
    case runState (hmapM distribute xpf) cs of
      (xpf', [])  -> return (x, [mkAnyF (HIn (K (mkBounds lb rb) :*: xpf'))])
      (_, _)      -> error "structure mismatch: too many children"
  Chainl p q  -> do
    lb <- getLeftBounds
    (x, [x']) <- toParsec' p
    let rest :: (a, AnyWithBounds fam) -> P.Parsec [sym] () (a, AnyWithBounds fam)
        rest (x, x') = P.option (x, x') $ do
          (f, [])   <- toParsec' q
          (y, [y']) <- toParsec' p
          rb <- getRightBounds
          let z = f x y
          let zpf = from z
          z' <- case runState (hmapM distribute zpf) [x', y'] of
            (z', [])  -> return (mkAnyF (HIn (K (mkBounds lb rb) :*: z')))
            (_, _)    -> error "structure mismatch: too many children"          
          rest (z, z')
    second pure <$> rest (x, x')

-- | Reifies a polymorphic parser as a Parsec parser that also yields a tree with subexpression bounds.
reify :: forall sym fam a. (Symbol sym, Show sym, Eq1 fam, HFunctor (PF fam), Ix fam a) => S.SatisfyA sym fam a -> P.Parsec [sym] () (a, WithBounds fam a)
reify p = do
  (x, cs) <- toParsec' p
  let check :: forall b. Maybe (a :=: b) -> WithBounds fam b -> P.Parsec [sym] () (a, WithBounds fam a)
      check mw x' = case mw of
        Nothing -> fail "The top-level value is not of the right type."
        Just Refl -> do
          return (x, x')
  case cs of
    [AnyF w x'] -> check (eq1 index w) x'
    _ -> fail "Parser yields multiple top-level values."

-- | For use in hmapM. Distributes a list of children over a pattern functor's children, overwriting them.
distribute :: (Eq1 s, Ix s ix) => s ix -> a -> State [AnyWithBounds s] (WithBounds s ix)
distribute w _ = do
  xs <- get
  case xs of
    [] -> error "structure mismatch: too few children"
    AnyF w' x : xs' -> case eq1 w w' of
      Nothing   -> error "structure mismatch: incompatible child type"
      Just Refl -> do put xs'; return x