{-# LANGUAGE TypeOperators #-}
module Zsyntax
( module Zsyntax.Formula
, search
, searchLabelled
, toLabelledGoal
, O.SearchRes
, O.Extraction(..)
, O.FailureReason(..)
, DecoratedLSequent
, Label
, O.extractResults
) where
import qualified Otter as O
import Zsyntax.Formula
import Zsyntax.Labelled.Rule.Interface
import Zsyntax.Labelled.Rule
import Zsyntax.Labelled.DerivationTerm
import Data.Foldable
import Control.Monad.State
import Data.Maybe (mapMaybe)
type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l
type Label = Int
toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label
toLabelledGoal s = evalState (neutralize s) 0
search :: Ord a
=> Sequent a
-> ( O.SearchRes (DecoratedLSequent a Label)
, [DecoratedLSequent a Label])
search = searchLabelled . toLabelledGoal
searchLabelled :: Ord a
=> GoalNSequent a Label
-> ( O.SearchRes (DecoratedLSequent a Label)
, [DecoratedLSequent a Label])
searchLabelled goal = O.search (toList seqs) rules isGoal
where
initial = initialRules goal
seqs = mapMaybe maySequent initial
rules = mapMaybe mayProperRule initial
isGoal s' = (toGoalSequent . _payload $ s') `O.subsumes` goal