src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55469 b19dd108f0c2
parent 55468 98b25c51e9e5
child 55470 46e6e1d91056
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -53,12 +53,19 @@
     1.4    val dest_case: Proof.context -> string -> typ list -> term ->
     1.5      (ctr_sugar * term list * term list) option
     1.6  
     1.7 +  type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list
     1.8 +
     1.9 +  val disc_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> binding
    1.10 +  val ctr_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'c
    1.11 +  val args_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'a list
    1.12 +  val sel_defaults_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> (binding * 'v) list
    1.13 +
    1.14    val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    1.15 -    (((bool * bool) * term list) * binding) *
    1.16 -      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    1.17 +    ((bool * bool) * binding) * (term, binding, term) ctr_spec list -> local_theory ->
    1.18      ctr_sugar * local_theory
    1.19 -  val parse_free_constructors_options: (bool * bool) parser
    1.20    val parse_bound_term: (binding * string) parser
    1.21 +  val parse_ctr_options: (bool * bool) parser
    1.22 +  val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a, string) ctr_spec parser
    1.23  end;
    1.24  
    1.25  structure Ctr_Sugar : CTR_SUGAR =
    1.26 @@ -278,11 +285,23 @@
    1.27  
    1.28  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    1.29  
    1.30 -fun prepare_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding),
    1.31 -    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    1.32 +type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list;
    1.33 +
    1.34 +fun disc_of_ctr_spec (((disc, _), _), _) = disc;
    1.35 +fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr;
    1.36 +fun args_of_ctr_spec ((_, args), _) = args;
    1.37 +fun sel_defaults_of_ctr_spec (_, ds) = ds;
    1.38 +
    1.39 +fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs)
    1.40 +    no_defs_lthy =
    1.41    let
    1.42      (* TODO: sanity checks on arguments *)
    1.43  
    1.44 +    val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
    1.45 +    val raw_disc_bindings = map disc_of_ctr_spec ctr_specs;
    1.46 +    val raw_sel_bindingss = map args_of_ctr_spec ctr_specs;
    1.47 +    val raw_sel_defaultss = map sel_defaults_of_ctr_spec ctr_specs;
    1.48 +
    1.49      val n = length raw_ctrs;
    1.50      val ks = 1 upto n;
    1.51  
    1.52 @@ -954,29 +973,28 @@
    1.53    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    1.54    prepare_free_constructors Syntax.read_term;
    1.55  
    1.56 -fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    1.57 -
    1.58 -val parse_bindings = parse_bracket_list parse_binding;
    1.59 -val parse_bindingss = parse_bracket_list parse_bindings;
    1.60 +val parse_bound_term = parse_binding --| @{keyword ":"} -- Parse.term;
    1.61  
    1.62 -val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
    1.63 -val parse_bound_terms = parse_bracket_list parse_bound_term;
    1.64 -val parse_bound_termss = parse_bracket_list parse_bound_terms;
    1.65 -
    1.66 -val parse_free_constructors_options =
    1.67 +val parse_ctr_options =
    1.68    Scan.optional (@{keyword "("} |-- Parse.list1
    1.69          (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    1.70        @{keyword ")"}
    1.71        >> (fn js => (member (op =) js 0, member (op =) js 1)))
    1.72      (false, false);
    1.73  
    1.74 +val parse_defaults =
    1.75 +  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
    1.76 +
    1.77 +fun parse_ctr_spec parse_ctr parse_arg =
    1.78 +  parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg --
    1.79 +  Scan.optional parse_defaults [];
    1.80 +
    1.81 +val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term parse_binding);
    1.82 +
    1.83  val _ =
    1.84    Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    1.85      "register an existing freely generated type's constructors"
    1.86 -    ((parse_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
    1.87 -        @{keyword "]"}) --
    1.88 -      parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    1.89 -        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
    1.90 +    (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
    1.91       >> free_constructors_cmd);
    1.92  
    1.93  end;