From 78cc58e3076ffd61add6d78b64371b6eb36d6ab2 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 3 Apr 2024 17:52:10 +0200 Subject: resolved requested changes --- compiler/ExtractBase.ml | 2 +- compiler/PrintPure.ml | 4 +--- compiler/SymbolicToPure.ml | 4 ++-- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index faca2bde..e399a89c 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1701,7 +1701,7 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") | TArrow _ -> "f" | TTraitType (_, name) -> name_from_type_ident name - | Error -> "@Error") + | Error -> "x") (* TODO : Check*) (** Generates a type variable basename. *) diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 12d554f2..97ea6048 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -616,9 +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 (meta, msg) -> - if Option.is_none meta then msg - else meta_to_string (Option.get meta) ^ " " ^ msg (* TODO formatting *) + | EError (_, _) -> "@Error" and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) (app : texpression) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 1701891f..53ab1c08 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1963,7 +1963,7 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info -let translate_meta (meta : Meta.meta option) (msg : string) : texpression = +let translate_error (meta : Meta.meta option) (msg : string) : texpression = { e = EError (meta, msg); ty = Error } let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = @@ -1992,7 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx - | Error (meta, msg) -> translate_meta meta msg + | Error (meta, msg) -> translate_error meta msg and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because -- cgit v1.2.3