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

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

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

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

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

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