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)

type Heap t m = Map (VarId t) (Binding t m)

State

data Binding t m

Constructors

VAR (VarId t)

indirection to other variable

NONVAR t

bound to term

ACTION (m Bool)

attributed variable, with given action

data HState t m

Constructors

HState

Fields

var_supply :: VarSupply t

heap :: Heap t m

Instances

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

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

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

initState :: HTerm t => HState t m

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

data Unify t

Constructors

t Unify t

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

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

unify two arbitrary terms

failure :: Monad m => m Bool

success :: Monad m => m Bool

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

bind a variable to a term

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

alias one variable to another

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

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

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