From 2deb3ba7d283af68adfae9ceede41a7ae9767504 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Thu, 26 Feb 2026 10:01:11 -0800 Subject: [PATCH] JSON: fix serialization error due to SituatedMsg --- chc/app/CHVersion.py | 2 +- chc/cmdline/jsonresultutil.py | 8 ++++---- chc/proof/CFunctionPO.py | 12 +++++++++++- chc/proof/CProofDiagnostic.py | 19 ++++++++++++++++++- 4 files changed, 34 insertions(+), 7 deletions(-) diff --git a/chc/app/CHVersion.py b/chc/app/CHVersion.py index 4d4e38f..58d6793 100644 --- a/chc/app/CHVersion.py +++ b/chc/app/CHVersion.py @@ -1 +1 @@ -chcversion: str = "0.2.0-2026-02-23" +chcversion: str = "0.2.0-2026-02-26" diff --git a/chc/cmdline/jsonresultutil.py b/chc/cmdline/jsonresultutil.py index fca9e6c..82c16da 100644 --- a/chc/cmdline/jsonresultutil.py +++ b/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") diff --git a/chc/proof/CFunctionPO.py b/chc/proof/CFunctionPO.py index e0f5be3..d095d13 100644 --- a/chc/proof/CFunctionPO.py +++ b/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 diff --git a/chc/proof/CProofDiagnostic.py b/chc/proof/CProofDiagnostic.py index 5f6a50f..e238c5f 100644 --- a/chc/proof/CProofDiagnostic.py +++ b/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)."""