matita/components/ng_extraction/mlutil.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: mlutil.mli 14786 2011-12-10 12:55:19Z letouzey $ i*)
  10
  11 open OcamlExtractionTable
  12 open Miniml
  13 open Coq
  14
  15 (*s Utility functions over ML types with meta. *)
  16
  17 val reset_meta_count : unit -> unit
  18 val new_meta : 'a -> ml_type
  19
  20 val type_subst : int -> ml_type -> ml_type -> ml_type
  21 val type_subst_list : ml_type list -> ml_type -> ml_type
  22 val type_subst_vect : ml_type array -> ml_type -> ml_type
  23
  24 val instantiation : ml_schema -> ml_type
  25
  26 val needs_magic : ml_type * ml_type -> bool
  27 val put_magic_if : bool -> ml_ast -> ml_ast
  28 val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
  29
  30 val generalizable : ml_ast -> bool
  31
  32 (*s ML type environment. *)
  33
  34 module Mlenv : sig
  35   type t
  36   val empty : t
  37
  38   (* get the n-th more recently entered schema and instantiate it. *)
  39   val get : t -> int -> ml_type
  40
  41   (* Adding a type in an environment, after generalizing free meta *)
  42   val push_gen : t -> ml_type -> t
  43
  44   (* Adding a type with no [Tvar] *)
  45   val push_type : t -> ml_type -> t
  46
  47   (* Adding a type with no [Tvar] nor [Tmeta] *)
  48   val push_std_type : t -> ml_type -> t
  49 end
  50
  51 (*s Utility functions over ML types without meta *)
  52
  53 val type_mem_kn : NUri.uri -> ml_type -> bool
  54
  55 val type_maxvar : ml_type -> int
  56
  57 val type_decomp : ml_type -> ml_type list * ml_type
  58 val type_recomp : ml_type list * ml_type -> ml_type
  59
  60 val var2var' : ml_type -> ml_type
  61
  62 type 'status abbrev_map =
  63  'status -> NReference.reference -> ('status * ml_type) option
  64
  65 val type_expand :
  66  #status as 'status -> 'status abbrev_map -> ml_type -> 'status * ml_type
  67 val type_simpl : #status as 'status -> ml_type -> 'status * ml_type
  68 val type_to_sign :
  69  #status as 'status -> 'status abbrev_map -> ml_type -> 'status * sign
  70 val type_to_signature :
  71  #status as 'status -> 'status abbrev_map -> ml_type -> 'status * signature
  72 val type_expunge :
  73  #status as 'status -> 'status abbrev_map -> ml_type -> 'status * ml_type
  74 val type_expunge_from_sign :
  75  #status as 'status -> 'status abbrev_map -> signature -> ml_type -> 'status * ml_type
  76
  77 val isDummy : ml_type -> bool
  78 val isKill : sign -> bool
  79
  80 val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast
  81 val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
  82
  83
  84 (*s Special identifiers. [dummy_name] is to be used for dead code
  85     and will be printed as [_] in concrete (Caml) code. *)
  86
  87 val anonymous_name : identifier
  88 val dummy_name : identifier
  89 val id_of_name : string -> identifier
  90 val id_of_mlid : ml_ident -> identifier
  91 val tmp_id : ml_ident -> ml_ident
  92
  93 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
  94     the list [idn;...;id1] and the term [t]. *)
  95
  96 val collect_lams : ml_ast -> ml_ident list * ml_ast
  97 val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast
  98 val remove_n_lams : int -> ml_ast -> ml_ast
  99 val nb_lams : ml_ast -> int
 100 val named_lams : ml_ident list -> ml_ast -> ml_ast
 101 val dummy_lams : ml_ast -> int -> ml_ast
 102 val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
 103
 104 val eta_args_sign : int -> signature -> ml_ast list
 105
 106 (*s Utility functions over ML terms. *)
 107
 108 val mlapp : ml_ast -> ml_ast list -> ml_ast
 109 val ast_map : (ml_ast -> ml_ast) -> ml_ast -> ml_ast
 110 val ast_map_lift : (int -> ml_ast -> ml_ast) -> int -> ml_ast -> ml_ast
 111 val ast_iter : (ml_ast -> unit) -> ml_ast -> unit
 112 val ast_occurs : int -> ml_ast -> bool
 113 val ast_occurs_itvl : int -> int -> ml_ast -> bool
 114 val ast_lift : int -> ml_ast -> ml_ast
 115 val ast_pop : ml_ast -> ml_ast
 116 val ast_subst : ml_ast -> ml_ast -> ml_ast
 117
 118 val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
 119
 120 val normalize : ml_ast -> ml_ast
 121 val optimize_fix : ml_ast -> ml_ast
 122 val inline : NReference.reference -> ml_ast -> bool
 123
 124 exception Impossible
 125 val branch_as_fun : ml_type list -> ml_branch -> ml_ast
 126 val branch_as_cst : ml_branch -> ml_ast
 127
 128 (* Classification of signatures *)
 129
 130 type sign_kind =
 131   | EmptySig
 132   | NonLogicalSig (* at least a [Keep] *)
 133   | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
 134   | SafeLogicalSig (* only [Kill Ktype] *)
 135
 136 val sign_kind : signature -> sign_kind
 137
 138 val sign_no_final_keeps : signature -> signature