src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51767 bbcdd8519253
parent 51766 f19a4d0ab1bf
child 51768 d2a236b10796
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:47:22 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 18:49:52 2013 +0200
     1.3 @@ -8,15 +8,15 @@
     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 ->
     1.8 +    (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
     1.9        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.10        BNF_FP.fp_result * local_theory) ->
    1.11 -    (bool * bool) * ((((binding * (binding * (typ * sort)) list) * binding) * mixfix) *
    1.12 +    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    1.13        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.14          mixfix) list) list ->
    1.15      local_theory -> local_theory
    1.16    val parse_datatype_cmd: bool ->
    1.17 -    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
    1.18 +    (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    1.19        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.20        BNF_FP.fp_result * local_theory) ->
    1.21      (local_theory -> local_theory) parser
    1.22 @@ -130,9 +130,10 @@
    1.23    reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
    1.24    handle THM _ => thm;
    1.25  
    1.26 -fun map_binding_of ((((b, _), _), _), _) = b;
    1.27 -fun type_args_named_constrained_of ((((_, ncAs), _), _), _) = ncAs;
    1.28 -fun type_binding_of (((_, b), _), _) = b;
    1.29 +fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs;
    1.30 +fun type_binding_of ((((_, b), _), _), _) = b;
    1.31 +fun map_binding_of (((_, (b, _)), _), _) = b;
    1.32 +fun rel_binding_of (((_, (_, b)), _), _) = b;
    1.33  fun mixfix_of ((_, mx), _) = mx;
    1.34  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
    1.35  
    1.36 @@ -159,6 +160,7 @@
    1.37      val fp_b_names = map Binding.name_of fp_bs;
    1.38      val fp_common_name = mk_common_name fp_b_names;
    1.39      val map_bs = map map_binding_of specs;
    1.40 +    val rel_bs = map rel_binding_of specs;
    1.41  
    1.42      fun prepare_type_arg (_, (ty, c)) =
    1.43        let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
    1.44 @@ -244,7 +246,7 @@
    1.45      val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
    1.46             fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
    1.47             fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
    1.48 -      fp_bnf construct_fp fp_bs mixfixes map_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    1.49 +      fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    1.50          no_defs_lthy0;
    1.51  
    1.52      val timer = time (Timer.startRealTimer ());
    1.53 @@ -1196,13 +1198,31 @@
    1.54    @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
    1.55    Scan.succeed [];
    1.56  
    1.57 -val parse_single_spec =
    1.58 -  parse_opt_binding_colon -- parse_type_args_named_constrained -- Parse.binding --
    1.59 -  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon --
    1.60 -      Parse.binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] --
    1.61 -    Parse.opt_mixfix));
    1.62 +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
    1.63 +
    1.64 +val no_map_rel = (Binding.empty, Binding.empty);
    1.65 +
    1.66 +(* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
    1.67 +   that we don't want them to be highlighted everywhere because of some obscure feature of the BNF
    1.68 +   package. *)
    1.69 +fun extract_map_rel ("map", b) = apfst (K b)
    1.70 +  | extract_map_rel ("rel", b) = apsnd (K b)
    1.71 +  | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);
    1.72  
    1.73 -val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
    1.74 +val parse_map_rel_bindings =
    1.75 +  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
    1.76 +    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
    1.77 +  Scan.succeed no_map_rel;
    1.78 +
    1.79 +val parse_ctr_spec =
    1.80 +  parse_opt_binding_colon -- Parse.binding -- Scan.repeat parse_ctr_arg --
    1.81 +  Scan.optional parse_defaults [] -- Parse.opt_mixfix;
    1.82 +
    1.83 +val parse_spec =
    1.84 +  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
    1.85 +  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
    1.86 +
    1.87 +val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
    1.88  
    1.89  fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
    1.90