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
135
136
137
138
139
140
141
142
143
144
145
146
|
(* $Id$ *)
open Pp
open Util
open Names
open Term
open Sign
open Evd
open Declarations
open Environ
let is_id_inst inst =
let is_id (id,c) = match kind_of_term c with
| IsVar id' -> id = id'
| _ -> false
in
List.for_all is_id inst
let instantiate sign c args =
let inst = instantiate_named_context sign args in
if is_id_inst inst then
c
else
replace_vars inst c
(* Vérifier que les instances des let-in sont compatibles ?? *)
let instantiate_sign_including_let sign args =
let rec instrec = function
| ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
| ([],[]) -> []
| ([],_) | (_,[]) ->
anomaly "Signature and its instance do not match"
in
instrec (sign,args)
let instantiate_evar sign c args =
let inst = instantiate_sign_including_let sign args in
if is_id_inst inst then
c
else
replace_vars inst c
let instantiate_constr sign c args =
if Options.immediate_discharge then
c
else
let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
instantiate sign c args
let instantiate_type sign tty args =
type_app (fun c -> instantiate_constr sign c args) tty
(* Constants. *)
(* constant_type gives the type of a constant *)
let constant_type env sigma (sp,args) =
let cb = lookup_constant sp env in
(* TODO: check args *)
(* instantiate_type cb.const_hyps *) cb.const_type (*(Array.to_list args)*)
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
let constant_value env (sp,args) =
let cb = lookup_constant sp env in
if cb.const_opaque then raise (NotEvaluableConst Opaque);
match cb.const_body with
| Some body ->
instantiate_constr cb.const_hyps body (Array.to_list args)
| None ->
raise (NotEvaluableConst NoBody)
let constant_opt_value env cst =
try Some (constant_value env cst)
with NotEvaluableConst _ -> None
(* Existentials. *)
let name_of_existential n = id_of_string ("?" ^ string_of_int n)
let existential_type sigma (n,args) =
let info = Evd.map sigma n in
let hyps = info.evar_hyps in
(* TODO: check args [this comment was in Typeops] *)
instantiate_evar hyps info.evar_concl (Array.to_list args)
exception NotInstantiatedEvar
let existential_value sigma (n,args) =
let info = Evd.map sigma n in
let hyps = info.evar_hyps in
match evar_body info with
| Evar_defined c ->
instantiate_evar hyps c (Array.to_list args)
| Evar_empty ->
raise NotInstantiatedEvar
let existential_opt_value sigma ev =
try Some (existential_value sigma ev)
with NotInstantiatedEvar -> None
type evaluable_reference =
| EvalConst of constant
| EvalVar of identifier
| EvalRel of int
| EvalEvar of existential
let mkEvalRef = function
| EvalConst cst -> mkConst cst
| EvalVar id -> mkVar id
| EvalRel n -> mkRel n
| EvalEvar ev -> mkEvar ev
let isEvalRef c = match kind_of_term c with
| IsConst _ | IsVar _ | IsRel _ | IsEvar _ -> true
| _ -> false
let destEvalRef c = match kind_of_term c with
| IsConst cst -> EvalConst cst
| IsVar id -> EvalVar id
| IsRel n -> EvalRel n
| IsEvar ev -> EvalEvar ev
| _ -> anomaly "Not an evaluable reference"
let evaluable_reference sigma env = function
| EvalConst (sp,_) -> evaluable_constant env sp
| EvalVar id -> evaluable_named_decl env id
| EvalRel n -> evaluable_rel_decl env n
| EvalEvar (ev,_) -> Evd.is_defined sigma ev
let reference_opt_value sigma env = function
| EvalConst cst -> constant_opt_value env cst
| EvalVar id -> lookup_named_value id env
| EvalRel n -> lookup_rel_value n env
| EvalEvar ev -> existential_opt_value sigma ev
exception NotEvaluable
let reference_value sigma env c =
match reference_opt_value sigma env c with
| None -> raise NotEvaluable
| Some d -> d
|
