Skip to content

Commit

Permalink
Fix typos in .hs files, refs Copilot-Language#560
Browse files Browse the repository at this point in the history
  • Loading branch information
philderbeast committed Jan 8, 2025
1 parent e85bb7a commit 94c2104
Show file tree
Hide file tree
Showing 18 changed files with 27 additions and 27 deletions.
2 changes: 1 addition & 1 deletion copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
--
Expand Down
6 changes: 3 additions & 3 deletions copilot-c99/tests/Test/Copilot/Compile/C99.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)))
]

Expand Down
2 changes: 1 addition & 1 deletion copilot-interpreter/src/Copilot/Interpret/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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@
Expand Down
4 changes: 2 additions & 2 deletions copilot-interpreter/src/Copilot/Interpret/Render.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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]]
Expand Down
4 changes: 2 additions & 2 deletions copilot-language/src/Copilot/Language/Analyze.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.)"
2 changes: 1 addition & 1 deletion copilot-libraries/src/Copilot/Library/Statistics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 )

Expand Down
2 changes: 1 addition & 1 deletion copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
8 changes: 4 additions & 4 deletions copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 (..)
Expand Down
2 changes: 1 addition & 1 deletion copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down
4 changes: 2 additions & 2 deletions copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
-- @
Expand All @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion copilot/examples/Array.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 #-}
Expand Down
2 changes: 1 addition & 1 deletion copilot/examples/Engine.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion copilot/examples/Voting.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion copilot/examples/WCV.hs
Original file line number Diff line number Diff line change
@@ -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 #-}
Expand Down

0 comments on commit 94c2104

Please sign in to comment.