Refactor addMethod

Pi-Squared-Inc · Aug 20, 2024 · 67c29ff · 67c29ff
1 parent f873c40
commit 67c29ff
Showing 1 changed file with 58 additions and 14 deletions.
diff --git a/rust-semantics/preprocessing/helpers.md b/rust-semantics/preprocessing/helpers.md
@@ -1,27 +1,71 @@
 ```k
 
 module RUST-PREPROCESSING-PRIVATE-HELPERS
+    imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
     imports private RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
 
-    syntax Identifier ::= getFunctionName(Function)  [function, total]
-    rule getFunctionName(_Q:FunctionQualifiers F:FunctionWithoutQualifiers)
-        => getFunctionName(F)
-    rule getFunctionName(F:FunctionWithWhere _B:BlockExpression)
-        => getFunctionName(F ;)
-    rule getFunctionName(F:FunctionWithReturnType _W:WhereClause ;)
-        => getFunctionName(F ;)
-    rule getFunctionName(F:FunctionWithParams _R:FunctionReturnType ;)
-        => getFunctionName(F ;)
-    rule getFunctionName(fn Name:Identifier _P:GenericParams ( ) ;)
-      => Name
-    rule getFunctionName(fn Name:Identifier ( ) ;)
+    syntax Error ::= error(String, KItem)
+
+    syntax FunctionWithParams ::= getFunctionWithParams(Function)  [function, total]
+    rule getFunctionWithParams(_Q:FunctionQualifiers F:FunctionWithoutQualifiers)
+        => getFunctionWithParams(F)
+    rule getFunctionWithParams(F:FunctionWithWhere _B:BlockExpression)
+        => getFunctionWithParams(F ;)
+    rule getFunctionWithParams(F:FunctionWithReturnType _W:WhereClause ;)
+        => getFunctionWithParams(F ;)
+    rule getFunctionWithParams(F:FunctionWithParams _R:FunctionReturnType ;)
+        => F
+
+    syntax Identifier ::= getFunctionWithParamsName(FunctionWithParams)  [function, total]
+    rule getFunctionWithParamsName(fn Name:Identifier _P:GenericParams ( ))
+        => Name
+    rule getFunctionWithParamsName(fn Name:Identifier ( ))
         => Name
-    rule getFunctionName(fn Name:Identifier  _P:GenericParams ( _Params:FunctionParameters ) ;)
+    rule getFunctionWithParamsName(fn Name:Identifier  _P:GenericParams ( _Params:FunctionParameters ))
         => Name
-    rule getFunctionName(fn Name:Identifier ( _Params:FunctionParameters ) ;)
+    rule getFunctionWithParamsName(fn Name:Identifier ( _Params:FunctionParameters ))
         => Name
 
+    syntax Identifier ::= getFunctionName(Function)  [function, total]
+    rule getFunctionName(F:Function)
+        => getFunctionWithParamsName(getFunctionWithParams(F))
+
+    syntax NormalizedFunctionParameterListOrError ::= extractFunctionNormalizedParams(Function)  [function, total]
+    rule extractFunctionNormalizedParams(F) => extractFunctionWithParamsNormalizedParams(getFunctionWithParams(F))
+
+    syntax NormalizedFunctionParameterListOrError ::= extractFunctionWithParamsNormalizedParams(FunctionWithParams)  [function, total]
+    rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier _P:GenericParams ( ))
+        => .NormalizedFunctionParameterList
+    rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( ))
+        => .NormalizedFunctionParameterList
+    rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier  _P:GenericParams ( Params:FunctionParameters ))
+        => normalizeParams(Params)
+    rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( Params:FunctionParameters ))
+        => normalizeParams(Params)
+
+    syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | Error
+
+    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
+
+    syntax NormalizedFunctionParameterListOrError ::= normalizeParams(FunctionParameters)  [function, total]
+    rule normalizeParams(_:SelfParam) => self : $selftype
+    rule normalizeParams(_:SelfParam , ) => self : $selftype
+    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 ::= 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