{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable         #-}

{-| Split tree for transforming pattern clauses into case trees.

The coverage checker generates a split tree from the clauses.
The clause compiler uses it to transform clauses to case trees.

The initial problem is a set of clauses.  The root node designates
on which argument to split and has subtrees for all the constructors.
Splitting continues until there is only a single clause left at
each leaf of the split tree.

-}
module Agda.TypeChecking.Coverage.SplitTree where

import Data.Tree
import Data.Data (Data, toConstr)

import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position

import Agda.Utils.Monad
import Agda.Utils.Pretty

#include "undefined.h"
import Agda.Utils.Impossible

type SplitTree  = SplitTree'  SplitTag
type SplitTrees = SplitTrees' SplitTag

-- | Abstract case tree shape.
data SplitTree' a
  = -- | No more splits coming. We are at a single, all-variable
    -- clause.
    SplittingDone
    { splitBindings :: Int       -- ^  The number of variables bound in the clause
    }
  | -- | A split is necessary.
    SplitAt
    { splitArg   :: Arg Int       -- ^ Arg. no to split at.
    , splitTrees :: SplitTrees' a -- ^ Sub split trees.
    }
  deriving (Data, Show)

-- | Split tree branching.  A finite map from constructor names to splittrees
--   A list representation seems appropriate, since we are expecting not
--   so many constructors per data type, and there is no need for
--   random access.
type SplitTrees' a = [(a, SplitTree' a)]

-- | Tag for labeling branches of a split tree. Each branch is associated to
--   either a constructor or a literal, or is a catchall branch (currently
--   only used for splitting on a literal type).
data SplitTag
  = SplitCon QName
  | SplitLit Literal
  | SplitCatchall
  deriving (Show, Eq, Ord, Data)

instance Pretty SplitTag where
  pretty (SplitCon c)  = pretty c
  pretty (SplitLit l)  = pretty l
  pretty SplitCatchall = underscore

-- * Printing a split tree

data SplitTreeLabel a = SplitTreeLabel
  { lblConstructorName :: Maybe a   -- ^ 'Nothing' for root of split tree
  , lblSplitArg        :: Maybe (Arg Int)
  , lblBindings        :: Maybe Int
  }
instance Pretty a => Pretty (SplitTreeLabel a) where
  pretty = \case
    SplitTreeLabel Nothing Nothing (Just n)  -> text $ "done, " ++ prettyShow n ++ " bindings"
    SplitTreeLabel Nothing (Just n) Nothing  -> text $ "split at " ++ prettyShow n
    SplitTreeLabel (Just q) Nothing (Just n) -> pretty q <+> text (" -> done, " ++ prettyShow n ++ " bindings")
    SplitTreeLabel (Just q) (Just n) Nothing -> pretty q <+> text (" -> split at " ++ prettyShow n)
    _ -> __IMPOSSIBLE__

-- | Convert a split tree into a 'Data.Tree' (for printing).
toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
toTree t = case t of
  SplittingDone n -> Node (SplitTreeLabel Nothing Nothing (Just n)) []
  SplitAt n ts    -> Node (SplitTreeLabel Nothing (Just n) Nothing) $ toTrees ts

toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees = map (\ (c,t) -> setCons c $ toTree t)
  where
    setCons :: a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
    setCons c (Node l ts) = Node (l { lblConstructorName = Just c }) ts

instance Pretty a => Pretty (SplitTree' a) where
  pretty = text . drawTree . fmap prettyShow . toTree

instance KillRange SplitTag where
  killRange = \case
    SplitCon c -> killRange1 SplitCon c
    SplitLit l -> killRange1 SplitLit l
    SplitCatchall -> SplitCatchall

instance KillRange a => KillRange (SplitTree' a) where
  killRange = \case
    SplittingDone n -> SplittingDone n
    SplitAt i ts    -> killRange1 (SplitAt i) ts