From 809291d5ef7371bfe8841b95126c0332da55578f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Mar 2020 17:52:16 -0400
Subject: [obligations] Pre-functionalize Program state

In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.

Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.

This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.

Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
---
 clib/cSig.mli | 1 +
 clib/hMap.ml  | 4 ++++
 2 files changed, 5 insertions(+)

(limited to 'clib')

diff --git a/clib/cSig.mli b/clib/cSig.mli
index ca888f875a..1305be42bd 100644
--- a/clib/cSig.mli
+++ b/clib/cSig.mli
@@ -83,6 +83,7 @@ sig
     val min_binding: 'a t -> (key * 'a)
     val max_binding: 'a t -> (key * 'a)
     val choose: 'a t -> (key * 'a)
+    val choose_opt: 'a t -> (key * 'a) option
     val split: key -> 'a t -> 'a t * 'a option * 'a t
     val find: key -> 'a t -> 'a
     val find_opt : key -> 'a t -> 'a option
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 3baa105fb0..210c48786b 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -356,6 +356,10 @@ struct
     let (_, m) = Int.Map.choose s in
     Map.choose m
 
+  let choose_opt s =
+    try Some (choose s)
+    with Not_found -> None
+
   let find k s =
     let h = M.hash k in
     let m = Int.Map.find h s in
-- 
cgit v1.2.3