# HG changeset patch # User haftmann # Date 1648139681 0 # Node ID a82f7f8a3c7bf5e7253eb365494053c0a8297074 # Parent b7a74a04ae4e2d41c9aefc3b942dfa4ea28a97f2 self-contained extraction auf clauses diff -r b7a74a04ae4e -r a82f7f8a3c7b src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Mar 24 16:34:40 2022 +0000 +++ b/src/Tools/Code/code_thingol.ML Thu Mar 24 16:34:41 2022 +0000 @@ -678,18 +678,21 @@ val thy = Proof_Context.theory_of ctxt; val ty = nth (binder_types (snd c_ty)) t_pos; val is_let = null case_pats; - fun mk_constr NONE _ = NONE - | mk_constr (SOME c) t = - let - val n = Code.args_number thy c; - in SOME ((c, (take n o binder_types o fastype_of o untag_term) t ---> ty), n) end; + fun select_clauses xs = + xs + |> nth_drop t_pos + |> curry (op ~~) case_pats + |> map_filter (fn (NONE, _) => NONE | (SOME _, x) => SOME x); + fun mk_constr c t = + let + val n = Code.args_number thy c; + in ((c, (take n o binder_types o fastype_of o untag_term) t ---> ty), n) end; val constrs = if is_let then [] - else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts)); + else map2 mk_constr (case_pats |> map_filter I) (select_clauses ts); val split_clauses = if is_let then (fn ts => (nth ts t_pos, nth_drop t_pos ts)) - else (fn ts => (nth ts t_pos, ts |> nth_drop t_pos |> curry (op ~~) case_pats - |> map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t))); + else (fn ts => (nth ts t_pos, select_clauses ts)); fun disjunctive_varnames ts = let val vs = (fold o fold_varnames) (insert (op =)) ts [];