# HG changeset patch # User haftmann # Date 1423984666 -3600 # Node ID 792691e4b311bb425560a399e14710903972d4f9 # Parent d3f4ddeaacc344ca1a78d773cc7cc80660da4b0a tuned diff -r d3f4ddeaacc3 -r 792691e4b311 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sun Feb 15 08:17:44 2015 +0100 +++ b/src/Tools/Code/code_thingol.ML Sun Feb 15 08:17:46 2015 +0100 @@ -672,41 +672,41 @@ val constrs = if null case_pats then [] else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts)); + fun disjunctive_varnames ts = + let + val vs = (fold o fold_varnames) (insert (op =)) ts []; + in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end; + fun purge_unused_vars_in t = + let + val vs = fold_varnames (insert (op =)) t []; + in + map_terms_bottom_up (fn IVar (SOME v) => + IVar (if member (op =) vs v then SOME v else NONE) | t => t) + end; + fun collapse_clause vs_map ts body = + case body + of IConst { sym = Constant c, ... } => if member (op =) undefineds c + then [] + else [(ts, body)] + | ICase { term = IVar (SOME v), clauses = clauses, ... } => + if forall (fn (pat', body') => exists_var pat' v + orelse not (exists_var body' v)) clauses + andalso forall (disjunctive_varnames ts o fst) clauses + then case AList.lookup (op =) vs_map v + of SOME i => maps (fn (pat', body') => + collapse_clause (AList.delete (op =) v vs_map) + (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses + | NONE => [(ts, body)] + else [(ts, body)] + | _ => [(ts, body)]; + fun mk_clause mk tys t = + let + val (vs, body) = unfold_abs_eta tys t; + val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs []; + val ts = map (IVar o fst) vs; + in map mk (collapse_clause vs_map ts body) end; fun casify constrs ty t_app ts = let - fun disjunctive_varnames ts = - let - val vs = (fold o fold_varnames) (insert (op =)) ts []; - in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end; - fun purge_unused_vars_in t = - let - val vs = fold_varnames (insert (op =)) t []; - in - map_terms_bottom_up (fn IVar (SOME v) => - IVar (if member (op =) vs v then SOME v else NONE) | t => t) - end; - fun collapse_clause vs_map ts body = - case body - of IConst { sym = Constant c, ... } => if member (op =) undefineds c - then [] - else [(ts, body)] - | ICase { term = IVar (SOME v), clauses = clauses, ... } => - if forall (fn (pat', body') => exists_var pat' v - orelse not (exists_var body' v)) clauses - andalso forall (disjunctive_varnames ts o fst) clauses - then case AList.lookup (op =) vs_map v - of SOME i => maps (fn (pat', body') => - collapse_clause (AList.delete (op =) v vs_map) - (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses - | NONE => [(ts, body)] - else [(ts, body)] - | _ => [(ts, body)]; - fun mk_clause mk tys t = - let - val (vs, body) = unfold_abs_eta tys t; - val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs []; - val ts = map (IVar o fst) vs; - in map mk (collapse_clause vs_map ts body) end; val t = nth ts t_pos; val ts_clause = nth_drop t_pos ts; val clauses = if null case_pats