1 files changed, 175 insertions, 68 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 6fc1195f..402fe4ff 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -299,10 +299,12 @@ let type_to_signature env t =
 
 let isKill = function Kill _ -> true | _ -> false
 
-let isDummy = function Tdummy _ -> true | _ -> false
+let isTdummy = function Tdummy _ -> true | _ -> false
+
+let isMLdummy = function MLdummy _ -> true | _ -> false
 
 let sign_of_id = function
-  | Dummy -> Kill Kother
+  | Dummy -> Kill Kprop
   | _ -> Keep
 
 (* Classification of signatures *)
@@ -310,45 +312,44 @@ let sign_of_id = function
 type sign_kind =
   | EmptySig
   | NonLogicalSig (* at least a [Keep] *)
-  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
   | SafeLogicalSig (* only [Kill Ktype] *)
+  | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *)
 
 let rec sign_kind = function
   | [] -> EmptySig
   | Keep :: _ -> NonLogicalSig
   | Kill k :: s ->
-      match sign_kind s with
-	| NonLogicalSig -> NonLogicalSig
-	| UnsafeLogicalSig -> UnsafeLogicalSig
-	| SafeLogicalSig | EmptySig ->
-	    if k == Kother then UnsafeLogicalSig else SafeLogicalSig
+     match k, sign_kind s with
+     | _, NonLogicalSig -> NonLogicalSig
+     | Ktype, (SafeLogicalSig | EmptySig) -> SafeLogicalSig
+     | _, _ -> UnsafeLogicalSig
 
 (* Removing the final [Keep] in a signature *)
 
 let rec sign_no_final_keeps = function
   | [] -> []
   | k :: s ->
-      let s' = k :: sign_no_final_keeps s in
-      match s' with [Keep] -> [] | _ -> s'
+     match k, sign_no_final_keeps s with
+     | Keep, [] -> []
+     | k, l -> k::l
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
-  let rec expunge s t =
-    if List.is_empty s then t else match t with
-      | Tmeta {contents = Some t} -> expunge s t
-      | Tarr (a,b) ->
-	  let t = expunge (List.tl s) b in
-	  if List.hd s == Keep then Tarr (a, t) else t
-      | Tglob (r,l) ->
-	  (match env r with
-	     | Some mlt -> expunge s (type_subst_list l mlt)
-	     | None -> assert false)
-      | _ -> assert false
+  let rec expunge s t = match s, t with
+    | [], _ -> t
+    | Keep :: s, Tarr(a,b) -> Tarr (a, expunge s b)
+    | Kill _ :: s, Tarr(a,b) -> expunge s b
+    | _, Tmeta {contents = Some t} -> expunge s t
+    | _, Tglob (r,l) ->
+       (match env r with
+	| Some mlt -> expunge s (type_subst_list l mlt)
+	| None -> assert false)
+    | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
   if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
-    Tarr (Tdummy Kother, t)
+    Tarr (Tdummy Kprop, t)
   else t
 
 let type_expunge env t =
@@ -385,7 +386,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLfix (i1, id1, t1), MLfix (i2, id2, t2) ->
   Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2
 | MLexn e1, MLexn e2 -> String.equal e1 e2
-| MLdummy, MLdummy -> true
+| MLdummy k1, MLdummy k2 -> k1 == k2
 | MLaxiom, MLaxiom -> true
 | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
 | _ -> false
@@ -420,7 +421,7 @@ let ast_iter_rel f =
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> ()
   in iter 0
 
 (*s Map over asts. *)
@@ -439,7 +440,7 @@ let ast_map f = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
   | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -457,7 +458,7 @@ let ast_map_lift f n = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
   | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
 
 (*s Iter over asts. *)
 
@@ -471,7 +472,7 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom  -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom  -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -507,9 +508,73 @@ let nb_occur_match =
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0
   in nb 1
 
+(* Replace unused variables by _ *)
+
+let dump_unused_vars a =
+  let rec ren env a = match a with
+    | MLrel i ->
+       let () = (List.nth env (i-1)) := true in a
+
+    | MLlam (id,b) ->
+       let occ_id = ref false in
+       let b' = ren (occ_id::env) b in
+       if !occ_id then if b' == b then a else MLlam(id,b')
+       else MLlam(Dummy,b')
+
+    | MLletin (id,b,c) ->
+       let occ_id = ref false in
+       let b' = ren env b in
+       let c' = ren (occ_id::env) c in
+       if !occ_id then
+         if b' == b && c' == c then a else MLletin(id,b',c')
+       else
+         (* 'let' without occurrence: shouldn't happen after simpl *)
+         MLletin(Dummy,b',c')
+
+    | MLcase (t,e,br) ->
+       let e' = ren env e in
+       let br' = Array.smartmap (ren_branch env) br in
+       if e' == e && br' == br then a else MLcase (t,e',br')
+
+    | MLfix (i,ids,v) ->
+       let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in
+       let v' = Array.smartmap (ren env') v in
+       if v' == v then a else MLfix (i,ids,v')
+
+    | MLapp (b,l) ->
+       let b' = ren env b and l' = List.smartmap (ren env) l in
+       if b' == b && l' == l then a else MLapp (b',l')
+
+    | MLcons(t,r,l) ->
+       let l' = List.smartmap (ren env) l in
+       if l' == l then a else MLcons (t,r,l')
+
+    | MLtuple l ->
+       let l' = List.smartmap (ren env) l in
+       if l' == l then a else MLtuple l'
+
+    | MLmagic b ->
+       let b' = ren env b in
+       if b' == b then a else MLmagic b'
+
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a
+
+    and ren_branch env ((ids,p,b) as tr) =
+      let occs = List.map (fun _ -> ref false) ids in
+      let b' = ren (List.rev_append occs env) b in
+      let ids' =
+        List.map2
+          (fun id occ -> if !occ then id else Dummy)
+          ids occs
+      in
+      if b' == b && List.equal eq_ml_ident ids ids' then tr
+      else (ids',p,b')
+  in
+  ren [] a
+
 (*s Lifting on terms.
     [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
 
@@ -559,7 +624,7 @@ let gen_subst v d t =
 	if i' < 1 then a
 	else if i' <= Array.length v then
 	  match v.(i'-1) with
-	    | None -> MLexn ("UNBOUND " ^ string_of_int i')
+	    | None -> assert false
 	    | Some u -> ast_lift n u
 	else MLrel (i+d)
     | a -> ast_map_lift subst n a
@@ -813,8 +878,8 @@ let census_add, census_max, census_clean =
     try h := add k i !h
     with Not_found -> h := (k, Int.Set.singleton i) :: !h
   in
-  let maxf k =
-    let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in
+  let maxf () =
+    let len = ref 0 and lst = ref Int.Set.empty and elm = ref MLaxiom in
     List.iter
       (fun (e, s) ->
 	 let n = Int.Set.cardinal s in
@@ -843,7 +908,7 @@ let factor_branches o typ br =
       if o.opt_case_cst then
 	(try census_add (branch_as_cst br.(i)) i with Impossible -> ());
     done;
-    let br_factor, br_set = census_max MLdummy in
+    let br_factor, br_set = census_max () in
     census_clean ();
     let n = Int.Set.cardinal br_set in
     if Int.equal n 0 then None
@@ -926,7 +991,7 @@ let iota_gen br hd =
   in iota 0 hd
 
 let is_atomic = function
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ -> true
   | _ -> false
 
 let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
@@ -948,9 +1013,20 @@ let expand_linear_let o id e =
 
 (* Some beta-iota reductions + simplifications. *)
 
+let rec unmagic = function MLmagic e -> unmagic e | e -> e
+let is_magic = function MLmagic _ -> true | _ -> false
+let magic_hd a = match a with
+  | MLmagic _ :: _ -> a
+  | e :: a -> MLmagic e :: a
+  | [] -> assert false
+
 let rec simpl o = function
   | MLapp (f, []) -> simpl o f
-  | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
+  | MLapp (MLapp(f,a),a') -> simpl o (MLapp(f,a@a'))
+  | MLapp (f, a) ->
+     (* When the head of the application is magic, no need for magic on args *)
+     let a = if is_magic f then List.map unmagic a else a in
+     simpl_app o (List.map (simpl o) a) (simpl o f)
   | MLcase (typ,e,br) ->
       let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in
       simpl_case o typ br (simpl o e)
@@ -970,12 +1046,18 @@ let rec simpl o = function
       if ast_occurs_itvl 1 n c.(i) then
 	MLfix (i, ids, Array.map (simpl o) c)
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
+  | MLmagic(MLmagic _ as e) -> simpl o e
+  | MLmagic(MLapp (f,l)) -> simpl o (MLapp (MLmagic f, l))
+  | MLmagic(MLletin(id,c,e)) -> simpl o (MLletin(id,c,MLmagic e))
+  | MLmagic(MLcase(typ,e,br)) ->
+     let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
+     simpl o (MLcase(typ,e,br'))
+  | MLmagic(MLexn _ as e) -> e
   | a -> ast_map (simpl o) a
 
 (* invariant : list [a] of arguments is non-empty *)
 
 and simpl_app o a = function
-  | MLapp (f',a') -> simpl_app o (a'@a) f'
   | MLlam (Dummy,t) ->
       simpl o (MLapp (ast_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
@@ -986,6 +1068,11 @@ and simpl_app o a = function
 	 | _ ->
 	     let a' = List.map (ast_lift 1) (List.tl a) in
 	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
+  | MLmagic (MLlam (id,t)) ->
+      (* When we've at least one argument, we permute the magic
+         and the lambda, to simplify things a bit (see #2795).
+         Alas, the 1st argument must also be magic then. *)
+      simpl_app o (magic_hd a) (MLlam (id,MLmagic t))
   | MLletin (id,e1,e2) when o.opt_let_app ->
       (* Application of a letin: we push arguments inside *)
       MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
@@ -998,7 +1085,7 @@ and simpl_app o a = function
 	     let a' = List.map (ast_lift k) a in
 	     (l, p, simpl o (MLapp (t,a')))) br
       in simpl o (MLcase (typ,e,br'))
-  | (MLdummy | MLexn _) as e -> e
+  | (MLdummy _ | MLexn _) as e -> e
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
@@ -1049,20 +1136,26 @@ let rec select_via_bl l args = match l,args with
 (*s [kill_some_lams] removes some head lambdas according to the signature [bl].
    This list is build on the identifier list model: outermost lambda
    is on the right.
-   [Rels] corresponding to removed lambdas are supposed not to occur, and
+   [Rels] corresponding to removed lambdas are not supposed to occur
+   (except maybe in the case of Kimplicit), and
    the other [Rels] are made correct via a [gen_subst].
    Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
 
+let is_impl_kill = function Kill (Kimplicit _) -> true | _ -> false
+
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
   let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
   if Int.equal n n' then ids,c
-  else if Int.equal n' 0 then [],ast_lift (-n) c
+  else if Int.equal n' 0 && not (List.exists is_impl_kill bl)
+  then [],ast_lift (-n) c
   else begin
     let v = Array.make n None in
     let rec parse_ids i j = function
       | [] -> ()
       | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l
+      | Kill (Kimplicit _ as k) :: l ->
+         v.(i) <- Some (MLdummy k); parse_ids (i+1) j l
       | Kill _ :: l -> parse_ids (i+1) j l
     in parse_ids 0 1 bl;
     select_via_bl bl ids, gen_subst v (n'-n) c
@@ -1070,11 +1163,19 @@ let kill_some_lams bl (ids,c) =
 
 (*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding
   to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or
-  if there is no lambda left at all. *)
+  if there is no lambda left at all. In addition, it now accepts a signature
+  that may mention some implicits. *)
 
-let kill_dummy_lams c =
+let rec merge_implicits ids s = match ids, s with
+  | [],_ -> []
+  | _,[] -> List.map sign_of_id ids
+  | Dummy::ids, _::s -> Kill Kprop :: merge_implicits ids s
+  | _::ids, (Kill (Kimplicit _) as k)::s -> k :: merge_implicits ids s
+  | _::ids, _::s -> Keep :: merge_implicits ids s
+
+let kill_dummy_lams sign c =
   let ids,c = collect_lams c in
-  let bl = List.map sign_of_id ids in
+  let bl = merge_implicits ids (List.rev sign) in
   if not (List.memq Keep bl) then raise Impossible;
   let rec fst_kill n = function
     | [] -> raise Impossible
@@ -1086,7 +1187,7 @@ let kill_dummy_lams c =
   let _, bl = List.chop skip bl in
   let c = named_lams ids_skip c in
   let ids',c = kill_some_lams bl (ids,c) in
-  ids, named_lams ids' c
+  (ids,bl), named_lams ids' c
 
 (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
    and a signature [s] and builds a eta-long version. *)
@@ -1100,12 +1201,12 @@ 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 :: ids) (MLdummy :: rels) (i+1) l
+    | Kill k :: l -> abs (Dummy :: ids) (MLdummy k :: rels) (i+1) l
   in abs ids [] 1 s
 
 (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e]
   in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas
-  corresponding to [Del] in [s]. *)
+  corresponding to [Kill _] in [s]. *)
 
 let case_expunge s e =
   let m = List.length s in
@@ -1123,17 +1224,18 @@ let term_expunge s (ids,c) =
   if List.is_empty s then c
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
-    if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
-      MLlam (Dummy, ast_lift 1 c)
+    if List.is_empty ids && lang () != Haskell &&
+       sign_kind s == UnsafeLogicalSig
+    then MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and
-  purge the args of [MLrel r] corresponding to a [dummy_name].
+(*s [kill_dummy_args (ids,bl) r t] looks for occurrences of [MLrel r] in [t]
+  and purge the args of [MLrel r] corresponding to a [Kill] in [bl].
   It makes eta-expansion if needed. *)
 
-let kill_dummy_args ids r t =
+let kill_dummy_args (ids,bl) r t =
   let m = List.length ids in
-  let bl = List.rev_map sign_of_id ids in
+  let sign = List.rev bl in
   let rec found n = function
     | MLrel r' when Int.equal r' (r + n) -> true
     | MLmagic e -> found n e
@@ -1144,41 +1246,46 @@ let kill_dummy_args ids r t =
 	let k = max 0 (m - (List.length a)) in
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
-	let a = select_via_bl bl (a @ (eta_args k)) in
+	let a = select_via_bl sign (a @ (eta_args k)) in
 	named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
     | e when found n e ->
-	let a = select_via_bl bl (eta_args m) in
+	let a = select_via_bl sign (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
     | e -> ast_map_lift killrec n e
   in killrec 0 t
 
 (*s The main function for local [dummy] elimination. *)
 
+let sign_of_args a =
+ List.map (function MLdummy k -> Kill k | _ -> Keep) a
+
 let rec kill_dummy = function
   | MLfix(i,fi,c) ->
       (try
-	 let ids,c = kill_dummy_fix i c in
-	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1))
+	 let k,c = kill_dummy_fix i c [] in
+	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args k 1 (MLrel 1))
        with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
   | MLapp (MLfix (i,fi,c),a) ->
       let a = List.map kill_dummy a in
+      (* Heuristics: if some arguments are implicit args, we try to
+         eliminate the corresponding arguments of the fixpoint *)
       (try
-	 let ids,c = kill_dummy_fix i c in
+	 let k,c = kill_dummy_fix i c (sign_of_args a) in
 	 let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
-	 let fake' = kill_dummy_args ids 1 fake in
+	 let fake' = kill_dummy_args k 1 fake in
 	 ast_subst (MLfix (i,fi,c)) fake'
        with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
   | MLletin(id, MLfix (i,fi,c),e) ->
       (try
-	 let ids,c = kill_dummy_fix i c in
-	 let e = kill_dummy (kill_dummy_args ids 1 e) in
+	 let k,c = kill_dummy_fix i c [] in
+	 let e = kill_dummy (kill_dummy_args k 1 e) in
 	 MLletin(id, MLfix(i,fi,c),e)
       with Impossible ->
 	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
   | MLletin(id,c,e) ->
       (try
-	 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
-	 let e = kill_dummy (kill_dummy_args ids 1 e) in
+	 let k,c = kill_dummy_lams [] (kill_dummy_hd c) in
+	 let e = kill_dummy (kill_dummy_args k 1 e) in
 	 let c = kill_dummy c in
 	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
@@ -1190,21 +1297,21 @@ and kill_dummy_hd = function
   | MLlam(id,e) -> MLlam(id, kill_dummy_hd e)
   | MLletin(id,c,e) ->
       (try
-	 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
-	 let e = kill_dummy_hd (kill_dummy_args ids 1 e) in
+	 let k,c = kill_dummy_lams [] (kill_dummy_hd c) in
+	 let e = kill_dummy_hd (kill_dummy_args k 1 e) in
 	 let c = kill_dummy c in
 	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
   | a -> a
 
-and kill_dummy_fix i c =
+and kill_dummy_fix i c s =
   let n = Array.length c in
-  let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in
+  let k,ci = kill_dummy_lams s (kill_dummy_hd c.(i)) in
   let c = Array.copy c in c.(i) <- ci;
   for j = 0 to (n-1) do
-    c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j))
+    c.(j) <- kill_dummy (kill_dummy_args k (n-i) c.(j))
   done;
-  ids,c
+  k,c
 
 (*s Putting things together. *)
 
@@ -1267,7 +1374,7 @@ let rec ml_size = function
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
-  | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0
+  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l