From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/opaqueproof.ml | 108 ++++++++++++++++++++++++++++----------------------
 1 file changed, 61 insertions(+), 47 deletions(-)

(limited to 'kernel/opaqueproof.ml')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 130f1eb0..a484c08e 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -1,14 +1,16 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
 open Univ
-open Term
+open Constr
 open Mod_subst
 
 type work_list = (Instance.t * Id.t array) Cmap.t * 
@@ -16,22 +18,31 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t } 
-type proofterm = (constr * Univ.universe_context_set) Future.computation
+  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
+type proofterm = (constr * Univ.ContextSet.t) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
-type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t
-let empty_opaquetab = Int.Map.empty, DirPath.initial
+type opaquetab = {
+  opaque_val : (cooking_info list * proofterm) Int.Map.t;
+  (** Actual proof terms *)
+  opaque_len : int;
+  (** Size of the above map *)
+  opaque_dir : DirPath.t;
+}
+let empty_opaquetab = {
+  opaque_val = Int.Map.empty;
+  opaque_len = 0;
+  opaque_dir = DirPath.initial;
+}
 
 (* hooks *)
 let default_get_opaque dp _ =
-  CErrors.error
-    ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+  CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
 let default_get_univ dp _ =
-  CErrors.error
-    ("Cannot access universe constraints of opaque proofs in library " ^
-    DirPath.to_string dp)
+  CErrors.user_err (Pp.pr_sequence Pp.str [
+    "Cannot access universe constraints of opaque proofs in library ";
+    DirPath.to_string dp])
 
 let get_opaque = ref default_get_opaque
 let get_univ = ref default_get_univ
@@ -42,62 +53,66 @@ let set_indirect_univ_accessor f = (get_univ := f)
 
 let create cu = Direct ([],cu)
 
-let turn_indirect dp o (prfs,odp) = match o with
+let turn_indirect dp o tab = match o with
   | Indirect (_,_,i) ->
-      if not (Int.Map.mem i prfs)
-      then CErrors.anomaly (Pp.str "Indirect in a different table")
-      else CErrors.anomaly (Pp.str "Already an indirect opaque")
+      if not (Int.Map.mem i tab.opaque_val)
+      then CErrors.anomaly (Pp.str "Indirect in a different table.")
+      else CErrors.anomaly (Pp.str "Already an indirect opaque.")
   | Direct (d,cu) ->
-      let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
-      let id = Int.Map.cardinal prfs in
-      let prfs = Int.Map.add id (d,cu) prfs in
-      let ndp =
-        if DirPath.equal dp odp then odp
-        else if DirPath.equal odp DirPath.initial then dp
+      (** Uncomment to check dynamically that all terms turned into
+          indirections are hashconsed. *)
+(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
+(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
+      let id = tab.opaque_len in
+      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+      let opaque_dir =
+        if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
+        else if DirPath.equal tab.opaque_dir DirPath.initial then dp
         else CErrors.anomaly
-          (Pp.str "Using the same opaque table for multiple dirpaths") in
-      Indirect ([],dp,id), (prfs, ndp)
+          (Pp.str "Using the same opaque table for multiple dirpaths.") in
+      let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
+      Indirect ([],dp,id), ntab
 
 let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
-  | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque")
+  | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
 let iter_direct_opaque f = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
-      Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
+      Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
 
 let discharge_direct_opaque ~cook_constr ci = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
-      Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
+      Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque (prfs,odp) = function
+let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> ignore(Future.join cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
         let fp = snd (Int.Map.find i prfs) in
         ignore(Future.join fp)
 
-let uuid_opaque (prfs,odp) = function
+let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> Some (Future.uuid cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then Some (Future.uuid (snd (Int.Map.find i prfs)))
       else None
 
-let force_proof (prfs,odp) = function
+let force_proof { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
-        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        then Future.chain (snd (Int.Map.find i prfs)) fst
         else !get_opaque dp i in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints (prfs,odp) = function
+let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
@@ -106,37 +121,36 @@ let force_constraints (prfs,odp) = function
         | None -> Univ.ContextSet.empty
         | Some u -> Future.force u
 
-let get_constraints (prfs,odp) = function
-  | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
+let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
+  | Direct (_,cu) -> Some(Future.chain cu snd)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
-      then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
+      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
-let get_proof (prfs,odp) = function
-  | Direct (_,cu) -> Future.chain ~pure:true cu fst
+let get_proof { opaque_val = prfs; opaque_dir = odp } = function
+  | Direct (_,cu) -> Future.chain cu fst
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
-        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        then Future.chain (snd (Int.Map.find i prfs)) fst
         else !get_opaque dp i in
-      Future.chain ~pure:true pt (fun c ->
+      Future.chain pt (fun c ->
         force_constr (List.fold_right subst_substituted l (from_val c)))
  
 module FMap = Future.UUIDMap
 
-let a_constr = Future.from_val (Term.mkRel 1)
+let a_constr = Future.from_val (mkRel 1)
 let a_univ = Future.from_val Univ.ContextSet.empty
 let a_discharge : cooking_info list = []
 
-let dump (otab,_) =
-  let n = Int.Map.cardinal otab in
+let dump { opaque_val = otab; opaque_len = n } =
   let opaque_table = Array.make n a_constr in
   let univ_table = Array.make n a_univ in
   let disch_table = Array.make n a_discharge in
   let f2t_map = ref FMap.empty in
   Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 ~greedy:true cu in
+    let c, u = Future.split2 cu in
     Future.sink u;
     Future.sink c;
     opaque_table.(n) <- c;
-- 
cgit v1.2.3