snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationEnv.ml

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml
index b6ae4e6beeed373ec00f7aaac2cb9c62c6674371..749e9148b979e7d7a137fef76f4968f556767afb 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationEnv.ml
+++ b/helm/ocaml/cic_notation/cicNotationEnv.ml
@@ -50,6 +50,8 @@ let lookup_value env name =
     snd (List.assoc name env)
   with Not_found -> raise (Value_not_found name)
 
+let remove env name = List.remove_assoc name env
+
 let lookup_term env name =
   match lookup_value env name with
   | TermValue x -> x
@@ -100,3 +102,22 @@ let rec well_typed ty value =
       List.for_all (fun value' -> well_typed ty' value') vl
   | _ -> false
 
+let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty))
+
+let coalesce_env declarations env_list =
+  let env0 = List.map list_binding_of_name declarations in
+  let grow_env_entry env n v =
+    List.map
+      (function
+        | (n', (ty, ListValue vl)) as entry ->
+            if n' = n then n', (ty, ListValue (v :: vl)) else entry
+        | _ -> assert false)
+      env
+  in
+  let grow_env env_i env =
+    List.fold_left
+      (fun env (n, (_, v)) -> grow_env_entry env n v)
+      env env_i
+  in
+  List.fold_right grow_env env_list env0
+