aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
blob: c971ed29939188e7b20f77e0a349fa2aaa25593a (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \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 work_list = identifier array Cmap.t * identifier array Mindmap.t

let pop_dirpath p = match repr_dirpath p with
  | [] -> anomaly "dirpath_prefix: empty dirpath"
  | _::l -> make_dirpath l

let pop_mind kn =
  let (mp,dir,l) = Names.repr_mind kn in
  Names.make_mind mp (pop_dirpath dir) l

let pop_con con =
  let (mp,dir,l) = Names.repr_con con in
  Names.make_con mp (pop_dirpath dir) l

type my_global_reference =
  | ConstRef of constant
  | IndRef of inductive
  | ConstructRef of constructor

let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)

let clear_cooking_sharing () = Hashtbl.clear cache

let share r (cstl,knl) =
  try Hashtbl.find cache r
  with Not_found ->
  let f,l =
    match r with
    | IndRef (kn,i) ->
	mkInd (pop_mind kn,i), Mindmap.find kn knl
    | ConstructRef ((kn,i),j) ->
	mkConstruct ((pop_mind kn,i),j), Mindmap.find kn knl
    | ConstRef cst ->
	mkConst (pop_con cst), Cmap.find cst cstl in
  let c = mkApp (f, Array.map mkVar l) in
  Hashtbl.add cache r c;
  (* has raised Not_found if not in work_list *)
  c

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

let empty_modlist = (Cmap.empty, Mindmap.empty)

let expmod_constr modlist c =
  let rec substrec c =
    match kind_of_term c with
      | Case (ci,p,t,br) ->
	  map_constr substrec (mkCase (update_case_info ci modlist,p,t,br))

      | Ind ind ->
	  (try
	    share (IndRef ind) modlist
	   with
	    | Not_found -> map_constr substrec c)

      | Construct cstr ->
	  (try
	    share (ConstructRef cstr) modlist
	   with
	    | Not_found -> map_constr substrec c)

      | Const cst ->
	  (try
	    share (ConstRef cst) modlist
	   with
	    | Not_found -> map_constr substrec c)

  | _ -> map_constr substrec c

  in
  if modlist = empty_modlist then c
  else under_outer_cast nf_betaiota (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 = {
  d_from : constant_body;
  d_abstract : named_context;
  d_modlist : work_list }

let on_body f =
  Option.map (fun c -> Declarations.from_val (f (Declarations.force c)))

let cook_constant env r =
  let cb = r.d_from in
  let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
  let body =
    on_body (fun c ->
      abstract_constant_body (expmod_constr r.d_modlist c) hyps)
      cb.const_body in
  let typ = match cb.const_type with
    | NonPolymorphicType t ->
	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
	NonPolymorphicType typ
    | PolymorphicArity (ctx,s) ->
	let t = mkArity (ctx,Type s.poly_level) in
	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
	let j = make_judge (force (Option.get body)) typ in
	Typeops.make_polymorphic_if_constant_for_ind env j
  in
  let boxed = Cemitcodes.is_boxed cb.const_body_code in
  (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)