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: mlutil.mli 14786 2011-12-10 12:55:19Z letouzey $ i*)
11 open OcamlExtractionTable
15 (*s Utility functions over ML types with meta. *)
17 val reset_meta_count : unit -> unit
18 val new_meta : 'a -> ml_type
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
24 val instantiation : ml_schema -> ml_type
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
30 val generalizable : ml_ast -> bool
32 (*s ML type environment. *)
38 (* get the n-th more recently entered schema and instantiate it. *)
39 val get : t -> int -> ml_type
41 (* Adding a type in an environment, after generalizing free meta *)
42 val push_gen : t -> ml_type -> t
44 (* Adding a type with no [Tvar] *)
45 val push_type : t -> ml_type -> t
47 (* Adding a type with no [Tvar] nor [Tmeta] *)
48 val push_std_type : t -> ml_type -> t
51 (*s Utility functions over ML types without meta *)
53 val type_mem_kn : NUri.uri -> ml_type -> bool
55 val type_maxvar : ml_type -> int
57 val type_decomp : ml_type -> ml_type list * ml_type
58 val type_recomp : ml_type list * ml_type -> ml_type
60 val var2var' : ml_type -> ml_type
62 type 'status abbrev_map =
63 'status -> NReference.reference -> ('status * ml_type) option
66 #status as 'status -> 'status abbrev_map -> ml_type -> 'status * ml_type
67 val type_simpl : #status as 'status -> ml_type -> 'status * ml_type
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
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
77 val isDummy : ml_type -> bool
78 val isKill : sign -> bool
80 val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast
81 val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
84 (*s Special identifiers. [dummy_name] is to be used for dead code
85 and will be printed as [_] in concrete (Caml) code. *)
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
93 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
94 the list [idn;...;id1] and the term [t]. *)
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
104 val eta_args_sign : int -> signature -> ml_ast list
106 (*s Utility functions over ML terms. *)
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
118 val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
120 val normalize : ml_ast -> ml_ast
121 val optimize_fix : ml_ast -> ml_ast
122 val inline : NReference.reference -> ml_ast -> bool
125 val branch_as_fun : ml_type list -> ml_branch -> ml_ast
126 val branch_as_cst : ml_branch -> ml_ast
128 (* Classification of signatures *)
132 | NonLogicalSig (* at least a [Keep] *)
133 | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
134 | SafeLogicalSig (* only [Kill Ktype] *)
136 val sign_kind : signature -> sign_kind
138 val sign_no_final_keeps : signature -> signature