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

8 files changed, 83 insertions, 49 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 693c92ece..835337952 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -536,8 +536,9 @@ let rec extract_term env mle mlt c args =
 	       in extract_term env mle mlt d' []
 	   | [] ->
 	       let env' = push_rel_assum (Name id, t) env in
-	       let id, a = try check_default env t; id, new_meta()
-	       with NotDefault d -> dummy_name, Tdummy d
+	       let id, a =
+		 try check_default env t; Id id, new_meta()
+		 with NotDefault d -> Dummy, Tdummy d
 	       in
 	       let b = new_meta () in
 	       (* If [mlt] cannot be unified with an arrow type, then magic! *)
@@ -554,7 +555,7 @@ let rec extract_term env mle mlt c args =
 	  let c1' = extract_term env mle a c1 [] in
 	  (* The type of [c1'] is generalized and stored in [mle]. *)
 	  let mle' = Mlenv.push_gen mle a in
-	  MLletin (id, c1', extract_term env' mle' mlt c2 args')
+	  MLletin (Id id, c1', extract_term env' mle' mlt c2 args')
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
@@ -777,7 +778,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	  assert (br_size = 1);
 	  let (_,ids,e') = extract_branch 0 in
 	  assert (List.length ids = 1);
-	  MLletin (List.hd ids,a,e')
+	  MLletin (tmp_id (List.hd ids),a,e')
 	end
       else
 	(* Standard case: we apply [extract_branch]. *)
@@ -842,7 +843,7 @@ let extract_std_constant env kn body typ =
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
   (* The lambdas names. *)
-  let ids = List.map (fun (n,_) -> id_of_name n) rels in
+  let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in
   (* The according Coq environment. *)
   let env = push_rels_assum rels env in
   (* The real extraction: *)
@@ -877,7 +878,7 @@ let extract_constant env kn cb =
 	   | (Info,TypeScheme) ->
 	       if not (is_custom r) then add_info_axiom r;
 	       let n = type_scheme_nb_args env typ in
-	       let ids = iterate (fun l -> anonymous::l) n [] in
+	       let ids = iterate (fun l -> anonymous_name::l) n [] in
 	       Dtype (r, ids, Taxiom)
            | (Info,Default) ->
 	       if not (is_custom r) then add_info_axiom r;
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'))
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 91c60d205..00df1a98d 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -92,15 +92,20 @@ type ml_ind = {
 
 (*s ML terms. *)
 
+type ml_ident =
+  | Dummy
+  | Id of identifier
+  | Tmp of identifier
+
 type ml_ast =
   | MLrel    of int
   | MLapp    of ml_ast * ml_ast list
-  | MLlam    of identifier * ml_ast
-  | MLletin  of identifier * ml_ast * ml_ast
+  | MLlam    of ml_ident * ml_ast
+  | MLletin  of ml_ident * ml_ast * ml_ast
   | MLglob   of global_reference
   | MLcons   of inductive_info * global_reference * ml_ast list
   | MLcase   of (inductive_info*case_info) * ml_ast *
-      (global_reference * identifier list * ml_ast) array
+      (global_reference * ml_ident list * ml_ast) array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
   | MLdummy
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 2aee7b8a9..2cd1ee708 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -25,14 +25,27 @@ exception Impossible
 
 (*S Names operations. *)
 
-let anonymous = id_of_string "x"
+let anonymous_name = id_of_string "x"
 let dummy_name = id_of_string "_"
 
+let anonymous = Id anonymous_name
+
 let id_of_name = function
-  | Anonymous -> anonymous
-  | Name id when id = dummy_name -> anonymous
+  | Anonymous -> anonymous_name
+  | Name id when id = dummy_name -> anonymous_name
   | Name id -> id
 
+let id_of_mlid = function
+  | Dummy -> dummy_name
+  | Id id -> id
+  | Tmp id -> id
+
+let tmp_id = function
+  | Id id -> Tmp id
+  | a -> a
+
+let is_tmp = function Tmp _ -> true | _ -> false
+
 (*S Operations upon ML types (with meta). *)
 
 let meta_count = ref 0
@@ -298,7 +311,9 @@ let isKill = function Kill _ -> true | _ -> false
 
 let isDummy = function Tdummy _ -> true | _ -> false
 
-let sign_of_id i = if i = dummy_name then Kill Kother else Keep
+let sign_of_id = function
+  | Dummy -> Kill Kother
+  | _ -> Keep
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
@@ -536,14 +551,14 @@ let rec anonym_lams a = function
 
 let rec dummy_lams a = function
   | 0 -> a
-  | n -> dummy_lams (MLlam (dummy_name,a)) (pred n)
+  | n -> dummy_lams (MLlam (Dummy,a)) (pred n)
 
 (*s mixed according to a signature. *)
 
 let rec anonym_or_dummy_lams a = function
   | [] -> a
   | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
-  | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
+  | Kill _ :: s -> MLlam(Dummy, anonym_or_dummy_lams a s)
 
 (*S Operations concerning eta. *)
 
@@ -603,12 +618,19 @@ let rec linear_beta_red a t = match a,t with
 	     MLletin (id, a0, linear_beta_red a t))
   | _ -> MLapp (t, a)
 
+let rec tmp_head_lams = function
+  | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t)
+  | e -> e
+
 (*s Applies a substitution [s] of constants by their body, plus
-  linear beta reductions at modified positions. *)
+  linear beta reductions at modified positions.
+  Moreover, we mark some lambdas as suitable for later linear
+  reduction (this helps the inlining of recursors).
+*)
 
 let rec ast_glob_subst s t = match t with
   | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
-      let a = List.map (ast_glob_subst s) a in
+      let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
       (try linear_beta_red a (Refmap.find refe s)
        with Not_found -> MLapp (f, a))
   | MLglob ((ConstRef kn) as refe) ->
@@ -692,7 +714,7 @@ let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
   | l,[] -> l
   | i::ids, i'::ids' ->
-      (if i = dummy_name then i' else i) :: (merge_ids ids ids')
+      (if i = Dummy then i' else i) :: (merge_ids ids ids')
 
 let is_exn = function MLexn _ -> true | _ -> false
 
@@ -765,11 +787,13 @@ let rec simpl o = function
   | MLcase (i,e,br) ->
       let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
       simpl_case o i br (simpl o e)
+  | MLletin(Dummy,_,e) -> simpl o (ast_pop e)
   | MLletin(id,c,e) ->
-      let e = (simpl o e) in
+      let e = simpl o e in
       if
-	(id = dummy_name) || (is_atomic c) || (is_atomic e) ||
-	(let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let))
+	(is_atomic c) || (is_atomic e) ||
+	(let n = nb_occur_match e in
+	 (n = 0 || (n=1 && (is_tmp id || o.opt_lin_let))))
       then
 	simpl o (ast_subst c e)
       else
@@ -783,12 +807,12 @@ let rec simpl o = function
 
 and simpl_app o a = function
   | MLapp (f',a') -> simpl_app o (a'@a) f'
-  | MLlam (id,t) when id = dummy_name ->
+  | MLlam (Dummy,t) ->
       simpl o (MLapp (ast_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
       (match nb_occur_match t with
 	 | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
-	 | 1 when o.opt_lin_beta ->
+	 | 1 when (is_tmp id || o.opt_lin_beta) ->
 	     simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
 	 | _ ->
 	     let a' = List.map (ast_lift 1) (List.tl a) in
@@ -896,7 +920,7 @@ let eta_expansion_sign s (ids,c) =
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
 	in ids, MLapp (ast_lift (i-1) c, a)
     | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
-    | Kill _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
+    | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l
   in abs ids [] 1 s
 
 (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e]
@@ -920,7 +944,7 @@ let term_expunge s (ids,c) =
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
     if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then
-      MLlam (dummy_name, ast_lift 1 c)
+      MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
 (*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and
@@ -1083,10 +1107,6 @@ let rec non_stricts add cand = function
       pop 1 (non_stricts add cand t)
   | MLrel n ->
       List.filter ((<>) n) cand
-  | MLapp (MLrel n, _) ->
-      List.filter ((<>) n) cand
-	(* In [(x y)] we say that only x is strict. Cf [sig_rec]. We may *)
-	(* gain something if x is replaced by a function like a projection *)
   | MLapp (t,l)->
       let cand = non_stricts false cand t in
       List.fold_left (non_stricts false) cand l
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 9c5feac82..7fd8006a5 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
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 107b5368f..1c19bf06b 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -176,11 +176,12 @@ 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 = List.map id_of_mlid fl in
 	let fl,env' = push_vars 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
@@ -238,7 +239,8 @@ let rec pp_expr par env args =
 		 if List.exists (ast_occurs_itvl 1 n) a
 		 then raise NoRecord
 		 else
-		   let ids,env' = push_vars (List.rev ids) env in
+		   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env
+		   in
 		   (pp_apply
 		      (pp_expr true env [] t ++ str "." ++
 		       pp_global Term (List.nth projs (n-i)))
@@ -294,7 +296,7 @@ and pp_ifthenelse par env expr pv = match pv with
   | _ -> raise Not_found
 
 and pp_one_pat env i (r,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 expr = pp_expr (expr_needs_par t) env' [] t in
   try
     let projs = find_projections i in
@@ -324,7 +326,7 @@ and pp_pat env (info,factors) pv =
 
 and pp_function env 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
   match t' with
     | MLcase(i,MLrel 1,pv) when fst i=Standard ->
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 50339d473..9cc34634a 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -72,10 +72,10 @@ let rec pp_expr env args =
         pp_expr 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
 	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
     | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id] env in
+	let i,env' = push_vars [id_of_mlid id] env in
 	apply
 	  (hv 0
 	     (hov 2
@@ -123,7 +123,7 @@ and pp_cons_args env = function
 
 
 and pp_one_pat env (r,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 args =
     if ids = [] then mt ()
     else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index df9f02dfd..866f499b5 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -400,10 +400,14 @@ let flag_of_int n =
       opt_lin_let = kth_digit n 9;
       opt_lin_beta = kth_digit n 10 }
 
-(* For the moment, we allow by default everything except the type-unsafe
-   optimization [opt_case_idg]. *)
-
-let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024
+(* For the moment, we allow by default everything except :
+   - the type-unsafe optimization [opt_case_idg]
+   - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
+     (may lead to complexity blow-up, subsumed by finer reductions
+      when inlining recursors).
+*)
+
+let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*)
 
 let int_flag_ref = ref int_flag_init
 let opt_flag_ref = ref (flag_of_int int_flag_init)