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
|
(************************************************************************)
(* 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
(** [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 lazy_constr =
| Indirect of substitution list * DirPath.t * int (* lib,index *)
| Direct of constr_substituted (* opaque in section or interactive session *)
(* TODO : this hcons function could probably be improved (for instance
hash the dir_path in the Indirect case) *)
let hcons_lazy_constr = function
| Direct c -> Direct (from_val (hcons_constr (force c)))
| Indirect _ as lc -> lc
let subst_lazy_constr sub = function
| Direct cs -> Direct (subst_constr_subst sub cs)
| Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
let default_get_opaque dp _ =
Errors.error
("Cannot access an opaque term in library " ^ DirPath.to_string dp)
let default_mk_opaque _ = None
let get_opaque = ref default_get_opaque
let mk_opaque = ref default_mk_opaque
let set_indirect_opaque_accessor f = (get_opaque := f)
let set_indirect_opaque_creator f = (mk_opaque := f)
let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque)
let force_lazy_constr = function
| Direct c -> c
| Indirect (l,dp,i) ->
List.fold_right subst_constr_subst l (from_val (!get_opaque dp i))
let turn_indirect lc = match lc with
| Indirect _ ->
Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
| Direct c ->
(* this constr_substituted shouldn't have been substituted yet *)
assert (fst (Mod_subst.repr_substituted c) == None);
match !mk_opaque (force c) with
| None -> lc
| Some (dp,i) -> Indirect ([],dp,i)
let force_opaque lc = force (force_lazy_constr lc)
let opaque_from_val c = Direct (from_val c)
|
