summaryrefslogtreecommitdiff
path: root/src/PureUtils.ml
diff options
context:
space:
mode:
authorSon Ho2022-02-23 18:28:53 +0100
committerSon Ho2022-02-23 18:28:53 +0100
commit1a980555aa7db64af2fb745e696ea595fb142c4a (patch)
tree67eaa979a9e96a8fdca7ddaecdf408c743d8bb29 /src/PureUtils.ml
parent453818ff089f14d4ccf887184ba54b0cb568ffe5 (diff)
Improve the code generation by inlining more let-bindings
Diffstat (limited to 'src/PureUtils.ml')
-rw-r--r--src/PureUtils.ml23
1 files changed, 23 insertions, 0 deletions
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 1ed072e9..f51f9415 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -347,3 +347,26 @@ module TypeCheck = struct
check_typed_rvalue ctx v)
av.variant_id av.field_values v.ty
end
+
+let is_value (e : texpression) : bool =
+ match e.e with Value _ -> true | _ -> false
+
+let is_var (e : texpression) : bool =
+ match e.e with
+ | Value (v, _) -> (
+ match v.value with
+ | RvPlace { var = _; projection = [] } -> true
+ | _ -> false)
+ | _ -> false
+
+let as_var (e : texpression) : VarId.id =
+ match e.e with
+ | Value (v, _) -> (
+ match v.value with
+ | RvPlace { var; projection = [] } -> var
+ | _ -> raise (Failure "Unreachable"))
+ | _ -> raise (Failure "Unreachable")
+
+(** Remove the external occurrences of [Meta] *)
+let rec unmeta (e : texpression) : texpression =
+ match e.e with Meta (_, e) -> unmeta e | _ -> e