simple-topes-0.1.0.0

Safe Haskell	Safe-Inferred
Language	Haskell2010

RSTT.Interpret

Contents

Compiling rules
Converting syntax

Synopsis

interpretIO :: String -> IO ()
interpretProgramIO :: Program -> IO ()
interpret :: String -> Either String [String]
unsafeParseTope :: String -> Tope
interpretProgram :: Program -> [String]
interpretDecl :: Decl -> StateT DefinedRules (Writer [String]) ()
convertRule :: TopeRule -> DefinedRules
tableauRule :: TopeRule -> Rules
tableauCutRule :: TopeRule -> Rules
collectRulePoints :: TopeRule -> Set Point
collectSequentPoints :: Sequent -> Set Point
collectTopePoints :: Tope -> Set Point
collectPointVars :: Point -> Set Var
data Substs = Substs {
- substCubeVars :: [(Var, Cube)]
- substPointVars :: [(Var, Point)]
- substTopeVars :: [(Var, Tope)]
}
matchSequent :: (MonadPlus f, MonadFail f) => Set Var -> Sequent -> Sequent -> f (Substs, [Tope])
matchVars :: Alternative f => Set Var -> Set Point -> f Substs
matchTopeContext :: (MonadPlus f, MonadFail f) => Substs -> TopeContext -> TopeContext -> f (Substs, TopeContext)
matchTope :: MonadPlus f => Tope -> Tope -> f Substs
matchPoint :: MonadPlus f => Point -> Point -> f Substs
matchTopes :: (MonadPlus f, MonadFail f) => Substs -> [Tope] -> [Tope] -> f (Substs, [Tope])
mergeSubsts :: MonadPlus f => Substs -> Substs -> f Substs
mergeManySubsts :: MonadPlus f => [Substs] -> f Substs
merge :: (MonadPlus f, Eq k, Eq v, Show k, Show v) => [(k, v)] -> [(k, v)] -> f [(k, v)]
normalizeSequent :: Sequent -> Sequent
nubSort :: Ord a => [a] -> [a]
applySubsts :: Substs -> Sequent -> Sequent
substInCubeContext :: [(Var, Cube)] -> CubeContext -> CubeContext
substInTopeContext :: [(Var, Point)] -> [(Var, Tope)] -> TopeContext -> TopeContext
substInTope :: [(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope
substInPoint :: [(Var, Point)] -> Point -> Point
convertSequent :: Sequent -> Sequent
convertCubeContext :: CubeContext -> CubeContext
convertCube :: Cube -> Cube
convertPoint :: Point -> Point
convertTope :: Tope -> Tope
convertTopeContext :: TopeContext -> TopeContext

Documentation

interpretIO :: String -> IO () Source #

interpretProgramIO :: Program -> IO () Source #

interpret :: String -> Either String [String] Source #

unsafeParseTope :: String -> Tope Source #

interpretProgram :: Program -> [String] Source #

interpretDecl :: Decl -> StateT DefinedRules (Writer [String]) () Source #

Compiling rules

convertRule :: TopeRule -> DefinedRules Source #

tableauRule :: TopeRule -> Rules Source #

tableauCutRule :: TopeRule -> Rules Source #

collectRulePoints :: TopeRule -> Set Point Source #

collectSequentPoints :: Sequent -> Set Point Source #

collectTopePoints :: Tope -> Set Point Source #

collectPointVars :: Point -> Set Var Source #

data Substs Source #

Constructors

Substs
Fields substCubeVars :: [(Var, Cube)] substPointVars :: [(Var, Point)] substTopeVars :: [(Var, Tope)]

Instances

Instances details

Semigroup Substs Source #
Instance details Defined in RSTT.Interpret Methods (<>) :: Substs -> Substs -> Substs # sconcat :: NonEmpty Substs -> Substs # stimes :: Integral b => b -> Substs -> Substs #

matchSequent :: (MonadPlus f, MonadFail f) => Set Var -> Sequent -> Sequent -> f (Substs, [Tope]) Source #

matchVars :: Alternative f => Set Var -> Set Point -> f Substs Source #

matchTopeContext :: (MonadPlus f, MonadFail f) => Substs -> TopeContext -> TopeContext -> f (Substs, TopeContext) Source #

matchTope :: MonadPlus f => Tope -> Tope -> f Substs Source #

matchPoint :: MonadPlus f => Point -> Point -> f Substs Source #

matchTopes :: (MonadPlus f, MonadFail f) => Substs -> [Tope] -> [Tope] -> f (Substs, [Tope]) Source #

mergeSubsts :: MonadPlus f => Substs -> Substs -> f Substs Source #

mergeManySubsts :: MonadPlus f => [Substs] -> f Substs Source #

merge :: (MonadPlus f, Eq k, Eq v, Show k, Show v) => [(k, v)] -> [(k, v)] -> f [(k, v)] Source #

normalizeSequent :: Sequent -> Sequent Source #

nubSort :: Ord a => [a] -> [a] Source #

applySubsts :: Substs -> Sequent -> Sequent Source #

substInCubeContext :: [(Var, Cube)] -> CubeContext -> CubeContext Source #

substInTopeContext :: [(Var, Point)] -> [(Var, Tope)] -> TopeContext -> TopeContext Source #

substInTope :: [(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope Source #

substInPoint :: [(Var, Point)] -> Point -> Point Source #

Converting syntax

convertSequent :: Sequent -> Sequent Source #

convertCubeContext :: CubeContext -> CubeContext Source #

convertCube :: Cube -> Cube Source #

convertPoint :: Point -> Point Source #

convertTope :: Tope -> Tope Source #

convertTopeContext :: TopeContext -> TopeContext Source #