{-# OPTIONS_GHC -Wunused-imports #-}

-- | Sanity checking for internal syntax. Mostly checking variable scoping.
module Agda.Syntax.Internal.SanityCheck where

import Control.Monad
import qualified Data.IntSet as Set

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


sanityCheckVars :: (Pretty a, Free a) => Telescope -> a -> TCM ()
sanityCheckVars :: forall a. (Pretty a, Free a) => Telescope -> a -> TCM ()
sanityCheckVars Telescope
tel a
v =
  case forall a. (a -> Bool) -> [a] -> [a]
filter Int -> Bool
bad (IntSet -> [Int]
Set.toList forall a b. (a -> b) -> a -> b
$ forall t. Free t => t -> IntSet
allFreeVars a
v) of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [Int]
xs -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM (Doc Aspects) -> m ()
alwaysReportSDoc [Char]
"impossible" Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ forall a. Doc a -> Int -> Doc a -> Doc a
hang Doc Aspects
"Sanity check failed for" Int
2
                   (forall a. Doc a -> Int -> Doc a -> Doc a
hang (forall a. Pretty a => a -> Doc Aspects
pretty Telescope
tel forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"|-") Int
2 (forall a. Pretty a => a -> Doc Aspects
pretty a
v))
            , forall a. [Char] -> Doc a
text forall a b. (a -> b) -> a -> b
$ [Char]
"out of scope: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Int]
xs ]
      forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    n :: Int
n     = forall a. Sized a => a -> Int
size Telescope
tel
    bad :: Int -> Bool
bad Int
x = Int
x forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
x forall a. Ord a => a -> a -> Bool
>= Int
n

-- | Check that @Γ ⊢ ρ : Δ@.
sanityCheckSubst :: (Pretty a, Free a) => Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst :: forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst Telescope
gamma Substitution' a
rho Telescope
delta = Telescope -> Substitution' a -> Telescope -> TCM ()
go Telescope
gamma Substitution' a
rho Telescope
delta
  where
    go :: Telescope -> Substitution' a -> Telescope -> TCM ()
go Telescope
gamma Substitution' a
rho Telescope
delta =
      case Substitution' a
rho of

        Substitution' a
IdS      -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Telescope
gamma forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size Telescope
delta) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$
            Doc Aspects
"idS:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a -> Int -> Doc a -> Doc a
hang (forall a. Pretty a => a -> Doc Aspects
pretty Telescope
gamma forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"/=") Int
2 (forall a. Pretty a => a -> Doc Aspects
pretty Telescope
delta)

        EmptyS Impossible
_ -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Telescope
delta) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$
            Doc Aspects
"emptyS:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc Aspects
pretty Telescope
delta forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"is not empty"

        a
v :# Substitution' a
rho -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Telescope
delta) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$ Doc Aspects
"consS: empty target"
          forall a. (Pretty a, Free a) => Telescope -> a -> TCM ()
sanityCheckVars Telescope
gamma a
v
          forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst Telescope
gamma Substitution' a
rho (Telescope -> Telescope
dropLast Telescope
delta)

        Strengthen Impossible
_ Int
n Substitution' a
rho -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Peano
natSize Telescope
delta forall a. Ord a => a -> a -> Bool
>= forall a. Enum a => Int -> a
toEnum Int
n) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$ Doc Aspects
"strS: empty target"
          forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst Telescope
gamma Substitution' a
rho (Int -> Telescope -> Telescope
dropLastN Int
n Telescope
delta)

        Wk Int
n Substitution' a
rho -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Peano
natSize Telescope
gamma forall a. Ord a => a -> a -> Bool
>= forall a. Enum a => Int -> a
toEnum Int
n) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$
            Doc Aspects
"wkS:" forall a. Doc a -> Doc a -> Doc a
<+> forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Doc Aspects
"|" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc Aspects
pretty Telescope
gamma forall a. Semigroup a => a -> a -> a
<> Doc Aspects
"|" , forall a. [Char] -> Doc a
text forall a b. (a -> b) -> a -> b
$ [Char]
"< " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n ]
          forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst (Int -> Telescope -> Telescope
dropLastN Int
n Telescope
gamma) Substitution' a
rho Telescope
delta

        Lift Int
n Substitution' a
rho -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Peano
natSize Telescope
gamma forall a. Ord a => a -> a -> Bool
>= forall a. Enum a => Int -> a
toEnum Int
n) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$
            Doc Aspects
"liftS: source" forall a. Doc a -> Doc a -> Doc a
<+> forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Doc Aspects
"|" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc Aspects
pretty Telescope
gamma forall a. Semigroup a => a -> a -> a
<> Doc Aspects
"|" , forall a. [Char] -> Doc a
text forall a b. (a -> b) -> a -> b
$ [Char]
"< " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n ]
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Peano
natSize Telescope
delta forall a. Ord a => a -> a -> Bool
>= forall a. Enum a => Int -> a
toEnum Int
n) forall a b. (a -> b) -> a -> b
$ Doc Aspects -> TCM ()
err forall a b. (a -> b) -> a -> b
$
            Doc Aspects
"liftS: target" forall a. Doc a -> Doc a -> Doc a
<+> forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Doc Aspects
"|" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc Aspects
pretty Telescope
delta forall a. Semigroup a => a -> a -> a
<> Doc Aspects
"|" , forall a. [Char] -> Doc a
text forall a b. (a -> b) -> a -> b
$ [Char]
"< " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n ]
          forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst (Int -> Telescope -> Telescope
dropLastN Int
n Telescope
gamma) Substitution' a
rho (Int -> Telescope -> Telescope
dropLastN Int
n Telescope
delta)

    dropLast :: Telescope -> Telescope
dropLast = ListTel -> Telescope
telFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a] -> [a]
initWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList
    dropLastN :: Int -> Telescope -> Telescope
dropLastN Int
n = ListTel -> Telescope
telFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
dropEnd Int
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList

    err :: Doc Aspects -> TCM ()
err Doc Aspects
reason = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM (Doc Aspects) -> m ()
alwaysReportSDoc [Char]
"impossible" Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ forall a. Doc a -> Int -> Doc a -> Doc a
hang Doc Aspects
"Sanity check failed for" Int
2 forall a b. (a -> b) -> a -> b
$
              forall a. Doc a -> Int -> Doc a -> Doc a
hang (forall a. Pretty a => a -> Doc Aspects
pretty Telescope
gamma forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"|-") Int
2 forall a b. (a -> b) -> a -> b
$
              forall a. Doc a -> Int -> Doc a -> Doc a
hang (forall a. Pretty a => a -> Doc Aspects
pretty Substitution' a
rho forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":") Int
2 forall a b. (a -> b) -> a -> b
$
                    forall a. Pretty a => a -> Doc Aspects
pretty Telescope
delta
            , Doc Aspects
reason ]
      forall a. HasCallStack => a
__IMPOSSIBLE__