Skip to content

Fix some small typos in the documentation #252

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
filipeom wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix some small typos in the documentation #252

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions doc/parsing.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,43 +5,43 @@

This library provides functors to create parsers from a given
representation of terms. This allows users to have a parser that
directly outputs temrs in the desired form, without needing to
directly outputs terms in the desired form, without needing to
translate the parser output into the specific AST used in a project.

Parsers (actually, the functors which generates parsers) typically takes
Parsers (actually, the functors which generate parsers) typically take
four module arguments:

- A representation of locations in files. This is used for reporting
parsing and lexing errors, but also to attach to each expression parsed
its location.
- A representation of identifiers. In some languages, there are syntactic
scopes, which are handled using namespaces for variable names. In order
to not pollute the Term module with it, the namespaces are dealt with
not to pollute the Term module with them, the namespaces are dealt with
in this module separately.
- A representation of terms. The functions in this module are used by the
parser to build the various types, terms and formulas corresponding
to the grammar of the input language. All functions of this module
typically takes as first (optional) argument a location (of the type
defined by the previous argument) so that is is possible to have
typically take as their first (optional) argument a location (of the type
defined by the previous argument) so that it is possible to have
locations for expressions.
- A representation of top-level directives. Languages usually defines
- A representation of top-level directives. Languages usually define
several top-level directives to more easily distinguish type definitions,
axioms, lemma, theorems to prove, new assertions, or even sometimes direct
axioms, lemmas, theorems to prove, new assertions, or even sometimes direct
commands for the solver (to set some options for instance). Again, the functions
in this module usually have a first optional argument to set the location
of the directives.

Some simple implementation of theses modules are provided in this library.
Some simple implementations of these modules are provided in this library.
See the next section for more information.

## Example

Examples of how to use the parsers can be found in src/main.ml . As mentionned
in the previous section, default implementation for the required functor arguments
are provided, and can be used.
Examples of how to use the parsers can be found in src/main.ml. As mentioned
in the previous section, default implementations for the required functor arguments
are provided and can be used.

For instance, the following code instantiates a parser for the smtlib language
and try to parse a file named "example.smt2" in the home of the current user:
and tries to parse a file named "example.smt2" in the home of the current user:

```ocaml
module P =
Expand Down
2 changes: 1 addition & 1 deletion doc/type.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ let () =

## Global architecture

Contrary to aprsing, where `dolmen` provides one parser for each language,
Contrary to parsing, where `dolmen` provides one parser for each language,
the typechecking part of `dolmen` provides one typechecker, which can be
parameterized depending on which language one wants to type-check.

Expand Down