Copyright	(c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	eugenk@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	None

CommonLogic.Parse_CLIF

Description

Parser of common logic interchange format

Synopsis

Documentation

cltext :: PrefixMap -> CharParser st TEXT_META

parser for getText

namedtext :: CharParser st (TEXT, [PrefixMapping])

text :: CharParser st (TEXT, [PrefixMapping])

phrase :: CharParser st ([PHRASE], [PrefixMapping])

prefix :: CharParser st [PrefixMapping]

comment_txt :: CharParser st (TEXT, [PrefixMapping])

pModule :: CharParser st (MODULE, [PrefixMapping])

parser for module

pModExcl :: CharParser st ([NAME], (TEXT, [PrefixMapping]))

parser for

importation :: CharParser st IMPORTATION

sentence :: CharParser st SENTENCE

parser for sentences

quantsent1 :: Bool -> Token -> CharParser st SENTENCE

quantsent2 :: Bool -> Token -> Maybe NAME -> CharParser st SENTENCE

quantsent3 :: Bool -> Maybe NAME -> [NAME_OR_SEQMARK] -> [(NAME_OR_SEQMARK, TERM)] -> SENTENCE -> Range -> SENTENCE

boundlist :: CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]

atom :: CharParser st ATOM

term :: CharParser st TERM

term_fun_cmt :: CharParser st TERM

termseq :: CharParser st TERM_SEQ

rolesetTerm :: CharParser st TERM

rolesetNT :: CharParser st (NAME, TERM)

rolesetSentence :: TERM -> [(NAME, TERM)] -> SENTENCE

rolesetFreeName :: TERM -> [(NAME, TERM)] -> NAME

rolesetAddToTerm :: NAME -> TERM -> SENTENCE

rolesetMixTerm :: NAME -> (NAME, TERM) -> SENTENCE

intNameOrSeqMark :: CharParser st NAME_OR_SEQMARK

symbItems :: GenParser Char st SYMB_ITEMS

Parse a list of comma separated symbols.

symbs :: GenParser Char st ([NAME_OR_SEQMARK], [Token])

parse a comma separated list of symbols

symbMapItems :: GenParser Char st SYMB_MAP_ITEMS

parse a list of symbol mappings

symbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])

parse a comma separated list of symbol mappings

symbMap :: GenParser Char st SYMB_OR_MAP

parsing one symbol or a mapping of one to a second symbol

symbMapS :: GenParser Char st SYMB_OR_MAP

symbMapN :: GenParser Char st SYMB_OR_MAP

basicSpec :: PrefixMap -> AParser st BASIC_SPEC

Toplevel parser for basic specs

parseBasicItems :: PrefixMap -> AParser st BASIC_ITEMS

parseSentences :: PrefixMap -> AParser st BASIC_ITEMS

parseClText :: PrefixMap -> AParser st BASIC_ITEMS

textToAn :: [TEXT_META] -> [Annoted TEXT_META]

parseAxItems :: PrefixMap -> AParser st BASIC_SPEC

parser for Axiom_items

parseAx :: PrefixMap -> AParser st BASIC_ITEMS

Toplevel parser for formulae

aFormula :: PrefixMap -> AParser st (Annoted TEXT_META)

Toplevel parser for formulae