content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  -- | Sanity checking for internal syntax. Mostly checking variable scoping.
  module Agda.Syntax.Internal.SanityCheck where
  
  import Control.Monad
  
  import Agda.Syntax.Internal
  import Agda.TypeChecking.Free
  import Agda.TypeChecking.Monad
  
  import Agda.Utils.List ( dropEnd, initWithDefault )
  import Agda.Syntax.Common.Pretty
  import Agda.Utils.Size
  import Agda.Utils.Impossible
  import qualified Agda.Utils.VarSet as VarSet
  
  
  sanityCheckVars :: (Pretty a, Free a) => Telescope -> a -> TCM ()
  sanityCheckVars tel v =
    case filter bad (VarSet.toAscList $ allFreeVars v) of
      [] -> return ()
      xs -> do
        alwaysReportSDoc "impossible" 1 . return $
          sep [ hang "Sanity check failed for" 2
                     (hang (pretty tel <+> "|-") 2 (pretty v))
              , text $ "out of scope: " ++ show xs ]
        __IMPOSSIBLE__
    where
      n     = size tel
      bad x = x < 0 || x >= n
  
  -- | Check that @Γ ⊢ ρ : Δ@.
  sanityCheckSubst :: (Pretty a, Free a) => Telescope -> Substitution' a -> Telescope -> TCM ()
  sanityCheckSubst gamma rho delta = go gamma rho delta
    where
      go gamma rho delta =
        case rho of
  
          IdS      -> do
            unless (size gamma == size delta) $ err $
              "idS:" <+> hang (pretty gamma <+> "/=") 2 (pretty delta)
  
          EmptyS _ -> do
            unless (null delta) $ err $
              "emptyS:" <+> pretty delta <+> "is not empty"
  
          v :# rho -> do
            when (null delta) $ err $ "consS: empty target"
            sanityCheckVars gamma v
            sanityCheckSubst gamma rho (dropLast delta)
  
          Strengthen _ n rho -> do
            unless (natSize delta >= toEnum n) $ err $ "strS: empty target"
            sanityCheckSubst gamma rho (dropLastN n delta)
  
          Wk n rho -> do
            unless (natSize gamma >= toEnum n) $ err $
              "wkS:" <+> sep [ "|" <> pretty gamma <> "|" , text $ "< " ++ show n ]
            sanityCheckSubst (dropLastN n gamma) rho delta
  
          Lift n rho -> do
            unless (natSize gamma >= toEnum n) $ err $
              "liftS: source" <+> sep [ "|" <> pretty gamma <> "|" , text $ "< " ++ show n ]
            unless (natSize delta >= toEnum n) $ err $
              "liftS: target" <+> sep [ "|" <> pretty delta <> "|" , text $ "< " ++ show n ]
            sanityCheckSubst (dropLastN n gamma) rho (dropLastN n delta)
  
      dropLast = telFromList . initWithDefault __IMPOSSIBLE__ . telToList
      dropLastN n = telFromList . dropEnd n . telToList
  
      err reason = do
        alwaysReportSDoc "impossible" 1 . return $
          sep [ hang "Sanity check failed for" 2 $
                hang (pretty gamma <+> "|-") 2 $
                hang (pretty rho <+> ":") 2 $
                      pretty delta
              , reason ]
        __IMPOSSIBLE__
  