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
|
(*i $Id$ i*)
open Pp
open Util
open Names
open Term
open Sign
open Declarations
open Instantiate
open Environ
open Reduction
(*s Cooking the constants. *)
type modification_action = ABSTRACT | ERASE
type 'a modification =
| NOT_OCCUR
| DO_ABSTRACT of 'a * modification_action list
| DO_REPLACE
type work_alist = (global_reference * global_reference modification) list
type recipe = {
d_from : section_path;
d_abstract : identifier list;
d_modlist : (global_reference * global_reference modification) list }
let interp_modif absfun oper (oper',modif) cl =
let rec interprec = function
| ([], cl) ->
(match oper' with
| ConstRef sp -> mkConst (sp,Array.of_list cl)
| ConstructRef sp -> mkMutConstruct (sp,Array.of_list cl)
| IndRef sp -> mkMutInd (sp,Array.of_list cl))
| (ERASE::tlm, c::cl) -> interprec (tlm,cl)
| (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
| _ -> assert false
in
interprec (modif,cl)
let modify_opers replfun absfun oper_alist =
let failure () =
anomalylabstrm "generic__modify_opers"
[< 'sTR"An oper which was never supposed to appear has just appeared" ;
'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC;
'sTR"report this error," ; 'sPC ;
'sTR"Or you are using a user-written tactic which calls" ; 'sPC ;
'sTR"generic__modify_opers, in which case the user-written code" ;
'sPC ; 'sTR"is broken - this function is an internal system" ;
'sPC ; 'sTR"for internal system use only" >]
in
let rec substrec c =
let op, cl = splay_constr c in
let cl' = Array.map substrec cl in
match op with
(* Hack pour le sp dans l'annotation du Cases *)
| OpMutCase (n,(spi,a,b,c,d) as oper) ->
(try
match List.assoc (IndRef spi) oper_alist with
| DO_ABSTRACT (IndRef spi',_) ->
gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
| _ -> raise Not_found
with
| Not_found -> gather_constr (op,cl'))
| OpMutInd spi ->
(try
(match List.assoc (IndRef spi) oper_alist with
| NOT_OCCUR -> failure ()
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun (IndRef spi) (oper',modif)
(Array.to_list cl')
| DO_REPLACE -> assert false)
with
| Not_found -> mkMutInd (spi,cl'))
| OpMutConstruct spi ->
(try
(match List.assoc (ConstructRef spi) oper_alist with
| NOT_OCCUR -> failure ()
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun (ConstructRef spi) (oper',modif)
(Array.to_list cl')
| DO_REPLACE -> assert false)
with
| Not_found -> mkMutConstruct (spi,cl'))
| OpConst sp ->
(try
(match List.assoc (ConstRef sp) oper_alist with
| NOT_OCCUR -> failure ()
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun (ConstRef sp) (oper',modif)
(Array.to_list cl')
| DO_REPLACE -> substrec (replfun (sp,cl')))
with
| Not_found -> mkConst (sp,cl'))
| _ -> gather_constr (op, cl')
in
if oper_alist = [] then fun x -> x else substrec
let expmod_constr oldenv modlist c =
let sigma = Evd.empty in
let simpfun =
if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
let expfun cst =
try
constant_value oldenv cst
with NotEvaluableConst Opaque ->
let (sp,_) = cst in
errorlabstrm "expmod_constr"
[< 'sTR"Cannot unfold the value of ";
'sTR(string_of_path sp); 'sPC;
'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
'sTR"and then require that theorems which use them"; 'sPC;
'sTR"be transparent" >];
in
let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
match kind_of_term c' with
| IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
| _ -> simpfun c'
let expmod_type oldenv modlist c =
type_app (expmod_constr oldenv modlist) c
let abstract_constant ids_to_abs hyps (body,typ) =
let abstract_once ((hyps,body,typ) as sofar) id =
match hyps with
| [] ->
sofar
| (hyp,c,t as decl)::rest ->
if hyp <> id then
sofar
else
let body' = match body with
| None -> None
| Some c -> Some (mkNamedLambda_or_LetIn decl c)
in
let typ' = mkNamedProd_or_LetIn decl typ in
(rest, body', typ')
in
let (_,body',typ') =
List.fold_left abstract_once (hyps,body,typ) ids_to_abs in
(body',typ')
let cook_constant env r =
let cb = lookup_constant r.d_from env in
let typ = expmod_type env r.d_modlist cb.const_type in
let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
let hyps = map_named_context (expmod_constr env r.d_modlist) cb.const_hyps in
abstract_constant r.d_abstract hyps (body,typ)
|
