Make progress on write_projection

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 04c5427b..dbe2ae83 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,3 +1,5 @@
+open Errors
+
 (** Signature for a module describing an identifier.
     
     We often need identifiers (for definitions, variables, etc.) and in
@@ -23,6 +25,8 @@ module type Id = sig
 
   val nth_opt : 'a vector -> id -> 'a option
 
+  val update_nth : 'a vector -> id -> 'a -> 'a vector
+
   module Set : Set.S with type elt = id
 
   val set_to_string : Set.t -> string
@@ -63,6 +67,12 @@ module IdGen () : Id = struct
 
   let nth_opt v id = List.nth_opt v id
 
+  let rec update_nth vec id v =
+    match (vec, id) with
+    | [], _ -> unreachable __LOC__
+    | _ :: vec', 0 -> v :: vec'
+    | x :: vec', _ -> x :: update_nth vec' (id - 1) v
+
   module Set = Set.Make (struct
     type t = id