1 (* Title: HOL/Tools/Nitpick/nitpick_nut.ML |
1 (* Title: HOL/Tools/Nitpick/nitpick_nut.ML |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2008, 2009 |
3 Copyright 2008, 2009, 2010 |
4 |
4 |
5 Nitpick underlying terms (nuts). |
5 Nitpick underlying terms (nuts). |
6 *) |
6 *) |
7 |
7 |
8 signature NITPICK_NUT = |
8 signature NITPICK_NUT = |
764 fun choose_rep_for_sels_for_constr scope (x as (_, T)) = |
764 fun choose_rep_for_sels_for_constr scope (x as (_, T)) = |
765 fold_rev (choose_rep_for_nth_sel_for_constr scope x) |
765 fold_rev (choose_rep_for_nth_sel_for_constr scope x) |
766 (~1 upto num_sels_for_constr_type T - 1) |
766 (~1 upto num_sels_for_constr_type T - 1) |
767 (* scope -> dtype_spec -> nut list * rep NameTable.table |
767 (* scope -> dtype_spec -> nut list * rep NameTable.table |
768 -> nut list * rep NameTable.table *) |
768 -> nut list * rep NameTable.table *) |
769 fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I |
769 fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I |
770 | choose_rep_for_sels_of_datatype scope {constrs, ...} = |
770 | choose_rep_for_sels_of_datatype scope {constrs, ...} = |
771 fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs |
771 fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs |
772 (* scope -> rep NameTable.table -> nut list * rep NameTable.table *) |
772 (* scope -> rep NameTable.table -> nut list * rep NameTable.table *) |
773 fun choose_reps_for_all_sels (scope as {datatypes, ...}) = |
773 fun choose_reps_for_all_sels (scope as {datatypes, ...}) = |
774 fold (choose_rep_for_sels_of_datatype scope) datatypes o pair [] |
774 fold (choose_rep_for_sels_of_datatype scope) datatypes o pair [] |