matita/components/ng_extraction/ocamlExtractionTable.mli

   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 (************************************************************************)
   8
   9 (*i $Id: table.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 open Coq
  12 open Miniml
  13
  14 type info
  15 type db
  16
  17 class type g_status =
  18  object ('self)
  19   method ocaml_extraction_db: db
  20   method get_info: info * 'self
  21  end
  22
  23 class virtual status :
  24  object ('self)
  25   inherit g_status
  26   inherit NCic.status
  27   method set_ocaml_extraction_db: db -> 'self
  28   method set_ocaml_extraction_status: #g_status -> 'self
  29  end
  30
  31 val refresh_uri_in_info:
  32  refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
  33  refresh_uri:(NUri.uri -> NUri.uri) ->
  34   info -> info
  35
  36 val set_keywords : Idset.t -> unit
  37
  38 val register_infos: db -> info -> db
  39
  40 val to_be_included : (#status as 'status) -> NUri.uri -> 'status * bool
  41
  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
  45
  46 val current_baseuri: #status -> string
  47
  48 val add_term : (#status as 'status) -> NReference.reference -> ml_decl -> 'status
  49 val lookup_term : #status -> NReference.reference -> ml_decl
  50
  51 val add_type: (#status as 'status) -> NReference.reference -> ml_schema -> 'status
  52 val lookup_type : #status -> NReference.reference -> ml_schema
  53
  54 val add_ind : (#status as 'status) -> ?dummy:bool -> NUri.uri -> ml_ind -> 'status
  55 val lookup_ind : #status -> NUri.uri -> ml_ind
  56
  57 val add_global_ids: (#status as 'status) -> string -> 'status
  58 val get_global_ids : #status -> Idset.t
  59
  60 val add_name_for_reference:
  61  (#status as 'status) -> NReference.reference -> string -> 'status
  62 val name_of_reference : #status -> NReference.reference -> string
  63
  64 val add_modname: (#status as 'status) -> string -> 'status
  65 val get_modnames : #status -> Idset.t
  66
  67 val add_modname_for_filename:
  68  (#status as 'status) -> string -> string -> 'status
  69 val modname_of_filename : #status -> string -> string
  70
  71 val guess_projection:
  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
  77
  78 val type_expand : unit -> bool
  79
  80 type opt_flag =
  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 *)
  92
  93 val optims :  unit -> opt_flag