summaryrefslogtreecommitdiff
path: root/compiler/PrintPure.ml
diff options
context:
space:
mode:
authorSon HO2024-04-04 16:09:48 +0200
committerGitHub2024-04-04 16:09:48 +0200
commit061d7f72bec27de46245afc82149271ca8c75627 (patch)
treeaddd12dec0c1f5a564f9204fda77301771ff5e46 /compiler/PrintPure.ml
parent3909a38f3f8c58c9f97d36777c52e02617ef70b4 (diff)
parent77208249c717579d1014f27592566069b8cd0eb2 (diff)
Merge pull request #106 from AeneasVerif/escherichia/error_catching
Added Error and EError to expressions and propagated related changes
Diffstat (limited to 'compiler/PrintPure.ml')
-rw-r--r--compiler/PrintPure.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..97ea6048 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
let trait_ref = trait_ref_to_string env false trait_ref in
let s = trait_ref ^ "::" ^ type_name in
if inside then "(" ^ s ^ ")" else s
+ | Error -> "@Error"
and generic_args_to_strings (env : fmt_env) (inside : bool)
(generics : generic_args) : string list =
@@ -615,6 +616,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
let e = meta_s ^ "\n" ^ indent ^ e in
if inside then "(" ^ e ^ ")" else e
| MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
+ | EError (_, _) -> "@Error"
and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
(inside : bool) (indent : string) (indent_incr : string) (app : texpression)