module Deontic.Civil.Invalidity () 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 PartialInvalidityAct = '[Conversion, HypotheticalIntent, Base]

-- §137 본문: 일부 무효이면 전부 무효
instance Adjudicate PartialInvalidityAct '[Base] where
  adjudicate :: PartialInvalidityAct
-> Facts PartialInvalidityAct -> Judgment '[Base]
adjudicate PartialInvalidityAct
_ Facts PartialInvalidityAct
facts
    | PartialInvalidityFacts -> Bool
pifPartVoid Facts PartialInvalidityAct
PartialInvalidityFacts
facts =
        Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Void
          (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
137 Maybe Int
forall a. Maybe a
Nothing)
          Text
"법률행위의 일부분이 무효인 때에는 그 전부를 무효로 한다."
    | Bool
otherwise =
        Verdict -> ArticleRef -> Text -> Judgment '[Base]
forall l. Verdict -> ArticleRef -> Text -> Judgment '[l]
JBase Verdict
Valid
          (Text -> Int -> Maybe Int -> ArticleRef
ArticleRef Text
"민법" Int
137 Maybe Int
forall a. Maybe a
Nothing)
          Text
"법률행위의 일부분이 무효가 아니므로 전부 유효하다."

-- §137 단서 + §139 단서
instance Adjudicate PartialInvalidityAct rest
      => Adjudicate PartialInvalidityAct (HypotheticalIntent ': rest) where
  adjudicate :: PartialInvalidityAct
-> Facts PartialInvalidityAct
-> Judgment (HypotheticalIntent : rest)
adjudicate PartialInvalidityAct
act Facts PartialInvalidityAct
facts
    | PartialInvalidityFacts -> Bool
pifHypotheticalIntent Facts PartialInvalidityAct
PartialInvalidityFacts
facts
    , let prev :: Judgment rest
prev = forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest PartialInvalidityAct
act Facts PartialInvalidityAct
facts
    , Judgment rest -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment rest
prev Verdict -> Verdict -> Bool
forall a. Eq a => a -> a -> Bool
== Verdict
Void =
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (HypotheticalIntent : 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
137 Maybe Int
forall a. Maybe a
Nothing)
                  Text
"그 무효부분이 없더라도 법률행위를 하였을 것이라고 인정되므로 나머지 부분은 유효하다."
    | PartialInvalidityFacts -> Bool
pifRatifiedWithKnowledge Facts PartialInvalidityAct
PartialInvalidityFacts
facts
    , let prev :: Judgment rest
prev = forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest PartialInvalidityAct
act Facts PartialInvalidityAct
facts
    , Judgment rest -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment rest
prev Verdict -> Verdict -> Bool
forall a. Eq a => a -> a -> Bool
== Verdict
Void =
        Judgment rest
-> Verdict
-> ArticleRef
-> Text
-> Judgment (HypotheticalIntent : 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
139 Maybe Int
forall a. Maybe a
Nothing)
                  Text
"당사자가 그 무효임을 알고 추인한 때에는 새로운 법률행위로 본다."
    | Bool
otherwise =
        Judgment rest -> Judgment (HypotheticalIntent : rest)
forall (prev :: [*]) l. Judgment prev -> Judgment (l : prev)
JDelegate (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest PartialInvalidityAct
act Facts PartialInvalidityAct
facts)

-- §138 무효행위의 전환
instance Adjudicate PartialInvalidityAct rest
      => Adjudicate PartialInvalidityAct (Conversion ': rest) where
  adjudicate :: PartialInvalidityAct
-> Facts PartialInvalidityAct -> Judgment (Conversion : rest)
adjudicate PartialInvalidityAct
act Facts PartialInvalidityAct
facts
    | PartialInvalidityFacts -> Bool
pifMeetsOtherReqs Facts PartialInvalidityAct
PartialInvalidityFacts
facts
    , PartialInvalidityFacts -> Bool
pifConversionIntent Facts PartialInvalidityAct
PartialInvalidityFacts
facts
    , let prev :: Judgment rest
prev = forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest PartialInvalidityAct
act Facts PartialInvalidityAct
facts
    , Judgment rest -> Verdict
forall (layers :: [*]). Judgment layers -> Verdict
verdict Judgment rest
prev Verdict -> Verdict -> Bool
forall a. Eq a => a -> a -> Bool
== Verdict
Void =
        Judgment rest
-> Verdict -> ArticleRef -> Text -> Judgment (Conversion : 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
138 Maybe Int
forall a. Maybe a
Nothing)
                  Text
"무효인 법률행위가 다른 법률행위의 요건을 구비하고 당사자가 그 무효를 알았더라면 다른 법률행위를 하는 것을 의욕하였으리라고 인정되므로 다른 법률행위로서 효력을 가진다."
    | Bool
otherwise =
        Judgment rest -> Judgment (Conversion : rest)
forall (prev :: [*]) l. Judgment prev -> Judgment (l : prev)
JDelegate (forall act (layers :: [*]).
Adjudicate act layers =>
act -> Facts act -> Judgment layers
adjudicate @_ @rest PartialInvalidityAct
act Facts PartialInvalidityAct
facts)