language derivations: add hypotheses, L example

Logic/Language/Derivation.hs

@@ -3,7 +3,8 @@ module Logic.Language.Derivation where
 import Logic.Language (Language(..))
 
 data Derivation symbol
-  = Axiom0 Integer
+  = Hypothesis [symbol]
+  | Axiom0 Integer
   | Axiom1 Integer [symbol]
   | Axiom2 Integer [symbol] [symbol]
   | Axiom3 Integer [symbol] [symbol] [symbol]
@@ -44,6 +45,9 @@ data DerivationResultIndexErrorPlace
 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

Logic/Language/Impl/L.hs

@@ -1,6 +1,7 @@
 module Logic.Language.Impl.L where
 
 import Logic.Language (Language(..))
+import Logic.Language.Derivation (Derivation(..))
 import Logic.Statement (Statement(..))
 import Logic.Parse
   ( Parser(..)
@@ -141,3 +142,12 @@ serializeL (Implies s1 s2) = do
   l1 <- serializeL s1
   l2 <- serializeL s2
   return $ [Open] ++ l1 ++ [Arrow] ++ l2 ++ [Close]
+
+deriveLExample1 :: Derivation AlphaL
+deriveLExample1 = step5
+  where
+    step1 = Hypothesis [Open, Variable 1, Arrow, Variable 2, Close]
+    step2 = Axiom2 0 [Open, Variable 1, Arrow, Variable 2, Close] [Variable 0]
+    step3 = Infer2 0 0 step2 step1
+    step4 = Axiom3 0 [Variable 0] [Variable 1] [Variable 2]
+    step5 = Infer2 0 0 step4 step3