Remove structural attribute (#3592)

More work for #3481

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

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

@@ -981,7 +981,7 @@ rectangle,rectangle
 }{}
 \lstdefinelanguage{k}{
 		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, structural, transition, superheat, supercool, search, rewrite, prec, gather, stream, multiplicity, when},
+       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},
        emphstyle={[3]\textit},
        literate=

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

@@ -2,7 +2,7 @@
 copyright: Copyright (c) K Team. All Rights Reserved.
 ---
 
-In more recent definitions, we prefer to make some `[structural]` rules
-`[macro]` rules.  Macros apply statically, before the program is executed,
-thus increasing the execution performance.  The `let` and `letrec` constructs
+In more recent definitions, we prefer to make some `[macro]` rules.
+Macros apply statically, before the program is executed, thus
+increasing the execution performance.  The `let` and `letrec` constructs
 here could be made into `[macro]`.

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

@@ -21,17 +21,6 @@ is nothing but syntactic sugar for
 
 This can be easily achieved with a rule, as shown in `lambda.k`.
 
-As a side point, which is not very relevant here but good to know, we may
-want the *desugaring* of `let` to not even count as a computational step, but
-as a mere *structural rearrangement* of the program so that other semantic
-rules (beta reduction, in our case) can match and apply.
-
-The K tool allows us to tag rules with the attribute `structural`, with
-precisely the intuition above.  You can think of structural rules as a kind
-of light rules, almost like macros, or like ones which apply *under the hood*,
-instantaneously.  There are several other uses for structural rules in K,
-which we will discuss later in this tutorial.
-
 Compile `lambda.k` and write some programs using `let` binders.  
 
 For example, consider a `lets.lambda` program which takes `arithmetic.lambda`

k-distribution/pl-tutorial/1_k/2_imp/README.md

@@ -16,7 +16,6 @@ Specifically, you will learn the following:
 * The additional syntax of the K syntactic category.
 * How the strictness annotations are automatically desugared into rules.
 * The first steps of the configuration abstraction mechanism.
-* The distinction between structural and computational rules.
 
 Like in the previous tutorial, this folder contains several lessons, each
 adding new features to IMP.  Do them in order.  Also, make sure you completed

k-distribution/pl-tutorial/1_k/2_imp/lesson_4/README.md

@@ -5,8 +5,7 @@ copyright: Copyright (c) K Team. All Rights Reserved.
 # Configuration Abstraction, Part 1; Types of Rules
 
 Here we will complete the K definition of IMP and, while doing so, we will
-learn the very first step of what we call _configuration abstraction_, and
-the semantic distinction between structural and computational rules.
+learn the very first step of what we call _configuration abstraction_.
 
 ## The IMP Semantic Rules
 
@@ -105,34 +104,6 @@ If you really want certain rewrites over syntactic terms to apply
 anywhere they match, then you should tag the rule with the attribute
 `anywhere`, which was discussed in Tutorial 1, Lesson 2.5.
 
-## Structural vs. Computational Rules
-
-The K rules are of two types: structural and computational. Intuitively,
-structural rules rearrange the configuration so that computational rules can
-apply. Structural rules therefore do not count as computational steps. A K
-semantics can be thought of as a generator of transition systems, one for each
-program. It is only the computational rules that create steps, or transitions,
-in the corresponding transition system, the structural rules being unobservable
-at this level. By default, rules are all assumed computational, except for
-the implicit heating/cooling rules that define evaluation strategies of
-language constructs, which are assumed structural. If you want to explicitly
-make a rule structural, then you should include the tag (or attribute)
-`structural` in square brackets right after the rule. These attributes may be
-taken into account by different K tools, so it is highly recommended to spend
-a moment or two after each rule and think whether you want it to be structural
-or computational.
-
-Let us do it. We want the lookup and the arithmetic and Boolean construct
-rules to be computational, because they make computational progress whenever
-they apply. However, the block rules can be very well structural, because
-we can regard them simply as syntactic grouping constructs. In general,
-we want to have as few computational rules as possible, because we want
-the resulting transition systems to be smaller for analysis purposes, but not
-too few to lose behaviors. For example, making the block rules structural
-loses no meaningful behaviors. Similarly, the sequential composition,
-the while loop unrolling, and the no-variable declaration rules can all
-safely be structural.
-
 Kompile and then krun the programs that you only parsed in Lesson 1. They
 should all execute as expected. The state cell shows the final state
 of the program. The `k` cell shows the final code contents, which should be

k-distribution/pl-tutorial/1_k/2_imp/lesson_4/imp.k

@@ -46,18 +46,18 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 // Stmt
   rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
   rule if (true)  S else _ => S
   rule if (false) _ else S => S
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 // Pgm
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
 // verification ids
   syntax Id ::= "n"     [token]

k-distribution/pl-tutorial/1_k/2_imp/lesson_5/imp.md

@@ -153,15 +153,10 @@ unit of the computation list structure `K`, that is, the empty task.
 Similarly, the non-empty blocks are dissolved and replaced by their statement
 contents, thus effectively giving them a bracket semantics; we can afford to
 do this only because we have no block-local variable declarations yet in IMP.
-Since we tagged the rules below as *structural*, the **K** tool structurally
-erases the block constructs from the computation structure, without
-considering their erasure as computational steps in the resulting transition
-systems.  You can make these rules computational (dropping the attribute
-`structural`) if you do want these to count as computational steps.
 
 ```k
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 ```
 
 ### Assignment
@@ -175,17 +170,10 @@ the assignment is dissolved.
 
 ### Sequential composition
 Sequential composition is simply structurally translated into **K**'s
-builtin task sequentialization operation.  You can make this rule
-computational (i.e., remove the `structural` attribute) if you
-want it to count as a computational step.  Recall that the semantics
-of a program in a programming language defined in **K** is the transition
-system obtained from the initial configuration holding that program
-and counting only the steps corresponding to computational rules as
-transitions (i.e., hiding the structural rules as unobservable, or
-internal steps).
+builtin task sequentialization operation.
 
 ```k
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 ```
 
 ### Conditional
@@ -202,10 +190,9 @@ argument is allowed to be evaluated.
 
 ### While loop
 We give the semantics of the `while` loop by unrolling.
-Note that we preferred to make the rule below structural.
 
 ```k
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 ```
 
 ### Programs
@@ -216,14 +203,11 @@ constructed with a head element followed by a tail list), we need to
 distinguish two cases, one when the list has at least one element and
 another when the list is empty.  In the first case we initialize the
 variable to 0 in the state, but only when the variable is not already
-declared (all variables are global and distinct in IMP).  We prefer to
-make the second rule structural, thinking of dissolving the residual
-empty `int;` declaration as a structural cleanup rather than as
-a computational step.
+declared (all variables are global and distinct in IMP).
 
 ```k
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 endmodule
 ```

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

@@ -111,9 +111,6 @@ When the item preceding the environment recovery task `Rho` in the
 computation becomes a value, replace the current environment with `Rho`
 and dissolve `Rho` from the computation.
 
-Before we kompile, let us make this rule and the lambda evaluation rule
-structural, because we do not want these to count as transitions.
-
 Let us kompile and ... fail:
 
     kompile lambda

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

@@ -19,7 +19,6 @@ module LAMBDA
 
   rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
        <env> Rho </env>
-    [structural]
   rule <k> closure(Rho,X,E) V:Val => E ~> Rho' ...</k>
        <env> Rho' => Rho[X <- !N] </env>
        <store>... .Map => (!N:Int |-> V) ...</store>
@@ -29,5 +28,4 @@ module LAMBDA
 
 // Auxiliary task
   rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
-    [structural]
 endmodule

k-distribution/pl-tutorial/1_k/3_lambda++/lesson_3/lambda.k

@@ -19,15 +19,13 @@ module LAMBDA
 
   rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
        <env> Rho </env>
-    [structural]
   rule <k> closure(Rho,X,E) V:Val => E ~> Rho' ...</k>
        <env> Rho' => Rho[X <- !N] </env>
        <store>... .Map => (!N:Int |-> V) ...</store>
   rule <k> X => V ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> V ...</store>
   rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
-    [structural]
 
   syntax Val ::= Int | Bool
   syntax Exp ::= Exp "*" Exp          [strict, left]

k-distribution/pl-tutorial/1_k/3_lambda++/lesson_4/lambda.k

@@ -19,15 +19,13 @@ module LAMBDA
 
   rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
        <env> Rho </env>
-    [structural]
   rule <k> closure(Rho,X,E) V:Val => E ~> Rho' ...</k>
        <env> Rho' => Rho[X <- !N] </env>
        <store>... .Map => (!N:Int |-> V) ...</store>
   rule <k> X => V ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> V ...</store>
   rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
-    [structural]
 
   syntax Val ::= Int | Bool
   syntax Exp ::= Exp "*" Exp          [strict, left]

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

@@ -46,7 +46,6 @@ the closure itself:
     rule <k> mu X . E => muclosure(Rho[X <- !N], E) ...</k>
          <env> Rho </env>
          <store>... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ...</store>
-      [structural]
 
 Since each time `mu X . E` is encountered during the evaluation it needs to
 evaluate `E`, we conclude that `muclosure` cannot be a value.  We can declare

k-distribution/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k

@@ -20,15 +20,13 @@ module LAMBDA
 
   rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
        <env> Rho </env>
-    [structural]
   rule <k> closure(Rho,X,E) V:Val => E ~> Rho' ...</k>
        <env> Rho' => Rho[X <- !N] </env>
        <store>... .Map => (!N:Int |-> V) ...</store>
   rule <k> X => V ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> V ...</store>
   rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
-    [structural]
 
   syntax Val ::= Int | Bool
   syntax Exp ::= Exp "*" Exp          [strict, left]
@@ -55,7 +53,6 @@ module LAMBDA
   rule <k> mu X . E => muclosure(Rho[X <- !N], E) ...</k>
        <env> Rho </env>
        <store>... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ...</store>
-    [structural]
   rule <k> muclosure(Rho,E) => E ~> Rho' ...</k>
        <env> Rho' => Rho </env>
 

k-distribution/pl-tutorial/1_k/3_lambda++/lesson_6/lambda.md

@@ -112,7 +112,6 @@ then switch back to caller's environment.
 
   rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
        <env> Rho </env>
-    [structural]
   rule <k> closure(Rho,X,E) V:Val => E ~> Rho' ...</k>
        <env> Rho' => Rho[X <- !N] </env>
        <store>... .Map => (!N:Int |-> V) ...</store>
@@ -128,7 +127,6 @@ in the **K** team to add it to the set of pre-defined **K** features.
 
 ```k
   rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
-    [structural]
 ```
 
 ### Arithmetic Constructs
@@ -182,7 +180,6 @@ back to the fixed-point.
   rule <k> mu X . E => muclosure(Rho[X <- !N], E) ...</k>
        <env> Rho </env>
        <store>... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ...</store>
-    [structural]
   rule <k> muclosure(Rho,E) => E ~> Rho' ...</k>
        <env> Rho' => Rho </env>
 ```

k-distribution/pl-tutorial/1_k/4_imp++/lesson_1/imp.k

@@ -55,17 +55,17 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 // Stmt
   rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
   rule if (true)  S else _ => S
   rule if (false) _ else S => S
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
   rule <k> int (X,Xs => Xs); ...</k>
        <state> Rho (.Map => X |-> 0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; => .  [structural]
+  rule int .Ids; => .
 endmodule

k-distribution/pl-tutorial/1_k/4_imp++/lesson_2/imp.k

@@ -57,19 +57,19 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 // Stmt
   rule <k> X = I:Int; => . ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
   rule if (true)  S else _ => S
   rule if (false) _ else S => S
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .  [structural]
+  rule int .Ids; => .
 endmodule

k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/README.md

@@ -67,13 +67,12 @@ therefore allows you to finely tune the generated language models using the
 
 To state which constructs are to be considered to generate transitions in the
 generated language model, and for other reasons, too, the K tool allows you to
-tag any production and any rule. You can do this the same way we tagged
-rules with the `structural` keyword in earlier tutorials: put the tag in
-brackets. You can associate multiple tags to the same construct or rule, and
-more than one construct or rule can have the same tag. As an example, let us
-tag the division construct with `division`, the lookup rule with `lookup` and
-the increment rule with `increment`. The tags of the rules are not needed
-in this lesson, we do it only to demonstrate that rules can also be tagged.
+tag any production and any rule by putting the tag in brackets. You can associate
+ multiple tags to the same construct or rule, and more than one construct or
+rule can have the same tag. As an example, let us tag the division construct
+with `division`, the lookup rule with `lookup` and the increment rule with
+`increment`. The tags of the rules are not needed in this lesson, we do it only
+to demonstrate that rules can also be tagged.
 
 The least intrusive way to enforce our current language to explore the
 entire space of behaviors due to the strictness of division is to `kompile` it

k-distribution/pl-tutorial/1_k/4_imp++/lesson_3/imp.k

@@ -60,19 +60,19 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 // Stmt
   rule <k> X = I:Int; => . ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
   rule if (true)  S else _ => S
   rule if (false) _ else S => S
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .  [structural]
+  rule int .Ids; => .
 endmodule