From 7b174080e399030cb24683c293e03a5d663cafd6 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 15 Jan 2026 14:18:32 +0100 Subject: [PATCH] Fix some small typos in the documentation --- doc/parsing.md | 24 ++++++++++++------------ doc/type.md | 2 +- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/doc/parsing.md b/doc/parsing.md index 16f1179a2..a6a21fde7 100644 --- a/doc/parsing.md +++ b/doc/parsing.md @@ -5,10 +5,10 @@ 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 @@ -16,32 +16,32 @@ four module arguments: 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 = diff --git a/doc/type.md b/doc/type.md index 02c718254..f9ef234b0 100644 --- a/doc/type.md +++ b/doc/type.md @@ -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.