Skip to content

Commit 882841e

Browse files
gtreptagtrepta
authored
Remove uses of latex attribute (#18)
* Remove uses of latex attribute * Add couple things to .gitignore
1 parent fa74d3c commit 882841e

File tree

32 files changed

+42
-46
lines changed

32 files changed

+42
-46
lines changed

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -1 +1,3 @@
11
*-kompiled
2+
*.depend
3+
*kore-exec.tar.gz

‎1_k/1_lambda/lesson_4/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
55
imports ID-SYNTAX
66

77
syntax Val ::= Id
8-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
8+
| "lambda" Id "." Exp
99
syntax Exp ::= Val
1010
| Exp Exp [strict, left]
1111
| "(" Exp ")" [bracket]

‎1_k/1_lambda/lesson_5/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
55
imports ID-SYNTAX
66

77
syntax Val ::= Id
8-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
8+
| "lambda" Id "." Exp
99
syntax Exp ::= Val
1010
| Exp Exp [strict, left]
1111
| "(" Exp ")" [bracket]

‎1_k/1_lambda/lesson_6/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
55
imports ID-SYNTAX
66

77
syntax Val ::= Id
8-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
8+
| "lambda" Id "." Exp
99
syntax Exp ::= Val
1010
| Exp Exp [strict, left]
1111
| "(" Exp ")" [bracket]

‎1_k/1_lambda/lesson_7/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
55
imports ID-SYNTAX
66

77
syntax Val ::= Id
8-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
8+
| "lambda" Id "." Exp
99
syntax Exp ::= Val
1010
| Exp Exp [strict, left]
1111
| "(" Exp ")" [bracket]

‎1_k/1_lambda/lesson_8/lambda.k

+2-2
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module LAMBDA-SYNTAX
55
imports ID-SYNTAX
66

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

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

‎1_k/1_lambda/lesson_9/lambda.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ interleaved) order.
7676
The initial syntax of our λ-calculus:
7777
```k
7878
syntax Val ::= Id
79-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
79+
| "lambda" Id "." Exp
8080
syntax Exp ::= Val
8181
| Exp Exp [left, strict]
8282
| "(" Exp ")" [bracket]
@@ -123,7 +123,7 @@ and faster to execute.
123123

124124
```k
125125
syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
126-
| "mu" Id "." Exp [latex(\mu{#1}.{#2})]
126+
| "mu" Id "." Exp
127127
rule letrec F:Id X:Id = E in E' => let F = mu F . lambda X . E in E'
128128
endmodule
129129
```

‎1_k/2_imp/lesson_1/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module IMP-SYNTAX
88
| "(" AExp ")" [bracket]
99
> AExp "+" AExp [left, strict]
1010
syntax BExp ::= Bool
11-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
11+
| AExp "<=" AExp [seqstrict]
1212
| "!" BExp [strict]
1313
| "(" BExp ")" [bracket]
1414
> BExp "&&" BExp [left, strict(1)]

‎1_k/2_imp/lesson_2/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module IMP-SYNTAX
88
| "(" AExp ")" [bracket]
99
> AExp "+" AExp [left, strict]
1010
syntax BExp ::= Bool
11-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
11+
| AExp "<=" AExp [seqstrict]
1212
| "!" BExp [strict]
1313
| "(" BExp ")" [bracket]
1414
> BExp "&&" BExp [left, strict(1)]

‎1_k/2_imp/lesson_3/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module IMP-SYNTAX
88
| "(" AExp ")" [bracket]
99
> AExp "+" AExp [left, strict]
1010
syntax BExp ::= Bool
11-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
11+
| AExp "<=" AExp [seqstrict]
1212
| "!" BExp [strict]
1313
| "(" BExp ")" [bracket]
1414
> BExp "&&" BExp [left, strict(1)]

‎1_k/2_imp/lesson_4/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module IMP-SYNTAX
88
| "(" AExp ")" [bracket]
99
> AExp "+" AExp [left, strict]
1010
syntax BExp ::= Bool
11-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
11+
| AExp "<=" AExp [seqstrict]
1212
| "!" BExp [strict]
1313
| "(" BExp ")" [bracket]
1414
> BExp "&&" BExp [left, strict(1)]

‎1_k/2_imp/lesson_5/imp.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ argument, because we want to give it a short-circuit semantics.
3333
| "(" AExp ")" [bracket]
3434
> AExp "+" AExp [left, strict, color(pink)]
3535
syntax BExp ::= Bool
36-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)]
36+
| AExp "<=" AExp [seqstrict]
3737
| "!" BExp [strict, color(pink)]
3838
| "(" BExp ")" [bracket]
3939
> BExp "&&" BExp [left, strict(1), color(pink)]

‎1_k/3_lambda++/lesson_1/lambda.k

+2-2
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ module LAMBDA-SYNTAX
77
imports KVAR-SYNTAX
88

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

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

3131
syntax Exp ::= "callcc" Exp [strict]

‎1_k/3_lambda++/lesson_2/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
module LAMBDA
44
imports DOMAINS
55
syntax Exp ::= Id
6-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
6+
| "lambda" Id "." Exp
77
| Exp Exp [strict, left]
88
| "(" Exp ")" [bracket]
99

‎1_k/3_lambda++/lesson_3/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
module LAMBDA
44
imports DOMAINS
55
syntax Exp ::= Id
6-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
6+
| "lambda" Id "." Exp
77
| Exp Exp [strict, left]
88
| "(" Exp ")" [bracket]
99

‎1_k/3_lambda++/lesson_4/lambda.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
module LAMBDA
44
imports DOMAINS
55
syntax Exp ::= Id
6-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
6+
| "lambda" Id "." Exp
77
| Exp Exp [strict, left]
88
| "(" Exp ")" [bracket]
99

‎1_k/3_lambda++/lesson_5/lambda.k

+2-2
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module LAMBDA
1010
</T>
1111

1212
syntax Exp ::= Id
13-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
13+
| "lambda" Id "." Exp
1414
| Exp Exp [strict, left]
1515
| "(" Exp ")" [bracket]
1616

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

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

5252
syntax Exp ::= muclosure(Map,Exp)

‎1_k/3_lambda++/lesson_6/lambda.md

+2-5
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ We move all the LAMBDA++ syntax here.
3939
syntax Exp ::= Val
4040
// Basic lambda-calculus syntax
4141
| Id
42-
| "lambda" Id "." Exp [latex(\lambda{#1}.{#2})]
42+
| "lambda" Id "." Exp
4343
| Exp Exp [strict, left]
4444
| "(" Exp ")" [bracket]
4545
// Arithmetic
@@ -52,7 +52,7 @@ We move all the LAMBDA++ syntax here.
5252
syntax Exp ::= "if" Exp "then" Exp "else" Exp [strict(1)] // Conditional
5353
| "let" Id "=" Exp "in" Exp [macro] // Let binder
5454
| "letrec" Id Id "=" Exp "in" Exp [macro] // Letrec
55-
| "mu" Id "." Exp [latex(\mu{#1}.{#2})] // Mu
55+
| "mu" Id "." Exp // Mu
5656
| "callcc" Exp [strict] // Callcc
5757
```
5858

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

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

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

193191
```k
194192
syntax Val ::= cc(Map,K)
195-
[latex(\textsf{closure}_{\texttt{callcc}}({#1},{#2}))]
196193
rule <k> (callcc V:Val => V cc(Rho,K)) ~> K </k> <env> Rho </env>
197194
rule <k> cc(Rho,K) V:Val ~> _ => V ~> K </k> <env> _ => Rho </env>
198195
endmodule

‎1_k/4_imp++/lesson_1/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module IMP-SYNTAX
1111
> AExp "/" AExp [left, strict]
1212
> AExp "+" AExp [left, strict]
1313
syntax BExp ::= Bool
14-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
14+
| AExp "<=" AExp [seqstrict]
1515
| "!" BExp [strict]
1616
| "(" BExp ")" [bracket]
1717
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_2/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module IMP-SYNTAX
1010
> AExp "/" AExp [left, strict]
1111
> AExp "+" AExp [left, strict]
1212
syntax BExp ::= Bool
13-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
13+
| AExp "<=" AExp [seqstrict]
1414
| "!" BExp [strict]
1515
| "(" BExp ")" [bracket]
1616
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_3/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module IMP-SYNTAX
1010
> AExp "/" AExp [left, strict]
1111
> AExp "+" AExp [left, strict]
1212
syntax BExp ::= Bool
13-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
13+
| AExp "<=" AExp [seqstrict]
1414
| "!" BExp [strict]
1515
| "(" BExp ")" [bracket]
1616
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_4/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module IMP-SYNTAX
1010
> AExp "/" AExp [left, strict]
1111
> AExp "+" AExp [left, strict]
1212
syntax BExp ::= Bool
13-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
13+
| AExp "<=" AExp [seqstrict]
1414
| "!" BExp [strict]
1515
| "(" BExp ")" [bracket]
1616
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_5/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ module IMP-SYNTAX
99
> AExp "/" AExp [left, strict]
1010
> AExp "+" AExp [left, strict]
1111
syntax BExp ::= Bool
12-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
12+
| AExp "<=" AExp [seqstrict]
1313
| "!" BExp [strict]
1414
| "(" BExp ")" [bracket]
1515
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_6/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module IMP-SYNTAX
1010
> AExp "/" AExp [left, strict]
1111
> AExp "+" AExp [left, strict]
1212
syntax BExp ::= Bool
13-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
13+
| AExp "<=" AExp [seqstrict]
1414
| "!" BExp [strict]
1515
| "(" BExp ")" [bracket]
1616
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_7/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ module IMP-SYNTAX
1212
> "spawn" Block
1313
> Id "=" AExp [strict(2)]
1414
syntax BExp ::= Bool
15-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
15+
| AExp "<=" AExp [seqstrict]
1616
| "!" BExp [strict]
1717
| "(" BExp ")" [bracket]
1818
> BExp "&&" BExp [left, strict(1)]

‎1_k/4_imp++/lesson_8/imp.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ of statements surrounded by curly brackets.
129129
> "spawn" Block
130130
> Id "=" AExp [strict(2)]
131131
syntax BExp ::= Bool
132-
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
132+
| AExp "<=" AExp [seqstrict]
133133
| "!" BExp [strict]
134134
| "(" BExp ")" [bracket]
135135
> BExp "&&" BExp [left, strict(1)]

‎1_k/5_types/lesson_1/imp.k

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ module IMP-SYNTAX
1212
> "spawn" Block [strict]
1313
> Id "=" AExp [strict(2)]
1414
syntax BExp ::= Bool
15-
| AExp "<=" AExp [strict, latex({#1}\leq{#2})]
15+
| AExp "<=" AExp [strict]
1616
| "!" BExp [strict]
1717
| "(" BExp ")" [bracket]
1818
> BExp "&&" BExp [left, strict]

‎2_languages/1_simple/1_untyped/simple-untyped.md

+2-3
Original file line numberDiff line numberDiff line change
@@ -438,7 +438,7 @@ not mention these: the configuration context of the rule is
438438
automatically transformed to match the declared configuration
439439
structure.
440440
```k
441-
syntax KItem ::= "undefined" [latex(\bot)]
441+
syntax KItem ::= "undefined"
442442
443443
rule <k> var X:Id; => .K ...</k>
444444
<env> Env => Env[X <- L] </env>
@@ -1147,8 +1147,7 @@ corresponding store lookup operation.
11471147
The following operation initializes a sequence of locations with the same
11481148
value:
11491149
```k
1150-
syntax Map ::= Int "..." Int "|->" K
1151-
[function, latex({#1}\ldots{#2}\mapsto{#3})]
1150+
syntax Map ::= Int "..." Int "|->" K [function]
11521151
rule N...M |-> _ => .Map requires N >Int M
11531152
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
11541153
```

‎2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md

+2-3
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,7 @@ location and then never allow that type to change. The typed
222222
undefined values effectively assign both a type and an undefined value
223223
to a location.
224224
```k
225-
syntax KItem ::= undefined(Type) [latex(\bot_{#1})]
225+
syntax KItem ::= undefined(Type)
226226
227227
rule <k> T:Type X:Id; => .K ...</k>
228228
<env> Env => Env[X <- L] </env>
@@ -578,8 +578,7 @@ Adds the corresponding depth to an array type
578578
```
579579
Sequences of locations.
580580
```k
581-
syntax Map ::= Int "..." Int "|->" K
582-
[function, latex({#1}\ldots{#2}\mapsto{#3})]
581+
syntax Map ::= Int "..." Int "|->" K [function]
583582
rule N...M |-> _ => .Map requires N >Int M
584583
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
585584

‎2_languages/2_kool/1_untyped/kool-untyped.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -381,7 +381,7 @@ object and method closures.
381381
The semantics below are taken verbatim from the untyped SIMPLE
382382
definition.
383383
```k
384-
syntax KItem ::= "undefined" [latex(\bot)]
384+
syntax KItem ::= "undefined"
385385
386386
rule <k> var X:Id; => .K ...</k>
387387
<env> Env => Env[X <- L] </env>
@@ -583,7 +583,7 @@ from SIMPLE unchanged.
583583
584584
585585
syntax Map ::= Int "..." Int "|->" K
586-
[function, latex({#1}\ldots{#2}\mapsto{#3})]
586+
[function]
587587
rule N...M |-> _ => .Map requires N >Int M
588588
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
589589
```

‎2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md

+2-3
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,7 @@ KOOL).
247247
syntax KResult ::= Vals
248248
249249
250-
syntax KItem ::= undefined(Type) [latex(\bot_{#1})]
250+
syntax KItem ::= undefined(Type)
251251
252252
rule <k> T:Type X:Id; => .K ...</k>
253253
<env> Env => Env[X <- L] </env>
@@ -402,8 +402,7 @@ KOOL).
402402
rule T:Type<_,Vs:Vals> => T[]<Vs>
403403
rule T:Type<.Vals> => T
404404
405-
syntax Map ::= Int "..." Int "|->" K
406-
[function, latex({#1}\ldots{#2}\mapsto{#3})]
405+
syntax Map ::= Int "..." Int "|->" K [function]
407406
rule N...M |-> _ => .Map requires N >Int M
408407
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M
409408

‎2_languages/2_kool/2_typed/2_static/kool-typed-static.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -891,7 +891,7 @@ is co-variant in the codomain and contra-variant in the domain).
891891
## Generic operations which could be part of the **K** framework
892892

893893
```k
894-
syntax KItem ::= stuck(K) [latex(\framebox{${#1}$})]
894+
syntax KItem ::= stuck(K)
895895
896896
syntax KItem ::= "discard"
897897
rule _:KResult ~> discard => .K

0 commit comments

Comments
 (0)