Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

1 files changed, 11 insertions, 0 deletions

diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 8d3b5258..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
@@ -399,6 +405,11 @@ let type_decl_is_enum (def : T.type_decl) : bool =
 let mk_state_ty : ty = Adt (Assumed State, [])
 let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
 
+let unwrap_result_ty (ty : ty) : ty =
+  match ty with
+  | Adt (Assumed Result, [ ty ]) -> ty
+  | _ -> failwith "not a result type"
+
 let mk_result_fail_texpression (ty : ty) : texpression =
   let type_args = [ ty ] in
   let ty = Adt (Assumed Result, type_args) in