module Theorem
( State, Tactic, mkGoal, isGoal, goal, subgoals, by, unify, basic,
conjL, conjR, disjL, disjR, impL, impR, negL, negR,
allL, allR, exL, exR) where
import Goal
import Formula
import Term
import Subst
data State r f v = State { goal :: (Formula r f v), subgoals :: [Goal r f v] }
mkGoal :: Formula r f v -> State r f v
mkGoal gf = clear (State gf [ [] :- [gf] ]) -- Note: Clear resets name supply
isGoal :: State r f v -> Bool
isGoal State { subgoals = [] } = True
isGoal _ = False
type Tactic r f v = State r f v -> [State r f v]
by :: Tactic r f v -> State r f v -> State r f v
by t s = head (t s ++ [s] )
unify :: (Eq r, Eq f, Eq v) => Tactic r f v
unify State {goal = g ,subgoals = sg} =
do { (h, sg', t) <- matches [] sg
; s <- unify' sg'
; return State {goal = g , subgoals = map (onAll (subst s)) (h ++ t)}
}
tactic :: (Goal r f v -> [(Formula r f v, Goal r f v)]) -> Primitive r f v -> Tactic r f v
tactic split prim State {goal = g, subgoals = sg} =
do { (h, sg', t) <- matches [] sg
; (f, gl) <- split sg'
; gs <- prim f gl
; return State {goal = g, subgoals = h ++ gs ++ t}
}
basic :: (Eq r, Eq f, Eq v) => Tactic r f v
basic = tactic splitL basic'
conjL = tactic splitL conjL'
conjR = tactic splitR conjR'
disjL = tactic splitL disjL'
disjR = tactic splitR disjR'
impL = tactic splitL impL'
impR = tactic splitR impR'
negL = tactic splitL negL'
negR = tactic splitR negR'
allL = tactic splitL allL'
allR :: Eq v => Tactic r String v
allR = tactic splitR allR'
exL :: Eq v => Tactic r String v
exL = tactic splitL exL'
exR = tactic splitR exR'
splitL :: Goal r f v -> [(Formula r f v, Goal r f v)]
splitL (g :- d) = [(f, (g' :- d)) | (f, g') <- split g]
splitR :: Goal r f v -> [(Formula r f v, Goal r f v)]
splitR (g :- d) = [(f, (g :- d')) | (f, d') <- split d]
split :: [a] -> [(a,[a])]
split as = [ (a, h++t) | (h, a, t) <- matches [] as ]
matches :: [a] -> [a] -> [([a], a, [a])]
matches as [] = []
matches as (x:xs) = (as, x, xs): matches (as++[x]) xs
onAll f (g :- d) = map f g :- map f d