Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into _update-deps/runtim…
Browse files Browse the repository at this point in the history 
…everification/k
  • Loading branch information
devops committed Mar 13, 2024
2 parents f4dbb09 + 882841e commit dae7348
Show file tree
Hide file tree
Showing 32 changed files with 42 additions and 46 deletions.
2 changes: 2 additions & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
*-kompiled
*.depend
*kore-exec.tar.gz
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_4/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
imports ID-SYNTAX

syntax Val ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_5/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
imports ID-SYNTAX

syntax Val ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_6/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
imports ID-SYNTAX

syntax Val ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_7/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
imports ID-SYNTAX

syntax Val ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
Expand Down
4 changes: 2 additions & 2 deletions 1_k/1_lambda/lesson_8/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
imports ID-SYNTAX

syntax Val ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
Expand All @@ -23,7 +23,7 @@ module LAMBDA-SYNTAX
rule let X = E in E':Exp => (lambda X . E') E

syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
| "mu" Id "." Exp [latex(\mu{#1}.{#2})]
| "mu" Id "." Exp
rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E'
endmodule

Expand Down
4 changes: 2 additions & 2 deletions 1_k/1_lambda/lesson_9/lambda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ interleaved) order.
The initial syntax of our λ-calculus:
```k
syntax Val ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [left, strict]
| "(" Exp ")" [bracket]
Expand Down Expand Up @@ -123,7 +123,7 @@ and faster to execute.

```k
syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
| "mu" Id "." Exp [latex(\mu{#1}.{#2})]
| "mu" Id "." Exp
rule letrec F:Id X:Id = E in E' => let F = mu F . lambda X . E in E'
endmodule
```
Expand Down
2 changes: 1 addition & 1 deletion 1_k/2_imp/lesson_1/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module IMP-SYNTAX
| "(" AExp ")" [bracket]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/2_imp/lesson_2/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module IMP-SYNTAX
| "(" AExp ")" [bracket]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/2_imp/lesson_3/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module IMP-SYNTAX
| "(" AExp ")" [bracket]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/2_imp/lesson_4/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module IMP-SYNTAX
| "(" AExp ")" [bracket]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/2_imp/lesson_5/imp.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ argument, because we want to give it a short-circuit semantics.
| "(" AExp ")" [bracket]
> AExp "+" AExp [left, strict, color(pink)]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict, color(pink)]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1), color(pink)]
Expand Down
4 changes: 2 additions & 2 deletions 1_k/3_lambda++/lesson_1/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module LAMBDA-SYNTAX
imports KVAR-SYNTAX

syntax Val ::= KVar
| "lambda" KVar "." Exp [binder, latex(\lambda{#1}.{#2})]
| "lambda" KVar "." Exp [binder]
syntax Exp ::= Val
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
Expand All @@ -25,7 +25,7 @@ module LAMBDA-SYNTAX
rule let X = E in E':Exp => (lambda X . E') E

syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro]
| "mu" KVar "." Exp [binder, latex(\mu{#1}.{#2})]
| "mu" KVar "." Exp [binder]
rule letrec F:KVar X = E in E' => let F = mu F . lambda X . E in E'

syntax Exp ::= "callcc" Exp [strict]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/3_lambda++/lesson_2/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
module LAMBDA
imports DOMAINS
syntax Exp ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]

Expand Down
2 changes: 1 addition & 1 deletion 1_k/3_lambda++/lesson_3/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
module LAMBDA
imports DOMAINS
syntax Exp ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]

Expand Down
2 changes: 1 addition & 1 deletion 1_k/3_lambda++/lesson_4/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
module LAMBDA
imports DOMAINS
syntax Exp ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]

Expand Down
4 changes: 2 additions & 2 deletions 1_k/3_lambda++/lesson_5/lambda.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module LAMBDA
</T>

syntax Exp ::= Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]

Expand Down Expand Up @@ -46,7 +46,7 @@ module LAMBDA
rule let X = E in E':Exp => (lambda X . E') E

syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
| "mu" Id "." Exp [latex(\mu{#1}.{#2})]
| "mu" Id "." Exp
rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E'

syntax Exp ::= muclosure(Map,Exp)
Expand Down
7 changes: 2 additions & 5 deletions 1_k/3_lambda++/lesson_6/lambda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ We move all the LAMBDA++ syntax here.
syntax Exp ::= Val
// Basic lambda-calculus syntax
| Id
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
| "lambda" Id "." Exp
| Exp Exp [strict, left]
| "(" Exp ")" [bracket]
// Arithmetic
Expand All @@ -52,7 +52,7 @@ We move all the LAMBDA++ syntax here.
syntax Exp ::= "if" Exp "then" Exp "else" Exp [strict(1)] // Conditional
| "let" Id "=" Exp "in" Exp [macro] // Let binder
| "letrec" Id Id "=" Exp "in" Exp [macro] // Letrec
| "mu" Id "." Exp [latex(\mu{#1}.{#2})] // Mu
| "mu" Id "." Exp // Mu
| "callcc" Exp [strict] // Callcc
```

Expand Down Expand Up @@ -108,7 +108,6 @@ then switch back to caller's environment.

```k
syntax Val ::= closure(Map,Id,Exp)
[latex(\textsf{closure}_\lambda({#1},{#2},{#3}))]
rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
<env> Rho </env>
Expand Down Expand Up @@ -176,7 +175,6 @@ back to the fixed-point.

```k
syntax Exp ::= muclosure(Map,Exp)
[latex(\textsf{closure}_\mu({#1},{#2}))]
rule <k> mu X . E => muclosure(Rho[X <- !N], E) ...</k>
<env> Rho </env>
<store>... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ...</store>
Expand All @@ -192,7 +190,6 @@ supposed to be executed. Forget the environment, and you get a wrong

```k
syntax Val ::= cc(Map,K)
[latex(\textsf{closure}_{\texttt{callcc}}({#1},{#2}))]
rule <k> (callcc V:Val => V cc(Rho,K)) ~> K </k> <env> Rho </env>
rule <k> cc(Rho,K) V:Val ~> _ => V ~> K </k> <env> _ => Rho </env>
endmodule
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_1/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ module IMP-SYNTAX
> AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_2/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module IMP-SYNTAX
> AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_3/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module IMP-SYNTAX
> AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_4/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module IMP-SYNTAX
> AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_5/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module IMP-SYNTAX
> AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_6/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module IMP-SYNTAX
> AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_7/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ module IMP-SYNTAX
> "spawn" Block
> Id "=" AExp [strict(2)]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/4_imp++/lesson_8/imp.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ of statements surrounded by curly brackets.
> "spawn" Block
> Id "=" AExp [strict(2)]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| AExp "<=" AExp [seqstrict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict(1)]
Expand Down
2 changes: 1 addition & 1 deletion 1_k/5_types/lesson_1/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ module IMP-SYNTAX
> "spawn" Block [strict]
> Id "=" AExp [strict(2)]
syntax BExp ::= Bool
| AExp "<=" AExp [strict, latex({#1}\leq{#2})]
| AExp "<=" AExp [strict]
| "!" BExp [strict]
| "(" BExp ")" [bracket]
> BExp "&&" BExp [left, strict]
Expand Down
5 changes: 2 additions & 3 deletions 2_languages/1_simple/1_untyped/simple-untyped.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -438,7 +438,7 @@ not mention these: the configuration context of the rule is
automatically transformed to match the declared configuration
structure.
```k
syntax KItem ::= "undefined" [latex(\bot)]
syntax KItem ::= "undefined"
rule <k> var X:Id; => .K ...</k>
<env> Env => Env[X <- L] </env>
Expand Down Expand Up @@ -1147,8 +1147,7 @@ corresponding store lookup operation.
The following operation initializes a sequence of locations with the same
value:
```k
syntax Map ::= Int "..." Int "|->" K
[function, latex({#1}\ldots{#2}\mapsto{#3})]
syntax Map ::= Int "..." Int "|->" K [function]
rule N...M |-> _ => .Map requires N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
```
Expand Down
5 changes: 2 additions & 3 deletions 2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ location and then never allow that type to change. The typed
undefined values effectively assign both a type and an undefined value
to a location.
```k
syntax KItem ::= undefined(Type) [latex(\bot_{#1})]
syntax KItem ::= undefined(Type)
rule <k> T:Type X:Id; => .K ...</k>
<env> Env => Env[X <- L] </env>
Expand Down Expand Up @@ -578,8 +578,7 @@ Adds the corresponding depth to an array type
```
Sequences of locations.
```k
syntax Map ::= Int "..." Int "|->" K
[function, latex({#1}\ldots{#2}\mapsto{#3})]
syntax Map ::= Int "..." Int "|->" K [function]
rule N...M |-> _ => .Map requires N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
Expand Down
4 changes: 2 additions & 2 deletions 2_languages/2_kool/1_untyped/kool-untyped.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -381,7 +381,7 @@ object and method closures.
The semantics below are taken verbatim from the untyped SIMPLE
definition.
```k
syntax KItem ::= "undefined" [latex(\bot)]
syntax KItem ::= "undefined"
rule <k> var X:Id; => .K ...</k>
<env> Env => Env[X <- L] </env>
Expand Down Expand Up @@ -583,7 +583,7 @@ from SIMPLE unchanged.
syntax Map ::= Int "..." Int "|->" K
[function, latex({#1}\ldots{#2}\mapsto{#3})]
[function]
rule N...M |-> _ => .Map requires N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
```
Expand Down
5 changes: 2 additions & 3 deletions 2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ KOOL).
syntax KResult ::= Vals
syntax KItem ::= undefined(Type) [latex(\bot_{#1})]
syntax KItem ::= undefined(Type)
rule <k> T:Type X:Id; => .K ...</k>
<env> Env => Env[X <- L] </env>
Expand Down Expand Up @@ -402,8 +402,7 @@ KOOL).
rule T:Type<_,Vs:Vals> => T[]<Vs>
rule T:Type<.Vals> => T
syntax Map ::= Int "..." Int "|->" K
[function, latex({#1}\ldots{#2}\mapsto{#3})]
syntax Map ::= Int "..." Int "|->" K [function]
rule N...M |-> _ => .Map requires N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
Expand Down
2 changes: 1 addition & 1 deletion 2_languages/2_kool/2_typed/2_static/kool-typed-static.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -891,7 +891,7 @@ is co-variant in the codomain and contra-variant in the domain).
## Generic operations which could be part of the **K** framework

```k
syntax KItem ::= stuck(K) [latex(\framebox{${#1}$})]
syntax KItem ::= stuck(K)
syntax KItem ::= "discard"
rule _:KResult ~> discard => .K
Expand Down

0 comments on commit dae7348

Please sign in to comment.