diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/extraction/modutil.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/extraction/modutil.mli')
-rw-r--r-- | plugins/extraction/modutil.mli | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli new file mode 100644 index 00000000..8e04a368 --- /dev/null +++ b/plugins/extraction/modutil.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Declarations +open Environ +open Libnames +open Miniml +open Mod_subst + +(*s Functions upon ML modules. *) + +val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool +val struct_type_search : (ml_type -> bool) -> ml_structure -> bool + +type do_ref = global_reference -> unit + +val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit +val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit + +val signature_of_structure : ml_structure -> ml_signature + +val msid_of_mt : ml_module_type -> module_path + +val get_decl_in_structure : global_reference -> ml_structure -> ml_decl + +(* Some transformations of ML terms. [optimize_struct] simplify + all beta redexes (when the argument does not occur, it is just + thrown away; when it occurs exactly once it is substituted; otherwise + a let-in redex is created for clarity) and iota redexes, plus some other + optimizations. The first argument is the list of objects we want to appear. +*) + +val optimize_struct : global_reference list -> ml_structure -> ml_structure |