From f57a38bb53dc06cef1cee78c60946aa5e6d3cf0b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 16 Apr 2010 14:12:57 +0000
Subject: Extraction: ad-hoc identifier type with annotations for reductions

 * An inductive constructor Dummy instead of a constant dummy_name
 * The Tmp constructor indicates that the corresponding MLlam or
   MLletin is extraction-specific and can be reduced if possible
 * When inlining a glob (for instance a recursor), we tag some
   lambdas as reducible. In (nat_rect Fo Fs n), the head lams of
   Fo and Fs are treated this way, in order for the recursive call
   inside nat_rect to be correctly pushed as deeper as possible.
 * This way, we can stop allowing by default linear beta/let
   reduction even under binders (can be activated back via
   Set Extraction Flag).
 * Btw, fix the strange definition of non_stricts for (x y).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/mlutil.mli | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'plugins/extraction/mlutil.mli')

diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 9c5feac826..7fd8006a59 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -69,22 +69,24 @@ val type_expunge : abbrev_map -> ml_type -> ml_type
 val isDummy : ml_type -> bool
 val isKill : sign -> bool
 
-val case_expunge : signature -> ml_ast -> identifier list * ml_ast
-val term_expunge : signature -> identifier list * ml_ast -> ml_ast
+val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast
+val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
 
 
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
 
-val anonymous : identifier
+val anonymous_name : identifier
 val dummy_name : identifier
 val id_of_name : name -> identifier
+val id_of_mlid : ml_ident -> identifier
+val tmp_id : ml_ident -> ml_ident
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
     the list [idn;...;id1] and the term [t]. *)
 
-val collect_lams : ml_ast -> identifier list * ml_ast
-val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
+val collect_lams : ml_ast -> ml_ident list * ml_ast
+val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast
 val nb_lams : ml_ast -> int
 
 val dummy_lams : ml_ast -> int -> ml_ast
-- 
cgit v1.2.3