content: {-# LANGUAGE TypeApplications #-}
  
  module Lamdu.Sugar.Convert.NodeActions.Extract
      ( makeExtract
      ) where
  
  import qualified Control.Lens.Extended as Lens
  import qualified Data.Property as Property
  import           Hyper
  import qualified Hyper.Syntax.Scheme as S
  import           Hyper.Type.Prune (Prune(..))
  import           Hyper.Unify (UVar)
  import           Hyper.Unify.Generalize (generalize)
  import qualified Lamdu.Cache as Cache
  import           Lamdu.Calc.Definition (depsGlobalTypes)
  import           Lamdu.Calc.Infer (runPureInfer)
  import qualified Lamdu.Calc.Term as V
  import qualified Lamdu.Calc.Type as T
  import qualified Lamdu.Data.Anchors as Anchors
  import qualified Lamdu.Data.Definition as Definition
  import qualified Lamdu.Data.Ops as DataOps
  import qualified Lamdu.Expr.IRef as ExprIRef
  import qualified Lamdu.Sugar.Convert.Input as Input
  import           Lamdu.Sugar.Convert.Monad (ConvertM(..))
  import qualified Lamdu.Sugar.Convert.Monad as ConvertM
  import qualified Lamdu.Sugar.Convert.PostProcess as PostProcess
  import qualified Lamdu.Sugar.Internal.EntityId as EntityId
  import           Lamdu.Sugar.Types
  import           Revision.Deltum.Transaction (Transaction)
  
  import           Lamdu.Prelude
  
  type T = Transaction
  
  makeExtract ::
      Monad m =>
      Input.Payload m # V.Term -> ConvertM m (T m ExtractDestination)
  makeExtract exprPl =
      Lens.view (ConvertM.scScopeInfo . ConvertM.siExtractPos) >>=
      \case
      Nothing -> mkExtractToDef exprPl <&> Lens.mapped %~ ExtractToDef
      Just outerScope ->
          mkExtractToLet (outerScope ^. ConvertM.osiPos) (exprPl ^. Input.stored)
          <&> ExtractToLet & pure
  
  mkExtractToDef :: Monad m => Input.Payload m # V.Term -> ConvertM m (T m EntityId)
  mkExtractToDef exprPl =
      (,,)
      <$> Lens.view id
      <*> ConvertM.postProcessAssert
      <*> ConvertM.cachedFunc Cache.infer
      <&>
      \(ctx, postProcess, infer) ->
      do
          let scheme =
                  generalize (exprPl ^. Input.inferredTypeUVar)
                  >>= S.saveScheme
                  & runPureInfer @(V.Scope # UVar) V.emptyScope (ctx ^. ConvertM.scInferContext)
                  & Lens._Left %~ (\x -> x :: T.TypeError # UVar)
                  & (^?! Lens._Right . _1)
          let deps = ctx ^. ConvertM.scFrozenDeps . Property.pVal
          newDefI <-
              Definition.Definition
              (Definition.BodyExpr (Definition.Expr valI deps)) scheme ()
              & DataOps.newPublicDefinitionWithPane (ctx ^. Anchors.codeAnchors)
          PostProcess.def infer (ctx ^. ConvertM.scDebugMonitors) newDefI
              >>=
              \case
              PostProcess.GoodExpr -> pure ()
              _ -> error "Bug!"
          let param = ExprIRef.globalId newDefI
          getVarI <- V.LVar param & V.BLeaf & ExprIRef.newValI
          (exprPl ^. Input.stored . ExprIRef.setIref) getVarI
          depsGlobalTypes . Lens.at param ?~ scheme
              & Property.pureModify (ctx ^. ConvertM.scFrozenDeps)
          postProcess
          EntityId.ofIRef newDefI & pure
      where
          valI = exprPl ^. Input.stored . ExprIRef.iref
  
  mkExtractToLet ::
      Monad m =>
      ExprIRef.HRef m # V.Term -> ExprIRef.HRef m # V.Term -> T m EntityId
  mkExtractToLet outerScope stored =
      do
          (param, lamI) <-
              if stored ^. ExprIRef.iref == extractPosI
              then
                  -- Give entire binder body a name (replace binder body
                  -- with "(\x -> x) stored")
                  DataOps.newIdentityLambda
              else
                  -- Give some subexpr in binder body a name (replace
                  -- binder body with "(\x -> assignmentBody) stored", and
                  -- stored becomes "x")
                  do
                      newParam <- ExprIRef.newVar
                      paramType <- _HCompose # Pruned & ExprIRef.newValI
                      lamI <-
                          V.TypedLam newParam paramType extractPosI & V.BLam
                          & ExprIRef.newValI
                      getVarI <- V.LVar newParam & V.BLeaf & ExprIRef.newValI
                      (stored ^. ExprIRef.setIref) getVarI
                      pure (newParam, lamI)
          V.App lamI oldStored & V.BApp & ExprIRef.newValI
              >>= outerScope ^. ExprIRef.setIref
          EntityId.ofTaggedEntity param Anchors.anonTag & pure
      where
          extractPosI = outerScope ^. ExprIRef.iref
          oldStored = stored ^. ExprIRef.iref
  