aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
blob: 7c3b8e60f0bb0b238006bf269bb68b72b3d03e00 (plain)
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
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(*i $Id$ i*)

open Pp
open Util
open Names
open Term
open Sign
open Declarations
open Environ
open Reduction

(*s Cooking the constants. *)

type 'a modification =
  | NOT_OCCUR
  | DO_ABSTRACT of 'a * constr array
  | DO_REPLACE of constant_body

type work_list =
    (constant * constant modification) list
    * (inductive * inductive modification) list
    * (constructor * constructor modification) list

type recipe = {
  d_from : constant_body;
  d_abstract : identifier list;
  d_modlist : work_list }

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 (constl,indl,cstrl) =
  let rec substrec c =
    let c' = map_constr substrec c in
    match kind_of_term c' with
      | Case (ci,p,t,br) ->
	  (try
	     match List.assoc ci.ci_ind indl with
	       | DO_ABSTRACT (ind,abs_vars) ->
		   let n' = Array.length abs_vars + ci.ci_npar in
                   let ci' = { ci with
                               ci_ind = ind;
                               ci_npar = n' } in
		   mkCase (ci',p,t,br)
	       | _ -> raise Not_found
	   with
	     | Not_found -> c')

      | Ind spi ->
	  (try
	     (match List.assoc spi indl with
		| NOT_OCCUR -> failure ()
		| DO_ABSTRACT (oper',abs_vars) ->
                    mkApp (mkInd oper', abs_vars)
		| DO_REPLACE _ -> assert false)
	   with 
	     | Not_found -> c')

      | Construct spi ->
	  (try
	     (match List.assoc spi cstrl with
		| NOT_OCCUR -> failure ()
		| DO_ABSTRACT (oper',abs_vars) ->
		    mkApp (mkConstruct oper', abs_vars)
		| DO_REPLACE _ -> assert false)
	   with 
	     | Not_found -> c')

      | Const kn ->
	  (try
	     (match List.assoc kn constl with
		| NOT_OCCUR -> failure ()
		| DO_ABSTRACT (oper',abs_vars) ->
		    mkApp (mkConst oper', abs_vars)
		| DO_REPLACE cb -> substrec (replfun (kn,cb)))
	   with 
	     | Not_found -> c')
  
    | _ -> c'
  in 
  if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec

let expmod_constr modlist c =
  let simpfun = 
    if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
  let expfun (kn,cb) = 
    if cb.const_opaque then
      errorlabstrm "expmod_constr"
	(str"Cannot unfold the value of " ++
        str(string_of_kn kn) ++ spc () ++
        str"You cannot declare local lemmas as being opaque" ++ spc () ++
        str"and then require that theorems which use them" ++ spc () ++
        str"be transparent");
    match cb.const_body with
      | Some body -> Declarations.force body
      | None -> assert false
  in
  let c' = modify_opers expfun modlist c in
  match kind_of_term c' with
    | Cast (value,typ) -> mkCast (simpfun value,simpfun typ)
    | _ -> simpfun c'

let expmod_type modlist c =
  type_app (expmod_constr modlist) c

let abstract_constant ids_to_abs hyps (body,typ) =
  let abstract_once_typ ((hyps,typ) as sofar) id =
    match hyps with
      | (hyp,c,t as decl)::rest when hyp = id ->
	  let typ' = mkNamedProd_wo_LetIn decl typ in
	  (rest, typ')
      | _ -> 
	  sofar
  in
  let abstract_once_body ((hyps,body) as sofar) id =
    match hyps with
      | (hyp,c,t as decl)::rest when hyp = id ->
	  let body' = mkNamedLambda_or_LetIn decl body in
	  (rest, body')
      | _ -> 
	  sofar
  in
  let (_,typ') =
    List.fold_left abstract_once_typ (hyps,typ) ids_to_abs 
  in
  let body' = match body with
      None -> None
    | Some l_body -> 
	Some (Declarations.from_val
		(let body = Declarations.force l_body in
		 let (_,body') = 
		   List.fold_left abstract_once_body (hyps,body) ids_to_abs
		 in
		   body'))
  in
    (body',typ')

let cook_constant env r =
  let cb = r.d_from in
  let typ = expmod_type r.d_modlist cb.const_type in
  let body = 
    option_app 
      (fun lconstr -> 
	 Declarations.from_val 
	   (expmod_constr r.d_modlist (Declarations.force lconstr))) 
      cb.const_body
  in
  let hyps =
    Sign.fold_named_context
      (fun d ctxt ->
        Sign.add_named_decl
          (map_named_declaration (expmod_constr r.d_modlist) d)
          ctxt)
      cb.const_hyps
      ~init:empty_named_context in
  let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
  (body, typ, cb.const_constraints, cb.const_opaque)