content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE QuantifiedConstraints #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# OPTIONS_HADDOCK show-extensions #-}
  
  
  -- |
  -- Module      :  Language.Spectacle.Lang
  -- Copyright   :  (c) Arista Networks, 2022-2023
  -- License     :  Apache License 2.0, see LICENSE
  --
  -- Stability   :  stable
  -- Portability :  non-portable (GHC extensions)
  --
  -- The 'Lang' monad and functions for defining Spectacles syntax as effects.
  --
  -- @since 1.0.0
  module Language.Spectacle.Lang
    ( -- * Lang
      Lang (Pure, Op, Scoped),
      runLang,
      send,
      scope,
      weaken,
  
      -- * Effects
      type EffectK,
      type ScopeK,
      FirstOrder,
      Effect,
  
      -- ** Membership
      type Members,
      Member (inject, project, injectS, projectS),
  
      -- ** Unions
      Op (OHere, OThere),
      Scoped (SHere, SThere),
      decomposeOp,
      extractOp,
      decomposeS,
      extractS,
    )
  where
  
  import Data.Functor.Loom (hoist, (~>~))
  import Language.Spectacle.Lang.Internal (Lang (Op, Pure, Scoped), scope, send)
  import Language.Spectacle.Lang.Member (Member (inject, injectS, project, projectS), type Members)
  import Language.Spectacle.Lang.Op (Op (OHere, OThere), decomposeOp, extractOp)
  import Language.Spectacle.Lang.Scoped
    ( Effect,
      EffectK,
      FirstOrder,
      ScopeK,
      Scoped (SHere, SThere),
      decomposeS,
      extractS,
    )
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  -- | Used to unwrap the pure value in 'Lang' after all of its effects have been discharged.
  --
  -- @since 1.0.0
  runLang :: Lang ctx '[] a -> a
  runLang (Pure x) = x
  runLang _ =
    -- @Lang ctx '[] a@ can only be constructed with 'Pure' or obtained by discharging all its
    -- effects, which would result in 'Pure'. Cases where @Lang ctx '[] a@ holds impure values mean
    -- that:
    --
    -- 1. An effect escaped the scope of 'Lang' and therefore was not discharged when the handler for
    -- that effect was run on 'Lang'. This not impossible but is /very/ difficult to do since the
    -- escaped effect would have to be hidden from 'Loom'. 'Lang' in a first-order operation,
    -- FO effects with resumptions to Lang, or intentionally weakening/coercing a @Lang ctx effs' a@
    -- into some other 'Lang' are all ways which basically guarantee that effects will be left
    -- unhandled.
    --
    -- 2. Operations like 'unsafeCoerce' were used to change the effect signature of 'Lang'.
    error
      "internal error: Lang match against Yield, this means that an effect escaped the scope of Lang \
      \and was left unhandled. This should be impossible."
  
  -- | Appends an effect label @eff@ to the head of a 'Lang's effect signature by the weakening rule
  -- for sum types.
  --
  -- @since 1.0.0
  weaken :: forall eff effs ctx a. Lang ctx effs a -> Lang ctx (eff ': effs) a
  weaken = \case
    Pure x -> pure x
    Op op k -> Op (OThere op) (weaken . k)
    Scoped scoped loom -> Scoped (SThere scoped) (loom ~>~ hoist weaken)
  