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
|
(*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_list =
(section_path * section_path modification) list
* (inductive_path * inductive_path modification) list
* (constructor_path * constructor_path modification) list
type recipe = {
d_from : section_path;
d_abstract : identifier list;
d_modlist : work_list }
let interp_modif absfun mkfun (sp,modif) cl =
let rec interprec = function
| ([], cl) -> mkfun (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, Array.to_list cl)
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" >]
let modify_opers replfun absfun (constl,indl,cstrl) =
let rec substrec c =
let op, cl = splay_constr c in
let cl' = Array.map substrec cl in
match op with
| OpMutCase (n,(spi,a,b,c,d) as oper) ->
(try
match List.assoc spi indl with
| DO_ABSTRACT (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 spi indl with
| NOT_OCCUR -> failure ()
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun mkMutInd (oper',modif) cl'
| DO_REPLACE -> assert false)
with
| Not_found -> mkMutInd (spi,cl'))
| OpMutConstruct spi ->
(try
(match List.assoc spi cstrl with
| NOT_OCCUR -> failure ()
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun mkMutConstruct (oper',modif) cl'
| DO_REPLACE -> assert false)
with
| Not_found -> mkMutConstruct (spi,cl'))
| OpConst sp ->
(try
(match List.assoc sp constl with
| NOT_OCCUR -> failure ()
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun mkConst (oper',modif) cl'
| DO_REPLACE -> substrec (replfun (sp,cl')))
with
| Not_found -> mkConst (sp,cl'))
| _ -> gather_constr (op, cl')
in
if (constl,indl,cstrl) = ([],[],[]) 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
| (hyp,c,t as decl)::rest when hyp = id ->
let body' = match body with
| None -> None
| Some c -> Some (mkNamedLambda_or_LetIn decl c)
in
let typ' = mkNamedProd_wo_LetIn decl typ in
(rest, body', typ')
| _ ->
sofar
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 = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in
abstract_constant r.d_abstract hyps (body,typ)
|
