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 )
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Impossible
sanityCheckVars :: (Pretty a, Free a) => Telescope -> a -> TCM ()
sanityCheckVars :: Telescope -> a -> TCM ()
sanityCheckVars tel :: Telescope
tel v :: a
v =
case (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter Int -> Bool
bad (IntSet -> [Int]
Set.toList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ a -> IntSet
forall t. Free t => t -> IntSet
allFreeVars a
v) of
[] -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
xs :: [Int]
xs -> do
VerboseKey -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "impossible" 1 (TCM Doc -> TCM ()) -> (Doc -> TCM Doc) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
sep [ Doc -> Int -> Doc -> Doc
hang "Sanity check failed for" 2
(Doc -> Int -> Doc -> Doc
hang (Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
tel Doc -> Doc -> Doc
<+> "|-") 2 (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
v))
, VerboseKey -> Doc
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "out of scope: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [Int] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [Int]
xs ]
TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
where
n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
bad :: Int -> Bool
bad x :: Int
x = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 Bool -> Bool -> Bool
|| Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n
sanityCheckSubst :: (Pretty a, Free a) => Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst :: Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst gamma :: Telescope
gamma rho :: Substitution' a
rho delta :: Telescope
delta = Telescope -> Substitution' a -> Telescope -> TCM ()
forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
go Telescope
gamma Substitution' a
rho Telescope
delta
where
go :: Telescope -> Substitution' a -> Telescope -> TCM ()
go gamma :: Telescope
gamma rho :: Substitution' a
rho delta :: Telescope
delta =
case Substitution' a
rho of
IdS -> Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "idS:" Doc -> Doc -> Doc
<+> Doc -> Int -> Doc -> Doc
hang (Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
gamma Doc -> Doc -> Doc
<+> "/=") 2 (Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
delta)
EmptyS _ -> Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "emptyS:" Doc -> Doc -> Doc
<+> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
delta Doc -> Doc -> Doc
<+> "is not empty"
v :: a
v :# rho :: Substitution' a
rho -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "consS: empty target"
Telescope -> a -> TCM ()
forall a. (Pretty a, Free a) => Telescope -> a -> TCM ()
sanityCheckVars Telescope
gamma a
v
Telescope -> Substitution' a -> Telescope -> TCM ()
forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst Telescope
gamma Substitution' a
rho (Telescope -> Telescope
dropLast Telescope
delta)
Strengthen _ rho :: Substitution' a
rho -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "strS: empty target"
Telescope -> Substitution' a -> Telescope -> TCM ()
forall a.
(Pretty a, Free a) =>
Telescope -> Substitution' a -> Telescope -> TCM ()
sanityCheckSubst Telescope
gamma Substitution' a
rho (Telescope -> Telescope
dropLast Telescope
delta)
Wk n :: Int
n rho :: Substitution' a
rho -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "wkS:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [ "|" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
gamma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> "|"
, VerboseKey -> Doc
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "< " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show Int
n ]
Telescope -> Substitution' a -> Telescope -> TCM ()
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 n :: Int
n rho :: Substitution' a
rho -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "liftS: source" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [ "|" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
gamma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> "|"
, VerboseKey -> Doc
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "< " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show Int
n ]
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
forall (m :: * -> *) b. MonadDebug m => Doc -> m b
err (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "liftS: target" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [ "|" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
delta Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> "|"
, VerboseKey -> Doc
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "< " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show Int
n ]
Telescope -> Substitution' a -> Telescope -> TCM ()
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 (ListTel -> Telescope)
-> (Telescope -> ListTel) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListTel -> ListTel
forall a. [a] -> [a]
init (ListTel -> ListTel)
-> (Telescope -> ListTel) -> Telescope -> ListTel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList
dropLastN :: Int -> Telescope -> Telescope
dropLastN n :: Int
n = ListTel -> Telescope
telFromList (ListTel -> Telescope)
-> (Telescope -> ListTel) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
dropEnd Int
n (ListTel -> ListTel)
-> (Telescope -> ListTel) -> Telescope -> ListTel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList
err :: Doc -> m b
err reason :: Doc
reason = do
VerboseKey -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCM Doc -> m ()
reportSDoc "impossible" 1 (TCM Doc -> m ()) -> (Doc -> TCM Doc) -> Doc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m ()) -> Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
sep [ Doc -> Int -> Doc -> Doc
hang "Sanity check failed for" 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc -> Int -> Doc -> Doc
hang (Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
gamma Doc -> Doc -> Doc
<+> "|-") 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc -> Int -> Doc -> Doc
hang (Substitution' a -> Doc
forall a. Pretty a => a -> Doc
pretty Substitution' a
rho Doc -> Doc -> Doc
<+> ":") 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
delta
, Doc
reason ]
m b
forall a. HasCallStack => a
__IMPOSSIBLE__