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])