content: {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
  {-# LANGUAGE DerivingStrategies, GeneralisedNewtypeDeriving #-}
  {-|
  Module      : Parsley.Internal.Backend.Machine.Identifiers
  Description : frontend specific identifiers.
  License     : BSD-3-Clause
  Maintainer  : Jamie Willis
  Stability   : experimental
  
  This module defines "identifiers", which are used to uniquely identify different
  nodes in the combinator tree (and abstract machine).
  
  @since 1.0.0.0
  -}
  module Parsley.Internal.Core.Identifiers (
      MVar(..), IMVar,
      ΣVar(..), IΣVar, SomeΣVar(..), getIΣVar
    ) where
  
  import Data.Array        (Ix)
  import Data.Function     (on)
  import Data.GADT.Compare (GEq, GCompare, gcompare, geq, GOrdering(..))
  import Data.Kind         (Type)
  import Data.Typeable     ((:~:)(Refl))
  import Data.Word         (Word64)
  import Unsafe.Coerce     (unsafeCoerce)
  
  {-|
  An identifier representing concrete registers and mutable state.
  
  @since 0.1.0.0
  -}
  newtype ΣVar (a :: Type) = ΣVar IΣVar
  {-|
  An identifier representing let-bound parsers, recursion, and iteration.
  
  @since 0.1.0.0
  -}
  newtype MVar (a :: Type) = MVar IMVar
  
  {-|
  Underlying untyped identifier, which is numeric but otherwise opaque.
  
  @since 0.1.0.0
  -}
  newtype IMVar = IMVar Word64 deriving newtype (Ord, Eq, Num, Enum, Show, Ix)
  
  {-|
  Underlying untyped identifier, which is numeric but otherwise opaque.
  
  @since 0.1.0.0
  -}
  newtype IΣVar = IΣVar Word64 deriving newtype (Ord, Eq, Num, Enum, Show, Ix)
  
  instance Show (MVar a) where show (MVar μ) = "μ" ++ show μ
  instance Show (ΣVar a) where show (ΣVar σ) = "σ" ++ show σ
  
  instance GEq ΣVar where
    geq (ΣVar u) (ΣVar v)
      | u == v    = Just (unsafeCoerce Refl)
      | otherwise = Nothing
  
  instance GCompare ΣVar where
    gcompare σ1@(ΣVar u) σ2@(ΣVar v) = case compare u v of
      LT -> GLT
      EQ -> case geq σ1 σ2 of Just Refl -> GEQ
      GT -> GGT
  
  {-|
  An identifier representing some concrete register, but where the type is existential.
  
  @since 0.1.0.0
  -}
  data SomeΣVar = forall r. SomeΣVar (ΣVar r)
  instance Eq SomeΣVar where (==) = (==) `on` getIΣVar
  instance Ord SomeΣVar where compare = compare `on` getIΣVar
  instance Show SomeΣVar where show (SomeΣVar σ) = show σ
  
  {-|
  Fetch the untyped identifier from under the existential.
  
  @since 0.1.0.0
  -}
  getIΣVar :: SomeΣVar -> IΣVar
  getIΣVar (SomeΣVar (ΣVar σ)) = σ
  
  instance GEq MVar where
    geq (MVar u) (MVar v)
      | u == v    = Just (unsafeCoerce Refl)
      | otherwise = Nothing
  
  instance GCompare MVar where
    gcompare μ1@(MVar u) μ2@(MVar v) = case compare u v of
      LT -> GLT
      EQ -> case geq μ1 μ2 of Just Refl -> GEQ
      GT -> GGT
  