1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 16:08:27 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 16:08:55 2012 +0200
1.3 @@ -480,7 +480,7 @@
1.4 corec_def), lthy)
1.5 end;
1.6 in
1.7 - wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, sel_binderss)) lthy'
1.8 + wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss, []))) lthy'
1.9 |> (if lfp then some_lfp_sugar else some_gfp_sugar)
1.10 end;
1.11
2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 16:08:27 2012 +0200
2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 16:08:55 2012 +0200
2.3 @@ -11,7 +11,8 @@
2.4 val mk_half_pairss: 'a list -> ('a * 'a) list list
2.5 val mk_ctr: typ list -> term -> term
2.6 val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
2.7 - ((bool * term list) * term) * (binding list * binding list list) -> local_theory ->
2.8 + ((bool * term list) * term) *
2.9 + (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
2.10 (term list list * thm list * thm list list) * local_theory
2.11 val parse_wrap_options: bool parser
2.12 end;
2.13 @@ -56,8 +57,7 @@
2.14
2.15 fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
2.16
2.17 -(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *)
2.18 -fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
2.19 +fun mk_undefined T = Const (@{const_name undefined}, T);
2.20
2.21 fun mk_ctr Ts ctr =
2.22 let val Type (_, Ts0) = body_type (fastype_of ctr) in
2.23 @@ -67,27 +67,29 @@
2.24 fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
2.25
2.26 fun name_of_ctr c =
2.27 - case head_of c of
2.28 + (case head_of c of
2.29 Const (s, _) => s
2.30 | Free (s, _) => s
2.31 - | _ => error "Cannot extract name of constructor";
2.32 + | _ => error "Cannot extract name of constructor");
2.33
2.34 fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
2.35 - (raw_disc_binders, raw_sel_binderss)) no_defs_lthy =
2.36 + (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy =
2.37 let
2.38 (* TODO: sanity checks on arguments *)
2.39 (* TODO: attributes (simp, case_names, etc.) *)
2.40 (* TODO: case syntax *)
2.41 (* TODO: integration with function package ("size") *)
2.42
2.43 - val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
2.44 - val case0 = prep_term no_defs_lthy raw_case;
2.45 -
2.46 - val n = length ctrs0;
2.47 + val n = length raw_ctrs;
2.48 val ks = 1 upto n;
2.49
2.50 val _ = if n > 0 then () else error "No constructors specified";
2.51
2.52 + val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
2.53 + val case0 = prep_term no_defs_lthy raw_case;
2.54 + val sel_defaultss =
2.55 + pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
2.56 +
2.57 val Type (fpT_name, As0) = body_type (fastype_of (hd ctrs0));
2.58 val b = Binding.qualified_name fpT_name;
2.59
2.60 @@ -194,11 +196,17 @@
2.61
2.62 fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k));
2.63
2.64 - fun mk_sel_case_args proto_sels T =
2.65 - map2 (fn Ts => fn i =>
2.66 - case AList.lookup (op =) proto_sels i of
2.67 - NONE => mk_undef T Ts
2.68 - | SOME (xs, x) => fold_rev Term.lambda xs x) ctr_Tss ks;
2.69 + fun mk_sel_case_args b proto_sels T =
2.70 + map2 (fn Ts => fn k =>
2.71 + (case AList.lookup (op =) proto_sels k of
2.72 + NONE =>
2.73 + let val def_T = Ts ---> T in
2.74 + (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
2.75 + NONE => mk_undefined def_T
2.76 + | SOME t => fold_rev (fn T => Term.lambda (Free (Name.uu, T))) Ts
2.77 + (Term.subst_atomic_types [(fastype_of t, T)] t))
2.78 + end
2.79 + | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
2.80
2.81 fun sel_spec b proto_sels =
2.82 let
2.83 @@ -216,7 +224,7 @@
2.84 " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
2.85 in
2.86 mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v,
2.87 - Term.list_comb (mk_case As T, mk_sel_case_args proto_sels T) $ v)
2.88 + Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
2.89 end;
2.90
2.91 val proto_selss = map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss;
2.92 @@ -537,11 +545,16 @@
2.93
2.94 fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
2.95 map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
2.96 - |> (fn thms => after_qed thms lthy)) oo
2.97 - prepare_wrap_datatype (K I) (* FIXME? (singleton o Type_Infer_Context.infer_types) *)
2.98 + |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
2.99
2.100 -val parse_bindings = @{keyword "["} |-- Parse.list Parse.binding --| @{keyword "]"};
2.101 -val parse_bindingss = @{keyword "["} |-- Parse.list parse_bindings --| @{keyword "]"};
2.102 +fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --| @{keyword "]"};
2.103 +
2.104 +val parse_bindings = parse_bracket_list Parse.binding;
2.105 +val parse_bindingss = parse_bracket_list parse_bindings;
2.106 +
2.107 +val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term;
2.108 +val parse_bound_terms = parse_bracket_list parse_bound_term;
2.109 +val parse_bound_termss = parse_bracket_list parse_bound_terms;
2.110
2.111 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
2.112 Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
2.113 @@ -553,7 +566,8 @@
2.114 val _ =
2.115 Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
2.116 ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
2.117 - Parse.term -- Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))
2.118 + Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
2.119 + Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
2.120 >> wrap_datatype_cmd);
2.121
2.122 end;