diff options
| -rw-r--r-- | src/PrintPure.ml | 2 | ||||
| -rw-r--r-- | src/Pure.ml | 7 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 2 |
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 |