Fix: No new resolver crash with partially resolved datatype update expressions (#5440)

Fixes #5331 
Fixes #5365

The only part that fixes the issue is the last line end of the file
PreTypeResolve.Expressions.cs, the rest is an automated conversion
If/then/else to a switch statement that helped debugging and makes the
code easier to maintain.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Author: MikaelMayer

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -0,0 +1,17 @@
+// RUN: %baredafny verify %args --type-system-refresh "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait Ins {
+    function step(s:State):State //requires safe?(s)
+}
+type Code = seq<Ins>
+datatype State = S(
+    clock:nat
+) {
+    function fetch_():Ins
+    const fetch := fetch_()
+    const step := fetch.step(this)
+    function run():State decreases clock {
+        if clock == 0 then this else step.(clock := clock - 1).run()
+    }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5331.dfy.expect

@@ -0,0 +1,9 @@
+// RUN: %baredafny verify %args --type-system-refresh "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype S  = S(
+    n:nat
+) {
+    function f():S { this }
+    function g():S { this.(n := 0).f() }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5365.dfy

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5365.dfy.expect

@@ -0,0 +1 @@
+No new resolver crash when datatype update expressions are partially resolved