blob: 376b069d0d22e5647d28eed07f814e28b9818a48 (
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
|
(***********************************************************************)
(* 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*)
(*s This module defines the generic part of the code production, as a
functor [Make] taking extraction parameters as argument (of type
[ExtractionParams]), including a renaming functor (of type
[Extraction.Renaming]) and returning a module to output the
code. *)
open Pp
open Names
open Miniml
open Vernacinterp
(*s Some utility functions, used in instance modules ([Caml], [Ocaml] and
[Haskell]). *)
val open_par : bool -> std_ppcmds
val close_par : bool -> std_ppcmds
val uncurry_list : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val uncurry_list2 : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
(*s Extraction parameters parsed on the command line. *)
type extraction_params = {
needed : identifier list; (*r constants to keep *)
expand : identifier list; (*r constants to expand *)
expansion : bool; (*r do we expand *)
exact : bool (*r without recursivity *)
}
val parse_param : vernac_arg list -> extraction_params
(*s The whole bunch of extraction parameters has the following signature. *)
module type ExtractionParams =
sig
(* optimisation function *)
val opt : extraction_params -> ml_decl list -> ml_decl list
(* file suffix *)
val suffixe : string
(* co-inductive types are (not) allowed *)
val cofix : bool
(* pretty-print function *)
val pp_of_env : ml_decl list -> std_ppcmds
(* the renaming functions *)
module Renaming : Extraction.Renaming
end
(*s The functor itself. *)
module Make : functor (M : ExtractionParams) ->
sig
module Translation : Extraction.Translation
val pp_recursive : extraction_params -> std_ppcmds
val write_extraction_file : string -> extraction_params -> unit
val write_extraction_module : identifier -> unit
end
|
