From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 13 Oct 2015 18:30:47 +0200
Subject: Fix some typos.

---
 plugins/extraction/CHANGES   |  6 +++---
 plugins/extraction/mlutil.ml | 14 +++++++-------
 2 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index fbcd01a15e..cf97ae3ab8 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -193,7 +193,7 @@ beginning of files. Possible clashes are dealt with.
 in extracted code. 
 
 
-* A few constants are explicitely declared to be inlined in extracted code. 
+* A few constants are explicitly declared to be inlined in extracted code.
 For the moment there are: 
 	Wf.Acc_rec
 	Wf.Acc_rect
@@ -234,12 +234,12 @@ Those two commands enable a precise control of what is inlined and what is not.
 
 Print Extraction Inline. 
 
-Sum up the current state of the table recording the custom inlings 
+Sum up the current state of the table recording the custom inlinings
 (Extraction (No)Inline). 
 
 Reset Extraction Inline. 
 
-Put the table recording the custom inlings back to empty. 
+Put the table recording the custom inlinings back to empty.
 
 As a consequence, there is no more need for options inside the commands of 
 extraction: 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9fdb0205f5..6fc1195fba 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -490,8 +490,8 @@ let ast_occurs_itvl k k' t =
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
-(* Number of occurences of [Rel 1] in [t], with special treatment of match:
-   occurences in different branches aren't added, but we rather use max. *)
+(* Number of occurrences of [Rel 1] in [t], with special treatment of match:
+   occurrences in different branches aren't added, but we rather use max. *)
 
 let nb_occur_match =
   let rec nb k = function
@@ -851,7 +851,7 @@ let factor_branches o typ br =
     else Some (br_factor, br_set)
   end
 
-(*s If all branches are functions, try to permut the case and the functions. *)
+(*s If all branches are functions, try to permute the case and the functions. *)
 
 let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
@@ -1127,7 +1127,7 @@ let term_expunge s (ids,c) =
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+(*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].
   It makes eta-expansion if needed. *)
 
@@ -1351,10 +1351,10 @@ let is_not_strict t =
    We expand small terms with at least one non-strict
    variable (i.e. a variable that may not be evaluated).
 
-   Futhermore we don't expand fixpoints.
+   Furthermore we don't expand fixpoints.
 
-   Moreover, as mentionned by X. Leroy (bug #2241),
-   inling a constant from inside an opaque module might
+   Moreover, as mentioned by X. Leroy (bug #2241),
+   inlining a constant from inside an opaque module might
    break types. To avoid that, we require below that
    both [r] and its body are globally visible. This isn't
    fully satisfactory, since [r] might not be visible (functor),
-- 
cgit v1.2.3


From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 plugins/extraction/extraction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6ae519ef60..1112c3b890 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -734,7 +734,7 @@ and extract_cst_app env mle mlt kn u args =
   if la >= ls
   then
     (* Enough args, cleanup already done in [mla], we only add the
-       additionnal dummy if needed. *)
+       additional dummy if needed. *)
     put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla))
   else
     (* Partially applied function with some logical arg missing.
@@ -748,7 +748,7 @@ and extract_cst_app env mle mlt kn u args =
 (*s Extraction of an inductive constructor applied to arguments. *)
 
 (* \begin{itemize}
-   \item In ML, contructor arguments are uncurryfied.
+   \item In ML, constructor arguments are uncurryfied.
    \item We managed to suppress logical parts inside inductive definitions,
    but they must appears outside (for partial applications for instance)
    \item We also suppressed all Coq parameters to the inductives, since
-- 
cgit v1.2.3


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/extraction')

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/extraction')

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/extraction')

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/extraction')

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/extraction')

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/extraction')

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/extraction')

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/extraction')

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/extraction')

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/extraction')

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


From 4b197ed247d1f30ff40fa59f85b070766f305bea Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 15 Dec 2015 11:15:00 +0100
Subject: Extraction: replace unused variable names by _ in funs and matchs
 (fix #2842)

 This is done via a unique pass which seems roughly linear in practice,
 even on big developments like CompCert. There's a List.nth in an env at
 each MLrel, that could be made logarithmic if necessary via Okasaki's
 skew list for instance.

 Another approach would be to keep names (as a form of documentation), but
 prefix them by _ to please OCaml's warnings. For now, let's be radical and
 use the _ pattern.
---
 plugins/extraction/mlutil.ml  | 69 +++++++++++++++++++++++++++++++++++++++++++
 plugins/extraction/mlutil.mli |  2 ++
 plugins/extraction/modutil.ml |  6 ++--
 3 files changed, 75 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index bfd0794de2..2b606bf13c 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -511,6 +511,75 @@ let nb_occur_match =
     | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0
   in nb 1
 
+(* Replace unused variables by _ *)
+
+let dump_unused_vars a =
+  let dump_id = function
+    | Dummy -> Dummy
+    | Id _ -> Id dummy_name
+    | Tmp _ -> Tmp dummy_name
+  in
+  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(dump_id id,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(dump_id id,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 dump_id id)
+          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. *)
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index c380dfb3e3..c07cee7136 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -111,6 +111,8 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast
 
 val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast
 
+val dump_unused_vars : ml_ast -> ml_ast
+
 val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index e8383bda59..6f354b1ce5 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -263,10 +263,12 @@ let dfix_to_mlfix rv av i =
    order to preserve the global interface, later [depcheck_se] will get
    rid of them if possible *)
 
+let optim_ast t = dump_unused_vars (normalize t)
+
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
-      let a = normalize (ast_glob_subst !s a) in
+      let a = optim_ast (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
       let d = match optimize_fix a with
@@ -276,7 +278,7 @@ let rec optim_se top to_appear s = function
       in
       (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
-      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
+      let av = Array.map (fun a -> optim_ast (ast_glob_subst !s a)) av in
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do
-- 
cgit v1.2.3


From 3c535011374382bc205a68b1cb59cfa7247d544a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 15 Dec 2015 17:46:25 +0100
Subject: Extraction: fix a few little glitches with my last commit (replacing
 unused vars by _)

---
 plugins/extraction/common.ml  |  5 +----
 plugins/extraction/haskell.ml |  6 +++++-
 plugins/extraction/mlutil.ml  | 11 +++--------
 plugins/extraction/modutil.ml | 11 +++++------
 plugins/extraction/ocaml.ml   |  6 +++++-
 5 files changed, 19 insertions(+), 20 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 97f856944c..8cf3b8194c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -171,10 +171,7 @@ let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
 
-let get_db_name n (db,_) =
-  let id = List.nth db (pred n) in
-  if Id.equal id dummy_name then Id.of_string "__" else id
-
+let get_db_name n (db,_) = List.nth db (pred n)
 
 (*S Renamings of global objects. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 00259750d6..da7a4265e6 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -143,7 +143,11 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+	let id = get_db_name n env in
+        (* Try to survive to the occurrence of a Dummy rel.
+           TODO: we should get rid of this hack (cf. #592) *)
+        let id = if Id.equal id dummy_name then Id.of_string "__" else id in
+        apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 2b606bf13c..eb3046f031 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -514,11 +514,6 @@ let nb_occur_match =
 (* Replace unused variables by _ *)
 
 let dump_unused_vars a =
-  let dump_id = function
-    | Dummy -> Dummy
-    | Id _ -> Id dummy_name
-    | Tmp _ -> Tmp dummy_name
-  in
   let rec ren env a = match a with
     | MLrel i ->
        let () = (List.nth env (i-1)) := true in a
@@ -527,7 +522,7 @@ let dump_unused_vars a =
        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(dump_id id,b')
+       else MLlam(Dummy,b')
 
     | MLletin (id,b,c) ->
        let occ_id = ref false in
@@ -537,7 +532,7 @@ let dump_unused_vars a =
          if b' == b && c' == c then a else MLletin(id,b',c')
        else
          (* 'let' without occurrence: shouldn't happen after simpl *)
-         MLletin(dump_id id,b',c')
+         MLletin(Dummy,b',c')
 
     | MLcase (t,e,br) ->
        let e' = ren env e in
@@ -572,7 +567,7 @@ let dump_unused_vars a =
       let b' = ren (List.rev_append occs env) b in
       let ids' =
         List.map2
-          (fun id occ -> if !occ then id else dump_id id)
+          (fun id occ -> if !occ then id else Dummy)
           ids occs
       in
       if b' == b && List.equal eq_ml_ident ids ids' then tr
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 6f354b1ce5..c3dc286cd1 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -263,29 +263,28 @@ let dfix_to_mlfix rv av i =
    order to preserve the global interface, later [depcheck_se] will get
    rid of them if possible *)
 
-let optim_ast t = dump_unused_vars (normalize t)
-
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
-      let a = optim_ast (ast_glob_subst !s a) in
+      let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
-      let d = match optimize_fix a with
+      let d = match dump_unused_vars (optimize_fix a) with
 	| MLfix (0, _, [|c|]) ->
 	  Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
 	| a -> Dterm (r, a, t)
       in
       (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
-      let av = Array.map (fun a -> optim_ast (ast_glob_subst !s a)) av in
+      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do
 	if inline rv.(i) fake_body
 	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
       done;
-      (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
+      let av' = Array.map dump_unused_vars av in
+      (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse)
   | (l,SEmodule m) :: lse ->
       let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
       in (l,SEmodule m) :: (optim_se top to_appear s lse)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 6ff4c25ec4..8c86c77112 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -178,7 +178,11 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+	let id = get_db_name n env in
+        (* Try to survive to the occurrence of a Dummy rel.
+           TODO: we should get rid of this hack (cf. #592) *)
+        let id = if Id.equal id dummy_name then Id.of_string "__" else id in
+        apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
-- 
cgit v1.2.3


From 0a89d4805a29628c82b994958362dc9d92709020 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 15 Dec 2015 18:56:08 +0100
Subject: Extraction: more cautious use of intermediate result caching (fix
 #3923)

 During an extraction, a few tables are maintained to cache
 intermediate results. Due to modules, the kernel_name index
 for these caching tables aren't enough. For instance, in
 bug #3923, a constant is first transparent (from inside the
 module) then opaque (when seen from the signature). The previous
 protections were actually obsolete (tests via visible_con), we
 now checks that the constant_body is still the same.
---
 plugins/extraction/extraction.ml | 100 +++++++++++++--------------------------
 plugins/extraction/table.ml      |  48 +++++++++++++------
 plugins/extraction/table.mli     |  19 +++++---
 3 files changed, 78 insertions(+), 89 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f4d14af624..2dc2420c46 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -201,36 +201,6 @@ let parse_ind_args si args relmax =
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
-let oib_equal o1 o2 =
-  Id.equal o1.mind_typename o2.mind_typename &&
-  List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
-    begin
-      match o1.mind_arity, o2.mind_arity with
-      | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
-	eq_constr c1 c2 && Sorts.equal s1 s2
-      | TemplateArity p1, TemplateArity p2 ->
-	let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in
-	  List.equal eq p1.template_param_levels p2.template_param_levels &&
-	    Univ.Universe.equal p1.template_level p2.template_level
-      | _, _ -> false
-    end &&
-    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
-
-let eq_record x y =
-  Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y
-
-let mib_equal m1 m2 =
-  Array.equal oib_equal m1.mind_packets m1.mind_packets &&
-  eq_record m1.mind_record m2.mind_record &&
-  (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite &&
-  Int.equal m1.mind_ntypes m2.mind_ntypes &&
-  List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
-  Int.equal m1.mind_nparams m2.mind_nparams &&
-  Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
-  List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
-  (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *)
-  (* m1.mind_universes = m2.mind_universes *)
-
 (*S Extraction of a type. *)
 
 (* [extract_type env db c args] is used to produce an ML type from the
@@ -360,14 +330,9 @@ and extract_type_scheme env db c p =
 
 and extract_ind env kn = (* kn is supposed to be in long form *)
   let mib = Environ.lookup_mind kn env in
-  try
-    (* For a same kn, we can get various bodies due to module substitutions.
-       We hence check that the mib has not changed from recording
-       time to retrieving time. Ideally we should also check the env. *)
-    let (mib0,ml_ind) = lookup_ind kn in
-    if not (mib_equal mib mib0) then raise Not_found;
-    ml_ind
-  with Not_found ->
+  match lookup_ind kn mib with
+  | Some ml_ind -> ml_ind
+  | None ->
     (* First, if this inductive is aliased via a Module,
        we process the original inductive if possible.
        When at toplevel of the monolithic case, we cannot do much
@@ -523,28 +488,25 @@ and extract_type_cons env db dbmap c i =
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
 and mlt_env env r = match r with
+  | IndRef _ | ConstructRef _ | VarRef _ -> None
   | ConstRef kn ->
-      (try
-	 if not (visible_con kn) then raise Not_found;
-	 match lookup_term kn with
-	   | Dtype (_,vl,mlt) -> Some mlt
+     let cb = Environ.lookup_constant kn env in
+     match cb.const_body with
+     | Undef _ | OpaqueDef _ -> None
+     | Def l_body ->
+        match lookup_typedef kn cb with
+        | Some _ as o -> o
+        | None ->
+           let typ = Typeops.type_of_constant_type env cb.const_type
+           (* FIXME not sure if we should instantiate univs here *) in
+	   match flag_of_type env typ with
+	   | Info,TypeScheme ->
+	      let body = Mod_subst.force_constr l_body in
+	      let s = type_sign env typ in
+	      let db = db_from_sign s in
+	      let t = extract_type_scheme env db body (List.length s)
+	      in add_typedef kn cb t; Some t
 	   | _ -> None
-       with Not_found ->
-	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type
- (* FIXME not sure if we should instantiate univs here *) in
-	 match cb.const_body with
-	   | Undef _ | OpaqueDef _ -> None
-	   | Def l_body ->
-	       (match flag_of_type env typ with
-		  | Info,TypeScheme ->
-		      let body = Mod_subst.force_constr l_body in
-		      let s,vl = type_sign_vl env typ in
-		      let db = db_from_sign s in
-		      let t = extract_type_scheme env db body (List.length s)
-		      in add_term kn (Dtype (r, vl, t)); Some t
-		  | _ -> None))
-  | _ -> None
 
 and expand env = type_expand (mlt_env env)
 and type2signature env = type_to_signature (mlt_env env)
@@ -555,16 +517,18 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env)
 (*s Extraction of the type of a constant. *)
 
 let record_constant_type env kn opt_typ =
-  try
-    if not (visible_con kn) then raise Not_found;
-    lookup_type kn
-  with Not_found ->
-    let typ = match opt_typ with
-      | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type
-      | Some typ -> typ
-    in let mlt = extract_type env [] 1 typ []
-    in let schema = (type_maxvar mlt, mlt)
-    in add_type kn schema; schema
+  let cb = lookup_constant kn env in
+  match lookup_cst_type kn cb with
+  | Some schema -> schema
+  | None ->
+     let typ = match opt_typ with
+       | None -> Typeops.type_of_constant_type env cb.const_type
+       | Some typ -> typ
+     in
+     let mlt = extract_type env [] 1 typ [] in
+     let schema = (type_maxvar mlt, mlt) in
+     let () = add_cst_type kn cb schema in
+     schema
 
 (*S Extraction of a term. *)
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 63d792e363..9feaea8cdb 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -72,8 +72,6 @@ let mp_length mp =
     | _ -> 1
   in len mp
 
-let visible_con kn = at_toplevel (base_mp (con_modpath kn))
-
 let rec prefixes_mp mp = match mp with
   | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
   | _ -> MPset.singleton mp
@@ -105,17 +103,30 @@ let labels_of_ref r =
 (* Theses tables are not registered within coq save/undo mechanism
    since we reset their contents at each run of Extraction *)
 
-(*s Constants tables. *)
+(* We use [constant_body] (resp. [mutual_inductive_body]) as checksum
+   to ensure that the table contents aren't outdated. *)
 
-let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t)
-let init_terms () = terms := Cmap_env.empty
-let add_term kn d = terms := Cmap_env.add kn d !terms
-let lookup_term kn = Cmap_env.find kn !terms
+(*s Constants tables. *)
 
-let types = ref (Cmap_env.empty : ml_schema Cmap_env.t)
-let init_types () = types := Cmap_env.empty
-let add_type kn s = types := Cmap_env.add kn s !types
-let lookup_type kn = Cmap_env.find kn !types
+let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t)
+let init_typedefs () = typedefs := Cmap_env.empty
+let add_typedef kn cb t =
+  typedefs := Cmap_env.add kn (cb,t) !typedefs
+let lookup_typedef kn cb =
+  try
+    let (cb0,t) = Cmap_env.find kn !typedefs in
+    if cb0 == cb then Some t else None
+  with Not_found -> None
+
+let cst_types =
+  ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t)
+let init_cst_types () = cst_types := Cmap_env.empty
+let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types
+let lookup_cst_type kn cb =
+  try
+    let (cb0,s) = Cmap_env.find kn !cst_types in
+    if cb0 == cb then Some s else None
+  with Not_found -> None
 
 (*s Inductives table. *)
 
@@ -124,7 +135,14 @@ let inductives =
 let init_inductives () = inductives := Mindmap_env.empty
 let add_ind kn mib ml_ind =
   inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = Mindmap_env.find kn !inductives
+let lookup_ind kn mib =
+  try
+    let (mib0,ml_ind) = Mindmap_env.find kn !inductives in
+    if mib == mib0 then Some ml_ind
+    else None
+  with Not_found -> None
+
+let unsafe_lookup_ind kn = snd (Mindmap_env.find kn !inductives)
 
 let inductive_kinds =
   ref (Mindmap_env.empty : inductive_kind Mindmap_env.t)
@@ -244,10 +262,10 @@ let safe_basename_of_global r =
     | ConstRef kn -> Label.to_id (con_label kn)
     | IndRef (kn,0) -> Label.to_id (mind_label kn)
     | IndRef (kn,i) ->
-      (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+      (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
     | ConstructRef ((kn,i),j) ->
-      (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
+      (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
        with Not_found -> last_chance r)
     | VarRef _ -> assert false
 
@@ -876,6 +894,6 @@ let extract_inductive r s l optstr =
 (*s Tables synchronization. *)
 
 let reset_tables () =
-  init_terms (); init_types (); init_inductives ();
+  init_typedefs (); init_cst_types (); init_inductives ();
   init_inductive_kinds (); init_recursors ();
   init_projs (); init_axioms (); init_opaques (); reset_modfile ()
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a6734dae86..916cf3ad6b 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -55,7 +55,6 @@ val string_of_modfile : module_path -> string
 val file_of_modfile : module_path -> string
 val is_toplevel : module_path -> bool
 val at_toplevel : module_path -> bool
-val visible_con : constant -> bool
 val mp_length : module_path -> int
 val prefixes_mp : module_path -> MPset.t
 val common_prefix_from_list :
@@ -65,14 +64,22 @@ val labels_of_ref : global_reference -> module_path * Label.t list
 
 (*s Some table-related operations *)
 
-val add_term : constant -> ml_decl -> unit
-val lookup_term : constant -> ml_decl
+(* For avoiding repeated extraction of the same constant or inductive,
+   we use cache functions below. Indexing by constant name isn't enough,
+   due to modules we could have a same constant name but different
+   content. So we check that the [constant_body] hasn't changed from
+   recording time to retrieving time. Same for inductive : we store
+   [mutual_inductive_body] as checksum. In both case, we should ideally
+   also check the env *)
 
-val add_type : constant -> ml_schema -> unit
-val lookup_type : constant -> ml_schema
+val add_typedef : constant -> constant_body -> ml_type -> unit
+val lookup_typedef : constant -> constant_body -> ml_type option
+
+val add_cst_type : constant -> constant_body -> ml_schema -> unit
+val lookup_cst_type : constant -> constant_body -> ml_schema option
 
 val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
-val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind
+val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option
 
 val add_inductive_kind : mutual_inductive -> inductive_kind -> unit
 val is_coinductive : global_reference -> bool
-- 
cgit v1.2.3


From 0c60735279301d22ac3e03f862f86997cb85bce0 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 16 Dec 2015 00:59:38 +0100
Subject: Extraction: fixed beta-red with Obj.magic (#2795 again) + other
 simplifications

 Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v)
 by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree:
 the argument v should also be magic now, otherwise it might not have
 the same type as x.

 This optimization is now correctly done, and to mitigate the potential inflation
 of Obj.magic, I've added a few simplification rules to avoid redundant magics,
 push them down inside terms, favor the form (Obj.magic f x y z), etc.
---
 plugins/extraction/mlutil.ml | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index eb3046f031..d06583010f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1035,6 +1035,13 @@ 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 *)
@@ -1053,8 +1060,17 @@ and simpl_app o a = function
 	     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))
+         and the lambda, to simplify things a bit (see #2795).
+         Alas, the 1st argument must also be magic then. *)
+      let a' = match a with
+        | MLmagic _ :: _ -> a
+        | e::a' -> MLmagic e::a'
+        | [] -> assert false
+      in
+      simpl_app o a' (MLlam (id,MLmagic t))
+  | MLmagic _ as e ->
+      (* When the head is magic, no need for magic on args *)
+      MLapp (e, List.map (function MLmagic e -> e | e -> e) a)
   | 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


From 53ab313dcf7ae524a9a8312658c1e9869a4039f7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 16 Dec 2015 11:43:53 +0100
Subject: Extraction: slightly better heuristic for Obj.magic simplifications

 On an application (f args) where the head is magic, we first remove Obj.magic
 on arguments before continuing with simplifications (that may push magic down
 inside the arguments).

 For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end
 with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as
 before.
---
 plugins/extraction/mlutil.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index d06583010f..62724f2119 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1013,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)
@@ -1047,7 +1058,6 @@ let rec simpl o = function
 (* 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 *)
@@ -1062,15 +1072,7 @@ and simpl_app o a = function
       (* 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. *)
-      let a' = match a with
-        | MLmagic _ :: _ -> a
-        | e::a' -> MLmagic e::a'
-        | [] -> assert false
-      in
-      simpl_app o a' (MLlam (id,MLmagic t))
-  | MLmagic _ as e ->
-      (* When the head is magic, no need for magic on args *)
-      MLapp (e, List.map (function MLmagic e -> e | e -> e) a)
+      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)))
-- 
cgit v1.2.3


From 5122a39888cfc6afd2383d59465324dd67b69f4a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 21 Dec 2015 18:56:43 +0100
Subject: Inclusion of functors with restricted signature is now forbidden (fix
 #3746)

 The previous behavior was to include the interface of such a functor,
 possibly leading to the creation of unexpected axioms, see bug report #3746.
 In the case of non-functor module with restricted signature, we could
 simply refer to the original objects (strengthening), but for a functor,
 the inner objects have no existence yet. As said in the new error message,
 a simple workaround is hence to first instantiate the functor, then include
 the local instance:

  Module LocalInstance := Funct(Args).
  Include LocalInstance.

 By the way, the mod_type_alg field is now filled more systematically,
 cf new comments in declarations.mli. This way, we could use it to know
 whether a module had been given a restricted signature (via ":"). Earlier,
 some mod_type_alg were None in situations not handled by the extraction
 (MEapply of module type).

 Some code refactoring on the fly.
---
 plugins/extraction/extract_env.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7014df83fd..9964280336 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -177,8 +177,7 @@ let factor_fix env l cb msb =
 
 let expand_mexpr env mp me =
   let inl = Some (Flags.get_inline_level()) in
-  let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in
-  sign
+  Mod_typing.translate_mse env (Some mp) inl me
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
@@ -231,10 +230,9 @@ let rec extract_structure_spec env mp reso = function
 
 (* From [module_expression] to specifications *)
 
-(* Invariant: the [me] given to [extract_mexpr_spec] should either come
-   from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
-   This way, any encountered [MEident] should be a true module type.
-*)
+(* Invariant: the [me_alg] given to [extract_mexpr_spec] and
+   [extract_mexpression_spec] should come from a [mod_type_alg] field.
+   This way, any encountered [MEident] should be a true module type. *)
 
 and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEident mp -> Visit.add_mp_all mp; MTident mp
@@ -247,7 +245,9 @@ 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 no_delta (*TODO*) me_struct
+  | MEapply _ ->
+     (* No higher-order module type in OCaml : we use the expanded version *)
+     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') ->
@@ -335,7 +335,8 @@ 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 no_delta ~all:true (expand_mexpr env mp me)
+      let sign,_,delta,_ = expand_mexpr env mp me in
+      extract_msignature env mp delta ~all:true sign
   | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp_all mp; Miniml.MEident mp
-- 
cgit v1.2.3


From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Dec 2015 22:35:09 +0100
Subject: Do not compose "str" and "to_string" whenever possible.

For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
---
 plugins/extraction/table.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 9feaea8cdb..30486879ee 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (Lib.current_mp ()) with
 	  | MPfile dp' when not (DirPath.equal dp dp') ->
-	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
+	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()
-- 
cgit v1.2.3


From 456e2be8af1d4a0cf2461d62dc5e1b4b24b2a552 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 4 Jan 2016 18:04:18 +0100
Subject: Extraction: msg_notice instead of msg_info.

---
 plugins/extraction/extract_env.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 9964280336..657a91c0c1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -542,7 +542,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
   if not (Int.equal (Buffer.length buf) 0) then begin
-    Pp.msg_info (str (Buffer.contents buf));
+    Pp.msg_notice (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -636,7 +636,7 @@ let simple_extraction r =
       in
       let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
       reset ();
-      Pp.msg_info ans
+      Pp.msg_notice ans
   | _ -> assert false
 
 
-- 
cgit v1.2.3


From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 6 Jan 2016 00:58:42 +0100
Subject: Protect code against changes in Map interface.

The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
---
 plugins/extraction/table.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 916cf3ad6b..4e638a0ace 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Miniml
 open Declarations
 
 module Refset' : CSig.SetS with type elt = global_reference
-module Refmap' : Map.S with type key = global_reference
+module Refmap' : CSig.MapS with type key = global_reference
 
 val safe_basename_of_global : global_reference -> Id.t
 
-- 
cgit v1.2.3


From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 8 Jan 2016 10:00:21 +0100
Subject: CLEANUP: kernel/context.ml{,i}

The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.

Some missing comments were added to the *.mli file.

The output of ocamldoc was checked whether it looks in a reasonable way.

"TODO: cleanup" was removed

The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)

The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)

The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)

The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})

The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.

Thrown exceptions are now documented.

Naming of formal parameters was made more consistent across different functions.

Comments of similar functions in different modules are now consistent.

Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
 It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
 we can see the comments also there and do not need to open a different file if we want to see it.)

When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)

"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)

An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
---
 plugins/extraction/extraction.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 2dc2420c46..923743eceb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Environ
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 plugins/extraction/ExtrOcamlBasic.v      | 2 +-
 plugins/extraction/ExtrOcamlBigIntConv.v | 2 +-
 plugins/extraction/ExtrOcamlIntConv.v    | 2 +-
 plugins/extraction/ExtrOcamlNatBigInt.v  | 2 +-
 plugins/extraction/ExtrOcamlNatInt.v     | 2 +-
 plugins/extraction/ExtrOcamlString.v     | 2 +-
 plugins/extraction/ExtrOcamlZBigInt.v    | 2 +-
 plugins/extraction/ExtrOcamlZInt.v       | 2 +-
 plugins/extraction/big.ml                | 2 +-
 plugins/extraction/common.ml             | 2 +-
 plugins/extraction/common.mli            | 2 +-
 plugins/extraction/extract_env.ml        | 2 +-
 plugins/extraction/extract_env.mli       | 2 +-
 plugins/extraction/extraction.ml         | 2 +-
 plugins/extraction/extraction.mli        | 2 +-
 plugins/extraction/g_extraction.ml4      | 2 +-
 plugins/extraction/haskell.ml            | 2 +-
 plugins/extraction/haskell.mli           | 2 +-
 plugins/extraction/miniml.mli            | 2 +-
 plugins/extraction/mlutil.ml             | 2 +-
 plugins/extraction/mlutil.mli            | 2 +-
 plugins/extraction/modutil.ml            | 2 +-
 plugins/extraction/modutil.mli           | 2 +-
 plugins/extraction/ocaml.ml              | 2 +-
 plugins/extraction/ocaml.mli             | 2 +-
 plugins/extraction/scheme.ml             | 2 +-
 plugins/extraction/scheme.mli            | 2 +-
 plugins/extraction/table.ml              | 2 +-
 plugins/extraction/table.mli             | 2 +-
 29 files changed, 29 insertions(+), 29 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 9dbda8216c..d9b000c2af 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 4cc76d86f3..c42938c8ec 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index eb43d69fe0..515fa52dfa 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 1386c2ad5f..3149e70298 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index a0930f15f4..7c607f7ae6 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index ce8025bfba..6af591eed3 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 3d59669a9c..9a1a4aa01b 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -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        *)
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 79d6749557..4d33174b35 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -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        *)
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index f2a965c902..44b81d762c 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.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        *)
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 8cf3b8194c..bb9e8e5f5b 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.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        *)
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index a8ab4fd3c8..2f5601964e 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -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        *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 657a91c0c1..41a068ff38 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.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        *)
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index e5fe76f58a..90f4f911b7 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -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        *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 2dc2420c46..10644da25d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.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        *)
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 6bd2541b24..cdda777a6c 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -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        *)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 3fe5a8c04e..aec9586895 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -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        *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index da7a4265e6..22519e3471 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.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        *)
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 99559bcedc..6f49320671 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -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        *)
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 681dceaa04..db33615228 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -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        *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 62724f2119..402fe4ffe6 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        *)
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index c07cee7136..c667552490 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -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        *)
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index c3dc286cd1..b5e8b48044 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.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        *)
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index ca32f02921..dc8708249a 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -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        *)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 8c86c77112..3cb3810cbc 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.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        *)
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 4e796792e3..f579a54b8b 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -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        *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 0b2a04d3f1..7b0f14dff7 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.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        *)
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index f0e36e09d9..5e1ec0d5e0 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -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        *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 9feaea8cdb..d7842e127d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.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        *)
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 4e638a0ace..2b163610e9 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -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        *)
-- 
cgit v1.2.3


From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 29 Jan 2016 10:13:12 +0100
Subject: CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.
---
 plugins/extraction/extraction.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 38aef62e1e..6c57bc2bbd 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -25,6 +25,7 @@ open Globnames
 open Miniml
 open Table
 open Mlutil
+open Context.Rel.Declaration
 (*i*)
 
 exception I of inductive_kind
@@ -74,7 +75,7 @@ type flag = info * scheme
 let rec flag_of_type env t : flag =
   let t = whd_betadeltaiota env none t in
   match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
+    | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
@@ -247,7 +248,7 @@ let rec extract_type env db j c args =
     | _ 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
+           | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
 	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
@@ -560,7 +561,7 @@ let rec extract_term env mle mlt c args =
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
-	let env' = push_rel (Name id, Some c1, t1) env in
+	let env' = push_rel (LocalDef (Name id, c1, t1)) env in
 	(* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
@@ -835,7 +836,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 
 let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in
+  let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
-- 
cgit v1.2.3


From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Mar 2016 16:57:05 +0100
Subject: Removing the special status of generic entries defined by Coq itself.

The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.

After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
---
 plugins/extraction/g_extraction.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec9586895..7bd07f6255 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -11,6 +11,10 @@
 (* ML names *)
 
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Pp
 open Names
 open Nameops
-- 
cgit v1.2.3


From fa9c33e37ca609981aca88d6f92b07882bd2f4f4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Apr 2016 16:05:15 +0200
Subject: Removing redundant *_TYPED AS clauses in EXTEND statements.

---
 plugins/extraction/g_extraction.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 7bd07f6255..ca4e13e125 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -35,7 +35,6 @@ let pr_int_or_id _ _ _ = function
   | ArgId id -> pr_id id
 
 ARGUMENT EXTEND int_or_id
-  TYPED AS int_or_id
   PRINTED BY pr_int_or_id
 | [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]
-- 
cgit v1.2.3