module Deontic.Civil.ConditionalAct () 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 ConditionalAct = '[BadFaithCondition, IllegalCondition, Base]

-- §147/§152: 조건/기한의 기본 효과
instance Adjudicate ConditionalAct '[Base] where
  adjudicate :: ConditionalAct -> Facts ConditionalAct -> Judgment '[Base]
adjudicate ConditionalAct
_ Facts ConditionalAct
facts = case (ConditionalFacts -> ConditionType
condType Facts ConditionalAct
ConditionalFacts
facts, ConditionalFacts -> ConditionState
condState Facts ConditionalAct
ConditionalFacts
facts) of
    (ConditionType
Suspensive, ConditionState
CondPending)   -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Pending (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
147 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
      Text
"정지조건이 성취되지 아니하여 효력이 발생하지 아니한다."
    (ConditionType
Suspensive, ConditionState
CondFulfilled) -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Valid (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
147 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
      Text
"정지조건이 성취하여 효력이 생긴다."
    (ConditionType
Resolutive, ConditionState
CondPending)   -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Valid (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
147 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2))
      Text
"해제조건이 성취되지 아니하여 효력이 존속한다."
    (ConditionType
Resolutive, ConditionState
CondFulfilled) -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Void (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
147 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2))
      Text
"해제조건이 성취하여 효력을 잃는다."
    (ConditionType
StartDate,  ConditionState
CondPending)   -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Pending (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
152 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
      Text
"시기가 도래하지 아니하여 효력이 발생하지 아니한다."
    (ConditionType
StartDate,  ConditionState
CondFulfilled) -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Valid (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
152 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
      Text
"시기가 도래하여 효력이 생긴다."
    (ConditionType
EndDate,    ConditionState
CondPending)   -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Valid (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
152 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2))
      Text
"종기가 도래하지 아니하여 효력이 존속한다."
    (ConditionType
EndDate,    ConditionState
CondFulfilled) -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Void (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
152 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2))
      Text
"종기가 도래하여 효력을 잃는다."
    -- impossible/illegal handled by upper layers; Base falls back to Pending
    (ConditionType
_, ConditionState
CondImpossible) -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Pending (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
147 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
      Text
"조건의 성취가 불가능하다."
    (ConditionType
_, ConditionState
CondIllegal)    -> Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Pending (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
147 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
      Text
"불법조건이다."

-- §151: 불법조건, 기성조건, 불능조건
instance Adjudicate ConditionalAct rest
      => Adjudicate ConditionalAct (IllegalCondition ': rest) where
  adjudicate :: ConditionalAct
-> Facts ConditionalAct -> Judgment (IllegalCondition : rest)
adjudicate ConditionalAct
act Facts ConditionalAct
facts = case ConditionalFacts -> ConditionState
condState Facts ConditionalAct
ConditionalFacts
facts of
    ConditionState
CondIllegal ->
      Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (IllegalCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                Verdict
Void
                (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
151 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
                Text
"조건이 선량한 풍속 기타 사회질서에 위반한 것인 때에는 그 법률행위는 무효로 한다."
    ConditionState
CondImpossible -> case ConditionalFacts -> ConditionType
condType Facts ConditionalAct
ConditionalFacts
facts of
      ConditionType
Suspensive ->
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (IllegalCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                  Verdict
Void
                  (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
151 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
3))
                  Text
"조건이 성취할 수 없는 것인 경우에 정지조건이면 그 법률행위는 무효로 한다."
      ConditionType
StartDate ->
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (IllegalCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                  Verdict
Void
                  (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
151 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
3))
                  Text
"시기가 도래할 수 없는 것인 경우 그 법률행위는 무효로 한다."
      ConditionType
Resolutive ->
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (IllegalCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                  Verdict
Valid
                  (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
151 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
3))
                  Text
"조건이 성취할 수 없는 것인 경우에 해제조건이면 조건 없는 법률행위로 한다."
      ConditionType
EndDate ->
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (IllegalCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> Verdict -> ArticleRef -> Text -> Judgment (l : prev)
JOverride (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                  Verdict
Valid
                  (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
151 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
3))
                  Text
"종기가 도래할 수 없는 것인 경우 기한 없는 법률행위로 한다."
    ConditionState
_ -> Judgment rest -> Judgment (IllegalCondition : rest)
forall (prev :: [*]) l. Judgment prev -> Judgment (l : prev)
JDelegate (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)

-- §150: 반신의행위
instance Adjudicate ConditionalAct rest
      => Adjudicate ConditionalAct (BadFaithCondition ': rest) where
  adjudicate :: ConditionalAct
-> Facts ConditionalAct -> Judgment (BadFaithCondition : rest)
adjudicate ConditionalAct
act Facts ConditionalAct
facts = case ConditionalFacts -> Maybe BadFaithKind
condBadFaith Facts ConditionalAct
ConditionalFacts
facts of
    Just BadFaithKind
BadFaithPrevention ->
      -- 성취 의제: re-evaluate as if condition fulfilled
      let deemedFacts :: ConditionalFacts
deemedFacts = Facts ConditionalAct
facts { condState = CondFulfilled, condBadFaith = Nothing }
          deemedResult :: Judgment (Resolvable ConditionalAct)
deemedResult = ConditionalAct
-> Facts ConditionalAct -> Judgment (Resolvable ConditionalAct)
forall act.
Adjudicate act (Resolvable act) =>
act -> Facts act -> Judgment (Resolvable act)
query ConditionalAct
act Facts ConditionalAct
ConditionalFacts
deemedFacts
      in Judgment rest
-> SomeJudgment
-> Verdict
-> ArticleRef
-> Text
-> Judgment (BadFaithCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> SomeJudgment
-> Verdict
-> ArticleRef
-> Text
-> Judgment (l : prev)
JCounterfactual (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                         (Judgment '[BadFaithCondition, IllegalCondition, Base]
-> SomeJudgment
forall (layers :: [*]). Judgment layers -> SomeJudgment
SomeJudgment Judgment '[BadFaithCondition, IllegalCondition, Base]
Judgment (Resolvable ConditionalAct)
deemedResult)
                         (Judgment '[BadFaithCondition, IllegalCondition, Base] -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment '[BadFaithCondition, IllegalCondition, Base]
Judgment (Resolvable ConditionalAct)
deemedResult)
                         (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
150 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1))
                         Text
"조건의 성취로 인하여 불이익을 받을 당사자가 신의성실에 반하여 조건의 성취를 방해한 때에는 상대방은 그 조건이 성취한 것으로 주장할 수 있다."
    Just BadFaithKind
BadFaithCausation ->
      -- 불성취 의제: re-evaluate as if condition pending
      let deemedFacts :: ConditionalFacts
deemedFacts = Facts ConditionalAct
facts { condState = CondPending, condBadFaith = Nothing }
          deemedResult :: Judgment (Resolvable ConditionalAct)
deemedResult = ConditionalAct
-> Facts ConditionalAct -> Judgment (Resolvable ConditionalAct)
forall act.
Adjudicate act (Resolvable act) =>
act -> Facts act -> Judgment (Resolvable act)
query ConditionalAct
act Facts ConditionalAct
ConditionalFacts
deemedFacts
      in Judgment rest
-> SomeJudgment
-> Verdict
-> ArticleRef
-> Text
-> Judgment (BadFaithCondition : rest)
forall (prev :: [*]) l.
Judgment prev
-> SomeJudgment
-> Verdict
-> ArticleRef
-> Text
-> Judgment (l : prev)
JCounterfactual (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)
                         (Judgment '[BadFaithCondition, IllegalCondition, Base]
-> SomeJudgment
forall (layers :: [*]). Judgment layers -> SomeJudgment
SomeJudgment Judgment '[BadFaithCondition, IllegalCondition, Base]
Judgment (Resolvable ConditionalAct)
deemedResult)
                         (Judgment '[BadFaithCondition, IllegalCondition, Base] -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment '[BadFaithCondition, IllegalCondition, Base]
Judgment (Resolvable ConditionalAct)
deemedResult)
                         (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
150 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2))
                         Text
"조건의 성취로 인하여 이익을 받을 당사자가 신의성실에 반하여 조건을 성취시킨 때에는 상대방은 그 조건이 성취하지 아니한 것으로 주장할 수 있다."
    Maybe BadFaithKind
Nothing ->
      Judgment rest -> Judgment (BadFaithCondition : rest)
forall (prev :: [*]) l. Judgment prev -> Judgment (l : prev)
JDelegate (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest ConditionalAct
act Facts ConditionalAct
facts)