Documentation

readTuple :: (Show a, Show b) => MSaxState a -> MSaxState b -> MSaxState (a, b) Source #

readWord :: MSaxState String Source #

readStr :: MSaxState String Source #

readInt :: MSaxState Int Source #

readInt' :: MSaxState Int Source #

readMappedInt :: Map Int a -> MSaxState a Source #

listToTypes :: Map Int HolType -> [Int] -> Maybe [HolType] Source #

readSharedHolType :: Map Int String -> Map Int HolType -> MSaxState (Map Int HolType) Source #

readParseType :: MSaxState HolParseType Source #

readTermInfo :: MSaxState HolTermInfo Source #

readSharedHolTerm :: Map Int HolType -> Map Int String -> Map Int Term -> MSaxState (Map Int Term) Source #

importData :: HetcatsOpts -> FilePath -> IO ([(String, [(String, Term)])], [(String, String)]) Source #

getTypes :: Map String Int -> HolType -> Map String Int Source #

mergeTypesOps :: (Map String Int, Map String HolType) -> (Map String Int, Map String HolType) -> (Map String Int, Map String HolType) Source #

getOps :: Term -> (Map String Int, Map String HolType) Source #

calcSig :: [(String, Term)] -> Sign Source #

sigDepends :: Sign -> Sign -> Bool Source #

prettifyTypeVarsTp :: HolType -> Map String String -> (HolType, Map String String) Source #

prettifyTypeVarsTm :: Term -> Map String String -> (Term, Map String String) Source #

prettifyTypeVars :: ([(String, [(String, Term)])], [(String, String)]) -> ([(String, [(String, Term)])], [(String, String)]) Source #

treeLevels :: [(String, String)] -> Map Int [(String, String)] Source #

makeNamedSentence :: String -> Term -> Named Sentence Source #

_insNodeDG :: Sign -> [Named Sentence] -> FilePath -> String -> (DGraph, Map String (String, Node, DGNodeLab)) -> (DGraph, Map String (String, Node, DGNodeLab)) Source #

anaHolLightFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv)) Source #