summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-09-22 18:13:56 +0200
committerSon Ho2022-09-22 18:13:56 +0200
commit2b79c533d98f1bec8d332f660b36a05152b4c7dc (patch)
tree670f54bb8dcdf66c83f01b61d9f34b15b24fd2af /src
parentc8ccd864e1fa6de3241d9dba184cf8ee4101e421 (diff)
Update PureMicroPasses.inline_useless_var_reassignments
Diffstat (limited to 'src')
-rw-r--r--src/PureMicroPasses.ml67
-rw-r--r--src/PureUtils.ml6
2 files changed, 39 insertions, 34 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 7927a068..c8ebfa6b 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -586,48 +586,47 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
match (monadic, lv.value) with
| false, PatVar (lv_var, _) ->
(* We can filter if: *)
- let filter = false in
- (* 1. Either:
- * - the left variable is unnamed or [inline_named] is true
- * - the right-expression is a variable
- *)
- let filter =
+ (* 1. the left variable is unnamed or [inline_named] is true *)
+ let filter_left =
match (inline_named, lv_var.basename) with
- | true, _ | _, None -> is_var re
- | _ -> filter
+ | true, _ | _, None -> true
+ | _ -> false
+ in
+ (* And either:
+ * 2.1 the right-expression is a variable or a global *)
+ let var_or_global = is_var re || is_global re in
+ (* Or:
+ * 2.2 the right-expression is a constant value, an ADT value,
+ * a projection or a primitive function call *and* the flag
+ * `inline_pure` is set *)
+ let pure_re =
+ is_const re
+ ||
+ let app, _ = destruct_apps re in
+ match app.e with
+ | Qualif qualif -> (
+ match qualif.id with
+ | AdtCons _ -> true (* ADT constructor *)
+ | Proj _ -> true (* Projector *)
+ | Func (Unop _ | Binop _) ->
+ true (* primitive function call *)
+ | Func (Regular _) -> false (* non-primitive function call *)
+ | _ -> false)
+ | _ -> false
in
- (* 2. Or:
- * - the left variable is an unnamed variable
- * - the right-expression is a value or a primitive function call
- *)
let filter =
- if inline_pure then
- let app, _ = destruct_apps re in
- match app.e with
- | Const _ | Var _ -> true (* constant or variable *)
- | Qualif qualif -> (
- match qualif.id with
- | AdtCons _ | Proj _ -> true (* ADT constructor *)
- | Func (Unop _ | Binop _) ->
- true (* primitive function call *)
- | Func (Regular _) ->
- false (* non-primitive function call *)
- | Global _ ->
- true (* Global constant or static *)
- )
- | _ -> filter
- else false
+ filter_left && (var_or_global || (inline_pure && pure_re))
in
- (* Update the environment and continue the exploration *)
+ (* Update the rhs (we may perform substitutions inside, and it is
+ * better to do them *before* we inline it *)
let re = self#visit_texpression env re in
- (* TODO: once rvalues and expressions are merged, filter the
- * let-binding (note that for now we leave it, expect it to
- * become useless, and wait for a subsequent pass to filter it) *)
- (* let env = add_subst lv_var.id re env in *)
+ (* Update the substitution environment *)
let env = if filter then VarId.Map.add lv_var.id re env else env in
+ (* Update the next expression *)
let e = self#visit_texpression env e in
- Let (monadic, lv, re, e)
+ (* Reconstruct the `let`, only if the binding is not filtered *)
+ if filter then e.e else Let (monadic, lv, re, e)
| _ -> super#visit_Let env monadic lv re e
(** Visit the let-bindings to filter the useless ones (and update
the substitution map while doing so *)
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index e72ff9d7..c3d4c983 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -173,6 +173,12 @@ let is_var (e : texpression) : bool =
let as_var (e : texpression) : VarId.id =
match e.e with Var v -> v | _ -> raise (Failure "Unreachable")
+let is_global (e : texpression) : bool =
+ match e.e with Qualif { id = Global _; _ } -> true | _ -> false
+
+let is_const (e : texpression) : bool =
+ match e.e with Const _ -> true | _ -> false
+
(** Remove the external occurrences of [Meta] *)
let rec unmeta (e : texpression) : texpression =
match e.e with Meta (_, e) -> unmeta e | _ -> e