This is the input module accompanying the implementation of Carneades. It defines a simple parser for a Carneades Argument Evaluation Structure (CAES).
Files are assumed to have the following order of content: one argument or attack on each line, ending in a dot. (Our parser is slightly more relaxed than this and doesn't care about whitespace.)
Argument names are assumed to consist only of letters and numbers. Arguments used in attacks should be declared separately as well.
For a complete example see http://www.cs.nott.ac.uk/~bmv/Code/examplecaes.txt (also included as an additional source file) or see the accompanying ExampleCAES module.
String containing a CAES.
If parsing fails, it propagates the parse error.
Parses the definition of a complete Carneades Argument Evaluation Structure (CAES).
A CAES is parsed in multiple stages:
First parsing zero or more arguments:
where a complete argument consists of
argument followed by an
argName (a letter followed by one or more letters and digits,
underscore or '; alternatively, a string literal), two lists of propositions,
and a conclusion.
Then, zero or more weights,
where a weight is declared by the string
weight followed by the name of a previously declared argument,
Double assigned to that argument.
Then, a list of assumptions,
where a list of assumptions is just the keyword
assumptions followed by a list of propositions.
Then a list of proof standard declarations,
where a proof standard is declared
by the string
standard followed by a proposition and the name of a proof
This is followed by an end of file token.