aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
blob: dffbb76c09c3533487277e63a0fd1cf4b4c0feb0 (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
(************************************************************************)
(*  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 KNmap.t

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

let pop_kn kn =
  let (mp,dir,l) = Names.repr_kn kn in
  Names.make_kn mp (dirpath_prefix dir) l

let pop_con con = 
  let (mp,dir,l) = Names.repr_con con in
  Names.make_con mp (dirpath_prefix 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_kn kn,i), KNmap.find kn knl
    | ConstructRef ((kn,i),j) -> 
	mkConstruct ((pop_kn kn,i),j), KNmap.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, KNmap.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 =
    abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in
  let boxed = Cemitcodes.is_boxed cb.const_body_code in
  (body, typ, cb.const_constraints, cb.const_opaque, boxed)