aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
blob: 23a578d99319afe95e4f664ef1fbe8ddc905bad4 (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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml
   as part of the rebuilding of Coq around a purely functional
   abstract type-checker, Nov 1999 *)

(* This module implements kernel-level discharching of local
   declarations over global constants and inductive types *)

open CErrors
open Util
open Names
open Term
open Constr
open Declarations
open Univ

module NamedDecl = Context.Named.Declaration

(*s Cooking the constants. *)

let pop_dirpath p = match DirPath.repr p with
  | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.")
  | _::l -> DirPath.make l

let pop_mind kn =
  let (mp,dir,l) = MutInd.repr3 kn in
  MutInd.make3 mp (pop_dirpath dir) l

let pop_con con =
  let (mp,dir,l) = Constant.repr3 con in
  Constant.make3 mp (pop_dirpath dir) l

type my_global_reference =
  | ConstRef of Constant.t
  | IndRef of inductive
  | ConstructRef of constructor

module RefHash =
struct
  type t = my_global_reference
  let equal gr1 gr2 = match gr1, gr2 with
  | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
  | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
  | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
  | _ -> false
  open Hashset.Combine
  let hash = function
  | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
  | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
  | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
end

module RefTable = Hashtbl.Make(RefHash)

let instantiate_my_gr gr u =
  match gr with
  | ConstRef c -> mkConstU (c, u)
  | IndRef i -> mkIndU (i, u)
  | ConstructRef c -> mkConstructU (c, u)

let share cache r (cstl,knl) =
  try RefTable.find cache r
  with Not_found ->
  let f,(u,l) =
    match r with
    | IndRef (kn,i) ->
	IndRef (pop_mind kn,i), Mindmap.find kn knl
    | ConstructRef ((kn,i),j) ->
	ConstructRef ((pop_mind kn,i),j), Mindmap.find kn knl
    | ConstRef cst ->
	ConstRef (pop_con cst), Cmap.find cst cstl in
  let c = (f, (u, Array.map mkVar l)) in
  RefTable.add cache r c;
  c

let share_univs cache r u l =
  let r', (u', args) = share cache r l in
    mkApp (instantiate_my_gr r' (Instance.append u' u), args)

let update_case_info cache ci modlist =
  try
    let ind, n =
      match share cache (IndRef ci.ci_ind) modlist with
      | (IndRef f,(u,l)) -> (f, Array.length l)
      | _ -> assert false in
    { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
  with Not_found ->
    ci

let is_empty_modlist (cm, mm) =
  Cmap.is_empty cm && Mindmap.is_empty mm

let expmod_constr cache modlist c =
  let share_univs = share_univs cache in
  let update_case_info = update_case_info cache in
  let rec substrec c =
    match kind c with
      | Case (ci,p,t,br) ->
	  Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))

      | Ind (ind,u) ->
	  (try
	    share_univs (IndRef ind) u modlist
	   with
	    | Not_found -> Constr.map substrec c)

      | Construct (cstr,u) ->
	  (try
	     share_univs (ConstructRef cstr) u modlist
	   with
	    | Not_found -> Constr.map substrec c)

      | Const (cst,u) ->
	  (try
	    share_univs (ConstRef cst) u modlist
	   with
	    | Not_found -> Constr.map substrec c)

      | Proj (p, c') ->
          (try 
	     let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
	     let make c = Projection.make c (Projection.unfolded p) in
	     match kind p' with
	     | Const (p',_) -> mkProj (make p', substrec c')
	     | App (f, args) -> 
	       (match kind f with 
	       | Const (p', _) -> mkProj (make p', substrec c')
	       | _ -> assert false)
	     | _ -> assert false
	   with Not_found -> Constr.map substrec c)

  | _ -> Constr.map substrec c

  in
  if is_empty_modlist modlist then c
  else substrec c

let abstract_constant_type =
   List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)

let abstract_constant_body =
  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)

type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool

type result = {
  cook_body : constant_def;
  cook_type : types;
  cook_proj : projection_body option;
  cook_universes : constant_universes;
  cook_inline : inline;
  cook_context : Context.Named.t option;
}

let on_body ml hy f = function
  | Undef _ as x -> x
  | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
  | OpaqueDef o ->
    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
                 { Opaqueproof.modlist = ml; abstract = hy } o)

let expmod_constr_subst cache modlist subst c =
  let subst = Univ.make_instance_subst subst in
  let c = expmod_constr cache modlist c in
    Vars.subst_univs_level_constr subst c

let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
  let cache = RefTable.create 13 in
  let expmod = expmod_constr_subst cache modlist subst in
  let hyps = Context.Named.map expmod vars in
  abstract_constant_body (expmod c) hyps

let lift_univs cb subst auctx0 =
  match cb.const_universes with
  | Monomorphic_const ctx ->
    assert (AUContext.is_empty auctx0);
    subst, (Monomorphic_const ctx)
  | Polymorphic_const auctx ->
    (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
        context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
        and another abstract context relative to the former context
        [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
        construct the lifted abstract universe context
        [0 ... n - 1 n ... n + m - 1 |=
          C{0, ... n - 1} ∪
          C'{0, ..., n - 1, n, ..., n + m - 1} ]
        together with the instance
        [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
    *)
    if (Univ.Instance.is_empty subst) then
      (** Still need to take the union for the constraints between globals *)
      subst, (Polymorphic_const (AUContext.union auctx0 auctx))
    else
      let ainst = Univ.make_abstract_instance auctx in
      let subst = Instance.append subst ainst in
      let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
      subst, (Polymorphic_const (AUContext.union auctx0 auctx'))

let cook_constant ~hcons env { from = cb; info } =
  let { Opaqueproof.modlist; abstract } = info in
  let cache = RefTable.create 13 in
  let abstract, usubst, abs_ctx = abstract in
  let usubst, univs = lift_univs cb usubst abs_ctx in
  let expmod = expmod_constr_subst cache modlist usubst in
  let hyps = Context.Named.map expmod abstract in
  let map c =
    let c = abstract_constant_body (expmod c) hyps in
    if hcons then Constr.hcons c else c
  in
  let body = on_body modlist (hyps, usubst, abs_ctx)
    map
    cb.const_body
  in
  let const_hyps =
    Context.Named.fold_outside (fun decl hyps ->
      List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
		  hyps)
      hyps ~init:cb.const_hyps in
  let typ = abstract_constant_type (expmod cb.const_type) hyps in
  let projection pb =
    let c' = abstract_constant_body (expmod pb.proj_body) hyps in
    let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
    let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in
    let ((mind, _), _), n' =
      try 
	let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
	  match kind c' with
	  | App (f,l) -> (destInd f, Array.length l)
	  | Ind ind -> ind, 0
	  | _ -> assert false 
      with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
    in 
    let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
      { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
	proj_eta = etab, etat;
	proj_type = ty'; proj_body = c' }
  in
  {
    cook_body = body;
    cook_type = typ;
    cook_proj = Option.map projection cb.const_proj;
    cook_universes = univs;
    cook_inline = cb.const_inline_code;
    cook_context = Some const_hyps;
  }

(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)

let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c