Fix module of TS verification return types

dev/test_data/common_meta_models/enum.py

@@ -9,6 +9,19 @@ class Result(Enum):
     Not_ok = "not-ok"
 
 
+@verification
+def negated(result: Result) -> Result:
+    """Negate :paramref:`result`, returning an enumeration literal."""
+    if result == Result.Ok:
+        return Result.Not_ok
+
+    return Result.Ok
+
+
+@invariant(
+    lambda self: negated(negated(self.some_result)) == self.some_result,
+    "Negating the result twice must give the result.",
+)
 class Something:
     some_result: Result
 

dev/test_data/intermediate/common_meta_models/enum/expected_symbol_table.txt

@@ -73,7 +73,35 @@ SymbolTable(
               name='some_result',
               argument='some_result',
               default=None)""")]),
-      invariants=[],
+      invariants=[
+        Invariant(
+          description='Negating the result twice must give the result.',
+          body=textwrap.dedent("""\
+            Comparison(
+              left=FunctionCall(
+                name='negated',
+                args=[
+                  FunctionCall(
+                    name='negated',
+                    args=[
+                      Member(
+                        instance=Name(
+                          identifier='self',
+                          original_node=...),
+                        name='some_result',
+                        original_node=...)],
+                    original_node=...)],
+                original_node=...),
+              op='EQ',
+              right=Member(
+                instance=Name(
+                  identifier='self',
+                  original_node=...),
+                name='some_result',
+                original_node=...),
+              original_node=...)"""),
+          specified_for='Reference to ConcreteClass Something',
+          parsed=...)],
       serialization=Serialization(
         with_model_type=False),
       description=None,
@@ -95,7 +123,34 @@ SymbolTable(
   named_unions=[],
   constants=[],
   constants_by_name=...,
-  verification_functions=[],
+  verification_functions=[
+    TranspilableVerification(
+      name='negated',
+      visibility='PUBLIC',
+      arguments=[
+        Argument(
+          name='result',
+          type_annotation=OurTypeAnnotation(
+            our_type='Reference to our type Result',
+            parsed=...),
+          default=None,
+          mutable=False,
+          parsed=...)],
+      returns=OurTypeAnnotation(
+        our_type='Reference to our type Result',
+        parsed=...),
+      description=DescriptionOfSignature(
+        summary='<paragraph>Negate <ReferenceToArgument refuri="result">result</ReferenceToArgument>, returning an enumeration literal.</paragraph>',
+        remarks=[],
+        arguments_by_name=[],
+        returns=None,
+        parsed=...),
+      contracts=Contracts(
+        preconditions=[],
+        snapshots=[],
+        postconditions=[]),
+      parsed=...,
+      arguments_by_name=...)],
   verification_functions_by_name=...,
   meta_model=MetaModel(
     description=None,

dev/test_data/main/cpp/expected/enum/expected_output/include/dummy/verification.hpp

@@ -212,6 +212,15 @@ class RecursiveVerification : public IVerification {
   const std::shared_ptr<types::IClass>& instance_;
 };  // class RecursiveVerification
 
+// region Verification functions
+
+/// \brief Negate \p result, returning an enumeration literal.
+types::Result Negated(
+  types::Result result
+);
+
+// endregion Verification functions
+
 }  // namespace verification
 /**@}*/
 

dev/test_data/main/cpp/expected/enum/expected_output/src/verification.cpp

@@ -37,6 +37,19 @@ Error::Error(
 
 // endregion struct Error
 
+// region Verification functions
+
+types::Result Negated(
+  types::Result result
+) {
+  if (result == types::Result::kOk) {
+    return types::Result::kNotOk;
+  }
+  return types::Result::kOk;
+}
+
+// endregion Verification functions
+
 namespace {
 
 /**
@@ -45,7 +58,7 @@ namespace {
  * A shape tells which checks apply to a value, see \ref ChecksOf.
  */
 enum class Shape : std::uint32_t {
-
+  kSomething = 0
 };  // enum class Shape
 
 /**
@@ -67,11 +80,33 @@ struct Check {
 
 // region Checks
 
+bool Something_0(
+  const void* value
+) {
+  const types::ISomething* that = (
+    static_cast<const types::ISomething*>(value)
+  );
+  return verification::Negated(
+    verification::Negated(
+      that->some_result()
+    )
+  ) == that->some_result();
+}
+
 /**
  * Give out the checks of the values of the \p shape.
  */
 const std::vector<Check>& ChecksOf(Shape shape) {
   switch (shape) {
+    case Shape::kSomething: {
+      static const std::vector<Check> checks = {
+        {
+          &Something_0,
+          L"Negating the result twice must give the result."
+        }
+      };
+      return checks;
+    }
     default:
       throw std::logic_error(
         common::Concat(
@@ -199,16 +234,87 @@ std::unique_ptr<IIterator> Empty() {
   return common::make_unique<EmptyIterator>();
 }
 
+/**
+ * Iterate over a single value which lives in the model.
+ */
+class OneIterator : public IIterator {
+ public:
+  OneIterator(
+    const void* value,
+    Shape shape
+  ) :
+    value_(value),
+    shape_(shape),
+    done_(true) {
+    // Intentionally empty.
+  }
+
+  void Start() override {
+    done_ = false;
+  }
+
+  void Next() override {
+    done_ = true;
+  }
+
+  bool Done() const override {
+    return done_;
+  }
+
+  const void* Value() const override {
+    return value_;
+  }
+
+  Shape ShapeOf() const override {
+    return shape_;
+  }
+
+  void AppendToPath(iteration::Path&) const override {
+    // Intentionally empty, as the value itself is the end of the path.
+  }
+
+  std::unique_ptr<IIterator> Clone() const override {
+    return common::make_unique<OneIterator>(*this);
+  }
+
+ private:
+  const void* value_;
+  Shape shape_;
+  bool done_;
+};  // class OneIterator
+
+std::unique_ptr<IIterator> One(
+  const void* value,
+  Shape shape
+) {
+  return common::make_unique<OneIterator>(value, shape);
+}
+
+std::unique_ptr<IIterator> Over_Something(
+  const types::ISomething& that,
+  bool
+) {
+  return One(&that, Shape::kSomething);
+}
+
 /**
  * Iterate over the values of the \p instance, dispatched on its runtime type.
  */
 std::unique_ptr<IIterator> DispatchOnModelType(
-  const types::IClass&,
-  bool
+  const types::IClass& instance,
+  bool recursive
 ) {
-  // NOTE (mristin):
-  // The instances of no class have anything to verify.
-  return Empty();
+  switch (instance.model_type()) {
+    case types::ModelType::kSomething:
+      return Over_Something(
+        dynamic_cast<const types::ISomething&>(instance),
+        recursive
+      );
+    default:
+      // NOTE (mristin):
+      // The instances of the other classes have nothing to verify.
+      return Empty();
+  }
 }
 
 // endregion Iteration over the values

dev/test_data/main/csharp/expected/enum/expected_output/dummy/verification.cs

@@ -31,6 +31,20 @@ namespace dummy
     /// </example>
     public static class Verification
     {
+        /// <summary>
+        /// Negate <paramref name="result" />, returning an enumeration literal.
+        /// </summary>
+        public static Result Negated(
+            Result result
+        )
+        {
+            if (result == Result.Ok)
+            {
+                return Result.NotOk;
+            }
+            return Result.Ok;
+        }  // public static Result Negated
+
         /// <summary>
         /// Hash allowed enum values for efficient validation of enums.
         /// </summary>
@@ -56,6 +70,14 @@ private class Transformer
                 Our.ISomething that
             )
             {
+                if (!(
+                    Verification.Negated(Verification.Negated(that.SomeResult)) == that.SomeResult))
+                {
+                    yield return new Reporting.Error(
+                        "Invariant violated:\n" +
+                        "Negating the result twice must give the result.");
+                }
+
                 foreach (var error in Verification.VerifyResult(that.SomeResult))
                 {
                     error.PrependSegment(

dev/test_data/main/golang/expected/enum/expected_output/verification/verification.go

@@ -44,6 +44,16 @@ func (ve *VerificationError) PathString() string {
 	return ourreporting.ToGolangPath(ve.Path)
 }
 
+// Negate result, returning an enumeration literal.
+func Negated(
+	result ourtypes.Result,
+) ourtypes.Result {
+	if result == ourtypes.ResultOk {
+		return ourtypes.ResultNotOk
+	}
+	return ourtypes.ResultOk
+}
+
 // Verify `that` instance of [ourtypes.ISomething].
 //
 // You have to supply the callback `onError` to iterate over the errors.
@@ -56,6 +66,17 @@ func VerifySomething(
 ) (abort bool) {
 	abort = false
 
+	if !(
+		Negated(Negated(that.SomeResult())) == that.SomeResult()) {
+		abort = onError(
+			newVerificationError(
+				"Negating the result twice must give the result.",),
+		)
+		if abort {
+			return
+		}
+	}
+
 	abort = VerifyResult(
 		that.SomeResult(),
 		func(err *VerificationError) bool {

dev/test_data/main/java/expected/enum/expected_output/src/main/java/dummy/verification/Verification.java

@@ -29,6 +29,17 @@
 import dummy.visitation.AbstractTransformer;
 
 public class Verification {
+  /**
+   * Negate {@code result}, returning an enumeration literal.
+   */
+  public static Result negated(
+    Result result) {
+    if (result == Result.OK) {
+        return Result.NOT_OK;
+    }
+    return Result.OK;
+  }
+
   /**
    * Hash allowed enum values for efficient validation of enums.
    */
@@ -56,6 +67,14 @@ public Stream<Reporting.Error> transformSomething(
       ISomething that) {
       Stream<Reporting.Error> errorStream = Stream.empty();
 
+      if (!(
+        negated(negated(that.getSomeResult())) == that.getSomeResult())) {
+        errorStream = Stream.<Reporting.Error>concat(errorStream,
+          Stream.of(new Reporting.Error(
+            "Invariant violated:\n" +
+            "Negating the result twice must give the result.")));
+      }
+
       errorStream = Stream.<Reporting.Error>concat(errorStream,
         Stream.of(that.getSomeResult())
           .flatMap(Verification::verifyResult)