# HG changeset patch # User blanchet # Date 1388754856 -3600 # Node ID 28b621fce2f9d15feefa8139191305b45b44a082 # Parent c63223067cab92509a375141e8047de02195bfa6 more SML-ish (less Haskell-ish) naming convention diff -r c63223067cab -r 28b621fce2f9 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 03 14:04:37 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 03 14:14:16 2014 +0100 @@ -478,8 +478,8 @@ disc: term, prems: term list, auto_gen: bool, - maybe_ctr_rhs: term option, - maybe_code_rhs: term option, + ctr_rhs_opt: term option, + code_rhs_opt: term option, user_eqn: term }; @@ -490,8 +490,8 @@ ctr: term, sel: term, rhs_term: term, - maybe_ctr_rhs: term option, - maybe_code_rhs: term option, + ctr_rhs_opt: term option, + code_rhs_opt: term option, user_eqn: term }; @@ -500,7 +500,7 @@ Sel of coeqn_data_sel; fun dissect_coeqn_disc fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) - maybe_ctr_rhs maybe_code_rhs prems' concl matchedsss = + ctr_rhs_opt code_rhs_opt prems' concl matchedsss = let fun find_subterm p = let (* FIXME \? *) @@ -556,14 +556,14 @@ disc = disc, prems = actual_prems, auto_gen = catch_all, - maybe_ctr_rhs = maybe_ctr_rhs, - maybe_code_rhs = maybe_code_rhs, + ctr_rhs_opt = ctr_rhs_opt, + code_rhs_opt = code_rhs_opt, user_eqn = user_eqn }, matchedsss') end; -fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) maybe_ctr_rhs - maybe_code_rhs eqn' maybe_of_spec eqn = +fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) ctr_rhs_opt + code_rhs_opt eqn' of_spec_opt eqn = let val (lhs, rhs) = HOLogic.dest_eq eqn handle TERM _ => @@ -576,7 +576,7 @@ handle Option.Option => primcorec_error_eqn "malformed selector argument in left-hand side" eqn; val {ctr, ...} = - (case maybe_of_spec of + (case of_spec_opt of SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs) | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn); @@ -589,14 +589,14 @@ ctr = ctr, sel = sel, rhs_term = rhs, - maybe_ctr_rhs = maybe_ctr_rhs, - maybe_code_rhs = maybe_code_rhs, + ctr_rhs_opt = ctr_rhs_opt, + code_rhs_opt = code_rhs_opt, user_eqn = user_eqn } end; fun dissect_coeqn_ctr fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list) eqn' - maybe_code_rhs prems concl matchedsss = + code_rhs_opt prems concl matchedsss = let val (lhs, rhs) = HOLogic.dest_eq concl; val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; @@ -606,17 +606,17 @@ handle Option.Option => primcorec_error_eqn "not a constructor" ctr; val disc_concl = betapply (disc, lhs); - val (maybe_eqn_data_disc, matchedsss') = if length basic_ctr_specs = 1 + val (eqn_data_disc_opt, matchedsss') = if length basic_ctr_specs = 1 then (NONE, matchedsss) else apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss - (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss); + (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss); val sel_concls = sels ~~ ctr_args |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)); (* val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} concl ^ "\nto\n \ " ^ - (is_some maybe_eqn_data_disc ? K (Syntax.string_of_term @{context} disc_concl ^ "\n \ ")) "" ^ + (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n \ ")) "" ^ space_implode "\n \ " (map (Syntax.string_of_term @{context}) sel_concls) ^ "\nfor premise(s)\n \ " ^ space_implode "\n \ " (map (Syntax.string_of_term @{context}) prems)); @@ -624,9 +624,9 @@ val eqns_data_sel = map (dissect_coeqn_sel fun_names basic_ctr_specss - (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs eqn' (SOME ctr)) sel_concls; + (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn' (SOME ctr)) sel_concls; in - (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss') + (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss') end; fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn' concl matchedsss = @@ -657,7 +657,7 @@ end; fun dissect_coeqn lthy has_call fun_names sequentials - (basic_ctr_specss : basic_corec_ctr_spec list list) eqn' maybe_of_spec matchedsss = + (basic_ctr_specss : basic_corec_ctr_spec list list) eqn' of_spec_opt matchedsss = let val eqn = drop_All eqn' handle TERM _ => primcorec_error_eqn "malformed function equation" eqn'; @@ -668,22 +668,22 @@ |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) |> head_of; - val maybe_rhs = concl |> perhaps (try HOLogic.dest_not) |> try (snd o HOLogic.dest_eq); + val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (snd o HOLogic.dest_eq); val discs = maps (map #disc) basic_ctr_specss; val sels = maps (maps #sels) basic_ctr_specss; val ctrs = maps (map #ctr) basic_ctr_specss; in if member (op =) discs head orelse - is_some maybe_rhs andalso - member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then + is_some rhs_opt andalso + member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then dissect_coeqn_disc fun_names sequentials basic_ctr_specss NONE NONE prems concl matchedsss |>> single else if member (op =) sels head then - ([dissect_coeqn_sel fun_names basic_ctr_specss NONE NONE eqn' maybe_of_spec concl], + ([dissect_coeqn_sel fun_names basic_ctr_specss NONE NONE eqn' of_spec_opt concl], matchedsss) else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso - member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then + member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn' NONE prems concl matchedsss else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso null prems then @@ -821,7 +821,7 @@ |> the o find_first (fn idx => not (exists (curry (op =) idx o #ctr_no) disc_eqns)); 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 maybe_sel_eqn = + val sel_eqn_opt = find_first (curry (op =) (Binding.name_of fun_binding) o #fun_name) sel_eqns; val extra_disc_eqn = { fun_name = Binding.name_of fun_binding, @@ -832,8 +832,8 @@ disc = #disc (nth ctr_specs n), prems = maps (s_not_conj o #prems) disc_eqns, auto_gen = true, - maybe_ctr_rhs = Option.map #maybe_ctr_rhs maybe_sel_eqn |> the_default NONE, - maybe_code_rhs = Option.map #maybe_ctr_rhs maybe_sel_eqn |> the_default NONE, + ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE, + code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE, user_eqn = undef_const}; in chop n disc_eqns ||> cons extra_disc_eqn |> (op @) @@ -857,7 +857,7 @@ op aconv (Logic.dest_implies (Thm.prop_of thm)) handle TERM _ => false; -fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy = +fun add_primcorec_ursive tac_opt opts fixes specs of_specs_opt lthy = let val thy = Proof_Context.theory_of lthy; @@ -878,7 +878,7 @@ val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); val eqns_data = fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (map snd specs) - maybe_of_specs [] + of_specs_opt [] |> flat o fst; val callssss = @@ -924,7 +924,7 @@ if a orelse c = c' orelse sequential then SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy []))) else - maybe_tac; + tac_opt; (* val _ = tracing ("exclusiveness properties:\n \ " ^ @@ -946,7 +946,7 @@ disc_eqnss; val syntactic_exhaustives = - map (fn disc_eqns => forall (null o #prems orf is_some o #maybe_code_rhs) disc_eqns + map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns orelse exists #auto_gen disc_eqns) disc_eqnss; val de_facto_exhaustives = @@ -965,7 +965,7 @@ mk_primcorec_nchotomy_tac ctxt disc_exhausts)) corec_specs syntactic_exhaustives nchotomy_goalss; val goalss = goalss' - |> (if is_none maybe_tac then + |> (if is_none tac_opt then append (map2 (fn true => K [] | false => map (rpair [])) syntactic_exhaustives nchotomy_goalss) else @@ -976,8 +976,8 @@ val def_thms = map (snd o snd) def_thms'; val nchotomy_thmss = nchotomy_taut_thmss - |> (if is_none maybe_tac then map2 append (take actual_nn thmss'') else I); - val exclude_thmss = thmss'' |> is_none maybe_tac ? drop actual_nn; + |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I); + val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn; val exhaust_thmss = map2 (fn false => K [] @@ -1072,30 +1072,30 @@ |> exists (null o snd) then [] else let - val (fun_name, fun_T, fun_args, prems, maybe_rhs) = + val (fun_name, fun_T, fun_args, prems, rhs_opt) = (find_first (curry (op =) ctr o #ctr) disc_eqns, find_first (curry (op =) ctr o #ctr) sel_eqns) |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x, - #maybe_ctr_rhs x)) - ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #maybe_ctr_rhs x)) + #ctr_rhs_opt x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #ctr_rhs_opt x)) |> the o merge_options; val m = length prems; val goal = - (if is_some maybe_rhs then - the maybe_rhs - else - filter (curry (op =) ctr o #ctr) sel_eqns - |> fst o finds ((op =) o apsnd #sel) sels - |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract) - |> curry list_comb ctr) + (case rhs_opt of + SOME rhs => rhs + | NONE => + filter (curry (op =) ctr o #ctr) sel_eqns + |> fst o finds ((op =) o apsnd #sel) sels + |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract) + |> curry list_comb ctr) |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems) |> curry Logic.list_all (map dest_Free fun_args); - val maybe_disc_thm = AList.lookup (op =) disc_alist disc; + val disc_thm_opt = AList.lookup (op =) disc_alist disc; val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist); in if prems = [@{term False}] then [] else - mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms + mk_primcorec_ctr_of_dtr_tac lthy m collapse disc_thm_opt sel_thms |> K |> Goal.prove lthy [] [] goal |> Thm.close_derivation |> pair ctr @@ -1104,22 +1104,22 @@ fun prove_code exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs = let - val maybe_fun_data = + val fun_data_opt = (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns, find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns) - |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) - ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x)) + |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x)) + ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x)) |> merge_options; in - (case maybe_fun_data of + (case fun_data_opt of NONE => [] - | SOME (fun_name, fun_T, fun_args, maybe_rhs) => + | SOME (fun_name, fun_T, fun_args, rhs_opt) => let val bound_Ts = List.rev (map fastype_of fun_args); val lhs = applied_fun_of fun_name fun_T fun_args; - val maybe_rhs_info = - (case maybe_rhs of + val rhs_info_opt = + (case rhs_opt of SOME rhs => let val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs; @@ -1143,27 +1143,27 @@ in SOME (prems, t) end; - val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs; + val ctr_conds_argss_opt = map prove_code_ctr ctr_specs; val exhaustive_code = exhaustive - orelse forall null (map_filter (try (fst o the)) maybe_ctr_conds_argss) - orelse forall is_some maybe_ctr_conds_argss + orelse forall null (map_filter (try (fst o the)) ctr_conds_argss_opt) + orelse forall is_some ctr_conds_argss_opt andalso exists #auto_gen disc_eqns; val rhs = (if exhaustive_code then - split_last (map_filter I maybe_ctr_conds_argss) ||> snd + split_last (map_filter I ctr_conds_argss_opt) ||> snd else Const (@{const_name Code.abort}, @{typ String.literal} --> (@{typ unit} --> body_type fun_T) --> body_type fun_T) $ HOLogic.mk_literal fun_name $ absdummy @{typ unit} (incr_boundvars 1 lhs) - |> pair (map_filter I maybe_ctr_conds_argss)) + |> pair (map_filter I ctr_conds_argss_opt)) |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u) in SOME (exhaustive_code, rhs, rhs, map snd ctr_alist) end); in - (case maybe_rhs_info of + (case rhs_info_opt of NONE => [] | SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) => let @@ -1263,13 +1263,13 @@ (goalss, after_qed, lthy') end; -fun add_primcorec_ursive_cmd maybe_tac opts (raw_fixes, raw_specs') lthy = +fun add_primcorec_ursive_cmd tac_opt opts (raw_fixes, raw_specs') lthy = let - val (raw_specs, maybe_of_specs) = + val (raw_specs, of_specs_opt) = split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy)); val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy; in - add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy + add_primcorec_ursive tac_opt opts fixes specs of_specs_opt lthy handle ERROR str => primcorec_error str end handle Primcorec_Error (str, eqns) => diff -r c63223067cab -r 28b621fce2f9 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 03 14:04:37 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 03 14:14:16 2014 +0100 @@ -130,9 +130,9 @@ (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents))))); -fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_fun sel_funs = +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_fun_opt sel_funs = HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' - (the_default (K all_tac) (Option.map rtac maybe_disc_fun)) THEN' REPEAT_DETERM_N m o atac) THEN + (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl); fun inst_split_eq ctxt split = @@ -168,11 +168,11 @@ fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'}); fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs - maybe_nchotomy = + nchotomy_opt = let val n = length ms; val (ms', fun_ctrs') = - (case maybe_nchotomy of + (case nchotomy_opt of NONE => (ms, fun_ctrs) | SOME nchotomy => (ms |> split_last ||> K [n - 1] |> op @, diff -r c63223067cab -r 28b621fce2f9 src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML Fri Jan 03 14:04:37 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML Fri Jan 03 14:14:16 2014 +0100 @@ -289,9 +289,9 @@ let val pT = HOLogic.mk_prodT (rec_type, res_type); - val maybe_suc = Option.map (fn x => x + 1); fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT) - | subst d (Abs (v, T, b)) = Abs (v, if d = SOME ~1 then pT else T, subst (maybe_suc d) b) + | subst d (Abs (v, T, b)) = + Abs (v, if d = SOME ~1 then pT else T, subst (Option.map (Integer.add 1) d) b) | subst d t = let val (u, vs) = strip_comb t; @@ -355,8 +355,8 @@ end; fun build_rec_arg lthy (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec) - (maybe_eqn_data : eqn_data option) = - (case maybe_eqn_data of + (eqn_data_opt : eqn_data option) = + (case eqn_data_opt of NONE => undef_const | SOME {ctr_args, left_args, right_args, rhs_term = t, ...} => let