tmp

Pi-Squared-Inc · Aug 20, 2024 · fb016fc · fb016fc
1 parent 67c29ff
commit fb016fc
Show file tree

Hide file tree

Showing 5 changed files with 53 additions and 96 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,2 +1,3 @@
 .build
+.DS_store
 tmp
diff --git a/rust-semantics/preprocessing/helpers.md b/rust-semantics/preprocessing/helpers.md
@@ -5,8 +5,6 @@ module RUST-PREPROCESSING-PRIVATE-HELPERS
     imports private RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
 
-    syntax Error ::= error(String, KItem)
-
     syntax FunctionWithParams ::= getFunctionWithParams(Function)  [function, total]
     rule getFunctionWithParams(_Q:FunctionQualifiers F:FunctionWithoutQualifiers)
         => getFunctionWithParams(F)
@@ -16,6 +14,8 @@ module RUST-PREPROCESSING-PRIVATE-HELPERS
         => getFunctionWithParams(F ;)
     rule getFunctionWithParams(F:FunctionWithParams _R:FunctionReturnType ;)
         => F
+    rule getFunctionWithParams(F:FunctionWithParams ;)
+        => F
 
     syntax Identifier ::= getFunctionWithParamsName(FunctionWithParams)  [function, total]
     rule getFunctionWithParamsName(fn Name:Identifier _P:GenericParams ( ))
@@ -44,36 +44,51 @@ module RUST-PREPROCESSING-PRIVATE-HELPERS
     rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( Params:FunctionParameters ))
         => normalizeParams(Params)
 
-    syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | Error
-
-    syntax NormalizedFunctionParameterListOrError ::= concat(NormalizedFunctionParameterOrError, NormalizedFunctionParameterListOrError)  [function, total]
+    syntax NormalizedFunctionParameterListOrError ::= concat(
+            NormalizedFunctionParameterOrError,
+            NormalizedFunctionParameterListOrError
+        )  [function, total]
     rule concat(P:NormalizedFunctionParameter, L:NormalizedFunctionParameterList) => P , L
-    rule concat(P:Error, _:NormalizedFunctionParameterList) => P
-    rule concat(_:NormalizedFunctionParameter, L:Error) => L
+    rule concat(P:SemanticsError, _:NormalizedFunctionParameterListOrError) => P
+    rule concat(_:NormalizedFunctionParameter, L:SemanticsError) => L
 
     syntax NormalizedFunctionParameterListOrError ::= normalizeParams(FunctionParameters)  [function, total]
-    rule normalizeParams(_:SelfParam) => self : $selftype
-    rule normalizeParams(_:SelfParam , ) => self : $selftype
+    // We should not need an explicit conactenation here, but the LLVM decision tree code crashes.
+    rule normalizeParams(_:SelfParam) => self : $selftype , .NormalizedFunctionParameterList
+    // We should not need an explicit conactenation here, but the LLVM decision tree code crashes.
+    rule normalizeParams(_:SelfParam , ) => self : $selftype , .NormalizedFunctionParameterList
     rule normalizeParams(_:SelfParam , F:FunctionParameterList) => concat(self : $selftype, normalizeParams(F))
     rule normalizeParams(_:SelfParam , F:FunctionParameterList , ) => concat(self : $selftype, normalizeParams(F))
     rule normalizeParams(F:FunctionParameterList ,) => normalizeParams(F)
     rule normalizeParams(.FunctionParameterList) => .NormalizedFunctionParameterList
     rule normalizeParams(P:FunctionParam , F:FunctionParameterList) => concat(normalizeParam(P), normalizeParams(F))
 
-    syntax NormalizedFunctionParameterOrError ::= NormalizedFunctionParameter | Error
+    syntax NormalizedFunctionParameterOrError ::= NormalizedFunctionParameter | SemanticsError
 
     syntax NormalizedFunctionParameterOrError ::= normalizeParam(FunctionParam)  [function, total]
     rule normalizeParam(_:OuterAttributes Name:Identifier : T:Type) => Name : T
     rule normalizeParam(P:FunctionParam) => error("unimplemented normalizedParam case", P:FunctionParam:KItem)
 
-    syntax NormalizedFunctionParameterList  ::= reverse(NormalizedFunctionParameterList)  [function, total]
-                                              // See https://github.com/runtimeverification/k/issues/4587
-                                              // for the "Non exhaustive match detected" warning
-                                              | #reverse(NormalizedFunctionParameterList, NormalizedFunctionParameterList)  [function, total]
-    rule reverse(L:NormalizedFunctionParameterList) => #reverse(L, .NormalizedFunctionParameterList)
-    rule #reverse(.NormalizedFunctionParameterList, R) => R
-    rule #reverse((P:NormalizedFunctionParameter , L:NormalizedFunctionParameterList), R)
-        => #reverse(L, (P , R))
+    syntax BlockExpressionOrSemicolon ::= getFunctionBlockOrSemicolon(Function)  [function, total]
+    rule getFunctionBlockOrSemicolon(_Q:FunctionQualifiers F:FunctionWithoutQualifiers)
+        => getFunctionBlockOrSemicolon(F)
+    rule getFunctionBlockOrSemicolon(_F:FunctionWithWhere B:BlockExpressionOrSemicolon)
+        => B
+
+    syntax Type ::= getFunctionReturnType(Function)
+    rule getFunctionReturnType(_Q:FunctionQualifiers F:FunctionWithoutQualifiers)
+        => getFunctionReturnType(F)
+    rule getFunctionReturnType(F:FunctionWithWhere _B:BlockExpression)
+        => getFunctionReturnType(F ;)
+    rule getFunctionReturnType(F:FunctionWithReturnType _W:WhereClause ;)
+        => getFunctionReturnType(F ;)
+    rule getFunctionReturnType(_F:FunctionWithParams -> R:Type ;)
+        => R
+    // https://doc.rust-lang.org/stable/reference/items/functions.html
+    // If the output type is not explicitly stated, it is the unit type.
+    rule getFunctionReturnType(_F:FunctionWithParams ;)
+        => ( ):Type
+
 endmodule
 
 ```
diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md
@@ -5,23 +5,6 @@ module INITIALIZATION
     imports private RUST-PREPROCESSING-PRIVATE-HELPERS
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
 
-    // rule
-    //     <k> crateInitializer
-    //         ( ... constantNames:(ListItem(Name:Identifier) => .List) _Cts:List
-    //         , constants: _Constants (Name |-> V:Value => .Map)
-    //         )
-    //         ...
-    //     </k>
-    //     <crate>
-    //       <constants>
-    //         .Bag =>
-    //           <constant>
-    //             <constant-name> Name:Identifier </constant-name>
-    //             <constant-value> V:Value </constant-value>
-    //           </constant>
-    //       </constants>
-    //       ...
-    //     </crate>
     rule constantInitializer(... constantNames : .List) => .K
 
     rule (.K => addMethod(TraitName, F, A))
@@ -46,51 +29,18 @@ module INITIALIZATION
                 </trait>
         </traits>
 
-    // rule addMethod(_Q:FunctionQualifiers F:FunctionWithoutQualifiers, A:OuterAttributes)
-    //     => addMethod(F:FunctionWithoutQualifiers, A)
-    rule addMethod(Trait:TypePath, (F:FunctionWithWhere B:BlockExpressionOrSemicolon):FunctionWithoutQualifiers, A:OuterAttributes)
-        => addMethod1(Trait, F, B, A)
-
-    // rule addMethod1(F:FunctionWithReturnType _W:WhereClause, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-    //     => addMethod1(F, B, A)
-    // rule addMethod1(F:FunctionWithParams -> RT:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-    //     => addMethod2(F, RT, B, A)
-    rule addMethod1(Trait:TypePath, F:FunctionWithParams, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-        => addMethod2(Trait, F, (), B, A)
-
-    // rule addMethod2(fn Name ( ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-    //     => addMethod4(Name, .NormalizedFunctionParameterList, T, B, A)
-    rule addMethod2(Trait:TypePath, fn Name (_:SelfParam), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-        => addMethod4(Trait, Name, (self : $selftype), T, B, A)
-    // rule addMethod2(fn Name (_:SelfParam , ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-    //     => addMethod4(Name, (self : $selftype), T, B, A)
-    // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-    //     => addMethod3(Name, (self : $selftype), P, T, B, A)
-    // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList ,), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
-    //     => addMethod3(Name, (self : $selftype) , P, T, B, A)
-
-    // rule addMethod3(
-    //         _MethodName:Identifier,
-    //         ReversedNormalizedParams:NormalizedFunctionParameterList
-    //             => (ParamName : ParamType , ReversedNormalizedParams),
-    //         (ParamName:Identifier : ParamType:Type , Params:FunctionParameterList)
-    //             => Params,
-    //         _MethodReturnType:Type, _B:BlockExpressionOrSemicolon, _A:OuterAttributes
-    //     )
-    // rule addMethod3(
-    //         MethodName:Identifier,
-    //         ReversedNormalizedParams:NormalizedFunctionParameterList,
-    //         .FunctionParameterList,
-    //         MethodReturnType:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes
-    //     )
-    //     => addMethod4(
-    //         MethodName,
-    //         reverse(ReversedNormalizedParams),
-    //         MethodReturnType, B, A
-    //     )
+    rule addMethod(Trait:TypePath, F:Function, A:OuterAttributes)
+        => #addMethod
+            ( Trait
+            , getFunctionName(F)
+            , extractFunctionNormalizedParams(F)
+            , getFunctionReturnType(F)
+            , getFunctionBlockOrSemicolon(F)
+            , A
+            )
 
     rule
-        <k> addMethod4(
+        <k> #addMethod(
                 Trait:TypePath,
                 Name:Identifier, P:NormalizedFunctionParameterList,
                 R:Type, B:BlockExpression,

diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md
@@ -25,27 +25,14 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
                                 )
 
     syntax Initializer  ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes)
-                          | addMethod1(
+                          | #addMethod(
                                 TypePath,
-                                FunctionWithWhere, BlockExpressionOrSemicolon,
+                                Identifier,
+                                NormalizedFunctionParameterListOrError,
+                                Type,
+                                BlockExpressionOrSemicolon,
                                 OuterAttributes
                             )
-                          | addMethod2(
-                                TypePath,
-                                FunctionWithParams, Type,
-                                BlockExpressionOrSemicolon, OuterAttributes
-                            )
-                          | addMethod3(
-                                TypePath,
-                                Identifier, NormalizedFunctionParameterList,
-                                FunctionParameterList, Type,
-                                BlockExpressionOrSemicolon, OuterAttributes
-                            )
-                          | addMethod4(
-                                TypePath,
-                                Identifier, NormalizedFunctionParameterList, Type,
-                                BlockExpressionOrSemicolon, OuterAttributes
-                            )
 
     // TODO: Move to a more generic place
     syntax Identifier ::= "self"  [token]

diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
@@ -10,12 +10,16 @@ module RUST-REPRESENTATION
     syntax MInt{32}
     syntax MInt{64}
 
+    syntax SemanticsError ::= error(String, KItem)
+
     syntax FunctionBodyRepresentation ::= block(BlockExpression)
                                         | "empty"
                                         | storageAccessor(StringLiteral)
     syntax NormalizedFunctionParameter ::= Identifier ":" Type
     syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","}
 
+    syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
+
     syntax Value  ::= i32(MInt{32})
                     | u32(MInt{32})
                     | i64(MInt{64})