aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/nativenorm.ml
blob: 5142af3567cdca71a49fa1d696b487511f3b20ac (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
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
(************************************************************************)
(*  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        *)
(************************************************************************)
open Pp
open CErrors
open Term
open Vars
open Environ
open Reduction
open Univ
open Declarations
open Names
open Inductive
open Util
open Nativecode
open Nativevalues
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration

(** This module implements normalization by evaluation to OCaml code *)

exception Find_at of int

let invert_tag cst tag reloc_tbl =
  try
    for j = 0 to Array.length reloc_tbl - 1 do
      let tagj,arity = reloc_tbl.(j) in
      if Int.equal tag tagj && (cst && Int.equal arity 0 || not(cst || Int.equal arity 0)) then
	raise (Find_at j)
      else ()
    done;raise Not_found
  with Find_at j -> (j+1)

let decompose_prod env t =
  let (name,dom,codom as res) = destProd (whd_all env t) in
  match name with
  | Anonymous -> (Name (id_of_string "x"),dom,codom)
  | _ -> res

let app_type env c =
  let t = whd_all env c in
  try destApp t with DestKO -> (t,[||])

 
let find_rectype_a env c =
  let (t, l) = app_type env c in
  match kind_of_term t with
  | Ind ind -> (ind, l)
  | _ -> raise Not_found

(* Instantiate inductives and parameters in constructor type *)

let type_constructor mind mib u typ params =
  let s = ind_subst mind mib u in
  let ctyp = substl s typ in
  let nparams = Array.length params in
  if Int.equal nparams 0 then ctyp
  else
    let _,ctyp = decompose_prod_n nparams ctyp in   
    substl (List.rev (Array.to_list params)) ctyp

let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
  let mib,mip = lookup_mind_specif env ind in
  let nparams = mib.mind_nparams in
  let params = Array.sub allargs 0 nparams in
  try
    if const then
      let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
      retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
    else
      raise Not_found
  with Not_found ->
  let i = invert_tag const tag mip.mind_reloc_tbl in
  let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
  (mkApp(mkConstructU((ind,i),u), params), ctyp)
 

let construct_of_constr const env tag typ =
  let t, l = app_type env typ in
  match kind_of_term t with
  | Ind (ind,u) -> 
      construct_of_constr_notnative const env tag ind u l
  | _ -> assert false

let construct_of_constr_const env tag typ = 
  fst (construct_of_constr true env tag typ)

let construct_of_constr_block = construct_of_constr false

let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
  let rtbl = mip.mind_reloc_tbl in
  (* [build_one_branch i cty] construit le type de la ieme branche (commence
     a 0) et les lambda correspondant aux realargs *)
  let build_one_branch i cty =
    let typi = type_constructor mind mib u cty params in
    let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
    let decl = List.map (on_snd EConstr.Unsafe.to_constr) decl in
    let indapp = EConstr.Unsafe.to_constr indapp in
    let decl_with_letin,_ = decompose_prod_assum typi in
    let ind,cargs = find_rectype_a env indapp in
    let nparams = Array.length params in
    let carity = snd (rtbl.(i)) in
    let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
    let codom =
      let ndecl = List.length decl in
      let papp = mkApp(lift ndecl p,crealargs) in
      if dep then
	let cstr = ith_constructor_of_inductive (fst ind) (i+1) in
        let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
	let params = Array.map (lift ndecl) params in
	let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in
	mkApp(papp,[|dep_cstr|])
      else papp
    in 
    decl, decl_with_letin, codom
  in Array.mapi build_one_branch mip.mind_nf_lc

let build_case_type dep p realargs c = 
  if dep then mkApp(mkApp(p, realargs), [|c|])
  else mkApp(p, realargs)

(* TODO move this function *)
let type_of_rel env n =
  env |> lookup_rel n |> RelDecl.get_type |> lift n

let type_of_prop = mkSort type1_sort

let type_of_sort s = 
  match s with
  | Prop _ -> type_of_prop
  | Type u -> mkType (Univ.super u)

let type_of_var env id =
  let open Context.Named.Declaration in
  try env |> lookup_named id |> get_type
  with Not_found ->
    anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.")

let sort_of_product env domsort rangsort =
  match (domsort, rangsort) with
    (* Product rule (s,Prop,Prop) *)
    | (_,       Prop Null)  -> rangsort
    (* Product rule (Prop/Set,Set,Set) *)
    | (Prop _,  Prop Pos) -> rangsort
    (* Product rule (Type,Set,?) *)
    | (Type u1, Prop Pos) ->
        if is_impredicative_set env then
          (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
          rangsort
        else
          (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
          Type (sup u1 type0_univ)
    (* Product rule (Prop,Type_i,Type_i) *)
    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
    (* Product rule (Prop,Type_i,Type_i) *)
    | (Prop Null, Type _)  -> rangsort
    (* Product rule (Type_i,Type_i,Type_i) *)
    | (Type u1, Type u2) -> Type (sup u1 u2)

(* normalisation of values *)

let branch_of_switch lvl ans bs = 
  let tbl = ans.asw_reloc in
  let branch i = 
    let tag,arity = tbl.(i) in
    let ci = 
      if Int.equal arity 0 then mk_const tag
      else mk_block tag (mk_rels_accu lvl arity) in
    bs ci in
  Array.init (Array.length tbl) branch

let rec nf_val env sigma v typ =
  match kind_of_value v with
  | Vaccu accu -> nf_accu env sigma accu
  | Vfun f -> 
      let lvl = nb_rel env in
      let name,dom,codom = 
	try decompose_prod env typ
	with DestKO ->
          CErrors.anomaly
            (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
      in
      let env = push_rel (LocalAssum (name,dom)) env in
      let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
      mkLambda(name,dom,body)
  | Vconst n -> construct_of_constr_const env n typ
  | Vblock b ->
      let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
      let args = nf_bargs env sigma b ctyp in
      mkApp(capp,args)

and nf_type env sigma v =
  match kind_of_value v with
  | Vaccu accu -> nf_accu env sigma accu
  | _ -> assert false

and nf_type_sort env sigma v =
  match kind_of_value v with
  | Vaccu accu -> 
      let t,s = nf_accu_type env sigma accu in
      let s = try destSort s with DestKO -> assert false in
      t, s
  | _ -> assert false

and nf_accu env sigma accu =
  let atom = atom_of_accu accu in
  if Int.equal (accu_nargs accu) 0 then nf_atom env sigma atom
  else
    let a,typ = nf_atom_type env sigma atom in
    let _, args = nf_args env sigma accu typ in
    mkApp(a,Array.of_list args)

and nf_accu_type env sigma accu =
  let atom = atom_of_accu accu in
  if Int.equal (accu_nargs accu) 0 then nf_atom_type env sigma atom
  else
    let a,typ = nf_atom_type env sigma atom in
    let t, args = nf_args env sigma accu typ in
    mkApp(a,Array.of_list args), t

and nf_args env sigma accu t =
  let aux arg (t,l) = 
    let _,dom,codom =
      try decompose_prod env t with
	DestKO ->
	CErrors.anomaly
	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
    in
    let c = nf_val env sigma arg dom in
    (subst1 c codom, c::l)
  in
  let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in
  t, List.rev l

and nf_bargs env sigma b t =
  let t = ref t in
  let len = block_size b in
  Array.init len
    (fun i ->
      let _,dom,codom =
	try decompose_prod env !t with
	  DestKO ->
	  CErrors.anomaly
	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
      in
      let c = nf_val env sigma (block_field b i) dom in
      t := subst1 c codom; c)

and nf_atom env sigma atom =
  match atom with
  | Arel i -> mkRel (nb_rel env - i)
  | Aconstant cst -> mkConstU cst
  | Aind ind -> mkIndU ind
  | Asort s -> mkSort s
  | Avar id -> mkVar id
  | Aprod(n,dom,codom) ->
      let dom = nf_type env sigma dom in
      let vn = mk_rel_accu (nb_rel env) in
      let env = push_rel (LocalAssum (n,dom)) env in
      let codom = nf_type env sigma (codom vn) in
      mkProd(n,dom,codom)
  | Ameta (mv,_) -> mkMeta mv
  | Aevar (ev,_) -> mkEvar ev
  | Aproj(p,c) ->
      let c = nf_accu env sigma c in
	mkProj(Projection.make p true,c)
  | _ -> fst (nf_atom_type env sigma atom)

and nf_atom_type env sigma atom =
  match atom with
  | Arel i ->
      let n = (nb_rel env - i) in
      mkRel n, type_of_rel env n
  | Aconstant cst ->
      mkConstU cst, Typeops.type_of_constant_in env cst
  | Aind ind ->
      mkIndU ind, Inductiveops.type_of_inductive env ind
  | Asort s ->
      mkSort s, type_of_sort s
  | Avar id ->
      mkVar id, type_of_var env id
  | Acase(ans,accu,p,bs) ->
      let a,ta = nf_accu_type env sigma accu in
      let ((mind,_),u as ind),allargs = find_rectype_a env ta in
      let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
      let nparams = mib.mind_nparams in
      let params,realargs = Array.chop nparams allargs in
      let pT = 
	hnf_prod_applist env 
	  (Inductiveops.type_of_inductive env ind) (Array.to_list params) in
      let pT = whd_all env pT in
      let dep, p = nf_predicate env sigma ind mip params p pT in
      (* Calcul du type des branches *)
      let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
      (* calcul des branches *)
      let bsw = branch_of_switch (nb_rel env) ans bs in
      let mkbranch i v =
       let decl,decl_with_letin,codom = btypes.(i) in
       let b = nf_val (Termops.push_rels_assum decl env) sigma v codom in
        Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
      in 
      let branchs = Array.mapi mkbranch bsw in
      let tcase = build_case_type dep p realargs a in
      let ci = ans.asw_ci in
      mkCase(ci, p, a, branchs), tcase 
  | Afix(tt,ft,rp,s) ->
      let tt = Array.map (fun t -> nf_type env sigma t) tt in
      let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in
      let lvl = nb_rel env in
      let nbfix = Array.length ft in
      let fargs = mk_rels_accu lvl (Array.length ft) in
      (* Third argument of the tuple is ignored by push_rec_types *)
      let env = push_rec_types (name,tt,[||]) env in
      (* We lift here because the types of arguments (in tt) will be evaluated
         in an environment where the fixpoints have been pushed *)
      let norm_body i v = nf_val env sigma (napply v fargs) (lift nbfix tt.(i)) in
      let ft = Array.mapi norm_body ft in
      mkFix((rp,s),(name,tt,ft)), tt.(s)
  | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) ->
      let tt = Array.map (nf_type env sigma) tt in
      let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in
      let lvl = nb_rel env in
      let fargs = mk_rels_accu lvl (Array.length ft) in
      let env = push_rec_types (name,tt,[||]) env in
      let ft = Array.mapi (fun i v -> nf_val env sigma (napply v fargs) tt.(i)) ft in
      mkCoFix(s,(name,tt,ft)), tt.(s)
  | Aprod(n,dom,codom) ->
      let dom,s1 = nf_type_sort env sigma dom in
      let vn = mk_rel_accu (nb_rel env) in
      let env = push_rel (LocalAssum (n,dom)) env in
      let codom,s2 = nf_type_sort env sigma (codom vn) in
      mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
  | Aevar(ev,ty) ->
     let ty = nf_type env sigma ty in
     mkEvar ev, ty
  | Ameta(mv,ty) ->
     let ty = nf_type env sigma ty in
     mkMeta mv, ty
  | Aproj(p,c) ->
      let c,tc = nf_accu_type env sigma c in
      let cj = make_judge c tc in
      let uj = Typeops.judge_of_projection env (Projection.make p true) cj in
      uj.uj_val, uj.uj_type


and  nf_predicate env sigma ind mip params v pT =
  match kind_of_value v, kind_of_term pT with
  | Vfun f, Prod _ ->
      let k = nb_rel env in
      let vb = f (mk_rel_accu k) in
      let name,dom,codom =
	try decompose_prod env pT with
	  DestKO ->
	  CErrors.anomaly
	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
      in
      let dep,body = 
	nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
      dep, mkLambda(name,dom,body)
  | Vfun f, _ -> 
      let k = nb_rel env in
      let vb = f (mk_rel_accu k) in
      let name = Name (id_of_string "c") in
      let n = mip.mind_nrealargs in
      let rargs = Array.init n (fun i -> mkRel (n-i)) in
      let params = if Int.equal n 0 then params else Array.map (lift n) params in
      let dom = mkApp(mkIndU ind,Array.append params rargs) in
      let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
      true, mkLambda(name,dom,body)
  | _, _ -> false, nf_type env sigma v

let evars_of_evar_map sigma =
  { Nativelambda.evars_val = Evd.existential_opt_value sigma;
    Nativelambda.evars_typ = Evd.existential_type sigma;
    Nativelambda.evars_metas = Evd.meta_type sigma }

let native_norm env sigma c ty =
  let c = EConstr.Unsafe.to_constr c in
  let ty = EConstr.Unsafe.to_constr ty in
  if Coq_config.no_native_compiler then
    user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
  else
  let penv = Environ.pre_env env in
  (*
  Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
  Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
  *)
  let ml_filename, prefix = Nativelib.get_ml_filename () in
  let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in
  match Nativelib.compile ml_filename code with
    | true, fn ->
        if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
        let t0 = Sys.time () in
        Nativelib.call_linker ~fatal:true prefix fn (Some upd);
        let t1 = Sys.time () in
        let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
        let res = nf_val env sigma !Nativelib.rt1 ty in
        let t2 = Sys.time () in
        let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
        EConstr.of_constr res
    | _ -> anomaly (Pp.str "Compilation failure.") 

let native_conv_generic pb sigma t =
  Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t

let native_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma)
    ~catch_incon:true ~pb env sigma t1 t2