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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(************************************************************************)
(* 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 Term
open Mod_subst
type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
type cooking_info = { modlist : work_list; abstract : Context.named_context }
(** [constr_substituted] are [constr] with possibly pending
substitutions of kernel names. *)
type constr_substituted = constr substituted
let from_val = from_val
let force = force subst_mps
let subst_constr_subst = subst_substituted
(** Opaque proof terms might be in some external tables.
The [force_opaque] function below allows to access these tables,
this might trigger the read of some extra parts of .vo files.
In the [Indirect] case, we accumulate "manually" a substitution
list, the younger one coming first. Nota: no [Direct] constructor
should end in a .vo, this is checked by coqchk.
*)
type proofterm = (constr * Univ.constraints) Future.computation
type lazy_constr =
(* subst, lib, index *)
| Indirect of substitution list * DirPath.t * int
(* opaque in section or interactive session *)
| Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation
(* TODO : this hcons function could probably be improved (for instance
hash the dir_path in the Indirect case) *)
let subst_lazy_constr sub = function
| Direct ([],cu) ->
Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
subst_constr_subst sub c, u))
| Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged")
| Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
let iter_direct_lazy_constr f = function
| Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr")
| Direct (d,cu) ->
Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u))
let discharge_direct_lazy_constr modlist abstract f = function
| Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr")
| Direct (d,cu) ->
Direct ({ modlist; abstract }::d,
Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
from_val (f (force c)), u))
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
let force_lazy_constr = function
| Direct (_,c) -> Future.force c
| Indirect (l,dp,i) ->
let c = Future.force (!get_opaque dp i) in
List.fold_right subst_constr_subst l (from_val c),
Future.force
(Option.default
(Future.from_val Univ.empty_constraint)
(!get_univ dp i))
let join_lazy_constr = function
| Direct (_,c) -> ignore(Future.force c)
| Indirect (_,dp,i) ->
!join_indirect_local_opaque dp i;
!join_indirect_local_univ dp i
let turn_indirect lc = match lc with
| Indirect _ ->
Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
| Direct (d,cu) ->
let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) ->
(* this constr_substituted shouldn't have been substituted yet *)
assert (fst (Mod_subst.repr_substituted c) == None);
hcons_constr (force c),u) in
match !mk_indirect (d,cu) with
| None -> lc
| Some (dp,i) -> Indirect ([],dp,i)
let force_opaque lc =
let c, _u = force_lazy_constr lc in force c
let force_opaque_w_constraints lc =
let c, u = force_lazy_constr lc in force c, u
let get_opaque_future_constraints lc = match lc with
| Indirect (_,dp,i) -> !get_univ dp i
| Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu))
let get_opaque_futures lc = match lc with
| Indirect _ -> assert false
| Direct (_,cu) ->
let cu =
Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in
Future.split2 ~greedy:true cu
let opaque_from_val cu =
Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u))
|
