module Horn.Monad where
import Control.Monad.State.Strict
import Horn.Logic.Clauses
Copyright By PowCoder代写 加微信 powcoder
type SolveM = StateT SolverState IO
data SolverState = Solver {nx :: Int}
initState = Solver {nx = 0}
——————————————————————-
getNx :: SolveM Int
——————————————————————-
getNx = nx <$> get
——————————————————————-
putNx :: Int -> SolveM ()
——————————————————————-
putNx n = do
put Solver {nx = n}
——————————————————————-
freshVar :: SolveM Var
——————————————————————-
freshVar = do
n <- getNx
putNx (n+1)
return $ Var ("tmp" ++ (show n))
-------------------------------------------------------------------
freshVars :: Int -> SolveM [Var]
——————————————————————-
freshVars k = do
replicateM k freshVar
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com