module Clingo.Inspection.Ground ( TermId (..), ElementId (..), AspifStmt (..), registerGroundObserver ) where import Control.Monad.IO.Class import Data.Text (Text, pack) import Foreign import Foreign.C import Numeric.Natural import Clingo.ProgramBuilding import Clingo.Internal.Types import Clingo.Internal.Utils import qualified Clingo.Raw as Raw newtype TermId = TermId { termId :: Raw.Identifier } deriving (Show, Eq, Ord) newtype ElementId = ElementId { elementId :: Raw.Identifier } deriving (Show, Eq, Ord) data AspifStmt s = GRule Bool [Atom s] [Literal s] | GWeightedRule Bool [Atom s] Natural [WeightedLiteral s] | GMinimize Natural [WeightedLiteral s] | GProject [Atom s] | GExternal (Atom s) ExternalType | GAssume [Literal s] | GHeuristic (Atom s) HeuristicType Integer Natural [Literal s] | GAcycEdge Node Node [Literal s] | GTheoryTermNumber TermId Integer | GTheoryTermString TermId Text | GTheoryTermTuple TermId [TermId] | GTheoryTermSet TermId [TermId] | GTheoryTermList TermId [TermId] | GTheoryTermFunction TermId TermId [TermId] | GTheoryElement ElementId [TermId] [Literal s] | GTheoryAtom (Maybe (Atom s)) TermId [ElementId] | GTheoryAtomGuard (Maybe (Atom s)) TermId [ElementId] TermId TermId mkRawGPO :: MonadIO m => (Bool -> IOSym s ()) -> (AspifStmt s -> IOSym s ()) -> m (Raw.GroundProgramObserver ()) mkRawGPO inf k = liftIO $ Raw.GroundProgramObserver <$> Raw.mkGpoInitProgram (\b _ -> reraiseIO (iosym (inf (toBool b)))) <*> pure nullFunPtr <*> pure nullFunPtr <*> Raw.mkGpoRule rul <*> Raw.mkGpoWeightRule wrule <*> Raw.mkGpoMinimize minim <*> Raw.mkGpoProject proj <*> Raw.mkGpoExternal exter <*> Raw.mkGpoAssume assum <*> Raw.mkGpoHeuristic heuristi <*> Raw.mkGpoAcycEdge acyc <*> Raw.mkGpoTheoryTermNum ttnum <*> Raw.mkGpoTheoryTermStr ttstr <*> Raw.mkGpoTheoryTermCmp ttcomp <*> Raw.mkGpoTheoryElement telem <*> Raw.mkGpoTheoryAtom tatom <*> Raw.mkGpoTheoryAtomGrd tatomg where rul b as an ls ln _ = reraiseIO $ do as' <- map Atom <$> peekArray (fromIntegral an) as ls' <- map Literal <$> peekArray (fromIntegral ln) ls iosym (k (GRule (toBool b) as' ls')) wrule b as an w ws wn _ = reraiseIO $ do as' <- map Atom <$> peekArray (fromIntegral an) as ws' <- map fromRawWeightedLiteral <$> peekArray (fromIntegral wn) ws iosym (k (GWeightedRule (toBool b) as' (fromIntegral w) ws')) minim w ws wn _ = reraiseIO $ do ws' <- map fromRawWeightedLiteral <$> peekArray (fromIntegral wn) ws iosym (k (GMinimize (fromIntegral w) ws')) proj as an _ = reraiseIO $ do as' <- map Atom <$> peekArray (fromIntegral an) as iosym (k (GProject as')) exter a t _ = reraiseIO $ iosym (k (GExternal (Atom a) (fromRawExtT t))) assum ls n _ = reraiseIO $ do ls' <- map Literal <$> peekArray (fromIntegral n) ls iosym (k (GAssume ls')) heuristi a t c d ls n _ = reraiseIO $ do let a' = Atom a t' = fromRawHeuT t c' = fromIntegral c d' = fromIntegral d ls' <- map Literal <$> peekArray (fromIntegral n) ls iosym (k (GHeuristic a' t' c' d' ls')) acyc a b ls n _ = reraiseIO $ do let a' = Node . fromIntegral $ a b' = Node . fromIntegral $ b ls' <- map Literal <$> peekArray (fromIntegral n) ls iosym (k (GAcycEdge a' b' ls')) ttnum i x _ = reraiseIO $ iosym (k (GTheoryTermNumber (TermId i) (fromIntegral x))) ttstr i t _ = reraiseIO $ do t' <- pack <$> peekCString t iosym (k (GTheoryTermString (TermId i) t')) ttcomp i a is n _ = reraiseIO $ do is' <- map TermId <$> peekArray (fromIntegral n) is case a of (-1) -> iosym (k (GTheoryTermTuple (TermId i) is')) (-2) -> iosym (k (GTheoryTermSet (TermId i) is')) (-3) -> iosym (k (GTheoryTermList (TermId i) is')) a' -> iosym (k (GTheoryTermFunction (TermId i) (TermId (fromIntegral a')) is')) telem i is n ls ln _ = reraiseIO $ do is' <- map TermId <$> peekArray (fromIntegral n) is ls' <- map Literal <$> peekArray (fromIntegral ln) ls iosym (k (GTheoryElement (ElementId i) is' ls')) tatom i t es n = reraiseIO $ do let i' = if i == 0 then Nothing else Just (Atom (fromIntegral i)) t' = TermId t es' <- map ElementId <$> peekArray (fromIntegral n) es iosym (k (GTheoryAtom i' t' es')) tatomg i t es n a b _ = reraiseIO $ do let i' = if i == 0 then Nothing else Just (Atom (fromIntegral i)) t' = TermId t a' = TermId a b' = TermId b es' <- map ElementId <$> peekArray (fromIntegral n) es iosym (k (GTheoryAtomGuard i' t' es' a' b')) registerGroundObserver :: (Bool -> IOSym s ()) -> (AspifStmt s -> IOSym s ()) -> Clingo s () registerGroundObserver i k = do ctrl <- askC gpo <- mkRawGPO i k marshall0 $ with gpo $ \ptr -> Raw.controlRegisterObserver ctrl ptr nullPtr