{-|
Copyright        : (c) Galois, Inc. 2025
Maintainer       : Langston Barrett <langston@galois.com>
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneKindSignatures #-}

module Lang.Crucible.Debug.Arg.Type
  ( type ArgType(..)
  , type Breakpoint
  , type Command
  , type Exactly
  , type Function
  , type Int
  , type Path
  , type Text
  , ArgTypeRepr(..)
  ) where

import Data.Kind (Type)
import Data.Parameterized.Classes (KnownRepr(knownRepr), ShowF (showF))
import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol, symbolRepr)
import Data.Type.Equality (TestEquality(testEquality), type (:~:)(Refl))
import GHC.TypeLits (KnownSymbol, Symbol)
import Lang.Crucible.Debug.Regex qualified as Rgx
import Prelude hiding (Int)
import Prettyprinter qualified as PP

-- | Type-level only
data ArgType
  = TBreakpoint
  | TCommand
  | TExactly Symbol
  | TFunction
  | TInt
  | TPath
  | TText

type Breakpoint = Rgx.Lit 'TBreakpoint
type Command = Rgx.Lit 'TCommand
type Exactly s = Rgx.Lit ('TExactly s)
type Function = Rgx.Lit 'TFunction
type Int = Rgx.Lit 'TInt
type Path = Rgx.Lit 'TPath
type Text = Rgx.Lit 'TText

-- | Value-level representative of 'ArgType'
type ArgTypeRepr :: ArgType -> Type
data ArgTypeRepr i where
  TBreakpointRepr :: ArgTypeRepr 'TBreakpoint
  TCommandRepr :: ArgTypeRepr 'TCommand
  TExactlyRepr :: SymbolRepr s -> ArgTypeRepr ('TExactly s)
  TFunctionRepr :: ArgTypeRepr 'TFunction
  TIntRepr :: ArgTypeRepr 'TInt
  TPathRepr :: ArgTypeRepr 'TPath
  TTextRepr :: ArgTypeRepr 'TText

instance Show (ArgTypeRepr t) where
  show :: ArgTypeRepr t -> String
show =
    \case
      ArgTypeRepr t
TBreakpointRepr -> String
"TBreakpointRepr"
      ArgTypeRepr t
TCommandRepr -> String
"TCommandRepr"
      TExactlyRepr SymbolRepr s
s -> String
"TExactlyRepr(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SymbolRepr s -> String
forall a. Show a => a -> String
show SymbolRepr s
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      ArgTypeRepr t
TFunctionRepr -> String
"TFunctionRepr"
      ArgTypeRepr t
TIntRepr -> String
"TIntRepr"
      ArgTypeRepr t
TPathRepr -> String
"TPathRepr"
      ArgTypeRepr t
TTextRepr -> String
"TTextRepr"

instance ShowF ArgTypeRepr where
  showF :: forall (t :: ArgType). ArgTypeRepr t -> String
showF = ArgTypeRepr tp -> String
forall a. Show a => a -> String
show

instance TestEquality ArgTypeRepr where
  testEquality :: forall (a :: ArgType) (b :: ArgType).
ArgTypeRepr a -> ArgTypeRepr b -> Maybe (a :~: b)
testEquality ArgTypeRepr a
r ArgTypeRepr b
r' =
    case (ArgTypeRepr a
r, ArgTypeRepr b
r') of
      (ArgTypeRepr a
TBreakpointRepr, ArgTypeRepr b
TBreakpointRepr) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      (ArgTypeRepr a
TBreakpointRepr, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (ArgTypeRepr a
TCommandRepr, ArgTypeRepr b
TCommandRepr) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      (ArgTypeRepr a
TCommandRepr, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (TExactlyRepr SymbolRepr s
s, TExactlyRepr SymbolRepr s
s') ->
        case SymbolRepr s -> SymbolRepr s -> Maybe (s :~: s)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b)
testEquality SymbolRepr s
s SymbolRepr s
s' of
          Just s :~: s
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
          Maybe (s :~: s)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (TExactlyRepr {}, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (ArgTypeRepr a
TFunctionRepr, ArgTypeRepr b
TFunctionRepr) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      (TFunctionRepr {}, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (ArgTypeRepr a
TIntRepr, ArgTypeRepr b
TIntRepr) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      (ArgTypeRepr a
TIntRepr, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (ArgTypeRepr a
TPathRepr, ArgTypeRepr b
TPathRepr) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      (ArgTypeRepr a
TPathRepr, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing
      (ArgTypeRepr a
TTextRepr, ArgTypeRepr b
TTextRepr) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      (ArgTypeRepr a
TTextRepr, ArgTypeRepr b
_) -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance KnownRepr ArgTypeRepr 'TBreakpoint where
  knownRepr :: ArgTypeRepr 'TBreakpoint
knownRepr = ArgTypeRepr 'TBreakpoint
TBreakpointRepr

instance KnownRepr ArgTypeRepr 'TCommand where
  knownRepr :: ArgTypeRepr 'TCommand
knownRepr = ArgTypeRepr 'TCommand
TCommandRepr

instance KnownSymbol s => KnownRepr ArgTypeRepr ('TExactly s) where
  knownRepr :: ArgTypeRepr ('TExactly s)
knownRepr = SymbolRepr s -> ArgTypeRepr ('TExactly s)
forall (s :: Symbol). SymbolRepr s -> ArgTypeRepr ('TExactly s)
TExactlyRepr SymbolRepr s
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol

instance KnownRepr ArgTypeRepr 'TFunction where
  knownRepr :: ArgTypeRepr 'TFunction
knownRepr = ArgTypeRepr 'TFunction
TFunctionRepr

instance KnownRepr ArgTypeRepr 'TInt where
  knownRepr :: ArgTypeRepr 'TInt
knownRepr = ArgTypeRepr 'TInt
TIntRepr

instance KnownRepr ArgTypeRepr 'TPath where
  knownRepr :: ArgTypeRepr 'TPath
knownRepr = ArgTypeRepr 'TPath
TPathRepr

instance KnownRepr ArgTypeRepr 'TText where
  knownRepr :: ArgTypeRepr 'TText
knownRepr = ArgTypeRepr 'TText
TTextRepr

instance PP.Pretty (ArgTypeRepr t) where
  pretty :: forall ann. ArgTypeRepr t -> Doc ann
pretty =
    \case
      ArgTypeRepr t
TBreakpointRepr -> Doc ann
"BREAKPOINT"
      ArgTypeRepr t
TCommandRepr -> Doc ann
"COMMAND"
      TExactlyRepr SymbolRepr s
s -> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (SymbolRepr s -> Text
forall (nm :: Symbol). SymbolRepr nm -> Text
symbolRepr SymbolRepr s
s)
      ArgTypeRepr t
TFunctionRepr -> Doc ann
"FUNCTION"
      ArgTypeRepr t
TIntRepr -> Doc ann
"INT"
      ArgTypeRepr t
TPathRepr -> Doc ann
"PATH"
      ArgTypeRepr t
TTextRepr -> Doc ann
"TEXT"