Control.CP.Herbrand.Herbrand

This module provides a Herbrand solver.

The type of terms is parameterized by the HTerm type class.

Documentation

class Ord (VarId t) => HTerm t where

Herbrand terms

Associated Types

type VarId t :: *

data VarSupply t :: *

Methods

varSupply :: VarSupply t

supplyVar :: VarSupply t -> (t, VarSupply t)

mkVar :: VarId t -> t

isVar :: t -> Maybe (VarId t)

children :: t -> ([t], [t] -> t)

nonvar_unify :: MonadState (HState t m) m => t -> t -> m Bool

Instances

HTerm PrologTerm

data Herbrand t a

Herbrand monad

Constructors

Herbrand

Fields

unH :: State (HState t (Herbrand t)) a

Instances

Monad (Herbrand t)

Functor (Herbrand t)

Applicative (Herbrand t)

HTerm t => Solver (Herbrand t)

Solver instance

HTerm t => Term (Herbrand t) t

MonadState (HState t (Herbrand t)) (Herbrand t)

failure :: Monad m => m Bool

success :: Monad m => m Bool

unify :: (HTerm t, MonadState (HState t m) m) => t -> t -> m Bool

unify two arbitrary terms

shallow_normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t

registerAction :: (HTerm t, MonadState (HState t m) m) => t -> m Bool -> m ()

data HState t m

Instances

MonadState (HState t (Herbrand t)) (Herbrand t)

Solver s => MonadState (HState t (HerbrandT t s)) (HerbrandT t s)

data Unify t

initState :: HTerm t => HState t m

addH :: (HTerm t, MonadState (HState t m) m) => Unify t -> m Bool

newvarH :: (HTerm t, MonadState (HState t m) m) => m t