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

-- | Turns a sequent into a labelled sequent that is suitable for proof search,
-- by breaking the linear context formulas into neutral formulas, and
-- labelling all subformulas with unique labels.
toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label
toLabelledGoal s = evalState (neutralize s) 0

-- | Searches for a derivation of the specified sequent.
--
-- @
-- search g == searchLabelled (toLabelledGoal g)
-- @
search :: Ord a
       => Sequent a
       -> ( O.SearchRes (DecoratedLSequent a Label)
          , [DecoratedLSequent a Label])
search = searchLabelled . toLabelledGoal

-- | Searches for a derivation of the specified goal sequent.
-- Returns the search results, as well as all searched sequents.
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