Minor refactor

kaist-plrg · Feb 20, 2024 · e32bdc7 · e32bdc7
1 parent 0a05023
commit e32bdc7
Show file tree

Hide file tree

Showing 3 changed files with 168 additions and 187 deletions.
diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml
@@ -153,16 +153,14 @@ module AlContext = struct
 
   type t = mode list
 
+  let tl = List.tl
+
   let is_reducible = function
     | [] | [ Return _ ] -> false
     | _ -> true
 
-  let get_context = List.hd
-
-  let pop_context = List.tl
-
   let get_name ctx =
-    match get_context ctx with
+    match List.hd ctx with
     | Al (name, _, _) -> name
     | Wasm _ -> "Wasm"
     | Execute _ -> "Execute"

diff --git a/spectec/src/backend-interpreter/ds.mli b/spectec/src/backend-interpreter/ds.mli
@@ -44,8 +44,8 @@ module AlContext : sig
   val execute : value -> mode
   val return : value -> mode
   type t = mode list
+  val tl : t -> t
   val is_reducible : t -> bool
-  val pop_context : t -> t
   val get_name : t -> string
   val add_instrs : instr list -> t -> t
   val set_env : env -> t -> t