Merge pull request #67 from sipma/jsonserialization

JSON: fix serialization error due to SituatedMsg

Author: sipma

chc/app/CHVersion.py

@@ -1 +1 @@
-chcversion: str = "0.2.0-2026-02-23"
+chcversion: str = "0.2.0-2026-02-26"

chc/cmdline/jsonresultutil.py

@@ -4,7 +4,7 @@
 # ------------------------------------------------------------------------------
 # The MIT License (MIT)
 #
-# Copyright (c) 2024  Aarno Labs LLC
+# Copyright (c) 2024-2026  Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -203,12 +203,12 @@ def ppo_to_json_result(po: "CFunctionPO") -> JSONResult:
     content["predicate"] = str(po.predicate)
     content["context"] = programcontext_to_json_result(po.context).content
     if po.is_closed:
-        content["expl"] = po.explanation
+        content["expl"] = po.explanation_txt
     else:
         if po.has_diagnostic():
-            content["argdiagnostics"] = po.diagnostic.argument_msgs
+            content["argdiagnostics"] = po.diagnostic.argument_msgs_txt
             content["keydiagnostics"] = po.diagnostic.keyword_msgs
-            content["msgdiagnostics"] = po.diagnostic.msgs
+            content["msgdiagnostics"] = po.diagnostic.msgs_txt
     return JSONResult("ppo", content, "ok")
 
 

chc/proof/CFunctionPO.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2022 Henny B. Sipma
-# Copyright (c) 2023-2024 Aarno Labs LLC
+# Copyright (c) 2023-2026 Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -185,6 +185,16 @@ def has_dependencies(self) -> bool:
     def explanation(self) -> Optional["SituatedMsg"]:
         return self._explanation
 
+    @property
+    def explanation_txt(self) -> Optional[str]:
+        """Returns the text of the explanation message without the additional
+        details."""
+
+        if self.explanation is not None:
+            return self.explanation.msg
+        else:
+            return None
+
     def has_explanation(self) -> bool:
         return self._explanation is not None
 

chc/proof/CProofDiagnostic.py

@@ -6,7 +6,7 @@
 #
 # Copyright (c) 2017-2020 Kestrel Technology LLC
 # Copyright (c) 2020-2022 Henny B. Sipma
-# Copyright (c) 2023-2024 Aarno Labs LLC
+# Copyright (c) 2023-2026 Aarno Labs LLC
 #
 # Permission is hereby granted, free of charge, to any person obtaining a copy
 # of this software and associated documentation files (the "Software"), to deal
@@ -148,6 +148,13 @@ def msgs(self) -> List[SituatedMsg]:
                         SituatedMsg(self.cd, x) for x in mnode.findall("msg")]
         return self._msgs
 
+    @property
+    def msgs_txt(self) -> List[str]:
+        """Returns the ext of the situated msgs without the additional
+        details."""
+
+        return [smsg.msg for smsg in self.msgs]
+
     @property
     def argument_msgs(self) -> Dict[int, List[SituatedMsg]]:
         """Returns argument-specific diagnostic messages.
@@ -168,6 +175,16 @@ def argument_msgs(self) -> Dict[int, List[SituatedMsg]]:
                             self._amsgs[int(xargindex)] = msgs
         return self._amsgs
 
+    @property
+    def argument_msgs_txt(self) -> Dict[int, List[str]]:
+        """Returns the texts of the situated msgs without the additional
+        details."""
+
+        result: Dict[int, List[str]] = {}
+        for (index, smsgs) in self.argument_msgs.items():
+            result[index] = [smsg.msg for smsg in smsgs]
+        return result
+
     @property
     def keyword_msgs(self) -> Dict[str, List[str]]:
         """Returns diagnostics with a known keyword (e.g., a domain name)."""