Merge pull request #1233 from vuittont60/main

Fix typos

doc/adr001-transpiler-architecture.md

@@ -8,7 +8,7 @@ This document describes a preliminary architecture of the Quint transpiler.  As
 rule, we are using a data-flow approach to parsing, in contrast to the pipeline
 approach, which can be found in textbooks. Our main assumption is that external
 contributors should be able to plug-in their code/passes to our pipeline.
-Hence, we have to be very careful when definining our assumptions about the
+Hence, we have to be very careful when defining our assumptions about the
 input and output of every pass.
 
 The use cases of this architecture are as follows:

doc/adr007-flattening.md

@@ -6,7 +6,7 @@
 
 ## 1. Summary
 
-This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannnot handle imports, instances and exports.
+This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannot handle imports, instances and exports.
 
 ## 2. Context
 
@@ -15,7 +15,7 @@ Our current strategy for flattening has intrinsic problems, and some issues that
 The existing flattener takes import/instance/export statements and replaces them with a copy of the definitions from that module, assigning new ids to those definitions and its inner IR components and adding namespaces when necessary. With this, there are two possible scenarios:
 
 1. All imports, instances and exports include all definitions (i.e. there is no `import A.foo`). In this case, we will end up with a module with all of the definitions from all used modules.
-2. There is some statement refering to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid.
+2. There is some statement referring to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid.
 
 Therefore, it is clear that we need some way of looking into the dependencies of definitions when copying them over, both to avoid (1) by copying only the necessary definitions, and to avoid (2) and ensure the flattened module has all the definitions it needs.
 

doc/design-principles.md

@@ -57,5 +57,5 @@
 - *Quint is CLI-first*:
 
    - The users should be able to parse and transpile Quint in the command-line.
-   - The intermediate transpiler outputs are avaiable in JSON.
-   - IDE support (such as a VSCode plugin) is a beatiful opt-in, not a requirement.
+   - The intermediate transpiler outputs are available in JSON.
+   - IDE support (such as a VSCode plugin) is a beautiful opt-in, not a requirement.

doc/quint.md

@@ -174,7 +174,7 @@ Options:
                                                                         [string]
   --out          output file (suppresses all console output)            [string]
   --out-itf      output the trace in the Informal Trace Format to file
-                 (supresses all console output)                         [string]
+                 (suppresses all console output)                         [string]
   --max-samples  the maximum on the number of traces to try
                                                        [number] [default: 10000]
   --max-steps    the maximum on the number of steps in every trace
@@ -269,7 +269,7 @@ Options:
                      filename)                                          [string]
   --out              output file (suppresses all console output)        [string]
   --out-itf          output the trace in the Informal Trace Format to file
-                     (supresses all console output)                     [string]
+                     (suppresses all console output)                     [string]
   --max-steps        the maximum number of steps in every trace
                                                           [number] [default: 10]
   --init             name of the initializer action   [string] [default: "init"]

doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt

@@ -50,7 +50,7 @@ module erc20 {
             | Error(_) => r
         }
 
-    // An auxilliary definition similar to Solidity's require
+    // An auxiliary definition similar to Solidity's require
     pure def require(r: Erc20Result, cond: bool, msg: str): Erc20Result =
         match r {
             | Error(_) => r

quint/src/cli.ts

@@ -149,7 +149,7 @@ const runCmd = {
         type: 'string',
       })
       .option('out-itf', {
-        desc: 'output the trace in the Informal Trace Format to file (supresses all console output)',
+        desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)',
         type: 'string',
       })
       .option('max-samples', {
@@ -212,7 +212,7 @@ const verifyCmd = {
         type: 'string',
       })
       .option('out-itf', {
-        desc: 'output the trace in the Informal Trace Format to file (supresses all console output)',
+        desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)',
         type: 'string',
       })
       .option('max-steps', {

quint/src/cliCommands.ts

@@ -67,7 +67,7 @@ interface OutputStage {
   // Test names output produced by 'run'
   status?: 'ok' | 'violation' | 'failure'
   trace?: QuintEx[]
-  /* Docstrings by defintion name by module name */
+  /* Docstrings by definition name by module name */
   documentation?: Map<string, Map<string, DocumentationEntry>>
   errors?: ErrorMessage[]
   warnings?: any[] // TODO it doesn't look like this is being used for anything. Should we remove it?
@@ -639,7 +639,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
   const veryfiyingFlat = { ...verifying, ...flattenedAnalysis, modules: [flatMain], table: flattenedTable }
   const parsedSpec = jsonStringOfOutputStage(pickOutputStage(veryfiyingFlat))
 
-  // We need to insert the data form CLI args into thier appropriate locations
+  // We need to insert the data form CLI args into their appropriate locations
   // in the Apalache config
   const config = {
     ...loadedConfig,