-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_HADDOCK not-home #-}

-- | A more ergonomic way of matching on classified instructions.
module Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr
  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr
  ) where

import Data.Singletons (Sing, SingI(..))

import Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types
import Morley.Michelson.Typed.Instr (Instr)

class WithClassifiedInstr instr where
  type WCIConstraint instr (cls' :: InstrClass) :: Constraint
  {- | Perform a computation with a classified instruction.

  Intended to be used with @LambdaCase@, e.g.

  @
  isRealInstr :: T.Instr a b -> Bool
  isRealInstr = withClassifiedInstr \\case
    'SFromMichelson' -> True
    'SStructural' -> False
    'SAdditional' -> \\case
      'C_Nop' -> False
      'C_Ext'{} -> True
    'SPhantom' -> False
  @

  You can use 'withClassifiedInstr' again to obtain a different classification:

  @
  go = 'withClassifiedInstr' \\case
    'SFailingNormal' -> 'withClassifiedInstr' \\case
      'SNoChildren' -> _
  @

  If you need to reference the original instruction, consider using '&' for
  convenient pointful syntax:

  @
  go i = i & 'withClassifiedInstr' \\case
    'SFailingNormal' -> 'withClassifiedInstr' \\case
      'SNoChildren' -> doStuffWith i
  @
  -}
  withClassifiedInstr
    :: forall t inp out r. ClassifyInstr t
    => (forall cls. (SingI cls, WCIConstraint instr cls)
        => Sing (GetClassified cls :: t)
        -> ClassifiedInstr cls inp out
        -> r)
    -> instr inp out
    -> r

instance WithClassifiedInstr Instr where
  type WCIConstraint Instr _ = ()
  withClassifiedInstr :: forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
 (SingI cls, WCIConstraint Instr cls) =>
 Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> Instr inp out -> r
withClassifiedInstr forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f Instr inp out
instr = case Instr inp out -> WellClassifiedInstr inp out
forall (inp :: [T]) (out :: [T]).
Instr inp out -> WellClassifiedInstr inp out
classifyInstr Instr inp out
instr of
    WCI ClassifiedInstr cls inp out
cinstr -> Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
forall (cls :: InstrClass).
(SingI cls, WCIConstraint Instr cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f (ClassifiedInstr cls inp out -> Sing (GetClassified cls)
forall t (c :: InstrClass) (inp :: [T]) (out :: [T]).
(SingI c, ClassifyInstr t) =>
ClassifiedInstr c inp out -> Sing (GetClassified c)
getInstrClass ClassifiedInstr cls inp out
cinstr) ClassifiedInstr cls inp out
cinstr

instance SingI cls => WithClassifiedInstr (ClassifiedInstr cls) where
  type WCIConstraint (ClassifiedInstr cls) cls' = cls ~ cls'
  withClassifiedInstr :: forall t (inp :: [T]) (out :: [T]) r.
ClassifyInstr t =>
(forall (cls :: InstrClass).
 (SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
 Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r)
-> ClassifiedInstr cls inp out -> r
withClassifiedInstr forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f ClassifiedInstr cls inp out
cinstr = Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
forall (cls :: InstrClass).
(SingI cls, WCIConstraint (ClassifiedInstr cls) cls) =>
Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r
f (ClassifiedInstr cls inp out -> Sing (GetClassified cls)
forall t (c :: InstrClass) (inp :: [T]) (out :: [T]).
(SingI c, ClassifyInstr t) =>
ClassifiedInstr c inp out -> Sing (GetClassified c)
getInstrClass ClassifiedInstr cls inp out
cinstr) ClassifiedInstr cls inp out
cinstr