{-# 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