{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Mikan.TypeChecking.Reduce.Monad
  ( enterClosure
  , getConstInfo
  , askR, applyWhenVerboseS
  ) where

import Prelude hiding (null)

import Control.Applicative

import Data.Map qualified as Map

import System.IO.Unsafe

import Mikan.Syntax.Common.Pretty () --instance only
import Mikan.Syntax.Internal

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Substitute

import Mikan.Utils.Monad

instance HasBuiltins ReduceM where
  getBuiltinThing :: SomeBuiltin -> ReduceM (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b =
    (Maybe (Builtin PrimFun)
 -> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe (Builtin PrimFun)
-> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)
      (SomeBuiltin
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins)
      (SomeBuiltin
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins)

withFreshR :: (ReadTCState m, HasFresh i) => (i -> m a) -> m a
withFreshR :: forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR i -> m a
f = do
  s <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  let (i, s') = nextFresh s
  withTCState (const s') (f i)

instance MonadAddContext ReduceM where
  withFreshName :: forall a. Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a
withFreshName Range
r ArgName
s Name -> ReduceM a
k = (NameId -> ReduceM a) -> ReduceM a
forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR ((NameId -> ReduceM a) -> ReduceM a)
-> (NameId -> ReduceM a) -> ReduceM a
forall a b. (a -> b) -> a -> b
$ \NameId
i -> Name -> ReduceM a
k (Range -> NameId -> ArgName -> Name
mkName Range
r NameId
i ArgName
s)

  addCtx :: forall a. Name -> Dom Type -> ReduceM a -> ReduceM a
addCtx = Name -> Dom Type -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
defaultAddCtx

  addLetBinding' :: forall a.
IsAxiom
-> Origin -> Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
addLetBinding' = IsAxiom
-> Origin -> Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding'

  {-# INLINE updateContext #-}
  updateContext :: forall a.
Substitution -> (Context -> Context) -> ReduceM a -> ReduceM a
updateContext Substitution
rho Context -> Context
f ReduceM a
ret = (CheckpointId -> ReduceM a) -> ReduceM a
forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR \CheckpointId
chkpt ->
    (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a
forall a. (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (  ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over' ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext Context -> Context
f
             (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv CheckpointId CheckpointId
-> CheckpointId -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv CheckpointId CheckpointId
Lens' TCEnv CheckpointId
eCurrentCheckpoint CheckpointId
chkpt
             (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
  TCEnv
  TCEnv
  (Map CheckpointId Substitution)
  (Map CheckpointId Substitution)
-> (Map CheckpointId Substitution -> Map CheckpointId Substitution)
-> TCEnv
-> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  TCEnv
  TCEnv
  (Map CheckpointId Substitution)
  (Map CheckpointId Substitution)
Lens' TCEnv (Map CheckpointId Substitution)
eCheckpoints (CheckpointId
-> Substitution
-> Map CheckpointId Substitution
-> Map CheckpointId Substitution
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CheckpointId
chkpt Substitution
forall a. Substitution' a
IdS (Map CheckpointId Substitution -> Map CheckpointId Substitution)
-> (Map CheckpointId Substitution -> Map CheckpointId Substitution)
-> Map CheckpointId Substitution
-> Map CheckpointId Substitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Substitution -> Substitution)
-> Map CheckpointId Substitution -> Map CheckpointId Substitution
forall a b. (a -> b) -> Map CheckpointId a -> Map CheckpointId b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg Substitution)
-> Substitution -> Substitution
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Substitution)
rho)))
            ReduceM a
ret

        -- let-bindings keep track of own their context

instance MonadDebug ReduceM where

  traceDebugMessage :: forall a.
VerboseKey -> VerboseLevel -> Doc -> ReduceM a -> ReduceM a
traceDebugMessage VerboseKey
k VerboseLevel
n Doc
s ReduceM a
cont = do
    ReduceEnv env st _ _ <- ReduceM ReduceEnv
askR
    unsafePerformIO $ do
      _ <- runTCM env st $ traceDebugMessage k n s $ pure ()
      return $ cont

  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReduceM Doc
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = do
    ReduceEnv env st _ _ <- ReduceM ReduceEnv
askR
    unsafePerformIO $ do
      (s , _) <- runTCM env st $ formatDebugMessage k n d
      return $ return s

#ifdef DEBUG
  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> ReduceM a -> ReduceM a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey
-> VerboseLevel
-> (ReduceM a -> ReduceM a)
-> ReduceM a
-> ReduceM a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((ReduceM a -> ReduceM a) -> ReduceM a -> ReduceM a)
-> (ReduceM a -> ReduceM a) -> ReduceM a -> ReduceM a
forall a b. (a -> b) -> a -> b
$
    ReduceM () -> (() -> ReduceM ()) -> ReduceM a -> ReduceM a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (VerboseKey -> VerboseLevel -> VerboseKey -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s) (ReduceM () -> () -> ReduceM ()
forall a b. a -> b -> a
const (ReduceM () -> () -> ReduceM ()) -> ReduceM () -> () -> ReduceM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> ReduceM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n)
#else
  verboseBracket k n s ma = ma
  {-# INLINE verboseBracket #-}
#endif

  getVerbosity :: ReduceM Verbosity
getVerbosity      = ReduceM Verbosity
forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  getProfileOptions :: ReduceM ProfileOptions
getProfileOptions = ReduceM ProfileOptions
forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions
  isDebugPrinting :: ReduceM Bool
isDebugPrinting   = ReduceM Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. ReduceM a -> ReduceM a
nowDebugPrinting  = ReduceM a -> ReduceM a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting

instance HasConstInfo ReduceM where
  getConstInfo' :: HasCallStack => QName -> ReduceM (Either SigError Definition)
getConstInfo' QName
q = do
    ReduceEnv env st _ _ <- ReduceM ReduceEnv
askR
    defaultGetConstInfo st env q

instance PureTCM ReduceM where