Add typos checks and fix typos it found

.github/workflows/typos.yml

@@ -0,0 +1,35 @@
+name: Typos
+
+permissions:
+  contents: read
+
+on:
+  pull_request:
+  push:
+
+env:
+  TYPOS_VER: v1.29.1
+  TYPOS_PLATFORM: x86_64-unknown-linux-musl
+  CLICOLOR: 1
+
+jobs:
+  typos:
+    defaults:
+      run:
+        shell: bash
+    runs-on: ubuntu-latest
+
+    steps:
+
+    - uses: actions/checkout@v4
+
+    - run: |
+        wget -q https://github.com/crate-ci/typos/releases/download/${{ env.TYPOS_VER }}/typos-${{ env.TYPOS_VER }}-${{ env.TYPOS_PLATFORM }}.tar.gz
+        tar -xf typos-${{ env.TYPOS_VER }}-${{ env.TYPOS_PLATFORM }}.tar.gz --one-top-level=typos-${{ env.TYPOS_VER }}
+        mkdir -p "$HOME/.local/bin"
+        mv typos-${{ env.TYPOS_VER }} "$HOME/.local/bin/typos-${{ env.TYPOS_VER }}"
+        chmod +x "$HOME/.local/bin/typos-${{ env.TYPOS_VER }}/typos"
+        echo "$HOME/.local/bin/typos-${{ env.TYPOS_VER }}" >> $GITHUB_PATH
+
+    - run: make markdown-typos
+    - run: make hs-typos

.typos.toml

@@ -0,0 +1,16 @@
+[type.hs]
+extend-glob = []
+extend-ignore-identifiers-re = []
+extend-ignore-words-re = []
+extend-ignore-re = []
+
+[type.hs.extend-identifiers]
+sIy = "sIy"
+vIy = "vIy"
+tre = "tre"
+inh = "inh"
+TypeLits = "TypeLits"
+fof = "fof"
+
+[type.hs.extend-words]
+alse = "alse"

Makefile

@@ -0,0 +1,36 @@
+all: help-banner help
+
+PHONY: help
+help: ## Show the commented targets.
+	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | \
+	sort | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'
+
+PHONY: help-banner
+help-banner: ## Show the help banner.
+	@echo "===================================================================="
+	@echo "§ all                  make with no arguments also shows this banner"
+	@echo "§ help                 make help will list targets with descriptions"
+	@echo "===================================================================="
+
+.PHONY: typos-install
+typos-install: ## Install typos-cli for typos target using cargo.
+	cargo install typos-cli
+
+GREP_EXCLUDE := grep -v -E 'dist-'
+FIND_NAMED := find . -type f -name
+
+.PHONY: markdown-typos
+markdown-typos: ## Find typos in Markdown .md files.
+	$(FIND_NAMED) '*.md' | $(GREP_EXCLUDE) | xargs typos
+
+.PHONY: markdown-fix-typos
+markdown-fix-typos: ## Fix typos in Markdown .md files.
+	$(FIND_NAMED) '*.md' | $(GREP_EXCLUDE) | xargs typos --write-changes
+
+.PHONY: hs-typos
+hs-typos: ## Find typos in Haskell .hs files.
+	$(FIND_NAMED) '*.hs' | $(GREP_EXCLUDE) | xargs typos
+
+.PHONY: hs-fix-typos
+hs-fix-typos: ## Fix typos in Haskell .hs files.
+	$(FIND_NAMED) '*.hs' | $(GREP_EXCLUDE) | xargs typos --write-changes

copilot-c99/src/Copilot/Compile/C99/CodeGen.hs

@@ -267,7 +267,7 @@ mkStep cSettings streams triggers exts =
     --
     -- We create temporary variables because:
     --
-    -- 1. We want to pass structs by reference intead of by value. To this end,
+    -- 1. We want to pass structs by reference instead of by value. To this end,
     --    we use C's & operator to obtain a reference to a temporary variable
     --    of a struct type and pass that to the handler function.
     --

copilot-c99/src/Copilot/Compile/C99/Compile.hs

@@ -283,7 +283,7 @@ typeTypes ty = case ty of
   _         -> [UType ty]
 
 -- | Collect all expression of a list of streams and triggers and wrap them
--- into an UEXpr.
+-- into an UExpr.
 gatherExprs :: [Stream] -> [Trigger] -> [UExpr]
 gatherExprs streams triggers =  map streamUExpr streams
                              ++ concatMap triggerUExpr triggers

copilot-c99/tests/Test/Copilot/Compile/C99.hs

@@ -240,9 +240,9 @@ arbitraryOpBoolBits =
     ]
 
 -- | Generator of functions that take Nums and produce booleans.
-arbitaryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a)
+arbitraryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a)
                        => Gen (Fun a Bool, [a] -> [Bool])
-arbitaryOpBoolOrdEqNum =
+arbitraryOpBoolOrdEqNum =
   frequency
     [ (1, funCompose2 <$> arbitraryOp2Eq  <*> arbitraryOpNum <*> arbitraryOpNum)
     , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpNum <*> arbitraryOpNum)
@@ -379,7 +379,7 @@ arbitraryOpIntegralBool = frequency
 
     -- we need to use +1 because certain operations overflow the number
   , (2, mkTestCase1
-          arbitaryOpBoolOrdEqNum
+          arbitraryOpBoolOrdEqNum
           (chooseBoundedIntegral (minBound + 1, maxBound)))
   ]
 

copilot-interpreter/src/Copilot/Interpret/Eval.hs

@@ -106,7 +106,7 @@ data ExecTrace = ExecTrace
 
 -- We could write this in a beautiful lazy style like above, but that creates a
 -- space leak in the interpreter that is hard to fix while maintaining laziness.
--- We take a more brute-force appraoch below.
+-- We take a more brute-force approach below.
 
 -- | Evaluate a specification for a number of steps.
 eval :: ShowType   -- ^ Show booleans as @0@\/@1@ (C) or @True@\/@False@

copilot-interpreter/src/Copilot/Interpret/Render.hs

@@ -16,7 +16,7 @@ import Text.PrettyPrint
 
 import Prelude hiding ((<>))
 
--- | Render an execution trace as a table, formatted to faciliate readability.
+-- | Render an execution trace as a table, formatted to facilitate readability.
 renderAsTable :: ExecTrace -> String
 renderAsTable
   ExecTrace
@@ -112,7 +112,7 @@ pad :: Int -> Int -> a -> [a] -> [a]
 pad lx max b ls = ls ++ replicate (max - lx) b
 
 -- | Pad a list of strings on the right with spaces.
-pad' :: Int      -- ^ Mininum number of spaces to add
+pad' :: Int      -- ^ Minimum number of spaces to add
      -> Int      -- ^ Maximum number of spaces to add
      -> [[Doc]]  -- ^ List of documents to pad
      -> [[Doc]]

copilot-language/src/Copilot/Language/Analyze.hs

@@ -60,13 +60,13 @@ instance Show AnalyzeException where
   show (DifferentTypes name) = badUsage $
     "The external symbol \'" ++ name ++ "\' has been declared to have two different types!"
   show (Redeclared name) = badUsage $
-    "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."
+    "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a function symbol, etc.)."
   show (BadNumberOfArgs name) = badUsage $
     "The function symbol \'" ++ name ++ "\' has been redeclared to have different number of arguments."
   show (BadFunctionArgType name) = badUsage $
     "The function symbol \'" ++ name ++ "\' has been redeclared to an argument with different types."
 
--- | 'Exception' instance so we can throw and catch 'AnalyzeExcetion's.
+-- | 'Exception' instance so we can throw and catch 'AnalyzeException's.
 instance Exception AnalyzeException
 
 -- | Max level of recursion supported. Any level above this constant

copilot-language/src/Copilot/Language/Operators/Integral.hs

@@ -46,4 +46,4 @@ x `mod` y = Op2 (Core.Mod typeOf) x y
 (Const x) ^ (Const y)  = Const (x P.^ y)
 (Const 2) ^ y          = (Const 1) .<<. y
 x ^ (Const y)          = foldl' ((P.*)) (Const 1) (replicate (P.fromIntegral y) x)
-_ ^ _                  = Err.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant.  (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentation of floats/doubles.)"
+_ ^ _                  = Err.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant.  (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentiation of floats/doubles.)"

copilot-libraries/src/Copilot/Library/Statistics.hs

@@ -32,7 +32,7 @@ min n s = nfoldl1 n smallest s
       smallest = \ x y -> mux ( x <= y ) x y
 
 -- | Mean value.  @n@ must not overflow
--- for word size @a@ for streams over which computation is peformed.
+-- for word size @a@ for streams over which computation is performed.
 mean :: ( Typed a, Eq a, Fractional a ) => Int -> Stream a -> Stream a
 mean n s = ( sum n s ) / ( fromIntegral n )
 

copilot-theorem/README.md

@@ -216,7 +216,7 @@ process* [7] and so we have no way to keep them.
 #### Types
 
 In these three formats, GADTs are used to statically ensure a part of the
-type-corectness of the specification, in the same spirit it is done in the
+type-correctness of the specification, in the same spirit it is done in the
 other Copilot libraries. *copilot-theorem* handles only three types which are
 `Integer`, `Real` and `Bool` and which are handled by the SMTLib standard.
 *copilot-theorem* works with *pure* reals and integers. Thus, it is unsafe in the
@@ -389,9 +389,9 @@ the model-checking techniques we are using.
 #### Limitations related to Copilot implementation
 
 The reification process used to build the `Core.Spec` object looses many
-informations about the structure of the original Copilot program. In fact, a
+information about the structure of the original Copilot program. In fact, a
 stream is kept in the reified program only if it is recursively defined.
-Otherwise, all its occurences will be inlined. Moreover, let's look at the
+Otherwise, all its occurrences will be inlined. Moreover, let's look at the
 `intCounter` function defined in the example `Grey.hs`:
 
 ```haskell
@@ -413,7 +413,7 @@ There are many problems with this:
 * It makes the inputs given to the SMT solvers larger and repetitive.
 
 We can't rewrite the Copilot reification process in order to avoid these
-inconvenients as these informations are lost by GHC itself before it occurs.
+inconvenients as these information are lost by GHC itself before it occurs.
 The only solution we can see would be to use *Template Haskell* to generate
 automatically some structural annotations, which might not be worth the dirt
 introduced.
@@ -423,7 +423,7 @@ introduced.
 ##### Limitations of the IC3 algorithm
 
 The IC3 algorithm was shown to be a very powerful tool for hardware
-certification. However, the problems encountered when verifying softwares are
+certification. However, the problems encountered when verifying software are
 much more complex. For now, very few non-inductive properties can be proved by
 *Kind2* when basic integer arithmetic is involved.
 
@@ -433,7 +433,7 @@ the inductiveness* (CTI) for a property, these techniques are used to find a
 lemma discarding it which is general enough so that all CTIs can be discarded
 in a finite number of steps.
 
-The lemmas found by the current version fo *Kind2* are often too weak. Some
+The lemmas found by the current version of *Kind2* are often too weak. Some
 suggestions to enhance this are presented in [1]. We hope some progress will be
 made in this area in a near future.
 
@@ -487,7 +487,7 @@ forAllCst l f = conj $ map (f . constant) l
 ```
 
 However, this solution isn't completely satisfying because the size of the
-property generated is proportionnal to the cardinal of `allowed`.
+property generated is proportional to the cardinal of `allowed`.
 
 #### Some scalability issues
 
@@ -517,7 +517,7 @@ in the Kind2 SMT solver.
 Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't
 support XML output of counterexamples. If the last feature is provided, it
 should be easy to implement counterexamples displaying in *copilot-theorem*. For
-this, we recommend to keep some informations about *observers* in
+this, we recommend to keep some information about *observers* in
 `TransSys.Spec` and to add one variable per observer in the Kind2 output file.
 
 #### Bad handling of non-linear operators and external functions
@@ -576,12 +576,12 @@ complexity added. It's especially true at the time I write this in the sense
 that:
 
 * Each predicate introduced is used only one time (which is true because
-  copilot doesn't handle functions or parametrized streams like Lustre does and
+  copilot doesn't handle functions or parameterized streams like Lustre does and
   everything is inlined during the reification process).
 * A similar form of structure could be obtained from a flattened Kind2 native
   input file with some basic static analysis by producing a dependency graph
   between variables.
-* For now, the *Kind2* model-checker ignores these structure informations.
+* For now, the *Kind2* model-checker ignores these structure information.
 
 However, the current code offers some nice transformation tools (node merging,
 `Renaming` monad...) which could be useful if you intend to write a tool for

copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs

@@ -9,7 +9,7 @@ import Copilot.Theorem.Kind2.AST
 
 import Data.List (intercalate)
 
--- | A tree of expressions, in which the leafs are strings.
+-- | A tree of expressions, in which the leaves are strings.
 type SSExpr = SExpr String
 
 -- | Reserved keyword prime.

copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs

@@ -8,7 +8,7 @@ module Copilot.Theorem.TransSys.Invariants
   , prop
   ) where
 
--- | Type class for types with additional invariants or contraints.
+-- | Type class for types with additional invariants or constraints.
 class HasInvariants a where
 
   invariants :: a -> [(String, Bool)]

copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs

@@ -74,11 +74,11 @@ data Node = Node
                                            --   its local name.
   , nodeConstrs       :: [Expr Bool] }
 
--- | Identifer of a variable in the local (within one node) namespace.
+-- | Identifier of a variable in the local (within one node) namespace.
 data Var      =  Var {varName :: String}
   deriving (Eq, Show, Ord)
 
--- | Identifer of a variable in the global namespace by specifying both a node
+-- | Identifier of a variable in the global namespace by specifying both a node
 -- name and a variable.
 data ExtVar   =  ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var }
   deriving (Eq, Ord)
@@ -115,7 +115,7 @@ foldExpr f expr = f expr <> fargs
 foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m
 foldUExpr f (U e) = foldExpr f e
 
--- | Apply an arbitrary transformation to the leafs of an expression.
+-- | Apply an arbitrary transformation to the leaves of an expression.
 transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t
 transformExpr f = tre
   where
@@ -126,7 +126,7 @@ transformExpr f = tre
     tre e                 = f e
 
 -- | The set of variables related to a node (union of the local variables and
--- the imported variables after deferencing them).
+-- the imported variables after dereferencing them).
 nodeVarsSet :: Node -> Set Var
 nodeVarsSet = liftA2 Set.union
   nodeLocalVarsSet

copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs

@@ -266,10 +266,10 @@ complete spec =
                 -- To get readable names, we don't prefix variables
                 -- which come from merged nodes as they are already
                 -- decorated
-                let preferedName
+                let preferredName
                      | head ncNodeIdSep `elem` n' = v
                      | otherwise = n' `prefix` v
-                alias <- getFreshName [preferedName, n' `prefix` v]
+                alias <- getFreshName [preferredName, n' `prefix` v]
                 return $ Bimap.tryInsert alias ev acc
 
           foldM tryImport (nodeImportedVars n) toImportVars

copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs

@@ -2,7 +2,7 @@
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE Safe                      #-}
 
--- | Types suported by the modular transition systems.
+-- | Types supported by the modular transition systems.
 module Copilot.Theorem.TransSys.Type
   ( Type (..)
   , U (..)

copilot-theorem/src/Copilot/Theorem/What4/Translate.hs

@@ -479,7 +479,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
       recip fiRepr e = do
         one <- fpLit fiRepr 1.0
         WFP.iFloatDiv @_ @fi sym fpRM one e
-  -- The argument should not cause the result to overflow or underlow
+  -- The argument should not cause the result to overflow or underflow
   (CE.Exp _, xe) -> liftIO $ fpSpecialOp WSF.Exp xe
   -- The argument should not be less than -0
   (CE.Sqrt _, xe) ->

copilot-theorem/tests/Test/Copilot/Theorem/What4.hs

@@ -69,7 +69,7 @@ testProveZ3False =
     spec :: Spec
     spec = propSpec propName $ Const typeOf False
 
--- | Test that Z3 is able to prove the following expresion valid:
+-- | Test that Z3 is able to prove the following expression valid:
 -- @
 --   for all (x :: Int8), constant x == constant x
 -- @
@@ -84,7 +84,7 @@ testProveZ3EqConst = forAll arbitrary $ \x ->
     spec x = propSpec propName $
       Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
 
--- | Test that Z3 is able to prove the following expresion valid:
+-- | Test that Z3 is able to prove the following expression valid:
 -- @
 --   for all (s :: MyStruct),
 --   ((s ## testField =$ (+1)) # testField) == ((s # testField) + 1)

copilot/examples/Array.hs

@@ -3,7 +3,7 @@
 -- | This is a simple example for arrays. As a program, it does not make much
 -- sense, however it shows of the features of arrays nicely.
 
--- | Enable compiler extension for type-level data, necesary for the array
+-- | Enable compiler extension for type-level data, necessary for the array
 -- length.
 
 {-# LANGUAGE DataKinds        #-}

copilot/examples/Engine.hs

@@ -9,7 +9,7 @@ module Main where
 import Language.Copilot
 import qualified Prelude as P
 
--- If the majority of the engine temperature probes exeeds 250 degrees, then
+-- If the majority of the engine temperature probes exceeds 250 degrees, then
 -- the cooler is engaged and remains engaged until the majority of the engine
 -- temperature probes drop to 250 or below.  Otherwise, trigger an immediate
 -- shutdown of the engine.

copilot/examples/Voting.hs

@@ -10,7 +10,7 @@ import Language.Copilot
 
 vote :: Spec
 vote = do
-  -- majority selects element with the biggest occurance.
+  -- majority selects element with the biggest occurrence.
   trigger "maj"  true [arg maj]
 
   -- aMajority checks if the selected element has a majority.