Always enforce Unix line endings, no trailing whitespace, file-ending…

… newlines, and spaces over tabs

CHANGELOG.md

@@ -7,7 +7,7 @@ K Framework 6.1.0
 
 Features
 --------
-- Added support for MacOS 13 Ventura. We dropped support for Ubuntu 20.04 Focal. 
+- Added support for MacOS 13 Ventura. We dropped support for Ubuntu 20.04 Focal.
   K can now be built from source on Apple Silicon. See README for more details.
 
 - Updated dependency to Java version 17 or higher.
@@ -188,14 +188,14 @@ Features
 
 - Adding the `comm` attribute on a simplification rule will now generate a similar rule
   with the top most LHS function reversed. The syntax declaration also needs this attribute.
-  
+
 - LLDB can now be used for debugging the llvm-backend on OSX.
 
 - The `kast` tool now allows access to the rule grammar by providing `--input rule`.
 
 - Added more claims filtering options for `kprove`: `--trusted`, `--exclude` and `--claims`.
 
-- Various improvements to error messages and made it easier to debug and profile a definition. 
+- Various improvements to error messages and made it easier to debug and profile a definition.
 
 Performance Improvements
 ------------------------
@@ -348,7 +348,7 @@ Documentation
 
 - Lessons Basic 2-21 of the new K tutorial have been written.
 
-- The option `--help-experimental` or `-X` is removed from all tools, and 
+- The option `--help-experimental` or `-X` is removed from all tools, and
   all the `--help` option lists are flattened.
 
 - Rename `pending-documentation.md` into `USER_MANUAL.md`
@@ -399,7 +399,7 @@ Dependency Updates
 ------------------
 
 - Haskell backend is updated to version [82b8a19](https://github.com/kframework/kore/commit/82b8a19bfc3fb7d9f3ca3f3e715ec7ae08b70a99).
-  
+
 - LLVM backend is updated to version [572cf69](https://github.com/kframework/llvm-backend/commit/572cf698be6baef5cdd01aa9239e32e9be89ec6a).
 
 - K Web Theme is updated to version [b458d14](https://github.com/runtimeverification/k-web-theme/commit/b458d1461c31760024ea06e0e50f25806ace5e2c).

README.md

@@ -319,7 +319,7 @@ nix build .
 This will build all of K and put a link to the resulting binaries in the `result/` folder.
 
 
-_Note: Mac users, especially those running M1/M2 Macs may find nix segfaulting on occasion. If this happens, try running the nix command like this: `GC_DONT_GC=1 nix build .`_ 
+_Note: Mac users, especially those running M1/M2 Macs may find nix segfaulting on occasion. If this happens, try running the nix command like this: `GC_DONT_GC=1 nix build .`_
 
 
 If you want to temporarily add the K binaries (such as `kompile` or `kast`) to the current shell, run
@@ -334,7 +334,7 @@ To run the integration tests:
 nix build .#test
 ```
 
-If you change any `pom.xml`, you must run 
+If you change any `pom.xml`, you must run
 
 ```
 nix run .#update-maven
@@ -425,7 +425,7 @@ Common build-time error messages:
         ```
 
         copy the `got:` hash (`sha256-fFlRqlLDZnVuoJniPvXjqdYEjnKxmFCEniavau/1gcQ=`) and replace it in `flake.nix`:
-        
+
         ```nix
         k-framework = { haskell-backend-bins, llvm-kompile-libs }:
             prev.callPackage ./nix/k.nix {

docs/developers/sort_inference.md

@@ -27,7 +27,7 @@ which is additionally subject to a *polarity* restriction. Informally, for a typ
 - *positive*, if `𝜏` describes a value produced by a term with type `T`
 
 As a concrete example, in a type like `(𝜏0 → 𝜏1) → 𝜏2`,
-- `𝜏2` is positive, as the term produces the value of type `𝜏2` as an output 
+- `𝜏2` is positive, as the term produces the value of type `𝜏2` as an output
 - `𝜏0 → 𝜏1` is negative, as the value of this type is given as an input to the term
 - `𝜏1` is negative, as the value of this type is also given as an input to the term (indirectly via the input function `𝜏0 → 𝜏1`)
 - `𝜏0` is positive, as the term itself must produce this value in order to call the input function `𝜏0 → 𝜏1`
@@ -50,8 +50,8 @@ Informally then, the polarity restriction enforces that type intersections can o
 - `𝜏 <: 𝜏1 and 𝜏 <: 𝜏2 iff 𝜏 <: 𝜏1 ⊓ 𝜏2`
 - `𝜏1 <: 𝜏 and 𝜏2 <: 𝜏 iff 𝜏1 ⊔ 𝜏2 <: 𝜏`
 
-In total then, any type variable with bounds `L <: 𝛼 <: U` can be encoded as a set-theoretic type by 
-- replacing every negative instance of `𝛼` with `𝛼 ⊓ U` 
+In total then, any type variable with bounds `L <: 𝛼 <: U` can be encoded as a set-theoretic type by
+- replacing every negative instance of `𝛼` with `𝛼 ⊓ U`
 - replacing every positive instance of `𝛼` with `𝛼 ⊔ L`
 
 Conversely, any set-theoretic type subject to the polarity restriction can be converted back to type variables with bounds by iteratively applying this process in reverse, i.e.,
@@ -62,7 +62,7 @@ For example, consider a term like
 ```
 𝜆𝑥 . { L = 𝑥 − 1 ; R = if 𝑥 < 0 then 0 else 𝑥 }
  ```
-where `nat <: int`, `- : int → int → int`, and `0 : nat`. 
+where `nat <: int`, `- : int → int → int`, and `0 : nat`.
 
 Prior to some simplification passes, SimpleSub will infer the type
 ```
@@ -145,7 +145,7 @@ case class CompactType(vars: Set[TypeVariable],
 ```
 The implementation of the compact function is straightforward and omitted here.
 
-We then perform two simplifications on these `CompactTypes` to remove unnecessary parametricity. We say that two type variables *co-occur* if they appear in the same union or intersection. The two simplifications are then as follows: 
+We then perform two simplifications on these `CompactTypes` to remove unnecessary parametricity. We say that two type variables *co-occur* if they appear in the same union or intersection. The two simplifications are then as follows:
 
 - If a type variable `𝛼` always co-occurs positively with some other type variable `β` and vice-versa, then  `𝛼` and `β` can be unified. The same applies for negative occurrences. For example, the obvious type for an `if-then-else` function `bool → 𝛼 → β → 𝛼 ⊔ β` is in fact equivalent to `bool → 𝛼 → 𝛼 → 𝛼`.
 
@@ -169,14 +169,14 @@ where
 ```
 prId : S1 → ... → SK → S
 ```
-is taken as a built-in in the SimpleSub language. 
+is taken as a built-in in the SimpleSub language.
 
 Then, given `t` any `Term` containing variables `x1, ..., xN`, define the translation
 ```
 translate(t) = 𝜆x1. ... 𝜆xN. translateBody(t)
 ```
 
-When we perform type inference on `translate(t)`, we will obtain a function type of the form `T1 → ... → TN → T`. This tells us that `x1 : T1`, ..., `xN : TN`, and, `term : T`, exactly as needed for sort inference! 
+When we perform type inference on `translate(t)`, we will obtain a function type of the form `T1 → ... → TN → T`. This tells us that `x1 : T1`, ..., `xN : TN`, and, `term : T`, exactly as needed for sort inference!
 
 There are a few final caveats, which can be easily addressed:
 - In K, we do not actually have a complete type lattice, and the intersections and unions of sorts may not actually exist. If we produce a type with such non-existent sorts, it is simply a type error.
@@ -205,12 +205,12 @@ When we perform inference on `translateSlice(t)`, the resulting type will have t
 ```
 Here, each `Ai` indicates the expected type of the `Ambiguity` associated to the identifier `ambi`.
 
-If an ambiguity's child does not itself contain ambiguities (as will always be true far enough down in the parse tree), we can "fold" that particular child into the type of the parent slice by simple function application, corresponding to choosing that child of the ambiguity for our final parse. 
+If an ambiguity's child does not itself contain ambiguities (as will always be true far enough down in the parse tree), we can "fold" that particular child into the type of the parent slice by simple function application, corresponding to choosing that child of the ambiguity for our final parse.
 
 Specifically, let `t` be the term as above and `c` its child slice. We can infer the type of the function application `translateSlice(t) translateSlice(c)` and will be left with either a type error or a type of the form
 ```
 (A21 → ... → A2N → A1)  → ... → (AK1 → ... → AKN → AK) → T1' → ... → TN' → T'`.
 ```
-which is the specialization of `translateSlice(t)`'s type when picking `c` as the value of the ambiguity. 
+which is the specialization of `translateSlice(t)`'s type when picking `c` as the value of the ambiguity.
 
 We can use this process to then iteratively collapse the tree of slices along all possible paths, starting from the leaves upward. Those paths that encounter type errors during substitution are pruned, while the others are collected into a set of all possible parses along with their inferred types. Unfortunately, this is `O(2^N)` in the worst case, but the hope is that the actual factors involved will be small.

k-distribution/include/kframework/builtin/ffi.md

@@ -25,7 +25,7 @@ module FFI-SYNTAX
 ```
 
 The FFIType sort is used to declare the native C ABI types of operands passed
-to the `#ffiCall` function. These types roughly correspond to the types 
+to the `#ffiCall` function. These types roughly correspond to the types
 declared in `ffi.h` by libffi.
 
 ```k
@@ -69,7 +69,7 @@ module FFI
 FFI Calls
 ---------
 
-The `#ffiCall` functions are designed to call a native C ABI function and 
+The `#ffiCall` functions are designed to call a native C ABI function and
 return a native result. They come in three variants:
 
 ### Non-variadic
@@ -78,7 +78,7 @@ In the first variant, `#ffiCall(Address, Args, ArgTypes, ReturnType)` takes
 an integer address of a function (which can be obtained from
 `#functionAddress`), a `List` of `Bytes` containing the arguments of the
 function, a `List` of `FFIType`s containing the types of the parameters of the
-function, and an `FFIType` containing the return type of the function, and 
+function, and an `FFIType` containing the return type of the function, and
 returns the return value of the function as a `Bytes`.
 
 ```k
@@ -138,15 +138,15 @@ a particular term does not have a fixed address across its entire lifetime
 in most cases. Sometimes this is undesirable, especially if you intend for
 the address of the memory to be taken by the semantics or if you intend
 to pass this memory directly to native code. As a result, the FFI module
-exposes the following unsafe APIs for memory management. Note that use of 
+exposes the following unsafe APIs for memory management. Note that use of
 these APIs leaves the burden of memory management completely on the user,
-and thus misuse of these functions can lead to things like use-after-free 
+and thus misuse of these functions can lead to things like use-after-free
 and other memory corruption bugs.
 
 ### Allocation
 
 `#alloc(Key, Size, Align)` will allocate `Size` bytes with an alignment
-requirement of `Align` (which must be a power of two), and return it as a 
+requirement of `Align` (which must be a power of two), and return it as a
 `Bytes` term. The memory is uniquely identified by its key and that key will
 be used later to free the memory. The memory is not implicitly freed by garbage
 collection; failure to call `#free` on the memory at a later date can lead to

k-distribution/include/kframework/builtin/kast.md

@@ -445,7 +445,7 @@ Additional Syntax for K Terms in Rules
 --------------------------------------
 
 Certain additional features are available when parsing the contents of rules
-and contexts. For more information on each of these, refer to K's 
+and contexts. For more information on each of these, refer to K's
 documentation.
 
 ```k
@@ -508,7 +508,7 @@ certain types of text, such as whitespace and comments. However, the specific
 syntax which each language must ignore is a little different from language
 to language, and thus you wish to specify it manually. You can do this by
 defining productions of the `#Layout` sort. For more information, refer to
-K's documentation. However, this module will be implicitly imported if no 
+K's documentation. However, this module will be implicitly imported if no
 productions are declared of sort `#Layout`. This module will also be used
 for the purposes of parsing K rules. If you wish to declare a language with
 no layout productions, simply create a sort declaration for the `#Layout` sort

k-distribution/include/kframework/builtin/rat.md

@@ -5,7 +5,7 @@ copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 Rational Numbers in K
 =====================
 
-K provides support for arbitrary-precision rational numbers represented as a 
+K provides support for arbitrary-precision rational numbers represented as a
 quotient between two integers. The sort representing these values is `Rat`.
 `Int` is a subsort of `Rat`, and it is guaranteed that any integer will be
 represented as an `Int` and can be matched as such on the left hand side

k-distribution/include/kframework/builtin/substitution.md

@@ -66,7 +66,7 @@ A production can be given the attribute `binder`. Such a production must have
 at least two nonterminals. The first nonterminal from left to right must be of
 sort `KVar`, and contains the bound variable. The last nonterminal from left
 to right contains the term that is bound. For example, I could describe lambdas
-in the lambda calculus with the production 
+in the lambda calculus with the production
 `syntax Val ::= "lambda" KVar "." Exp [binder]`.
 
 Substitution

k-distribution/include/kframework/html/k-definition.css

@@ -110,7 +110,7 @@ top : 3px;
 {
 color : black;
 border-width: 3px;
-display: inline-block; 
+display: inline-block;
 padding: 10px;
 padding-left: 20px;
 padding-right: 20px;
@@ -123,7 +123,7 @@ text-align: left;
 {
 color : black;
 border-width: 1px;
-display: inline-block; 
+display: inline-block;
 padding: 10px;
 padding-left: 20px;
 padding-right: 20px;
@@ -158,4 +158,3 @@ background-color: #f2f2f2;
 border-color: #000000;
 background-color: #e5e5e5;
 }
-

k-distribution/include/kframework/html/k-documentation.css

@@ -86,7 +86,7 @@ top : 3px;
 {
 color : black;
 border-width: 3px;
-display: inline-block; 
+display: inline-block;
 padding: 10px;
 padding-left: 20px;
 padding-right: 20px;
@@ -99,7 +99,7 @@ text-align: left;
 {
 /*color : black;
 border-width: 1px;
-display: inline-block; 
+display: inline-block;
 padding: 10px;
 padding-left: 20px;
 padding-right: 20px;