--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 19 13:38:21 2014 +0200
@@ -151,10 +151,10 @@
fun propagate_units css =
(case List.partition (can the_single) css of
- ([], _) => css
- | ([u] :: uss, css') =>
- [u] :: propagate_units (map (propagate_unit_neg (s_not u))
- (map (propagate_unit_pos u) (uss @ css'))));
+ ([], _) => css
+ | ([u] :: uss, css') =>
+ [u] :: propagate_units (map (propagate_unit_neg (s_not u))
+ (map (propagate_unit_pos u) (uss @ css'))));
fun s_conjs cs =
if member (op aconv) cs @{const False} then @{const False}
@@ -526,33 +526,31 @@
end;
in abs 0 end;
-type coeqn_data_disc = {
- fun_name: string,
- fun_T: typ,
- fun_args: term list,
- ctr: term,
- ctr_no: int,
- disc: term,
- prems: term list,
- auto_gen: bool,
- ctr_rhs_opt: term option,
- code_rhs_opt: term option,
- eqn_pos: int,
- user_eqn: term
-};
+type coeqn_data_disc =
+ {fun_name: string,
+ fun_T: typ,
+ fun_args: term list,
+ ctr: term,
+ ctr_no: int,
+ disc: term,
+ prems: term list,
+ auto_gen: bool,
+ ctr_rhs_opt: term option,
+ code_rhs_opt: term option,
+ eqn_pos: int,
+ user_eqn: term};
-type coeqn_data_sel = {
- fun_name: string,
- fun_T: typ,
- fun_args: term list,
- ctr: term,
- sel: term,
- rhs_term: term,
- ctr_rhs_opt: term option,
- code_rhs_opt: term option,
- eqn_pos: int,
- user_eqn: term
-};
+type coeqn_data_sel =
+ {fun_name: string,
+ fun_T: typ,
+ fun_args: term list,
+ ctr: term,
+ sel: term,
+ rhs_term: term,
+ ctr_rhs_opt: term option,
+ code_rhs_opt: term option,
+ eqn_pos: int,
+ user_eqn: term};
datatype coeqn_data =
Disc of coeqn_data_disc |
@@ -585,17 +583,13 @@
handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl;
val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
- val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in
- null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds
- end;
+ val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args;
+ val _ = null fixeds orelse
+ primcorec_error_eqns "function argument(s) are fixed in context" fixeds;
- val _ =
- let
- val bad = prems'
- |> filter (exists_subterm (fn Free (v, _) => member (op =) fun_names v | _ => false))
- in
- null bad orelse primcorec_error_eqns "corecursive call(s) in condition(s)" bad
- end;
+ val bad =
+ filter (exists_subterm (fn Free (v, _) => member (op =) fun_names v | _ => false)) prems';
+ val _ = null bad orelse primcorec_error_eqns "corecursive call(s) in condition(s)" bad;
val _ = forall is_Free fun_args orelse
primcorec_error_eqn ("non-variable function argument \"" ^
@@ -606,8 +600,8 @@
primcorec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ "\"")
applied_fun end;
- val SOME (sequential, basic_ctr_specs) =
- AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name;
+ val (sequential, basic_ctr_specs) =
+ the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name);
val discs = map #disc basic_ctr_specs;
val ctrs = map #ctr basic_ctr_specs;
@@ -622,7 +616,6 @@
val _ = if is_some disc' andalso perhaps (try HOLogic.dest_not) concl <> the disc'
then primcorec_error_eqn "malformed discriminator formula" concl else ();
-
val _ = is_some disc' orelse is_some eq_ctr0 orelse
primcorec_error_eqn "no discriminator in equation" concl;
val ctr_no' =
@@ -647,20 +640,10 @@
val _ = check_extra_variables lthy fun_args fun_names user_eqn;
in
- (Disc {
- fun_name = fun_name,
- fun_T = fun_T,
- fun_args = fun_args,
- ctr = ctr,
- ctr_no = ctr_no,
- disc = disc,
- prems = actual_prems,
- auto_gen = catch_all,
- ctr_rhs_opt = ctr_rhs_opt,
- code_rhs_opt = code_rhs_opt,
- eqn_pos = eqn_pos,
- user_eqn = user_eqn
- }, matchedsss')
+ (Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
+ disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt,
+ code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn},
+ matchedsss')
end;
fun dissect_coeqn_sel lthy fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos
@@ -690,18 +673,9 @@
val _ = check_extra_variables lthy fun_args fun_names user_eqn;
in
- Sel {
- fun_name = fun_name,
- fun_T = fun_T,
- fun_args = fun_args,
- ctr = ctr,
- sel = sel,
- rhs_term = rhs,
- ctr_rhs_opt = ctr_rhs_opt,
- code_rhs_opt = code_rhs_opt,
- eqn_pos = eqn_pos,
- user_eqn = user_eqn
- }
+ Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel,
+ rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos,
+ user_eqn = user_eqn}
end;
fun dissect_coeqn_ctr lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
@@ -712,7 +686,7 @@
val _ = check_extra_variables lthy fun_args fun_names (drop_all eqn0);
- val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
+ val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
@@ -744,7 +718,7 @@
val _ = check_extra_variables lthy fun_args fun_names concl;
- val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
+ val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ =>
if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs)
@@ -753,11 +727,11 @@
val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs);
val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
- binder_types (fastype_of ctr)
- |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
- if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
- |> curry Term.list_comb ctr
- |> curry HOLogic.mk_eq lhs);
+ binder_types (fastype_of ctr)
+ |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
+ if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
+ |> curry Term.list_comb ctr
+ |> curry HOLogic.mk_eq lhs);
val sequentials = replicate (length fun_names) false;
in
@@ -786,15 +760,14 @@
val ctrs = maps (map #ctr) basic_ctr_specss;
in
if member (op =) discs head orelse
- is_some rhs_opt andalso
- member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso
- member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
+ (is_some rhs_opt andalso
+ member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso
+ member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then
dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
matchedsss
|>> single
else if member (op =) sels head then
- (null prems orelse
- primcorec_error_eqn "premise(s) in selector formula" eqn;
+ (null prems orelse primcorec_error_eqn "premise(s) in selector formula" eqn;
([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt
concl], matchedsss))
else if is_some rhs_opt andalso
@@ -948,22 +921,21 @@
val n = 0 upto length ctr_specs
|> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns));
val {ctr, disc, ...} = nth ctr_specs n;
+ val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
+
+ val fun_name = Binding.name_of fun_binding;
+ val fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs)));
val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
|> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
- val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
- val extra_disc_eqn = {
- fun_name = Binding.name_of fun_binding,
- fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
- fun_args = fun_args,
- ctr = ctr,
- ctr_no = n,
- disc = disc,
- prems = maps (s_not_conj o #prems) disc_eqns,
- auto_gen = true,
- ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
- code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE,
- eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *),
- user_eqn = undef_const};
+ val prems = maps (s_not_conj o #prems) disc_eqns;
+ val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE;
+ val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE;
+ val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *);
+
+ val extra_disc_eqn =
+ {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = n,
+ disc = disc, prems = prems, auto_gen = true, ctr_rhs_opt = ctr_rhs_opt,
+ code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = undef_const};
in
chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
end
@@ -1195,7 +1167,7 @@
({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...}
: coeqn_data_sel) =
let
- val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs;
+ val ctr_spec = the (find_first (curry (op =) ctr o #ctr) ctr_specs);
val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
(find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems);