diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 50 |
1 files changed, 22 insertions, 28 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index aaf2d0c3..856a481e 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - (*s Target language for extraction: a core ML called MiniML. *) open Pp @@ -73,8 +71,7 @@ type ml_ind_packet = { ip_logical : bool; ip_sign : signature; ip_vars : identifier list; - ip_types : (ml_type list) array; - mutable ip_optim_id_ok : bool option + ip_types : (ml_type list) array } (* [ip_nparams] contains the number of parameters. *) @@ -99,28 +96,17 @@ type ml_ident = | Tmp of identifier (** We now store some typing information on constructors - and cases to avoid type-unsafe optimisations. - For cases, we also store the set of branches to merge - in a common pattern, either "_ -> c" or "x -> f x" + and cases to avoid type-unsafe optimisations. This will be + either the type of the applied constructor or the type + of the head of the match. *) -type constructor_info = { - c_kind : inductive_kind; - c_typs : ml_type list; -} - -type branch_same = - | BranchNone - | BranchFun of Intset.t - | BranchCst of Intset.t +(** Nota : the constructor [MLtuple] and the extension of [MLcase] + to general patterns have been proposed by P.N. Tollitte for + his Relation Extraction plugin. [MLtuple] is currently not + used by the main extraction, as well as deep patterns. *) -type match_info = { - m_kind : inductive_kind; - m_typs : ml_type list; - m_same : branch_same -} - -type ml_branch = global_reference * ml_ident list * ml_ast +type ml_branch = ml_ident list * ml_pattern * ml_ast and ml_ast = | MLrel of int @@ -128,24 +114,32 @@ and ml_ast = | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference - | MLcons of constructor_info * global_reference * ml_ast list - | MLcase of match_info * ml_ast * ml_branch array + | MLcons of ml_type * global_reference * ml_ast list + | MLtuple of ml_ast list + | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy | MLaxiom | MLmagic of ml_ast +and ml_pattern = + | Pcons of global_reference * ml_pattern list + | Ptuple of ml_pattern list + | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *) + | Pwild + | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + (*s ML declarations. *) type ml_decl = - | Dind of kernel_name * ml_ind + | Dind of mutual_inductive * ml_ind | Dtype of global_reference * identifier list * ml_type | Dterm of global_reference * ml_ast * ml_type | Dfix of global_reference array * ml_ast array * ml_type array type ml_spec = - | Sind of kernel_name * ml_ind + | Sind of mutual_inductive * ml_ind | Stype of global_reference * identifier list * ml_type option | Sval of global_reference * ml_type |