1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Univ
open Term
open Mod_subst
type work_list = (Instance.t * Id.t array) Cmap.t *
(Instance.t * Id.t array) Mindmap.t
type cooking_info = {
modlist : work_list;
abstract : Context.named_context in_universe_context }
type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
| Direct of cooking_info list * proofterm
| NoIndirect of substitution list * proofterm
(* hooks *)
let default_get_opaque dp _ =
Errors.error
("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
let default_get_univ dp _ =
Errors.error
("Cannot access universe constraints of opaque proofs in library " ^
DirPath.to_string dp)
let default_mk_indirect _ = None
let default_join_indirect_local_opaque _ _ = ()
let default_join_indirect_local_univ _ _ = ()
let get_opaque = ref default_get_opaque
let get_univ = ref default_get_univ
let join_indirect_local_opaque = ref default_join_indirect_local_opaque
let join_indirect_local_univ = ref default_join_indirect_local_univ
let mk_indirect = ref default_mk_indirect
let set_indirect_opaque_accessor f = (get_opaque := f)
let set_indirect_univ_accessor f = (get_univ := f)
let set_indirect_creator f = (mk_indirect := f)
let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
let set_join_indirect_local_univ f = join_indirect_local_univ := f
let reset_indirect_creator () = mk_indirect := default_mk_indirect
(* /hooks *)
let create cu = Direct ([],cu)
let turn_indirect o = match o with
| Indirect _
| NoIndirect _ -> Errors.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
match !mk_indirect (d,cu) with
| None -> Future.sink cu; NoIndirect([],cu)
| Some (dp,i) -> Indirect ([],dp,i)
let subst_opaque sub = function
| Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
| NoIndirect (s,uc) -> NoIndirect (sub::s,uc)
| Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque")
let iter_direct_opaque f = function
| Indirect _
| NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
| Direct (d,cu) ->
Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
let discharge_direct_opaque ~cook_constr ci = function
| Indirect _
| NoIndirect _ -> Errors.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))
let join_opaque = function
| Direct (_,cu) -> ignore(Future.join cu)
| NoIndirect (_,cu) -> ignore(Future.join cu)
| Indirect (_,dp,i) ->
!join_indirect_local_opaque dp i;
!join_indirect_local_univ dp i
let force_proof = function
| Direct (_,cu) ->
fst(Future.force cu)
| NoIndirect (l,cu) ->
let c, _ = Future.force cu in
force_constr (List.fold_right subst_substituted l (from_val c))
| Indirect (l,dp,i) ->
let c = Future.force (!get_opaque dp i) in
force_constr (List.fold_right subst_substituted l (from_val c))
let force_constraints = function
| Direct (_,cu)
| NoIndirect(_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
match !get_univ dp i with
| None -> Univ.ContextSet.empty
| Some u -> Future.force u
let get_constraints = function
| Direct (_,cu)
| NoIndirect(_,cu) -> Some(Future.chain ~pure:true cu snd)
| Indirect (_,dp,i) -> !get_univ dp i
let get_proof = function
| Direct (_,cu) -> Future.chain ~pure:true cu fst
| NoIndirect(l,cu) ->
Future.chain ~pure:true cu (fun (c,_) ->
force_constr (List.fold_right subst_substituted l (from_val c)))
| Indirect (l,dp,i) ->
Future.chain ~pure:true (!get_opaque dp i) (fun c ->
force_constr (List.fold_right subst_substituted l (from_val c)))
|
