{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

{-| Proof-irrelevant propositions.
-}

module Mikan.TypeChecking.Irrelevance where

import Mikan.Syntax.Internal

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Telescope

import Mikan.Utils.Either (fromRightM)
import Mikan.Utils.Monad

import Mikan.Utils.Impossible

-- * Propositions

-- | Is a type a proposition?  (Needs reduction.)

{-# SPECIALIZE isPropM :: Dom Type -> TCM Bool #-}
isPropM :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool
isPropM :: forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM a
a = do
  let s :: Sort
s = a -> Sort
forall a. LensSort a => a -> Sort
getSort a
a
  VerboseKey -> VerboseLevel -> TCMT IO Doc -> m Bool -> m Bool
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m a -> m a
traceSDoc VerboseKey
"tc.prop" VerboseLevel
80 (TCMT IO Doc
"Is " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"in Prop?") do
  Sort -> Bool
forall t. Sort' t -> Bool
isProp (Sort -> Bool) -> m Sort -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Sort
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Sort
s

allPropTel
  :: (PureTCM m, MonadBlock m)
  => Telescope -> m Bool
allPropTel :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Telescope -> m Bool
allPropTel =
  (Dom (ArgName, Type) -> m Bool -> m Bool)
-> m Bool -> Telescope -> m Bool
forall (m :: * -> *) b.
MonadAddContext m =>
(Dom (ArgName, Type) -> m b -> m b) -> m b -> Telescope -> m b
foldrTelescopeM (m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M (m Bool -> m Bool -> m Bool)
-> (Dom (ArgName, Type) -> m Bool)
-> Dom (ArgName, Type)
-> m Bool
-> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> m Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM (Dom Type -> m Bool)
-> (Dom (ArgName, Type) -> Dom Type)
-> Dom (ArgName, Type)
-> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd) (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)

-- * Fibrant types

-- | Is a type fibrant (i.e. Type, Prop)?

isFibrant :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool
isFibrant :: forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant = (Blocker -> m Bool) -> m (Either Blocker Bool) -> m Bool
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM Blocker -> m Bool
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (m (Either Blocker Bool) -> m Bool)
-> (a -> m (Either Blocker Bool)) -> a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m (Either Blocker Bool)
forall a (m :: * -> *).
(LensSort a, PureTCM m) =>
a -> m (Either Blocker Bool)
isFibrant'

isFibrant' :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)
isFibrant' :: forall a (m :: * -> *).
(LensSort a, PureTCM m) =>
a -> m (Either Blocker Bool)
isFibrant' a
s =
  Sort
-> (Blocker -> Sort -> m (Either Blocker Bool))
-> (NotBlocked -> Sort -> m (Either Blocker Bool))
-> m (Either Blocker Bool)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
s) (\ Blocker
blocker Sort
_ -> Either Blocker Bool -> m (Either Blocker Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker Bool -> m (Either Blocker Bool))
-> Either Blocker Bool -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Blocker -> Either Blocker Bool
forall a b. a -> Either a b
Left Blocker
blocker) \ NotBlocked
_ ->
    Either Blocker Bool -> m (Either Blocker Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker Bool -> m (Either Blocker Bool))
-> (Sort -> Either Blocker Bool) -> Sort -> m (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right (Bool -> Either Blocker Bool)
-> (Sort -> Bool) -> Sort -> Either Blocker Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      Univ Univ
u Level' Term
_       -> Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
      Inf Univ
u Integer
_        -> Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
      LevelUniv{}    -> Bool
False
      IntervalUniv{} -> Bool
False
      CofUniv{}      -> Bool
False
      PiSort{}       -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      FunSort{}      -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      UnivSort{}     -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaS{}        -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      DefS{}         -> Bool
False
      DummyS{}       -> Bool
False


-- | Cofibrant types are those that could be the domain of a fibrant
--   pi type. (Notion by C. Sattler).
isCoFibrantSort :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)
isCoFibrantSort :: forall a (m :: * -> *).
(LensSort a, PureTCM m) =>
a -> m (Either Blocker Bool)
isCoFibrantSort a
s =
  Sort
-> (Blocker -> Sort -> m (Either Blocker Bool))
-> (NotBlocked -> Sort -> m (Either Blocker Bool))
-> m (Either Blocker Bool)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
s) (\ Blocker
blocker Sort
_ -> Either Blocker Bool -> m (Either Blocker Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker Bool -> m (Either Blocker Bool))
-> Either Blocker Bool -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Blocker -> Either Blocker Bool
forall a b. a -> Either a b
Left Blocker
blocker) \ NotBlocked
_ ->
    Either Blocker Bool -> m (Either Blocker Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Blocker Bool -> m (Either Blocker Bool))
-> (Sort -> Either Blocker Bool) -> Sort -> m (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right (Bool -> Either Blocker Bool)
-> (Sort -> Bool) -> Sort -> Either Blocker Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      Univ Univ
u Level' Term
_       -> Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
      Inf Univ
u Integer
_        -> Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
      LevelUniv{}    -> Bool
False
      CofUniv{}      -> Bool
False
      IntervalUniv{} -> Bool
True
      PiSort{}       -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      FunSort{}      -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      UnivSort{}     -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaS{}        -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      DefS{}         -> Bool
False
      DummyS{}       -> Bool
False