module Deontic.Civil.Cancellation () where

import Deontic.Core.Types
import Deontic.Core.Verdict
import Deontic.Core.Adjudicate
import Deontic.Core.Layer (Base, Resolvable)
import Deontic.Civil.Types

type instance Resolvable CancellableAct = '[ConstructiveRatification, GeneralRatification, Base]

-- Base: 취소 또는 현상 유지
instance Adjudicate CancellableAct '[Base] where
  adjudicate :: CancellableAct -> Facts CancellableAct -> Judgment '[Base]
adjudicate CancellableAct
act Facts CancellableAct
facts
    | CancellableAct -> Verdict
caPriorVerdict CancellableAct
act Verdict -> Verdict -> Bool
forall a. Eq a => a -> a -> Bool
/= Verdict
Voidable =
        Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase (CancellableAct -> Verdict
caPriorVerdict CancellableAct
act)
          (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
141 Maybe Int
forall a. Maybe a
Nothing)
          Text
"취소할 수 있는 법률행위가 아니므로 취소의 대상이 되지 아니한다."
    | CancellationFacts -> Bool
cnfCancelled Facts CancellableAct
CancellationFacts
facts =
        Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Void
          (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
141 Maybe Int
forall a. Maybe a
Nothing)
          Text
"취소된 법률행위는 처음부터 무효인 것으로 본다."
    | Bool
otherwise =
        Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Voidable
          (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
141 Maybe Int
forall a. Maybe a
Nothing)
          Text
"취소할 수 있는 법률행위로서 취소권이 행사되지 아니하였다."

-- §143-§144: 추인
instance Adjudicate CancellableAct rest
      => Adjudicate CancellableAct (GeneralRatification ': rest) where
  adjudicate :: CancellableAct
-> Facts CancellableAct -> Judgment (GeneralRatification : rest)
adjudicate CancellableAct
act Facts CancellableAct
facts
    | CancellationFacts -> Bool
cnfRatified Facts CancellableAct
CancellationFacts
facts
    , CancellationFacts -> Bool
cnfCauseCeased Facts CancellableAct
CancellationFacts
facts Bool -> Bool -> Bool
|| CancellationFacts -> Bool
cnfRatifierIsGuardian Facts CancellableAct
CancellationFacts
facts
    , let prev :: Judgment rest
prev = forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest CancellableAct
act Facts CancellableAct
facts
    , Judgment rest -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment rest
prev Verdict -> Verdict -> Bool
forall a. Eq a => a -> a -> Bool
/= Verdict
Valid =
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (GeneralRatification : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride Judgment rest
prev
                  Verdict
Valid
                  (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
143 Maybe Int
forall a. Maybe a
Nothing)
                  Text
"취소할 수 있는 법률행위를 추인한 후에는 취소하지 못한다."
    | Bool
otherwise =
        Judgment rest -> Judgment (GeneralRatification : rest)
forall (prev :: [*]) l. Judgment prev -> Judgment (l : prev)
JDelegate (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest CancellableAct
act Facts CancellableAct
facts)

-- §145: 법정추인
instance Adjudicate CancellableAct rest
      => Adjudicate CancellableAct (ConstructiveRatification ': rest) where
  adjudicate :: CancellableAct
-> Facts CancellableAct
-> Judgment (ConstructiveRatification : rest)
adjudicate CancellableAct
act Facts CancellableAct
facts
    | Just ConstructiveRatificationEvent
_ <- CancellationFacts -> Maybe ConstructiveRatificationEvent
cnfConstructive Facts CancellableAct
CancellationFacts
facts
    , Bool -> Bool
not (CancellationFacts -> Bool
cnfObjectionReserved Facts CancellableAct
CancellationFacts
facts)
    , let prev :: Judgment rest
prev = forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest CancellableAct
act Facts CancellableAct
facts
    , Judgment rest -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment rest
prev Verdict -> Verdict -> Bool
forall a. Eq a => a -> a -> Bool
/= Verdict
Valid =
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (ConstructiveRatification : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride Judgment rest
prev
                  Verdict
Valid
                  (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
145 Maybe Int
forall a. Maybe a
Nothing)
                  Text
"추인할 수 있는 후에 법정추인 사유가 있으므로 추인한 것으로 본다."
    | Bool
otherwise =
        Judgment rest -> Judgment (ConstructiveRatification : rest)
forall (prev :: [*]) l. Judgment prev -> Judgment (l : prev)
JDelegate (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest CancellableAct
act Facts CancellableAct
facts)