src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51758 55963309557b
parent 51757 7babcb61aa5c
child 51766 f19a4d0ab1bf
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:20 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:21 2013 +0200
     1.3 @@ -8,15 +8,16 @@
     1.4  signature BNF_FP_DEF_SUGAR =
     1.5  sig
     1.6    val datatypes: bool ->
     1.7 -    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
     1.8 -      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     1.9 +    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
    1.10 +      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.11        BNF_FP.fp_result * local_theory) ->
    1.12 -    (bool * bool) * (((((binding * typ) * sort) list * binding) * mixfix) * ((((binding * binding) *
    1.13 -      (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    1.14 +    (bool * bool) * ((((binding * (binding * (typ * sort)) list) * binding) * mixfix) *
    1.15 +      ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.16 +        mixfix) list) list ->
    1.17      local_theory -> local_theory
    1.18    val parse_datatype_cmd: bool ->
    1.19 -    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
    1.20 -      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.21 +    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
    1.22 +      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.23        BNF_FP.fp_result * local_theory) ->
    1.24      (local_theory -> local_theory) parser
    1.25  end;
    1.26 @@ -129,7 +130,8 @@
    1.27    reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
    1.28    handle THM _ => thm;
    1.29  
    1.30 -fun type_args_constrained_of (((cAs, _), _), _) = cAs;
    1.31 +fun map_binding_of ((((b, _), _), _), _) = b;
    1.32 +fun type_args_named_constrained_of ((((_, ncAs), _), _), _) = ncAs;
    1.33  fun type_binding_of (((_, b), _), _) = b;
    1.34  fun mixfix_of ((_, mx), _) = mx;
    1.35  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
    1.36 @@ -156,16 +158,17 @@
    1.37      val fp_bs = map type_binding_of specs;
    1.38      val fp_b_names = map Binding.name_of fp_bs;
    1.39      val fp_common_name = mk_common_name fp_b_names;
    1.40 +    val map_bs = map map_binding_of specs;
    1.41  
    1.42 -    fun prepare_type_arg ((_, ty), c) =
    1.43 +    fun prepare_type_arg (_, (ty, c)) =
    1.44        let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
    1.45          TFree (s, prepare_constraint no_defs_lthy0 c)
    1.46        end;
    1.47  
    1.48 -    val Ass0 = map (map prepare_type_arg o type_args_constrained_of) specs;
    1.49 +    val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
    1.50      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    1.51      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    1.52 -    val set_bss = map (map (fst o fst) o type_args_constrained_of) specs;
    1.53 +    val set_bss = map (map fst o type_args_named_constrained_of) specs;
    1.54  
    1.55      val (((Bs0, Cs), Xs), no_defs_lthy) =
    1.56        no_defs_lthy0
    1.57 @@ -180,7 +183,8 @@
    1.58        locale and shadows an existing global type*)
    1.59      val fake_thy =
    1.60        Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy
    1.61 -        (type_binding_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
    1.62 +          (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec))))
    1.63 +        specs;
    1.64      val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
    1.65  
    1.66      fun mk_fake_T b =
    1.67 @@ -240,7 +244,8 @@
    1.68      val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
    1.69             fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
    1.70             fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
    1.71 -      fp_bnf construct_fp fp_bs mixfixes set_bss (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    1.72 +      fp_bnf construct_fp fp_bs mixfixes map_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    1.73 +        no_defs_lthy0;
    1.74  
    1.75      val timer = time (Timer.startRealTimer ());
    1.76  
    1.77 @@ -1181,21 +1186,21 @@
    1.78  val parse_defaults =
    1.79    @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
    1.80  
    1.81 -(* Identical to unexported function of the same name in "Pure/Isar/parse.ML" *)
    1.82 -fun parse_type_arguments arg =
    1.83 -  arg >> single || @{keyword "("} |-- Parse.!!! (Parse.list1 arg --| @{keyword ")"}) ||
    1.84 +val parse_type_arg_constrained =
    1.85 +  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
    1.86 +
    1.87 +val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained
    1.88 +
    1.89 +val parse_type_args_named_constrained =
    1.90 +  parse_type_arg_constrained >> (single o pair Binding.empty) ||
    1.91 +  @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
    1.92    Scan.succeed [];
    1.93  
    1.94 -val parse_type_arg_constrained =
    1.95 -  parse_opt_binding_colon -- Parse.type_ident --
    1.96 -  Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
    1.97 -
    1.98 -val parse_type_args_constrained = parse_type_arguments parse_type_arg_constrained;
    1.99 -
   1.100  val parse_single_spec =
   1.101 -  parse_type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
   1.102 -  (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
   1.103 -    Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix));
   1.104 +  parse_opt_binding_colon -- parse_type_args_named_constrained -- Parse.binding --
   1.105 +  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon --
   1.106 +      Parse.binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] --
   1.107 +    Parse.opt_mixfix));
   1.108  
   1.109  val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
   1.110