From 94c210488d96d8ea16c692df0da5fa6469a9fc4c Mon Sep 17 00:00:00 2001
From: Phil de Joux <philderbeast@gmail.com>
Date: Wed, 8 Jan 2025 13:38:47 -0500
Subject: [PATCH] Fix typos in .hs files, refs #560

---
 copilot-c99/src/Copilot/Compile/C99/CodeGen.hs            | 2 +-
 copilot-c99/tests/Test/Copilot/Compile/C99.hs             | 6 +++---
 copilot-interpreter/src/Copilot/Interpret/Eval.hs         | 2 +-
 copilot-interpreter/src/Copilot/Interpret/Render.hs       | 4 ++--
 copilot-language/src/Copilot/Language/Analyze.hs          | 4 ++--
 .../src/Copilot/Language/Operators/Integral.hs            | 2 +-
 copilot-libraries/src/Copilot/Library/Statistics.hs       | 2 +-
 copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs  | 2 +-
 .../src/Copilot/Theorem/TransSys/Invariants.hs            | 2 +-
 copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs      | 8 ++++----
 copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs | 4 ++--
 copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs      | 2 +-
 copilot-theorem/src/Copilot/Theorem/What4/Translate.hs    | 2 +-
 copilot-theorem/tests/Test/Copilot/Theorem/What4.hs       | 4 ++--
 copilot/examples/Array.hs                                 | 2 +-
 copilot/examples/Engine.hs                                | 2 +-
 copilot/examples/Voting.hs                                | 2 +-
 copilot/examples/WCV.hs                                   | 2 +-
 18 files changed, 27 insertions(+), 27 deletions(-)

diff --git a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
index ce822e55..a06c4d61 100644
--- a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
+++ b/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.
     --
diff --git a/copilot-c99/tests/Test/Copilot/Compile/C99.hs b/copilot-c99/tests/Test/Copilot/Compile/C99.hs
index 60276e87..78b5fc66 100644
--- a/copilot-c99/tests/Test/Copilot/Compile/C99.hs
+++ b/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)))
   ]
 
diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
index 462b5853..6a142c7a 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs
+++ b/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@
diff --git a/copilot-interpreter/src/Copilot/Interpret/Render.hs b/copilot-interpreter/src/Copilot/Interpret/Render.hs
index 3b6241a8..82a10526 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Render.hs
+++ b/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]]
diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs
index 04de14ed..379c40b4 100644
--- a/copilot-language/src/Copilot/Language/Analyze.hs
+++ b/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
diff --git a/copilot-language/src/Copilot/Language/Operators/Integral.hs b/copilot-language/src/Copilot/Language/Operators/Integral.hs
index e4d05249..e95437c5 100644
--- a/copilot-language/src/Copilot/Language/Operators/Integral.hs
+++ b/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.)"
diff --git a/copilot-libraries/src/Copilot/Library/Statistics.hs b/copilot-libraries/src/Copilot/Library/Statistics.hs
index d6e0330b..775cc6f3 100644
--- a/copilot-libraries/src/Copilot/Library/Statistics.hs
+++ b/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 )
 
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
index 6851d46f..5c3fb0ae 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
+++ b/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.
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs
index 3a41d615..ebf566ac 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs
+++ b/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)]
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
index d2a95338..92bf9633 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
+++ b/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
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
index 79edd282..1a66704a 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
+++ b/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
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs
index e1408f04..eff4bcd8 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs
+++ b/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 (..)
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index f6ced33b..40ddc9b3 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/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) ->
diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
index dbd98eb4..7039e8a0 100644
--- a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
+++ b/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)
diff --git a/copilot/examples/Array.hs b/copilot/examples/Array.hs
index 7f43a21b..3769ad86 100644
--- a/copilot/examples/Array.hs
+++ b/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        #-}
diff --git a/copilot/examples/Engine.hs b/copilot/examples/Engine.hs
index 1200170f..d8e7bbea 100644
--- a/copilot/examples/Engine.hs
+++ b/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.
diff --git a/copilot/examples/Voting.hs b/copilot/examples/Voting.hs
index d534fe2c..aaf23e64 100644
--- a/copilot/examples/Voting.hs
+++ b/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.
diff --git a/copilot/examples/WCV.hs b/copilot/examples/WCV.hs
index 3ac016fb..4636bacb 100644
--- a/copilot/examples/WCV.hs
+++ b/copilot/examples/WCV.hs
@@ -1,6 +1,6 @@
 -- | This example shows an implementation of the Well-Clear Violation
 -- algorithm, it follows the implementation described in 'Analysis of
--- Well-Clear Bounday Models for the Integration of UAS in the NAS',
+-- Well-Clear Boundary Models for the Integration of UAS in the NAS',
 -- https://ntrs.nasa.gov/citations/20140010078.
 
 {-# LANGUAGE DataKinds        #-}