# LANGUAGE DataKinds , DeriveFunctor , FlexibleContexts , LambdaCase , TypeApplications , TypeOperators #
module Path.Elab where

import Control.Carrier.Class
import Control.Carrier.Error.Either
import Control.Carrier.Reader hiding (Local)
import Control.Carrier.Writer.Strict
import Control.Monad (foldM)
import Data.Bifunctor (Bifunctor (..))
import Data.Foldable (foldl')
import qualified Data.Map as Map
import Data.Void
import Path.Core
import Path.Error
import Path.Module as Module
import Path.Name
import Path.Plicity (Plicit (..))
import Path.Problem
import Path.Scope
import Path.Span
import Path.Stack as Stack
import qualified Path.Surface as Surface
import Path.Syntax
import Path.Term
import Prelude hiding (pi)

assume :: ( Carrier sig m
          , Member (Error Notice) sig
          , Member (Reader Globals) sig
          , Member (Reader Excerpt) sig
          )
       => Qualified
       -> m (Term (Problem :+: Core) (Var (Fin n) Qualified) ::: Term (Problem :+: Core) (Var (Fin n) Qualified))
assume v = asks (Stack.find ((== v) . typedTerm)) >>= maybe (freeVariables (pure v)) (pure . (Var (F v) :::) . fmap F . typedType)

intro :: Monad m
      => (Term (Problem :+: Core) (Var (Fin ('S n)) a) -> m (Term (Problem :+: Core) (Var (Fin ('S n)) a) ::: Term (Problem :+: Core) (Var (Fin ('S n)) a)))
      -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
intro body = do
  let _A = meta type'
      _B = meta type'
  u <- goalIs _B (body (first FS <$> _A))
  pure (lamFin u ::: piFin _A _B)

> ) : :  
      => m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
      -> (Term (Problem :+: Core) (Var (Fin ('S n)) a) -> m (Term (Problem :+: Core) (Var (Fin ('S n)) a) ::: Term (Problem :+: Core) (Var (Fin ('S n)) a)))
      -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
t --> body = do
  t' <- goalIs type' t
  b' <- goalIs type' (body (first FS <$> t'))
  pure (piFin t' b' ::: type')

app :: Monad m
    => m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
    -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
    -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
app f a = do
  let _A = meta type'
      _B = meta type'
      _F = piFin _A _B
  f' <- goalIs _F f
  a' <- goalIs _A a
  pure (f' $$ a' ::: _F $$ a')


goalIs :: Monad m
       => Term (Problem :+: Core) (Var (Fin n) a)
       -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
       -> m (Term (Problem :+: Core) (Var (Fin n) a))
goalIs ty2 m = do
  tm1 ::: ty1 <- m
  let tm2 = meta (ty1 === ty2)
  pure (tm1 === tm2)

meta
  :: Term (Problem :+: Core) (Var (Fin n) a)
  -> Term (Problem :+: Core) (Var (Fin n) a)
meta ty = existsFin ty (pure (B FZ))


elab
  :: ( Carrier sig m
     , Member (Error Notice) sig
     , Member (Reader Globals) sig
     , Member (Reader Excerpt) sig
     )
  => Vec n (Term (Problem :+: Core) (Var (Fin n) Qualified))
  -> Term Surface.Surface (Var (Fin n) Qualified)
  -> m (Term (Problem :+: Core) (Var (Fin n) Qualified) ::: Term (Problem :+: Core) (Var (Fin n) Qualified))
elab ctx = \case
    Var (B n) -> pure (pure (B n) ::: ctx ! n)
    Var (F n) -> assume n
    Term t -> case t of
      Surface.Lam _ b -> intro (\ t -> elab' (VS t (fmap (first FS) <$> ctx)) (fromScopeFin <$> b))
      f Surface.:$ (_ :< a) -> app (elab' ctx f) (elab' ctx a)
      Surface.Type -> pure (type' ::: type')
> \ t ' - > elab ' ( VS t ' ( fmap ( first FS ) < $ > ctx ) ) ( fromScopeFin < $ > b )
  where elab' ctx m = spanIs (elab ctx <$> m)

elabDecl :: ( Carrier sig m
            , Member (Error Notice) sig
            , Member (Reader Globals) sig
            , Member (Reader ModuleName) sig
            )
         => Decl (Term Surface.Surface Qualified)
         -> m (Decl (Term (Problem :+: Core) Qualified))
elabDecl (Decl name d tm ty) = do
  ty' <- runSpanned (fmap strengthen . goalIs type' . elab VZ . fmap F) ty
  moduleName <- ask
  tm' <- runSpanned (fmap strengthen . local (:> (moduleName :.: name) ::: unSpanned ty') . goalIs (F <$> unSpanned ty') . elab VZ . fmap F) tm
  pure (Decl name d tm' ty')
  where strengthen :: Term (Problem :+: Core) (Var (Fin 'Z) Qualified) -> Term (Problem :+: Core) Qualified
        strengthen = fmap (var absurdFin id)

elabModule :: ( Carrier sig m
              , Member (Error Notice) sig
              , Member (Reader (ModuleGraph (Term (Problem :+: Core)) Void)) sig
              , Member (Writer (Stack Notice)) sig
              )
           => Module (Term Surface.Surface) Qualified
           -> m (Module (Term (Problem :+: Core)) Qualified)
elabModule m = runReader (moduleName m) . local @(ModuleGraph (Term (Problem :+: Core)) Void) (Module.restrict (Map.keysSet (moduleImports m))) $ do
  FIXME : do a topo sort on the decls ? or at least make their types known first ? or … ?
  decls <- foldM go mempty (moduleDecls m)
  pure m { moduleDecls = decls }
  where go decls decl = local (extendGraph decls) . withGlobals $ do
          (extendModule decls <$> elabDecl (instantiate (pure . qualified . (moduleDecls m Map.!)) <$> decl)) `catchError` ((decls <$) . logError)
        extendModule decls decl = Map.insert (declName decl) (bind (Just . unqualified) <$> decl) decls
        extendGraph decls (ModuleGraph g) = ModuleGraph @(Term (Problem :+: Core)) @Void (Map.insert (moduleName m) (bindTEither Left m { moduleDecls = decls }) g)
        qualified = (moduleName m :.:) . declName
        unqualified (_ :.: u) = u

withGlobals
  :: (Carrier sig m, Member (Reader (ModuleGraph (Term (Problem :+: Core)) Void)) sig)
  => ReaderC Globals m a
  -> m a
withGlobals m = do
  ctx <- asks @(ModuleGraph (Term (Problem :+: Core)) Void) toContext
  runReader @Globals ctx m
  where toContext g = foldl' definitions Nil (modules g)
        definitions ctx m = foldl' define ctx (moduleDecls m)
          where define ctx d = ctx :> (moduleName m :.: declName d) ::: inst (declType d)
                inst t = instantiateEither (pure . either (moduleName m :.:) id) (unSpanned t)

logError :: (Member (Writer (Stack Notice)) sig, Carrier sig m) => Notice -> m ()
logError = tell . (Nil :>)


type Globals = Stack (Qualified ::: Term (Problem :+: Core) Qualified)


identity, identityT, constant, constantT, constantTQ :: Term (Problem :+: Core) String

identity = lam "A" (lam "a" (pure "a"))
identityT = pi ("A" ::: type') (pi ("_" ::: pure "A") (pure "A"))
constant = lam "A" (lam "B" (lam "a" (lam "b" (pure "a"))))
constantT = pi ("A" ::: type') (pi ("B" ::: type') (pi ("_" ::: pure "A") (pi ("_" ::: pure "B") (pure "A"))))

constantTQ
  = exists ("_A" ::: type') (pi ("A" ::: pure "_A")
  ( exists ("_B" ::: type') (pi ("B" ::: pure "_B")
  ( pi ("_" ::: pure "A") (pi ("_" ::: pure "B") (pure "A"))))))

> body = do
# LANGUAGE DataKinds , DeriveFunctor , FlexibleContexts , LambdaCase , TypeApplications , TypeOperators #
module Path.Elab where

import Control.Carrier.Class
import Control.Carrier.Error.Either
import Control.Carrier.Reader hiding (Local)
import Control.Carrier.Writer.Strict
import Control.Monad (foldM)
import Data.Bifunctor (Bifunctor (..))
import Data.Foldable (foldl')
import qualified Data.Map as Map
import Data.Void
import Path.Core
import Path.Error
import Path.Module as Module
import Path.Name
import Path.Plicity (Plicit (..))
import Path.Problem
import Path.Scope
import Path.Span
import Path.Stack as Stack
import qualified Path.Surface as Surface
import Path.Syntax
import Path.Term
import Prelude hiding (pi)

assume :: ( Carrier sig m
          , Member (Error Notice) sig
          , Member (Reader Globals) sig
          , Member (Reader Excerpt) sig
          )
       => Qualified
       -> m (Term (Problem :+: Core) (Var (Fin n) Qualified) ::: Term (Problem :+: Core) (Var (Fin n) Qualified))
assume v = asks (Stack.find ((== v) . typedTerm)) >>= maybe (freeVariables (pure v)) (pure . (Var (F v) :::) . fmap F . typedType)

intro :: Monad m
      => (Term (Problem :+: Core) (Var (Fin ('S n)) a) -> m (Term (Problem :+: Core) (Var (Fin ('S n)) a) ::: Term (Problem :+: Core) (Var (Fin ('S n)) a)))
      -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
intro body = do
  let _A = meta type'
      _B = meta type'
  u <- goalIs _B (body (first FS <$> _A))
  pure (lamFin u ::: piFin _A _B)

> ) : :  
      => m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
      -> (Term (Problem :+: Core) (Var (Fin ('S n)) a) -> m (Term (Problem :+: Core) (Var (Fin ('S n)) a) ::: Term (Problem :+: Core) (Var (Fin ('S n)) a)))
      -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
  t' <- goalIs type' t
  b' <- goalIs type' (body (first FS <$> t'))
  pure (piFin t' b' ::: type')

app :: Monad m
    => m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
    -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
    -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
app f a = do
  let _A = meta type'
      _B = meta type'
      _F = piFin _A _B
  f' <- goalIs _F f
  a' <- goalIs _A a
  pure (f' $$ a' ::: _F $$ a')


goalIs :: Monad m
       => Term (Problem :+: Core) (Var (Fin n) a)
       -> m (Term (Problem :+: Core) (Var (Fin n) a) ::: Term (Problem :+: Core) (Var (Fin n) a))
       -> m (Term (Problem :+: Core) (Var (Fin n) a))
goalIs ty2 m = do
  tm1 ::: ty1 <- m
  let tm2 = meta (ty1 === ty2)
  pure (tm1 === tm2)

meta
  :: Term (Problem :+: Core) (Var (Fin n) a)
  -> Term (Problem :+: Core) (Var (Fin n) a)
meta ty = existsFin ty (pure (B FZ))


elab
  :: ( Carrier sig m
     , Member (Error Notice) sig
     , Member (Reader Globals) sig
     , Member (Reader Excerpt) sig
     )
  => Vec n (Term (Problem :+: Core) (Var (Fin n) Qualified))
  -> Term Surface.Surface (Var (Fin n) Qualified)
  -> m (Term (Problem :+: Core) (Var (Fin n) Qualified) ::: Term (Problem :+: Core) (Var (Fin n) Qualified))
elab ctx = \case
    Var (B n) -> pure (pure (B n) ::: ctx ! n)
    Var (F n) -> assume n
    Term t -> case t of
      Surface.Lam _ b -> intro (\ t -> elab' (VS t (fmap (first FS) <$> ctx)) (fromScopeFin <$> b))
      f Surface.:$ (_ :< a) -> app (elab' ctx f) (elab' ctx a)
      Surface.Type -> pure (type' ::: type')
> \ t ' - > elab ' ( VS t ' ( fmap ( first FS ) < $ > ctx ) ) ( fromScopeFin < $ > b )
  where elab' ctx m = spanIs (elab ctx <$> m)

elabDecl :: ( Carrier sig m
            , Member (Error Notice) sig
            , Member (Reader Globals) sig
            , Member (Reader ModuleName) sig
            )
         => Decl (Term Surface.Surface Qualified)
         -> m (Decl (Term (Problem :+: Core) Qualified))
elabDecl (Decl name d tm ty) = do
  ty' <- runSpanned (fmap strengthen . goalIs type' . elab VZ . fmap F) ty
  moduleName <- ask
  tm' <- runSpanned (fmap strengthen . local (:> (moduleName :.: name) ::: unSpanned ty') . goalIs (F <$> unSpanned ty') . elab VZ . fmap F) tm
  pure (Decl name d tm' ty')
  where strengthen :: Term (Problem :+: Core) (Var (Fin 'Z) Qualified) -> Term (Problem :+: Core) Qualified
        strengthen = fmap (var absurdFin id)

elabModule :: ( Carrier sig m
              , Member (Error Notice) sig
              , Member (Reader (ModuleGraph (Term (Problem :+: Core)) Void)) sig
              , Member (Writer (Stack Notice)) sig
              )
           => Module (Term Surface.Surface) Qualified
           -> m (Module (Term (Problem :+: Core)) Qualified)
elabModule m = runReader (moduleName m) . local @(ModuleGraph (Term (Problem :+: Core)) Void) (Module.restrict (Map.keysSet (moduleImports m))) $ do
  FIXME : do a topo sort on the decls ? or at least make their types known first ? or … ?
  decls <- foldM go mempty (moduleDecls m)
  pure m { moduleDecls = decls }
  where go decls decl = local (extendGraph decls) . withGlobals $ do
          (extendModule decls <$> elabDecl (instantiate (pure . qualified . (moduleDecls m Map.!)) <$> decl)) `catchError` ((decls <$) . logError)
        extendModule decls decl = Map.insert (declName decl) (bind (Just . unqualified) <$> decl) decls
        extendGraph decls (ModuleGraph g) = ModuleGraph @(Term (Problem :+: Core)) @Void (Map.insert (moduleName m) (bindTEither Left m { moduleDecls = decls }) g)
        qualified = (moduleName m :.:) . declName
        unqualified (_ :.: u) = u

withGlobals
  :: (Carrier sig m, Member (Reader (ModuleGraph (Term (Problem :+: Core)) Void)) sig)
  => ReaderC Globals m a
  -> m a
withGlobals m = do
  ctx <- asks @(ModuleGraph (Term (Problem :+: Core)) Void) toContext
  runReader @Globals ctx m
  where toContext g = foldl' definitions Nil (modules g)
        definitions ctx m = foldl' define ctx (moduleDecls m)
          where define ctx d = ctx :> (moduleName m :.: declName d) ::: inst (declType d)
                inst t = instantiateEither (pure . either (moduleName m :.:) id) (unSpanned t)

logError :: (Member (Writer (Stack Notice)) sig, Carrier sig m) => Notice -> m ()
logError = tell . (Nil :>)


type Globals = Stack (Qualified ::: Term (Problem :+: Core) Qualified)


identity, identityT, constant, constantT, constantTQ :: Term (Problem :+: Core) String

identity = lam "A" (lam "a" (pure "a"))
identityT = pi ("A" ::: type') (pi ("_" ::: pure "A") (pure "A"))
constant = lam "A" (lam "B" (lam "a" (lam "b" (pure "a"))))
constantT = pi ("A" ::: type') (pi ("B" ::: type') (pi ("_" ::: pure "A") (pi ("_" ::: pure "B") (pure "A"))))

constantTQ
  = exists ("_A" ::: type') (pi ("A" ::: pure "_A")
  ( exists ("_B" ::: type') (pi ("B" ::: pure "_B")
  ( pi ("_" ::: pure "A") (pi ("_" ::: pure "B") (pure "A"))))))
