summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEscherichia2024-04-03 17:52:10 +0200
committerEscherichia2024-04-03 17:52:10 +0200
commit78cc58e3076ffd61add6d78b64371b6eb36d6ab2 (patch)
tree5028b81de17c7d700ee64381e5b80fbf7e54c415
parenta2a219145587deb0ade9fa7d60171765cd722162 (diff)
resolved requested changes
-rw-r--r--compiler/ExtractBase.ml2
-rw-r--r--compiler/PrintPure.ml4
-rw-r--r--compiler/SymbolicToPure.ml4
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