Merge remote-tracking branch 'origin/develop'

CHANGELOG.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 K Framework 6.1.0

CONTRIBUTING.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 # K Framework Contributor Guide

README.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 permalink: README.html
 ---
 

docs/ktools.md

@@ -383,4 +383,3 @@ with the kserver active it takes 2m. You can start the kserver in two ways.
 
 Because we reuse caches, you should stop and restart the server between runs.
 The Nailgun implementation hasn't been updated in the last 3-5 years, and it's not compatible with Java 18 onwards.
-

k-distribution/INSTALL.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 Installing the K Framework
 ==========================

k-distribution/include/kframework/README.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 K Builtins

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 Basic Builtin Types in K

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 K Foreign Function Interface

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 Syntax of JSON

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 K Language Features

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 K Prelude

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 Rational Numbers in K

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

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 Capture-Aware Substitution in K

k-distribution/include/kframework/builtin/unification.k

@@ -1,4 +1,4 @@
-// Copyright (c) K Team. All Rights Reserved.
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 require "domains.md"
 module UNIFICATION
   imports SET

k-distribution/include/kframework/documentation.k

@@ -1,4 +1,4 @@
-// Copyright (c) K Team. All Rights Reserved.
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module DOCUMENTATION
     configuration <k> $PGM:K </k>
 endmodule

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

@@ -1,4 +1,4 @@
-/* Copyright (c) K Team. All Rights Reserved. */
+/* Copyright (c) Runtime Verification, Inc. All Rights Reserved. */
 .bold
 {
 font-weight: bold;
@@ -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

@@ -1,4 +1,4 @@
-/* Copyright (c) K Team. All Rights Reserved. */
+/* Copyright (c) Runtime Verification, Inc. All Rights Reserved. */
 .bold
 {
 font-weight: bold;
@@ -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;

k-distribution/include/kframework/latex/k.sty

@@ -1,4 +1,4 @@
-% Copyright (c) K Team. All Rights Reserved.
+% Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 \NeedsTeXFormat{LaTeX2e}
 \ProvidesPackage{k}[2012/02/14 Package for typesetting K Framework definitions http://k-framework.org]
 
@@ -9,7 +9,7 @@
 % \RequirePackage{etextools} % for xifstrequal
 % \RequirePackage{stringstrings} % for \stringlength
 
-\SetupKeyvalOptions{family=k,prefix=k@} 
+\SetupKeyvalOptions{family=k,prefix=k@}
 
 
 \DeclareStringOption[bubble]{style}  % the default style for cells & stuff
@@ -19,7 +19,7 @@
 \ProcessKeyvalOptions*
 
 % Usage Examples %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Next command uses the default style (bubble) with tight edges for cells. 
+% Next command uses the default style (bubble) with tight edges for cells.
 % \usepackage[tight]{k}
 %
 % Next command changes the default style to mathematic cells.
@@ -41,7 +41,7 @@
 % If the default was set to math, use bubble instead of math above.
 
 % Some exported commands (useful for manually writing K):
-% \kall, \kprefix, \ksuffix, and \kmiddle are used to specify cells which are 
+% \kall, \kprefix, \ksuffix, and \kmiddle are used to specify cells which are
 % either complete, open to the right, open to the left, and open both ways,
 % respectively .
 
@@ -89,7 +89,7 @@
 
 \RequirePackage[small,compact]{titlesec}
 %\titleformat{command}[shape]{format}{label}{sep}{before}[after]
-% shape ::= hang | block | display | runin | leftmargin | rightmargin 
+% shape ::= hang | block | display | runin | leftmargin | rightmargin
 %         | drop | wrap | frame
 % sep is mandatory to be a length.
 % more on http://www.ctex.org/documents/packages/layout/titlesec.pdf
@@ -745,7 +745,7 @@ $\mid\;{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]\;}%
                                         {\pgfpointanchor{current bounding box}{north east}}}
     \pgfextractx{\k@cellContentWidth}{\k@cellContentBBox}%
     \pgfextracty{\k@cellContentHeight}{\k@cellContentBBox}%
-    
+
     \begin{pgfonlayer}{background}
       \ifdraft{%
         \path (cell content.center)
@@ -826,7 +826,7 @@ rectangle,rectangle
                       \setlength{\k@ruptureStepSize}{\n3}%
                       \setlength{\k@ruptureStepSize}{.25\k@ruptureStepSize}%
                      }%
-                     
+
                     % Draw counter-clock-wise, starting from the
                     % lower right corner.
                     (cell body.south east)
@@ -849,7 +849,7 @@ rectangle,rectangle
                     % Bottom (just close the path)
                     -- cycle;
     \end{pgfonlayer}
-    
+
     % Add extra space above and below the cell.
     \path[use as bounding box] (current bounding box.south west) ++(0,-.3333em)
                                rectangle (current bounding box.north east) ++(0,.3333em);
@@ -918,12 +918,12 @@ rectangle,rectangle
 \newcommand{\ksentence}[7][]{%
   \par\indent
   \k@ruleLabel{#3}{#2}\hspace{1em}$%
-  \ifthenelse{\equal{#1}{}}{}{%  
-   \left(% 
+  \ifthenelse{\equal{#1}{}}{}{%
+   \left(%
   }%
   #4%
-  \ifthenelse{\equal{#1}{}}{}{%  
-   \right)% 
+  \ifthenelse{\equal{#1}{}}{}{%
+   \right)%
   }%
     $%
   \ifthenelse{\equal{#5}{}}{}{%
@@ -933,8 +933,8 @@ rectangle,rectangle
     \whenEns{#6}%
   }%
   \k@markPosition%
-  \ifthenelse{\equal{#7}{}}{}{%  
-   \ruleAttributes{#7}% 
+  \ifthenelse{\equal{#7}{}}{}{%
+   \ruleAttributes{#7}%
   }%
   \par\ \par
 }
@@ -974,39 +974,38 @@ rectangle,rectangle
                %frame=tb,
                columns=flexible,
                mathescape=false,
-			   upquote=true,
+               upquote=true,
 % 				literate=
 % 	   			{"}{\textquotedbl}1
        }
 }{}
 \lstdefinelanguage{k}{
-		upquote=true,
+       upquote=true,
        morekeywords={kompile, kast, krun, require, HOLE, configuration, module, end, imports, rule, macro, op, ops, syntax, sort, sorts, subsort, subsorts, context, HOLE, hybrid, strict, seqstrict, binder, color, latex, kvar, transition, superheat, supercool, search, rewrite, prec, gather, stream, multiplicity, when},
-        emph={[3]Map, Set, Bag, List, K, KLabel, KResult, KProper, CellLabel, SetItem, BagItem, ListItem, MapItem, Int, Bool, String, Id},
+       emph={[3]Map, Set, Bag, List, K, KLabel, KResult, KProper, CellLabel, SetItem, BagItem, ListItem, MapItem, Int, Bool, String, Id},
        emphstyle={[3]\textit},
        literate=
        {LT}{$<$}3
-       {LEQ}{$<=$}4 
-%       {.K}{$\kdot{\it K}$}2 
-%       {.List}{$\kdot{\it List}$}4 
+       {LEQ}{$<=$}4
+%       {.K}{$\kdot{\it K}$}2
+%       {.List}{$\kdot{\it List}$}4
        {PROMPT}{\$}1
        {...<}{${\ellipses}\langle$}2
-       {>}{$\rangle$}1 
+       {>}{$\rangle$}1
        {>...}{$\rangle{\ellipses}$}2
-       {+Int}{$+{\rm\scriptstyle Int}$}4 
-       {*Int}{$*{\rm\scriptstyle Int}$}4 
-       {/Int}{$/{\rm\scriptstyle Int}$}4 
-       {LeqInt}{${<}{=}{\rm\scriptstyle Int}$}9 
-       {!=Int}{${!}{=}{\rm\scriptstyle Int}$}5 
-       {==Bool}{${=}{=}{\rm\scriptstyle Bool}$}7 
-       {=/=Bool}{${=}{/}{=}{\rm\scriptstyle Bool}$}9 
-       {notBool}{${\tt not}{\rm\scriptstyle Bool}$}5 
-       {<}{$\langle$}1 
-       {_}{$\_$}1 {~}{$\_$}1 
-       {=>}{$\;=\!>$}5 
-       {->}{{$->$}}3 
-       {~>}{{$\sim\!\!>$}}3  
-       {|->}{$\;|-\!\!>$}5 
+       {+Int}{$+{\rm\scriptstyle Int}$}4
+       {*Int}{$*{\rm\scriptstyle Int}$}4
+       {/Int}{$/{\rm\scriptstyle Int}$}4
+       {LeqInt}{${<}{=}{\rm\scriptstyle Int}$}9
+       {!=Int}{${!}{=}{\rm\scriptstyle Int}$}5
+       {==Bool}{${=}{=}{\rm\scriptstyle Bool}$}7
+       {=/=Bool}{${=}{/}{=}{\rm\scriptstyle Bool}$}9
+       {notBool}{${\tt not}{\rm\scriptstyle Bool}$}5
+       {<}{$\langle$}1
+       {_}{$\_$}1 {~}{$\_$}1
+       {=>}{$\;=\!>$}5
+       {->}{{$->$}}3
+       {~>}{{$\sim\!\!>$}}3
+       {|->}{$\;|-\!\!>$}5
 }
 \newcommand{\ka}[1]{\mbox{\lstinline[language=k]{#1}}}
-

k-distribution/pl-tutorial/1_k/1_lambda/README.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 ## Part 1: Defining LAMBDA

k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/NOTES.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 We now support the following line to the syntax module:

k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/README.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 # Syntax Modules and Basic K Commands
@@ -112,4 +112,4 @@ This way, we obtain our first programming language defined using K.
 
 Go to [Lesson 2, LAMBDA: Module Importing, Rules, Variables](../lesson_2/README.md)
 
-[MOVIE (out of date) [4'07"]](https://youtu.be/y5Tf1EZVj8E)
+[MOVIE (out of date) [4'07"]](https://youtu.be/y5Tf1EZVj8E)

k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/lambda.k

@@ -1,4 +1,4 @@
-// Copyright (c) K Team. All Rights Reserved.
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX

k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/NOTES.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 This folder has been added after the original tutorial was made

k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/lambda.k

@@ -1,4 +1,4 @@
-// Copyright (c) K Team. All Rights Reserved.
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
 require "substitution.md"
 

k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/NOTES.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 Substitution has been reimplemented in the meanwhile, where the fresh

k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/README.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 # Module Importing, Rules, Variables

k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/lambda.k

@@ -1,4 +1,4 @@
-// Copyright (c) K Team. All Rights Reserved.
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
 require "substitution.md"
 

k-distribution/pl-tutorial/1_k/1_lambda/lesson_3/NOTES.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 When we say "previous lesson" we refer to lesson 2.  This will need to change

k-distribution/pl-tutorial/1_k/1_lambda/lesson_3/README.md

@@ -1,5 +1,5 @@
 ---
-copyright: Copyright (c) K Team. All Rights Reserved.
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 # Evaluation Strategies using Strictness
@@ -41,4 +41,4 @@ in order to write human readable and interesting programs.
 
 Go to [Lesson 4, LAMBDA: Generating Documentation; Latex Attributes](../lesson_4/README.md).
 
-[MOVIE (out of date) [2'20"]](https://youtu.be/aul1x6bd1YM)
+[MOVIE (out of date) [2'20"]](https://youtu.be/aul1x6bd1YM)