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 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) (limited to 'plugins/extraction/mlutil.ml') 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. *) -- 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/mlutil.ml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'plugins/extraction/mlutil.ml') 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 -- 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/mlutil.ml') 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/mlutil.ml') 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