blob: 55d80d84675850011b98156838e038ec50d6fd92 (
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
|
(***********************************************************************)
(* 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_control
open Pp
open System
open Util
open Names
open Vernacinterp
open Mlimport
open Miniml
open Genpp
(*s Utility functions. *)
let open_par = function true -> [< 'sTR"(" >] | false -> [< >]
let close_par = function true -> [< 'sTR")" >] | false -> [< >]
(* uncurry_list : ('a -> std_pcmds) -> 'a list -> std_ppcmds
* formats a list [x1;...;xn] in its uncurried form (x1,...,xn). *)
let uncurry_list f = function
[] -> [< >]
| [x] -> [< (f x) >]
| xl -> [< 'sTR"(" ;
prlist_with_sep (fun () -> [< 'sTR", " >]) (fun x -> (f x)) xl ;
'sTR")"
>]
let uncurry_list2 f = function
[] -> [< >]
| [x] -> [< (f x) >]
| xl -> [< 'sTR"(" ;
hOV 0 [< prlist_with_sep
(fun () -> [< 'sTR"," ; 'sPC >])
(fun x -> (f x)) xl ;
'sTR")" >]
>]
type extraction_params = {
needed : identifier list;
expand : identifier list;
expansion : bool;
exact : bool
}
let list_ids =
List.map (function (VARG_IDENTIFIER id) -> id | _ -> assert false)
let rec parse_rem op = function
VARG_STRING "noopt" :: r ->
parse_rem
{ needed = op.needed; expand = op.expand;
expansion = false; exact = op.exact } r
| VARG_STRING "exact" :: r ->
parse_rem
{ needed = op.needed; expand = op.expand;
expansion = op.expansion; exact = true } r
| VARG_STRING "expand" :: VARG_VARGLIST l :: r ->
parse_rem { needed = op.needed; expand = op.expand @ list_ids l;
expansion = op.expansion; exact = op.exact } r
| [] -> op
| _ -> assert false
let parse_param = function
VARG_VARGLIST l :: r ->
parse_rem { needed = list_ids l; expand = [];
expansion = true; exact = false } r
| _ -> assert false
module type ExtractionParams = sig
val opt : extraction_params -> ml_decl list -> ml_decl list
val suffixe : string
val cofix : bool
val pp_of_env : ml_decl list -> std_ppcmds
module Renaming : Extraction.Renaming
end
module Make = functor (M : ExtractionParams) -> struct
module Translation = Extraction.Make(M.Renaming)
let change_names =
map_succeed
(fun id -> try Extraction.get_global_name id
with Anomaly _ -> failwith "caught")
let exact prm env =
let keep = function
| Dtype il ->
List.exists (fun (_,id,_) -> List.mem id prm.needed) il
| Dabbrev (id,_,_) -> List.mem id prm.needed
| Dglob (id,_) -> List.mem id prm.needed
in
map_succeed
(fun d -> if not (keep d) then failwith "caught" else d) env
let pp cicenv prm =
let mlenv = Translation.extract M.cofix cicenv in
let needed' = change_names prm.needed in
let expand' = change_names prm.expand in
let prm' =
{ needed = needed' ; expand = expand' ;
expansion = prm.expansion ; exact = prm.exact }
in
let env = M.opt prm' mlenv in
let env = if prm'.exact then exact prm' env else env in
M.pp_of_env env
let pp_recursive prm =
let gl = List.map (Nametab.sp_of_id CCI) prm.needed in
let cicenv = Close_env.close gl in
pp cicenv prm
let write file strm =
let chan = open_trapping_failure open_out file M.suffixe in
let ft = with_output_to chan in
(try pP_with ft strm ; pp_flush_with ft ()
with e -> pp_flush_with ft () ; close_out chan; raise e);
close_out chan
let write_extraction_file file prm =
(* TODO: comment tester qu'il n'y a pas de section ouverte et
pemettre pour autant la compilation (donc une section
particuliere qui est le module) if Lib.cwd() <> [] then
errorlabstrm "Genpp.Pp_to_file.write_extraction_file" [< 'sTR
"There are still open sections !" >]; *)
let strm = pp_recursive prm in
write file strm
let write_extraction_module m =
let cicenv = Close_env.module_env m in
let idl = List.map (Environ.id_of_global (Global.env())) cicenv in
let prm =
{ needed = idl; expand = []; expansion = false; exact = true } in
let strm = pp cicenv prm in
let file = string_of_id m in
write file strm
end
|
