summaryrefslogtreecommitdiff
path: root/kernel/opaqueproof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/opaqueproof.ml')
-rw-r--r--kernel/opaqueproof.ml108
1 files changed, 61 insertions, 47 deletions
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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 20:45:54 +0000