1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
9 (*i $Id: table.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
19 method ocaml_extraction_db: db
20 method get_info: info * 'self
23 class virtual status :
27 method set_ocaml_extraction_db: db -> 'self
28 method set_ocaml_extraction_status: #g_status -> 'self
31 val refresh_uri_in_info:
32 refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
33 refresh_uri:(NUri.uri -> NUri.uri) ->
36 val set_keywords : Idset.t -> unit
38 val register_infos: db -> info -> db
40 val to_be_included : #status as 'status -> NUri.uri -> 'status * bool
42 val open_file: #status as 'status -> baseuri:string -> string -> 'status
43 val print_ppcmds : #status -> in_ml:bool -> std_ppcmds -> unit
44 val close_file: #status as 'status -> 'status
46 val current_baseuri: #status -> string
48 val add_term : #status as 'status -> NReference.reference -> ml_decl -> 'status
49 val lookup_term : #status -> NReference.reference -> ml_decl
51 val add_type: #status as 'status -> NReference.reference -> ml_schema -> 'status
52 val lookup_type : #status -> NReference.reference -> ml_schema
54 val add_ind : #status as 'status -> ?dummy:bool -> NUri.uri -> ml_ind -> 'status
55 val lookup_ind : #status -> NUri.uri -> ml_ind
57 val add_global_ids: #status as 'status -> string -> 'status
58 val get_global_ids : #status -> Idset.t
60 val add_name_for_reference:
61 #status as 'status -> NReference.reference -> string -> 'status
62 val name_of_reference : #status -> NReference.reference -> string
64 val add_modname: #status as 'status -> string -> 'status
65 val get_modnames : #status -> Idset.t
67 val add_modname_for_filename:
68 #status as 'status -> string -> string -> 'status
69 val modname_of_filename : #status -> string -> string
72 #status as 'status -> NUri.uri -> int -> 'status
73 val confirm_projection:
74 #status as 'status -> NReference.reference -> 'status
75 val is_projection : #status -> NReference.reference -> bool
76 val projection_arity : #status -> NReference.reference -> int
78 val type_expand : unit -> bool
81 { opt_kill_dum : bool; (* 1 *)
82 opt_fix_fun : bool; (* 2 *)
83 opt_case_iot : bool; (* 4 *)
84 opt_case_idr : bool; (* 8 *)
85 opt_case_idg : bool; (* 16 *)
86 opt_case_cst : bool; (* 32 *)
87 opt_case_fun : bool; (* 64 *)
88 opt_case_app : bool; (* 128 *)
89 opt_let_app : bool; (* 256 *)
90 opt_lin_let : bool; (* 512 *)
91 opt_lin_beta : bool } (* 1024 *)
93 val optims : unit -> opt_flag