summaryrefslogtreecommitdiff
path: root/src/PureMicroPasses.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/PureMicroPasses.ml16
1 files changed, 14 insertions, 2 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 5cd07fbe..aab19c11 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -213,8 +213,20 @@ let compute_pretty_names (def : fun_def) : fun_def =
List.map (fun (v, mp) -> (update_typed_lvalue ctx v, mp)) lvs
in
(ctx, Let (Call (lvs, call), e))
- | Assign (lv, lmp, rv, rmp) -> raise Unimplemented
- | Deconstruct (lvs, opt_variant_id, rv, rmp) -> raise Unimplemented
+ | Assign (lv, lmp, rv, rmp) ->
+ let ctx = add_left_constraint_typed_value lmp lv ctx in
+ let ctx = add_opt_right_constraint rmp rv ctx in
+ let ctx, e = update_expression e ctx in
+ let lv = update_typed_lvalue ctx lv in
+ (ctx, Let (Assign (lv, lmp, rv, rmp), e))
+ | Deconstruct (lvs, opt_variant_id, rv, rmp) ->
+ let ctx = add_left_constraint_var_or_dummy_list ctx lvs in
+ let ctx = add_opt_right_constraint rmp rv ctx in
+ let ctx, e = update_expression e ctx in
+ let lvs =
+ List.map (fun (v, mp) -> (update_var_or_dummy ctx v, mp)) lvs
+ in
+ (ctx, Let (Deconstruct (lvs, opt_variant_id, rv, rmp), e))
(* *)
and update_switch_body (scrut : typed_rvalue) (mp : mplace option)
(body : switch_body) (ctx : pn_ctx) : pn_ctx * expression =