From c8953e8f80c02b19ede2c319ab401bb0242ba002 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 19 Feb 2024 15:45:23 -0600 Subject: [PATCH] Replace usages of when with requires --- 1_k/4_imp++/lesson_2/imp.k | 2 +- 1_k/4_imp++/lesson_3/imp.k | 2 +- 1_k/4_imp++/lesson_4/imp.k | 2 +- 1_k/4_imp++/lesson_5/imp.k | 2 +- 1_k/4_imp++/lesson_8/imp.md | 2 +- .../2_typed/2_dynamic/simple-typed-dynamic.md | 22 ++++++------ 2_languages/2_kool/1_untyped/kool-untyped.md | 36 +++++++++---------- .../2_typed/2_static/kool-typed-static.md | 20 +++++------ .../1_untyped/1_environment/fun-untyped.md | 4 +-- 9 files changed, 46 insertions(+), 46 deletions(-) diff --git a/1_k/4_imp++/lesson_2/imp.k b/1_k/4_imp++/lesson_2/imp.k index 2c97d073..700741a8 100644 --- a/1_k/4_imp++/lesson_2/imp.k +++ b/1_k/4_imp++/lesson_2/imp.k @@ -48,7 +48,7 @@ module IMP rule X:Id => I ... ... X |-> N ... ... N |-> I ... - rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I // BExp diff --git a/1_k/4_imp++/lesson_3/imp.k b/1_k/4_imp++/lesson_3/imp.k index 2b7a30ae..f6f73fc0 100644 --- a/1_k/4_imp++/lesson_3/imp.k +++ b/1_k/4_imp++/lesson_3/imp.k @@ -51,7 +51,7 @@ module IMP rule ++X => I +Int 1 ... ... X |-> N ... ... N |-> (I => I +Int 1) ... - rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I // BExp diff --git a/1_k/4_imp++/lesson_4/imp.k b/1_k/4_imp++/lesson_4/imp.k index 0bcd442e..c5fbb14b 100644 --- a/1_k/4_imp++/lesson_4/imp.k +++ b/1_k/4_imp++/lesson_4/imp.k @@ -55,7 +55,7 @@ module IMP ... N |-> (I => I +Int 1) ... rule read() => I ... ListItem(I:Int) => .List ... - rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I rule Str1 + Str2 => Str1 +String Str2 diff --git a/1_k/4_imp++/lesson_5/imp.k b/1_k/4_imp++/lesson_5/imp.k index 98a52845..98034792 100644 --- a/1_k/4_imp++/lesson_5/imp.k +++ b/1_k/4_imp++/lesson_5/imp.k @@ -54,7 +54,7 @@ module IMP ... N |-> (I => I +Int 1) ... rule read() => I ... ListItem(I:Int) => .List ... - rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I rule Str1 + Str2 => Str1 +String Str2 diff --git a/1_k/4_imp++/lesson_8/imp.md b/1_k/4_imp++/lesson_8/imp.md index 05c8169b..e6181194 100644 --- a/1_k/4_imp++/lesson_8/imp.md +++ b/1_k/4_imp++/lesson_8/imp.md @@ -302,7 +302,7 @@ configuration. ### Arithmetic constructs ```k - rule I1 / I2 => I1 /Int I2 when I2 =/=Int 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 rule I1 + I2 => I1 +Int I2 rule - I => 0 -Int I ``` diff --git a/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md b/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md index 722f1db1..292e7187 100644 --- a/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md +++ b/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md @@ -241,7 +241,7 @@ right type to the allocated locations. ... .Map => L |-> array(T, L +Int 1, N) (L +Int 1)...(L +Int N) |-> undefined(T) ... L:Int => L +Int 1 +Int N - when N >=Int 0 + requires N >=Int 0 context _:Type _::Exp[HOLE::Exps]; ``` @@ -312,8 +312,8 @@ When done with the first pass, call `main()`. rule Str1 + Str2 => Str1 +String Str2 rule I1 - I2 => I1 -Int I2 rule I1 * I2 => I1 *Int I2 - rule I1 / I2 => I1 /Int I2 when I2 =/=K 0 - rule I1 % I2 => I1 %Int I2 when I2 =/=K 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0 + rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0 rule - I => 0 -Int I rule I1 < I2 => I1 I1 <=Int I2 @@ -338,7 +338,7 @@ Check array bounds, as part of the dynamic typing policy. // Same comment as for simple untyped regarding [anywhere] rule array(_:Type, L:Int, M:Int)[N:Int] => lookup(L +Int N) - when N >=Int 0 andBool N =Int 0 andBool N C) _ => Env - when typeOf(V) ==K T // check the type of the returned value + requires typeOf(V) ==K T // check the type of the returned value ``` Like the `undefined` above, `nothing` also gets tagged with a type now. The empty `return` statement is @@ -396,7 +396,7 @@ preserved: context (HOLE => lvalue(HOLE)) = _ rule loc(L) = V:Val => V ... ... L |-> (V' => V) ... - when typeOf(V) ==K typeOf(V') + requires typeOf(V) ==K typeOf(V') ``` ### Statements @@ -438,7 +438,7 @@ preserved: We only allow printing integers and strings: ```k rule print(V:Val, Es => Es); ... ... .List => ListItem(V) - when typeOf(V) ==K int orBool typeOf(V) ==K string + requires typeOf(V) ==K int orBool typeOf(V) ==K string rule print(.Vals); => . ``` @@ -509,7 +509,7 @@ values, in which case our semantics below works fine: rule acquire V:Val; => . ... ... .Map => V |-> 0 ... Busy (.Set => SetItem(V)) - when (notBool(V in Busy:Set)) + requires (notBool(V in Busy:Set)) rule acquire V; => . ... ... V:Val |-> (N:Int => N +Int 1) ... @@ -520,7 +520,7 @@ values, in which case our semantics below works fine: ```k rule release V:Val; => . ... ... V |-> (N => N:Int -Int 1) ... - when N >Int 0 + requires N >Int 0 rule release V; => . ... ... V:Val |-> 0 => .Map ... ... SetItem(V) => .Set ... @@ -580,8 +580,8 @@ Sequences of locations. ```k syntax Map ::= Int "..." Int "|->" K [function, latex({#1}\ldots{#2}\mapsto{#3})] - rule N...M |-> _ => .Map when N >Int M - rule N...M |-> K => N |-> K (N +Int 1)...M |-> K when N <=Int M + rule N...M |-> _ => .Map requires N >Int M + rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M // Type of a value. syntax Type ::= typeOf(K) [function] diff --git a/2_languages/2_kool/1_untyped/kool-untyped.md b/2_languages/2_kool/1_untyped/kool-untyped.md index 27f98f73..593e33c2 100644 --- a/2_languages/2_kool/1_untyped/kool-untyped.md +++ b/2_languages/2_kool/1_untyped/kool-untyped.md @@ -396,7 +396,7 @@ definition. ... .Map => L |-> array(L +Int 1, N) (L +Int 1) ... (L +Int N) |-> undefined ... L:Int => L +Int 1 +Int N - when N >=Int 0 + requires N >=Int 0 syntax Id ::= "$1" [token] | "$2" [token] @@ -425,8 +425,8 @@ definition. rule Str1 + Str2 => Str1 +String Str2 rule I1 - I2 => I1 -Int I2 rule I1 * I2 => I1 *Int I2 - rule I1 / I2 => I1 /Int I2 when I2 =/=K 0 - rule I1 % I2 => I1 %Int I2 when I2 =/=K 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0 + rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0 rule - I => 0 -Int I rule I1 < I2 => I1 I1 <=Int I2 @@ -535,14 +535,14 @@ from SIMPLE unchanged. rule acquire V:Val; => . ... ... .Map => V |-> 0 ... Busy (.Set => SetItem(V)) - when (notBool(V in Busy:Set)) + requires (notBool(V in Busy:Set)) rule acquire V; => . ... ... V:Val |-> (N:Int => N +Int 1) ... rule release V:Val; => . ... ... V |-> (N => N:Int -Int 1) ... - when N >Int 0 + requires N >Int 0 rule release V; => . ... ... V:Val |-> 0 => .Map ... ... SetItem(V) => .Set ... @@ -584,8 +584,8 @@ from SIMPLE unchanged. syntax Map ::= Int "..." Int "|->" K [function, latex({#1}\ldots{#2}\mapsto{#3})] - rule N...M |-> _ => .Map when N >Int M - rule N...M |-> K => N |-> K (N +Int 1)...M |-> K when N <=Int M + rule N...M |-> _ => .Map requires N >Int M + rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M ``` ## Changes to the existing untyped SIMPLE semantics @@ -858,9 +858,9 @@ current object is not altered by `super`, so future method invocations see the entire object, as needed for dynamic method dispatch. ```k rule X:Id => this . X ... Env:Map - when notBool(X in keys(Env)) + requires notBool(X in keys(Env)) - context HOLE._::Id when (HOLE =/=K super) + context HOLE._::Id requires (HOLE =/=K super) // TODO: explain how Assoc matching has been replaced with two rules here. // Maybe also improve it a bit. @@ -875,7 +875,7 @@ invocations see the entire object, as needed for dynamic method dispatch. => lookupMember(ListItem(envStackFrame(Class,Env)) EStack, X) rule objectClosure(Class:Id, (ListItem(envStackFrame(Class':Id,_)) => .List) _) . _X:Id - when Class =/=K Class' + requires Class =/=K Class' /* rule super . X => lookupMember(EStack, X) ... Class @@ -886,7 +886,7 @@ invocations see the entire object, as needed for dynamic method dispatch. rule super . _X ... Class ListItem(envStackFrame(Class':Id,_)) => .List ... - when Class =/=K Class' + requires Class =/=K Class' ``` ## Method invocation @@ -916,9 +916,9 @@ method call or the array access. rule (X:Id => this . X)(_:Exps) ... Env - when notBool(X in keys(Env)) + requires notBool(X in keys(Env)) - context HOLE._::Id(_) when HOLE =/=K super + context HOLE._::Id(_) requires HOLE =/=K super rule (objectClosure(_, EStack) . X => lookupMember(EStack, X:Id))(_:Exps) @@ -934,7 +934,7 @@ method call or the array access. rule (super . _X)(_:Exps) ... Class ListItem(envStackFrame(Class':Id,_)) => .List ... - when Class =/=K Class' + requires Class =/=K Class' // TODO(KORE): fix getKLabel #1801 rule (A:Exp(B:Exps))(C:Exps) => A(B) ~> #freezerFunCall(C) @@ -968,7 +968,7 @@ argument does not evaluate to an object. instanceOf C => true rule objectClosure(_, (ListItem(envStackFrame(C,_)) => .List) _) - instanceOf C' when C =/=K C' + instanceOf C' requires C =/=K C' //TODO: remove the sort cast ::Id of C above, when sort inference bug fixed rule objectClosure(_, .List) instanceOf _ => false @@ -1005,7 +1005,7 @@ evaluated, and finally the second rule initiates the lookup for the member's location based on the current class of the object. ```k rule lvalue(X:Id => this . X) ... Env - when notBool(X in keys(Env)) + requires notBool(X in keys(Env)) context lvalue((HOLE . _)::Exp) @@ -1020,7 +1020,7 @@ member's location based on the current class of the object. X)) rule lvalue(objectClosure(Class, (ListItem(envStackFrame(Class':Id,_)) => .List) _) . _X) - when Class =/=K Class' + requires Class =/=K Class' ``` ## Lookup member @@ -1043,7 +1043,7 @@ starting with the most concrete class and going up in the hierarchy. // when notBool(X in keys(Env)) rule lookupMember(ListItem(envStackFrame(_, Env)) Rest, X) => lookupMember(Rest, X) - when notBool(X in keys(Env)) + requires notBool(X in keys(Env)) //TODO: beautify the above endmodule diff --git a/2_languages/2_kool/2_typed/2_static/kool-typed-static.md b/2_languages/2_kool/2_typed/2_static/kool-typed-static.md index fbf938ef..7d06610e 100644 --- a/2_languages/2_kool/2_typed/2_static/kool-typed-static.md +++ b/2_languages/2_kool/2_typed/2_static/kool-typed-static.md @@ -363,7 +363,7 @@ typed SIMPLE, so we do not discuss them much here. rule read() => int - rule print(T:Type, Ts => Ts); when T ==K int orBool T ==K string + rule print(T:Type, Ts => Ts); requires T ==K int orBool T ==K string rule print(.Types); => stmt @@ -407,7 +407,7 @@ typed SIMPLE, so we do not discuss them much here. // We would like to say: // context ltype(HOLE:LValue) // but we currently cannot type the HOLE - context ltype(HOLE) when isLValue(HOLE) + context ltype(HOLE) requires isLValue(HOLE) // OLD approach: // syntax Exp ::= ltype(Exp) [function] @@ -459,7 +459,7 @@ at the end of this module). ```k rule T:Type X:Id; => checkType(T) ~> stmt ... Rho (.Map => X |-> T) - when notBool(X in keys(Rho)) + requires notBool(X in keys(Rho)) rule T:Type X:Id; => stuck(T X;) ... ... X |-> _ ... @@ -633,7 +633,7 @@ checks for cycles. SetItem(C) Cs:Set (.Set => SetItem(C')) ... ... C C' ... - when notBool(C' in (SetItem(C) Cs)) [priority(25)] + requires notBool(C' in (SetItem(C) Cs)) [priority(25)] rule (... C @@ -713,7 +713,7 @@ wait. Finally, the sixth rule below reports an error when the rule X:Id => this . X ... Rho - when notBool(X in keys(Rho)) + requires notBool(X in keys(Rho)) // OLD approach: // rule ltype(E:Exp . X:Id) => E . X @@ -726,7 +726,7 @@ wait. Finally, the sixth rule below reports an error when the C1 C2:Id Rho - when notBool(X in keys(Rho)) + requires notBool(X in keys(Rho)) rule `class`(Object) . X:Id => stuck(`class`(Object) . X) ... C:Id @@ -764,7 +764,7 @@ of the language need to insert runtime checks for downcasting to be safe. ... .List => ListItem("Classes \"" +String Id2String(C1) +String "\" and \"" +String Id2String(C2) +String "\" are incompatible!\n") - when notBool(C1 in S2) andBool notBool(C2 in S1) + requires notBool(C1 in S2) andBool notBool(C2 in S1) ``` ## Cleanup tasks @@ -837,7 +837,7 @@ The subclass relation introduces a subtyping relation. rule checkSubtype((T:Type,Ts),(T':Type,Ts')) => checkSubtype(T,T') ~> checkSubtype(Ts,Ts') - when Ts =/=K .Types + requires Ts =/=K .Types rule checkSubtype(.Types,.Types) => . rule checkSubtype(.Types,void) => . @@ -851,7 +851,7 @@ check that the types used in the program actually exists syntax KItem ::= checkType(Types) rule checkType(T:Type,Ts:Types) => checkType(T) ~> checkType(Ts) - when Ts =/=K .Types + requires Ts =/=K .Types rule checkType(.Types) => . rule checkType(int) => . rule checkType(bool) => . @@ -883,7 +883,7 @@ is co-variant in the codomain and contra-variant in the domain). C C':Id Rho - when notBool(F in keys(Rho)) + requires notBool(F in keys(Rho)) rule checkMethod(_:Id,_,Object) => . ``` diff --git a/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md index 5bf5bdfd..04393e3d 100644 --- a/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md +++ b/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md @@ -478,8 +478,8 @@ add more values later. ```k rule I1 * I2 => I1 *Int I2 - rule I1 / I2 => I1 /Int I2 when I2 =/=K 0 - rule I1 % I2 => I1 %Int I2 when I2 =/=K 0 + rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0 + rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0 rule I1 + I2 => I1 +Int I2 rule S1 ^ S2 => S1 +String S2 rule I1 - I2 => I1 -Int I2