{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}

#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
#endif

-- | 'KillRange' instances for data structures from "Agda.TypeChecking.Monad.Base".

-- Andreas, 2014-05-03
module Agda.TypeChecking.Monad.Base.KillRange where

import Data.Map (Map)
import qualified Data.Map as Map

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.CompiledClause

import Agda.Utils.Permutation

instance KillRange Signature where
  killRange (Sig secs defs) = killRange2 Sig secs defs

instance KillRange Sections where
  killRange = fmap killRange

instance KillRange Definitions where
  killRange = fmap killRange

instance KillRange Section where
  killRange (Section tel freeVars) = killRange2 Section tel freeVars

instance KillRange Definition where
  killRange (Defn ai name t pols occs displ mut compiled rew inst def) =
    killRange11 Defn ai name t pols occs displ mut compiled rew inst def
    -- TODO clarify: Keep the range in the defName field?

instance KillRange NLPat where
  killRange (PVar x)   = killRange1 PVar x
  killRange (PWild)    = PWild
  killRange (PDef x y) = killRange2 PDef x y
  killRange (PTerm x)  = killRange1 PTerm x

instance KillRange RewriteRule where
  killRange (RewriteRule q gamma lhs rhs t) =
    killRange5 RewriteRule q gamma lhs rhs t

instance KillRange CompiledRepresentation where
  killRange = id

instance KillRange Defn where
  killRange def =
    case def of
      Axiom -> Axiom
      Function cls comp inv mut isAbs delayed proj static copy term extlam with cop ->
        killRange13 Function cls comp inv mut isAbs delayed proj static copy term extlam with cop
      Datatype a b c d e f g h i j   -> killRange10 Datatype a b c d e f g h i j
      Record a b c d e f g h i j k l -> killRange12 Record a b c d e f g h i j k l
      Constructor a b c d e          -> killRange5 Constructor a b c d e
      Primitive a b c d              -> killRange4 Primitive a b c d

instance KillRange MutualId where
  killRange = id

instance KillRange c => KillRange (FunctionInverse' c) where
  killRange NotInjective = NotInjective
  killRange (Inverse m)  = Inverse $ killRangeMap m

instance KillRange TermHead where
  killRange SortHead     = SortHead
  killRange PiHead       = PiHead
  killRange (ConsHead q) = ConsHead $ killRange q

instance KillRange Projection where
  killRange (Projection a b c d e) = killRange4 Projection a b c d e

instance KillRange Occurrence where
  killRange = id

instance KillRange a => KillRange (Open a) where
  killRange = fmap killRange

instance KillRange DisplayForm where
  killRange (Display n vs dt) = killRange3 Display n vs dt

instance KillRange Polarity where
  killRange = id

instance KillRange DisplayTerm where
  killRange dt =
    case dt of
      DWithApp dt dts args -> killRange3 DWithApp dt dts args
      DCon q dts        -> killRange2 DCon q dts
      DDef q dts        -> killRange2 DDef q dts
      DDot v            -> killRange1 DDot v
      DTerm v           -> killRange1 DTerm v

-- * KillRange on CompiledClause

instance KillRange c => KillRange (WithArity c) where
  killRange = fmap killRange

instance KillRange c => KillRange (Case c) where
  killRange (Branches con lit all) = Branches
    (killRangeMap con)
    (killRangeMap lit)
    (killRange all)

instance KillRange CompiledClauses where
  killRange (Case i br) = killRange2 Case i br
  killRange (Done xs v) = killRange2 Done xs v
  killRange Fail        = Fail

-- * KillRange on standard data types and Utils

instance KillRange a => KillRange (Drop a) where
  killRange = fmap killRange

-- | Overlaps with @KillRange [a]@.
#if __GLASGOW_HASKELL__ >= 710
instance {-# OVERLAPPING #-} KillRange String where
#else
instance KillRange String where
#endif
  killRange = id

-- | Remove ranges in keys and values of a map.
killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)
killRangeMap = Map.mapKeysMonotonic killRange . Map.map killRange