OCaml warns when there is a .ml file but no .mli file. This commit adds
almost all the missing .mli files. The remaining ones are the *_ast.ml
files, as the .mli files would be verbatim copies.
This is inspired from the python printer/parser, the changes are:
- and, or, and then, or else are now supported instead of /\, \/, &&, ||
- different (LTGT) is now '/=' instead of '<>'
- allowing A'Last, A'First using "name" attributes
- allowing the notation "for all i in A .. B => stuff"
- allowing syntax for arrays as A(I) using new attributes "syntax" (also
the reason why we need to pass a name table to the parser)
- some constants are printed as "(cst:type)" (This is not real Ada syntax
and should probably be replaced by "type'(cst)"
This also adds a test at tests/ada_terms/print_test.adb
This adds new cases in any_pp: note that all these cases are needed as we
cannot use the legacyprinter for calls to, for instance, print_ls.
This would have the disadvantage that, when printed twice (reload), idents
gets reprinted which would change their disambiguation number (break at
every reload).
Also, pass the task to the printer in order to be able to detect which
lsymbols are used in record fields definitions.
Parser edition with respect to the Why3 parser:
- Removing qualification (not usable in transformation anyway)
- QUOTE disallowed in ident: still allowing it for type variable
- the ada parser uses a naming table during the parsing phase. The naming
table does not influence the parsing but is used to generate different
trees depending on the names recognized. It is useful to distinct a
function from an array in application as the syntax is the same.
Note that the naming_table is passed with a reference: we may want to
improve this in the future (no other known solution to the author of this
message).
New attributes appears:
- [@syntax:array:] followed by name of the getter function to be used:
this is used to know which function should be used as getter for this type
during the parsing.
- [@syntax:getter:] followed by its own name: this is used to know during
the printing if the function should be removed from the display to
simplify the notation. The name is checked in case attributes of a
specific ident are derived or copied to another one.
Add README with some changes in to be changed syntax
This is a proof of concept of the external printing/parsing. This works by
adding externally defined (from Pretty) elements to the standard
printing/parsing. We use the example of the Python plugin to show how it
works:
- the tasks should contain new notations (example python: /\ replaced by "and")
- the new notations can be used in the transformations (example python:
"assert (0 == 0 and b > 1)"
The file format contained in the session is used to decide which external
parser/printer to use. These are registered in a similar way that language,
parser, or transformations are registered. For example, a goal whose ancestor
is a python file (according to the file format inside the session) will be
printed with the Python external printer; and transformations originating
from this goal will be parsed with the same language.
