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

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6973bb454..579f42df5 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -121,11 +121,11 @@ let rec pp_expr par env args =
         pp_expr par env (stl @ args) f
     | MLlam _ as a ->
       	let fl,a' = collect_lams a in
-	let fl,env' = push_vars fl env in
+	let fl,env' = push_vars (List.map id_of_mlid fl) env in
 	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
 	apply (pp_par par' st)
     | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id] env in
+	let i,env' = push_vars [id_of_mlid id] env in
 	let pp_id = pr_id (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
@@ -166,7 +166,7 @@ let rec pp_expr par env args =
 
 and pp_pat env factors pv =
   let pp_one_pat (name,ids,t) =
-    let ids,env' = push_vars (List.rev ids) env in
+    let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
     let par = expr_needs_par t in
     hov 2 (pp_global Cons name ++
 	   (match ids with
@@ -204,7 +204,7 @@ and pp_fix par env i (ids,bl) args =
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
-  let bl,env' = push_vars bl env in
+  let bl,env' = push_vars (List.map id_of_mlid bl) env in
   (f ++ pr_binding (List.rev bl) ++
      str " =" ++ fnl () ++ str "  " ++
      hov 2 (pp_expr false env' [] t'))