Changed to using Tactics themselves as hypotheses.

luqui · Jun 11, 2009 · 1b4d766 · 1b4d766
1 parent 6e550dd
commit 1b4d766
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 25 deletions.
diff --git a/ixi/IXi/Proof.hs b/ixi/IXi/Proof.hs
@@ -20,7 +20,7 @@ data Proof
     | XiRule Name Proof Proof
     | HXiRule Name Proof Proof
     | HHRule
-    | XIHRule Int
+    | XIHRule Proof
     | Theorem Theorem
 
 hypothesis = Hypothesis
@@ -56,7 +56,9 @@ checkProof (HXiRule name hproof hxiproof) seq = do
 
 checkProof HHRule seq = S.hhRule seq
 
-checkProof (XIHRule z) seq = S.xihRule z seq
+checkProof (XIHRule pf) seq = do
+    seq' <- S.xihRule seq
+    checkProof pf seq'
 
 checkProof (Theorem (MkTheorem t _)) (hyps S.:|- goal)
     | goal == t = Right ()

diff --git a/ixi/IXi/Sequent.hs b/ixi/IXi/Sequent.hs
@@ -58,7 +58,7 @@ xiRule _ _ = invalid "Goal is not a Xi-form"
 hxiRule :: Name -> Sequent -> Err (Sequent, Sequent)
 hxiRule name (hyps :|- H :% (Xi :% a :% b))
     | nameFree name a || nameFree name b || any (nameFree name) hyps
-        = invalid "Name must no be free in environment"
+        = invalid "Name must not be free in environment"
     | otherwise
         = valid (hyps :|- H :% (a :% n), (a :% n):hyps :|- H :% (b :% n))
     where n = NameVar name
@@ -72,8 +72,8 @@ newName :: Sequent -> Name
 newName seq = safeName' (goal seq : hypotheses seq)
 
 -- conservative extension, Γ,x |- Hx
-xihRule :: Int -> Sequent -> Err ()
+xihRule :: Sequent -> Err Sequent
-xihRule z (hyps :|- goal)
+xihRule (hyps :|- goal) =
-    | not (0 <= z && z <= length hyps) = invalid "Index out of range"
+    case goal of 
-    | not (H :% (hyps !! z) == goal) = invalid "Hypothesis does not match goal"
+        H :% x -> valid (hyps :|- x)
-    | otherwise = valid ()
+        _ -> invalid "Goal is not an H-form"
diff --git a/ixi/IXi/Tactic.hs b/ixi/IXi/Tactic.hs
@@ -1,6 +1,6 @@
 module IXi.Tactic 
-    ( Tactic, Hypothesis
+    ( Tactic
-    , hypothesis, conversion, implRule, xiRule, hxiRule, hhRule, xihRule, theorem
+    , conversion, implRule, xiRule, hxiRule, hhRule, xihRule, theorem
     , inspect, (>|<)
     , newName
     , prove
@@ -15,16 +15,13 @@ import Control.Applicative
 import Control.Monad (ap, MonadPlus(..))
 
 newtype Tactic = Tactic { unTactic :: Seq.Sequent -> Seq.Err P.Proof }
-newtype Hypothesis = Hypothesis Int  -- index from the end
 
-topHyp :: Seq.Sequent -> Hypothesis
+topHyp :: Seq.Sequent -> Tactic
-topHyp seq = Hypothesis (length (Seq.hypotheses seq) - 1)
+topHyp seq = Tactic $ \seq' -> do
-
+    () <- Seq.hypothesis ix seq'
-hypothesis :: Hypothesis -> Tactic
-hypothesis (Hypothesis z) = Tactic $ \seq -> do
-    let ix = length (Seq.hypotheses seq) - z - 1
-    () <- Seq.hypothesis ix seq
     return (P.hypothesis ix)
+    where
+    ix = length (Seq.hypotheses seq) - 1
 
 conversion :: Conversion -> Tactic -> Tactic
 conversion conv rest = Tactic $ \seq -> do
@@ -39,14 +36,14 @@ implRule p pxTac xpqTac = Tactic $ \seq -> do
     xpqPf <- unTactic xpqTac xpqSeq
     return (P.implRule p pxPf xpqPf)
 
-xiRule :: Name -> Tactic -> (Hypothesis -> Tactic) -> Tactic
+xiRule :: Name -> Tactic -> (Tactic -> Tactic) -> Tactic
 xiRule name hTac implTac = Tactic $ \seq -> do
     (hSeq, implSeq) <- Seq.xiRule name seq
     hPf <- unTactic hTac hSeq
     implPf <- unTactic (implTac (topHyp implSeq)) implSeq
     return (P.xiRule name hPf implPf)
 
-hxiRule :: Name -> Tactic -> (Hypothesis -> Tactic) -> Tactic
+hxiRule :: Name -> Tactic -> (Tactic -> Tactic) -> Tactic
 hxiRule name hTac implTac = Tactic $ \seq -> do
     (hSeq, implSeq) <- Seq.hxiRule name seq
     hPf <- unTactic hTac hSeq
@@ -58,11 +55,11 @@ hhRule = Tactic $ \seq -> do
     () <- Seq.hhRule seq
     return P.hhRule
 
-xihRule :: Hypothesis -> Tactic
+xihRule :: Tactic -> Tactic
-xihRule (Hypothesis z) = Tactic $ \seq -> do
+xihRule tac = Tactic $ \seq -> do
-    let ix = length (Seq.hypotheses seq) - z - 1
+    seq' <- Seq.xihRule seq
-    () <- Seq.xihRule ix seq
+    pf <- unTactic tac seq'
-    return (P.xihRule ix)
+    return (P.xihRule pf)
 
 theorem :: P.Theorem -> Tactic
 theorem thm = Tactic $ \seq -> do