summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-27 18:37:51 +0100
committerSon Ho2022-01-27 18:37:51 +0100
commitea254c8af48ad5b4efd56624de40a9cb42452dd2 (patch)
treee1fa356b2437e9846de3095b8ba68cbc823656d2
parent46390b3ea190b6307c87f10df1c375d5b30c6b52 (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--src/PrintPure.ml2
-rw-r--r--src/Pure.ml7
-rw-r--r--src/SymbolicToPure.ml2
3 files changed, 8 insertions, 3 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index bf898424..3d41e67d 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -328,7 +328,7 @@ let rec expression_to_string (fmt : ast_formatter) (indent : string)
(indent_incr : string) (e : expression) : string =
match e with
| Return v -> indent ^ "return " ^ typed_rvalue_to_string fmt v
- | Panic -> indent ^ "panic"
+ | Fail -> indent ^ "fail"
| Let (lb, e) -> let_to_string fmt indent indent_incr lb e
| Switch (scrutinee, body) ->
switch_to_string fmt indent indent_incr scrutinee body
diff --git a/src/Pure.ml b/src/Pure.ml
index 0016aedb..45609273 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -188,10 +188,15 @@ type let_bindings =
(** **Rk.:** here, [expression] is not at all equivalent to the expressions
used in CFIM. They are lambda-calculus expressions, and are thus actually
more general than the CFIM statements, in a sense.
+
+ TODO: actually when I defined [expression] I still had Rust in mind, so
+ it is not a "textbook" lambda calculus expression (still quite constrained).
+ As we want to do transformations on it, through micro-passes, it would be
+ good to update it and make it more "regular".
*)
type expression =
| Return of typed_rvalue
- | Panic
+ | Fail
| Let of let_bindings * expression
(** Let bindings include the let-bindings introduced because of function calls *)
| Switch of typed_rvalue * switch_body
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 420c7eda..53073563 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -892,7 +892,7 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression =
match e with
| S.Return opt_v -> translate_return opt_v ctx
- | Panic -> Panic
+ | Panic -> Fail
| FunCall (call, e) -> translate_function_call call e ctx
| EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
| Expansion (sv, exp) -> translate_expansion sv exp ctx