From 5550d920b831ec080cac236840132770bf1ba754 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 28 Nov 2015 10:16:54 +0100
Subject: Extraction: avoid generating some blanks at end-of-line

---
 plugins/extraction/ocaml.ml | 38 +++++++++++++++++++-------------------
 1 file changed, 19 insertions(+), 19 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 8c482b4b1d..45f5614af2 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -74,7 +74,7 @@ let preamble _ comment used_modules usf =
   (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
 
 let sig_preamble _ comment used_modules usf =
-  pp_header_comment comment ++ fnl () ++ fnl () ++
+  pp_header_comment comment ++
   prlist pp_open used_modules ++
   (if List.is_empty used_modules then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
@@ -524,13 +524,13 @@ let pp_decl = function
         let ids, def =
 	  try
 	    let ids,s = find_type_custom r in
-	    pp_string_parameters ids, str "=" ++ spc () ++ str s
+	    pp_string_parameters ids, str " =" ++ spc () ++ str s
 	  with Not_found ->
 	    pp_parameters l,
-	    if t == Taxiom then str "(* AXIOM TO BE REALIZED *)"
-	    else str "=" ++ spc () ++ pp_type false l t
+	    if t == Taxiom then str " (* AXIOM TO BE REALIZED *)"
+	    else str " =" ++ spc () ++ pp_type false l t
 	in
-	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
+	hov 2 (str "type " ++ ids ++ name ++ def)
     | Dterm (r, a, t) ->
 	let def =
 	  if is_custom r then str (" = " ^ find_custom r)
@@ -577,15 +577,15 @@ let pp_spec = function
       let ids, def =
 	try
 	  let ids, s = find_type_custom r in
-	  pp_string_parameters ids,  str "= " ++ str s
+	  pp_string_parameters ids, str " =" ++ spc () ++ str s
 	with Not_found ->
 	  let ids = pp_parameters l in
 	  match ot with
 	    | None -> ids, mt ()
-	    | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)"
-	    | Some t -> ids, str "=" ++ spc () ++ pp_type false l t
+	    | Some Taxiom -> ids, str " (* AXIOM TO BE REALIZED *)"
+	    | Some t -> ids, str " =" ++ spc () ++ pp_type false l t
       in
-      hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
+      hov 2 (str "type " ++ ids ++ name ++ def)
 
 let pp_alias_spec ren = function
   | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
@@ -602,7 +602,7 @@ let rec pp_specif = function
   | (l,Spec s) ->
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++
+	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
 	 pp_alias_spec ren s
        with Not_found -> pp_spec s)
@@ -610,15 +610,15 @@ let rec pp_specif = function
       let def = pp_module_type [] mt in
       let def' = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
-      hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
+      hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
+	 fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
        with Not_found -> Pp.mt ())
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
-      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
+      hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 fnl () ++ str ("module type "^ren^" = ") ++ name
@@ -641,7 +641,7 @@ and pp_module_type params = function
       let l = List.fold_left try_pp_specif [] sign in
       let l = List.rev l in
       pop_visible ();
-      str "sig " ++ fnl () ++
+      str "sig" ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
 	fnl () ++ str "end"
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
@@ -672,7 +672,7 @@ let rec pp_structure_elem = function
   | (l,SEdecl d) ->
        (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++
+	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
 	 fnl () ++ str "end" ++ fnl () ++
 	 pp_alias_decl ren d
 	with Not_found -> pp_decl d)
@@ -686,8 +686,8 @@ let rec pp_structure_elem = function
       let def = pp_module_expr [] m.ml_mod_expr in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1
-	(str "module " ++ name ++ typ ++ str " = " ++
-	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++
+	(str "module " ++ name ++ typ ++ str " =" ++
+	 (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 fnl () ++ str ("module "^ren^" = ") ++ name
@@ -695,7 +695,7 @@ let rec pp_structure_elem = function
   | (l,SEmodtype m) ->
       let def = pp_module_type [] m in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
-      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
+      hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
          fnl () ++ str ("module type "^ren^" = ") ++ name
@@ -719,7 +719,7 @@ and pp_module_expr params = function
       let l = List.fold_left try_pp_structure_elem [] sel in
       let l = List.rev l in
       pop_visible ();
-      str "struct " ++ fnl () ++
+      str "struct" ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
       fnl () ++ str "end"
 
-- 
cgit v1.2.3


From e2915d2e615a271c90d9e8c8599a428ed15828b5 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 29 Nov 2015 01:05:06 +0100
Subject: Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)

 The ind_equiv field wasn't correctly set, due to some kernel names
 glitches (canonical vs. user). The fix is to take into account the
 delta_resolver while traversing module structures.
---
 plugins/extraction/extract_env.ml | 113 +++++++++++++++++++-------------------
 1 file changed, 58 insertions(+), 55 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 0f846013b2..1d7f614564 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -78,56 +78,51 @@ module type VISIT = sig
   (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
   val add_ref : global_reference -> unit
+  val add_kn : kernel_name -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
 
   (* Test functions:
      is a particular object a needed dependency for the current extraction ? *)
   val needed_ind : mutual_inductive -> bool
-  val needed_con : constant -> bool
+  val needed_cst : constant -> bool
   val needed_mp : module_path -> bool
   val needed_mp_all : module_path -> bool
 end
 
 module Visit : VISIT = struct
   type must_visit =
-      { mutable ind : KNset.t; mutable con : KNset.t;
-	mutable mp : MPset.t; mutable mp_all : MPset.t }
+      { mutable kn : KNset.t;
+        mutable mp : MPset.t;
+        mutable mp_all : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { ind = KNset.empty ; con = KNset.empty ;
-	    mp = MPset.empty; mp_all = MPset.empty }
+  let v = { kn = KNset.empty; mp = MPset.empty; mp_all = MPset.empty }
   (* the accessor functions *)
   let reset () =
-    v.ind <- KNset.empty;
-    v.con <- KNset.empty;
+    v.kn <- KNset.empty;
     v.mp <- MPset.empty;
     v.mp_all <- MPset.empty
-  let needed_ind i = KNset.mem (user_mind i) v.ind
-  let needed_con c = KNset.mem (user_con c) v.con
+  let needed_ind i = KNset.mem (user_mind i) v.kn
+  let needed_cst c = KNset.mem (user_con c) v.kn
   let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
   let needed_mp_all mp = MPset.mem mp v.mp_all
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
   let add_mp_all mp =
-    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp;
+    check_loaded_modfile mp;
+    v.mp <- MPset.union (prefixes_mp mp) v.mp;
     v.mp_all <- MPset.add mp v.mp_all
-  let add_ind i =
-    let kn = user_mind i in
-    v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
-  let add_con c =
-    let kn = user_con c in
-    v.con <- KNset.add kn v.con; add_mp (modpath kn)
+  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
   let add_ref = function
-    | ConstRef c -> add_con c
-    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind
+    | ConstRef c -> add_kn (user_con c)
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind)
     | VarRef _ -> assert false
   let add_decl_deps = decl_iter_references add_ref add_ref add_ref
   let add_spec_deps = spec_iter_references add_ref add_ref add_ref
 end
 
 let add_field_label mp = function
-  | (lab, SFBconst _) -> Visit.add_ref (ConstRef (Constant.make2 mp lab))
-  | (lab, SFBmind _) -> Visit.add_ref (IndRef (MutInd.make2 mp lab, 0))
+  | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab)
   | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
 
 let rec add_labels mp = function
@@ -193,36 +188,44 @@ let rec mp_of_mexpr = function
   | MEwith (seb,_) -> mp_of_mexpr seb
   | _ -> assert false
 
+let no_delta = Mod_subst.empty_delta_resolver
+
 let env_for_mtb_with_def env mp me idl =
   let struc = Modops.destr_nofunctor me in
   let l = Label.of_id (List.hd idl) in
   let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in
   let before = fst (List.split_when spot struc) in
-  Modops.add_structure mp before empty_delta_resolver env
+  Modops.add_structure mp before no_delta env
+
+let make_cst resolver mp l =
+  Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
+
+let make_mind resolver mp l =
+  Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l)
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)
 
-let rec extract_structure_spec env mp = function
+let rec extract_structure_spec env mp reso = function
   | [] -> []
   | (l,SFBconst cb) :: msig ->
-      let kn = Constant.make2 mp l in
-      let s = extract_constant_spec env kn cb in
-      let specs = extract_structure_spec env mp msig in
+      let c = make_cst reso mp l in
+      let s = extract_constant_spec env c cb in
+      let specs = extract_structure_spec env mp reso msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let mind = MutInd.make2 mp l in
+      let mind = make_mind reso mp l in
       let s = Sind (mind, extract_inductive env mind) in
-      let specs = extract_structure_spec env mp msig in
+      let specs = extract_structure_spec env mp reso msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmodule mb) :: msig ->
-      let specs = extract_structure_spec env mp msig in
+      let specs = extract_structure_spec env mp reso msig in
       let spec = extract_mbody_spec env mb.mod_mp mb in
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig ->
-      let specs = extract_structure_spec env mp msig in
+      let specs = extract_structure_spec env mp reso msig in
       let spec = extract_mbody_spec env mtb.mod_mp mtb in
       (l,Smodtype spec) :: specs
 
@@ -244,7 +247,7 @@ and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
       MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
-  | MEapply _ -> extract_msignature_spec env mp1 me_struct
+  | MEapply _ -> extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
 
 and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MoreFunctor (mbid, mtb, me_alg') ->
@@ -258,19 +261,19 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
 		extract_mexpression_spec env' mp1 (me_struct',me_alg'))
   | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
 
-and extract_msignature_spec env mp1 = function
+and extract_msignature_spec env mp1 reso = function
   | NoFunctor struc ->
-      let env' = Modops.add_structure mp1 struc empty_delta_resolver env in
-      MTsig (mp1, extract_structure_spec env' mp1 struc)
+      let env' = Modops.add_structure mp1 struc reso env in
+      MTsig (mp1, extract_structure_spec env' mp1 reso struc)
   | MoreFunctor (mbid, mtb, me) ->
       let mp = MPbound mbid in
       let env' = Modops.add_module_type mp mtb env in
       MTfunsig (mbid, extract_mbody_spec env mp mtb,
-		extract_msignature_spec env' mp1 me)
+		extract_msignature_spec env' mp1 reso me)
 
 and extract_mbody_spec env mp mb = match mb.mod_type_alg with
   | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
-  | None -> extract_msignature_spec env mp mb.mod_type
+  | None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to implementations.
@@ -279,31 +282,31 @@ and extract_mbody_spec env mp mb = match mb.mod_type_alg with
    important: last to first ensures correct dependencies.
 *)
 
-let rec extract_structure env mp ~all = function
+let rec extract_structure env mp reso ~all = function
   | [] -> []
   | (l,SFBconst cb) :: struc ->
       (try
 	 let vl,recd,struc = factor_fix env l cb struc in
-	 let vc = Array.map (Constant.make2 mp) vl in
-	 let ms = extract_structure env mp ~all struc in
-	 let b = Array.exists Visit.needed_con vc in
+	 let vc = Array.map (make_cst reso mp) vl in
+	 let ms = extract_structure env mp reso ~all struc in
+	 let b = Array.exists Visit.needed_cst vc in
 	 if all || b then
 	   let d = extract_fixpoint env vc recd in
 	   if (not b) && (logical_decl d) then ms
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms
        with Impossible ->
-	 let ms = extract_structure env mp ~all struc in
-	 let c = Constant.make2 mp l in
-	 let b = Visit.needed_con c in
+	 let ms = extract_structure env mp reso ~all struc in
+	 let c = make_cst reso mp l in
+	 let b = Visit.needed_cst c in
 	 if all || b then
 	   let d = extract_constant env c cb in
 	   if (not b) && (logical_decl d) then ms
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms)
   | (l,SFBmind mib) :: struc ->
-      let ms = extract_structure env mp ~all struc in
-      let mind = MutInd.make2 mp l in
+      let ms = extract_structure env mp reso ~all struc in
+      let mind = make_mind reso mp l in
       let b = Visit.needed_ind mind in
       if all || b then
 	let d = Dind (mind, extract_inductive env mind) in
@@ -311,14 +314,14 @@ let rec extract_structure env mp ~all = function
 	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
   | (l,SFBmodule mb) :: struc ->
-      let ms = extract_structure env mp ~all struc in
+      let ms = extract_structure env mp reso ~all struc in
       let mp = MPdot (mp,l) in
       let all' = all || Visit.needed_mp_all mp in
       if all' || Visit.needed_mp mp then
 	(l,SEmodule (extract_module env mp ~all:all' mb)) :: ms
       else ms
   | (l,SFBmodtype mtb) :: struc ->
-      let ms = extract_structure env mp ~all struc in
+      let ms = extract_structure env mp reso ~all struc in
       let mp = MPdot (mp,l) in
       if all || Visit.needed_mp mp then
         (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms
@@ -332,7 +335,7 @@ and extract_mexpr env mp = function
       (* In Haskell/Scheme, we expand everything.
          For now, we also extract everything, dead code will be removed later
          (see [Modutil.optimize_struct]. *)
-      extract_msignature env mp ~all:true (expand_mexpr env mp me)
+      extract_msignature env mp no_delta ~all:true (expand_mexpr env mp me)
   | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp_all mp; Miniml.MEident mp
@@ -350,17 +353,17 @@ and extract_mexpression env mp = function
          extract_mbody_spec env mp1 mtb,
 	 extract_mexpression env' mp me)
 
-and extract_msignature env mp ~all = function
+and extract_msignature env mp reso ~all = function
   | NoFunctor struc ->
-      let env' = Modops.add_structure mp struc empty_delta_resolver env in
-      Miniml.MEstruct (mp,extract_structure env' mp ~all struc)
+      let env' = Modops.add_structure mp struc reso env in
+      Miniml.MEstruct (mp,extract_structure env' mp reso ~all struc)
   | MoreFunctor (mbid, mtb, me) ->
       let mp1 = MPbound mbid in
       let env' = Modops.add_module_type mp1 mtb	env in
       Miniml.MEfunctor
         (mbid,
          extract_mbody_spec env mp1 mtb,
-	 extract_msignature env' mp ~all me)
+	 extract_msignature env' mp reso ~all me)
 
 and extract_module env mp ~all mb =
   (* A module has an empty [mod_expr] when :
@@ -376,8 +379,8 @@ and extract_module env mp ~all mb =
       (* This module has a signature, otherwise it would be FullStruct.
          We extract just the elements required by this signature. *)
       let () = add_labels mp mb.mod_type in
-      extract_msignature env mp ~all:false sign
-    | FullStruct -> extract_msignature env mp ~all mb.mod_type
+      extract_msignature env mp mb.mod_delta ~all:false sign
+    | FullStruct -> extract_msignature env mp mb.mod_delta ~all mb.mod_type
   in
   (* Slight optimization: for modules without explicit signatures
      ([FullStruct] case), we build the type out of the extracted
@@ -399,7 +402,7 @@ let mono_environment refs mpl =
   let l = List.rev (environment_until None) in
   List.rev_map
     (fun (mp,struc) ->
-      mp, extract_structure env mp ~all:(Visit.needed_mp_all mp) struc)
+      mp, extract_structure env mp no_delta ~all:(Visit.needed_mp_all mp) struc)
     l
 
 (**************************************)
@@ -650,7 +653,7 @@ let extraction_library is_rec m =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, extract_structure env mp true struc) :: l
+    then (mp, extract_structure env mp no_delta true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
-- 
cgit v1.2.3


From a4d48ce98d7ae0cf07c653ed75700ed6f182936a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 30 Nov 2015 16:40:46 +0100
Subject: Extraction: check for remaining implicits after dead code removal
 (fix #4243)

---
 plugins/extraction/modutil.ml | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 8158ac647e..53c9f59878 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -404,12 +404,16 @@ let optimize_struct to_appear struc =
     List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
       struc
   in
-  ignore (struct_ast_search check_implicits opt_struc);
-  if library () then
-    List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc
-  else begin
-    reset_needed ();
-    List.iter add_needed (fst to_appear);
-    List.iter add_needed_mp (snd to_appear);
-    depcheck_struct opt_struc
-  end
+  let mini_struc =
+    if library () then
+      List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc
+    else
+      begin
+        reset_needed ();
+        List.iter add_needed (fst to_appear);
+        List.iter add_needed_mp (snd to_appear);
+        depcheck_struct opt_struc
+      end
+  in
+  ignore (struct_ast_search check_implicits mini_struc);
+  mini_struc
-- 
cgit v1.2.3


From ec5455d7351c05a58ae99d5a300dc8576f8c9360 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 4 Dec 2015 18:39:47 +0100
Subject: Extraction: nicer implementation of Implicits

 Instead of the original hacks (embedding implicits in string msg in MLexn !)
 we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use
 of the i-th argument of constant or constructor r when this argument has been
 declared as implicit.

 A new option Set/Unset Extraction SafeImplicits controls what happens
 when some implicits still occur after an extraction : fail in safe mode,
 or otherwise produce some code nonetheless. This code is probably buggish
 if the implicits are actually used to do anything relevant (match, function
 call, etc), but it might also be fine if the implicits are just passed along.
 And anyway, this unsafe mode could help figure what's going on.

 Note: the MLdummy now expected a kill_reason, just as Tdummy.
 These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit.

 Some minor refactoring on the fly.
---
 plugins/extraction/extract_env.ml |  4 +-
 plugins/extraction/extraction.ml  | 70 ++++++++++++------------------
 plugins/extraction/haskell.ml     |  7 ++-
 plugins/extraction/json.ml        |  2 +-
 plugins/extraction/miniml.mli     | 15 ++++---
 plugins/extraction/mlutil.ml      | 90 +++++++++++++++++++++------------------
 plugins/extraction/mlutil.mli     |  5 ++-
 plugins/extraction/modutil.ml     | 23 +++++-----
 plugins/extraction/ocaml.ml       |  9 ++--
 plugins/extraction/scheme.ml      |  2 +-
 plugins/extraction/table.ml       | 71 ++++++++++++++++++++----------
 plugins/extraction/table.mli      |  6 +--
 12 files changed, 166 insertions(+), 138 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1d7f614564..3d32398ffd 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -498,8 +498,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
   let d = descr () in
   reset_renaming_tables AllButExternal;
   let unsafe_needs = {
-    mldummy = struct_ast_search ((==) MLdummy) struc;
-    tdummy = struct_type_search Mlutil.isDummy struc;
+    mldummy = struct_ast_search Mlutil.isMLdummy struc;
+    tdummy = struct_type_search Mlutil.isTdummy struc;
     tunknown = struct_type_search ((==) Tunknown) struc;
     magic =
       if lang () != Haskell then false
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 1112c3b890..f4d14af624 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -91,7 +91,7 @@ exception NotDefault of kill_reason
 let check_default env t =
   match flag_of_type env t with
     | _,TypeScheme -> raise (NotDefault Ktype)
-    | Logic,_ -> raise (NotDefault Kother)
+    | Logic,_ -> raise (NotDefault Kprop)
     | _ -> ()
 
 let is_info_scheme env t = match flag_of_type env t with
@@ -103,7 +103,7 @@ let is_info_scheme env t = match flag_of_type env t with
 let rec type_sign env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
-	(if is_info_scheme env t then Keep else Kill Kother)
+	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
@@ -137,7 +137,7 @@ let rec type_sign_vl env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
-	if not (is_info_scheme env t) then Kill Kother::s, vl
+	if not (is_info_scheme env t) then Kill Kprop::s, vl
 	else Keep::s, (make_typvar n vl) :: vl
     | _ -> [],[]
 
@@ -154,25 +154,12 @@ let sign_with_implicits r s nb_params =
   let implicits = implicits_of_global r in
   let rec add_impl i = function
     | [] -> []
-    | sign::s ->
-	let sign' =
-	  if sign == Keep && Int.List.mem i implicits
-          then Kill Kother else sign
-	in sign' :: add_impl (succ i) s
+    | Keep::s when Int.Set.mem i implicits ->
+       Kill (Kimplicit (r,i)) :: add_impl (i+1) s
+    | sign::s -> sign :: add_impl (i+1) s
   in
   add_impl (1+nb_params) s
 
-(* Enriching a exception message *)
-
-let rec handle_exn r n fn_name = function
-  | MLexn s ->
-      (try Scanf.sscanf s "UNBOUND %d%!"
-	 (fun i ->
-	    assert ((0 < i) && (i <= n));
-	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with Scanf.Scan_failure _ | End_of_file -> MLexn s)
-  | a -> ast_map (handle_exn r n fn_name) a
-
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
@@ -285,10 +272,10 @@ let rec extract_type env db j c args =
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ ->
-		      let reason = if lvl == TypeScheme then Ktype else Kother in
+		      let reason = if lvl == TypeScheme then Ktype else Kprop in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother
+    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
     | Rel n ->
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -458,7 +445,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	if p.ip_logical then raise (I Standard);
 	if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
 	let typ = p.ip_types.(0) in
-	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
+	let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in
 	if not (keep_singleton ()) &&
 	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
 	then raise (I Singleton);
@@ -479,7 +466,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let mp = MutInd.modpath kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
-	  | _::l, typ::typs when isDummy (expand env typ) ->
+	  | _::l, typ::typs when isTdummy (expand env typ) ->
 	      select_fields l typs
 	  | Anonymous::l, typ::typs ->
 	      None :: (select_fields l typs)
@@ -655,7 +642,7 @@ and extract_maybe_term env mle mlt c =
   try check_default env (type_of env c);
     extract_term env mle mlt c []
   with NotDefault d ->
-    put_magic (mlt, Tdummy d) MLdummy
+    put_magic (mlt, Tdummy d) (MLdummy d)
 
 (*s Generic way to deal with an application. *)
 
@@ -723,11 +710,11 @@ and extract_cst_app env mle mlt kn u args =
 	else mla
       with e when Errors.noncritical e -> mla
   in
-  (* For strict languages, purely logical signatures with at least
-     one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
+  (* For strict languages, purely logical signatures lead to a dummy lam
+     (except when [Kill Ktype] everywhere). So a [MLdummy] is left
      accordingly. *)
   let optdummy = match sign_kind s_full with
-    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy]
+    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy Kprop]
     | _ -> []
   in
   (* Different situations depending of the number of arguments: *)
@@ -826,8 +813,8 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
 	assert (Int.equal br_size 1);
-	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
+	let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in
+	let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in
 	let e = extract_maybe_term env mle mlt br.(0) in
 	snd (case_expunge s e)
       end
@@ -851,8 +838,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge s e in
-	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
-	(List.rev ids, Pusual r, e')
+	(List.rev ids, Pusual r, e)
       in
       if mi.ind_kind == Singleton then
 	begin
@@ -960,8 +946,6 @@ let extract_std_constant env kn body typ =
   let e = extract_term env mle t' c [] in
   (* Expunging term and type from dummy lambdas. *)
   let trm = term_expunge s (ids,e) in
-  let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm
-  in
   trm, type_expunge_from_sign env s t
 
 (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
@@ -979,8 +963,8 @@ let extract_axiom env kn typ =
 
 let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in
-  let types = Array.make n (Tdummy Kother)
-  and terms = Array.make n MLdummy in
+  let types = Array.make n (Tdummy Kprop)
+  and terms = Array.make n (MLdummy Kprop) in
   let kns = Array.to_list vkn in
   current_fixpoints := kns;
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
@@ -1022,7 +1006,7 @@ let extract_constant env kn cb =
   in
   match flag_of_type env typ with
     | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
-    | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother)
+    | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
@@ -1047,7 +1031,7 @@ let extract_constant_spec env kn cb =
   let typ = Typeops.type_of_constant_type env cb.const_type in
   match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
-    | (Logic, Default) -> Sval (r, Tdummy Kother)
+    | (Logic, Default) -> Sval (r, Tdummy Kprop)
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	(match cb.const_body with
@@ -1075,8 +1059,8 @@ let extract_constr env c =
   reset_meta_count ();
   let typ = type_of env c in
   match flag_of_type env typ with
-    | (_,TypeScheme) -> MLdummy, Tdummy Ktype
-    | (Logic,_) -> MLdummy, Tdummy Kother
+    | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype
+    | (Logic,_) -> MLdummy Kprop, Tdummy Kprop
     | (Info,Default) ->
       let mlt = extract_type env [] 1 typ [] in
       extract_term env Mlenv.empty mlt c [], mlt
@@ -1090,7 +1074,7 @@ let extract_inductive env kn =
       | [] -> []
       | t::l ->
 	  let l' = filter (succ i) l in
-	  if isDummy (expand env t) || Int.List.mem i implicits then l'
+	  if isTdummy (expand env t) || Int.Set.mem i implicits then l'
 	  else t::l'
     in filter (1+ind.ind_nparams) l
   in
@@ -1102,11 +1086,11 @@ let extract_inductive env kn =
 (*s Is a [ml_decl] logical ? *)
 
 let logical_decl = function
-  | Dterm (_,MLdummy,Tdummy _) -> true
+  | Dterm (_,MLdummy _,Tdummy _) -> true
   | Dtype (_,[],Tdummy _) -> true
   | Dfix (_,av,tv) ->
-      (Array.for_all ((==) MLdummy) av) &&
-      (Array.for_all isDummy tv)
+      (Array.for_all isMLdummy av) &&
+      (Array.for_all isTdummy tv)
   | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 37b4142073..530eb2ff89 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -200,8 +200,11 @@ let rec pp_expr par env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy k ->
+        (* An [MLdummy] may be applied, but I don't really care. *)
+        (match msg_of_implicit k with
+         | "" -> str "__"
+         | s -> str "__" ++ spc () ++ pp_bracket_comment (str s))
     | MLmagic a ->
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 125dc86b82..df79c585e5 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -153,7 +153,7 @@ let rec json_expr env = function
       ("what", json_str "expr:exception");
       ("msg", json_str s)
     ]
-  | MLdummy -> json_dict [("what", json_str "expr:dummy")]
+  | MLdummy _ -> json_dict [("what", json_str "expr:dummy")]
   | MLmagic a -> json_dict [
       ("what", json_str "expr:coerce");
       ("value", json_expr env a)
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index b7dee6cb14..681dceaa04 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -16,11 +16,16 @@ open Globnames
    object expects, and what these arguments will become in the ML
    object. *)
 
-(* We eliminate from terms:  1) types 2) logical parts.
-   [Kother] stands both for logical or other reasons
-   (for instance user-declared implicit arguments w.r.t. extraction). *)
+(* We eliminate from terms:
+   1) types
+   2) logical parts
+   3) user-declared implicit arguments of a constant of constructor
+*)
 
-type kill_reason = Ktype | Kother
+type kill_reason =
+  | Ktype
+  | Kprop
+  | Kimplicit of global_reference * int  (* n-th arg of a cst or construct *)
 
 type sign = Keep | Kill of kill_reason
 
@@ -118,7 +123,7 @@ and ml_ast =
   | MLcase   of ml_type * ml_ast * ml_branch array
   | MLfix    of int * Id.t array * ml_ast array
   | MLexn    of string
-  | MLdummy
+  | MLdummy  of kill_reason
   | MLaxiom
   | MLmagic  of ml_ast
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 6fc1195fba..402370eece 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -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,7 +508,7 @@ 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
 
 (*s Lifting on terms.
@@ -559,7 +560,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 +814,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 +844,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 +927,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
@@ -998,7 +999,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 +1050,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
@@ -1100,12 +1107,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,8 +1130,9 @@ 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
@@ -1267,7 +1275,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
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 0a71d2c838..c380dfb3e3 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type
 val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type
 
 val eq_ml_type : ml_type -> ml_type -> bool
-val isDummy : ml_type -> bool
+val isTdummy : ml_type -> bool
+val isMLdummy : ml_ast -> bool
 val isKill : sign -> bool
 
 val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast
@@ -125,8 +126,8 @@ exception Impossible
 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] *)
 
 val sign_kind : signature -> sign_kind
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 53c9f59878..e8383bda59 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -100,7 +100,7 @@ let ast_iter_references do_term do_cons do_type a =
 	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
-      | MLdummy | MLaxiom | MLmagic _ -> ()
+      | MLdummy _ | MLaxiom | MLmagic _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
@@ -387,16 +387,15 @@ let is_prefix pre s =
   in
   is_prefix_aux 0
 
-let check_implicits = function
-  | MLexn s ->
-      if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then
-	begin
-	  if is_prefix "UNBOUND" s then assert false;
-	  if is_prefix "IMPLICIT" s then
-	    error_non_implicit (String.sub s 9 (String.length s - 9));
-	end;
-      false
-  | _ -> false
+exception RemainingImplicit of kill_reason
+
+let check_for_remaining_implicits struc =
+  let check = function
+    | MLdummy (Kimplicit _ as k) -> raise (RemainingImplicit k)
+    | _ -> false
+  in
+  try ignore (struct_ast_search check struc)
+  with RemainingImplicit k -> err_or_warn_remaining_implicit k
 
 let optimize_struct to_appear struc =
   let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
@@ -415,5 +414,5 @@ let optimize_struct to_appear struc =
         depcheck_struct opt_struc
       end
   in
-  ignore (struct_ast_search check_implicits mini_struc);
+  let () = check_for_remaining_implicits mini_struc in
   mini_struc
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 45f5614af2..257c6e9716 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -199,8 +199,11 @@ let rec pp_expr par env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy k ->
+        (* An [MLdummy] may be applied, but I don't really care. *)
+        (match msg_of_implicit k with
+         | "" -> str "__"
+         | s -> str "__" ++ spc () ++ str ("(* "^s^" *)"))
     | MLmagic a ->
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
     | MLaxiom ->
@@ -352,7 +355,7 @@ and pp_function env t =
     | MLcase(Tglob(r,_),MLrel 1,pv) when
 	not (is_coinductive r) && List.is_empty (get_record_fields r) &&
 	not (is_custom_match pv) ->
-	if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then
+	if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
 	  v 0 (pp_pat env' pv)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index cc8b6d8e79..4901cf1807 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -126,7 +126,7 @@ let rec pp_expr env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	paren (str "error" ++ spc () ++ qs s)
-    | MLdummy ->
+    | MLdummy _ ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
 	pp_expr env args a
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a57c39eef1..63d792e363 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -401,16 +401,34 @@ let error_MPfile_as_mod mp b =
 	    "Monolithic Extraction cannot deal with this situation.\n"^
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
-let msg_non_implicit r n id =
-  let name = match id with
-    | Anonymous -> ""
-    | Name id -> "(" ^ Id.to_string id ^ ") "
-  in
-  "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
-
-let error_non_implicit msg =
-  err (str (msg ^ " still occurs after extraction.") ++
-       fnl () ++ str "Please check the Extraction Implicit declarations.")
+let argnames_of_global r =
+  let typ = Global.type_of_global_unsafe r in
+  let rels,_ =
+    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
+  List.rev_map fst rels
+
+let msg_of_implicit = function
+  | Kimplicit (r,i) ->
+     let name = match List.nth (argnames_of_global r) (i-1) with
+       | Anonymous -> ""
+       | Name id -> "(" ^ Id.to_string id ^ ") "
+     in
+     (String.ordinal i)^" argument "^name^"of "^(string_of_global r)
+  | Ktype | Kprop -> ""
+
+let error_remaining_implicit k =
+  let s = msg_of_implicit k in
+  err (str ("An implicit occurs after extraction : "^s^".") ++ fnl () ++
+       str "Please check your Extraction Implicit declarations." ++ fnl() ++
+       str "You might also try Unset Extraction SafeImplicits to force" ++
+       fnl() ++ str "the extraction of unsafe code and review it manually.")
+
+let warning_remaining_implicit k =
+  let s = msg_of_implicit k in
+  msg_warning
+    (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
+     str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl ()
+     ++ str "but this code is potentially unsafe, please review it manually.")
 
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
@@ -635,32 +653,39 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extraction Implicit *)
 
+let safe_implicit = my_bool_option "SafeImplicits" true
+
+let err_or_warn_remaining_implicit k =
+  if safe_implicit () then
+    error_remaining_implicit k
+  else
+    warning_remaining_implicit k
+
 type int_or_id = ArgInt of int | ArgId of Id.t
 
 let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit"
 
 let implicits_of_global r =
- try Refmap'.find r !implicits_table with Not_found -> []
+ try Refmap'.find r !implicits_table with Not_found -> Int.Set.empty
 
 let add_implicits r l =
-  let typ = Global.type_of_global_unsafe r in
-  let rels,_ =
-    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
-  let names = List.rev_map fst rels in
+  let names = argnames_of_global r in
   let n = List.length names in
-  let check = function
+  let add_arg s = function
     | ArgInt i ->
-	if 1 <= i && i <= n then i
+	if 1 <= i && i <= n then Int.Set.add i s
 	else err (int i ++ str " is not a valid argument number for " ++
 		  safe_pr_global r)
     | ArgId id ->
-	(try List.index Name.equal (Name id) names
-	 with Not_found ->
-	   err (str "No argument " ++ pr_id id ++ str " for " ++
-		safe_pr_global r))
+       try
+         let i = List.index Name.equal (Name id) names in
+         Int.Set.add i s
+       with Not_found ->
+	 err (str "No argument " ++ pr_id id ++ str " for " ++
+	      safe_pr_global r)
   in
-  let l' = List.map check l in
-  implicits_table := Refmap'.add r l' !implicits_table
+  let ints = List.fold_left add_arg Int.Set.empty l in
+  implicits_table := Refmap'.add r ints !implicits_table
 
 (* Registration of operations for rollback. *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 648f232114..a6734dae86 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -38,8 +38,8 @@ val error_MPfile_as_mod : module_path -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
-val msg_non_implicit : global_reference -> int -> Name.t -> string
-val error_non_implicit : string -> 'a
+val msg_of_implicit : kill_reason -> string
+val err_or_warn_remaining_implicit : kill_reason -> unit
 
 val info_file : string -> unit
 
@@ -166,7 +166,7 @@ val to_keep : global_reference -> bool
 
 (*s Table for implicits arguments *)
 
-val implicits_of_global : global_reference -> int list
+val implicits_of_global : global_reference -> Int.Set.t
 
 (*s Table for user-given custom ML extractions. *)
 
-- 
cgit v1.2.3


From 123cbdfef1733a1786109bd1b97ccfa3f62c0d1c Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 00:33:29 +0100
Subject: Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty
 phrase")

---
 plugins/extraction/haskell.ml |  3 +-
 plugins/extraction/ocaml.ml   | 70 ++++++++++++++++++++-----------------------
 plugins/extraction/scheme.ml  |  3 +-
 3 files changed, 37 insertions(+), 39 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 530eb2ff89..dd66a6a98f 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -334,7 +334,8 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
+	    (not (is_custom r) &&
+             match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 257c6e9716..259ec49c07 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -392,11 +392,11 @@ let pp_Dfix (rv,c,t) =
     (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
   in
   let rec pp init i =
-    if i >= Array.length rv then
-      (if init then failwith "empty phrase" else mt ())
+    if i >= Array.length rv then mt ()
     else
       let void = is_inline_custom rv.(i) ||
-	(not (is_custom rv.(i)) && match c.(i) with MLexn "UNUSED" -> true | _ -> false)
+	(not (is_custom rv.(i)) &&
+         match c.(i) with MLexn "UNUSED" -> true | _ -> false)
       in
       if void then pp init (i+1)
       else
@@ -469,8 +469,8 @@ let pp_coind pl name =
 
 let pp_ind co kn ind =
   let prefix = if co then "__" else "" in
-  let some = ref false in
-  let init= ref (str "type ") in
+  let initkwd = str "type " in
+  let nextkwd = fnl () ++ str "and " in
   let names =
     Array.mapi (fun i p -> if p.ip_logical then mt () else
 		  pp_global Type (IndRef (kn,i)))
@@ -483,29 +483,20 @@ let pp_ind co kn ind =
 	   p.ip_types)
       ind.ind_packets
   in
-  let rec pp i =
+  let rec pp i kwd =
     if i >= Array.length ind.ind_packets then mt ()
     else
       let ip = (kn,i) in
       let ip_equiv = ind.ind_equiv, i in
       let p = ind.ind_packets.(i) in
-      if is_custom (IndRef ip) then pp (i+1)
-      else begin
-	some := true;
-	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
-	else
-	  let s = !init in
-	  begin
-	    init := (fnl () ++ str "and ");
-	    s ++
-	    (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
-	    pp_one_ind
-	      prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
-	    pp (i+1)
-	  end
-      end
+      if is_custom (IndRef ip) then pp (i+1) kwd
+      else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd
+      else
+	kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
+	pp_one_ind prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
+	pp (i+1) nextkwd
   in
-  let st = pp 0 in if !some then st else failwith "empty phrase"
+  pp 0 initkwd
 
 
 (*s Pretty-printing of a declaration. *)
@@ -518,8 +509,8 @@ let pp_mind kn i =
     | Standard -> pp_ind false kn i
 
 let pp_decl = function
-    | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
-    | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+    | Dtype (r,_,_) when is_inline_custom r -> mt ()
+    | Dterm (r,_,_) when is_inline_custom r -> mt ()
     | Dind (kn,i) -> pp_mind kn i
     | Dtype (r, l, t) ->
         let name = pp_global Type r in
@@ -567,8 +558,8 @@ let pp_alias_decl ren = function
 	rv
 
 let pp_spec = function
-  | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
-  | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+  | Sval (r,_) when is_inline_custom r -> mt ()
+  | Stype (r,_,_) when is_inline_custom r -> mt ()
   | Sind (kn,i) -> pp_mind kn i
   | Sval (r,t) ->
       let def = pp_type false [] t in
@@ -638,7 +629,8 @@ and pp_module_type params = function
   | MTsig (mp, sign) ->
       push_visible mp params;
       let try_pp_specif l x =
-	try pp_specif x :: l with Failure "empty phrase" -> l
+        let px = pp_specif x in
+        if Pp.is_empty px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_specif *)
       let l = List.fold_left try_pp_specif [] sign in
@@ -716,7 +708,8 @@ and pp_module_expr params = function
   | MEstruct (mp, sel) ->
       push_visible mp params;
       let try_pp_structure_elem l x =
-	try pp_structure_elem x :: l with Failure "empty phrase" -> l
+        let px = pp_structure_elem x in
+        if Pp.is_empty px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_structure_elem *)
       let l = List.fold_left try_pp_structure_elem [] sel in
@@ -726,26 +719,31 @@ and pp_module_expr params = function
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
       fnl () ++ str "end"
 
+let rec prlist_sep_nonempty sep f = function
+  | [] -> mt ()
+  | [h] -> f h
+  | h::t ->
+     let e = f h in
+     let r = prlist_sep_nonempty sep f t in
+     if Pp.is_empty e then r
+     else e ++ sep () ++ r
+
 let do_struct f s =
-  let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
-  in
   let ppl (mp,sel) =
     push_visible mp [];
-    let p = prlist_strict pp sel in
+    let p = prlist_sep_nonempty fnl2 f sel in
     (* for monolithic extraction, we try to simulate the unavailability
        of [MPfile] in names by artificially nesting these [MPfile] *)
     (if modular () then pop_visible ()); p
   in
-  let p = prlist_strict ppl s in
+  let p = prlist_sep_nonempty fnl2 ppl s in
   (if not (modular ()) then repeat (List.length s) pop_visible ());
-  p
+  p ++ fnl ()
 
 let pp_struct s = do_struct pp_structure_elem s
 
 let pp_signature s = do_struct pp_specif s
 
-let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
-
 let ocaml_descr = {
   keywords = keywords;
   file_suffix = ".ml";
@@ -757,5 +755,3 @@ let ocaml_descr = {
   pp_sig = pp_signature;
   pp_decl = pp_decl;
 }
-
-
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 4901cf1807..0b2a04d3f1 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -183,7 +183,8 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
+	    (not (is_custom r) &&
+             match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
-- 
cgit v1.2.3


From 1e7f3425a8d83fd8606959ec81e91b8e05607b06 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 09:27:45 +0100
Subject: Extraction: fix a pretty-print issue

 Some explicit '\n' in Pp.str were interacting badly with Format boxes
 in Compcert, leading to right-flushed "sig..end" blocks in some .mli
---
 plugins/extraction/ocaml.ml | 31 +++++++++++++++++++------------
 1 file changed, 19 insertions(+), 12 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 259ec49c07..7efe0b4e1f 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -55,29 +55,36 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
   Id.Set.empty
 
-let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
+(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"],
+   the '\n' character interacts badly with the Format boxing mechanism *)
+
+let pp_open mp = str ("open "^ string_of_modfile mp) ++ fnl ()
 
 let pp_comment s = str "(* " ++ hov 0 s ++ str " *)"
 
 let pp_header_comment = function
   | None -> mt ()
-  | Some com -> pp_comment com ++ fnl () ++ fnl ()
+  | Some com -> pp_comment com ++ fnl2 ()
+
+let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+
+let pp_tdummy usf =
+  if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
+
+let pp_mldummy usf =
+  if usf.mldummy then
+    str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl ()
+  else mt ()
 
 let preamble _ comment used_modules usf =
   pp_header_comment comment ++
-  prlist pp_open used_modules ++
-  (if List.is_empty used_modules then mt () else fnl ()) ++
-  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
-  (if usf.mldummy then
-     str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
-   else mt ()) ++
-  (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
+  then_nl (prlist pp_open used_modules) ++
+  then_nl (pp_tdummy usf ++ pp_mldummy usf)
 
 let sig_preamble _ comment used_modules usf =
   pp_header_comment comment ++
-  prlist pp_open used_modules ++
-  (if List.is_empty used_modules then mt () else fnl ()) ++
-  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
+  then_nl (prlist pp_open used_modules) ++
+  then_nl (pp_tdummy usf)
 
 (*s The pretty-printer for Ocaml syntax*)
 
-- 
cgit v1.2.3


From a2a81cec811a8257e47ceb1b9ea3de6d1c2607ee Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 09:57:50 +0100
Subject: Extraction: also get rid of explicit '\n' for haskell

---
 plugins/extraction/haskell.ml | 71 ++++++++++++++++++++++---------------------
 1 file changed, 37 insertions(+), 34 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index dd66a6a98f..00259750d6 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -35,56 +35,59 @@ let keywords =
 let pp_comment s = str "-- " ++ s ++ fnl ()
 let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
 
+(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"],
+   the '\n' character interacts badly with the Format boxing mechanism *)
+
 let preamble mod_name comment used_modules usf =
-  let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
+  let pp_import mp = str ("import qualified "^ string_of_modfile mp) ++ fnl ()
   in
   (if not (usf.magic || usf.tunknown) then mt ()
    else
      str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
-     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
-  ++ fnl () ++ fnl ()
+     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}" ++ fnl2 ())
   ++
   (match comment with
     | None -> mt ()
-    | Some com -> pp_bracket_comment com ++ fnl () ++ fnl ())
+    | Some com -> pp_bracket_comment com ++ fnl2 ())
   ++
   str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
   str "import qualified Prelude" ++ fnl () ++
-  prlist pp_import used_modules ++ fnl () ++
-  (if List.is_empty used_modules then mt () else fnl ()) ++
+  prlist pp_import used_modules ++ fnl ()
+  ++
   (if not (usf.magic || usf.tunknown) then mt ()
-   else str "\
-\n#ifdef __GLASGOW_HASKELL__\
-\nimport qualified GHC.Base\
-\nimport qualified GHC.Prim\
-\n#else\
-\n-- HUGS\
-\nimport qualified IOExts\
-\n#endif" ++ fnl2 ())
+   else
+     str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
+     str "import qualified GHC.Base" ++ fnl () ++
+     str "import qualified GHC.Prim" ++ fnl () ++
+     str "#else" ++ fnl () ++
+     str "-- HUGS" ++ fnl () ++
+     str "import qualified IOExts" ++ fnl () ++
+     str "#endif" ++ fnl2 ())
   ++
   (if not usf.magic then mt ()
-   else str "\
-\n#ifdef __GLASGOW_HASKELL__\
-\nunsafeCoerce :: a -> b\
-\nunsafeCoerce = GHC.Base.unsafeCoerce#\
-\n#else\
-\n-- HUGS\
-\nunsafeCoerce :: a -> b\
-\nunsafeCoerce = IOExts.unsafeCoerce\
-\n#endif" ++ fnl2 ())
+   else
+     str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
+     str "unsafeCoerce :: a -> b" ++ fnl () ++
+     str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl () ++
+     str "#else" ++ fnl () ++
+     str "-- HUGS" ++ fnl () ++
+     str "unsafeCoerce :: a -> b" ++ fnl () ++
+     str "unsafeCoerce = IOExts.unsafeCoerce" ++ fnl () ++
+     str "#endif" ++ fnl2 ())
   ++
   (if not usf.tunknown then mt ()
-   else str "\
-\n#ifdef __GLASGOW_HASKELL__\
-\ntype Any = GHC.Prim.Any\
-\n#else\
-\n-- HUGS\
-\ntype Any = ()\
-\n#endif" ++ fnl2 ())
+   else
+     str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
+     str "type Any = GHC.Prim.Any" ++ fnl () ++
+     str "#else" ++ fnl () ++
+     str "-- HUGS" ++ fnl () ++
+     str "type Any = ()" ++ fnl () ++
+     str "#endif" ++ fnl2 ())
   ++
   (if not usf.mldummy then mt ()
-   else str "__ :: any" ++ fnl () ++
-        str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
+   else
+     str "__ :: any" ++ fnl () ++
+     str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
 
 let pp_abst = function
   | [] -> (mt ())
@@ -120,7 +123,7 @@ let rec pp_type par vl t =
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "()"
     | Tunknown -> str "Any"
-    | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
+    | Taxiom -> str "() -- AXIOM TO BE REALIZED" ++ fnl ()
  in
   hov 0 (pp_rec par t)
 
@@ -323,7 +326,7 @@ let pp_decl = function
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
 	  with Not_found ->
 	    prlist (fun id -> pr_id id ++ str " ") l ++
-	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
+	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl ()
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
 	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
-- 
cgit v1.2.3


From b1cfb65fbf7c11cb5b9acc8039bcf5e36882a685 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 11:11:49 +0100
Subject: Extraction: cosmetically avoid generating spaces on empty lines

---
 plugins/extraction/extract_env.ml |  2 +-
 plugins/extraction/ocaml.ml       | 19 ++++++++++++-------
 2 files changed, 13 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3d32398ffd..7014df83fd 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -458,7 +458,7 @@ let print_one_decl struc mp decl =
   push_visible mp [];
   let ans = d.pp_decl decl in
   pop_visible ();
-  ans
+  v 0 ans
 
 (*s Extraction of a ml struct to a file. *)
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 7efe0b4e1f..6ff4c25ec4 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -388,9 +388,14 @@ and pp_fix par env i (ids,bl) args =
 	  fnl () ++
 	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
+(* Ad-hoc double-newline in v boxes, with enough negative whitespace
+   to avoid indenting the intermediate blank line *)
+
+let cut2 () = brk (0,-100000) ++ brk (0,0)
+
 let pp_val e typ =
   hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++
-  str " **)")  ++ fnl2 ()
+  str " **)")  ++ cut2 ()
 
 (*s Pretty-printing of [Dfix] *)
 
@@ -411,7 +416,7 @@ let pp_Dfix (rv,c,t) =
 	  if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
 	  else pp_function (empty_env ()) c.(i)
 	in
-	(if init then mt () else fnl2 ()) ++
+	(if init then mt () else cut2 ()) ++
 	pp_val names.(i) t.(i) ++
 	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
 	pp false (i+1)
@@ -644,7 +649,7 @@ and pp_module_type params = function
       let l = List.rev l in
       pop_visible ();
       str "sig" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
 	fnl () ++ str "end"
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
       let ids = pp_parameters (rename_tvars keywords vl) in
@@ -723,7 +728,7 @@ and pp_module_expr params = function
       let l = List.rev l in
       pop_visible ();
       str "struct" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
       fnl () ++ str "end"
 
 let rec prlist_sep_nonempty sep f = function
@@ -738,14 +743,14 @@ let rec prlist_sep_nonempty sep f = function
 let do_struct f s =
   let ppl (mp,sel) =
     push_visible mp [];
-    let p = prlist_sep_nonempty fnl2 f sel in
+    let p = prlist_sep_nonempty cut2 f sel in
     (* for monolithic extraction, we try to simulate the unavailability
        of [MPfile] in names by artificially nesting these [MPfile] *)
     (if modular () then pop_visible ()); p
   in
-  let p = prlist_sep_nonempty fnl2 ppl s in
+  let p = prlist_sep_nonempty cut2 ppl s in
   (if not (modular ()) then repeat (List.length s) pop_visible ());
-  p ++ fnl ()
+  v 0 p ++ fnl ()
 
 let pp_struct s = do_struct pp_structure_elem s
 
-- 
cgit v1.2.3


From 7d2f7e1665136f5d7a2882f733ae807e1a55dc7c Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 19:46:25 +0100
Subject: Extraction: propagate implicit args in inner fixpoint (bug #4243 part
 2)

 In front of "let rec f x y = ... in f n m", if n is now an implicit argument,
 then the argument x of the inner fixpoint f is also considered as implicit.
 This optimization is rather ad-hoc, since we only handle MLapp(MLfix()) for
 now, and the implicit argument should be reused verbatim as argument.
 Note that it might happen that x cannot be implicit in f. But in this
 case we would have add an error message about n still occurring somewhere...
 At least this small heuristic was easy to add, and was sufficient to solve
 the part 2 of bug #4243.
---
 plugins/extraction/mlutil.ml | 61 +++++++++++++++++++++++++++-----------------
 1 file changed, 37 insertions(+), 24 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 402370eece..70249193e5 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1077,11 +1077,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
@@ -1093,7 +1101,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. *)
@@ -1135,13 +1143,13 @@ let term_expunge s (ids,c) =
     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
@@ -1152,41 +1160,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))
@@ -1198,21 +1211,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. *)
 
-- 
cgit v1.2.3


From ce395ca02311bbe6ecc1b2782e74312272dd15ec Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 14 Dec 2015 22:31:41 +0100
Subject: Extraction: allow basic beta-reduction even through a MLmagic (fix
 #2795)

 This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
 to properly investigate the interaction between all the other optimizations
 and MLmagic. But well, at least this precise bug is fixed now.
---
 plugins/extraction/mlutil.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 70249193e5..bfd0794de2 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -987,6 +987,10 @@ 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) *)
+      simpl_app o 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)))
-- 
cgit v1.2.3