{-# LANGUAGE OverloadedStrings #-}
-- | Rendering judgments as human-readable reasoning chains.
--
-- The 'Step' type extracts the reasoning chain from a 'Judgment' GADT.
-- The 'Renderer' typeclass allows jurisdiction-specific output formats.
module Deontic.Render
  ( Renderer(..)
  , judgmentSteps
  , someJudgmentSteps
  , Step(..)
  , StepKind(..)
  ) where

import Data.Text (Text)
import Deontic.Core.Types (ArticleRef)
import Deontic.Core.Verdict (Verdict)
import Deontic.Core.Adjudicate (Judgment(..), SomeJudgment(..))

-- | A single step in the reasoning chain
data Step = Step
  { Step -> StepKind
stepKind       :: StepKind
  , Step -> Verdict
stepVerdict    :: Verdict
  , Step -> ArticleRef
stepArticle    :: ArticleRef
  , Step -> Text
stepSourceText :: Text
  } deriving (Step -> Step -> Bool
(Step -> Step -> Bool) -> (Step -> Step -> Bool) -> Eq Step
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Step -> Step -> Bool
== :: Step -> Step -> Bool
$c/= :: Step -> Step -> Bool
/= :: Step -> Step -> Bool
Eq, Int -> Step -> ShowS
[Step] -> ShowS
Step -> String
(Int -> Step -> ShowS)
-> (Step -> String) -> ([Step] -> ShowS) -> Show Step
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Step -> ShowS
showsPrec :: Int -> Step -> ShowS
$cshow :: Step -> String
show :: Step -> String
$cshowList :: [Step] -> ShowS
showList :: [Step] -> ShowS
Show)

-- | What happened at each layer of the reasoning chain.
data StepKind
  = Applied        -- ^ Base rule was applied directly
  | Overridden     -- ^ This layer overrode a lower layer's verdict
  | Delegated      -- ^ This layer delegated to a lower layer (no override)
  | Counterfactual -- ^ This layer applied a counterfactual (§150-style)
  deriving (StepKind -> StepKind -> Bool
(StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool) -> Eq StepKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StepKind -> StepKind -> Bool
== :: StepKind -> StepKind -> Bool
$c/= :: StepKind -> StepKind -> Bool
/= :: StepKind -> StepKind -> Bool
Eq, Int -> StepKind -> ShowS
[StepKind] -> ShowS
StepKind -> String
(Int -> StepKind -> ShowS)
-> (StepKind -> String) -> ([StepKind] -> ShowS) -> Show StepKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StepKind -> ShowS
showsPrec :: Int -> StepKind -> ShowS
$cshow :: StepKind -> String
show :: StepKind -> String
$cshowList :: [StepKind] -> ShowS
showList :: [StepKind] -> ShowS
Show)

-- | Extract the reasoning steps from a Judgment GADT (bottom-up)
judgmentSteps :: Judgment layers -> [Step]
judgmentSteps :: forall (layers :: [*]). Judgment layers -> [Step]
judgmentSteps (JBase Verdict
v ArticleRef
ref Text
txt) =
  [StepKind -> Verdict -> ArticleRef -> Text -> Step
Step StepKind
Applied Verdict
v ArticleRef
ref Text
txt]
judgmentSteps (JOverride Judgment prev
prev Verdict
v ArticleRef
ref Text
txt) =
  Judgment prev -> [Step]
forall (layers :: [*]). Judgment layers -> [Step]
judgmentSteps Judgment prev
prev [Step] -> [Step] -> [Step]
forall a. [a] -> [a] -> [a]
++ [StepKind -> Verdict -> ArticleRef -> Text -> Step
Step StepKind
Overridden Verdict
v ArticleRef
ref Text
txt]
judgmentSteps (JDelegate Judgment prev
prev) =
  Judgment prev -> [Step]
forall (layers :: [*]). Judgment layers -> [Step]
judgmentSteps Judgment prev
prev
judgmentSteps (JCounterfactual Judgment prev
prev SomeJudgment
_hyp Verdict
v ArticleRef
ref Text
txt) =
  Judgment prev -> [Step]
forall (layers :: [*]). Judgment layers -> [Step]
judgmentSteps Judgment prev
prev [Step] -> [Step] -> [Step]
forall a. [a] -> [a] -> [a]
++ [StepKind -> Verdict -> ArticleRef -> Text -> Step
Step StepKind
Counterfactual Verdict
v ArticleRef
ref Text
txt]

-- | Extract steps from an existentially-wrapped judgment
someJudgmentSteps :: SomeJudgment -> [Step]
someJudgmentSteps :: SomeJudgment -> [Step]
someJudgmentSteps (SomeJudgment Judgment layers
j) = Judgment layers -> [Step]
forall (layers :: [*]). Judgment layers -> [Step]
judgmentSteps Judgment layers
j

-- | Renderer typeclass — jurisdiction-specific output
class Renderer r where
  renderJudgment :: r -> Judgment layers -> Text