{-# LANGUAGE GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses,
    UndecidableInstances, DeriveGeneric, RecordWildCards, TupleSections #-}
module CG.Prover (module X,System(..),solve,findAll,findFirst) where


import CG.Prover.Base as X
import CG.Prover.Ins  as X
import Data.Hashable       (Hashable(..))
import Data.HashSet   as S (insert,member,empty)
import Data.Maybe          (mapMaybe)
import Data.Void           (Void)


-- |Search for proofs of the given goals using the given system, using
--  either breadth-first search (for finite systems) or depth-limited
--  interleaved breadth-first search (for infinite systems).
--  Note: this algorithm performs loop-checking under the assumption
--  that /unary/ rules may cause loops, and rules of other arities
--  make progress.
solve :: (Operator c, Guardable c, Hashable c, Ord c) => System c -> Int -> [Term c Void] -> [(Term c Void, Term String Void)]
solve System{..} depth goals
  | finite    = concatMap (\goal -> map (goal,) (findAll goal rules)) goals
  | otherwise = findFirst depth goals rules


-- |Search for proofs of the given goal using the gives rules using
--  breadth-first search.
--  Note: this algorithm performs loop-checking under the assumption
--  that /unary/ rules may cause loops, and rules of other arities
--  make progress.
findAll :: (Operator c, Guardable c, Hashable c, Ord c) => Term c Void -> [Rule c Int] -> [Term String Void]
findAll goal rules = slv [(S.empty,[goal],head)] []
  where
    slv [                    ] [ ] = []
    slv [                    ] acc = slv (reverse acc) []
    slv ((_   ,  [],prf):prfs) acc = prf [] : slv prfs acc
    slv ((seen,g:gs,prf):prfs) acc
      | S.member g seen = slv prfs acc
      | otherwise       = slv prfs (mapMaybe step rules ++ acc)
      where
        step (Rule n grd a ps c) =
          if runGuard grd g
          then do s <- runIns (ins g c)
                  let prf'  = prf . build n a
                  let seen' | a == 1    = S.insert g seen
                            | otherwise = S.empty
                  ps' <- mapM (subst s) ps
                  return (seen', ps' ++ gs, prf')
          else fail ("Cannot apply rule `"++n++"'")


-- |Search for proofs of the given goal using the gives rules using
--  depth-limited breadth-first search.
--  Note: this algorithm performs loop-checking under the assumption
--  that /unary/ rules may cause loops, and rules of other arities
--  make progress.
findFirst :: (Guardable c, Hashable c, Ord c)
          => Int           -- ^ Search Depth
          -> [Term c Void] -- ^ Goal Terms
          -> [Rule c Int]  -- ^ Inference rules
          -> [(Term c Void, Term String Void)]
findFirst d goals rules = slv (d + 1) (fmap (\g -> (S.empty,g,[g],head)) goals) []
  where
    slv 0                        _   _ = []
    slv _ [                      ] [ ] = []
    slv d [                      ] acc = slv (d - 1) (reverse acc) []
    slv _ ((_   ,o,  [],prf):_   ) _   = [(o, prf [])]
    slv d ((seen,o,g:gs,prf):prfs) acc
      | S.member g seen = slv d prfs acc
      | otherwise       = slv d prfs (mapMaybe step rules ++ acc)
      where
        step (Rule n grd a ps c) =
          if runGuard grd g
          then do s <- runIns (ins g c)
                  let prf'  = prf . build n a
                  let seen' | a == 1    = S.insert g seen
                            | otherwise = S.empty
                  ps' <- mapM (subst s) ps
                  return (seen', o, ps' ++ gs, prf')
          else fail ("Cannot apply rule `"++n++"'")


-- |Build a proof by adding a new constructor.
build :: r -> Int -> [Term r Void] -> [Term r Void]
build n a ts = let (xs,ys) = splitAt a ts in Con n xs : ys