Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove uses of latex attribute #18

Merged
merged 2 commits into from
Mar 13, 2024
Merged

Remove uses of latex attribute #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7283452
Remove uses of latex attribute
gtrepta Mar 12, 2024
b5d2d2f
Add couple things to .gitignore
gtrepta Mar 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading