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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: redexpr.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
open Pp
open Util
open Names
open Term
open Declarations
open Libnames
open Rawterm
open Reductionops
open Tacred
open Closure
open RedFlags
open Libobject
(* call by value normalisation function using the virtual machine *)
let cbv_vm env _ c =
let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
Vnorm.cbv_vm env c ctyp
let set_strategy_one ref l =
let k =
match ref with
| EvalConstRef sp -> ConstKey sp
| EvalVarRef id -> VarKey id in
Conv_oracle.set_strategy k l;
match k,l with
ConstKey sp, Conv_oracle.Opaque ->
Csymtable.set_opaque_const sp
| ConstKey sp, _ ->
let cb = Global.lookup_constant sp in
if cb.const_body <> None & cb.const_opaque then
errorlabstrm "set_transparent_const"
(str "Cannot make" ++ spc () ++
Nametab.pr_global_env Idset.empty (ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.");
Csymtable.set_transparent_const sp
| _ -> ()
let cache_strategy (_,str) =
List.iter
(fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
str
let subst_strategy (_,subs,(local,obj)) =
local,
list_smartmap
(fun (k,ql as entry) ->
let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
if ql==ql' then entry else (k,ql'))
obj
let map_strategy f l =
let l' = List.fold_right
(fun (lev,ql) str ->
let ql' = List.fold_right
(fun q ql ->
match f q with
Some q' -> q' :: ql
| None -> ql) ql [] in
if ql'=[] then str else (lev,ql')::str) l [] in
if l'=[] then None else Some (false,l')
let export_strategy (local,obj) =
if local then None else
map_strategy (function
EvalVarRef _ -> None
| EvalConstRef _ as q -> Some q) obj
let classify_strategy (_,(local,_ as obj)) =
if local then Dispose else Substitute obj
let disch_ref ref =
match ref with
EvalConstRef c ->
let c' = Lib.discharge_con c in
if c==c' then Some ref else Some (EvalConstRef c')
| _ -> Some ref
let discharge_strategy (_,(local,obj)) =
if local then None else
map_strategy disch_ref obj
let (inStrategy,outStrategy) =
declare_object {(default_object "STRATEGY") with
cache_function = (fun (_,obj) -> cache_strategy obj);
load_function = (fun _ (_,obj) -> cache_strategy obj);
subst_function = subst_strategy;
discharge_function = discharge_strategy;
classify_function = classify_strategy;
export_function = export_strategy }
let set_strategy local str =
Lib.add_anonymous_leaf (inStrategy (local,str))
let _ =
Summary.declare_summary "Transparent constants and variables"
{ Summary.freeze_function = Conv_oracle.freeze;
Summary.unfreeze_function = Conv_oracle.unfreeze;
Summary.init_function = Conv_oracle.init;
Summary.survive_module = false;
Summary.survive_section = false }
(* Generic reduction: reduction functions used in reduction tactics *)
type red_expr = (constr, evaluable_global_reference) red_expr_gen
let make_flag_constant = function
| EvalVarRef id -> fVAR id
| EvalConstRef sp -> fCONST sp
let make_flag f =
let red = no_red in
let red = if f.rBeta then red_add red fBETA else red in
let red = if f.rIota then red_add red fIOTA else red in
let red = if f.rZeta then red_add red fZETA else red in
let red =
if f.rDelta then (* All but rConst *)
let red = red_add red fDELTA in
let red = red_add_transparent red (Conv_oracle.get_transp_state()) in
List.fold_right
(fun v red -> red_sub red (make_flag_constant v))
f.rConst red
else (* Only rConst *)
let red = red_add_transparent (red_add red fDELTA) all_opaque in
List.fold_right
(fun v red -> red_add red (make_flag_constant v))
f.rConst red
in red
let is_reference c =
try let _ref = global_of_constr c in true with _ -> false
let red_expr_tab = ref Stringmap.empty
let declare_red_expr s f =
try
let _ = Stringmap.find s !red_expr_tab in
error ("There is already a reduction expression of name "^s)
with Not_found ->
red_expr_tab := Stringmap.add s f !red_expr_tab
let out_arg = function
| ArgVar _ -> anomaly "Unevaluated or_var variable"
| ArgArg x -> x
let out_with_occurrences ((b,l),c) =
((b,List.map out_arg l), c)
let reduction_of_red_expr = function
| Red internal ->
if internal then (try_red_product,DEFAULTcast)
else (red_product,DEFAULTcast)
| Hnf -> (hnf_constr,DEFAULTcast)
| Simpl (Some (_,c as lp)) ->
(contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast)
| Simpl None -> (simpl,DEFAULTcast)
| Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
| Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
| Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
| Fold cl -> (fold_commands cl,DEFAULTcast)
| Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
| ExtraRedExpr s ->
(try (Stringmap.find s !red_expr_tab,DEFAULTcast)
with Not_found -> error("unknown user-defined reduction \""^s^"\""))
| CbvVm -> (cbv_vm ,VMcast)
|
