diff options
| author | letouzey | 2011-11-28 16:10:46 +0000 |
|---|---|---|
| committer | letouzey | 2011-11-28 16:10:46 +0000 |
| commit | 4f523e7d25ed22b6e41cabf1c2bd091afc0fde7f (patch) | |
| tree | 641577f5554c30485dbd0ce076002f890fbe0ef3 /plugins/extraction/common.mli | |
| parent | 98279dced2c1e01c89d3c79cb2a9f03e5dcd82e1 (diff) | |
Extraction: Richer patterns in matchs as proposed by P.N. Tollitte
The MLcase has notably changed:
- No more case_info in it, but only a type annotation
- No more "one branch for one constructor", but rather a sequence
of patterns. Earlier "full" pattern correspond to pattern Pusual.
Patterns Pwild and Prel allow to encode optimized matchs without
hacks as earlier. Other pattern situations aren't used (yet)
by extraction, but only by P.N Tollitte's code.
A MLtuple constructor has been introduced. It isn't used by
the extraction for the moment, but only but P.N. Tollitte's code.
Many pretty-print functions in ocaml.ml and other have been reorganized
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 1d8fe77ab3..02a496bec1 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -22,7 +22,17 @@ val fnl2 : unit -> std_ppcmds val space_if : bool -> std_ppcmds val pp_par : bool -> std_ppcmds -> std_ppcmds + +(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *) val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds + +(** Same as [pp_apply], but with also protection of the head by parenthesis *) +val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds + +val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds +val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds + val pr_binding : identifier list -> std_ppcmds val rename_id : identifier -> Idset.t -> identifier |