module Interaction where
import PrelSequent
import Sequent
import PrSequent
-- operations for interactive theorem proving. AR 8/4/1999 -- 13/4
refine :: (AbsCalculus,Proof) -> [Int] -> (Int,Int) -> Ident -> (Proof,String)
refine (calculus,tree) ints (i,j) ident =
case lookup ints [z | Left z <- goalsOfProof tree] of
Just (ant,suc) ->
case refineLocal calculus ident goal of
Ok obs -> (replace tree ints (Proof ident goal (map (newGoal obs) obs)),"")
Bad s -> (tree,s)
where
goal = (activate i ant, activate j suc)
newParams obls = [(p, Meta (refreshP p)) | Right p <- obls]
newGoal obls g = case g of
(Left sequent) -> Goal (refreshS obls sequent)
(Right param) -> Param (refreshP param)
refreshS obls (an,su) = (map sp an, map sp su)
where ---
sp = substFormula [] makeParams (newParams obls)
refreshP p = refreshIdent (paramsOfProof tree) p
activate int [] = []
activate int cont = let n=int-1 in
if length cont < n then cont
else cont!!n : take n cont ++ drop (n+1) cont
_ -> (tree, "no such goal")
instantiate :: AbsCalculus -> Ident -> Term -> Proof -> Proof
instantiate calc param term proof =
case proof of
Goal (ant,suc) -> Goal (substIn ant, substIn suc)
Param x -> proof
Proof rule (a,s) proofs -> Proof rule (substIn a, substIn s) (instProofs proofs)
where
substIn = map (substFormula symbs substTerm [(param,term)])
where symbs = [] --- freeVariablesOfTerm term
instProofs pp = map (instantiate calc param term) (filter (/=(Param param)) pp)
remove :: Proof -> [Int] -> (Proof,String)
remove tree ints =
case lookup ints (map fst (nodesOfProof tree)) of
Just sequent -> (replace tree ints (Goal sequent),"")
_ -> (tree, prGoalId ints +++ "does not exist")
refineLocal :: AbsCalculus -> Ident -> Sequent -> Err Obligations
refineLocal calculus ident sequent =
case lookup ident calculus of
Just rule ->
case rule sequent of
Just obls -> Ok obls
_ -> Bad ("rule" +++ ident +++ "does not apply")
_ -> Bad ("rule" +++ ident +++ "does not exist")
applicableRules :: AbsCalculus -> Sequent -> [((Ident,AbsRule),Obligations)]
applicableRules calc sequent = [ ((i,r),seqs r) | (i,r) <- calc, ok r] where
ok r = case r sequent of
Just _ -> True
_ -> False
seqs r = case r sequent of
Just ss -> ss
_ -> []
allApplicableRules :: AbsCalculus -> Sequent ->
[((Sequent,(Int,Int)),((Ident,AbsRule),Obligations))]
allApplicableRules calc sequent =
[((sq',i),app) | (sq',i) <- ordsOfSequent sequent,
app <- applicableRules calc sq']
replace :: Proof -> [Int] -> Proof -> Proof
replace tree ints tree' =
case (tree,tail ints) of
(_, []) -> tree'
(Proof c s trs, k:n) | k <= length trs ->
Proof c s (t1 ++ [tr'] ++ tail t2)
where (t1,t2) = splitAt (k-1) trs
tr' = replace (head t2) (k:n) tree'
_ -> tree
tryRefine :: (AbsCalculus,Proof) -> [Int] -> Int -> (Proof,String)
tryRefine (calculus,tree) goal limit =
case lookup goal [x | Left x <- goalsOfProof tree] of
Just sequent ->
case tryMethod calculus limit sequent of
proof:_ -> (replace tree goal proof,"")
[] -> (tree, "no proof found")
_ -> (tree, prGoalId goal +++ "does not exist")
tryMethod :: AbsCalculus -> Int -> Sequent -> [Proof]
tryMethod calculus limit sequent =
case limit of
0 -> [Proof i sequent' [] | (sequent',_) <- ordsOfSequent sequent,
((i,r),obls) <- applicableRules calculus sequent',
null [x | Left x <- obls]]
_ -> [Proof i sequent' pp | (sequent',_) <- ordsOfSequent sequent,
((i,r),ss) <- applicableRules calculus sequent',
pp <- tryToEach (limit - 1) ss]
where
tryToEach n ss = combinations (map (tryMethod calculus n) [x | Left x <- ss])