97 lines
3.4 KiB
Haskell
97 lines
3.4 KiB
Haskell
module Logic.Language.Derivation where
|
|
|
|
import Logic.Language (Language(..))
|
|
|
|
data Derivation symbol
|
|
= Hypothesis [symbol]
|
|
| Axiom0 Integer
|
|
| Axiom1 Integer [symbol]
|
|
| Axiom2 Integer [symbol] [symbol]
|
|
| Axiom3 Integer [symbol] [symbol] [symbol]
|
|
| Infer1 Integer Integer (Derivation symbol)
|
|
| Infer2 Integer Integer (Derivation symbol) (Derivation symbol)
|
|
deriving (Eq, Show)
|
|
|
|
data DerivationError s
|
|
= SelectIndexError (DerivationSelectIndexError s)
|
|
| ResultIndexError (DerivationResultIndexError s)
|
|
| NotWellFormed [s]
|
|
deriving Show
|
|
|
|
data DerivationSelectIndexError s = DerivationSelectIndexError
|
|
{ dserrSelectPlace :: DerivationSelectIndexErrorPlace
|
|
, dserrSelectErrorIndex :: Integer
|
|
, dserrSize :: Int
|
|
, dserrWffs :: [[s]]
|
|
} deriving Show
|
|
|
|
data DerivationSelectIndexErrorPlace
|
|
= AxiomSelect
|
|
| InferSelect
|
|
deriving Show
|
|
|
|
data DerivationResultIndexError s = DerivationResultIndexError
|
|
{ drerrPlace :: DerivationResultIndexErrorPlace
|
|
, drerrSelectIndex :: Integer
|
|
, drerrResultIndex :: Integer
|
|
, drerrResult :: [[s]]
|
|
, drerrTheorems :: [[s]]
|
|
} deriving Show
|
|
|
|
data DerivationResultIndexErrorPlace
|
|
= InferResult
|
|
deriving Show
|
|
|
|
resolveDerivation :: Language s => Derivation s -> Either (DerivationError s) [s]
|
|
resolveDerivation derivation =
|
|
case derivation of
|
|
(Hypothesis wff)
|
|
| not $ isWellFormed wff -> Left $ NotWellFormed wff
|
|
| otherwise -> Right wff
|
|
(Axiom0 index) -> trySelect AxiomSelect axiom0 index []
|
|
(Axiom1 index wff1)
|
|
| not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
|
|
| otherwise -> do
|
|
rule <- trySelect AxiomSelect axiom1 index [wff1]
|
|
return $ rule wff1
|
|
(Axiom2 index wff1 wff2)
|
|
| not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
|
|
| not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
|
|
| otherwise -> do
|
|
rule <- trySelect AxiomSelect axiom2 index [wff1, wff2]
|
|
return $ rule wff1 wff2
|
|
(Axiom3 index wff1 wff2 wff3)
|
|
| not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
|
|
| not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
|
|
| not $ isWellFormed wff3 -> Left $ NotWellFormed wff3
|
|
| otherwise -> do
|
|
rule <- trySelect AxiomSelect axiom3 index [wff1, wff2, wff3]
|
|
return $ rule wff1 wff2 wff3
|
|
(Infer1 selectIndex resultIndex deriv1) -> do
|
|
theorem1 <- resolveDerivation deriv1
|
|
rule <- trySelect InferSelect infer1 selectIndex [theorem1]
|
|
let result = rule theorem1
|
|
tryResult InferResult selectIndex resultIndex result [theorem1]
|
|
(Infer2 selectIndex resultIndex deriv1 deriv2) -> do
|
|
theorem1 <- resolveDerivation deriv1
|
|
theorem2 <- resolveDerivation deriv2
|
|
rule <- trySelect InferSelect infer2 selectIndex [theorem1, theorem2]
|
|
let result = rule theorem1 theorem2
|
|
tryResult InferResult selectIndex resultIndex result [theorem1, theorem2]
|
|
where
|
|
trySelect place list index wffs = maybe
|
|
(Left $ SelectIndexError $ DerivationSelectIndexError place index (length list) wffs)
|
|
Right $
|
|
get index list
|
|
|
|
tryResult place selectIndex resultIndex list theorems = maybe
|
|
(Left $ ResultIndexError $ DerivationResultIndexError place selectIndex resultIndex list theorems)
|
|
Right $
|
|
get resultIndex list
|
|
|
|
get :: Integer -> [a] -> Maybe a
|
|
get 0 (x:xs) = Just x
|
|
get index [] = Nothing
|
|
get index (x:xs)
|
|
| index >= 1 = get (index - 1) xs
|
|
| otherwise = Nothing
|