formal language derivations

Logic/Language/Derivation.hs

@@ -0,0 +1,93 @@
+module Logic.Language.Derivation where
+
+import Logic.Language (Language(..))
+
+data Derivation 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
+    (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